Strict plurisubharmonicity, strong q-pseudoconvexity and the Morse index

Let f be a real function on a complex vector space V of complex dimension n. The function is strictly plurisubharmonic at x if its Levi form TauCeti.leviForm f x is positive definite, and strongly q-pseudoconvex at x if the Levi form is positive definite on some complex subspace of dimension at least n - q; here positivity means that the real part of the Levi diagonal is positive. When f is C² the Levi form is Hermitian (TauCeti.isSymm_leviForm), and this says that it has at least n - q positive eigenvalues. With this convention, which counts positive directions at the point itself, strong 0-pseudoconvexity is strict plurisubharmonicity. In the Andreotti–Grauert convention, which counts n - q + 1 positive directions, it is strong (q + 1)-convexity.

The main result bounds the real Morse index: if f is strongly q-pseudoconvex at x, then the negative index of inertia of the real Hessian of f at x is at most n + q; in particular a strictly plurisubharmonic function has Morse index at most n. The linear-algebraic input is LinearMap.BilinForm.sigNeg_add_finrank_le_of_re_leviForm_pos. Both conditions are preserved by restriction along holomorphic immersions and by post-composition with increasing convex functions of one real variable, and strict plurisubharmonicity is preserved by sums.

Strong q-pseudoconvexity is stable under C² perturbations. For a fixed positive complex subspace this follows by testing the Levi diagonal on its compact real unit sphere. Consequently the bilinear forms with at least dim_ℂ V - q positive directions form an open set. If the second derivative of f varies continuously on a set U, its distance from the complement of this open set gives a continuous positive tolerance on U within which every perturbation remains strongly q-pseudoconvex.

Main definitions

• TauCeti.IsStrictlyPlurisubharmonicAt f x: the Levi form of f at x is positive definite.
• TauCeti.IsStronglyPseudoconvexAt q f x: the Levi form of f at x is positive definite on a complex subspace of codimension at most q.

Main results

• TauCeti.isStrictlyPlurisubharmonicAt_iff_hessianQuadraticForm: strict plurisubharmonicity is positivity of Hess f(v, v) + Hess f(I • v, I • v).
• TauCeti.isStronglyPseudoconvexAt_zero_iff: strong 0-pseudoconvexity is strict plurisubharmonicity.
• TauCeti.IsStronglyPseudoconvexAt.morseIndex_le: the index bound λ ≤ n + q.
• TauCeti.IsStrictlyPlurisubharmonicAt.morseIndex_le: the index bound λ ≤ n.
• TauCeti.IsStronglyPseudoconvexAt.comp, TauCeti.IsStrictlyPlurisubharmonicAt.comp: restriction along a holomorphic map with injective derivative.
• TauCeti.IsStronglyPseudoconvexAt.scalar_comp, TauCeti.IsStrictlyPlurisubharmonicAt.scalar_comp: post-composition with a function φ with φ' > 0 and φ'' ≥ 0.
• TauCeti.isOpen_setOf_re_leviForm_posOnSubspace: having an admissible Levi-positive complex subspace is open on continuous bilinear forms.
• TauCeti.exists_continuousOn_pos_forall_isStronglyPseudoconvexAt: strong q-pseudoconvexity is open in the fine C² topology, with a varying positive tolerance.

References

• J. Milnor, Morse Theory, Princeton University Press, 1963, Section 7.
• R. Hain, Notes on the Morse theory of complex manifolds, Section 2.
• A. Andreotti and H. Grauert, Théorèmes de finitude pour la cohomologie des espaces complexes, Bull. Soc. Math. France 90 (1962).

def TauCeti.IsStrictlyPlurisubharmonicAt {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] (f : V → ℝ) (x : V) : Prop

A real function f is strictly plurisubharmonic at x if its Levi form at x is positive definite: 0 < Re (leviForm f x v v) for every v ≠ 0. For C² functions the Levi form is Hermitian, so its diagonal is real.

def TauCeti.IsStronglyPseudoconvexAt {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] [FiniteDimensional ℂ V] (q : ℕ) (f : V → ℝ) (x : V) : Prop

