The Hardy–Littlewood maximal function

The centred Hardy–Littlewood maximal function of f is

M f x = ⨆ r > 0, ⨍⁻ y in ball x r, ‖f y‖ₑ ∂μ,

the largest average of ‖f‖ over a ball centred at x. This file defines it, records the two endpoint bounds it satisfies, and proves the maximal inequality in both of its forms: the weak type (1,1) bound

t * μ {x | t < M f x} ≤ 4 ^ n * ∫⁻ x, ‖f x‖ₑ ∂μ

and, for 1 < p < ∞, the strong type (p, p) bound ‖M f‖_p ≤ C(n, p) * ‖f‖_p, for μ an additive Haar measure on a real normed space of finite dimension n.

The maximal inequality is the first item of Lane B of the PDE roadmap, the estimate that drives the Calderón–Zygmund theory and, through it, the Lᵖ regularity theory for elliptic equations. It is also where the classical asymmetric pair of endpoints originates: M is bounded on L^∞ (TauCeti.maximalFunction_le_eLpNormEssSup) but, in positive dimension, not on L¹ — a failure not formalised here — so the correct L¹ statement is the weak-type bound, and the strong (p, p) bounds are obtained from those two ends by Marcinkiewicz interpolation. The qualification matters: the L¹ failure is a positive-dimensional phenomenon, since in dimension 0 every ball is the whole space and the averages defining M f collapse to ‖f‖ₑ.

The proof

The weak-type bound is the Vitali covering argument, isolated here as TauCeti.mul_measure_le_of_forall_exists_ball: if every point of a set S is the centre of a ball of radius at most R on which ∫⁻ g is at least t times the measure of the ball, then t * μ S ≤ 4 ^ n * ∫⁻ g. Mathlib's Vitali.exists_disjoint_subfamily_covering_enlargement_closedBall extracts a pairwise disjoint subfamily of those balls whose fourfold enlargements still cover S; the enlargement costs the factor 4 ^ n because a Haar measure scales a ball of radius r by r ^ n, and disjointness turns the sum of the integrals over the selected balls into a single integral over their union.

Applying this to S = {x | t < M f x} needs a uniform bound on the radii it selects, and that is where finiteness of ∫⁻ ‖f‖ₑ enters: a ball whose average exceeds t has measure less than ∫⁻ ‖f‖ₑ / t, which in positive dimension bounds its radius. In dimension 0 it does not — every ball is the whole space — and that degenerate case is proved separately.

The strong type (p, p) bound then comes from TauCeti.lintegral_rpow_le_of_mul_meas_lt_le_of_le_eLpNormEssSup, the operator-level diagonal case of Marcinkiewicz interpolation. That theorem performs the reusable split at height c * t. Here c = d = 2⁻¹, so the low part is bounded by t / 2, its maximal function never reaches t, and the weak-type bound applied to the high part gives t * μ {M f > t} ≤ 2 * 4 ^ n * ∫⁻ x in {‖f‖ₑ > t / 2}, ‖f x‖ₑ ∂μ.

Main declarations

• TauCeti.maximalFunction: the centred Hardy–Littlewood maximal function, with TauCeti.setLAverage_le_maximalFunction, TauCeti.maximalFunction_le and TauCeti.lt_maximalFunction_iff as its interface.
• TauCeti.maximalFunction_const: the maximal function of a constant is that constant, so the normalisation is the intended one.
• TauCeti.maximalFunction_mono_ae, TauCeti.maximalFunction_congr_ae: M is monotone in ‖f‖ₑ almost everywhere, so M f depends on f only through ‖f‖ₑ and only up to a null set.
• TauCeti.maximalFunction_enorm: replacing a function by its extended norm leaves its maximal function unchanged.
• TauCeti.maximalFunction_zero, TauCeti.maximalFunction_add_le, TauCeti.maximalFunction_const_smul: M is sublinear. Subadditivity and the endpoint bounds feed directly into TauCeti.lintegral_rpow_le_of_mul_meas_lt_le_of_le_eLpNormEssSup.
• TauCeti.maximalFunction_le_eLpNormEssSup: the L^∞ endpoint.
• TauCeti.lowerSemicontinuous_maximalFunction, TauCeti.measurable_maximalFunction: the superlevel sets {x | t < M f x} are open, so M f is Borel measurable.
• TauCeti.mul_measure_le_of_forall_exists_ball: the Vitali covering estimate.
• TauCeti.mul_measure_lt_maximalFunction_le, TauCeti.measure_lt_maximalFunction_le: the maximal inequality, in product and in quotient form.
• TauCeti.ae_maximalFunction_lt_top: the maximal function of an L¹ function is finite almost everywhere.
• TauCeti.lintegral_rpow_maximalFunction_le, TauCeti.eLpNorm_maximalFunction_le: the strong type (p, p) maximal inequality for 1 < p < ∞, with an explicit constant.
• TauCeti.eLpNorm_maximalFunction_lt_top, TauCeti.ae_maximalFunction_lt_top_of_eLpNorm_ne_top: a function with finite Lᵖ seminorm has a maximal function with finite Lᵖ seminorm for 1 < p ≤ ∞, and the maximal function is finite almost everywhere for every 1 ≤ p ≤ ∞.

