The maximum principle and decaying classical harmonic functions

The scalar second derivative is nonpositive at a local maximum.

The Hessian quadratic form is nonpositive at a local maximum.

theorem LiebThirring.second_deriv_nonpos_at_local_max {f : ℝ → ℝ} {a : ℝ} (hf : ContDiffAt ℝ 2 f a) (hm : IsLocalMax f a) : iteratedDeriv 2 f a ≤ 0

The scalar second derivative is nonpositive at a local maximum.

theorem LiebThirring.hessian_nonpos_at_local_max {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} {x : E} (hf : ContDiffAt ℝ 2 f x) (hm : IsLocalMax f x) (v : E) : ((fderiv ℝ (fderiv ℝ f) x) v) v ≤ 0

The Hessian quadratic form is nonpositive at a local maximum.

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

The Laplacian of a C² function is nonpositive at a local maximum.

theorem LiebThirring.laplacian_norm_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (x : E) : Laplacian.laplacian (fun (y : E) => ‖y‖ ^ 2) x = 2 * ↑(Module.finrank ℝ E)

The Euclidean quadratic barrier has Laplacian twice the dimension.

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

A function with positive Laplacian cannot have a local maximum.

theorem LiebThirring.le_of_laplacian_eq_zero_on_closedBall {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [Nontrivial E] {h : E → ℝ} {c x : E} {R M : ℝ} (hR : 0 < R) (hh : ∀ y ∈ Metric.closedBall c R, ContDiffAt ℝ 2 h y) (hΔ : ∀ y ∈ Metric.ball c R, Laplacian.laplacian h y = 0) (hbd : ∀ y ∈ Metric.sphere c R, h y ≤ M) (hx : x ∈ Metric.closedBall c R) : h x ≤ M

The maximum principle on a closed ball, proved with the quadratic barrier.

theorem LiebThirring.nonpos_of_laplacian_eq_zero_of_tendsto {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [Nontrivial E] {h : E → ℝ} (hh : ContDiff ℝ 2 h) (hΔ : ∀ (x : E), Laplacian.laplacian h x = 0) (hd : Filter.Tendsto h (Filter.cocompact E) (nhds 0)) (x : E) : h x ≤ 0

A globally C² harmonic function decaying at infinity is nonpositive.

theorem LiebThirring.eq_zero_of_laplacian_eq_zero_of_tendsto {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [Nontrivial E] {h : E → ℝ} (hh : ContDiff ℝ 2 h) (hΔ : ∀ (x : E), Laplacian.laplacian h x = 0) (hd : Filter.Tendsto h (Filter.cocompact E) (nhds 0)) : h = 0

Uniqueness for classical harmonic functions decaying at infinity.