expect_dite_eq' — Mathlib

English

Variant with f : ∀ j, j = i → M: the average of the dependent if h : j = i then f j h else 0 over j equals f(i) restricted by h, divided by card ι.

Русский

Вариант с f : ∀ j, j = i → M: среднее зависимого ite по j равно f(i) с условием h, деленное на card ι.

LaTeX

$$$\mathbb{E}_j (\text{if } j = i \text{ then } f(j, h) \text{ else } 0) = \frac{f(i, h')}{\\mathrm{card}(\\iota)}$$$

Lean4

theorem expect_dite_eq' (i : ι) (f : ∀ j, j = i → M) : 𝔼 j, (if h : j = i then f j h else 0) = f i rfl /ℚ card ι := by
  simp

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