Martingale convergence theorems

Lévy's downward theorem for conditional expectations along a decreasing filtration.

This is the flagship of the reverse-martingale infrastructure: the finite-horizon reversal (Martingale/Reverse.lean), the pathwise crossing adapters (Martingale/Crossings/), the reverse-martingale upcrossing bound (Crossings/Bounds.lean), and the antitone-limit existence result (Martingale/AntitoneLimit.lean) all feed into tendsto_ae_condExp_iInf.

Main results

• tendsto_ae_condExp_iInf: Lévy's downward theorem — for antitone 𝔽, the sequence μ[f | 𝔽 n] converges a.e. to μ[f | ⨅ n, 𝔽 n] (the reverse-martingale limit), spelled in the Mathlib convergence-API grammar (conclusion-first).
• tendsto_eLpNorm_condExp_iInf: the L¹ form of the same theorem — the convergence also holds in L¹, i.e. eLpNorm (μ[f | 𝔽 n] - μ[f | ⨅ n, 𝔽 n]) 1 μ → 0, the form most downstream analytic uses want; it mirrors Mathlib's upward MeasureTheory.tendsto_eLpNorm_condExp.
• MemLp.tendsto_eLpNorm_condExp_iInf: the Lᵖ form — for f ∈ Lᵖ with p < ∞, the convergence holds in Lᵖ.
• measure_inter_eq_mul_of_forall_zero_or_one_iInf: factorization along a decreasing filtration with μ-trivial intersection — if B' n is 𝔽 n-measurable with μ (B' n) and μ (A ∩ B' n) independent of n, then μ (A ∩ B) = μ A * μ B.
• condExp_inter_ae_eq_mul_iInf: the conditional form of this factorization, for an arbitrary tail — if the tail-conditional expectations of the indicators of B' n and A ∩ B' n do not depend on n, then the corresponding conditional expectations for A and B factorize.

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

The downward theorems are adapted from cameronfreer/exchangeability (Probability/Martingale/Convergence.lean, pin e0532e59ceff23edab44dda9ab0655debbc9cc22). The filtration factorization adapts the private Lévy-downward factorization step of Graphon/RelRestrictionIndependence.lean in cameronfreer/graphon (Apache 2.0) at commit 175911f9d2e053f2a33d966658dfce0e4ae2811d.

theorem MeasureTheory.tendsto_ae_condExp_iInf {Ω : Type u_1} [MeasurableSpace Ω] {μ : Measure Ω} [IsFiniteMeasure μ] {𝔽 : ℕ → MeasurableSpace Ω} (h_filtration : Antitone 𝔽) (h_le0 : 𝔽 0 ≤ inferInstance) (f : Ω → ℝ) : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => μ[f | 𝔽 n] ω) Filter.atTop (nhds (μ[f | ⨅ (n : ℕ), 𝔽 n] ω))

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

For a decreasing filtration 𝔽ₙ, the sequence μ[f | 𝔽ₙ] converges almost surely to μ[f | ⨅ₙ 𝔽ₙ] — the reverse-martingale (Lévy downward) limit. As in Mathlib's upward MeasureTheory.tendsto_ae_condExp, no integrability hypothesis is needed: condExp vanishes on non-integrable arguments, so the statement is trivial there.

theorem MeasureTheory.tendsto_eLpNorm_condExp_iInf {Ω : Type u_1} [MeasurableSpace Ω] {μ : Measure Ω} [IsFiniteMeasure μ] {𝔽 : ℕ → MeasurableSpace Ω} (h_filtration : Antitone 𝔽) (h_le0 : 𝔽 0 ≤ inferInstance) (f : Ω → ℝ) : Filter.Tendsto (fun (n : ℕ) => eLpNorm (μ[f | 𝔽 n] - μ[f | ⨅ (n : ℕ), 𝔽 n]) 1 μ) Filter.atTop (nhds 0)

