re_expect — Mathlib

English

The real part of the finite expectation equals the finite expectation of the real parts: Re(𝔼 f) = 𝔼 Re(f).

Русский

Действительная часть конечного ожидания равна ожиданию действительных частей: Re(𝔼 f) = 𝔼 Re(f).

LaTeX

$$$$ \operatorname{Re}\left( \mathbb{E}_{i \in s} f(i) \right) = \mathbb{E}_{i \in s} \operatorname{Re}\big( f(i) \big) $$$$

Lean4

@[simp]
theorem re_expect (f : α → ℂ) : (𝔼 i ∈ s, f i).re = 𝔼 i ∈ s, (f i).re :=
  map_expect (LinearMap.mk reAddGroupHom.toAddHom (by simp)) f s

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