Documentation

Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential

Unique derivative sets in manifolds #

In this file, we prove various properties of unique derivative sets in manifolds.

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] [SmoothManifoldWithCorners I 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'] [SmoothManifoldWithCorners I' 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] [SmoothManifoldWithCorners I 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'] [SmoothManifoldWithCorners I' 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] [SmoothManifoldWithCorners I 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'] [SmoothManifoldWithCorners I' 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] [SmoothManifoldWithCorners I 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'] [SmoothManifoldWithCorners I' 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] [SmoothManifoldWithCorners I 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'] [SmoothManifoldWithCorners I' 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.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] [SmoothManifoldWithCorners I M] {s : Set 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.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] [SmoothManifoldWithCorners I 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) (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 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_8} [NormedAddCommGroup F] [NormedSpace ๐•œ F] {Z : M โ†’ Type u_9} [TopologicalSpace (Bundle.TotalSpace F Z)] [(b : M) โ†’ TopologicalSpace (Z b)] [(b : M) โ†’ AddCommMonoid (Z b)] [(b : M) โ†’ Module ๐•œ (Z b)] [FiberBundle F Z] [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
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] [SmoothManifoldWithCorners I M] {s : Set M} {F : Type u_8} [NormedAddCommGroup F] [NormedSpace ๐•œ F] {Z : M โ†’ Type u_9} [TopologicalSpace (Bundle.TotalSpace F Z)] [(b : M) โ†’ TopologicalSpace (Z b)] [(b : M) โ†’ AddCommMonoid (Z b)] [(b : M) โ†’ Module ๐•œ (Z b)] [FiberBundle F Z] [VectorBundle ๐•œ F Z] [SmoothVectorBundle F Z I] {p : Bundle.TotalSpace F Z} (hs : UniqueMDiffWithinAt I s p.proj) :
UniqueMDiffWithinAt (I.prod (modelWithCornersSelf ๐•œ F)) (Bundle.TotalSpace.proj โปยน' s) p
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] [SmoothManifoldWithCorners I M] {s : Set M} {F : Type u_8} [NormedAddCommGroup F] [NormedSpace ๐•œ F] (Z : M โ†’ Type u_9) [TopologicalSpace (Bundle.TotalSpace F Z)] [(b : M) โ†’ TopologicalSpace (Z b)] [(b : M) โ†’ AddCommMonoid (Z b)] [(b : M) โ†’ Module ๐•œ (Z b)] [FiberBundle F Z] [VectorBundle ๐•œ F Z] [SmoothVectorBundle F Z I] {b : M} (hs : UniqueMDiffWithinAt I s b) (x : Z b) :
UniqueMDiffWithinAt (I.prod (modelWithCornersSelf ๐•œ F)) (Bundle.TotalSpace.proj โปยน' s) { proj := b, snd := x }
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] [SmoothManifoldWithCorners I M] {s : Set M} {F : Type u_8} [NormedAddCommGroup F] [NormedSpace ๐•œ F] (Z : M โ†’ Type u_9) [TopologicalSpace (Bundle.TotalSpace F Z)] [(b : M) โ†’ TopologicalSpace (Z b)] [(b : M) โ†’ AddCommMonoid (Z b)] [(b : M) โ†’ Module ๐•œ (Z b)] [FiberBundle F Z] [VectorBundle ๐•œ F Z] [SmoothVectorBundle F Z I] (hs : UniqueMDiffOn I s) :
UniqueMDiffOn (I.prod (modelWithCornersSelf ๐•œ F)) (Bundle.TotalSpace.proj โปยน' s)

In a smooth fiber bundle, the preimage under the projection of a set with unique differential in the basis also has unique differential.

theorem UniqueMDiffOn.tangentBundle_proj_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] [SmoothManifoldWithCorners I M] {s : Set M} (hs : UniqueMDiffOn I s) :
UniqueMDiffOn I.tangent (Bundle.TotalSpace.proj โปยน' s)

The preimage under the projection from the tangent bundle of a set with unique differential in the basis also has unique differential.