Continuous subharmonic functions

Let E be a finite-dimensional real inner product space with its volume measure. This file defines continuous subharmonic functions u : E → ℝ on a set U by the local sub-mean-value inequality: u is continuous on U, and at every x ∈ U the value u x is at most the average of u over ball x r for arbitrarily small radii r > 0. No differentiability is assumed, so the class is closed under pointwise maxima, which is what Perron's method for the Dirichlet problem needs.

The main result is the comparison principle: a subharmonic function on a bounded open set U that lies below a harmonic function h on frontier U, both continuous on closure U, lies below h on all of closure U. Applied to balls, it shows that the definition used here implies the one of Gilbarg–Trudinger, Section 2.8: a subharmonic function lies below every harmonic function that dominates it on the boundary sphere of a ball. The proof reduces to the maximum principle for the sub-mean-value property on a compact superlevel set (TauCeti.exists_mem_frontier_isMaxOn_of_le_setAverage_ball).

The comparison principle also holds between a subharmonic function u and a superharmonic function w (one with -w subharmonic): if u ≤ w on frontier U, both continuous on closure U, then u ≤ w on closure U. This is the form needed to compare members of the Perron family with upper barriers.

Main declarations

• TauCeti.SubharmonicOn: continuous functions with the local sub-mean-value inequality.
• InnerProductSpace.HarmonicOnNhd.subharmonicOn: harmonic functions are subharmonic.
• TauCeti.SubharmonicOn.frequently_le_setAverage_of_le: a continuous function touching a subharmonic function from above satisfies the sub-mean-value inequality at the contact point.
• TauCeti.SubharmonicOn.sup: the pointwise maximum of two subharmonic functions is subharmonic.
• TauCeti.SubharmonicOn.const_smul: a nonnegative multiple of a subharmonic function is subharmonic.
• TauCeti.SubharmonicOn.sub_harmonicOnNhd: subtracting a harmonic function preserves subharmonicity.
• TauCeti.SubharmonicOn.le_of_le_frontier: the comparison principle on a bounded open set.
• TauCeti.SubharmonicOn.le_of_le_sphere: the comparison principle on a ball.
• TauCeti.SubharmonicOn.le_of_le_frontier_of_subharmonicOn_neg: the comparison principle between a subharmonic and a superharmonic function on a bounded open set.

References

• D. Gilbarg, N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, Section 2.8.

structure TauCeti.SubharmonicOn {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (u : E → ℝ) (U : Set E) : Prop

A function u is subharmonic on U if it is continuous on U and satisfies the local sub-mean-value inequality there: at every x ∈ U, the value u x is at most the average of u over ball x r for arbitrarily small radii r > 0.

• continuousOn : ContinuousOn u U

  A subharmonic function is continuous.

• frequently_le_setAverage (x : E) : x ∈ U → ∃ᶠ (r : ℝ) in nhdsWithin 0 (Set.Ioi 0), u x ≤ ⨍ (y : E) in Metric.ball x r, u y

  The local sub-mean-value inequality.

theorem TauCeti.SubharmonicOn.mono {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {u : E → ℝ} {U V : Set E} (hu : SubharmonicOn u U) (hVU : V ⊆ U) : SubharmonicOn u V

A function subharmonic on a set is subharmonic on every subset.

theorem InnerProductSpace.HarmonicOnNhd.subharmonicOn {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {u : E → ℝ} {U : Set E} (hu : HarmonicOnNhd u U) : TauCeti.SubharmonicOn u U

A harmonic function is subharmonic.

theorem TauCeti.SubharmonicOn.frequently_le_setAverage_of_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {v w : E → ℝ} {U : Set E} (hv : SubharmonicOn v U) (hU : IsOpen U) (hw : ContinuousOn w U) (hvw : ∀ y ∈ U, v y ≤ w y) {x : E} (hx : x ∈ U) (hwx : w x = v x) : ∃ᶠ (r : ℝ) in nhdsWithin 0 (Set.Ioi 0), w x ≤ ⨍ (y : E) in Metric.ball x r, w y

A function w, continuous on the open set U, that lies above a subharmonic function v on U and touches it at x ∈ U satisfies the sub-mean-value inequality at x.

theorem TauCeti.SubharmonicOn.sup {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {u v : E → ℝ} {U : Set E} (hu : SubharmonicOn u U) (hv : SubharmonicOn v U) (hU : IsOpen U) : SubharmonicOn (u ⊔ v) U

The pointwise maximum of two subharmonic functions on an open set is subharmonic.

theorem TauCeti.SubharmonicOn.const_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {u : E → ℝ} {U : Set E} (hu : SubharmonicOn u U) {c : ℝ} (hc : 0 ≤ c) : SubharmonicOn (c • u) U

A nonnegative multiple of a subharmonic function is subharmonic.

theorem TauCeti.SubharmonicOn.sub_harmonicOnNhd {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {u h : E → ℝ} {U : Set E} (hu : SubharmonicOn u U) (hh : InnerProductSpace.HarmonicOnNhd h U) (hU : IsOpen U) : SubharmonicOn (u - h) U

Subtracting a harmonic function from a subharmonic function on an open set gives a subharmonic function.

theorem TauCeti.SubharmonicOn.le_of_le_frontier {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {u h : E → ℝ} {U : Set E} [Nontrivial E] (hU : IsOpen U) (hUb : Bornology.IsBounded U) (hu : SubharmonicOn u U) (huc : ContinuousOn u (closure U)) (hh : InnerProductSpace.HarmonicOnNhd h U) (hhc : ContinuousOn h (closure U)) (hle : ∀ x ∈ frontier U, u x ≤ h x) (x : E) : x ∈ closure U → u x ≤ h x

The comparison principle for subharmonic functions. Let U be a bounded open set, u subharmonic and h harmonic on U, both continuous on closure U. If u ≤ h on frontier U, then u ≤ h on closure U.

theorem TauCeti.SubharmonicOn.le_of_le_sphere {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {u h : E → ℝ} [Nontrivial E] {c : E} {r : ℝ} (hu : SubharmonicOn u (Metric.ball c r)) (huc : ContinuousOn u (Metric.closedBall c r)) (hh : InnerProductSpace.HarmonicOnNhd h (Metric.ball c r)) (hhc : ContinuousOn h (Metric.closedBall c r)) (hle : ∀ x ∈ Metric.sphere c r, u x ≤ h x) (x : E) : x ∈ Metric.closedBall c r → u x ≤ h x

The comparison principle on a ball. A function subharmonic on ball c r and continuous on closedBall c r lies below every function harmonic on ball c r and continuous on closedBall c r that dominates it on sphere c r.

theorem TauCeti.SubharmonicOn.le_of_le_frontier_of_subharmonicOn_neg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {u w : E → ℝ} {U : Set E} [Nontrivial E] (hU : IsOpen U) (hUb : Bornology.IsBounded U) (hu : SubharmonicOn u U) (huc : ContinuousOn u (closure U)) (hw : SubharmonicOn (-w) U) (hwc : ContinuousOn w (closure U)) (hle : ∀ x ∈ frontier U, u x ≤ w x) (x : E) : x ∈ closure U → u x ≤ w x

The comparison principle between a subharmonic and a superharmonic function. Let U be a bounded open set, u subharmonic on U and w superharmonic on U (that is, -w is subharmonic), both continuous on closure U. If u ≤ w on frontier U, then u ≤ w on closure U.