RellichKondrachov.Geometry.Manifold.Sobolev.ChartMeasure

Pushforward measures on the model space arising from charts.

For chart-based Sobolev spaces on a manifold M, it is convenient to transport the ambient measure on M to a measure on the model space E using extChartAt. This file defines the resulting measures and records basic finiteness instances needed by the Euclidean Sobolev baseline.

@[implicit_reducible]

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

Borel σ-algebra on the model space E.

Equations

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

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

@[implicit_reducible]

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

Borel σ-algebra on the model space E.

Equations

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

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

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

theorem RellichKondrachov.Geometry.Manifold.Sobolev.isFiniteMeasureOnCompacts_of_isFiniteMeasure {α : Type u_4} [TopologicalSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] : MeasureTheory.IsFiniteMeasureOnCompacts μ

Any finite measure is finite on compact sets.

Chart measures

Given a measure μ on M, each chart center d.center i yields a pushforward measure on E along the extended chart extChartAt I (d.center i).

We define this as a pushforward of the restricted measure μ.restrict (extChartAt I (d.center i)).source so that the value of extChartAt outside its source is irrelevant.

noncomputable def RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.chartMeasure {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.Measure E

The pushforward of a measure μ on M along the extended chart extChartAt.

Equations

• d.chartMeasure μ i = MeasureTheory.Measure.map (↑(extChartAt I (d.center i))) (μ.restrict (extChartAt I (d.center i)).source)

theorem RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.aemeasurable_extChartAt {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.ι) : AEMeasurable (↑(extChartAt I (d.center i))) (μ.restrict (extChartAt I (d.center i)).source)

The extended chart is a.e.-measurable with respect to the restricted measure on its source.

instance RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.instIsFiniteMeasurechartMeasure {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.IsFiniteMeasure μ] : MeasureTheory.IsFiniteMeasure (d.chartMeasure μ i)

instance RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.instIsFiniteMeasureOnCompactschartMeasure {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.IsFiniteMeasure μ] : MeasureTheory.IsFiniteMeasureOnCompacts (d.chartMeasure μ i)