Dyadic telescoping estimate and Campanato limit

Halving the radius moves the ball mean by at most campanatoConst d · M · r^α, so the means at the dyadic radii r, r/2, r/4, … form a Cauchy sequence with an explicit geometric bound. Summing that geometric series and closing the gap to an arbitrary smaller radius with abs_ballAverage_sub_le_of_le gives the estimate the whole characterisation rests on,

|u_{x,r} - u_{x,s}| ≤ campanatoLimitConst d α · M · r^α for every 0 < s ≤ r,

with B(x,r) ⊆ Ω. Since the bound does not degrade as s → 0, the means converge, and the limit

campanatoLimit u x = lim_k u_{x, 2^{-k}}

inherits the same bound. That limit is the Hölder representative produced in EllipticPdes.Campanato.Holder.

noncomputable def EllipticPdes.Campanato.campanatoLimitConst (d : ℕ) (α : ℝ) : ℝ

The constant of the telescoped estimate: the geometric sum of the dyadic steps, plus one more step to reach an arbitrary radius below the ladder.

Equations

• EllipticPdes.Campanato.campanatoLimitConst d α = EllipticPdes.Campanato.campanatoConst d * (1 / (1 - (1 / 2) ^ α) + 1)

theorem EllipticPdes.Campanato.campanatoLimitConst_nonneg {d : ℕ} {α : ℝ} (hα : 0 < α) : 0 ≤ campanatoLimitConst d α

The telescoped constant is nonnegative.

theorem EllipticPdes.Campanato.abs_ballAverage_sub_le_of_le_radius {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) (hxr : Metric.ball x r ⊆ Ω) : |ballAverage u x r - ballAverage u x s| ≤ campanatoLimitConst d α * M * r ^ α

Telescoped estimate. For every radius s below r, with B(x, r) ⊆ Ω, the two means differ by at most campanatoLimitConst d α · M · r^α. The bound is uniform in s, which is what makes the means converge as the radius shrinks.

noncomputable def EllipticPdes.Campanato.campanatoLimit {d : ℕ} (u : EuclideanSpace ℝ (Fin d) → ℝ) (x : EuclideanSpace ℝ (Fin d)) : ℝ

Campanato limit. The limit of the means of u over the balls B(x, 2^{-k}). Under the Campanato hypothesis this limit exists at every point of the open set, equals u almost everywhere, and is the Hölder representative.

Equations

• EllipticPdes.Campanato.campanatoLimit u x = Filter.atTop.limUnder fun (k : ℕ) => EllipticPdes.Campanato.ballAverage u x ((1 / 2) ^ k)

theorem EllipticPdes.Campanato.tendsto_ballAverage_campanatoLimit {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {u : EuclideanSpace ℝ (Fin d) → ℝ} {α M : ℝ} (hα : 0 < α) (hM : 0 ≤ M) (hΩ : IsOpen Ω) (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict Ω)) (hcamp : CampanatoOn Ω u α M) {x : EuclideanSpace ℝ (Fin d)} (hx : x ∈ Ω) : Filter.Tendsto (fun (k : ℕ) => ballAverage u x ((1 / 2) ^ k)) Filter.atTop (nhds (campanatoLimit u x))

The dyadic means converge at every point of the open set.

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

Distance from the mean at any admissible radius to the limit. This is the estimate the Hölder bound consumes: the representative is reached from every scale at the Campanato rate.