`RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.Rellich` #

Euclidean Rellich–Kondrachov compactness for fixed compact support (Lebesgue volume).

This file discharges the “Euclidean heart” needed by the manifold Rellich glue: for a fixed compact set K ⊆ E, the inclusion H¹ → L² is compact when restricted to the closed subspace of H¹ whose L² component is supported in K (a.e.).

The proof uses:

the Euclidean H¹ translation estimate ‖τ_a u - u‖₂ ≤ ‖a‖ · ‖∇u‖₂ (TranslationEstimateH1);
the Fréchet–Kolmogorov / smoothing-based L² compactness criterion (L2CompactnessCriterion).

Main definitions / results #

RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.h1On: the closed subspace of H¹(volume) whose L² component is supported in K (a.e.).
RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.h1OnToL2: the restricted inclusion map h1On K →L[ℝ] L²(volume).
RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.isCompactOperator_h1OnToL2: compactness of the inclusion.

Tracking: Beads lean-103.5.2.26.5.3.2.1.

source

@[implicit_reducible]

def RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.instMeasurableSpaceRellich {E : Type u_1} [NormedAddCommGroup E] :

MeasurableSpace E

Borel σ-algebra on the model space E.

Equations

RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.instMeasurableSpaceRellich = borel E

Instances For

source

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.instBorelSpaceRellich {E : Type u_1} [NormedAddCommGroup E] :

BorelSpace E

source

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.instOpensMeasurableSpaceRellich {E : Type u_1} [NormedAddCommGroup E] :

OpensMeasurableSpace E

source

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.instMeasurableAddRellich {E : Type u_1} [NormedAddCommGroup E] :

MeasurableAdd E

source

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.instMeasurableNegRellich {E : Type u_1} [NormedAddCommGroup E] :

MeasurableNeg E

source

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.instFactOneLeTwoSobolevEuclideanRellich :

Fact (1 ≤ 2)

Supported `H¹` subspace #

source

noncomputable def RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.h1On {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [CompleteSpace E] (K : Set E) (hKm : MeasurableSet K) :

Submodule ℝ ↥(h1 MeasureTheory.volume)

The subspace of H¹(volume) whose L² component is (a.e.) supported in K.

We model “supported in K” as belonging to the closed range of the extension-by-zero map Lp(volume.restrict K) →ₗᵢ Lp(volume).

Equations

One or more equations did not get rendered due to their size.

Instances For

source

noncomputable def RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.h1OnToL2 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [CompleteSpace E] (K : Set E) (hKm : MeasurableSet K) :

↥(h1On K hKm) →L[ℝ ] ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)

The inclusion h1On K → L²(volume) as a continuous linear map.

Equations

One or more equations did not get rendered due to their size.

Instances For

Euclidean Rellich on fixed compact support #

source

theorem RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.isCompactOperator_h1OnToL2 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [CompleteSpace E] {K : Set E} (_hK : IsCompact K) (hKm : MeasurableSet K) :

IsCompactOperator ⇑(h1OnToL2 K hKm)

Euclidean Rellich–Kondrachov compactness (Lebesgue): on a fixed compact support K, the inclusion H¹ → L² is a compact operator.

Codomain restriction and a compact map into `L²(volume.restrict K)` #

The definition of h1On forces the image of h1OnToL2 to lie in the (closed) range of the extension-by-zero map from volume.restrict K. We record a codomain-restricted version and a convenient compact map to the restricted L² space.

source