First order partial differential relations for maps between manifolds

This file contains fundamental definitions about first order partial differential relations for maps between manifolds and relating them to the local story of first order partial differential relations for maps between vector spaces.

Given manifolds M and M' modelled on I and I', a first order partial differential relation for maps from M to M' is a set in the 1-jet bundle J¹(M, M'), also known as OneJetBundle I M I' M'.

Fundamental definitions

@[reducible]

def RelMfld {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] {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'] : Type (max (max (max u_6 u_4) u_3) u_1)

A first-order differential relation for maps from M to N is a subset of the 1-jet bundle.

Equations

• RelMfld I M I' M' = Set (OneJetBundle I M I' M')

structure FormalSol {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'] (R : RelMfld I M I' M') extends OneJetSec I M I' M' : Type (max (max (max u_1 u_3) u_4) u_6)

• bs : M → M'
• ϕ (x : M) : TangentSpace I x →L[ℝ] TangentSpace I' (self.bs x)
• smooth' : ContMDiff I ((I.prod I').prod (modelWithCornersSelf ℝ (E →L[ℝ] E'))) ↑⊤ fun (x : M) => OneJetBundle.mk x (self.bs x) (self.ϕ x)
• is_sol' (x : M) : self.toOneJetSec x ∈ R

theorem FormalSol.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'} {R : RelMfld I M I' M'} {x y : FormalSol R} (bs : x.bs = y.bs) (ϕ : x.ϕ = y.ϕ) : x = y

instance instFunLikeFormalSolOneJetBundleReal {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'] (R : RelMfld I M I' M') : FunLike (FormalSol R) M (OneJetBundle I M I' M')

Equations

• instFunLikeFormalSolOneJetBundleReal R = { coe := fun (F : FormalSol R) => ⇑F.toOneJetSec, coe_injective' := ⋯ }

def mkFormalSol {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'] {R : RelMfld I M I' M'} (F : M → OneJetBundle I M I' M') (hsec : ∀ (x : M), (F x).proj.1 = x) (hsol : ∀ (x : M), F x ∈ R) (hsmooth : ContMDiff I ((I.prod I').prod (modelWithCornersSelf ℝ (E →L[ℝ] E'))) (↑⊤) F) : FormalSol R

Equations

• mkFormalSol F hsec hsol hsmooth = { bs := fun (m : M) => (F m).proj.2, ϕ := fun (m : M) => (F m).snd, smooth' := ⋯, is_sol' := ⋯ }

@[simp]

theorem mkFormalSol_apply {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'] {R : RelMfld I M I' M'} (F : M → OneJetBundle I M I' M') (hsec : ∀ (x : M), (F x).proj.1 = x) (hsol : ∀ (x : M), F x ∈ R) (hsmooth : ContMDiff I ((I.prod I').prod (modelWithCornersSelf ℝ (E →L[ℝ] E'))) ↑⊤ ↿F) : ⇑(mkFormalSol F hsec hsol hsmooth) = F

@[simp]

theorem mkFormalSol_bs_apply {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'] {R : RelMfld I M I' M'} (F : M → OneJetBundle I M I' M') (hsec : ∀ (x : M), (F x).proj.1 = x) (hsol : ∀ (x : M), F x ∈ R) (hsmooth : ContMDiff I ((I.prod I').prod (modelWithCornersSelf ℝ (E →L[ℝ] E'))) ↑⊤ ↿F) (x : M) : (mkFormalSol F hsec hsol hsmooth).bs x = (F x).proj.2

@[simp]

theorem FormalSol.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'] {R : RelMfld I M I' M'} {S : OneJetSec I M I' M'} {h : ∀ (x : M), S x ∈ R} {x : M} : { toOneJetSec := S, is_sol' := h } x = S x

theorem FormalSol.coe_inj_iff {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'] {R : RelMfld I M I' M'} {S T : FormalSol R} : S = T ↔ ∀ (x : M), S x = T x

theorem FormalSol.coe_inj {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'] {R : RelMfld I M I' M'} {S T : FormalSol R} (h : ∀ (x : M), S x = T x) : S = T

@[simp]

theorem FormalSol.toOneJetSec_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'] {R : RelMfld I M I' M'} (S : FormalSol R) {x : M} : S.toOneJetSec x = S x

theorem FormalSol.is_sol {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'] {R : RelMfld I M I' M'} (F : FormalSol R) (x : M) : F x ∈ R

theorem FormalSol.coe_apply {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'] {R : RelMfld I M I' M'} (F : FormalSol R) (x : M) : F x = { proj := (x, F.bs x), snd := F.ϕ x }

theorem FormalSol.fst_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'] {R : RelMfld I M I' M'} (F : FormalSol R) (x : M) : (F x).proj = (x, F.bs x)

theorem FormalSol.snd_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'] {R : RelMfld I M I' M'} (F : FormalSol R) (x : M) : (F x).snd = F.ϕ x

theorem FormalSol.is_sec {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'] {R : RelMfld I M I' M'} (F : FormalSol R) (x : M) : (F x).proj.1 = x

theorem FormalSol.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'] {R : RelMfld I M I' M'} (F : FormalSol R) (x : M) : F.bs x = (F x).proj.2

Ampleness

instance instNormedAddCommGroupPullbackProdCoeContMDiffMapRealModelProdProdSomeENatTopSndTangentSpaceProjContinuousLinearMapIdOneJetSpace {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] {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'] (σ : OneJetBundle I M I' M') : NormedAddCommGroup ((⇑ContMDiffMap.snd *ᵖ (TangentSpace I')) σ.proj)

Equations

• instNormedAddCommGroupPullbackProdCoeContMDiffMapRealModelProdProdSomeENatTopSndTangentSpaceProjContinuousLinearMapIdOneJetSpace σ = inst✝⁴

instance instNormedSpaceRealPullbackProdCoeContMDiffMapModelProdProdSomeENatTopSndTangentSpaceProjContinuousLinearMapIdOneJetSpace {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] {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'] (σ : OneJetBundle I M I' M') : NormedSpace ℝ ((⇑ContMDiffMap.snd *ᵖ (TangentSpace I')) σ.proj)

Equations

• instNormedSpaceRealPullbackProdCoeContMDiffMapModelProdProdSomeENatTopSndTangentSpaceProjContinuousLinearMapIdOneJetSpace σ = inst✝³

instance instNormedAddCommGroupPullbackProdCoeContMDiffMapRealModelProdProdSomeENatTopSndTangentSpaceMk_sphereEversion {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] {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'] (x : M) (x' : M') : NormedAddCommGroup ((⇑ContMDiffMap.snd *ᵖ (TangentSpace I')) (x, x'))

Equations

• instNormedAddCommGroupPullbackProdCoeContMDiffMapRealModelProdProdSomeENatTopSndTangentSpaceMk_sphereEversion x x' = inst✝⁴

instance instNormedSpaceRealPullbackProdCoeContMDiffMapModelProdProdSomeENatTopSndTangentSpaceMk_sphereEversion {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] {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'] (x : M) (x' : M') : NormedSpace ℝ ((⇑ContMDiffMap.snd *ᵖ (TangentSpace I')) (x, x'))

Equations

• instNormedSpaceRealPullbackProdCoeContMDiffMapModelProdProdSomeENatTopSndTangentSpaceMk_sphereEversion x x' = inst✝³

def RelMfld.slice {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] {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'] (R : RelMfld I M I' M') (σ : OneJetBundle I M I' M') (p : DualPair (TangentSpace I σ.proj.1)) : Set (TangentSpace I' σ.proj.2)

The slice R(σ,p).

Equations

• R.slice σ p = {w : TangentSpace I' σ.proj.2 | OneJetBundle.mk σ.proj.1 σ.proj.2 (p.update σ.snd w) ∈ R}

theorem mem_slice {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] {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'] {R : RelMfld I M I' M'} {σ : OneJetBundle I M I' M'} {p : DualPair (TangentSpace I σ.proj.1)} {w : TangentSpace I' σ.proj.2} : w ∈ R.slice σ p ↔ OneJetBundle.mk σ.proj.1 σ.proj.2 (p.update σ.snd w) ∈ R

For some reason rw [mem_setOf_eq] fails after unfolding slice, but rewriting with this lemma works.

theorem slice_mk_update {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] {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'] {R : RelMfld I M I' M'} {σ : OneJetBundle I M I' M'} {p : DualPair (TangentSpace I σ.proj.1)} (x : E') : R.slice (OneJetBundle.mk σ.proj.1 σ.proj.2 (p.update σ.snd x)) p = R.slice σ p

def RelMfld.Ample {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] {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'] (R : RelMfld I M I' M') : Prop

A differential relation is ample if all its slices are ample sets.

Equations

• R.Ample = ∀ ⦃σ : OneJetBundle I M I' M'⦄ (p : DualPair (TangentSpace I σ.proj.1)), AmpleSet (R.slice σ p)

theorem RelMfld.ample_iff {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] {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'] (R : RelMfld I M I' M') : R.Ample ↔ ∀ ⦃σ : OneJetBundle I M I' M'⦄ (p : DualPair (TangentSpace I σ.proj.1)), σ ∈ R → AmpleSet (R.slice σ p)

Families of formal solutions.

structure FamilyFormalSol {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] (R : RelMfld I M I' M') extends FamilyOneJetSec I M I' M' J N : Type (max (max (max (max u_1 u_3) u_4) u_6) u_9)

A family of formal solutions indexed by manifold N is a function from N into formal solutions in such a way that the function is smooth as a function of all arguments.

• bs : N → M → M'
• ϕ (n : N) (m : M) : TangentSpace I m →L[ℝ] TangentSpace I' (self.bs n m)
• smooth' : ContMDiff (J.prod I) ((I.prod I').prod (modelWithCornersSelf ℝ (E →L[ℝ] E'))) ↑⊤ fun (p : N × M) => OneJetBundle.mk p.2 (self.bs p.1 p.2) (self.ϕ p.1 p.2)
• is_sol' (t : N) (x : M) : (self.toFamilyOneJetSec t) x ∈ R

theorem FamilyFormalSol.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} {R : RelMfld I M I' M'} {x y : FamilyFormalSol J N R} (bs : x.bs = y.bs) (ϕ : x.ϕ = y.ϕ) : x = y

instance instFunLikeFamilyFormalSolFormalSol {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] {R : RelMfld I M I' M'} : FunLike (FamilyFormalSol J N R) N (FormalSol R)

Equations

• instFunLikeFamilyFormalSolFormalSol J N = { coe := fun (S : FamilyFormalSol J N R) (n : N) => { toOneJetSec := S.toFamilyOneJetSec n, is_sol' := ⋯ }, coe_injective' := ⋯ }

@[simp]

theorem FamilyFormalSol.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] {R : RelMfld I M I' M'} {S : FamilyOneJetSec I M I' M' J N} {h : ∀ (t : N) (x : M), (S t) x ∈ R} {t : N} {x : M} : ({ toFamilyOneJetSec := S, is_sol' := h } t) x = (S t) x

theorem FamilyFormalSol.coe_mk_toOneJetSec {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] {R : RelMfld I M I' M'} {S : FamilyOneJetSec I M I' M' J N} {h : ∀ (t : N) (x : M), (S t) x ∈ R} {t : N} : ({ toFamilyOneJetSec := S, is_sol' := h } t).toOneJetSec = S t

theorem FamilyFormalSol.toFamilyOneJetSec_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] {R : RelMfld I M I' M'} (S : FamilyFormalSol J N R) {t : N} {x : M} : (S.toFamilyOneJetSec t) x = (S t) x

@[simp]

theorem FamilyFormalSol.toFamilyOneJetSec_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] {R : RelMfld I M I' M'} (S : FamilyFormalSol J N R) {t : N} : S.toFamilyOneJetSec t = (S t).toOneJetSec

theorem FamilyFormalSol.is_sol {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] {R : RelMfld I M I' M'} (S : FamilyFormalSol J N R) {t : N} {x : M} : (S t) x ∈ R

def FamilyFormalSol.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'] {R : RelMfld I M I' M'} (S : FamilyFormalSol J' N' R) (f : ContMDiffMap J J' N N' ↑⊤) : FamilyFormalSol J N R

Reindex a family along a smooth function f.

Equations

• S.reindex f = { toFamilyOneJetSec := S.reindex f, is_sol' := ⋯ }

Homotopies of formal solutions.

@[reducible, inline]

abbrev HtpyFormalSol {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'] (R : RelMfld I M I' M') : Type (max (max (max (max u_1 u_3) u_4) u_6) 0)

A homotopy of formal solutions is a family indexed by ℝ

Equations

• HtpyFormalSol R = FamilyFormalSol (modelWithCornersSelf ℝ ℝ) ℝ R

def mkHtpyFormalSol {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'] {R : RelMfld I M I' M'} (F : ℝ → M → OneJetBundle I M I' M') (hsec : ∀ (t : ℝ) (x : M), (F t x).proj.1 = x) (hsol : ∀ (t : ℝ) (x : M), F t x ∈ R) (hsmooth : ContMDiff ((modelWithCornersSelf ℝ ℝ).prod I) ((I.prod I').prod (modelWithCornersSelf ℝ (E →L[ℝ] E'))) ↑⊤ ↿F) : HtpyFormalSol R

Equations

• mkHtpyFormalSol F hsec hsol hsmooth = { bs := fun (t : ℝ) (m : M) => (F t m).proj.2, ϕ := fun (t : ℝ) (m : M) => (F t m).snd, smooth' := ⋯, is_sol' := ⋯ }

@[simp]

theorem mkHtpyFormalSol_apply {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'] {R : RelMfld I M I' M'} (F : ℝ → M → OneJetBundle I M I' M') (hsec : ∀ (t : ℝ) (x : M), (F t x).proj.1 = x) (hsol : ∀ (t : ℝ) (x : M), F t x ∈ R) (hsmooth : ContMDiff ((modelWithCornersSelf ℝ ℝ).prod I) ((I.prod I').prod (modelWithCornersSelf ℝ (E →L[ℝ] E'))) ↑⊤ ↿F) (t : ℝ) : ⇑((mkHtpyFormalSol F hsec hsol hsmooth) t) = F t

def FormalSol.constHtpy {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'] {R : RelMfld I M I' M'} (F : FormalSol R) : HtpyFormalSol R

The constant homotopy of formal solution associated to a formal solution.

Equations

• F.constHtpy = { bs := fun (x : ℝ) => F.bs, ϕ := fun (x : ℝ) => F.ϕ, smooth' := ⋯, is_sol' := ⋯ }

def emptyHtpyFormalSol {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'] (R : RelMfld I M I' M') [IsEmpty M] : HtpyFormalSol R

The empty homotopy of formal solution associated to any relation whose source manifold is empty. This is required to avoid a silly nonemptyness assumption in the main theorems.

Equations

• emptyHtpyFormalSol R = { bs := fun (_t : ℝ) (x : M) => ⋯.elim, ϕ := fun (_t : ℝ) (x : M) => ⋯.elim, smooth' := ⋯, is_sol' := ⋯ }

The h-principle

def RelMfld.SatisfiesHPrincipleWeak {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] {EX : Type u_16} [NormedAddCommGroup EX] [NormedSpace ℝ EX] {HX : Type u_17} [TopologicalSpace HX] {IX : ModelWithCorners ℝ EX HX} {X : Type u_18} [MetricSpace X] [ChartedSpace HX X] [IsManifold IX (↑⊤) X] (R : RelMfld I M IX X) (C : Set M) (ε : M → ℝ) : Prop

A relation R satisfies the (non-parametric) relative C⁰-dense h-principle w.r.t. a subset C of the domain if for every formal solution 𝓕₀ that is holonomic near C there is a homotopy between 𝓕₀ and a holonomic solution that is constant near C and ε-close to 𝓕₀. This is a temporary version with a slightly weaker conclusion. The weak version has ∀ x ∈ C, ∀ t : ℝ, 𝓕 t x = 𝓕₀ x while the strong one has ∀ᶠ x near C, ∀ t, 𝓕 t x = 𝓕₀ x. The strong version is easy to derive from the weak one if we prove the weak one for all closed sets, see RelMfld.satisfiesHPrinciple_of_weak below. The reason why the weak one is more convenient for us is we will prove the h-principle using a sequence of homotopy of formal solutions and we don't want to keep control of a fixed neighborhood of C independant from the sequence index.

Equations

• One or more equations did not get rendered due to their size.

def RelMfld.SatisfiesHPrinciple {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] {EX : Type u_16} [NormedAddCommGroup EX] [NormedSpace ℝ EX] {HX : Type u_17} [TopologicalSpace HX] {IX : ModelWithCorners ℝ EX HX} {X : Type u_18} [MetricSpace X] [ChartedSpace HX X] [IsManifold IX (↑⊤) X] (R : RelMfld I M IX X) (C : Set M) (ε : M → ℝ) : Prop

A relation R satisfies the (non-parametric) relative C⁰-dense h-principle w.r.t. a subset C of the domain if for every formal solution 𝓕₀ that is holonomic near C there is a homotopy between 𝓕₀ and a holonomic solution that is constant near C and ε-close to 𝓕₀.

Equations

• One or more equations did not get rendered due to their size.

theorem RelMfld.satisfiesHPrinciple_of_weak {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] {EX : Type u_16} [NormedAddCommGroup EX] [NormedSpace ℝ EX] {HX : Type u_17} [TopologicalSpace HX] {IX : ModelWithCorners ℝ EX HX} {X : Type u_18} [MetricSpace X] [ChartedSpace HX X] [IsManifold IX (↑⊤) X] [FiniteDimensional ℝ E] [T2Space M] [SigmaCompactSpace M] {R : RelMfld I M IX X} {ε : M → ℝ} {C : Set M} (hC : IsClosed C) (h : ∀ (A : Set M), IsClosed A → R.SatisfiesHPrincipleWeak A ε) : R.SatisfiesHPrinciple C ε

def RelMfld.SatisfiesHPrincipleWith {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] {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] {EX : Type u_16} [NormedAddCommGroup EX] [NormedSpace ℝ EX] {HX : Type u_17} [TopologicalSpace HX] {IX : ModelWithCorners ℝ EX HX} {X : Type u_18} [MetricSpace X] [ChartedSpace HX X] [IsManifold IX (↑⊤) X] (R : RelMfld I M IX X) (C : Set (P × M)) (ε : M → ℝ) : Prop

A relation R satisfies the parametric relative C⁰-dense h-principle w.r.t. manifold P, C ⊆ P × M and ε : M → ℝ if for every family of formal solutions 𝓕₀ indexed by a manifold with boundary P that is holonomic near C, there is a homotopy 𝓕 between 𝓕₀ and a holonomic solution, in such a way that 𝓕 is constant near C and ε-close to 𝓕₀.

Equations

• One or more equations did not get rendered due to their size.

theorem RelMfld.SatisfiesHPrincipleWith.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] {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] {EX : Type u_16} [NormedAddCommGroup EX] [NormedSpace ℝ EX] {HX : Type u_17} [TopologicalSpace HX] {IX : ModelWithCorners ℝ EX HX} {X : Type u_18} [MetricSpace X] [ChartedSpace HX X] [IsManifold IX (↑⊤) X] {R : RelMfld I M IX X} {C : Set (P × M)} {ε : M → ℝ} (h : SatisfiesHPrincipleWith IP R C ε) (𝓕₀ : FamilyFormalSol IP P R) (h2 : ∀ᶠ (p : P × M) in nhdsSet C, (𝓕₀ p.1).IsHolonomicAt p.2) : ∃ (f : P → M → X), ContMDiff (IP.prod I) IX (↑⊤) (Function.uncurry f) ∧ (∀ᶠ (p : P × M) in nhdsSet C, f p.1 p.2 = 𝓕₀.bs p.1 p.2) ∧ (∀ (p : P) (m : M), dist (f p m) ((𝓕₀ p).bs m) ≤ ε m) ∧ ∀ (p : P) (m : M), oneJetExt I IX (f p) m ∈ R

If a relation satisfies the parametric relative C⁰-dense h-principle wrt some data then we can forget the homotopy and get a family of solutions from every family of formal solutions.

Localisation of one jet sections

In order to use the local story of convex integration, we need a way to turn a one jet section into local ones, then apply the local story to build a homotopy of one jets section and transfer back to the original manifolds. There is a dissymetry here: we use maps from whole vector spaces to open sets in manifold.

The global manifolds are called M and N'. We don't assume the local ones are vector spaces, there are manifolds X and Y that will be vector spaces in the next section.

Transfer from J¹(X, Y) to J¹(M, N) and localized relations

def OpenSmoothEmbedding.transfer {EX : Type u_1} [NormedAddCommGroup EX] [NormedSpace ℝ EX] {HX : Type u_2} [TopologicalSpace HX] {IX : ModelWithCorners ℝ EX HX} {X : Type u_3} [TopologicalSpace X] [ChartedSpace HX X] {EM : Type u_4} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_5} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} {M : Type u_6} [TopologicalSpace M] [ChartedSpace HM M] {EY : Type u_7} [NormedAddCommGroup EY] [NormedSpace ℝ EY] {HY : Type u_8} [TopologicalSpace HY] {IY : ModelWithCorners ℝ EY HY} {Y : Type u_9} [TopologicalSpace Y] [ChartedSpace HY Y] {EN : Type u_10} [NormedAddCommGroup EN] [NormedSpace ℝ EN] {HN : Type u_11} [TopologicalSpace HN] {IN : ModelWithCorners ℝ EN HN} {N : Type u_12} [TopologicalSpace N] [ChartedSpace HN N] (φ : OpenSmoothEmbedding IX X IM M) (ψ : OpenSmoothEmbedding IY Y IN N) : OneJetBundle IX X IY Y → OneJetBundle IM M IN N

Transfer map between one jet bundles induced by open smooth embedding into the source and targets.

Equations

• φ.transfer ψ = OneJetBundle.map IY IN ↑φ ↑ψ fun (x : X) => ↑(φ.fderiv x).symm

@[simp]

theorem OpenSmoothEmbedding.transfer_proj_fst {EX : Type u_1} [NormedAddCommGroup EX] [NormedSpace ℝ EX] {HX : Type u_2} [TopologicalSpace HX] {IX : ModelWithCorners ℝ EX HX} {X : Type u_3} [TopologicalSpace X] [ChartedSpace HX X] {EM : Type u_4} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_5} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} {M : Type u_6} [TopologicalSpace M] [ChartedSpace HM M] {EY : Type u_7} [NormedAddCommGroup EY] [NormedSpace ℝ EY] {HY : Type u_8} [TopologicalSpace HY] {IY : ModelWithCorners ℝ EY HY} {Y : Type u_9} [TopologicalSpace Y] [ChartedSpace HY Y] {EN : Type u_10} [NormedAddCommGroup EN] [NormedSpace ℝ EN] {HN : Type u_11} [TopologicalSpace HN] {IN : ModelWithCorners ℝ EN HN} {N : Type u_12} [TopologicalSpace N] [ChartedSpace HN N] (φ : OpenSmoothEmbedding IX X IM M) (ψ : OpenSmoothEmbedding IY Y IN N) (a✝ : OneJetBundle IX X IY Y) : (φ.transfer ψ a✝).proj.1 = ↑φ a✝.proj.1

@[simp]

theorem OpenSmoothEmbedding.transfer_proj_snd {EX : Type u_1} [NormedAddCommGroup EX] [NormedSpace ℝ EX] {HX : Type u_2} [TopologicalSpace HX] {IX : ModelWithCorners ℝ EX HX} {X : Type u_3} [TopologicalSpace X] [ChartedSpace HX X] {EM : Type u_4} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_5} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} {M : Type u_6} [TopologicalSpace M] [ChartedSpace HM M] {EY : Type u_7} [NormedAddCommGroup EY] [NormedSpace ℝ EY] {HY : Type u_8} [TopologicalSpace HY] {IY : ModelWithCorners ℝ EY HY} {Y : Type u_9} [TopologicalSpace Y] [ChartedSpace HY Y] {EN : Type u_10} [NormedAddCommGroup EN] [NormedSpace ℝ EN] {HN : Type u_11} [TopologicalSpace HN] {IN : ModelWithCorners ℝ EN HN} {N : Type u_12} [TopologicalSpace N] [ChartedSpace HN N] (φ : OpenSmoothEmbedding IX X IM M) (ψ : OpenSmoothEmbedding IY Y IN N) (a✝ : OneJetBundle IX X IY Y) : (φ.transfer ψ a✝).proj.2 = ↑ψ a✝.proj.2

theorem OpenSmoothEmbedding.smooth_transfer {EX : Type u_1} [NormedAddCommGroup EX] [NormedSpace ℝ EX] {HX : Type u_2} [TopologicalSpace HX] {IX : ModelWithCorners ℝ EX HX} {X : Type u_3} [TopologicalSpace X] [ChartedSpace HX X] [IsManifold IX (↑⊤) X] {EM : Type u_4} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_5} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} {M : Type u_6} [TopologicalSpace M] [ChartedSpace HM M] [IsManifold IM (↑⊤) M] {EY : Type u_7} [NormedAddCommGroup EY] [NormedSpace ℝ EY] {HY : Type u_8} [TopologicalSpace HY] {IY : ModelWithCorners ℝ EY HY} {Y : Type u_9} [TopologicalSpace Y] [ChartedSpace HY Y] [IsManifold IY (↑⊤) Y] {EN : Type u_10} [NormedAddCommGroup EN] [NormedSpace ℝ EN] {HN : Type u_11} [TopologicalSpace HN] {IN : ModelWithCorners ℝ EN HN} {N : Type u_12} [TopologicalSpace N] [ChartedSpace HN N] [IsManifold IN (↑⊤) N] (φ : OpenSmoothEmbedding IX X IM M) (ψ : OpenSmoothEmbedding IY Y IN N) : ContMDiff ((IX.prod IY).prod (modelWithCornersSelf ℝ (EX →L[ℝ] EY))) ((IM.prod IN).prod (modelWithCornersSelf ℝ (EM →L[ℝ] EN))) (↑⊤) (φ.transfer ψ)

theorem OneJetBundle.continuous_transfer {EX : Type u_1} [NormedAddCommGroup EX] [NormedSpace ℝ EX] {HX : Type u_2} [TopologicalSpace HX] {IX : ModelWithCorners ℝ EX HX} {X : Type u_3} [TopologicalSpace X] [ChartedSpace HX X] [IsManifold IX (↑⊤) X] {EM : Type u_4} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_5} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} {M : Type u_6} [TopologicalSpace M] [ChartedSpace HM M] [IsManifold IM (↑⊤) M] {EY : Type u_7} [NormedAddCommGroup EY] [NormedSpace ℝ EY] {HY : Type u_8} [TopologicalSpace HY] {IY : ModelWithCorners ℝ EY HY} {Y : Type u_9} [TopologicalSpace Y] [ChartedSpace HY Y] [IsManifold IY (↑⊤) Y] {EN : Type u_10} [NormedAddCommGroup EN] [NormedSpace ℝ EN] {HN : Type u_11} [TopologicalSpace HN] {IN : ModelWithCorners ℝ EN HN} {N : Type u_12} [TopologicalSpace N] [ChartedSpace HN N] [IsManifold IN (↑⊤) N] (φ : OpenSmoothEmbedding IX X IM M) (ψ : OpenSmoothEmbedding IY Y IN N) : Continuous (φ.transfer ψ)

theorem OpenSmoothEmbedding.range_transfer {EX : Type u_1} [NormedAddCommGroup EX] [NormedSpace ℝ EX] {HX : Type u_2} [TopologicalSpace HX] {IX : ModelWithCorners ℝ EX HX} {X : Type u_3} [TopologicalSpace X] [ChartedSpace HX X] {EM : Type u_4} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_5} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} {M : Type u_6} [TopologicalSpace M] [ChartedSpace HM M] {EY : Type u_7} [NormedAddCommGroup EY] [NormedSpace ℝ EY] {HY : Type u_8} [TopologicalSpace HY] {IY : ModelWithCorners ℝ EY HY} {Y : Type u_9} [TopologicalSpace Y] [ChartedSpace HY Y] {EN : Type u_10} [NormedAddCommGroup EN] [NormedSpace ℝ EN] {HN : Type u_11} [TopologicalSpace HN] {IN : ModelWithCorners ℝ EN HN} {N : Type u_12} [TopologicalSpace N] [ChartedSpace HN N] (φ : OpenSmoothEmbedding IX X IM M) (ψ : OpenSmoothEmbedding IY Y IN N) : Set.range (φ.transfer ψ) = Bundle.TotalSpace.proj ⁻¹' Set.range ↑φ ×ˢ Set.range ↑ψ

theorem OpenSmoothEmbedding.isOpen_range_transfer {EX : Type u_1} [NormedAddCommGroup EX] [NormedSpace ℝ EX] {HX : Type u_2} [TopologicalSpace HX] {IX : ModelWithCorners ℝ EX HX} {X : Type u_3} [TopologicalSpace X] [ChartedSpace HX X] {EM : Type u_4} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_5} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} {M : Type u_6} [TopologicalSpace M] [ChartedSpace HM M] [IsManifold IM (↑⊤) M] {EY : Type u_7} [NormedAddCommGroup EY] [NormedSpace ℝ EY] {HY : Type u_8} [TopologicalSpace HY] {IY : ModelWithCorners ℝ EY HY} {Y : Type u_9} [TopologicalSpace Y] [ChartedSpace HY Y] {EN : Type u_10} [NormedAddCommGroup EN] [NormedSpace ℝ EN] {HN : Type u_11} [TopologicalSpace HN] {IN : ModelWithCorners ℝ EN HN} {N : Type u_12} [TopologicalSpace N] [ChartedSpace HN N] [IsManifold IN (↑⊤) N] (φ : OpenSmoothEmbedding IX X IM M) (ψ : OpenSmoothEmbedding IY Y IN N) : IsOpen (Set.range (φ.transfer ψ))

def RelMfld.localize {EX : Type u_1} [NormedAddCommGroup EX] [NormedSpace ℝ EX] {HX : Type u_2} [TopologicalSpace HX] {IX : ModelWithCorners ℝ EX HX} {X : Type u_3} [TopologicalSpace X] [ChartedSpace HX X] {EM : Type u_4} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_5} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} {M : Type u_6} [TopologicalSpace M] [ChartedSpace HM M] {EY : Type u_7} [NormedAddCommGroup EY] [NormedSpace ℝ EY] {HY : Type u_8} [TopologicalSpace HY] {IY : ModelWithCorners ℝ EY HY} {Y : Type u_9} [TopologicalSpace Y] [ChartedSpace HY Y] {EN : Type u_10} [NormedAddCommGroup EN] [NormedSpace ℝ EN] {HN : Type u_11} [TopologicalSpace HN] {IN : ModelWithCorners ℝ EN HN} {N : Type u_12} [TopologicalSpace N] [ChartedSpace HN N] (φ : OpenSmoothEmbedding IX X IM M) (ψ : OpenSmoothEmbedding IY Y IN N) (R : RelMfld IM M IN N) : RelMfld IX X IY Y

localize a relation

Equations

• RelMfld.localize φ ψ R = φ.transfer ψ ⁻¹' R

instance instNormedAddCommGroupTangentSpaceReal_sphereEversion {EY : Type u_7} [NormedAddCommGroup EY] [NormedSpace ℝ EY] {HY : Type u_8} [TopologicalSpace HY] {IY : ModelWithCorners ℝ EY HY} {Y : Type u_9} [TopologicalSpace Y] [ChartedSpace HY Y] (y : Y) : NormedAddCommGroup (TangentSpace IY y)

Equations

• instNormedAddCommGroupTangentSpaceReal_sphereEversion y = inst✝⁴

instance instNormedSpaceRealTangentSpace_sphereEversion {EY : Type u_7} [NormedAddCommGroup EY] [NormedSpace ℝ EY] {HY : Type u_8} [TopologicalSpace HY] {IY : ModelWithCorners ℝ EY HY} {Y : Type u_9} [TopologicalSpace Y] [ChartedSpace HY Y] (y : Y) : NormedSpace ℝ (TangentSpace IY y)

Equations

• instNormedSpaceRealTangentSpace_sphereEversion y = inst✝³

theorem RelMfld.Ample.localize {EX : Type u_1} [NormedAddCommGroup EX] [NormedSpace ℝ EX] {HX : Type u_2} [TopologicalSpace HX] {IX : ModelWithCorners ℝ EX HX} {X : Type u_3} [TopologicalSpace X] [ChartedSpace HX X] {EM : Type u_4} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_5} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} {M : Type u_6} [TopologicalSpace M] [ChartedSpace HM M] {EY : Type u_7} [NormedAddCommGroup EY] [NormedSpace ℝ EY] {HY : Type u_8} [TopologicalSpace HY] {IY : ModelWithCorners ℝ EY HY} {Y : Type u_9} [TopologicalSpace Y] [ChartedSpace HY Y] {EN : Type u_10} [NormedAddCommGroup EN] [NormedSpace ℝ EN] {HN : Type u_11} [TopologicalSpace HN] {IN : ModelWithCorners ℝ EN HN} {N : Type u_12} [TopologicalSpace N] [ChartedSpace HN N] (φ : OpenSmoothEmbedding IX X IM M) (ψ : OpenSmoothEmbedding IY Y IN N) {R : RelMfld IM M IN N} (hR : R.Ample) : (RelMfld.localize φ ψ R).Ample

Ampleness survives localization

Localized 1-jet sections

def OneJetSec.localize {EX : Type u_1} [NormedAddCommGroup EX] [NormedSpace ℝ EX] {HX : Type u_2} [TopologicalSpace HX] {IX : ModelWithCorners ℝ EX HX} {X : Type u_3} [TopologicalSpace X] [ChartedSpace HX X] [IsManifold IX (↑⊤) X] {EM : Type u_4} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_5} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} {M : Type u_6} [TopologicalSpace M] [ChartedSpace HM M] [IsManifold IM (↑⊤) M] {EY : Type u_7} [NormedAddCommGroup EY] [NormedSpace ℝ EY] {HY : Type u_8} [TopologicalSpace HY] {IY : ModelWithCorners ℝ EY HY} {Y : Type u_9} [TopologicalSpace Y] [ChartedSpace HY Y] [IsManifold IY (↑⊤) Y] {EN : Type u_10} [NormedAddCommGroup EN] [NormedSpace ℝ EN] {HN : Type u_11} [TopologicalSpace HN] {IN : ModelWithCorners ℝ EN HN} {N : Type u_12} [TopologicalSpace N] [ChartedSpace HN N] [IsManifold IN (↑⊤) N] (F : OneJetSec IM M IN N) (φ : OpenSmoothEmbedding IX X IM M) (ψ : OpenSmoothEmbedding IY Y IN N) (hF : Set.range (F.bs ∘ ↑φ) ⊆ Set.range ↑ψ) : OneJetSec IX X IY Y

Localize a one-jet section in two open embeddings. It maps x to (x, y, (D_y(g))⁻¹ ∘ F_φ(φ x) ∘ D_x(φ)) where y : M := g⁻¹(F_{bs}(φ x)).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem OneJetSec.localize_bs {EX : Type u_1} [NormedAddCommGroup EX] [NormedSpace ℝ EX] {HX : Type u_2} [TopologicalSpace HX] {IX : ModelWithCorners ℝ EX HX} {X : Type u_3} [TopologicalSpace X] [ChartedSpace HX X] [IsManifold IX (↑⊤) X] {EM : Type u_4} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_5} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} {M : Type u_6} [TopologicalSpace M] [ChartedSpace HM M] [IsManifold IM (↑⊤) M] {EY : Type u_7} [NormedAddCommGroup EY] [NormedSpace ℝ EY] {HY : Type u_8} [TopologicalSpace HY] {IY : ModelWithCorners ℝ EY HY} {Y : Type u_9} [TopologicalSpace Y] [ChartedSpace HY Y] [IsManifold IY (↑⊤) Y] {EN : Type u_10} [NormedAddCommGroup EN] [NormedSpace ℝ EN] {HN : Type u_11} [TopologicalSpace HN] {IN : ModelWithCorners ℝ EN HN} {N : Type u_12} [TopologicalSpace N] [ChartedSpace HN N] [IsManifold IN (↑⊤) N] (F : OneJetSec IM M IN N) (φ : OpenSmoothEmbedding IX X IM M) (ψ : OpenSmoothEmbedding IY Y IN N) (hF : Set.range (F.bs ∘ ↑φ) ⊆ Set.range ↑ψ) (x : X) : (F.localize φ ψ hF).bs x = ψ.invFun (F.bs (↑φ x))

@[simp]

theorem OneJetSec.localize_ϕ {EX : Type u_1} [NormedAddCommGroup EX] [NormedSpace ℝ EX] {HX : Type u_2} [TopologicalSpace HX] {IX : ModelWithCorners ℝ EX HX} {X : Type u_3} [TopologicalSpace X] [ChartedSpace HX X] [IsManifold IX (↑⊤) X] {EM : Type u_4} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_5} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} {M : Type u_6} [TopologicalSpace M] [ChartedSpace HM M] [IsManifold IM (↑⊤) M] {EY : Type u_7} [NormedAddCommGroup EY] [NormedSpace ℝ EY] {HY : Type u_8} [TopologicalSpace HY] {IY : ModelWithCorners ℝ EY HY} {Y : Type u_9} [TopologicalSpace Y] [ChartedSpace HY Y] [IsManifold IY (↑⊤) Y] {EN : Type u_10} [NormedAddCommGroup EN] [NormedSpace ℝ EN] {HN : Type u_11} [TopologicalSpace HN] {IN : ModelWithCorners ℝ EN HN} {N : Type u_12} [TopologicalSpace N] [ChartedSpace HN N] [IsManifold IN (↑⊤) N] (F : OneJetSec IM M IN N) (φ : OpenSmoothEmbedding IX X IM M) (ψ : OpenSmoothEmbedding IY Y IN N) (hF : Set.range (F.bs ∘ ↑φ) ⊆ Set.range ↑ψ) (x : X) : (F.localize φ ψ hF).ϕ x = let y := ψ.invFun (F.bs (↑φ x)); (↑(ψ.fderiv y).symm).comp (ContinuousLinearMap.comp (F (↑φ x)).snd ↑(φ.fderiv x))

