Harnack's inequality in every dimension

Let E be a finite-dimensional real inner product space of dimension n. This file proves Harnack's inequality for nonnegative harmonic functions u : E → ℝ: on a compact subset K of a preconnected open set U, the values of u are comparable,

u x ≤ C * u y for all x, y ∈ K,

with a constant C that depends only on K and U, not on u. Equivalently, sup_K u ≤ C * inf_K u.

The argument is the classical one through the mean-value property on balls (InnerProductSpace.HarmonicOnNhd.setIntegral_ball_eq). If closedBall x r ⊆ closedBall y s, then for u ≥ 0 the integral of u over ball x r is at most its integral over ball y s, and the mean-value property turns this into r ^ n * u x ≤ s ^ n * u y. Choosing the balls as in Gilbarg–Trudinger gives the local estimate u x ≤ 3 ^ n * u y for x, y ∈ ball c r when u is harmonic and nonnegative on ball c (4 * r). The global inequality follows by chaining the local one: along the preconnected set U for comparability of any two points, and over a finite cover of K for uniformity of the constant.

The planar inequality with the sharp Poisson-kernel constant is TauCeti.Analysis.PDE.Harnack.Planar.

Main declarations

• InnerProductSpace.HarmonicOnNhd.le_div_pow_mul_of_nonneg: nested balls compare values, u x ≤ (s / r) ^ n * u y when r + dist x y ≤ s.
• InnerProductSpace.HarmonicOnNhd.le_three_pow_mul_of_nonneg: the local Harnack inequality u x ≤ 3 ^ n * u y on ball c r, for u harmonic and nonnegative on ball c (4 * r).
• IsCompact.harnack_inequality: Harnack's inequality on a compact subset of a preconnected open set.

References

• L. C. Evans, Partial Differential Equations, Section 2.2.2, Theorem 11.
• D. Gilbarg, N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, Theorem 2.5.

theorem InnerProductSpace.HarmonicOnNhd.le_div_pow_mul_of_nonneg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {u : E → ℝ} {x y : E} {r s : ℝ} (hu : HarmonicOnNhd u (Metric.closedBall y s)) (hnonneg : ∀ z ∈ Metric.ball y s, 0 ≤ u z) (hr : 0 < r) (hxy : r + dist x y ≤ s) : u x ≤ (s / r) ^ Module.finrank ℝ E * u y

Nested balls compare the values of a nonnegative harmonic function. If u is harmonic on a neighbourhood of closedBall y s and nonnegative on ball y s, and closedBall x r lies inside closedBall y s in the sense that r + dist x y ≤ s, then u x ≤ (s / r) ^ n * u y, where n is the dimension of E.

theorem InnerProductSpace.HarmonicOnNhd.le_three_pow_mul_of_nonneg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {u : E → ℝ} {x y c : E} {r : ℝ} (hu : HarmonicOnNhd u (Metric.ball c (4 * r))) (hnonneg : ∀ z ∈ Metric.ball c (4 * r), 0 ≤ u z) (hx : x ∈ Metric.ball c r) (hy : y ∈ Metric.ball c r) : u x ≤ 3 ^ Module.finrank ℝ E * u y

The local Harnack inequality. If u is harmonic and nonnegative on ball c (4 * r), then any two of its values on ball c r are within the factor 3 ^ n of each other, where n is the dimension of E.

theorem IsCompact.harnack_inequality {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {K U : Set E} (hK : IsCompact K) (hU : IsOpen U) (hUc : IsPreconnected U) (hKU : K ⊆ U) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (u : E → ℝ), InnerProductSpace.HarmonicOnNhd u U → (∀ z ∈ U, 0 ≤ u z) → ∀ x ∈ K, ∀ y ∈ K, u x ≤ C * u y

Harnack's inequality. Let K be a compact subset of a preconnected open set U. There is a constant C, depending only on K and U, such that every function u harmonic and nonnegative on U satisfies u x ≤ C * u y for all x, y ∈ K; that is, sup_K u ≤ C * inf_K u.