Antitone-filtration limit existence #
Reverse-martingale infrastructure: a.e. existence of the limit of μ[f | 𝔽 n] along an antitone
filtration. Identifying this limit as μ[f | ⨅ n, 𝔽 n] (Lévy's downward theorem) is a forthcoming
Layer-4 result that will consume this existence lemma.
Main results #
exists_integrable_tendsto_ae_condExp_of_antitone: a.e. limit existence for antitone filtrations.
Adapted from cameronfreer/exchangeability
(Probability/Martingale/Crossings/AntitoneLimit.lean, pin
e0532e59ceff23edab44dda9ab0655debbc9cc22). Written Mathlib-shaped for eventual upstreaming.
theorem
MeasureTheory.exists_integrable_tendsto_ae_condExp_of_antitone
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : Measure Ω}
[IsFiniteMeasure μ]
{𝔽 : ℕ → MeasurableSpace Ω}
(h_antitone : Antitone 𝔽)
(h_le : ∀ (n : ℕ), 𝔽 n ≤ inferInstance)
(f : Ω → ℝ)
(hf : Integrable f μ)
:
∃ (Xlim : Ω → ℝ),
Integrable Xlim μ ∧ ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => μ[f | 𝔽 n] ω) Filter.atTop (nhds (Xlim ω))
A.S. existence of the limit of μ[f | 𝔽 n] for integrable f along an antitone filtration —
the L¹ reverse-martingale (Lévy downward) limit.