English
If g' is a map between modules (compatible with the structures), then applying g' to birkhoffAverage_R f g n x equals birkhoffAverage_S f (g' ∘ g) n x.
Русский
При помощи отображения g' между модулями среднее Биркхоффа трансформируется посредством композиции: g'(birkhoffAverage_R f g n x) = birkhoffAverage_S f (g' ∘ g) n x.
LaTeX
$$$g'\bigl(\mathrm{birkhoffAverage}(R,f,g,n,x)\bigr) = \mathrm{birkhoffAverage}(S,f,g' \circ g,n,x).$$$
Lean4
theorem map_birkhoffAverage (S : Type*) {F N : Type*} [DivisionSemiring S] [AddCommMonoid N] [Module S N]
[FunLike F M N] [AddMonoidHomClass F M N] (g' : F) (f : α → α) (g : α → M) (n : ℕ) (x : α) :
g' (birkhoffAverage R f g n x) = birkhoffAverage S f (g' ∘ g) n x := by
simp only [birkhoffAverage, map_inv_natCast_smul g' R S, map_birkhoffSum]
