expect_ite_mem — Mathlib

English

Let s be a finite set and f: ι → M. Then 𝔼 i, (if i ∈ s then f i else 0) equals s.dens times 𝔼 i ∈ s, f i.

Русский

Пусть s — конечное множество и f: ι → M. Тогда 𝔼 i (if i ∈ s then f(i) иначе 0) = s.dens · 𝔼 i ∈ s, f(i).

LaTeX

$$$\mathbb{E}_{i} (\mathbf{1}_{i \in s} f(i)) = \operatorname{dens}(s) \cdot \mathbb{E}_{i \in s} f(i)$$$

Lean4

@[simp]
theorem expect_ite_mem (s : Finset ι) (f : ι → M) : 𝔼 i, (if i ∈ s then f i else 0) = s.dens • 𝔼 i ∈ s, f i := by
  simp [Finset.expect_ite_mem, dens]

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