Sub-mean-value functions on ℂ and maximum principles

SubMeanOn g s: g is continuous on s and satisfies the sub-mean-value inequality g c ≤ circleAverage g c r for every circle whose closed disk lies in s. MeanEqOn is the two-sided variant. These are the working notions of sub/harmonicity at the ℂ-chart level (Anghel–Stan arXiv:2008.12189, Definition 2, with all radii; Hubbard §1.2, Definition 1.2.1).

Main results: closure under max and under addition of a MeanEqOn function, the strong maximum principle on connected opens, and the boundary comparison principle on bounded opens. All are elementary consequences of the circle average inequality and a clopen argument.

structure Rado.SubMeanOn (g : ℂ → ℝ) (s : Set ℂ) : Prop

g is continuous and satisfies the sub-mean-value inequality on every circle whose closed disk lies in s.

• continuousOn : ContinuousOn g s
• submean (c : ℂ) (r : ℝ) : 0 < r → Metric.closedBall c r ⊆ s → g c ≤ Real.circleAverage g c r

structure Rado.MeanEqOn (h : ℂ → ℝ) (s : Set ℂ) : Prop

h is continuous and satisfies the mean-value equality on every circle whose closed disk lies in s.

• continuousOn : ContinuousOn h s
• mean_eq (c : ℂ) (r : ℝ) : 0 < r → Metric.closedBall c r ⊆ s → Real.circleAverage h c r = h c

theorem Rado.MeanEqOn.subMeanOn {h : ℂ → ℝ} {s : Set ℂ} (hh : MeanEqOn h s) : SubMeanOn h s

theorem Rado.MeanEqOn.neg {h : ℂ → ℝ} {s : Set ℂ} (hh : MeanEqOn h s) : MeanEqOn (-h) s

theorem Rado.SubMeanOn.mono {g : ℂ → ℝ} {s t : Set ℂ} (hg : SubMeanOn g s) (hts : t ⊆ s) : SubMeanOn g t

theorem Rado.SubMeanOn.max {g₁ g₂ : ℂ → ℝ} {s : Set ℂ} (h₁ : SubMeanOn g₁ s) (h₂ : SubMeanOn g₂ s) : SubMeanOn (fun (z : ℂ) => Max.max (g₁ z) (g₂ z)) s

theorem Rado.SubMeanOn.add_meanEq {g h : ℂ → ℝ} {s : Set ℂ} (hg : SubMeanOn g s) (hh : MeanEqOn h s) : SubMeanOn (g + h) s

theorem Rado.SubMeanOn.const {a : ℝ} {s : Set ℂ} : SubMeanOn (fun (x : ℂ) => a) s

structure Rado.SubMeanLocalOn (g : ℂ → ℝ) (s : Set ℂ) : Prop

Continuity plus the sub-mean-value inequality on all sufficiently small circles around each point.

• continuousOn : ContinuousOn g s
• submean_small (z : ℂ) : z ∈ s → ∀ᶠ (r : ℝ) in nhdsWithin 0 (Set.Ioi 0), g z ≤ Real.circleAverage g z r

theorem Rado.SubMeanLocalOn.mono {g : ℂ → ℝ} {s t : Set ℂ} (hg : SubMeanLocalOn g s) (hts : t ⊆ s) : SubMeanLocalOn g t

theorem Rado.SubMeanLocalOn.eqOn_const_of_isMaxOn {g : ℂ → ℝ} {s : Set ℂ} (hs : IsOpen s) (hsc : IsPreconnected s) (hg : SubMeanLocalOn g s) {x₀ : ℂ} (hx₀ : x₀ ∈ s) (hmax : IsMaxOn g s x₀) : Set.EqOn g (fun (x : ℂ) => g x₀) s

Small circles suffice for the strong maximum principle.

theorem Rado.SubMeanLocalOn.le_of_frontier_le {g : ℂ → ℝ} {U : Set ℂ} (hU : IsOpen U) (hUb : Bornology.IsBounded U) (hg : SubMeanLocalOn g U) (hgc : ContinuousOn g (closure U)) {M : ℝ} (hbd : ∀ x ∈ frontier U, g x ≤ M) (x : ℂ) : x ∈ closure U → g x ≤ M

Small circles suffice for the boundary comparison principle.

theorem Rado.SubMeanOn.localOn {g : ℂ → ℝ} {s : Set ℂ} (hg : SubMeanOn g s) (hs : IsOpen s) : SubMeanLocalOn g s

On an open set, the global sub-mean property supplies its local variant.

theorem Rado.SubMeanOn.eqOn_const_of_isMaxOn {g : ℂ → ℝ} {s : Set ℂ} (hs : IsOpen s) (hsc : IsPreconnected s) (hg : SubMeanOn g s) {x₀ : ℂ} (hx₀ : x₀ ∈ s) (hmax : IsMaxOn g s x₀) : Set.EqOn g (fun (x : ℂ) => g x₀) s

Strong maximum principle. A sub-mean-value function on a connected open set that attains its supremum is constant.

theorem Rado.SubMeanOn.le_of_frontier_le {g : ℂ → ℝ} {U : Set ℂ} (hU : IsOpen U) (hUb : Bornology.IsBounded U) (hg : SubMeanOn g U) (hgc : ContinuousOn g (closure U)) {M : ℝ} (hbd : ∀ x ∈ frontier U, g x ≤ M) (x : ℂ) : x ∈ closure U → g x ≤ M

Boundary comparison principle. A sub-mean-value function on a bounded open set, continuous up to the closure and ≤ M on the frontier, is ≤ M everywhere on the closure.

theorem Rado.MeanEqOn.eqOn_closure_of_frontier {u v : ℂ → ℝ} {U : Set ℂ} (hU : IsOpen U) (hUb : Bornology.IsBounded U) (hu : MeanEqOn u U) (hv : MeanEqOn v U) (huc : ContinuousOn u (closure U)) (hvc : ContinuousOn v (closure U)) (hb : Set.EqOn u v (frontier U)) : Set.EqOn u v (closure U)

Uniqueness from boundary values: two mean-value functions on a bounded open set, continuous up to the closure and equal on the frontier, agree on the closure.