Wirtinger derivatives

For a function g : V → W between complex normed spaces, the Wirtinger derivatives of g at x are the complex-linear and complex-antilinear parts of its real derivative:

∂g(x) v = (Dg(x) v - I • Dg(x)(I • v)) / 2, \bar∂g(x) v = (Dg(x) v + I • Dg(x)(I • v)) / 2.

In holomorphic coordinates z_j = x_j + I y_j with coordinate vectors e_j, these are the classical operators ∂g(x) e_j = ∂g/∂z_j = (∂g/∂x_j - I ∂g/∂y_j) / 2 and \bar∂g(x) e_j = ∂g/∂(conj z_j) = (∂g/∂x_j + I ∂g/∂y_j) / 2.

Their comparison with the Levi form is in TauCeti.Analysis.Complex.Wirtinger.LeviForm.

Main definitions

• TauCeti.wirtingerDeriv g x: the complex-linear Wirtinger derivative ∂g(x) : V →L[ℂ] W.
• TauCeti.conjWirtingerDeriv g x: the complex-antilinear Wirtinger derivative \bar∂g(x) : V →L⋆[ℂ] W.

Main results

• TauCeti.wirtingerDeriv_add_conjWirtingerDeriv: ∂g + \bar∂g = Dg.
• TauCeti.norm_wirtingerDeriv_apply_le, TauCeti.norm_conjWirtingerDeriv_apply_le: both Wirtinger derivatives are bounded by the real derivative, ‖∂g(x) v‖ ≤ ‖Dg(x)‖ ‖v‖.
• TauCeti.coe_wirtingerDeriv_eq_complexLinearPart, TauCeti.coe_conjWirtingerDeriv_eq_complexAntilinearPart: the Wirtinger derivatives are the complex-linear and complex-antilinear parts of the real derivative.
• TauCeti.conjWirtingerDeriv_ofReal_comp_apply: for real-valued f, \bar∂f = conj ∂f.
• TauCeti.wirtingerDeriv_smul_apply, TauCeti.conjWirtingerDeriv_smul_apply: the product rules ∂(c g) = c ∂g + (∂c) g and \bar∂(c g) = c \bar∂g + (\bar∂c) g for a complex-valued factor c.
• TauCeti.norm_wirtingerDeriv_smul_sub_smul_le, TauCeti.norm_conjWirtingerDeriv_smul_sub_smul_le: for a real factor χ, ‖∂(χ u)(x) v - χ ∂u(x) v‖ ≤ ‖Dχ(x)‖ ‖v‖ ‖u(x)‖, and likewise for \bar∂.
• ContDiffAt.conjWirtingerDeriv_apply: the conjugate Wirtinger derivative of a C^(m+1) map is C^m.
• DifferentiableAt.conjWirtingerDeriv_eq_zero, DifferentiableAt.wirtingerDeriv_eq_fderiv: for complex differentiable g, \bar∂g = 0 and ∂g is the complex derivative.
• TauCeti.conjWirtingerDeriv_const_smul: \bar∂ commutes with complex scalar multiplication.
• TauCeti.conjWirtingerDeriv_eq_sum_smul: \bar∂ depends complex-linearly on the real derivative.
• TauCeti.conjWirtingerDeriv_fun_sum: \bar∂ of a finite sum of real-differentiable functions.
• TauCeti.conjWirtingerDeriv_fun_mul, TauCeti.conjWirtingerDeriv_fun_pow: the Leibniz and power rules for complex-valued functions.
• TauCeti.conjWirtingerDeriv_apply_eq_conjWirtingerDeriv_line: \bar∂g(x) v is the one-variable conjugate Wirtinger derivative of the restriction of g to the complex line t ↦ x + t • v.
• ContDiffAt.hasFDerivAt_conjWirtingerDeriv_apply: the derivative of y ↦ \bar∂g(y) u for a C² map g, in terms of the second derivative of g.
• TauCeti.conjWirtingerDeriv_conjWirtingerDeriv_comm: second conjugate Wirtinger derivatives of a C² map commute.

