birkhoffSum — Mathlib

English

A second simp lemma asserting birkhoffAverage R f g 1 = g, as a direct corollary of the previous variant.

Русский

Еще одна простая лемма, утверждающая birkhoffAverage R f g 1 = g как следствие предыдущего утверждения.

LaTeX

$$$\mathrm{birkhoffAverage}(R,f,g,1) = g$$$

Lean4

/-- The sum of values of `g` on the first `n` points of the orbit of `x` under `f`. -/
def birkhoffSum (f : α → α) (g : α → M) (n : ℕ) (x : α) : M :=
  ∑ k ∈ range n, g (f^[k] x)

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