Invariant measurable representatives

Within the ambient-almost-everywhere strongly measurable real-valued functions, this file identifies almost-everywhere invariance under a nonsingular endomorphism with almost-everywhere strong measurability for Mathlib's invariant σ-algebra.

The nontrivial direction replaces an almost invariant real-valued function by a pointwise invariant representative. For an ambient-measurable representative g, the replacement is the real part of

limsup (fun n => g (T^[n] ω)).

Dropping the first term does not change this limsup, so the replacement is pointwise invariant. Nonsingularity transports the original a.e. invariance along every iterate, making the replacement a.e. equal to g.

Main results

• aestronglyMeasurable_invariants_of_comp_ae_eq — an ambient-a.e. strongly measurable, a.e. invariant function has an invariant measurable representative;
• aestronglyMeasurable_invariants_iff_comp_ae_eq — the characteristic equivalence;
• fixedSpace_eq_lpMeas_invariants — the Lᵖ fixed space is exactly Mathlib's lpMeas subspace for the invariant σ-algebra.

The construction and proof are adapted from cameronfreer/exchangeability, Exchangeability/Ergodic/ShiftInvariantRepresentatives.lean and Exchangeability/Ergodic/InvariantSigma.lean, at commit e0532e59ceff23edab44dda9ab0655debbc9cc22. This version is generalized from the path-space shift to an arbitrary nonsingular endomorphism at the function level (and a measure-preserving one on Lᵖ) and uses MeasurableSpace.invariants directly, as required by the Exchangeability roadmap.

Invariant representatives

theorem TauCeti.Probability.aestronglyMeasurable_invariants_of_comp_ae_eq {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {T : Ω → Ω} (hT : MeasureTheory.Measure.QuasiMeasurePreserving T μ μ) {f : Ω → ℝ} (hf : MeasureTheory.AEStronglyMeasurable f μ) (hfix : f ∘ T =ᵐ[μ] f) : MeasureTheory.AEStronglyMeasurable f μ

An ambient-almost-everywhere strongly measurable, almost-everywhere invariant real-valued function has a representative measurable for Mathlib's invariant σ-algebra.

The nonsingular endomorphism is arbitrary: path-space shift is the specialization used by the Koopman route to de Finetti's theorem.

theorem TauCeti.Probability.AEStronglyMeasurable.comp_ae_eq_of_invariants {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {T : Ω → Ω} {E : Type u_2} [TopologicalSpace E] [TopologicalSpace.PseudoMetrizableSpace E] [MeasurableSpace E] [BorelSpace E] [MeasurableSingletonClass E] (hT : MeasureTheory.Measure.QuasiMeasurePreserving T μ μ) {f : Ω → E} (hf : MeasureTheory.AEStronglyMeasurable f μ) : f ∘ T =ᵐ[μ] f

A function almost-everywhere strongly measurable for the invariant σ-algebra is almost everywhere fixed by composition.

@[simp]

theorem TauCeti.Probability.aestronglyMeasurable_invariants_iff_comp_ae_eq {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {T : Ω → Ω} (hT : MeasureTheory.Measure.QuasiMeasurePreserving T μ μ) {f : Ω → ℝ} (hf : MeasureTheory.AEStronglyMeasurable f μ) : MeasureTheory.AEStronglyMeasurable f μ ↔ f ∘ T =ᵐ[μ] f

Within the ambient-almost-everywhere strongly measurable real-valued functions, almost-everywhere strong measurability for the invariant σ-algebra is equivalent to almost-everywhere invariance under composition.

The invariant subspace of Lᵖ

theorem TauCeti.Probability.mem_fixedSpace_iff_aestronglyMeasurable_invariants {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {p : ENNReal} {T : Ω → Ω} (hT : MeasureTheory.MeasurePreserving T μ μ) (f : ↥(MeasureTheory.Lp ℝ p μ)) : f ∈ fixedSpace T hT ↔ MeasureTheory.AEStronglyMeasurable (↑↑f) μ

Membership in the Lᵖ fixed space is equivalent to almost-everywhere strong measurability for the invariant σ-algebra.

theorem TauCeti.Probability.fixedSpace_eq_lpMeas_invariants {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {p : ENNReal} (T : Ω → Ω) (hT : MeasureTheory.MeasurePreserving T μ μ) : fixedSpace T hT = MeasureTheory.lpMeas ℝ ℝ (MeasurableSpace.invariants T) p μ

The Lᵖ fixed space of a measure-preserving endomorphism is the subspace of functions almost-everywhere strongly measurable for its invariant σ-algebra.