birkhoffSum_of_comp_eq — Mathlib

English

If φ ∘ f = φ (i.e., φ is invariant under f), then for all n ∈ ℕ and x ∈ α, birkhoffSum f φ n x = n · φ(x).

Русский

Если φ ∘ f = φ, то для всех n ∈ ℕ и x ∈ α сумма Биркхоффа равна n · φ(x).

LaTeX

$$$\\mathrm{birkhoffSum}(f,\\varphi,n,x)=n\\cdot \\varphi(x)$$$

Lean4

/-- If a function `φ` is invariant under a function `f` (i.e., `φ ∘ f = φ`), then the Birkhoff sum
of `φ` over `f` for `n` iterations is equal to `n • φ`. -/
theorem birkhoffSum_of_comp_eq {f : α → α} {φ : α → M} (h : φ ∘ f = φ) (n : ℕ) : birkhoffSum f φ n = n • φ :=
  by
  funext x
  suffices ∀ k, φ (f^[k] x) = φ x by simp [birkhoffSum, this]
  intro k
  exact congrFun (iterate_invariant h k) x

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