Conditional expectation converges in L¹ along a decreasing filtration (Lévy's downward theorem, L¹ form).

For a decreasing filtration 𝔽ₙ, the sequence μ[f | 𝔽ₙ] converges in L¹ to μ[f | ⨅ₙ 𝔽ₙ]. This upgrades the almost-everywhere statement tendsto_ae_condExp_iInf: the conditional expectations μ[f | 𝔽ₙ] of a fixed integrable function form a uniformly integrable family, so their a.e. convergence is convergence in L¹ by Vitali's theorem. As in Mathlib's upward MeasureTheory.tendsto_eLpNorm_condExp, which this is the downward analogue of, no integrability hypothesis is needed: condExp vanishes on non-integrable arguments, so the statement is trivial there.

theorem MeasureTheory.MemLp.tendsto_eLpNorm_condExp_iInf {Ω : Type u_1} [MeasurableSpace Ω] {μ : Measure Ω} [IsFiniteMeasure μ] {𝔽 : ℕ → MeasurableSpace Ω} (h_filtration : Antitone 𝔽) (h_le0 : 𝔽 0 ≤ inferInstance) {p : ENNReal} (hp : p ≠ ⊤) {f : Ω → ℝ} (hf : MemLp f p μ) : Filter.Tendsto (fun (n : ℕ) => eLpNorm (μ[f | 𝔽 n] - μ[f | ⨅ (n : ℕ), 𝔽 n]) p μ) Filter.atTop (nhds 0)

Conditional expectation converges in Lᵖ along a decreasing filtration (Lévy's downward theorem, Lᵖ form).

For a decreasing filtration 𝔽ₙ, a finite exponent p and f ∈ Lᵖ, the sequence μ[f | 𝔽ₙ] converges in Lᵖ to μ[f | ⨅ₙ 𝔽ₙ]. For p = 1 the integrability hypothesis is superfluous; see tendsto_eLpNorm_condExp_iInf.

theorem MeasureTheory.measure_inter_eq_mul_of_forall_zero_or_one_iInf {Ω : Type u_1} [MeasurableSpace Ω] {μ : Measure Ω} {𝔽 : ℕ → MeasurableSpace Ω} (hanti : Antitone 𝔽) (h𝔽 : 𝔽 0 ≤ inst✝) (htriv : ∀ (s : Set Ω), MeasurableSet s → μ s = 0 ∨ μ s = 1) {A B : Set Ω} (hA : MeasurableSet A) {B' : ℕ → Set Ω} (hB' : ∀ (n : ℕ), MeasurableSet (B' n)) (hBmass : ∀ (n : ℕ), μ (B' n) = μ B) (hjoint : ∀ (n : ℕ), μ (A ∩ B' n) = μ (A ∩ B)) : μ (A ∩ B) = μ A * μ B

Factorization along a decreasing filtration with trivial tail. If B' n is 𝔽 n-measurable along an antitone sequence of sub-σ-algebras whose intersection is μ-trivial, and neither μ (B' n) nor μ (A ∩ B' n) depends on n, then μ (A ∩ B) = μ A * μ B. This is the step that turns tail triviality into independence of events readable far apart.

theorem MeasureTheory.condExp_inter_ae_eq_mul_iInf {Ω : Type u_1} [MeasurableSpace Ω] {μ : Measure Ω} [IsFiniteMeasure μ] {𝔽 : ℕ → MeasurableSpace Ω} (hanti : Antitone 𝔽) (h𝔽 : 𝔽 0 ≤ inst✝) {A B : Set Ω} (hA : MeasurableSet A) {B' : ℕ → Set Ω} (hB' : ∀ (n : ℕ), MeasurableSet (B' n)) (hBmass : ∀ (n : ℕ), μ[(B' n).indicator fun (ω : Ω) => 1 | ⨅ (n : ℕ), 𝔽 n] =ᵐ[μ] μ[B.indicator fun (ω : Ω) => 1 | ⨅ (n : ℕ), 𝔽 n]) (hjoint : ∀ (n : ℕ), μ[(A ∩ B' n).indicator fun (ω : Ω) => 1 | ⨅ (n : ℕ), 𝔽 n] =ᵐ[μ] μ[(A ∩ B).indicator fun (ω : Ω) => 1 | ⨅ (n : ℕ), 𝔽 n]) : μ[(A ∩ B).indicator fun (ω : Ω) => 1 | ⨅ (n : ℕ), 𝔽 n] =ᵐ[μ] μ[A.indicator fun (ω : Ω) => 1 | ⨅ (n : ℕ), 𝔽 n] * μ[B.indicator fun (ω : Ω) => 1 | ⨅ (n : ℕ), 𝔽 n]

Conditional factorization along a decreasing filtration. If B' n is 𝔽 n-measurable and the tail-conditional expectations of the indicators of B' n and A ∩ B' n agree with those of B and A ∩ B, respectively, then the following factorization identity holds almost everywhere: μ⟦A ∩ B | ⨅ n, 𝔽 n⟧ = μ⟦A | ⨅ n, 𝔽 n⟧ * μ⟦B | ⨅ n, 𝔽 n⟧.

This is the conditional form of measure_inter_eq_mul_of_forall_zero_or_one_iInf, and needs no triviality of the tail.