birkhoffSum_ae_eq_of_ae_eq — Mathlib

English

If φ =ᵐ[μ] ψ (a.e. equal observables), then for every n, birkhoffSum f φ n =ᵐ[μ] birkhoffSum f ψ n.

Русский

Если наблюдаемые φ и ψ равны почти повсюду, то для каждого n сумма Биркхоффа по φ равна почти повсюду сумме по ψ.

LaTeX

$$$\\mathrm{birkhoffSum}(f,\\varphi,n)=^{\\mu}\\mathrm{birkhoffSum}(f,\\psi,n)$$$

Lean4

/-- If observables  `φ` and `ψ` are `μ`-a.e. equal then the corresponding `birkhoffSum` are
`μ`-a.e. equal. -/
theorem birkhoffSum_ae_eq_of_ae_eq (hf : QuasiMeasurePreserving f μ μ) (hφ : φ =ᵐ[μ] ψ) n :
    birkhoffSum f φ n =ᵐ[μ] birkhoffSum f ψ n :=
  by
  apply Eventually.mono _ (fun _ => Finset.sum_congr rfl)
  apply ae_all_iff.mpr (fun i => ?_)
  exact (hf.iterate i).ae (hφ.mono (fun _ h _ => h))

Похожие утверждения