birkhoffSum_succ — Mathlib

English

For any f,g and n, the Birkhoff sum with n+1 terms satisfies: birkhoffSum f g (n+1) x = birkhoffSum f g n x + g(f^{[n]} x).

Русский

Для любых f,g и n сумма Биркхоффа с n+1 членом равна предыдущей суммы плюс g на следующем элементе орбиты: birkhoffSum(n+1) = birkhoffSum(n) + g(f^{[n]} x).

LaTeX

$$$\mathrm{birkhoffSum}(f,g,n+1,x) = \mathrm{birkhoffSum}(f,g,n,x) + g(f^{[n]} x).$$$

Lean4

theorem birkhoffSum_succ (f : α → α) (g : α → M) (n : ℕ) (x : α) :
    birkhoffSum f g (n + 1) x = birkhoffSum f g n x + g (f^[n] x) :=
  sum_range_succ _ _

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