theorem transfer_localize {EX : Type u_1} [NormedAddCommGroup EX] [NormedSpace ℝ EX] {HX : Type u_2} [TopologicalSpace HX] {IX : ModelWithCorners ℝ EX HX} {X : Type u_3} [TopologicalSpace X] [ChartedSpace HX X] [IsManifold IX (↑⊤) X] {EM : Type u_4} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_5} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} {M : Type u_6} [TopologicalSpace M] [ChartedSpace HM M] [IsManifold IM (↑⊤) M] {EY : Type u_7} [NormedAddCommGroup EY] [NormedSpace ℝ EY] {HY : Type u_8} [TopologicalSpace HY] {IY : ModelWithCorners ℝ EY HY} {Y : Type u_9} [TopologicalSpace Y] [ChartedSpace HY Y] [IsManifold IY (↑⊤) Y] {EN : Type u_10} [NormedAddCommGroup EN] [NormedSpace ℝ EN] {HN : Type u_11} [TopologicalSpace HN] {IN : ModelWithCorners ℝ EN HN} {N : Type u_12} [TopologicalSpace N] [ChartedSpace HN N] [IsManifold IN (↑⊤) N] (F : OneJetSec IM M IN N) (φ : OpenSmoothEmbedding IX X IM M) (ψ : OpenSmoothEmbedding IY Y IN N) (hF : Set.range (F.bs ∘ ↑φ) ⊆ Set.range ↑ψ) (x : X) : φ.transfer ψ ((F.localize φ ψ hF) x) = F (↑φ x)

