The Hardy–Littlewood maximal theorem

Proved

DbarRegularity.maximalFunction_bounds

by Mazecto · Oct 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

calderon-zygmundcauchy-riemannelliptic-regularityharmonic-analysissingular-integrals

Let $Mf$ be the Hardy–Littlewood maximal function of $f:\mathbb{R}^d\to\mathbb{C}$ . $\mathbb{R}^d$ carries Lebesgue measure $m$ , and $\|\cdot\|_p$ is the $L^p(\mathbb{R}^d)$ norm. Then:

if $f\in L^p(\mathbb{R}^d)$ for some $1\le p\le\infty$ , then $Mf(x)<\infty$ for almost every $x$ ;
there is a constant $A$ depending only on $d$ such that for every $f\in L^1(\mathbb{R}^d)$ and every $\alpha>0$ ,

m\{x: Mf(x)>\alpha\}\le\frac{A}{\alpha}\int_{\mathbb{R}^d}|f|\,dx;

for every $1<p\le\infty$ there is a constant $A_p$ depending only on $p$ and $d$ such that every $f\in L^p(\mathbb{R}^d)$ has $Mf\in L^p(\mathbb{R}^d)$ and $\|Mf\|_p\le A_p\|f\|_p$ .

Formalization Note maximalFunction f is valued in ℝ≥0∞; part 3 asserts MemLp (maximalFunction f) p and bounds its eLpNorm. $p$ is in ℝ≥0∞, so $p=\infty$ is included in parts 1 and 3. The constants are in ℝ≥0 and are chosen before $f$ (and $\alpha$ ). Stein remarks that $A=5^d$ will do in part 2; the statement asks only for some constant depending on $d$ .

Preamble

import Definitions.Def_DbarRegularity_Setting
import Mathlib.Analysis.Calculus.ContDiff.Basic

Formal statement

namespace DbarRegularity

open MeasureTheory Metric Filter Topology
open scoped ENNReal NNReal ContDiff

/-- Stein, *Singular Integrals*, Chapter I, § 1.3, Theorem 1 (p. 5): the Hardy–Littlewood maximal
function `M f` of `f` on `ℝ^d`
(a) is finite almost everywhere when `f ∈ L^p`, `1 ≤ p ≤ ∞`;
(b) is of weak type `(1, 1)`: `|{M f > α}| ≤ (A / α) ‖f‖₁` with `A` depending only on `d`;
(c) is in `L^p` with `‖M f‖_p ≤ A_p ‖f‖_p` when `f ∈ L^p`, `1 < p ≤ ∞`, with `A_p` depending only
on `p` and `d`. -/
theorem maximalFunction_bounds (d : ℕ) :
    (∀ p : ℝ≥0∞, 1 ≤ p → ∀ f : EuclideanSpace ℝ (Fin d) → ℂ, MemLp f p →
      ∀ᵐ x, maximalFunction f x < ⊤) ∧
    (∃ A : ℝ≥0, ∀ f : EuclideanSpace ℝ (Fin d) → ℂ, Integrable f → ∀ α : ℝ≥0, 0 < α →
      volume {x | (α : ℝ≥0∞) < maximalFunction f x} ≤ (A : ℝ≥0∞) / α * ∫⁻ x, ‖f x‖ₑ) ∧
    (∀ p : ℝ≥0∞, 1 < p → ∃ A : ℝ≥0, ∀ f : EuclideanSpace ℝ (Fin d) → ℂ, MemLp f p →
      MemLp (maximalFunction f) p ∧
        eLpNorm (maximalFunction f) p volume ≤ A * eLpNorm f p volume) := by sorry

end DbarRegularity

Source

E. M. Stein, Singular Integrals and Differentiability Properties of Functions, Princeton Mathematical Series 30, Princeton University Press (1970), ISBN 0-691-08079-8, Chapter I, § 1.3, Theorem 1, p. 5

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Read-back: `DbarRegularity.maximalFunction_bounds`

Setting. Fixed $d\in\mathbb N$ ; functions $f:\mathbb R^d\to\mathbb C$ , Lebesgue measure.

Hypotheses. Only $d$ (any natural number, $d=0$ allowed).

Definitions used. maximalFunction ( $Mf$ , $[0,\infty]$ -valued Hardy–Littlewood maximal function over open balls); MemLp, eLpNorm, Integrable, lower integral $\int^-\|f\|_e$ .

Conclusion. A conjunction of three statements:

(a) $\forall p\in[1,\infty]\ \forall f\in L^p(\mathbb R^d):\ Mf(x)<\infty$ for a.e. $x$ .

(b) $\exists A\in[0,\infty)\ \forall f\in L^1(\mathbb R^d)\ \forall \alpha\in(0,\infty):\ \big|\{x:\alpha<Mf(x)\}\big|\le \dfrac{A}{\alpha}\displaystyle\int|f|$ .

(c) $\forall p\in(1,\infty]\ \exists A_p\in[0,\infty)\ \forall f\in L^p(\mathbb R^d):\ Mf\in L^p$ (as an $[0,\infty]$ -valued function: a.e.-strongly measurable with finite eLpNorm) and $\|Mf\|_p\le A_p\|f\|_p$ .

Quantifier order: $d$ first; in (b) $A=A(d)$ before $f,\alpha$ ; in (c) $A_p=A_p(d,p)$ before $f$ .

Degenerate cases. $p=\infty$ is included in (a) and (c) (true: $Mf\le\|f\|_\infty$ , $A_\infty=1$ ). $d=0$ : $Mf=|f|$ pointwise; all three hold trivially ( $A=1$ ). $\alpha>0$ avoids ENNReal division by $0$ ; $A/\alpha<\infty$ .

Remarks. MemLp for an ℝ≥0∞-valued function is valid here (ENorm ℝ≥0∞ with $\|x\|_e=x$ ). $Mf$ is lower semicontinuous, hence measurable. The weak bound uses the strict superlevel set $\{\alpha<Mf\}$ , as in the standard statement.

Soundness checks.

No Bochner integrals or toReal appear; $\int^-\|f\|_e$ is the true $L^1$ norm. Constants $A$ are ℝ≥0, so they cannot be $\top$ . MemLp hypotheses include measurability, so no junk. Nothing is vacuous: $L^p$ functions exist, and the conclusions are non-trivial for $d\ge1$ .
Constants depend only on $d$ (and $p$ in (c)), chosen before $f$ and $\alpha$ : this is the standard Hardy–Littlewood maximal theorem (Stein Ch. I, Thm 1). Plausibly TRUE as written.

Verdict: no mis-formalization observed

Human review

Endorsed by Shuze Chen · Oct 13, 2026
Confirmed by the moderator at approval.
Endorsed by Mazecto · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

The Hardy–Littlewood maximal theorem

Read-back: DbarRegularity.maximalFunction_bounds

Read-back: `DbarRegularity.maximalFunction_bounds`