Centered C1 oscillation controlled by the gradient potential

Proved

HunterPDE.Sobolev.centered_ball_oscillation_le_potential

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

lebesgue-integrationmorrey-inequalitypotential-theory

Let $n\ge1$ . There is a finite constant $C_n\ge0$ such that every $C^1$ function $f:\mathbb R^n\to\mathbb R$ , center $x$ , and radius $r>0$ satisfy

\int_{B(x,r)}|f(x)-f(z)|\,dz\le |B(x,r)|C_n\int_{B(x,r)}|\nabla f(z)|\,|z-x|^{1-n}\,dz.

This centered estimate expresses mean oscillation in terms of a first-order potential and can be used independently of any choice of Lebesgue exponent. Compact support is not required.

Formalization Note Both integrals are nonnegative extended integrals. Real powers specify the value of the kernel at the center; that value does not affect a Lebesgue integral.

Preamble

import Mathlib.Analysis.Calculus.Gradient.Basic
import Mathlib.Analysis.Calculus.ContDiff.Basic
import Mathlib.Analysis.InnerProductSpace.PiL2
import Mathlib.MeasureTheory.Function.LpSeminorm.Basic
import Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
import Mathlib.Analysis.SpecialFunctions.Pow.Real

open MeasureTheory
set_option autoImplicit false

Formal statement

theorem HunterPDE.Sobolev.centered_ball_oscillation_le_potential {n : ℕ} (hn : 0 < n) :
    ∃ C : NNReal, ∀ f : EuclideanSpace ℝ (Fin n) → ℝ,
      ContDiff ℝ 1 f → ∀ (x : EuclideanSpace ℝ (Fin n)) (r : ℝ), 0 < r →
      (∫⁻ z in Metric.ball x r, ENNReal.ofReal |f x - f z|) ≤
        volume (Metric.ball x r) * (C : ENNReal) *
          (∫⁻ z in Metric.ball x r, ENNReal.ofReal ‖gradient f z‖ *
            ENNReal.ofReal (‖z - x‖ ^ (1 - (n : ℝ)))) := by sorry

Source

Hunter, Notes on Partial Differential Equations (revised 6/18/2014), https://www.math.ucdavis.edu/~hunter/pdes/pde_notes.pdf, pp. 68–69, proof of Theorem 3.36, equation (3.14). The argument uses only C1 regularity and is stated here without the unused compact-support hypothesis.

View graph