theorem OneJetSec.localize_bs_fun {EX : Type u_1} [NormedAddCommGroup EX] [NormedSpace ℝ EX] {HX : Type u_2} [TopologicalSpace HX] {IX : ModelWithCorners ℝ EX HX} {X : Type u_3} [TopologicalSpace X] [ChartedSpace HX X] [IsManifold IX (↑⊤) X] {EM : Type u_4} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_5} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} {M : Type u_6} [TopologicalSpace M] [ChartedSpace HM M] [IsManifold IM (↑⊤) M] {EY : Type u_7} [NormedAddCommGroup EY] [NormedSpace ℝ EY] {HY : Type u_8} [TopologicalSpace HY] {IY : ModelWithCorners ℝ EY HY} {Y : Type u_9} [TopologicalSpace Y] [ChartedSpace HY Y] [IsManifold IY (↑⊤) Y] {EN : Type u_10} [NormedAddCommGroup EN] [NormedSpace ℝ EN] {HN : Type u_11} [TopologicalSpace HN] {IN : ModelWithCorners ℝ EN HN} {N : Type u_12} [TopologicalSpace N] [ChartedSpace HN N] [IsManifold IN (↑⊤) N] (F : OneJetSec IM M IN N) (φ : OpenSmoothEmbedding IX X IM M) (ψ : OpenSmoothEmbedding IY Y IN N) (hF : Set.range (F.bs ∘ ↑φ) ⊆ Set.range ↑ψ) : (F.localize φ ψ hF).bs = ψ.invFun ∘ F.bs ∘ ↑φ

