Birkhoff sum and average for quasi-measure-preserving maps

Given a map f and measure μ, under the assumption of QuasiMeasurePreserving f μ μ we prove:

• birkhoffSum_ae_eq_of_ae_eq: if observables φ and ψ are μ-a.e. equal then the corresponding birkhoffSum f are μ-a.e. equal.

• birkhoffAverage_ae_eq_of_ae_eq: if observables φ and ψ are μ-a.e. equal then the corresponding birkhoffAverage R f are μ-a.e. equal.

theorem MeasureTheory.QuasiMeasurePreserving.birkhoffSum_ae_eq_of_ae_eq {α : Type u_1} {M : Type u_2} [MeasurableSpace α] [AddCommMonoid M] {f : α → α} {μ : Measure α} {φ ψ : α → M} (hf : QuasiMeasurePreserving f μ μ) (hφ : φ =ᵐ[μ] ψ) (n : ℕ) : birkhoffSum f φ n =ᵐ[μ] birkhoffSum f ψ n

If observables φ and ψ are μ-a.e. equal then the corresponding birkhoffSum are μ-a.e. equal.

theorem MeasureTheory.QuasiMeasurePreserving.birkhoffAverage_ae_eq_of_ae_eq {α : Type u_1} {M : Type u_2} [MeasurableSpace α] [AddCommMonoid M] {f : α → α} {μ : Measure α} {φ ψ : α → M} (R : Type u_3) [DivisionSemiring R] [Module R M] (hf : QuasiMeasurePreserving f μ μ) (hφ : φ =ᵐ[μ] ψ) (n : ℕ) : birkhoffAverage R f φ n =ᵐ[μ] birkhoffAverage R f ψ n

If observables φ and ψ are μ-a.e. equal then the corresponding birkhoffAverage are μ-a.e. equal.

@[deprecated MeasureTheory.QuasiMeasurePreserving.birkhoffSum_ae_eq_of_ae_eq (since := "2026-09-23")]

theorem MeasureTheory.Measure.QuasiMeasurePreserving.birkhoffSum_ae_eq_of_ae_eq {α : Type u_1} {M : Type u_2} [MeasurableSpace α] [AddCommMonoid M] {f : α → α} {μ : Measure α} {φ ψ : α → M} (hf : QuasiMeasurePreserving f μ μ) (hφ : φ =ᵐ[μ] ψ) (n : ℕ) : birkhoffSum f φ n =ᵐ[μ] birkhoffSum f ψ n

Alias of MeasureTheory.QuasiMeasurePreserving.birkhoffSum_ae_eq_of_ae_eq.

---

If observables φ and ψ are μ-a.e. equal then the corresponding birkhoffSum are μ-a.e. equal.

@[deprecated MeasureTheory.QuasiMeasurePreserving.birkhoffAverage_ae_eq_of_ae_eq (since := "2026-09-23")]

theorem MeasureTheory.Measure.QuasiMeasurePreserving.birkhoffAverage_ae_eq_of_ae_eq {α : Type u_1} {M : Type u_2} [MeasurableSpace α] [AddCommMonoid M] {f : α → α} {μ : Measure α} {φ ψ : α → M} (R : Type u_3) [DivisionSemiring R] [Module R M] (hf : QuasiMeasurePreserving f μ μ) (hφ : φ =ᵐ[μ] ψ) (n : ℕ) : birkhoffAverage R f φ n =ᵐ[μ] birkhoffAverage R f ψ n

Alias of MeasureTheory.QuasiMeasurePreserving.birkhoffAverage_ae_eq_of_ae_eq.

---

If observables φ and ψ are μ-a.e. equal then the corresponding birkhoffAverage are μ-a.e. equal.