English
Differentiability in the complex sense inside a set is equivalent to real differentiability together with the CR relation on the derivative.
Русский
Дифференцируемость в смысле комплексных перемещений внутри множества эквивалентна вещественной дифференцируемости вместе с отношением CR для производной.
LaTeX
$$DifferentiableWithinAt f s x \\iff (DifferentiableWithinAt Real f s x) ∧ (fderivWithin Real f s x I = I • fderivWithin Real f s x 1)$$
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_hasDerivWithinAt (h₁ : DifferentiableWithinAt ℝ f s x)
(h₂ : fderivWithin ℝ f s x I = I • fderivWithin ℝ f s x 1) :
HasDerivWithinAt f ((fderivWithin ℝ f s x).complexOfReal h₂ 1) s x :=
by
rw [hasDerivWithinAt_iff_hasFDerivWithinAt, smulRight_one_one]
exact h₁.hasFDerivWithinAt.complexOfReal h₂
