Strong maximal estimates

This file records the direct layer-cake proof of the strong maximal estimate from the weak estimate in HardyLittlewood. The proof uses truncation at half the level and Tonelli's theorem, so it does not depend on an abstract interpolation package.

noncomputable def CKN.Foundation.Parabolic.parabolicMaximalStrongConstant (p : ℝ) : ENNReal

Explicit strong-type coefficient for the parabolic maximal operator.

Equations

• CKN.Foundation.Parabolic.parabolicMaximalStrongConstant p = 2 ^ p * ENNReal.ofReal (10 ^ 5) * ENNReal.ofReal p / ENNReal.ofReal (p - 1)

@[reducible, inline]

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

Parabolic ball family used in the strong-type maximal-function proof.

Equations

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

noncomputable def CKN.Foundation.Parabolic.highPart (f : ParabolicPoint → ENNReal) (a : ENNReal) : ParabolicPoint → ENNReal

Part of a nonnegative parabolic source strictly above the truncation level.

Equations

• CKN.Foundation.Parabolic.highPart f a = {z : CKN.Foundation.Parabolic.ParabolicPoint | a < f z}.indicator f

noncomputable def CKN.Foundation.Parabolic.lowPart (f : ParabolicPoint → ENNReal) (a : ENNReal) : ParabolicPoint → ENNReal

Part of a nonnegative parabolic source at or below the truncation level.

Equations

• CKN.Foundation.Parabolic.lowPart f a = {z : CKN.Foundation.Parabolic.ParabolicPoint | f z ≤ a}.indicator f

noncomputable def CKN.Foundation.Parabolic.positiveRpow (p t : ℝ) : ℝ

Positive-time power weight for the maximal-function distribution integral.

Equations

• CKN.Foundation.Parabolic.positiveRpow p t = if 0 < t then Real.exp ((p - 2) * Real.log t) else 0

noncomputable def CKN.Foundation.Parabolic.weightedTailIntegrand (f : ParabolicPoint → ENNReal) (p t : ℝ) (z : ParabolicPoint) : ENNReal

Weighted upper-tail integrand in the parabolic maximal-function estimate.

Equations

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

theorem CKN.Foundation.Parabolic.lintegral_rpow_parabolicMaximalFunction_le {f : ParabolicPoint → ENNReal} (hf : Measurable f) {p : ℝ} (hp : 1 < p) (hfp : ∫⁻ (z : ParabolicPoint), f z ^ p < ⊤) : ∫⁻ (z : ParabolicPoint), parabolicMaximalFunction f z ^ p ≤ parabolicMaximalStrongConstant p * ∫⁻ (z : ParabolicPoint), f z ^ p

theorem CKN.Foundation.Parabolic.lintegral_rpow_parabolicMaximalFunction_ofReal_le (f : ParabolicPoint → ℝ) (hf : Measurable f) {p : ℝ} (hp : 1 < p) (hfp : ∫⁻ (z : ParabolicPoint), ENNReal.ofReal ‖f z‖ ^ p < ⊤) : ∫⁻ (z : ParabolicPoint), parabolicMaximalFunction (fun (z : ParabolicPoint) => ENNReal.ofReal ‖f z‖) z ^ p ≤ parabolicMaximalStrongConstant p * ∫⁻ (z : ParabolicPoint), ENNReal.ofReal ‖f z‖ ^ p

theorem CKN.Foundation.Parabolic.setLIntegral_rpow_parabolicMaximalFunction_indicator_le (U : Set ParabolicPoint) (hU : MeasurableSet U) : IsOpen U → Bornology.IsBounded U → ∀ {f : ParabolicPoint → ENNReal} (hf : Measurable f) {p : ℝ} (hp : 1 < p) (hfp : ∫⁻ (z : ParabolicPoint) in U, f z ^ p < ⊤), ∫⁻ (z : ParabolicPoint) in U, parabolicMaximalFunction (U.indicator f) z ^ p ≤ parabolicMaximalStrongConstant p * ∫⁻ (z : ParabolicPoint) in U, f z ^ p