Harnack's inequality on a planar disk

This file proves the Harnack inequality for real-valued harmonic functions on a disk in the complex plane. Mathlib's Poisson integral formula writes the value at an interior point as a circle average weighted by the Poisson kernel; its sharp upper and lower bounds give the centered Harnack estimate directly.

The Poisson formula first gives the estimate from a sign hypothesis on a boundary circle and propagates that sign throughout the disk. Applying this result on concentric intermediate disks and passing to the outer radius gives the usual formulation for a nonnegative harmonic function on an open disk. The pairwise form on a closed subdisk has the standard constant ((R + r) / (R - r)) ^ 2.

The argument is the classical Poisson-kernel proof; see Evans, Partial Differential Equations, Chapter 2, Section 2.2.

Main declarations

• TauCeti.harnack_inequality_center: the sharp two-sided comparison with the value at the center of a disk.
• TauCeti.harnack_inequality: any two values on a smaller closed disk differ by at most the standard Harnack factor.
• TauCeti.eq_zero_on_ball_of_harmonicOnNhd_of_nonneg_of_eq_zero: a nonnegative harmonic function that vanishes at an interior point vanishes throughout the disk.

theorem TauCeti.harnack_inequality_center_of_nonneg_on_sphere {f : ℂ → ℝ} {c w : ℂ} {R : ℝ} (hf : InnerProductSpace.HarmonicOnNhd f (Metric.closedBall c R)) (hnonneg : ∀ z ∈ Metric.sphere c R, 0 ≤ f z) (hw : w ∈ Metric.ball c R) : (R - ‖w - c‖) / (R + ‖w - c‖) * f c ≤ f w ∧ f w ≤ (R + ‖w - c‖) / (R - ‖w - c‖) * f c

The centered Harnack inequality on a planar disk.

If f is harmonic on a neighborhood of the closed disk of radius R about c and is nonnegative on its boundary circle, then every w in the open disk satisfies

(R - ‖w - c‖) / (R + ‖w - c‖) * f c ≤ f w ≤ (R + ‖w - c‖) / (R - ‖w - c‖) * f c.

The boundary-only sign assumption is sufficient: both inequalities follow from the Poisson integral formula and the pointwise bounds on the Poisson kernel.

theorem TauCeti.nonneg_of_mem_ball_of_harmonicOnNhd_of_nonneg_on_sphere {f : ℂ → ℝ} {c w : ℂ} {R : ℝ} (hf : InnerProductSpace.HarmonicOnNhd f (Metric.closedBall c R)) (hnonneg : ∀ z ∈ Metric.sphere c R, 0 ≤ f z) (hw : w ∈ Metric.ball c R) : 0 ≤ f w

A function harmonic near a closed planar disk and nonnegative on its boundary circle is nonnegative throughout the open disk.

theorem TauCeti.harnack_inequality_of_nonneg_on_sphere {f : ℂ → ℝ} {c : ℂ} {R : ℝ} (hf : InnerProductSpace.HarmonicOnNhd f (Metric.closedBall c R)) (hnonneg : ∀ z ∈ Metric.sphere c R, 0 ≤ f z) {r : ℝ} (hr : 0 ≤ r) (hrR : r < R) {x y : ℂ} (hx : x ∈ Metric.closedBall c r) (hy : y ∈ Metric.closedBall c r) : f x ≤ ((R + r) / (R - r)) ^ 2 * f y

Harnack's inequality on a smaller planar disk.

Let 0 ≤ r < R. If f is harmonic on a neighborhood of closedBall c R and nonnegative on its boundary, then for any x, y ∈ closedBall c r,

f x ≤ ((R + r) / (R - r)) ^ 2 * f y.

This pairwise form follows by comparing both values with f c.

theorem TauCeti.eq_zero_on_ball_of_harmonicOnNhd_of_nonneg_on_sphere_of_eq_zero {f : ℂ → ℝ} {c w : ℂ} {R : ℝ} (hf : InnerProductSpace.HarmonicOnNhd f (Metric.closedBall c R)) (hnonneg : ∀ z ∈ Metric.sphere c R, 0 ≤ f z) (hw : w ∈ Metric.ball c R) (hfw : f w = 0) : Set.EqOn f 0 (Metric.ball c R)

If a function is harmonic near a closed planar disk, is nonnegative on the boundary, and vanishes at an interior point, then it vanishes throughout the open disk.

This is the zero case of Harnack's inequality, and is the strong minimum principle for this setting.

theorem TauCeti.harnack_inequality_center {f : ℂ → ℝ} {c w : ℂ} {R : ℝ} (hf : InnerProductSpace.HarmonicOnNhd f (Metric.ball c R)) (hnonneg : ∀ z ∈ Metric.ball c R, 0 ≤ f z) (hw : w ∈ Metric.ball c R) : (R - ‖w - c‖) / (R + ‖w - c‖) * f c ≤ f w ∧ f w ≤ (R + ‖w - c‖) / (R - ‖w - c‖) * f c

The centered Harnack inequality on an open planar disk.

If f is harmonic and nonnegative throughout the open disk of radius R about c, then every w in the disk satisfies the sharp two-sided comparison with f c.

theorem TauCeti.harnack_inequality {f : ℂ → ℝ} {c : ℂ} {R : ℝ} (hf : InnerProductSpace.HarmonicOnNhd f (Metric.ball c R)) (hnonneg : ∀ z ∈ Metric.ball c R, 0 ≤ f z) {r : ℝ} (hr : 0 ≤ r) (hrR : r < R) {x y : ℂ} (hx : x ∈ Metric.closedBall c r) (hy : y ∈ Metric.closedBall c r) : f x ≤ ((R + r) / (R - r)) ^ 2 * f y

Harnack's inequality on a smaller closed disk.

Let 0 ≤ r < R. If f is harmonic and nonnegative throughout ball c R, then for any x, y ∈ closedBall c r,

f x ≤ ((R + r) / (R - r)) ^ 2 * f y.

theorem TauCeti.eq_zero_on_ball_of_harmonicOnNhd_of_nonneg_of_eq_zero {f : ℂ → ℝ} {c w : ℂ} {R : ℝ} (hf : InnerProductSpace.HarmonicOnNhd f (Metric.ball c R)) (hnonneg : ∀ z ∈ Metric.ball c R, 0 ≤ f z) (hw : w ∈ Metric.ball c R) (hfw : f w = 0) : Set.EqOn f 0 (Metric.ball c R)

A nonnegative harmonic function on an open planar disk that vanishes at one point vanishes throughout the disk. This is the zero case of Harnack's inequality.