Documentation

SphereEversion.Local.OneJet

Spaces of 1-jets and their sections #

For real normed spaces E and F, this file defines the space OneJetSec E F of 1-jets of maps from E to F as E × F × (E →L[ℝ] F).

A section 𝓕 : JetSet E F of this space is a map (𝓕.f, 𝓕.φ) : E → F × (E →L[ℝ] F).

It is holonomic at x, spelled 𝓕.IsHolonomicAt x if the differential of 𝓕.f at x is 𝓕.φ x.

We then introduced parametrized families of sections, and especially homotopies of sections, with type HtpyJetSec E F and their concatenation operation HtpyJetSec.comp.

Implementation note: the time parameter t for homotopies is any real number, but all the homotopies we will construct will be constant for t ≤ 0 and t ≥ 1. It looks like this imposes more smoothness constraints at t = 0 and t = 1 (requiring flat functions), but this is needed for smooth concatenations anyway.

Spaces of 1-jets #

@[reducible, inline]

abbrev OneJet (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] (F : Type u_2) [NormedAddCommGroup F] [NormedSpace ℝ F] :

Type (max u_1 u_2 u_1)

The space of 1-jets of maps from E to F.

Equations

OneJet E F = (E × F × (E →L[ℝ ] F))

Instances For

instance instMetricSpaceOneJet (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] (F : Type u_2) [NormedAddCommGroup F] [NormedSpace ℝ F] :

MetricSpace (OneJet E F)

Equations

instMetricSpaceOneJet E F = inferInstanceAs (MetricSpace (E × F × (E →L[ℝ ] F)))

structure JetSec (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] (F : Type u_2) [NormedAddCommGroup F] [NormedSpace ℝ F] :

Type (max u_1 u_2)

A smooth section of J¹(E, F) → E.

f : E → F
f_diff : 𝒞 (↑⊤) self.f
φ : E → E →L[ℝ ] F
φ_diff : 𝒞 (↑⊤) self.φ

Instances For

theorem JetSec.ext {E : Type u_1} {inst✝ : NormedAddCommGroup E} {inst✝¹ : NormedSpace ℝ E} {F : Type u_2} {inst✝² : NormedAddCommGroup F} {inst✝³ : NormedSpace ℝ F} {x y : JetSec E F} (f : x.f = y.f) (φ : x.φ = y.φ) :

x = y

instance JetSec.instFunLikeProdContinuousLinearMapRealId {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] :

FunLike (JetSec E F) E (F × (E →L[ℝ ] F))

Equations

JetSec.instFunLikeProdContinuousLinearMapRealId = { coe := fun (𝓕 : JetSec E F) (x : E) => (𝓕.f x, 𝓕.φ x), coe_injective' := ⋯ }

@[simp]

theorem JetSec.mk_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E → F) (f_diff : 𝒞 (↑⊤) f) (φ : E → E →L[ℝ ] F) (φ_diff : 𝒞 (↑⊤) φ) (x : E) :

{ f := f, f_diff := f_diff, φ := φ, φ_diff := φ_diff } x = (f x, φ x)

