The Levi form of a real function on a complex vector space

For a real-valued function f on a complex normed space V, the Levi form of f at x is the Levi form LinearMap.BilinForm.leviForm of its real second derivative D²f(x): the sesquilinear form leviForm f x whose real and imaginary parts are

Re (leviForm f x v w) = (D²f(x)(v, w) + D²f(x)(I • v, I • w)) / 4, Im (leviForm f x v w) = (D²f(x)(I • v, w) - D²f(x)(v, I • w)) / 4.

In holomorphic coordinates z_j = x_j + I y_j with coordinate vectors e_j, its matrix entries are the Wirtinger second derivatives, with the arguments reversed: for C² f, leviForm f x (e_k) (e_j) = ∂²f / ∂z_j ∂(conj z_k). For C² f its diagonal value leviForm f x v v is the real number (D²f(x)(v, v) + D²f(x)(I • v, I • v)) / 4. Unlike the real Hessian, which is intrinsic only at critical points, the Levi form transforms as a Hermitian form under holomorphic changes of variables at every point. Positive definiteness of the Levi form is strict plurisubharmonicity.

This file gives the calculus of the Levi form: its value on the diagonal in terms of the Hessian quadratic form, Hermitian symmetry, the sum rule, the product rule, the rule for post-composition with a function of one real variable, invariance under holomorphic maps, and the vanishing of the Levi form of the real part of a holomorphic function.

It also shows that strict positivity of the Levi form survives small C² perturbations. The real part of the Levi diagonal moves by at most ‖D²g(y) - D²f(x)‖ ‖v‖² / 2 when (f, x) is replaced by (g, y). On a finite-dimensional space a Levi form which depends continuously on the point and is positive definite at every point of a compact set has a uniform lower bound c ‖v‖² there, and the set of continuous bilinear forms with positive definite Levi form is open. Consequently, for f whose second derivative is continuous on a set U, strict Levi positivity of f on U is open in the fine (Whitney) C² topology: it survives every perturbation whose second derivative stays within a continuous positive tolerance ε(x) of that of f.

Finally, it gives the inertia of a Levi flat function, such as the real part of a holomorphic function.

Main definitions

• TauCeti.leviForm f x: the Levi form of f : V → ℝ at x.

Main results

• TauCeti.leviForm_apply_self: the diagonal of the Levi form is one quarter of Hess f(v, v) + Hess f(I • v, I • v).
• TauCeti.re_leviForm_nonpos_of_isLocalMax: at a local maximum, the Levi form is nonpositive on every diagonal.
• TauCeti.isSymm_leviForm: the Levi form of a C² function is Hermitian.
• TauCeti.leviForm_add, TauCeti.leviForm_sum, TauCeti.leviForm_neg, TauCeti.leviForm_smul: the Levi form is real linear in the function.
• TauCeti.leviForm_mul_apply: the product rule L(f g) = f L g + g L f + (conj (∂f) ⊗ ∂g + conj (∂g) ⊗ ∂f).
• TauCeti.leviForm_scalar_comp_apply: the composition rule L(φ ∘ f) = φ'(f) L f + φ''(f) conj (∂f) ⊗ ∂f, and TauCeti.le_re_leviForm_scalar_comp_apply_self: where φ'' ≥ 0, the diagonal of L(φ ∘ f) dominates φ'(f) times the diagonal of L f.
• TauCeti.leviForm_comp_apply: invariance under holomorphic maps, L(f ∘ g)(v, w) = L f(Dg v, Dg w); in particular the Levi form transforms as a Hermitian form under holomorphic changes of coordinates.
• TauCeti.hessianQuadraticForm_re, TauCeti.leviForm_re_eq_zero: the real Hessian of the real part of a holomorphic function is the real part of its complex Hessian, and its Levi form vanishes (it is pluriharmonic).
• TauCeti.abs_re_leviForm_apply_self_sub_le: the Levi diagonal is Lipschitz in the second derivative, with constant ‖v‖² / 2.
• IsCompact.exists_pos_mul_sq_norm_le_re_leviForm: a continuous family of bilinear forms whose Levi forms are positive definite on a compact set has a uniform lower bound c ‖v‖² there.
• IsCompact.exists_pos_forall_sub_mul_sq_norm_le_re_leviForm: for f with second derivative continuous on a compact set K and Levi form positive definite there, the Levi form has a uniform lower bound c ‖v‖² on K, which a perturbation lowers by at most half the change of the second derivative.
• TauCeti.isOpen_setOf_forall_re_leviForm_toBilinForm_pos: positive definiteness of the Levi form is an open condition on continuous bilinear forms.
• TauCeti.exists_continuousOn_pos_forall_re_leviForm_pos: strict Levi positivity is open in the fine C² topology, with a continuous positive tolerance function.
• TauCeti.morseIndex_neg_eq_of_leviForm_eq_zero, TauCeti.morseIndex_eq_finrank_of_leviForm_eq_zero: if the Levi form vanishes, then multiplication by I exchanges the positive and negative directions of the Hessian, so a nondegenerate Hessian has Morse index the complex dimension.

