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 noncommuting two-noise equation requires an area term

Example

Let $W^{1}, W^{2}$ be independent standard Brownian coordinates and solve from $(0, 0)$ the two-dimensional SDE $d X_{t}^{1} = d W_{t}^{1}, d X_{t}^{2} = X_{t}^{1} d W_{t}^{2} .$ Its diffusion fields are $σ_{1} (x_{1}, x_{2}) = (1, 0)$ and $σ_{2} (x_{1}, x_{2}) = (0, x_{1})$ . They are noncommuting: $L_{1} σ_{2} = (0, 1)$ while $L_{2} σ_{1} = (0, 0)$ . On the first step, the exact second coordinate and its Milstein Taylor increment are $I_{12} = \int_{0}^{h} W_{s}^{1} d W_{s}^{2}$ . Although $I_{12} + I_{21} = Δ W^{1} Δ W^{2}$ , the individual area term is not determined by the two endpoint increments.

Facts & Assumptions

Given: AC; a filtered probability space whose filtration satisfies the usual conditions; and a standard two-dimensional Brownian motion $W = (W^{1}, W^{2})$ adapted to that filtration such that $W_{t} - W_{s}$ is independent of $F_{s}$ and has its standard two-dimensional normal law with covariance $(t - s) I_{2}$ for every $0 \leq s < t$ (for example, the usual augmentation of the joint natural filtration of $(W^{1}, W^{2})$ ), as required by Continuous Brownian Ito processes; a step length $h > 0$ ; and the It^o integrals in the Definition.

[F1]

Continuous Brownian Ito processes: Brownian coordinates are independent and increments after time zero are normal with their stated variances.

[F2]

Milstein updates, iterated Brownian integrals, and commutative noise: $L_{i} σ_{j} = D σ_{j} σ_{i}$ and $I_{i j} = \int_{0}^{h} W_{s}^{i} d W_{s}^{j}$ .

[L1]

Product identity and conditional moments for iterated Brownian integrals: $I_{12} + I_{21} = Δ W^{1} Δ W^{2}$ .

[F3]

Ito isometry and linearity in predictable L2: $E I_{12}^{2} = E \int_{0}^{h} (W_{s}^{1})^{2} d s$ .

[F4]

Standard normal and normal laws: Brownian increments have Gaussian densities, and independent coordinates have product law.

[F5]

Conditional expectation given a sigma algebra: conditional expectation is characterized by integrals on events in the conditioning sigma algebra.

[F6]

Basic algebra and order properties of conditional expectation: conditional expectation is linear, preserves expectation, and is $L^{1}$ -contractive.

[F7]

Cauchy-Schwarz for random variables: $E ∣ Z ∣ \leq (E ∣ Z ∣^{2})^{1 / 2}$ for square-integrable $Z$ .

[F8]

Conditional expectation is the l2 orthogonal projection: for $I \in L^{2}$ and $J = E [I ∣ G]$ , $E [(I - J) Z] = 0$ for every $Z \in L^{2} (G)$ , in particular $Z = J$ .

[A1]

The Axiom of Choice: AC is inherited through [F1], [F3], and the conditional-expectation interface [F6].

Verification

Given: The assumptions above.

1.1F1F2givenalgebra

The Jacobian of $σ_{2}$ sends $(1, 0)$ to $(0, 1)$ , so $L_{1} σ_{2} = (0, 1)$ ; the Jacobian of the constant field $σ_{1}$ is zero, so $L_{2} σ_{1} = (0, 0)$ . Thus commutativity fails. Starting from $X_{0} = (0, 0)$ , the first coordinate is $W_{t}^{1}$ and the second is $\int_{0}^{t} W_{s}^{1} d W_{s}^{2}$ . The general Milstein Taylor update [F2] therefore has second-coordinate increment $I_{12}$ on the first step.

1.2F3L1given

