Sobolev embedding theorem (Morrey regime)

sobolev_embedding_morrey — a formalization challenge from the lean-eval benchmark.

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.

Formal statement

/-- **Sobolev embedding theorem (Morrey regime).** If `n < p`,
`0 < α ≤ 1` and `r + α < k − n/p`, then every `W^{k,p}(ℝⁿ)` function
has a `C^{r,α}` representative. -/
theorem sobolev_embedding {n k r : ℕ} {α p : ℝ}
    (_hp : (n : ℝ) < p) (_hα : 0 < α) (_hα1 : α ≤ 1)
    (_hgap : (r : ℝ) + α < (k : ℝ) - n / p)
    (f : E n → ℝ) (_hf : MemSobolevWk k (ENNReal.ofReal p) f) :
    ∃ g : E n → ℝ, f =ᵐ[volume] g ∧ MemHolder r α g := by
  sorry

Informal solution sketch

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.

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).

How to submit

Challenge.lean and Solution.lean are part of the trusted benchmark and must not be modified. Write your proof in Submission.lean (plus any local modules under Submission/). Mathlib may be used freely; anything not in Mathlib has to be inlined into the submission.

Comparator configuration

• Solution module: Solution
• Theorems checked: sobolev_embedding
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Kim Morrison.