integral_re_add_im — Mathlib

English

For f: X → 𝕜 integrable on a set i, we have ∫_i Re(f) + (∫_i Im(f)) I = ∫_i f.

Русский

Для интегрируемой функции f: X → 𝕜 на множества i имеем ∫_i Re(f) + i ∫_i Im(f) = ∫_i f.

LaTeX

$$$\\left(\\int_{x\\in i} \\operatorname{Re}(f(x)) \\,d\\mu\\right) + i\\left(\\int_{x\\in i} \\operatorname{Im}(f(x)) \\,d\\mu\\right) = \\int_{x\\in i} f(x) \\,d\\mu$$$

Lean4

theorem integral_re_add_im {f : X → 𝕜} (hf : Integrable f μ) :
    ((∫ x, RCLike.re (f x) ∂μ : ℝ) : 𝕜) + (∫ x, RCLike.im (f x) ∂μ : ℝ) * RCLike.I = ∫ x, f x ∂μ := by
  rw [← integral_ofReal, ← integral_ofReal, integral_coe_re_add_coe_im hf]

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