The Laplacian at an interior local extremum

At an interior local maximum of a C² function the Laplacian is nonpositive, and at an interior local minimum it is nonnegative; this is the second-derivative form of the maximum principle. The Laplacian is the trace of the Hessian, and TauCeti.Analysis.Calculus.DerivativeTest signs each diagonal Hessian entry at a local extremum.

Main declarations

• TauCeti.laplacian_nonpos_of_isLocalMax / TauCeti.laplacian_nonneg_of_isLocalMin: the Laplacian is nonpositive at a local maximum and nonnegative at a local minimum.
• TauCeti.not_isLocalMax_of_laplacian_pos / TauCeti.not_isLocalMin_of_laplacian_neg: a strictly subharmonic function (0 < Δ f x) has no interior local maximum, the classical first step of the maximum principle; the superharmonic mirror image has no interior local minimum.

theorem TauCeti.laplacian_nonpos_of_isLocalMax {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} (hf : ContDiffAt ℝ 2 f x) (hmax : IsLocalMax f x) : Laplacian.laplacian f x ≤ 0

Maximum principle, second-derivative form. At an interior local maximum of a C² function the Laplacian is nonpositive.

theorem TauCeti.laplacian_nonneg_of_isLocalMin {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} (hf : ContDiffAt ℝ 2 f x) (hmin : IsLocalMin f x) : 0 ≤ Laplacian.laplacian f x

Minimum principle, second-derivative form. At an interior local minimum of a C² function the Laplacian is nonnegative.

theorem TauCeti.not_isLocalMax_of_laplacian_pos {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} (hf : ContDiffAt ℝ 2 f x) (hlap : 0 < Laplacian.laplacian f x) : ¬IsLocalMax f x

A strictly subharmonic C² function (0 < Δ f x) has no interior local maximum at x. This is the classical opening move of the maximum principle.

theorem TauCeti.not_isLocalMin_of_laplacian_neg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → ℝ} {x : E} (hf : ContDiffAt ℝ 2 f x) (hlap : Laplacian.laplacian f x < 0) : ¬IsLocalMin f x

A strictly superharmonic C² function (Δ f x < 0) has no interior local minimum at x.