Sobolev embedding theorem (Morrey regime)

sobolev_embedding_morrey

Submitter: Kim Morrison.

Notes: If n < p, 0 < α ≤ 1, and r + α < k − n/p, then every W^(k,p)(ℝⁿ) function has a C^(r,α) representative. Weak-derivative Sobolev spaces W^(k,p) are defined via the distributional pairing ∫ f · D^m φ = (−1)^|m| ∫ g · φ on smooth compactly-supported φ, with the LocallyIntegrable f conjunct essential to faithfulness — without it, non-a.e.-measurable f would collapse every distributional pairing to the default value the Bochner integral assigns outside integrability hypotheses, so f would vacuously satisfy W^(k,p) membership. The Hölder space C^(r,α) here imposes r-times continuous differentiability, α-Hölder continuity of the r-th derivative, and boundedness of derivatives up to order r. The theorem is listed as §111 in Knill's *Some Fundamental Theorems in Mathematics*.

Source: C.B. Morrey, 'Functions of several variables and absolute continuity, II', Duke Math. J. 6 (1940) 187–215; full Sobolev-embedding development in *Multiple Integrals in the Calculus of Variations*, Springer 1966. Listed as §111 in O. Knill, *Some Fundamental Theorems in Mathematics* (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: The Morrey-regime proof has two pieces. (1) **Morrey's lemma**: if f ∈ W^(1,p)(B_1(0)) with p > n, then f has a (1 − n/p)-Hölder continuous representative on B_1(0), with explicit Hölder constant `C · ‖∇f‖_{L^p}`. The proof bounds `|f(x) − f(y)|` by averaging the radial fundamental-solution potential representation against `∇f` and applying Hölder's inequality with exponent p — using p > n to absorb the singular kernel `|x − z|^{1−n}` in L^{p'}. (2) **Iteration on derivatives**: for k > 1, apply Morrey's lemma to D^{k−1} f ∈ W^(1,p), yielding (1 − n/p)-Hölder continuity of the (k−1)-th derivative, hence f ∈ C^{k−1, 1 − n/p}. The general r + α < k − n/p case interpolates: every derivative up to order r is bounded, the r-th derivative is α-Hölder for any α < min(1, k − n/p − r). Mathlib has Gagliardo–Nirenberg–Sobolev (the subcritical L^p → L^q embedding, `eLpNorm_le_eLpNorm_fderiv_*`), Bessel-potential `H^{s,p}` spaces (`TemperedDistribution.MemSobolev`), and `HolderWith`/`iteratedFDeriv`, but no weak-derivative Sobolev space `W^{k,p}` and no Morrey-regime embedding into Hölder spaces.

theorem declaration uses `sorry`sobolev_embedding {n k r : ℕ} {α p : ℝ}
    (_hp : (n : ℝ) < p) (_hα : 0 < α) (_hα1 : α ≤ 1)
    (_hgap : (r : ℝ) + α < (k : ℝ) - n / p)
    (f : LeanEval.Analysis.SobolevMorreyProblem.E n → ℝ) (_hf : LeanEval.Analysis.SobolevMorreyProblem.MemSobolevWk k (ENNReal.ofReal p) f) :
    ∃ g : LeanEval.Analysis.SobolevMorreyProblem.E n → ℝ, f =ᵐ[volume] g ∧ LeanEval.Analysis.SobolevMorreyProblem.MemHolder r α g := byn:ℕk:ℕr:ℕα:ℝp:ℝ_hp:↑n < p_hα:0 < α_hα1:α ≤ 1_hgap:↑r + α < ↑k - ↑n / pf:E n → ℝ_hf:MemSobolevWk k (ENNReal.ofReal p) f⊢ ∃ g, f =ᶠ[ae volume] g ∧ LeanEval.Analysis.SobolevMorreyProblem.MemHolder r α g
  sorryAll goals completed! 🐙

Solved by

• @GanjinZero with Seed Prover (ByteDance) on Jun 5, 2026