RellichKondrachov.Geometry.Manifold.Sobolev.RellichKondrachov

Infrastructure for proving Rellich–Kondrachov compact embeddings on compact manifolds.

This file is intentionally small: it packages the operator-theoretic glue showing that the manifold embedding H¹ → L² (defined as a finite sum of chart contributions in Sobolev.EmbeddingL2) is compact once each chart contribution is compact.

The analytic heart of Rellich (compactness on Euclidean chart domains) is tracked separately.

Main results

• RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.isCompactOperator_h1ToL2_of_summands
• RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.isCompactOperator_h2ToL2_of_summands

@[implicit_reducible]

def RellichKondrachov.Geometry.Manifold.Sobolev.instMeasurableSpaceMRellichKondrachov {M : Type u_3} [TopologicalSpace M] : MeasurableSpace M

Borel σ-algebra on the manifold M.

Equations

• RellichKondrachov.Geometry.Manifold.Sobolev.instMeasurableSpaceMRellichKondrachov = borel M

theorem RellichKondrachov.Geometry.Manifold.Sobolev.instBorelSpaceMRellichKondrachov {M : Type u_3} [TopologicalSpace M] : BorelSpace M

@[implicit_reducible]

def RellichKondrachov.Geometry.Manifold.Sobolev.instMeasurableSpaceERellichKondrachov {E : Type u_1} [NormedAddCommGroup E] : MeasurableSpace E

Borel σ-algebra on the model space E.

Equations

• RellichKondrachov.Geometry.Manifold.Sobolev.instMeasurableSpaceERellichKondrachov = borel E

theorem RellichKondrachov.Geometry.Manifold.Sobolev.instBorelSpaceERellichKondrachov {E : Type u_1} [NormedAddCommGroup E] : BorelSpace E

theorem RellichKondrachov.Geometry.Manifold.Sobolev.instOpensMeasurableSpaceERellichKondrachov {E : Type u_1} [NormedAddCommGroup E] : OpensMeasurableSpace E

theorem RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.isCompactOperator_h1ToL2_of_summands {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {H : Type u_2} [TopologicalSpace H] {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [IsManifold I ⊤ M] [IsManifold I 1 M] [I.Boundaryless] [CompactSpace M] (d : FiniteChartData H M I) (μ : MeasureTheory.Measure M) [MeasureTheory.IsFiniteMeasure μ] (h : ∀ (i : d.ι), IsCompactOperator fun (x : ↥(d.h1 μ)) => (d.chartToGlobalL2 μ i) ((d.h1ToChartL2 μ i) x)) : IsCompactOperator fun (x : ↥(d.h1 μ)) => (d.h1ToL2 μ) x

If each chart contribution in the definition of h1ToL2 is a compact operator, then the manifold inclusion H¹ → L² is a compact operator.

theorem RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.isCompactOperator_h2ToL2_of_summands {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {H : Type u_2} [TopologicalSpace H] {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [IsManifold I ⊤ M] [I.Boundaryless] [CompactSpace M] (d : FiniteChartData H M I) (μ : MeasureTheory.Measure M) [MeasureTheory.IsFiniteMeasure μ] (h : ∀ (i : d.ι), IsCompactOperator fun (x : ↥(d.h2 μ)) => (d.chartToGlobalL2 μ i) ((d.h2ToChartL2 μ i) x)) : IsCompactOperator fun (x : ↥(d.h2 μ)) => (d.h2ToL2 μ) x

If each chart contribution in the definition of h2ToL2 is a compact operator, then the manifold inclusion H² → L² is a compact operator.