The finite-p Sobolev space carries its canonical seminorm

Proved

HunterPDE.Compactness.exists_sobolev_seminorm

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

functional-analysissobolev-spacesweak-derivatives

For every open subset of Euclidean space and every finite exponent $1\le p<\infty$ , the raw representatives in $W^{k,p}$ form a real vector subspace, and their Sobolev norm is the extended-real image of a finite real seminorm on that subspace. No quotient by almost-everywhere equality is taken. The seminorm may therefore vanish on nonzero raw functions. This assertion includes the triangle inequality, absolute homogeneity, finiteness, and closure under real linear combinations for the chosen weak-derivative representatives.

Preamble

import Definitions.Def_HunterPDE_Compactness_Sobolev
import Definitions.Def_HunterPDE_Compactness_HalfSpace
import Mathlib.Analysis.Seminorm
open MeasureTheory HunterPDE.Compactness
open scoped ENNReal NNReal
set_option autoImplicit false

Formal statement

theorem HunterPDE.Compactness.exists_sobolev_seminorm {n k : ℕ} {p : ℝ≥0∞} (hp : 1 ≤ p) (hp' : p ≠ ∞)
    (Ω : Set (EuclideanSpace ℝ (Fin n))) (hΩ : IsOpen Ω) :
    ∃ W : Submodule ℝ (EuclideanSpace ℝ (Fin n) → ℝ),
      (∀ f, f ∈ W ↔ MemW k p Ω f) ∧
      ∃ q : Seminorm ℝ W, ∀ f : W,
        ENNReal.ofReal (q f) = sobolevNorm k p Ω f := by sorry

Source

J. K. Hunter, Notes on Partial Differential Equations, revised 6/18/2014, https://www.math.ucdavis.edu/~hunter/pdes/ch3.pdf, Definition 3.23, printed pp.58–59. Seminorm formulation on raw representatives of the Sobolev norm; standard consequence of weak-derivative linearity, uniqueness and finite-sum Minkowski.

View graph