re_im_iff — Mathlib

English

The integrability of a complex-valued function f is equivalent to the integrability of its real and imaginary parts.

Русский

Интегрируемость комплекснозначной функции f эквивалентна интегрируемости её вещественной и мнимой частей.

LaTeX

$$$\mathrm{Integrable}(f,\mu) \Leftrightarrow \mathrm{Integrable}(\operatorname{Re}(f),\mu) \land \mathrm{Integrable}(\operatorname{Im}(f),\mu).$$$

Lean4

theorem re_im_iff :
    Integrable (fun x => RCLike.re (f x)) μ ∧ Integrable (fun x => RCLike.im (f x)) μ ↔ Integrable f μ :=
  by
  simp_rw [← memLp_one_iff_integrable]
  exact memLp_re_im_iff

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