Birkhoff averages of the Lᵖ composition operator

The Birkhoff sums and averages of the composition (Koopman) operator of a measure-preserving map T on Lᵖ are elements of Lᵖ, while the ergodic theorems a probabilist states are about the pointwise Birkhoff averages birkhoffAverage ℝ T f n of an observable. This file records that the two agree: an Lᵖ Birkhoff average of g is represented by the pointwise Birkhoff average of the coercion ⇑g. For another representative f =ᵐ[μ] ⇑g, compose with Mathlib's Measure.QuasiMeasurePreserving.birkhoffAverage_ae_eq_of_ae_eq.

Main results

• coeFn_iterate_compMeasurePreserving — iterating the composition operator composes with the iterated transformation;
• coeFn_birkhoffSum_compMeasurePreserving and coeFn_birkhoffAverage_compMeasurePreserving — the Birkhoff sums and averages of the composition operator are represented by the pointwise Birkhoff sums and averages of the coercion of the argument.

theorem TauCeti.Probability.coeFn_iterate_compMeasurePreserving {Ω : Type u_1} {E : Type u_2} [MeasurableSpace Ω] [NormedAddCommGroup E] {μ : MeasureTheory.Measure Ω} {p : ENNReal} {T : Ω → Ω} (hT : MeasureTheory.MeasurePreserving T μ μ) (g : ↥(MeasureTheory.Lp E p μ)) (n : ℕ) : ↑↑((⇑(MeasureTheory.Lp.compMeasurePreserving T hT))^[n] g) =ᵐ[μ] ↑↑g ∘ T^[n]

Iterating the Lᵖ composition operator composes with the iterated transformation.

theorem TauCeti.Probability.coeFn_birkhoffSum_compMeasurePreserving {Ω : Type u_1} {E : Type u_2} [MeasurableSpace Ω] [NormedAddCommGroup E] {μ : MeasureTheory.Measure Ω} {p : ENNReal} {T : Ω → Ω} (hT : MeasureTheory.MeasurePreserving T μ μ) (g : ↥(MeasureTheory.Lp E p μ)) (n : ℕ) : ↑↑(birkhoffSum (⇑(MeasureTheory.Lp.compMeasurePreserving T hT)) id n g) =ᵐ[μ] birkhoffSum T (↑↑g) n

The Birkhoff sums of the Lᵖ composition operator are represented by the pointwise Birkhoff sums of the coercion of g.

theorem TauCeti.Probability.coeFn_birkhoffAverage_compMeasurePreserving {Ω : Type u_1} {E : Type u_2} [MeasurableSpace Ω] [NormedAddCommGroup E] {μ : MeasureTheory.Measure Ω} {p : ENNReal} [NormedSpace ℝ E] {T : Ω → Ω} (hT : MeasureTheory.MeasurePreserving T μ μ) (g : ↥(MeasureTheory.Lp E p μ)) (n : ℕ) : ↑↑(birkhoffAverage ℝ (⇑(MeasureTheory.Lp.compMeasurePreserving T hT)) id n g) =ᵐ[μ] birkhoffAverage ℝ T (↑↑g) n

The Birkhoff averages of the Lᵖ composition operator are represented by the pointwise Birkhoff averages of the coercion of g.