expect_image — Mathlib

English

Let s ⊆ ι, t ⊆ κ and f : ι → κ → M. Then E_{(i,j)∈s×t} f(i,j) = E_{i∈s} E_{j∈t} f(i,j).

Русский

Пусть s ⊆ ι, t ⊆ κ и f : ι → κ → M. Тогда среднее по произведению равно вложенным средним: E_{(i,j)∈s×t} f(i,j) = E_{i∈s} E_{j∈t} f(i,j).

LaTeX

$$$\mathbb{E}_{(i,j)\in s\times t} f(i,j) = \mathbb{E}_{i\in s}\,\mathbb{E}_{j\in t} f(i,j).$$$

Lean4

@[simp]
theorem expect_image [DecidableEq ι] {m : κ → ι} (hm : (t : Set κ).InjOn m) : 𝔼 i ∈ t.image m, f i = 𝔼 i ∈ t, f (m i) :=
  by simp_rw [expect, card_image_of_injOn hm, sum_image hm]

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