Vector fields in manifolds #
We study functions of the form V : Π (x : M) → TangentSpace I x on a manifold, i.e.,
vector fields.
We define the pullback of a vector field under a map, as
VectorField.mpullback I I' f V x := (mfderiv I I' f x).inverse (V (f x))
(together with the same notion within a set). Note that the pullback uses the junk-value pattern:
if the derivative of the map is not invertible, then pullback is given the junk value zero.
We start developing API around this notion.
All these are given in the VectorField namespace because pullbacks, Lie brackets, and so on,
are notions that make sense in a variety of contexts. We also prefix the notions with m to
distinguish the manifold notions from the vector space notions.
For notions that come naturally in other namespaces for dot notation, we specify vectorField in
the name to lift ambiguities. For instance, the fact that the Lie bracket of two smooth vector
fields is smooth will be ContMDiffAt.mlieBracket_vectorField.
Note that a smoothness assumption for a vector field is written by seeing the vector field as
a function from M to its tangent bundle through a coercion, as in:
MDifferentiableWithinAt I I.tangent (fun y ↦ (V y : TangentBundle I M)) s x.
instance
instIsManifoldOfNatWithTopENatOfMinSmoothness
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{n : ℕ}
[n.AtLeastTwo]
[IsManifold I (minSmoothness 𝕜 (OfNat.ofNat n)) M]
:
IsManifold I (OfNat.ofNat n) M
instance
instIsManifoldOfNatWithTopENatOfMinSmoothness_1
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (minSmoothness 𝕜 1) M]
:
IsManifold I 1 M
instance
instIsManifoldMinSmoothnessOfNatWithTopENat
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (minSmoothness 𝕜 3) M]
:
IsManifold I (minSmoothness 𝕜 2) M
instance
instIsManifoldMinSmoothnessOfNatWithTopENat_1
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (minSmoothness 𝕜 2) M]
:
IsManifold I (minSmoothness 𝕜 1) M
Pullback of vector fields in manifolds #
def
VectorField.mpullbackWithin
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
(I : ModelWithCorners 𝕜 E H)
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
(I' : ModelWithCorners 𝕜 E' H')
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
(f : M → M')
(V : (x : M') → TangentSpace I' x)
(s : Set M)
(x : M)
:
TangentSpace I x
The pullback of a vector field under a map between manifolds, within a set s. If the
derivative of the map within s is not invertible, then pullback is given the junk value zero.
Equations
- VectorField.mpullbackWithin I I' f V s x = (mfderivWithin I I' f s x).inverse (V (f x))
Instances For
def
VectorField.mpullback
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
(I : ModelWithCorners 𝕜 E H)
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
(I' : ModelWithCorners 𝕜 E' H')
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
(f : M → M')
(V : (x : M') → TangentSpace I' x)
(x : M)
:
TangentSpace I x
The pullback of a vector field under a map between manifolds. If the derivative of the map is not invertible, then pullback is given the junk value zero.
Equations
- VectorField.mpullback I I' f V x = (mfderiv I I' f x).inverse (V (f x))
Instances For
theorem
VectorField.mpullbackWithin_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{x : M}
{V : (x : M') → TangentSpace I' x}
:
theorem
VectorField.mpullbackWithin_smul_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{x : M}
{V : (x : M') → TangentSpace I' x}
{c : 𝕜}
:
theorem
VectorField.mpullbackWithin_smul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{V : (x : M') → TangentSpace I' x}
{c : 𝕜}
:
theorem
VectorField.mpullbackWithin_add_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{x : M}
{V V₁ : (x : M') → TangentSpace I' x}
:
theorem
VectorField.mpullbackWithin_add
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{V V₁ : (x : M') → TangentSpace I' x}
:
theorem
VectorField.mpullbackWithin_neg_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{x : M}
{V : (x : M') → TangentSpace I' x}
:
theorem
VectorField.mpullbackWithin_neg
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{V : (x : M') → TangentSpace I' x}
:
theorem
VectorField.mpullbackWithin_id
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{x : M}
{V : (x : M) → TangentSpace I x}
(h : UniqueMDiffWithinAt I s x)
:
theorem
VectorField.mpullback_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{x : M}
{V : (x : M') → TangentSpace I' x}
:
theorem
VectorField.mpullback_smul_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{x : M}
{V : (x : M') → TangentSpace I' x}
{c : 𝕜}
:
theorem
VectorField.mpullback_smul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{V : (x : M') → TangentSpace I' x}
{c : 𝕜}
:
theorem
VectorField.mpullback_add_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{x : M}
{V V₁ : (x : M') → TangentSpace I' x}
:
theorem
VectorField.mpullback_add
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{V V₁ : (x : M') → TangentSpace I' x}
:
theorem
VectorField.mpullback_neg_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{x : M}
{V : (x : M') → TangentSpace I' x}
:
theorem
VectorField.mpullback_neg
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{V : (x : M') → TangentSpace I' x}
:
@[simp]
theorem
VectorField.mpullbackWithin_univ
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{V : (x : M') → TangentSpace I' x}
:
theorem
VectorField.mpullbackWithin_eq_pullbackWithin
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{f : E → E'}
{V : E' → E'}
{s : Set E}
:
mpullbackWithin (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') f V s = pullbackWithin 𝕜 f V s
theorem
VectorField.mpullback_eq_pullback
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{f : E → E'}
{V : E' → E'}
:
@[simp]
theorem
VectorField.mpullback_id
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{V : (x : M) → TangentSpace I x}
:
theorem
VectorField.mpullbackWithin_comp_of_left
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{H'' : Type u_8}
[TopologicalSpace H'']
{E'' : Type u_9}
[NormedAddCommGroup E'']
[NormedSpace 𝕜 E'']
{I'' : ModelWithCorners 𝕜 E'' H''}
{M'' : Type u_10}
[TopologicalSpace M'']
[ChartedSpace H'' M'']
{g : M' → M''}
{f : M → M'}
{V : (x : M'') → TangentSpace I'' x}
{s : Set M}
{t : Set M'}
{x₀ : M}
(hf : MDifferentiableWithinAt I I' f s x₀)
(h : Set.MapsTo f s t)
(hu : UniqueMDiffWithinAt I s x₀)
(hg' : (mfderivWithin I' I'' g t (f x₀)).IsInvertible)
:
theorem
VectorField.mpullbackWithin_comp_of_right
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{H'' : Type u_8}
[TopologicalSpace H'']
{E'' : Type u_9}
[NormedAddCommGroup E'']
[NormedSpace 𝕜 E'']
{I'' : ModelWithCorners 𝕜 E'' H''}
{M'' : Type u_10}
[TopologicalSpace M'']
[ChartedSpace H'' M'']
{g : M' → M''}
{f : M → M'}
{V : (x : M'') → TangentSpace I'' x}
{s : Set M}
{t : Set M'}
{x₀ : M}
(hg : MDifferentiableWithinAt I' I'' g t (f x₀))
(h : Set.MapsTo f s t)
(hu : UniqueMDiffWithinAt I s x₀)
(hf' : (mfderivWithin I I' f s x₀).IsInvertible)
:
Regularity of pullback of vector fields #
In this paragraph, we assume that the model space is complete, to ensure that the set of invertible linear maps is open and that inversion is a smooth map there. Otherwise, the pullback of vector fields could behave wildly, even at points where the derivative of the map is invertible.
theorem
MDifferentiableWithinAt.mpullbackWithin_vectorField_inter
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{x₀ : M}
{V : (x : M') → TangentSpace I' x}
{n : WithTop ℕ∞}
{t : Set M'}
[IsManifold I 2 M]
[IsManifold I' 2 M']
[CompleteSpace E]
(hV : MDifferentiableWithinAt I' I'.tangent (fun (y : M') => { proj := y, snd := V y }) t (f x₀))
(hf : ContMDiffWithinAt I I' n f s x₀)
(hf' : (mfderivWithin I I' f s x₀).IsInvertible)
(hx₀ : x₀ ∈ s)
(hs : UniqueMDiffOn I s)
(hmn : 2 ≤ n)
:
MDifferentiableWithinAt I I.tangent (fun (y : M) => { proj := y, snd := VectorField.mpullbackWithin I I' f V s y })
(s ∩ f ⁻¹' t) x₀
The pullback of a differentiable vector field by a C^n function with 2 ≤ n is
differentiable. Version within a set at a point.
theorem
MDifferentiableWithinAt.mpullbackWithin_vectorField_inter_of_eq
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{x₀ : M}
{V : (x : M') → TangentSpace I' x}
{n : WithTop ℕ∞}
{t : Set M'}
{y₀ : M'}
[IsManifold I 2 M]
[IsManifold I' 2 M']
[CompleteSpace E]
(hV : MDifferentiableWithinAt I' I'.tangent (fun (y : M') => { proj := y, snd := V y }) t y₀)
(hf : ContMDiffWithinAt I I' n f s x₀)
(hf' : (mfderivWithin I I' f s x₀).IsInvertible)
(hx₀ : x₀ ∈ s)
(hs : UniqueMDiffOn I s)
(hmn : 2 ≤ n)
(h : y₀ = f x₀)
:
MDifferentiableWithinAt I I.tangent (fun (y : M) => { proj := y, snd := VectorField.mpullbackWithin I I' f V s y })
(s ∩ f ⁻¹' t) x₀
theorem
MDifferentiableOn.mpullbackWithin_vectorField_inter
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{V : (x : M') → TangentSpace I' x}
{n : WithTop ℕ∞}
{t : Set M'}
[IsManifold I 2 M]
[IsManifold I' 2 M']
[CompleteSpace E]
(hV : MDifferentiableOn I' I'.tangent (fun (y : M') => { proj := y, snd := V y }) t)
(hf : ContMDiffOn I I' n f s)
(hf' : ∀ x ∈ s ∩ f ⁻¹' t, (mfderivWithin I I' f s x).IsInvertible)
(hs : UniqueMDiffOn I s)
(hmn : 2 ≤ n)
:
MDifferentiableOn I I.tangent (fun (y : M) => { proj := y, snd := VectorField.mpullbackWithin I I' f V s y })
(s ∩ f ⁻¹' t)
The pullback of a differentiable vector field by a C^n function with 2 ≤ n is
differentiable. Version on a set.
theorem
MDifferentiableWithinAt.mpullback_vectorField_preimage
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{x₀ : M}
{V : (x : M') → TangentSpace I' x}
{n : WithTop ℕ∞}
{t : Set M'}
[IsManifold I 2 M]
[IsManifold I' 2 M']
[CompleteSpace E]
(hV : MDifferentiableWithinAt I' I'.tangent (fun (y : M') => { proj := y, snd := V y }) t (f x₀))
(hf : ContMDiffAt I I' n f x₀)
(hf' : (mfderiv I I' f x₀).IsInvertible)
(hmn : 2 ≤ n)
:
MDifferentiableWithinAt I I.tangent (fun (y : M) => { proj := y, snd := VectorField.mpullback I I' f V y }) (f ⁻¹' t) x₀
The pullback of a differentiable vector field by a C^n function with 2 ≤ n is
differentiable. Version within a set at a point, but with full pullback.
theorem
MDifferentiableWithinAt.mpullback_vectorField_preimage_of_eq
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{x₀ : M}
{V : (x : M') → TangentSpace I' x}
{n : WithTop ℕ∞}
{t : Set M'}
{y₀ : M'}
[IsManifold I 2 M]
[IsManifold I' 2 M']
[CompleteSpace E]
(hV : MDifferentiableWithinAt I' I'.tangent (fun (y : M') => { proj := y, snd := V y }) t y₀)
(hf : ContMDiffAt I I' n f x₀)
(hf' : (mfderiv I I' f x₀).IsInvertible)
(hmn : 2 ≤ n)
(hy₀ : y₀ = f x₀)
:
MDifferentiableWithinAt I I.tangent (fun (y : M) => { proj := y, snd := VectorField.mpullback I I' f V y }) (f ⁻¹' t) x₀
The pullback of a differentiable vector field by a C^n function with 2 ≤ n is
differentiable. Version within a set at a point, but with full pullback.
theorem
MDifferentiableOn.mpullback_vectorField_preimage
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{V : (x : M') → TangentSpace I' x}
{n : WithTop ℕ∞}
{t : Set M'}
[IsManifold I 2 M]
[IsManifold I' 2 M']
[CompleteSpace E]
(hV : MDifferentiableOn I' I'.tangent (fun (y : M') => { proj := y, snd := V y }) t)
(hf : ContMDiff I I' n f)
(hf' : ∀ x ∈ f ⁻¹' t, (mfderiv I I' f x).IsInvertible)
(hmn : 2 ≤ n)
:
MDifferentiableOn I I.tangent (fun (y : M) => { proj := y, snd := VectorField.mpullback I I' f V y }) (f ⁻¹' t)
The pullback of a differentiable vector field by a C^n function with 2 ≤ n is
differentiable. Version on a set, but with full pullback
theorem
MDifferentiableAt.mpullback_vectorField
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{x₀ : M}
{V : (x : M') → TangentSpace I' x}
{n : WithTop ℕ∞}
[IsManifold I 2 M]
[IsManifold I' 2 M']
[CompleteSpace E]
(hV : MDifferentiableAt I' I'.tangent (fun (y : M') => { proj := y, snd := V y }) (f x₀))
(hf : ContMDiffAt I I' n f x₀)
(hf' : (mfderiv I I' f x₀).IsInvertible)
(hmn : 2 ≤ n)
:
MDifferentiableAt I I.tangent (fun (y : M) => { proj := y, snd := VectorField.mpullback I I' f V y }) x₀
The pullback of a differentiable vector field by a C^n function with 2 ≤ n is
differentiable. Version at a point.
theorem
MDifferentiable.mpullback_vectorField
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{V : (x : M') → TangentSpace I' x}
{n : WithTop ℕ∞}
[IsManifold I 2 M]
[IsManifold I' 2 M']
[CompleteSpace E]
(hV : MDifferentiable I' I'.tangent fun (y : M') => { proj := y, snd := V y })
(hf : ContMDiff I I' n f)
(hf' : ∀ (x : M), (mfderiv I I' f x).IsInvertible)
(hmn : 2 ≤ n)
:
MDifferentiable I I.tangent fun (y : M) => { proj := y, snd := VectorField.mpullback I I' f V y }
The pullback of a differentiable vector field by a C^n function with 2 ≤ n is
differentiable.
theorem
ContMDiffWithinAt.mpullbackWithin_vectorField_inter
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{x₀ : M}
{V : (x : M') → TangentSpace I' x}
{m n : WithTop ℕ∞}
{t : Set M'}
[IsManifold I n M]
[IsManifold I' n M']
[CompleteSpace E]
[IsManifold I 1 M]
[IsManifold I' 1 M']
(hV : ContMDiffWithinAt I' I'.tangent m (fun (y : M') => { proj := y, snd := V y }) t (f x₀))
(hf : ContMDiffWithinAt I I' n f s x₀)
(hf' : (mfderivWithin I I' f s x₀).IsInvertible)
(hx₀ : x₀ ∈ s)
(hs : UniqueMDiffOn I s)
(hmn : m + 1 ≤ n)
:
ContMDiffWithinAt I I.tangent m (fun (y : M) => { proj := y, snd := VectorField.mpullbackWithin I I' f V s y })
(s ∩ f ⁻¹' t) x₀
The pullback of a C^m vector field by a C^n function with invertible derivative and
m + 1 ≤ n is C^m.
Version within a set at a point.
theorem
ContMDiffWithinAt.mpullbackWithin_vectorField_inter_of_eq
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{x₀ : M}
{V : (x : M') → TangentSpace I' x}
{m n : WithTop ℕ∞}
{t : Set M'}
{y₀ : M'}
[IsManifold I n M]
[IsManifold I' n M']
[CompleteSpace E]
[IsManifold I 1 M]
[IsManifold I' 1 M']
(hV : ContMDiffWithinAt I' I'.tangent m (fun (y : M') => { proj := y, snd := V y }) t y₀)
(hf : ContMDiffWithinAt I I' n f s x₀)
(hf' : (mfderivWithin I I' f s x₀).IsInvertible)
(hx₀ : x₀ ∈ s)
(hs : UniqueMDiffOn I s)
(hmn : m + 1 ≤ n)
(h : f x₀ = y₀)
:
ContMDiffWithinAt I I.tangent m (fun (y : M) => { proj := y, snd := VectorField.mpullbackWithin I I' f V s y })
(s ∩ f ⁻¹' t) x₀
theorem
ContMDiffWithinAt.mpullbackWithin_vectorField_of_mem
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{x₀ : M}
{V : (x : M') → TangentSpace I' x}
{m n : WithTop ℕ∞}
{t : Set M'}
[IsManifold I n M]
[IsManifold I' n M']
[CompleteSpace E]
[IsManifold I 1 M]
[IsManifold I' 1 M']
(hV : ContMDiffWithinAt I' I'.tangent m (fun (y : M') => { proj := y, snd := V y }) t (f x₀))
(hf : ContMDiffWithinAt I I' n f s x₀)
(hf' : (mfderivWithin I I' f s x₀).IsInvertible)
(hx₀ : x₀ ∈ s)
(hs : UniqueMDiffOn I s)
(hmn : m + 1 ≤ n)
(hst : f ⁻¹' t ∈ nhdsWithin x₀ s)
:
ContMDiffWithinAt I I.tangent m (fun (y : M) => { proj := y, snd := VectorField.mpullbackWithin I I' f V s y }) s x₀
The pullback of a C^m vector field by a C^n function with invertible derivative and
with m + 1 ≤ n is C^m.
Version within a set at a point.
theorem
ContMDiffWithinAt.mpullbackWithin_vectorField_of_mem_of_eq
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{x₀ : M}
{V : (x : M') → TangentSpace I' x}
{m n : WithTop ℕ∞}
{t : Set M'}
{y₀ : M'}
[IsManifold I n M]
[IsManifold I' n M']
[CompleteSpace E]
[IsManifold I 1 M]
[IsManifold I' 1 M']
(hV : ContMDiffWithinAt I' I'.tangent m (fun (y : M') => { proj := y, snd := V y }) t y₀)
(hf : ContMDiffWithinAt I I' n f s x₀)
(hf' : (mfderivWithin I I' f s x₀).IsInvertible)
(hx₀ : x₀ ∈ s)
(hs : UniqueMDiffOn I s)
(hmn : m + 1 ≤ n)
(hst : f ⁻¹' t ∈ nhdsWithin x₀ s)
(hy₀ : f x₀ = y₀)
:
ContMDiffWithinAt I I.tangent m (fun (y : M) => { proj := y, snd := VectorField.mpullbackWithin I I' f V s y }) s x₀
The pullback of a C^m vector field by a C^n function with invertible derivative and
with m + 1 ≤ n is C^m.
Version within a set at a point.
theorem
ContMDiffWithinAt.mpullbackWithin_vectorField
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{x₀ : M}
{V : (x : M') → TangentSpace I' x}
{m n : WithTop ℕ∞}
{t : Set M'}
[IsManifold I n M]
[IsManifold I' n M']
[CompleteSpace E]
[IsManifold I 1 M]
[IsManifold I' 1 M']
(hV : ContMDiffWithinAt I' I'.tangent m (fun (y : M') => { proj := y, snd := V y }) t (f x₀))
(hf : ContMDiffWithinAt I I' n f s x₀)
(hf' : (mfderivWithin I I' f s x₀).IsInvertible)
(hx₀ : x₀ ∈ s)
(hs : UniqueMDiffOn I s)
(hmn : m + 1 ≤ n)
(hst : Set.MapsTo f s t)
:
ContMDiffWithinAt I I.tangent m (fun (y : M) => { proj := y, snd := VectorField.mpullbackWithin I I' f V s y }) s x₀
The pullback of a C^m vector field by a C^n function with invertible derivative and
with m + 1 ≤ n is C^m.
Version within a set at a point.
theorem
ContMDiffWithinAt.mpullbackWithin_vectorField_of_eq
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{x₀ : M}
{V : (x : M') → TangentSpace I' x}
{m n : WithTop ℕ∞}
{t : Set M'}
{y₀ : M'}
[IsManifold I n M]
[IsManifold I' n M']
[CompleteSpace E]
[IsManifold I 1 M]
[IsManifold I' 1 M']
(hV : ContMDiffWithinAt I' I'.tangent m (fun (y : M') => { proj := y, snd := V y }) t y₀)
(hf : ContMDiffWithinAt I I' n f s x₀)
(hf' : (mfderivWithin I I' f s x₀).IsInvertible)
(hx₀ : x₀ ∈ s)
(hs : UniqueMDiffOn I s)
(hmn : m + 1 ≤ n)
(hst : Set.MapsTo f s t)
(h : f x₀ = y₀)
:
ContMDiffWithinAt I I.tangent m (fun (y : M) => { proj := y, snd := VectorField.mpullbackWithin I I' f V s y }) s x₀
The pullback of a C^m vector field by a C^n function with invertible derivative and
with m + 1 ≤ n is C^m.
Version within a set at a point.
theorem
ContMDiffWithinAt.mpullbackWithin_vectorField'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{x₀ : M}
{V : (x : M') → TangentSpace I' x}
{m n : WithTop ℕ∞}
{t : Set M'}
[IsManifold I n M]
[IsManifold I' n M']
[CompleteSpace E]
[IsManifold I 1 M]
[IsManifold I' 1 M']
{u : Set M}
(hV : ContMDiffWithinAt I' I'.tangent m (fun (y : M') => { proj := y, snd := V y }) t (f x₀))
(hf : ContMDiffWithinAt I I' n f u x₀)
(hf' : (mfderivWithin I I' f u x₀).IsInvertible)
(hx₀ : x₀ ∈ s)
(hs : UniqueMDiffOn I s)
(hmn : m + 1 ≤ n)
(hst : f ⁻¹' t ∈ nhdsWithin x₀ s)
(hu : s ⊆ u)
:
ContMDiffWithinAt I I.tangent m (fun (y : M) => { proj := y, snd := VectorField.mpullbackWithin I I' f V u y }) s x₀
The pullback of a C^m vector field by a C^n function with invertible derivative and
with m + 1 ≤ n is C^m.
Version within a set at a point, with a set used for the pullback possibly larger.
theorem
ContMDiffWithinAt.mpullbackWithin_vectorField_of_eq'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{x₀ : M}
{V : (x : M') → TangentSpace I' x}
{m n : WithTop ℕ∞}
{t : Set M'}
{y₀ : M'}
[IsManifold I n M]
[IsManifold I' n M']
[CompleteSpace E]
[IsManifold I 1 M]
[IsManifold I' 1 M']
{u : Set M}
(hV : ContMDiffWithinAt I' I'.tangent m (fun (y : M') => { proj := y, snd := V y }) t y₀)
(hf : ContMDiffWithinAt I I' n f u x₀)
(hf' : (mfderivWithin I I' f u x₀).IsInvertible)
(hx₀ : x₀ ∈ s)
(hs : UniqueMDiffOn I s)
(hmn : m + 1 ≤ n)
(hst : f ⁻¹' t ∈ nhdsWithin x₀ s)
(hu : s ⊆ u)
(hy₀ : f x₀ = y₀)
:
ContMDiffWithinAt I I.tangent m (fun (y : M) => { proj := y, snd := VectorField.mpullbackWithin I I' f V u y }) s x₀
The pullback of a C^m vector field by a C^n function with invertible derivative and
with m + 1 ≤ n is C^m.
Version within a set at a point, with a set used for the pullback possibly larger.
theorem
ContMDiffOn.mpullbackWithin_vectorField_inter
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{V : (x : M') → TangentSpace I' x}
{m n : WithTop ℕ∞}
{t : Set M'}
[IsManifold I n M]
[IsManifold I' n M']
[CompleteSpace E]
[IsManifold I 1 M]
[IsManifold I' 1 M']
(hV : ContMDiffOn I' I'.tangent m (fun (y : M') => { proj := y, snd := V y }) t)
(hf : ContMDiffOn I I' n f s)
(hf' : ∀ x ∈ s ∩ f ⁻¹' t, (mfderivWithin I I' f s x).IsInvertible)
(hs : UniqueMDiffOn I s)
(hmn : m + 1 ≤ n)
:
ContMDiffOn I I.tangent m (fun (y : M) => { proj := y, snd := VectorField.mpullbackWithin I I' f V s y }) (s ∩ f ⁻¹' t)
The pullback of a C^m vector field by a C^n function with invertible derivative and
with m + 1 ≤ n is C^m.
Version on a set.
theorem
ContMDiffWithinAt.mpullback_vectorField_preimage
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{x₀ : M}
{V : (x : M') → TangentSpace I' x}
{m n : WithTop ℕ∞}
{t : Set M'}
[IsManifold I n M]
[IsManifold I' n M']
[CompleteSpace E]
[IsManifold I 1 M]
[IsManifold I' 1 M']
(hV : ContMDiffWithinAt I' I'.tangent m (fun (y : M') => { proj := y, snd := V y }) t (f x₀))
(hf : ContMDiffAt I I' n f x₀)
(hf' : (mfderiv I I' f x₀).IsInvertible)
(hmn : m + 1 ≤ n)
:
ContMDiffWithinAt I I.tangent m (fun (y : M) => { proj := y, snd := VectorField.mpullback I I' f V y }) (f ⁻¹' t) x₀
The pullback of a C^m vector field by a C^n function with invertible derivative and
with m + 1 ≤ n is C^m.
Version within a set at a point, but with full pullback.
theorem
ContMDiffWithinAt.mpullback_vectorField_preimage_of_eq
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{x₀ : M}
{V : (x : M') → TangentSpace I' x}
{m n : WithTop ℕ∞}
{t : Set M'}
{y₀ : M'}
[IsManifold I n M]
[IsManifold I' n M']
[CompleteSpace E]
[IsManifold I 1 M]
[IsManifold I' 1 M']
(hV : ContMDiffWithinAt I' I'.tangent m (fun (y : M') => { proj := y, snd := V y }) t y₀)
(hf : ContMDiffAt I I' n f x₀)
(hf' : (mfderiv I I' f x₀).IsInvertible)
(hmn : m + 1 ≤ n)
(hy₀ : y₀ = f x₀)
:
ContMDiffWithinAt I I.tangent m (fun (y : M) => { proj := y, snd := VectorField.mpullback I I' f V y }) (f ⁻¹' t) x₀
The pullback of a C^m vector field by a C^n function with invertible derivative and
with m + 1 ≤ n is C^m.
Version within a set at a point, but with full pullback.
theorem
ContMDiffWithinAt.mpullback_vectorField_of_mem_nhdsWithin
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{x₀ : M}
{V : (x : M') → TangentSpace I' x}
{m n : WithTop ℕ∞}
{t : Set M'}
[IsManifold I n M]
[IsManifold I' n M']
[CompleteSpace E]
[IsManifold I 1 M]
[IsManifold I' 1 M']
(hV : ContMDiffWithinAt I' I'.tangent m (fun (y : M') => { proj := y, snd := V y }) t (f x₀))
(hf : ContMDiffAt I I' n f x₀)
(hf' : (mfderiv I I' f x₀).IsInvertible)
(hmn : m + 1 ≤ n)
(hst : f ⁻¹' t ∈ nhdsWithin x₀ s)
:
ContMDiffWithinAt I I.tangent m (fun (y : M) => { proj := y, snd := VectorField.mpullback I I' f V y }) s x₀
The pullback of a C^m vector field by a C^n function with invertible derivative and
with m + 1 ≤ n is C^m.
Version within a set at a point, but with full pullback.
theorem
ContMDiffWithinAt.mpullback_vectorField_of_mem_nhdsWithin_of_eq
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{s : Set M}
{x₀ : M}
{V : (x : M') → TangentSpace I' x}
{m n : WithTop ℕ∞}
{t : Set M'}
{y₀ : M'}
[IsManifold I n M]
[IsManifold I' n M']
[CompleteSpace E]
[IsManifold I 1 M]
[IsManifold I' 1 M']
(hV : ContMDiffWithinAt I' I'.tangent m (fun (y : M') => { proj := y, snd := V y }) t y₀)
(hf : ContMDiffAt I I' n f x₀)
(hf' : (mfderiv I I' f x₀).IsInvertible)
(hmn : m + 1 ≤ n)
(hst : f ⁻¹' t ∈ nhdsWithin x₀ s)
(hy₀ : y₀ = f x₀)
:
ContMDiffWithinAt I I.tangent m (fun (y : M) => { proj := y, snd := VectorField.mpullback I I' f V y }) s x₀
The pullback of a C^m vector field by a C^n function with invertible derivative and
with m + 1 ≤ n is C^m.
Version within a set at a point, but with full pullback.
theorem
ContMDiffOn.mpullback_vectorField_preimage
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{V : (x : M') → TangentSpace I' x}
{m n : WithTop ℕ∞}
{t : Set M'}
[IsManifold I n M]
[IsManifold I' n M']
[CompleteSpace E]
[IsManifold I 1 M]
[IsManifold I' 1 M']
(hV : ContMDiffOn I' I'.tangent m (fun (y : M') => { proj := y, snd := V y }) t)
(hf : ContMDiff I I' n f)
(hf' : ∀ x ∈ f ⁻¹' t, (mfderiv I I' f x).IsInvertible)
(hmn : m + 1 ≤ n)
:
ContMDiffOn I I.tangent m (fun (y : M) => { proj := y, snd := VectorField.mpullback I I' f V y }) (f ⁻¹' t)
The pullback of a C^m vector field by a C^n function with invertible derivative and
with m + 1 ≤ n is C^m.
Version on a set, but with full pullback
theorem
ContMDiffAt.mpullback_vectorField_preimage
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{x₀ : M}
{V : (x : M') → TangentSpace I' x}
{m n : WithTop ℕ∞}
[IsManifold I n M]
[IsManifold I' n M']
[CompleteSpace E]
[IsManifold I 1 M]
[IsManifold I' 1 M']
(hV : ContMDiffAt I' I'.tangent m (fun (y : M') => { proj := y, snd := V y }) (f x₀))
(hf : ContMDiffAt I I' n f x₀)
(hf' : (mfderiv I I' f x₀).IsInvertible)
(hmn : m + 1 ≤ n)
:
ContMDiffAt I I.tangent m (fun (y : M) => { proj := y, snd := VectorField.mpullback I I' f V y }) x₀
The pullback of a C^m vector field by a C^n function with invertible derivative and
with m + 1 ≤ n is C^m.
Version at a point.
theorem
ContMDiff.mpullback_vectorField
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{H' : Type u_5}
[TopologicalSpace H']
{E' : Type u_6}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{f : M → M'}
{V : (x : M') → TangentSpace I' x}
{m n : WithTop ℕ∞}
[IsManifold I n M]
[IsManifold I' n M']
[CompleteSpace E]
[IsManifold I 1 M]
[IsManifold I' 1 M']
(hV : ContMDiff I' I'.tangent m fun (y : M') => { proj := y, snd := V y })
(hf : ContMDiff I I' n f)
(hf' : ∀ (x : M), (mfderiv I I' f x).IsInvertible)
(hmn : m + 1 ≤ n)
:
ContMDiff I I.tangent m fun (y : M) => { proj := y, snd := VectorField.mpullback I I' f V y }
The pullback of a C^m vector field by a C^n function with invertible derivative and
with m + 1 ≤ n is C^m.
theorem
VectorField.contMDiffWithinAt_mpullbackWithin_extChartAt_symm
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{x : M}
{m n : WithTop ℕ∞}
[IsManifold I n M]
[CompleteSpace E]
[IsManifold I 1 M]
{V : (x : M) → TangentSpace I x}
(hV : ContMDiffWithinAt I I.tangent m (fun (x : M) => { proj := x, snd := V x }) s x)
(hs : UniqueMDiffOn I s)
(hx : x ∈ s)
(hmn : m + 1 ≤ n)
:
ContMDiffWithinAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E).tangent m
(fun (y : E) =>
{ proj := y, snd := mpullbackWithin (modelWithCornersSelf 𝕜 E) I (↑(extChartAt I x).symm) V (Set.range ↑I) y })
((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) x)
theorem
VectorField.eventually_contMDiffWithinAt_mpullbackWithin_extChartAt_symm
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{x : M}
{m n : WithTop ℕ∞}
[IsManifold I n M]
[CompleteSpace E]
[IsManifold I 1 M]
{V : (x : M) → TangentSpace I x}
(hV : ContMDiffWithinAt I I.tangent m (fun (x : M) => { proj := x, snd := V x }) s x)
(hs : UniqueMDiffOn I s)
(hx : x ∈ s)
(hmn : m + 1 ≤ n)
(hm : m ≠ ↑⊤)
:
∀ᶠ (y : M) in nhdsWithin x s, ContMDiffWithinAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E).tangent m
(fun (z : E) =>
{ proj := z, snd := mpullbackWithin (modelWithCornersSelf 𝕜 E) I (↑(extChartAt I x).symm) V (Set.range ↑I) z })
((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) y)
theorem
VectorField.eventuallyEq_mpullback_mpullbackWithin_extChartAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{x : M}
[IsManifold I 1 M]
(V : (x : M) → TangentSpace I x)
:
V =ᶠ[nhdsWithin x s] mpullback I (modelWithCornersSelf 𝕜 E) (↑(extChartAt I x))
(mpullbackWithin (modelWithCornersSelf 𝕜 E) I (↑(extChartAt I x).symm) V (Set.range ↑I))
The Lie bracket of vector fields in manifolds #
def
VectorField.mlieBracketWithin
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
(I : ModelWithCorners 𝕜 E H)
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
(V W : (x : M) → TangentSpace I x)
(s : Set M)
(x₀ : M)
:
TangentSpace I x₀
The Lie bracket of two vector fields in a manifold, within a set.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
VectorField.mlieBracket
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
(I : ModelWithCorners 𝕜 E H)
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
(V W : (x : M) → TangentSpace I x)
(x₀ : M)
:
TangentSpace I x₀
The Lie bracket of two vector fields in a manifold.
Equations
- VectorField.mlieBracket I V W x₀ = VectorField.mlieBracketWithin I V W Set.univ x₀
Instances For
theorem
VectorField.mlieBracketWithin_def
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{V W : (x : M) → TangentSpace I x}
:
mlieBracketWithin I V W s = fun (x₀ : M) =>
mpullback I (modelWithCornersSelf 𝕜 E) (↑(extChartAt I x₀))
(lieBracketWithin 𝕜 (mpullbackWithin (modelWithCornersSelf 𝕜 E) I (↑(extChartAt I x₀).symm) V (Set.range ↑I))
(mpullbackWithin (modelWithCornersSelf 𝕜 E) I (↑(extChartAt I x₀).symm) W (Set.range ↑I))
(↑(extChartAt I x₀).symm ⁻¹' s ∩ Set.range ↑I))
x₀
theorem
VectorField.mlieBracketWithin_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{x₀ : M}
{V W : (x : M) → TangentSpace I x}
:
mlieBracketWithin I V W s x₀ = (mfderiv I (modelWithCornersSelf 𝕜 E) (↑(extChartAt I x₀)) x₀).inverse
(lieBracketWithin 𝕜 (mpullbackWithin (modelWithCornersSelf 𝕜 E) I (↑(extChartAt I x₀).symm) V (Set.range ↑I))
(mpullbackWithin (modelWithCornersSelf 𝕜 E) I (↑(extChartAt I x₀).symm) W (Set.range ↑I))
(↑(extChartAt I x₀).symm ⁻¹' s ∩ Set.range ↑I) (↑(extChartAt I x₀) x₀))
theorem
VectorField.mlieBracketWithin_eq_lieBracketWithin
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{V W : (x : E) → TangentSpace (modelWithCornersSelf 𝕜 E) x}
{s : Set E}
:
@[simp]
theorem
VectorField.mlieBracketWithin_univ
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{V W : (x : M) → TangentSpace I x}
:
theorem
VectorField.mlieBracketWithin_eq_zero_of_eq_zero
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{x : M}
{V W : (x : M) → TangentSpace I x}
(hV : V x = 0)
(hW : W x = 0)
:
theorem
VectorField.mlieBracketWithin_swap_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{x : M}
{V W : (x : M) → TangentSpace I x}
:
theorem
VectorField.mlieBracketWithin_swap
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{V W : (x : M) → TangentSpace I x}
:
theorem
VectorField.mlieBracket_swap_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{x : M}
{V W : (x : M) → TangentSpace I x}
:
theorem
VectorField.mlieBracket_swap
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{V W : (x : M) → TangentSpace I x}
:
@[simp]
theorem
VectorField.mlieBracketWithin_self
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{V : (x : M) → TangentSpace I x}
:
@[simp]
theorem
VectorField.mlieBracket_self
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{V : (x : M) → TangentSpace I x}
:
theorem
VectorField.mlieBracketWithin_congr_set'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s t : Set M}
{x : M}
{V W : (x : M) → TangentSpace I x}
(y : M)
(h : s =ᶠ[nhdsWithin x {y}ᶜ] t)
:
Variant of mlieBracketWithin_congr_set where one requires the sets to coincide only in
the complement of a point.
theorem
VectorField.mlieBracketWithin_congr_set
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s t : Set M}
{x : M}
{V W : (x : M) → TangentSpace I x}
(h : s =ᶠ[nhds x] t)
:
theorem
VectorField.mlieBracketWithin_inter
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s t : Set M}
{x : M}
{V W : (x : M) → TangentSpace I x}
(ht : t ∈ nhds x)
:
theorem
VectorField.mlieBracketWithin_of_mem_nhds
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{x : M}
{V W : (x : M) → TangentSpace I x}
(h : s ∈ nhds x)
:
theorem
VectorField.mlieBracketWithin_of_isOpen
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{x : M}
{V W : (x : M) → TangentSpace I x}
(hs : IsOpen s)
(hx : x ∈ s)
:
theorem
VectorField.mlieBracketWithin_eventually_congr_set'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s t : Set M}
{x : M}
{V W : (x : M) → TangentSpace I x}
(y : M)
(h : s =ᶠ[nhdsWithin x {y}ᶜ] t)
:
Variant of mlieBracketWithin_eventually_congr_set where one requires the sets to coincide only
in the complement of a point.
theorem
VectorField.mlieBracketWithin_eventually_congr_set
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s t : Set M}
{x : M}
{V W : (x : M) → TangentSpace I x}
(h : s =ᶠ[nhds x] t)
:
theorem
Filter.EventuallyEq.mlieBracketWithin_vectorField_eq
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{x : M}
{V W V₁ W₁ : (x : M) → TangentSpace I x}
(hV : V₁ =ᶠ[nhdsWithin x s] V)
(hxV : V₁ x = V x)
(hW : W₁ =ᶠ[nhdsWithin x s] W)
(hxW : W₁ x = W x)
:
theorem
Filter.EventuallyEq.mlieBracketWithin_vectorField_eq_of_mem
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{x : M}
{V W V₁ W₁ : (x : M) → TangentSpace I x}
(hV : V₁ =ᶠ[nhdsWithin x s] V)
(hW : W₁ =ᶠ[nhdsWithin x s] W)
(hx : x ∈ s)
:
theorem
Filter.EventuallyEq.mlieBracketWithin_vectorField'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s t : Set M}
{x : M}
{V W V₁ W₁ : (x : M) → TangentSpace I x}
(hV : V₁ =ᶠ[nhdsWithin x s] V)
(hW : W₁ =ᶠ[nhdsWithin x s] W)
(ht : t ⊆ s)
:
If vector fields coincide on a neighborhood of a point within a set, then the Lie brackets also coincide on a neighborhood of this point within this set. Version where one considers the Lie bracket within a subset.
theorem
Filter.EventuallyEq.mlieBracketWithin_vectorField
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{x : M}
{V W V₁ W₁ : (x : M) → TangentSpace I x}
(hV : V₁ =ᶠ[nhdsWithin x s] V)
(hW : W₁ =ᶠ[nhdsWithin x s] W)
:
theorem
Filter.EventuallyEq.mlieBracketWithin_vectorField_of_insert
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{x : M}
{V W V₁ W₁ : (x : M) → TangentSpace I x}
(hV : V₁ =ᶠ[nhdsWithin x (insert x s)] V)
(hW : W₁ =ᶠ[nhdsWithin x (insert x s)] W)
:
theorem
Filter.EventuallyEq.mlieBracketWithin_vectorField_eq_nhds
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{x : M}
{V W V₁ W₁ : (x : M) → TangentSpace I x}
(hV : V₁ =ᶠ[nhds x] V)
(hW : W₁ =ᶠ[nhds x] W)
:
theorem
VectorField.mlieBracketWithin_congr
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{x : M}
{V W V₁ W₁ : (x : M) → TangentSpace I x}
(hV : Set.EqOn V₁ V s)
(hVx : V₁ x = V x)
(hW : Set.EqOn W₁ W s)
(hWx : W₁ x = W x)
:
theorem
VectorField.mlieBracketWithin_congr'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{x : M}
{V W V₁ W₁ : (x : M) → TangentSpace I x}
(hV : Set.EqOn V₁ V s)
(hW : Set.EqOn W₁ W s)
(hx : x ∈ s)
:
Version of mlieBracketWithin_congr in which one assumes that the point belongs to the
given set.
theorem
Filter.EventuallyEq.mlieBracket_vectorField_eq
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{x : M}
{V W V₁ W₁ : (x : M) → TangentSpace I x}
(hV : V₁ =ᶠ[nhds x] V)
(hW : W₁ =ᶠ[nhds x] W)
:
theorem
Filter.EventuallyEq.mlieBracket_vectorField
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{x : M}
{V W V₁ W₁ : (x : M) → TangentSpace I x}
(hV : V₁ =ᶠ[nhds x] V)
(hW : W₁ =ᶠ[nhds x] W)
:
theorem
MDifferentiableWithinAt.differentiableWithinAt_mpullbackWithin_vectorField
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{x : M}
{V : (x : M) → TangentSpace I x}
[IsManifold I 2 M]
[CompleteSpace E]
(hV : MDifferentiableWithinAt I I.tangent (fun (x : M) => { proj := x, snd := V x }) s x)
:
DifferentiableWithinAt 𝕜
(VectorField.mpullbackWithin (modelWithCornersSelf 𝕜 E) I (↑(extChartAt I x).symm) V (Set.range ↑I))
(↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I) (↑(extChartAt I x) x)
theorem
VectorField.mlieBracketWithin_smul_left
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{x : M}
{V W : (x : M) → TangentSpace I x}
{c : 𝕜}
[IsManifold I 2 M]
[CompleteSpace E]
(hV : MDifferentiableWithinAt I I.tangent (fun (x : M) => { proj := x, snd := V x }) s x)
(hs : UniqueMDiffWithinAt I s x)
:
theorem
VectorField.mlieBracket_smul_left
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{x : M}
{V W : (x : M) → TangentSpace I x}
{c : 𝕜}
[IsManifold I 2 M]
[CompleteSpace E]
(hV : MDifferentiableAt I I.tangent (fun (x : M) => { proj := x, snd := V x }) x)
:
theorem
VectorField.mlieBracketWithin_smul_right
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{x : M}
{V W : (x : M) → TangentSpace I x}
{c : 𝕜}
[IsManifold I 2 M]
[CompleteSpace E]
(hW : MDifferentiableWithinAt I I.tangent (fun (x : M) => { proj := x, snd := W x }) s x)
(hs : UniqueMDiffWithinAt I s x)
:
theorem
VectorField.mlieBracket_smul_right
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{x : M}
{V W : (x : M) → TangentSpace I x}
{c : 𝕜}
[IsManifold I 2 M]
[CompleteSpace E]
(hW : MDifferentiableAt I I.tangent (fun (x : M) => { proj := x, snd := W x }) x)
:
theorem
VectorField.mlieBracketWithin_add_left
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{x : M}
{V W V₁ : (x : M) → TangentSpace I x}
[IsManifold I 2 M]
[CompleteSpace E]
(hV : MDifferentiableWithinAt I I.tangent (fun (x : M) => { proj := x, snd := V x }) s x)
(hV₁ : MDifferentiableWithinAt I I.tangent (fun (x : M) => { proj := x, snd := V₁ x }) s x)
(hs : UniqueMDiffWithinAt I s x)
:
theorem
VectorField.mlieBracket_add_left
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{x : M}
{V W V₁ : (x : M) → TangentSpace I x}
[IsManifold I 2 M]
[CompleteSpace E]
(hV : MDifferentiableAt I I.tangent (fun (x : M) => { proj := x, snd := V x }) x)
(hV₁ : MDifferentiableAt I I.tangent (fun (x : M) => { proj := x, snd := V₁ x }) x)
:
theorem
VectorField.mlieBracketWithin_add_right
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{x : M}
{V W W₁ : (x : M) → TangentSpace I x}
[IsManifold I 2 M]
[CompleteSpace E]
(hW : MDifferentiableWithinAt I I.tangent (fun (x : M) => { proj := x, snd := W x }) s x)
(hW₁ : MDifferentiableWithinAt I I.tangent (fun (x : M) => { proj := x, snd := W₁ x }) s x)
(hs : UniqueMDiffWithinAt I s x)
:
theorem
VectorField.mlieBracket_add_right
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{x : M}
{V W W₁ : (x : M) → TangentSpace I x}
[IsManifold I 2 M]
[CompleteSpace E]
(hW : MDifferentiableAt I I.tangent (fun (x : M) => { proj := x, snd := W x }) x)
(hW₁ : MDifferentiableAt I I.tangent (fun (x : M) => { proj := x, snd := W₁ x }) x)
:
theorem
VectorField.mlieBracketWithin_of_mem_nhdsWithin
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s t : Set M}
{x : M}
{V W : (x : M) → TangentSpace I x}
[IsManifold I 2 M]
[CompleteSpace E]
(st : t ∈ nhdsWithin x s)
(hs : UniqueMDiffWithinAt I s x)
(hV : MDifferentiableWithinAt I I.tangent (fun (x : M) => { proj := x, snd := V x }) t x)
(hW : MDifferentiableWithinAt I I.tangent (fun (x : M) => { proj := x, snd := W x }) t x)
:
theorem
VectorField.mlieBracketWithin_subset
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s t : Set M}
{x : M}
{V W : (x : M) → TangentSpace I x}
[IsManifold I 2 M]
[CompleteSpace E]
(st : s ⊆ t)
(ht : UniqueMDiffWithinAt I s x)
(hV : MDifferentiableWithinAt I I.tangent (fun (x : M) => { proj := x, snd := V x }) t x)
(hW : MDifferentiableWithinAt I I.tangent (fun (x : M) => { proj := x, snd := W x }) t x)
:
theorem
VectorField.mlieBracketWithin_eq_mlieBracket
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s : Set M}
{x : M}
{V W : (x : M) → TangentSpace I x}
[IsManifold I 2 M]
[CompleteSpace E]
(hs : UniqueMDiffWithinAt I s x)
(hV : MDifferentiableAt I I.tangent (fun (x : M) => { proj := x, snd := V x }) x)
(hW : MDifferentiableAt I I.tangent (fun (x : M) => { proj := x, snd := W x }) x)
:
theorem
DifferentiableWithinAt.mlieBracketWithin_congr_mono
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{H : Type u_2}
[TopologicalSpace H]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
[TopologicalSpace M]
[ChartedSpace H M]
{s t : Set M}
{x : M}
{V W V₁ W₁ : (x : M) → TangentSpace I x}
[IsManifold I 2 M]
[CompleteSpace E]
(hV : MDifferentiableWithinAt I I.tangent (fun (x : M) => { proj := x, snd := V x }) s x)
(hVs : Set.EqOn V₁ V t)
(hVx : V₁ x = V x)
(hW : MDifferentiableWithinAt I I.tangent (fun (x : M) => { proj := x, snd := W x }) s x)
(hWs : Set.EqOn W₁ W t)
(hWx : W₁ x = W x)
(hxt : UniqueMDiffWithinAt I t x)
(h₁ : t ⊆ s)
: