Subharmonic functions of one complex variable

A real-valued function on an open subset of ℂ is subharmonic if it is upper semicontinuous and satisfies the local submean inequality: at every point, for all sufficiently small radii the function is integrable on the circle and its value at the center is at most its circle average. This is the definition of [Ransford][Ransford1995], Potential Theory in the Complex Plane, Definition 2.2.1, and of [Fritzsche–Grauert][FritzscheGrauert2002], Chapter II, Section 2, with the harmonic-majorant condition replaced by the submean inequality. Locality is then immediate. The submean inequality on every closed disc in the domain and the plurisubharmonic theory are developed in later files.

Only real-valued functions are considered; the value -∞ is not admitted.

This file proves closure under sums, nonnegative multiples and maxima, gives the holomorphic examples (real parts, positive powers of norms, logarithms of nonvanishing moduli), and proves the maximum principle: a subharmonic function on a preconnected open set that attains its supremum is constant. On a disc, if it is upper semicontinuous on the closed disc, it is bounded by its supremum on the boundary circle.

References: [Fritzsche–Grauert][FritzscheGrauert2002] (2002), Chapter II, Section 2; [Range][Range1986] (1986), Chapter II, Section 5; [Ransford][Ransford1995] (1995), Chapter 2.

Main definitions

• HasSubmeanAt: The local submean property at a point: for every sufficiently small radius, the function is integrable on the circle and its value at the center is bounded by its circle average.
• SubharmonicOn: A real function is subharmonic on a set if it is upper semicontinuous there and has the local submean property at each of its points.

Main results

• SubharmonicOn.eqOn_const_of_isMaxOn: Maximum principle. A subharmonic function on a preconnected open set that attains its supremum at a point is constant.
• SubharmonicOn.le_of_le_sphere: Maximum principle on a disc. A function subharmonic on an open disc and upper semicontinuous on the closed disc is bounded by any bound valid on the boundary circle.

References

• [K. Fritzsche and H. Grauert, From Holomorphic Functions to Complex Manifolds][FritzscheGrauert2002]
• [R. M. Range, Holomorphic Functions and Integral Representations in Several Complex Variables][Range1986]
• [T. Ransford, Potential Theory in the Complex Plane][Ransford1995]

def SeveralComplexVariables.HasSubmeanAt (u : ℂ → ℝ) (a : ℂ) : Prop

The local submean property at a point: for every sufficiently small radius, the function is integrable on the circle and its value at the center is bounded by its circle average.

Equations

• SeveralComplexVariables.HasSubmeanAt u a = ∀ᶠ (r : ℝ) in nhdsWithin 0 (Set.Ioi 0), CircleIntegrable u a r ∧ u a ≤ Real.circleAverage u a r

def SeveralComplexVariables.SubharmonicOn (u : ℂ → ℝ) (U : Set ℂ) : Prop

A real function is subharmonic on a set if it is upper semicontinuous there and has the local submean property at each of its points. The set is intended to be open.

Equations

• SeveralComplexVariables.SubharmonicOn u U = (UpperSemicontinuousOn u U ∧ ∀ a ∈ U, SeveralComplexVariables.HasSubmeanAt u a)

theorem SeveralComplexVariables.SubharmonicOn.upperSemicontinuousOn {u : ℂ → ℝ} {U : Set ℂ} (h : SubharmonicOn u U) : UpperSemicontinuousOn u U

A subharmonic function is upper semicontinuous.

theorem SeveralComplexVariables.SubharmonicOn.hasSubmeanAt {u : ℂ → ℝ} {U : Set ℂ} {a : ℂ} (h : SubharmonicOn u U) (ha : a ∈ U) : HasSubmeanAt u a

A subharmonic function has the local submean property at each point of its domain.

theorem SeveralComplexVariables.SubharmonicOn.mono {u : ℂ → ℝ} {U V : Set ℂ} (h : SubharmonicOn u U) (hV : V ⊆ U) : SubharmonicOn u V

Subharmonicity restricts to subsets.

