Vector-valued local Rellich compactness

For a finite-dimensional target, restriction of a weakly differentiable Lᵖ field to an open set compactly contained in its domain is compact for every 1 ≤ p ≤ ∞. No boundary condition or boundedness of the ambient domain is required. The graph-space version retains an arbitrary preceding space and field-selection map, so it also applies to higher weak-derivative steps.

TauCeti.WeakDerivStep.restrictBaseL restricts the selected field, and TauCeti.WeakDerivStep.isCompactOperator_restrictBaseL proves its compactness. The proof projects to scalar coordinates using toW1pL, applies TauCeti.W1p.isCompactOperator_valueL_restrictL, and reconstructs the field in a finite basis through TauCeti.isCompactOperator_of_forall_isCompactOperator_compLpL_comp. Finite dimensionality of the target is essential: constant fields valued in an infinite orthonormal sequence already obstruct local norm compactness.

In particular this supplies compact restriction of W^{1,2}(ℝ,F) paths to bounded intervals (TauCeti.WeakDerivStep.isCompactOperator_smul_restrictBaseL), the compact error term in the Fredholm estimates for first-order trajectory operators.

Reference

H. Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations, Theorem 9.16 (Rellich--Kondrachov); the vector-valued extension is coordinatewise.

theorem TauCeti.WeakDerivStep.isCompactOperator_restrictBaseL {E : Type u_1} {F : Type u_2} {X : Type u_3} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [SeminormedAddCommGroup X] [NormedSpace ℝ X] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega V : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] [FiniteDimensional ℝ F] (base : X →L[ℝ] ↥(MeasureTheory.Lp F p (mu.restrict ↑Omega))) (hVc : IsCompact (closure ↑V)) (hVO : closure ↑V ⊆ ↑Omega) : IsCompactOperator ⇑(restrictBaseL base ⋯)

Restriction to a compactly contained open subset is compact for a finite-dimensional target and 1 ≤ p ≤ ∞. The preceding space need not be complete.

theorem TauCeti.WeakDerivStep.isCompactOperator_smul_restrictBaseL {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] (K R : ℝ) : IsCompactOperator ⇑(K • restrictBaseL (ContinuousLinearMap.id ℝ ↥(MeasureTheory.Lp F 2 (MeasureTheory.volume.restrict ↑⊤))) ⋯)

Restriction of W^{1,2}(ℝ, F) paths to a bounded interval, scaled by a constant, is compact.