expect_eq_zero

Mathlib.Algebra.BigOperators.Expect

URI: https://scilib.ai/kg/mathlib#Finset.expect_eq_zero

English

If f(i)=0 for all i∈s, then 𝔼 i∈s f(i) = 0.

Русский

Если f(i) = 0 для всех i∈s, то 𝔼 i∈s f(i) = 0.

LaTeX

$$$$ \\mathbb{E}_{i \\in s} f(i) = 0 \\quad \\text{если } \\forall i \\in s,\\ f(i)=0. $$$$

Lean4

theorem expect_eq_zero (h : ∀ i ∈ s, f i = 0) : 𝔼 i ∈ s, f i = 0 :=
  (expect_congr rfl h).trans s.expect_const_zero

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

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

Разделы

Аффилиация

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