birkhoffAverage_sub — Mathlib

English

BirkhoffAverage is linear with respect to subtraction of second arguments: 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_sub {f : α → α} {g g' : α → M} :
    birkhoffAverage R f (g - g') = birkhoffAverage R f g - birkhoffAverage R f g' :=
  by
  funext _ x
  simp [birkhoffAverage, birkhoffSum, smul_sub]

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