Here ∂f = (Df(x)(·) - I * Df(x)(I • ·)) / 2 is the complex-linear part of the real differential. The statements use the complex-linear extension StrongDual.extendRCLike (Df(x)) = 2 ∂f, which accounts for their factor 1/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.
• J. Milnor, Morse Theory, Princeton University Press, 1963, Section 7.

noncomputable def TauCeti.leviForm {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] (f : V → ℝ) (x : V) : V →ₗ⋆[ℂ] V →ₗ[ℂ] ℂ

The Levi form of a real function f at x: the sesquilinear form (D²f(x)(v, w) + D²f(x)(I • v, I • w) + I * (D²f(x)(I • v, w) - D²f(x)(v, I • w))) / 4, conjugate-linear in v and complex-linear in w. Its matrix entries in holomorphic coordinates are the Wirtinger derivatives, with the arguments reversed: for C² f and coordinate vectors e_j, leviForm f x (e_k) (e_j) = ∂²f / ∂z_j ∂(conj z_k).

theorem TauCeti.leviForm_def {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] (f : V → ℝ) (x : V) : leviForm f x = (fderiv ℝ (fderiv ℝ f) x).toBilinForm.leviForm

@[simp]

theorem TauCeti.re_leviForm_apply {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] (f : V → ℝ) (x v w : V) : (((leviForm f x) v) w).re = (((fderiv ℝ (fderiv ℝ f) x) v) w + ((fderiv ℝ (fderiv ℝ f) x) (Complex.I • v)) (Complex.I • w)) / 4

The real part of the Levi form.

@[simp]

theorem TauCeti.im_leviForm_apply {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] (f : V → ℝ) (x v w : V) : (((leviForm f x) v) w).im = (((fderiv ℝ (fderiv ℝ f) x) (Complex.I • v)) w - ((fderiv ℝ (fderiv ℝ f) x) v) (Complex.I • w)) / 4

The imaginary part of the Levi form.

theorem TauCeti.leviForm_apply_self {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] {f : V → ℝ} {x : V} (hf : ContDiffAt ℝ 2 f x) (v : V) : ((leviForm f x) v) v = ↑(((hessianQuadraticForm f x) v + (hessianQuadraticForm f x) (Complex.I • v)) / 4)

The diagonal of the Levi form. For a C² function, leviForm f x v v is the real number (Hess f(v, v) + Hess f(I • v, I • v)) / 4.

theorem TauCeti.re_leviForm_nonpos_of_isLocalMax {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] {f : V → ℝ} {x : V} (hf : ContDiffAt ℝ 2 f x) (hmax : IsLocalMax f x) (v : V) : (((leviForm f x) v) v).re ≤ 0