Implementation notes

Both derivatives are built from the totalized real derivative fderiv ℝ g x, so at a point where g is not real-differentiable both are the junk value 0. Results that need a genuine derivative therefore assume differentiability; for instance, the converse "\bar∂g = 0 implies complex differentiability" (TauCeti.differentiableAt_iff_conjWirtingerDeriv_eq_zero in TauCeti.Analysis.Complex.Wirtinger.Holomorphic) assumes DifferentiableAt ℝ g x.

References

• R. Hain, Notes on the Morse theory of complex manifolds.
• L. Hörmander, An introduction to complex analysis in several variables, Chapter II.

noncomputable def TauCeti.wirtingerDeriv {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup W] [NormedSpace ℂ W] (g : V → W) (x : V) : V →L[ℂ] W

The Wirtinger derivative ∂g(x) of a function into a complex normed space: the complex-linear part v ↦ (Dg(x) v - I • Dg(x)(I • v)) / 2 of its real derivative (ContinuousLinearMap.complexLinearPart). On a coordinate vector e_j it is ∂g / ∂z_j. Like fderiv ℝ g x, from which it is built, it is the junk value 0 at points where g is not real-differentiable, so results that need a genuine derivative assume differentiability of g at x.

noncomputable def TauCeti.conjWirtingerDeriv {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup W] [NormedSpace ℂ W] (g : V → W) (x : V) : V →L⋆[ℂ] W

The conjugate Wirtinger derivative \bar∂g(x) of a function into a complex normed space: the complex-antilinear part v ↦ (Dg(x) v + I • Dg(x)(I • v)) / 2 of its real derivative (ContinuousLinearMap.complexAntilinearPart). On a coordinate vector e_j it is ∂g / ∂(conj z_j). Like fderiv ℝ g x, from which it is built, it is the junk value 0 at points where g is not real-differentiable, so results that need a genuine derivative assume differentiability of g at x.

theorem TauCeti.wirtingerDeriv_eq_complexLinearPart {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup W] [NormedSpace ℂ W] (g : V → W) (x : V) : wirtingerDeriv g x = (fderiv ℝ g x).complexLinearPart

The Wirtinger derivative is the complex-linear part of the real derivative.

theorem TauCeti.conjWirtingerDeriv_eq_complexAntilinearPart {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup W] [NormedSpace ℂ W] (g : V → W) (x : V) : conjWirtingerDeriv g x = (fderiv ℝ g x).complexAntilinearPart

The conjugate Wirtinger derivative is the complex-antilinear part of the real derivative.

theorem TauCeti.wirtingerDeriv_apply {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup W] [NormedSpace ℂ W] (g : V → W) (x v : V) : (wirtingerDeriv g x) v = 2⁻¹ • ((fderiv ℝ g x) v - Complex.I • (fderiv ℝ g x) (Complex.I • v))

The defining formula of the Wirtinger derivative.

theorem TauCeti.conjWirtingerDeriv_apply {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup W] [NormedSpace ℂ W] (g : V → W) (x v : V) : (conjWirtingerDeriv g x) v = 2⁻¹ • ((fderiv ℝ g x) v + Complex.I • (fderiv ℝ g x) (Complex.I • v))

The defining formula of the conjugate Wirtinger derivative.

@[simp]

theorem TauCeti.wirtingerDeriv_add_conjWirtingerDeriv {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup W] [NormedSpace ℂ W] (g : V → W) (x v : V) : (wirtingerDeriv g x) v + (conjWirtingerDeriv g x) v = (fderiv ℝ g x) v

The two Wirtinger derivatives add up to the real derivative.

theorem TauCeti.norm_wirtingerDeriv_apply_le {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup W] [NormedSpace ℂ W] (g : V → W) (x v : V) : ‖(wirtingerDeriv g x) v‖ ≤ ‖fderiv ℝ g x‖ * ‖v‖

