Rellich--Kondrachov for zero-boundary first-order Sobolev spaces

This file proves that the canonical value map

W^{1,p}_0(Ω) → Lᵖ(Ω)

is a compact operator, for 1 ≤ p < ∞ and a bounded open subset Ω of a finite-dimensional real inner-product space. No regularity of the boundary is needed: a zero-boundary Sobolev function extends by zero to a whole-space Sobolev function, and the extension is supported in Ω.

The proof applies the Fréchet--Kolmogorov criterion to the zero-extended values of the open unit ball. Their Lᵖ norms are uniformly bounded by their Sobolev norms, their supports lie in the fixed bounded set Ω, and the whole-space Sobolev translation estimate bounds every translation increment by ‖h‖ ‖∇u‖ₚ. Restriction back to Ω then gives compactness of the canonical value map TauCeti.W1p0.valueL.

The corresponding statement for all of W^{1,p}(Ω) requires a boundary-regular extension operator and is not claimed here.

Main declaration

• TauCeti.W1p0.isCompactOperator_valueL: Rellich--Kondrachov for W^{1,p}_0(Ω).

References

Lane A.6 of TauCetiRoadmap/PDE/README.md; H. Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations, Corollary 9.16; L. C. Evans, Partial Differential Equations, Section 5.7. The compactness criterion used here is the Kolmogorov--Riesz form proved in TauCeti/MeasureTheory/Function/Lp/FrechetKolmogorov.lean.

theorem TauCeti.W1p0.isCompactOperator_valueL {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) (hOmega : Bornology.IsBounded ↑Omega) : IsCompactOperator ⇑valueL

Rellich--Kondrachov for zero-boundary Sobolev spaces. If Ω is bounded and 1 ≤ p < ∞, the canonical value map W^{1,p}_0(Ω) → Lᵖ(Ω) is a compact operator.

No boundary regularity is assumed. The zero-boundary condition is what permits extension by zero without creating a distributional boundary term.