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)
• condExp_tendsto_iSup: Lévy upward theorem (increasing filtration, wraps mathlib)

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? See iSup_ofAntitone_eq_F0: for antitone F, we have ⨆ i, F i.ofDual = F 0, not ⨅ n, F n. Applying Lévy's upward theorem would give convergence to the wrong limit.

theorem Exchangeability.Probability.condExp_tendsto_iSup {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {𝔽 : ℕ → MeasurableSpace Ω} (h_filtration : Monotone 𝔽) (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 increasing filtration (Lévy's upward theorem).

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

Implementation: Direct wrapper around mathlib's MeasureTheory.tendsto_ae_condExp from Mathlib.Probability.Martingale.Convergence.

Implementation Notes

Current Status:

• ✅ condExp_tendsto_iSup (Lévy upward): Complete wrapper around mathlib
• 🚧 condExp_tendsto_iInf (Lévy downward): Structure in place, 3 sorries remain

Proof structure for downward theorem:

1. ✅ revFiltration, revCE: Time-reversal infrastructure for finite horizons
2. ✅ revCE_martingale: Reversed process is a forward martingale
3. 🚧 condExp_exists_ae_limit_antitone: A.S. existence via upcrossing bounds
4. 🚧 uniformIntegrable_condexp_antitone: UI via de la Vallée-Poussin
5. 🚧 ae_limit_is_condexp_iInf: Limit identification via Vitali + tower
6. ✅ condExp_tendsto_iInf: Main theorem (wraps step 5)

Remaining work (3 sorries):

• Upcrossing bounds for reverse martingales (step 3)
• de la Vallée-Poussin + Jensen for UI (step 4)
• Vitali convergence + limit identification (step 5)

See PROOF_PLAN_condExp_tendsto_iInf.md for detailed mathematical strategy.

Dependencies from Mathlib:

• ✅ MeasureTheory.tendsto_ae_condExp: Lévy upward (used)
• ✅ Filtration: Filtration structure (used)
• ✅ condExp_condExp_of_le: Tower property (used)
• ❌ Reverse martingale convergence: Not available (proving it here)
• Future work: Upcrossing inequality, Vitali convergence, de la Vallée-Poussin