expect_univ — Mathlib

English

Suppose s=t and p and q agree on t; if f(i)=g(i) whenever q(i) holds, then the expectations with predicates p and q coincide: 𝔼 i∈s with p i, f i = 𝔼 i∈t with q i, g i.

Русский

Пусть s=t, предикаты p и q совпадают на t; если f(i)=g(i) там, где q(i) истинно, то средние значения совпадают: 𝔼 i∈s с p i, f i = 𝔼 i∈t с q i, g i.

LaTeX

$$$$ \\mathbb{E}_{i \\in s}^{p} f(i) = \\mathbb{E}_{i \\in t}^{q} g(i) \\quad \\text{если } s=t \\text{ и } \\forall i\\in t,\; p(i) \\iff q(i), \\; f(i)=g(i) \\text{ когда } q(i). $$$$

Lean4

theorem expect_univ [Fintype ι] : 𝔼 i, f i = (∑ i, f i) /ℚ Fintype.card ι := by rw [expect, card_univ]

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