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.
Azuma-Hoeffding inequality
Statement
Assume AC. Let be a martingale. Suppose finite -measurable and deterministic satisfy almost surely. Then for every , and the analogous lower-tail bound holds, with the zero-denominator expression interpreted as .
Facts & Assumptions
Given: The hypotheses, objects, and conventions in the Statement.
Conditional Hoeffding bound for bounded martingale differences controls each conditional exponential moment.
Tower property of conditional expectation iterates those controls through the filtration.
Markov's inequality for random variables supplies the exponential Markov bound.
The Axiom of Choice is inherited from the conditional-expectation and martingale interfaces.
Taking out what is known permits the bounded -measurable accumulated exponential to be taken outside conditional expectation.
Proof
Let and . For , F1, F2, and F5 give The final inequality follows by finite induction, with the empty sum at time .
Markov applied to yields If , the quadratic is minimized at , giving .
If , every . F1's hypotheses then force every almost surely, so the event is empty for , agreeing with the stated convention. Apply step 1.1, step 2.1 to , whose endpoints are , to obtain the lower-tail bound. AC has exactly the inherited role in F4.
Depends on
Used by
- Symmetric bounded-increment Azuma bound Corollary
Dependency tree · two levels
17 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
- Roch, Notes 20: Azuma's Inequality, Theorem 20.8 and proof, pp. 3–4 (standard reference, not scraped)