Campanato's characterisation of Hölder continuity

A function whose mean oscillation over balls decays at the rate r^α has a representative that is Hölder continuous with exponent α, and the Hölder constant is controlled by the Campanato constant. This is property (H3) of Fernández-Real and Ros-Oton, Regularity Theory for Elliptic PDE. The C^{k,α} scale of Schauder theory rests on it.

Two facts finish the proof. The Lebesgue differentiation theorem identifies campanatoLimit u with u almost everywhere, so the limit is a representative. The two-centre comparison abs_ballAverage_sub_of_dist_le, applied at the radius 2 |x - y|, together with the telescoped estimate at each of the two centres, bounds |campanatoLimit u x - campanatoLimit u y| by C · M · |x - y|^α.

The hypothesis quantifies over balls contained in B(c, R), so the pair estimate needs both B(x, 2|x-y|) and B(y, 2|x-y|) inside B(c, R). That holds for x, y in the concentric ball B(c, ρ) whenever 5ρ ≤ R, which is the form campanato_holderOnWith takes. Passing from the concentric ball to all of B(c, R) is a separate chaining argument, property (H1') of the same source, and is not carried out here.

theorem EllipticPdes.Campanato.closedBall_ae_eq_ball {d : ℕ} (hd : 0 < d) (x : EuclideanSpace ℝ (Fin d)) (r : ℝ) : Metric.closedBall x r =ᵐ[MeasureTheory.volume] Metric.ball x r

A closed ball and the corresponding open ball agree up to a null set, because a sphere is Lebesgue null in positive dimension.

theorem EllipticPdes.Campanato.campanatoLimit_ae_eq {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {u : EuclideanSpace ℝ (Fin d) → ℝ} {α M : ℝ} (hd : 0 < d) (hα : 0 < α) (hM : 0 ≤ M) (hΩ : IsOpen Ω) (hΩfin : MeasureTheory.volume Ω ≠ ⊤) (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict Ω)) (hcamp : CampanatoOn Ω u α M) : campanatoLimit u =ᵐ[MeasureTheory.volume.restrict Ω] u

Campanato limit as a representative of u. By the Lebesgue differentiation theorem the ball means converge to u almost everywhere, and by tendsto_ballAverage_campanatoLimit they converge to campanatoLimit u everywhere on the open set, so the two agree almost everywhere.

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

The Hölder constant Campanato's characterisation produces: two telescoped estimates, one at each centre, plus the two-centre comparison, all evaluated at the radius 2 |x - y|.

Equations

• EllipticPdes.Campanato.campanatoHolderConst d α = (2 * EllipticPdes.Campanato.campanatoLimitConst d α + EllipticPdes.Campanato.campanatoConst d) * 2 ^ α

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

The Hölder constant is nonnegative.

theorem EllipticPdes.Campanato.abs_campanatoLimit_sub_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 y : EuclideanSpace ℝ (Fin d)} (hx : x ∈ Ω) (hy : y ∈ Ω) (hne : x ≠ y) (hxr : Metric.ball x (2 * dist x y) ⊆ Ω) (hyr : Metric.ball y (2 * dist x y) ⊆ Ω) : |campanatoLimit u x - campanatoLimit u y| ≤ campanatoHolderConst d α * M * dist x y ^ α

Pair estimate. Two values of the Campanato limit differ by at most campanatoHolderConst d α · M · |x - y|^α, provided the balls of radius 2 |x - y| about the two points lie in Ω. Both means at that radius are within reach of their limits by the telescoped estimate, and they are within reach of each other by the two-centre comparison.

theorem EllipticPdes.Campanato.campanato_holderOnWith {d : ℕ} (hd : 0 < d) {u : EuclideanSpace ℝ (Fin d) → ℝ} {α M : ℝ} (hα : 0 < α) (hM : 0 ≤ M) {c : EuclideanSpace ℝ (Fin d)} {R ρ : ℝ} (hρ : 0 < ρ) (hRρ : 5 * ρ ≤ R) (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (Metric.ball c R))) (hcamp : CampanatoOn (Metric.ball c R) u α M) : campanatoLimit u =ᵐ[MeasureTheory.volume.restrict (Metric.ball c ρ)] u ∧ HolderOnWith (campanatoHolderConst d α * M).toNNReal α.toNNReal (campanatoLimit u) (Metric.ball c ρ)

Campanato's characterisation of Hölder continuity. Let u be square integrable on the ball B(c, R) and suppose its mean oscillation decays at the Campanato rate,

∫_{B(x,r)} |u - u_{x,r}|² ≤ M² r^{d + 2α} for every ball B(x, r) ⊆ B(c, R),

with 0 < α. Then campanatoLimit u is a representative of u on every concentric ball B(c, ρ) with 5ρ ≤ R, and it is Hölder continuous there with exponent α and constant campanatoHolderConst d α · M.

The factor 5 comes from the hypothesis: the pair estimate at x, y ∈ B(c, ρ) uses the balls of radius 2 |x - y| < 4ρ about both points, and those lie in B(c, R) exactly when 5ρ ≤ R.