Plain-English statement
A continuous square-integrable martingale is controlled uniformly in time by four times its terminal second moment.
Mathematical statement
E[sup_(0<=t<=T) |M_t|^2] <= 4 E[|M_T|^2].
Intuition
Finite Doob control is applied on nested dyadic observation grids; path continuity turns the increasing grid maxima into the full time supremum.
Conditions
- a martingale on the filtration
- almost-everywhere continuous paths
- terminal L2 integrability
- finite horizon
Why these conditions cannot be dropped
- martingality drives the maximal inequality
- continuity makes dyadic observations exhaustive
- terminal L2 integrability makes the bound finite
Proof route
- prove the finite discrete Doob inequality
- sample on each dyadic grid
- show grid maxima increase to the continuous supremum
- pass to the limit by monotone convergence
Lean interface notes
- the constant four is derived rather than assumed
- the theorem feeds the uniform Borel-Cantelli construction
Read the mathematics first, then descend into Lean
You do not need to know Lean before opening this panel. The page keeps the paper-level theorem, rigorous proof obligations, exact Lean declaration, and proof dependencies as separate layers so a first-time reader can move down one layer at a time.
Proof architecture
Start with the tree when learning: prerequisites sit below the theorem and downstream results sit above it. Switch to the network when you want to understand where this declaration lives in the local formal library. Every mapped node is clickable.
Graph rule: only dependencies found by the ASTIS source scan are drawn. Missing tactic indirection is treated as an under-approximation; the site never invents an edge just to make a prettier graph.
How to read the exact Lean declaration
Read a Lean theorem left-to-right exactly as you would unpack a mathematical sentence: name → ambient types → automatically inferred structures → explicit hypotheses → conclusion → proof. Then read the proof top-to-bottom as transformations of the current goal.
- NameWhat reusable mathematical fact is being created?
- ParametersWhich symbols are arbitrary, and which structures are inferred by typeclass search?
- PropositionAfter the colon, translate the Lean expression back into a paper statement.
- Proof actionsAfter
by, ask what each tactic does to the mathematical goal—not only what syntax it uses.
Syntax used on this page
This glossary is filtered to syntax that actually occurs in the declaration above. Open a symbol only when you meet it, rather than memorizing Lean grammar in advance.
Source voice and ASTIS voice stay separate
When Samplinglib shows a short quotation from Chewi, it is labeled as a source excerpt and linked to the canonical book page. Intuition, expanded proof steps, hidden regularity assumptions, and Lean explanations are ASTIS-authored commentary. A quotation never substitutes for a formal proof, and an ASTIS explanation is never attributed to the textbook author.
Lean statement
theorem doobL2_continuous
[IsFiniteMeasure mu] {filtration : Filtration ℝ≥0 m}
{M : ℝ≥0 → Omega → ℝ} (hM : Martingale M filtration mu)
{T : ℝ≥0} (hT : 0 < T)
(hcont : ∀ᵐ omega ∂mu, ContinuousOn (fun t => M t omega) (Icc 0 T))
(a : ℝ) :
ENNReal.ofReal a ^ (2 : ℝ) * mu (continuousExceedEvent M T a) ≤
4 * eLpNorm (M T) 2 mu ^ (2 : ℝ) := by
have hsubset : continuousExceedEvent M T a ≤ᵐ[mu]
dyadicMaxEventAll M T a := by
filter_upwards [hcont] with omega hcontinuous homega
obtain ⟨t, ht, hexceed⟩ := homega
exact continuousOn_mem_dyadicMaxEventAll hT hcontinuous ht hexceed
calc
ENNReal.ofReal a ^ (2 : ℝ) * mu (continuousExceedEvent M T a) ≤
ENNReal.ofReal a ^ (2 : ℝ) * mu (dyadicMaxEventAll M T a) :=
mul_le_mul_of_nonneg_left (MeasureTheory.measure_mono_ae hsubset) bot_le
_ ≤ 4 * eLpNorm (M T) 2 mu ^ (2 : ℝ) :=
pow_mul_measure_dyadicMaxEventAll_le hM T a
end ContinuousDoobL2
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheoryOpen AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ContinuousDoobL2.lean:268published source at 7bcd37294df1