ofReal_expect — Mathlib

English

Let s be a finite index set and f: α → ℂ. The real part of the average of f over s equals the average of the real parts of f.

Русский

Пусть s — конечный индексный набор, а f: α → ℂ. Действительная часть среднего значения f по s равна среднему значению действительных частей f(i).

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, norm_cast]
theorem ofReal_expect (f : α → ℝ) : (𝔼 i ∈ s, f i : ℝ) = 𝔼 i ∈ s, (f i : ℂ) :=
  map_expect ofRealHom ..

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