The maximal function defined here is the centred one, whose averages are over the balls centred at the point. The uncentred variant, over all balls containing the point, is comparable to it with a dimensional constant and is not needed downstream.

References

• E. Stein, Singular Integrals and Differentiability Properties of Functions, Chapter I.
• L. Grafakos, Classical Fourier Analysis, Section 2.1.

noncomputable def TauCeti.maximalFunction {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [ENorm F] (μ : MeasureTheory.Measure X) (f : X → F) (x : X) : ENNReal

The centred Hardy–Littlewood maximal function of f with respect to μ: the supremum over the radii r > 0 of the average of ‖f‖ₑ over the ball of radius r centred at x.

The averages are taken in ℝ≥0∞, so this is defined for every f, taking the value ∞ at the points where the averages are unbounded.

Equations

• TauCeti.maximalFunction μ f x = ⨆ (r : ℝ), ⨆ (_ : r > 0), ⨍⁻ (y : X) in Metric.ball x r, ‖f y‖ₑ ∂μ

theorem TauCeti.maximalFunction_def {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [ENorm F] (μ : MeasureTheory.Measure X) (f : X → F) (x : X) : maximalFunction μ f x = ⨆ (r : ℝ), ⨆ (_ : r > 0), ⨍⁻ (y : X) in Metric.ball x r, ‖f y‖ₑ ∂μ

theorem TauCeti.setLAverage_le_maximalFunction {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [ENorm F] {r : ℝ} (μ : MeasureTheory.Measure X) (f : X → F) (x : X) (hr : 0 < r) : ⨍⁻ (y : X) in Metric.ball x r, ‖f y‖ₑ ∂μ ≤ maximalFunction μ f x

Every ball average is at most the maximal function: the introduction rule.

theorem TauCeti.maximalFunction_le {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [ENorm F] {μ : MeasureTheory.Measure X} {f : X → F} {x : X} {a : ENNReal} (h : ∀ r > 0, ⨍⁻ (y : X) in Metric.ball x r, ‖f y‖ₑ ∂μ ≤ a) : maximalFunction μ f x ≤ a

A bound holding for every ball average bounds the maximal function: the elimination rule.

theorem TauCeti.lt_maximalFunction_iff {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [ENorm F] {μ : MeasureTheory.Measure X} {f : X → F} {x : X} {t : ENNReal} : t < maximalFunction μ f x ↔ ∃ r > 0, t < ⨍⁻ (y : X) in Metric.ball x r, ‖f y‖ₑ ∂μ

The maximal function exceeds t exactly when some ball average does.

theorem TauCeti.maximalFunction_mono_ae {X : Type u_1} {F : Type u_2} {F' : Type u_3} [PseudoMetricSpace X] [MeasurableSpace X] [ENorm F] [ENorm F'] {μ : MeasureTheory.Measure X} {f : X → F} {g : X → F'} {x : X} (h : ∀ᵐ (y : X) ∂μ, ‖f y‖ₑ ≤ ‖g y‖ₑ) : maximalFunction μ f x ≤ maximalFunction μ g x

If ‖f‖ₑ ≤ ‖g‖ₑ almost everywhere, then M f ≤ M g.

theorem TauCeti.maximalFunction_congr_ae {X : Type u_1} {F : Type u_2} {F' : Type u_3} [PseudoMetricSpace X] [MeasurableSpace X] [ENorm F] [ENorm F'] {μ : MeasureTheory.Measure X} {f : X → F} {g : X → F'} {x : X} (h : ∀ᵐ (y : X) ∂μ, ‖f y‖ₑ = ‖g y‖ₑ) : maximalFunction μ f x = maximalFunction μ g x

Functions whose norms agree almost everywhere have the same maximal function.

@[simp]

theorem TauCeti.maximalFunction_enorm {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [ENorm F] (μ : MeasureTheory.Measure X) (f : X → F) : (maximalFunction μ fun (x : X) => ‖f x‖ₑ) = maximalFunction μ f

Replacing a function by its extended norm leaves its maximal function unchanged.

theorem TauCeti.maximalFunction_le_eLpNormEssSup {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [ENorm F] (μ : MeasureTheory.Measure X) (f : X → F) (x : X) : maximalFunction μ f x ≤ MeasureTheory.eLpNormEssSup f μ

The L^∞ endpoint of the maximal inequality: the maximal function of f is bounded by the essential supremum of ‖f‖, with constant 1.

@[simp]

theorem TauCeti.maximalFunction_const {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [ENorm F] [ProperSpace X] (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts μ] (c : F) (x : X) : maximalFunction μ (fun (x : X) => c) x = ‖c‖ₑ

The maximal function of a constant is that constant: the averages defining it are normalised, so no factor of the measure of a ball is left behind.

@[simp]

theorem TauCeti.maximalFunction_const_smul {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [ENorm F] {𝕜 : Type u_4} [NNNorm 𝕜] [SMul 𝕜 F] [ENormSMulClass 𝕜 F] (μ : MeasureTheory.Measure X) (c : 𝕜) (f : X → F) (x : X) : maximalFunction μ (c • f) x = ‖c‖ₑ * maximalFunction μ f x

The maximal function is positively homogeneous: scaling f by c scales M f by ‖c‖ₑ. This is the first half of the sublinearity of M, the second being TauCeti.maximalFunction_add_le.

@[simp]

theorem TauCeti.maximalFunction_zero {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] {G : Type u_4} [TopologicalSpace G] [ESeminormedAddMonoid G] (μ : MeasureTheory.Measure X) (x : X) : maximalFunction μ 0 x = 0

The maximal function of the zero function is zero.

theorem TauCeti.maximalFunction_add_le {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} {G : Type u_4} [TopologicalSpace G] [ESeminormedAddMonoid G] {f g : X → G} (hf : AEMeasurable (fun (y : X) => ‖f y‖ₑ) μ) (x : X) : maximalFunction μ (f + g) x ≤ maximalFunction μ f x + maximalFunction μ g x

The maximal function is subadditive, the second half of that sublinearity. Only the norm of the first summand need be measurable.

theorem TauCeti.mul_measure_le_of_forall_exists_ball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {t : ENNReal} {S : Set E} {R : ℝ} {g : E → ENNReal} (hS : ∀ x ∈ S, ∃ r ∈ Set.Ioc 0 R, t * μ (Metric.ball x r) ≤ ∫⁻ (y : E) in Metric.ball x r, g y ∂μ) : t * μ S ≤ 4 ^ Module.finrank ℝ E * ∫⁻ (y : E), g y ∂μ

The Vitali covering estimate. If every point of S is the centre of a ball of radius at most R on which ∫⁻ g is at least t times the measure of the ball, then t * μ S ≤ 4 ^ n * ∫⁻ g, with n the dimension of the space.

The factor 4 ^ n is the cost of passing from a pairwise disjoint subfamily of those balls to its fourfold enlargement, which still covers S.

theorem TauCeti.lowerSemicontinuous_maximalFunction {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] [ENorm F] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (f : E → F) : LowerSemicontinuous (maximalFunction μ f)

The superlevel sets of the maximal function are open: enlarging the radius slightly keeps the average of ‖f‖ₑ above t, at every nearby centre.

theorem TauCeti.measurable_maximalFunction {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] [ENorm F] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (f : E → F) : Measurable (maximalFunction μ f)

The maximal function is Borel measurable, being lower semicontinuous. No hypothesis on f is needed: the supremum defining M f is over balls, not over values of f.

theorem TauCeti.mul_measure_lt_maximalFunction_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] [ENorm F] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (f : E → F) (t : ENNReal) : t * μ {x : E | t < maximalFunction μ f x} ≤ 4 ^ Module.finrank ℝ E * ∫⁻ (x : E), ‖f x‖ₑ ∂μ

The Hardy–Littlewood maximal inequality, the weak-type (1,1) bound: the measure of the set where the maximal function exceeds t, multiplied by t, is at most 4 ^ n times the L¹ norm of f, with n the dimension of the space.

No integrability hypothesis is needed: the bound is vacuous when ∫⁻ x, ‖f x‖ₑ ∂μ = ∞.

theorem TauCeti.measure_lt_maximalFunction_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] [ENorm F] {t : ENNReal} (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (f : E → F) (ht : t ≠ 0) : μ {x : E | t < maximalFunction μ f x} ≤ (4 ^ Module.finrank ℝ E * ∫⁻ (x : E), ‖f x‖ₑ ∂μ) / t

The Hardy–Littlewood maximal inequality, in quotient form.

theorem TauCeti.ae_maximalFunction_lt_top {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] [ENorm F] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (f : E → F) (hf : ∫⁻ (x : E), ‖f x‖ₑ ∂μ ≠ ⊤) : ∀ᵐ (x : E) ∂μ, maximalFunction μ f x < ⊤

The maximal function of an L¹ function is finite almost everywhere: the maximal inequality with t → ∞.

theorem TauCeti.lintegral_rpow_maximalFunction_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] [ENorm F] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {f : E → F} (hf : AEMeasurable (fun (x : E) => ‖f x‖ₑ) μ) {p : ℝ} (hp : 1 < p) : ∫⁻ (x : E), maximalFunction μ f x ^ p ∂μ ≤ ENNReal.ofReal (2 * p * 2 ^ (p - 1) / (p - 1)) * 4 ^ Module.finrank ℝ E * ∫⁻ (x : E), ‖f x‖ₑ ^ p ∂μ

The Hardy–Littlewood maximal inequality, the strong-type (p, p) bound for 1 < p < ∞, as an inequality between the integrals ∫⁻ ‖·‖ₑ ^ p:

∫⁻ (M f) ^ p ∂μ ≤ (2 * p * 2 ^ (p - 1) / (p - 1)) * 4 ^ n * ∫⁻ ‖f‖ₑ ^ p ∂μ.

The constant degenerates as p → 1, as it must in positive dimension, where M is not bounded on L¹.

theorem TauCeti.eLpNorm_maximalFunction_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] [ENorm F] [TopologicalSpace F] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {f : E → F} (hf : AEMeasurable (fun (x : E) => ‖f x‖ₑ) μ) {p : ENNReal} (hp : 1 < p) (hp_top : p ≠ ⊤) : MeasureTheory.eLpNorm (maximalFunction μ f) p μ ≤ (ENNReal.ofReal (2 * p.toReal * 2 ^ (p.toReal - 1) / (p.toReal - 1)) * 4 ^ Module.finrank ℝ E) ^ (1 / p.toReal) * MeasureTheory.eLpNorm f p μ

The Hardy–Littlewood maximal inequality, the strong-type (p, p) bound for 1 < p < ∞, in terms of representative-level Lᵖ seminorms.

Together with TauCeti.maximalFunction_le_eLpNormEssSup (the case p = ∞) and TauCeti.mul_measure_lt_maximalFunction_le (the weak-type substitute at p = 1), this gives the representative-level strong estimate for the maximal function. The resulting finiteness statement is recorded by TauCeti.eLpNorm_maximalFunction_lt_top below.

theorem TauCeti.eLpNorm_maximalFunction_lt_top {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] [ENorm F] [TopologicalSpace F] {p : ENNReal} {f : E → F} (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (hf : AEMeasurable (fun (x : E) => ‖f x‖ₑ) μ) (hf_top : MeasureTheory.eLpNorm f p μ ≠ ⊤) (hp : 1 < p) : MeasureTheory.eLpNorm (maximalFunction μ f) p μ < ⊤

The maximal function of an Lᵖ function has finite Lᵖ seminorm when 1 < p ≤ ∞.

theorem TauCeti.ae_maximalFunction_lt_top_of_eLpNorm_ne_top {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] [ENorm F] [TopologicalSpace F] {p : ENNReal} (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (f : E → F) (hf_top : MeasureTheory.eLpNorm f p μ ≠ ⊤) (hp : 1 ≤ p) : ∀ᵐ (x : E) ∂μ, maximalFunction μ f x < ⊤

The maximal function of a function with finite Lᵖ seminorm is finite almost everywhere when 1 ≤ p, including both endpoints.