complexToReal_fderiv — Mathlib

English

For a function f: ℂ → E with HasStrictDerivAt f f' x, the real-linear derivative is f' acted via the real-linear combination reCLM.smulRight f' + I • imCLM.smulRight f'.

Русский

Для функции f: ℂ → E с HasStrictDerivAt f f' x реальная линейная производная задаётся как сумма образований через действительную и мнимую части.

LaTeX

$$$\displaystyle \text{If } h: HasStrictDerivAt f f' x, \text{ then } Df(x) = reCLM.smulRight f' + I \cdot imCLM.smulRight f'. $$$

Lean4

theorem complexToReal_fderiv {f : ℂ → ℂ} {f' x : ℂ} (h : HasStrictDerivAt f f' x) :
    HasStrictFDerivAt f (f' • (1 : ℂ →L[ℝ] ℂ)) x := by
  simpa only [Complex.restrictScalars_one_smulRight] using h.hasStrictFDerivAt.restrictScalars ℝ

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