theorem SeveralComplexVariables.HasSubmeanAt.exists_forall_lt {u : ℂ → ℝ} {a : ℂ} (h : HasSubmeanAt u a) : ∃ ρ > 0, ∀ (r : ℝ), 0 < r → r < ρ → CircleIntegrable u a r ∧ u a ≤ Real.circleAverage u a r

The local submean property provides a radius below which the inequality holds.

theorem SeveralComplexVariables.hasSubmeanAt_of_forall_lt {u : ℂ → ℝ} {a : ℂ} {ρ : ℝ} (hρ : 0 < ρ) (h : ∀ (r : ℝ), 0 < r → r < ρ → CircleIntegrable u a r ∧ u a ≤ Real.circleAverage u a r) : HasSubmeanAt u a

Conversely, a radius bound gives the local submean property.

theorem SeveralComplexVariables.subharmonicOn_of_locally {u : ℂ → ℝ} {U : Set ℂ} (h : ∀ a ∈ U, ∃ V ∈ nhds a, SubharmonicOn u (V ∩ U)) : SubharmonicOn u U

Subharmonicity is a local property.

theorem SeveralComplexVariables.hasSubmeanAt_const (c : ℝ) (a : ℂ) : HasSubmeanAt (fun (x : ℂ) => c) a

Constants have the local submean property.

theorem SeveralComplexVariables.subharmonicOn_const (c : ℝ) (U : Set ℂ) : SubharmonicOn (fun (x : ℂ) => c) U

Constants are subharmonic.

theorem SeveralComplexVariables.HasSubmeanAt.add {u v : ℂ → ℝ} {a : ℂ} (hu : HasSubmeanAt u a) (hv : HasSubmeanAt v a) : HasSubmeanAt (fun (z : ℂ) => u z + v z) a

The local submean property is additive.

theorem SeveralComplexVariables.SubharmonicOn.add {u v : ℂ → ℝ} {U : Set ℂ} (hu : SubharmonicOn u U) (hv : SubharmonicOn v U) : SubharmonicOn (fun (z : ℂ) => u z + v z) U

Sums of subharmonic functions are subharmonic.

theorem SeveralComplexVariables.HasSubmeanAt.const_mul {u : ℂ → ℝ} {a : ℂ} {c : ℝ} (hc : 0 ≤ c) (hu : HasSubmeanAt u a) : HasSubmeanAt (fun (z : ℂ) => c * u z) a

Nonnegative multiples preserve the local submean property.

theorem SeveralComplexVariables.SubharmonicOn.const_mul {u : ℂ → ℝ} {U : Set ℂ} {c : ℝ} (hc : 0 ≤ c) (hu : SubharmonicOn u U) : SubharmonicOn (fun (z : ℂ) => c * u z) U

Nonnegative multiples of subharmonic functions are subharmonic.

theorem SeveralComplexVariables.HasSubmeanAt.sup {u v : ℂ → ℝ} {a : ℂ} (hu : HasSubmeanAt u a) (hv : HasSubmeanAt v a) : HasSubmeanAt (fun (z : ℂ) => max (u z) (v z)) a

The pointwise maximum preserves the local submean property.

theorem SeveralComplexVariables.SubharmonicOn.sup {u v : ℂ → ℝ} {U : Set ℂ} (hu : SubharmonicOn u U) (hv : SubharmonicOn v U) : SubharmonicOn (fun (z : ℂ) => max (u z) (v z)) U

The pointwise maximum of two subharmonic functions is subharmonic.

theorem SeveralComplexVariables.hasSubmeanAt_of_circleAverage_eq {u : ℂ → ℝ} {a : ℂ} {ρ : ℝ} (hρ : 0 < ρ) (hc : ContinuousOn u (Metric.ball a ρ)) (h : ∀ (r : ℝ), 0 < r → r < ρ → Real.circleAverage u a r = u a) : HasSubmeanAt u a

A continuous function whose circle averages over all small circles equal its value at the center has the local submean property; this applies to harmonic functions.

