English
If the Cauchy-Riemann equation holds for a real differentiable f, then the complex derivative equals the complexOfReal of the real derivative.
Русский
Если для вещественно дифференцируемой функции f выполняется уравнение Коши–Римана, то комплексная производная равна complexOfReal у её вещественной производной.
LaTeX
$$fderivWithin f s x = (fderivWithin Real f s x).complexOfReal h₂$$
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_fderivWithin (h₁ : DifferentiableWithinAt ℝ f s x)
(h₂ : fderivWithin ℝ f s x I = I • fderivWithin ℝ f s x 1) (hs : UniqueDiffWithinAt ℝ s x) :
fderivWithin ℂ f s x = (fderivWithin ℝ f s x).complexOfReal h₂ :=
by
have :=
((differentiableWithinAt_complex_iff_differentiableWithinAt_real hs).2 ⟨h₁, h₂⟩).restrictScalars_fderivWithin ℝ hs
simpa [DFunLike.ext_iff]