theorem JetSec.eq_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {𝓕 𝓕' : JetSec E F} {x : E} :

𝓕 x = 𝓕' x ↔ 𝓕.f x = 𝓕'.f x ∧ 𝓕.φ x = 𝓕'.φ x

theorem JetSec.coe_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (𝓕 : JetSec E F) (x : E) :

𝓕 x = (𝓕.f x, 𝓕.φ x)

theorem JetSec.ext' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {𝓕 𝓕' : JetSec E F} (h : ∀ (x : E), 𝓕 x = 𝓕' x) :

𝓕 = 𝓕'

Holonomic sections #

def JetSec.IsHolonomicAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (𝓕 : JetSec E F) (x : E) :

A jet section 𝓕 is holonomic if its linear map part at x is the derivative of its function part at x.

Equations

𝓕.IsHolonomicAt x = (D 𝓕.f x = 𝓕.φ x)

Instances For

theorem JetSec.IsHolonomicAt.congr {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {𝓕 𝓕' : JetSec E F} {x : E} (h : 𝓕.IsHolonomicAt x) (h' : ⇑𝓕 =ᶠ[nhds x] ⇑𝓕') :

𝓕'.IsHolonomicAt x

def JetSec.IsPartHolonomicAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (𝓕 : JetSec E F) (E' : Submodule ℝ E) (x : E) :

A formal solution 𝓕 of R is partially holonomic in the direction of some subspace E' if its linear map part at x is the derivative of its function part at x in restriction to E'.

Equations

𝓕.IsPartHolonomicAt E' x = ∀ v ∈ E', (D 𝓕.f x) v = (𝓕.φ x) v

Instances For

theorem Filter.Eventually.isPartHolonomicAt_congr {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {𝓕 𝓕' : JetSec E F} {s : Set E} (h : ∀ᶠ (x : E) in nhdsSet s, 𝓕 x = 𝓕' x) (E' : Submodule ℝ E) :

∀ᶠ (x : E) in nhdsSet s, 𝓕.IsPartHolonomicAt E' x ↔ 𝓕'.IsPartHolonomicAt E' x

theorem JetSec.IsPartHolonomicAt.sup {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (𝓕 : JetSec E F) {E' E'' : Submodule ℝ E} {x : E} (h' : 𝓕.IsPartHolonomicAt E' x) (h'' : 𝓕.IsPartHolonomicAt E'' x) :

𝓕.IsPartHolonomicAt (E' ⊔ E'') x

theorem JetSec.isPartHolonomicAt_top {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {𝓕 : JetSec E F} {x : E} :

𝓕.IsPartHolonomicAt ⊤ x ↔ 𝓕.IsHolonomicAt x

@[simp]

theorem JetSec.isPartHolonomicAt_bot {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (𝓕 : JetSec E F) :

𝓕.IsPartHolonomicAt ⊥ = fun (x : E) => True

Homotopies of sections #

structure FamilyJetSec (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] (F : Type u_2) [NormedAddCommGroup F] [NormedSpace ℝ F] (P : Type u_3) [NormedAddCommGroup P] [NormedSpace ℝ P] :

Type (max (max u_1 u_2) u_3)

A parametrized family of sections of J¹(E, F).

f : P → E → F
f_diff : 𝒞 ↑⊤ ↿self.f
φ : P → E → E →L[ℝ ] F
φ_diff : 𝒞 ↑⊤ ↿self.φ

Instances For

@[reducible]

def HtpyJetSec (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] (F : Type u_2) [NormedAddCommGroup F] [NormedSpace ℝ F] :

Type (max (max u_1 u_2) 0)

A homotopy of sections of J¹(E, F).

Equations

HtpyJetSec E F = FamilyJetSec E F ℝ

Instances For

instance FamilyJetSec.instFunLikeJetSec {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {P : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] :

FunLike (FamilyJetSec E F P) P (JetSec E F)

Equations

FamilyJetSec.instFunLikeJetSec = { coe := fun (S : FamilyJetSec E F P) (t : P) => { f := S.f t, f_diff := ⋯, φ := S.φ t, φ_diff := ⋯ }, coe_injective' := ⋯ }

@[simp]

theorem FamilyJetSec.mk_apply_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {P : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] (f : P → E → F) (f_diff : 𝒞 ↑⊤ ↿f) (φ : P → E → E →L[ℝ ] F) (φ_diff : 𝒞 ↑⊤ ↿φ) (t : P) (x : E) :

({ f := f, f_diff := f_diff, φ := φ, φ_diff := φ_diff } t) x = (f t x, φ t x)

@[simp]

theorem FamilyJetSec.mk_apply_f {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {P : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] (f : P → E → F) (f_diff : 𝒞 ↑⊤ ↿f) (φ : P → E → E →L[ℝ ] F) (φ_diff : 𝒞 ↑⊤ ↿φ) (t : P) :

({ f := f, f_diff := f_diff, φ := φ, φ_diff := φ_diff } t).f = f t

@[simp]

theorem FamilyJetSec.mk_apply_φ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {P : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] (f : P → E → F) (f_diff : 𝒞 ↑⊤ ↿f) (φ : P → E → E →L[ℝ ] F) (φ_diff : 𝒞 ↑⊤ ↿φ) (t : P) :

({ f := f, f_diff := f_diff, φ := φ, φ_diff := φ_diff } t).φ = φ t

theorem FamilyJetSec.contDiff_f {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {P : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] (𝓕 : FamilyJetSec E F P) {n : ℕ∞} :

𝒞 ↑n ↿𝓕.f

theorem FamilyJetSec.contDiff_φ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {P : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] (𝓕 : FamilyJetSec E F P) {n : ℕ∞} :

𝒞 ↑n ↿𝓕.φ

def JetSec.constHtpy {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (𝓕 : JetSec E F) :

The constant homotopy of formal solutions at a given formal solution. It will be used as junk value for constructions of formal homotopies that need additional assumptions and also for trivial induction initialization.

Equations

𝓕.constHtpy = { f := fun (x : ℝ) => 𝓕.f, f_diff := ⋯, φ := fun (x : ℝ) => 𝓕.φ, φ_diff := ⋯ }

Instances For

@[simp]

theorem JetSec.constHtpy_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (𝓕 : JetSec E F) (t : ℝ) :

𝓕.constHtpy t = 𝓕

Concatenation of homotopies of sections #

In this part of the file we build a concatenation operation for homotopies of 1-jet sections. We first need to introduce a smooth step function on ℝ. There is already a version of this in mathlib called smooth_transition but that version is not locally constant near 0 and 1, which is not convenient enough for gluing purposes.

def smoothStep :

A smooth step function on ℝ.

Equations

smoothStep t = (2 * t - 1 / 2).smoothTransition

Instances For

theorem smoothStep.smooth :

𝒞 (↑⊤) smoothStep

@[simp]

theorem smoothStep.zero :

smoothStep 0 = 0

@[simp]

theorem smoothStep.one :

smoothStep 1 = 1

theorem smoothStep.mem (t : ℝ) :

smoothStep t ∈ unitInterval

theorem smoothStep.abs_le (t : ℝ) :

|smoothStep t| ≤ 1

theorem smoothStep.of_lt {t : ℝ} (h : t < 1 / 4) :

smoothStep t = 0

theorem smoothStep.pos_of_gt {t : ℝ} (h : 1 / 4 < t) :

0 < smoothStep t

theorem smoothStep.of_gt {t : ℝ} (h : 3 / 4 < t) :

smoothStep t = 1

theorem htpy_jet_sec_comp_aux {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {f g : ℝ → E → F} (hf : 𝒞 ↑⊤ ↿f) (hg : 𝒞 ↑⊤ ↿g) (hfg : f 1 = g 0) :

𝒞 ↑⊤ ↿fun (t : ℝ) (x : E) => if t ≤ 1 / 2 then f (smoothStep (2 * t)) x else g (smoothStep (2 * t - 1)) x

def HtpyJetSec.comp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (𝓕 𝓖 : HtpyJetSec E F) (h : 𝓕 1 = 𝓖 0) :

Concatenation of homotopies of formal solution. The result depend on our choice of a smooth step function in order to keep smoothness with respect to the time parameter.

Equations

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

Instances For

@[simp]

theorem HtpyJetSec.comp_of_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (𝓕 𝓖 : HtpyJetSec E F) (h : 𝓕 1 = 𝓖 0) {t : ℝ} (ht : t ≤ 1 / 2) :

(𝓕.comp 𝓖 h) t = 𝓕 (smoothStep (2 * t))

theorem HtpyJetSec.comp_le_0 {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (𝓕 𝓖 : HtpyJetSec E F) (h : 𝓕 1 = 𝓖 0) :

∀ᶠ (t : ℝ) in nhdsSet (Set.Iic 0), (𝓕.comp 𝓖 h) t = 𝓕 0

theorem HtpyJetSec.comp_0 {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (𝓕 𝓖 : HtpyJetSec E F) (h : 𝓕 1 = 𝓖 0) :

(𝓕.comp 𝓖 h) 0 = 𝓕 0

@[simp]

theorem HtpyJetSec.comp_of_not_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (𝓕 𝓖 : HtpyJetSec E F) (h : 𝓕 1 = 𝓖 0) {t : ℝ} (ht : ¬t ≤ 1 / 2) :

(𝓕.comp 𝓖 h) t = 𝓖 (smoothStep (2 * t - 1))

theorem HtpyJetSec.comp_ge_1 {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (𝓕 𝓖 : HtpyJetSec E F) (h : 𝓕 1 = 𝓖 0) :

∀ᶠ (t : ℝ) in nhdsSet (Set.Ici 1), (𝓕.comp 𝓖 h) t = 𝓖 1

@[simp]

theorem HtpyJetSec.comp_1 {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (𝓕 𝓖 : HtpyJetSec E F) (h : 𝓕 1 = 𝓖 0) :

(𝓕.comp 𝓖 h) 1 = 𝓖 1