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

Euler discretization bias and path-to-path variance

Example

Let $X_{0}$ take values in ${1, 2}$ with probability $1 / 2$ each, and consider the random-initial-value ODE $x^{'} (t) = x (t)$ on $0 \leq t \leq 1$ . Its exact endpoint is $X_{1} = e X_{0}$ , and the target is $θ = E [X_{1}^{2}]$ . Define the one-step explicit Euler rule at $h = 1$ by $X_{1}^{h} = X_{0} + h X_{0} = 2 X_{0}$ . For an integer $M \geq 2$ , independently simulate initial values $X_{0}^{(1)}, \dots, X_{0}^{(M)}$ with this law, set $Y_{r} : = (2 X_{0}^{(r)})^{2}$ , and return ${\overline{Y}}_{M} : = M^{- 1} \sum_{r = 1}^{M} Y_{r}$ .

Facts & Assumptions

Given: The ODE, initial-value law, one-step Euler rule, and independent path simulations specified in the Example. Compute the discretized-target bias and the path-simulation variance.

[F1]

A scalar error ledger uses successive same-scale references and defines each stage error as the adjacent difference. (Successive statistical and computational error targets)

[F2]

The total error along a finite scalar reference chain is the sum of its signed stage errors. (Pathwise error decomposition along a reference chain)

[F3]

For $M \geq 2$ IID finite-variance replicate outputs with variance $τ^{2}$ , the variance of their average is $τ^{2} / M$ . (Unbiased variance estimate from independent computation replicates)

[F4]

For real $a < b$ , a real function continuous on $[a, b]$ and differentiable on $(a, b)$ satisfies $f (b) - f (a) = f^{'} (c) (b - a)$ for some $c \in (a, b)$ . (The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ )

[F5]

$e = \exp (1)$ for $\exp (x) = \sum_{k = 0}^{\infty} x^{k} / k!$ . (The real exponential function and the number $e$ by a power series)

[F6]

$\exp$ is differentiable with $(\exp)^{'} = \exp$ . (The exponential function is smooth and $(\exp)^{'} = \exp$ )

[F7]

The derivative of a differentiable composition is given by the chain rule. (The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ )

[F8]

IID means common distribution and mutual independence. (Identical distribution and IID families)

[F9]

A function differentiable at a limit point is continuous there. (A function differentiable at $c$ is continuous at $c$ )

[F10]

Applying measurable maps coordinatewise to independent random variables preserves independence. (Measurable coordinatewise functions preserve independence)

[F11]

Products of measurable real-valued functions and their real scalar multiples are measurable. (Arithmetic and lattice operations preserve measurability whenever they are defined)

[A1]

$X_{0}$ equals $1$ and $2$ with probabilities $1 / 2$ each; an ODE solution $x$ is defined and differentiable on an open interval containing $[0, 1]$ , satisfies $x^{'} = x$ , and has initial value $x (0) = X_{0}$ .

[A2]

The discretization is the explicitly defined one-step rule $X_{1}^{h} = X_{0} + h X_{0}$ at $h = 1$ ; the $M$ simulated initial values are IID copies of $X_{0}$ .

Verification

1.1givenA1F4F5F6F7F9algebra

By [F5] and [F6], $x_{*} (t) = X_{0} \exp (t)$ solves the stated initial-value problem. For any solution $x$ , put $f (t) = \exp (- t)$ and $u (t) = f (t) x (t)$ . By [F6] and [F7], $f^{'} (t) = - f (t)$ . For $h \neq 0$ with $t + h \in [0, 1]$ , $\frac{u (t + h) - u (t)}{h} = f (t + h) \frac{x (t + h) - x (t)}{h} + x (t) \frac{f (t + h) - f (t)}{h}$ . As $h \to 0$ , continuity of $f$ and differentiability of $x, f$ make the right side tend to $f (t) x^{'} (t) + x (t) f^{'} (t) = 0$ because $x^{'} = x$ . Thus $u^{'} = 0$ on $(0, 1)$ . The solution $x$ is continuous at $0, 1$ by [F9], so $u$ is continuous on $[0, 1]$ ; [F4] gives $u (1) = u (0) = X_{0}$ . The same derivative calculation applied to the continuous product $v (t) = f (t) \exp (t)$ gives $v^{'} = 0$ on $(0, 1)$ ; [F4] then yields $\exp (- 1) e = v (1) = v (0) = 1$ , since $\exp (0) = 1$ by [F5]. Multiplying $u (1) = X_{0}$ by $e$ therefore gives $x (1) = e X_{0}$ . By [F5] and $E [X_{0}^{2}] = (1 + 4) / 2 = 5 / 2$ , the exact target is $θ = e^{2} E [X_{0}^{2}] = (5 / 2) e^{2}$ .

1.2givenA1A2F5algebra

The Euler update gives $X_{1}^{h} = 2 X_{0}$ , so the exact-arithmetic discretized target is $θ_{h} = E [4 X_{0}^{2}] = 10$ . Since $e = \sum_{k = 0}^{\infty} 1 / k! > 2$ , its bias is $10 - (5 / 2) e^{2} < 0$ .

1.3givenA1A2F8algebra

By [F8] and [A2], a single simulated squared Euler endpoint is $4 X_{0}^{2}$ , equal to $4$ or $16$ with equal probability. Its mean is $10$ and its variance is $((4 - 10)^{2} + (16 - 10)^{2}) / 2 = 36$ .

2.1F3F8F10F11step 1.2step 1.3A2algebra

By [F11], $z \mapsto 4 z^{2}$ is measurable; by [F8] and [A2] the initial values are IID, so [F10] makes the outputs independent. Their common two-point law is computed in step 1.3, hence they are IID. Then [F3] gives variance $36 / M$ for their average, while the discretization bias in step 1.2 remains $10 - (5 / 2) e^{2}$ for every $M$ .

3.1F1F2step 1.1step 1.2step 2.1algebra∎

For a realized path average ${\overline{Y}}_{M}$ , the ledger chain $θ, θ_{h}, {\overline{Y}}_{M}$ gives ${\overline{Y}}_{M} - θ = (θ_{h} - θ) + ({\overline{Y}}_{M} - θ_{h})$ by [F1] and [F2], separating discretization bias from path-simulation error.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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