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.
Optional sampling for bounded stopping times
Statement
Assume AC. If is a martingale and are stopping times bounded by a deterministic , then so . For a submartingale the conditional and expectation inequalities point upward; for a supermartingale they point downward.
Facts & Assumptions
Given: The hypotheses, objects, and conventions in the Statement.
Sigma-algebra at a stopping time gives the events usable in conditional testing.
A stopped random variable is measurable at the stopping time gives the required measurability of stopped values.
Bounded predictable transforms preserve martingales gives zero expected martingale transforms. Nonnegative predictable transforms preserve submartingale gains gives the upward sign for submartingales and nonnegative holdings; applying it to gives the downward sign for supermartingales.
Conditional expectation as an ae class identifies a conditional expectation from all event integrals.
The Axiom of Choice supplies conditional-expectation representatives.
Proof
Put for . Both and lie in , so is nonnegative, bounded, and predictable. On the probability-one event , the finite pathwise telescope is The integral identities below use this almost-sure equality; no equality is asserted on a null outcome with .
Fix . On , ; hence and the first factor on the right is -measurable by F1. Thus is another bounded nonnegative predictable process.
Apply F3's one-step conditional calculation and sum: for a submartingale, for a martingale equality holds, and for a supermartingale the inequality reverses. Almost-sure boundedness identifies every stopped value almost surely with a finite sum of integrable variables, while F2 gives -measurability of . F4 therefore identifies the stated conditional relation. Taking gives the expectation relation. AC has exactly the role in F5.
Depends on
Used by
Dependency tree · two levels
21 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
- van der Vaart, Martingales, Diffusions and Financial Mathematics, Theorem 2.42 and proof, pp. 21–22 (standard reference, not scraped)