aemeasurable_of_re_im — Mathlib

English

If Re(f) and Im(f) are a.e.-measurable, then f is a.e.-measurable.

Русский

Если Re(f) и Im(f) равномерно измеримы почти всюду, то f измерима почти всюду.

LaTeX

$$$ (AEMeasurable (\\operatorname{Re} \\circ f) μ) \\land (AEMeasurable (\\operatorname{Im} \\circ f) μ) \\Rightarrow AEMeasurable(f μ) $$$

Lean4

theorem aemeasurable_of_re_im (hre : AEMeasurable (fun x => RCLike.re (f x)) μ)
    (him : AEMeasurable (fun x => RCLike.im (f x)) μ) : AEMeasurable f μ :=
  by
  convert
    AEMeasurable.add (M := 𝕜) (RCLike.measurable_ofReal.comp_aemeasurable hre)
      ((RCLike.measurable_ofReal.comp_aemeasurable him).mul_const RCLike.I)
  exact (RCLike.re_add_im _).symm

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