A real function f on a finite-dimensional complex space V is strongly q-pseudoconvex at x if there is a complex subspace P with dim_ℂ V ≤ dim_ℂ P + q on which the Levi form at x is positive definite: 0 < Re (leviForm f x v v) for every nonzero v ∈ P. When f is C² the Levi form is Hermitian, and by Sylvester's law of inertia for Hermitian forms the largest dimension of such a subspace is the number of positive eigenvalues, so the condition says that the Levi form has at least dim_ℂ V - q positive eigenvalues. For q ≥ dim_ℂ V the condition always holds, and strong 0-pseudoconvexity is strict plurisubharmonicity.

theorem TauCeti.isStrictlyPlurisubharmonicAt_iff {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] {f : V → ℝ} {x : V} : IsStrictlyPlurisubharmonicAt f x ↔ ∀ (v : V), v ≠ 0 → 0 < (((leviForm f x) v) v).re

The defining property of strict plurisubharmonicity.

theorem TauCeti.isStronglyPseudoconvexAt_iff {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] {f : V → ℝ} {x : V} {q : ℕ} [FiniteDimensional ℂ V] : IsStronglyPseudoconvexAt q f x ↔ ∃ (P : Submodule ℂ V), Module.finrank ℂ V ≤ Module.finrank ℂ ↥P + q ∧ ∀ v ∈ P, v ≠ 0 → 0 < (((leviForm f x) v) v).re

The defining property of strong q-pseudoconvexity.

theorem TauCeti.isStrictlyPlurisubharmonicAt_iff_hessianQuadraticForm {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] {f : V → ℝ} {x : V} : IsStrictlyPlurisubharmonicAt f x ↔ ∀ (v : V), v ≠ 0 → 0 < (hessianQuadraticForm f x) v + (hessianQuadraticForm f x) (Complex.I • v)

Strict plurisubharmonicity in terms of the real Hessian: f is strictly plurisubharmonic at x exactly when Hess f(v, v) + Hess f(I • v, I • v) > 0 for every v ≠ 0.

theorem TauCeti.IsStronglyPseudoconvexAt.mono {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] {f : V → ℝ} {x : V} {q r : ℕ} [FiniteDimensional ℂ V] (h : IsStronglyPseudoconvexAt q f x) (hqr : q ≤ r) : IsStronglyPseudoconvexAt r f x

Strong q-pseudoconvexity is weaker for larger q.

theorem TauCeti.IsStrictlyPlurisubharmonicAt.isStronglyPseudoconvexAt {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] {f : V → ℝ} {x : V} [FiniteDimensional ℂ V] (h : IsStrictlyPlurisubharmonicAt f x) (q : ℕ) : IsStronglyPseudoconvexAt q f x

A strictly plurisubharmonic function is strongly q-pseudoconvex for every q.

@[simp]

theorem TauCeti.isStronglyPseudoconvexAt_zero_iff {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] {f : V → ℝ} {x : V} [FiniteDimensional ℂ V] : IsStronglyPseudoconvexAt 0 f x ↔ IsStrictlyPlurisubharmonicAt f x

Strong 0-pseudoconvexity is strict plurisubharmonicity.

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

Strict plurisubharmonicity at a point depends only on the germ of the function there.

theorem TauCeti.IsStronglyPseudoconvexAt.congr_of_eventuallyEq {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] {f g : V → ℝ} {x : V} {q : ℕ} [FiniteDimensional ℂ V] (h : IsStronglyPseudoconvexAt q f x) (hfg : g =ᶠ[nhds x] f) : IsStronglyPseudoconvexAt q g x

Strong q-pseudoconvexity at a point depends only on the germ of the function there.

theorem TauCeti.IsStronglyPseudoconvexAt.morseIndex_le {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] {f : V → ℝ} {x : V} {q : ℕ} [FiniteDimensional ℂ V] (h : IsStronglyPseudoconvexAt q f x) : morseIndex f x ≤ Module.finrank ℂ V + q

The Morse index bound λ ≤ n + q. If f is strongly q-pseudoconvex at x, then the negative index of inertia of the real Hessian of f at x is at most dim_ℂ V + q.

theorem TauCeti.IsStrictlyPlurisubharmonicAt.morseIndex_le {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] {f : V → ℝ} {x : V} (h : IsStrictlyPlurisubharmonicAt f x) : morseIndex f x ≤ Module.finrank ℂ V

The Morse index bound λ ≤ n. The real Hessian of a strictly plurisubharmonic function has negative index of inertia at most the complex dimension.

