Levi convex boundaries

A local C² defining function for an open set U at a boundary point p is a C² function ρ on an open neighborhood V of p, vanishing at p, with nonzero derivative at p, such that U ∩ V is the set where ρ is negative. The complex tangent space at p is the kernel of the complex-linear part of the derivative of ρ. The set U satisfies the Levi condition at p if the Levi form of every local defining function is positive semidefinite on the complex tangent space; it is Levi pseudoconvex if this holds at every boundary point. Quantifying over all defining functions avoids the lemma that two defining functions differ by a positive factor.

This file proves that convex open sets are Levi pseudoconvex: along a real tangent line the defining function vanishes to first order at p, so a negative second derivative would put two symmetric points of the line into U and, by convexity, the boundary point itself.

It also provides the complex-linear part complexPart ℓ of a real functional ℓ, with ℓ (ζ • c) = Re (ζ * complexPart ℓ c), and the decomposition of a symmetric real bilinear form along a complex line into a Hermitian part, the Levi form, and the real part of a complex quadratic term. Both are used for the Levi polynomial in LeviConvexity.Necessity.

References: [Fritzsche–Grauert][FritzscheGrauert2002] (2002), Chapter II, Section 4; [Range][Range1986] (1986), Chapter II, Sections 2.4–2.6.

Main definitions

• complexPart: The complex-linear part of a real functional: ℓ c - I * ℓ (I • c).
• IsLocalDefiningFunction: A local C² defining function for U at p on the open neighborhood V: ρ p = 0, the real derivative of ρ at p is nonzero, and U ∩ V is the negative sublevel set of ρ in V.
• HasC2Boundary: A set has C² boundary if every boundary point has a local defining function.
• IsComplexTangent: The complex tangent space of the level set of ρ at p: the kernel of the complex-linear part of the derivative.
• IsLeviPseudoconvexAt: The Levi condition at a boundary point: the Levi form of every local defining function is positive semidefinite on the complex tangent space.
• IsLeviPseudoconvex: Levi pseudoconvexity: the Levi condition at every boundary point.

Main results

• bilinear_smul_smul_eq: Quadratic decomposition along a complex line. For a symmetric real bilinear form B, B (ζ • w) (ζ • w) / 2 is ‖ζ‖ ^ 2 times the Hermitian part (B w w + B (I • w) (I • w)) / 4 plus the real part of ζ ^ 2 times the complex quadratic coefficient (B w w - B (I • w) (I • w)) / 4 - I / 2 * B w (I • w).
• Convex.isLeviPseudoconvex: Convex open sets are Levi pseudoconvex ([Range][Range1986], Lemma 2.10).

References

• [K. Fritzsche and H. Grauert, From Holomorphic Functions to Complex Manifolds][FritzscheGrauert2002]
• [R. M. Range, Holomorphic Functions and Integral Representations in Several Complex Variables][Range1986]

@[reducible, inline]

