A constant controlled by an Lp norm and a uniform oscillation bound

Proved

MeasureTheory.enorm_const_le_of_ae_sub_le

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

lp-spacesmeasure-theorymorrey-inequality

Let $(X,\mu)$ be a measure space with $0<\mu(X)<\infty$ , let $1\le p<\infty$ , and let $f:X\to\mathbb R$ be almost everywhere strongly measurable. If $c\in\mathbb R$ and $K\in[0,\infty]$ satisfy $|c-f(y)|\le K$ almost everywhere, then

|c|\le K+\mu(X)^{-1/p}\|f\|_{L^p(\mu)}.

This finite-measure estimate turns a local oscillation bound into a pointwise size bound. It applies to arbitrary finite measures, including restrictions to balls.

Preamble

import Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality

open MeasureTheory

Formal statement

theorem MeasureTheory.enorm_const_le_of_ae_sub_le {X : Type*} [MeasurableSpace X] (μ : Measure X) {p : ENNReal}
    (hp : 1 ≤ p) (hpt : p ≠ ⊤) (hμ0 : μ Set.univ ≠ 0) (hμt : μ Set.univ ≠ ⊤)
    (f : X → ℝ) (hf : AEStronglyMeasurable f μ) (c : ℝ) (K : ENNReal)
    (hK : ∀ᵐ y ∂μ, ‖c - f y‖ₑ ≤ K) :
    ‖c‖ₑ ≤ K + (μ Set.univ ^ (1 / p.toReal))⁻¹ * eLpNorm f p μ := by sorry

Source

Hunter, Notes on Partial Differential Equations (revised 6/18/2014), https://www.math.ucdavis.edu/~hunter/pdes/pde_notes.pdf, p. 70, proof of Theorem 3.36, final unit-ball averaging argument; generalized to finite measure spaces

View graph