Complex Morse theory, affine topology and weak Lefschetz
The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.
TheoremThe index bound for strongly q-pseudoconvex functions on a complex manifold#
At a
critical point x of a function f which is C² at x and strongly q-pseudoconvex at x, the
Morse index of f is at most dim_ℂ E + q.
TauCeti.IsManifoldStronglyPseudoconvexAt.manifoldMorseIndex_le.{u_1, u_2} {E : Type u_1}
{M : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] [TopologicalSpace M] [ChartedSpace E M]
{f : M → ℝ} {x : M} [FiniteDimensional ℂ E] [IsManifold (modelWithCornersSelf ℂ E) 2 M] {q : ℕ}
(h : TauCeti.IsManifoldStronglyPseudoconvexAt E q f x)
(hf : ContMDiffAt (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ ℝ) 2 f x)
(hcrit : d% f x = 0) :
TauCeti.manifoldMorseIndex (modelWithCornersSelf ℝ E) f x ≤ Module.finrank ℂ E + q
Lean
Formalized in Tau Ceti as TauCeti.IsManifoldStronglyPseudoconvexAt.manifoldMorseIndex_le.
Sources
Uses 2 · Used by 2
TheoremQuadraticForm.isTotallyReal_of_add_comp_posDef#
A submodule on which Q is nonpositive is totally real for a linear endomorphism J if
Q(v) + Q(Jv) is positive for every nonzero v.
QuadraticForm.isTotallyReal_of_add_comp_posDef.{u_1, u_2} {R : Type u_1} {E : Type u_2}
[CommSemiring R] [PartialOrder R] [IsOrderedAddMonoid R] [AddCommMonoid E] [_root_.Module R E]
(Q : QuadraticForm R E) {W : Submodule R E} (J : E →ₗ[R] E)
(hQJ : QuadraticMap.PosDef (Q + QuadraticMap.comp Q J)) (hW : ∀ v ∈ W, Q v ≤ 0) :
TauCeti.IsTotallyReal J W
Used by 1
λ ≤ nTheoremThe complex Hessian identity for squared distance#
For a holomorphic C² map, the sum
of the real Hessian on v and I • v is four times the squared norm of the complex derivative.
The identity holds at every point; at a critical point it is the intrinsic Hessian identity used
in the squared-distance Morse-index estimate.
TauCeti.fderiv_fderiv_norm_sq_sub_comp_add_I_smul.{u_1, u_2} {V : Type u_1} {E : Type u_2}
[NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup E] [InnerProductSpace ℂ E]
{i : V → E} {a : E} {x : V} (hi : ContDiffAt ℂ 2 i x) (v : V) :
((fderiv ℝ (fderiv ℝ fun y => ‖i y - a‖ ^ 2) x) v) v +
((fderiv ℝ (fderiv ℝ fun y => ‖i y - a‖ ^ 2) x) (Complex.I • v)) (Complex.I • v) =
4 * ‖(fderiv ℂ i x) v‖ ^ 2
Lean
Formalized in Tau Ceti as TauCeti.fderiv_fderiv_norm_sq_sub_comp_add_I_smul.
Sources
TheoremPaired principal curvatures#
For a C² holomorphic map, multiplication by I identifies
the generalized κ- and -κ-eigenspaces of each shape operator, so they have the same
dimension. For k = 1 these are the geometric multiplicities of the principal curvatures κ
and -κ.
ContDiffAt.finrank_genEigenspace_shapeOperator_neg.{u_1, u_2} {V : Type u_1} {E : Type u_2}
[NormedAddCommGroup V] [NormedSpace ℂ V] [FiniteDimensional ℂ V] [NormedAddCommGroup E]
[InnerProductSpace ℂ E] {i : V → E} {x : V} (hi : ContDiffAt ℂ 2 i x) (ν : E) (κ : ℝ) (k : ℕ∞) :
Module.finrank ℝ ↥(((TauCeti.shapeOperator i x ν).genEigenspace (-κ)) k) =
Module.finrank ℝ ↥(((TauCeti.shapeOperator i x ν).genEigenspace κ) k)
Lean
Formalized in Tau Ceti as ContDiffAt.finrank_genEigenspace_shapeOperator_neg.
Sources
Uses 1 · Used by 1
TheoremSymmetric focal points#
For a holomorphic immersion and a normal vector ν, the points
i x + ν and i x - ν have the same focal multiplicity, possibly zero: one is a focal point of
i at x exactly when the other is, and the Hessians at x of squared distance from them have
null spaces of the same dimension.
ContDiffAt.finrank_ker_fderiv_fderiv_norm_sq_sub_sub_comp.{u_1, u_2} {V : Type u_1} {E : Type u_2}
[NormedAddCommGroup V] [NormedSpace ℂ V] [FiniteDimensional ℂ V] [NormedAddCommGroup E]
[InnerProductSpace ℂ E] {i : V → E} {x : V} (hi : ContDiffAt ℂ 2 i x)
(h : Function.Injective ⇑(fderiv ℂ i x)) {ν : E} (hν : ν ∈ (↑(fderiv ℝ i x)).rangeᗮ) :
Module.finrank ℝ ↥(↑(fderiv ℝ (fderiv ℝ fun y => ‖i y - (i x - ν)‖ ^ 2) x)).ker =
Module.finrank ℝ ↥(↑(fderiv ℝ (fderiv ℝ fun y => ‖i y - (i x + ν)‖ ^ 2) x)).ker
Lean
Formalized in Tau Ceti as ContDiffAt.finrank_ker_fderiv_fderiv_norm_sq_sub_sub_comp.
Sources
Uses 2
DefinitionTauCeti.leviForm#
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).
TauCeti.leviForm.{u_1} {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] (f : V → ℝ) (x : V) :
V →ₗ⋆[ℂ] V →ₗ[ℂ] ℂ
DefinitionTauCeti.shapeOperator#
The shape operator S_ν of i : V → E at x in the direction ν: the endomorphism of
V with ⟪Di(x) (S_ν v), Di(x) w⟫ = ⟪ν, B(v, w)⟫ for all v and w, where B is the second
fundamental form. It is defined when Di(x) is injective, so that the induced metric
⟪Di(x) v, Di(x) w⟫ is nondegenerate, and is 0 otherwise.
TauCeti.shapeOperator.{u_1, u_2} {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V]
[NormedSpace ℝ V] [FiniteDimensional ℝ V] [NormedAddCommGroup E] [InnerProductSpace ℝ E]
(i : V → E) (x : V) (ν : E) : Module.End ℝ V
Used by 2
DefinitionTauCeti.complexProjectiveZeroLocus#
The common zero locus of a family of polynomials in N variables, as a set of complex lines
in ℂ^N: a line belongs to it when every polynomial of the family vanishes at every vector of
the line. The line of L is L.submodule, which is the underlying submodule of
Projectivization.equivSubmodule ℂ (Fin N → ℂ) L.
TauCeti.complexProjectiveZeroLocus.{u_1} {N : ℕ} {ι : Type u_1} (p : ι → MvPolynomial (Fin N) ℂ) :
Set (Projectivization ℂ (Fin N → ℂ))
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.