expect_apply — Mathlib

English

Let e: ι → κ be a bijection, and f: ι → M, g: κ → M with f(i) = g(e(i)) for all i. Then the averages of f and g are equal:

Русский

Пусть e: ι → κ — биекция, и f: ι → M, g: κ → M удовлетворяют f(i) = g(e(i)) для всех i. Тогда средние значения f и g совпадают.

LaTeX

$$$\mathbb{E}_{i \\in \mathrm{univ}} f(i) = \mathbb{E}_{i \\in \mathrm{univ}} g(i)$, при условии $f(i) = g(e(i))$ для биекции $e$.$$

Lean4

@[simp]
theorem expect_apply {α : Type*} {π : α → Type*} [∀ a, CommSemiring (π a)] [∀ a, Module ℚ≥0 (π a)] (s : Finset ι)
    (f : ι → ∀ a, π a) (a : α) : (𝔼 i ∈ s, f i) a = 𝔼 i ∈ s, f i a := by simp [expect]

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