Documentation

LeanPool.RellichKondrachov.Geometry.Manifold.Sobolev.ChartMeasureLp

RellichKondrachov.Geometry.Manifold.Sobolev.ChartMeasureLp #

L²-level utilities for chart pushforward measures.

Given d : FiniteChartData and a measure μ on M, ChartMeasure defines the pushforward measure chartMeasure μ i on the model space E along the extended chart extChartAt I (d.center i).

This file provides:

Main definitions #

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

Borel σ-algebra on the manifold M.

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

    Borel σ-algebra on the model space E.

    Equations
    Instances For
      source
      theorem RellichKondrachov.Geometry.Manifold.Sobolev.instBorelSpaceEChartMeasureLp {E : Type u_1} [NormedAddCommGroup E] :
      BorelSpace E
      source
      theorem RellichKondrachov.Geometry.Manifold.Sobolev.instOpensMeasurableSpaceChartMeasureLp {E : Type u_1} [NormedAddCommGroup E] :
      OpensMeasurableSpace E
      source
      noncomputable def RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.extChartAtMk {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [IsManifold I ⊤ M] (d : FiniteChartData H M I) (μ : MeasureTheory.Measure M) (i : d.ι) :
      M → E

      A measurable modification of the extended chart extChartAt, relative to the restricted measure on the chart source.

      Equations
      Instances For
        source
        theorem RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.extChartAt_ae_eq_extChartAtMk {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [IsManifold I ⊤ M] (d : FiniteChartData H M I) (μ : MeasureTheory.Measure M) (i : d.ι) :
        ↑(extChartAt I (d.center i)) =ᵐ[μ.restrict (extChartAt I (d.center i)).source] d.extChartAtMk μ i
        source
        theorem RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.measurePreserving_extChartAtMk {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [IsManifold I ⊤ M] (d : FiniteChartData H M I) (μ : MeasureTheory.Measure M) (i : d.ι) :
        MeasureTheory.MeasurePreserving (d.extChartAtMk μ i) (μ.restrict (extChartAt I (d.center i)).source) (d.chartMeasure μ i)

        The measurable modification extChartAtMk is measure-preserving from the restricted measure on the chart source to chartMeasure.

        source
        noncomputable def RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.chartPullbackL2 {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [IsManifold I ⊤ M] (d : FiniteChartData H M I) {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] (μ : MeasureTheory.Measure M) (i : d.ι) :
        ↥(MeasureTheory.Lp F 2 (d.chartMeasure μ i)) →ₗᵢ[ℝ] ↥(MeasureTheory.Lp F 2 (μ.restrict (extChartAt I (d.center i)).source))

        Pull back L² functions on the chart model space E to L² functions on M, using the measure-preserving measurable modification extChartAtMk.

        Equations
        Instances For