expect_const

Mathlib.Algebra.BigOperators.Expect

URI: https://scilib.ai/kg/mathlib#Fintype.expect_const

English

Let I be finite and nonempty; the average of a constant a over I equals a:

Русский

Пусть I конечно и непусто. Тогда среднее константы a по I равно a.

LaTeX

$$$\mathbb{E}_{i \\in \mathrm{univ}} a = a$$$

Lean4

theorem expect_const [Nonempty ι] (a : M) : 𝔼 _i : ι, a = a :=
  Finset.expect_const univ_nonempty _

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

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

Разделы

Аффилиация

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