theorem OneJetSec.localize_mem_iff {EX : Type u_1} [NormedAddCommGroup EX] [NormedSpace ℝ EX] {HX : Type u_2} [TopologicalSpace HX] {IX : ModelWithCorners ℝ EX HX} {X : Type u_3} [TopologicalSpace X] [ChartedSpace HX X] [IsManifold IX (↑⊤) X] {EM : Type u_4} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_5} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} {M : Type u_6} [TopologicalSpace M] [ChartedSpace HM M] [IsManifold IM (↑⊤) M] {EY : Type u_7} [NormedAddCommGroup EY] [NormedSpace ℝ EY] {HY : Type u_8} [TopologicalSpace HY] {IY : ModelWithCorners ℝ EY HY} {Y : Type u_9} [TopologicalSpace Y] [ChartedSpace HY Y] [IsManifold IY (↑⊤) Y] {EN : Type u_10} [NormedAddCommGroup EN] [NormedSpace ℝ EN] {HN : Type u_11} [TopologicalSpace HN] {IN : ModelWithCorners ℝ EN HN} {N : Type u_12} [TopologicalSpace N] [ChartedSpace HN N] [IsManifold IN (↑⊤) N] (F : OneJetSec IM M IN N) (φ : OpenSmoothEmbedding IX X IM M) (ψ : OpenSmoothEmbedding IY Y IN N) {R : RelMfld IM M IN N} (hF : Set.range (F.bs ∘ ↑φ) ⊆ Set.range ↑ψ) {x : X} : (F.localize φ ψ hF) x ∈ RelMfld.localize φ ψ R ↔ F (↑φ x) ∈ R

