map_expect — Mathlib

English

Let F be a linear map and f : ι → M. Then applying F to the average of f over a finite index set yields the average of F∘f: F( E_{i∈s} f(i) ) = E_{i∈s} F( f(i) ).

Русский

Пусть F — линейное отображение и f: ι → M. Тогда применение F к среднему по конечному набору индексов дает среднее значения F(f(i)):

LaTeX

$$$F\left(\mathbb{E}_{i\in s} f(i)\right) = \mathbb{E}_{i\in s} F(f(i)).$$$

Lean4

theorem _root_.map_expect {F : Type*} [FunLike F M N] [LinearMapClass F ℚ≥0 M N] (g : F) (f : ι → M) (s : Finset ι) :
    g (𝔼 i ∈ s, f i) = 𝔼 i ∈ s, g (f i) := by simp only [expect, map_smul, map_sum]

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