English
For i, a function f(j,i) depending on equality j=i, the average equals f(i,rfl)/|s| when i∈s, else 0.
Русский
Для зависимого от i f(j,i) среднее по j∈s от условия j=i равно f(i,rfl)/|s|, если i∈s, иначе 0.
LaTeX
$$$$ \\mathbb{E}_{j \\in s} (f(j,i) \\text{ if } j=i \\text{ else } 0) = \\begin{cases} \\dfrac{f(i, rfl)}{|s|}, & i \\in s \\\\ 0, & i \\notin s \\end{cases}. $$$$
Lean4
/-- Reorder an average.
The difference with `Finset.expect_bij'` is that the bijection is specified as a surjective
injection, rather than by an inverse function.
The difference with `Finset.expect_nbij` is that the bijection is allowed to use membership of the
domain of the average, rather than being a non-dependent function. -/
theorem expect_bij (i : ∀ a ∈ s, κ) (hi : ∀ a ha, i a ha ∈ t) (h : ∀ a ha, f a = g (i a ha))
(i_inj : ∀ a₁ ha₁ a₂ ha₂, i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂) (i_surj : ∀ b ∈ t, ∃ a ha, i a ha = b) :
𝔼 i ∈ s, f i = 𝔼 i ∈ t, g i := by simp_rw [expect, card_bij i hi i_inj i_surj, sum_bij i hi i_inj i_surj h]