theorem SeveralComplexVariables.circleAverage_re_eq_of_analyticAt {a : ℂ} {f : ℂ → ℂ} (hf : AnalyticAt ℂ f a) : ∃ ρ > 0, ∀ (r : ℝ), 0 < r → r < ρ → Real.circleAverage (fun (z : ℂ) => (f z).re) a r = (f a).re

Real parts of holomorphic functions have the local submean property, with equality.

theorem AnalyticOnNhd.subharmonicOn_re {U : Set ℂ} {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f U) : SeveralComplexVariables.SubharmonicOn (fun (z : ℂ) => (f z).re) U

The real part of a holomorphic function is subharmonic.

theorem AnalyticOnNhd.subharmonicOn_neg_re {U : Set ℂ} {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f U) : SeveralComplexVariables.SubharmonicOn (fun (z : ℂ) => -(f z).re) U

Minus the real part of a holomorphic function is subharmonic.

theorem AnalyticOnNhd.subharmonicOn_norm_rpow {U : Set ℂ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] (hU : IsOpen U) {f : ℂ → F} {p : ℝ} (hp : 0 < p) (hf : AnalyticOnNhd ℂ f U) : SeveralComplexVariables.SubharmonicOn (fun (z : ℂ) => ‖f z‖ ^ p) U

Positive powers of the norm of a holomorphic function are subharmonic.

theorem AnalyticOnNhd.subharmonicOn_log_norm {U : Set ℂ} (hU : IsOpen U) {f : ℂ → ℂ} (hf : AnalyticOnNhd ℂ f U) (hne : ∀ z ∈ U, f z ≠ 0) : SeveralComplexVariables.SubharmonicOn (fun (z : ℂ) => Real.log ‖f z‖) U

The logarithm of the modulus of a nonvanishing holomorphic function is subharmonic.

theorem SeveralComplexVariables.circleAverage_lt_of_lt {u : ℂ → ℝ} {a : ℂ} {r M : ℝ} (hr : 0 < r) (hint : CircleIntegrable u a r) (hle : ∀ z ∈ Metric.sphere a r, u z ≤ M) (husc : UpperSemicontinuousOn u (Metric.sphere a r)) {z : ℂ} (hz : z ∈ Metric.sphere a r) (hlt : u z < M) : Real.circleAverage u a r < M

A circle-integrable function bounded by M on a circle, upper semicontinuous there and strictly below M at one point, has circle average strictly below M.

theorem SeveralComplexVariables.SubharmonicOn.eventually_eq_of_isMaxOn {u : ℂ → ℝ} {U : Set ℂ} {a : ℂ} (hU : IsOpen U) (hu : SubharmonicOn u U) (ha : a ∈ U) (hmax : ∀ z ∈ U, u z ≤ u a) : ∀ᶠ (z : ℂ) in nhds a, u z = u a

A subharmonic function attaining its supremum at a point is constant near that point.

theorem SeveralComplexVariables.SubharmonicOn.eqOn_const_of_isMaxOn {u : ℂ → ℝ} {U : Set ℂ} {a : ℂ} (hU : IsOpen U) (hc : IsPreconnected U) (hu : SubharmonicOn u U) (ha : a ∈ U) (hmax : ∀ z ∈ U, u z ≤ u a) (z : ℂ) : z ∈ U → u z = u a

Maximum principle. A subharmonic function on a preconnected open set that attains its supremum at a point is constant.

theorem SeveralComplexVariables.SubharmonicOn.le_of_le_sphere {u : ℂ → ℝ} {a : ℂ} {r M : ℝ} (hr : 0 < r) (hu : SubharmonicOn u (Metric.ball a r)) (husc : UpperSemicontinuousOn u (Metric.closedBall a r)) (hM : ∀ z ∈ Metric.sphere a r, u z ≤ M) (z : ℂ) : z ∈ Metric.closedBall a r → u z ≤ M

Maximum principle on a disc. A function subharmonic on an open disc and upper semicontinuous on the closed disc is bounded by any bound valid on the boundary circle.