birkhoffAverage_ae_eq_of_ae_eq — Mathlib

English

If φ =ᵐ[μ] ψ, then for every n, birkhoffAverage R f φ n =ᵐ[μ] birkhoffAverage R f ψ n.

Русский

Если φ =ᵐ[μ] ψ, то для каждого n верно birkhoffAverage R f φ n =ᵐ[μ] birkhoffAverage R f ψ n.

LaTeX

$$$\\mathrm{birkhoffAverage}(R,f,φ,n)=^{\\mu}\\mathrm{birkhoffAverage}(R,f,ψ,n)$$$

Lean4

/-- If observables `φ` and `ψ` are `μ`-a.e. equal then the corresponding `birkhoffAverage` are
 `μ`-a.e. equal. -/
theorem birkhoffAverage_ae_eq_of_ae_eq (R : Type*) [DivisionSemiring R] [Module R M] (hf : QuasiMeasurePreserving f μ μ)
    (hφ : φ =ᵐ[μ] ψ) n : birkhoffAverage R f φ n =ᵐ[μ] birkhoffAverage R f ψ n :=
  EventuallyEq.const_smul (birkhoffSum_ae_eq_of_ae_eq hf hφ n) (n : R)⁻¹

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