diff --git a/SphereEversion/Global/Gromov.lean b/SphereEversion/Global/Gromov.lean index beeeaf67..67910282 100644 --- a/SphereEversion/Global/Gromov.lean +++ b/SphereEversion/Global/Gromov.lean @@ -68,9 +68,8 @@ theorem RelMfld.Ample.satisfiesHPrinciple (hRample : R.Ample) (hRopen : IsOpen R change ContMDiffAt _ _ _ (f ∘ fun p : ℝ × M ↦ (a * p.1 + b, p.2)) (t, x) change ContMDiffAt _ _ _ f ((fun p : ℝ × M ↦ (a * p.1 + b, p.2)) (t, x)) at h have : - ContMDiffAt (𝓘(ℝ, ℝ).prod IM) (𝓘(ℝ, ℝ).prod IM) ∞ (fun p : ℝ × M ↦ (a * p.1 + b, p.2)) - (t, x) := - haveI h₁ : ContMDiffAt 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) ∞ (fun t ↦ a * t + b) t := + CMDiffAt ∞ (fun p : ℝ × M ↦ (a * p.1 + b, p.2)) (t, x) := + haveI h₁ : CMDiffAt ∞ (fun t ↦ a * t + b) t := contMDiffAt_iff_contDiffAt.mpr (((contDiffAt_id : ContDiffAt ℝ ∞ id t).const_smul a).add contDiffAt_const) h₁.prodMap contMDiffAt_id diff --git a/SphereEversion/Global/Immersion.lean b/SphereEversion/Global/Immersion.lean index 2abc9f9d..29dbb9be 100644 --- a/SphereEversion/Global/Immersion.lean +++ b/SphereEversion/Global/Immersion.lean @@ -142,7 +142,7 @@ theorem immersion_antipodal_sphere : Immersion (𝓡 n) 𝓘(ℝ, E) -- The other direction elaborates much worse. (contDiff_neg.contMDiff).comp (contMDiff_coe_sphere.of_le le_top) diff_injective x := by - change Injective (mfderiv (𝓡 n) 𝓘(ℝ, E) (-fun x : sphere (0 : E) 1 ↦ (x : E)) x) + change Injective (mfderiv% (-fun x : sphere (0 : E) 1 ↦ (x : E)) x) rw [mfderiv_neg] exact neg_injective.comp (mfderiv_coe_sphere_injective x) @@ -168,8 +168,7 @@ variable (ω : Orientation ℝ E (Fin 3)) -- this result holds mutatis mutandis in `ℝ^n` theorem smooth_bs : - ContMDiff (𝓘(ℝ, ℝ).prod (𝓡 2)) 𝓘(ℝ, E) ∞ - fun p : ℝ × (sphere (0 : E) 1) ↦ (1 - p.1) • (p.2 : E) + p.1 • -(p.2: E) := by + CMDiff ∞ fun p : ℝ × (sphere (0 : E) 1) ↦ (1 - p.1) • (p.2 : E) + p.1 • -(p.2: E) := by refine (ContMDiff.smul (I := 𝓘(ℝ)) ?_ ?_).add (contMDiff_fst.smul ?_) · exact (contDiff_const.sub contDiff_id).contMDiff.comp contMDiff_fst · exact (contMDiff_coe_sphere.of_le le_top).comp contMDiff_snd @@ -181,6 +180,8 @@ def formalEversionAux : FamilyOneJetSec (𝓡 2) 𝕊² 𝓘(ℝ, E) E 𝓘(ℝ, (fun p : ℝ × 𝕊² ↦ ω.rot (p.1, p.2)) (by intro p + -- Note: elaborators would infer another model on the domain, namely `𝓘(ℝ, ℝ).prod 𝓘(ℝ, E)` + -- In any case, this should not work, as we have a product of normed spaces? have : ContMDiffAt 𝓘(ℝ, ℝ × E) 𝓘(ℝ, E →L[ℝ] E) ∞ ω.rot (p.1, p.2) := by refine ((ω.contDiff_rot ?_).of_le le_top).contMDiffAt exact ne_zero_of_mem_unit_sphere p.2 @@ -209,9 +210,9 @@ theorem formalEversionHolAtZero {t : ℝ} (ht : t < 1 / 4) : (formalEversion E ω t).toOneJetSec.IsHolonomic := by intro x change - mfderiv (𝓡 2) 𝓘(ℝ, E) (fun y : 𝕊² ↦ ((1 : ℝ) - smoothStep t) • (y : E) + + mfderiv% (fun y : 𝕊² ↦ ((1 : ℝ) - smoothStep t) • (y : E) + smoothStep t • -(y : E)) x = - (ω.rot (smoothStep t, x)).comp (mfderiv (𝓡 2) 𝓘(ℝ, E) (fun y : 𝕊² ↦ (y : E)) x) + (ω.rot (smoothStep t, x)).comp (mfderiv% (fun y : 𝕊² ↦ (y : E)) x) simp_rw [smoothStep.of_lt ht, ω.rot_zero, ContinuousLinearMap.id_comp] congr with y simp [smoothStep.of_lt ht] @@ -221,10 +222,10 @@ theorem formalEversionHolAtOne {t : ℝ} (ht : 3 / 4 < t) : (formalEversion E ω t).toOneJetSec.IsHolonomic := by intro x change - mfderiv (𝓡 2) 𝓘(ℝ, E) (fun y : 𝕊² ↦ ((1 : ℝ) - smoothStep t) • (y : E) + + mfderiv% (fun y : 𝕊² ↦ ((1 : ℝ) - smoothStep t) • (y : E) + smoothStep t • -(y : E)) x = - (ω.rot (smoothStep t, x)).comp (mfderiv (𝓡 2) 𝓘(ℝ, E) (fun y : 𝕊² ↦ (y : E)) x) - trans mfderiv (𝓡 2) 𝓘(ℝ, E) (-fun y : 𝕊² ↦ (y : E)) x + (ω.rot (smoothStep t, x)).comp (mfderiv% (fun y : 𝕊² ↦ (y : E)) x) + trans mfderiv% (-fun y : 𝕊² ↦ (y : E)) x · congr 2 with y simp [smoothStep.of_gt ht] ext v @@ -285,13 +286,13 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] -- move to Mathlib.Geometry.Manifold.ContMDiff.Product lemma ContMDiff.prod_left {n : ℕ∞} (x : M) : - ContMDiff I' (I.prod I') n fun p : M' ↦ (⟨x, p⟩ : M × M') := by + CMDiff n fun p : M' ↦ (⟨x, p⟩ : M × M') := by rw [contMDiff_prod_iff] exact ⟨contMDiff_const, contMDiff_id⟩ -- move to Mathlib.Geometry.Manifold.ContMDiff.Product theorem ContMDiff.uncurry_left {n : ℕ∞} {f : M → M' → P} - (hf : ContMDiff (I.prod I') IP n ↿f) (x : M) : CMDiff n (f x) := by + (hf : CMDiff n ↿f) (x : M) : CMDiff n (f x) := by have : f x = (uncurry f) ∘ fun p : M' ↦ ⟨x, p⟩ := by ext; simp -- or just `apply hf.comp (ContMDiff.prod_left I I' x)` rw [this]; exact hf.comp (ContMDiff.prod_left I I' x) @@ -300,8 +301,7 @@ end helper theorem sphere_eversion : ∃ f : ℝ → 𝕊² → E, - ContMDiff (𝓘(ℝ, ℝ).prod (𝓡 2)) 𝓘(ℝ, E) ∞ ↿f ∧ - (f 0 = fun x : 𝕊² ↦ (x : E)) ∧ (f 1 = fun x : 𝕊² ↦ -(x : E)) ∧ + CMDiff ∞ ↿f ∧ (f 0 = fun x : 𝕊² ↦ (x : E)) ∧ (f 1 = fun x : 𝕊² ↦ -(x : E)) ∧ ∀ t, Immersion (𝓡 2) 𝓘(ℝ, E) (f t) ∞ := by classical let ω : Orientation ℝ E (Fin 3) := diff --git a/SphereEversion/Global/OneJetBundle.lean b/SphereEversion/Global/OneJetBundle.lean index 80eabca1..651331d0 100644 --- a/SphereEversion/Global/OneJetBundle.lean +++ b/SphereEversion/Global/OneJetBundle.lean @@ -337,12 +337,12 @@ theorem contMDiff_oneJetBundle_proj : theorem ContMDiff.oneJetBundle_proj {f : N → J¹MM'} (hf : ContMDiff J ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ∞ f) : - ContMDiff J (I.prod I') ∞ fun x ↦ (f x).1 := + CMDiff ∞ fun x ↦ (f x).1 := contMDiff_oneJetBundle_proj.comp hf theorem ContMDiffAt.oneJetBundle_proj {f : N → J¹MM'} {x₀ : N} (hf : ContMDiffAt J ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ∞ f x₀) : - ContMDiffAt J (I.prod I') ∞ (fun x ↦ (f x).1) x₀ := + CMDiffAt ∞ (fun x ↦ (f x).1) x₀ := (contMDiff_oneJetBundle_proj _).comp x₀ hf /-- The constructor of `OneJetBundle`, in case `Sigma.mk` will not give the right type. -/ @@ -365,11 +365,10 @@ theorem oneJetBundle_mk_snd {x : M} {y : M'} {f : OneJetSpace I I' (x, y)} : set_option backward.isDefEq.respectTransparency false in theorem contMDiffAt_oneJetBundle {f : N → J¹MM'} {x₀ : N} : ContMDiffAt J ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ∞ f x₀ ↔ - CMDiffAt ∞ (fun x ↦ (f x).1.1) x₀ ∧ - CMDiffAt ∞ (fun x ↦ (f x).1.2) x₀ ∧ - ContMDiffAt J 𝓘(𝕜, E →L[𝕜] E') ∞ - (inTangentCoordinates I I' (fun x ↦ (f x).1.1) (fun x ↦ (f x).1.2) (fun x ↦ (f x).2) - x₀) x₀ := by + CMDiffAt ∞ (fun x ↦ (f x).1.1) x₀ ∧ CMDiffAt ∞ (fun x ↦ (f x).1.2) x₀ ∧ + CMDiffAt ∞ + (inTangentCoordinates I I' (fun x ↦ (f x).1.1) (fun x ↦ (f x).1.2) (fun x ↦ (f x).2) x₀) + x₀ := by simp_rw [Bundle.contMDiffAt_totalSpace, contMDiffAt_prod_iff, and_assoc, oneJetBundle_trivializationAt] rfl @@ -377,13 +376,12 @@ theorem contMDiffAt_oneJetBundle {f : N → J¹MM'} {x₀ : N} : theorem contMDiffAt_oneJetBundle_mk {f : N → M} {g : N → M'} {ϕ : N → E →L[𝕜] E'} {x₀ : N} : ContMDiffAt J ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ∞ (fun x ↦ OneJetBundle.mk (f x) (g x) (ϕ x) : N → J¹MM') x₀ ↔ - CMDiffAt ∞ f x₀ ∧ CMDiffAt ∞ g x₀ ∧ - ContMDiffAt J 𝓘(𝕜, E →L[𝕜] E') ∞ (inTangentCoordinates I I' f g ϕ x₀) x₀ := + CMDiffAt ∞ f x₀ ∧ CMDiffAt ∞ g x₀ ∧ CMDiffAt ∞ (inTangentCoordinates I I' f g ϕ x₀) x₀ := contMDiffAt_oneJetBundle theorem ContMDiffAt.oneJetBundle_mk {f : N → M} {g : N → M'} {ϕ : N → E →L[𝕜] E'} {x₀ : N} (hf : CMDiffAt ∞ f x₀) (hg : CMDiffAt ∞ g x₀) - (hϕ : ContMDiffAt J 𝓘(𝕜, E →L[𝕜] E') ∞ (inTangentCoordinates I I' f g ϕ x₀) x₀) : + (hϕ : CMDiffAt ∞ (inTangentCoordinates I I' f g ϕ x₀) x₀) : ContMDiffAt J ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ∞ (fun x ↦ OneJetBundle.mk (f x) (g x) (ϕ x) : N → J¹MM') x₀ := contMDiffAt_oneJetBundle.mpr ⟨hf, hg, hϕ⟩ @@ -421,9 +419,9 @@ theorem ContinuousAt.inTangentCoordinates_comp {f : N → M} {g : N → M'} {h : theorem ContMDiffAt.clm_comp_inTangentCoordinates {f : N → M} {g : N → M'} {h : N → N'} {ϕ' : N → E' →L[𝕜] F'} {ϕ : N → E →L[𝕜] E'} {n : N} (hg : ContinuousAt g n) - (hϕ' : ContMDiffAt J 𝓘(𝕜, E' →L[𝕜] F') ∞ (inTangentCoordinates I' J' g h ϕ' n) n) - (hϕ : ContMDiffAt J 𝓘(𝕜, E →L[𝕜] E') ∞ (inTangentCoordinates I I' f g ϕ n) n) : - ContMDiffAt J 𝓘(𝕜, E →L[𝕜] F') ∞ (inTangentCoordinates I J' f h (fun n ↦ ϕ' n ∘L ϕ n) n) n := + (hϕ' : CMDiffAt ∞ (inTangentCoordinates I' J' g h ϕ' n) n) + (hϕ : CMDiffAt ∞ (inTangentCoordinates I I' f g ϕ n) n) : + CMDiffAt ∞ (inTangentCoordinates I J' f h (fun n ↦ ϕ' n ∘L ϕ n) n) n := (hϕ'.clm_comp hϕ).congr_of_eventuallyEq hg.inTangentCoordinates_comp variable (I') @@ -518,13 +516,11 @@ theorem OneJetBundle.map_id (x : J¹MM') : theorem ContMDiffAt.oneJetBundle_map {f : M'' → M → N} {g : M'' → M' → N'} {x₀ : M''} {Dfinv : ∀ (z : M'') (x : M), TangentSpace% (f z x) →L[𝕜] TangentSpace% x} {k : M'' → J¹MM'} - (hf : ContMDiffAt (I''.prod I) J ∞ f.uncurry (x₀, (k x₀).1.1)) - (hg : ContMDiffAt (I''.prod I') J' ∞ g.uncurry (x₀, (k x₀).1.2)) + (hf : CMDiffAt ∞ f.uncurry (x₀, (k x₀).1.1)) + (hg : CMDiffAt ∞ g.uncurry (x₀, (k x₀).1.2)) (hDfinv : - ContMDiffAt I'' 𝓘(𝕜, F →L[𝕜] E) ∞ - (inTangentCoordinates J I (fun x ↦ f x (k x).1.1) (fun x ↦ (k x).1.1) - (fun x ↦ Dfinv x (k x).1.1) x₀) - x₀) + CMDiffAt ∞ (inTangentCoordinates J I (fun x ↦ f x (k x).1.1) (fun x ↦ (k x).1.1) + (fun x ↦ Dfinv x (k x).1.1) x₀) x₀) (hk : ContMDiffAt I'' ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ∞ k x₀) : ContMDiffAt I'' ((J.prod J').prod 𝓘(𝕜, F →L[𝕜] F')) ∞ (fun z ↦ OneJetBundle.map I' J' (f z) (g z) (Dfinv z) (k z)) x₀ := by @@ -532,7 +528,7 @@ theorem ContMDiffAt.oneJetBundle_map {f : M'' → M → N} {g : M'' → M' → N refine ContMDiffAt.oneJet_comp _ _ ?_ ?_ · refine ContMDiffAt.oneJet_comp _ _ ?_ ?_ · refine hk.2.1.oneJetBundle_mk (hg.comp x₀ (contMDiffAt_id.prodMk hk.2.1)) ?_ - exact ContMDiffAt.mfderiv g (fun x ↦ (k x).1.2) hg hk.2.1 le_rfl + exact hg.mfderiv g (fun x ↦ (k x).1.2) hk.2.1 le_rfl · exact hk.1.oneJetBundle_mk hk.2.1 hk.2.2 apply (hf.comp x₀ (contMDiffAt_id.prodMk hk.1)).oneJetBundle_mk hk.1 apply hDfinv @@ -554,9 +550,9 @@ theorem mapLeft_eq_map (f : M → N) (Dfinv : ∀ x : M, TangentSpace% (f x) → theorem ContMDiffAt.mapLeft {f : N' → M → N} {x₀ : N'} {Dfinv : ∀ (z : N') (x : M), TangentSpace% (f z x) →L[𝕜] TangentSpace% x} {g : N' → J¹MM'} - (hf : ContMDiffAt (J'.prod I) J ∞ f.uncurry (x₀, (g x₀).1.1)) + (hf : CMDiffAt ∞ f.uncurry (x₀, (g x₀).1.1)) (hDfinv : - ContMDiffAt J' 𝓘(𝕜, F →L[𝕜] E) ∞ + CMDiffAt ∞ (inTangentCoordinates J I (fun x ↦ f x (g x).1.1) (fun x ↦ (g x).1.1) (fun x ↦ Dfinv x (g x).1.1) x₀) x₀) diff --git a/SphereEversion/Global/OneJetSec.lean b/SphereEversion/Global/OneJetSec.lean index 6e73c25e..892d0fae 100644 --- a/SphereEversion/Global/OneJetSec.lean +++ b/SphereEversion/Global/OneJetSec.lean @@ -224,7 +224,7 @@ protected theorem contMDiff (S : FamilyOneJetSec I M I' M' J N) : S.contMDiff' theorem contMDiff_bs (S : FamilyOneJetSec I M I' M' J N) : - ContMDiff (J.prod I) I' ∞ fun p : N × M ↦ S.bs p.1 p.2 := + CMDiff ∞ fun p : N × M ↦ S.bs p.1 p.2 := contMDiff_oneJetBundle_proj.snd.comp S.contMDiff theorem contMDiff_coe_bs (S : FamilyOneJetSec I M I' M' J N) {p : N} : CMDiff ∞ (S.bs p) := @@ -244,14 +244,12 @@ def reindex (S : FamilyOneJetSec I M I' M' J' N') (f : C^∞⟮J, N; J', N'⟯) def uncurry (S : FamilyOneJetSec I M I' M' IP P) : OneJetSec (IP.prod I) (P × M) I' M' where bs p := S.bs p.1 p.2 ϕ p := - (mfderiv (IP.prod I) I' (fun z : P × M ↦ S.bs z.1 p.2) p) + - S.ϕ p.1 p.2 ∘L mfderiv (IP.prod I) I Prod.snd p + (mfderiv% (fun z : P × M ↦ S.bs z.1 p.2) p) + S.ϕ p.1 p.2 ∘L mfderiv (IP.prod I) I Prod.snd p contMDiff' := by refine ContMDiff.oneJet_add ?_ ?_ · intro y refine contMDiffAt_id.oneJetBundle_mk (S.contMDiff_bs y) ?_ - have : ContMDiffAt ((IP.prod I).prod (IP.prod I)) I' ∞ - (Function.uncurry fun x z : P × M ↦ S.bs z.1 x.2) (y, y) := + have : CMDiffAt ∞ (Function.uncurry fun x z : P × M ↦ S.bs z.1 x.2) (y, y) := S.contMDiff_bs.comp (contMDiff_snd.fst.prodMk contMDiff_fst.snd) (y, y) apply ContMDiffAt.mfderiv (fun x z : P × M ↦ S.bs z.1 x.2) id this contMDiffAt_id (mod_cast le_top) diff --git a/SphereEversion/Global/ParametricityForFree.lean b/SphereEversion/Global/ParametricityForFree.lean index d125dff7..65fa455d 100644 --- a/SphereEversion/Global/ParametricityForFree.lean +++ b/SphereEversion/Global/ParametricityForFree.lean @@ -156,7 +156,7 @@ def FamilyFormalSol.uncurry (S : FamilyFormalSol IP P R) : FormalSol (R.relativi theorem FamilyFormalSol.uncurry_ϕ' (S : FamilyFormalSol IP P R) (p : P × M) : S.uncurry.ϕ p = - mfderiv IP I' (fun z ↦ S.bs z p.2) p.1 ∘L ContinuousLinearMap.fst ℝ EP E + + mfderiv% (fun z ↦ S.bs z p.2) p.1 ∘L ContinuousLinearMap.fst ℝ EP E + S.ϕ p.1 p.2 ∘L ContinuousLinearMap.snd ℝ EP E := S.toFamilyOneJetSec.uncurry_ϕ' p @@ -169,17 +169,15 @@ def FamilyOneJetSec.curry (S : FamilyOneJetSec (IP.prod I) (P × M) I' M' J N) : rintro ⟨⟨t, s⟩, x⟩ refine contMDiffAt_snd.oneJetBundle_mk (S.contMDiff_bs.comp contMDiff_prod_assoc _) ?_ have h1 : - ContMDiffAt ((J.prod IP).prod I) 𝓘(ℝ, EP × E →L[ℝ] E') ∞ - (inTangentCoordinates (IP.prod I) I' (fun p : (N × P) × M ↦ (p.1.2, p.2)) + CMDiffAt ∞ (inTangentCoordinates (IP.prod I) I' (fun p : (N × P) × M ↦ (p.1.2, p.2)) (fun p : (N × P) × M ↦ (S p.1.1).bs (p.1.2, p.2)) (fun p : (N × P) × M ↦ (S p.1.1).ϕ (p.1.2, p.2)) ((t, s), x)) ((t, s), x) := by apply (contMDiffAt_oneJetBundle.mp <| (S.contMDiff (t, (s, x))).comp ((t, s), x) (contMDiff_prod_assoc ((t, s), x))).2.2 have h2 : - ContMDiffAt ((J.prod IP).prod I) 𝓘(ℝ, E →L[ℝ] EP × E) ∞ - (inTangentCoordinates I (IP.prod I) Prod.snd (fun p : (N × P) × M ↦ (p.1.2, p.2)) - (fun p : (N × P) × M ↦ mfderiv I (IP.prod I) (fun x : M ↦ (p.1.2, x)) p.2) ((t, s), x)) + CMDiffAt ∞ (inTangentCoordinates I (IP.prod I) Prod.snd (fun p : (N × P) × M ↦ (p.1.2, p.2)) + (fun p : (N × P) × M ↦ mfderiv% (fun x : M ↦ (p.1.2, x)) p.2) ((t, s), x)) ((t, s), x) := by apply ContMDiffAt.mfderiv (fun (p : (N × P) × M) (x : M) ↦ (p.1.2, x)) Prod.snd diff --git a/SphereEversion/Global/Relation.lean b/SphereEversion/Global/Relation.lean index 1438ed24..1b68ffe7 100644 --- a/SphereEversion/Global/Relation.lean +++ b/SphereEversion/Global/Relation.lean @@ -385,13 +385,13 @@ theorem RelMfld.SatisfiesHPrincipleWith.bs {R : RelMfld I M IX X} {C : Set (P × (h : R.SatisfiesHPrincipleWith IP C ε) (𝓕₀ : FamilyFormalSol IP P R) (h2 : ∀ᶠ p : P × M near C, (𝓕₀ p.1).toOneJetSec.IsHolonomicAt p.2) : ∃ f : P → M → X, - (ContMDiff (IP.prod I) IX ∞ <| uncurry f) ∧ + (CMDiff ∞ (uncurry f)) ∧ (∀ᶠ p : P × M near C, f p.1 p.2 = 𝓕₀.bs p.1 p.2) ∧ (∀ p m, dist (f p m) ((𝓕₀ p).bs m) ≤ ε m) ∧ ∀ p m, oneJetExt I IX (f p) m ∈ R := by rcases h 𝓕₀ h2 with ⟨𝓕, _, h₂, h₃, h₄⟩ refine ⟨fun s ↦ (𝓕 (1, s)).bs, ?_, ?_, ?_, ?_⟩ · let j : C^∞⟮IP, P; 𝓘(ℝ, ℝ).prod IP, ℝ × P⟯ := - ⟨fun p ↦ (1, p), ContMDiff.prodMk contMDiff_const contMDiff_id⟩ + ⟨fun p ↦ (1, p), contMDiff_const.prodMk contMDiff_id⟩ rw [show (uncurry fun s ↦ (𝓕 (1, s)).bs) = Prod.snd ∘ π _ (OneJetSpace I IX) ∘ fun p : P × M ↦ 𝓕.reindex j p.1 p.2 diff --git a/SphereEversion/Global/SmoothEmbedding.lean b/SphereEversion/Global/SmoothEmbedding.lean index 1bdbb8a8..8062257f 100644 --- a/SphereEversion/Global/SmoothEmbedding.lean +++ b/SphereEversion/Global/SmoothEmbedding.lean @@ -86,7 +86,7 @@ variable [IsManifold I ∞ M] [IsManifold I' ∞ M'] /- Note that we are slightly abusing the fact that `TangentSpace I x` and `TangentSpace I (f.invFun (f x))` are both definitionally `E` below. -/ -def fderiv (x : M) : TangentSpace% x ≃L[𝕜] TangentSpace% (f x) := +def fderiv (x : M) : TangentSpace I x ≃L[𝕜] TangentSpace I' (f x) := have h₁ : MDiffAt f.invFun (f x) := ((f.contMDiffOn_inv (f x) (mem_range_self x)).mdifferentiableWithinAt (by simp)).mdifferentiableAt @@ -419,8 +419,8 @@ open Function /-- This is lemma `lem:smooth_updating` in the blueprint. -/ theorem contMDiff_update (f : M' → M → N) (g : M' → X → Y) {k : M' → M} {K : Set X} - (hK : IsClosed (φ '' K)) (hf : ContMDiff (IM'.prod IM) IN ∞ (uncurry f)) - (hg : ContMDiff (IM'.prod IX) IY ∞ (uncurry g)) (hk : CMDiff ∞ k) + (hK : IsClosed (φ '' K)) (hf : CMDiff ∞ (uncurry f)) + (hg : CMDiff ∞ (uncurry g)) (hk : CMDiff ∞ k) (hg' : ∀ y x, x ∉ K → f y (φ x) = ψ (g y x)) : CMDiff ∞ fun x ↦ update φ ψ (f x) (g x) (k x) := by have hK' : ∀ x, k x ∉ φ '' K → update φ ψ (f x) (g x) (k x) = f x (k x) := fun x hx ↦ diff --git a/SphereEversion/Global/TwistOneJetSec.lean b/SphereEversion/Global/TwistOneJetSec.lean index 6a82186c..542e9ea7 100644 --- a/SphereEversion/Global/TwistOneJetSec.lean +++ b/SphereEversion/Global/TwistOneJetSec.lean @@ -33,7 +33,7 @@ variable {f : N → J¹[𝕜, E, I, M, V]} -- todo: remove or use to prove `contMDiff_one_jet_eucl_bundle` theorem contMDiffAt_one_jet_eucl_bundle' {x₀ : N} : ContMDiffAt J (I.prod 𝓘(𝕜, E →L[𝕜] V)) ∞ f x₀ ↔ CMDiffAt ∞ (fun x ↦ (f x).1) x₀ ∧ - ContMDiffAt J 𝓘(𝕜, E →L[𝕜] V) ∞ (fun x ↦ show E →L[𝕜] V from + CMDiffAt ∞ (fun x ↦ show E →L[𝕜] V from (f x).2 ∘L (trivializationAt E (TangentSpace I : M → _) (f x₀).1).symmL 𝕜 (f x).1) x₀ := by simp_rw [contMDiffAt_hom_bundle, inCoordinates, Trivial.trivializationAt, Trivial.trivialization_continuousLinearMapAt] @@ -43,7 +43,7 @@ theorem contMDiffAt_one_jet_eucl_bundle' {x₀ : N} : theorem contMDiffAt_one_jet_eucl_bundle {x₀ : N} : ContMDiffAt J (I.prod 𝓘(𝕜, E →L[𝕜] V)) ∞ f x₀ ↔ CMDiffAt ∞ (fun x ↦ (f x).1) x₀ ∧ - ContMDiffAt J 𝓘(𝕜, E →L[𝕜] V) ∞ (fun x ↦ show E →L[𝕜] V from + CMDiffAt ∞ (fun x ↦ show E →L[𝕜] V from (f x).2 ∘L (trivializationAt E (TangentSpace I) (f x₀).proj).symmL 𝕜 (f x).proj) x₀ := by rw [contMDiffAt_hom_bundle, and_congr_right_iff] intro hf @@ -60,7 +60,7 @@ theorem contMDiffAt_one_jet_eucl_bundle {x₀ : N} : theorem ContMDiffAt.one_jet_eucl_bundle_mk' {f : N → M} {ϕ : N → E →L[𝕜] V} {x₀ : N} (hf : CMDiffAt ∞ f x₀) - (hϕ : ContMDiffAt J 𝓘(𝕜, E →L[𝕜] V) ∞ (fun x ↦ show E →L[𝕜] V from + (hϕ : CMDiffAt ∞ (fun x ↦ show E →L[𝕜] V from ϕ x ∘L (trivializationAt E (TangentSpace I : M → _) (f x₀)).symmL 𝕜 (f x)) x₀) : ContMDiffAt J (I.prod 𝓘(𝕜, E →L[𝕜] V)) ∞ (fun x ↦ Bundle.TotalSpace.mk (f x) (ϕ x) : N → J¹[𝕜, E, I, M, V]) x₀ := @@ -68,7 +68,7 @@ theorem ContMDiffAt.one_jet_eucl_bundle_mk' {f : N → M} {ϕ : N → E →L[ theorem ContMDiffAt.one_jet_eucl_bundle_mk {f : N → M} {ϕ : N → E →L[𝕜] V} {x₀ : N} (hf : CMDiffAt ∞ f x₀) - (hϕ : ContMDiffAt J 𝓘(𝕜, E →L[𝕜] V) ∞ (fun x ↦ show E →L[𝕜] V from + (hϕ : CMDiffAt ∞ (fun x ↦ show E →L[𝕜] V from ϕ x ∘L (trivializationAt E (TangentSpace I) (f x₀)).symmL 𝕜 (f x)) x₀) : ContMDiffAt J (I.prod 𝓘(𝕜, E →L[𝕜] V)) ∞ (fun x ↦ Bundle.TotalSpace.mk (f x) (ϕ x) : N → J¹[𝕜, E, I, M, V]) x₀ := @@ -208,7 +208,7 @@ theorem FamilyOneJetEuclSec.contMDiff (s : FamilyOneJetEuclSec I M V J N) : variable {V'} -def familyJoin {f : N × M → V} (hf : ContMDiff (J.prod I) 𝓘(ℝ, V) ∞ f) +def familyJoin {f : N × M → V} (hf : CMDiff ∞ f) (s : FamilyOneJetEuclSec I M V J N) : FamilyOneJetSec I M 𝓘(ℝ, V) V J N where bs n m := (incl I M V (s (n, m), f (n, m))).1.2 @@ -219,9 +219,8 @@ def familyJoin {f : N × M → V} (hf : ContMDiff (J.prod I) 𝓘(ℝ, V) ∞ f) set_option backward.isDefEq.respectTransparency false in def familyTwist (s : OneJetEuclSec I M V) (i : N × M → V →L[ℝ] V') - (hi : ∀ x₀ : N × M, ContMDiffAt (J.prod I) 𝓘(ℝ, V →L[ℝ] V') ∞ i x₀) : - FamilyOneJetEuclSec I M V' J N - where + (hi : ∀ x₀ : N × M, CMDiffAt ∞ i x₀) : + FamilyOneJetEuclSec I M V' J N where toFun p := ⟨p.2, (i p).comp (s p.2).2⟩ is_sec' p := rfl contMDiff' := by diff --git a/SphereEversion/ToMathlib/ExistsOfConvex.lean b/SphereEversion/ToMathlib/ExistsOfConvex.lean index eeb90b53..9113be1b 100644 --- a/SphereEversion/ToMathlib/ExistsOfConvex.lean +++ b/SphereEversion/ToMathlib/ExistsOfConvex.lean @@ -110,10 +110,6 @@ variable {H₁ M₁ H₂ M₂ : Type*} [TopologicalSpace H₂] (I₂ : ModelWithCorners ℝ E₂ H₂) [TopologicalSpace M₂] [ChartedSpace H₂ M₂] [IsManifold I₂ ∞ M₂] -@[inherit_doc] local notation "𝓒" => ContMDiff (I₁.prod I₂) 𝓘(ℝ, F) - -@[inherit_doc] local notation "𝓒_on" => ContMDiffOn (I₁.prod I₂) 𝓘(ℝ, F) - omit [FiniteDimensional ℝ E₁] [FiniteDimensional ℝ E₂] [IsManifold I₁ ∞ M₁] [IsManifold I₂ ∞ M₂] in theorem reallyConvex_contMDiffAtProd {x : M₁} (n : ℕ∞) : @@ -134,8 +130,8 @@ omit [FiniteDimensional ℝ E₂] [IsManifold I₂ ∞ M₂] in theorem exists_contMDiff_of_convex₂ {P : M₁ → (M₂ → F) → Prop} [SigmaCompactSpace M₁] [T2Space M₁] (hP : ∀ x, Convex ℝ {f | P x f}) {n : ℕ∞} (hP' : ∀ x : M₁, ∃ U ∈ 𝓝 x, ∃ f : M₁ → M₂ → F, - 𝓒_on n (uncurry f) (U ×ˢ (univ : Set M₂)) ∧ ∀ y ∈ U, P y (f y)) : - ∃ f : M₁ → M₂ → F, 𝓒 n (uncurry f) ∧ ∀ x, P x (f x) := by + CMDiff[U ×ˢ (univ : Set M₂)] n (uncurry f) ∧ ∀ y ∈ U, P y (f y)) : + ∃ f : M₁ → M₂ → F, CMDiff n (uncurry f) ∧ ∀ x, P x (f x) := by let PP : (Σ x : M₁, Germ (𝓝 x) (M₂ → F)) → Prop := fun p ↦ p.2.ContMDiffAtProd I₁ I₂ n ∧ P p.1 p.2.value have hPP : ∀ x : M₁, ReallyConvex (smoothGerm I₁ x) {φ | PP ⟨x, φ⟩} := fun x ↦ by