noncomputable abbrev SeveralComplexVariables.complexPart {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (ℓ : E →L[ℝ] ℝ) : E →L[ℂ] ℂ

The complex-linear part c ↦ ℓ c - I * ℓ (I • c) of a real functional: Mathlib's StrongDual.extendRCLike with the scalar field fixed to ℂ.

Equations

• SeveralComplexVariables.complexPart ℓ = StrongDual.extendRCLike ℓ

theorem SeveralComplexVariables.complexPart_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (ℓ : E →L[ℝ] ℝ) (c : E) : (complexPart ℓ) c = ↑(ℓ c) - Complex.I * ↑(ℓ (Complex.I • c))

The defining formula of the complex-linear part.

theorem SeveralComplexVariables.apply_smul_eq_re_mul_complexPart {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (ℓ : E →L[ℝ] ℝ) (ζ : ℂ) (c : E) : ℓ (ζ • c) = (ζ * (complexPart ℓ) c).re

A real functional on a complex multiple is the real part of the complex multiple of its complex-linear part.

theorem SeveralComplexVariables.re_complexPart {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (ℓ : E →L[ℝ] ℝ) (c : E) : ((complexPart ℓ) c).re = ℓ c

The real part of the complex part of a real functional is the functional itself.

theorem SeveralComplexVariables.exists_complexPart_ne_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {ℓ : E →L[ℝ] ℝ} (hℓ : ℓ ≠ 0) : ∃ (c : E), (complexPart ℓ) c ≠ 0

A nonzero real functional has a vector on which its complex-linear part is nonzero.

theorem SeveralComplexVariables.exists_complexPart_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {ℓ : E →L[ℝ] ℝ} (hℓ : ℓ ≠ 0) (q : ℂ) : ∃ (c : E), (complexPart ℓ) c = q

Every complex value is attained by the complex-linear part of a nonzero real functional.

theorem SeveralComplexVariables.bilinear_smul_smul_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (B : E →L[ℝ] E →L[ℝ] ℝ) {w : E} (hsymm : (B w) (Complex.I • w) = (B (Complex.I • w)) w) (ζ : ℂ) : 1 / 2 * (B (ζ • w)) (ζ • w) = ‖ζ‖ ^ 2 * (((B w) w + (B (Complex.I • w)) (Complex.I • w)) / 4) + (ζ ^ 2 * (↑(((B w) w - (B (Complex.I • w)) (Complex.I • w)) / 4) - Complex.I / 2 * ↑((B w) (Complex.I • w)))).re

Quadratic decomposition along a complex line. For a symmetric real bilinear form B, B (ζ • w) (ζ • w) / 2 is ‖ζ‖ ^ 2 times the Hermitian part (B w w + B (I • w) (I • w)) / 4 plus the real part of ζ ^ 2 times the complex quadratic coefficient (B w w - B (I • w) (I • w)) / 4 - I / 2 * B w (I • w).

structure SeveralComplexVariables.IsLocalDefiningFunction {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (U : Set E) (p : E) (ρ : E → ℝ) (V : Set E) : Prop

A local C² defining function for U at p on the open neighborhood V: ρ p = 0, the real derivative of ρ at p is nonzero, and U ∩ V is the negative sublevel set of ρ in V.

• isOpen : IsOpen V

  The defining neighborhood is open.

• mem : p ∈ V

  The boundary point lies in the defining neighborhood.

• contDiffOn : ContDiffOn ℝ 2 ρ V

  The defining function is twice continuously real differentiable.

• eq_zero : ρ p = 0

  The defining function vanishes at the boundary point.

• fderiv_ne : fderiv ℝ ρ p ≠ 0

  The real derivative is nonzero at the boundary point.

• inter_eq : U ∩ V = {z : E | ρ z < 0} ∩ V

  The domain is the negative sublevel set in the defining neighborhood.

def SeveralComplexVariables.HasC2Boundary {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (U : Set E) : Prop

A set has C² boundary if every boundary point has a local defining function.

Equations

• SeveralComplexVariables.HasC2Boundary U = ∀ p ∈ frontier U, ∃ (ρ : E → ℝ) (V : Set E), SeveralComplexVariables.IsLocalDefiningFunction U p ρ V

def SeveralComplexVariables.IsComplexTangent {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (ρ : E → ℝ) (p w : E) : Prop

The complex tangent space of the level set of ρ at p: the kernel of the complex-linear part of the derivative.

Equations

• SeveralComplexVariables.IsComplexTangent ρ p w = ((fderiv ℝ ρ p) w = 0 ∧ (fderiv ℝ ρ p) (Complex.I • w) = 0)

def SeveralComplexVariables.IsLeviPseudoconvexAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (U : Set E) (p : E) : Prop

The Levi condition at a boundary point: the Levi form of every local defining function is positive semidefinite on the complex tangent space.

Equations

• One or more equations did not get rendered due to their size.

def SeveralComplexVariables.IsLeviPseudoconvex {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (U : Set E) : Prop

Levi pseudoconvexity: the Levi condition at every boundary point.

Equations

• SeveralComplexVariables.IsLeviPseudoconvex U = ∀ p ∈ frontier U, SeveralComplexVariables.IsLeviPseudoconvexAt U p

theorem SeveralComplexVariables.IsComplexTangent.smul_I {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {ρ : E → ℝ} {p w : E} (h : IsComplexTangent ρ p w) : IsComplexTangent ρ p (Complex.I • w)

The complex tangent space is closed under multiplication by I.

theorem SeveralComplexVariables.IsLocalDefiningFunction.mem_of_neg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {U : Set E} {p : E} {ρ : E → ℝ} {V : Set E} (h : IsLocalDefiningFunction U p ρ V) {z : E} (hz : z ∈ V) (hρ : ρ z < 0) : z ∈ U

Points near p where the defining function is negative lie in U.

theorem SeveralComplexVariables.IsLocalDefiningFunction.neg_of_mem {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {U : Set E} {p : E} {ρ : E → ℝ} {V : Set E} (h : IsLocalDefiningFunction U p ρ V) {z : E} (hz : z ∈ V) (hU : z ∈ U) : ρ z < 0

Points of V in U have negative defining function.

theorem SeveralComplexVariables.IsLocalDefiningFunction.fderiv_fderiv_nonneg_of_convex {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {U : Set E} {p : E} {ρ : E → ℝ} {V : Set E} (hU : IsOpen U) (hconv : Convex ℝ U) (hp : p ∈ frontier U) (h : IsLocalDefiningFunction U p ρ V) {w : E} (hw : (fderiv ℝ ρ p) w = 0) : 0 ≤ ((fderiv ℝ (fderiv ℝ ρ) p) w) w

Along a real tangent direction, the second derivative of a defining function of a convex open set is nonnegative.

theorem Convex.isLeviPseudoconvex {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {U : Set E} (hU : IsOpen U) (hconv : Convex ℝ U) : SeveralComplexVariables.IsLeviPseudoconvex U

Convex open sets are Levi pseudoconvex ([Range][Range1986], Lemma 2.10).