The parabolic Hardy--Littlewood maximal function

This file defines the uncentred maximal function using the genuine parabolic metric from Basic. The weak estimate is proved by the Vitali covering theorem. The covering argument follows the general metric-measure argument in Carleson/ToMathlib/HardyLittlewood.lean from the Carleson project, released under Apache 2.0.

@[reducible, inline]

abbrev CKN.Foundation.Parabolic.hardyLittlewoodParabolicMetricBall (z : ParabolicPoint) (r : ℝ) : Set ParabolicPoint

Parabolic metric-ball family used by the maximal operator.

Equations

• CKN.Foundation.Parabolic.hardyLittlewoodParabolicMetricBall z r = Metric.ball z r

noncomputable def CKN.Foundation.Parabolic.parabolicMaximalFunction (f : ParabolicPoint → ENNReal) (z : ParabolicPoint) : ENNReal

Uncentered Hardy–Littlewood maximal function over parabolic balls.

Equations

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

theorem CKN.Foundation.Parabolic.parabolicMaximalFunction_average_le {f : ParabolicPoint → ENNReal} {c z : ParabolicPoint} {r : ℝ} (hz : z ∈ hardyLittlewoodParabolicMetricBall c r) : ⨍⁻ (y : ParabolicPoint) in hardyLittlewoodParabolicMetricBall c r, f y ∂MeasureTheory.volume ≤ parabolicMaximalFunction f z

theorem CKN.Foundation.Parabolic.lowerSemicontinuous_parabolicMaximalFunction (f : ParabolicPoint → ENNReal) : LowerSemicontinuous (parabolicMaximalFunction f)

theorem CKN.Foundation.Parabolic.measurable_parabolicMaximalFunction (f : ParabolicPoint → ENNReal) : Measurable (parabolicMaximalFunction f)

def CKN.Foundation.Parabolic.parabolicMaximalLevelBalls (f : ParabolicPoint → ENNReal) (l : ENNReal) (n : ℕ) : Set (ParabolicPoint × ℝ)

Parabolic balls of bounded positive radius with average above a chosen level.

Equations

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

theorem CKN.Foundation.Parabolic.measure_parabolicMaximalFunction_lt_le (f : ParabolicPoint → ENNReal) {l : ENNReal} (hl : 0 < l) : MeasureTheory.volume {z : ParabolicPoint | l < parabolicMaximalFunction f z} ≤ ENNReal.ofReal (10 ^ 5) / l * ∫⁻ (y : ParabolicPoint), f y