The Fefferman–Stein maximal inequality #
This file was automatically generated by Codex.
The classical vector maximal theorem supplies the general mixed norm estimate in
blueprint lem:vector-maximal. The intended reusable statement covers all outer
and inner exponents greater than one and finite inner measure spaces.
The interpolation and scalar maximal foundations below are adapted from
../lean-variationalsw/VariationalSW/Auto/MarcinkiewiczInterpolation.lean and
../lean-variationalsw/VariationalSW/Auto/HardyLittlewoodMaximal.lean, originally
generated by Claude (2026, Joris Roos, Apache 2.0). The weighted estimate and duality
argument are adapted from its Fefferman–Stein proof. Its existing final theorem
only covers finite Hilbert families; here weighted duality is used for general
inner exponents and measures. feffermanStein_mixed covers all exponents greater
than one and arbitrary finite inner measure spaces, with fsMixedConst_ne_top
certifying a constant independent of the inner space.
Reference: C. Fefferman and E. M. Stein, Some maximal inequalities, American Journal of Mathematics 93 (1971), 107–115, https://doi.org/10.2307/2373450.
Elementary power integrals on the half-line #
∫_0^u t^(r-1) dt = u^r / r for r > 0, written with an indicator on (0, ∞).
∫_u^∞ t^(-r-1) dt = u^(-r) / r for u > 0, r > 0, written with an indicator on
(0, ∞).
Tonelli for the truncation integrals #
Exchange of the t-integral over (0, ∞) and the space integral for integrands supported
on a measurable subset S of ℝ × α (Tonelli).
Measurability in t of the truncated space integrals.
The low-truncation Tonelli identity:
∫_0^∞ t^(r-1) ∫_{c t < φ} φ^q dμ dt = (c^(-r)/r) ∫ φ^(q+r) dμ.
The high-truncation Tonelli identity:
∫_0^∞ t^(-r-1) ∫_{φ ≤ c t} φ^q dμ dt = (c^r/r) ∫ φ^(q-r) dμ for 0 < r < q.
From a split distributional bound to an Lᵖ bound #
The core of the real interpolation argument. If the distribution function of g at every
height t > 0 is controlled by K₁ t^(-a) ∫_{‖f‖ > c t} ‖f‖^a + K₂ t^(-b) ∫_{‖f‖ ≤ c t} ‖f‖^b,
then ∫ ‖g‖^p ≤ p (K₁ c^(a-p)/(p-a) + K₂ c^(b-p)/(b-p)) ∫ ‖f‖^p for 0 < a < p < b
(layer-cake formula followed by Tonelli).
Distribution functions, weak type, sublinearity #
The distribution function t ↦ ν {x | t < ‖g x‖} of g : β → F, with t : ℝ≥0∞.
Instances For
T is of weak type (a, a) with constant A on the class of inputs D:
ν {‖T f‖ > t} ≤ (A ‖f‖_{L^a(μ)} / t)^a for all f ∈ D and all t > 0.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The L^∞ endpoint hypothesis with constant B: if ‖f x‖ ≤ s for every x, then
‖T f y‖ ≤ B s for ν-almost every y (for f ∈ D).
Equations
Instances For
T is subadditive in pointwise norm on D: ‖T (f + g)‖ ≤ ‖T f‖ + ‖T g‖ ν-a.e.
Equations
Instances For
D is closed under the two truncations f 𝟙_{‖f‖ > s} and f 𝟙_{‖f‖ ≤ s}, s > 0, used
in the proof of the Marcinkiewicz interpolation theorem.
Equations
Instances For
The distribution function at a real height.
‖f‖_{L^p}^p = ∫ ‖f‖^p for 0 < p < ∞ and a.e. strongly measurable f.
‖f‖_{L^p} = (∫ ‖f‖^p)^(1/p) for 0 < p < ∞ and a.e. strongly measurable f.
Truncation and the split of the distribution function #
The upper truncation f 𝟙_{‖f‖ > s} of an a.e. strongly measurable function is a.e.
strongly measurable.
The lower truncation f 𝟙_{‖f‖ ≤ s} of an a.e. strongly measurable function is a.e.
strongly measurable.
Subadditivity splits the distribution function of T f at height t into those of the
truncations of f at height s, each at height t / 2.
A weak-type (a, a) bound at height t / 2, written in the normalized form used in the
interpolation argument.
The L^∞ endpoint hypothesis makes the distribution function of T g vanish at heights
above B s, for ‖g‖ ≤ s everywhere.
Constants #
The free-parameter constant p 2^a A^a c^(a-p)/(p-a) of the endpoint case b = ∞.
Equations
Instances For
marcinkiewiczBoundTop is finite.
The Marcinkiewicz interpolation theorem #
Marcinkiewicz interpolation with an L^∞ endpoint, free truncation parameter (the
endpoint estimate in the proof of Blueprint Lemma 2.3 (lem:interpolation)): if T is
subadditive on a truncation closed class D, of weak type (a, a) with constant A, and
‖f‖ ≤ s implies ‖T f‖ ≤ B s a.e. (for f ∈ D), then for 0 < a < p, every c > 0 with
B c ≤ 1/2 and every f ∈ D, ∫ ‖T f‖^p ≤ p 2^a A^a c^(a-p)/(p-a) ∫ ‖f‖^p.
The average μ(B(x,r))⁻¹ ∫_{B(x,r)} ‖f‖ of ‖f‖ over the closed ball B(x,r), valued in
ℝ≥0∞. With the conventions of ℝ≥0∞ it vanishes when μ(B(x,r)) = 0 or μ(B(x,r)) = ∞
(in particular for r < 0).
Equations
- TrilinearHT.Auto.ClassicalMaximal.hlBallAverage μ f x r = (μ (Metric.closedBall x r))⁻¹ * ∫⁻ (y : X) in Metric.closedBall x r, ‖f y‖ₑ ∂μ
Instances For
The centered Hardy–Littlewood maximal function over closed balls,
M f(x) = sup_r μ(B(x,r))⁻¹ ∫_{B(x,r)} ‖f‖, valued in ℝ≥0∞. Radii r < 0 and balls of measure
0 or ∞ contribute 0; the radius r = 0 (the ball B(x,0)) is included.
Equations
- TrilinearHT.Auto.ClassicalMaximal.hlMaximal μ f x = ⨆ (r : ℝ), TrilinearHT.Auto.ClassicalMaximal.hlBallAverage μ f x r
Instances For
A closed ball is contained in its threefold dilate.
Finite Vitali covering lemma, largest-first selection (proof of Blueprint Lemma 2.4
(lem:maximal)): every finite family of closed balls B(c i, r i), i ∈ s, has a pairwise
disjoint subfamily S ⊆ s such that every ball of the family is contained in the threefold
dilate B(c j, 3 r j) of a selected ball with r i ≤ r j.
Finite covering estimate (proof of Blueprint Lemma 2.4 (lem:maximal)): if μ satisfies
the doubling condition μ(B(x,3r)) ≤ C μ(B(x,r)) and every ball of a finite family satisfies
μ(B_i) ≤ t⁻¹ ∫_{B_i} ‖f‖, then μ(⋃ B_i) ≤ C t⁻¹ ∫ ‖f‖.
If the average over B(x,r) exceeds t, then r ≥ 0 and μ(B(x,r)) ≤ t⁻¹ ∫_{B(x,r)} ‖f‖.
Averages are monotone in the pointwise norm (almost everywhere).
The maximal function is monotone in the pointwise norm (almost everywhere).
The maximal function only depends on the almost everywhere class of the input.
Subadditivity of averages for a.e. strongly measurable inputs.
Subadditivity of the maximal function: M (f + g) ≤ M f + M g for a.e. strongly measurable
f.
If ‖f‖ ≤ c almost everywhere, then M f ≤ c everywhere.
Continuity of the ball measure from above, in the form used for the maximal function: the
average over B(x,r) is at most the supremum of the averages over B(x,q), q > r rational
(if balls have finite measure).
Rational radii suffice: M f(x) = sup_{q ∈ ℚ} μ(B(x,q))⁻¹ ∫_{B(x,q)} ‖f‖ (if balls have
finite measure).
For a fixed radius, the average is a measurable function of the center (a measurable parameter integral).
Measurability of the maximal function (proof of Blueprint Lemma 2.4 (lem:maximal)):
if balls have finite measure (and X is second countable, μ s-finite), then M f is
measurable for every a.e. strongly measurable f; rational radii suffice.
The finite covering estimate applied to balls on which the average exceeds t.
Weak type (1,1) on inner regular spaces (Blueprint Lemma 2.4 (lem:maximal), weak bound,
the Euclidean case): let X be second countable, μ s-finite and inner regular (with respect to
compact sets), with balls of finite measure and μ(B(x,3r)) ≤ C μ(B(x,r)) for all x, r ≥ 0.
Then for every a.e. strongly measurable f and every t, μ {M f > t} ≤ C t⁻¹ ∫ ‖f‖
(proved on finite subcovers of compact subsets of the level set).
Strong type (p, p) via Marcinkiewicz interpolation #
The truncated real-valued maximal function min (M f) N: a real-valued, everywhere
subadditive operator to which the Marcinkiewicz interpolation theorem applies.
Equations
Instances For
The strong type constant C_p = (2^p p C / (p - 1))^(1/p) of the Hardy–Littlewood maximal
theorem, for doubling constant C and 1 < p < ∞.
Equations
- TrilinearHT.Auto.ClassicalMaximal.hlMaximalConst C p = ENNReal.ofReal (2 ^ p * p * ↑C / (p - 1)) ^ (1 / p)
Instances For
The strong type constant is finite.
Strong type (p, p) in integral form, from the weak type (1, 1) bound (proof of
Blueprint Lemma 2.4 (lem:maximal)): Marcinkiewicz interpolation between weak (1,1) and
L^∞ gives ∫ (M f)^p ≤ 2^p p C/(p-1) ∫ ‖f‖^p for 1 < p < ∞.
Strong type (p, p), from the weak type (1, 1) bound: if M satisfies the weak
(1,1) bound with constant C for all a.e. strongly measurable inputs, then
‖M f‖_p ≤ C_p ‖f‖_p for 1 < p < ∞, C_p = hlMaximalConst C p.
Hardy–Littlewood maximal theorem, strong type (p, p) (Blueprint Lemma 2.4
(lem:maximal), strong bound, the Euclidean case): let X be second countable, μ s-finite
and inner regular, with balls of finite measure and μ(B(x,3r)) ≤ C μ(B(x,r)) (r ≥ 0). For
1 < p < ∞ and every a.e. strongly measurable f, ‖M f‖_p ≤ C_p ‖f‖_p with
C_p = (2^p p C/(p-1))^(1/p).
Cubes in ℝⁿ: the sup metric on Fin n → ℝ and E = EuclideanSpace ℝ (Fin n) #
Cubes in the lattice G = ℤⁿ #
Scaling of the volume of Euclidean balls.
The constant of the Hardy–Littlewood maximal theorem in integral form.
Equations
- TrilinearHT.Auto.ClassicalMaximal.fsK n q = ENNReal.ofReal (2 ^ q * q * ↑(3 ^ n) / (q - 1))
Instances For
The Hardy–Littlewood maximal theorem on ℝⁿ in integral form:
∫ (M f)^q ≤ K ∫ ‖f‖^q for 1 < q < ∞.
The ball estimate behind the weighted weak type bound: if the average of ‖f‖ over
B = B(c,r) exceeds τ, then w(3B) ≤ 4ⁿ τ⁻¹ ∫_B ‖f‖ M w.
Weighted weak type (1,1) (Fefferman–Stein): for every weight w and τ > 0,
w {M f > τ} ≤ 4ⁿ τ⁻¹ ∫ ‖f‖ M w.
The constant of the weighted maximal inequality at exponent q.
Equations
- TrilinearHT.Auto.ClassicalMaximal.fsKwPow n q = TrilinearHT.Auto.ClassicalMaximal.marcinkiewiczBoundTop 1 q (4 ^ n) (1 / 2)
Instances For
The Fefferman–Stein weighted inequality: for every weight w (a.e. strongly measurable
and real-valued; only |w| matters) and every f, ∫ (M f)^q |w| ≤ C ∫ ‖f‖^q M w, with C
for q > 1, with the constant depending only on n and q.
Constant supplied by scalar weighted duality.
Equations
Instances For
Finite extended-real cancellation in the duality argument; adapted from
../lean-variationalsw/VariationalSW/Auto/CalderonZygmund.lean, lines 422–436.
Weighted testing against the scalar maximal operator gives an L^r estimate.
Bounded compactly supported tests suffice in the proof, even when the integrals are infinite.
The scalar maximal operator acts in the Euclidean variable only.
Equations
- TrilinearHT.Auto.ClassicalMaximal.mixedMaximal f p = TrilinearHT.Auto.ClassicalMaximal.hlMaximal MeasureTheory.volume (fun (y : EuclideanSpace ℝ (Fin n)) => f (y, p.2)) p.1
Instances For
The vector maximal inequality when the outer exponent exceeds the inner exponent, valid on any sigma-finite inner measure space with a constant independent of that space.
Iterated extended L^p(L^s) norm of a nonnegative function.
Equations
Instances For
Hölder's inequality applied in the inner variable and then in the outer variable.
The optimizing weight for mixed-norm duality; zero inner fibers receive weight zero.
Equations
Instances For
Mixed dual testing for finite-valued functions with finite inner powers and total norm.
Mixed dual testing without finiteness restrictions on the tested function.
The inner measure is finite; truncation in value and the Euclidean variable removes
the hypotheses of mixedENorm_le_of_finite_test.
Taking a power of a function rescales both mixed-norm exponents.
Upper mixed-norm maximal-function constant obtained from the dual estimate.
Equations
Instances For
The weighted maximal inequality with a weight depending on both variables.
A second weighted duality argument handles the outer exponent below the inner one.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A finite constant depending only on Euclidean dimension and the two exponents.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Fefferman–Stein vector maximal inequality, for every 1 < p,s < ∞ and
every finite inner measure space. The maximal function acts only in ℝ^n, and
the constant is independent of the inner space and the function.
Reference: Fefferman–Stein, Some maximal inequalities (1971), pp. 107–115.
This integral formulation permits either mixed norm to be infinite.