TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

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 strong order one of BAOAB

Statement

Assume the force and model hypotheses of Moment-weighted local defect bounds for BAOAB. 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} ∣^{2} < \infty$ , independent of $σ (W_{t} - W_{0} : 0 \leq t \leq T)$ . Initialize both BAOAB and the exact underdamped Langevin solution at this same $Z_{0}$ . Couple each BAOAB OU draw to the same Brownian path as the exact solution by taking the standardized exact OU integral on that grid interval. If $Z_{n}^{B}$ is the BAOAB state and $Z_{t_{n}}$ the exact state at $t_{n} = n h$ , then a constant $C_{T}$ independent of $N$ satisfies $\max_{0 \leq n \leq N} E ∣ Z_{n}^{B} - Z_{t_{n}} ∣^{2} \leq C_{T} h^{2} .$ Thus the grid-point root-mean-square strong error is $O (h)$ on the fixed finite interval. No invariant-law or long-time error rate is asserted.

Facts & Assumptions

Given: The SDE and force assumptions in Moment-weighted local defect bounds for BAOAB, a common $F_{0}$ -measurable initial state $Z_{0} \in L^{2}$ independent of $σ (W_{t} - W_{0} : 0 \leq t \leq T)$ , initialization of both processes at this state, a fixed horizon $T > 0$ , $h = T / N \leq 1$ , and the prescribed Brownian coupling.

[F1]

Global strong well-posedness for Lipschitz Itô SDEs: the exact solution exists globally and has a finite second moment uniformly on $[0, T]$ under the stated globally Lipschitz, linear-growth drift.

[L1]

Moment-weighted local defect bounds for BAOAB: the exact and BAOAB one-step residuals have conditional mean $O (h^{2} (1 + ∣ Z_{n} ∣))$ and conditional second moment $O (h^{3} (1 + ∣ Z_{n} ∣^{2}))$ ; for the same Brownian noise, the BAOAB residual is $C h$ -Lipschitz in the starting state.

[A1]

The Axiom of Choice: AC is inherited through the SDE and It^o interfaces in [F1] and [L1]; the error recurrence uses no further choice.

Proof

Given: The assumptions above.

1.1F1L1givenalgebra

The exact solution has $\sup_{t \leq T} E ∣ Z_{t} ∣^{2} < \infty$ by [F1]. Each B or A half-step changes the state by a quantity bounded by $C h (1 + ∣ z ∣)$ , because $F$ has linear growth and $M^{- 1}$ is fixed. For the O step, $p \mapsto a p + η$ with $0 < a < 1$ , $E [η ∣ F_{n}] = 0$ , and $E ∣ η ∣^{2} \leq C h$ by [L1], so $E [∣ a p + η ∣^{2} ∣ F_{n}] \leq ∣ p ∣^{2} + C h$ . Expanding the squares of the finitely many B/A/O stage updates and using $2 ∣ x ∣ ∣ y ∣ \leq h ∣ x ∣^{2} + h^{- 1} ∣ y ∣^{2}$ shows $E [1 + ∣ Z_{n + 1}^{B} ∣^{2} ∣ F_{n}] \leq (1 + C h) (1 + ∣ Z_{n}^{B} ∣^{2}) + C h$ . Iterating this scalar inequality for $N h = T$ yields $\max_{n \leq N} E ∣ Z_{n}^{B} ∣^{2} \leq C_{T} (1 + E ∣ Z_{0} ∣^{2})$ .

1.2F1L1givenalgebra

Write $e_{n} = Z_{n}^{B} - Z_{t_{n}}$ . Apply [L1] at the common state $Z_{t_{n}}$ and at the two actual states, and subtract the two one-step expansions. The result is [F1, L1, given, algebra] $e_{n + 1} = e_{n} + h (b (Z_{n}^{B}) - b (Z_{t_{n}})) + Δ_{n} + δ_{n},$ where $Δ_{n} = R^{B} (Z_{n}^{B}) - R^{B} (Z_{t_{n}})$ and $δ_{n} = R^{B} (Z_{t_{n}}) - R^{E} (Z_{t_{n}})$ . Let $d_{n} = E [Δ_{n} ∣ F_{t_{n}}]$ and $M_{n + 1} = Δ_{n} - d_{n}$ . The residual Lipschitz bound in [L1] gives $∣ d_{n} ∣ \leq C h ∣ e_{n} ∣$ and $E ∣ M_{n + 1} ∣^{2} \leq C h^{2} E ∣ e_{n} ∣^{2}$ . Put $r_{n} = E [δ_{n} ∣ F_{t_{n}}]$ and $Q_{n + 1} = δ_{n} - r_{n}$ . Conditional Jensen and [L1], together with the exact-state moment bound from [F1], give $E ∣ r_{n} ∣^{2} \leq C h^{4}$ and $E ∣ Q_{n + 1} ∣^{2} \leq C h^{3}$ . Both $M_{n + 1}$ and $Q_{n + 1}$ have conditional mean zero. Hence, with $u_{n} = b (Z_{n}^{B}) - b (Z_{t_{n}}) + d_{n} / h$ , the error recurrence is $e_{n + 1} = e_{n} + h u_{n} + r_{n} + M_{n + 1} + Q_{n + 1}$ , where $∣ u_{n} ∣ \leq C ∣ e_{n} ∣$ by global Lipschitz continuity of $b$ and the bound on $d_{n}$ .

2.1F1L1A1step 1.2algebra∎

Since $e_{n} + h u_{n} + r_{n}$ is $F_{t_{n}}$ -measurable, its cross expectation with the centered sum $M_{n + 1} + Q_{n + 1}$ is zero. Young's inequality and the bounds in step 1.2 give [F1, L1, A1, step 1.2, algebra] $E ∣ e_{n} + h u_{n} + r_{n} ∣^{2} \leq (1 + C h) E ∣ e_{n} ∣^{2} + C h^{3},$ $E ∣ M_{n + 1} + Q_{n + 1} ∣^{2} \leq 2 C h^{2} E ∣ e_{n} ∣^{2} + 2 C h^{3} \leq C h E ∣ e_{n} ∣^{2} + C h^{3} .$ Therefore $E ∣ e_{n + 1} ∣^{2} \leq (1 + C h) E ∣ e_{n} ∣^{2} + C h^{3}$ . Starting from $e_{0} = 0$ and iterating gives $E ∣ e_{n} ∣^{2} \leq C h^{3} \sum_{j = 0}^{n - 1} (1 + C h)^{j} \leq C_{T} h^{3} N e^{C T} \leq C_{T} h^{2}$ for each $n \leq N$ , because $N h = T$ . Taking the maximum over the finitely many grid indices proves the statement. AC enters only through [A1].

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

24 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

Adam Telatovich and Xiantao Li, Strong Convergence Analysis for Numerical Methods for the Langevin Dynamics Model and Higher-order Operator-splitting Schemes, §§3.1–3.2 and 5.2 (standard reference, not scraped)
Benedict Leimkuhler and Charles Matthews, Rational Construction of Stochastic Numerical Methods for Molecular Sampling, §2 and Appendix (standard reference, not scraped)