Squared distance along a differentiable map #
For a map i : V → E into a real inner product space and a point a : E, this file computes the
first and second derivatives of the squared-distance function
x ↦ ‖i x - a‖ ^ 2.
A point is critical exactly when the displacement from a is orthogonal to the range of Di.
The Hessian is twice the sum of the pullback metric term and the pairing of the displacement
with D²i. For a holomorphic map between complex normed spaces, the latter terms cancel between
v and I • v. Consequently the Levi diagonal is exactly ‖Di(v)‖², and a holomorphic immersion
pulls squared distance back to a strictly plurisubharmonic function.
These formulas are the local inner-product-space calculation behind squared-distance exhaustions of closed complex submanifolds. No immersion hypothesis is needed until strict positivity is deduced.
The same calculus gives the first and second derivatives of the Gaussian
x ↦ exp (-α ‖x - a‖ ^ 2) of the squared distance, the classical barrier of Hopf's
boundary-point lemma for elliptic operators with variable coefficients.
The file also computes the Hessian of the radial profile (σ ‖y - c‖² + ε)^(-β), the barrier
of the Krylov–Safonov measure estimate.
Main results #
TauCeti.fderiv_norm_sq_sub_comp: the first derivative of squared distance along a map.TauCeti.fderiv_norm_sq_sub_comp_eq_zero_iff: the critical-point normal-vector test.TauCeti.fderiv_fderiv_norm_sq_sub_comp_apply: the full Hessian formula.TauCeti.hasFDerivAt_exp_neg_mul_norm_sub_sq,TauCeti.fderiv_fderiv_exp_neg_mul_norm_sub_sq_apply: the first and second derivatives ofx ↦ exp (-α ‖x - a‖ ^ 2).TauCeti.fderiv_fderiv_rpow_mul_norm_sq_sub_add_apply: the Hessian of(σ ‖y - c‖² + ε)^(-β).TauCeti.fderiv_fderiv_norm_sq_apply_complex: the real second derivative of complex squared norm is twice the real part of the inner product.TauCeti.fderiv_fderiv_norm_sq_sub_comp_add_I_smul: the complex Hessian identity.TauCeti.re_leviForm_norm_sq_sub_comp_apply_self: the Levi diagonal of squared distance.TauCeti.isStrictlyPlurisubharmonicAt_norm_sq_sub_comp: strict plurisubharmonicity along a holomorphic immersion.
References #
- J. Milnor, Morse Theory, Princeton University Press, 1963, Section 7.
- R. Hain, Notes on the Morse theory of complex manifolds, Section 2.
The derivative of squared distance from a along a differentiable map i is the pairing
with 2 • (i x - a), precomposed with the derivative of i.
The critical-point normal-vector test. Squared distance from a along i is critical at
x exactly when the displacement i x - a is orthogonal to the range of Di(x).
The Hessian of squared distance along a map. It is twice the sum of the pullback inner product and the pairing of the displacement with the second derivative of the map.
The derivative of the Gaussian x ↦ exp (-α ‖x - a‖ ^ 2) of the squared distance from a
is -2 α exp (-α ‖x - a‖ ^ 2) ⟪x - a, ·⟫.
The second derivative of the Gaussian x ↦ exp (-α ‖x - a‖ ^ 2) of the squared distance from
a is (4 α² ⟪x - a, v⟫ ⟪x - a, w⟫ - 2 α ⟪v, w⟫) exp (-α ‖x - a‖ ^ 2).
The radial profile (σ ‖y - c‖² + ε)^(-β) is smooth when σ ≥ 0 and ε > 0.
The Hessian of a power of a shifted squared distance. For σ ≥ 0 and ε > 0, with
s = σ ‖x - c‖² + ε, the second derivative of (σ ‖y - c‖² + ε)^(-β) at x is
4 σ² β (β + 1) s^(-β-2) ⟪x - c, v⟫ ⟪x - c, w⟫ - 2 σ β s^(-β-1) ⟪v, w⟫.
The real second derivative of the squared norm of a complex inner product space is
2 * Re ⟪v, w⟫_ℂ.
The 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.
The Levi diagonal of squared distance along a holomorphic C² map is the squared norm of its
complex derivative.
Squared distance pulled back along a holomorphic immersion is strictly plurisubharmonic at the point of immersion.