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.
Second moment is the expected predictable quadratic variation
Statement
Assume AC. For a real square-integrable martingale and every , with all three terms finite. In particular, gives .
Facts & Assumptions
Given: The hypotheses and conventions in the statement.
The square-minus-bracket process is a martingale with initial M0 squared. Square minus predictable quadratic variation is a martingale.
Conditional expectation is linear, order preserving and expectation preserving. Basic algebra and order properties of conditional expectation.
Finite linear combinations remain integrable and their integrals are linear. The Lebesgue integral is linear on .
Assume AC. The Axiom of Choice.
For a square-integrable martingale, predictable quadratic variation is an integrable finite sum of conditional square increments. Predictable quadratic variation in discrete time.
Proof
By [F1], is integrable and for each . Expectation preservation gives . Induction over the finitely many times up to yields , also at . The invocations of F1 and F2 are made under the AC assumption F4.
For the finite integral linearity used here, augment each finite disjoint display of a nonnegative simple function by its zero-coefficient complement. Pairwise intersections of two augmented displays partition the whole space and have equal coefficients on nonempty cells, so finite additivity and prove representation independence. Common refinements give simple addition and monotonicity, while scalar zero is direct and positive scalars are termwise. Supremum over simple minorants, increasing simple approximation and the sets for give monotone convergence and nonnegative additivity. Positive/negative and real/imaginary decompositions then give finite linearity. The square is integrable by the square-integrability hypothesis, and the bracket is integrable by [F5], so this local linearity gives . Rearranging the finite equality from step 1.1 proves the formula. If its second moment is zero. At the bracket is zero and the equation reads .
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
20 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)