The Wirtinger derivative is bounded by the real derivative: ‖∂g(x) v‖ ≤ ‖Dg(x)‖ ‖v‖.

theorem TauCeti.norm_conjWirtingerDeriv_apply_le {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup W] [NormedSpace ℂ W] (g : V → W) (x v : V) : ‖(conjWirtingerDeriv g x) v‖ ≤ ‖fderiv ℝ g x‖ * ‖v‖

The conjugate Wirtinger derivative is bounded by the real derivative: ‖\bar∂g(x) v‖ ≤ ‖Dg(x)‖ ‖v‖.

theorem TauCeti.coe_wirtingerDeriv_eq_complexLinearPart {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup W] [NormedSpace ℂ W] (g : V → W) (x : V) : ⇑(wirtingerDeriv g x) = ⇑(complexLinearPart (DistribSMul.toLinearMap ℝ V Complex.I) (DistribSMul.toLinearMap ℝ W Complex.I) ↑(fderiv ℝ g x))

The Wirtinger derivative is the complex-linear part TauCeti.complexLinearPart of the real derivative, for the complex structures given by multiplication by I.

theorem TauCeti.coe_conjWirtingerDeriv_eq_complexAntilinearPart {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup W] [NormedSpace ℂ W] (g : V → W) (x : V) : ⇑(conjWirtingerDeriv g x) = ⇑(complexAntilinearPart (DistribSMul.toLinearMap ℝ V Complex.I) (DistribSMul.toLinearMap ℝ W Complex.I) ↑(fderiv ℝ g x))

The conjugate Wirtinger derivative is the complex-antilinear part TauCeti.complexAntilinearPart of the real derivative, for the complex structures given by multiplication by I.

theorem Filter.EventuallyEq.wirtingerDeriv_eq {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup W] [NormedSpace ℂ W] {g₁ g : V → W} {x : V} (h : g₁ =ᶠ[nhds x] g) : TauCeti.wirtingerDeriv g₁ x = TauCeti.wirtingerDeriv g x

The Wirtinger derivative only depends on the germ of the function.

theorem Filter.EventuallyEq.conjWirtingerDeriv_eq {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup W] [NormedSpace ℂ W] {g₁ g : V → W} {x : V} (h : g₁ =ᶠ[nhds x] g) : TauCeti.conjWirtingerDeriv g₁ x = TauCeti.conjWirtingerDeriv g x

The conjugate Wirtinger derivative only depends on the germ of the function.

theorem TauCeti.wirtingerDeriv_add {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup W] [NormedSpace ℂ W] {g₁ g₂ : V → W} {x : V} (h₁ : DifferentiableAt ℝ g₁ x) (h₂ : DifferentiableAt ℝ g₂ x) : wirtingerDeriv (g₁ + g₂) x = wirtingerDeriv g₁ x + wirtingerDeriv g₂ x

The Wirtinger derivative is additive on real-differentiable functions.

theorem TauCeti.wirtingerDeriv_sub {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup W] [NormedSpace ℂ W] {g₁ g₂ : V → W} {x : V} (h₁ : DifferentiableAt ℝ g₁ x) (h₂ : DifferentiableAt ℝ g₂ x) : wirtingerDeriv (g₁ - g₂) x = wirtingerDeriv g₁ x - wirtingerDeriv g₂ x

The Wirtinger derivative commutes with subtraction of real-differentiable functions.

theorem TauCeti.conjWirtingerDeriv_add {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup W] [NormedSpace ℂ W] {g₁ g₂ : V → W} {x : V} (h₁ : DifferentiableAt ℝ g₁ x) (h₂ : DifferentiableAt ℝ g₂ x) : conjWirtingerDeriv (g₁ + g₂) x = conjWirtingerDeriv g₁ x + conjWirtingerDeriv g₂ x

The conjugate Wirtinger derivative is additive on real-differentiable functions.

