English
If a complex-valued function e is differentiable at a real point z with derivative e', then the real-valued function x ↦ Re(e(x)) is differentiable at z with derivative Re(e').
Русский
Если функция e: ℂ → ℂ дифференцируема в действительной точке z с производной e', то функция x ↦ Re(e(x)) дифференцируема в z и её производная равна Re(e').
LaTeX
$$$\displaystyle \text{If } e: \mathbb{C} \to \mathbb{C},\ z\in\mathbb{R},\ e'\in\mathbb{C},\ \text{and } e \text{ is differentiable at } z \text{ with } e',\ \text{then } x \mapsto \Re(e(x))\text{ is differentiable at } z\text{ with derivative } \Re(e').$$$
Lean4
/-- If a complex function `e` is differentiable at a real point, then the function `ℝ → ℝ` given by
the real part of `e` is also differentiable at this point, with a derivative equal to the real part
of the complex derivative. -/
theorem real_of_complex (h : HasDerivAt e e' z) : HasDerivAt (fun x : ℝ => (e x).re) e'.re z :=
by
have A : HasFDerivAt ((↑) : ℝ → ℂ) ofRealCLM z := ofRealCLM.hasFDerivAt
have B : HasFDerivAt e ((ContinuousLinearMap.smulRight 1 e' : ℂ →L[ℂ] ℂ).restrictScalars ℝ) (ofRealCLM z) :=
h.hasFDerivAt.restrictScalars ℝ
have C : HasFDerivAt re reCLM (e (ofRealCLM z)) := reCLM.hasFDerivAt
simpa using (C.comp z (B.comp z A)).hasDerivAt
