English
If e: ℂ → ℂ is ContDiffAt of order n at Complex.ofReal(z) along the complex domain, then the real-valued map x ↦ Re(e(Complex.ofReal x)) is ContDiffAt of order n at z as a function from ℝ to ℝ.
Русский
Если e: ℂ → ℂ имеет континуальную дифференцируемость порядка n в точке Complex.ofReal(z), то функция x ↦ Re(e(Complex.ofReal x)) с области ℝ → ℝ тоже обладает континуальной дифференцируемостью порядка n в z.
LaTeX
$$$\displaystyle \text{If } e: \mathbb{C} \to \mathbb{C} \text{ is ContDiff }_\mathbb{C}^n( e ) \text{ at } \mathbb{C}.ofReal(z), \text{ then } x \mapsto \Re(e(\mathbb{C}.ofReal(x))) \text{ is ContDiff }_\mathbb{R}^n\text{ at } z.$$$
Lean4
theorem real_of_complex {n : WithTop ℕ∞} (h : ContDiffAt ℂ n e z) : ContDiffAt ℝ n (fun x : ℝ => (e x).re) z :=
by
have A : ContDiffAt ℝ n ((↑) : ℝ → ℂ) z := ofRealCLM.contDiff.contDiffAt
have B : ContDiffAt ℝ n e z := h.restrict_scalars ℝ
have C : ContDiffAt ℝ n re (e z) := reCLM.contDiff.contDiffAt
exact C.comp z (B.comp z A)
