Sobolev endpoint embedding for weakly differentiable functions

Proved

HunterPDE.Sobolev.sobolev_endpoint_embedding

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

sobolev-embeddingsobolev-spaces

Let $1\le p<n$ and $p^*=np/(n-p)$ . There is a nonnegative constant $C$ , chosen before the function, such that every $f\in W^{1,p}(\mathbb R^n)$ lies in $L^{p^*}(\mathbb R^n)$ and

\|f\|_{p^*}\le C\|f\|_{W^{1,p}}.

This is the endpoint step in the proof of Theorem 3.31: extend the compact smooth Gagliardo–Nirenberg–Sobolev inequality by the density theorem. The norm is the sum over multi-indices in Definition 3.23. No assertion about intermediate exponents is assumed.

Preamble

import Definitions.Def_HunterPDE_Sobolev_SobolevSpace
import Definitions.Def_HunterPDE_Sobolev_SobolevConjugate

open MeasureTheory HunterPDE.Sobolev

Formal statement

theorem HunterPDE.Sobolev.sobolev_endpoint_embedding {n : ℕ} {p : ℝ}
    (hp : 1 ≤ p) (hpn : p < n) :
    ∃ C : NNReal, ∀ f : EuclideanSpace ℝ (Fin n) → ℝ,
      MemW 1 (ENNReal.ofReal p) Set.univ f →
        MemLp f (ENNReal.ofReal (sobolevConjugate n p)) volume ∧
          eLpNorm f (ENNReal.ofReal (sobolevConjugate n p)) volume ≤
            (C : ENNReal) * sobolevNorm 1 (ENNReal.ofReal p) Set.univ f := by sorry

Source

Hunter, Notes on Partial Differential Equations (revised 6/18/2014), https://www.math.ucdavis.edu/~hunter/pdes/ch3.pdf, p. 66, Theorem 3.31, first two paragraphs of its proof; Theorems 3.24 and 3.28

View graph