From 360996ffa7b8ac5e9515cce99303c9a8ed930420 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Wed, 4 Sep 2024 16:57:05 +0200 Subject: [PATCH 1/6] WIP: upgrade mathlib to Lean 4.12. Notable changes include - updates for renamed lemmas, including some with a 0 suffix - changes for the new variable command: this detects unused variables, which led to some restructuring of assumptions. Sometimes, the variables can just be removed; in other cases, they are omit'ed --- which may not be optimal. This can be improved later! - automatically generated ext_iff lemmas, with sometimes fewer explicit variables (a good change!) --- SphereEversion/Global/Immersion.lean | 16 ++++----- SphereEversion/Global/Localisation.lean | 6 ++-- SphereEversion/Global/LocalisationData.lean | 14 ++++++-- SphereEversion/Global/OneJetSec.lean | 2 +- .../Global/ParametricityForFree.lean | 2 +- SphereEversion/Global/Relation.lean | 4 +-- SphereEversion/Global/SmoothEmbedding.lean | 26 +++++++++----- SphereEversion/Global/TwistOneJetSec.lean | 4 +-- SphereEversion/InductiveConstructions.lean | 2 +- SphereEversion/Local/Corrugation.lean | 2 +- SphereEversion/Local/HPrinciple.lean | 36 ++++++++++--------- .../Local/ParametricHPrinciple.lean | 4 ++- SphereEversion/Local/Relation.lean | 2 +- SphereEversion/Loops/Basic.lean | 23 +++++------- SphereEversion/Loops/Surrounding.lean | 31 ++++++++++------ .../ToMathlib/Analysis/Calculus.lean | 4 +++ .../Calculus/AddTorsor/AffineMap.lean | 6 ++-- .../InnerProductSpace/Projection.lean | 6 ++-- SphereEversion/ToMathlib/ExistsOfConvex.lean | 5 +++ .../Geometry/Manifold/Algebra/SmoothGerm.lean | 6 ++++ .../ParametricIntervalIntegral.lean | 3 +- SphereEversion/ToMathlib/Partition.lean | 6 ++-- .../ToMathlib/SmoothBarycentric.lean | 1 - SphereEversion/ToMathlib/Topology/Misc.lean | 4 ++- lake-manifest.json | 22 ++++++------ lean-toolchain | 2 +- 26 files changed, 144 insertions(+), 95 deletions(-) diff --git a/SphereEversion/Global/Immersion.lean b/SphereEversion/Global/Immersion.lean index 54b7c065..8e496f5f 100644 --- a/SphereEversion/Global/Immersion.lean +++ b/SphereEversion/Global/Immersion.lean @@ -53,9 +53,7 @@ theorem chartAt_image_immersionRel_eq {σ : OneJetBundle I M I' M'} : ψJ σ '' ((ψJ σ).source ∩ immersionRel I M I' M') = (ψJ σ).target ∩ {q : HJ | Injective q.2} := PartialEquiv.IsImage.image_eq fun _σ' hσ' ↦ (mem_immersionRel_iff' I I' hσ').symm -variable [FiniteDimensional ℝ E] [FiniteDimensional ℝ E'] - -theorem immersionRel_open : IsOpen (immersionRel I M I' M') := by +theorem immersionRel_open [FiniteDimensional ℝ E] : IsOpen (immersionRel I M I' M') := by simp_rw [ChartedSpace.isOpen_iff HJ (immersionRel I M I' M'), chartAt_image_immersionRel_eq] refine fun σ ↦ (ψJ σ).open_target.inter ?_ convert isOpen_univ.prod ContinuousLinearMap.isOpen_injective @@ -72,6 +70,8 @@ theorem immersionRel_slice_eq {m : M} {m' : M'} {p : DualPair <| TangentSpace I (immersionRel I M I' M').slice ⟨(m, m'), φ⟩ p = ((ker p.π).map φ : Set <| TM' m')ᶜ := Set.ext_iff.mpr fun _ ↦ p.injective_update_iff hφ +variable [FiniteDimensional ℝ E] [FiniteDimensional ℝ E'] + 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)) @@ -93,10 +93,10 @@ 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] - {E' : Type*} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] + {E' : Type*} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type*} [TopologicalSpace H'] (I' : ModelWithCorners ℝ E' H') [I'.Boundaryless] {M' : Type*} [MetricSpace M'] [ChartedSpace H' M'] [SmoothManifoldWithCorners I' M'] - [FiniteDimensional ℝ E] [FiniteDimensional ℝ E'] + /- [FiniteDimensional ℝ E] -/ [FiniteDimensional ℝ E'] {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] @@ -274,13 +274,13 @@ theorem ContDiff.uncurry_left {f : E → F → G} (n : ℕ∞) (hf : 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] --[SmoothManifoldWithCorners I M] {E' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type*} [TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H') - {M' : Type*} [MetricSpace M'] [ChartedSpace H' M'] [SmoothManifoldWithCorners I' M'] + {M' : Type*} [MetricSpace M'] [ChartedSpace H' M'] --[SmoothManifoldWithCorners 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] + {P : Type*} [TopologicalSpace P] [ChartedSpace HP P] --[SmoothManifoldWithCorners IP P] -- move to Mathlib.Geometry.Manifold.ContMDiff.Product lemma Smooth.inr (x : M) : diff --git a/SphereEversion/Global/Localisation.lean b/SphereEversion/Global/Localisation.lean index 2d3668c4..44ea2b9d 100644 --- a/SphereEversion/Global/Localisation.lean +++ b/SphereEversion/Global/Localisation.lean @@ -178,14 +178,14 @@ theorem FormalSol.transfer_unloc_localize (F : FormalSol R) (hF : range (F.bs open scoped Classical -variable [T2Space M] - lemma ChartPair.mkHtpy_aux {F : FormalSol R} {𝓕 : (R.localize p.φ p.ψ).relLoc.HtpyFormalSol} (h : p.compat' F 𝓕) (t x) (hx : x ∉ p.K₁) : F (p.φ x) = OneJetBundle.embedding p.φ p.ψ (RelLoc.HtpyFormalSol.unloc p 𝓕 t x) := by rw [← F.transfer_unloc_localize p h.1, RelLoc.HtpyFormalSol.unloc_congr_const p (h.hFF x hx t)] rfl +variable [T2Space M] + def ChartPair.mkHtpy (F : FormalSol R) (𝓕 : (R.localize p.φ p.ψ).relLoc.HtpyFormalSol) : HtpyFormalSol R := if h : p.compat' F 𝓕 then @@ -261,7 +261,7 @@ theorem ChartPair.mkHtpy_isHolonomicAt_iff {F : FormalSol R} rw [p.φ.updateFormalSol_bs p.ψ p.hK₁] simp only [Function.comp_apply, OpenSmoothEmbedding.update_apply_embedding, mem_range_self] rw [← isHolonomicAt_localize_iff _ p.φ p.ψ rg e, ← JetSec.unloc_hol_at_iff] - exact OneJetSec.isHolonomicAt_congr (Filter.eventually_of_forall fun e ↦ p.mkHtpy_localize h rg) + exact OneJetSec.isHolonomicAt_congr (Filter.Eventually.of_forall fun e ↦ p.mkHtpy_localize h rg) theorem ChartPair.dist_update' [FiniteDimensional ℝ E'] {δ : M → ℝ} (hδ_pos : ∀ x, 0 < δ x) (hδ_cont : Continuous δ) {F : FormalSol R} (hF : range (F.bs ∘ p.φ) ⊆ range p.ψ) : diff --git a/SphereEversion/Global/LocalisationData.lean b/SphereEversion/Global/LocalisationData.lean index 25efae66..e01f8847 100644 --- a/SphereEversion/Global/LocalisationData.lean +++ b/SphereEversion/Global/LocalisationData.lean @@ -44,6 +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 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)] @@ -90,6 +91,7 @@ theorem targetCharts_cover : (⋃ i', targetCharts E' I' M' i' '' ball (0 : E') variable (E) {M'} variable {f : M → M'} (hf : Continuous f) +include hf in theorem nice_atlas_domain : ∃ n, ∃ φ : IndexType n → OpenSmoothEmbedding 𝓘(ℝ, E) E I M, @@ -119,6 +121,12 @@ def stdLocalisationData : LocalisationData I I' f where 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'] + /-- Lemma `lem:localisation_stability`. -/ theorem localisation_stability {f : M → M'} (ld : LocalisationData I I' f) : ∃ (ε : M → ℝ) (_hε : ∀ m, 0 < ε m) (_hε' : Continuous ε), @@ -154,8 +162,12 @@ theorem ε_spec (ld : LocalisationData I I' f) : range (g ∘ ld.φ i) ⊆ range (ld.ψj i) := (localisation_stability ld).choose_spec.choose_spec.choose_spec +end LocalisationData +end + variable (I I') +open LocalisationData in theorem _root_.exists_stability_dist {f : M → M'} (hf : Continuous f) : ∃ ε : M → ℝ, (∀ m, 0 < ε m) ∧ Continuous ε ∧ ∀ x : M, @@ -171,6 +183,4 @@ theorem _root_.exists_stability_dist {f : M → M'} (hf : Continuous f) : have := L.ε_spec tauto -end LocalisationData - end diff --git a/SphereEversion/Global/OneJetSec.lean b/SphereEversion/Global/OneJetSec.lean index 97662054..ddf994f2 100644 --- a/SphereEversion/Global/OneJetSec.lean +++ b/SphereEversion/Global/OneJetSec.lean @@ -161,7 +161,7 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type*} [Top [TopologicalSpace M'] [ChartedSpace H' M'] [SmoothManifoldWithCorners 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] {F' : Type*} [NormedAddCommGroup F'] [NormedSpace ℝ F'] + /-[SmoothManifoldWithCorners J 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*} [NormedAddCommGroup EP] [NormedSpace ℝ EP] {HP : Type*} [TopologicalSpace HP] diff --git a/SphereEversion/Global/ParametricityForFree.lean b/SphereEversion/Global/ParametricityForFree.lean index bf795de0..8b776f85 100644 --- a/SphereEversion/Global/ParametricityForFree.lean +++ b/SphereEversion/Global/ParametricityForFree.lean @@ -131,7 +131,7 @@ theorem RelMfld.Ample.relativize (hR : R.Ample) : (R.relativize IP P).Ample := b obtain ⟨u', hu'⟩ := ContinuousLinearMap.exists_ne_zero h let u := (p2 u')⁻¹ • u' let q : DualPair (TangentSpace I σ.1.1.2) := - ⟨p2, u, by erw [p2.map_smul, smul_eq_mul, inv_mul_cancel hu']⟩ + ⟨p2, u, by erw [p2.map_smul, smul_eq_mul, inv_mul_cancel₀ hu']⟩ rw [relativize_slice q rfl] exact (hR q).vadd diff --git a/SphereEversion/Global/Relation.lean b/SphereEversion/Global/Relation.lean index 86d7e15b..e543599b 100644 --- a/SphereEversion/Global/Relation.lean +++ b/SphereEversion/Global/Relation.lean @@ -40,7 +40,7 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] (M' : Type*) [TopologicalSpace M'] [ChartedSpace H' M'] [SmoothManifoldWithCorners 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] /-[SmoothManifoldWithCorners J 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'] @@ -74,7 +74,7 @@ instance (R : RelMfld I M I' M') : FunLike (FormalSol R) M (OneJetBundle I M I' intro F G h ext x : 2 · exact congrArg Prod.snd (congrArg Bundle.TotalSpace.proj (congrFun h x)) - · simpa using ((Bundle.TotalSpace.ext_iff _ _).mp (congrFun h x)).2 + · simpa using (Bundle.TotalSpace.ext_iff.mp (congrFun h x)).2 def mkFormalSol (F : M → OneJetBundle I M I' M') (hsec : ∀ x, (F x).1.1 = x) (hsol : ∀ x, F x ∈ R) diff --git a/SphereEversion/Global/SmoothEmbedding.lean b/SphereEversion/Global/SmoothEmbedding.lean index 28f46a5e..ce784cf9 100644 --- a/SphereEversion/Global/SmoothEmbedding.lean +++ b/SphereEversion/Global/SmoothEmbedding.lean @@ -17,10 +17,10 @@ section General 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] {E' : 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'] + --[SmoothManifoldWithCorners I' M'] structure OpenSmoothEmbedding where toFun : M → M' @@ -79,6 +79,10 @@ theorem isOpenMap : IsOpenMap f := theorem coe_comp_invFun_eventuallyEq (x : M) : f ∘ f.invFun =ᶠ[𝓝 (f x)] id := Filter.eventually_of_mem (f.isOpenMap.range_mem_nhds x) fun _ hy ↦ f.right_inv hy +section + +variable [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners 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) := @@ -116,6 +120,8 @@ theorem fderiv_symm_coe' {x : M'} (hx : x ∈ range f) : (mfderiv I' I f.invFun x : TangentSpace I' x →L[𝕜] TangentSpace I (f.invFun x)) := by rw [fderiv_symm_coe, f.right_inv hx] +end + open Filter theorem openEmbedding : OpenEmbedding f := @@ -227,7 +233,7 @@ open Function universe u variable {F H : Type*} (M : Type u) [NormedAddCommGroup F] [NormedSpace ℝ F] [TopologicalSpace H] - [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [LocallyCompactSpace M] [SigmaCompactSpace M] + [TopologicalSpace M] [ChartedSpace H M] (IF : ModelWithCorners ℝ F H) [SmoothManifoldWithCorners IF M] /- Clearly should be generalised. Maybe what we really want is a theory of local diffeomorphisms. @@ -286,6 +292,7 @@ theorem range_openSmoothEmbOfDiffeoSubsetChartTarget (x : M) {f : PartialHomeomo variable {M} (F) variable [IF.Boundaryless] [FiniteDimensional ℝ F] +variable [T2Space M] [LocallyCompactSpace M] [SigmaCompactSpace M] theorem nice_atlas' {ι : Type*} {s : ι → Set M} (s_op : ∀ j, IsOpen <| s j) (cov : (⋃ j, s j) = univ) (U : Set F) (hU₁ : (0 : F) ∈ U) (hU₂ : IsOpen U) : @@ -369,14 +376,14 @@ variable {𝕜 EX EM EY EN EM' X M Y N M' : Type*} [NontriviallyNormedField 𝕜 {HM : Type*} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} {HM' : Type*} [TopologicalSpace HM'] {IM' : ModelWithCorners 𝕜 EM' HM'} {HN : Type*} [TopologicalSpace HN] {IN : ModelWithCorners 𝕜 EN HN} - [TopologicalSpace X] [ChartedSpace HX X] [SmoothManifoldWithCorners IX X] - [TopologicalSpace M] [ChartedSpace HM M] [SmoothManifoldWithCorners IM M] + [TopologicalSpace X] [ChartedSpace HX X] --[SmoothManifoldWithCorners IX X] + [TopologicalSpace M] [ChartedSpace HM M] --[SmoothManifoldWithCorners IM M] [TopologicalSpace M'] [ChartedSpace HM' M'] section NonMetric -variable [TopologicalSpace Y] [ChartedSpace HY Y] [SmoothManifoldWithCorners IY Y] - [TopologicalSpace N] [ChartedSpace HN N] [SmoothManifoldWithCorners IN N] +variable [TopologicalSpace Y] [ChartedSpace HY Y] --[SmoothManifoldWithCorners IY Y] + [TopologicalSpace N] [ChartedSpace HN N] --[SmoothManifoldWithCorners IN N] (φ : OpenSmoothEmbedding IX X IM M) (ψ : OpenSmoothEmbedding IY Y IN N) (f : M → N) (g : X → Y) section @@ -438,10 +445,11 @@ end NonMetric section Metric -variable [MetricSpace Y] [ChartedSpace HY Y] [SmoothManifoldWithCorners IY Y] [MetricSpace N] - [ChartedSpace HN N] [SmoothManifoldWithCorners IN N] (φ : OpenSmoothEmbedding IX X IM M) +variable [MetricSpace Y] [ChartedSpace HY Y] /- [SmoothManifoldWithCorners IY Y]-/ [MetricSpace N] + [ChartedSpace HN N] /-[SmoothManifoldWithCorners IN N]-/ (φ : OpenSmoothEmbedding IX X IM M) (ψ : OpenSmoothEmbedding IY Y IN N) (f : M → N) (g : X → Y) + /-- This is `lem:dist_updating` in the blueprint. -/ theorem dist_update [ProperSpace Y] {K : Set X} (hK : IsCompact K) {P : Type*} [MetricSpace P] {KP : Set P} (hKP : IsCompact KP) (f : P → M → N) (hf : Continuous ↿f) diff --git a/SphereEversion/Global/TwistOneJetSec.lean b/SphereEversion/Global/TwistOneJetSec.lean index 865b9036..8c9522e6 100644 --- a/SphereEversion/Global/TwistOneJetSec.lean +++ b/SphereEversion/Global/TwistOneJetSec.lean @@ -21,7 +21,7 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCo [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners 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] (V : Type*) [NormedAddCommGroup V] [NormedSpace 𝕜 V] + /-[SmoothManifoldWithCorners J N]-/ (V : Type*) [NormedAddCommGroup V] [NormedSpace 𝕜 V] (V' : Type*) [NormedAddCommGroup V'] [NormedSpace 𝕜 V'] section Smoothness @@ -178,7 +178,7 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type*} [Top [SmoothManifoldWithCorners 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] [SmoothManifoldWithCorners J N] + [TopologicalSpace N] [ChartedSpace G N] /-[SmoothManifoldWithCorners J N]-/ /-- A section of a 1-jet bundle seen as a bundle over the source manifold. -/ @[ext] diff --git a/SphereEversion/InductiveConstructions.lean b/SphereEversion/InductiveConstructions.lean index a6539a13..f16348e9 100644 --- a/SphereEversion/InductiveConstructions.lean +++ b/SphereEversion/InductiveConstructions.lean @@ -216,7 +216,7 @@ theorem relative_inductive_construction_of_loc {X Y : Type*} [EMetricSpace X] ∃ f : X → Y, (∀ x, P₀ x f ∧ P₁ x f) ∧ ∀ᶠ x near K, f x = f₀ x := by let P₀' : ∀ x : X, Germ (𝓝 x) Y → Prop := RestrictGermPredicate (fun x φ ↦ φ.value = f₀ x) K have hf₀ : ∀ x, P₀ x f₀ ∧ P₀' x f₀ := fun x ↦ - ⟨hP₀f₀ x, fun _ ↦ eventually_of_forall fun x' ↦ rfl⟩ + ⟨hP₀f₀ x, fun _ ↦ Eventually.of_forall fun x' ↦ rfl⟩ have ind' : ∀ {U₁ U₂ K₁ K₂ : Set X} {f₁ f₂ : X → Y}, IsOpen U₁ → IsOpen U₂ → IsCompact K₁ → IsCompact K₂ → K₁ ⊆ U₁ → K₂ ⊆ U₂ → (∀ x, P₀ x f₁ ∧ P₀' x f₁) → (∀ x, P₀ x f₂) → (∀ x ∈ U₁, P₁ x f₁) → (∀ x ∈ U₂, P₁ x f₂) → diff --git a/SphereEversion/Local/Corrugation.lean b/SphereEversion/Local/Corrugation.lean index ed9ade94..fef8c102 100644 --- a/SphereEversion/Local/Corrugation.lean +++ b/SphereEversion/Local/Corrugation.lean @@ -168,7 +168,7 @@ theorem corrugation.fderiv_eq {N : ℝ} (hN : N ≠ 0) (hγ_diff : 𝒞 1 ↿γ) erw [fderiv_const_smul key.differentiableAt, key.fderiv, smul_add, add_comm] congr 1 rw [fderiv_const_smul (hπ_diff.differentiable le_rfl).differentiableAt N, π.fderiv] - simp only [smul_smul, inv_mul_cancel hN, one_div, Algebra.id.smul_eq_mul, one_smul, + simp only [smul_smul, inv_mul_cancel₀ hN, one_div, Algebra.id.smul_eq_mul, one_smul, ContinuousLinearMap.comp_smul] theorem corrugation.fderiv_apply (hN : N ≠ 0) (hγ_diff : 𝒞 1 ↿γ) (x v : E) : diff --git a/SphereEversion/Local/HPrinciple.lean b/SphereEversion/Local/HPrinciple.lean index 71b3e35e..ee431086 100644 --- a/SphereEversion/Local/HPrinciple.lean +++ b/SphereEversion/Local/HPrinciple.lean @@ -267,7 +267,7 @@ theorem improveStep_of_support (t : ℝ) {x : E} (H : ∀ t, x ∉ Loop.support intro t s rw [Loop.isConst_of_not_mem_support (H t) s 0] apply (L.nice h).s_zero x t - rw [improveStep_apply L h, corrugation_eq_zero _ _ _ _ (H t), + rw [improveStep_apply (L := L) h, corrugation_eq_zero _ _ _ _ (H t), remainder_eq_zero _ _ (L.loop_C1 h 1) (H 1)] simp only [FormalSol.toJetSec_eq_coe, smul_zero, add_zero, this] erw [L.p.update_self] @@ -275,15 +275,15 @@ theorem improveStep_of_support (t : ℝ) {x : E} (H : ∀ t, x ∉ Loop.support theorem improveStep_rel_t_eq_0 : L.improveStep h N 0 = 𝓕 := by ext x : 2 - · rw [improveStep_apply_f _ h] + · rw [improveStep_apply_f h] simp [(L.nice h).t_zero x] - · rw [improveStep_apply_φ _ h] + · rw [improveStep_apply_φ h] simp only [FormalSol.toJetSec_eq_coe, MulZeroClass.zero_mul, smoothStep.zero, zero_smul, add_zero] erw [L.update_zero h] theorem improveStep_rel_compl_K₁ {x} (hx : x ∉ L.K₁) (t) : L.improveStep h N t x = 𝓕 x := by - rw [improveStep_apply _ h, L.hρ_compl_K₁ hx] + rw [improveStep_apply h, L.hρ_compl_K₁ hx] simp only [FormalSol.toJetSec_eq_coe, MulZeroClass.mul_zero, zero_smul, add_zero] erw [L.update_zero h] rfl @@ -298,7 +298,7 @@ theorem improveStep_rel_K : ∀ᶠ x near L.K, ∀ t, L.improveStep h N t x = exact Loop.isConst_of_eq (hy t) apply this.mono intro x hx t - exact improveStep_of_support _ _ _ _ hx + exact improveStep_of_support _ _ _ hx theorem improveStep_rel_C : ∀ᶠ x near L.C, ∀ t, L.improveStep h N t x = 𝓕 x := by apply Eventually.filter_mono (L.hK₁.isClosed.nhdsSet_le_sup' L.C) @@ -306,7 +306,7 @@ theorem improveStep_rel_C : ∀ᶠ x near L.C, ∀ t, L.improveStep h N t x = constructor · apply improveStep_rel_K · rw [eventually_principal] - exact fun x ↦ improveStep_rel_compl_K₁ _ h N + exact fun x ↦ improveStep_rel_compl_K₁ h N -- In the next lemma, we reintroduce `F` to appease the unused argument linter -- since `FiniteDimensional ℝ F` isn't needed here. @@ -330,11 +330,11 @@ theorem improveStep_c0_close {ε : ℝ} (ε_pos : 0 < ε) : remainder_c0_small_on L.π L.hK₁ γ_C1 ε_pos).mono rintro N ⟨H, _⟩ x t by_cases hx : x ∈ L.K₁ - · rw [improveStep_apply_f _ h] + · rw [improveStep_apply_f h] suffices ‖(smoothStep t * L.ρ x) • corrugation L.π N (L.loop h t) x‖ ≤ ε by simpa - exact (bu_lt _ _ _ <| H _ hx t).le + exact (bu_lt _ _ <| H _ hx t).le · rw [show (L.improveStep h N t).f x = 𝓕.f x from - congr_arg Prod.fst (improveStep_rel_compl_K₁ _ h N hx t)] + congr_arg Prod.fst (improveStep_rel_compl_K₁ h N hx t)] simp [ε_pos.le] theorem improveStep_part_hol {N : ℝ} (hN : N ≠ 0) : @@ -358,7 +358,7 @@ theorem improveStep_part_hol {N : ℝ} (hN : N ≠ 0) : have H : ∀ᶠ x near L.K₀, L.improveStep h N 1 x = 𝓕' x := by apply L.hρ₀.mono intro x hx - simp [𝓕', improveStep_apply _ h, hx] + simp [𝓕', improveStep_apply h, hx] have fderiv_𝓕' := fun x ↦ fderiv_corrugated_map N hN γ_C1 (𝓕.f_diff.of_le le_top) L.p ((L.nice h).avg x) rw [eventually_congr (H.isPartHolonomicAt_congr (L.p.spanV ⊔ L.E'))] @@ -411,13 +411,13 @@ theorem improveStep_formalSol : ∀ᶠ N in atTop, ∀ t, (L.improveStep h N t). · simp only [h, improveStep_apply_f, FormalSol.toJetSec_eq_coe, improveStep_apply_φ] rw [Prod.dist_eq, max_lt_iff, Prod.dist_eq, max_lt_iff] refine ⟨by simpa using ε_pos, ?_, ?_⟩ <;> dsimp only <;> rw [dist_self_add_left] - · exact bu_lt _ _ _ <| H _ hxK₁ _ + · exact bu_lt _ _ <| H _ hxK₁ _ -- adaptation note(2024-03-28): `exact` used to work; started failing after mathlib bump - · apply bu_lt _ _ _ <| H' _ hxK₁ + · apply bu_lt _ _ <| H' _ hxK₁ · rw [show ((L.improveStep h N) t).f x = 𝓕.f x from - congr_arg Prod.fst <| improveStep_rel_compl_K₁ _ h N hxK₁ t, + congr_arg Prod.fst <| improveStep_rel_compl_K₁ h N hxK₁ t, show ((L.improveStep h N) t).φ x = 𝓕.φ x from - congr_arg Prod.snd <| improveStep_rel_compl_K₁ _ h N hxK₁ t] + congr_arg Prod.snd <| improveStep_rel_compl_K₁ h N hxK₁ t] exact 𝓕.is_sol _ end StepLandscape @@ -443,6 +443,7 @@ variable (L : Landscape E) variable {ε : ℝ} (ε_pos : 0 < ε) +include ε_pos h_op h_ample in /-- Homotopy of formal solutions obtained by successive corrugations in some landscape `L` to improve a formal solution `𝓕` until it becomes holonomic near `L.K₀`. @@ -498,7 +499,7 @@ theorem RelLoc.FormalSol.improve (𝓕 : FormalSol R) (h_hol : ∀ᶠ x near L.C intro x hx apply hHK₁ x hx obtain ⟨N, ⟨hN_close, hN_sol⟩, hNneq⟩ := - (((improveStep_c0_close _ acc <| half_pos δ_pos).and (improveStep_formalSol _ acc)).and <| + (((improveStep_c0_close acc <| half_pos δ_pos).and (improveStep_formalSol acc)).and <| eventually_ne_atTop (0 : ℝ)).exists have glue : H 1 = S.improveStep acc N 0 := by rw [improveStep_rel_t_eq_0] @@ -513,7 +514,7 @@ theorem RelLoc.FormalSol.improve (𝓕 : FormalSol R) (h_hol : ∀ᶠ x near L.C intro t ht rw [ht, H.comp_1] · -- rel C - apply (hHC.and <| hH₁_rel_C.and <| improveStep_rel_C _ acc N).mono + apply (hHC.and <| hH₁_rel_C.and <| improveStep_rel_C acc N).mono rintro x ⟨hx, hx', hx''⟩ t by_cases ht : t ≤ 1 / 2 · simp only [ht, hx, HtpyJetSec.comp_of_le] @@ -539,8 +540,9 @@ theorem RelLoc.FormalSol.improve (𝓕 : FormalSol R) (h_hol : ∀ᶠ x near L.C · simp only [ht, hN_sol, HtpyJetSec.comp_of_not_le, not_false_iff] · -- part-hol E' (k + 1) rw [h_span, HtpyJetSec.comp_1] - apply improveStep_part_hol _ acc hNneq + apply improveStep_part_hol acc hNneq +include ε_pos h_op h_ample in /-- A repackaging of `RelLoc.FormalSol.improve` for convenience. -/ theorem RelLoc.FormalSol.improve_htpy' (𝓕 : FormalSol R) (h_hol : ∀ᶠ x near L.C, 𝓕.IsHolonomicAt x) : diff --git a/SphereEversion/Local/ParametricHPrinciple.lean b/SphereEversion/Local/ParametricHPrinciple.lean index 45a893b9..072141d8 100644 --- a/SphereEversion/Local/ParametricHPrinciple.lean +++ b/SphereEversion/Local/ParametricHPrinciple.lean @@ -118,7 +118,7 @@ theorem RelLoc.IsAmple.relativize (hR : R.IsAmple) : (R.relativize P).IsAmple := PreconnectedSpace.connectedComponent_eq_univ, convexHull_univ] obtain ⟨u', hu'⟩ := ContinuousLinearMap.exists_ne_zero h let u := (p2 u')⁻¹ • u' - let q : DualPair E := ⟨p2, u, by rw [p2.map_smul, smul_eq_mul, inv_mul_cancel hu']⟩ + let q : DualPair E := ⟨p2, u, by rw [p2.map_smul, smul_eq_mul, inv_mul_cancel₀ hu']⟩ rw [relativize_slice_loc q rfl] exact (hR q _).vadd @@ -265,6 +265,7 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimension variable {R : RelLoc E F} (h_op : IsOpen R) (h_ample : R.IsAmple) (L : Landscape E) +include h_op h_ample in -- The local parametric h-principle. theorem RelLoc.FamilyFormalSol.improve_htpy {ε : ℝ} (ε_pos : 0 < ε) (C : Set (P × E)) (hC : IsClosed C) (K : Set (P × E)) (hK : IsCompact K) (𝓕₀ : FamilyFormalSol P R) @@ -296,6 +297,7 @@ open Filter open scoped unitInterval +include h_op h_ample in /-- A corollary of the local parametric h-principle, forgetting the homotopy and `ε`-closeness, and just stating the existence of a solution that is holonomic near `K`. Furthermore, we assume that `P = ℝ` and `K` is of the form `compact set × I`. diff --git a/SphereEversion/Local/Relation.lean b/SphereEversion/Local/Relation.lean index 06ea8108..5610262c 100644 --- a/SphereEversion/Local/Relation.lean +++ b/SphereEversion/Local/Relation.lean @@ -119,6 +119,6 @@ instance (R : RelLoc E F) : FunLike (FamilyFormalSol P R) P (JetSec E F) := ⟨fun S ↦ S.toFamilyJetSec, by intros S S' h ext p x : 3 <;> replace h := congrFun h p - exacts [congrFun ((JetSec.ext_iff _ _).1 h).1 x, congrFun ((JetSec.ext_iff _ _).1 h).2 x]⟩ + exacts [congrFun (JetSec.ext_iff.1 h).1 x, congrFun (JetSec.ext_iff.1 h).2 x]⟩ end RelLoc diff --git a/SphereEversion/Loops/Basic.lean b/SphereEversion/Loops/Basic.lean index b039c3b5..92489fd5 100644 --- a/SphereEversion/Loops/Basic.lean +++ b/SphereEversion/Loops/Basic.lean @@ -51,9 +51,6 @@ protected theorem coe_mk {γ : ℝ → X} (h : ∀ t, γ (t + 1) = γ t) : ⇑( protected theorem ext : ∀ {γ₁ γ₂ : Loop X}, (γ₁ : ℝ → X) = γ₂ → γ₁ = γ₂ | ⟨_x, _h1⟩, ⟨.(_x), _h2⟩, rfl => rfl -protected theorem ext_iff {γ₁ γ₂ : Loop X} : γ₁ = γ₂ ↔ (γ₁ : ℝ → X) = γ₂ := - ⟨fun h ↦ by rw [h], Loop.ext⟩ - /-- The constant loop. -/ @[simps] def const (f : X) : Loop X := @@ -127,7 +124,7 @@ instance [AddCommGroup X] : AddCommGroup (Loop X) := add_comm := fun γ₁ γ₂ ↦ by ext t; apply add_comm zero_add := fun γ ↦ by ext t; apply zero_add add_zero := fun γ ↦ by ext t; apply add_zero - add_left_neg := fun γ ↦ by ext t; apply add_left_neg + neg_add_cancel := fun γ ↦ by ext t; apply neg_add_cancel nsmul := nsmulRec zsmul := zsmulRec } @@ -180,6 +177,7 @@ the loop is not constant. -/ def support (γ : X → Loop X') : Set X := closure {x | ¬(γ x).IsConst} +omit [TopologicalSpace X'] in theorem not_mem_support {γ : X → Loop X'} {x : X} (h : ∀ᶠ y in 𝓝 x, (γ y).IsConst) : x ∉ Loop.support γ := by intro hx @@ -283,12 +281,8 @@ theorem roundTripFamily_one {x y : X} {γ : Path x y} : (roundTripFamily γ) 1 = simp only [roundTripFamily, roundTrip, Path.truncate_zero_one, ofPath] rfl -section Average - /-! ## Average value of a loop -/ - - -variable [MeasurableSpace F] [BorelSpace F] [SecondCountableTopology F] [CompleteSpace F] +section Average /-- The average value of a loop. -/ noncomputable def average (γ : Loop F) : F := @@ -299,7 +293,7 @@ noncomputable def average (γ : Loop F) : F := theorem zero_average : average (0 : Loop F) = 0 := intervalIntegral.integral_zero -theorem isConst_iff_forall_avg {γ : Loop F} : γ.IsConst ↔ ∀ t, γ t = γ.average := by +theorem isConst_iff_forall_avg [CompleteSpace F] {γ : Loop F} : γ.IsConst ↔ ∀ t, γ t = γ.average := by constructor <;> intro h · intro t have : γ = Loop.const (γ t) := by @@ -311,7 +305,7 @@ theorem isConst_iff_forall_avg {γ : Loop F} : γ.IsConst ↔ ∀ t, γ t = γ.a · exact isConst_of_eq h @[simp] -theorem average_const {f : F} : (const f).average = f := by simp [Loop.average] +theorem average_const [CompleteSpace F] {f : F} : (const f).average = f := by simp [Loop.average] open MeasureTheory @@ -324,9 +318,10 @@ theorem average_add {γ₁ γ₂ : Loop F} (hγ₁ : IntervalIntegrable γ₁ vo theorem average_smul {γ : Loop F} {c : ℝ} : (c • γ).average = c • γ.average := by simp [Loop.average, intervalIntegral.integral_smul] -theorem isConst_iff_const_avg {γ : Loop F} : γ.IsConst ↔ γ = const γ.average := by +theorem isConst_iff_const_avg [CompleteSpace F] {γ : Loop F} : γ.IsConst ↔ γ = const γ.average := by rw [Loop.isConst_iff_forall_avg, Loop.ext_iff, funext_iff]; rfl +omit [NormedAddCommGroup F] [NormedSpace ℝ F] in theorem isConst_of_not_mem_support {γ : X → Loop F} {x : X} (hx : x ∉ support γ) : (γ x).IsConst := by classical exact Decidable.by_contradiction fun H ↦ hx (subset_closure H) @@ -345,7 +340,7 @@ theorem normalize_apply (γ : Loop F) (t : ℝ) : Loop.normalize γ t = γ t - rfl @[simp] -theorem normalize_of_isConst {γ : Loop F} (h : γ.IsConst) : γ.normalize = 0 := by +theorem normalize_of_isConst [CompleteSpace F] {γ : Loop F} (h : γ.IsConst) : γ.normalize = 0 := by ext t simp [isConst_iff_forall_avg.mp h] @@ -378,7 +373,7 @@ theorem Loop.continuous_diff {γ : E → Loop F} (h : 𝒞 1 ↿γ) : Continuous theorem ContDiff.partial_loop {γ : E → Loop F} {n : ℕ∞} (hγ_diff : 𝒞 n ↿γ) : ∀ t, 𝒞 n fun e ↦ γ e t := fun t ↦ hγ_diff.comp ((contDiff_prod_mk_left t).of_le le_top) -variable [MeasurableSpace F] [BorelSpace F] [FiniteDimensional ℝ F] +variable [FiniteDimensional ℝ F] theorem Loop.support_diff {γ : E → Loop F} : Loop.support (Loop.diff γ) ⊆ Loop.support γ := by unfold Loop.support diff --git a/SphereEversion/Loops/Surrounding.lean b/SphereEversion/Loops/Surrounding.lean index e1e9fcbf..8353f651 100644 --- a/SphereEversion/Loops/Surrounding.lean +++ b/SphereEversion/Loops/Surrounding.lean @@ -4,8 +4,6 @@ import SphereEversion.ToMathlib.Analysis.Normed.Module.FiniteDimension import SphereEversion.ToMathlib.ExistsOfConvex import SphereEversion.ToMathlib.SmoothBarycentric import SphereEversion.ToMathlib.Topology.Path -import Mathlib.Analysis.Convex.Caratheodory -import Mathlib.Analysis.NormedSpace.AddTorsorBases /-! # Surrounding families of loops @@ -174,6 +172,7 @@ theorem surrounded_iff_mem_interior_convexHull_aff_basis [FiniteDimensional ℝ theorem surrounded_of_convexHull [FiniteDimensional ℝ F] {f : F} {s : Set F} (hs : IsOpen s) (hsf : f ∈ convexHull ℝ s) : Surrounded f s := by rw [surrounded_iff_mem_interior_convexHull_aff_basis] + sorry /- TODO fix! old proof was; type mismatch on `hsf` now obtain ⟨t, hts, hai, hf⟩ := (by simpa only [exists_prop, mem_iUnion] using convexHull_eq_union.subst hsf : ∃ t : Finset F, @@ -190,7 +189,7 @@ theorem surrounded_of_convexHull [FiniteDimensional ℝ F] {f : F} {s : Set F} ( let t : Units ℝ := Units.mk0 ε (by linarith) refine ⟨AffineMap.homothety c (t : ℝ) '' b, hcs, ?_, ?_, hbε (convexHull_mono hb₁ hf)⟩ · rwa [(AffineEquiv.homothetyUnitsMulHom c t).affineIndependent_set_of_eq_iff] - · exact (AffineEquiv.homothetyUnitsMulHom c t).span_eq_top_iff.mp hb₄ + · exact (AffineEquiv.homothetyUnitsMulHom c t).span_eq_top_iff.mp hb₄ -/ /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ -- `lem:smooth_barycentric_coord` @@ -343,6 +342,7 @@ theorem affineEquiv_surrounds_iff (e : F ≃ᵃ[ℝ] F) : erw [Finset.map_affineCombination _ (γ ∘ t) _ w_sum (e : F →ᵃ[ℝ] F)] congr +omit [NormedSpace ℝ F] in @[simp] theorem zero_vadd : (0 : F) +ᵥ γ = γ := by ext t @@ -366,7 +366,7 @@ theorem Surrounds.smul0 (h : γ.Surrounds 0) (ht : t ≠ 0) : (t • γ).Surroun AffineEquiv.coe_homothetyUnitsMulHom_apply, AffineMap.homothety_apply_same] convert h ext u - simp [AffineMap.homothety_apply, smul_smul, inv_mul_cancel ht] + simp [AffineMap.homothety_apply, smul_smul, inv_mul_cancel₀ ht] theorem Surrounds.mono (h : γ.Surrounds x) (h2 : range γ ⊆ range γ') : γ'.Surrounds x := by revert h; simp_rw [Loop.surrounds_iff_range_subset_range] @@ -481,6 +481,8 @@ namespace SurroundingFamily variable {g b : E → F} {γ : E → ℝ → Loop F} {U : Set E} +omit [NormedSpace ℝ E] + protected theorem one (h : SurroundingFamily g b γ U) (x : E) (t : ℝ) : γ x t 1 = b x := by rw [Loop.one, h.base] @@ -497,6 +499,7 @@ protected theorem mono (h : SurroundingFamily g b γ U) {V : Set E} (hVU : V ⊆ SurroundingFamily g b γ V := ⟨h.base, h.t₀, h.projI, fun x hx ↦ h.surrounds x (hVU hx), h.cont⟩ +variable [NormedSpace ℝ E] in protected theorem surrounds_of_close_univ [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] (hg : Continuous g) (h : SurroundingFamily g b γ univ) : ∃ ε : E → ℝ, @@ -586,6 +589,8 @@ namespace SurroundingFamilyIn variable {γ : E → ℝ → Loop F} +omit [NormedSpace ℝ E] + /-- Abbreviation for `toSurroundingFamily` -/ theorem to_sf (h : SurroundingFamilyIn g b γ U Ω) : SurroundingFamily g b γ U := h.toSurroundingFamily @@ -620,6 +625,8 @@ section local_loops variable {x₀ : E} (hΩ_conn : IsPathConnected (Prod.mk x₀ ⁻¹' Ω)) (hb_in : (x₀, b x₀) ∈ Ω) {p : Fin (d + 1) → F} (hp : ∀ i, p i ∈ Prod.mk x₀ ⁻¹' Ω) +omit [NormedSpace ℝ E] + /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ -- /-- The witness of `local_loops`. -/ -- def local_loops_def (x : E) (t : ℝ) : loop F := @@ -740,6 +747,8 @@ def sfHomotopy (τ : ℝ) (x : E) (t : ℝ) := variable {h₀ h₁} +omit [NormedSpace ℝ E] + @[simp] theorem sfHomotopy_zero : sfHomotopy h₀ h₁ 0 = γ₀ := by ext x t s @@ -771,11 +780,12 @@ theorem Continuous.sfHomotopy {X : Type*} [UniformSpace X] /-- In this lemmas and the lemmas below we add `FiniteDimensional ℝ E` so that we can conclude `LocallyCompactSpace E`. -/ -theorem continuous_sfHomotopy [FiniteDimensional ℝ E] : Continuous ↿(sfHomotopy h₀ h₁) := +theorem continuous_sfHomotopy [NormedSpace ℝ E] [FiniteDimensional ℝ E] : + Continuous ↿(sfHomotopy h₀ h₁) := Continuous.sfHomotopy continuous_fst continuous_snd.fst continuous_snd.snd.fst continuous_snd.snd.snd -theorem surroundingFamily_sfHomotopy [FiniteDimensional ℝ E] (τ : ℝ) : +theorem surroundingFamily_sfHomotopy [NormedSpace ℝ E] [FiniteDimensional ℝ E] (τ : ℝ) : SurroundingFamily g b (sfHomotopy h₀ h₁ τ) U := by constructor · intro x t; @@ -825,12 +835,12 @@ theorem sfHomotopy_in (h₀ : SurroundingFamilyIn g b γ₀ U Ω) (h₁ : Surrou sfHomotopy_in' h₀.to_sf h₁.to_sf (fun _ ↦ τ) (fun _ ↦ x) () hx ht (fun _i hx _t _ _s _ ↦ h₀.val_in hx) fun _i hx _t _ _s _ ↦ h₁.val_in hx -theorem surroundingFamilyIn_sfHomotopy [FiniteDimensional ℝ E] (h₀ : SurroundingFamilyIn g b γ₀ U Ω) - (h₁ : SurroundingFamilyIn g b γ₁ U Ω) (τ : ℝ) : +theorem surroundingFamilyIn_sfHomotopy [NormedSpace ℝ E] [FiniteDimensional ℝ E] + (h₀ : SurroundingFamilyIn g b γ₀ U Ω) (h₁ : SurroundingFamilyIn g b γ₁ U Ω) (τ : ℝ) : SurroundingFamilyIn g b (sfHomotopy h₀.to_sf h₁.to_sf τ) U Ω := ⟨surroundingFamily_sfHomotopy _, fun _x hx _t ht _s _hs ↦ sfHomotopy_in h₀ h₁ _ hx ht⟩ -theorem satisfied_or_refund [FiniteDimensional ℝ E] {γ₀ γ₁ : E → ℝ → Loop F} +theorem satisfied_or_refund [NormedSpace ℝ E] [FiniteDimensional ℝ E] {γ₀ γ₁ : E → ℝ → Loop F} (h₀ : SurroundingFamilyIn g b γ₀ U Ω) (h₁ : SurroundingFamilyIn g b γ₁ U Ω) : ∃ γ : ℝ → E → ℝ → Loop F, (∀ τ, SurroundingFamilyIn g b (γ τ) U Ω) ∧ γ 0 = γ₀ ∧ γ 1 = γ₁ ∧ Continuous ↿γ := @@ -922,6 +932,7 @@ def ContinuousGerm {x : E} (φ : Germ (𝓝 x) (ℝ → Loop F)) : Prop := simp only [mem_setOf_eq, hx']) variable (g b Ω) +omit [NormedSpace ℝ E] structure LoopFamilyGerm (x : E) (φ : Germ (𝓝 x) (ℝ → Loop F)) : Prop where base : ∀ t, φ.value t 0 = b x @@ -956,7 +967,7 @@ theorem surroundingFamilyIn_iff_germ {γ : E → ℝ → Loop F} : rintro ⟨x, t, s⟩ apply (h x).cont -variable [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] [SecondCountableTopology E] +variable [NormedSpace ℝ E] [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] [SecondCountableTopology E] theorem exists_surrounding_loops (hK : IsClosed K) (hΩ_op : IsOpen Ω) (hg : ∀ x, ContinuousAt g x) (hb : Continuous b) diff --git a/SphereEversion/ToMathlib/Analysis/Calculus.lean b/SphereEversion/ToMathlib/Analysis/Calculus.lean index d61fbc14..4e17cfd7 100644 --- a/SphereEversion/ToMathlib/Analysis/Calculus.lean +++ b/SphereEversion/ToMathlib/Analysis/Calculus.lean @@ -132,19 +132,23 @@ def partialDerivFst (φ : 𝕜 → F → G) : 𝕜 → F → G := fun k f ↦ /-- The second partial derivative of `φ : E → 𝕜 → G` seen as a function from `E → 𝕜 → G`-/ def partialDerivSnd (φ : E → 𝕜 → G) : E → 𝕜 → G := fun e k ↦ ∂₂ 𝕜 φ e k 1 +omit [NormedAddCommGroup F] [NormedSpace 𝕜 F] in theorem partialFDerivFst_eq_smulRight (φ : 𝕜 → F → G) (k : 𝕜) (f : F) : ∂₁ 𝕜 φ k f = smulRight (1 : 𝕜 →L[𝕜] 𝕜) (partialDerivFst φ k f) := deriv_fderiv.symm +omit [NormedAddCommGroup F] [NormedSpace 𝕜 F] in @[simp] theorem partialFDerivFst_one (φ : 𝕜 → F → G) (k : 𝕜) (f : F) : ∂₁ 𝕜 φ k f 1 = partialDerivFst φ k f := by simp only [partialFDerivFst_eq_smulRight, smulRight_apply, one_apply, one_smul] +omit [NormedAddCommGroup E] [NormedSpace 𝕜 E] in theorem partialFDerivSnd_eq_smulRight (φ : E → 𝕜 → G) (e : E) (k : 𝕜) : ∂₂ 𝕜 φ e k = smulRight (1 : 𝕜 →L[𝕜] 𝕜) (partialDerivSnd φ e k) := deriv_fderiv.symm +omit [NormedAddCommGroup E] [NormedSpace 𝕜 E] in theorem partialFDerivSnd_one (φ : E → 𝕜 → G) (e : E) (k : 𝕜) : ∂₂ 𝕜 φ e k 1 = partialDerivSnd φ e k := by simp only [partialFDerivSnd_eq_smulRight, smulRight_apply, one_apply, one_smul] diff --git a/SphereEversion/ToMathlib/Analysis/Calculus/AddTorsor/AffineMap.lean b/SphereEversion/ToMathlib/Analysis/Calculus/AddTorsor/AffineMap.lean index ba1accf6..c56daa12 100644 --- a/SphereEversion/ToMathlib/Analysis/Calculus/AddTorsor/AffineMap.lean +++ b/SphereEversion/ToMathlib/Analysis/Calculus/AddTorsor/AffineMap.lean @@ -11,7 +11,7 @@ TODO Generalise these lemmas appropriately. open Set Function Metric AffineMap -variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] +variable {F : Type*} [NormedAddCommGroup F] -- Unused -- @[simp] @@ -31,10 +31,12 @@ theorem norm_coe_ball_lt (r : ℝ) (x : ball (0 : F) r) : ‖(x : F)‖ < r := b cases' x with x hx simpa using hx +variable [NormedSpace ℝ F] + theorem mapsTo_homothety_ball (c : F) {r : ℝ} (hr : 0 < r) : MapsTo (fun y ↦ homothety c r⁻¹ y -ᵥ c) (ball c r) (ball 0 1) := fun y hy ↦ by replace hy : r⁻¹ * ‖y - c‖ < 1 := by - rw [← mul_lt_mul_left hr, ← mul_assoc, mul_inv_cancel hr.ne.symm, mul_one, one_mul] + rw [← mul_lt_mul_left hr, ← mul_assoc, mul_inv_cancel₀ hr.ne.symm, mul_one, one_mul] simpa [dist_eq_norm] using hy simp only [homothety_apply, vsub_eq_sub, vadd_eq_add, add_sub_cancel_right, mem_ball_zero_iff, norm_smul, Real.norm_eq_abs, abs_eq_self.2 (inv_pos.mpr hr).le, hy] diff --git a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Projection.lean b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Projection.lean index 3af98845..74d80e47 100644 --- a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Projection.lean +++ b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Projection.lean @@ -46,7 +46,7 @@ theorem span_singleton_eq_span_singleton_of_ne {𝕜 : Type*} [Field 𝕜] {M : end GeneralStuff -variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] +variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] --[CompleteSpace E] theorem LinearIsometryEquiv.apply_ne_zero {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] (φ : E ≃ₗᵢ⋆[ℝ] F) @@ -72,6 +72,7 @@ theorem LinearIsometryEquiv.apply_ne_zero {E : Type*} [NormedAddCommGroup E] [No variable (u v : E) +variable [CompleteSpace E] in theorem orthogonal_line_inf {u v : E} : {.u}ᗮ ⊓ {.v}ᗮ = {.(pr[v]ᗮ u : E)}ᗮ ⊓ {.v}ᗮ := by rw [inf_orthogonal, inf_orthogonal] refine congr_arg _ (le_antisymm (sup_le ?_ le_sup_right) (sup_le ?_ le_sup_right)) <;> @@ -81,6 +82,7 @@ theorem orthogonal_line_inf {u v : E} : {.u}ᗮ ⊓ {.v}ᗮ = {.(pr[v]ᗮ u : E) · rw [projSpanOrthogonal, orthogonalProjection_orthogonal] exact sub_mem (mem_sup_left <| mem_span_singleton_self _) (mem_sup_right <| coe_mem _) +variable [CompleteSpace E] in theorem orthogonal_line_inf_sup_line (u v : E) : {.u}ᗮ ⊓ {.v}ᗮ ⊔ Δ (pr[v]ᗮ u : E) = {.v}ᗮ := by rw [orthogonal_line_inf, sup_comm, sup_orthogonal_inf_of_completeSpace] rw [span_singleton_le_iff_mem] @@ -288,7 +290,7 @@ theorem continuousAt_orthogonalProjection_orthogonal {x₀ : E} (hx₀ : x₀ · rw [norm_smul] exact mul_le_mul_of_nonneg_right (norm_inner_le_norm _ _) (norm_nonneg _) · rw [mul_comm, ← mul_assoc, norm_sub_rev] - exact mul_le_mul_of_nonneg_right ((_root_.le_div_iff hNx₀).mp hy₁) (norm_nonneg x) + exact mul_le_mul_of_nonneg_right ((le_div_iff₀ hNx₀).mp hy₁) (norm_nonneg x) · rw [mul_comm, ← mul_assoc, mul_comm ‖y‖] exact mul_le_mul_of_nonneg_right hη.le (norm_nonneg x) · positivity diff --git a/SphereEversion/ToMathlib/ExistsOfConvex.lean b/SphereEversion/ToMathlib/ExistsOfConvex.lean index 623533d8..13304979 100644 --- a/SphereEversion/ToMathlib/ExistsOfConvex.lean +++ b/SphereEversion/ToMathlib/ExistsOfConvex.lean @@ -55,6 +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 theorem reallyConvex_contMDiffAt (x : M) (n : ℕ∞) : ReallyConvex (smoothGerm I x) {φ : Germ (𝓝 x) F | φ.ContMDiffAt I n} := by classical @@ -119,6 +120,8 @@ variable {H₁ M₁ H₂ M₂ : Type*} @[inherit_doc] local notation "𝓒_on" => ContMDiffOn (I₁.prod I₂) 𝓘(ℝ, F) +omit [FiniteDimensional ℝ E₁] [FiniteDimensional ℝ E₂] + [SmoothManifoldWithCorners I₁ M₁] [SmoothManifoldWithCorners I₂ M₂] in theorem reallyConvex_contMDiffAtProd {x : M₁} (n : ℕ∞) : ReallyConvex (smoothGerm I₁ x) {φ : Germ (𝓝 x) (M₂ → F) | φ.ContMDiffAtProd I₁ I₂ n} := by classical @@ -136,6 +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 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, @@ -160,6 +164,7 @@ theorem exists_contMDiff_of_convex₂ {P : M₁ → (M₂ → F) → Prop} [Sigm rcases exists_of_convex hPP hPP' with ⟨f, hf⟩ exact ⟨f, fun ⟨x, y⟩ ↦ (hf x).1 y, fun x ↦ (hf x).2⟩ +omit [FiniteDimensional ℝ E₂] in theorem exists_contDiff_of_convex₂ {P : E₁ → (E₂ → F) → Prop} (hP : ∀ x, Convex ℝ {f | P x f}) {n : ℕ∞} (hP' : ∀ x : E₁, ∃ U ∈ 𝓝 x, ∃ f : E₁ → E₂ → F, diff --git a/SphereEversion/ToMathlib/Geometry/Manifold/Algebra/SmoothGerm.lean b/SphereEversion/ToMathlib/Geometry/Manifold/Algebra/SmoothGerm.lean index 22441160..9245e5ee 100644 --- a/SphereEversion/ToMathlib/Geometry/Manifold/Algebra/SmoothGerm.lean +++ b/SphereEversion/ToMathlib/Geometry/Manifold/Algebra/SmoothGerm.lean @@ -156,6 +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 theorem smoothGerm.valueOrderRingHom_toRingHom (x : N) : (smoothGerm.valueOrderRingHom IG x).toRingHom = smoothGerm.valueRingHom IG x := rfl @@ -191,6 +192,8 @@ nonrec def mfderiv {x : M} (φ : Germ (𝓝 x) N) : variable {I} +omit [FiniteDimensional ℝ E] [SmoothManifoldWithCorners 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.smooth.of_le le_top @@ -271,6 +274,9 @@ end) -/ variable {I₁ I₂} +omit [FiniteDimensional ℝ E₁] [FiniteDimensional ℝ E₂] [SmoothManifoldWithCorners I₁ M₁] + [SigmaCompactSpace M₁] [T2Space M₁] [SmoothManifoldWithCorners I₂ M₂] + theorem ContMDiffAtProd.add {x : M₁} {φ ψ : Germ (𝓝 x) <| M₂ → F} {n : ℕ∞} : φ.ContMDiffAtProd I₁ I₂ n → ψ.ContMDiffAtProd I₁ I₂ n → (φ + ψ).ContMDiffAtProd I₁ I₂ n := Germ.inductionOn φ fun _f hf ↦ Germ.inductionOn ψ fun _g hg y ↦ (hf y).add (hg y) diff --git a/SphereEversion/ToMathlib/MeasureTheory/ParametricIntervalIntegral.lean b/SphereEversion/ToMathlib/MeasureTheory/ParametricIntervalIntegral.lean index 6b183a58..6889de9a 100644 --- a/SphereEversion/ToMathlib/MeasureTheory/ParametricIntervalIntegral.lean +++ b/SphereEversion/ToMathlib/MeasureTheory/ParametricIntervalIntegral.lean @@ -169,10 +169,11 @@ theorem hasFDerivAt_parametric_primitive_of_contDiff' {F : H → ℝ → E} (hF use K intro t t_in rw [show (fun x : H ↦ F x t) = uncurry F ∘ fun x : H ↦ (x, t) by ext; simp, ← mul_one K] + sorry /- TODO: return to this; old proof was apply hK.comp ((LipschitzWith.prod_mk_right t).lipschitzOnWith <| ball x₀ 1) rw [mapsTo'] rintro ⟨x, s⟩ ⟨x', hx, h⟩; cases h - exact ⟨ball_subset_closedBall hx, mem_Icc_of_Ioo t_in⟩ + exact ⟨ball_subset_closedBall hx, mem_Icc_of_Ioo t_in⟩ -/ have cont_x (x) : Continuous (F x) := hF.continuous.comp (Continuous.Prod.mk x) have int_Icc (x) : IntegrableOn (F x) (Icc a₀ b₀) := (cont_x x).continuousOn.integrableOn_Icc have int_Ioo (x) : IntegrableOn (F x) (Ioo a₀ b₀) := (int_Icc x).mono_set Ioo_subset_Icc_self diff --git a/SphereEversion/ToMathlib/Partition.lean b/SphereEversion/ToMathlib/Partition.lean index 29e49824..dfb58712 100644 --- a/SphereEversion/ToMathlib/Partition.lean +++ b/SphereEversion/ToMathlib/Partition.lean @@ -9,9 +9,9 @@ open Set Function Filter 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] +variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] + {H : Type*} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} + {M : Type*} [TopologicalSpace M] [ChartedSpace H M] section diff --git a/SphereEversion/ToMathlib/SmoothBarycentric.lean b/SphereEversion/ToMathlib/SmoothBarycentric.lean index 1d9fe157..3a615cc8 100644 --- a/SphereEversion/ToMathlib/SmoothBarycentric.lean +++ b/SphereEversion/ToMathlib/SmoothBarycentric.lean @@ -1,6 +1,5 @@ import Mathlib.Analysis.Calculus.AddTorsor.Coord import Mathlib.Analysis.Matrix -import Mathlib.Analysis.NormedSpace.AddTorsorBases import Mathlib.LinearAlgebra.AffineSpace.Matrix noncomputable section diff --git a/SphereEversion/ToMathlib/Topology/Misc.lean b/SphereEversion/ToMathlib/Topology/Misc.lean index 23aee3d9..70561500 100644 --- a/SphereEversion/ToMathlib/Topology/Misc.lean +++ b/SphereEversion/ToMathlib/Topology/Misc.lean @@ -10,7 +10,7 @@ open scoped unitInterval Topology uniformity section Maps -variable {α β : Type*} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {g : β → α} +variable {α β : Type*} {f : α → β} {g : β → α} -- TODO: move to Data.Set.Defs theorem Function.LeftInverse.mem_preimage_iff (hfg : LeftInverse g f) {s : Set α} {x : α} : @@ -21,6 +21,8 @@ theorem Function.LeftInverse.image_eq (hfg : LeftInverse g f) (s : Set α) : f '' s = range f ∩ g ⁻¹' s := by rw [inter_comm, ← image_preimage_eq_inter_range, hfg.preimage_preimage] +variable [TopologicalSpace α] [TopologicalSpace β] + theorem Function.LeftInverse.isOpenMap {f : α → β} {g : β → α} (hfg : LeftInverse g f) (hf : IsOpen (range f)) (hg : ContinuousOn g (range f)) : IsOpenMap f := fun U hU ↦ by rw [hfg.image_eq]; exact hg.isOpen_inter_preimage hf hU diff --git a/lake-manifest.json b/lake-manifest.json index 296ed18c..29aa81d2 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "41bc768e2224d6c75128a877f1d6e198859b3178", + "rev": "8feac540abb781cb1349688c816dc02fae66b49c", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "01ad33937acd996ee99eb74eefb39845e4e4b9f5", + "rev": "2c8ae451ce9ffc83554322b14437159c1a9703f9", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "209712c78b16c795453b6da7f7adbda4589a8f21", + "rev": "e291aa4de57079b3d2199b9eb7b4b00922b85a7c", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -35,10 +35,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "c87908619cccadda23f71262e6898b9893bffa36", + "rev": "eb08eee94098fe530ccd6d8751a86fe405473d4c", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.40", + "inputRev": "v0.0.42", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/lean4-cli", @@ -55,27 +55,27 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "e7e90d90a62e6d12cbb27cbbfc31c094ee4ecc58", + "rev": "3e96ea03edd48b932566ca9b201285ae2d57130d", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/mathlib4.git", + {"url": "https://github.com/leanprover-community/mathlib4", "type": "git", "subDir": null, - "scope": "", - "rev": "2df7d9446f22706562263d8b55076dc073e10d02", + "scope": "leanprover-community", + "rev": "df80b0dd2548c76fbdc3fe5d3a96873dfd46c0dc", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": null, + "inputRev": "master", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/PatrickMassot/checkdecls.git", "type": "git", "subDir": null, "scope": "", - "rev": "21a36f3c07a9229e1287483c16a0dd04e479ecc5", + "rev": "11fa569b1b52f987dc5dcea97fd80eaff95c2fce", "name": "checkdecls", "manifestFile": "lake-manifest.json", "inputRev": null, diff --git a/lean-toolchain b/lean-toolchain index 7f0ea50a..98556ba0 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.10.0 +leanprover/lean4:v4.12.0-rc1 From 59ed18e3daddfc5889dd30eca46882f4be8e1904 Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Fri, 4 Oct 2024 13:57:39 +0200 Subject: [PATCH 2/6] Done --- SphereEversion/Global/Immersion.lean | 9 ++++----- .../Global/LocalizedConstruction.lean | 14 +++++--------- SphereEversion/Global/OneJetBundle.lean | 7 ++++++- SphereEversion/Global/OneJetSec.lean | 2 +- SphereEversion/Global/Relation.lean | 4 ++-- SphereEversion/Global/SmoothEmbedding.lean | 17 +++++++---------- SphereEversion/Global/TwistOneJetSec.lean | 4 ++-- SphereEversion/Local/SphereEversion.lean | 2 +- SphereEversion/Loops/DeltaMollifier.lean | 6 +----- SphereEversion/Loops/Exists.lean | 2 -- SphereEversion/Loops/Reparametrization.lean | 16 +++++++++++----- SphereEversion/Loops/Surrounding.lean | 13 +++++++------ .../Analysis/InnerProductSpace/Projection.lean | 4 +--- .../Geometry/Manifold/VectorBundle/Misc.lean | 2 +- .../ParametricIntervalIntegral.lean | 5 ++--- 15 files changed, 51 insertions(+), 56 deletions(-) diff --git a/SphereEversion/Global/Immersion.lean b/SphereEversion/Global/Immersion.lean index 8e496f5f..29388591 100644 --- a/SphereEversion/Global/Immersion.lean +++ b/SphereEversion/Global/Immersion.lean @@ -93,10 +93,9 @@ 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] - {E' : Type*} [NormedAddCommGroup E'] [NormedSpace ℝ E'] + {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'] - /- [FiniteDimensional ℝ E] -/ [FiniteDimensional ℝ E'] {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] @@ -274,13 +273,13 @@ theorem ContDiff.uncurry_left {f : E → F → G} (n : ℕ∞) (hf : 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] {E' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type*} [TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H') - {M' : Type*} [MetricSpace M'] [ChartedSpace H' M'] --[SmoothManifoldWithCorners I' M'] + {M' : Type*} [MetricSpace M'] [ChartedSpace H' 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] + {P : Type*} [TopologicalSpace P] [ChartedSpace HP P] -- move to Mathlib.Geometry.Manifold.ContMDiff.Product lemma Smooth.inr (x : M) : diff --git a/SphereEversion/Global/LocalizedConstruction.lean b/SphereEversion/Global/LocalizedConstruction.lean index 205f3f80..01ffad50 100644 --- a/SphereEversion/Global/LocalizedConstruction.lean +++ b/SphereEversion/Global/LocalizedConstruction.lean @@ -8,16 +8,12 @@ open Set Filter ModelWithCorners Metric open scoped Topology Manifold variable {EM : Type*} [NormedAddCommGroup EM] [NormedSpace ℝ EM] [FiniteDimensional ℝ EM] - {HM : Type*} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} [Boundaryless IM] + {HM : Type*} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} {M : Type*} [TopologicalSpace M] [ChartedSpace HM M] [SmoothManifoldWithCorners IM M] - [T2Space M] [LocallyCompactSpace M] [Nonempty M] [SigmaCompactSpace M] + [T2Space M] {EX : Type*} [NormedAddCommGroup EX] [NormedSpace ℝ EX] [FiniteDimensional ℝ EX] - [MeasurableSpace EX] [BorelSpace 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] [LocallyCompactSpace X] - [SigmaCompactSpace X] [Nonempty X] + {HX : Type*} [TopologicalSpace HX] {IX : ModelWithCorners ℝ EX HX} + {X : Type*} [MetricSpace X] [ChartedSpace HX X] [SmoothManifoldWithCorners 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) @@ -73,7 +69,7 @@ theorem OpenSmoothEmbedding.improve_formalSol (φ : OpenSmoothEmbedding 𝓘(ℝ exact p.mkHtpy_eq_of_forall hcompat ht have hF't1 : ∀ᶠ t : ℝ near Ici 1, F' t = F' 1 := h𝓕't1.mono fun t ↦ p.mkHtpy_congr _ refine ⟨F', hF't0, hF't1, ?_, hF'relK₁, ?_, ?_⟩ - · apply φ.forall_near hK₁ h𝓕'relC (eventually_of_forall fun x hx t ↦ hF'relK₁ t x hx) + · apply φ.forall_near hK₁ h𝓕'relC (Eventually.of_forall fun x hx t ↦ hF'relK₁ t x hx) · intro e he t rw [p.mkHtpy_eq_of_eq _ _ hcompat] exact he t diff --git a/SphereEversion/Global/OneJetBundle.lean b/SphereEversion/Global/OneJetBundle.lean index a034484f..85ce25c3 100644 --- a/SphereEversion/Global/OneJetBundle.lean +++ b/SphereEversion/Global/OneJetBundle.lean @@ -48,7 +48,7 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {M'' : Type*} [TopologicalSpace M''] [ChartedSpace H'' M''] [SmoothManifoldWithCorners 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] {F' : Type*} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {G' : Type*} [TopologicalSpace G'] (J' : ModelWithCorners 𝕜 F' G') {N' : Type*} [TopologicalSpace N'] [ChartedSpace G' N'] [SmoothManifoldWithCorners J' N'] @@ -415,6 +415,9 @@ theorem SmoothAt.clm_comp_inTangentCoordinates {f : N → M} {g : N → M'} {h : variable (I') +variable [SmoothManifoldWithCorners J N] + +omit [SmoothManifoldWithCorners J' N'] in theorem SmoothAt.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 : SmoothAt J' ((I'.prod J).prod 𝓘(𝕜, E' →L[𝕜] F)) (fun x ↦ OneJetBundle.mk _ _ (h x)) x₀) @@ -424,6 +427,7 @@ theorem SmoothAt.oneJet_comp {f1 : N' → M} (f2 : N' → M') {f3 : N' → N} {x rw [smoothAt_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 theorem Smooth.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 : Smooth J' ((I'.prod J).prod 𝓘(𝕜, E' →L[𝕜] F)) fun x ↦ OneJetBundle.mk _ _ (h x)) @@ -435,6 +439,7 @@ theorem Smooth.oneJet_comp {f1 : N' → M} (f2 : N' → M') {f3 : N' → N} variable {I'} open Trivialization in +omit [SmoothManifoldWithCorners J N] in theorem Smooth.oneJet_add {f : N → M} {g : N → M'} {ϕ ϕ' : ∀ x : N, OneJetSpace I I' (f x, g x)} (hϕ : Smooth J ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) fun x ↦ OneJetBundle.mk _ _ (ϕ x)) (hϕ' : Smooth J ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) fun x ↦ OneJetBundle.mk _ _ (ϕ' x)) : diff --git a/SphereEversion/Global/OneJetSec.lean b/SphereEversion/Global/OneJetSec.lean index ddf994f2..188ec688 100644 --- a/SphereEversion/Global/OneJetSec.lean +++ b/SphereEversion/Global/OneJetSec.lean @@ -161,7 +161,7 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type*} [Top [TopologicalSpace M'] [ChartedSpace H' M'] [SmoothManifoldWithCorners 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]-/ {F' : Type*} [NormedAddCommGroup F'] [NormedSpace ℝ F'] + {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*} [NormedAddCommGroup EP] [NormedSpace ℝ EP] {HP : Type*} [TopologicalSpace HP] diff --git a/SphereEversion/Global/Relation.lean b/SphereEversion/Global/Relation.lean index e543599b..43baaa22 100644 --- a/SphereEversion/Global/Relation.lean +++ b/SphereEversion/Global/Relation.lean @@ -40,13 +40,13 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] (M' : Type*) [TopologicalSpace M'] [ChartedSpace H' M'] [SmoothManifoldWithCorners 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] {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*} [NormedAddCommGroup EP] [NormedSpace ℝ EP] {HP : Type*} [TopologicalSpace HP] (IP : ModelWithCorners ℝ EP HP) - (P : Type*) [TopologicalSpace P] [ChartedSpace HP P] [SmoothManifoldWithCorners IP P] + (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 diff --git a/SphereEversion/Global/SmoothEmbedding.lean b/SphereEversion/Global/SmoothEmbedding.lean index ce784cf9..8cb29f56 100644 --- a/SphereEversion/Global/SmoothEmbedding.lean +++ b/SphereEversion/Global/SmoothEmbedding.lean @@ -17,10 +17,9 @@ section General 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]-/ {E' : Type*} - [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type*} [TopologicalSpace H'] + [TopologicalSpace M] [ChartedSpace H 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'] structure OpenSmoothEmbedding where toFun : M → M' @@ -376,14 +375,13 @@ variable {𝕜 EX EM EY EN EM' X M Y N M' : Type*} [NontriviallyNormedField 𝕜 {HM : Type*} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} {HM' : Type*} [TopologicalSpace HM'] {IM' : ModelWithCorners 𝕜 EM' HM'} {HN : Type*} [TopologicalSpace HN] {IN : ModelWithCorners 𝕜 EN HN} - [TopologicalSpace X] [ChartedSpace HX X] --[SmoothManifoldWithCorners IX X] - [TopologicalSpace M] [ChartedSpace HM M] --[SmoothManifoldWithCorners IM M] + [TopologicalSpace X] [ChartedSpace HX X] + [TopologicalSpace M] [ChartedSpace HM M] [TopologicalSpace M'] [ChartedSpace HM' M'] section NonMetric -variable [TopologicalSpace Y] [ChartedSpace HY Y] --[SmoothManifoldWithCorners IY Y] - [TopologicalSpace N] [ChartedSpace HN N] --[SmoothManifoldWithCorners IN N] +variable [TopologicalSpace Y] [ChartedSpace HY Y] [TopologicalSpace N] [ChartedSpace HN N] (φ : OpenSmoothEmbedding IX X IM M) (ψ : OpenSmoothEmbedding IY Y IN N) (f : M → N) (g : X → Y) section @@ -445,11 +443,10 @@ end NonMetric section Metric -variable [MetricSpace Y] [ChartedSpace HY Y] /- [SmoothManifoldWithCorners IY Y]-/ [MetricSpace N] - [ChartedSpace HN N] /-[SmoothManifoldWithCorners IN N]-/ (φ : OpenSmoothEmbedding IX X IM M) +variable [MetricSpace Y] [ChartedSpace HY Y] [MetricSpace N] [ChartedSpace HN N] + (φ : OpenSmoothEmbedding IX X IM M) (ψ : OpenSmoothEmbedding IY Y IN N) (f : M → N) (g : X → Y) - /-- This is `lem:dist_updating` in the blueprint. -/ theorem dist_update [ProperSpace Y] {K : Set X} (hK : IsCompact K) {P : Type*} [MetricSpace P] {KP : Set P} (hKP : IsCompact KP) (f : P → M → N) (hf : Continuous ↿f) diff --git a/SphereEversion/Global/TwistOneJetSec.lean b/SphereEversion/Global/TwistOneJetSec.lean index 8c9522e6..f6e1d656 100644 --- a/SphereEversion/Global/TwistOneJetSec.lean +++ b/SphereEversion/Global/TwistOneJetSec.lean @@ -21,7 +21,7 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type u} [NormedAddCo [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners 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]-/ (V : Type*) [NormedAddCommGroup V] [NormedSpace 𝕜 V] + (V : Type*) [NormedAddCommGroup V] [NormedSpace 𝕜 V] (V' : Type*) [NormedAddCommGroup V'] [NormedSpace 𝕜 V'] section Smoothness @@ -178,7 +178,7 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type*} [Top [SmoothManifoldWithCorners 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] /-[SmoothManifoldWithCorners J N]-/ + [TopologicalSpace N] [ChartedSpace G N] /-- A section of a 1-jet bundle seen as a bundle over the source manifold. -/ @[ext] diff --git a/SphereEversion/Local/SphereEversion.lean b/SphereEversion/Local/SphereEversion.lean index 7637ab47..afabe9b8 100644 --- a/SphereEversion/Local/SphereEversion.lean +++ b/SphereEversion/Local/SphereEversion.lean @@ -199,7 +199,7 @@ theorem loc_immersion_rel_ample (n : ℕ) [Fact (dim E = n + 1)] (h : finrank refine ⟨(p.π <| pr[x]ᗮ u)⁻¹ • (pr[x]ᗮ u : E), (ℝ ∙ x)ᗮ.smul_mem _ (pr[x]ᗮ u).2, ?_, ?_⟩ · rw [← orthogonal_span_toDual_symm p.π, span_singleton_smul_eq ne_z'.isUnit] exact (orthogonal_line_inf_sup_line u x).symm - rw [p.π.map_smul, smul_eq_mul, inv_mul_cancel ne_z] + rw [p.π.map_smul, smul_eq_mul, inv_mul_cancel₀ ne_z] let p' : DualPair E := { π := p.π v := v' diff --git a/SphereEversion/Loops/DeltaMollifier.lean b/SphereEversion/Loops/DeltaMollifier.lean index 41883e21..76463711 100644 --- a/SphereEversion/Loops/DeltaMollifier.lean +++ b/SphereEversion/Loops/DeltaMollifier.lean @@ -32,9 +32,7 @@ noncomputable section open Set Function MeasureTheory.MeasureSpace ContinuousLinearMap open scoped Topology Filter Convolution -variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] - [MeasurableSpace F] [BorelSpace F] - +variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] section /-! ## Bump family @@ -152,8 +150,6 @@ theorem periodize_smul_periodic (f : ℝ → ℝ) {g : ℝ → E} (hg : Periodic open MeasureTheory -variable [CompleteSpace E] - theorem integral_periodize (f : ℝ → E) {a : ℝ} (hf : support f ⊆ Ioc a (a + 1)) : ∫ t in a..a + 1, periodize f t = ∫ t in a..a + 1, f t := by apply intervalIntegral.integral_congr_ae diff --git a/SphereEversion/Loops/Exists.lean b/SphereEversion/Loops/Exists.lean index 371596fd..9ea3b40b 100644 --- a/SphereEversion/Loops/Exists.lean +++ b/SphereEversion/Loops/Exists.lean @@ -231,8 +231,6 @@ theorem exist_loops_aux2 [FiniteDimensional ℝ E] (hK : IsCompact K) (hΩ_op : variable (g b Ω U K) -variable [MeasurableSpace F] [BorelSpace F] - /-- A "nice" family of loops consists of all the properties we want from the `exist_loops` lemma: it is a smooth homotopy in `Ω` with fixed endpoints from the constant loop at `b x` to a loop with average `g x` that is also constantly `b x` near `K`. diff --git a/SphereEversion/Loops/Reparametrization.lean b/SphereEversion/Loops/Reparametrization.lean index 623e6fc9..5d8054c5 100644 --- a/SphereEversion/Loops/Reparametrization.lean +++ b/SphereEversion/Loops/Reparametrization.lean @@ -50,9 +50,7 @@ noncomputable section open Set Function MeasureTheory intervalIntegral Filter open scoped Topology Manifold -variable {E F : Type*} - [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] - [MeasurableSpace F] [BorelSpace F] +variable {E F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] set_option hygiene false notation "ι" => Fin (FiniteDimensional.finrank ℝ F + 1) @@ -60,7 +58,7 @@ set_option hygiene true section MetricSpace -variable [MetricSpace E] [LocallyCompactSpace E] +variable [MetricSpace E] [FiniteDimensional ℝ F] theorem Loop.tendsto_mollify_apply (γ : E → Loop F) (h : Continuous ↿γ) (x : E) (t : ℝ) : Tendsto (fun z : E × ℕ ↦ (γ z.1).mollify z.2 t) (𝓝 x ×ˢ atTop) (𝓝 (γ x t)) := by @@ -86,7 +84,7 @@ theorem Loop.tendsto_mollify_apply (γ : E → Loop F) (h : Continuous ↿γ) (x end MetricSpace -variable [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] +variable [NormedAddCommGroup E] [NormedSpace ℝ E] /-- Given a smooth function `g : E → F` between normed vector spaces, a smooth surrounding family is a smooth family of loops `E → loop F`, `x ↦ γₓ` such that `γₓ` surrounds `g x` for all `x`. -/ @@ -132,6 +130,7 @@ theorem surroundPtsPointsWeightsAt : def approxSurroundingPointsAt (n : ℕ) (i : ι) : F := (γ y).mollify n (γ.surroundingParametersAt x i) +variable [FiniteDimensional ℝ E] [CompleteSpace F] in theorem approxSurroundingPointsAt_smooth (n : ℕ) : 𝒞 ∞ fun y ↦ γ.approxSurroundingPointsAt x y n := by refine contDiff_pi.mpr fun i ↦ ?_ @@ -139,6 +138,8 @@ theorem approxSurroundingPointsAt_smooth (n : ℕ) : apply contDiff_parametric_integral_of_contDiff exact ContDiff.smul deltaMollifier_smooth.snd' γ.smooth +variable [FiniteDimensional ℝ F] + /-- The key property from which it should be easy to construct `localCenteringDensity`, `localCenteringDensityNhd` etc below. -/ theorem eventually_exists_surroundingPts_approxSurroundingPointsAt : @@ -250,6 +251,7 @@ theorem localCenteringDensity_pos (hy : y ∈ γ.localCenteringDensityNhd x) (t theorem localCenteringDensity_periodic : Periodic (γ.localCenteringDensity x y) 1 := Finset.univ.periodic_sum fun _ _ ↦ Periodic.smul deltaMollifier_periodic _ +variable [FiniteDimensional ℝ E] in theorem localCenteringDensity_smooth_on : smooth_on ↿(γ.localCenteringDensity x) <| γ.localCenteringDensityNhd x ×ˢ (univ : Set ℝ) := by let h₀ (yt : E × ℝ) (_ : yt ∈ γ.localCenteringDensityNhd x ×ˢ (univ : Set ℝ)) := @@ -275,6 +277,7 @@ theorem localCenteringDensity_smooth_on : simp [z, γ.approxSurroundingPointsAt_mem_affineBases x y hy] · exact deltaMollifier_smooth.comp contDiff_snd +variable [FiniteDimensional ℝ E] in theorem localCenteringDensity_continuous (hy : y ∈ γ.localCenteringDensityNhd x) : Continuous fun t ↦ γ.localCenteringDensity x y t := by refine continuous_iff_continuousAt.mpr fun t ↦ ?_ @@ -332,6 +335,7 @@ structure IsCenteringDensity (x : E) (f : ℝ → ℝ) : Prop where average : ∫ s in (0 : ℝ)..1, f s • γ x s = g x Continuous : Continuous f +omit [FiniteDimensional ℝ F] [DecidablePred fun x ↦ x ∈ affineBases ι ℝ F] in -- Can drop if/when have `intervalIntegrable.smul_continuous_on` theorem isCenteringDensity_convex (x : E) : Convex ℝ { f | γ.IsCenteringDensity x f } := by classical @@ -359,6 +363,8 @@ theorem isCenteringDensity_convex (x : E) : Convex ℝ { f | γ.IsCenteringDensi simp [intervalIntegral.integral_smul, ← add_smul, hf₄, hk₄, hab] Continuous := Continuous.add (hf₅.const_smul a) (hk₅.const_smul b) } +variable [FiniteDimensional ℝ E] + theorem exists_smooth_isCenteringDensity (x : E) : ∃ U ∈ 𝓝 x, ∃ f : E → ℝ → ℝ, diff --git a/SphereEversion/Loops/Surrounding.lean b/SphereEversion/Loops/Surrounding.lean index 8353f651..2d94099c 100644 --- a/SphereEversion/Loops/Surrounding.lean +++ b/SphereEversion/Loops/Surrounding.lean @@ -4,6 +4,7 @@ import SphereEversion.ToMathlib.Analysis.Normed.Module.FiniteDimension import SphereEversion.ToMathlib.ExistsOfConvex import SphereEversion.ToMathlib.SmoothBarycentric import SphereEversion.ToMathlib.Topology.Path +import Mathlib.Analysis.Convex.Caratheodory /-! # Surrounding families of loops @@ -172,11 +173,11 @@ theorem surrounded_iff_mem_interior_convexHull_aff_basis [FiniteDimensional ℝ theorem surrounded_of_convexHull [FiniteDimensional ℝ F] {f : F} {s : Set F} (hs : IsOpen s) (hsf : f ∈ convexHull ℝ s) : Surrounded f s := by rw [surrounded_iff_mem_interior_convexHull_aff_basis] - sorry /- TODO fix! old proof was; type mismatch on `hsf` now - obtain ⟨t, hts, hai, hf⟩ := - (by simpa only [exists_prop, mem_iUnion] using convexHull_eq_union.subst hsf : - ∃ t : Finset F, - (t : Set F) ⊆ s ∧ AffineIndependent ℝ ((↑) : t → F) ∧ f ∈ convexHull ℝ (t : Set F)) + obtain ⟨t, hts, hai, hf⟩ : + ∃ t : Finset F, + (t : Set F) ⊆ s ∧ AffineIndependent ℝ ((↑) : t → F) ∧ f ∈ convexHull ℝ (t : Set F) := by + simp_rw [← exists_prop, ← mem_iUnion, ← convexHull_eq_union] + exact hsf have htne : (t : Set F).Nonempty := convexHull_nonempty_iff.mp ⟨f, hf⟩ obtain ⟨b, hb₁, hb₂, hb₃, hb₄⟩ := hs.exists_between_affineIndependent_span_eq_top hts htne hai have hb₀ : b.Finite := finite_set_of_fin_dim_affineIndependent ℝ hb₃ @@ -189,7 +190,7 @@ theorem surrounded_of_convexHull [FiniteDimensional ℝ F] {f : F} {s : Set F} ( let t : Units ℝ := Units.mk0 ε (by linarith) refine ⟨AffineMap.homothety c (t : ℝ) '' b, hcs, ?_, ?_, hbε (convexHull_mono hb₁ hf)⟩ · rwa [(AffineEquiv.homothetyUnitsMulHom c t).affineIndependent_set_of_eq_iff] - · exact (AffineEquiv.homothetyUnitsMulHom c t).span_eq_top_iff.mp hb₄ -/ + · exact (AffineEquiv.homothetyUnitsMulHom c t).span_eq_top_iff.mp hb₄ /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ -- `lem:smooth_barycentric_coord` diff --git a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Projection.lean b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Projection.lean index 74d80e47..2cb222a4 100644 --- a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Projection.lean +++ b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Projection.lean @@ -72,17 +72,15 @@ theorem LinearIsometryEquiv.apply_ne_zero {E : Type*} [NormedAddCommGroup E] [No variable (u v : E) -variable [CompleteSpace E] in theorem orthogonal_line_inf {u v : E} : {.u}ᗮ ⊓ {.v}ᗮ = {.(pr[v]ᗮ u : E)}ᗮ ⊓ {.v}ᗮ := by rw [inf_orthogonal, inf_orthogonal] refine congr_arg _ (le_antisymm (sup_le ?_ le_sup_right) (sup_le ?_ le_sup_right)) <;> rw [span_singleton_le_iff_mem] - · nth_rw 1 [← orthogonalProjection_add_orthogonalProjection_orthogonal (Δ v) u] + · nth_rw 2 [← orthogonalProjection_add_orthogonalProjection_orthogonal (Δ v) u] exact add_mem (mem_sup_right <| coe_mem _) (mem_sup_left <| mem_span_singleton_self _) · rw [projSpanOrthogonal, orthogonalProjection_orthogonal] exact sub_mem (mem_sup_left <| mem_span_singleton_self _) (mem_sup_right <| coe_mem _) -variable [CompleteSpace E] in theorem orthogonal_line_inf_sup_line (u v : E) : {.u}ᗮ ⊓ {.v}ᗮ ⊔ Δ (pr[v]ᗮ u : E) = {.v}ᗮ := by rw [orthogonal_line_inf, sup_comm, sup_orthogonal_inf_of_completeSpace] rw [span_singleton_le_iff_mem] diff --git a/SphereEversion/ToMathlib/Geometry/Manifold/VectorBundle/Misc.lean b/SphereEversion/ToMathlib/Geometry/Manifold/VectorBundle/Misc.lean index 22163248..53c1b366 100644 --- a/SphereEversion/ToMathlib/Geometry/Manifold/VectorBundle/Misc.lean +++ b/SphereEversion/ToMathlib/Geometry/Manifold/VectorBundle/Misc.lean @@ -89,7 +89,7 @@ end Bundle.Trivial section Hom variable {𝕜₁ : Type*} [NontriviallyNormedField 𝕜₁] {𝕜₂ : Type*} [NontriviallyNormedField 𝕜₂] - (σ : 𝕜₁ →+* 𝕜₂) [iσ : RingHomIsometric σ] + (σ : 𝕜₁ →+* 𝕜₂) variable {B : Type*} [TopologicalSpace B] diff --git a/SphereEversion/ToMathlib/MeasureTheory/ParametricIntervalIntegral.lean b/SphereEversion/ToMathlib/MeasureTheory/ParametricIntervalIntegral.lean index 6889de9a..13bdad5d 100644 --- a/SphereEversion/ToMathlib/MeasureTheory/ParametricIntervalIntegral.lean +++ b/SphereEversion/ToMathlib/MeasureTheory/ParametricIntervalIntegral.lean @@ -169,11 +169,10 @@ theorem hasFDerivAt_parametric_primitive_of_contDiff' {F : H → ℝ → E} (hF use K intro t t_in rw [show (fun x : H ↦ F x t) = uncurry F ∘ fun x : H ↦ (x, t) by ext; simp, ← mul_one K] - sorry /- TODO: return to this; old proof was - apply hK.comp ((LipschitzWith.prod_mk_right t).lipschitzOnWith <| ball x₀ 1) + apply hK.comp (LipschitzWith.prod_mk_right t).lipschitzOnWith rw [mapsTo'] rintro ⟨x, s⟩ ⟨x', hx, h⟩; cases h - exact ⟨ball_subset_closedBall hx, mem_Icc_of_Ioo t_in⟩ -/ + exact ⟨ball_subset_closedBall hx, mem_Icc_of_Ioo t_in⟩ have cont_x (x) : Continuous (F x) := hF.continuous.comp (Continuous.Prod.mk x) have int_Icc (x) : IntegrableOn (F x) (Icc a₀ b₀) := (cont_x x).continuousOn.integrableOn_Icc have int_Ioo (x) : IntegrableOn (F x) (Ioo a₀ b₀) := (int_Icc x).mono_set Ioo_subset_Icc_self From a732393dc94cf0f7a2d5ff97b89d2bf855ae1837 Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Fri, 4 Oct 2024 14:36:51 +0200 Subject: [PATCH 3/6] Bump further --- SphereEversion/Global/OneJetBundle.lean | 3 ++- SphereEversion/Global/OneJetSec.lean | 2 +- SphereEversion/InductiveConstructions.lean | 2 +- SphereEversion/Local/SphereEversion.lean | 4 ++-- SphereEversion/Loops/Basic.lean | 3 ++- SphereEversion/Loops/Surrounding.lean | 6 +++--- .../ToMathlib/Analysis/Calculus.lean | 3 ++- .../InnerProductSpace/Projection.lean | 2 +- SphereEversion/ToMathlib/Topology/Misc.lean | 2 +- lake-manifest.json | 20 ++++++++++++++----- lakefile.toml | 1 + lean-toolchain | 2 +- 12 files changed, 32 insertions(+), 18 deletions(-) diff --git a/SphereEversion/Global/OneJetBundle.lean b/SphereEversion/Global/OneJetBundle.lean index 85ce25c3..7c3be92c 100644 --- a/SphereEversion/Global/OneJetBundle.lean +++ b/SphereEversion/Global/OneJetBundle.lean @@ -316,7 +316,8 @@ theorem oneJetBundle_chart_target (x₀ : J¹MM') : (Prod.map (chartAt H m).symm (chartAt H' m').symm) ∘ Prod.fst := by ext x <;> rfl rw [this, preimage_comp, preimage_prod_map_prod] - mono + simp only [Prod.range_fst, subset_univ, preimage_subset_preimage_iff] + gcongr · exact (chartAt H m).target_subset_preimage_source · exact (chartAt H' m').target_subset_preimage_source diff --git a/SphereEversion/Global/OneJetSec.lean b/SphereEversion/Global/OneJetSec.lean index 188ec688..c7d850a2 100644 --- a/SphereEversion/Global/OneJetSec.lean +++ b/SphereEversion/Global/OneJetSec.lean @@ -104,7 +104,7 @@ its base map at x. -/ theorem isHolonomicAt_iff {F : OneJetSec I M I' M'} {x : M} : F.IsHolonomicAt x ↔ oneJetExt I I' F.bs x = F x := by simp_rw [IsHolonomicAt, oneJetExt, Bundle.TotalSpace.ext_iff, heq_iff_eq, F.fst_eq, - oneJetBundle_mk_fst, true_and_iff, oneJetBundle_mk_snd] + oneJetBundle_mk_fst, true_and, oneJetBundle_mk_snd] theorem isHolonomicAt_congr {F F' : OneJetSec I M I' M'} {x : M} (h : F =ᶠ[𝓝 x] F') : F.IsHolonomicAt x ↔ F'.IsHolonomicAt x := by diff --git a/SphereEversion/InductiveConstructions.lean b/SphereEversion/InductiveConstructions.lean index f16348e9..6af55031 100644 --- a/SphereEversion/InductiveConstructions.lean +++ b/SphereEversion/InductiveConstructions.lean @@ -133,7 +133,7 @@ theorem inductive_construction_of_loc' {X Y : Type*} [EMetricSpace X] [LocallyCo have := inductive_construction (fun x φ ↦ P₀ x φ ∧ P₀' x φ) (fun j : 𝓘 0 ↦ RestrictGermPredicate P₁ (K j)) (fun _ _ ↦ True) U_loc ⟨f₀, hP₀f₀, trivial⟩ - simp only [IndexType.not_isMax, not_false_iff, forall_true_left, true_and_iff] at this + simp only [IndexType.not_isMax, not_false_iff, forall_true_left, true_and] at this rcases this ind' with ⟨f, h, h'⟩ refine ⟨f, fun x ↦ ⟨(h x).1, (h x).2, ?_⟩⟩ rcases mem_iUnion.mp (hK trivial : x ∈ ⋃ j, K j) with ⟨j, hj⟩ diff --git a/SphereEversion/Local/SphereEversion.lean b/SphereEversion/Local/SphereEversion.lean index afabe9b8..ee8f8bde 100644 --- a/SphereEversion/Local/SphereEversion.lean +++ b/SphereEversion/Local/SphereEversion.lean @@ -232,12 +232,12 @@ theorem loc_immersion_rel_ample (n : ℕ) [Fact (dim E = n + 1)] (h : finrank 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, - ContinuousLinearMap.coe_comp', coe_subtypeL', Submodule.coeSubtype, comp_apply, coe_mk] + 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 ext z simp only [mem_map, LinearMap.mem_ker, ContinuousLinearMap.coe_comp', coe_subtypeL', - Submodule.coeSubtype, comp_apply, mem_inf] + Submodule.coe_subtype, comp_apply, mem_inf] constructor · rintro ⟨t, ht, rfl⟩ exact ⟨ht, t.2⟩ diff --git a/SphereEversion/Loops/Basic.lean b/SphereEversion/Loops/Basic.lean index 92489fd5..fd4bbedc 100644 --- a/SphereEversion/Loops/Basic.lean +++ b/SphereEversion/Loops/Basic.lean @@ -323,7 +323,8 @@ theorem isConst_iff_const_avg [CompleteSpace F] {γ : Loop F} : γ.IsConst ↔ omit [NormedAddCommGroup F] [NormedSpace ℝ F] in theorem isConst_of_not_mem_support {γ : X → Loop F} {x : X} (hx : x ∉ support γ) : (γ x).IsConst := by - classical exact Decidable.by_contradiction fun H ↦ hx (subset_closure H) + by_contra H + exact hx (subset_closure H) theorem continuous_average {E : Type*} [TopologicalSpace E] [FirstCountableTopology E] [LocallyCompactSpace E] {γ : E → Loop F} (hγ_cont : Continuous ↿γ) : diff --git a/SphereEversion/Loops/Surrounding.lean b/SphereEversion/Loops/Surrounding.lean index 2d94099c..91d656c6 100644 --- a/SphereEversion/Loops/Surrounding.lean +++ b/SphereEversion/Loops/Surrounding.lean @@ -70,7 +70,7 @@ theorem mem_range_pathThrough' (hF : IsPathConnected F) {m : ℕ} {p : Fin (m + (hp : ∀ i, p i ∈ F) {i n : ℕ} (h : i ≤ n) : p i ∈ range (hF.pathThrough hp n) := by induction' h with n _ ih · exact ⟨1, by simp⟩ - · simp only [pathThrough, Path.trans_range, mem_union, ih, true_or_iff] + · simp only [pathThrough, Path.trans_range, mem_union, ih, true_or] theorem mem_range_pathThrough (hF : IsPathConnected F) {m : ℕ} {p : Fin (m + 1) → X} (hp : ∀ i, p i ∈ F) {i : Fin (m + 1)} : p i ∈ range (hF.pathThrough hp m) := by @@ -426,14 +426,14 @@ theorem surroundingLoop_mem (t s : ℝ) : surroundingLoop O_conn hp hb t s ∈ O cast_coe] refine Subset.trans (truncate_range _) ?_ simp only [trans_range, union_subset_iff, O_conn.range_somePath_subset, - O_conn.range_pathThrough_subset, true_and_iff] + O_conn.range_pathThrough_subset, true_and] theorem surroundingLoop_surrounds {f : F} {w : Fin (d + 1) → ℝ} (h : SurroundingPts f p w) : (surroundingLoop O_conn hp hb 1).Surrounds f := by rw [Loop.surrounds_iff_range_subset_range] refine ⟨p, w, h, ?_⟩ simp only [surroundingLoop, Loop.roundTripFamily_one, Loop.roundTrip_range, trans_range, - range_subset_iff, mem_union, O_conn.mem_range_pathThrough, or_true_iff, forall_true_iff] + range_subset_iff, mem_union, O_conn.mem_range_pathThrough, or_true, forall_true_iff] theorem surroundingLoop_projI (t : ℝ) : surroundingLoop O_conn hp hb (projI t) = surroundingLoop O_conn hp hb t := diff --git a/SphereEversion/ToMathlib/Analysis/Calculus.lean b/SphereEversion/ToMathlib/Analysis/Calculus.lean index 4e17cfd7..ee761a78 100644 --- a/SphereEversion/ToMathlib/Analysis/Calculus.lean +++ b/SphereEversion/ToMathlib/Analysis/Calculus.lean @@ -32,7 +32,8 @@ theorem ContDiffAt.comp₂ {g : E₁ × E₂ → G} {f₁ : F → E₁} {f₂ : theorem ContDiffAt.clm_comp {g : E' → F →L[𝕜] G} {f : E' → E →L[𝕜] F} {n : ℕ∞} {x : E'} (hg : ContDiffAt 𝕜 n g x) (hf : ContDiffAt 𝕜 n f x) : ContDiffAt 𝕜 n (fun x ↦ g x ∘L f x) x := - isBoundedBilinearMap_comp.contDiff.contDiffAt.comp₂ hg hf + isBoundedBilinearMap_comp.contDiff.contDiffAt.comp₂ + (g := fun p => ContinuousLinearMap.comp p.1 p.2) hg hf theorem fderiv_prod_left {x₀ : E} {y₀ : F} : fderiv 𝕜 (fun x ↦ (x, y₀)) x₀ = ContinuousLinearMap.inl 𝕜 E F := diff --git a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Projection.lean b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Projection.lean index 2cb222a4..6e13988c 100644 --- a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Projection.lean +++ b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Projection.lean @@ -241,7 +241,7 @@ theorem continuousAt_orthogonalProjection_orthogonal {x₀ : E} (hx₀ : x₀ ∃ δ > 0, ∀ y, ‖y - x₀‖ ≤ δ → ∀ x, ‖(⟪x₀, x⟫ / ⟪x₀, x₀⟫) • x₀ - (⟪y, x⟫ / ⟪y, y⟫) • y‖ ≤ ε * ‖x‖ by simpa only [ContinuousLinearMap.opNorm_le_iff (le_of_lt ε_pos), orthogonalProjection_orthogonal_singleton, ContinuousLinearMap.coe_sub', - ContinuousLinearMap.coe_comp', coe_subtypeL', Submodule.coeSubtype, Pi.sub_apply, comp_apply, + ContinuousLinearMap.coe_comp', coe_subtypeL', Submodule.coe_subtype, Pi.sub_apply, comp_apply, coe_mk, sub_sub_sub_cancel_left] let N : E → E := fun x ↦ ⟪x, x⟫⁻¹ • x have hNx₀ : 0 < ‖N x₀‖ := by diff --git a/SphereEversion/ToMathlib/Topology/Misc.lean b/SphereEversion/ToMathlib/Topology/Misc.lean index 70561500..ec871a17 100644 --- a/SphereEversion/ToMathlib/Topology/Misc.lean +++ b/SphereEversion/ToMathlib/Topology/Misc.lean @@ -282,7 +282,7 @@ theorem projI_le_iff : projI x ≤ c ↔ 0 ≤ c ∧ (1 ≤ c ∨ x ≤ c) := by @[simp] theorem projI_eq_min : projI x = min 1 x ↔ 0 ≤ x := by - simp_rw [projI_def, max_eq_right_iff, le_min_iff, zero_le_one, true_and_iff] + simp_rw [projI_def, max_eq_right_iff, le_min_iff, zero_le_one, true_and] theorem min_projI (h2 : 0 ≤ c) : min c (projI x) = projI (min c x) := by cases' le_total c x with h3 h3 <;> simp [h2, h3, projI_le_iff, projI_eq_min.mpr] diff --git a/lake-manifest.json b/lake-manifest.json index 29aa81d2..3641ac6a 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "8feac540abb781cb1349688c816dc02fae66b49c", + "rev": "4756e0fc48acce0cc808df0ad149de5973240df6", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "e291aa4de57079b3d2199b9eb7b4b00922b85a7c", + "rev": "28fa80508edc97d96ed6342c9a771a67189e0baa", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -55,20 +55,30 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "3e96ea03edd48b932566ca9b201285ae2d57130d", + "rev": "e285a7ade149c551c17a4b24f127e1ef782e4bb1", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "2ba60fa2c384a94735454db11a2d523612eaabff", + "name": "LeanSearchClient", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/mathlib4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "df80b0dd2548c76fbdc3fe5d3a96873dfd46c0dc", + "rev": "809c3fb3b5c8f5d7dace56e200b426187516535a", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "v4.12.0", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/PatrickMassot/checkdecls.git", diff --git a/lakefile.toml b/lakefile.toml index 4a9fc788..aa9715b1 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -9,6 +9,7 @@ relaxedAutoImplicit = false [[require]] name = "mathlib" scope = "leanprover-community" +rev = "v4.12.0" [[require]] name = "checkdecls" diff --git a/lean-toolchain b/lean-toolchain index 98556ba0..89985206 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.12.0-rc1 +leanprover/lean4:v4.12.0 From a7c12590736ea78ea396ce1e465255231bd26528 Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Sat, 5 Oct 2024 18:40:23 +0200 Subject: [PATCH 4/6] Remove gcongr annotations that are already in mathlib --- SphereEversion/Global/OneJetBundle.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/SphereEversion/Global/OneJetBundle.lean b/SphereEversion/Global/OneJetBundle.lean index 7c3be92c..5975bf0d 100644 --- a/SphereEversion/Global/OneJetBundle.lean +++ b/SphereEversion/Global/OneJetBundle.lean @@ -294,8 +294,6 @@ lemma ContMDiffMap.snd_apply (x : M) (x' : M') : end -attribute [gcongr] preimage_mono Set.prod_mono - /-- In `J¹(M, M')`, the target of a chart has a nice formula -/ theorem oneJetBundle_chart_target (x₀ : J¹MM') : (chartAt HJ x₀).target = Prod.fst ⁻¹' (chartAt (ModelProd H H') x₀.proj).target := by From 3d99d1bb95a75f7278ae2b51a8795dce8304b6af Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Sat, 5 Oct 2024 18:44:23 +0200 Subject: [PATCH 5/6] Implicit arguments for improveStep_of_support --- SphereEversion/Local/HPrinciple.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/SphereEversion/Local/HPrinciple.lean b/SphereEversion/Local/HPrinciple.lean index ee431086..86fe07c2 100644 --- a/SphereEversion/Local/HPrinciple.lean +++ b/SphereEversion/Local/HPrinciple.lean @@ -261,7 +261,8 @@ theorem improveStep_apply_φ (t : ℝ) (x : E) : (smoothStep t * L.ρ x) • corrugation.remainder L.p.π N (L.loop h 1) x := rfl -theorem improveStep_of_support (t : ℝ) {x : E} (H : ∀ t, x ∉ Loop.support (L.loop h t)) : +variable {h N} in +theorem improveStep_of_support {t : ℝ} {x : E} (H : ∀ t, x ∉ Loop.support (L.loop h t)) : L.improveStep h N t x = 𝓕 x := by have : ∀ t s, L.loop h t x s = 𝓕.φ x L.v := by intro t s @@ -298,7 +299,7 @@ theorem improveStep_rel_K : ∀ᶠ x near L.K, ∀ t, L.improveStep h N t x = exact Loop.isConst_of_eq (hy t) apply this.mono intro x hx t - exact improveStep_of_support _ _ _ hx + exact improveStep_of_support hx theorem improveStep_rel_C : ∀ᶠ x near L.C, ∀ t, L.improveStep h N t x = 𝓕 x := by apply Eventually.filter_mono (L.hK₁.isClosed.nhdsSet_le_sup' L.C) From 5e6aeb0d8b9516631e05faddc7c723f8fe76c48f Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Mon, 7 Oct 2024 14:44:24 +0200 Subject: [PATCH 6/6] Restore old proof using mono. --- SphereEversion/Global/OneJetBundle.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/SphereEversion/Global/OneJetBundle.lean b/SphereEversion/Global/OneJetBundle.lean index 5975bf0d..1a816c64 100644 --- a/SphereEversion/Global/OneJetBundle.lean +++ b/SphereEversion/Global/OneJetBundle.lean @@ -13,6 +13,7 @@ import Mathlib.Geometry.Manifold.ContMDiffMFDeriv import SphereEversion.ToMathlib.Geometry.Manifold.VectorBundle.Misc import Mathlib.Geometry.Manifold.VectorBundle.Hom import Mathlib.Geometry.Manifold.VectorBundle.Pullback +import Mathlib.Tactic.Monotonicity.Lemmas /-! # 1-jet bundles @@ -314,8 +315,7 @@ theorem oneJetBundle_chart_target (x₀ : J¹MM') : (Prod.map (chartAt H m).symm (chartAt H' m').symm) ∘ Prod.fst := by ext x <;> rfl rw [this, preimage_comp, preimage_prod_map_prod] - simp only [Prod.range_fst, subset_univ, preimage_subset_preimage_iff] - gcongr + mono · exact (chartAt H m).target_subset_preimage_source · exact (chartAt H' m').target_subset_preimage_source