im_expect — Mathlib

English

The imaginary part of the finite expectation equals the finite expectation of the imaginary parts: Im(𝔼 f) = 𝔼 Im(f).

Русский

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

LaTeX

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

Lean4

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

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