expect_ite_eq' — Mathlib

English

A second bijection-based averaging identity, mirroring the previous bijection lemma with a different presentation of the index map.

Русский

Вторая идентичность усреднения по биекции, повторяющая предыдущий факт с иным представлением отображения индексов.

LaTeX

$$$$ \\mathbb{E}_{i \\in s} f(i) = \\mathbb{E}_{i \\in t} g(i) $$ under the same bijection conditions as above.$$

Lean4

@[simp]
theorem expect_ite_eq' (i : ι) (f : ι → M) : 𝔼 j ∈ s, (if j = i then f j else 0) = if i ∈ s then f i /ℚ #s else 0 := by
  split_ifs <;> simp [expect, *]

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