Comparing two ball means under the Campanato hypothesis

Every estimate Campanato's characterisation needs is one instance of a single comparison. If a ball B(z, σ) sits inside both B(x, r) and B(y, t), then averaging the elementary bound

(a - b)² ≤ 2 (u - a)² + 2 (u - b)²

over B(z, σ) turns the two Campanato integrals into a bound on (u_{x,r} - u_{y,t})², with the volume of the common ball in the denominator. That is sq_ballAverage_sub_le, and no Hölder or Cauchy-Schwarz inequality enters: the left-hand side is a constant, so its mean over B(z, σ) is itself.

Three instances follow, each with the single constant campanatoConst d = √(2^{d+4} / |B(0,1)|).

• abs_ballAverage_sub_le_of_le: two concentric balls of comparable radii, s ≤ r ≤ 2 s.
• abs_ballAverage_sub_half_le: the dyadic step s = r / 2, which drives the telescoping.
• abs_ballAverage_sub_of_dist_le: two centres at distance at most r / 2, at the same radius.

This is the computational core of property (H3) of Fernández-Real and Ros-Oton, Regularity Theory for Elliptic PDE.

theorem EllipticPdes.Campanato.sq_ballAverage_sub_le {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {u : EuclideanSpace ℝ (Fin d) → ℝ} {α M : ℝ} (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict Ω)) (hcamp : CampanatoOn Ω u α M) {x y z : EuclideanSpace ℝ (Fin d)} {r t σ : ℝ} (hr : 0 < r) (ht : 0 < t) (hσ : 0 < σ) (hxr : Metric.ball x r ⊆ Ω) (hyt : Metric.ball y t ⊆ Ω) (hzx : Metric.ball z σ ⊆ Metric.ball x r) (hzy : Metric.ball z σ ⊆ Metric.ball y t) : (ballAverage u x r - ballAverage u y t) ^ 2 * (σ ^ ↑d * unitBallVolume d) ≤ 2 * M ^ 2 * (r ^ (↑d + 2 * α) + t ^ (↑d + 2 * α))

Comparison of two ball means. When B(z, σ) lies inside both B(x, r) and B(y, t), the squared difference of the two means is controlled by the two Campanato integrals divided by the volume of the common ball. Averaging (a - b)² ≤ 2 (u - a)² + 2 (u - b)² over B(z, σ) is the whole proof.

noncomputable def EllipticPdes.Campanato.campanatoConst (d : ℕ) : ℝ

The single constant every mean comparison in this file uses.

Equations

• EllipticPdes.Campanato.campanatoConst d = √(2 ^ (d + 4) / EllipticPdes.Campanato.unitBallVolume d)

theorem EllipticPdes.Campanato.campanatoConst_pos {d : ℕ} : 0 < campanatoConst d

The Campanato constant is positive.

theorem EllipticPdes.Campanato.campanatoConst_nonneg {d : ℕ} : 0 ≤ campanatoConst d

The Campanato constant is nonnegative.

theorem EllipticPdes.Campanato.sq_campanatoConst_mul (d : ℕ) : campanatoConst d ^ 2 * unitBallVolume d = 2 ^ (d + 4)

The defining identity of the Campanato constant, in the cleared form the estimates use.

theorem EllipticPdes.Campanato.abs_ballAverage_sub_le_of_le {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {u : EuclideanSpace ℝ (Fin d) → ℝ} {α M : ℝ} (hα : 0 ≤ α) (hM : 0 ≤ M) (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict Ω)) (hcamp : CampanatoOn Ω u α M) {x : EuclideanSpace ℝ (Fin d)} {r s : ℝ} (hs : 0 < s) (hsr : s ≤ r) (hrs : r ≤ 2 * s) (hxr : Metric.ball x r ⊆ Ω) : |ballAverage u x r - ballAverage u x s| ≤ campanatoConst d * M * r ^ α

Concentric balls of comparable radii. For s ≤ r ≤ 2 s the two means differ by at most campanatoConst d · M · r^α.

theorem EllipticPdes.Campanato.abs_ballAverage_sub_half_le {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {u : EuclideanSpace ℝ (Fin d) → ℝ} {α M : ℝ} (hα : 0 ≤ α) (hM : 0 ≤ M) (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict Ω)) (hcamp : CampanatoOn Ω u α M) {x : EuclideanSpace ℝ (Fin d)} {r : ℝ} (hr : 0 < r) (hxr : Metric.ball x r ⊆ Ω) : |ballAverage u x r - ballAverage u x (r / 2)| ≤ campanatoConst d * M * r ^ α

Dyadic step. Halving the radius moves the mean by at most campanatoConst d · M · r^α. This is the estimate the telescoping sums.

theorem EllipticPdes.Campanato.abs_ballAverage_sub_of_dist_le {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {u : EuclideanSpace ℝ (Fin d) → ℝ} {α M : ℝ} (hM : 0 ≤ M) (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict Ω)) (hcamp : CampanatoOn Ω u α M) {x y : EuclideanSpace ℝ (Fin d)} {r : ℝ} (hr : 0 < r) (hxy : dist x y ≤ r / 2) (hxr : Metric.ball x r ⊆ Ω) (hyr : Metric.ball y r ⊆ Ω) : |ballAverage u x r - ballAverage u y r| ≤ campanatoConst d * M * r ^ α

Two centres at the same radius. When the centres are at distance at most r / 2, the two means differ by at most campanatoConst d · M · r^α.