Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 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.

Brownian quadratic variation on dyadic partitions

Statement

Let B be a standard Brownian motion Brownian motion and fix T>0. For n≥1 let πn be the dyadic partition of [0,T] with points kT/2n, k=0,…,2n, and let Qn:=∑k=12n(BkT/2n−B(k−1)T/2n)2=[B]Tπn in the notation of Quadratic variation along a partition sequence. Then Qn→T in L2 and almost surely as n→∞.

Facts & Assumptions

Given: AC, a standard Brownian motion B, T>0, and the dyadic partitions πn above with h=T/2n.

[F1]

The increments of B over disjoint intervals are independent with laws N(0,h) for interval length h. Brownian motion

[F2]

If Xt−Xs has law N(0,∣t−s∣) then E∣Xt−Xs∣2m=cm∣t−s∣m with cm=(2m−1)!!; in particular E(ΔB)2=h and E(ΔB)4=3h2 for an increment of length h. Gaussian even moments for Brownian increments

[F3]

Chebyshev: P(∣X−EX∣≥λ)≤Var⁡(X)/λ2 for a square-integrable real X and λ>0. Chebyshev's inequality for random variables

[F4]

First Borel-Cantelli: if ∑nP(Gn)<∞ then almost surely only finitely many Gn occur. First Borel-Cantelli lemma for events

[F5]

[B]Tπn denotes the terminal quadratic sum along the named partition sequence πn, whose mesh T/2n tends to zero. Quadratic variation along a partition sequence

[F6]

AC is the ambient assumption of the Brownian and normal-law interfaces. The Axiom of Choice

Proof

technique · direct
1.1F1F2

Writing Δk:=Bkh−B(k−1)h for k=1,…,2n, [F1] and [F2] give EΔk2=h and EΔk4=3h2, so the centered variables Yk:=Δk2−h satisfy EYk=0 and Var⁡(Yk)=EΔk4−(EΔk2)2=3h2−h2=2h2.

2.1step 1.1F1

Qn−T=∑k=12nYk has mean 0, and [F1] makes the Yk independent, so Var⁡(Qn−T)=∑kVar⁡(Yk)=2n⋅2(T/2n)2=2T2/2n; hence E(Qn−T)2=2T2/2n→0 and Qn→T in L2.

3.1step 2.1F3F4

For every ε>0, [F3] gives P(∣Qn−T∣≥ε)≤Var⁡(Qn−T)/ε2=2T2/(2nε2), which is summable in n; applying [F4] to Gn={∣Qn−T∣≥1m} for each m≥1 and intersecting the resulting probability-one events over m shows that almost surely Qn→T.

4.1step 2.1step 3.1F5F6given∎

The degeneracies are covered: T>0 is required, so h>0 and the sums are nonempty with 2n≥2 terms; the partition sequence is the one named in [F5], with mesh T/2n→0 and with consecutive refinements πn⊆πn+1, so no ambiguity of convention arises at t=T, where the step and partial-increment conventions coincide by Quadratic variation along a partition sequence; and AC enters only through [F6].

Source notes

Lawler, Theorems 2.8.1 and 2.8.2, proves the mean-square convergence of the dyadic quadratic sums and their almost-sure convergence along meshes whose sizes are summable (here T/2n). The computation above is the direct one: the second and fourth Gaussian moments of the increments give Var⁡(Qn−T)=2T2/2n, Chebyshev gives summable error probabilities, and Borel-Cantelli upgrades to almost-sure convergence.

Depends on

Used by

Dependency tree · two levels

27 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