theorem TauCeti.conjWirtingerDeriv_sub {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup W] [NormedSpace ℂ W] {g₁ g₂ : V → W} {x : V} (h₁ : DifferentiableAt ℝ g₁ x) (h₂ : DifferentiableAt ℝ g₂ x) : conjWirtingerDeriv (g₁ - g₂) x = conjWirtingerDeriv g₁ x - conjWirtingerDeriv g₂ x

The conjugate Wirtinger derivative commutes with subtraction of real-differentiable functions.

theorem TauCeti.conjWirtingerDeriv_const_smul {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup W] [NormedSpace ℂ W] {g : V → W} {x : V} (c : ℂ) : conjWirtingerDeriv (c • g) x = c • conjWirtingerDeriv g x

The conjugate Wirtinger derivative commutes with multiplication by a complex constant.

theorem TauCeti.conjWirtingerDeriv_apply_eq_conjWirtingerDeriv_line {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) (v : V) : (conjWirtingerDeriv g x) v = (conjWirtingerDeriv (fun (t : ℂ) => g (x + t • v)) 0) 1

The conjugate Wirtinger derivative in the direction v is the one-variable conjugate Wirtinger derivative ∂/∂(conj t) of the restriction t ↦ g (x + t • v) to the complex line through x in the direction v.

theorem ContDiffAt.conjWirtingerDeriv_apply {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup W] [NormedSpace ℂ W] {g : V → W} {x : V} {m n : WithTop ℕ∞} (hg : ContDiffAt ℝ n g x) (hmn : m + 1 ≤ n) (v : V) : ContDiffAt ℝ m (fun (z : V) => (TauCeti.conjWirtingerDeriv g z) v) x

The conjugate Wirtinger derivative of a C^(m+1) map, evaluated on a fixed vector, is C^m.

@[simp]

theorem DifferentiableAt.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) : TauCeti.conjWirtingerDeriv g x = 0

For complex differentiable g, the conjugate Wirtinger derivative vanishes: this is the Cauchy–Riemann equation \bar∂g = 0.

@[simp]

theorem DifferentiableAt.wirtingerDeriv_eq_fderiv {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) : TauCeti.wirtingerDeriv g x = fderiv ℂ g x

For complex differentiable g, the Wirtinger derivative is the complex derivative.

theorem TauCeti.wirtingerDeriv_id {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] (x : V) : wirtingerDeriv id x = ContinuousLinearMap.id ℂ V

The Wirtinger derivative of the identity is the identity: ∂z = 1.

theorem TauCeti.conjWirtingerDeriv_id {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] (x : V) : conjWirtingerDeriv id x = 0

The conjugate Wirtinger derivative of the identity vanishes: \bar∂z = 0.

theorem TauCeti.conjWirtingerDeriv_ofReal_comp_apply {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] (f : V → ℝ) (x v : V) : (conjWirtingerDeriv (fun (y : V) => ↑(f y)) x) v = (starRingEnd ℂ) ((wirtingerDeriv (fun (y : V) => ↑(f y)) x) v)

For a real function, the conjugate Wirtinger derivative is the complex conjugate of the Wirtinger derivative.

theorem TauCeti.wirtingerDeriv_smul_apply {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup W] [NormedSpace ℂ W] {c : V → ℂ} {g : V → W} {x : V} (hc : DifferentiableAt ℝ c x) (hg : DifferentiableAt ℝ g x) (v : V) : (wirtingerDeriv (fun (y : V) => c y • g y) x) v = c x • (wirtingerDeriv g x) v + (wirtingerDeriv c x) v • g x

The product rule for the Wirtinger derivative: for a complex-valued factor c, ∂(c g) = c ∂g + (∂c) g.

theorem TauCeti.conjWirtingerDeriv_smul_apply {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup W] [NormedSpace ℂ W] {c : V → ℂ} {g : V → W} {x : V} (hc : DifferentiableAt ℝ c x) (hg : DifferentiableAt ℝ g x) (v : V) : (conjWirtingerDeriv (fun (y : V) => c y • g y) x) v = c x • (conjWirtingerDeriv g x) v + (conjWirtingerDeriv c x) v • g x