theorem isHolonomicAt_localize_iff {EX : Type u_1} [NormedAddCommGroup EX] [NormedSpace ℝ EX] {HX : Type u_2} [TopologicalSpace HX] {IX : ModelWithCorners ℝ EX HX} {X : Type u_3} [TopologicalSpace X] [ChartedSpace HX X] [IsManifold IX (↑⊤) X] {EM : Type u_4} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_5} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} {M : Type u_6} [TopologicalSpace M] [ChartedSpace HM M] [IsManifold IM (↑⊤) M] {EY : Type u_7} [NormedAddCommGroup EY] [NormedSpace ℝ EY] {HY : Type u_8} [TopologicalSpace HY] {IY : ModelWithCorners ℝ EY HY} {Y : Type u_9} [TopologicalSpace Y] [ChartedSpace HY Y] [IsManifold IY (↑⊤) Y] {EN : Type u_10} [NormedAddCommGroup EN] [NormedSpace ℝ EN] {HN : Type u_11} [TopologicalSpace HN] {IN : ModelWithCorners ℝ EN HN} {N : Type u_12} [TopologicalSpace N] [ChartedSpace HN N] [IsManifold IN (↑⊤) N] (F : OneJetSec IM M IN N) (φ : OpenSmoothEmbedding IX X IM M) (ψ : OpenSmoothEmbedding IY Y IN N) (hF : Set.range (F.bs ∘ ↑φ) ⊆ Set.range ↑ψ) (x : X) : (F.localize φ ψ hF).IsHolonomicAt x ↔ F.IsHolonomicAt (↑φ x)

