English
For all f: α→α and g,g': α→G with G AddCommGroup, birkhoffSum f (g - g') n x = birkhoffSum f g n x - birkhoffSum f g' n x for all n and x.
Русский
Для любых f: α→α и наблюдаемых g,g': α→G, где G — AddCommGroup, выполняется birkhoffSum(f, g - g', n, x) = birkhoffSum(f, g, n, x) - birkhoffSum(f, g', n, x).
LaTeX
$$$\\mathrm{birkhoffSum}(f,g-g',n,x)=\\mathrm{birkhoffSum}(f,g,n,x)-\\mathrm{birkhoffSum}(f,g',n,x)$$$
Lean4
theorem birkhoffSum_sub (f : α → α) (g g' : α → G) (n : ℕ) (x : α) :
birkhoffSum f (g - g') n x = birkhoffSum f g n x - birkhoffSum f g' n x := by simp [birkhoffSum]