The maximum principle for the sub-mean-value property

Let E be a nontrivial finite-dimensional real normed space with an additive Haar measure μ. This file proves that a function u, continuous on a compact set K, with u x ≤ ⨍ y in ball x r, u y ∂μ for arbitrarily small r > 0 at every interior point x of K, attains its maximum over K on frontier K. No differentiability is assumed, so this applies to continuous subharmonic functions in their mean-value formulation, and to differences of a continuous function with the mean-value property and a harmonic function.

The argument

Among the points where the maximum M is attained, take one, z, farthest from a fixed maximum point. If z were interior, then on a small ball about z contained in K the continuous function u ≤ M would have average at least M, so by the equality case of Jensen's inequality (StrictConvex.ae_eq_const_or_average_mem_interior) it would equal M on the whole ball, which contains maximum points farther away than z.

Main declarations

• TauCeti.exists_mem_frontier_isMaxOn_of_le_setAverage_ball: a continuous function with the sub-mean-value property on balls at the interior points of a compact set attains its maximum on the frontier.
• TauCeti.le_of_le_setAverage_ball_le_frontier, TauCeti.ge_of_setAverage_ball_le_ge_frontier: the weak maximum and minimum principles for the sub- and super-mean-value properties.

References

• L. C. Evans, Partial Differential Equations, Section 2.2.3, Theorem 4.
• D. Gilbarg, N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, Section 2.8.

theorem TauCeti.exists_mem_frontier_isMaxOn_of_le_setAverage_ball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [Nontrivial E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {u : E → ℝ} {K : Set E} (hK : IsCompact K) (hne : K.Nonempty) (hu : ContinuousOn u K) (hsub : ∀ x ∈ interior K, ∃ᶠ (r : ℝ) in nhdsWithin 0 (Set.Ioi 0), u x ≤ ⨍ (y : E) in Metric.ball x r, u y ∂μ) : ∃ x ∈ frontier K, IsMaxOn u K x

Maximum principle for the sub-mean-value property. Let K be a nonempty compact set and let u be continuous on K. If at every interior point x of K the value u x is at most the average of u over ball x r for arbitrarily small radii r > 0, then u attains its maximum over K at a point of frontier K.

theorem TauCeti.le_of_le_setAverage_ball_le_frontier {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [Nontrivial E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {u : E → ℝ} {K : Set E} (hK : IsCompact K) {m : ℝ} (hu : ContinuousOn u K) (hsub : ∀ x ∈ interior K, ∃ᶠ (r : ℝ) in nhdsWithin 0 (Set.Ioi 0), u x ≤ ⨍ (y : E) in Metric.ball x r, u y ∂μ) (hbdry : ∀ ⦃x : E⦄, x ∈ frontier K → u x ≤ m) ⦃x : E⦄ : x ∈ K → u x ≤ m

Weak maximum principle for the sub-mean-value property. Let K be compact and let u be continuous on K. If at every interior point x of K the value u x is at most the average of u over ball x r for arbitrarily small radii r > 0, then any bound m that u respects on frontier K bounds u on all of K.

theorem TauCeti.ge_of_setAverage_ball_le_ge_frontier {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [Nontrivial E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {u : E → ℝ} {K : Set E} (hK : IsCompact K) {m : ℝ} (hu : ContinuousOn u K) (hsup : ∀ x ∈ interior K, ∃ᶠ (r : ℝ) in nhdsWithin 0 (Set.Ioi 0), ⨍ (y : E) in Metric.ball x r, u y ∂μ ≤ u x) (hbdry : ∀ ⦃x : E⦄, x ∈ frontier K → m ≤ u x) ⦃x : E⦄ : x ∈ K → m ≤ u x

Weak minimum principle for the super-mean-value property. Let K be compact and let u be continuous on K. If at every interior point x of K the value u x is at least the average of u over ball x r for arbitrarily small radii r > 0, then any lower bound m that u respects on frontier K bounds u from below on all of K.