Unique derivative sets in manifolds #
In this file, we prove various properties of unique derivative sets in manifolds.
image_denseRange: supposefis differentiable onsand its derivative at every point ofshas dense range. Ifshas the unique differential property, then so doesf '' s.uniqueMDiffOn_preimage: the unique differential property is preserved by local diffeomorphismsuniqueDiffOn_target_inter: the unique differential property is preserved by pullbacks of extended chartstangentBundle_proj_preimage: ifshas the unique differential property, its preimage under the tangent bundle projection also has
Unique derivative sets in manifolds #
theorem
UniqueMDiffWithinAt.image_denseRange
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{s : Set M}
{x : M}
(hs : UniqueMDiffWithinAt I s x)
{f : M โ M'}
{f' : E โL[๐] E'}
(hf : HasMFDerivWithinAt I I' f s x f')
(hd : DenseRange โf')
:
UniqueMDiffWithinAt I' (f '' s) (f x)
If s has the unique differential property at x, f is differentiable within s at xand its derivative has dense range, thenf '' shas the unique differential property atf x`.
theorem
UniqueMDiffOn.image_denseRange'
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{s : Set M}
(hs : UniqueMDiffOn I s)
{f : M โ M'}
{f' : M โ E โL[๐] E'}
(hf : โ x โ s, HasMFDerivWithinAt I I' f s x (f' x))
(hd : โ x โ s, DenseRange โ(f' x))
:
UniqueMDiffOn I' (f '' s)
If s has the unique differential property, f is differentiable on s and its derivative
at every point of s has dense range, then f '' s has the unique differential property.
This version uses the HasMFDerivWithinAt predicate.
theorem
UniqueMDiffOn.image_denseRange
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{s : Set M}
(hs : UniqueMDiffOn I s)
{f : M โ M'}
(hf : MDifferentiableOn I I' f s)
(hd : โ x โ s, DenseRange โ(mfderivWithin I I' f s x))
:
UniqueMDiffOn I' (f '' s)
If s has the unique differential property, f is differentiable on s and its derivative
at every point of s has dense range, then f '' s has the unique differential property.
theorem
UniqueMDiffWithinAt.preimage_partialHomeomorph
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{s : Set M}
{x : M}
(hs : UniqueMDiffWithinAt I s x)
{e : PartialHomeomorph M M'}
(he : PartialHomeomorph.MDifferentiable I I' e)
(hx : x โ e.source)
:
UniqueMDiffWithinAt I' (e.target โฉ โe.symm โปยน' s) (โe x)
theorem
UniqueMDiffOn.uniqueMDiffOn_preimage
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{s : Set M}
(hs : UniqueMDiffOn I s)
{e : PartialHomeomorph M M'}
(he : PartialHomeomorph.MDifferentiable I I' e)
:
UniqueMDiffOn I' (e.target โฉ โe.symm โปยน' s)
If a set has the unique differential property, then its image under a local diffeomorphism also has the unique differential property.
theorem
UniqueMDiffOn.uniqueMDiffOn_target_inter
{๐ : 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]
{s : Set M}
[SmoothManifoldWithCorners I M]
(hs : UniqueMDiffOn I s)
(x : M)
:
UniqueMDiffOn (modelWithCornersSelf ๐ E) ((extChartAt I x).target โฉ โ(extChartAt I x).symm โปยน' s)
If a set in a manifold has the unique derivative property, then its pullback by any extended chart, in the vector space, also has the unique derivative property.
theorem
UniqueMDiffOn.uniqueDiffOn_target_inter
{๐ : 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]
{s : Set M}
[SmoothManifoldWithCorners I M]
(hs : UniqueMDiffOn I s)
(x : M)
:
UniqueDiffOn ๐ ((extChartAt I x).target โฉ โ(extChartAt I x).symm โปยน' s)
If a set in a manifold has the unique derivative property, then its pullback by any extended chart, in the vector space, also has the unique derivative property.
theorem
UniqueMDiffOn.uniqueDiffWithinAt_range_inter
{๐ : 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]
{s : Set M}
[SmoothManifoldWithCorners I M]
(hs : UniqueMDiffOn I s)
(x : M)
(y : E)
(hy : y โ (extChartAt I x).target โฉ โ(extChartAt I x).symm โปยน' s)
:
UniqueDiffWithinAt ๐ (Set.range โI โฉ โ(extChartAt I x).symm โปยน' s) y
theorem
UniqueMDiffOn.uniqueDiffOn_inter_preimage
{๐ : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace ๐ E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners ๐ E' H'}
{M'' : Type u_8}
[TopologicalSpace M'']
[ChartedSpace H' M'']
{s : Set M}
[SmoothManifoldWithCorners I M]
(hs : UniqueMDiffOn I s)
(x : M)
(y : M'')
{f : M โ M''}
(hf : ContinuousOn f s)
:
UniqueDiffOn ๐ ((extChartAt I x).target โฉ โ(extChartAt I x).symm โปยน' (s โฉ f โปยน' (extChartAt I' y).source))
When considering functions between manifolds, this statement shows up often. It entails the unique differential of the pullback in extended charts of the set where the function can be read in the charts.
theorem
UniqueMDiffWithinAt.bundle_preimage
{๐ : 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]
{s : Set M}
{F : Type u_9}
[NormedAddCommGroup F]
[NormedSpace ๐ F]
{Z : M โ Type u_10}
[TopologicalSpace (Bundle.TotalSpace F Z)]
[(b : M) โ TopologicalSpace (Z b)]
[FiberBundle F Z]
{p : Bundle.TotalSpace F Z}
(hs : UniqueMDiffWithinAt I s p.proj)
:
UniqueMDiffWithinAt (I.prod (modelWithCornersSelf ๐ F)) (Bundle.TotalSpace.proj โปยน' s) p
In a fiber bundle, the preimage under the projection of a set with unique differentials in the base has unique differentials in the bundle.
@[deprecated UniqueMDiffWithinAt.bundle_preimage]
theorem
UniqueMDiffWithinAt.smooth_bundle_preimage
{๐ : 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]
{s : Set M}
{F : Type u_9}
[NormedAddCommGroup F]
[NormedSpace ๐ F]
{Z : M โ Type u_10}
[TopologicalSpace (Bundle.TotalSpace F Z)]
[(b : M) โ TopologicalSpace (Z b)]
[FiberBundle F Z]
{p : Bundle.TotalSpace F Z}
(hs : UniqueMDiffWithinAt I s p.proj)
:
UniqueMDiffWithinAt (I.prod (modelWithCornersSelf ๐ F)) (Bundle.TotalSpace.proj โปยน' s) p
Alias of UniqueMDiffWithinAt.bundle_preimage.
In a fiber bundle, the preimage under the projection of a set with unique differentials in the base has unique differentials in the bundle.
theorem
UniqueMDiffWithinAt.bundle_preimage'
{๐ : 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]
{s : Set M}
{F : Type u_9}
[NormedAddCommGroup F]
[NormedSpace ๐ F]
(Z : M โ Type u_10)
[TopologicalSpace (Bundle.TotalSpace F Z)]
[(b : M) โ TopologicalSpace (Z b)]
[FiberBundle F Z]
{b : M}
(hs : UniqueMDiffWithinAt I s b)
(x : Z b)
:
UniqueMDiffWithinAt (I.prod (modelWithCornersSelf ๐ F)) (Bundle.TotalSpace.proj โปยน' s) { proj := b, snd := x }
In a fiber bundle, the preimage under the projection of a set with unique differentials
in the base has unique differentials in the bundle. Version with a point โจb, xโฉ.
@[deprecated UniqueMDiffWithinAt.bundle_preimage']
theorem
UniqueMDiffWithinAt.smooth_bundle_preimage'
{๐ : 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]
{s : Set M}
{F : Type u_9}
[NormedAddCommGroup F]
[NormedSpace ๐ F]
(Z : M โ Type u_10)
[TopologicalSpace (Bundle.TotalSpace F Z)]
[(b : M) โ TopologicalSpace (Z b)]
[FiberBundle F Z]
{b : M}
(hs : UniqueMDiffWithinAt I s b)
(x : Z b)
:
UniqueMDiffWithinAt (I.prod (modelWithCornersSelf ๐ F)) (Bundle.TotalSpace.proj โปยน' s) { proj := b, snd := x }
Alias of UniqueMDiffWithinAt.bundle_preimage'.
In a fiber bundle, the preimage under the projection of a set with unique differentials
in the base has unique differentials in the bundle. Version with a point โจb, xโฉ.
theorem
UniqueMDiffOn.bundle_preimage
{๐ : 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]
{s : Set M}
{F : Type u_9}
[NormedAddCommGroup F]
[NormedSpace ๐ F]
(Z : M โ Type u_10)
[TopologicalSpace (Bundle.TotalSpace F Z)]
[(b : M) โ TopologicalSpace (Z b)]
[FiberBundle F Z]
(hs : UniqueMDiffOn I s)
:
UniqueMDiffOn (I.prod (modelWithCornersSelf ๐ F)) (Bundle.TotalSpace.proj โปยน' s)
In a fiber bundle, the preimage under the projection of a set with unique differentials in the base has unique differentials in the bundle.
@[deprecated UniqueMDiffOn.bundle_preimage]
theorem
UniqueMDiffOn.smooth_bundle_preimage
{๐ : 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]
{s : Set M}
{F : Type u_9}
[NormedAddCommGroup F]
[NormedSpace ๐ F]
(Z : M โ Type u_10)
[TopologicalSpace (Bundle.TotalSpace F Z)]
[(b : M) โ TopologicalSpace (Z b)]
[FiberBundle F Z]
(hs : UniqueMDiffOn I s)
:
UniqueMDiffOn (I.prod (modelWithCornersSelf ๐ F)) (Bundle.TotalSpace.proj โปยน' s)
Alias of UniqueMDiffOn.bundle_preimage.
In a fiber bundle, the preimage under the projection of a set with unique differentials in the base has unique differentials in the bundle.
theorem
Trivialization.mdifferentiable
{๐ : 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]
{F : Type u_9}
[NormedAddCommGroup F]
[NormedSpace ๐ F]
(Z : M โ Type u_10)
[TopologicalSpace (Bundle.TotalSpace F Z)]
[(b : M) โ TopologicalSpace (Z b)]
[FiberBundle F Z]
[(b : M) โ AddCommMonoid (Z b)]
[(b : M) โ Module ๐ (Z b)]
[VectorBundle ๐ F Z]
[SmoothVectorBundle F Z I]
(e : Trivialization F Bundle.TotalSpace.proj)
[MemTrivializationAtlas e]
:
PartialHomeomorph.MDifferentiable (I.prod (modelWithCornersSelf ๐ F)) (I.prod (modelWithCornersSelf ๐ F))
e.toPartialHomeomorph