σ-Algebra Helpers for AEStronglyMeasurable

This file provides helper lemmas for establishing AEStronglyMeasurable with respect to infima of σ-algebras and limits of sequences. These are useful for working with tail σ-algebras and reverse martingales.

Main results

• aestronglyMeasurable_iInf_antitone: AEStronglyMeasurable is preserved under infimum of antitone σ-algebras
• aestronglyMeasurable_sub_of_tendsto_ae: AEStronglyMeasurable for sub-σ-algebras is preserved under a.e. pointwise limits

References

• Kallenberg (2005), Foundations of Modern Probability, for general treatment

Lemma: AEStronglyMeasurable for infimum of σ-algebras

For real-valued functions, if f is AEStronglyMeasurable with respect to each σ-algebra in an antitone (decreasing) sequence, then f is AEStronglyMeasurable with respect to their infimum.

Mathematical justification:

1. For each N, we have a representative g_N with StronglyMeasurable[m N] g_N and f =ᵐ[μ] g_N
2. For ℝ-valued functions, StronglyMeasurable ↔ Measurable (via Measurable.stronglyMeasurable)
3. If f is Measurable[m N] for each N, then f is Measurable[⨅ N, m N] (by measurableSet_iInf)
4. Hence f is StronglyMeasurable[⨅ N, m N], giving AEStronglyMeasurable

The technical challenge is constructing a common representative from the a.e.-equal witnesses. This is a standard measure-theoretic result that requires infrastructure not readily available in current mathlib (dealing with representatives that differ on null sets for different σ-algebras).

References:

• Kallenberg (2005), Foundations of Modern Probability, for general treatment
• The result follows from properties of L² projections onto closed subspaces

theorem aestronglyMeasurable_iInf_antitone {α : Type u_1} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {m : ℕ → MeasurableSpace α} (h_anti : Antitone m) (_h_le : ∀ (N : ℕ), m N ≤ m₀) (f : α → ℝ) (hf : ∀ (N : ℕ), MeasureTheory.AEStronglyMeasurable f μ) : MeasureTheory.AEStronglyMeasurable f μ

theorem aestronglyMeasurable_sub_of_tendsto_ae {α : Type u_1} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {m : MeasurableSpace α} (_hm : m ≤ m₀) {f : ℕ → α → ℝ} {g : α → ℝ} (hf_meas : ∀ (n : ℕ), Measurable (f n)) (hlim : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds (g x))) : MeasureTheory.AEStronglyMeasurable g μ

AEStronglyMeasurable for a sub-σ-algebra is preserved under a.e. pointwise limits.

If f n are all Measurable[m] where m ≤ m₀, and f n → g a.e. (wrt a measure on m₀), then g is AEStronglyMeasurable[m] (with the witness being the limsup, which is Measurable[m]).

This is the key lemma for "closedness" of L²[m] under L² limits: we extract an a.e.-convergent subsequence and apply this.