Crossings: Antitone-Filtration Convergence

The reverse-martingale convergence theorem chain, ending in ae_limit_is_condexp_iInf, used by Probability/Martingale/Convergence.lean.

Main Results

• condExp_exists_ae_limit_antitone: A.S. limit existence for antitone filtrations
• ae_limit_is_condexp_iInf: Limit equals condExp w.r.t. intersection σ-algebra

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

A.S. existence of the limit of μ[f | 𝔽 n] along an antitone filtration.

This uses the upcrossing inequality applied to the time-reversed martingales to show that the original sequence has finitely many upcrossings and downcrossings a.e., hence converges a.e.

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

Identification: the a.s. limit equals μ[f | ⨅ n, 𝔽 n].

Uses uniform integrability to pass from a.e. convergence to L¹ convergence, then uses L¹-continuity of conditional expectation to identify the limit.