birkhoffAverage_one

Mathlib.Dynamics.BirkhoffSum.Average

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

English

For any f,g,x, the Birkhoff average with n = 1 equals g(x): birkhoffAverage_R f g 1 x = g(x).

Русский

Для любых f, g, x среднее Биркхоффа при n = 1 равно g(x).

LaTeX

$$$\mathrm{birkhoffAverage}(R,f,g,1,x) = g(x)$.$$

Lean4

theorem birkhoffAverage_one (f : α → α) (g : α → M) (x : α) : birkhoffAverage R f g 1 x = g x := by
  simp [birkhoffAverage]

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

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

Разделы

Аффилиация

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