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