birkhoffAverage_eq — Mathlib

English

If f : α → α and x is a fixed point of f (f(x) = x), then for any g: α → M and any n ≠ 0, birkhoffAverage_R f g n x = g(x).

Русский

Если x фиксирована точка при f, то среднее Биркхоффа на орбите через n шагов равняется значению g в x.

LaTeX

$$$\text{If } h\colon f(x)=x,\; \forall n\neq 0:\quad birkhoffAverage(R,f,g,n,x)=g(x).$$$

Lean4

theorem birkhoffAverage_eq [CharZero R] {f : α → α} {x : α} (h : IsFixedPt f x) (g : α → M) {n : ℕ} (hn : n ≠ 0) :
    birkhoffAverage R f g n x = g x :=
  by
  rw [birkhoffAverage, h.birkhoffSum_eq, ← Nat.cast_smul_eq_nsmul R, inv_smul_smul₀]
  rwa [Nat.cast_ne_zero]

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