birkhoffSum_eq — Mathlib

English

If x is a fixed point of f (i.e., f(x) = x), then for every observable g: α → M and every n ∈ ℕ, birkhoffSum f g n x = n · g(x).

Русский

Если x является фиксированной точкой функции f (f(x) = x), то для любого наблюдаемого g: α → M и любого n ∈ ℕ выполняется birkhoffSum(f,g,n,x) = n · g(x).

LaTeX

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

Lean4

theorem birkhoffSum_eq {f : α → α} {x : α} (h : IsFixedPt f x) (g : α → M) (n : ℕ) : birkhoffSum f g n x = n • g x := by
  simp [birkhoffSum, (h.iterate _).eq]

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