The Euclidean Hardy--Littlewood maximal function

This module defines the uncentred maximal function on Vec3 and proves its weak (1,1) estimate by the metric Vitali covering theorem.

@[reducible, inline]

abbrev CKN.Foundation.Euclidean.hardyLittlewoodMetricBall (c : Parabolic.Vec3) (r : ℝ) : Set Parabolic.Vec3

Metric-ball family used by the Euclidean Hardy–Littlewood maximal operator.

Equations

• CKN.Foundation.Euclidean.hardyLittlewoodMetricBall c r = Metric.ball c r

noncomputable def CKN.Foundation.Euclidean.maximalFunction (f : Parabolic.Vec3 → ENNReal) (z : Parabolic.Vec3) : ENNReal

The uncentred Hardy--Littlewood maximal function on Vec3.

Equations

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

theorem CKN.Foundation.Euclidean.volume_metricBall_eq {x : Parabolic.Vec3} {r : ℝ} (hr : 0 < r) : MeasureTheory.volume (Metric.ball x r) = ENNReal.ofReal ((2 * r) ^ 3)

theorem CKN.Foundation.Euclidean.maximalFunction_average_le {f : Parabolic.Vec3 → ENNReal} {c z : Parabolic.Vec3} {r : ℝ} (hz : z ∈ hardyLittlewoodMetricBall c r) : ⨍⁻ (y : Parabolic.Vec3) in hardyLittlewoodMetricBall c r, f y ∂MeasureTheory.volume ≤ maximalFunction f z

theorem CKN.Foundation.Euclidean.lowerSemicontinuous_maximalFunction (f : Parabolic.Vec3 → ENNReal) : LowerSemicontinuous (maximalFunction f)

theorem CKN.Foundation.Euclidean.measurable_maximalFunction (f : Parabolic.Vec3 → ENNReal) : Measurable (maximalFunction f)

def CKN.Foundation.Euclidean.maximalLevelBalls (f : Parabolic.Vec3 → ENNReal) (l : ENNReal) (n : ℕ) : Set (Parabolic.Vec3 × ℝ)

Positive-radius balls of bounded radius whose average exceeds the chosen level.

Equations

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

theorem CKN.Foundation.Euclidean.measure_maximalFunction_lt_le (f : Parabolic.Vec3 → ENNReal) {l : ENNReal} (hl : 0 < l) : MeasureTheory.volume {z : Parabolic.Vec3 | l < maximalFunction f z} ≤ ENNReal.ofReal (5 ^ 3) / l * ∫⁻ (y : Parabolic.Vec3), f y

The weak (1,1) estimate for the Euclidean maximal function.