From embeddings X ↪ M and Y ↪ N to J¹(X, Y) ↪ J¹(M, N)

def OneJetBundle.embedding {EX : Type u_1} [NormedAddCommGroup EX] [NormedSpace ℝ EX] {HX : Type u_2} [TopologicalSpace HX] {IX : ModelWithCorners ℝ EX HX} {X : Type u_3} [TopologicalSpace X] [ChartedSpace HX X] [IsManifold IX (↑⊤) X] {EM : Type u_4} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_5} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} {M : Type u_6} [TopologicalSpace M] [ChartedSpace HM M] [IsManifold IM (↑⊤) M] {EY : Type u_7} [NormedAddCommGroup EY] [NormedSpace ℝ EY] {HY : Type u_8} [TopologicalSpace HY] {IY : ModelWithCorners ℝ EY HY} {Y : Type u_9} [TopologicalSpace Y] [ChartedSpace HY Y] [IsManifold IY (↑⊤) Y] {EN : Type u_10} [NormedAddCommGroup EN] [NormedSpace ℝ EN] {HN : Type u_11} [TopologicalSpace HN] {IN : ModelWithCorners ℝ EN HN} {N : Type u_12} [TopologicalSpace N] [ChartedSpace HN N] [IsManifold IN (↑⊤) N] (φ : OpenSmoothEmbedding IX X IM M) (ψ : OpenSmoothEmbedding IY Y IN N) : OpenSmoothEmbedding ((IX.prod IY).prod (modelWithCornersSelf ℝ (EX →L[ℝ] EY))) (OneJetBundle IX X IY Y) ((IM.prod IN).prod (modelWithCornersSelf ℝ (EM →L[ℝ] EN))) (OneJetBundle IM M IN N)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem OneJetBundle.embedding_toFun {EX : Type u_1} [NormedAddCommGroup EX] [NormedSpace ℝ EX] {HX : Type u_2} [TopologicalSpace HX] {IX : ModelWithCorners ℝ EX HX} {X : Type u_3} [TopologicalSpace X] [ChartedSpace HX X] [IsManifold IX (↑⊤) X] {EM : Type u_4} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_5} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} {M : Type u_6} [TopologicalSpace M] [ChartedSpace HM M] [IsManifold IM (↑⊤) M] {EY : Type u_7} [NormedAddCommGroup EY] [NormedSpace ℝ EY] {HY : Type u_8} [TopologicalSpace HY] {IY : ModelWithCorners ℝ EY HY} {Y : Type u_9} [TopologicalSpace Y] [ChartedSpace HY Y] [IsManifold IY (↑⊤) Y] {EN : Type u_10} [NormedAddCommGroup EN] [NormedSpace ℝ EN] {HN : Type u_11} [TopologicalSpace HN] {IN : ModelWithCorners ℝ EN HN} {N : Type u_12} [TopologicalSpace N] [ChartedSpace HN N] [IsManifold IN (↑⊤) N] (φ : OpenSmoothEmbedding IX X IM M) (ψ : OpenSmoothEmbedding IY Y IN N) (a✝ : OneJetBundle IX X IY Y) : ↑(embedding φ ψ) a✝ = φ.transfer ψ a✝

@[simp]

theorem OneJetBundle.embedding_invFun {EX : Type u_1} [NormedAddCommGroup EX] [NormedSpace ℝ EX] {HX : Type u_2} [TopologicalSpace HX] {IX : ModelWithCorners ℝ EX HX} {X : Type u_3} [TopologicalSpace X] [ChartedSpace HX X] [IsManifold IX (↑⊤) X] {EM : Type u_4} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_5} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} {M : Type u_6} [TopologicalSpace M] [ChartedSpace HM M] [IsManifold IM (↑⊤) M] {EY : Type u_7} [NormedAddCommGroup EY] [NormedSpace ℝ EY] {HY : Type u_8} [TopologicalSpace HY] {IY : ModelWithCorners ℝ EY HY} {Y : Type u_9} [TopologicalSpace Y] [ChartedSpace HY Y] [IsManifold IY (↑⊤) Y] {EN : Type u_10} [NormedAddCommGroup EN] [NormedSpace ℝ EN] {HN : Type u_11} [TopologicalSpace HN] {IN : ModelWithCorners ℝ EN HN} {N : Type u_12} [TopologicalSpace N] [ChartedSpace HN N] [IsManifold IN (↑⊤) N] (φ : OpenSmoothEmbedding IX X IM M) (ψ : OpenSmoothEmbedding IY Y IN N) (a✝ : OneJetBundle IM M IN N) : (embedding φ ψ).invFun a✝ = OneJetBundle.map IN IY φ.invFun ψ.invFun (fun (x : M) => ↑(φ.fderiv (φ.invFun x))) a✝

Updating 1-jet sections and formal solutions

theorem OpenSmoothEmbedding.Jupdate_aux {EX : Type u_1} [NormedAddCommGroup EX] [NormedSpace ℝ EX] {HX : Type u_2} [TopologicalSpace HX] {IX : ModelWithCorners ℝ EX HX} {X : Type u_3} [TopologicalSpace X] [ChartedSpace HX X] [IsManifold IX (↑⊤) X] {EM : Type u_4} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_5} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} {M : Type u_6} [TopologicalSpace M] [ChartedSpace HM M] [IsManifold IM (↑⊤) M] {EY : Type u_7} [NormedAddCommGroup EY] [NormedSpace ℝ EY] {HY : Type u_8} [TopologicalSpace HY] {IY : ModelWithCorners ℝ EY HY} {Y : Type u_9} [TopologicalSpace Y] [ChartedSpace HY Y] [IsManifold IY (↑⊤) Y] {EN : Type u_10} [NormedAddCommGroup EN] [NormedSpace ℝ EN] {HN : Type u_11} [TopologicalSpace HN] {IN : ModelWithCorners ℝ EN HN} {N : Type u_12} [TopologicalSpace N] [ChartedSpace HN N] [IsManifold IN (↑⊤) N] (φ : OpenSmoothEmbedding IX X IM M) (ψ : OpenSmoothEmbedding IY Y IN N) (F : OneJetSec IM M IN N) (G : OneJetSec IX X IY Y) (m : M) : (φ.update (OneJetBundle.embedding φ ψ) (⇑F) (⇑G) m).proj.1 = m

def OpenSmoothEmbedding.Jupdate {EX : Type u_1} [NormedAddCommGroup EX] [NormedSpace ℝ EX] {HX : Type u_2} [TopologicalSpace HX] {IX : ModelWithCorners ℝ EX HX} {X : Type u_3} [TopologicalSpace X] [ChartedSpace HX X] [IsManifold IX (↑⊤) X] {EM : Type u_4} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_5} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} {M : Type u_6} [TopologicalSpace M] [ChartedSpace HM M] [IsManifold IM (↑⊤) M] {EY : Type u_7} [NormedAddCommGroup EY] [NormedSpace ℝ EY] {HY : Type u_8} [TopologicalSpace HY] {IY : ModelWithCorners ℝ EY HY} {Y : Type u_9} [TopologicalSpace Y] [ChartedSpace HY Y] [IsManifold IY (↑⊤) Y] {EN : Type u_10} [NormedAddCommGroup EN] [NormedSpace ℝ EN] {HN : Type u_11} [TopologicalSpace HN] {IN : ModelWithCorners ℝ EN HN} {N : Type u_12} [TopologicalSpace N] [ChartedSpace HN N] [IsManifold IN (↑⊤) N] (φ : OpenSmoothEmbedding IX X IM M) (ψ : OpenSmoothEmbedding IY Y IN N) {K : Set X} [T2Space M] (F : OneJetSec IM M IN N) (G : HtpyOneJetSec IX X IY Y) (hK : IsCompact K) (hFG : ∀ (t : ℝ), ∀ x ∉ K, F (↑φ x) = ↑(OneJetBundle.embedding φ ψ) ((G t) x)) : HtpyOneJetSec IM M IN N

