ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-22

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.

Variance of dyadic quadratic variation

Example

With the notation of Expected dyadic quadratic variation, the dyadic quadratic sum $Q_{n} = \sum_{k = 1}^{2^{n}} (B_{k h} - B_{(k - 1) h})^{2}$ over $[0, T]$ has $Var (Q_{n}) = \frac{2 T^{2}}{2^{n}},$ so $Q_{n} \to T$ in $L^{2}$ as $n \to \infty$ .

Facts & Assumptions

Given: AC, a standard Brownian motion $B$ , $T > 0$ , $n \geq 1$ with $h = T / 2^{n}$ and $Δ_{k} = B_{k h} - B_{(k - 1) h}$ .

[F1]

The increments over disjoint intervals are independent with laws $N (0, h)$ , and $E (Δ B)^{2} = h$ , $E (Δ B)^{4} = 3 h^{2}$ for an increment of length $h$ . Brownian motion Gaussian even moments for Brownian increments

[F2]

The mean of the dyadic sum is $E Q_{n} = T$ . Expected dyadic quadratic variation

[F3]

AC is the ambient assumption of the Brownian interfaces. The Axiom of Choice

Verification

technique · direct

1.1

For each $k$ , [F1] gives $Var (Δ_{k}^{2}) = E Δ_{k}^{4} - (E Δ_{k}^{2})^{2} = 3 h^{2} - h^{2} = 2 h^{2}$ .

givenF1

2.1

The variables $Δ_{k}^{2}$ are functions of increments over disjoint intervals, hence independent by [F1], so the variance of the sum is the sum of the variances: $Var (Q_{n}) = \sum_{k = 1}^{2^{n}} 2 h^{2} = 2^{n} \cdot 2 (T / 2^{n})^{2} = 2 T^{2} / 2^{n}$ .

step 1.1F1

3.1

Since $E Q_{n} = T$ by [F2], $E (Q_{n} - T)^{2} = Var (Q_{n}) = 2 T^{2} / 2^{n} \to 0$ , which is the $L^{2}$ convergence $Q_{n} \to T$ .

step 2.1F2

4.1

The cases are covered: the independence of the squared increments is the only place where the joint law is used; the value $n = 1$ is included and gives $Var (Q_{1}) = T^{2}$ ; the limit is taken as $n \to \infty$ with $T$ fixed and positive; and AC enters only through [F3].

step 2.1F3given∎

Source notes

Lawler, Theorem 2.8.1, obtains the variance of the quadratic sums from the fourth Gaussian moment and the independence of the increments, giving the mean-square convergence used in the dyadic quadratic-variation theorem.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

18 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

Gregory F. Lawler, Stochastic Calculus: An Introduction with Applications, Theorem 2.8.1 (standard reference, not scraped)