Holomorphy and the conjugate Wirtinger derivative

For a real-differentiable map between complex normed spaces, vanishing of the conjugate Wirtinger derivative characterizes complex differentiability. The real-differentiability hypothesis is essential because the totalized real derivative vanishes at nondifferentiable points. In one variable the real differential has coefficients wirtingerDeriv f x 1 and conjWirtingerDeriv f x 1 in the basis dz, dbar z; testing the latter coefficient alone detects its vanishing.

These statements connect the real differential and its type decomposition with holomorphy.

References

• L. Hörmander, An Introduction to Complex Analysis in Several Variables, Chapter II.

theorem TauCeti.differentiableAt_iff_conjWirtingerDeriv_eq_zero {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup W] [NormedSpace ℂ W] {g : V → W} {x : V} (hg : DifferentiableAt ℝ g x) : DifferentiableAt ℂ g x ↔ conjWirtingerDeriv g x = 0

A real-differentiable map between complex normed spaces is complex differentiable exactly when its conjugate Wirtinger derivative vanishes.

theorem TauCeti.differentiableAt_iff_conjWirtingerDeriv_apply_one_eq_zero {W : Type u_2} [NormedAddCommGroup W] [NormedSpace ℂ W] {f : ℂ → W} {x : ℂ} (hf : DifferentiableAt ℝ f x) : DifferentiableAt ℂ f x ↔ (conjWirtingerDeriv f x) 1 = 0

For a real-differentiable function of one complex variable, the single equation conjWirtingerDeriv f x 1 = 0 characterizes complex differentiability.