Ball means and the Campanato decay hypothesis

The C^{k,α} scale of Schauder theory rests on Campanato's characterisation of Hölder continuity: a function whose mean oscillation over balls decays like r^α has a Hölder representative of exponent α. This file fixes the two objects that characterisation is stated through, the mean

u_{x,r} = ⨍_{B(x,r)} u

written ballAverage u x r, and the decay hypothesis

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

written CampanatoOn Ω u α M. The hypothesis quantifies over balls contained in Ω, which is the form property (H3) of Fernández-Real and Ros-Oton takes, so every mean in sight is a mean over a ball and has the exact volume r^d · |B(0,1)|.

The rest of the file records what the estimates downstream need: the volume of a ball as a real number, and the integrability of u and of (u - c)² on a ball, both read off from MemLp u 2 (volume.restrict Ω).

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

The volume of the unit ball of EuclideanSpace ℝ (Fin d), as a real number. Every ball volume in this library is a multiple of it, so it is convenient to name it once.

Equations

• EllipticPdes.Campanato.unitBallVolume d = (MeasureTheory.volume (Metric.ball 0 1)).toReal

theorem EllipticPdes.Campanato.unitBallVolume_pos {d : ℕ} : 0 < unitBallVolume d

The unit ball has positive volume.

theorem EllipticPdes.Campanato.measureReal_ball {d : ℕ} (x : EuclideanSpace ℝ (Fin d)) {r : ℝ} (hr : 0 < r) : MeasureTheory.volume.real (Metric.ball x r) = r ^ d * unitBallVolume d

The volume of B(x, r) is r^d times the volume of the unit ball.

theorem EllipticPdes.Campanato.measureReal_ball_rpow {d : ℕ} (x : EuclideanSpace ℝ (Fin d)) {r : ℝ} (hr : 0 < r) : MeasureTheory.volume.real (Metric.ball x r) = r ^ ↑d * unitBallVolume d

The volume of B(x, r) written with a real exponent, the form the decay hypothesis uses.

instance EllipticPdes.Campanato.isFiniteMeasure_restrict_ball {d : ℕ} (x : EuclideanSpace ℝ (Fin d)) (r : ℝ) : MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict (Metric.ball x r))

The restriction of Lebesgue measure to a ball is finite.

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

Mean of u over the ball B(x, r). Campanato's hypothesis measures the oscillation of u about this value, and the characterisation produces the Hölder representative as the limit of these means as r → 0.

Equations

• EllipticPdes.Campanato.ballAverage u x r = ⨍ (y : EuclideanSpace ℝ (Fin d)) in Metric.ball x r, u y

def EllipticPdes.Campanato.CampanatoOn {d : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin d))) (u : EuclideanSpace ℝ (Fin d) → ℝ) (α M : ℝ) : Prop

Campanato decay hypothesis. The mean oscillation of u over every ball contained in Ω decays at the rate r^{d + 2α}, with constant M. For 0 < α ≤ 1 this forces u to have a Hölder representative of exponent α on the interior of Ω; that is the content of EllipticPdes.Campanato.campanato_holderOnWith.

Equations

• One or more equations did not get rendered due to their size.

theorem EllipticPdes.Campanato.CampanatoOn.mono {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {u : EuclideanSpace ℝ (Fin d) → ℝ} {α M M' : ℝ} (h : CampanatoOn Ω u α M) (hM : 0 ≤ M) (hMM : M ≤ M') : CampanatoOn Ω u α M'

The decay hypothesis weakens when the constant grows.

theorem EllipticPdes.Campanato.CampanatoOn.mono_set {d : ℕ} {Ω Ω' : Set (EuclideanSpace ℝ (Fin d))} {u : EuclideanSpace ℝ (Fin d) → ℝ} {α M : ℝ} (h : CampanatoOn Ω u α M) (hΩ : Ω' ⊆ Ω) : CampanatoOn Ω' u α M

The decay hypothesis shrinks with the domain.

theorem EllipticPdes.Campanato.memLp_two_ball {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {u : EuclideanSpace ℝ (Fin d) → ℝ} (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict Ω)) {x : EuclideanSpace ℝ (Fin d)} {r : ℝ} (hsub : Metric.ball x r ⊆ Ω) : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (Metric.ball x r))

Square integrability on Ω restricts to any ball inside Ω.

theorem EllipticPdes.Campanato.memLp_two_sub_const {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {u : EuclideanSpace ℝ (Fin d) → ℝ} (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict Ω)) {x : EuclideanSpace ℝ (Fin d)} {r : ℝ} (hsub : Metric.ball x r ⊆ Ω) (c : ℝ) : MeasureTheory.MemLp (fun (y : EuclideanSpace ℝ (Fin d)) => u y - c) 2 (MeasureTheory.volume.restrict (Metric.ball x r))

Subtracting a constant preserves square integrability on a ball.

theorem EllipticPdes.Campanato.integrableOn_sq_sub_const {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {u : EuclideanSpace ℝ (Fin d) → ℝ} (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict Ω)) {x : EuclideanSpace ℝ (Fin d)} {r : ℝ} (hsub : Metric.ball x r ⊆ Ω) (c : ℝ) : MeasureTheory.IntegrableOn (fun (y : EuclideanSpace ℝ (Fin d)) => (u y - c) ^ 2) (Metric.ball x r) MeasureTheory.volume

The squared deviation of u from a constant is integrable on a ball inside Ω.