measurable_arg — Mathlib

English

The complex argument function arg: ℂ → ℝ is measurable.

Русский

Функция arg: ℂ → ℝ измерима.

LaTeX

$$$\\\\operatorname{Measurable}(\\\\operatorname{arg})$$$

Lean4

@[measurability]
theorem measurable_arg : Measurable arg :=
  have A : Measurable fun x : ℂ => Real.arcsin (x.im / ‖x‖) :=
    Real.measurable_arcsin.comp (measurable_im.div measurable_norm)
  have B : Measurable fun x : ℂ => Real.arcsin ((-x).im / ‖x‖) :=
    Real.measurable_arcsin.comp ((measurable_im.comp measurable_neg).div measurable_norm)
  Measurable.ite (isClosed_le continuous_const continuous_re).measurableSet A <|
    Measurable.ite (isClosed_le continuous_const continuous_im).measurableSet (B.add_const _) (B.sub_const _)

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