Wirtinger derivatives and the Levi form

The Levi form TauCeti.leviForm f x of a real function f is defined from the real second derivative. This file compares it with the second Wirtinger derivatives TauCeti.wirtingerDeriv and TauCeti.conjWirtingerDeriv: for C² real f, the mixed Wirtinger derivative ∂²f / ∂z_j ∂(conj z_k), taken in either order, is the Levi form entry leviForm f x (e_k) (e_j). Consequently, in any complex basis e of V, the Hermitian form with matrix L_{j \bar k} = ∂²f / ∂z_j ∂(conj z_k) evaluated at the coordinates ξ_j = dz_j(v) of a real tangent vector v is one quarter of the real second-derivative sum D²f(x)(v, v) + D²f(x)(I • v, I • v).

Main results

• TauCeti.wirtingerDeriv_conjWirtingerDeriv_eq_leviForm, TauCeti.conjWirtingerDeriv_wirtingerDeriv_eq_leviForm: the mixed second Wirtinger derivatives of a C² real function, in either order, are the entries of its Levi form.
• TauCeti.toMatrix₂_leviForm: the matrix of the Levi form in a complex basis is the matrix of mixed second Wirtinger derivatives.
• TauCeti.sum_wirtingerDeriv_conjWirtingerDeriv_eq_hessianQuadraticForm: the Levi matrix evaluated on the coordinates of v is (D²f(x)(v, v) + D²f(x)(I • v, I • v)) / 4.

References

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

theorem TauCeti.wirtingerDeriv_conjWirtingerDeriv_eq_leviForm {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] {f : V → ℝ} {x : V} (hf : ContDiffAt ℝ 2 f x) (v w : V) : (wirtingerDeriv (fun (y : V) => (conjWirtingerDeriv (fun (z : V) => ↑(f z)) y) v) x) w = ((leviForm f x) v) w

Wirtinger comparison. For a C² real function f, the mixed second Wirtinger derivative ∂_w \bar∂_v f, that is ∂²f / ∂z_j ∂(conj z_k) for coordinate vectors v = e_k and w = e_j, is the Levi form leviForm f x v w.

theorem TauCeti.conjWirtingerDeriv_wirtingerDeriv_eq_leviForm {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] {f : V → ℝ} {x : V} (hf : ContDiffAt ℝ 2 f x) (v w : V) : (conjWirtingerDeriv (fun (y : V) => (wirtingerDeriv (fun (z : V) => ↑(f z)) y) w) x) v = ((leviForm f x) v) w

Wirtinger comparison, in the other order. For a C² real function f, the mixed second Wirtinger derivative \bar∂_v ∂_w f is the Levi form leviForm f x v w.

theorem TauCeti.toMatrix₂_leviForm {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] {f : V → ℝ} {x : V} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (hf : ContDiffAt ℝ 2 f x) (b : Module.Basis ι ℂ V) : (LinearMap.toMatrix₂ b b) (leviForm f x) = Matrix.of fun (k j : ι) => (wirtingerDeriv (fun (y : V) => (conjWirtingerDeriv (fun (z : V) => ↑(f z)) y) (b k)) x) (b j)

The Levi matrix. In a complex basis b of V, the matrix of the Levi form of a C² real function has (k, j) entry the mixed second Wirtinger derivative ∂²f / ∂z_j ∂(conj z_k).

theorem TauCeti.sum_wirtingerDeriv_conjWirtingerDeriv_eq_hessianQuadraticForm {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] {f : V → ℝ} {x : V} {ι : Type u_2} [Fintype ι] (hf : ContDiffAt ℝ 2 f x) (b : Module.Basis ι ℂ V) (v : V) : ∑ j : ι, ∑ k : ι, (b.repr v) j * (starRingEnd ℂ) ((b.repr v) k) * (wirtingerDeriv (fun (y : V) => (conjWirtingerDeriv (fun (z : V) => ↑(f z)) y) (b k)) x) (b j) = ↑(((hessianQuadraticForm f x) v + (hessianQuadraticForm f x) (Complex.I • v)) / 4)

The diagonal of the Levi matrix. In a complex basis b of V, with holomorphic coordinates ξ_j = dz_j(v) of v, the Hermitian form ∑ L_{j \bar k} ξ_j conj ξ_k with Levi matrix L_{j \bar k} = ∂²f / ∂z_j ∂(conj z_k) of a C² real function f is one quarter of the real second-derivative sum D²f(x)(v, v) + D²f(x)(I • v, I • v).