re_ofReal — Mathlib

English

If f is analytic on the image of the real-to-complex embedding, then the real-variable function x ↦ Im(f(Reals)) is analytic on the real domain.

Русский

Если f аналитична на образе отображения из действительных чисел в комплекс, то функция x ↦ Im(f(x)) от действительных переменных аналитична на вещественной области.

LaTeX

$$$\\text{AnalyticOn}_\\mathbb{R}(\\operatorname{Im}\nabla f)(s) \\text{ if } \\text{AnalyticOn}_\\mathbb{C} f(\\operatorname{Set.image}(\\text{Real.ofReal},s))$$$

Lean4

theorem re_ofReal (hf : AnalyticWithinAt ℂ f (ofReal '' s) x) : AnalyticWithinAt ℝ (fun x : ℝ ↦ (f x).re) s x :=
  ((Complex.reCLM.analyticWithinAt _ _).comp hf.restrictScalars (mapsTo_image f _)).comp
    (Complex.ofRealCLM.analyticWithinAt _ _) (mapsTo_image ofReal s)

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