From c8247c688213c7828fb75d47e9f8792ce0f57919 Mon Sep 17 00:00:00 2001 From: sgouezel Date: Tue, 14 Jan 2025 14:45:07 +0100 Subject: [PATCH] fix --- SphereEversion.lean | 3 +- SphereEversion/Global/Gromov.lean | 14 +- SphereEversion/Global/Immersion.lean | 39 +++-- SphereEversion/Global/Localisation.lean | 12 +- SphereEversion/Global/LocalisationData.lean | 16 +- .../Global/LocalizedConstruction.lean | 6 +- SphereEversion/Global/OneJetBundle.lean | 163 +++++++++--------- SphereEversion/Global/OneJetSec.lean | 50 +++--- .../Global/ParametricityForFree.lean | 30 ++-- SphereEversion/Global/Relation.lean | 67 +++---- SphereEversion/Global/SmoothEmbedding.lean | 42 ++--- SphereEversion/Global/TwistOneJetSec.lean | 54 +++--- SphereEversion/Indexing.lean | 1 + SphereEversion/InductiveConstructions.lean | 2 +- SphereEversion/Local/DualPair.lean | 3 +- SphereEversion/Local/HPrinciple.lean | 6 +- SphereEversion/Local/OneJet.lean | 3 +- .../Local/ParametricHPrinciple.lean | 8 +- SphereEversion/Local/SphereEversion.lean | 6 +- SphereEversion/Loops/DeltaMollifier.lean | 4 +- SphereEversion/Loops/Exists.lean | 29 ++-- SphereEversion/Loops/Reparametrization.lean | 5 +- SphereEversion/Loops/Surrounding.lean | 5 +- SphereEversion/Main.lean | 11 +- SphereEversion/Notations.lean | 4 +- .../ToMathlib/Algebra/Periodic.lean | 3 +- .../ToMathlib/Analysis/Calculus.lean | 12 +- SphereEversion/ToMathlib/Analysis/CutOff.lean | 4 +- SphereEversion/ToMathlib/ExistsOfConvex.lean | 20 +-- .../Geometry/Manifold/Algebra/SmoothGerm.lean | 46 ++--- .../Geometry/Manifold/Immersion.lean | 8 +- .../Geometry/Manifold/MiscManifold.lean | 18 +- .../Manifold/SmoothManifoldWithCorners.lean | 2 +- .../ToMathlib/Topology/Algebra/Module.lean | 2 +- .../ToMathlib/Topology/HausdorffDistance.lean | 36 ---- SphereEversion/ToMathlib/Topology/Misc.lean | 1 + .../ToMathlib/Topology/Paracompact.lean | 2 +- SphereEversion/ToMathlib/Topology/Path.lean | 2 +- .../Separation/{Basic.lean => Hausdorff.lean} | 3 +- .../Unused/GeometryManifoldMisc.lean | 20 +-- lake-manifest.json | 30 ++-- lean-toolchain | 2 +- 42 files changed, 382 insertions(+), 412 deletions(-) delete mode 100644 SphereEversion/ToMathlib/Topology/HausdorffDistance.lean rename SphereEversion/ToMathlib/Topology/Separation/{Basic.lean => Hausdorff.lean} (94%) diff --git a/SphereEversion.lean b/SphereEversion.lean index 09232630..5537275e 100644 --- a/SphereEversion.lean +++ b/SphereEversion.lean @@ -57,9 +57,8 @@ import SphereEversion.ToMathlib.Order.Filter.Basic import SphereEversion.ToMathlib.Partition import SphereEversion.ToMathlib.SmoothBarycentric import SphereEversion.ToMathlib.Topology.Algebra.Module -import SphereEversion.ToMathlib.Topology.HausdorffDistance import SphereEversion.ToMathlib.Topology.Misc import SphereEversion.ToMathlib.Topology.Paracompact import SphereEversion.ToMathlib.Topology.Path -import SphereEversion.ToMathlib.Topology.Separation.Basic +import SphereEversion.ToMathlib.Topology.Separation.Hausdorff import SphereEversion.ToMathlib.Unused.Fin diff --git a/SphereEversion/Global/Gromov.lean b/SphereEversion/Global/Gromov.lean index 84749560..15764426 100644 --- a/SphereEversion/Global/Gromov.lean +++ b/SphereEversion/Global/Gromov.lean @@ -14,19 +14,17 @@ noncomputable section open Set Filter ModelWithCorners Metric -open scoped Topology Manifold - -local notation "∞" => (⊤ : ℕ∞) +open scoped Topology Manifold ContDiff variable {EM : Type*} [NormedAddCommGroup EM] [NormedSpace ℝ EM] [FiniteDimensional ℝ EM] {HM : Type*} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} [Boundaryless IM] - {M : Type*} [TopologicalSpace M] [ChartedSpace HM M] [SmoothManifoldWithCorners IM M] + {M : Type*} [TopologicalSpace M] [ChartedSpace HM M] [IsManifold IM ∞ M] [T2Space M] [SigmaCompactSpace M] {EX : Type*} [NormedAddCommGroup EX] [NormedSpace ℝ EX] [FiniteDimensional ℝ EX] {HX : Type*} [TopologicalSpace HX] {IX : ModelWithCorners ℝ EX HX} [Boundaryless IX] -- note: X is a metric space {X : Type*} - [MetricSpace X] [ChartedSpace HX X] [SmoothManifoldWithCorners IX X] [SigmaCompactSpace X] + [MetricSpace X] [ChartedSpace HX X] [IsManifold IX ∞ X] [SigmaCompactSpace X] {R : RelMfld IM M IX X} {A : Set M} {δ : M → ℝ} @[inherit_doc] local notation "J¹" => OneJetBundle IM M IX X @@ -312,7 +310,7 @@ theorem RelMfld.Ample.satisfiesHPrinciple (hRample : R.Ample) (hRopen : IsOpen R _ = τ x := by simp [F, η] · rw [union_assoc, Eventually.union_nhdsSet] at hF'hol replace hF'hol := hF'hol.2 - simp_rw [← L.iUnion_succ'] at hF'hol + simp_rw [L.iUnion_succ'] exact hF'hol · exact F'.smooth · intro t x hx @@ -342,7 +340,7 @@ theorem RelMfld.Ample.satisfiesHPrinciple (hRample : R.Ample) (hRopen : IsOpen R variable {EP : Type*} [NormedAddCommGroup EP] [NormedSpace ℝ EP] [FiniteDimensional ℝ EP] {HP : Type*} [TopologicalSpace HP] {IP : ModelWithCorners ℝ EP HP} [Boundaryless IP] - {P : Type*} [TopologicalSpace P] [ChartedSpace HP P] [SmoothManifoldWithCorners IP P] + {P : Type*} [TopologicalSpace P] [ChartedSpace HP P] [IsManifold IP ∞ P] [SigmaCompactSpace P] [T2Space P] {C : Set (P × M)} /- @@ -364,7 +362,7 @@ theorem RelMfld.Ample.satisfiesHPrincipleWith (hRample : R.Ample) (hRopen : IsOp variable {E' : Type*} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] {H' : Type*} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} [I'.Boundaryless] {M' : Type*} [TopologicalSpace M'] [ChartedSpace H' M'] - [SmoothManifoldWithCorners I' M'] [SigmaCompactSpace M'] [T2Space M'] + [IsManifold I' ∞ M'] [SigmaCompactSpace M'] [T2Space M'] /- Since every (σ-compact) manifold is metrizable, the metric space assumption can be removed. diff --git a/SphereEversion/Global/Immersion.lean b/SphereEversion/Global/Immersion.lean index 2033073f..26644f85 100644 --- a/SphereEversion/Global/Immersion.lean +++ b/SphereEversion/Global/Immersion.lean @@ -13,19 +13,20 @@ open Metric Module Set Function LinearMap Filter ContinuousLinearMap open scoped Manifold Topology -local notation "∞" => (⊤ : ℕ∞) +-- Can't open ContDiff because `ω` conflicts with the notation for orientation below +local notation "∞" => ((⊤ : ℕ∞) : WithTop ℕ∞) section General variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type*} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type*} [TopologicalSpace M] - [ChartedSpace H M] [SmoothManifoldWithCorners I M] + [ChartedSpace H M] [IsManifold I ∞ M] {E' : Type*} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type*} [TopologicalSpace H'] (I' : ModelWithCorners ℝ E' H') - {M' : Type*} [TopologicalSpace M'] [ChartedSpace H' M'] [SmoothManifoldWithCorners I' M'] + {M' : Type*} [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' ∞ M'] {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type*} [TopologicalSpace G] (J : ModelWithCorners ℝ F G) - (N : Type*) [TopologicalSpace N] [ChartedSpace G N] [SmoothManifoldWithCorners J N] + (N : Type*) [TopologicalSpace N] [ChartedSpace G N] [IsManifold J ∞ N] @[inherit_doc] local notation "TM" => TangentSpace I @[inherit_doc] local notation "TM'" => TangentSpace I' @@ -37,7 +38,7 @@ variable (M M') in def immersionRel : RelMfld I M I' M' := {σ | Injective σ.2} -omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] in +omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] in @[simp] theorem mem_immersionRel_iff {σ : OneJetBundle I M I' M'} : σ ∈ immersionRel I M I' M' ↔ Injective (σ.2 : TangentSpace I _ →L[ℝ] TangentSpace I' _) := @@ -67,7 +68,7 @@ theorem immersionRel_open [FiniteDimensional ℝ E] : IsOpen (immersionRel I M I · infer_instance · infer_instance -omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] in +omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] in @[simp] theorem immersionRel_slice_eq {m : M} {m' : M'} {p : DualPair <| TangentSpace I m} {φ : TangentSpace I m →L[ℝ] TangentSpace I' m'} (hφ : Injective φ) : @@ -76,7 +77,7 @@ theorem immersionRel_slice_eq {m : M} {m' : M'} {p : DualPair <| TangentSpace I variable [FiniteDimensional ℝ E] [FiniteDimensional ℝ E'] -omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] in +omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] in theorem immersionRel_ample (h : finrank ℝ E < finrank ℝ E') : (immersionRel I M I' M').Ample := by rw [RelMfld.ample_iff] rintro ⟨⟨m, m'⟩, φ : TangentSpace I m →L[ℝ] TangentSpace I' m'⟩ (p : DualPair (TangentSpace I m)) @@ -97,13 +98,13 @@ section Generalbis variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type*} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) [I.Boundaryless] - {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] + {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M] {E' : Type*} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] {H' : Type*} [TopologicalSpace H'] (I' : ModelWithCorners ℝ E' H') [I'.Boundaryless] - {M' : Type*} [MetricSpace M'] [ChartedSpace H' M'] [SmoothManifoldWithCorners I' M'] + {M' : Type*} [MetricSpace M'] [ChartedSpace H' M'] [IsManifold I' ∞ M'] {EP : Type*} [NormedAddCommGroup EP] [NormedSpace ℝ EP] [FiniteDimensional ℝ EP] {HP : Type*} [TopologicalSpace HP] {IP : ModelWithCorners ℝ EP HP} [IP.Boundaryless] - {P : Type*} [TopologicalSpace P] [ChartedSpace HP P] [SmoothManifoldWithCorners IP P] + {P : Type*} [TopologicalSpace P] [ChartedSpace HP P] [IsManifold IP ∞ P] {C : Set (P × M)} {ε : M → ℝ} variable (M M' IP P) @@ -125,17 +126,17 @@ variable {n : ℕ} (E : Type*) [NormedAddCommGroup E] [InnerProductSpace ℝ E] /-- The inclusion of `𝕊^n` into `ℝ^{n+1}` is an immersion. -/ theorem immersion_inclusion_sphere : Immersion (𝓡 n) 𝓘(ℝ, E) - (fun x : sphere (0 : E) 1 ↦ (x : E)) ⊤ where - contMDiff := contMDiff_coe_sphere + (fun x : sphere (0 : E) 1 ↦ (x : E)) ∞ where + contMDiff := contMDiff_coe_sphere.of_le le_top diff_injective := mfderiv_coe_sphere_injective /-- The antipodal map on `𝕊^n ⊆ ℝ^{n+1}` is an immersion. -/ theorem immersion_antipodal_sphere : Immersion (𝓡 n) 𝓘(ℝ, E) - (fun x : sphere (0 : E) 1 ↦ -(x : E)) ⊤ where + (fun x : sphere (0 : E) 1 ↦ -(x : E)) ∞ where contMDiff := -- Write this as the composition of `coe_sphere` and the antipodal map on `E`. -- The other direction elaborates much worse. - (contDiff_neg.contMDiff).comp contMDiff_coe_sphere + (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) rw [mfderiv_neg] @@ -167,12 +168,12 @@ theorem smooth_bs : fun p : ℝ × (sphere (0 : E) 1) ↦ (1 - p.1) • (p.2 : E) + p.1 • -(p.2: E) := by refine (ContMDiff.smul ?_ ?_).add (contMDiff_fst.smul ?_) · exact (contDiff_const.sub contDiff_id).contMDiff.comp contMDiff_fst - · exact contMDiff_coe_sphere.comp contMDiff_snd - · exact (contDiff_neg.contMDiff.comp contMDiff_coe_sphere).comp contMDiff_snd + · exact (contMDiff_coe_sphere.of_le le_top).comp contMDiff_snd + · exact (contDiff_neg.contMDiff.comp (contMDiff_coe_sphere.of_le le_top)).comp contMDiff_snd def formalEversionAux : FamilyOneJetSec (𝓡 2) 𝕊² 𝓘(ℝ, E) E 𝓘(ℝ, ℝ) ℝ := familyJoin (smooth_bs E) <| - familyTwist (drop (oneJetExtSec ⟨((↑) : 𝕊² → E), contMDiff_coe_sphere⟩)) + familyTwist (drop (oneJetExtSec ⟨((↑) : 𝕊² → E), contMDiff_coe_sphere.of_le le_top⟩)) (fun p : ℝ × 𝕊² ↦ ω.rot (p.1, p.2)) (by intro p @@ -180,7 +181,7 @@ def formalEversionAux : FamilyOneJetSec (𝓡 2) 𝕊² 𝓘(ℝ, E) E 𝓘(ℝ, refine ((ω.contDiff_rot ?_).of_le le_top).contMDiffAt exact ne_zero_of_mem_unit_sphere p.2 apply this.comp p (f := fun (p : ℝ × sphere 0 1) ↦ (p.1, (p.2 : E))) - apply contMDiff_fst.prod_mk_space (contMDiff_coe_sphere.comp contMDiff_snd)) + apply contMDiff_fst.prod_mk_space ((contMDiff_coe_sphere.of_le le_top).comp contMDiff_snd)) /-- A formal eversion of a two-sphere into its ambient Euclidean space. -/ def formalEversionAux2 : HtpyFormalSol 𝓡_imm := @@ -309,7 +310,7 @@ theorem sphere_eversion : ∃ f : ℝ → 𝕊² → E, ContMDiff (𝓘(ℝ, ℝ).prod (𝓡 2)) 𝓘(ℝ, E) ∞ ↿f ∧ (f 0 = fun x : 𝕊² ↦ (x : E)) ∧ (f 1 = fun x : 𝕊² ↦ -(x : E)) ∧ - ∀ t, Immersion (𝓡 2) 𝓘(ℝ, E) (f t) ⊤ := by + ∀ t, Immersion (𝓡 2) 𝓘(ℝ, E) (f t) ∞ := by classical let ω : Orientation ℝ E (Fin 3) := ((stdOrthonormalBasis _ _).reindex <| diff --git a/SphereEversion/Global/Localisation.lean b/SphereEversion/Global/Localisation.lean index 2611165b..2941b7b6 100644 --- a/SphereEversion/Global/Localisation.lean +++ b/SphereEversion/Global/Localisation.lean @@ -11,7 +11,7 @@ is about embedding any manifold into another one). noncomputable section -open scoped Topology Manifold +open scoped Topology Manifold ContDiff open Set ContinuousLinearMap section Loc @@ -112,10 +112,10 @@ end Unloc universe u₁ u₂ u₃ u₄ u₅ u₆ variable {E : Type u₁} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u₂} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) - (M : Type u₃) [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] + (M : Type u₃) [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M] {E' : Type u₄} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u₅} [TopologicalSpace H'] (I' : ModelWithCorners ℝ E' H') - (M' : Type u₆) [MetricSpace M'] [ChartedSpace H' M'] [SmoothManifoldWithCorners I' M'] + (M' : Type u₆) [MetricSpace M'] [ChartedSpace H' M'] [IsManifold I' ∞ M'] {R : RelMfld I M I' M'} /-- A pair of charts together with a compact subset of the first vector space. -/ @@ -147,7 +147,7 @@ structure ChartPair.compat' (F : FormalSol R) (𝓕 : (R.localize p.φ p.ψ).rel def RelLoc.HtpyFormalSol.unloc : _root_.HtpyFormalSol (RelMfld.localize p.φ p.ψ R) := { 𝓕.toHtpyJetSec.unloc with is_sol' := 𝓕.is_sol } -omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] in +omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] in theorem RelLoc.HtpyFormalSol.unloc_congr {𝓕 𝓕' : (R.localize p.φ p.ψ).relLoc.HtpyFormalSol} {t t' x} (h : 𝓕 t x = 𝓕' t' x) : 𝓕.unloc p t x = 𝓕'.unloc p t' x := by ext1 @@ -157,7 +157,7 @@ theorem RelLoc.HtpyFormalSol.unloc_congr {𝓕 𝓕' : (R.localize p.φ p.ψ).re · change (𝓕 t x).2 = (𝓕' t' x).2 rw [h] -omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] in +omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] in theorem RelLoc.HtpyFormalSol.unloc_congr_const {𝓕 : (R.localize p.φ p.ψ).relLoc.HtpyFormalSol} {𝓕' : (R.localize p.φ p.ψ).relLoc.FormalSol} {t x} (h : 𝓕 t x = 𝓕' x) : 𝓕.unloc p t x = 𝓕'.unloc x := by @@ -168,7 +168,7 @@ theorem RelLoc.HtpyFormalSol.unloc_congr_const {𝓕 : (R.localize p.φ p.ψ).re · change (𝓕 t x).2 = (𝓕' x).2 rw [h] -omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] in +omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] in theorem RelLoc.HtpyFormalSol.unloc_congr' {𝓕 𝓕' : (R.localize p.φ p.ψ).relLoc.HtpyFormalSol} {t t'} (h : 𝓕 t = 𝓕' t') : 𝓕.unloc p t = 𝓕'.unloc p t' := by apply FormalSol.coe_inj diff --git a/SphereEversion/Global/LocalisationData.lean b/SphereEversion/Global/LocalisationData.lean index e01f8847..1af084e2 100644 --- a/SphereEversion/Global/LocalisationData.lean +++ b/SphereEversion/Global/LocalisationData.lean @@ -3,7 +3,7 @@ import SphereEversion.Global.SmoothEmbedding noncomputable section -open scoped Manifold +open scoped Manifold ContDiff open Set Metric @@ -12,10 +12,10 @@ section variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) - {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] + {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M] {E' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type*} [TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H') - {M' : Type*} [TopologicalSpace M'] [ChartedSpace H' M'] [SmoothManifoldWithCorners I' M'] + {M' : Type*} [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' ∞ M'] /-- Definition `def:localisation_data`. -/ structure LocalisationData (f : M → M') where @@ -44,7 +44,7 @@ abbrev ψj : IndexType ld.N → OpenSmoothEmbedding 𝓘(𝕜, E') E' I' M' := def ι (L : LocalisationData I I' f) := IndexType L.N -omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] in +omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] in theorem iUnion_succ' {β : Type*} (s : ld.ι → Set β) (i : IndexType ld.N) : (⋃ j ≤ i, s j) = (⋃ j < i, s j) ∪ s i := by simp only [(fun _ ↦ le_iff_lt_or_eq : ∀ j, j ≤ i ↔ j < i ∨ j = i)] @@ -64,11 +64,11 @@ open ModelWithCorners variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {M : Type*} [TopologicalSpace M] [SigmaCompactSpace M] [LocallyCompactSpace M] [T2Space M] {H : Type*} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) [Boundaryless I] [Nonempty M] - [ChartedSpace H M] [SmoothManifoldWithCorners I M] + [ChartedSpace H M] [IsManifold I ∞ M] (E' : Type*) [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] {H' : Type*} [TopologicalSpace H'] (I' : ModelWithCorners ℝ E' H') [Boundaryless I'] {M' : Type*} [MetricSpace M'] [SigmaCompactSpace M'] [LocallyCompactSpace M'] - [Nonempty M'] [ChartedSpace H' M'] [SmoothManifoldWithCorners I' M'] + [Nonempty M'] [ChartedSpace H' M'] [IsManifold I' ∞ M'] variable (M') @@ -124,8 +124,8 @@ variable {E E' I I'} section omit [FiniteDimensional ℝ E] [SigmaCompactSpace M] [LocallyCompactSpace M] [T2Space M] - [I.Boundaryless] [Nonempty M] [SmoothManifoldWithCorners I M] [I'.Boundaryless] - [SigmaCompactSpace M'] [LocallyCompactSpace M'] [Nonempty M'] [SmoothManifoldWithCorners I' M'] + [I.Boundaryless] [Nonempty M] [IsManifold I ∞ M] [I'.Boundaryless] + [SigmaCompactSpace M'] [LocallyCompactSpace M'] [Nonempty M'] [IsManifold I' ∞ M'] /-- Lemma `lem:localisation_stability`. -/ theorem localisation_stability {f : M → M'} (ld : LocalisationData I I' f) : diff --git a/SphereEversion/Global/LocalizedConstruction.lean b/SphereEversion/Global/LocalizedConstruction.lean index 1656e7a4..12d8fa96 100644 --- a/SphereEversion/Global/LocalizedConstruction.lean +++ b/SphereEversion/Global/LocalizedConstruction.lean @@ -5,15 +5,15 @@ noncomputable section open Set Filter ModelWithCorners Metric -open scoped Topology Manifold +open scoped Topology Manifold ContDiff variable {EM : Type*} [NormedAddCommGroup EM] [NormedSpace ℝ EM] [FiniteDimensional ℝ EM] {HM : Type*} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} - {M : Type*} [TopologicalSpace M] [ChartedSpace HM M] [SmoothManifoldWithCorners IM M] + {M : Type*} [TopologicalSpace M] [ChartedSpace HM M] [IsManifold IM ∞ M] [T2Space M] {EX : Type*} [NormedAddCommGroup EX] [NormedSpace ℝ EX] [FiniteDimensional ℝ EX] {HX : Type*} [TopologicalSpace HX] {IX : ModelWithCorners ℝ EX HX} - {X : Type*} [MetricSpace X] [ChartedSpace HX X] [SmoothManifoldWithCorners IX X] + {X : Type*} [MetricSpace X] [ChartedSpace HX X] [IsManifold IX ∞ X] theorem OpenSmoothEmbedding.improve_formalSol (φ : OpenSmoothEmbedding 𝓘(ℝ, EM) EM IM M) (ψ : OpenSmoothEmbedding 𝓘(ℝ, EX) EX IX X) {R : RelMfld IM M IX X} (hRample : R.Ample) diff --git a/SphereEversion/Global/OneJetBundle.lean b/SphereEversion/Global/OneJetBundle.lean index b113f807..bb8d08e2 100644 --- a/SphereEversion/Global/OneJetBundle.lean +++ b/SphereEversion/Global/OneJetBundle.lean @@ -35,65 +35,65 @@ noncomputable section open Filter Set Equiv Bundle ContinuousLinearMap -open scoped Manifold Topology Bundle +open scoped Manifold Topology Bundle ContDiff variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) - {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] + {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M] {E' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type*} [TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H') - {M' : Type*} [TopologicalSpace M'] [ChartedSpace H' M'] [SmoothManifoldWithCorners I' M'] + {M' : Type*} [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' ∞ M'] {E'' : Type*} [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H'' : Type*} [TopologicalSpace H''] {I'' : ModelWithCorners 𝕜 E'' H''} - {M'' : Type*} [TopologicalSpace M''] [ChartedSpace H'' M''] [SmoothManifoldWithCorners I'' M''] + {M'' : Type*} [TopologicalSpace M''] [ChartedSpace H'' M''] [IsManifold I'' ∞ M''] {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type*} [TopologicalSpace G] (J : ModelWithCorners 𝕜 F G) {N : Type*} [TopologicalSpace N] [ChartedSpace G N] {F' : Type*} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {G' : Type*} [TopologicalSpace G'] (J' : ModelWithCorners 𝕜 F' G') - {N' : Type*} [TopologicalSpace N'] [ChartedSpace G' N'] [SmoothManifoldWithCorners J' N'] + {N' : Type*} [TopologicalSpace N'] [ChartedSpace G' N'] [IsManifold J' ∞ N'] {E₂ : Type*} [NormedAddCommGroup E₂] [NormedSpace 𝕜 E₂] {H₂ : Type*} [TopologicalSpace H₂] {I₂ : ModelWithCorners 𝕜 E₂ H₂} - {M₂ : Type*} [TopologicalSpace M₂] [ChartedSpace H₂ M₂] [SmoothManifoldWithCorners I₂ M₂] + {M₂ : Type*} [TopologicalSpace M₂] [ChartedSpace H₂ M₂] [IsManifold I₂ ∞ M₂] {E₃ : Type*} [NormedAddCommGroup E₃] [NormedSpace 𝕜 E₃] {H₃ : Type*} [TopologicalSpace H₃] {I₃ : ModelWithCorners 𝕜 E₃ H₃} - {M₃ : Type*} [TopologicalSpace M₃] [ChartedSpace H₃ M₃] [SmoothManifoldWithCorners I₃ M₃] + {M₃ : Type*} [TopologicalSpace M₃] [ChartedSpace H₃ M₃] [IsManifold I₃ ∞ M₃] @[inherit_doc] local notation "σ" => RingHom.id 𝕜 instance deleteme1 : ∀ x : M × M', - Module 𝕜 (((ContMDiffMap.fst : C^⊤⟮I.prod I', M × M'; I, M⟯) *ᵖ (TangentSpace I)) x) := by + Module 𝕜 (((ContMDiffMap.fst : C^∞⟮I.prod I', M × M'; I, M⟯) *ᵖ (TangentSpace I)) x) := by infer_instance instance deleteme2 : ∀ x : M × M', - Module 𝕜 (((ContMDiffMap.snd : C^⊤⟮I.prod I', M × M'; I', M'⟯) *ᵖ (TangentSpace I')) x) := by + Module 𝕜 (((ContMDiffMap.snd : C^∞⟮I.prod I', M × M'; I', M'⟯) *ᵖ (TangentSpace I')) x) := by infer_instance instance deleteme3 : - VectorBundle 𝕜 E ((ContMDiffMap.fst : C^⊤⟮I.prod I', M × M'; I, M⟯) *ᵖ (TangentSpace I)) := by + VectorBundle 𝕜 E ((ContMDiffMap.fst : C^∞⟮I.prod I', M × M'; I, M⟯) *ᵖ (TangentSpace I)) := by infer_instance instance deleteme4 : - VectorBundle 𝕜 E' ((ContMDiffMap.snd : C^⊤⟮I.prod I', M × M'; I', M'⟯) *ᵖ (TangentSpace I')) := by + VectorBundle 𝕜 E' ((ContMDiffMap.snd : C^∞⟮I.prod I', M × M'; I', M'⟯) *ᵖ (TangentSpace I')) := by infer_instance instance deleteme5 : - SmoothVectorBundle E ((ContMDiffMap.fst : C^⊤⟮I.prod I', M × M'; I, M⟯) *ᵖ (TangentSpace I)) + ContMDiffVectorBundle ∞ E ((ContMDiffMap.fst : C^∞⟮I.prod I', M × M'; I, M⟯) *ᵖ (TangentSpace I)) (I.prod I') := by infer_instance instance deleteme6 : - SmoothVectorBundle E' ((ContMDiffMap.snd : C^⊤⟮I.prod I', M × M'; I', M'⟯) *ᵖ (TangentSpace I')) + ContMDiffVectorBundle ∞ E' ((ContMDiffMap.snd : C^∞⟮I.prod I', M × M'; I', M'⟯) *ᵖ (TangentSpace I')) (I.prod I') := by infer_instance set_option linter.unusedVariables false in /-- The fibers of the one jet-bundle. -/ def OneJetSpace (p : M × M') : Type _ := Bundle.ContinuousLinearMap σ - ((ContMDiffMap.fst : C^⊤⟮I.prod I', M × M'; I, M⟯) *ᵖ (TangentSpace I)) - ((ContMDiffMap.snd : C^⊤⟮I.prod I', M × M'; I', M'⟯) *ᵖ (TangentSpace I')) p + ((ContMDiffMap.fst : C^∞⟮I.prod I', M × M'; I, M⟯) *ᵖ (TangentSpace I)) + ((ContMDiffMap.snd : C^∞⟮I.prod I', M × M'; I', M'⟯) *ᵖ (TangentSpace I')) p instance (p : M × M') : TopologicalSpace (OneJetSpace I I' p) := by delta OneJetSpace @@ -130,7 +130,7 @@ variable {I I' M M'} @[inherit_doc] local notation "HJ" => ModelProd (ModelProd H H') (E →L[𝕜] E') -omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] in +omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] in @[ext] theorem OneJetBundle.ext {x y : J¹MM'} (h : x.1.1 = y.1.1) (h' : x.1.2 = y.1.2) (h'' : x.2 = y.2) : x = y := by @@ -166,7 +166,7 @@ instance : VectorBundle 𝕜 (E →L[𝕜] E') FJ¹MM' := by delta OneJetSpace infer_instance -instance : SmoothVectorBundle (E →L[𝕜] E') (OneJetSpace I I' : M × M' → Type _) (I.prod I') := by +instance : ContMDiffVectorBundle ∞ (E →L[𝕜] E') (OneJetSpace I I' : M × M' → Type _) (I.prod I') := by delta OneJetSpace infer_instance @@ -174,8 +174,8 @@ instance : ChartedSpace HJ J¹MM' := by delta OneJetSpace OneJetBundle infer_instance -instance : SmoothManifoldWithCorners ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) J¹MM' := by - apply Bundle.TotalSpace.smoothManifoldWithCorners +instance : IsManifold ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ∞ J¹MM' := by + apply Bundle.TotalSpace.isManifold end OneJetBundleInstances @@ -323,16 +323,16 @@ theorem oneJetBundle_chart_target (x₀ : J¹MM') : section Maps theorem contMDiff_oneJetBundle_proj : - ContMDiff ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) (I.prod I') ⊤ (π (E →L[𝕜] E') FJ¹MM') := by + ContMDiff ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) (I.prod I') ∞ (π (E →L[𝕜] E') FJ¹MM') := by apply contMDiff_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 := + (hf : ContMDiff J ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ∞ f) : ContMDiff J (I.prod I') ∞ 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₀ := + (hf : ContMDiffAt J ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ∞ f x₀) : + ContMDiffAt J (I.prod I') ∞ (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. -/ @@ -340,23 +340,23 @@ theorem ContMDiffAt.oneJetBundle_proj {f : N → J¹MM'} {x₀ : N} def OneJetBundle.mk (x : M) (y : M') (f : OneJetSpace I I' (x, y)) : J¹MM' := ⟨(x, y), f⟩ -omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] in +omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] in @[simp, mfld_simps] theorem oneJetBundle_mk_fst {x : M} {y : M'} {f : OneJetSpace I I' (x, y)} : (OneJetBundle.mk x y f).1 = (x, y) := rfl -omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] in +omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] in @[simp, mfld_simps] theorem oneJetBundle_mk_snd {x : M} {y : M'} {f : OneJetSpace I I' (x, y)} : (OneJetBundle.mk x y f).2 = f := rfl theorem contMDiffAt_oneJetBundle {f : N → J¹MM'} {x₀ : N} : - ContMDiffAt J ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ⊤ f x₀ ↔ - ContMDiffAt J I ⊤ (fun x ↦ (f x).1.1) x₀ ∧ - ContMDiffAt J I' ⊤ (fun x ↦ (f x).1.2) x₀ ∧ - ContMDiffAt J 𝓘(𝕜, E →L[𝕜] E') ⊤ + ContMDiffAt J ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ∞ f x₀ ↔ + ContMDiffAt J I ∞ (fun x ↦ (f x).1.1) x₀ ∧ + ContMDiffAt J I' ∞ (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 simp_rw [Bundle.contMDiffAt_totalSpace, contMDiffAt_prod_iff, and_assoc, @@ -364,16 +364,16 @@ theorem contMDiffAt_oneJetBundle {f : N → J¹MM'} {x₀ : N} : rfl 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')) ⊤ + ContMDiffAt J ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ∞ (fun x ↦ OneJetBundle.mk (f x) (g x) (ϕ x) : N → J¹MM') x₀ ↔ - ContMDiffAt J I ⊤ f x₀ ∧ - ContMDiffAt J I' ⊤ g x₀ ∧ ContMDiffAt J 𝓘(𝕜, E →L[𝕜] E') ⊤ (inTangentCoordinates I I' f g ϕ x₀) x₀ := + ContMDiffAt J I ∞ f x₀ ∧ + ContMDiffAt J I' ∞ g x₀ ∧ ContMDiffAt J 𝓘(𝕜, E →L[𝕜] E') ∞ (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 : ContMDiffAt J I ⊤ f x₀) (hg : ContMDiffAt J I' ⊤ g x₀) - (hϕ : ContMDiffAt J 𝓘(𝕜, E →L[𝕜] E') ⊤ (inTangentCoordinates I I' f g ϕ x₀) x₀) : - ContMDiffAt J ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ⊤ + (hf : ContMDiffAt J I ∞ f x₀) (hg : ContMDiffAt J I' ∞ g x₀) + (hϕ : ContMDiffAt J 𝓘(𝕜, E →L[𝕜] E') ∞ (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ϕ⟩ @@ -385,12 +385,12 @@ def oneJetExt (f : M → M') : M → OneJetBundle I M I' M' := fun x ↦ variable {I I'} -theorem ContMDiffAt.oneJetExt {f : M → M'} {x : M} (hf : ContMDiffAt I I' ⊤ f x) : - ContMDiffAt I ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ⊤ (oneJetExt I I' f) x := +theorem ContMDiffAt.oneJetExt {f : M → M'} {x : M} (hf : ContMDiffAt I I' ∞ f x) : + ContMDiffAt I ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ∞ (oneJetExt I I' f) x := contMDiffAt_id.oneJetBundle_mk hf (hf.mfderiv_const le_rfl) -theorem ContMDiff.oneJetExt {f : M → M'} (hf : ContMDiff I I' ⊤ f) : - ContMDiff I ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ⊤ (oneJetExt I I' f) := +theorem ContMDiff.oneJetExt {f : M → M'} (hf : ContMDiff I I' ∞ f) : + ContMDiff I ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ∞ (oneJetExt I I' f) := fun x ↦ ((hf x).contMDiffAt univ_mem).oneJetExt theorem ContinuousAt.inTangentCoordinates_comp {f : N → M} {g : N → M'} {h : N → N'} @@ -410,42 +410,42 @@ 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ϕ' : 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ϕ'.clm_comp hϕ).congr_of_eventuallyEq hg.inTangentCoordinates_comp variable (I') -variable [SmoothManifoldWithCorners J N] +variable [IsManifold J ∞ N] -omit [SmoothManifoldWithCorners J' N'] in +omit [IsManifold J' ∞ N'] in theorem ContMDiffAt.oneJet_comp {f1 : N' → M} (f2 : N' → M') {f3 : N' → N} {x₀ : N'} {h : ∀ x : N', OneJetSpace I' J (f2 x, f3 x)} {g : ∀ x : N', OneJetSpace I I' (f1 x, f2 x)} - (hh : ContMDiffAt J' ((I'.prod J).prod 𝓘(𝕜, E' →L[𝕜] F)) ⊤ (fun x ↦ OneJetBundle.mk _ _ (h x)) x₀) - (hg : ContMDiffAt J' ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ⊤ (fun x ↦ OneJetBundle.mk _ _ (g x)) x₀) : - ContMDiffAt J' ((I.prod J).prod 𝓘(𝕜, E →L[𝕜] F)) ⊤ + (hh : ContMDiffAt J' ((I'.prod J).prod 𝓘(𝕜, E' →L[𝕜] F)) ∞ (fun x ↦ OneJetBundle.mk _ _ (h x)) x₀) + (hg : ContMDiffAt J' ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ∞ (fun x ↦ OneJetBundle.mk _ _ (g x)) x₀) : + ContMDiffAt J' ((I.prod J).prod 𝓘(𝕜, E →L[𝕜] F)) ∞ (fun x ↦ OneJetBundle.mk (f1 x) (f3 x) (h x ∘L g x) : N' → OneJetBundle I M J N) x₀ := by rw [contMDiffAt_oneJetBundle_mk] at hh hg ⊢ exact ⟨hg.1, hh.2.1, hh.2.2.clm_comp_inTangentCoordinates hg.2.1.continuousAt hg.2.2⟩ -omit [SmoothManifoldWithCorners J' N'] in +omit [IsManifold J' ∞ N'] in theorem ContMDiff.oneJet_comp {f1 : N' → M} (f2 : N' → M') {f3 : N' → N} {h : ∀ x : N', OneJetSpace I' J (f2 x, f3 x)} {g : ∀ x : N', OneJetSpace I I' (f1 x, f2 x)} - (hh : ContMDiff J' ((I'.prod J).prod 𝓘(𝕜, E' →L[𝕜] F)) ⊤ fun x ↦ OneJetBundle.mk _ _ (h x)) - (hg : ContMDiff J' ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ⊤ fun x ↦ OneJetBundle.mk _ _ (g x)) : - ContMDiff J' ((I.prod J).prod 𝓘(𝕜, E →L[𝕜] F)) ⊤ + (hh : ContMDiff J' ((I'.prod J).prod 𝓘(𝕜, E' →L[𝕜] F)) ∞ fun x ↦ OneJetBundle.mk _ _ (h x)) + (hg : ContMDiff J' ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ∞ fun x ↦ OneJetBundle.mk _ _ (g x)) : + ContMDiff J' ((I.prod J).prod 𝓘(𝕜, E →L[𝕜] F)) ∞ (fun x ↦ OneJetBundle.mk (f1 x) (f3 x) (h x ∘L g x) : N' → OneJetBundle I M J N) := fun x₀ ↦ hh.contMDiffAt.oneJet_comp I' f2 (hg x₀) variable {I'} open Trivialization in -omit [SmoothManifoldWithCorners J N] in +omit [IsManifold J ∞ N] in theorem ContMDiff.oneJet_add {f : N → M} {g : N → M'} {ϕ ϕ' : ∀ x : N, OneJetSpace I I' (f x, g x)} - (hϕ : ContMDiff J ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ⊤ fun x ↦ OneJetBundle.mk _ _ (ϕ x)) - (hϕ' : ContMDiff J ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ⊤ fun x ↦ OneJetBundle.mk _ _ (ϕ' x)) : - ContMDiff J ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ⊤ fun x ↦ + (hϕ : ContMDiff J ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ∞ fun x ↦ OneJetBundle.mk _ _ (ϕ x)) + (hϕ' : ContMDiff J ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ∞ fun x ↦ OneJetBundle.mk _ _ (ϕ' x)) : + ContMDiff J ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ∞ fun x ↦ OneJetBundle.mk (f x) (g x) (ϕ x + ϕ' x) := by intro x specialize hϕ x @@ -472,9 +472,9 @@ protected def OneJetBundle.map (f : M → N) (g : M' → N') variable {I' J'} -omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] - [SmoothManifoldWithCorners I₂ M₂] [SmoothManifoldWithCorners I₃ M₃] - [SmoothManifoldWithCorners J' N'] [SmoothManifoldWithCorners J N] in +omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] + [IsManifold I₂ ∞ M₂] [IsManifold I₃ ∞ M₃] + [IsManifold J' ∞ N'] [IsManifold J ∞ N] in theorem OneJetBundle.map_map {f₂ : N → M₂} {f : M → N} {g₂ : N' → M₃} {g : M' → N'} {Dfinv : ∀ x : M, TangentSpace J (f x) →L[𝕜] TangentSpace I x} {Df₂inv : ∀ x : N, TangentSpace I₂ (f₂ x) →L[𝕜] TangentSpace J x} {x : J¹MM'} @@ -487,9 +487,9 @@ theorem OneJetBundle.map_map {f₂ : N → M₂} {f : M → N} {g₂ : N' → M · dsimp only [OneJetBundle.map, OneJetBundle.mk] simp_rw [← ContinuousLinearMap.comp_assoc, mfderiv_comp x.1.2 hg₂ hg] -omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] - [SmoothManifoldWithCorners I₂ M₂] [SmoothManifoldWithCorners I₃ M₃] - [SmoothManifoldWithCorners J' N'] [SmoothManifoldWithCorners J N] in +omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] + [IsManifold I₂ ∞ M₂] [IsManifold I₃ ∞ M₃] + [IsManifold J' ∞ N'] [IsManifold J ∞ N] in theorem OneJetBundle.map_id (x : J¹MM') : OneJetBundle.map I' I' id id (fun x ↦ ContinuousLinearMap.id 𝕜 (TangentSpace I x)) x = x := by -- Porting note: was `ext _` in Lean 3 @@ -503,15 +503,15 @@ 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 J (f z x) →L[𝕜] TangentSpace I 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 : 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)) (hDfinv : - ContMDiffAt I'' 𝓘(𝕜, F →L[𝕜] E) ⊤ + 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₀) - (hk : ContMDiffAt I'' ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ⊤ k x₀) : - ContMDiffAt I'' ((J.prod J').prod 𝓘(𝕜, F →L[𝕜] F')) ⊤ + (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 rw [contMDiffAt_oneJetBundle] at hk refine ContMDiffAt.oneJet_comp _ _ ?_ ?_ @@ -528,9 +528,9 @@ def mapLeft (f : M → N) (Dfinv : ∀ x : M, TangentSpace J (f x) →L[𝕜] Ta J¹MM' → OneJetBundle J N I' M' := fun p ↦ OneJetBundle.mk (f p.1.1) p.1.2 (p.2 ∘L Dfinv p.1.1) set_option linter.style.multiGoal false in -omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] - [SmoothManifoldWithCorners I₂ M₂] [SmoothManifoldWithCorners I₃ M₃] - [SmoothManifoldWithCorners J' N'] [SmoothManifoldWithCorners J N] in +omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] + [IsManifold I₂ ∞ M₂] [IsManifold I₃ ∞ M₃] + [IsManifold J' ∞ N'] [IsManifold J ∞ N] in theorem mapLeft_eq_map (f : M → N) (Dfinv : ∀ x : M, TangentSpace J (f x) →L[𝕜] TangentSpace I x) : mapLeft f Dfinv = OneJetBundle.map I' I' f (id : M' → M') Dfinv := by ext x; rfl; rfl; dsimp only [OneJetBundle.map, mapLeft, oneJetBundle_mk_snd] @@ -538,14 +538,14 @@ theorem mapLeft_eq_map (f : M → N) (Dfinv : ∀ x : M, TangentSpace J (f x) theorem ContMDiffAt.mapLeft {f : N' → M → N} {x₀ : N'} {Dfinv : ∀ (z : N') (x : M), TangentSpace J (f z x) →L[𝕜] TangentSpace I x} {g : N' → J¹MM'} - (hf : ContMDiffAt (J'.prod I) J ⊤ f.uncurry (x₀, (g x₀).1.1)) + (hf : ContMDiffAt (J'.prod I) J ∞ f.uncurry (x₀, (g x₀).1.1)) (hDfinv : - ContMDiffAt J' 𝓘(𝕜, F →L[𝕜] E) ⊤ + ContMDiffAt J' 𝓘(𝕜, F →L[𝕜] E) ∞ (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₀) - (hg : ContMDiffAt J' ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ⊤ g x₀) : - ContMDiffAt J' ((J.prod I').prod 𝓘(𝕜, F →L[𝕜] E')) ⊤ (fun z ↦ mapLeft (f z) (Dfinv z) (g z)) x₀ := by + (hg : ContMDiffAt J' ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ∞ g x₀) : + ContMDiffAt J' ((J.prod I').prod 𝓘(𝕜, F →L[𝕜] E')) ∞ (fun z ↦ mapLeft (f z) (Dfinv z) (g z)) x₀ := by simp_rw [mapLeft_eq_map]; exact hf.oneJetBundle_map contMDiffAt_snd hDfinv hg /-- The projection `J¹(E × P, F) → J¹(E, F)`. Not actually used. -/ @@ -556,26 +556,25 @@ def bundleFst : OneJetBundle (J.prod I) (N × M) I' M' → OneJetBundle J N I' M def bundleSnd : OneJetBundle (J.prod I) (N × M) I' M' → J¹MM' := mapLeft Prod.snd fun x ↦ mfderiv I (J.prod I) (fun y ↦ (x.1, y)) x.2 -omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] - [SmoothManifoldWithCorners I₂ M₂] [SmoothManifoldWithCorners I₃ M₃] - [SmoothManifoldWithCorners J' N'] [SmoothManifoldWithCorners J N] in +omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] + [IsManifold I₂ ∞ M₂] [IsManifold I₃ ∞ M₃] + [IsManifold J' ∞ N'] [IsManifold J ∞ N] in theorem bundleSnd_eq (x : OneJetBundle (J.prod I) (N × M) I' M') : bundleSnd x = (mapLeft Prod.snd (fun _ ↦ ContinuousLinearMap.inr 𝕜 F E) x : J¹MM') := by simp_rw [bundleSnd, mfderiv_prod_right]; rfl theorem contMDiff_bundleSnd : ContMDiff (((J.prod I).prod I').prod 𝓘(𝕜, F × E →L[𝕜] E')) ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) - ⊤ (bundleSnd : OneJetBundle (J.prod I) (N × M) I' M' → J¹MM') := by + ∞ (bundleSnd : OneJetBundle (J.prod I) (N × M) I' M' → J¹MM') := by intro x₀ refine ContMDiffAt.mapLeft contMDiffAt_snd.snd ?_ contMDiffAt_id - have : - ContMDiffAt (((J.prod I).prod I').prod 𝓘(𝕜, F × E →L[𝕜] E')) 𝓘(𝕜, E →L[𝕜] F × E) ⊤ + have : ContMDiffAt (((J.prod I).prod I').prod 𝓘(𝕜, F × E →L[𝕜] E')) 𝓘(𝕜, E →L[𝕜] F × E) ∞ (inTangentCoordinates I (J.prod I) _ _ _ x₀) x₀ := - ContMDiffAt.mfderiv (fun (x : OneJetBundle (J.prod I) (N × M) I' M') (y : M) ↦ (x.1.1.1, y)) - (fun x : OneJetBundle (J.prod I) (N × M) I' M' ↦ x.1.1.2) ?_ ?_ le_top + ContMDiffAt.mfderiv (n := ∞) + (fun (x : OneJetBundle (J.prod I) (N × M) I' M') (y : M) ↦ (x.1.1.1, y)) + (fun x : OneJetBundle (J.prod I) (N × M) I' M' ↦ x.1.1.2) ?_ ?_ le_rfl · exact this · exact (contMDiff_oneJetBundle_proj.fst.fst.prod_map contMDiff_id).contMDiffAt - -- slow · exact contMDiff_oneJetBundle_proj.fst.snd.contMDiffAt -- slow diff --git a/SphereEversion/Global/OneJetSec.lean b/SphereEversion/Global/OneJetSec.lean index cdc53ce6..d20c2905 100644 --- a/SphereEversion/Global/OneJetSec.lean +++ b/SphereEversion/Global/OneJetSec.lean @@ -27,7 +27,7 @@ noncomputable section open Set Function Filter ChartedSpace SmoothManifoldWithCorners -open scoped Topology Manifold +open scoped Topology Manifold ContDiff section General @@ -36,18 +36,18 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (M : Type*) [TopologicalSpace M] [ChartedSpace H M] - [SmoothManifoldWithCorners I M] + [IsManifold I ∞ M] -- declare a smooth manifold `M'` over the pair `(E', H')`. {E' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type*} [TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H') (M' : Type*) [TopologicalSpace M'] [ChartedSpace H' M'] - [SmoothManifoldWithCorners I' M'] + [IsManifold I' ∞ M'] /-- A section of a 1-jet bundle seen as a bundle over the source manifold. -/ @[ext] structure OneJetSec where bs : M → M' ϕ : ∀ x : M, TangentSpace I x →L[𝕜] TangentSpace I' (bs x) - smooth' : ContMDiff I ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ⊤ fun x ↦ OneJetBundle.mk x (bs x) (ϕ x) + smooth' : ContMDiff I ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ∞ fun x ↦ OneJetBundle.mk x (bs x) (ϕ x) instance : FunLike (OneJetSec I M I' M') M (OneJetBundle I M I' M') where coe := fun S x ↦ OneJetBundle.mk x (S.bs x) (S.ϕ x) @@ -64,7 +64,7 @@ variable {I M I' M'} namespace OneJetSec protected def mk' (F : M → OneJetBundle I M I' M') (hF : ∀ m, (F m).1.1 = m) - (h2F : ContMDiff I ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ⊤ F) : OneJetSec I M I' M' := + (h2F : ContMDiff I ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ∞ F) : OneJetSec I M I' M' := ⟨fun x ↦ (F x).1.2, fun x ↦ (F x).2, by convert h2F using 1; ext m; exacts [(hF m).symm, rfl, rfl]⟩ theorem coe_apply (F : OneJetSec I M I' M') (x : M) : F x = ⟨(x, F.bs x), F.ϕ x⟩ := @@ -83,15 +83,15 @@ theorem bs_eq (F : OneJetSec I M I' M') (x : M) : F.bs x = (F x).1.2 := rfl protected theorem smooth (F : OneJetSec I M I' M') : - ContMDiff I ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ⊤ F := + ContMDiff I ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ∞ F := F.smooth' theorem smooth_eta (F : OneJetSec I M I' M') : - ContMDiff I ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ⊤ + ContMDiff I ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) ∞ (fun x ↦ OneJetBundle.mk x (F.bs x) (F x).2 : M → OneJetBundle I M I' M') := F.smooth -theorem smooth_bs (F : OneJetSec I M I' M') : ContMDiff I I' ⊤ F.bs := +theorem smooth_bs (F : OneJetSec I M I' M') : ContMDiff I I' ∞ F.bs := contMDiff_oneJetBundle_proj.snd.comp F.smooth /-- A section of J¹(M, M') is holonomic at (x : M) if its linear map part is the derivative @@ -147,7 +147,7 @@ def IsHolonomicGerm {x : M} (φ : Germ (𝓝 x) (OneJetBundle I M I' M')) : Prop exact fun f g H ↦ propext ⟨key f g H, key g f H.symm⟩) /-- The one-jet extension of a function, seen as a section of the 1-jet bundle. -/ -def oneJetExtSec (f : C^⊤⟮I, M; I', M'⟯) : OneJetSec I M I' M' := +def oneJetExtSec (f : C^∞⟮I, M; I', M'⟯) : OneJetSec I M I' M' := ⟨f, mfderiv I I' f, f.contMDiff.oneJetExt⟩ end General @@ -156,17 +156,17 @@ section Real variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type*} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type*) [TopologicalSpace M] [ChartedSpace H M] - [SmoothManifoldWithCorners I M] {E' : Type*} [NormedAddCommGroup E'] [NormedSpace ℝ E'] + [IsManifold I ∞ M] {E' : Type*} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type*} [TopologicalSpace H'] (I' : ModelWithCorners ℝ E' H') (M' : Type*) - [TopologicalSpace M'] [ChartedSpace H' M'] [SmoothManifoldWithCorners I' M'] {F : Type*} + [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' ∞ M'] {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type*} [TopologicalSpace G] (J : ModelWithCorners ℝ F G) (N : Type*) [TopologicalSpace N] [ChartedSpace G N] {F' : Type*} [NormedAddCommGroup F'] [NormedSpace ℝ F'] {G' : Type*} [TopologicalSpace G'] (J' : ModelWithCorners ℝ F' G') (N' : Type*) - [TopologicalSpace N'] [ChartedSpace G' N'] [SmoothManifoldWithCorners J' N'] {EP : Type*} + [TopologicalSpace N'] [ChartedSpace G' N'] [IsManifold J' ∞ N'] {EP : Type*} [NormedAddCommGroup EP] [NormedSpace ℝ EP] {HP : Type*} [TopologicalSpace HP] {IP : ModelWithCorners ℝ EP HP} {P : Type*} [TopologicalSpace P] [ChartedSpace HP P] - [SmoothManifoldWithCorners IP P] + [IsManifold IP ∞ P] /-- A family of jet sections indexed by manifold `N` is a function from `N` into jet sections in such a way that the function is smooth as a function of all arguments. -/ @@ -174,7 +174,7 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type*} [Top bs : N → M → M' ϕ : ∀ (n : N) (m : M), TangentSpace I m →L[ℝ] TangentSpace I' (bs n m) smooth' : - ContMDiff (J.prod I) ((I.prod I').prod 𝓘(ℝ, E →L[ℝ] E')) ⊤ fun p : N × M ↦ + ContMDiff (J.prod I) ((I.prod I').prod 𝓘(ℝ, E →L[ℝ] E')) ∞ fun p : N × M ↦ OneJetBundle.mk p.2 (bs p.1 p.2) (ϕ p.1 p.2) instance : FunLike (FamilyOneJetSec I M I' M' J N) N (OneJetSec I M I' M') where @@ -193,13 +193,13 @@ namespace FamilyOneJetSec variable {I M I' M' J N J' N'} protected def mk' (FF : N → M → OneJetBundle I M I' M') (hF : ∀ n m, (FF n m).1.1 = m) - (h2F : ContMDiff (J.prod I) ((I.prod I').prod 𝓘(ℝ, E →L[ℝ] E')) ⊤ (uncurry FF)) : + (h2F : ContMDiff (J.prod I) ((I.prod I').prod 𝓘(ℝ, E →L[ℝ] E')) ∞ (uncurry FF)) : FamilyOneJetSec I M I' M' J N := ⟨fun s x ↦ (FF s x).1.2, fun s x ↦ (FF s x).2, by convert h2F using 1; ext ⟨s, m⟩; exacts [(hF s m).symm, rfl, rfl]⟩ theorem coe_mk' (FF : N → M → OneJetBundle I M I' M') (hF : ∀ n m, (FF n m).1.1 = m) - (h2F : ContMDiff (J.prod I) ((I.prod I').prod 𝓘(ℝ, E →L[ℝ] E')) ⊤ (uncurry FF)) (x : N) : + (h2F : ContMDiff (J.prod I) ((I.prod I').prod 𝓘(ℝ, E →L[ℝ] E')) ∞ (uncurry FF)) (x : N) : FamilyOneJetSec.mk' FF hF h2F x = OneJetSec.mk' (FF x) (hF x) (h2F.comp (contMDiff_const.prod_mk contMDiff_id)) := rfl @@ -216,18 +216,18 @@ theorem coe_ϕ (S : FamilyOneJetSec I M I' M' J N) (s : N) : (S s).ϕ = S.ϕ s : rfl protected theorem smooth (S : FamilyOneJetSec I M I' M' J N) : - ContMDiff (J.prod I) ((I.prod I').prod 𝓘(ℝ, E →L[ℝ] E')) ⊤ fun p : N × M ↦ S p.1 p.2 := + ContMDiff (J.prod I) ((I.prod I').prod 𝓘(ℝ, E →L[ℝ] E')) ∞ fun p : N × M ↦ S p.1 p.2 := S.smooth' theorem smooth_bs (S : FamilyOneJetSec I M I' M' J N) : - ContMDiff (J.prod I) I' ⊤ fun p : N × M ↦ S.bs p.1 p.2 := + ContMDiff (J.prod I) I' ∞ fun p : N × M ↦ S.bs p.1 p.2 := contMDiff_oneJetBundle_proj.snd.comp S.smooth -theorem smooth_coe_bs (S : FamilyOneJetSec I M I' M' J N) {p : N} : ContMDiff I I' ⊤ (S.bs p) := +theorem smooth_coe_bs (S : FamilyOneJetSec I M I' M' J N) {p : N} : ContMDiff I I' ∞ (S.bs p) := (S p).smooth_bs /-- Reindex a family along a smooth function `f`. -/ -def reindex (S : FamilyOneJetSec I M I' M' J' N') (f : C^⊤⟮J, N; J', N'⟯) : +def reindex (S : FamilyOneJetSec I M I' M' J' N') (f : C^∞⟮J, N; J', N'⟯) : FamilyOneJetSec I M I' M' J N where bs t := S.bs (f t) ϕ t := S.ϕ (f t) @@ -245,10 +245,11 @@ def uncurry (S : FamilyOneJetSec I M I' M' IP P) : OneJetSec (IP.prod I) (P × M refine ContMDiff.oneJet_add ?_ ?_ · intro y refine contMDiffAt_id.oneJetBundle_mk (S.smooth_bs y) ?_ - have : ContMDiffAt ((IP.prod I).prod (IP.prod I)) I' ⊤ + 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) := S.smooth_bs.comp (contMDiff_snd.fst.prod_mk contMDiff_fst.snd) (y, y) - apply ContMDiffAt.mfderiv (fun x z : P × M ↦ S.bs z.1 x.2) id this contMDiffAt_id le_top + apply ContMDiffAt.mfderiv (fun x z : P × M ↦ S.bs z.1 x.2) id this contMDiffAt_id + (mod_cast le_top) · exact ContMDiff.oneJet_comp I (fun p : P × M ↦ p.2) S.smooth contMDiff_snd.oneJetExt theorem uncurry_ϕ' (S : FamilyOneJetSec I M I' M' IP P) (p : P × M) : @@ -267,8 +268,9 @@ theorem isHolonomicAt_uncurry (S : FamilyOneJetSec I M I' M' IP P) {p : P × M} S.uncurry.IsHolonomicAt p ↔ (S p.1).IsHolonomicAt p.2 := by simp_rw [OneJetSec.IsHolonomicAt, OneJetSec.snd_eq, S.uncurry_ϕ] rw [show S.uncurry.bs = fun x ↦ S.uncurry.bs x from rfl, funext S.uncurry_bs] - simp_rw [mfderiv_prod_eq_add (S.smooth_bs.mdifferentiableAt le_top), mfderiv_snd, add_right_inj] - erw [mfderiv_comp p (S.smooth_coe_bs.mdifferentiableAt le_top) + simp_rw [mfderiv_prod_eq_add (S.smooth_bs.mdifferentiableAt (mod_cast le_top)), + mfderiv_snd, add_right_inj] + erw [mfderiv_comp p (S.smooth_coe_bs.mdifferentiableAt (mod_cast le_top)) (contMDiff_snd.mdifferentiableAt le_top), mfderiv_snd] exact (show Surjective (ContinuousLinearMap.snd ℝ EP E) from Prod.snd_surjective).clm_comp_injective.eq_iff diff --git a/SphereEversion/Global/ParametricityForFree.lean b/SphereEversion/Global/ParametricityForFree.lean index 973fc3be..ac51cfb4 100644 --- a/SphereEversion/Global/ParametricityForFree.lean +++ b/SphereEversion/Global/ParametricityForFree.lean @@ -11,7 +11,7 @@ open ChartedSpace SmoothManifoldWithCorners open LinearMap (ker) -open scoped Topology Manifold Pointwise +open scoped Topology Manifold Pointwise ContDiff section ParameterSpace @@ -20,18 +20,18 @@ section ParameterSpace variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type*} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type*} [TopologicalSpace M] [ChartedSpace H M] - [SmoothManifoldWithCorners I M] {E' : Type*} [NormedAddCommGroup E'] [NormedSpace ℝ E'] + [IsManifold I ∞ M] {E' : Type*} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type*} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {M' : Type*} - [TopologicalSpace M'] [ChartedSpace H' M'] [SmoothManifoldWithCorners I' M'] {EP : Type*} + [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' ∞ M'] {EP : Type*} [NormedAddCommGroup EP] [NormedSpace ℝ EP] {HP : Type*} [TopologicalSpace HP] {IP : ModelWithCorners ℝ EP HP} {P : Type*} [TopologicalSpace P] [ChartedSpace HP P] - [SmoothManifoldWithCorners IP P] {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] + [IsManifold IP ∞ P] {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type*} [TopologicalSpace G] {J : ModelWithCorners ℝ F G} {N : Type*} [TopologicalSpace N] - [ChartedSpace G N] [SmoothManifoldWithCorners J N] {EX : Type*} [NormedAddCommGroup EX] + [ChartedSpace G N] [IsManifold J ∞ N] {EX : Type*} [NormedAddCommGroup EX] [NormedSpace ℝ EX] {HX : Type*} [TopologicalSpace HX] {IX : ModelWithCorners ℝ EX HX} -- note: X is a metric space {X : Type*} - [MetricSpace X] [ChartedSpace HX X] [SmoothManifoldWithCorners IX X] + [MetricSpace X] [ChartedSpace HX X] [IsManifold IX ∞ X] variable {R : RelMfld I M I' M'} @@ -40,7 +40,7 @@ variable (IP P) in def RelMfld.relativize (R : RelMfld I M I' M') : RelMfld (IP.prod I) (P × M) I' M' := bundleSnd ⁻¹' R -omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] [SmoothManifoldWithCorners IP P] in +omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] [IsManifold IP ∞ P] in theorem RelMfld.mem_relativize (R : RelMfld I M I' M') (w : OneJetBundle (IP.prod I) (P × M) I' M') : w ∈ R.relativize IP P ↔ @@ -64,7 +64,7 @@ variable {σ : OneJetBundle (IP.prod I) (P × M) I' M'} #check (R.relativize IP P).slice σ p #check (R.slice (bundleSnd σ) q : Set <| TangentSpace I' σ.proj.2) -/ -omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] [SmoothManifoldWithCorners IP P] in +omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] [IsManifold IP ∞ P] in theorem relativize_slice {σ : OneJetBundle (IP.prod I) (P × M) I' M'} {p : DualPair <| TangentSpace (IP.prod I) σ.1.1} (q : DualPair <| TangentSpace I σ.1.1.2) (hpq : p.π.comp (ContinuousLinearMap.inr ℝ EP E) = q.π) : @@ -93,7 +93,7 @@ theorem relativize_slice {σ : OneJetBundle (IP.prod I) (P × M) I' M'} erw [← preimage_vadd_neg, mem_preimage, mem_slice, R.mem_relativize] congr! -omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] [SmoothManifoldWithCorners IP P] in +omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] [IsManifold IP ∞ P] in theorem relativize_slice_eq_univ {σ : OneJetBundle (IP.prod I) (P × M) I' M'} {p : DualPair <| TangentSpace (IP.prod I) σ.1.1} (hp : p.π.comp (ContinuousLinearMap.inr ℝ EP E) = 0) : @@ -120,7 +120,7 @@ theorem relativize_slice_eq_univ {σ : OneJetBundle (IP.prod I) (P × M) I' M'} simp [this, exists_const, forall_const] variable (IP P) in -omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] [SmoothManifoldWithCorners IP P] in +omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] [IsManifold IP ∞ P] in theorem RelMfld.Ample.relativize (hR : R.Ample) : (R.relativize IP P).Ample := by intro σ p let p2 := p.π.comp (ContinuousLinearMap.inr ℝ EP E) @@ -173,7 +173,7 @@ def FamilyOneJetSec.curry (S : FamilyOneJetSec (IP.prod I) (P × M) I' M' J N) : rintro ⟨⟨t, s⟩, x⟩ refine contMDiffAt_snd.oneJetBundle_mk (S.smooth_bs.comp contMDiff_prod_assoc _) ?_ have h1 : - ContMDiffAt ((J.prod IP).prod I) 𝓘(ℝ, EP × E →L[ℝ] E') ⊤ + 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)) (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)) @@ -182,15 +182,15 @@ def FamilyOneJetSec.curry (S : FamilyOneJetSec (IP.prod I) (P × M) I' M' J N) : (contMDiffAt_oneJetBundle.mp <| ContMDiffAt.comp ((t, s), x) (S.smooth (t, (s, x))) (contMDiff_prod_assoc ((t, s), x))).2.2 have h2 : - ContMDiffAt ((J.prod IP).prod I) 𝓘(ℝ, E →L[ℝ] EP × E) ⊤ + 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)) ((t, s), x) := by apply ContMDiffAt.mfderiv (fun (p : (N × P) × M) (x : M) ↦ (p.1.2, x)) Prod.snd (contMDiffAt_fst.fst.snd.prod_mk contMDiffAt_snd : - ContMDiffAt (((J.prod IP).prod I).prod I) (IP.prod I) ⊤ _ (((t, s), x), x)) - (contMDiffAt_snd : ContMDiffAt ((J.prod IP).prod I) _ ⊤ _ _) le_top + ContMDiffAt (((J.prod IP).prod I).prod I) (IP.prod I) ∞ _ (((t, s), x), x)) + (contMDiffAt_snd : ContMDiffAt ((J.prod IP).prod I) _ ∞ _ _) (mod_cast le_top) exact h1.clm_comp_inTangentCoordinates (continuousAt_fst.snd.prod continuousAt_snd) h2 theorem FamilyOneJetSec.curry_bs (S : FamilyOneJetSec (IP.prod I) (P × M) I' M' J N) (p : N × P) @@ -217,7 +217,7 @@ theorem FamilyOneJetSec.isHolonomicAt_curry (S : FamilyOneJetSec (IP.prod I) (P {t : N} {s : P} {x : M} (hS : (S t).IsHolonomicAt (s, x)) : (S.curry (t, s)).IsHolonomicAt x := by simp_rw [OneJetSec.IsHolonomicAt, (S.curry _).snd_eq, S.curry_ϕ] at hS ⊢ rw [show (S.curry (t, s)).bs = fun x ↦ (S.curry (t, s)).bs x from rfl, funext (S.curry_bs _)] - refine (mfderiv_comp x ((S t).smooth_bs.mdifferentiableAt le_top) + refine (mfderiv_comp x ((S t).smooth_bs.mdifferentiableAt (mod_cast le_top)) (mdifferentiableAt_const.prod_mk (contMDiff_id.mdifferentiableAt le_top))).trans ?_ rw [id, hS] diff --git a/SphereEversion/Global/Relation.lean b/SphereEversion/Global/Relation.lean index cdbeff88..ab69a7fe 100644 --- a/SphereEversion/Global/Relation.lean +++ b/SphereEversion/Global/Relation.lean @@ -25,7 +25,7 @@ open Filter hiding map_smul open ChartedSpace SmoothManifoldWithCorners -open scoped Topology Manifold Bundle +open scoped Topology Manifold Bundle ContDiff section Defs @@ -34,23 +34,23 @@ section Defs variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type*} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) - (M : Type*) [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] + (M : Type*) [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M] {E' : Type*} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type*} [TopologicalSpace H'] (I' : ModelWithCorners ℝ E' H') - (M' : Type*) [TopologicalSpace M'] [ChartedSpace H' M'] [SmoothManifoldWithCorners I' M'] + (M' : Type*) [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' ∞ M'] {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type*} [TopologicalSpace G] (J : ModelWithCorners ℝ F G) (N : Type*) [TopologicalSpace N] [ChartedSpace G N] {F' : Type*} [NormedAddCommGroup F'] [NormedSpace ℝ F'] {G' : Type*} [TopologicalSpace G'] (J' : ModelWithCorners ℝ F' G') - (N' : Type*) [TopologicalSpace N'] [ChartedSpace G' N'] [SmoothManifoldWithCorners J' N'] + (N' : Type*) [TopologicalSpace N'] [ChartedSpace G' N'] [IsManifold J' ∞ N'] {EP : Type*} [NormedAddCommGroup EP] [NormedSpace ℝ EP] {HP : Type*} [TopologicalSpace HP] (IP : ModelWithCorners ℝ EP HP) (P : Type*) [TopologicalSpace P] [ChartedSpace HP P] {EX : Type*} [NormedAddCommGroup EX] [NormedSpace ℝ EX] {HX : Type*} [TopologicalSpace HX] {IX : ModelWithCorners ℝ EX HX} -- note: X is a metric space - {X : Type*} [MetricSpace X] [ChartedSpace HX X] [SmoothManifoldWithCorners IX X] + {X : Type*} [MetricSpace X] [ChartedSpace HX X] [IsManifold IX ∞ X] @[inherit_doc] local notation "TM" => TangentSpace I @@ -78,7 +78,7 @@ instance (R : RelMfld I M I' M') : FunLike (FormalSol R) M (OneJetBundle I M I' def mkFormalSol (F : M → OneJetBundle I M I' M') (hsec : ∀ x, (F x).1.1 = x) (hsol : ∀ x, F x ∈ R) - (hsmooth : ContMDiff I ((I.prod I').prod 𝓘(ℝ, E →L[ℝ] E')) ⊤ F) : FormalSol R + (hsmooth : ContMDiff I ((I.prod I').prod 𝓘(ℝ, E →L[ℝ] E')) ∞ F) : FormalSol R where bs m := (F m).1.2 ϕ m := (F m).2 @@ -95,7 +95,7 @@ def mkFormalSol (F : M → OneJetBundle I M I' M') (hsec : ∀ x, (F x).1.1 = x) @[simp] theorem mkFormalSol_apply (F : M → OneJetBundle I M I' M') (hsec : ∀ x, (F x).1.1 = x) - (hsol : ∀ x, F x ∈ R) (hsmooth : ContMDiff I ((I.prod I').prod 𝓘(ℝ, E →L[ℝ] E')) ⊤ ↿F) : + (hsol : ∀ x, F x ∈ R) (hsmooth : ContMDiff I ((I.prod I').prod 𝓘(ℝ, E →L[ℝ] E')) ∞ ↿F) : (mkFormalSol F hsec hsol hsmooth : M → OneJetBundle I M I' M') = F := by ext x <;> try rfl rw [hsec] @@ -103,7 +103,7 @@ theorem mkFormalSol_apply (F : M → OneJetBundle I M I' M') (hsec : ∀ x, (F x @[simp] theorem mkFormalSol_bs_apply (F : M → OneJetBundle I M I' M') (hsec : ∀ x, (F x).1.1 = x) - (hsol : ∀ x, F x ∈ R) (hsmooth : ContMDiff I ((I.prod I').prod 𝓘(ℝ, E →L[ℝ] E')) ⊤ ↿F) (x : M) : + (hsol : ∀ x, F x ∈ R) (hsmooth : ContMDiff I ((I.prod I').prod 𝓘(ℝ, E →L[ℝ] E')) ∞ ↿F) (x : M) : (mkFormalSol F hsec hsol hsmooth).bs x = (F x).1.2 := rfl @@ -154,20 +154,20 @@ open scoped Manifold Bundle search. There was no problem in Lean 3. -/ instance (σ : OneJetBundle I M I' M') : - NormedAddCommGroup (((ContMDiffMap.snd : C^⊤⟮I.prod I', M × M'; I', M'⟯) *ᵖ TM') σ.proj) := by + NormedAddCommGroup (((ContMDiffMap.snd : C^∞⟮I.prod I', M × M'; I', M'⟯) *ᵖ TM') σ.proj) := by assumption instance (σ : OneJetBundle I M I' M') : - NormedSpace ℝ (((ContMDiffMap.snd : C^⊤⟮I.prod I', M × M'; I', M'⟯) *ᵖ TM') σ.proj) := by + NormedSpace ℝ (((ContMDiffMap.snd : C^∞⟮I.prod I', M × M'; I', M'⟯) *ᵖ TM') σ.proj) := by assumption instance (x : M) (x' : M') : - NormedAddCommGroup (((ContMDiffMap.snd : C^⊤⟮I.prod I', M × M'; I', M'⟯) *ᵖ TM') + NormedAddCommGroup (((ContMDiffMap.snd : C^∞⟮I.prod I', M × M'; I', M'⟯) *ᵖ TM') (x, x')) := by assumption instance (x : M) (x' : M') : - NormedSpace ℝ (((ContMDiffMap.snd : C^⊤⟮I.prod I', M × M'; I', M'⟯) *ᵖ TM') + NormedSpace ℝ (((ContMDiffMap.snd : C^∞⟮I.prod I', M × M'; I', M'⟯) *ᵖ TM') (x, x')) := by assumption @@ -176,14 +176,14 @@ def RelMfld.slice (R : RelMfld I M I' M') (σ : OneJetBundle I M I' M') (p : Dua Set (TM' σ.1.2) := {w : TM' σ.1.2 | OneJetBundle.mk σ.1.1 σ.1.2 (p.update σ.2 w) ∈ R} -omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] in +omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] in /-- For some reason `rw [mem_setOf_eq]` fails after unfolding `slice`, but rewriting with this lemma works. -/ theorem mem_slice {R : RelMfld I M I' M'} {σ : OneJetBundle I M I' M'} {p : DualPair <| TM σ.1.1} {w : TM' σ.1.2} : w ∈ R.slice σ p ↔ OneJetBundle.mk σ.1.1 σ.1.2 (p.update σ.2 w) ∈ R := Iff.rfl -omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] in +omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] in theorem slice_mk_update {R : RelMfld I M I' M'} {σ : OneJetBundle I M I' M'} {p : DualPair <| TM σ.1.1} (x : E') : R.slice (OneJetBundle.mk σ.1.1 σ.1.2 (p.update σ.2 x)) p = (R.slice σ p : Set E') := by @@ -197,7 +197,7 @@ theorem slice_mk_update {R : RelMfld I M I' M'} {σ : OneJetBundle I M I' M'} def RelMfld.Ample (R : RelMfld I M I' M') : Prop := ∀ ⦃σ : OneJetBundle I M I' M'⦄ (p : DualPair <| TM σ.1.1), AmpleSet (R.slice σ p) -omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] in +omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] in theorem RelMfld.ample_iff (R : RelMfld I M I' M') : R.Ample ↔ ∀ ⦃σ : OneJetBundle I M I' M'⦄ (p : DualPair <| TM σ.1.1), σ ∈ R → AmpleSet (R.slice σ p) := by @@ -258,7 +258,7 @@ theorem is_sol (S : FamilyFormalSol J N R) {t : N} {x : M} : S t x ∈ R := S.is_sol' t x /-- Reindex a family along a smooth function `f`. -/ -def reindex (S : FamilyFormalSol J' N' R) (f : C^⊤⟮J, N; J', N'⟯) : FamilyFormalSol J N R := +def reindex (S : FamilyFormalSol J' N' R) (f : C^∞⟮J, N; J', N'⟯) : FamilyFormalSol J N R := ⟨S.toFamilyOneJetSec.reindex f, fun t ↦ S.is_sol' (f t)⟩ end FamilyFormalSol @@ -272,7 +272,7 @@ abbrev HtpyFormalSol (R : RelMfld I M I' M') := def mkHtpyFormalSol (F : ℝ → M → OneJetBundle I M I' M') (hsec : ∀ t x, (F t x).1.1 = x) (hsol : ∀ t x, F t x ∈ R) - (hsmooth : ContMDiff (𝓘(ℝ).prod I) ((I.prod I').prod 𝓘(ℝ, E →L[ℝ] E')) ⊤ ↿F) : HtpyFormalSol R + (hsmooth : ContMDiff (𝓘(ℝ).prod I) ((I.prod I').prod 𝓘(ℝ, E →L[ℝ] E')) ∞ ↿F) : HtpyFormalSol R where bs t m := (F t m).1.2 ϕ t m := (F t m).2 @@ -290,7 +290,7 @@ def mkHtpyFormalSol (F : ℝ → M → OneJetBundle I M I' M') (hsec : ∀ t x, @[simp] theorem mkHtpyFormalSol_apply (F : ℝ → M → OneJetBundle I M I' M') (hsec : ∀ t x, (F t x).1.1 = x) (hsol : ∀ t x, F t x ∈ R) - (hsmooth : ContMDiff (𝓘(ℝ).prod I) ((I.prod I').prod 𝓘(ℝ, E →L[ℝ] E')) ⊤ ↿F) (t : ℝ) : + (hsmooth : ContMDiff (𝓘(ℝ).prod I) ((I.prod I').prod 𝓘(ℝ, E →L[ℝ] E')) ∞ ↿F) (t : ℝ) : (mkHtpyFormalSol F hsec hsol hsmooth t : M → OneJetBundle I M I' M') = F t := by ext x <;> try rfl rw [hsec] @@ -387,12 +387,12 @@ 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) ∧ + (ContMDiff (IP.prod I) IX ∞ <| 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⟯ := + · let j : C^∞⟮IP, P; 𝓘(ℝ, ℝ).prod IP, ℝ × P⟯ := ⟨fun p ↦ (1, p), ContMDiff.prod_mk contMDiff_const contMDiff_id⟩ rw [show (uncurry fun s ↦ (𝓕 (1, s)).bs) = @@ -429,16 +429,16 @@ there are manifolds `X` and `Y` that will be vector spaces in the next section. variable {EX : Type*} [NormedAddCommGroup EX] [NormedSpace ℝ EX] {HX : Type*} [TopologicalSpace HX] {IX : ModelWithCorners ℝ EX HX} - {X : Type*} [TopologicalSpace X] [ChartedSpace HX X] [SmoothManifoldWithCorners IX X] + {X : Type*} [TopologicalSpace X] [ChartedSpace HX X] [IsManifold IX ∞ X] {EM : Type*} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type*} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} - {M : Type*} [TopologicalSpace M] [ChartedSpace HM M] [SmoothManifoldWithCorners IM M] + {M : Type*} [TopologicalSpace M] [ChartedSpace HM M] [IsManifold IM ∞ M] {EY : Type*} [NormedAddCommGroup EY] [NormedSpace ℝ EY] {HY : Type*} [TopologicalSpace HY] {IY : ModelWithCorners ℝ EY HY} - {Y : Type*} [TopologicalSpace Y] [ChartedSpace HY Y] [SmoothManifoldWithCorners IY Y] + {Y : Type*} [TopologicalSpace Y] [ChartedSpace HY Y] [IsManifold IY ∞ Y] {EN : Type*} [NormedAddCommGroup EN] [NormedSpace ℝ EN] {HN : Type*} [TopologicalSpace HN] {IN : ModelWithCorners ℝ EN HN} - {N : Type*} [TopologicalSpace N] [ChartedSpace HN N] [SmoothManifoldWithCorners IN N] + {N : Type*} [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} @@ -469,7 +469,7 @@ def OpenSmoothEmbedding.transfer : OneJetBundle IX X IY Y → OneJetBundle IM M OneJetBundle.map IY IN φ ψ fun x ↦ (φ.fderiv x).symm theorem OpenSmoothEmbedding.smooth_transfer : - ContMDiff ((IX.prod IY).prod 𝓘(ℝ, EX →L[ℝ] EY)) ((IM.prod IN).prod 𝓘(ℝ, EM →L[ℝ] EN)) ⊤ + ContMDiff ((IX.prod IY).prod 𝓘(ℝ, EX →L[ℝ] EY)) ((IM.prod IN).prod 𝓘(ℝ, EM →L[ℝ] EN)) ∞ (φ.transfer ψ) := by intro x refine ContMDiffAt.oneJetBundle_map (φ.contMDiff_to.contMDiffAt.comp _ contMDiffAt_snd) @@ -478,15 +478,15 @@ theorem OpenSmoothEmbedding.smooth_transfer : have' := ContMDiffAt.mfderiv (fun _ ↦ φ.invFun) (fun x : OneJetBundle IX X IY Y ↦ φ x.1.1) ((φ.contMDiffAt_inv <| _).comp (x, φ x.1.1) contMDiffAt_snd) - (φ.contMDiff_to.contMDiffAt.comp x (contMDiff_oneJetBundle_proj.fst x)) le_top + (φ.contMDiff_to.contMDiffAt.comp x (contMDiff_oneJetBundle_proj.fst x)) (mod_cast le_top) · simp [contMDiffOn_inv] at this; exact this exact mem_range_self _ theorem OneJetBundle.continuous_transfer : Continuous (φ.transfer ψ) := (OpenSmoothEmbedding.smooth_transfer _ _).continuous -omit [SmoothManifoldWithCorners IX X] [SmoothManifoldWithCorners IM M] - [SmoothManifoldWithCorners IY Y] [SmoothManifoldWithCorners IN N] in +omit [IsManifold IX ∞ X] [IsManifold IM ∞ M] + [IsManifold IY ∞ Y] [IsManifold IN ∞ N] in theorem OpenSmoothEmbedding.range_transfer : range (φ.transfer ψ) = π _ (OneJetSpace IM IN) ⁻¹' range φ ×ˢ range ψ := by ext σ; constructor @@ -506,7 +506,7 @@ theorem OpenSmoothEmbedding.range_transfer : erw [(φ.fderiv x).apply_symm_apply] rfl -omit [SmoothManifoldWithCorners IX X] [SmoothManifoldWithCorners IY Y] in +omit [IsManifold IX ∞ X] [IsManifold IY ∞ Y] in theorem OpenSmoothEmbedding.isOpen_range_transfer : IsOpen (range (φ.transfer ψ)) := by rw [φ.range_transfer ψ] exact (φ.isOpen_range.prod ψ.isOpen_range).preimage oneJetBundle_proj_continuous @@ -522,8 +522,8 @@ instance (y : Y) : NormedAddCommGroup (TY y) := by assumption instance (y : Y) : NormedSpace ℝ (TY y) := by assumption -omit [SmoothManifoldWithCorners IX X] [SmoothManifoldWithCorners IM M] - [SmoothManifoldWithCorners IY Y] [SmoothManifoldWithCorners IN N] in +omit [IsManifold IX ∞ X] [IsManifold IM ∞ M] + [IsManifold IY ∞ Y] [IsManifold IN ∞ N] in /-- Ampleness survives localization -/ theorem RelMfld.Ample.localize (hR : R.Ample) : (R.localize φ ψ).Ample := by intro x p @@ -620,7 +620,7 @@ def OneJetBundle.embedding : OpenSmoothEmbedding IXY J¹XY IMN J¹MN where left_inv' {σ} := by rw [OpenSmoothEmbedding.transfer, OneJetBundle.map_map]; rotate_left · exact (ψ.contMDiffAt_inv'.mdifferentiableAt (by simp)) - · exact ψ.contMDiff_to.contMDiffAt.mdifferentiableAt (le_top) + · exact ψ.contMDiff_to.contMDiffAt.mdifferentiableAt (mod_cast le_top) conv_rhs => rw [← OneJetBundle.map_id σ] congr 1 · rw [OpenSmoothEmbedding.invFun_comp_coe] @@ -640,7 +640,8 @@ def OneJetBundle.embedding : OpenSmoothEmbedding IXY J¹XY IMN J¹MN where have' := ContMDiffAt.mfderiv (fun _ ↦ φ) (fun x : OneJetBundle IM M IN N ↦ φ.invFun x.1.1) (φ.contMDiff_to.contMDiffAt.comp _ contMDiffAt_snd) - ((φ.contMDiffAt_inv _).comp _ (contMDiff_oneJetBundle_proj.fst (φ.transfer ψ x))) le_top + ((φ.contMDiffAt_inv _).comp _ (contMDiff_oneJetBundle_proj.fst (φ.transfer ψ x))) + (mod_cast le_top) · dsimp only [id] refine this.congr_of_eventuallyEq ?_ refine Filter.eventually_of_mem ((φ.isOpen_range_transfer ψ).mem_nhds (mem_range_self _)) ?_ diff --git a/SphereEversion/Global/SmoothEmbedding.lean b/SphereEversion/Global/SmoothEmbedding.lean index 84d29302..4e3b326f 100644 --- a/SphereEversion/Global/SmoothEmbedding.lean +++ b/SphereEversion/Global/SmoothEmbedding.lean @@ -13,7 +13,7 @@ noncomputable section open Set Equiv -open scoped Manifold Topology +open scoped Manifold Topology ContDiff section General @@ -28,8 +28,8 @@ structure OpenSmoothEmbedding where invFun : M' → M left_inv' : ∀ {x}, invFun (toFun x) = x isOpen_range : IsOpen (range toFun) - contMDiff_to : ContMDiff I I' ⊤ toFun - contMDiffOn_inv : ContMDiffOn I' I ⊤ invFun (range toFun) + contMDiff_to : ContMDiff I I' ∞ toFun + contMDiffOn_inv : ContMDiffOn I' I ∞ invFun (range toFun) attribute [coe] OpenSmoothEmbedding.toFun @@ -59,10 +59,10 @@ theorem right_inv {y : M'} (hy : y ∈ range f) : f (f.invFun y) = y := by obtain ⟨x, rfl⟩ := hy; rw [f.left_inv] -theorem contMDiffAt_inv {y : M'} (hy : y ∈ range f) : ContMDiffAt I' I ⊤ f.invFun y := +theorem contMDiffAt_inv {y : M'} (hy : y ∈ range f) : ContMDiffAt I' I ∞ f.invFun y := (f.contMDiffOn_inv y hy).contMDiffAt <| f.isOpen_range.mem_nhds hy -theorem contMDiffAt_inv' {x : M} : ContMDiffAt I' I ⊤ f.invFun (f x) := +theorem contMDiffAt_inv' {x : M} : ContMDiffAt I' I ∞ f.invFun (f x) := f.contMDiffAt_inv <| mem_range_self x theorem leftInverse : Function.LeftInverse f.invFun f := @@ -82,15 +82,15 @@ theorem coe_comp_invFun_eventuallyEq (x : M) : f ∘ f.invFun =ᶠ[𝓝 (f x)] i section -variable [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] +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 I x ≃L[𝕜] TangentSpace I' (f x) := have h₁ : MDifferentiableAt I' I f.invFun (f x) := - ((f.contMDiffOn_inv (f x) (mem_range_self x)).mdifferentiableWithinAt le_top).mdifferentiableAt + ((f.contMDiffOn_inv (f x) (mem_range_self x)).mdifferentiableWithinAt (mod_cast le_top)).mdifferentiableAt (f.isOpenMap.range_mem_nhds x) - have h₂ : MDifferentiableAt I I' f x := f.contMDiff_to.mdifferentiableAt le_top + have h₂ : MDifferentiableAt I I' f x := f.contMDiff_to.mdifferentiableAt (mod_cast le_top) ContinuousLinearEquiv.equivOfInverse (mfderiv I I' f x) (mfderiv I' I f.invFun (f x)) (by intro v @@ -106,18 +106,18 @@ def fderiv (x : M) : TangentSpace I x ≃L[𝕜] TangentSpace I' (f x) := (f.coe_comp_invFun_eventuallyEq x)).mfderiv, ContinuousLinearMap.coe_id', id]) -omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] in +omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] in @[simp] theorem fderiv_coe (x : M) : (f.fderiv x : TangentSpace I x →L[𝕜] TangentSpace I' (f x)) = mfderiv I I' f x := by ext; rfl -omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] in +omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] in @[simp] theorem fderiv_symm_coe (x : M) : ((f.fderiv x).symm : TangentSpace I' (f x) →L[𝕜] TangentSpace I x) = mfderiv I' I f.invFun (f x) := by ext; rfl -omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] in +omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] in theorem fderiv_symm_coe' {x : M'} (hx : x ∈ range f) : ((f.fderiv (f.invFun x)).symm : TangentSpace I' (f (f.invFun x)) →L[𝕜] TangentSpace I (f.invFun x)) = @@ -238,14 +238,14 @@ universe u variable {F H : Type*} (M : Type u) [NormedAddCommGroup F] [NormedSpace ℝ F] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] - (IF : ModelWithCorners ℝ F H) [SmoothManifoldWithCorners IF M] + (IF : ModelWithCorners ℝ F H) [IsManifold IF ∞ M] /- Clearly should be generalised. Maybe what we really want is a theory of local diffeomorphisms. Note that the input `f` is morally an `OpenSmoothEmbedding` but stated in terms of `ContDiff` instead of `ContMDiff`. This is more convenient for our purposes. -/ def openSmoothEmbOfDiffeoSubsetChartTarget (x : M) {f : PartialHomeomorph F F} (hf₁ : f.source = univ) - (hf₂ : ContDiff ℝ (⊤: ℕ∞) f) (hf₃ : ContDiffOn ℝ (⊤: ℕ∞) f.symm f.target) + (hf₂ : ContDiff ℝ ∞ f) (hf₃ : ContDiffOn ℝ ∞ f.symm f.target) (hf₄ : range f ⊆ IF '' (chartAt H x).target) : OpenSmoothEmbedding 𝓘(ℝ, F) F IF M where toFun := (extChartAt IF x).symm ∘ f @@ -282,13 +282,13 @@ def openSmoothEmbOfDiffeoSubsetChartTarget (x : M) {f : PartialHomeomorph F F} ( @[simp] theorem coe_openSmoothEmbOfDiffeoSubsetChartTarget (x : M) {f : PartialHomeomorph F F} - (hf₁ : f.source = univ) (hf₂ : ContDiff ℝ (⊤: ℕ∞) f) (hf₃ : ContDiffOn ℝ (⊤: ℕ∞) f.symm f.target) + (hf₁ : f.source = univ) (hf₂ : ContDiff ℝ ∞ f) (hf₃ : ContDiffOn ℝ ∞ f.symm f.target) (hf₄ : range f ⊆ IF '' (chartAt H x).target) : (openSmoothEmbOfDiffeoSubsetChartTarget M IF x hf₁ hf₂ hf₃ hf₄ : F → M) = (extChartAt IF x).symm ∘ f := by simp [openSmoothEmbOfDiffeoSubsetChartTarget] theorem range_openSmoothEmbOfDiffeoSubsetChartTarget (x : M) {f : PartialHomeomorph F F} - (hf₁ : f.source = univ) (hf₂ : ContDiff ℝ (⊤: ℕ∞) f) (hf₃ : ContDiffOn ℝ (⊤: ℕ∞) f.symm f.target) + (hf₁ : f.source = univ) (hf₂ : ContDiff ℝ ∞ f) (hf₃ : ContDiffOn ℝ ∞ f.symm f.target) (hf₄ : range f ⊆ IF '' (chartAt H x).target) : range (openSmoothEmbOfDiffeoSubsetChartTarget M IF x hf₁ hf₂ hf₃ hf₄) = (extChartAt IF x).symm '' range f := by @@ -327,8 +327,8 @@ theorem nice_atlas' {ι : Type*} {s : ι → Set M} (s_op : ∀ j, IsOpen <| s j obtain ⟨t, ht₁, ht₂, ht₃, ht₄⟩ := exists_countable_locallyFinite_cover surjective_id hW₀ hW₁ hB let g : M × ℝ → PartialHomeomorph F F := fun z ↦ diffeomorphToNhd (extChartAt IF z.1 z.1) z.2 have hg₁ : ∀ z, (g z).source = univ := by simp [g] - have hg₂ : ∀ z, ContDiff ℝ (⊤: ℕ∞) (g z) := by simp [g] - have hg₃ : ∀ z, ContDiffOn ℝ (⊤: ℕ∞) (g z).symm (g z).target := by simp [g] + have hg₂ : ∀ z, ContDiff ℝ ∞ (g z) := by simp [g] + have hg₃ : ∀ z, ContDiffOn ℝ ∞ (g z).symm (g z).target := by simp [g] refine ⟨M × ℝ, t, fun z ↦ openSmoothEmbOfDiffeoSubsetChartTarget M IF z.1.1 (hg₁ z.1) (hg₂ z.1) (hg₃ z.1) ?_, ht₁, fun z ↦ ?_, ?_, ?_⟩ @@ -421,10 +421,10 @@ open Function /-- This is lemma `lem:smooth_updating` in the blueprint. -/ theorem smooth_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 : ContMDiff IM' IM ⊤ k) + (hK : IsClosed (φ '' K)) (hf : ContMDiff (IM'.prod IM) IN ∞ (uncurry f)) + (hg : ContMDiff (IM'.prod IX) IY ∞ (uncurry g)) (hk : ContMDiff IM' IM ∞ k) (hg' : ∀ y x, x ∉ K → f y (φ x) = ψ (g y x)) : - ContMDiff IM' IN ⊤ fun x ↦ update φ ψ (f x) (g x) (k x) := by + ContMDiff IM' IN ∞ 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 ↦ nice_update_of_eq_outside_compact_aux φ ψ (f x) (g x) (hg' x) hx refine contMDiff_of_locally_contMDiffOn fun x ↦ ?_ @@ -441,7 +441,7 @@ theorem smooth_update (f : M' → M → N) (g : M' → X → Y) {k : M' → M} { (contMDiffOn_congr h₄).mpr <| ψ.contMDiff_to.comp_contMDiffOn <| hg.comp_contMDiffOn (contMDiffOn_id.prod_mk <| φ.contMDiffOn_inv.comp hk.contMDiffOn Subset.rfl)⟩ · refine ⟨k ⁻¹' V, h₂, ?_, (contMDiffOn_congr hK').mpr - (hf.comp ((contMDiff_id (n := ⊤)).prod_mk hk)).contMDiffOn⟩ + (hf.comp ((contMDiff_id (n := ∞)).prod_mk hk)).contMDiffOn⟩ exact ((Set.ext_iff.mp h₃ (k x)).mpr trivial).resolve_right hx end NonMetric diff --git a/SphereEversion/Global/TwistOneJetSec.lean b/SphereEversion/Global/TwistOneJetSec.lean index e5fcbe18..abff5332 100644 --- a/SphereEversion/Global/TwistOneJetSec.lean +++ b/SphereEversion/Global/TwistOneJetSec.lean @@ -11,14 +11,14 @@ noncomputable section open Set Equiv Bundle ContinuousLinearMap -open scoped Manifold Bundle Topology +open scoped Manifold Bundle Topology ContDiff section ArbitraryField universe u v variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (M : Type*) - [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {F : Type*} + [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M] {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type*} [TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type*} [TopologicalSpace N] [ChartedSpace G N] (V : Type*) [NormedAddCommGroup V] [NormedSpace 𝕜 V] @@ -34,8 +34,8 @@ 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₀ ↔ ContMDiffAt J I ⊤ (fun x ↦ (f x).1) x₀ ∧ - ContMDiffAt J 𝓘(𝕜, E →L[𝕜] V) ⊤ (fun x ↦ show E →L[𝕜] V from + ContMDiffAt J (I.prod 𝓘(𝕜, E →L[𝕜] V)) ∞ f x₀ ↔ ContMDiffAt J I ∞ (fun x ↦ (f x).1) x₀ ∧ + ContMDiffAt J 𝓘(𝕜, E →L[𝕜] V) ∞ (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,9 +43,9 @@ theorem contMDiffAt_one_jet_eucl_bundle' {x₀ : N} : simp_rw [ContinuousLinearMap.id_comp] theorem contMDiffAt_one_jet_eucl_bundle {x₀ : N} : - ContMDiffAt J (I.prod 𝓘(𝕜, E →L[𝕜] V)) ⊤ f x₀ ↔ - ContMDiffAt J I ⊤ (fun x ↦ (f x).1) x₀ ∧ - ContMDiffAt J 𝓘(𝕜, E →L[𝕜] V) ⊤ (fun x ↦ show E →L[𝕜] V from + ContMDiffAt J (I.prod 𝓘(𝕜, E →L[𝕜] V)) ∞ f x₀ ↔ + ContMDiffAt J I ∞ (fun x ↦ (f x).1) x₀ ∧ + ContMDiffAt J 𝓘(𝕜, E →L[𝕜] V) ∞ (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 @@ -61,18 +61,18 @@ theorem contMDiffAt_one_jet_eucl_bundle {x₀ : N} : simp_rw [ContinuousLinearMap.id_comp] theorem ContMDiffAt.one_jet_eucl_bundle_mk' {f : N → M} {ϕ : N → E →L[𝕜] V} {x₀ : N} - (hf : ContMDiffAt J I ⊤ f x₀) - (hϕ : ContMDiffAt J 𝓘(𝕜, E →L[𝕜] V) ⊤ (fun x ↦ show E →L[𝕜] V from + (hf : ContMDiffAt J I ∞ f x₀) + (hϕ : ContMDiffAt J 𝓘(𝕜, E →L[𝕜] V) ∞ (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)) ⊤ + ContMDiffAt J (I.prod 𝓘(𝕜, E →L[𝕜] V)) ∞ (fun x ↦ Bundle.TotalSpace.mk (f x) (ϕ x) : N → J¹[𝕜, E, I, M, V]) x₀ := contMDiffAt_one_jet_eucl_bundle'.mpr ⟨hf, hϕ⟩ theorem ContMDiffAt.one_jet_eucl_bundle_mk {f : N → M} {ϕ : N → E →L[𝕜] V} {x₀ : N} - (hf : ContMDiffAt J I ⊤ f x₀) - (hϕ : ContMDiffAt J 𝓘(𝕜, E →L[𝕜] V) ⊤ (fun x ↦ show E →L[𝕜] V from + (hf : ContMDiffAt J I ∞ f x₀) + (hϕ : ContMDiffAt J 𝓘(𝕜, E →L[𝕜] V) ∞ (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)) ⊤ + ContMDiffAt J (I.prod 𝓘(𝕜, E →L[𝕜] V)) ∞ (fun x ↦ Bundle.TotalSpace.mk (f x) (ϕ x) : N → J¹[𝕜, E, I, M, V]) x₀ := contMDiffAt_one_jet_eucl_bundle.mpr ⟨hf, hϕ⟩ @@ -85,7 +85,7 @@ section Sections structure OneJetEuclSec where toFun : M → J¹[𝕜, E, I, M, V] is_sec' : ∀ p, (toFun p).1 = p - smooth' : ContMDiff I (I.prod 𝓘(𝕜, E →L[𝕜] V)) ⊤ toFun + smooth' : ContMDiff I (I.prod 𝓘(𝕜, E →L[𝕜] V)) ∞ toFun variable {I M V} @@ -100,7 +100,7 @@ theorem OneJetEuclSec.is_sec (s : OneJetEuclSec I M V) (p : M) : (s p).1 = p := s.is_sec' p @[simp] -theorem OneJetEuclSec.smooth (s : OneJetEuclSec I M V) : ContMDiff I (I.prod 𝓘(𝕜, E →L[𝕜] V)) ⊤ s := +theorem OneJetEuclSec.smooth (s : OneJetEuclSec I M V) : ContMDiff I (I.prod 𝓘(𝕜, E →L[𝕜] V)) ∞ s := s.smooth' end Sections @@ -121,9 +121,9 @@ def proj (v : OneJetBundle I M 𝓘(𝕜, V) V) : J¹[𝕜, E, I, M, V] := ⟨v.1.1, v.2⟩ theorem smooth_proj : ContMDiff ((I.prod 𝓘(𝕜, V)).prod 𝓘(𝕜, E →L[𝕜] V)) (I.prod 𝓘(𝕜, E →L[𝕜] V)) - ⊤ (proj I M V) := by + ∞ (proj I M V) := by intro x₀ - have : ContMDiffAt ((I.prod 𝓘(𝕜, V)).prod 𝓘(𝕜, E →L[𝕜] V)) _ ⊤ id x₀ := contMDiffAt_id + have : ContMDiffAt ((I.prod 𝓘(𝕜, V)).prod 𝓘(𝕜, E →L[𝕜] V)) _ ∞ id x₀ := contMDiffAt_id simp_rw (config := { unfoldPartialApp := true }) [contMDiffAt_oneJetBundle, inTangentCoordinates, inCoordinates, TangentBundle.continuousLinearMapAt_model_space, ContinuousLinearMap.one_def] at this dsimp only [TangentSpace] at this @@ -149,9 +149,9 @@ def incl (v : J¹[𝕜, E, I, M, V] × V) : OneJetBundle I M 𝓘(𝕜, V) V := ⟨(v.1.1, v.2), v.1.2⟩ theorem smooth_incl : ContMDiff ((I.prod 𝓘(𝕜, E →L[𝕜] V)).prod 𝓘(𝕜, V)) - ((I.prod 𝓘(𝕜, V)).prod 𝓘(𝕜, E →L[𝕜] V)) ⊤ (incl I M V) := by + ((I.prod 𝓘(𝕜, V)).prod 𝓘(𝕜, E →L[𝕜] V)) ∞ (incl I M V) := by intro x₀ - have : ContMDiffAt ((I.prod 𝓘(𝕜, E →L[𝕜] V)).prod 𝓘(𝕜, V)) _ ⊤ Prod.fst x₀ := contMDiffAt_fst + have : ContMDiffAt ((I.prod 𝓘(𝕜, E →L[𝕜] V)).prod 𝓘(𝕜, V)) _ ∞ Prod.fst x₀ := contMDiffAt_fst rw [contMDiffAt_one_jet_eucl_bundle] at this refine this.1.oneJetBundle_mk contMDiffAt_snd ?_ unfold inTangentCoordinates inCoordinates TangentSpace @@ -159,12 +159,12 @@ theorem smooth_incl : ContMDiff ((I.prod 𝓘(𝕜, E →L[𝕜] V)).prod 𝓘( ContinuousLinearMap.id_comp] exact this.2 -omit [SmoothManifoldWithCorners I M] in +omit [IsManifold I ∞ M] in @[simp] theorem incl_fst_fst (v : J¹[𝕜, E, I, M, V] × V) : (incl I M V v).1.1 = v.1.1 := rfl -omit [SmoothManifoldWithCorners I M] in +omit [IsManifold I ∞ M] in @[simp] theorem incl_snd (v : J¹[𝕜, E, I, M, V] × V) : (incl I M V v).1.2 = v.2 := rfl @@ -177,7 +177,7 @@ section familyTwist variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type*} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type*) [TopologicalSpace M] [ChartedSpace H M] - [SmoothManifoldWithCorners I M] (V : Type*) [NormedAddCommGroup V] [NormedSpace ℝ V] + [IsManifold I ∞ M] (V : Type*) [NormedAddCommGroup V] [NormedSpace ℝ V] (V' : Type*) [NormedAddCommGroup V'] [NormedSpace ℝ V'] {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type*} [TopologicalSpace G] (J : ModelWithCorners ℝ F G) (N : Type*) [TopologicalSpace N] [ChartedSpace G N] @@ -187,7 +187,7 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type*} [Top structure FamilyOneJetEuclSec where toFun : N × M → J¹[ℝ, E, I, M, V] is_sec' : ∀ p, (toFun p).1 = p.2 - smooth' : ContMDiff (J.prod I) (I.prod 𝓘(ℝ, E →L[ℝ] V)) ⊤ toFun + smooth' : ContMDiff (J.prod I) (I.prod 𝓘(ℝ, E →L[ℝ] V)) ∞ toFun instance : FunLike (FamilyOneJetEuclSec I M V J N) (N × M) J¹[ℝ, E, I, M, V] where coe := FamilyOneJetEuclSec.toFun @@ -204,12 +204,12 @@ theorem FamilyOneJetEuclSec.is_sec (s : FamilyOneJetEuclSec I M V J N) (p : N × @[simp] theorem FamilyOneJetEuclSec.smooth (s : FamilyOneJetEuclSec I M V J N) : - ContMDiff (J.prod I) (I.prod 𝓘(ℝ, E →L[ℝ] V)) ⊤ s := + ContMDiff (J.prod I) (I.prod 𝓘(ℝ, E →L[ℝ] V)) ∞ s := s.smooth' variable {V'} -def familyJoin {f : N × M → V} (hf : ContMDiff (J.prod I) 𝓘(ℝ, V) ⊤ f) +def familyJoin {f : N × M → V} (hf : ContMDiff (J.prod I) 𝓘(ℝ, V) ∞ 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,7 +219,7 @@ def familyJoin {f : N × M → V} (hf : ContMDiff (J.prod I) 𝓘(ℝ, V) ⊤ f) ext : 1 <;> simp def familyTwist (s : OneJetEuclSec I M V) (i : N × M → V →L[ℝ] V') - (i_smooth : ∀ x₀ : N × M, ContMDiffAt (J.prod I) 𝓘(ℝ, V →L[ℝ] V') ⊤ i x₀) : + (i_smooth : ∀ x₀ : N × M, ContMDiffAt (J.prod I) 𝓘(ℝ, V →L[ℝ] V') ∞ i x₀) : FamilyOneJetEuclSec I M V' J N where toFun p := ⟨p.2, (i p).comp (s p.2).2⟩ @@ -228,7 +228,7 @@ def familyTwist (s : OneJetEuclSec I M V) (i : N × M → V →L[ℝ] V') intro x₀ refine contMDiffAt_snd.one_jet_eucl_bundle_mk' ?_ simp_rw [ContinuousLinearMap.comp_assoc] - have : ContMDiffAt (J.prod I) _ ⊤ (fun x : N × M ↦ _) x₀ := s.smooth.comp contMDiff_snd x₀ + have : ContMDiffAt (J.prod I) _ ∞ (fun x : N × M ↦ _) x₀ := s.smooth.comp contMDiff_snd x₀ rw [contMDiffAt_one_jet_eucl_bundle'] at this refine (i_smooth x₀).clm_comp ?_ convert this.2 <;> simp [s.is_sec] diff --git a/SphereEversion/Indexing.lean b/SphereEversion/Indexing.lean index b4079f02..59606163 100644 --- a/SphereEversion/Indexing.lean +++ b/SphereEversion/Indexing.lean @@ -169,3 +169,4 @@ theorem IndexType.exists_by_induction {α : Type*} (P : IndexType n → α → P convert hF' _ _ (key i) hi rcases i.exists_castSucc_eq hi with ⟨i, rfl⟩ simp_rw [IndexType.succ_castSuccEmb, f, induction_succ] + rfl diff --git a/SphereEversion/InductiveConstructions.lean b/SphereEversion/InductiveConstructions.lean index 03962b38..059d371d 100644 --- a/SphereEversion/InductiveConstructions.lean +++ b/SphereEversion/InductiveConstructions.lean @@ -241,7 +241,7 @@ theorem relative_inductive_construction_of_loc {X Y : Type*} [EMetricSpace X] · rwa [hK₁'K₂'] at hf · apply h'f.filter_mono; gcongr rcases inductive_construction_of_loc P₀ P₀' P₁ hf₀ loc ind' with ⟨f, hf⟩ - simp only [forall_and, forall_restrictGermPredicate_iff] at hf ⊢ + simp only [forall_and, forall_restrictGermPredicate_iff, P₀'] at hf ⊢ exact ⟨f, ⟨hf.1, hf.2.2⟩, hf.2.1⟩ end inductive_construction diff --git a/SphereEversion/Local/DualPair.lean b/SphereEversion/Local/DualPair.lean index 993af256..1859d59f 100644 --- a/SphereEversion/Local/DualPair.lean +++ b/SphereEversion/Local/DualPair.lean @@ -35,6 +35,8 @@ open Function ContinuousLinearMap open LinearMap (ker) +open scoped ContDiff + /-! ## General theory -/ section NoNorm @@ -182,7 +184,6 @@ end NoNorm namespace DualPair -local notation "∞" => (⊤ : ℕ∞) variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] diff --git a/SphereEversion/Local/HPrinciple.lean b/SphereEversion/Local/HPrinciple.lean index 83f937b7..6bb7a429 100644 --- a/SphereEversion/Local/HPrinciple.lean +++ b/SphereEversion/Local/HPrinciple.lean @@ -53,14 +53,12 @@ need to access its components only once. noncomputable section -open scoped unitInterval Filter Topology +open scoped unitInterval Filter Topology ContDiff open Filter Set RelLoc open LinearMap (ker) -local notation "∞" => (⊤ : ℕ∞) - variable (E : Type*) [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]{G : Type*} [NormedAddCommGroup G] [NormedSpace ℝ G] @@ -527,7 +525,7 @@ theorem RelLoc.FormalSol.improve (𝓕 : FormalSol R) (h_hol : ∀ᶠ x near L.C by_cases ht : t ≤ 1 / 2 · simp only [ht, hx, hHK₁, HtpyJetSec.comp_of_le, not_false_iff] · simp only [ht, hx, hH₁_K₁, improveStep_rel_compl_K₁, HtpyJetSec.comp_of_not_le, - not_false_iff] + not_false_iff, S] · -- C⁰-close intro x t by_cases ht : t ≤ 1 / 2 diff --git a/SphereEversion/Local/OneJet.lean b/SphereEversion/Local/OneJet.lean index 354f09a3..146270da 100644 --- a/SphereEversion/Local/OneJet.lean +++ b/SphereEversion/Local/OneJet.lean @@ -27,9 +27,8 @@ noncomputable section open Set Function Real Filter -open scoped unitInterval Topology +open scoped unitInterval Topology ContDiff -local notation "∞" => (⊤ : ℕ∞) variable (E : Type*) [NormedAddCommGroup E] [NormedSpace ℝ E] (F : Type*) [NormedAddCommGroup F] [NormedSpace ℝ F] diff --git a/SphereEversion/Local/ParametricHPrinciple.lean b/SphereEversion/Local/ParametricHPrinciple.lean index f2d5b037..72f8e1e2 100644 --- a/SphereEversion/Local/ParametricHPrinciple.lean +++ b/SphereEversion/Local/ParametricHPrinciple.lean @@ -21,9 +21,7 @@ open Metric FiniteDimensional Set Function RelLoc open LinearMap (ker) -open scoped Topology Pointwise - -local notation "∞" => (⊤ : ℕ∞) +open scoped Topology Pointwise ContDiff section ParameterSpace @@ -192,10 +190,10 @@ theorem RelLoc.FamilyFormalSol.uncurry_φ' (S : R.FamilyFormalSol P) (p : P × E def FamilyJetSec.curry (S : FamilyJetSec (P × E) F G) : FamilyJetSec E F (G × P) where f p x := (S p.1).f (p.2, x) φ p x := (S p.1).φ (p.2, x) ∘L fderiv ℝ (fun x ↦ (p.2, x)) x - f_diff := S.f_diff.comp ((contDiff_prodAssoc : ContDiff ℝ ⊤ (Equiv.prodAssoc G P E)).of_le le_top) + f_diff := S.f_diff.comp ((contDiff_prodAssoc : ContDiff ℝ ω (Equiv.prodAssoc G P E)).of_le le_top) φ_diff := by refine (S.φ_diff.comp - ((contDiff_prodAssoc : ContDiff ℝ ⊤ (Equiv.prodAssoc G P E)).of_le le_top)).clm_comp ?_ + ((contDiff_prodAssoc : ContDiff ℝ ω (Equiv.prodAssoc G P E)).of_le le_top)).clm_comp ?_ refine ContDiff.fderiv ?_ contDiff_snd le_top exact contDiff_fst.fst.snd.prod contDiff_snd diff --git a/SphereEversion/Local/SphereEversion.lean b/SphereEversion/Local/SphereEversion.lean index 09907d3d..70892462 100644 --- a/SphereEversion/Local/SphereEversion.lean +++ b/SphereEversion/Local/SphereEversion.lean @@ -231,7 +231,7 @@ theorem loc_immersion_rel_ample (n : ℕ) [Fact (dim E = n + 1)] (h : finrank let p'' : DualPair (ℝ ∙ x)ᗮ := ⟨p.π.comp j, ⟨v', v'_in⟩, hπv'⟩ have eq : ((ℝ ∙ x)ᗮ : Set E).restrict (p'.update φ w) = p''.update (φ.comp j) w := by ext z - simp only [p', j, DualPair.update, restrict_apply, ContinuousLinearMap.add_apply, + simp only [p', j, DualPair.update, restrict_apply, ContinuousLinearMap.add_apply, p'', ContinuousLinearMap.coe_comp', coe_subtypeL', Submodule.coe_subtype, comp_apply, coe_mk] have eq' : map (φ.comp j) (ker p''.π) = map φ (ker p.π ⊓ (ℝ ∙ x)ᗮ) := by have : map (↑j) (ker p''.π) = ker p.π ⊓ (ℝ ∙ x)ᗮ := by @@ -258,7 +258,7 @@ def locFormalEversionAuxφ [Fact (dim E = 3)] (ω : Orientation ℝ E (Fin 3)) ( ω.rot (t, x) - (2 * t) • Submodule.subtypeL (ℝ ∙ x) ∘L orthogonalProjection (ℝ ∙ x) section AssumeFiniteDimensional -local notation "∞" => (⊤ : ℕ∞) +local notation "∞" => ((⊤ : ℕ∞) : WithTop ℕ∞) variable [Fact (dim E = 3)] [FiniteDimensional ℝ E] (ω : Orientation ℝ E (Fin 3)) @@ -411,7 +411,7 @@ end AssumeFiniteDimensional open scoped unitInterval -local notation "∞" => (⊤ : ℕ∞) +local notation "∞" => ((⊤ : ℕ∞) : WithTop ℕ∞) theorem sphere_eversion_of_loc [Fact (dim E = 3)] : ∃ f : ℝ → E → E, diff --git a/SphereEversion/Loops/DeltaMollifier.lean b/SphereEversion/Loops/DeltaMollifier.lean index d1d5b977..6c5b51fb 100644 --- a/SphereEversion/Loops/DeltaMollifier.lean +++ b/SphereEversion/Loops/DeltaMollifier.lean @@ -30,7 +30,7 @@ convolutions. noncomputable section open Set Function MeasureTheory.MeasureSpace ContinuousLinearMap -open scoped Topology Filter Convolution +open scoped Topology Filter Convolution ContDiff variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] section @@ -192,8 +192,6 @@ theorem intervalIntegral_periodize_smul (f : ℝ → ℝ) (γ : Loop E) {a b c d end -local notation "∞" => (⊤ : ℕ∞) - section DeltaApprox /-! ## An approximate Dirac "on the circle". -/ diff --git a/SphereEversion/Loops/Exists.lean b/SphereEversion/Loops/Exists.lean index de8ce64a..0517ef91 100644 --- a/SphereEversion/Loops/Exists.lean +++ b/SphereEversion/Loops/Exists.lean @@ -1,13 +1,11 @@ import SphereEversion.Loops.Reparametrization import SphereEversion.ToMathlib.Analysis.CutOff -import SphereEversion.ToMathlib.Topology.HausdorffDistance +import Mathlib.Topology.MetricSpace.HausdorffDistance noncomputable section open Set Function Int Metric Filter Real MeasureTheory -open scoped MeasureTheory.Measure Topology unitInterval - -local notation "∞" => (⊤ : ℕ∞) +open scoped MeasureTheory.Measure Topology unitInterval ContDiff variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type*} [NormedAddCommGroup F] {g b : E → F} {Ω : Set (E × F)} {U K C : Set E} @@ -30,7 +28,8 @@ theorem exist_loops_aux1 (hK : IsCompact K) (hΩ_op : IsOpen Ω) (hb : 𝒞 ∞ surrounding_loop_of_convexHull isOpen_univ isConnected_univ (by rw [convexHull_univ]; exact mem_univ 0) (mem_univ (0 : F)) obtain ⟨ε₀, hε₀, V, hV, hεΩ⟩ := - hK.exists_thickening_image hΩ_op (continuous_id.prod_mk hb.continuous) fun x _ ↦ b_in x + hK.exists_thickening_image_subset hΩ_op + (fun x hx ↦ (continuous_id.prod_mk hb.continuous).continuousAt) fun x _ ↦ b_in x let range_γ₀ := (fun i : ℝ × ℝ ↦ ‖γ₀ i.1 i.2‖) '' I ×ˢ I have h4γ₀ : BddAbove range_γ₀ := (isCompact_Icc.prod isCompact_Icc).bddAbove_image hγ₀_cont.norm.continuousOn @@ -202,14 +201,22 @@ theorem exist_loops_aux2 [FiniteDimensional ℝ E] (hK : IsCompact K) (hΩ_op : ((EventuallyEq.rfl.prod_mk <| EventuallyEq.rfl.prod_mk <| (fract_eventuallyEq hs).comp_tendsto continuousAt_id.snd'.snd').fun_comp ↿γ₅) refine ⟨γ, ⟨⟨?_, ?_, ?_, ?_, hγ.continuous⟩, ?_⟩, hγ, ?_⟩ - · intro x t; simp_rw [fract_zero]; rw [hγ₅C]; · exact hγ₃.base x _ - exact Or.inr (by rw [mem_preimage, fract_zero]; exact h0C₁) - · intro x s; simp_rw [smoothTransition.zero_of_nonpos le_rfl]; rw [hγ₅C] + · intro x t + simp_rw [γ, fract_zero] + rw [hγ₅C] + · exact hγ₃.base x _ + · exact Or.inr (by rw [mem_preimage, fract_zero]; exact h0C₁) + · intro x s + simp_rw [γ, smoothTransition.zero_of_nonpos le_rfl] + rw [hγ₅C] · exact hγ₃.t₀ x (fract s) · exact Or.inl (show (0 : ℝ) ≤ 5⁻¹ by norm_num) - · intro x t s; simp_rw [smoothTransition_projI] - · rintro x -; apply hγε₁; intro s - simp_rw [← (γ₃ x 1).fract_eq s, smoothTransition.one_of_one_le le_rfl] + · intro x t s + simp_rw [γ, smoothTransition_projI] + · rintro x - + apply hγε₁ + intro s + simp_rw [← (γ₃ x 1).fract_eq s, γ, smoothTransition.one_of_one_le le_rfl] exact (hγ₅₄ (x, 1, fract s)).trans_le ((min_le_left _ _).trans <| min_le_right _ _) · rintro x - t - s -; rw [← not_mem_compl_iff] by_cases hΩ : Ωᶜ.Nonempty; swap diff --git a/SphereEversion/Loops/Reparametrization.lean b/SphereEversion/Loops/Reparametrization.lean index 9691c859..75671c4e 100644 --- a/SphereEversion/Loops/Reparametrization.lean +++ b/SphereEversion/Loops/Reparametrization.lean @@ -299,8 +299,9 @@ theorem localCenteringDensity_integral_eq_one (hy : y ∈ γ.localCenteringDensi · have h : γ.approxSurroundingPointsAt x y n ∈ affineBases ι ℝ F := γ.approxSurroundingPointsAt_mem_affineBases x y hy simp_rw [← smul_eq_mul, intervalIntegral.integral_smul, deltaMollifier_integral_eq_one, - Algebra.id.smul_eq_mul, mul_one, evalBarycentricCoords_apply_of_mem_bases ι ℝ F (g y) h, - AffineBasis.coords_apply, AffineBasis.sum_coord_apply_eq_one] + Algebra.id.smul_eq_mul, mul_one] + rw [evalBarycentricCoords_apply_of_mem_bases ι ℝ F (g y) h] + simp_rw [AffineBasis.coords_apply, AffineBasis.sum_coord_apply_eq_one] · simp_rw [← smul_eq_mul] refine fun i hi ↦ (Continuous.const_smul ?_ _).intervalIntegrable 0 1 exact deltaMollifier_smooth.continuous diff --git a/SphereEversion/Loops/Surrounding.lean b/SphereEversion/Loops/Surrounding.lean index 9ce81ca5..24cce472 100644 --- a/SphereEversion/Loops/Surrounding.lean +++ b/SphereEversion/Loops/Surrounding.lean @@ -33,7 +33,7 @@ The key results are: -- to obtain that normed spaces are locally connected open Set Function Module Int Prod Path Filter -open scoped Topology unitInterval +open scoped Topology unitInterval ContDiff namespace IsPathConnected @@ -900,7 +900,8 @@ theorem extend_loops {U₀ U₁ K₀ K₁ : Set E} (hU₀ : IsOpen U₀) (hU₁ ?_, ?_⟩, ?_⟩ · rintro x ((hx | hx) | hx) · simp_rw [heq2 x hx, h₀.surrounds x (hVU₀ <| subset_closure hx)] - · simp_rw [γ, (hγ <| ρ x).surrounds x hx] + · simp_rw [γ] + exact (hγ <| ρ x).surrounds x hx · simp_rw [γ, h1ρ (subset_closure hx), Pi.one_apply, sfHomotopy_one, h₁.surrounds x (hVU₁ hx)] · exact Continuous.sfHomotopy ρ.continuous.fst' continuous_fst continuous_snd.fst continuous_snd.snd diff --git a/SphereEversion/Main.lean b/SphereEversion/Main.lean index b8c23b4b..24ff12f3 100644 --- a/SphereEversion/Main.lean +++ b/SphereEversion/Main.lean @@ -2,8 +2,7 @@ import SphereEversion.Global.Immersion open Metric FiniteDimensional Set ModelWithCorners -open scoped Manifold Topology -local notation "∞" => (⊤ : ℕ∞) +open scoped Manifold Topology ContDiff /-! # The sphere eversion project @@ -31,7 +30,7 @@ theorem Smale : (-- `f 1` is the antipodal map, sending `x` to `-x` and f 1 = fun x : 𝕊² ↦ -(x : ℝ³)) ∧ -- every `f t` is an immersion. - ∀ t, Immersion (𝓡 2) 𝓘(ℝ, ℝ³) (f t) ⊤ := + ∀ t, Immersion (𝓡 2) 𝓘(ℝ, ℝ³) (f t) ∞ := sphere_eversion ℝ³ end Smale @@ -49,11 +48,11 @@ section Gromov variable (n n' d : ℕ) {M : Type*} [TopologicalSpace M] [ChartedSpace (ℝ^n) M] - [SmoothManifoldWithCorners (𝓡 n) M] [T2Space M] [SigmaCompactSpace M] - {M' : Type*} [MetricSpace M'] [ChartedSpace (ℝ^n') M'] [SmoothManifoldWithCorners (𝓡 n') M'] + [IsManifold (𝓡 n) ∞ M] [T2Space M] [SigmaCompactSpace M] + {M' : Type*} [MetricSpace M'] [ChartedSpace (ℝ^n') M'] [IsManifold (𝓡 n') ∞ M'] [SigmaCompactSpace M'] {P : Type*} [TopologicalSpace P] [ChartedSpace (ℝ^d) P] - [SmoothManifoldWithCorners (𝓡 d) P] [T2Space P] [SigmaCompactSpace P] + [IsManifold (𝓡 d) ∞ P] [T2Space P] [SigmaCompactSpace P] /-- Gromov's flexibility theorem for open and ample first order partial differential relations for maps between manifolds. -/ diff --git a/SphereEversion/Notations.lean b/SphereEversion/Notations.lean index 54281641..f6e3cbda 100644 --- a/SphereEversion/Notations.lean +++ b/SphereEversion/Notations.lean @@ -1,6 +1,6 @@ import Mathlib.Analysis.Calculus.ContDiff.Basic -open scoped Topology +open scoped Topology ContDiff notation "𝒞" => ContDiff ℝ @@ -8,7 +8,7 @@ notation "hull" => convexHull ℝ notation "D" => fderiv ℝ -notation "smooth_on" => ContDiffOn ℝ (⊤ : ℕ∞) +notation "smooth_on" => ContDiffOn ℝ ∞ -- `∀ᶠ x near s, p x` means property `p` holds at every point in a neighborhood of the set `s`. notation3 (prettyPrint := false) diff --git a/SphereEversion/ToMathlib/Algebra/Periodic.lean b/SphereEversion/ToMathlib/Algebra/Periodic.lean index 2019bc70..29d65f69 100644 --- a/SphereEversion/ToMathlib/Algebra/Periodic.lean +++ b/SphereEversion/ToMathlib/Algebra/Periodic.lean @@ -1,5 +1,6 @@ import Mathlib.Analysis.Normed.Order.Lattice -import SphereEversion.ToMathlib.Topology.Separation.Basic +import Mathlib.Algebra.Periodic +import SphereEversion.ToMathlib.Topology.Separation.Hausdorff -- TODO: the file this references doesn't exist in mathlib any more; rename this one appropriately! diff --git a/SphereEversion/ToMathlib/Analysis/Calculus.lean b/SphereEversion/ToMathlib/Analysis/Calculus.lean index f988b541..3bf46e06 100644 --- a/SphereEversion/ToMathlib/Analysis/Calculus.lean +++ b/SphereEversion/ToMathlib/Analysis/Calculus.lean @@ -23,7 +23,7 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCom [NormedSpace 𝕜 E] {E₁ : Type*} [NormedAddCommGroup E₁] [NormedSpace 𝕜 E₁] {E₂ : Type*} [NormedAddCommGroup E₂] [NormedSpace 𝕜 E₂] {E' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type*} - [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : ℕ∞} + [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : WithTop ℕ∞} theorem fderiv_prod_left {x₀ : E} {y₀ : F} : fderiv 𝕜 (fun x ↦ (x, y₀)) x₀ = ContinuousLinearMap.inl 𝕜 E F := @@ -36,7 +36,7 @@ theorem fderiv_prod_right {x₀ : E} {y₀ : F} : theorem HasFDerivAt.partial_fst {φ : E → F → G} {φ' : E × F →L[𝕜] G} {e₀ : E} {f₀ : F} (h : HasFDerivAt (uncurry φ) φ' (e₀, f₀)) : HasFDerivAt (fun e ↦ φ e f₀) (φ'.comp (inl 𝕜 E F)) e₀ := by - apply h.comp e₀ <| hasFDerivAt_prod_mk_left e₀ f₀ + exact h.comp e₀ <| hasFDerivAt_prod_mk_left (𝕜 := 𝕜) e₀ f₀ theorem HasFDerivAt.partial_snd {φ : E → F → G} {φ' : E × F →L[𝕜] G} {e₀ : E} {f₀ : F} (h : HasFDerivAt (uncurry φ) φ' (e₀, f₀)) : @@ -48,10 +48,12 @@ theorem fderiv_prod_eq_add {f : E × F → G} {p : E × F} (hf : DifferentiableA fderiv 𝕜 (fun z : E × F ↦ f (z.1, p.2)) p + fderiv 𝕜 (fun z : E × F ↦ f (p.1, z.2)) p := by have H₁ : fderiv 𝕜 (fun z : E × F ↦ f (z.1, p.2)) p = (fderiv 𝕜 f p).comp (.comp (.inl 𝕜 E F) (.fst 𝕜 E F)) := - (hf.hasFDerivAt.comp _ (hasFDerivAt_fst.prod (hasFDerivAt_const _ _))).fderiv + (hf.hasFDerivAt.comp p + ((hasFDerivAt_fst (𝕜 := 𝕜) (E := E) (F := F)).prod (hasFDerivAt_const p.2 _))).fderiv have H₂ : fderiv 𝕜 (fun z : E × F ↦ f (p.1, z.2)) p = (fderiv 𝕜 f p).comp (.comp (.inr 𝕜 E F) (.snd 𝕜 E F)) := - (hf.hasFDerivAt.comp _ ((hasFDerivAt_const _ _).prod hasFDerivAt_snd)).fderiv + (hf.hasFDerivAt.comp _ ((hasFDerivAt_const p.1 _).prod + (hasFDerivAt_snd (𝕜 := 𝕜) (E := E) (F := F)))).fderiv rw [H₁, H₂, ← comp_add, comp_fst_add_comp_snd, coprod_inl_inr, ContinuousLinearMap.comp_id] variable (𝕜) @@ -81,7 +83,7 @@ theorem fderiv_partial_snd {φ : E → F → G} {φ' : E × F →L[𝕜] G} {e theorem DifferentiableAt.hasFDerivAt_partial_fst {φ : E → F → G} {e₀ : E} {f₀ : F} (h : DifferentiableAt 𝕜 (uncurry φ) (e₀, f₀)) : HasFDerivAt (fun e ↦ φ e f₀) (partialFDerivFst 𝕜 φ e₀ f₀) e₀ := by - apply (h.comp e₀ <| differentiableAt_id.prod <| differentiableAt_const f₀).hasFDerivAt + apply (h.comp e₀ <| differentiableAt_id.prod <| differentiableAt_const f₀).hasFDerivAt (𝕜 := 𝕜) theorem DifferentiableAt.hasFDerivAt_partial_snd {φ : E → F → G} {e₀ : E} {f₀ : F} (h : DifferentiableAt 𝕜 (uncurry φ) (e₀, f₀)) : diff --git a/SphereEversion/ToMathlib/Analysis/CutOff.lean b/SphereEversion/ToMathlib/Analysis/CutOff.lean index c6b1b950..c8b80bac 100644 --- a/SphereEversion/ToMathlib/Analysis/CutOff.lean +++ b/SphereEversion/ToMathlib/Analysis/CutOff.lean @@ -2,13 +2,13 @@ import Mathlib.Geometry.Manifold.PartitionOfUnity open Set Filter -open scoped Manifold Topology +open scoped Manifold Topology ContDiff -- The bundled versions of this lemma has been merged to mathlib. -- TODO: add the unbundled version, or (better) re-write sphere-eversion accordingly. theorem exists_contDiff_one_nhds_of_interior {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s t : Set E} (hs : IsClosed s) (hd : s ⊆ interior t) : - ∃ f : E → ℝ, ContDiff ℝ (⊤: ℕ∞) f ∧ (∀ᶠ x in 𝓝ˢ s, f x = 1) ∧ (∀ x ∉ t, f x = 0) ∧ + ∃ f : E → ℝ, ContDiff ℝ ∞ f ∧ (∀ᶠ x in 𝓝ˢ s, f x = 1) ∧ (∀ x ∉ t, f x = 0) ∧ ∀ x, f x ∈ Icc (0 : ℝ) 1 := let ⟨f, hfs, hft, hf01⟩ := exists_smooth_one_nhds_of_subset_interior 𝓘(ℝ, E) hs hd ⟨f, f.contMDiff.contDiff, hfs, hft, hf01⟩ diff --git a/SphereEversion/ToMathlib/ExistsOfConvex.lean b/SphereEversion/ToMathlib/ExistsOfConvex.lean index 92f17a54..18091795 100644 --- a/SphereEversion/ToMathlib/ExistsOfConvex.lean +++ b/SphereEversion/ToMathlib/ExistsOfConvex.lean @@ -2,7 +2,7 @@ import SphereEversion.ToMathlib.Partition noncomputable section -open scoped Topology Manifold +open scoped Topology Manifold ContDiff open Set Function Filter @@ -12,7 +12,7 @@ variable {ι : Type*} variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type*} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type*} [TopologicalSpace M] - [ChartedSpace H M] [SmoothManifoldWithCorners I M] [SigmaCompactSpace M] [T2Space M] + [ChartedSpace H M] [IsManifold I ∞ M] [SigmaCompactSpace M] [T2Space M] section @@ -47,7 +47,7 @@ variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] variable {G : Type*} [NormedAddCommGroup G] [NormedSpace ℝ G] {HG : Type*} [TopologicalSpace HG] (IG : ModelWithCorners ℝ G HG) {N : Type*} [TopologicalSpace N] [ChartedSpace HG N] - [SmoothManifoldWithCorners IG N] + [IsManifold IG ∞ N] @[inherit_doc] local notation "𝓒" => ContMDiff I 𝓘(ℝ, F) @@ -55,7 +55,7 @@ variable {G : Type*} [NormedAddCommGroup G] [NormedSpace ℝ G] {HG : Type*} [To variable (I) -omit [FiniteDimensional ℝ E] [SmoothManifoldWithCorners I M] [SigmaCompactSpace M] [T2Space M] in +omit [FiniteDimensional ℝ E] [IsManifold I ∞ M] [SigmaCompactSpace M] [T2Space M] in theorem reallyConvex_contMDiffAt (x : M) (n : ℕ∞) : ReallyConvex (smoothGerm I x) {φ : Germ (𝓝 x) F | φ.ContMDiffAt I n} := by classical @@ -112,16 +112,16 @@ variable {E₁ E₂ F : Type*} variable {H₁ M₁ H₂ M₂ : Type*} [TopologicalSpace H₁] (I₁ : ModelWithCorners ℝ E₁ H₁) - [TopologicalSpace M₁] [ChartedSpace H₁ M₁] [SmoothManifoldWithCorners I₁ M₁] + [TopologicalSpace M₁] [ChartedSpace H₁ M₁] [IsManifold I₁ ∞ M₁] [TopologicalSpace H₂] (I₂ : ModelWithCorners ℝ E₂ H₂) - [TopologicalSpace M₂] [ChartedSpace H₂ M₂] [SmoothManifoldWithCorners I₂ M₂] + [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₂] - [SmoothManifoldWithCorners I₁ M₁] [SmoothManifoldWithCorners I₂ M₂] in + [IsManifold I₁ ∞ M₁] [IsManifold I₂ ∞ M₂] in theorem reallyConvex_contMDiffAtProd {x : M₁} (n : ℕ∞) : ReallyConvex (smoothGerm I₁ x) {φ : Germ (𝓝 x) (M₂ → F) | φ.ContMDiffAtProd I₁ I₂ n} := by classical @@ -139,7 +139,7 @@ theorem reallyConvex_contMDiffAtProd {x : M₁} (n : ℕ∞) : refine (smoothGerm.contMDiffAt _).smul_prod (w_supp ?_) simpa [H] using hφ -omit [FiniteDimensional ℝ E₂] [SmoothManifoldWithCorners I₂ M₂] in +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, @@ -184,12 +184,12 @@ variable {ι : Type*} variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type*} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type*} [TopologicalSpace M] - [ChartedSpace H M] [SmoothManifoldWithCorners I M] [SigmaCompactSpace M] [T2Space M] + [ChartedSpace H M] [IsManifold I ∞ M] [SigmaCompactSpace M] [T2Space M] open TopologicalSpace example {f : E → ℝ} (h : ∀ x : E, ∃ U ∈ 𝓝 x, ∃ ε : ℝ, ∀ x' ∈ U, 0 < ε ∧ ε ≤ f x') : - ∃ f' : E → ℝ, ContDiff ℝ (⊤: ℕ∞) f' ∧ ∀ x, 0 < f' x ∧ f' x ≤ f x := by + ∃ f' : E → ℝ, ContDiff ℝ ∞ f' ∧ ∀ x, 0 < f' x ∧ f' x ≤ f x := by let P : E → ℝ → Prop := fun x t ↦ 0 < t ∧ t ≤ f x have hP : ∀ x, Convex ℝ {y | P x y} := fun x ↦ convex_Ioc _ _ apply exists_contDiff_of_convex hP diff --git a/SphereEversion/ToMathlib/Geometry/Manifold/Algebra/SmoothGerm.lean b/SphereEversion/ToMathlib/Geometry/Manifold/Algebra/SmoothGerm.lean index 1f3d9213..1a0d5f23 100644 --- a/SphereEversion/ToMathlib/Geometry/Manifold/Algebra/SmoothGerm.lean +++ b/SphereEversion/ToMathlib/Geometry/Manifold/Algebra/SmoothGerm.lean @@ -21,7 +21,7 @@ noncomputable section open Filter Set -open scoped Manifold Topology +open scoped Manifold Topology ContDiff -- FIXME: move to `Manifold/Algebra/SmoothFunctions`, around line 46 section @@ -34,12 +34,12 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {N : Type*} [TopologicalSpace N] [ChartedSpace H N] {E'' : Type*} [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H'' : Type*} [TopologicalSpace H''] {I'' : ModelWithCorners 𝕜 E'' H''} {N' : Type*} [TopologicalSpace N'] [ChartedSpace H'' N'] - {G : Type*} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H' G] [SmoothMul I' G] + {G : Type*} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H' G] [ContMDiffMul I' ∞ G] @[to_additive] -theorem SmoothMap.coe_prod {ι : Type*} (f : ι → C^⊤⟮I, N; I', G⟯) (s : Finset ι) : +theorem SmoothMap.coe_prod {ι : Type*} (f : ι → C^∞⟮I, N; I', G⟯) (s : Finset ι) : ⇑(∏ i in s, f i) = ∏ i in s, ⇑(f i) := - map_prod (SmoothMap.coeFnMonoidHom : C^⊤⟮I, N; I', G⟯ →* N → G) f s + map_prod (ContMDiffMap.coeFnMonoidHom : C^∞⟮I, N; I', G⟯ →* N → G) f s end @@ -56,28 +56,28 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] (F : Type*) [NormedAddCommGroup F] [NormedSpace ℝ F] (G : Type*) [AddCommGroup G] [Module ℝ G] /-- The map `C^∞(N, ℝ) → Germ (𝓝 x) ℝ` as a ring homomorphism. -/ -def RingHom.germOfContMDiffMap (x : N) : C^⊤⟮I, N; 𝓘(ℝ), ℝ⟯ →+* Germ (𝓝 x) ℝ := - RingHom.comp (Germ.coeRingHom _) SmoothMap.coeFnRingHom +def RingHom.germOfContMDiffMap (x : N) : C^∞⟮I, N; 𝓘(ℝ), ℝ⟯ →+* Germ (𝓝 x) ℝ := + RingHom.comp (Germ.coeRingHom _) ContMDiffMap.coeFnRingHom /-- All germs of smooth functions `N → ℝ` at `x : N`, as a subring of `Germ (𝓝 x) ℝ`. -/ def smoothGerm (x : N) : Subring (Germ (𝓝 x) ℝ) := (RingHom.germOfContMDiffMap I x).range -instance (x : N) : Coe C^⊤⟮I, N; 𝓘(ℝ), ℝ⟯ (smoothGerm I x) := +instance (x : N) : Coe C^∞⟮I, N; 𝓘(ℝ), ℝ⟯ (smoothGerm I x) := ⟨fun f ↦ ⟨(f : N → ℝ), ⟨f, rfl⟩⟩⟩ @[simp] -theorem smoothGerm.coe_coe (f : C^⊤⟮I, N; 𝓘(ℝ), ℝ⟯) (x : N) : +theorem smoothGerm.coe_coe (f : C^∞⟮I, N; 𝓘(ℝ), ℝ⟯) (x : N) : ((f : smoothGerm I x) : (𝓝 x).Germ ℝ) = (f : (𝓝 x).Germ ℝ) := rfl @[simp] -theorem smoothGerm.coe_sum {ι} (f : ι → C^⊤⟮I, N; 𝓘(ℝ), ℝ⟯) (s : Finset ι) (x : N) : - ((∑ i in s, f i : C^⊤⟮I, N; 𝓘(ℝ), ℝ⟯) : smoothGerm I x) = ∑ i in s, (f i : smoothGerm I x) := +theorem smoothGerm.coe_sum {ι} (f : ι → C^∞⟮I, N; 𝓘(ℝ), ℝ⟯) (s : Finset ι) (x : N) : + ((∑ i in s, f i : C^∞⟮I, N; 𝓘(ℝ), ℝ⟯) : smoothGerm I x) = ∑ i in s, (f i : smoothGerm I x) := map_sum (RingHom.rangeRestrict (RingHom.germOfContMDiffMap I x)) f s @[simp] -theorem smoothGerm.coe_eq_coe (f g : C^⊤⟮I, N; 𝓘(ℝ), ℝ⟯) {x : N} (h : ∀ᶠ y in 𝓝 x, f y = g y) : +theorem smoothGerm.coe_eq_coe (f g : C^∞⟮I, N; 𝓘(ℝ), ℝ⟯) {x : N} (h : ∀ᶠ y in 𝓝 x, f y = g y) : (f : smoothGerm I x) = (g : smoothGerm I x) := by ext apply Quotient.sound @@ -142,13 +142,13 @@ variable {ι : Type*} variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type*} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type*} [TopologicalSpace M] - [ChartedSpace H M] [SmoothManifoldWithCorners I M] [SigmaCompactSpace M] [T2Space M] + [ChartedSpace H M] [IsManifold I ∞ M] [SigmaCompactSpace M] [T2Space M] variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] variable {G : Type*} [NormedAddCommGroup G] [NormedSpace ℝ G] {HG : Type*} [TopologicalSpace HG] (IG : ModelWithCorners ℝ G HG) {N : Type*} [TopologicalSpace N] [ChartedSpace HG N] - [SmoothManifoldWithCorners IG N] + [IsManifold IG ∞ N] def smoothGerm.valueOrderRingHom (x : N) : smoothGerm IG x →+*o ℝ := Filter.Germ.valueOrderRingHom.comp <| Subring.orderedSubtype _ @@ -156,7 +156,7 @@ def smoothGerm.valueOrderRingHom (x : N) : smoothGerm IG x →+*o ℝ := def smoothGerm.valueRingHom (x : N) : smoothGerm IG x →+* ℝ := Filter.Germ.valueRingHom.comp <| Subring.subtype _ -omit [SmoothManifoldWithCorners IG N] in +omit [IsManifold IG ∞ N] in theorem smoothGerm.valueOrderRingHom_toRingHom (x : N) : (smoothGerm.valueOrderRingHom IG x).toRingHom = smoothGerm.valueRingHom IG x := rfl @@ -171,7 +171,7 @@ def valueₛₗ {F} [AddCommMonoid F] [Module ℝ F] (x : N) : variable (I) -protected def ContMDiffAt' {x : M} (φ : Germ (𝓝 x) N) (n : ℕ∞) : Prop := +protected def ContMDiffAt' {x : M} (φ : Germ (𝓝 x) N) (n : WithTop ℕ∞) : Prop := Quotient.liftOn' φ (fun f ↦ ContMDiffAt I IG n f x) fun f g h ↦ propext <| by constructor @@ -180,7 +180,7 @@ protected def ContMDiffAt' {x : M} (φ : Germ (𝓝 x) N) (n : ℕ∞) : Prop := /-- The predicate selecting germs of `ContMDiffAt` functions. TODO: merge with the next def that generalizes target space -/ -protected nonrec def ContMDiffAt {x : M} (φ : Germ (𝓝 x) F) (n : ℕ∞) : Prop := +protected nonrec def ContMDiffAt {x : M} (φ : Germ (𝓝 x) F) (n : WithTop ℕ∞) : Prop := φ.ContMDiffAt' I 𝓘(ℝ, F) n -- currently unused @@ -192,10 +192,12 @@ nonrec def mfderiv {x : M} (φ : Germ (𝓝 x) N) : variable {I} -omit [FiniteDimensional ℝ E] [SmoothManifoldWithCorners I M] [SigmaCompactSpace M] [T2Space M] +omit [FiniteDimensional ℝ E] [IsManifold I ∞ M] [SigmaCompactSpace M] [T2Space M] theorem _root_.smoothGerm.contMDiffAt {x : M} (φ : smoothGerm I x) {n : ℕ∞} : - (φ : Germ (𝓝 x) ℝ).ContMDiffAt I n := by rcases φ with ⟨_, g, rfl⟩; apply g.contMDiff.of_le le_top + (φ : Germ (𝓝 x) ℝ).ContMDiffAt I n := by + rcases φ with ⟨_, g, rfl⟩ + apply g.contMDiff.of_le (mod_cast le_top) protected nonrec theorem ContMDiffAt.add {x : M} {φ ψ : Germ (𝓝 x) F} {n : ℕ∞} : φ.ContMDiffAt I n → ψ.ContMDiffAt I n → (φ + ψ).ContMDiffAt I n := @@ -225,10 +227,10 @@ variable {E₁ E₂ F H₁ M₁ H₂ M₂ : Type*} [NormedAddCommGroup E₂] [NormedSpace ℝ E₂] [FiniteDimensional ℝ E₂] [NormedAddCommGroup F] [NormedSpace ℝ F] [TopologicalSpace H₁] (I₁ : ModelWithCorners ℝ E₁ H₁) - [TopologicalSpace M₁] [ChartedSpace H₁ M₁] [SmoothManifoldWithCorners I₁ M₁] + [TopologicalSpace M₁] [ChartedSpace H₁ M₁] [IsManifold I₁ ∞ M₁] [SigmaCompactSpace M₁] [T2Space M₁] [TopologicalSpace H₂] (I₂ : ModelWithCorners ℝ E₂ H₂) - [TopologicalSpace M₂] [ChartedSpace H₂ M₂] [SmoothManifoldWithCorners I₂ M₂] + [TopologicalSpace M₂] [ChartedSpace H₂ M₂] [IsManifold I₂ ∞ M₂] open scoped Filter @@ -274,8 +276,8 @@ end) -/ variable {I₁ I₂} -omit [FiniteDimensional ℝ E₁] [FiniteDimensional ℝ E₂] [SmoothManifoldWithCorners I₁ M₁] - [SigmaCompactSpace M₁] [T2Space M₁] [SmoothManifoldWithCorners I₂ M₂] +omit [FiniteDimensional ℝ E₁] [FiniteDimensional ℝ E₂] [IsManifold I₁ ∞ M₁] + [SigmaCompactSpace M₁] [T2Space M₁] [IsManifold I₂ ∞ M₂] theorem ContMDiffAtProd.add {x : M₁} {φ ψ : Germ (𝓝 x) <| M₂ → F} {n : ℕ∞} : φ.ContMDiffAtProd I₁ I₂ n → ψ.ContMDiffAtProd I₁ I₂ n → (φ + ψ).ContMDiffAtProd I₁ I₂ n := diff --git a/SphereEversion/ToMathlib/Geometry/Manifold/Immersion.lean b/SphereEversion/ToMathlib/Geometry/Manifold/Immersion.lean index 5012c840..8e2783fa 100644 --- a/SphereEversion/ToMathlib/Geometry/Manifold/Immersion.lean +++ b/SphereEversion/ToMathlib/Geometry/Manifold/Immersion.lean @@ -36,7 +36,7 @@ noncomputable section open Set Function -open scoped Manifold +open scoped Manifold ContDiff -- Let `M` be a manifold with corners over the pair `(E, H)`. -- Let `M'` be a manifold with corners over the pair `(E', H')`. @@ -44,21 +44,19 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [instE: NormedAddCommGroup E] [instE': NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type*} [TopologicalSpace M] [ChartedSpace H M] - [SmoothManifoldWithCorners I M] {E' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type*} [TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H') {M' : Type*} [TopologicalSpace M'] [ChartedSpace H' M'] - [SmoothManifoldWithCorners I' M'] section Definition /-- A `C^n` immersion `f : M → M` is a `C^n` map whose differential is injective at every point. -/ -structure Immersion (f : M → M') (n : ℕ∞) : Prop where +structure Immersion (f : M → M') (n : WithTop ℕ∞) : Prop where contMDiff : ContMDiff I I' n f diff_injective : ∀ p, Injective (mfderiv I I' f p) /-- An injective `C^n` immersion -/ -structure InjImmersion (f : M → M') (n : ℕ∞) extends Immersion I I' f n : Prop where +structure InjImmersion (f : M → M') (n : WithTop ℕ∞) extends Immersion I I' f n : Prop where injective : Injective f end Definition diff --git a/SphereEversion/ToMathlib/Geometry/Manifold/MiscManifold.lean b/SphereEversion/ToMathlib/Geometry/Manifold/MiscManifold.lean index 5a2d526a..ba23df6e 100644 --- a/SphereEversion/ToMathlib/Geometry/Manifold/MiscManifold.lean +++ b/SphereEversion/ToMathlib/Geometry/Manifold/MiscManifold.lean @@ -2,13 +2,13 @@ import Mathlib.Geometry.Manifold.ContMDiff.Product open Set Function Filter -open scoped Manifold Topology +open scoped Manifold Topology ContDiff noncomputable section -section SmoothManifoldWithCorners +section IsManifold -open SmoothManifoldWithCorners +open IsManifold variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] @@ -27,7 +27,7 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E'' : Type*} [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] {H'' : Type*} [TopologicalSpace H''] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type*} [TopologicalSpace M''] [ChartedSpace H'' M''] - {e : PartialHomeomorph M H} {f : M → M'} {m n : ℕ∞} {s : Set M} {x x' : M} + {e : PartialHomeomorph M H} {f : M → M'} {m n : WithTop ℕ∞} {s : Set M} {x x' : M} theorem contMDiff_prod {f : M → M' × N'} : ContMDiff I (I'.prod J') n f ↔ @@ -40,13 +40,13 @@ theorem contMDiffAt_prod {f : M → M' × N'} {x : M} : ⟨fun h ↦ ⟨h.fst, h.snd⟩, fun h ↦ h.1.prod_mk h.2⟩ theorem smooth_prod {f : M → M' × N'} : - ContMDiff I (I'.prod J') (⊤: ℕ∞) f ↔ - (ContMDiff I I' ⊤ fun x ↦ (f x).1) ∧ ContMDiff I J' ⊤ fun x ↦ (f x).2 := + ContMDiff I (I'.prod J') ∞ f ↔ + (ContMDiff I I' ∞ fun x ↦ (f x).1) ∧ ContMDiff I J' ∞ fun x ↦ (f x).2 := contMDiff_prod theorem smoothAt_prod {f : M → M' × N'} {x : M} : - ContMDiffAt I (I'.prod J') (⊤: ℕ∞) f x ↔ - ContMDiffAt I I' ⊤ (fun x ↦ (f x).1) x ∧ ContMDiffAt I J' ⊤ (fun x ↦ (f x).2) x := + ContMDiffAt I (I'.prod J') ∞ f x ↔ + ContMDiffAt I I' ∞ (fun x ↦ (f x).1) x ∧ ContMDiffAt I J' ∞ (fun x ↦ (f x).2) x := contMDiffAt_prod -end SmoothManifoldWithCorners +end IsManifold diff --git a/SphereEversion/ToMathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean b/SphereEversion/ToMathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean index fc1b70a7..e836fa46 100644 --- a/SphereEversion/ToMathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean +++ b/SphereEversion/ToMathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean @@ -1,4 +1,4 @@ -import Mathlib.Geometry.Manifold.SmoothManifoldWithCorners +import Mathlib.Geometry.Manifold.IsManifold open scoped Topology diff --git a/SphereEversion/ToMathlib/Topology/Algebra/Module.lean b/SphereEversion/ToMathlib/Topology/Algebra/Module.lean index dfcb90e9..515a18a1 100644 --- a/SphereEversion/ToMathlib/Topology/Algebra/Module.lean +++ b/SphereEversion/ToMathlib/Topology/Algebra/Module.lean @@ -1,4 +1,4 @@ -import Mathlib.Topology.Algebra.Module.Basic +import Mathlib.Topology.Algebra.Module.Equiv namespace ContinuousLinearMap diff --git a/SphereEversion/ToMathlib/Topology/HausdorffDistance.lean b/SphereEversion/ToMathlib/Topology/HausdorffDistance.lean deleted file mode 100644 index 6b2812f3..00000000 --- a/SphereEversion/ToMathlib/Topology/HausdorffDistance.lean +++ /dev/null @@ -1,36 +0,0 @@ -import Mathlib.Topology.MetricSpace.Thickening - -open Set Metric - -open scoped Topology - -variable {α β : Type*} [PseudoMetricSpace α] [PseudoMetricSpace β] - --- this whole file is being PRed in #10303 -namespace Metric - -theorem thickening_ball (x : α) (ε δ : ℝ) : thickening ε (ball x δ) ⊆ ball x (ε + δ) := by - rw [← thickening_singleton, ← thickening_singleton] - apply thickening_thickening_subset - -theorem infDist_pos_iff_not_mem_closure {x : α} {s : Set α} (hs : s.Nonempty) : - 0 < infDist x s ↔ x ∉ closure s := by - rw [isClosed_closure.not_mem_iff_infDist_pos hs.closure, infDist_closure] - -end Metric - -open Metric - -theorem IsCompact.exists_thickening_image {f : α → β} {K : Set α} {U : Set β} (hK : IsCompact K) - (ho : IsOpen U) (hf : Continuous f) (hKU : MapsTo f K U) : - ∃ ε > 0, ∃ V ∈ 𝓝ˢ K, thickening ε (f '' V) ⊆ U := by - rcases (hK.image hf).exists_thickening_subset_open ho hKU.image_subset with ⟨r, hr₀, hr⟩ - refine ⟨r / 2, half_pos hr₀, f ⁻¹' thickening (r / 2) (f '' K), - hf.tendsto_nhdsSet (mapsTo_image _ _) (thickening_mem_nhdsSet _ (half_pos hr₀)), ?_⟩ - calc - thickening (r / 2) (f '' (f ⁻¹' thickening (r / 2) (f '' K))) ⊆ - thickening (r / 2) (thickening (r / 2) (f '' K)) := - thickening_subset_of_subset _ (image_preimage_subset _ _) - _ ⊆ thickening (r / 2 + r / 2) (f '' K) := (thickening_thickening_subset _ _ _) - _ = thickening r (f '' K) := by rw [add_halves] - _ ⊆ U := hr diff --git a/SphereEversion/ToMathlib/Topology/Misc.lean b/SphereEversion/ToMathlib/Topology/Misc.lean index d81984d2..2d5cddc6 100644 --- a/SphereEversion/ToMathlib/Topology/Misc.lean +++ b/SphereEversion/ToMathlib/Topology/Misc.lean @@ -2,6 +2,7 @@ import Mathlib.Topology.ShrinkingLemma import Mathlib.Analysis.Convex.Normed import Mathlib.Topology.EMetricSpace.Paracompact import Mathlib.Topology.Algebra.Order.Floor +import Mathlib.Algebra.Periodic noncomputable section diff --git a/SphereEversion/ToMathlib/Topology/Paracompact.lean b/SphereEversion/ToMathlib/Topology/Paracompact.lean index 57a07ef7..0c8412ea 100644 --- a/SphereEversion/ToMathlib/Topology/Paracompact.lean +++ b/SphereEversion/ToMathlib/Topology/Paracompact.lean @@ -1,4 +1,4 @@ -import Mathlib.Topology.Separation.Basic +import Mathlib.Topology.Separation.Hausdorff import Mathlib.Data.Real.Basic import Mathlib.Order.Interval.Finset.Nat diff --git a/SphereEversion/ToMathlib/Topology/Path.lean b/SphereEversion/ToMathlib/Topology/Path.lean index 5e3d67fa..373bbc80 100644 --- a/SphereEversion/ToMathlib/Topology/Path.lean +++ b/SphereEversion/ToMathlib/Topology/Path.lean @@ -95,7 +95,7 @@ theorem subset_range_strans_right {x : X} {γ γ' : Path x x} {t₀ : I} (h : t have h2 : t₀ ≤ t' := le_add_of_nonneg_right this have h3 := sub_ne_zero.mpr (unitInterval.coe_ne_one.mpr h).symm use t' - simp [h2, unitInterval.coe_ne_one.mpr h, h3] + simp [h2, unitInterval.coe_ne_one.mpr h, h3, t'] theorem range_strans_subset {x : X} {γ γ' : Path x x} {t₀ : I} : range (γ.strans γ' t₀) ⊆ range γ ∪ range γ' := by diff --git a/SphereEversion/ToMathlib/Topology/Separation/Basic.lean b/SphereEversion/ToMathlib/Topology/Separation/Hausdorff.lean similarity index 94% rename from SphereEversion/ToMathlib/Topology/Separation/Basic.lean rename to SphereEversion/ToMathlib/Topology/Separation/Hausdorff.lean index 454cdefd..9d6f9d76 100644 --- a/SphereEversion/ToMathlib/Topology/Separation/Basic.lean +++ b/SphereEversion/ToMathlib/Topology/Separation/Hausdorff.lean @@ -1,5 +1,4 @@ -import Mathlib.Topology.Separation.Basic - +import Mathlib.Topology.Separation.Hausdorff open Set Function variable {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] diff --git a/SphereEversion/ToMathlib/Unused/GeometryManifoldMisc.lean b/SphereEversion/ToMathlib/Unused/GeometryManifoldMisc.lean index c4e592e8..fc32c253 100644 --- a/SphereEversion/ToMathlib/Unused/GeometryManifoldMisc.lean +++ b/SphereEversion/ToMathlib/Unused/GeometryManifoldMisc.lean @@ -61,7 +61,7 @@ variable {𝕜 B F M : Type*} {E : B → Type*} [NontriviallyNormedField 𝕜] [ theorem VectorBundleCore.smoothAt_coordChange {ι} (Z : VectorBundleCore 𝕜 B F ι) [Z.IsSmooth IB] (i j : ι) {x₀ : B} (hx₀ : x₀ ∈ Z.baseSet i ∩ Z.baseSet j) : - ContMDiffAt IB 𝓘(𝕜, F →L[𝕜] F) ⊤ (Z.coordChange i j) x₀ := + ContMDiffAt IB 𝓘(𝕜, F →L[𝕜] F) ∞ (Z.coordChange i j) x₀ := (Z.contMDiffOn_coordChange IB i j).contMDiffAt <| ((Z.isOpen_baseSet i).inter (Z.isOpen_baseSet j)).mem_nhds hx₀ @@ -70,7 +70,7 @@ variable [SmoothVectorBundle F E IB] theorem smoothAt_coord_change (e e' : Trivialization F (π F E)) {x₀ : B} (hx₀ : x₀ ∈ e.baseSet ∩ e'.baseSet) [MemTrivializationAtlas e] [MemTrivializationAtlas e'] : - ContMDiffAt IB 𝓘(𝕜, F →L[𝕜] F) ⊤ (fun b : B ↦ (e.coordChangeL 𝕜 e' b : F →L[𝕜] F)) x₀ := + ContMDiffAt IB 𝓘(𝕜, F →L[𝕜] F) ∞ (fun b : B ↦ (e.coordChangeL 𝕜 e' b : F →L[𝕜] F)) x₀ := (contMDiffOn_coordChangeL e e').contMDiffAt <| (e.open_baseSet.inter e'.open_baseSet).mem_nhds hx₀ variable {IB} @@ -98,11 +98,11 @@ variable {𝕜 B F M : Type*} {E : B → Type*} [NontriviallyNormedField 𝕜] [ {n : ℕ∞} [FiberBundle F E] [VectorBundle 𝕜 F E] {e e' : Trivialization F (π F E)} variable (IB) -variable [SmoothManifoldWithCorners IB B] [SmoothVectorBundle F E IB] +variable [IsManifold IB ∞B] [SmoothVectorBundle F E IB] theorem Trivialization.smoothAt (e : Trivialization F (π F E)) [MemTrivializationAtlas e] {x₀ : TotalSpace F E} (hx₀ : x₀.proj ∈ e.baseSet) : - ContMDiffAt (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) ⊤ e x₀ := by + ContMDiffAt (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) ∞ e x₀ := by rw [smoothAt_prod] refine ⟨(contMDiffAt_proj E).congr_of_eventuallyEq ?_, ?_⟩ · exact eventually_of_mem (e.open_source.mem_nhds <| e.mem_source.mpr hx₀) fun x hx ↦ e.coe_fst hx @@ -111,7 +111,7 @@ theorem Trivialization.smoothAt (e : Trivialization F (π F E)) [MemTrivializati let e' := trivializationAt F E x₀.proj let c := (extChartAt IB x₀.proj).symm have h0 := (extChartAt IB x₀.proj).left_inv (mem_extChartAt_source x₀.proj) - have : ContMDiffWithinAt 𝓘(𝕜, EB × F) 𝓘(𝕜, F) ⊤ + have : ContMDiffWithinAt 𝓘(𝕜, EB × F) 𝓘(𝕜, F) ∞ (fun x : EB × F ↦ e'.coordChangeL 𝕜 e (c x.1) x.2) (Prod.fst ⁻¹' range IB) (extChartAt IB x₀.proj x₀.proj, (e' x₀).2) := by sorry /-refine ContMDiffWithinAt.clm_apply (𝕜 := 𝕜) ?_ contDiffWithinAt_snd.contMDiffWithinAt @@ -146,12 +146,12 @@ theorem Trivialization.smoothOn (e : Trivialization F (π F E)) [MemTrivializati theorem smoothAt_trivializationAt {x₀ : B} {x : TotalSpace F E} (hx : x.proj ∈ (trivializationAt F E x₀).baseSet) : - ContMDiffAt (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) ⊤ (trivializationAt F E x₀) x := + ContMDiffAt (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) ∞ (trivializationAt F E x₀) x := (trivializationAt F E x₀).smoothAt IB hx -omit [SmoothManifoldWithCorners IB B] in +omit [IsManifold IB ∞B] in theorem smoothOn_trivializationAt (x₀ : B) : - ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) ⊤ (trivializationAt F E x₀) + ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) ∞ (trivializationAt F E x₀) (trivializationAt F E x₀).source := (trivializationAt F E x₀).contMDiffOn @@ -177,8 +177,8 @@ variable {f : M → M'} {m n : ℕ∞} {s : Set M} {x x' : M} [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] {F₂ : Type*} [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] -variable [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] - [SmoothManifoldWithCorners J N] +variable [IsManifold I ∞ M] [IsManifold I' ∞ M'] + [IsManifold J ∞ N] -- lemma cont_mdiff_within_at_insert : -- cont_mdiff_within_at I I' n f (insert x' s) x ↔ cont_mdiff_within_at I I' n f s x := diff --git a/lake-manifest.json b/lake-manifest.json index d8d10128..873bd288 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "7edf946a4217aa3aa911290811204096e8464ada", + "rev": "75d7aea6c81efeb68701164edaaa9116f06b91ba", "name": "checkdecls", "manifestFile": "lake-manifest.json", "inputRev": null, @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "808600f8f099dc32f03fd226140ffcbddbddf71b", + "rev": "ed1d44ffe1d3eb1ca29f5284fe9de5cae7de9099", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -25,17 +25,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "8e5cb8d424df462f84997dd68af6f40e347c3e35", + "rev": "1622a8693b31523c8f82db48e01b14c74bc1f155", "name": "plausible", "manifestFile": "lake-manifest.json", - "inputRev": "v4.15.0-rc1", + "inputRev": "v4.16.0-rc1", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/LeanSearchClient", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d7caecce0d0f003fd5e9cce9a61f1dd6ba83142b", + "rev": "003ff459cdd85de551f4dcf95cdfeefe10f20531", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,47 +45,47 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ed3b856bd8893ade75cafe13e8544d4c2660f377", + "rev": "f72319c9686788305a8ab059f3c4d8c724785c83", "name": "importGraph", "manifestFile": "lake-manifest.json", - "inputRev": "v4.15.0-rc1", + "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2b000e02d50394af68cfb4770a291113d94801b5", + "rev": "07f60e90998dfd6592688a14cd67bd4e384b77b2", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.48", + "inputRev": "v0.0.50", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "43bcb1964528411e47bfa4edd0c87d1face1fce4", + "rev": "79402ad9ab4be9a2286701a9880697e2351e4955", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "v4.16.0-rc1", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ad942fdf0b15c38bface6acbb01d63855a2519ac", + "rev": "f0c584bcb14c5adfb53079781eeea75b26ebbd32", "name": "Qq", "manifestFile": "lake-manifest.json", - "inputRev": "v4.14.0", + "inputRev": "v4.15.0", "inherited": true, - "configFile": "lakefile.lean"}, + "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "9e583efcea920afa13ee2a53069821a2297a94c0", + "rev": "c104265c34eb8181af14e8dbc14c2f034292cb02", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lean-toolchain b/lean-toolchain index cf25a981..2ffc30ce 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.15.0-rc1 +leanprover/lean4:v4.16.0-rc2 \ No newline at end of file