ExampleConstruction: Literature-sourcedVerification: 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.

ULA has a biased invariant variance for a standard Gaussian target

Example

Assume AC. Take the standard Gaussian target $π = N (0, 1)$ , potential $U (x) = x^{2} / 2$ , and ULA step size $γ = 1$ . Its invariant law is $N (0, 2)$ , so the unadjusted chain does not preserve the target variance.

Facts & Assumptions

Given: AC, the standard Gaussian target, and ULA with $γ = 1$ .

[A1]

AC is assumed in the standard-normal target and fresh ULA-noise construction. The Axiom of Choice

[F1]

Under this potential, $\nabla U (x) = x$ and the update is $X^{'} = \sqrt{2} Z$ , independent of the current state, where $Z \sim N (0, 1)$ . Unadjusted Langevin algorithm (ULA) Standard normal and normal laws

[F2]

For every $0 < γ < 2$ , the Gaussian ULA invariant law is $N (0, 2 / (2 - γ))$ , and its variance is $2 / (2 - γ)$ . The Gaussian ULA invariant law has variance $2 / (2 - γ)$

[F3]

The target $N (0, 1)$ has variance $1$ . Characteristic function of a normal law

Verification

Given: AC; the standard Gaussian target and $γ = 1$ .

1.1A1F1F2givenalgebra

Substituting $γ = 1$ in [F2] gives the invariant law $N (0, 2)$ and variance $2$ . Equivalently, [F1] shows every transition row equals $N (0, 2)$ , so this law is invariant directly.

2.1A1F3step 1.1algebra∎

By [F3], the target has variance $1$ . Since the invariant law in step 1.1 has variance $2$ , the two laws differ. The choice $γ = 1$ is interior to $0 < γ < 2$ , the regime of the invariant-law theorem.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

42 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, §3.3 (standard reference, not scraped)
Gautam Iyer, Lecture 20: Langevin Monte Carlo, course notes, §3.1 (standard reference, not scraped)