At a local maximum of a real C² function, the Levi form is nonpositive on the diagonal.

theorem TauCeti.isSymm_leviForm {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] {f : V → ℝ} {x : V} (hf : ContDiffAt ℝ 2 f x) : (leviForm f x).IsSymm

The Levi form of a C² function is Hermitian.

theorem TauCeti.leviForm_congr_of_eventuallyEq {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] {f g : V → ℝ} {x : V} (hfg : f =ᶠ[nhds x] g) : leviForm f x = leviForm g x

The Levi form depends only on the germ of the function at the point.

theorem TauCeti.leviForm_add {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] {f g : V → ℝ} {x : V} (hf : ContDiffAt ℝ 2 f x) (hg : ContDiffAt ℝ 2 g x) : leviForm (f + g) x = leviForm f x + leviForm g x

The sum rule.

@[simp]

theorem TauCeti.leviForm_neg {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] (f : V → ℝ) (x : V) : leviForm (-f) x = -leviForm f x

Negating a function negates its Levi form.

@[simp]

theorem TauCeti.leviForm_smul {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] (a : ℝ) (f : V → ℝ) (x : V) : leviForm (a • f) x = ↑a • leviForm f x

The Levi form is real homogeneous in the function.

theorem TauCeti.leviForm_sum {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] {x : V} {ι : Type u_3} (s : Finset ι) {f : ι → V → ℝ} (hf : ∀ i ∈ s, ContDiffAt ℝ 2 (f i) x) : leviForm (∑ i ∈ s, f i) x = ∑ i ∈ s, leviForm (f i) x

The sum rule for finite sums.

theorem TauCeti.leviForm_mul_apply {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] {f g : V → ℝ} {x : V} (hf : ContDiffAt ℝ 2 f x) (hg : ContDiffAt ℝ 2 g x) (v w : V) : ((leviForm (f * g) x) v) w = ↑(f x) * ((leviForm g x) v) w + ↑(g x) * ((leviForm f x) v) w + 4⁻¹ * ((starRingEnd ℂ) ((StrongDual.extendRCLike (fderiv ℝ f x)) v) * (StrongDual.extendRCLike (fderiv ℝ g x)) w + (starRingEnd ℂ) ((StrongDual.extendRCLike (fderiv ℝ g x)) v) * (StrongDual.extendRCLike (fderiv ℝ f x)) w)

The product rule for the Levi form. Writing ∂f for the complex-linear extension StrongDual.extendRCLike of the real differential Df(x), the Levi form of f g at x is f(x) L g + g(x) L f + (conj (∂f v) ∂g w + conj (∂g v) ∂f w) / 4.

theorem TauCeti.leviForm_scalar_comp_apply {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] {f : V → ℝ} {x : V} {φ : ℝ → ℝ} (hφ : ContDiffAt ℝ 2 φ (f x)) (hf : ContDiffAt ℝ 2 f x) (v w : V) : ((leviForm (φ ∘ f) x) v) w = ↑(deriv φ (f x)) * ((leviForm f x) v) w + ↑(iteratedDeriv 2 φ (f x)) * (4⁻¹ * ((starRingEnd ℂ) ((StrongDual.extendRCLike (fderiv ℝ f x)) v) * (StrongDual.extendRCLike (fderiv ℝ f x)) w))

The composition rule for post-composition with a function of one real variable. Writing ∂f for the complex-linear extension StrongDual.extendRCLike of Df(x), the Levi form of φ ∘ f at x is φ'(f x) L f + φ''(f x) conj (∂f v) ∂f w / 4.

theorem TauCeti.le_re_leviForm_scalar_comp_apply_self {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] {f : V → ℝ} {x : V} {φ : ℝ → ℝ} (hφ : ContDiffAt ℝ 2 φ (f x)) (hf : ContDiffAt ℝ 2 f x) (hφ₂ : 0 ≤ iteratedDeriv 2 φ (f x)) (v : V) : deriv φ (f x) * (((leviForm f x) v) v).re ≤ (((leviForm (φ ∘ f) x) v) v).re