The product rule for the conjugate Wirtinger derivative: for a complex-valued factor c, \bar∂(c g) = c \bar∂g + (\bar∂c) g.

theorem TauCeti.norm_wirtingerDeriv_smul_sub_smul_le {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup W] [NormedSpace ℂ W] {χ : V → ℝ} {u : V → W} {x : V} (hχ : DifferentiableAt ℝ χ x) (hu : DifferentiableAt ℝ u x) (v : V) : ‖(wirtingerDeriv (fun (y : V) => χ y • u y) x) v - χ x • (wirtingerDeriv u x) v‖ ≤ ‖fderiv ℝ χ x‖ * ‖v‖ * ‖u x‖

Against a real factor χ, ∂(χ u) differs from χ ∂u by (∂χ) u, whose norm is at most ‖Dχ‖ ‖v‖ ‖u‖.

theorem TauCeti.norm_conjWirtingerDeriv_smul_sub_smul_le {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup W] [NormedSpace ℂ W] {χ : V → ℝ} {u : V → W} {x : V} (hχ : DifferentiableAt ℝ χ x) (hu : DifferentiableAt ℝ u x) (v : V) : ‖(conjWirtingerDeriv (fun (y : V) => χ y • u y) x) v - χ x • (conjWirtingerDeriv u x) v‖ ≤ ‖fderiv ℝ χ x‖ * ‖v‖ * ‖u x‖

Against a real factor χ, \bar∂(χ u) differs from χ \bar∂u by (\bar∂χ) u, whose norm is at most ‖Dχ‖ ‖v‖ ‖u‖.

theorem TauCeti.conjWirtingerDeriv_eq_sum_smul {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup W] [NormedSpace ℂ W] {f : V → W} {x : V} {ι : Type u_3} {s : Finset ι} {c : ι → ℂ} {g : ι → V → W} (h : fderiv ℝ f x = ∑ i ∈ s, c i • fderiv ℝ (g i) x) : conjWirtingerDeriv f x = ∑ i ∈ s, c i • conjWirtingerDeriv (g i) x

The conjugate Wirtinger derivative depends complex-linearly on the real derivative: if Df(x) = ∑ cᵢ Dgᵢ(x) with complex coefficients, then \bar∂f(x) = ∑ cᵢ \bar∂gᵢ(x).

theorem TauCeti.conjWirtingerDeriv_fun_sum {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup W] [NormedSpace ℂ W] {ι : Type u_3} {s : Finset ι} {g : ι → V → W} {x : V} (h : ∀ i ∈ s, DifferentiableAt ℝ (g i) x) : conjWirtingerDeriv (fun (y : V) => ∑ i ∈ s, g i y) x = ∑ i ∈ s, conjWirtingerDeriv (g i) x

The conjugate Wirtinger derivative of a finite sum of real-differentiable functions is the sum of their conjugate Wirtinger derivatives.

theorem TauCeti.conjWirtingerDeriv_fun_mul {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] {f g : V → ℂ} {x : V} (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) : conjWirtingerDeriv (fun (y : V) => f y * g y) x = f x • conjWirtingerDeriv g x + g x • conjWirtingerDeriv f x

The Leibniz rule for the conjugate Wirtinger derivative: \bar∂(f g) = f \bar∂g + g \bar∂f.

theorem TauCeti.conjWirtingerDeriv_fun_pow {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] {f : V → ℂ} {x : V} (hf : DifferentiableAt ℝ f x) (n : ℕ) : conjWirtingerDeriv (fun (y : V) => f y ^ n) x = (↑n * f x ^ (n - 1)) • conjWirtingerDeriv f x

The conjugate Wirtinger derivative of a power: \bar∂(fⁿ) = n f^(n-1) \bar∂f.

