Extended manifold charts as measurable embeddings #
Mathlib's extended chart at a point is a PartialEquiv between a manifold and its model vector
space. Its restrictions to the chart source and target are mutually continuous, hence the chart
restricted to its source is a measurable embedding for Borel measurable spaces. This is the
form used to transport measures between a manifold and coordinates.
Main results #
TauCeti.measurableEmbedding_extChartAt_restrict: an extended chart restricted to its source is a measurable embedding.TauCeti.MeasurableSet.image_extChartAt: the image of a measurable subset of a chart source is measurable in the model space.
@[instance_reducible]
The Borel measurable space on the model vector space, used in this file.
Equations
Instances For
The model vector space's measurable space is its Borel measurable space.
theorem
TauCeti.measurableEmbedding_extChartAt_restrict
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
[MeasurableSpace M]
[BorelSpace M]
(x : M)
:
MeasurableEmbedding ((extChartAt I x).source.domRestrict ↑(extChartAt I x))
The extended chart at x, restricted to its source, is a measurable embedding for the Borel
measurable spaces.
theorem
MeasurableSet.image_extChartAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
[MeasurableSpace M]
[BorelSpace M]
{s : Set M}
(hs : MeasurableSet s)
(x : M)
(hsource : s ⊆ (extChartAt I x).source)
:
MeasurableSet (↑(extChartAt I x) '' s)
The image of a measurable subset of an extended chart's source is measurable in the model space.