Post-composition with a convex function. If φ'' ≥ 0 at f x, then the diagonal of the Levi form of φ ∘ f dominates φ'(f x) times the diagonal of the Levi form of f. In particular, if moreover φ'(f x) > 0, post-composition with φ preserves strict positivity of the Levi form at x.

theorem TauCeti.leviForm_comp_apply {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup W] [NormedSpace ℂ W] {f : V → ℝ} {g : W → V} {b : W} (hf : ContDiffAt ℝ 2 f (g b)) (hg : ContDiffAt ℂ 2 g b) (v w : W) : ((leviForm (f ∘ g) b) v) w = ((leviForm f (g b)) ((fderiv ℂ g b) v)) ((fderiv ℂ g b) w)

Invariance under holomorphic maps. If g : W → V is complex C² at b and f is real C² at g b, then the Levi form of f ∘ g at b is the Levi form of f at g b evaluated on the images under the complex derivative of g. The second derivative of g contributes to the real Hessian of f ∘ g but not to its Levi form, because it is complex bilinear.

The real part of a holomorphic function

theorem TauCeti.hessianQuadraticForm_re {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] {x : V} {g : V → ℂ} (hg : ContDiffAt ℂ 2 g x) (v : V) : (hessianQuadraticForm (fun (z : V) => (g z).re) x) v = (((fderiv ℂ (fderiv ℂ g) x) v) v).re

The Hessian quadratic form of the real part of a holomorphic function is the real part of its complex Hessian.

@[simp]

theorem TauCeti.leviForm_re_eq_zero {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] {x : V} {g : V → ℂ} (hg : ContDiffAt ℂ 2 g x) : leviForm (fun (z : V) => (g z).re) x = 0

The real part of a holomorphic function is pluriharmonic: its Levi form vanishes.

Perturbations of the Levi form

theorem ContinuousLinearMap.abs_re_leviForm_toBilinForm_apply_self_le {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] (B : V →L[ℝ] V →L[ℝ] ℝ) (v : V) : |((B.toBilinForm.leviForm v) v).re| ≤ ‖B‖ * ‖v‖ ^ 2 / 2

The real part of the Levi diagonal of a continuous real bilinear form B is at most ‖B‖ ‖v‖² / 2 in absolute value.

theorem TauCeti.abs_re_leviForm_apply_self_sub_le {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] (f g : V → ℝ) (x y v : V) : |(((leviForm g y) v) v).re - (((leviForm f x) v) v).re| ≤ ‖fderiv ℝ (fderiv ℝ g) y - fderiv ℝ (fderiv ℝ f) x‖ * ‖v‖ ^ 2 / 2

The Levi diagonal is Lipschitz in the second derivative. Replacing f at x by g at y changes the real part of the Levi diagonal by at most ‖D²g(y) - D²f(x)‖ ‖v‖² / 2.

theorem IsCompact.exists_pos_mul_sq_norm_le_re_leviForm {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] [FiniteDimensional ℂ V] {X : Type u_3} [TopologicalSpace X] {K : Set X} (hK : IsCompact K) {B : X → V →L[ℝ] V →L[ℝ] ℝ} (hB : ContinuousOn B K) (hpos : ∀ x ∈ K, ∀ (v : V), v ≠ 0 → 0 < (((B x).toBilinForm.leviForm v) v).re) : ∃ c > 0, ∀ x ∈ K, ∀ (v : V), c * ‖v‖ ^ 2 ≤ (((B x).toBilinForm.leviForm v) v).re

Uniform Levi positivity on compact sets. Let B be a family of continuous real bilinear forms on a finite-dimensional complex space, continuous on a compact set K. If the Levi form of every B x, x ∈ K, is positive definite, then it is bounded below by c ‖v‖² for a single c > 0.

