English
For all f: α→α and g: α→G, the difference between the n-th Birkhoff sum at f x and at x equals g(f^[n] x) − g(x): birkhoffSum f g n (f x) - birkhoffSum f g n x = g (f^[n] x) - g x.
Русский
Разность между n-й суммой Биркхоффа на точке f x и на x равна g(f^[n] x) − g(x).
LaTeX
$$$\\mathrm{birkhoffSum}(f,g,n,f x)-\\mathrm{birkhoffSum}(f,g,n,x)=g(f^{[n]}x)-g(x)$$$
Lean4
/-- Birkhoff sum is "almost invariant" under `f`:
the difference between `birkhoffSum f g n (f x)` and `birkhoffSum f g n x`
is equal to `g (f^[n] x) - g x`. -/
theorem birkhoffSum_apply_sub_birkhoffSum (f : α → α) (g : α → G) (n : ℕ) (x : α) :
birkhoffSum f g n (f x) - birkhoffSum f g n x = g (f^[n] x) - g x := by
rw [← sub_eq_iff_eq_add.2 (birkhoffSum_succ f g n x), ← sub_eq_iff_eq_add.2 (birkhoffSum_succ' f g n x), ← sub_add, ←
sub_add, sub_add_comm]
