English
Let f: α → α, g: α → M with M an AddCommMonoid. For all m, n ∈ ℕ and x ∈ α, the Birkhoff sum over m + n terms equals the sum of the first m terms at x and the next n terms along the orbit starting at f^m(x): b( f, g, m+n, x ) = b( f, g, m, x ) + b( f, g, n, f^[m](x)).
Русский
Пусть f: α → α, g: α → M, где M — аддитивный коммутативный моноид. Для любых m,n ∈ ℕ и x ∈ α сумма Биркхоффа по длине m+n равна сумме первых m слагаемых в точке x плюс сумму следующих n слагаемых вдоль орбиты, начиная с f^m(x): birkhoffSum(f,g,m+n,x) = birkhoffSum(f,g,m,x) + birkhoffSum(f,g,n,f^[m] x).
LaTeX
$$$\\mathrm{birkhoffSum}(f,g,m+n,x)=\\mathrm{birkhoffSum}(f,g,m,x)+\\mathrm{birkhoffSum}(f,g,n,f^{[m]}x)$$$
Lean4
theorem birkhoffSum_add (f : α → α) (g : α → M) (m n : ℕ) (x : α) :
birkhoffSum f g (m + n) x = birkhoffSum f g m x + birkhoffSum f g n (f^[m] x) := by
simp_rw [birkhoffSum, sum_range_add, add_comm m, iterate_add_apply]
