Hardy–Littlewood maximal function

TheoremMaximal functions of bounded a.e.-null sequences tend to zero a.e#●ready to prove

Let \((f_n)_{n \in \mathbb{N}}\) be a sequence of functions \(f_n : \mathbb{R} \to \mathbb{R}\), each Lebesgue measurable on \([0,1]\), such that \(f_n(x) \in [0,1]\) for every \(n\) and every \(x \in [0,1]\), and \(f_n(x) \to 0\) as \(n \to \infty\) for almost every \(x \in [0,1]\). For \(x \in [0,1]\) let

\[Mf_n(x) = \sup_I \frac{1}{|I|} \int_I |f_n(y)|\,dy,\]

where the supremum is taken over all closed intervals \(I = [a,b]\) with \(a < b\) and \(x \in I \subseteq [0,1]\), and \(|I| = b - a\). Then \(Mf_n(x) \to 0\) as \(n \to \infty\) for almost every \(x \in [0,1]\).

public theorem_wanted ae_tendsto_maximal_zero_of_ae_tendsto_zero_of_bounded
    (f : ℕ → ℝ → ℝ)
    (hf_meas : ∀ n, AEMeasurable (f n) (MeasureTheory.volume.restrict (Set.Icc (0 : ℝ) 1)))
    (hf_range : ∀ n x, x ∈ Set.Icc (0 : ℝ) 1 → f n x ∈ Set.Icc (0 : ℝ) 1)
    (h_lim : ∀ᵐ x ∂(MeasureTheory.volume.restrict (Set.Icc (0 : ℝ) 1)),
        Filter.Tendsto (fun n => f n x) Filter.atTop (𝓝 (0 : ℝ)))
    (Mf : ℕ → ℝ → ℝ)
    (hMf : ∀ n x, Mf n x = sSup {r : ℝ | ∃ a b : ℝ, x ∈ Set.Icc a b ∧
      Set.Icc a b ⊆ Set.Icc (0 : ℝ) 1 ∧ 0 < b - a ∧
        r = (b - a)⁻¹ * ∫ y in Set.Icc a b, |f n y| ∂MeasureTheory.volume}) :
    ∀ᵐ x ∂(MeasureTheory.volume.restrict (Set.Icc (0 : ℝ) 1)),
      Filter.Tendsto (fun n => Mf n x) Filter.atTop (𝓝 (0 : ℝ))

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Measure and integration; Classical measure theory), problem ma_proofbench_l2_74.

TheoremThe maximal function of a singular measure is infinite almost everywhere for that measure#●ready to prove

The maximal function of a singular measure is infinite almost everywhere for that measure. Let \(n\) be a natural number and let \(\mu\) be a Borel measure on \(\mathbb{R}^n\) that is mutually singular with respect to Lebesgue measure \(m_n\). Write \(B(x, r)\) for the open ball of radius \(r\) about \(x\) and define \(M_\mu : \mathbb{R}^n \to [0, \infty]\) by

\[ M_\mu(x) = \sup_{r>0} \frac{\mu(B(x, r))}{m_n(B(x, r))}. \]

Then \(\mu(\{x \in \mathbb{R}^n : M_\mu(x) < \infty\}) = 0\).

public theorem_wanted measure_setOf_maximalFunction_lt_top_eq_zero_of_mutuallySingular
    {n : ℕ}
    (μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n)))
    (hsing : MeasureTheory.Measure.MutuallySingular μ MeasureTheory.volume)
    (Mmu : EuclideanSpace ℝ (Fin n) → ENNReal)
    (hMdef : ∀ x : EuclideanSpace ℝ (Fin n),
      Mmu x = ⨆ (r : ℝ) (_ : 0 < r),
        μ (Metric.ball x r) / MeasureTheory.volume (Metric.ball x r)) :
    μ {x : EuclideanSpace ℝ (Fin n) | Mmu x < ⊤} = 0

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Measure and integration; Classical measure theory), problem ma_proofbench_l2_44.

2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.