SphereEversion.Global.ParametricityForFree

Fundamental definitions #

def RelMfld.relativize {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'] {EP : Type u_7} [NormedAddCommGroup EP] [NormedSpace ℝ EP] {HP : Type u_8} [TopologicalSpace HP] (IP : ModelWithCorners ℝ EP HP) (P : Type u_9) [TopologicalSpace P] [ChartedSpace HP P] (R : RelMfld I M I' M') :

RelMfld (IP.prod I) (P × M) I' M'

The relation 𝓡 ^ P

Equations

RelMfld.relativize IP P R = bundleSnd ⁻¹' R

Instances For

source

theorem RelMfld.mem_relativize {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'] {EP : Type u_7} [NormedAddCommGroup EP] [NormedSpace ℝ EP] {HP : Type u_8} [TopologicalSpace HP] {IP : ModelWithCorners ℝ EP HP} {P : Type u_9} [TopologicalSpace P] [ChartedSpace HP P] (R : RelMfld I M I' M') (w : OneJetBundle (IP.prod I) (P × M) I' M') :

w ∈ relativize IP P R ↔ OneJetBundle.mk w.proj.1.2 w.proj.2 (ContinuousLinearMap.comp w.snd (ContinuousLinearMap.inr ℝ EP E)) ∈ R

source

theorem RelMfld.isOpen_relativize {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_7} [NormedAddCommGroup EP] [NormedSpace ℝ EP] {HP : Type u_8} [TopologicalSpace HP] {IP : ModelWithCorners ℝ EP HP} {P : Type u_9} [TopologicalSpace P] [ChartedSpace HP P] [IsManifold IP (↑⊤) P] (R : RelMfld I M I' M') (h2 : IsOpen R) :

IsOpen (relativize IP P R)

source

theorem relativize_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'] {EP : Type u_7} [NormedAddCommGroup EP] [NormedSpace ℝ EP] {HP : Type u_8} [TopologicalSpace HP] {IP : ModelWithCorners ℝ EP HP} {P : Type u_9} [TopologicalSpace P] [ChartedSpace HP P] {R : RelMfld I M I' M'} {σ : OneJetBundle (IP.prod I) (P × M) I' M'} {p : DualPair (TangentSpace (IP.prod I) σ.proj.1)} (q : DualPair (TangentSpace I σ.proj.1.2)) (hpq : p.π.comp (ContinuousLinearMap.inr ℝ EP E) = q.π) :

(RelMfld.relativize IP P R).slice σ p = σ.snd (p.v - id (0, q.v)) +ᵥ id (R.slice (bundleSnd σ) q)

source

theorem relativize_slice_eq_univ {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'] {EP : Type u_7} [NormedAddCommGroup EP] [NormedSpace ℝ EP] {HP : Type u_8} [TopologicalSpace HP] {IP : ModelWithCorners ℝ EP HP} {P : Type u_9} [TopologicalSpace P] [ChartedSpace HP P] {R : RelMfld I M I' M'} {σ : OneJetBundle (IP.prod I) (P × M) I' M'} {p : DualPair (TangentSpace (IP.prod I) σ.proj.1)} (hp : p.π.comp (ContinuousLinearMap.inr ℝ EP E) = 0) :

((RelMfld.relativize IP P R).slice σ p).Nonempty ↔ (RelMfld.relativize IP P R).slice σ p = Set.univ

source

theorem RelMfld.Ample.relativize {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'] {EP : Type u_7} [NormedAddCommGroup EP] [NormedSpace ℝ EP] {HP : Type u_8} [TopologicalSpace HP] (IP : ModelWithCorners ℝ EP HP) (P : Type u_9) [TopologicalSpace P] [ChartedSpace HP P] {R : RelMfld I M I' M'} (hR : R.Ample) :

(RelMfld.relativize IP P R).Ample

source

theorem FamilyOneJetSec.uncurry_mem_relativize {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_7} [NormedAddCommGroup EP] [NormedSpace ℝ EP] {HP : Type u_8} [TopologicalSpace HP] {IP : ModelWithCorners ℝ EP HP} {P : Type u_9} [TopologicalSpace P] [ChartedSpace HP P] [IsManifold IP (↑⊤) P] {R : RelMfld I M I' M'} (S : FamilyOneJetSec I M I' M' IP P) {s : P} {x : M} :

S.uncurry (s, x) ∈ RelMfld.relativize IP P R ↔ (S s) x ∈ R

source

def FamilyFormalSol.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_7} [NormedAddCommGroup EP] [NormedSpace ℝ EP] {HP : Type u_8} [TopologicalSpace HP] {IP : ModelWithCorners ℝ EP HP} {P : Type u_9} [TopologicalSpace P] [ChartedSpace HP P] [IsManifold IP (↑⊤) P] {R : RelMfld I M I' M'} (S : FamilyFormalSol IP P R) :

FormalSol (RelMfld.relativize IP P R)

Equations

S.uncurry = { toOneJetSec := S.uncurry, is_sol' := ⋯ }

Instances For

source

theorem FamilyFormalSol.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_7} [NormedAddCommGroup EP] [NormedSpace ℝ EP] {HP : Type u_8} [TopologicalSpace HP] {IP : ModelWithCorners ℝ EP HP} {P : Type u_9} [TopologicalSpace P] [ChartedSpace HP P] [IsManifold IP (↑⊤) P] {R : RelMfld I M I' M'} (S : FamilyFormalSol IP P R) (p : P × M) :

S.uncurry.ϕ p = (mfderiv IP I' (fun (z : P) => S.bs z p.2) p.1).comp (ContinuousLinearMap.fst ℝ EP E) + (S.ϕ p.1 p.2).comp (ContinuousLinearMap.snd ℝ EP E)

source

def FamilyOneJetSec.curry {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_7} [NormedAddCommGroup EP] [NormedSpace ℝ EP] {HP : Type u_8} [TopologicalSpace HP] {IP : ModelWithCorners ℝ EP HP} {P : Type u_9} [TopologicalSpace P] [ChartedSpace HP P] [IsManifold IP (↑⊤) P] {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] [IsManifold J (↑⊤) N] (S : FamilyOneJetSec (IP.prod I) (P × M) I' M' J N) :

FamilyOneJetSec I M I' M' (J.prod IP) (N × P)

Equations

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

Instances For

source

theorem FamilyOneJetSec.curry_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_7} [NormedAddCommGroup EP] [NormedSpace ℝ EP] {HP : Type u_8} [TopologicalSpace HP] {IP : ModelWithCorners ℝ EP HP} {P : Type u_9} [TopologicalSpace P] [ChartedSpace HP P] [IsManifold IP (↑⊤) P] {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] [IsManifold J (↑⊤) N] (S : FamilyOneJetSec (IP.prod I) (P × M) I' M' J N) (p : N × P) (x : M) :

(S.curry p).bs x = (S p.1).bs (p.2, x)

source

theorem FamilyOneJetSec.curry_ϕ {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_7} [NormedAddCommGroup EP] [NormedSpace ℝ EP] {HP : Type u_8} [TopologicalSpace HP] {IP : ModelWithCorners ℝ EP HP} {P : Type u_9} [TopologicalSpace P] [ChartedSpace HP P] [IsManifold IP (↑⊤) P] {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] [IsManifold J (↑⊤) N] (S : FamilyOneJetSec (IP.prod I) (P × M) I' M' J N) (p : N × P) (x : M) :

(S.curry p).ϕ x = ((S p.1).ϕ (p.2, x)).comp (mfderiv I (IP.prod I) (fun (x : M) => (p.2, x)) x)

source

(S.curry p).ϕ x = ((S p.1).ϕ (p.2, x)).comp (ContinuousLinearMap.inr ℝ EP E)

source

theorem FormalSol.eq_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'} {F₁ F₂ : FormalSol R} {x : M} :

F₁ x = F₂ x ↔ F₁.bs x = F₂.bs x ∧ F₁.ϕ x = F₂.ϕ x

source

(S.curry (t, s)).IsHolonomicAt x

source

(S.curry p) x ∈ R

source

def FamilyFormalSol.curry {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_7} [NormedAddCommGroup EP] [NormedSpace ℝ EP] {HP : Type u_8} [TopologicalSpace HP] {IP : ModelWithCorners ℝ EP HP} {P : Type u_9} [TopologicalSpace P] [ChartedSpace HP P] [IsManifold IP (↑⊤) P] {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] [IsManifold J (↑⊤) N] {R : RelMfld I M I' M'} (S : FamilyFormalSol J N (RelMfld.relativize IP P R)) :

FamilyFormalSol (J.prod IP) (N × P) R

Equations

S.curry = { toFamilyOneJetSec := S.curry, is_sol' := ⋯ }

Instances For

source

(S.curry p).ϕ x = ((S p.1).ϕ (p.2, x)).comp (ContinuousLinearMap.inr ℝ EP E)

source

(𝓕.curry (t, s)) x = (𝓕₀ s) x

source

theorem RelMfld.SatisfiesHPrinciple.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_7} [NormedAddCommGroup EP] [NormedSpace ℝ EP] {HP : Type u_8} [TopologicalSpace HP] {IP : ModelWithCorners ℝ EP HP} {P : Type u_9} [TopologicalSpace P] [ChartedSpace HP P] [IsManifold IP (↑⊤) P] {EX : Type u_13} [NormedAddCommGroup EX] [NormedSpace ℝ EX] {HX : Type u_14} [TopologicalSpace HX] {IX : ModelWithCorners ℝ EX HX} {X : Type u_15} [MetricSpace X] [ChartedSpace HX X] [IsManifold IX (↑⊤) X] (R : RelMfld I M IX X) {C : Set (P × M)} (ε : M → ℝ) (h : (relativize IP P R).SatisfiesHPrinciple C fun (x : P × M) => ε x.2) :

SatisfiesHPrincipleWith IP R C ε