Update a global homotopy of 1-jet-sections F using a local one G.

Equations

• φ.Jupdate ψ F G hK hFG = FamilyOneJetSec.mk' (fun (t : ℝ) => φ.update (OneJetBundle.embedding φ ψ) ⇑F ⇑(G t)) ⋯ ⋯

theorem OpenSmoothEmbedding.Jupdate_apply {EX : Type u_1} [NormedAddCommGroup EX] [NormedSpace ℝ EX] {HX : Type u_2} [TopologicalSpace HX] {IX : ModelWithCorners ℝ EX HX} {X : Type u_3} [TopologicalSpace X] [ChartedSpace HX X] [IsManifold IX (↑⊤) X] {EM : Type u_4} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_5} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} {M : Type u_6} [TopologicalSpace M] [ChartedSpace HM M] [IsManifold IM (↑⊤) M] {EY : Type u_7} [NormedAddCommGroup EY] [NormedSpace ℝ EY] {HY : Type u_8} [TopologicalSpace HY] {IY : ModelWithCorners ℝ EY HY} {Y : Type u_9} [TopologicalSpace Y] [ChartedSpace HY Y] [IsManifold IY (↑⊤) Y] {EN : Type u_10} [NormedAddCommGroup EN] [NormedSpace ℝ EN] {HN : Type u_11} [TopologicalSpace HN] {IN : ModelWithCorners ℝ EN HN} {N : Type u_12} [TopologicalSpace N] [ChartedSpace HN N] [IsManifold IN (↑⊤) N] (φ : OpenSmoothEmbedding IX X IM M) (ψ : OpenSmoothEmbedding IY Y IN N) {K : Set X} [T2Space M] {F : OneJetSec IM M IN N} {G : HtpyOneJetSec IX X IY Y} (hK : IsCompact K) (hFG : ∀ (t : ℝ), ∀ x ∉ K, F (↑φ x) = ↑(OneJetBundle.embedding φ ψ) ((G t) x)) (t : ℝ) (m : M) : ((φ.Jupdate ψ F G hK hFG) t) m = φ.update (OneJetBundle.embedding φ ψ) (⇑F) (⇑(G t)) m

theorem OpenSmoothEmbedding.Jupdate_bs {EX : Type u_1} [NormedAddCommGroup EX] [NormedSpace ℝ EX] {HX : Type u_2} [TopologicalSpace HX] {IX : ModelWithCorners ℝ EX HX} {X : Type u_3} [TopologicalSpace X] [ChartedSpace HX X] [IsManifold IX (↑⊤) X] {EM : Type u_4} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_5} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} {M : Type u_6} [TopologicalSpace M] [ChartedSpace HM M] [IsManifold IM (↑⊤) M] {EY : Type u_7} [NormedAddCommGroup EY] [NormedSpace ℝ EY] {HY : Type u_8} [TopologicalSpace HY] {IY : ModelWithCorners ℝ EY HY} {Y : Type u_9} [TopologicalSpace Y] [ChartedSpace HY Y] [IsManifold IY (↑⊤) Y] {EN : Type u_10} [NormedAddCommGroup EN] [NormedSpace ℝ EN] {HN : Type u_11} [TopologicalSpace HN] {IN : ModelWithCorners ℝ EN HN} {N : Type u_12} [TopologicalSpace N] [ChartedSpace HN N] [IsManifold IN (↑⊤) N] (φ : OpenSmoothEmbedding IX X IM M) (ψ : OpenSmoothEmbedding IY Y IN N) {K : Set X} [T2Space M] (F : OneJetSec IM M IN N) (G : HtpyOneJetSec IX X IY Y) (t : ℝ) (hK : IsCompact K) (hFG : ∀ (t : ℝ), ∀ x ∉ K, F (↑φ x) = ↑(OneJetBundle.embedding φ ψ) ((G t) x)) : ((φ.Jupdate ψ F G hK hFG) t).bs = φ.update ψ F.bs (G t).bs

theorem OpenSmoothEmbedding.Jupdate_localize {EX : Type u_1} [NormedAddCommGroup EX] [NormedSpace ℝ EX] {HX : Type u_2} [TopologicalSpace HX] {IX : ModelWithCorners ℝ EX HX} {X : Type u_3} [TopologicalSpace X] [ChartedSpace HX X] [IsManifold IX (↑⊤) X] {EM : Type u_4} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_5} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} {M : Type u_6} [TopologicalSpace M] [ChartedSpace HM M] [IsManifold IM (↑⊤) M] {EY : Type u_7} [NormedAddCommGroup EY] [NormedSpace ℝ EY] {HY : Type u_8} [TopologicalSpace HY] {IY : ModelWithCorners ℝ EY HY} {Y : Type u_9} [TopologicalSpace Y] [ChartedSpace HY Y] [IsManifold IY (↑⊤) Y] {EN : Type u_10} [NormedAddCommGroup EN] [NormedSpace ℝ EN] {HN : Type u_11} [TopologicalSpace HN] {IN : ModelWithCorners ℝ EN HN} {N : Type u_12} [TopologicalSpace N] [ChartedSpace HN N] [IsManifold IN (↑⊤) N] (φ : OpenSmoothEmbedding IX X IM M) (ψ : OpenSmoothEmbedding IY Y IN N) {K : Set X} [T2Space M] {F : OneJetSec IM M IN N} {G : HtpyOneJetSec IX X IY Y} (hK : IsCompact K) (hFG : ∀ (t : ℝ), ∀ x ∉ K, F (↑φ x) = ↑(OneJetBundle.embedding φ ψ) ((G t) x)) (t : ℝ) (rg : Set.range (((φ.Jupdate ψ F G hK hFG) t).bs ∘ ↑φ) ⊆ Set.range ↑ψ) (x : X) : (((φ.Jupdate ψ F G hK hFG) t).localize φ ψ rg) x = (G t) x

def OpenSmoothEmbedding.updateFormalSol {EX : Type u_1} [NormedAddCommGroup EX] [NormedSpace ℝ EX] {HX : Type u_2} [TopologicalSpace HX] {IX : ModelWithCorners ℝ EX HX} {X : Type u_3} [TopologicalSpace X] [ChartedSpace HX X] [IsManifold IX (↑⊤) X] {EM : Type u_4} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_5} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} {M : Type u_6} [TopologicalSpace M] [ChartedSpace HM M] [IsManifold IM (↑⊤) M] {EY : Type u_7} [NormedAddCommGroup EY] [NormedSpace ℝ EY] {HY : Type u_8} [TopologicalSpace HY] {IY : ModelWithCorners ℝ EY HY} {Y : Type u_9} [TopologicalSpace Y] [ChartedSpace HY Y] [IsManifold IY (↑⊤) Y] {EN : Type u_10} [NormedAddCommGroup EN] [NormedSpace ℝ EN] {HN : Type u_11} [TopologicalSpace HN] {IN : ModelWithCorners ℝ EN HN} {N : Type u_12} [TopologicalSpace N] [ChartedSpace HN N] [IsManifold IN (↑⊤) N] (φ : OpenSmoothEmbedding IX X IM M) (ψ : OpenSmoothEmbedding IY Y IN N) {R : RelMfld IM M IN N} {K : Set X} [T2Space M] (F : FormalSol R) (G : HtpyFormalSol (RelMfld.localize φ ψ R)) (hK : IsCompact K) (hFG : ∀ (t : ℝ), ∀ x ∉ K, F (↑φ x) = ↑(OneJetBundle.embedding φ ψ) ((G t) x)) : HtpyFormalSol R

Update a global formal solutions F using a homotopy of local ones G.

Equations