theorem IsCompact.exists_pos_forall_sub_mul_sq_norm_le_re_leviForm {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] [FiniteDimensional ℂ V] {K : Set V} (hK : IsCompact K) {f : V → ℝ} (hf : ContinuousOn (fun (x : V) => fderiv ℝ (fderiv ℝ f) x) K) (hpos : ∀ x ∈ K, ∀ (v : V), v ≠ 0 → 0 < (((TauCeti.leviForm f x) v) v).re) : ∃ c > 0, ∀ (g : V → ℝ), ∀ x ∈ K, ∀ (v : V), (c - ‖fderiv ℝ (fderiv ℝ g) x - fderiv ℝ (fderiv ℝ f) x‖ / 2) * ‖v‖ ^ 2 ≤ (((TauCeti.leviForm g x) v) v).re

Continuity of the Levi lower bound under C² perturbations on compact sets. Let f have second derivative continuous on a compact set K of a finite-dimensional complex space, with positive definite Levi form at every point of K. Then there is c > 0 such that, for every function g, the Levi diagonal of g at x ∈ K is at least (c - ‖D²g(x) - D²f(x)‖ / 2) ‖v‖². In particular every g whose second derivative stays within 2 c of that of f on K has positive definite Levi form on K.

theorem TauCeti.isOpen_setOf_forall_re_leviForm_toBilinForm_pos {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] [FiniteDimensional ℂ V] : IsOpen {B : V →L[ℝ] V →L[ℝ] ℝ | ∀ (v : V), v ≠ 0 → 0 < ((B.toBilinForm.leviForm v) v).re}

Positivity of the Levi form is an open condition. On a finite-dimensional complex space, the continuous real bilinear forms whose Levi form is positive definite form an open set.

theorem TauCeti.exists_continuousOn_pos_forall_re_leviForm_pos {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] [FiniteDimensional ℂ V] {U : Set V} {f : V → ℝ} (hf : ContinuousOn (fun (x : V) => fderiv ℝ (fderiv ℝ f) x) U) (hpos : ∀ x ∈ U, ∀ (v : V), v ≠ 0 → 0 < (((leviForm f x) v) v).re) : ∃ (ε : V → ℝ), ContinuousOn ε U ∧ (∀ x ∈ U, 0 < ε x) ∧ ∀ (g : V → ℝ), ∀ x ∈ U, ‖fderiv ℝ (fderiv ℝ g) x - fderiv ℝ (fderiv ℝ f) x‖ < ε x → ∀ (v : V), v ≠ 0 → 0 < (((leviForm g x) v) v).re

Strict Levi positivity is open in the fine C² topology. Let f have second derivative continuous on a set U of a finite-dimensional complex space, with positive definite Levi form at every point of U. Then there is a tolerance ε, continuous and positive on U, such that the Levi form of any function g is positive definite at each x ∈ U where ‖D²g(x) - D²f(x)‖ < ε x.

Inertia of a Levi-flat function

theorem TauCeti.morseIndex_neg_eq_of_leviForm_eq_zero {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] {f : V → ℝ} {x : V} (h : leviForm f x = 0) : morseIndex (-f) x = morseIndex f x

Inertia of a Levi-flat function. If the Levi form of f vanishes at x, then multiplication by I exchanges the positive and negative directions of the Hessian, so f and -f have the same Morse index at x.

theorem TauCeti.morseIndex_eq_finrank_of_leviForm_eq_zero {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] {f : V → ℝ} {x : V} (h : leviForm f x = 0) (hnd : QuadraticMap.Nondegenerate) : morseIndex f x = Module.finrank ℂ V

The Morse index of a Levi-flat function. If the Levi form of f vanishes at x and its Hessian there is nondegenerate, then the Morse index of f at x is the complex dimension. This applies to the real part of a holomorphic function, by TauCeti.leviForm_re_eq_zero.