TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)

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.

Square minus predictable quadratic variation is a martingale

Statement

Assume AC. For every real square-integrable martingale $M$ , the process $Z_{n} = M_{n}^{2} - ⟨ M ⟩_{n}$ is a martingale with $Z_{0} = M_{0}^{2}$ . Also $W_{n} = (M_{n} - M_{0})^{2} - ⟨ M ⟩_{n}$ is a martingale starting at zero. The initial variable $M_{0}$ may be random and need not vanish.

Facts & Assumptions

Given: The hypotheses and conventions in the statement.

[F1]

The bracket is integrable predictable and its increment is the conditional squared martingale increment. Predictable quadratic variation in discrete time.

[F2]

Martingale increments have zero past conditional expectation. Martingales and martingale differences correspond.

[F3]

Square-integrable variables have an integrable product by Cauchy–Schwarz. Cauchy-Schwarz for random variables.

[F4]

A finite measurable factor may be taken out when its product with the integrable input is integrable. Taking out what is known.

[F5]

Conditional expectation is linear, order preserving and expectation preserving. Basic algebra and order properties of conditional expectation.

[F6]

An integrable variable measurable for the conditioning sigma-algebra conditions to itself. Conditioning a known variable and an independent variable.

[F7]

Finite linear combinations remain integrable and their integrals are linear. The Lebesgue integral is linear on $L^{1} (μ)$ .

[F8]

Finite real sums and products are measurable. Arithmetic and lattice operations preserve measurability whenever they are defined.

[F9]

AC supplies the inherited conditional-expectation existence and any stated choice of versions. The Axiom of Choice.

Proof

technique · direct

1.1

Put $D_{n} = M_{n} - M_{n - 1}$ for $n \geq 1$ . It is in $L^{2}$ by $D_{n}^{2} \leq 2 M_{n}^{2} + 2 M_{n - 1}^{2}$ , and its conditional mean given $F_{n - 1}$ is zero. Cauchy–Schwarz gives $E ∣ M_{n - 1} D_{n} ∣ \leq (E M_{n - 1}^{2})^{1 / 2} (E D_{n}^{2})^{1 / 2} < \infty$ . The factor $M_{n - 1}$ is finite and known at time $n - 1$ , so taking-out is legitimate and gives $E [M_{n - 1} D_{n} ∣ F_{n - 1}] = M_{n - 1} E [D_{n} ∣ F_{n - 1}] = 0$ .

givenF2F3F4

2.1

For the finite integral and conditional linearity used here, augment every finite disjoint nonnegative-simple display by its zero-coefficient complement. Intersections of two augmented displays partition the space and carry equal coefficients on nonempty cells, so finite additivity and $0 \cdot (+ \infty) = 0$ prove representation independence. Common refinements give simple addition and monotonicity; scalar zero is direct and positive scalars are termwise. Supremum over simple minorants, increasing simple approximation and the sets ${f_{j} \geq c s}$ for $0 < c < 1$ give monotone convergence and nonnegative additivity. Positive/negative and real/imaginary decompositions give finite $L^{1}$ linearity; substituting these facts at the base validates the event-integral construction and algebra of the cited conditional expectations. The square and bracket are adapted and integrable, hence so is $Z$ . Expand $M_{n}^{2} - M_{n - 1}^{2} = 2 M_{n - 1} D_{n} + D_{n}^{2}$ . Every term is integrable. Conditional linearity and step 1.1 give $E [M_{n}^{2} - M_{n - 1}^{2} ∣ F_{n - 1}] = E [D_{n}^{2} ∣ F_{n - 1}] = ⟨ M ⟩_{n} - ⟨ M ⟩_{n - 1}$ . The last difference is known at time $n - 1$ . Subtracting it and conditioning the known $Z_{n - 1}$ proves $E [Z_{n} ∣ F_{n - 1}] = Z_{n - 1}$ . The initial bracket is zero, so $Z_{0} = M_{0}^{2}$ .

F1F5F6F7F8step 1.1construct

3.1

Set $N_{n} = M_{n} - M_{0}$ . Since $M_{0}$ is $F_{0}$ -measurable, it is known for every $F_{n}$ . Linearity gives $E [N_{n + 1} ∣ F_{n}] = M_{n} - M_{0} = N_{n}$ . Also $N_{n}^{2} \leq 2 M_{n}^{2} + 2 M_{0}^{2}$ is integrable, so $N$ is a square-integrable martingale with $N_{0} = 0$ . Its increments equal $D_{n}$ , hence $⟨ N ⟩ = ⟨ M ⟩$ as classes. Apply the already proved step 2.1 to $N$ to conclude that $W = N^{2} - ⟨ M ⟩$ is a martingale with $W_{0} = 0$ . AC is inherited from CE and bracket version construction; no unproved assertion about the product $M_{0} M_{n}$ is used.

givenF1F5F6F7F8F9step 2.1∎

Depends on

Used by

Dependency tree · two levels

29 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

Durrett, Probability: Theory and Examples, fifth edition (standard reference, not scraped)