σ-algebra helpers for AEStronglyMeasurable

A helper lemma for establishing AEStronglyMeasurable with respect to the infimum of an antitone sequence of σ-algebras, used when working with tail σ-algebras and reverse martingales.

Main results

• aestronglyMeasurable_of_tendsto_ae': an a.e. pointwise limit of AEStronglyMeasurable[m] functions is AEStronglyMeasurable[m], for an arbitrary measurable space m on α, unrelated to the measure's ambient σ-algebra m₀ (Mathlib's aestronglyMeasurable_of_tendsto_ae covers only the m = m₀ case).
• aestronglyMeasurable_iInf_of_antitone: if a function is AEStronglyMeasurable with respect to each σ-algebra in an antitone sequence, then it is AEStronglyMeasurable with respect to their infimum.
• aestronglyMeasurable_iInf_of_tendsto_ae_antitone: an a.e. limit of a sequence adapted to an antitone family 𝔽 is AEStronglyMeasurable[⨅ n, 𝔽 n].

The result holds for a codomain in any second-countable conditionally complete linear order with the order topology and Borel σ-algebra (ℝ qualifies). The witness σ-algebras m N need not be related to the measure's ambient σ-algebra m₀.

Adapted from cameronfreer/exchangeability (Probability/SigmaAlgebraHelpers.lean, pin e0532e59ceff23edab44dda9ab0655debbc9cc22); the two a.e.-limit lemmas (aestronglyMeasurable_of_tendsto_ae', aestronglyMeasurable_iInf_of_tendsto_ae_antitone) are adapted from the same source. These general-m / antitone statements have no Mathlib equivalent. Written Mathlib-shaped for eventual upstreaming.

theorem TauCeti.MeasureTheory.aestronglyMeasurable_iInf_of_antitone {β : Type u_1} [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] [SecondCountableTopology β] [TopologicalSpace.PseudoMetrizableSpace β] [MeasurableSpace β] [BorelSpace β] {α : Type u_2} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {m : ℕ → MeasurableSpace α} (h_anti : Antitone m) (f : α → β) (hf : ∀ (N : ℕ), MeasureTheory.AEStronglyMeasurable f μ) : MeasureTheory.AEStronglyMeasurable f μ

AEStronglyMeasurable for the infimum of an antitone sequence of σ-algebras.

If f is AEStronglyMeasurable with respect to each σ-algebra in an antitone (decreasing) sequence, then f is AEStronglyMeasurable with respect to their infimum.

theorem TauCeti.MeasureTheory.aestronglyMeasurable_of_tendsto_ae' {β : Type u_1} [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] [SecondCountableTopology β] [TopologicalSpace.PseudoMetrizableSpace β] [MeasurableSpace β] [BorelSpace β] {α : Type u_2} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {m : MeasurableSpace α} {f : ℕ → α → β} {g : α → β} (hf : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ) (hlim : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds (g x))) : MeasureTheory.AEStronglyMeasurable g μ

A.e. pointwise limit of AEStronglyMeasurable[m] functions is AEStronglyMeasurable[m], for an arbitrary measurable space m on α (no assumed relation to the measure's ambient σ-algebra m₀). Mathlib's aestronglyMeasurable_of_tendsto_ae covers only the m = m₀ case.

theorem TauCeti.MeasureTheory.aestronglyMeasurable_iInf_of_tendsto_ae_antitone {β : Type u_1} [ConditionallyCompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] [SecondCountableTopology β] [TopologicalSpace.PseudoMetrizableSpace β] [MeasurableSpace β] [BorelSpace β] {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {𝔽 : ℕ → MeasurableSpace Ω} (h_antitone : Antitone 𝔽) {g : ℕ → Ω → β} {Xlim : Ω → β} (hg_meas : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (g n) μ) (h_tendsto : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => g n ω) Filter.atTop (nhds (Xlim ω))) : MeasureTheory.AEStronglyMeasurable Xlim μ

A.e. limit of an adapted antitone sequence is ⨅ n, 𝔽 n-AEStronglyMeasurable.

For antitone 𝔽, if each g n is 𝔽 n-a.e.-strongly-measurable and g n → Xlim a.e., then Xlim is AEStronglyMeasurable[⨅ n, 𝔽 n]. Codomain β at the same order level as the rest of this section (ℝ qualifies).