TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge 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.

Finite-time weak order two of BAOAB

Statement

Assume the model data of Underdamped Langevin equation and canonical Gibbs density, $V \in C^{8}$ , and $D^{j} V$ is globally bounded for $2 \leq j \leq 8$ . Let $T > 0$ , $N \geq 1$ , $h = T / N \leq 1$ , and let $Z_{0}$ be a common $F_{0}$ -measurable $R^{2 d}$ -valued initial state with $E ∣ Z_{0} ∣^{6} < \infty$ , independent of $σ (W_{t} - W_{0} : 0 \leq t \leq T)$ ; initialize both processes at this state. Let $ϕ \in C_{b}^{8} (R^{2 d})$ . Run BAOAB by taking each fresh Gaussian vector to be the standardized exact OU integral on that grid interval from the same Brownian motion that drives the exact SDE. If $Z_{N}^{B}$ is its state after $N$ steps and $Z_{T}$ is the exact SDE state, then $∣ E ϕ (Z_{N}^{B}) - E ϕ (Z_{T}) ∣ \leq C_{T, ϕ, Z_{0}} h^{2} .$ The order is a finite-time weak order statement under the displayed smoothness and moment assumptions; it gives no invariant-measure bias or ergodicity conclusion.

Facts & Assumptions

Given: The hypotheses above and a uniform grid $t_{n} = n h$ on $[0, T]$ ; the initial state is common, $F_{0}$ -measurable, and independent of $σ (W_{t} - W_{0} : 0 \leq t \leq T)$ , and the BAOAB OU draws use the prescribed Brownian coupling.

[F1]

Underdamped Langevin equation and canonical Gibbs density: $C_{b}^{8}$ means bounded continuous derivatives through order eight, and the total generator is $L = A + B + O$ with the three operators in Symmetric BAOAB one-step weak expansion.

[F2]

Symmetric BAOAB one-step weak expansion: for test functions $ψ \in C_{b}^{6}$ with a common bound on derivatives through order six, $∣ K_{h} ψ (z) - P_{h} ψ (z) ∣ \leq C h^{3} (1 + ∣ z ∣^{3})$ uniformly under the stated model assumptions. The lemma's general $C_{P}^{6}$ branch instead permits an exponent depending on the test-function growth.

[F3]

Global strong well-posedness for Lipschitz Itô SDEs: the exact solution exists uniquely and globally for the globally Lipschitz, linearly growing drift.

[F4]

Multidimensional Ito formula for Brownian-driven processes: It^o's formula supplies the generator moment estimate for smooth Lyapunov functions and the short-time semigroup expansion.

[F5]

Dominated convergence: dominated pointwise convergence permits differentiation limits and integral limits under the stated integrable bounds.

[F6]

Fatou's lemma: the integral of a nonnegative pointwise limit is at most the limit inferior of the integrals.

[A1]

The Axiom of Choice: AC is inherited through [F2]–[F6]; the finite-grid argument uses no further choice.

Proof

Given: The assumptions above.

1.1F1F2F3F4F6givenalgebra

Put $W_{s} (z) = (1 + ∣ z ∣^{2})^{s}$ for integer $s \geq 1$ . The drift $b$ has linear growth and bounded derivatives of positive order, and $G$ is constant, so $∣ L W_{s} (z) ∣ \leq C_{s} W_{s} (z)$ . Applying [F4] to the solution stopped on radius $R$ , taking expectations and applying Gronwall gives $E W_{s} (Z_{t \land τ_{R}}) \leq e^{C_{s} t} E W_{s} (Z_{0})$ ; Fatou’s lemma [F6] as $R \to \infty$ gives uniformly bounded exact moments through order six on $[0, T]$ . Each B or A stage has the form $z + h δ (z)$ with $∣ δ (z) ∣ \leq C (1 + ∣ z ∣)$ , hence the mean-value formula and Young’s inequality give $W_{s} (z + h δ (z)) \leq (1 + C h) W_{s} (z) + C h$ . In the O stage $p$ becomes $a p + η$ ; conditional terms linear in $η$ vanish and terms of degree $j \geq 2$ have moments at most $C_{j} h^{j / 2}$ , so Young’s inequality gives the same stage bound. Composing five stages and iterating over $N h = T$ yields $\max_{n \leq N} E W_{s} (Z_{n}^{B}) \leq C_{T}$ for $s \leq 3$ .

2.1F1F2F3F5step 1.1

For $0 \leq t \leq T$ , the solution flow is differentiable through order six in its initial state. The first derivative solves $\dot{J} = D b (Z_{t}) J$ ; each higher derivative solves the same linear equation with forcing a finite sum of products of lower flow derivatives and bounded derivatives of $b$ . Induction and Gronwall bound these derivatives uniformly. Differentiating $P_{t} ϕ (z) = E ϕ (Z_{t}^{z})$ under expectation is justified by bounded derivatives of $ϕ$ and the flow bounds, so $P_{t} ϕ$ has bounded derivatives through order six uniformly. Together with the Markov bound $∥ P_{t} ϕ ∥_{\infty} \leq ∥ ϕ ∥_{\infty}$ , these derivative estimates give a common $C_{b}^{6}$ bound for $ψ_{n} = P_{T - t_{n + 1}} ϕ$ . Apply precisely the bounded-test branch of [F2], whose cubic weight is uniform in $n, N$ ; no generic polynomial-growth exponent is substituted.

3.1A1F2F3F5F6step 1.1step 2.1algebra∎

Let $K_{h}$ be the BAOAB transition and $P_{h}$ the exact transition. Inserting one exact transition at a time and using the Markov property gives [A1, F2, F3, F5, F6, step 1.1, step 2.1, algebra] $E ϕ (Z_{N}^{B}) - E ϕ (Z_{T}) = \sum_{n = 0}^{N - 1} E [(K_{h} - P_{h}) P_{T - t_{n + 1}} ϕ (Z_{n}^{B})] .$ By [F2] and step 2.1, each summand has absolute value at most $C h^{3} E (1 + ∣ Z_{n}^{B} ∣^{3}) \leq C_{T} h^{3}$ using the $s = 2$ moment bound in step 1.1. Summing $N = T / h$ terms gives $C_{T} N h^{3} = C_{T} T h^{2}$ . The result is finite-time weak order two and says nothing about invariant bias.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

69 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

Benedict Leimkuhler and Charles Matthews, Rational Construction of Stochastic Numerical Methods for Molecular Sampling, §§2–3 and Appendix (standard reference, not scraped)
Jean-Noël Roux, Stéphane Rodts, and Gabriel Stoltz, Introduction à la physique statistique et à la physique quantique, §§5.2.1–5.2.2 (standard reference, not scraped)
Assyr Abdulle, Gilles Vilmart, and Konstantinos C. Zygalakis, Long time accuracy of Lie-Trotter splitting methods for Langevin dynamics, §§2.2–3.1 (standard reference, not scraped)