Harmonic and subharmonic functions on a Riemann surface

Chartwise notions for u : X → ℝ on the eval problem's Riemann surface (step 3 of Rado/PLAN.md): SurfaceHarmonicOn / SurfaceSubharmonicOn via chart representatives over the maximal atlas (so no subharmonic ∘ holomorphic invariance is ever needed), chart invariance (of_chartwise), and the local-to-global bridge SubMeanLocalOn — the sub-mean-value inequality on small circles implies it on all circles, via the maximum principle and comparison with the Poisson extension.

def Rado.chartImage {X : Type u_1} [TopologicalSpace X] (e : OpenPartialHomeomorph X ℂ) (s : Set X) : Set ℂ

The image of s in the chart e.

Equations

• Rado.chartImage e s = ↑e '' (s ∩ e.source)

theorem Rado.isOpen_chartImage {X : Type u_1} [TopologicalSpace X] (e : OpenPartialHomeomorph X ℂ) {s : Set X} (hs : IsOpen s) : IsOpen (chartImage e s)

theorem Rado.chartImage_subset_target {X : Type u_1} [TopologicalSpace X] (e : OpenPartialHomeomorph X ℂ) (s : Set X) : chartImage e s ⊆ e.target

theorem Rado.mem_chartImage_of_mem {X : Type u_1} [TopologicalSpace X] {e : OpenPartialHomeomorph X ℂ} {s : Set X} {x : X} (hx : x ∈ s) (hxe : x ∈ e.source) : ↑e x ∈ chartImage e s

theorem Rado.mapsTo_symm_chartImage {X : Type u_1} [TopologicalSpace X] {e : OpenPartialHomeomorph X ℂ} {s : Set X} : Set.MapsTo (↑e.symm) (chartImage e s) s

theorem Rado.continuousOn_comp_chart_symm {X : Type u_1} [TopologicalSpace X] {g : X → ℝ} (e : OpenPartialHomeomorph X ℂ) {s : Set X} (hg : ContinuousOn g s) : ContinuousOn (g ∘ ↑e.symm) (chartImage e s)

A continuous function on s reads as continuous through any chart.

Harmonic and subharmonic functions on a Riemann surface

def Rado.SurfaceHarmonicOn {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (u : X → ℝ) (s : Set X) : Prop

u : X → ℝ is harmonic on s: every chart representative is harmonic.

Equations

• Rado.SurfaceHarmonicOn u s = ∀ e ∈ Rado.riemannAtlas X, InnerProductSpace.HarmonicOnNhd (u ∘ ↑e.symm) (Rado.chartImage e s)

structure Rado.SurfaceSubharmonicOn {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (g : X → ℝ) (s : Set X) : Prop

g : X → ℝ is subharmonic on s: continuous, and every chart representative satisfies the sub-mean-value inequality.

• continuousOn : ContinuousOn g s
• subMeanOn (e : OpenPartialHomeomorph X ℂ) : e ∈ riemannAtlas X → SubMeanOn (g ∘ ↑e.symm) (chartImage e s)

theorem Rado.SurfaceHarmonicOn.continuousOn {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] {u : X → ℝ} {s : Set X} (hu : SurfaceHarmonicOn u s) : ContinuousOn u s

theorem Rado.SurfaceHarmonicOn.mono {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {u : X → ℝ} {s : Set X} (hu : SurfaceHarmonicOn u s) {t : Set X} (hts : t ⊆ s) : SurfaceHarmonicOn u t

theorem Rado.SurfaceHarmonicOn.of_chartwise {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {u : X → ℝ} {s : Set X} (h : ∀ x ∈ s, ∃ e ∈ riemannAtlas X, x ∈ e.source ∧ InnerProductSpace.HarmonicAt (u ∘ ↑e.symm) (↑e x)) : SurfaceHarmonicOn u s

To be harmonic it suffices to be harmonic in one maximal-atlas chart around each point (chart invariance, via HarmonicOnNhd.comp_analytic).

theorem Rado.SurfaceHarmonicOn.surfaceSubharmonicOn {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] {u : X → ℝ} {s : Set X} (hu : SurfaceHarmonicOn u s) : SurfaceSubharmonicOn u s

theorem Rado.SurfaceHarmonicOn.neg {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {u : X → ℝ} {s : Set X} (hu : SurfaceHarmonicOn u s) : SurfaceHarmonicOn (-u) s

theorem Rado.SurfaceSubharmonicOn.mono {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {g : X → ℝ} {s : Set X} (hg : SurfaceSubharmonicOn g s) {t : Set X} (hts : t ⊆ s) : SurfaceSubharmonicOn g t

theorem Rado.SurfaceSubharmonicOn.max {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {g₁ g₂ : X → ℝ} {s : Set X} (h₁ : SurfaceSubharmonicOn g₁ s) (h₂ : SurfaceSubharmonicOn g₂ s) : SurfaceSubharmonicOn (fun (x : X) => Max.max (g₁ x) (g₂ x)) s

Local-to-global bridge for the sub-mean-value property

SubMeanOn (in Rado/Complex/SubMean.lean) demands the sub-mean inequality on every circle whose closed disk lies in the domain. Verifications (gluing in the harmonic replacement) naturally produce only small circles. The bridge is classical: small circles give the maximum principle, the maximum principle gives comparison with the Poisson extension on any closed disk, and comparison gives the inequality on the full circle (InnerProductSpace.HarmonicContOnCl.circleAverage_eq closes the loop at the boundary radius).

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

The bridge: on an open set, the sub-mean-value inequality on small circles implies it on all circles (compare with the Poisson extension on any legal closed disk).

theorem Rado.SurfaceSubharmonicOn.of_locally {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {g : X → ℝ} {s : Set X} (h : ∀ x ∈ s, ∃ (V : Set X), IsOpen V ∧ x ∈ V ∧ V ⊆ s ∧ SurfaceSubharmonicOn g V) : SurfaceSubharmonicOn g s

Subharmonicity is local.