theorem TauCeti.wirtingerDeriv_apply_eq_smul_apply_one {W : Type u_2} [NormedAddCommGroup W] [NormedSpace ℂ W] {f : ℂ → W} (x v : ℂ) : (wirtingerDeriv f x) v = v • (wirtingerDeriv f x) 1

In one variable the Wirtinger derivative is determined by its value at 1.

theorem TauCeti.conjWirtingerDeriv_apply_eq_conj_smul_apply_one {W : Type u_2} [NormedAddCommGroup W] [NormedSpace ℂ W] {f : ℂ → W} (x v : ℂ) : (conjWirtingerDeriv f x) v = (starRingEnd ℂ) v • (conjWirtingerDeriv f x) 1

In one variable the conjugate Wirtinger derivative is determined by its value at 1 through complex-antilinearity.

theorem TauCeti.fderiv_apply_eq_smul_wirtingerDeriv_add_smul_conjWirtingerDeriv {W : Type u_2} [NormedAddCommGroup W] [NormedSpace ℂ W] {f : ℂ → W} (x v : ℂ) : (fderiv ℝ f x) v = v • (wirtingerDeriv f x) 1 + (starRingEnd ℂ) v • (conjWirtingerDeriv f x) 1

In one variable the real differential is the sum of its dz and dbar z terms. This identity also holds for the totalized derivative, without a differentiability assumption.

theorem TauCeti.norm_fderiv_le_norm_wirtingerDeriv_add_norm_conjWirtingerDeriv {W : Type u_2} [NormedAddCommGroup W] [NormedSpace ℂ W] (f : ℂ → W) (x : ℂ) : ‖fderiv ℝ f x‖ ≤ ‖(wirtingerDeriv f x) 1‖ + ‖(conjWirtingerDeriv f x) 1‖

In one variable the real derivative is controlled by its two Wirtinger parts: ‖Df(x)‖ ≤ ‖∂f(x)‖ + ‖bar∂f(x)‖.

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

In one variable the conjugate Wirtinger derivative vanishes exactly when its value at 1 vanishes, since it is complex-antilinear.

Second conjugate Wirtinger derivatives

theorem ContDiffOn.conjWirtingerDeriv_apply_of_isOpen {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup W] [NormedSpace ℂ W] {g : V → W} {s : Set V} {m n : WithTop ℕ∞} (hg : ContDiffOn ℝ n g s) (hs : IsOpen s) (hmn : m + 1 ≤ n) (v : V) : ContDiffOn ℝ m (fun (y : V) => (TauCeti.conjWirtingerDeriv g y) v) s

A conjugate Wirtinger derivative of a C^{m+1} map on an open set is C^m there.

theorem ContDiffAt.hasFDerivAt_conjWirtingerDeriv_apply {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup W] [NormedSpace ℂ W] {g : V → W} {x : V} (hg : ContDiffAt ℝ 2 g x) (u : V) : HasFDerivAt (fun (y : V) => (TauCeti.conjWirtingerDeriv g y) u) (2⁻¹ • ((fderiv ℝ (fderiv ℝ g) x).flip u + Complex.I • (fderiv ℝ (fderiv ℝ g) x).flip (Complex.I • u))) x

For a C² map, the conjugate Wirtinger derivative y ↦ \bar∂g(y) u in a fixed direction u is differentiable, with derivative built from the second derivative of g.

theorem TauCeti.conjWirtingerDeriv_conjWirtingerDeriv_comm {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup W] [NormedSpace ℂ W] {g : V → W} {x : V} (hg : ContDiffAt ℝ 2 g x) (v w : V) : (conjWirtingerDeriv (fun (y : V) => (conjWirtingerDeriv g y) v) x) w = (conjWirtingerDeriv (fun (y : V) => (conjWirtingerDeriv g y) w) x) v

Symmetry of second conjugate Wirtinger derivatives. For a C² map, \bar∂_w \bar∂_v g = \bar∂_v \bar∂_w g; on coordinate vectors this is ∂²g / ∂(conj z_j) ∂(conj z_k) = ∂²g / ∂(conj z_k) ∂(conj z_j).