integral_coe_re_add_coe_im — Mathlib

English

For f: X → 𝕜 integrable, the integral equals the sum of its real and imaginary parts with appropriate embeddings: ∫ Re(f) + (∫ Im(f)) I = ∫ f.

Русский

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

LaTeX

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

Lean4

theorem integral_coe_re_add_coe_im {f : X → 𝕜} (hf : Integrable f μ) :
    ∫ x, (re (f x) : 𝕜) ∂μ + (∫ x, (im (f x) : 𝕜) ∂μ) * RCLike.I = ∫ x, f x ∂μ :=
  by
  rw [mul_comm, ← smul_eq_mul, ← integral_smul, ← integral_add]
  · congr
    ext1 x
    rw [smul_eq_mul, mul_comm, RCLike.re_add_im]
  · exact hf.re.ofReal
  · exact hf.im.ofReal.smul (𝕜 := 𝕜) (β := 𝕜) RCLike.I

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