expect_ite_zero — Mathlib

English

Let p: ι → Prop with DecidablePred p; if at most one i satisfies p, then the average of ite(p i) a over i equals a/card ι when there exists i with p i, otherwise 0:

Русский

Пусть p: ι → Prop с разрешённым выбором. Если не более одного i удовлетворяет p, то среднее по i от ite(p i) a равно a/card ι при существовании i с p i, иначе 0.

LaTeX

$$$\mathbb{E}_i \operatorname{ite}(p(i), a, 0) = \operatorname{ite}(\exists i, p(i)) \left( \frac{a}{\\mathrm{card}(\\iota)} \right) 0$$$

Lean4

theorem expect_ite_zero (p : ι → Prop) [DecidablePred p] (h : ∀ i j, p i → p j → i = j) (a : M) :
    𝔼 i, ite (p i) a 0 = ite (∃ i, p i) (a /ℚ Fintype.card ι) 0 := by simp [univ.expect_ite_zero p (by simpa using h)]

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