English
An alternative naming for the zero-average property, birkhoffAverage_zero' holds: birkhoffAverage R f g 0 = 0.
Русский
Альтернативное наименование нулевого среднего: birkhoffAverage_zero' утверждает birkhoffAverage R f g 0 = 0.
LaTeX
$$$\mathrm{birkhoffAverage}(R,f,g,0) = 0.$$$
Lean4
/-- Birkhoff average is "almost invariant" under `f`:
the difference between `birkhoffAverage R f g n (f x)` and `birkhoffAverage R f g n x`
is equal to `(n : R)⁻¹ • (g (f^[n] x) - g x)`. -/
theorem birkhoffAverage_apply_sub_birkhoffAverage (f : α → α) (g : α → M) (n : ℕ) (x : α) :
birkhoffAverage R f g n (f x) - birkhoffAverage R f g n x = (n : R)⁻¹ • (g (f^[n] x) - g x) := by
simp only [birkhoffAverage, birkhoffSum_apply_sub_birkhoffSum, ← smul_sub]