Local Rellich compactness for first-order Sobolev functions

Restriction of the values of arbitrary W^{1,p}(Ω) functions to an open V with compact closure inside Ω is compact into Lᵖ(V), for 1 ≤ p < ∞. No boundary regularity or vanishing trace is required: a smooth cutoff equal to one near closure V turns each Sobolev function into a zero-boundary Sobolev function on Ω, to which Rellich--Kondrachov applies on a bounded subdomain containing closure V. This local compactness is used when passing to limits in interior elliptic estimates and weak-solution arguments.

The global compactness theorem for zero-boundary functions is TauCeti.W1p0.isCompactOperator_valueL.

Reference

H. Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations, Theorem 9.16 (Rellich--Kondrachov compact embedding on bounded C¹ domains). The local statement here follows by cutoff localization and the zero-boundary theorem above.

theorem TauCeti.W1p.isCompactOperator_valueL_restrictL {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega V : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) (hVc : IsCompact (closure ↑V)) (hVO : closure ↑V ⊆ ↑Omega) : IsCompactOperator ⇑(valueL ∘SL restrictL ⋯)

Local Rellich--Kondrachov compactness. If V has compact closure contained in Ω and 1 ≤ p < ∞, restriction of values from W^{1,p}(Ω) to Lᵖ(V) is compact. Neither the boundedness nor the boundary regularity of Ω is required.