birkhoffAverage_add — Mathlib

English

BirkhoffAverage is additive in the second argument: birkhoffAverage_R f (g+g') = birkhoffAverage_R f g + birkhoffAverage_R f g'.

Русский

Среднее Биркхоффа по сумме функций равно сумме средних: birkhoffAverage_R f (g+g') = birkhoffAverage_R f g + birkhoffAverage_R f g'.

LaTeX

$$$\mathrm{birkhoffAverage}(R,f,g+g',n,x) = \mathrm{birkhoffAverage}(R,f,g,n,x) + \mathrm{birkhoffAverage}(R,f,g',n,x).$$$

Lean4

theorem birkhoffAverage_add {f : α → α} {g g' : α → M} :
    birkhoffAverage R f (g + g') = birkhoffAverage R f g + birkhoffAverage R f g' :=
  by
  funext _ x
  simp [birkhoffAverage, birkhoffSum, sum_add_distrib, smul_add]

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