birkhoffAverage_apply_sub_birkhoffAverage

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]

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