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.Euclidean.maximalStrongConstant (p : ℝ) : ENNReal

Explicit strong-type coefficient for the Euclidean maximal operator.

Equations

• CKN.Foundation.Euclidean.maximalStrongConstant p = 2 ^ p * ENNReal.ofReal (5 ^ 3) * ENNReal.ofReal p / ENNReal.ofReal (p - 1)

@[reducible, inline]

abbrev CKN.Foundation.Euclidean.strongTypeMetricBall (z : Parabolic.Vec3) (r : ℝ) : Set Parabolic.Vec3

Metric-ball family used in the maximal operator's strong-type estimate.

Equations

• CKN.Foundation.Euclidean.strongTypeMetricBall z r = Metric.ball z r

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

Part of an extended nonnegative function strictly above a truncation level.

Equations

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

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

Part of an extended nonnegative function at or below a truncation level.

Equations

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

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

The weight t ^ (p - 2) on positive inputs, extended by zero elsewhere.

Equations

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

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

Weighted upper-tail integrand in the strong-type maximal-function estimate.

Equations

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

theorem CKN.Foundation.Euclidean.ae_lt_top_maximalFunction {f : Parabolic.Vec3 → ENNReal} (hf : Measurable f) {p : ℝ} (hp : 1 < p) (hfp : ∫⁻ (z : Parabolic.Vec3), f z ^ p < ⊤) : ∀ᵐ (z : Parabolic.Vec3), maximalFunction f z < ⊤

theorem CKN.Foundation.Euclidean.lintegral_rpow_maximalFunction_le {f : Parabolic.Vec3 → ENNReal} (hf : Measurable f) {p : ℝ} (hp : 1 < p) (hfp : ∫⁻ (z : Parabolic.Vec3), f z ^ p < ⊤) : ∫⁻ (z : Parabolic.Vec3), maximalFunction f z ^ p ≤ maximalStrongConstant p * ∫⁻ (z : Parabolic.Vec3), f z ^ p

theorem CKN.Foundation.Euclidean.maximalFunction_le_essSup (f : Parabolic.Vec3 → ENNReal) (z : Parabolic.Vec3) : maximalFunction f z ≤ essSup f MeasureTheory.volume

theorem CKN.Foundation.Euclidean.lintegral_rpow_maximalFunction_ofReal_le (f : Parabolic.Vec3 → ℝ) (hf : Measurable f) {p : ℝ} (hp : 1 < p) (hfp : ∫⁻ (z : Parabolic.Vec3), ENNReal.ofReal ‖f z‖ ^ p < ⊤) : ∫⁻ (z : Parabolic.Vec3), maximalFunction (fun (z : Parabolic.Vec3) => ENNReal.ofReal ‖f z‖) z ^ p ≤ maximalStrongConstant p * ∫⁻ (z : Parabolic.Vec3), ENNReal.ofReal ‖f z‖ ^ p

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