English
Let e: ℂ → ℂ be differentiable at a real point z with complex 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},\ \text{and } e \text{ is differentiable at } z \text{ with derivative } e', \\ \text{then } (x \mapsto \Re(e(x)))'|_{x=z} = \Re(e').$$$
Lean4
/-- If a complex function is differentiable at a real point, then the induced real function is also
differentiable at this point, with a derivative equal to the real part of the complex derivative. -/
theorem real_of_complex (h : HasStrictDerivAt e e' z) : HasStrictDerivAt (fun x : ℝ => (e x).re) e'.re z :=
by
have A : HasStrictFDerivAt ((↑) : ℝ → ℂ) ofRealCLM z := ofRealCLM.hasStrictFDerivAt
have B : HasStrictFDerivAt e ((ContinuousLinearMap.smulRight 1 e' : ℂ →L[ℂ] ℂ).restrictScalars ℝ) (ofRealCLM z) :=
h.hasStrictFDerivAt.restrictScalars ℝ
have C : HasStrictFDerivAt re reCLM (e (ofRealCLM z)) := reCLM.hasStrictFDerivAt
simpa using (C.comp z (B.comp z A)).hasStrictDerivAt
