Documentation

LeanPool.RellichKondrachov.Geometry.Manifold.Sobolev.RellichKondrachovRiemannian.Global

RellichKondrachov.Geometry.Manifold.Sobolev.RellichKondrachovRiemannian.Global #

Finite-atlas assembly: turn the per-chart compactness result into compactness of the global H¹ → L² map for the Riemannian volume measure.

source
@[implicit_reducible]
def RellichKondrachov.Geometry.Manifold.Sobolev.instMeasurableSpaceMGlobal {M : Type u_3} [TopologicalSpace M] :
MeasurableSpace M

Borel σ-algebra on the manifold M.

Equations
Instances For
    source
    theorem RellichKondrachov.Geometry.Manifold.Sobolev.instBorelSpaceMGlobal {M : Type u_3} [TopologicalSpace M] :
    BorelSpace M
    source
    @[implicit_reducible]
    def RellichKondrachov.Geometry.Manifold.Sobolev.instMeasurableSpaceEGlobal {E : Type u_1} [NormedAddCommGroup E] :
    MeasurableSpace E

    Borel σ-algebra on the model space E.

    Equations
    Instances For
      source
      theorem RellichKondrachov.Geometry.Manifold.Sobolev.instBorelSpaceEGlobal {E : Type u_1} [NormedAddCommGroup E] :
      BorelSpace E
      source
      theorem RellichKondrachov.Geometry.Manifold.Sobolev.instOpensMeasurableSpaceGlobal {E : Type u_1} [NormedAddCommGroup E] :
      OpensMeasurableSpace E
      source
      theorem RellichKondrachov.Geometry.Manifold.Sobolev.instIsFiniteMeasureriemannianVolumeMeasureGlobal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] (I : ModelWithCorners ℝ E H) [IsManifold I 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] [T3Space M] [CompactSpace M] :
      MeasureTheory.IsFiniteMeasure (Riemannian.riemannianVolumeMeasure I)
      source
      theorem RellichKondrachov.Geometry.Manifold.Sobolev.RiemannianFiniteChartData.isCompactOperator_h1ToL2_riemannianVolume {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ 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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] [I.Boundaryless] [T3Space M] [CompactSpace M] (dR : RiemannianFiniteChartData I) :
      IsCompactOperator fun (x : ↥(dR.d.h1 (Riemannian.riemannianVolumeMeasure I))) => (dR.d.h1ToL2 (Riemannian.riemannianVolumeMeasure I)) x