Theorems · Theorem · dynamical systems

dist_birkhoffAverage_birkhoffAverage

∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] (𝕜 : Type u_3) [inst_1 : RCLike 𝕜]
  [inst_2 : NormedSpace 𝕜 E] (f : α → α) (g : α → E) (n : ℕ) (x y : α),
  dist (birkhoffAverage 𝕜 f g n x) (birkhoffAverage 𝕜 f g n y) = dist (birkhoffSum f g n x) (birkhoffSum f g n y) / ↑n

Defined in

Mathlib.Dynamics.BirkhoffSum.NormedSpace

Cited by

2 results in Mathlib

Foundations

Depth 162 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupRCLikeNormedSpace