LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6-luna)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Radial gradient drift forces potential coercivity

Statement

Let $d \geq 1$ , $U \in C^{2} (R^{d})$ , and suppose $\nabla U$ is $L$ -Lipschitz for some $L > 0$ . Let $x_{⋆}$ be a global minimizer, normalize $U (x_{⋆}) = 0$ , and assume that for some $ρ > 0$ , $α \in (1, 2]$ , and $M_{ρ} \geq 0$ , $⟨ \nabla U (x), x - x_{⋆} ⟩ \geq ρ ∥ x - x_{⋆} ∥^{α} whenever ∥ x - x_{⋆} ∥ \geq M_{ρ} .$ Then every $x \in R^{d}$ satisfies $U (x) \geq \frac{ρ}{α + 1} ∥ x - x_{⋆} ∥^{α} - a_{α}, a_{α} : = \frac{ρ M_{ρ}^{α}}{α + 1} + \frac{L M_{ρ}^{2}}{2} .$

Facts & Assumptions

Given: The hypotheses in the Statement; $\nabla U$ is the Euclidean coordinate gradient and $⟨ \cdot, \cdot ⟩$ and $∥ \cdot ∥$ are the Euclidean inner product and norm.

[A1]

The differentiability, global-minimizer, Lipschitz-gradient, and radial-drift hypotheses are exactly those stated above. The gradient convention is The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case and the inner product is The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ .

[F1]

At an interior differentiable local minimum, the gradient vanishes. Fermat's theorem: an interior differentiable local extremum has zero gradient

[F2]

The derivative of a composition with a differentiable path is given by the total-derivative chain rule. The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$

[F3]

A continuous derivative integrates to the endpoint difference. Newton–Leibniz needs only continuity on $[a, b]$ , differentiability on $(a, b)$ , and a Riemann-integrable extension of the interior derivative

[F4]

$∣ ⟨ u, v ⟩ ∣ \leq ∥ u ∥ ∥ v ∥$ . Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation

Proof

Given: The potential and constants in the Statement.

1.1A1F1F2F3F4

Put $h = x - x_{⋆}$ and $r = ∥ h ∥$ . By [F1], $\nabla U (x_{⋆}) = 0$ . The path $g (t) = U (x_{⋆} + t h)$ is continuously differentiable, and [F2]–[F3] give $U (x) - U (x_{⋆}) = \int_{0}^{1} ⟨ \nabla U (x_{⋆} + t h), h ⟩ d t .$ For $0 \leq t \leq 1$ , Lipschitz continuity gives $∥ \nabla U (x_{⋆} + t h) ∥ \leq L t r$ , hence the integrand is at least $- L t r^{2}$ by [F4].

2.1A1step 1.1algebra

If $r < M_{ρ}$ , integrating the bound from step 1.1 over $[0, 1]$ yields $U (x) - U (x_{⋆}) \geq - L r^{2} / 2 \geq - L M_{ρ}^{2} / 2$ . Since $r^{α} \leq M_{ρ}^{α}$ , this is at least $ρ r^{α} / (α + 1) - a_{α}$ .

2.2A1step 1.1algebra

Suppose $r \geq M_{ρ}$ and $r > 0$ . On $0 \leq t \leq M_{ρ} / r$ , the bound in step 1.1 integrates to at least $- L M_{ρ}^{2} / 2$ . On $M_{ρ} / r \leq t \leq 1$ , the radial assumption gives $t ⟨ \nabla U (x_{⋆} + t h), h ⟩ \geq ρ t^{α} r^{α} .$ For $t \in (0, 1]$ , division by $t$ and $t^{α - 1} \geq t^{α}$ show that the path derivative is at least $ρ t^{α} r^{α}$ .

3.1step 2.2algebra

Integrating the outer-segment bound in step 2.2 and adding the inner-segment bound gives $U (x) - U (x_{⋆}) \geq - \frac{L M_{ρ}^{2}}{2} + \frac{ρ r^{α}}{α + 1} (1 - (M_{ρ} / r)^{α + 1}) .$ Because $r \geq M_{ρ}$ , $M_{ρ}^{α + 1} / r \leq M_{ρ}^{α}$ , so this is at least $ρ r^{α} / (α + 1) - a_{α}$ .

4.1step 2.1step 3.1algebra∎

If $r = 0$ , the claimed inequality reads $0 \geq - a_{α}$ and holds because $a_{α} \geq 0$ . Steps 2.1 and 3.1 cover all other $r$ , proving the bound.

Depends on

Used by

Dependency tree · two levels

34 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Alain Durmus and Éric Moulines, Non-asymptotic convergence analysis for the Unadjusted Langevin Algorithm, Lemma 6 and proof §4.2 (standard reference, not scraped)