The maximal function of f is at most that of its large part plus the truncation level

Proved

DbarRegularity.maximalFunction_le_indicator_add

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

harmonic-analysismaximal-functionmeasure-theory

Let $Mf$ be the Hardy–Littlewood maximal function of $f:\mathbb{R}^d\to\mathbb{C}$ ,

Mf(x)=\sup_{r>0}\frac{1}{|B(x,r)|}\int_{B(x,r)}|f(y)|\,dy\in[0,\infty],

where $B(x,r)$ is the open ball and $|\cdot|$ is Lebesgue measure. For $\beta\in[0,\infty]$ let $f^\beta=f\,\mathbf 1_{\{|f|>\beta\}}$ be the part of $f$ where $|f|$ exceeds $\beta$ . Then for every $x\in\mathbb{R}^d$ ,

Mf(x)\le Mf^\beta(x)+\beta.

The inequality controls the maximal function of $f$ by that of its large part, up to the truncation level $\beta$ .

Formalization Note. maximalFunction (from Definitions.Def_DbarRegularity_Setting) takes values in ℝ≥0∞; $\beta$ is in ℝ≥0∞ and $f^\beta$ is {y | β < ‖f y‖ₑ}.indicator f. No measurability or integrability is assumed on $f$ .

Preamble

import Definitions.Def_DbarRegularity_Setting

Formal statement

namespace DbarRegularity

open MeasureTheory
open scoped ENNReal

/-- Splitting off the values of `f` of size at most `β`: for every `β ∈ [0, ∞]`,
`M f ≤ M (f · 1_{|f| > β}) + β` at every point. -/
theorem maximalFunction_le_indicator_add (d : ℕ) (f : EuclideanSpace ℝ (Fin d) → ℂ) (β : ℝ≥0∞)
    (x : EuclideanSpace ℝ (Fin d)) :
    maximalFunction f x ≤ maximalFunction ({y | β < ‖f y‖ₑ}.indicator f) x + β := by sorry

end DbarRegularity

Source

Auxiliary statement for E. M. Stein, Singular Integrals and Differentiability Properties of Functions, Princeton Mathematical Series 30, Princeton University Press (1970), Chapter I, § 1.3, Theorem 1 (c), p. 5

View graph