Campanato decay of a Hölder function

A function that is Hölder of exponent α on Ω oscillates by at most K (2r)^α over any ball of radius r contained in Ω, so its mean oscillation there is bounded by K (2r)^α as well, and squaring and integrating over a ball of volume r^d |B(0,1)| gives the Campanato bound with

M = K · 2^α · √|B(0,1)|.

Together with campanato_holderOnWith this makes CampanatoOn a characterisation of Hölder continuity, which is the form Schauder theory consumes: a Hölder coefficient feeds in a Campanato decay rate, and a Campanato decay rate feeds out a Hölder bound.

theorem EllipticPdes.Campanato.abs_sub_ballAverage_le_of_holderOnWith {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {u : EuclideanSpace ℝ (Fin d) → ℝ} {α : ℝ} (hα : 0 < α) {K : NNReal} (hu : HolderOnWith K α.toNNReal u Ω) {x : EuclideanSpace ℝ (Fin d)} {r : ℝ} (hr : 0 < r) (hxr : Metric.ball x r ⊆ Ω) (y : EuclideanSpace ℝ (Fin d)) : y ∈ Metric.ball x r → |u y - ballAverage u x r| ≤ ↑K * (2 * r) ^ α

A Hölder function stays within K (2r)^α of its mean over any ball of radius r inside the set where the Hölder bound holds.

theorem EllipticPdes.Campanato.campanatoOn_of_holderOnWith {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {u : EuclideanSpace ℝ (Fin d) → ℝ} {α : ℝ} (hα : 0 < α) {K : NNReal} (hu : HolderOnWith K α.toNNReal u Ω) : CampanatoOn Ω u α (↑K * 2 ^ α * √(unitBallVolume d))

Converse of Campanato's characterisation. A function that is Hölder of exponent α with constant K on Ω satisfies the Campanato decay hypothesis on Ω with constant K · 2^α · √|B(0,1)|. Squaring the mean-oscillation bound K (2r)^α and integrating over a ball of volume r^d |B(0,1)| is the whole proof.