Harmonic replacement and Perron's principle

Step 4 of Rado/PLAN.md: surfaceReplace (replace a subharmonic function inside a chart disk by the Dirichlet solution of its boundary values, Anghel– Stan Remark 4 — Hausdorffness genuinely needed, see the counterexample at surfaceReplace_surfaceSubharmonicOn), Perron families, Harnack's principle for monotone sequences of harmonic functions, and Perron's principle: the upper envelope of a Perron family is harmonic (IsPerronFamily.surfaceHarmonicOn_perronSup; Anghel–Stan Theorem 6, Hubbard Prop. 1.2.3).

Harmonic replacement and Perron families

noncomputable def Rado.surfaceReplace {X : Type u_1} [TopologicalSpace X] (g : X → ℝ) (e : OpenPartialHomeomorph X ℂ) (c : ℂ) (r : ℝ) : X → ℝ

Replace g inside the closed disk e.symm '' closedBall c r by the Dirichlet solution with g's boundary values, read through the chart.

Equations

• Rado.surfaceReplace g e c r x = if _h : x ∈ e.source ∧ ↑e x ∈ Metric.closedBall c r then Rado.poissonExtension (g ∘ ↑e.symm) c r (↑e x) else g x

structure Rado.IsReplaceDisk {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (e : OpenPartialHomeomorph X ℂ) (c : ℂ) (r : ℝ) (s : Set X) : Prop

Data for a legal replacement disk: a maximal-atlas chart and a closed disk in its target whose preimage lies in s.

• mem_atlas : e ∈ riemannAtlas X
• r_pos : 0 < r
• closedBall_subset : Metric.closedBall c r ⊆ e.target
• preimage_subset : ↑e.symm '' Metric.closedBall c r ⊆ s

theorem Rado.IsReplaceDisk.compact_preimage {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {s : Set X} {e : OpenPartialHomeomorph X ℂ} {c : ℂ} {r : ℝ} (hd : IsReplaceDisk e c r s) : IsCompact (↑e.symm '' Metric.closedBall c r)

theorem Rado.surfaceReplace_eqOn_compl {X : Type u_1} [TopologicalSpace X] {g : X → ℝ} {e : OpenPartialHomeomorph X ℂ} {c : ℂ} {r : ℝ} : Set.EqOn (surfaceReplace g e c r) g (↑e.symm '' Metric.closedBall c r)ᶜ

The replacement agrees with g off the closed replacement disk.

theorem Rado.surfaceReplace_surfaceSubharmonicOn {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {g : X → ℝ} {s : Set X} {e : OpenPartialHomeomorph X ℂ} {c : ℂ} {r : ℝ} [T2Space X] (hs : IsOpen s) (hg : SurfaceSubharmonicOn g s) (hd : IsReplaceDisk e c r s) : SurfaceSubharmonicOn (surfaceReplace g e c r) s

The replacement is subharmonic (Anghel–Stan Remark 4): with [T2Space X] the compact replacement disk is closed, and the replacement is subharmonic on s — harmonic inside the disk, equal to g outside, and the sub-mean inequality glues across the circle because g ≤ surfaceReplace g there.

The Hausdorff hypothesis is genuinely needed: on the plane with doubled origin, with g = ‖chart value‖², the replacement on the copy-1 unit disk is ≡ 1 on the shared punctured disk but 0 at the doubled origin, which lies in the closure of the replacement disk but outside e.source — so the replacement fails to be continuous, let alone subharmonic.

theorem Rado.le_surfaceReplace {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {g : X → ℝ} {s : Set X} {e : OpenPartialHomeomorph X ℂ} {c : ℂ} {r : ℝ} (hg : SurfaceSubharmonicOn g s) (hd : IsReplaceDisk e c r s) (x : X) : x ∈ s → g x ≤ surfaceReplace g e c r x

g is dominated by its replacement (comparison principle).

theorem Rado.surfaceReplace_surfaceHarmonicOn {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {g : X → ℝ} {s : Set X} {e : OpenPartialHomeomorph X ℂ} {c : ℂ} {r : ℝ} (hg : SurfaceSubharmonicOn g s) (hd : IsReplaceDisk e c r s) : SurfaceHarmonicOn (surfaceReplace g e c r) (↑e.symm '' Metric.ball c r)

The replacement is harmonic in the open replacement disk.

theorem Rado.surfaceReplace_mem_Icc {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {g : X → ℝ} {s : Set X} {e : OpenPartialHomeomorph X ℂ} {c : ℂ} {r : ℝ} (hg : SurfaceSubharmonicOn g s) (hd : IsReplaceDisk e c r s) (hb : ∀ x ∈ s, g x ∈ Set.Icc 0 1) (x : X) : x ∈ s → surfaceReplace g e c r x ∈ Set.Icc 0 1

The replacement stays in [0,1] if g does (on s).

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

A Perron family on s: a nonempty set of [0,1]-valued subharmonic functions, closed under pairwise max and under harmonic replacement on disks inside s (Anghel–Stan Definition 5, with the [0,1] normalization that suffices for Radó).

• nonempty : 𝓕.Nonempty
• subharmonic (g : X → ℝ) : g ∈ 𝓕 → SurfaceSubharmonicOn g s
• bounds (g : X → ℝ) : g ∈ 𝓕 → ∀ x ∈ s, g x ∈ Set.Icc 0 1
• max_mem (g₁ : X → ℝ) : g₁ ∈ 𝓕 → ∀ g₂ ∈ 𝓕, (fun (x : X) => max (g₁ x) (g₂ x)) ∈ 𝓕
• replace_mem (g : X → ℝ) : g ∈ 𝓕 → ∀ (e : OpenPartialHomeomorph X ℂ) (c : ℂ) (r : ℝ), IsReplaceDisk e c r s → surfaceReplace g e c r ∈ 𝓕

noncomputable def Rado.perronSup {X : Type u_1} (𝓕 : Set (X → ℝ)) : X → ℝ

The upper envelope of a family of functions.

Equations

• Rado.perronSup 𝓕 x = sSup ((fun (g : X → ℝ) => g x) '' 𝓕)

Harnack's principle for monotone sequences of harmonic functions

The Perron approximation sequence

theorem Rado.IsPerronFamily.surfaceHarmonicOn_perronSup {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] {𝓕 : Set (X → ℝ)} {s : Set X} (hs : IsOpen s) (h𝓕 : IsPerronFamily 𝓕 s) : SurfaceHarmonicOn (perronSup 𝓕) s

Perron's principle (Anghel–Stan Theorem 6, Hubbard Prop. 1.2.3): the upper envelope of a Perron family is harmonic.

theorem Rado.IsPerronFamily.le_perronSup {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {𝓕 : Set (X → ℝ)} {s : Set X} (h𝓕 : IsPerronFamily 𝓕 s) {g : X → ℝ} (hg : g ∈ 𝓕) (x : X) : x ∈ s → g x ≤ perronSup 𝓕 x

theorem Rado.IsPerronFamily.perronSup_le {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {𝓕 : Set (X → ℝ)} {s : Set X} (h𝓕 : IsPerronFamily 𝓕 s) {M : ℝ} {x : X} (hM : ∀ g ∈ 𝓕, g x ≤ M) : perronSup 𝓕 x ≤ M

theorem Rado.subMeanOn_congr {g₁ g₂ : ℂ → ℝ} {s : Set ℂ} (hg : SubMeanOn g₁ s) (h : Set.EqOn g₂ g₁ s) : SubMeanOn g₂ s

SubMeanOn transfers along equality on the domain.

theorem Rado.surfaceSubharmonicOn_congr {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {g₁ g₂ : X → ℝ} {s : Set X} (hg : SurfaceSubharmonicOn g₁ s) (h : Set.EqOn g₂ g₁ s) : SurfaceSubharmonicOn g₂ s

SurfaceSubharmonicOn transfers along equality on the domain.