birkhoffSum_one

Mathlib.Dynamics.BirkhoffSum.Basic

URI: https://scilib.ai/kg/mathlib#birkhoffSum_one

English

The Birkhoff sum for n = 1 equals g(x): birkhoffSum f g 1 x = g(x).

Русский

Сумма Биркхоффа за один шаг равна g(x).

LaTeX

$$$\mathrm{birkhoffSum}(f,g,1,x) = g(x)$$$

Lean4

theorem birkhoffSum_one (f : α → α) (g : α → M) (x : α) : birkhoffSum f g 1 x = g x :=
  sum_range_one _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru