complexToReal_fderiv — Mathlib

English

If f: ℂ → E has HasDerivWithinAt f f' s x, then the same real-linear derivative form holds: f' decomposed as re and im parts via the real-linear maps.

Русский

Если у f: ℂ → E есть HasDerivWithinAt f f' s x, то та же форма для веществено-линейной производной сохраняется: разложение по действительной и мнимой частям через соответствующие отображения.

LaTeX

$$$\displaystyle HasFDerivWithinAt f (reCLM.smulRight f' + I • imCLM.smulRight f') s x$$$

Lean4

theorem complexToReal_fderiv {f : ℂ → ℂ} {s : Set ℂ} {f' x : ℂ} (h : HasDerivWithinAt f f' s x) :
    HasFDerivWithinAt f (f' • (1 : ℂ →L[ℝ] ℂ)) s x := by
  simpa only [Complex.restrictScalars_one_smulRight] using h.hasFDerivWithinAt.restrictScalars ℝ

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