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.
Product martingale from independent mean one factors
Example
Assume AC. For given independent real integrable with , the products and form a martingale for and . Factors may be signed.
Facts & Assumptions
Given: The hypotheses and conventions in the example.
Generated sigma-algebras exist and are minimal. Nonempty intersections of sigma-algebras are sigma-algebras, so the generated sigma-algebra exists and is minimal.
Finite real arithmetic preserves measurability. Arithmetic and lattice operations preserve measurability whenever they are defined.
Finite products of integrable functions of independent variables are integrable, and expectations factor. Expectations factor over finite products of independent random variables.
The sigma-algebra of a finite past is independent of the next variable sigma-algebra. Disjoint groups of an independent sigma-algebra family remain independent.
An integrable variable independent of a sigma-algebra has constant conditional mean equal to its expectation. Conditioning a known variable and an independent variable.
A finite measurable factor may be taken out when its product with the integrable input is integrable. Taking out what is known.
AC supplies the inherited conditional-expectation existence and any stated choice of versions. The Axiom of Choice.
Verification
The generated finite-history sigma-algebras form a filtration; finite products are adapted. Apply factorization to the Borel functions to get for ; at it equals one. Group independence separates from the finite past, so (also for the trivial past at zero).
The variable is finite and -measurable. Both and are integrable by step 1.1. The unbounded taking-out clause therefore gives . This proves the martingale assertion Martingale submartingale and supermartingale. AC is inherited from CE; neither positivity nor identical distribution of factors was used. If one adjoins the deterministic factor , the displayed filtration is exactly the natural filtration of the resulting zero-based factor process Natural filtration of a process, not necessarily that of the products.
For example take with four equal masses, let be its coordinates and for . Each first factor has mean and absolute mean ; coordinate rectangle counting proves independence. The four values of are , so and . Conditional on the product averages , and conditional on it averages .
Depends on
- Martingale submartingale and supermartingale
- Natural filtration of a process
- Nonempty intersections of sigma-algebras are sigma-algebras, so the generated sigma-algebra exists and is minimal
- Expectations factor over finite products of independent random variables
- Disjoint groups of an independent sigma-algebra family remain independent
- Conditioning a known variable and an independent variable
- Taking out what is known
- Arithmetic and lattice operations preserve measurability whenever they are defined
- The Axiom of Choice
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
32 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)