By [L1], the endpoints determine $I_{12} + I_{21} = U V$ , where $U = Δ W^{1}$ and $V = Δ W^{2}$ . Let $π_{n} = {0 = s_{0} < \dots < s_{q_{n}} = h}$ be deterministic partitions with mesh $∣ π_{n} ∣ \to 0$ , and put $S_{n} = \sum_{k = 0}^{q_{n} - 1} W_{s_{k}}^{1} (W_{s_{k + 1}}^{2} - W_{s_{k}}^{2})$ . The It^o isometry [F3] gives $E ∣ S_{n} - I_{12} ∣^{2} = \sum_{k} \int_{s_{k}}^{s_{k + 1}} (s - s_{k}) d s \leq h ∣ π_{n} ∣ / 2 \to 0$ .

2.1F1F5F6F7step 1.2algebra

For $0 < s < h$ , write $A = W_{s}^{1}$ and $U - A = W_{h}^{1} - W_{s}^{1}$ ; their joint density is $p_{s} (a) p_{h - s} (u - a)$ , where $p_{r}$ is the $N (0, r)$ density. Dividing by the marginal density $p_{h} (u)$ and completing the square gives $E [A ∣ U = u] = (s / h) u$ . At $s = 0$ and $s = h$ the same formula follows from $A = 0$ and $A = U$ , respectively. For $ℓ_{k} = s_{k + 1} - s_{k}$ , the pair $B_{k} = W_{s_{k + 1}}^{2} - W_{s_{k}}^{2}$ and $V - B_{k}$ has density $p_{ℓ_{k}} (b) p_{h - ℓ_{k}} (v - b)$ when $ℓ_{k} < h$ ; completing the square gives $E [B_{k} ∣ V = v] = (ℓ_{k} / h) v$ , and if $ℓ_{k} = h$ then $B_{k} = V$ gives the same result. Independence of the two Brownian coordinate processes [F1] makes the joint density of $(A, U, B_{k}, V)$ the product of these two pair densities. Dividing by $p_{h} (u) p_{h} (v)$ shows that the conditional density of $(A, B_{k})$ given $(U, V) = (u, v)$ factors, so $E [A B_{k} ∣ U, V] = (s / h) U (ℓ_{k} / h) V$ . Therefore $E [S_{n} ∣ σ (U, V)] = \frac{U V}{h^{2}} \sum_{k} s_{k} (s_{k + 1} - s_{k}) ⟶ \frac{U V}{2},$ because the sum is a left Riemann sum for $\int_{0}^{h} s d s = h^{2} / 2$ . By [F7], step 1.2 implies $S_{n} \to I_{12}$ in $L^{1}$ ; conditional expectation is $L^{1}$ -contractive by [F6], so [F5] gives $E [I_{12} ∣ σ (U, V)] = U V / 2$ .

3.1F1F3F4F5F8step 2.1A1algebra∎

The isometry [F3] gives $E I_{12}^{2} = \int_{0}^{h} E (W_{s}^{1})^{2} d s = h^{2} / 2$ . Also $U, V$ are independent with second moments $h$ , so step 2.1 gives $J : = E [I_{12} ∣ σ (U, V)] = U V / 2$ and $E J^{2} = E [U^{2} V^{2}] / 4 = h^{2} / 4$ . By [F8], $E [(I_{12} - J) J] = 0$ ; expanding the square therefore gives $E ∣ I_{12} - J ∣^{2} = E I_{12}^{2} - E J^{2} = h^{2} / 4 > 0$ . If $I_{12}$ were a measurable function of $(U, V)$ , the conditional-expectation identity [F5] would give $I_{12} = J$ almost surely, contradicting this positive residual. Thus the endpoint increments do not determine the required area sample, and any approximation has a separate error and cost.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

50 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

Kloeden and Platen, Numerical Solution of Stochastic Differential Equations, Example 10.3.4, printed pp. 349-350 (standard reference, not scraped)