theorem TauCeti.IsStrictlyPlurisubharmonicAt.comp {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup W] [NormedSpace ℂ W] {f : V → ℝ} {g : W → V} {b : W} (h : IsStrictlyPlurisubharmonicAt f (g b)) (hf : ContDiffAt ℝ 2 f (g b)) (hg : ContDiffAt ℂ 2 g b) (hg' : Function.Injective ⇑(fderiv ℂ g b)) : IsStrictlyPlurisubharmonicAt (f ∘ g) b

Restriction along a holomorphic immersion. If f is strictly plurisubharmonic at g b and the complex derivative of the holomorphic map g at b is injective, then f ∘ g is strictly plurisubharmonic at b.

theorem TauCeti.IsStronglyPseudoconvexAt.comp {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup W] [NormedSpace ℂ W] {q : ℕ} [FiniteDimensional ℂ V] [FiniteDimensional ℂ W] {f : V → ℝ} {g : W → V} {b : W} (h : IsStronglyPseudoconvexAt q f (g b)) (hf : ContDiffAt ℝ 2 f (g b)) (hg : ContDiffAt ℂ 2 g b) (hg' : Function.Injective ⇑(fderiv ℂ g b)) : IsStronglyPseudoconvexAt q (f ∘ g) b

Restriction along a holomorphic immersion. If f is strongly q-pseudoconvex at g b and the complex derivative of the holomorphic map g at b is injective, then f ∘ g is strongly q-pseudoconvex at b: the preimage of a positive subspace of codimension at most q is a positive subspace of codimension at most q.

theorem TauCeti.IsStrictlyPlurisubharmonicAt.scalar_comp {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] {f : V → ℝ} {x : V} {φ : ℝ → ℝ} (h : IsStrictlyPlurisubharmonicAt f x) (hφ : ContDiffAt ℝ 2 φ (f x)) (hf : ContDiffAt ℝ 2 f x) (hφ₁ : 0 < deriv φ (f x)) (hφ₂ : 0 ≤ iteratedDeriv 2 φ (f x)) : IsStrictlyPlurisubharmonicAt (φ ∘ f) x

Post-composition with a function φ of one real variable with φ'(f x) > 0 and φ''(f x) ≥ 0 preserves strict plurisubharmonicity at x.

theorem TauCeti.IsStronglyPseudoconvexAt.scalar_comp {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] {f : V → ℝ} {x : V} {q : ℕ} [FiniteDimensional ℂ V] {φ : ℝ → ℝ} (h : IsStronglyPseudoconvexAt q f x) (hφ : ContDiffAt ℝ 2 φ (f x)) (hf : ContDiffAt ℝ 2 f x) (hφ₁ : 0 < deriv φ (f x)) (hφ₂ : 0 ≤ iteratedDeriv 2 φ (f x)) : IsStronglyPseudoconvexAt q (φ ∘ f) x

Post-composition with a function φ of one real variable with φ'(f x) > 0 and φ''(f x) ≥ 0 preserves strong q-pseudoconvexity at x.

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

The sum of two C² functions strictly plurisubharmonic at x is strictly plurisubharmonic at x.

Perturbation openness

theorem TauCeti.isOpen_setOf_re_leviForm_posOnSubspace {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] (q : ℕ) : IsOpen {B : V →L[ℝ] V →L[ℝ] ℝ | ∃ (P : Submodule ℂ V), Module.finrank ℂ V ≤ Module.finrank ℂ ↥P + q ∧ ∀ v ∈ P, v ≠ 0 → 0 < ((B.toBilinForm.leviForm v) v).re}

Strong q-pseudoconvexity is open on bilinear forms. On a finite-dimensional complex space, the continuous real bilinear forms whose Levi form is positive definite on some complex subspace of codimension at most q form an open set. (If V is not finite-dimensional, then finrank ℂ V = 0 and the set is everything.)

The statement uses the additive dimension inequality from IsStronglyPseudoconvexAt, which also covers q ≥ dim_ℂ V without truncated subtraction.

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

Strong q-pseudoconvexity is open in the fine C² topology. Let the second derivative of f vary continuously on U, and suppose f is strongly q-pseudoconvex at every point of U. Then there is a tolerance ε, continuous and positive on U, such that every function whose second derivative differs from that of f by less than ε x remains strongly q-pseudoconvex at x.

No regularity of the perturbing function is required beyond the displayed pointwise control of its totalized second derivative.