complexOfReal_fderiv — Mathlib

English

If h₁ and h₂ hold, then the complex derivative equals the complexOfReal of the real derivative.

Русский

Если выполняются условия h₁ и h₂, то комплексная производная равна complexOfReal от вещественной производной.

LaTeX

$$(fderiv Real f x) .complexOfReal h₂ = fderiv ℂ f x$$

Lean4

/-- In cases where the **Cauchy-Riemann Equation** guarantees complex differentiability at `x`, the
complex derivative equals `ContinuousLinearMap.complexOfReal` of the real derivative.
-/
theorem complexOfReal_fderiv (h₁ : DifferentiableAt ℝ f x) (h₂ : fderiv ℝ f x I = I • fderiv ℝ f x 1) :
    (fderiv ℝ f x).complexOfReal h₂ = fderiv ℂ f x :=
  (h₁.hasFDerivAt.complexOfReal_hasFDerivAt h₂).fderiv.symm

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