LemmaStatement: AI-adaptedProof: 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.

Exponential Lyapunov drift for the formal Langevin generator

Statement

Let $d \geq 1$ , $U \in C^{2} (R^{d})$ , and suppose $\nabla U$ is $L$ -Lipschitz with $L > 0$ . Let $x_{⋆}$ be a global minimizer with $U (x_{⋆}) = 0$ , and assume the radial condition of Radial gradient drift forces potential coercivity with parameters $ρ > 0$ , $α \in (1, 2]$ , and $M_{ρ} \geq 0$ . For $0 < s < 1$ , set $W_{s} (x) = e^{s U (x)}, L_{U} f (x) : = \sum_{i = 1}^{d} \partial_{i i} f (x) - ⟨ \nabla U (x), \nabla f (x) ⟩,$ where $L_{U}$ is only the displayed formal differential operator here. Define $K_{s} : = \max {M_{ρ}, {(\frac{2 d L}{(1 - s) ρ^{2}})}^{1 / (2 (α - 1))}}, β_{s} : = 2 s d L \exp (s L K_{s}^{2} / 2) .$ Then for every $x \in R^{d}$ , $L_{U} W_{s} (x) \leq - s d L W_{s} (x) + β_{s} 1_{{∥ x - x_{⋆} ∥ \leq K_{s}}} .$

Facts & Assumptions

Given: $U$ , $x_{⋆}$ , and the constants in the Statement.

[A1]

$U \in C^{2}$ , its gradient is $L$ -Lipschitz, $x_{⋆}$ is a global minimizer with $U (x_{⋆}) = 0$ , and the stated radial drift condition holds. The Euclidean inner product and gradient are those of The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ and The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case, the Hessian convention is The Hessian matrix and critical points of a scalar field, and the radial condition is from Radial gradient drift forces potential coercivity.

[F1]

A differentiable function at an interior local minimum has zero gradient. Fermat's theorem: an interior differentiable local extremum has zero gradient

[F2]

The chain rule computes derivatives of compositions. The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$

[F3]

$∣ ⟨ 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

[F4]

The fundamental theorem of calculus integrates a continuous derivative along a compact interval. Newton–Leibniz needs only continuity on $[a, b]$ , differentiability on $(a, b)$ , and a Riemann-integrable extension of the interior derivative

Proof

Given: The hypotheses and formal operator in the Statement.

1.1A1F1algebra

By [F1], $\nabla U (x_{⋆}) = 0$ . For each coordinate vector $e_{i}$ , the Lipschitz bound gives $∣ \frac{\partial_{i} U (x + h e_{i}) - \partial_{i} U (x)}{h} ∣ \leq L (h \neq 0) .$ Taking $h \to 0$ yields $∣ \partial_{i i} U (x) ∣ \leq L$ , so $\sum_{i} \partial_{i i} U (x) \leq d L$ .

2.1F2step 1.1algebra

Applying [F2] coordinatewise to $W_{s} = e^{s U}$ gives $\nabla W_{s} = s W_{s} \nabla U, \sum_{i} \partial_{i i} W_{s} = s W_{s} \sum_{i} \partial_{i i} U + s^{2} W_{s} ∥ \nabla U ∥^{2} .$ Substitution in the displayed definition of $L_{U}$ therefore gives $L_{U} W_{s} = s W_{s} (\sum_{i} \partial_{i i} U - (1 - s) ∥ \nabla U ∥^{2}) .$

3.1A1F3step 2.1algebra

If $r = ∥ x - x_{⋆} ∥ \geq M_{ρ}$ and $r > 0$ , radial drift and [F3] imply $∥ \nabla U (x) ∥ \geq ρ r^{α - 1}$ . Thus when $r > K_{s}$ , the formula in step 2.1 and $r > K_{s}$ give $L_{U} W_{s} (x) \leq s W_{s} (x) (d L - (1 - s) ρ^{2} r^{2 (α - 1)}) \leq - s d L W_{s} (x) .$ The same conclusion holds for $r \geq K_{s}$ by the definition of $K_{s}$ .

3.2A1F1F2F4step 1.1step 2.1

For $h = x - x_{⋆}$ and $0 \leq t \leq 1$ , Lipschitz continuity and [F1] give $∥ \nabla U (x_{⋆} + t h) ∥ \leq L t r$ . The chain rule and [F4] therefore yield $U (x) - U (x_{⋆}) \leq L r^{2} / 2$ . Since $U (x_{⋆}) = 0$ , on $r \leq K_{s}$ we have $W_{s} (x) \leq e^{s L K_{s}^{2} / 2}$ . Also $\sum_{i} \partial_{i i} U \leq d L$ by step 1.1, so step 2.1 implies $L_{U} W_{s} + s d L W_{s} \leq 2 s d L e^{s L K_{s}^{2} / 2} = β_{s}$ .

4.1step 3.1step 3.2∎

On $r > K_{s}$ use step 3.1, and on $r \leq K_{s}$ use step 3.2. These two regions cover $R^{d}$ and give the displayed drift inequality.

Depends on

Used by

Radial drift gives weighted geometric contraction of Langevin diffusion Theorem

Dependency tree · two levels

38 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, Proposition 7 and proof §4.3 (standard reference, not scraped)