expect_sub_distrib — Mathlib

English

Let S ⊆ ι, T ⊆ κ, f : ι → M, g : κ → M and i : ι → κ, j : κ → ι such that i and j induce a bijection between the domains S and T and f = g ∘ i on S, then E_{i∈S} f(i) = E_{i∈T} g(i).

Русский

Пусть S ⊆ ι, T ⊆ κ, f : ι → M, g : κ → M и отображения i и j создают биекцию между S и T, причём f = g ∘ i на S, тогда среднее по S от f равно среднему по T от g.

LaTeX

$$$\exists i:S \to T, j:T \to S\ (\text{bijective})\ \wedge (\forall s\in S, f(s) = g(i(s))) \Rightarrow \dfrac{1}{|S|}\sum_{s\in S} f(s) = \dfrac{1}{|T|}\sum_{t\in T} g(t).$$$

Lean4

theorem expect_sub_distrib (s : Finset ι) (f g : ι → M) : 𝔼 i ∈ s, (f i - g i) = 𝔼 i ∈ s, f i - 𝔼 i ∈ s, g i := by
  simp only [expect, sum_sub_distrib, smul_sub]

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