• φ.updateFormalSol ψ F G hK hFG = { toFamilyOneJetSec := φ.Jupdate ψ F.toOneJetSec G.toFamilyOneJetSec hK hFG, is_sol' := ⋯ }

theorem OpenSmoothEmbedding.updateFormalSol_apply {EX : Type u_1} [NormedAddCommGroup EX] [NormedSpace ℝ EX] {HX : Type u_2} [TopologicalSpace HX] {IX : ModelWithCorners ℝ EX HX} {X : Type u_3} [TopologicalSpace X] [ChartedSpace HX X] [IsManifold IX (↑⊤) X] {EM : Type u_4} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_5} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} {M : Type u_6} [TopologicalSpace M] [ChartedSpace HM M] [IsManifold IM (↑⊤) M] {EY : Type u_7} [NormedAddCommGroup EY] [NormedSpace ℝ EY] {HY : Type u_8} [TopologicalSpace HY] {IY : ModelWithCorners ℝ EY HY} {Y : Type u_9} [TopologicalSpace Y] [ChartedSpace HY Y] [IsManifold IY (↑⊤) Y] {EN : Type u_10} [NormedAddCommGroup EN] [NormedSpace ℝ EN] {HN : Type u_11} [TopologicalSpace HN] {IN : ModelWithCorners ℝ EN HN} {N : Type u_12} [TopologicalSpace N] [ChartedSpace HN N] [IsManifold IN (↑⊤) N] (φ : OpenSmoothEmbedding IX X IM M) (ψ : OpenSmoothEmbedding IY Y IN N) {R : RelMfld IM M IN N} {K : Set X} [T2Space M] {F : FormalSol R} {G : HtpyFormalSol (RelMfld.localize φ ψ R)} (hK : IsCompact K) (hFG : ∀ (t : ℝ), ∀ x ∉ K, F (↑φ x) = ↑(OneJetBundle.embedding φ ψ) ((G t) x)) (t : ℝ) (x : M) : ((φ.updateFormalSol ψ F G hK hFG) t) x = { proj := (x, (φ.update (OneJetBundle.embedding φ ψ) (⇑F) (⇑(G t)) x).proj.2), snd := (φ.update (OneJetBundle.embedding φ ψ) (⇑F) (⇑(G t)) x).snd }

theorem OpenSmoothEmbedding.updateFormalSol_bs' {EX : Type u_1} [NormedAddCommGroup EX] [NormedSpace ℝ EX] {HX : Type u_2} [TopologicalSpace HX] {IX : ModelWithCorners ℝ EX HX} {X : Type u_3} [TopologicalSpace X] [ChartedSpace HX X] [IsManifold IX (↑⊤) X] {EM : Type u_4} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_5} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} {M : Type u_6} [TopologicalSpace M] [ChartedSpace HM M] [IsManifold IM (↑⊤) M] {EY : Type u_7} [NormedAddCommGroup EY] [NormedSpace ℝ EY] {HY : Type u_8} [TopologicalSpace HY] {IY : ModelWithCorners ℝ EY HY} {Y : Type u_9} [TopologicalSpace Y] [ChartedSpace HY Y] [IsManifold IY (↑⊤) Y] {EN : Type u_10} [NormedAddCommGroup EN] [NormedSpace ℝ EN] {HN : Type u_11} [TopologicalSpace HN] {IN : ModelWithCorners ℝ EN HN} {N : Type u_12} [TopologicalSpace N] [ChartedSpace HN N] [IsManifold IN (↑⊤) N] (φ : OpenSmoothEmbedding IX X IM M) (ψ : OpenSmoothEmbedding IY Y IN N) {R : RelMfld IM M IN N} {K : Set X} [T2Space M] {F : FormalSol R} {G : HtpyFormalSol (RelMfld.localize φ ψ R)} (hK : IsCompact K) (hFG : ∀ (t : ℝ), ∀ x ∉ K, F (↑φ x) = ↑(OneJetBundle.embedding φ ψ) ((G t) x)) (t : ℝ) : ((φ.updateFormalSol ψ F G hK hFG) t).bs = fun (x : M) => (φ.update (OneJetBundle.embedding φ ψ) (⇑F) (⇑(G t)) x).proj.2

theorem OpenSmoothEmbedding.updateFormalSol_bs {EX : Type u_1} [NormedAddCommGroup EX] [NormedSpace ℝ EX] {HX : Type u_2} [TopologicalSpace HX] {IX : ModelWithCorners ℝ EX HX} {X : Type u_3} [TopologicalSpace X] [ChartedSpace HX X] [IsManifold IX (↑⊤) X] {EM : Type u_4} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_5} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} {M : Type u_6} [TopologicalSpace M] [ChartedSpace HM M] [IsManifold IM (↑⊤) M] {EY : Type u_7} [NormedAddCommGroup EY] [NormedSpace ℝ EY] {HY : Type u_8} [TopologicalSpace HY] {IY : ModelWithCorners ℝ EY HY} {Y : Type u_9} [TopologicalSpace Y] [ChartedSpace HY Y] [IsManifold IY (↑⊤) Y] {EN : Type u_10} [NormedAddCommGroup EN] [NormedSpace ℝ EN] {HN : Type u_11} [TopologicalSpace HN] {IN : ModelWithCorners ℝ EN HN} {N : Type u_12} [TopologicalSpace N] [ChartedSpace HN N] [IsManifold IN (↑⊤) N] (φ : OpenSmoothEmbedding IX X IM M) (ψ : OpenSmoothEmbedding IY Y IN N) {R : RelMfld IM M IN N} {K : Set X} [T2Space M] {F : FormalSol R} {G : HtpyFormalSol (RelMfld.localize φ ψ R)} (hK : IsCompact K) (hFG : ∀ (t : ℝ), ∀ x ∉ K, F (↑φ x) = ↑(OneJetBundle.embedding φ ψ) ((G t) x)) (t : ℝ) : ((φ.updateFormalSol ψ F G hK hFG) t).bs = φ.update ψ F.bs (G t).bs

@[simp]

theorem OpenSmoothEmbedding.updateFormalSol_apply_of_mem {EX : Type u_1} [NormedAddCommGroup EX] [NormedSpace ℝ EX] {HX : Type u_2} [TopologicalSpace HX] {IX : ModelWithCorners ℝ EX HX} {X : Type u_3} [TopologicalSpace X] [ChartedSpace HX X] [IsManifold IX (↑⊤) X] {EM : Type u_4} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_5} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} {M : Type u_6} [TopologicalSpace M] [ChartedSpace HM M] [IsManifold IM (↑⊤) M] {EY : Type u_7} [NormedAddCommGroup EY] [NormedSpace ℝ EY] {HY : Type u_8} [TopologicalSpace HY] {IY : ModelWithCorners ℝ EY HY} {Y : Type u_9} [TopologicalSpace Y] [ChartedSpace HY Y] [IsManifold IY (↑⊤) Y] {EN : Type u_10} [NormedAddCommGroup EN] [NormedSpace ℝ EN] {HN : Type u_11} [TopologicalSpace HN] {IN : ModelWithCorners ℝ EN HN} {N : Type u_12} [TopologicalSpace N] [ChartedSpace HN N] [IsManifold IN (↑⊤) N] (φ : OpenSmoothEmbedding IX X IM M) (ψ : OpenSmoothEmbedding IY Y IN N) {R : RelMfld IM M IN N} {K : Set X} [T2Space M] {F : FormalSol R} {G : HtpyFormalSol (RelMfld.localize φ ψ R)} (hK : IsCompact K) (hFG : ∀ (t : ℝ), ∀ x ∉ K, F (↑φ x) = ↑(OneJetBundle.embedding φ ψ) ((G t) x)) (t : ℝ) {m : M} (hx : m ∈ Set.range ↑φ) : ((φ.updateFormalSol ψ F G hK hFG) t) m = φ.transfer ψ ((G t) (φ.invFun m))

theorem OpenSmoothEmbedding.updateFormalSol_apply_image {EX : Type u_1} [NormedAddCommGroup EX] [NormedSpace ℝ EX] {HX : Type u_2} [TopologicalSpace HX] {IX : ModelWithCorners ℝ EX HX} {X : Type u_3} [TopologicalSpace X] [ChartedSpace HX X] [IsManifold IX (↑⊤) X] {EM : Type u_4} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_5} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} {M : Type u_6} [TopologicalSpace M] [ChartedSpace HM M] [IsManifold IM (↑⊤) M] {EY : Type u_7} [NormedAddCommGroup EY] [NormedSpace ℝ EY] {HY : Type u_8} [TopologicalSpace HY] {IY : ModelWithCorners ℝ EY HY} {Y : Type u_9} [TopologicalSpace Y] [ChartedSpace HY Y] [IsManifold IY (↑⊤) Y] {EN : Type u_10} [NormedAddCommGroup EN] [NormedSpace ℝ EN] {HN : Type u_11} [TopologicalSpace HN] {IN : ModelWithCorners ℝ EN HN} {N : Type u_12} [TopologicalSpace N] [ChartedSpace HN N] [IsManifold IN (↑⊤) N] (φ : OpenSmoothEmbedding IX X IM M) (ψ : OpenSmoothEmbedding IY Y IN N) {R : RelMfld IM M IN N} {K : Set X} [T2Space M] {F : FormalSol R} {G : HtpyFormalSol (RelMfld.localize φ ψ R)} (hK : IsCompact K) (hFG : ∀ (t : ℝ), ∀ x ∉ K, F (↑φ x) = ↑(OneJetBundle.embedding φ ψ) ((G t) x)) (t : ℝ) {x : X} : ((φ.updateFormalSol ψ F G hK hFG) t) (↑φ x) = φ.transfer ψ ((G t) x)