Documentation

TauCeti.Geometry.Manifold.Riemannian.MaximumPrinciple

The maximum principle for the Laplace–Beltrami operator #

On a boundaryless Riemannian manifold, this file proves the pointwise second-derivative test for the Riemannian Hessian and the Laplace–Beltrami operator Δ = div ∘ grad, and the resulting comparison principle for semilinear elliptic equations on a compact manifold.

At a critical point of a C² function the Levi-Civita correction term of the Hessian vanishes, so the Riemannian Hessian is the ordinary second derivative of the function read in the preferred chart. Consequently the Hessian is negative semidefinite at a local maximum and positive semidefinite at a local minimum, and the same holds for its trace Δ.

On a compact boundaryless manifold, evaluating at a maximum of u - v gives the comparison principle: if h(x, ·) is strictly increasing for every x, a subsolution h(x, u) ≤ Δ u lies below a supersolution Δ v ≤ h(x, v). In particular a semilinear equation Δ u = h(x, u) with strictly increasing nonlinearity has at most one C² solution. This is the uniqueness mechanism for the curvature equation of conformal metrics on closed surfaces.

Main results #

References #

theorem TauCeti.Manifold.hessian_self_nonpos_of_isLocalMax {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {f : M → ℝ} {x : M} (hf : ContMDiffAt I (modelWithCornersSelf ℝ ℝ) 2 f x) (hmax : IsLocalMax f x) (v : TangentSpace I x) :
hessian I f x v v ≤ 0

At a local maximum of a C² function on a boundaryless Riemannian manifold, the Hessian is negative semidefinite.

At a local maximum of a C² function on a boundaryless Riemannian manifold, the Laplace–Beltrami operator Δ = div ∘ grad is nonpositive.

theorem TauCeti.Manifold.hessian_self_nonneg_of_isLocalMin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {f : M → ℝ} {x : M} (hf : ContMDiffAt I (modelWithCornersSelf ℝ ℝ) 2 f x) (hmin : IsLocalMin f x) (v : TangentSpace I x) :
0 ≤ hessian I f x v v

At a local minimum of a C² function on a boundaryless Riemannian manifold, the Hessian is positive semidefinite.

At a local minimum of a C² function on a boundaryless Riemannian manifold, the Laplace–Beltrami operator Δ = div ∘ grad is nonnegative.

theorem TauCeti.Manifold.le_of_le_laplaceBeltrami_of_laplaceBeltrami_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] [CompactSpace M] {h : M → ℝ → ℝ} (hh : ∀ (x : M), StrictMono (h x)) {u v : M → ℝ} (hu : ContMDiff I (modelWithCornersSelf ℝ ℝ) 2 u) (hv : ContMDiff I (modelWithCornersSelf ℝ ℝ) 2 v) (hsub : ∀ (x : M), h x (u x) ≤ laplaceBeltrami I u x) (hsuper : ∀ (x : M), laplaceBeltrami I v x ≤ h x (v x)) :
u ≤ v

The comparison principle for semilinear equations Δ u = h(x, u) on a compact boundaryless Riemannian manifold, with h(x, ·) strictly increasing for every x: a C² subsolution h(x, u) ≤ Δ u lies below a C² supersolution Δ v ≤ h(x, v).