Boundary maximum principles for strictly subharmonic functions

TauCeti.Analysis.InnerProductSpace.Laplacian.LocalExtr proves the local second-derivative obstruction: a C² scalar function with 0 < Δ f x has no local maximum at x. This file turns that local statement into the compact-set boundary form used as the first maximum-principle handoff in the PDE roadmap.

The compact-to-boundary handoff uses Mathlib's IsCompact.exists_isMaxOn / IsCompact.exists_isMinOn extreme-value APIs and IsMaxOn.isLocalMax / IsMinOn.isLocalMin localization APIs.

If a continuous function on a compact set has positive Laplacian at every interior point where the second derivative is available, then some maximum point lies on the frontier. The dual minimum statement holds for negative Laplacian.

Main declarations

• TauCeti.exists_mem_frontier_isMaxOn_of_laplacian_pos: a strictly subharmonic function on the interior of a compact set attains a maximum on the frontier.
• TauCeti.exists_mem_frontier_isMinOn_of_laplacian_neg: a strictly superharmonic function on the interior of a compact set attains a minimum on the frontier.

theorem TauCeti.exists_mem_frontier_isMaxOn_of_forall_mem_interior_not_isLocalMax {X : Type u_1} {β : Type u_2} [TopologicalSpace X] [TopologicalSpace β] [LinearOrder β] [ClosedIciTopology β] {K : Set X} (hK : IsCompact K) (hne : K.Nonempty) {f : X → β} (hcont : ContinuousOn f K) (hnot : ∀ ⦃x : X⦄, x ∈ interior K → ¬IsLocalMax f x) : ∃ x ∈ frontier K, IsMaxOn f K x

If every interior point of a compact set is forbidden from being a local maximum, then a continuous function on the compact set has a maximum point on the frontier.

theorem TauCeti.exists_mem_frontier_isMinOn_of_forall_mem_interior_not_isLocalMin {X : Type u_1} {β : Type u_2} [TopologicalSpace X] [TopologicalSpace β] [LinearOrder β] [ClosedIicTopology β] {K : Set X} (hK : IsCompact K) (hne : K.Nonempty) {f : X → β} (hcont : ContinuousOn f K) (hnot : ∀ ⦃x : X⦄, x ∈ interior K → ¬IsLocalMin f x) : ∃ x ∈ frontier K, IsMinOn f K x

If every interior point of a compact set is forbidden from being a local minimum, then a continuous function on the compact set has a minimum point on the frontier.

theorem TauCeti.exists_mem_frontier_isMaxOn_of_laplacian_pos {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {K : Set E} (hK : IsCompact K) (hne : K.Nonempty) {f : E → ℝ} (hcont : ContinuousOn f K) (hcd : ∀ ⦃x : E⦄, x ∈ interior K → ContDiffAt ℝ 2 f x) (hlap : ∀ ⦃x : E⦄, x ∈ interior K → 0 < Laplacian.laplacian f x) : ∃ x ∈ frontier K, IsMaxOn f K x

Boundary maximum principle for strictly subharmonic functions.

Let K be compact and nonempty. If f is continuous on K, is C² at every interior point, and satisfies 0 < Δ f x throughout interior K, then some maximum point of f on K lies on frontier K.

theorem TauCeti.exists_mem_frontier_isMinOn_of_laplacian_neg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {K : Set E} (hK : IsCompact K) (hne : K.Nonempty) {f : E → ℝ} (hcont : ContinuousOn f K) (hcd : ∀ ⦃x : E⦄, x ∈ interior K → ContDiffAt ℝ 2 f x) (hlap : ∀ ⦃x : E⦄, x ∈ interior K → Laplacian.laplacian f x < 0) : ∃ x ∈ frontier K, IsMinOn f K x

Boundary minimum principle for strictly superharmonic functions.

Let K be compact and nonempty. If f is continuous on K, is C² at every interior point, and satisfies Δ f x < 0 throughout interior K, then some minimum point of f on K lies on frontier K.