ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-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.

A verified weak-order contract for the Ornstein–Uhlenbeck process

Example

Work on a complete filtered probability space whose filtration is right-continuous and contains all $P$ -null subsets of $F$ in $F_{0}$ . Let $W$ be an adapted standard one-dimensional Brownian motion whose increments after time $s$ are independent of $F_{s}$ . On $[0, 1]$ , take $d X_{t} = - X_{t} d t + d W_{t}$ with $X_{0} = 0$ and bounded Lipschitz payoff $φ (x) = \cos x$ . For $0 \leq t \leq 1$ , put $r (t) = e^{t - 1}$ and $u (t, x) = \exp ⁣ (- \frac{1 - r (t)^{2}}{4}) \cos (r (t) x) .$ This value function satisfies the backward equation, the mixed derivative growth requirement with $q = 2$ , and the moment threshold $p \geq 12$ . Thus the conditional weak theorem applies and gives Euler weak error $O (h)$ .

Facts & Assumptions

Given: AC; the complete usual filtered Brownian setup above; $T = 1$ ; the $F_{0}$ -measurable initial value $X_{0} = 0$ ; the Ornstein–Uhlenbeck SDE and payoff displayed in the Example; and Euler step size $0 < h \leq 1$ with $1 / h \in N$ .

[F1]

For a one-dimensional continuous Brownian Itô process and $F \in C^{1, 2}$ , Itô's formula has drift $F_{t} + b F_{x} + \frac{1}{2} σ^{2} F_{x x}$ and stochastic term $σ F_{x} d W$ . One-dimensional Ito formula

[F2]

An Itô integral with deterministic $h \in L^{2} [0, T]$ has centered normal law $N (0, \int_{0}^{T} h (s)^{2} d s)$ . Deterministic Ito integrals are Gaussian

[F3]

A $N (m, v)$ variable has characteristic function $t \mapsto \exp (i m t - v t^{2} / 2)$ . Characteristic function of a normal law

[F4]

The Euler interpolation on a grid interval is $Y_{t} = Y_{k} + b (t_{k}, Y_{k}) (t - t_{k}) + σ (t_{k}, Y_{k}) (W_{t} - W_{t_{k}})$ . Euler–Maruyama step process and continuous interpolation

[F5]

Under the Euler coefficient and initial-moment hypotheses, for every finite $p \geq 2$ the step and continuous interpolation have uniformly bounded pointwise $p$ th moments. Euler–Maruyama uniform moments and interpolation increments

[F6]

For a scalar standard normal $Z$ , $E ∣ Z ∣^{12} = 11!! < \infty$ by the Gaussian even-moment lemma at $m = 6$ . The normal scaling convention gives $N (0, v)$ as the law of $\sqrt{v} Z$ , including $v = 0$ . Gaussian even moments for Brownian increments Standard normal and normal laws

[F7]

If the bounded test payoff's backward value function has the stated mixed derivatives and $p \geq 2 q + 8$ moments, the weak Euler error is at most $C h$ . Euler–Maruyama weak order one under backward regularity

[A1]

AC is included because the Brownian, deterministic-integral Gaussian, normal-characteristic-function and normal-moment suppliers in [F1]–[F3], [F6] adopt it. The Axiom of Choice

Verification

Given: The hypotheses in the Statement or Example and the facts above.

1.1A1F1F2given

Apply [F1] to $e^{t} X_{t}$ . The drift terms cancel, so $X_{t} = \int_{0}^{t} e^{- (t - s)} d W_{s} .$ For a solution started at $(t, x)$ , the same calculation gives $X_{1}^{t, x} = r (t) x + \int_{t}^{1} e^{- (1 - s)} d W_{s} .$ By [F2], the last integral is $N (0, (1 - r (t)^{2}) / 2)$ .

1.2givenalgebra

Since $r^{'} = r$ and $A (t) : = e^{- (1 - r (t)^{2}) / 4}$ satisfies $A^{'} / A = r^{2} / 2$ , direct differentiation gives $u_{t} = A (\frac{r^{2}}{2} \cos (r x) - r x \sin (r x)), u_{x} = - A r \sin (r x), u_{x x} = - A r^{2} \cos (r x) .$ For the generator $L = - x \partial_{x} + \frac{1}{2} \partial_{x x}$ , these formulas imply $(\partial_{t} + L) u = 0$ . Every mixed derivative $\partial_{t}^{j} \partial_{x}^{k} u$ with $j \leq 2$ , $k \leq 4$ is a finite sum of bounded smooth coefficient functions times $x^{a} \sin (r x)$ or $x^{a} \cos (r x)$ with $a \leq 2$ ; hence it is bounded by $C (1 + ∣ x ∣^{2})$ . The backward contract holds with $q = 2$ .

2.1F2F3step 1.1algebra

By [F3], for that normal variable $Z$ , $E e^{i Z} = e^{- (1 - r^{2}) / 4}$ . Taking the real part after multiplying by $e^{i r x}$ gives $E \cos (X_{1}^{t, x}) = e^{- (1 - r (t)^{2}) / 4} \cos (r (t) x) = u (t, x) .$ Thus $u$ is the stated backward value function and $u (1, x) = \cos x$ .

2.2F2F5F6givenstep 1.1

The exact process is centered normal at each time with variance $(1 - e^{- 2 t}) / 2 \leq 1 / 2$ by [F2], so [F6] at order $12$ gives $E ∣ X_{t} ∣^{12} = 11!! {(1 - e^{- 2 t}) / 2}^{6} \leq 11!! / 64$ uniformly in $t \in [0, 1]$ , including $t = 0$ . For the Euler process, $b (x) = - x$ is globally Lipschitz with linear growth, $σ (x) = 1$ is globally Lipschitz with linear growth, the time modulus is zero, and $X_{0} = 0$ has every moment. Applying [F5] at $p = 12$ therefore gives uniform pointwise 12th moments for $Y^{h}$ and ${\overset{ˉ}{Y}}^{h}$ . The threshold is $p = 12 = 2 q + 8$ .

3.1A1F4F7step 2.1step 1.2step 2.2∎

The payoff is bounded and $1$ -Lipschitz. By [F4], the interpolation agrees with the Euler recursion at $T$ , so the conclusion of [F7] applies to $Y_{N}^{h}$ . Steps 2.1–2.2 verify its backward regularity and moment premises, giving $∣ E \cos (X_{1}) - E \cos (Y_{N}^{h}) ∣ \leq C h$ . AC is inherited through [A1].

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

105 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.