expect_add_distrib

Mathlib.Algebra.BigOperators.Expect

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

English

The expectation distributes over addition: E_s (f + g) = E_s f + E_s g.

Русский

Ожидание распределяется по сложению: E_s(f + g) = E_s f + E_s g.

LaTeX

$$$$ \\mathbb{E}_{i \\in s} (f(i) + g(i)) = \\mathbb{E}_{i \\in s} f(i) + \\mathbb{E}_{i \\in s} g(i). $$$$

Lean4

theorem expect_add_distrib (s : Finset ι) (f g : ι → M) : 𝔼 i ∈ s, (f i + g i) = 𝔼 i ∈ s, f i + 𝔼 i ∈ s, g i := by
  simp [expect, sum_add_distrib]

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

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

Разделы

Аффилиация

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