Martingale Convergence Theorems

The two key results: Lévy's upward and downward theorems for conditional expectations.

Main Results

• condExp_tendsto_iInf: Lévy downward theorem (decreasing filtration)

References

• Kallenberg, Probabilistic Symmetries and Invariance Principles (2005), Section 1
• Durrett, Probability: Theory and Examples (2019), Section 5.5
• Williams, Probability with Martingales (1991), Theorem 12.12

theorem Exchangeability.Probability.condExp_tendsto_iInf {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {𝔽 : ℕ → MeasurableSpace Ω} (h_filtration : Antitone 𝔽) (h_le : ∀ (n : ℕ), 𝔽 n ≤ inferInstance) (f : Ω → ℝ) (h_f_int : MeasureTheory.Integrable f μ) : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => μ[f | 𝔽 n] ω) Filter.atTop (nhds (μ[f | ⨅ (n : ℕ), 𝔽 n] ω))

Conditional expectation converges along decreasing filtration (Lévy's downward theorem).

For a decreasing filtration 𝔽ₙ and integrable f, the sequence Mₙ := E[f | 𝔽ₙ] converges a.s. to E[f | ⨅ₙ 𝔽ₙ].

Proof strategy: Use the upcrossing inequality approach:

1. Define upcrossings for interval [a,b]
2. Prove upcrossing inequality: E[# upcrossings] ≤ E[|X₀ - a|] / (b - a)
3. Show: finitely many upcrossings a.e. for all rational [a,b]
4. Deduce: the sequence {E[f | 𝔽 n]} converges a.e.
5. Identify the limit as E[f | ⨅ 𝔽 n] using tower property

Why not use OrderDual reindexing? For antitone F, the supremum ⨆ i : ℕᵒᵈ, F i.ofDual equals F 0 (since F 0 is the largest element of the chain), not ⨅ n, F n. So applying Lévy's upward theorem to the dualised filtration would give convergence to μ[f | F 0], the wrong limit.

Implementation notes

condExp_tendsto_iInf is proved via the chain:

1. revFiltration, revCEFinite: Time-reversal infrastructure (Martingale/Reverse.lean)
2. revCE_martingale: Reversed process is a forward martingale
3. condExp_exists_ae_limit_antitone: A.S. existence via upcrossing bounds (Martingale/Crossings.lean)
4. Integrable.uniformIntegrable_condExp (mathlib): UI of conditional expectations
5. ae_limit_is_condexp_iInf: Limit identification via Vitali convergence + tower
6. condExp_tendsto_iInf: Wraps step 5

Mathlib dependencies: Filtration, condExp_condExp_of_le (tower property). Reverse martingale convergence is not available in mathlib; the chain above proves it locally for the Lévy downward case.