Adams Bridge

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

theorem CKN.Foundation.Parabolic.Morrey.cylinderPowerIntegral_le_morreyNorm_pow {p q : ℝ} (hp : 0 < p) {f : ParabolicPoint → ℝ} : AEMeasurable f MeasureTheory.volume → ∀ {z : ParabolicPoint} {r : ℝ} (hr : 0 < r), cylinderPowerIntegral p f z r ≤ ENNReal.ofReal r ^ (5 * (1 - p / q)) * morreyNorm p q f ^ p

The cylinder integral is bounded by the Morrey seminorm at every scale.

theorem CKN.Foundation.Parabolic.Morrey.volume_metricBall_lower {z : ParabolicPoint} {r : ℝ} (hr : 0 < r) : ENNReal.ofReal (r ^ 5) * MeasureTheory.volume (parabolicCylinder 0 0 1) ≤ MeasureTheory.volume (Metric.ball z r)

A metric ball has the volume forced by the contained parabolic cylinder.

theorem CKN.Foundation.Parabolic.Morrey.metricBall_average_le_morreyNorm {q : ℝ} (hq : 1 ≤ q) {f : ParabolicPoint → ℝ} (hf : AEMeasurable f MeasureTheory.volume) {z : ParabolicPoint} {r : ℝ} (hr : 0 < r) : (∫⁻ (w : ParabolicPoint) in Metric.ball z r, ENNReal.ofReal |f w|) / MeasureTheory.volume (Metric.ball z r) ≤ ENNReal.ofReal 2 ^ (5 * (1 - 1 / q)) / MeasureTheory.volume (parabolicCylinder 0 0 1) * ENNReal.ofReal r ^ (-(5 / q)) * morreyNorm 1 q f

Metric-ball averages are controlled by the cylinder Morrey seminorm.

theorem CKN.Foundation.Parabolic.Morrey.metricBall_average_le_morreyNorm_of_lower_p {p q : ℝ} (hp : 1 ≤ p) (hpq : p ≤ q) {f : ParabolicPoint → ℝ} (hf : AEMeasurable f MeasureTheory.volume) {z : ParabolicPoint} {r : ℝ} (hr : 0 < r) : (∫⁻ (w : ParabolicPoint) in Metric.ball z r, ENNReal.ofReal |f w|) / MeasureTheory.volume (Metric.ball z r) ≤ ENNReal.ofReal 2 ^ (5 * (1 - 1 / q)) / MeasureTheory.volume (parabolicCylinder 0 0 1) * ENNReal.ofReal r ^ (-(5 / q)) * MeasureTheory.volume (parabolicCylinder 0 0 1) ^ (1 - 1 / p) * morreyNorm p q f

The same metric-ball estimate with a higher integrability exponent.

theorem CKN.Foundation.Parabolic.Morrey.parabolicMaximalFunction_add_le' {F G : ParabolicPoint → ENNReal} (hF : Measurable F) : Measurable G → ∀ (z : ParabolicPoint), parabolicMaximalFunction (F + G) z ≤ parabolicMaximalFunction F z + parabolicMaximalFunction G z

The maximal function is subadditive on nonnegative measurable data.

theorem CKN.Foundation.Parabolic.Morrey.parabolicMaximalFunction_compl_ball_le {p q : ℝ} (hp : 1 ≤ p) (hpq : p ≤ q) {f : ParabolicPoint → ℝ} (hf : Measurable f) {c z : ParabolicPoint} {r : ℝ} (hr : 0 < r) (hz : z ∈ Metric.ball c r) : parabolicMaximalFunction ((Metric.ball c (4 * r))ᶜ.indicator fun (w : ParabolicPoint) => ENNReal.ofReal |f w|) z ≤ ENNReal.ofReal 2 ^ (5 * (1 - 1 / q)) / MeasureTheory.volume (parabolicCylinder 0 0 1) * ENNReal.ofReal r ^ (-(5 / q)) * MeasureTheory.volume (parabolicCylinder 0 0 1) ^ (1 - 1 / p) * morreyNorm p q f

A maximal-function tail outside a doubled ball is bounded by a Morrey norm.