Sections of 1-jet bundles #
In this file we study sections of 1-jet bundles. This is the direct continuation
of OneJetBundle.lean but it imports more files, hence the cut.
Main definitions #
In this file we consider two manifolds M and M' with models I and I'
OneJetSet I M I' M': smooth sections ofOneJetBundle I M I' M' → M
structure
OneJetSec
{𝕜 : 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]
[IsManifold 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']
[IsManifold I' (↑⊤) M']
:
Type (max (max (max u_2 u_4) u_5) u_7)
A section of a 1-jet bundle seen as a bundle over the source manifold.
- bs : M → M'
- smooth' : ContMDiff I ((I.prod I').prod (modelWithCornersSelf 𝕜 (E →L[𝕜] E'))) ↑⊤ fun (x : M) => OneJetBundle.mk x (self.bs x) (self.ϕ x)
Instances For
theorem
OneJetSec.ext
{𝕜 : Type u_1}
{inst✝ : NontriviallyNormedField 𝕜}
{E : Type u_2}
{inst✝¹ : NormedAddCommGroup E}
{inst✝² : NormedSpace 𝕜 E}
{H : Type u_3}
{inst✝³ : TopologicalSpace H}
{I : ModelWithCorners 𝕜 E H}
{M : Type u_4}
{inst✝⁴ : TopologicalSpace M}
{inst✝⁵ : ChartedSpace H M}
{inst✝⁶ : IsManifold I (↑⊤) M}
{E' : Type u_5}
{inst✝⁷ : NormedAddCommGroup E'}
{inst✝⁸ : NormedSpace 𝕜 E'}
{H' : Type u_6}
{inst✝⁹ : TopologicalSpace H'}
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
{inst✝¹⁰ : TopologicalSpace M'}
{inst✝¹¹ : ChartedSpace H' M'}
{inst✝¹² : IsManifold I' (↑⊤) M'}
{x y : OneJetSec I M I' M'}
(bs : x.bs = y.bs)
(ϕ : x.ϕ = y.ϕ)
:
instance
instFunLikeOneJetSecOneJetBundle
{𝕜 : 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]
[IsManifold 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']
[IsManifold I' (↑⊤) M']
:
FunLike (OneJetSec I M I' M') M (OneJetBundle I M I' M')
Equations
- instFunLikeOneJetSecOneJetBundle I M I' M' = { coe := fun (S : OneJetSec I M I' M') (x : M) => OneJetBundle.mk x (S.bs x) (S.ϕ x), coe_injective' := ⋯ }
def
OneJetSec.mk'
{𝕜 : 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]
[IsManifold 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']
[IsManifold I' (↑⊤) M']
(F : M → OneJetBundle I M I' M')
(hF : ∀ (m : M), (F m).proj.1 = m)
(h2F : ContMDiff I ((I.prod I').prod (modelWithCornersSelf 𝕜 (E →L[𝕜] E'))) (↑⊤) F)
:
OneJetSec I M I' M'
Equations
- OneJetSec.mk' F hF h2F = { bs := fun (x : M) => (F x).proj.2, ϕ := fun (x : M) => (F x).snd, smooth' := ⋯ }
Instances For
theorem
OneJetSec.coe_apply
{𝕜 : 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]
[IsManifold 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']
[IsManifold I' (↑⊤) M']
(F : OneJetSec I M I' M')
(x : M)
:
theorem
OneJetSec.fst_eq
{𝕜 : 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]
[IsManifold 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']
[IsManifold I' (↑⊤) M']
(F : OneJetSec I M I' M')
(x : M)
:
theorem
OneJetSec.snd_eq
{𝕜 : 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]
[IsManifold 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']
[IsManifold I' (↑⊤) M']
(F : OneJetSec I M I' M')
(x : M)
:
theorem
OneJetSec.is_sec
{𝕜 : 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]
[IsManifold 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']
[IsManifold I' (↑⊤) M']
(F : OneJetSec I M I' M')
(x : M)
:
theorem
OneJetSec.bs_eq
{𝕜 : 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]
[IsManifold 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']
[IsManifold I' (↑⊤) M']
(F : OneJetSec I M I' M')
(x : M)
:
theorem
OneJetSec.smooth
{𝕜 : 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]
[IsManifold 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']
[IsManifold I' (↑⊤) M']
(F : OneJetSec I M I' M')
:
theorem
OneJetSec.smooth_eta
{𝕜 : 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]
[IsManifold 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']
[IsManifold I' (↑⊤) M']
(F : OneJetSec I M I' M')
:
ContMDiff I ((I.prod I').prod (modelWithCornersSelf 𝕜 (E →L[𝕜] E'))) ↑⊤ fun (x : M) =>
OneJetBundle.mk x (F.bs x) (F x).snd
theorem
OneJetSec.smooth_bs
{𝕜 : 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]
[IsManifold 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']
[IsManifold I' (↑⊤) M']
(F : OneJetSec I M I' M')
:
def
OneJetSec.IsHolonomicAt
{𝕜 : 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]
[IsManifold 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']
[IsManifold I' (↑⊤) M']
(F : OneJetSec I M I' M')
(x : M)
:
A section of J¹(M, M') is holonomic at (x : M) if its linear map part is the derivative of its base map at x.
Instances For
theorem
OneJetSec.isHolonomicAt_iff
{𝕜 : 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]
[IsManifold 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']
[IsManifold I' (↑⊤) M']
{F : OneJetSec I M I' M'}
{x : M}
:
A section of J¹(M, M') is holonomic at (x : M) iff it coincides with the 1-jet extension of its base map at x.
theorem
OneJetSec.isHolonomicAt_congr
{𝕜 : 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]
[IsManifold 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']
[IsManifold I' (↑⊤) M']
{F F' : OneJetSec I M I' M'}
{x : M}
(h : ⇑F =ᶠ[nhds x] ⇑F')
:
theorem
OneJetSec.IsHolonomicAt.congr
{𝕜 : 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]
[IsManifold 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']
[IsManifold I' (↑⊤) M']
{F F' : OneJetSec I M I' M'}
{x : M}
(hF : F.IsHolonomicAt x)
(h : ⇑F =ᶠ[nhds x] ⇑F')
:
F'.IsHolonomicAt x
def
OneJetSec.IsHolonomic
{𝕜 : 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]
[IsManifold 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']
[IsManifold I' (↑⊤) M']
(F : OneJetSec I M I' M')
:
A map from M to J¹(M, M') is holonomic if its linear map part is the derivative of its base map at every point.
Equations
- F.IsHolonomic = ∀ (x : M), F.IsHolonomicAt x
Instances For
def
IsHolonomicGerm
{𝕜 : 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']
{x : M}
(φ : (nhds x).Germ (OneJetBundle I M I' M'))
:
Equations
- IsHolonomicGerm φ = Quotient.liftOn' φ (fun (F : M → OneJetBundle I M I' M') => mfderiv I I' (fun (x' : M) => (F x').proj.2) x = (F x).snd) ⋯
Instances For
def
oneJetExtSec
{𝕜 : 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]
[IsManifold 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']
[IsManifold I' (↑⊤) M']
(f : ContMDiffMap I I' M M' ↑⊤)
:
OneJetSec I M I' M'
The one-jet extension of a function, seen as a section of the 1-jet bundle.
Equations
- oneJetExtSec f = { bs := ⇑f, ϕ := mfderiv I I' ⇑f, smooth' := ⋯ }
Instances For
structure
FamilyOneJetSec
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
(I : ModelWithCorners ℝ E H)
(M : Type u_3)
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_5}
[TopologicalSpace H']
(I' : ModelWithCorners ℝ E' H')
(M' : Type u_6)
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{F : Type u_7}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{G : Type u_8}
[TopologicalSpace G]
(J : ModelWithCorners ℝ F G)
(N : Type u_9)
[TopologicalSpace N]
[ChartedSpace G N]
:
Type (max (max (max (max u_1 u_3) u_4) u_6) u_9)
A family of jet sections indexed by manifold N is a function from N into jet sections
in such a way that the function is smooth as a function of all arguments.
- bs : N → M → M'
Instances For
theorem
FamilyOneJetSec.ext
{E : Type u_1}
{inst✝ : NormedAddCommGroup E}
{inst✝¹ : NormedSpace ℝ E}
{H : Type u_2}
{inst✝² : TopologicalSpace H}
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
{inst✝³ : TopologicalSpace M}
{inst✝⁴ : ChartedSpace H M}
{inst✝⁵ : IsManifold I (↑⊤) M}
{E' : Type u_4}
{inst✝⁶ : NormedAddCommGroup E'}
{inst✝⁷ : NormedSpace ℝ E'}
{H' : Type u_5}
{inst✝⁸ : TopologicalSpace H'}
{I' : ModelWithCorners ℝ E' H'}
{M' : Type u_6}
{inst✝⁹ : TopologicalSpace M'}
{inst✝¹⁰ : ChartedSpace H' M'}
{inst✝¹¹ : IsManifold I' (↑⊤) M'}
{F : Type u_7}
{inst✝¹² : NormedAddCommGroup F}
{inst✝¹³ : NormedSpace ℝ F}
{G : Type u_8}
{inst✝¹⁴ : TopologicalSpace G}
{J : ModelWithCorners ℝ F G}
{N : Type u_9}
{inst✝¹⁵ : TopologicalSpace N}
{inst✝¹⁶ : ChartedSpace G N}
{x y : FamilyOneJetSec I M I' M' J N}
(bs : x.bs = y.bs)
(ϕ : x.ϕ = y.ϕ)
:
instance
instFunLikeFamilyOneJetSecOneJetSecReal
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
(I : ModelWithCorners ℝ E H)
(M : Type u_3)
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_5}
[TopologicalSpace H']
(I' : ModelWithCorners ℝ E' H')
(M' : Type u_6)
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{F : Type u_7}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{G : Type u_8}
[TopologicalSpace G]
(J : ModelWithCorners ℝ F G)
(N : Type u_9)
[TopologicalSpace N]
[ChartedSpace G N]
:
FunLike (FamilyOneJetSec I M I' M' J N) N (OneJetSec I M I' M')
Equations
- instFunLikeFamilyOneJetSecOneJetSecReal I M I' M' J N = { coe := fun (S : FamilyOneJetSec I M I' M' J N) (t : N) => { bs := S.bs t, ϕ := S.ϕ t, smooth' := ⋯ }, coe_injective' := ⋯ }
def
FamilyOneJetSec.mk'
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
{M' : Type u_6}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{F : Type u_7}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{G : Type u_8}
[TopologicalSpace G]
{J : ModelWithCorners ℝ F G}
{N : Type u_9}
[TopologicalSpace N]
[ChartedSpace G N]
(FF : N → M → OneJetBundle I M I' M')
(hF : ∀ (n : N) (m : M), (FF n m).proj.1 = m)
(h2F : ContMDiff (J.prod I) ((I.prod I').prod (modelWithCornersSelf ℝ (E →L[ℝ] E'))) (↑⊤) (Function.uncurry FF))
:
FamilyOneJetSec I M I' M' J N
Equations
- FamilyOneJetSec.mk' FF hF h2F = { bs := fun (s : N) (x : M) => (FF s x).proj.2, ϕ := fun (s : N) (x : M) => (FF s x).snd, smooth' := ⋯ }
Instances For
theorem
FamilyOneJetSec.coe_mk'
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
{M' : Type u_6}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{F : Type u_7}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{G : Type u_8}
[TopologicalSpace G]
{J : ModelWithCorners ℝ F G}
{N : Type u_9}
[TopologicalSpace N]
[ChartedSpace G N]
(FF : N → M → OneJetBundle I M I' M')
(hF : ∀ (n : N) (m : M), (FF n m).proj.1 = m)
(h2F : ContMDiff (J.prod I) ((I.prod I').prod (modelWithCornersSelf ℝ (E →L[ℝ] E'))) (↑⊤) (Function.uncurry FF))
(x : N)
:
@[simp]
theorem
FamilyOneJetSec.bs_eq_coe_bs
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
{M' : Type u_6}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{F : Type u_7}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{G : Type u_8}
[TopologicalSpace G]
{J : ModelWithCorners ℝ F G}
{N : Type u_9}
[TopologicalSpace N]
[ChartedSpace G N]
(S : FamilyOneJetSec I M I' M' J N)
(s : N)
:
theorem
FamilyOneJetSec.bs_eq
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
{M' : Type u_6}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{F : Type u_7}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{G : Type u_8}
[TopologicalSpace G]
{J : ModelWithCorners ℝ F G}
{N : Type u_9}
[TopologicalSpace N]
[ChartedSpace G N]
(S : FamilyOneJetSec I M I' M' J N)
(s : N)
(x : M)
:
@[simp]
theorem
FamilyOneJetSec.coe_ϕ
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
{M' : Type u_6}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{F : Type u_7}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{G : Type u_8}
[TopologicalSpace G]
{J : ModelWithCorners ℝ F G}
{N : Type u_9}
[TopologicalSpace N]
[ChartedSpace G N]
(S : FamilyOneJetSec I M I' M' J N)
(s : N)
:
theorem
FamilyOneJetSec.smooth
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
{M' : Type u_6}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{F : Type u_7}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{G : Type u_8}
[TopologicalSpace G]
{J : ModelWithCorners ℝ F G}
{N : Type u_9}
[TopologicalSpace N]
[ChartedSpace G N]
(S : FamilyOneJetSec I M I' M' J N)
:
theorem
FamilyOneJetSec.smooth_bs
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
{M' : Type u_6}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{F : Type u_7}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{G : Type u_8}
[TopologicalSpace G]
{J : ModelWithCorners ℝ F G}
{N : Type u_9}
[TopologicalSpace N]
[ChartedSpace G N]
(S : FamilyOneJetSec I M I' M' J N)
:
theorem
FamilyOneJetSec.smooth_coe_bs
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
{M' : Type u_6}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{F : Type u_7}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{G : Type u_8}
[TopologicalSpace G]
{J : ModelWithCorners ℝ F G}
{N : Type u_9}
[TopologicalSpace N]
[ChartedSpace G N]
(S : FamilyOneJetSec I M I' M' J N)
{p : N}
:
def
FamilyOneJetSec.reindex
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
{M' : Type u_6}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{F : Type u_7}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{G : Type u_8}
[TopologicalSpace G]
{J : ModelWithCorners ℝ F G}
{N : Type u_9}
[TopologicalSpace N]
[ChartedSpace G N]
{F' : Type u_10}
[NormedAddCommGroup F']
[NormedSpace ℝ F']
{G' : Type u_11}
[TopologicalSpace G']
{J' : ModelWithCorners ℝ F' G'}
{N' : Type u_12}
[TopologicalSpace N']
[ChartedSpace G' N']
(S : FamilyOneJetSec I M I' M' J' N')
(f : ContMDiffMap J J' N N' ↑⊤)
:
FamilyOneJetSec I M I' M' J N
Reindex a family along a smooth function f.
Equations
Instances For
def
FamilyOneJetSec.uncurry
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
{M' : Type u_6}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{EP : Type u_13}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_14}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
{P : Type u_15}
[TopologicalSpace P]
[ChartedSpace HP P]
[IsManifold IP (↑⊤) P]
(S : FamilyOneJetSec I M I' M' IP P)
:
Turn a family of sections of J¹(M, M') parametrized by N into a section of J¹(N × M, M').
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
FamilyOneJetSec.uncurry_ϕ
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
{M' : Type u_6}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{EP : Type u_13}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_14}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
{P : Type u_15}
[TopologicalSpace P]
[ChartedSpace HP P]
[IsManifold IP (↑⊤) P]
(S : FamilyOneJetSec I M I' M' IP P)
(p : P × M)
:
@[simp]
theorem
FamilyOneJetSec.uncurry_bs
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
{M' : Type u_6}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{EP : Type u_13}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_14}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
{P : Type u_15}
[TopologicalSpace P]
[ChartedSpace HP P]
[IsManifold IP (↑⊤) P]
(S : FamilyOneJetSec I M I' M' IP P)
(p : P × M)
:
theorem
FamilyOneJetSec.uncurry_ϕ'
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
{M' : Type u_6}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{EP : Type u_13}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_14}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
{P : Type u_15}
[TopologicalSpace P]
[ChartedSpace HP P]
[IsManifold IP (↑⊤) P]
(S : FamilyOneJetSec I M I' M' IP P)
(p : P × M)
:
theorem
FamilyOneJetSec.isHolonomicAt_uncurry
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_5}
[TopologicalSpace H']
{I' : ModelWithCorners ℝ E' H'}
{M' : Type u_6}
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
{EP : Type u_13}
[NormedAddCommGroup EP]
[NormedSpace ℝ EP]
{HP : Type u_14}
[TopologicalSpace HP]
{IP : ModelWithCorners ℝ EP HP}
{P : Type u_15}
[TopologicalSpace P]
[ChartedSpace HP P]
[IsManifold IP (↑⊤) P]
(S : FamilyOneJetSec I M I' M' IP P)
{p : P × M}
:
@[reducible]
def
HtpyOneJetSec
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
(I : ModelWithCorners ℝ E H)
(M : Type u_3)
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I (↑⊤) M]
{E' : Type u_4}
[NormedAddCommGroup E']
[NormedSpace ℝ E']
{H' : Type u_5}
[TopologicalSpace H']
(I' : ModelWithCorners ℝ E' H')
(M' : Type u_6)
[TopologicalSpace M']
[ChartedSpace H' M']
[IsManifold I' (↑⊤) M']
:
Type (max (max (max (max u_1 u_3) u_4) u_6) 0)
A homotopy of 1-jet sections is a family of 1-jet sections indexed by ℝ
Equations
- HtpyOneJetSec I M I' M' = FamilyOneJetSec I M I' M' (modelWithCornersSelf ℝ ℝ) ℝ