LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generated

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.

ULA's Gaussian kernel satisfies an exponential drift bound

Statement

Assume AC. Let $d \geq 1$ , $U \in C^{2} (R^{d})$ , and suppose $\nabla U$ is $L$ -Lipschitz for $L > 0$ . Let $x_{⋆}$ be a global minimizer with $U (x_{⋆}) = 0$ . Suppose that for $ρ > 0$ , $α \in (1, 2]$ , and $M_{ρ} \geq 0$ , $⟨ \nabla U (x), x - x_{⋆} ⟩ \geq ρ ∥ x - x_{⋆} ∥^{α} if ∥ x - x_{⋆} ∥ \geq M_{ρ} .$ For $0 < γ < L^{- 1}$ , define $K_{γ} : = \max {M_{ρ}, {(\frac{2 d [- \log (1 - L γ)] / γ + 4}{ρ^{2}})}^{1 / (2 (α - 1))}}, V (x) : = e^{U (x) / 2},$ and let $P_{γ}$ be the ULA proposal kernel. Then $P_{γ} V (x) : = \int V (y) P_{γ} (x, d y) \leq e^{- γ} V (x) + e^{L K_{γ}^{2} / 4} (1 - L γ)^{- d / 2} 1_{{∥ x - x_{⋆} ∥ \leq K_{γ}}} .$

Facts & Assumptions

Given: AC; $d, L, U, x_{⋆}, ρ, α, M_{ρ}, γ$ as in the Statement; and the ULA update.

[A1]

$U$ is twice continuously differentiable, has $L$ -Lipschitz gradient, has the stated global minimizer and radial drift, and is normalized by $U (x_{⋆}) = 0$ . The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case

[F1]

At a differentiable local minimum in Euclidean space, the gradient is zero. 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, and a continuous derivative integrates to its endpoint difference. The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ Newton–Leibniz needs only continuity on $[a, b]$ , differentiability on $(a, b)$ , and a Riemann-integrable extension of the interior derivative

[F3]

$∣ ⟨ u, v ⟩ ∣ \leq ∥ u ∥ ∥ v ∥$ . The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ 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 standard $d$ -dimensional normal has density $(2 π)^{- d / 2} e^{- ∥ z ∥^{2} / 2}$ , and the ULA proposal has the displayed Gaussian density. The Axiom of Choice Multivariate normal law, including singular covariance A positive-definite multivariate normal law has its Gaussian density The ULA Gaussian proposal is a probability kernel with a positive density Unadjusted Langevin algorithm (ULA) Lebesgue measurable sets, the family $L (R^{n})$ , and the restricted set function $λ_{n}$

[F5]

The Borel function $V = e^{U / 2}$ is measurable under countable choice; AC implies countable choice. Continuous functions on Euclidean spaces are Borel measurable AC supplies countable selections and prescribed serial paths The Axiom of Countable Choice ( ${A C}_{ω}$ )

[F6]

A nonnegative integral is unchanged by the stated $C^{1}$ change of variables, and $\int_{R} e^{- z^{2}} d z = \sqrt{π}$ . A C^1 diffeomorphism satisfies the change-of-variables formula for nonnegative Lebesgue measurable functions The Gaussian integral $\int_{- \infty}^{\infty} e^{- x^{2}} d x = \sqrt{π}$

[F7]

Finite-dimensional Lebesgue measure is the finite product of one-dimensional Lebesgue measures on Borel sets, and Tonelli factors nonnegative product-measurable integrals. On Borel subsets of R^{m+n}, the product lambda_m times lambda_n agrees with lambda_{m+n} Tonelli's theorem for nonnegative measurable functions on a sigma-finite product

[F8]

Under [A1], $U (x) \geq c ∥ x - x_{⋆} ∥^{α} - a_{α}$ , where $c = ρ / (α + 1) > 0$ and $a_{α}$ is finite. Radial gradient drift forces potential coercivity

[F9]

Under countable choice, $\int_{R} e^{- ∣ z ∣} d z < \infty$ . The real-line exponential tail is Lebesgue integrable

Proof

Given: The hypotheses in the Statement.

1.1A1F1F2F3

By [F1], $\nabla U (x_{⋆}) = 0$ . For $h = y - x$ , apply [F2] to $t \mapsto U (x + t h)$ and subtract $⟨ \nabla U (x), h ⟩$ from the endpoint difference. The remaining integral is $\int_{0}^{1} ⟨ \nabla U (x + t h) - \nabla U (x), h ⟩ d t \leq \int_{0}^{1} L t ∥ h ∥^{2} d t = \frac{L}{2} ∥ h ∥^{2},$ by [A1] and [F3]. Thus $U (y) \leq U (x) + ⟨ \nabla U (x), y - x ⟩ + L ∥ y - x ∥^{2} / 2$ for all $x, y$ .

1.2A1F3algebra

Put $r = ∥ x - x_{⋆} ∥$ . If $r \geq M_{ρ}$ and $r > 0$ , the radial condition and [F3] give $ρ r^{α} \leq ⟨ \nabla U (x), x - x_{⋆} ⟩ \leq ∥ \nabla U (x) ∥ r,$ so $∥ \nabla U (x) ∥ \geq ρ r^{α - 1}$ .

1.3F4F6F7

For $c < 1 / 2$ and $β \in R$ , completing the square and applying [F6] gives $\frac{1}{\sqrt{2 π}} \int_{R} e^{- (1 / 2 - c) z^{2} + β z} d z = (1 - 2 c)^{- 1 / 2} e^{β^{2} / (2 (1 - 2 c))} .$ For $b \in R^{d}$ , apply this with $β = b_{i}$ for each $i < d$ . The product density in [F4], Lebesgue product identification, and Tonelli's theorem [F7] therefore give, for $Z \sim N_{d} (0, I_{d})$ , $E e^{c ∥ Z ∥^{2} + ⟨ b, Z ⟩} = (1 - 2 c)^{- d / 2} \exp ⁣ (\frac{∥ b ∥^{2}}{2 (1 - 2 c)}) .$

1.4A1F3F5F6F7F8F9step 1.1algebra

Verify the target normalizer before using the proposal-kernel conclusion of [F4]. Put $r = ∥ x - x_{⋆} ∥$ , $c = ρ / (α + 1)$ , and $k = c / \sqrt{d} > 0$ . Since $r^{α} \geq r - 1$ for $r \geq 0$ and $\sum_{i < d} ∣ x_{i} - x_{⋆, i} ∣ \leq \sqrt{d} r$ by [F3], [F8] gives $e^{- U (x)} \leq e^{a_{α} + c} e^{- c r} \leq e^{a_{α} + c} \prod_{i < d} e^{- k ∣ x_{i} - x_{⋆, i} ∣} .$ Translation and scaling [F6], followed by [F7] and [F9], show that the right-hand side has finite integral. Step 1.1 also gives $U (x) \leq L r^{2} / 2$ , so [F6]–[F7] imply $\int_{R^{d}} e^{- U (x)} d x \geq \int_{R^{d}} e^{- L ∥ x - x_{⋆} ∥^{2} / 2} d x = (2 π / L)^{d / 2} > 0.$ Continuity supplies Borel measurability as in [F5]. Thus all target hypotheses of the ULA algorithm and its proposal-kernel lemma hold.

2.1A1F4F5step 1.1step 1.3step 1.4algebra

Write $g = \nabla U (x)$ and $Y = x - γ g + \sqrt{2 γ} Z$ , the ULA update. Step 1.1 and [F4] imply $\frac{E V (Y)}{V (x)} \leq E \exp ⁣ (\frac{1}{2} ⟨ g, - γ g + \sqrt{2 γ} Z ⟩ + \frac{L}{4} ∥ - γ g + \sqrt{2 γ} Z ∥^{2}) .$ In step 1.3 take $c = L γ / 2$ and $b = \sqrt{2 γ} (1 - L γ) g / 2$ . Since $1 - 2 c = 1 - L γ > 0$ , expanding the exponent and collecting its $∥ g ∥^{2}$ terms gives $P_{γ} V (x) \leq V (x) (1 - L γ)^{- d / 2} \exp ⁣ (- \frac{γ ∥ g ∥^{2}}{4}) .$

3.1A1step 1.2step 2.1algebra

If $r \geq K_{γ}$ , then step 1.2 and the definition of $K_{γ}$ give $\frac{d}{2} [- \log (1 - L γ)] - \frac{γ ∥ g ∥^{2}}{4} \leq \frac{d}{2} [- \log (1 - L γ)] - \frac{γ ρ^{2} K_{γ}^{2 (α - 1)}}{4} \leq - γ .$ Step 2.1 therefore yields $P_{γ} V (x) \leq e^{- γ} V (x)$ on this region.

4.1A1F1step 1.1step 2.1step 3.1algebra∎

If $r \leq K_{γ}$ , use step 1.1 with starting point $x_{⋆}$ and [F1] to obtain $U (x) \leq L r^{2} / 2$ , so $V (x) \leq e^{L K_{γ}^{2} / 4}$ . Bounding the exponential factor in step 2.1 by one gives $P_{γ} V (x) \leq e^{L K_{γ}^{2} / 4} (1 - L γ)^{- d / 2} .$ Together with step 3.1, this proves the asserted drift inequality on both regions.

Depends on

Used by

ULA invariant laws have uniform exponential moments on the needed step ranges Lemma

Dependency tree · two levels

114 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 8 and proof §4.4 (standard reference, not scraped)