English
For a finite type ι, the average of the product involving a Boolean-like weight ite(i = j) equals the diagonal value f(i): E_{j} ite(i=j) N 0 · f(j) = f(i).
Русский
Для конечного типа ι среднее от произведения с весом-вектором in{j=i} равно диагональному значению: E_{j} 1_{j=i} N 0 · f(j) = f(i).
LaTeX
$$$\mathbb{E}_{j} \big( \mathbf{1}_{\{j=i\}} \cdot (|\iota|)_{cast} \cdot 0 \big) \cdot f(j) = f(i)$.$$
Lean4
theorem expect_boole_mul [Fintype ι] [Nonempty ι] [DecidableEq ι] (f : ι → M) (i : ι) :
𝔼 j, ite (i = j) (Fintype.card ι : M) 0 * f j = f i :=
by
simp_rw [expect_univ, ite_mul, zero_mul, sum_ite_eq, if_pos (mem_univ _)]
rw [← @NNRat.cast_natCast M, ← NNRat.smul_def, inv_smul_smul₀]
simp [Fintype.card_ne_zero]
