From 5da707efa4d11399d3dca6ed85aa96156cc71efb Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Mon, 12 Jan 2026 23:35:08 +0100 Subject: [PATCH 1/7] Bump mathlib --- lake-manifest.json | 16 ++++++++-------- lakefile.toml | 1 - 2 files changed, 8 insertions(+), 9 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 73116e3a..92d3cc0a 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,17 +15,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "32d24245c7a12ded17325299fd41d412022cd3fe", + "rev": "c1d772d6329adbf19893119c31cea6c4127420e7", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.27.0-rc1", + "inputRev": "master", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "8d3713f36dda48467eb61f8c1c4db89c49a6251a", + "rev": "b3dd6c3ebc0a71685e86bea9223be39ea4c299fb", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "19e5f5cc9c21199be466ef99489e3acab370f079", + "rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "4eb26e1a4806b200ddfe5179d0c2a0fae56c54a7", + "rev": "cff9dd30f2c161b9efd7c657cafed1f967645890", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "fb12f5535c80e40119286d9575c9393562252d21", + "rev": "fa78cf032194308a950a264ed87b422a2a7c1c6c", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "523ec6fc8062d2f470fdc8de6f822fe89552b5e6", + "rev": "8920dcbb96a4e8bf641fc399ac9c0888e4a6be72", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "6254bed25866358ce4f841fa5a13b77de04ffbc8", + "rev": "5ba0380f2fb45c69448d80429ef6c22bf5973cfa", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lakefile.toml b/lakefile.toml index eb9d9319..a81f4756 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -11,7 +11,6 @@ linter.flexible = true [[require]] name = "mathlib" scope = "leanprover-community" -rev = "v4.27.0-rc1" [[require]] name = "checkdecls" From 1d85ab1304987dcbb394ed1a1f8fa4972314ba64 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Mon, 12 Jan 2026 23:37:33 +0100 Subject: [PATCH 2/7] wip --- SphereEversion.lean | 1 - SphereEversion/Local/OneJet.lean | 4 +- .../ToMathlib/Algebra/Ring/Periodic.lean | 2 +- .../ToMathlib/Analysis/Convex/Basic.lean | 39 +------------------ SphereEversion/ToMathlib/Analysis/CutOff.lean | 2 +- SphereEversion/ToMathlib/Data/Nat/Basic.lean | 1 + SphereEversion/ToMathlib/ExistsOfConvex.lean | 4 +- SphereEversion/ToMathlib/Topology/Misc.lean | 11 +----- .../Topology/Separation/Hausdorff.lean | 12 ------ 9 files changed, 10 insertions(+), 66 deletions(-) delete mode 100644 SphereEversion/ToMathlib/Topology/Separation/Hausdorff.lean diff --git a/SphereEversion.lean b/SphereEversion.lean index cd05b4e7..e0cccddc 100644 --- a/SphereEversion.lean +++ b/SphereEversion.lean @@ -57,5 +57,4 @@ import SphereEversion.ToMathlib.Topology.Algebra.Module import SphereEversion.ToMathlib.Topology.Misc import SphereEversion.ToMathlib.Topology.Paracompact import SphereEversion.ToMathlib.Topology.Path -import SphereEversion.ToMathlib.Topology.Separation.Hausdorff import SphereEversion.ToMathlib.Unused.Fin diff --git a/SphereEversion/Local/OneJet.lean b/SphereEversion/Local/OneJet.lean index d7b372d4..a6cecac8 100644 --- a/SphereEversion/Local/OneJet.lean +++ b/SphereEversion/Local/OneJet.lean @@ -304,7 +304,7 @@ theorem HtpyJetSec.comp_le_0 (𝓕 𝓖 : HtpyJetSec E F) (h) : -- unused -- @[simp] can prove this theorem HtpyJetSec.comp_0 (𝓕 𝓖 : HtpyJetSec E F) (h) : 𝓕.comp 𝓖 h 0 = 𝓕 0 := - (𝓕.comp_le_0 𝓖 h).self_of_nhdsSet 0 right_mem_Iic + (𝓕.comp_le_0 𝓖 h).self_of_nhdsSet 0 self_mem_Iic @[simp] theorem HtpyJetSec.comp_of_not_le (𝓕 𝓖 : HtpyJetSec E F) (h) {t : ℝ} (ht : ¬t ≤ 1 / 2) : @@ -325,6 +325,6 @@ theorem HtpyJetSec.comp_ge_1 (𝓕 𝓖 : HtpyJetSec E F) (h) : ∀ᶠ t near Ic @[simp] theorem HtpyJetSec.comp_1 (𝓕 𝓖 : HtpyJetSec E F) (h) : 𝓕.comp 𝓖 h 1 = 𝓖 1 := - (𝓕.comp_ge_1 𝓖 h).self_of_nhdsSet 1 left_mem_Ici + (𝓕.comp_ge_1 𝓖 h).self_of_nhdsSet 1 self_mem_Iic end HtpyJetSec diff --git a/SphereEversion/ToMathlib/Algebra/Ring/Periodic.lean b/SphereEversion/ToMathlib/Algebra/Ring/Periodic.lean index 5f1dc99d..c15699ee 100644 --- a/SphereEversion/ToMathlib/Algebra/Ring/Periodic.lean +++ b/SphereEversion/ToMathlib/Algebra/Ring/Periodic.lean @@ -1,6 +1,6 @@ import Mathlib.Analysis.Normed.Order.Lattice import Mathlib.Algebra.Ring.Periodic -import SphereEversion.ToMathlib.Topology.Separation.Hausdorff +import Mathlib.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/Convex/Basic.lean b/SphereEversion/ToMathlib/Analysis/Convex/Basic.lean index e6676f6a..703fcfe2 100644 --- a/SphereEversion/ToMathlib/Analysis/Convex/Basic.lean +++ b/SphereEversion/ToMathlib/Analysis/Convex/Basic.lean @@ -4,18 +4,6 @@ import Mathlib.Algebra.Order.Hom.Ring open Function Set --- TODO: move this lemma and the following one -theorem map_finsum {β α γ : Type*} [AddCommMonoid β] [AddCommMonoid γ] - {G : Type*} [FunLike G β γ] [AddMonoidHomClass G β γ] (g : G) - {f : α → β} (hf : (Function.support f).Finite) : - g (∑ᶠ i, f i) = ∑ᶠ i, g (f i) := - (g : β →+ γ).map_finsum hf - -@[to_additive] -theorem finprod_eq_prod_of_mulSupport_subset_of_finite {α M} [CommMonoid M] (f : α → M) {s : Set α} - (h : mulSupport f ⊆ s) (hs : s.Finite) : ∏ᶠ i, f i = ∏ i ∈ hs.toFinset, f i := by - apply finprod_eq_prod_of_mulSupport_subset f; rwa [Set.Finite.coe_toFinset] - section variable {𝕜 𝕜' E E₂ E' : Type*} [Semiring 𝕜] [PartialOrder 𝕜] --[IsOrderedRing 𝕜] @@ -48,29 +36,6 @@ theorem support_finite_of_finsum_eq_of_neZero {M : Type*} {ι : Sort _} [AddComm rw [h] apply NeZero.ne -@[to_additive] -theorem Subsingleton.mulSupport_eq {α β} [Subsingleton β] [One β] (f : α → β) : - mulSupport f = ∅ := by - rw [mulSupport_eq_empty_iff]; apply Subsingleton.elim - -theorem support_finite_of_finsum_eq_one {M : Type*} {ι : Sort _} [NonAssocSemiring M] {f : ι → M} - (h : ∑ᶠ i, f i = 1) : (support f).Finite := by - cases subsingleton_or_nontrivial M - · simp_rw [Subsingleton.support_eq, finite_empty] - exact support_finite_of_finsum_eq_of_neZero h - -theorem finsum_sum_filter {α β M : Type*} [AddCommMonoid M] (f : β → α) (s : Finset β) - [DecidableEq α] (g : β → M) : - ∑ᶠ x : α, ∑ y ∈ Finset.filter (fun j : β ↦ f j = x) s, g y = ∑ k ∈ s, g k := by - rw [finsum_eq_finset_sum_of_support_subset] - · rw [Finset.sum_image'] - exact fun _ _ ↦ rfl - · intro x hx - rw [mem_support] at hx - obtain ⟨a, h, -⟩ := Finset.exists_ne_zero_of_sum_ne_zero hx - simp only [Finset.mem_filter, Finset.coe_image, mem_image, SetLike.mem_coe] at h ⊢ - exact ⟨a, h⟩ - theorem sum_mem_reallyConvexHull [IsOrderedRing 𝕜] {s : Set E} {ι : Type*} {t : Finset ι} {w : ι → 𝕜} {z : ι → E} (h₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : ∑ i ∈ t, w i = 1) (hz : ∀ i ∈ t, z i ∈ s) : @@ -147,7 +112,7 @@ theorem ReallyConvex.finsum_mem [Nontrivial 𝕜] [IsOrderedRing 𝕜] (hs : ReallyConvex 𝕜 s) {ι : Type*} {w : ι → 𝕜} {z : ι → E} (h₀ : ∀ i, 0 ≤ w i) (h₁ : ∑ᶠ i, w i = 1) (hz : ∀ i ∈ support w, z i ∈ s) : ∑ᶠ i, w i • z i ∈ s := by - rw [finsum_eq_sum_of_support_subset_of_finite _ _ (support_finite_of_finsum_eq_one h₁)] + rw [finsum_eq_sum_of_support_subset_of_finite _ _ (finite_support_of_finsum_eq_one h₁)] swap; · exact support_smul_subset_left w z apply hs.sum_mem fun i _ ↦ h₀ i · rw [← finsum_eq_sum, h₁] @@ -181,7 +146,7 @@ theorem ReallyConvex.preimageₛₗ (f : E →ₛₗ[σ.toRingHom] E') {s : Set · simp_rw [preimage_empty, reallyConvex_empty] · simp_rw [preimage_univ, reallyConvex_univ] · refine Or.inr fun w hw h2w h3w ↦ ?_ - have h4w : (support w).Finite := support_finite_of_finsum_eq_one h3w + have h4w : (support w).Finite := finite_support_of_finsum_eq_one h3w have : (support fun x ↦ w x • x).Finite := h4w.subset (support_smul_subset_left w id) simp_rw [mem_preimage, map_finsum f this, map_smulₛₗ f] apply hs.finsum_mem diff --git a/SphereEversion/ToMathlib/Analysis/CutOff.lean b/SphereEversion/ToMathlib/Analysis/CutOff.lean index c8b80bac..d195cd29 100644 --- a/SphereEversion/ToMathlib/Analysis/CutOff.lean +++ b/SphereEversion/ToMathlib/Analysis/CutOff.lean @@ -10,5 +10,5 @@ theorem exists_contDiff_one_nhds_of_interior {E : Type*} [NormedAddCommGroup 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) ∧ ∀ x, f x ∈ Icc (0 : ℝ) 1 := - let ⟨f, hfs, hft, hf01⟩ := exists_smooth_one_nhds_of_subset_interior 𝓘(ℝ, E) hs hd + let ⟨f, hfs, hft, hf01⟩ := exists_contMDiffMap_one_nhds_of_subset_interior 𝓘(ℝ, E) hs hd ⟨f, f.contMDiff.contDiff, hfs, hft, hf01⟩ diff --git a/SphereEversion/ToMathlib/Data/Nat/Basic.lean b/SphereEversion/ToMathlib/Data/Nat/Basic.lean index d94ced5c..7945d3f8 100644 --- a/SphereEversion/ToMathlib/Data/Nat/Basic.lean +++ b/SphereEversion/ToMathlib/Data/Nat/Basic.lean @@ -1,3 +1,4 @@ +import Mathlib.Data.Nat.Notation import Mathlib.Logic.Function.Basic import Mathlib.Tactic.Choose diff --git a/SphereEversion/ToMathlib/ExistsOfConvex.lean b/SphereEversion/ToMathlib/ExistsOfConvex.lean index 468ab8de..63205e5a 100644 --- a/SphereEversion/ToMathlib/ExistsOfConvex.lean +++ b/SphereEversion/ToMathlib/ExistsOfConvex.lean @@ -58,7 +58,7 @@ theorem reallyConvex_contMDiffAt (x : M) (n : ℕ∞) : classical rw [Nontrivial.reallyConvex_iff] rintro w _w_pos w_supp w_sum - have : (support w).Finite := support_finite_of_finsum_eq_one w_sum + have : (support w).Finite := finite_support_of_finsum_eq_one w_sum set fin_supp := this.toFinset with H have : (support fun i : (𝓝 x).Germ F ↦ w i • i) ⊆ fin_supp := by rw [Set.Finite.coe_toFinset] @@ -121,7 +121,7 @@ theorem reallyConvex_contMDiffAtProd {x : M₁} (n : ℕ∞) : classical rw [Nontrivial.reallyConvex_iff] rintro w _w_pos w_supp w_sum - have : (support w).Finite := support_finite_of_finsum_eq_one w_sum + have : (support w).Finite := finite_support_of_finsum_eq_one w_sum set fin_supp := this.toFinset with H have : (support fun i : (𝓝 x).Germ (M₂ → F) ↦ w i • i) ⊆ fin_supp := by rw [Set.Finite.coe_toFinset] diff --git a/SphereEversion/ToMathlib/Topology/Misc.lean b/SphereEversion/ToMathlib/Topology/Misc.lean index eb742e5b..9e1879cd 100644 --- a/SphereEversion/ToMathlib/Topology/Misc.lean +++ b/SphereEversion/ToMathlib/Topology/Misc.lean @@ -14,15 +14,6 @@ section Maps variable {α β : Type*} {f : α → β} {g : β → α} --- TODO: move to Data.Set.Defs -theorem Function.LeftInverse.mem_preimage_iff (hfg : LeftInverse g f) {s : Set α} {x : α} : - f x ∈ g ⁻¹' s ↔ x ∈ s := by rw [Set.mem_preimage, hfg x] - --- TODO: move to Data.Set.Basic -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) @@ -152,7 +143,7 @@ theorem IsOpen.preimage_fract' {s : Set ℝ} (hs : IsOpen s) (h2s : 0 ∈ s → rcases eq_or_ne (fract x) 0 with (hx' | hx') · have H : (0 : ℝ) ∈ s := by rwa [hx'] at hx specialize h2s H - rcases fract_eq_zero_iff.mp hx' with ⟨n, rfl⟩; clear hx hx' + rcases _root_.fract_eq_zero_iff.mp hx' with ⟨n, rfl⟩; clear hx hx' have s_mem_0 := hs.mem_nhds H rcases(nhds_basis_zero_abs_lt ℝ).mem_iff.mp s_mem_0 with ⟨δ, δ_pos, hδ⟩ rcases(nhdsWithin_hasBasis (nhds_basis_Ioo_pos (1 : ℝ)) _).mem_iff.mp h2s with ⟨ε, ε_pos, hε⟩ diff --git a/SphereEversion/ToMathlib/Topology/Separation/Hausdorff.lean b/SphereEversion/ToMathlib/Topology/Separation/Hausdorff.lean deleted file mode 100644 index 45649697..00000000 --- a/SphereEversion/ToMathlib/Topology/Separation/Hausdorff.lean +++ /dev/null @@ -1,12 +0,0 @@ -import Mathlib.Topology.Separation.Hausdorff - -theorem t2Space_iff_of_isOpenQuotientMap {α β : Type*} [TopologicalSpace α] - [TopologicalSpace β] {π : α → β} (h : IsOpenQuotientMap π) : - T2Space β ↔ IsClosed {q : α × α | π q.1 = π q.2} := by - rw [t2_iff_isClosed_diagonal] - replace h := IsOpenQuotientMap.prodMap h h - constructor <;> intro H - · exact H.preimage h.continuous - · simp_rw [← isOpen_compl_iff] at H ⊢ - convert h.isOpenMap _ H - exact (h.surjective.image_preimage _).symm From 473ad25b0e6be8c5391f6604083289ee96d8b781 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Mon, 12 Jan 2026 23:47:16 +0100 Subject: [PATCH 3/7] Fix errors, related to 1 <= n hypotheses --- SphereEversion/Global/OneJetSec.lean | 8 ++++---- SphereEversion/Global/SmoothEmbedding.lean | 4 ++-- SphereEversion/InductiveConstructions.lean | 2 +- SphereEversion/Loops/Basic.lean | 4 ++-- SphereEversion/ToMathlib/Analysis/Calculus.lean | 11 ++++++----- SphereEversion/ToMathlib/Analysis/ContDiff.lean | 4 ++-- .../MeasureTheory/ParametricIntervalIntegral.lean | 8 ++++---- 7 files changed, 21 insertions(+), 20 deletions(-) diff --git a/SphereEversion/Global/OneJetSec.lean b/SphereEversion/Global/OneJetSec.lean index 6a1aa4c1..a67cad4f 100644 --- a/SphereEversion/Global/OneJetSec.lean +++ b/SphereEversion/Global/OneJetSec.lean @@ -264,7 +264,7 @@ theorem uncurry_ϕ' (S : FamilyOneJetSec I M I' M' IP P) (p : P × M) : congr 1 convert mfderiv_comp p ((S.contMDiff_bs.comp (contMDiff_id.prodMk contMDiff_const)).mdifferentiable - (by simp) p.1) (contMDiff_fst.mdifferentiable le_top p) + (by simp) p.1) (contMDiff_fst.mdifferentiable one_ne_zero p) simp_rw [mfderiv_fst] rfl @@ -272,10 +272,10 @@ 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.contMDiff_bs.mdifferentiableAt (mod_cast le_top)), + simp_rw [mfderiv_prod_eq_add (S.contMDiff_bs.mdifferentiableAt (by simp)), mfderiv_snd, add_right_inj] - erw [mfderiv_comp p (S.contMDiff_coe_bs.mdifferentiableAt (mod_cast le_top)) - (contMDiff_snd.mdifferentiableAt le_top), mfderiv_snd] + erw [mfderiv_comp p (S.contMDiff_coe_bs.mdifferentiableAt (by simp)) + (contMDiff_snd.mdifferentiableAt one_ne_zero), mfderiv_snd] exact (show Surjective (ContinuousLinearMap.snd ℝ EP E) from Prod.snd_surjective).clm_comp_injective.eq_iff diff --git a/SphereEversion/Global/SmoothEmbedding.lean b/SphereEversion/Global/SmoothEmbedding.lean index d922eca1..2608dbe8 100644 --- a/SphereEversion/Global/SmoothEmbedding.lean +++ b/SphereEversion/Global/SmoothEmbedding.lean @@ -89,9 +89,9 @@ variable [IsManifold I ∞ M] [IsManifold I' ∞ M'] 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 (mod_cast le_top)).mdifferentiableAt + (mem_range_self x)).mdifferentiableWithinAt (by simp)).mdifferentiableAt (f.isOpenMap.range_mem_nhds x) - have h₂ : MDifferentiableAt I I' f x := f.contMDiff_to.mdifferentiableAt (mod_cast le_top) + have h₂ : MDifferentiableAt I I' f x := f.contMDiff_to.mdifferentiableAt (by simp) ContinuousLinearEquiv.equivOfInverse (mfderiv% f x) (mfderiv% f.invFun (f x)) (by intro v diff --git a/SphereEversion/InductiveConstructions.lean b/SphereEversion/InductiveConstructions.lean index 2a082307..a36384b2 100644 --- a/SphereEversion/InductiveConstructions.lean +++ b/SphereEversion/InductiveConstructions.lean @@ -326,7 +326,7 @@ theorem inductive_htpy_construction' {X Y : Type*} [TopologicalSpace X] {N : ℕ rcases eq_or_lt_of_le ht with (rfl | ht) · apply Quotient.sound replace hpast_F' : ↿F' =ᶠ[𝓝 (0, x)] fun q : ℝ × X ↦ F (T i.toNat, q.2) := by - have : 𝓝 (0 : ℝ) ≤ 𝓝ˢ (Iic 0) := nhds_le_nhdsSet right_mem_Iic + have : 𝓝 (0 : ℝ) ≤ 𝓝ˢ (Iic 0) := nhds_le_nhdsSet self_mem_Iic apply mem_of_superset (prod_mem_nhds (hpast_F'.filter_mono this) univ_mem) rintro ⟨t', x'⟩ ⟨ht', -⟩ exact (congr_fun ht' x' : _) diff --git a/SphereEversion/Loops/Basic.lean b/SphereEversion/Loops/Basic.lean index f89612ec..aaeb7690 100644 --- a/SphereEversion/Loops/Basic.lean +++ b/SphereEversion/Loops/Basic.lean @@ -411,9 +411,9 @@ theorem Loop.diff_normalize {γ : E → Loop F} (hγ_diff : 𝒞 1 ↿γ) (e : E (Loop.diff γ e).normalize = Loop.diff (fun e ↦ (γ e).normalize) e := by ext t x simp only [Loop.diff_apply, Loop.normalize_apply, partialFDerivFst] - rw [fderiv_fun_sub ((hγ_diff.partial_loop t).differentiable le_rfl).differentiableAt, + rw [fderiv_fun_sub ((hγ_diff.partial_loop t).differentiable (by simp)).differentiableAt, Loop.average_diff hγ_diff] - exact (hγ_diff.loop_average.differentiable le_rfl).differentiableAt + exact (hγ_diff.loop_average.differentiable (by simp)).differentiableAt variable {γ} diff --git a/SphereEversion/ToMathlib/Analysis/Calculus.lean b/SphereEversion/ToMathlib/Analysis/Calculus.lean index afe88d7b..d8c43cd1 100644 --- a/SphereEversion/ToMathlib/Analysis/Calculus.lean +++ b/SphereEversion/ToMathlib/Analysis/Calculus.lean @@ -128,7 +128,7 @@ def partialDerivSnd (φ : E → 𝕜 → G) : E → 𝕜 → G := fun e k ↦ 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 + toSpanSingleton_deriv.symm omit [NormedAddCommGroup F] [NormedSpace 𝕜 F] in @[simp] @@ -139,7 +139,7 @@ theorem partialFDerivFst_one (φ : 𝕜 → F → G) (k : 𝕜) (f : F) : 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 + toSpanSingleton_deriv.symm omit [NormedAddCommGroup E] [NormedSpace 𝕜 E] in theorem partialFDerivSnd_one (φ : E → 𝕜 → G) (e : E) (k : 𝕜) : @@ -203,11 +203,12 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type*} [Nor theorem ContDiff.lipschitzOnWith {s : Set E} {f : E → F} {n} (hf : ContDiff ℝ n f) (hn : 1 ≤ n) (hs : Convex ℝ s) (hs' : IsCompact s) : ∃ K, LipschitzOnWith K f s := by - rcases (bddAbove_iff_exists_ge (0 : ℝ)).mp (hs'.image (hf.continuous_fderiv hn).norm).bddAbove - with ⟨M, M_nonneg, hM⟩ + obtain ⟨M, M_nonneg, hM⟩ := (bddAbove_iff_exists_ge (0 : ℝ)).mp + (hs'.image (hf.continuous_fderiv (by positivity)).norm).bddAbove simp_rw [forall_mem_image] at hM use ⟨M, M_nonneg⟩ - exact Convex.lipschitzOnWith_of_nnnorm_fderiv_le (fun x _ ↦ hf.differentiable hn x) hM hs + exact Convex.lipschitzOnWith_of_nnnorm_fderiv_le + (fun x _ ↦ hf.differentiable (by positivity) x) hM hs end RealCalculus diff --git a/SphereEversion/ToMathlib/Analysis/ContDiff.lean b/SphereEversion/ToMathlib/Analysis/ContDiff.lean index 98332c55..40609931 100644 --- a/SphereEversion/ToMathlib/Analysis/ContDiff.lean +++ b/SphereEversion/ToMathlib/Analysis/ContDiff.lean @@ -164,10 +164,10 @@ theorem contDiff_parametric_symm [CompleteSpace E] [CompleteSpace F] {f : E → rintro ⟨x, y⟩ apply HasFDerivAt.prodMk · simp only [ContinuousLinearEquiv.coe_refl, ContinuousLinearMap.id_comp, hasFDerivAt_fst] - have diff : Differentiable 𝕜 (uncurry fun x y ↦ f x y) := hf.differentiable (mod_cast le_top) + have diff : Differentiable 𝕜 (uncurry fun x y ↦ f x y) := hf.differentiable (by simp) rw [show (fun x : E × F ↦ (f x.fst) x.snd) = uncurry fun x y ↦ f x y by ext; rfl] apply DifferentiableAt.hasFDerivAt_coprod - · exact hf.differentiable (mod_cast le_top) _ + · exact hf.differentiable (by simp) _ · exact diff.differentiableAt.hasFDerivAt_partial_fst · rw [← hf' x y] exact diff.differentiableAt.hasFDerivAt_partial_snd diff --git a/SphereEversion/ToMathlib/MeasureTheory/ParametricIntervalIntegral.lean b/SphereEversion/ToMathlib/MeasureTheory/ParametricIntervalIntegral.lean index 61412637..0c016c9b 100644 --- a/SphereEversion/ToMathlib/MeasureTheory/ParametricIntervalIntegral.lean +++ b/SphereEversion/ToMathlib/MeasureTheory/ParametricIntervalIntegral.lean @@ -181,10 +181,10 @@ theorem hasFDerivAt_parametric_primitive_of_contDiff' {F : H → ℝ → E} (hF NNReal.coe_nonneg K · apply ae_of_all intro t - apply (ContDiff.hasStrictFDerivAt _ le_rfl).hasFDerivAt + apply (ContDiff.hasStrictFDerivAt _ one_ne_zero).hasFDerivAt rw [show (fun x ↦ F x t) = uncurry F ∘ fun x ↦ (x, t) by ext; simp] exact hF.comp ((contDiff_prodMk_left t).of_le le_top) - · exact (ContDiff.hasStrictFDerivAt hs le_rfl).hasFDerivAt + · exact (ContDiff.hasStrictFDerivAt hs (by simp)).hasFDerivAt · rfl · apply Continuous.aestronglyMeasurable have : @@ -193,12 +193,12 @@ theorem hasFDerivAt_parametric_primitive_of_contDiff' {F : H → ℝ → E} (hF (fderiv ℝ <| uncurry F) ∘ fun t ↦ (x₀, t) := by ext t have : HasFDerivAt (fun e ↦ F e t) ((fderiv ℝ (uncurry F) (x₀, t)).comp (inl ℝ H ℝ)) x₀ := - (hF.hasStrictFDerivAt le_rfl).hasFDerivAt.comp _ (hasFDerivAt_prodMk_left _ _) + (hF.hasStrictFDerivAt (by norm_num)).hasFDerivAt.comp _ (hasFDerivAt_prodMk_left _ _) rw [this.fderiv] rfl rw [this] exact (inl ℝ H ℝ).compRightL.continuous.comp - ((hF.continuous_fderiv le_rfl).comp <| Continuous.prodMk_right x₀) + ((hF.continuous_fderiv (by norm_num)).comp <| Continuous.prodMk_right x₀) · simp_rw [ae_restrict_iff' measurableSet_Ioo] filter_upwards with t t_in rw [nnabs_coe K] From dedf48584144b6ec701e44929f5c829291aceee1 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Mon, 12 Jan 2026 23:54:16 +0100 Subject: [PATCH 4/7] More --- .../ToMathlib/MeasureTheory/ParametricIntervalIntegral.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/SphereEversion/ToMathlib/MeasureTheory/ParametricIntervalIntegral.lean b/SphereEversion/ToMathlib/MeasureTheory/ParametricIntervalIntegral.lean index 0c016c9b..ffc4de3b 100644 --- a/SphereEversion/ToMathlib/MeasureTheory/ParametricIntervalIntegral.lean +++ b/SphereEversion/ToMathlib/MeasureTheory/ParametricIntervalIntegral.lean @@ -74,7 +74,8 @@ theorem hasFDerivAt_parametric_primitive_of_lip' (F : H → ℝ → E) (F' : ℝ replace hF_meas : ∀ᶠ x in 𝓝 x₀, AEStronglyMeasurable (F x) (volume.restrict (Ι a (s x₀))) := Eventually.mono (ball_mem_nhds x₀ ε_pos) fun x hx ↦ hF_meas_ball hx ha hsx₀ replace hF_int : IntervalIntegrable (F x₀) volume a (s x₀) := hF_int_ball x₀ x₀_in ha hsx₀ - exact (hasFDerivAt_integral_of_dominated_loc_of_lip_interval ε_pos hF_meas hF_int hF'_meas + exact (hasFDerivAt_integral_of_dominated_loc_of_lip_interval (ball_mem_nhds x₀ ε_pos) + hF_meas hF_int hF'_meas (ae_restrict_of_ae_restrict_of_subset (ordConnected_Ioo.uIoc_subset ha hsx₀) h_lipsch) (bound_int ha hsx₀) h_diff).2 have D₂ : HasFDerivAt (fun x ↦ φ x₀ (s x)) ((toSpanSingleton ℝ (F x₀ (s x₀))).comp s') x₀ := by From 2f694dbb8754866f1f1761e8b9ac8af769f60da0 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Tue, 13 Jan 2026 15:03:37 +0100 Subject: [PATCH 5/7] Fix remaining errors, and minor golfs --- SphereEversion/Global/Relation.lean | 2 +- SphereEversion/Local/Corrugation.lean | 6 ++--- SphereEversion/Local/DualPair.lean | 27 +++++++++---------- .../Analysis/InnerProductSpace/Dual.lean | 7 ++--- 4 files changed, 18 insertions(+), 24 deletions(-) diff --git a/SphereEversion/Global/Relation.lean b/SphereEversion/Global/Relation.lean index 12c62401..67b3cf2b 100644 --- a/SphereEversion/Global/Relation.lean +++ b/SphereEversion/Global/Relation.lean @@ -613,7 +613,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 (mod_cast le_top) + · exact ψ.contMDiff_to.contMDiffAt.mdifferentiableAt (by simp) conv_rhs => rw [← OneJetBundle.map_id σ] congr 1 · rw [OpenSmoothEmbedding.invFun_comp_coe] diff --git a/SphereEversion/Local/Corrugation.lean b/SphereEversion/Local/Corrugation.lean index 9c66ba21..21125488 100644 --- a/SphereEversion/Local/Corrugation.lean +++ b/SphereEversion/Local/Corrugation.lean @@ -167,7 +167,7 @@ theorem corrugation.fderiv_eq {N : ℝ} (hN : N ≠ 0) (hγ_diff : 𝒞 1 ↿γ) have key := (hasFDerivAt_parametric_primitive_of_contDiff' diff (hπ_diff.const_smul N) x₀ 0).2 erw [fderiv_const_smul key.differentiableAt, key.fderiv, smul_add, add_comm] congr 1 - rw [fderiv_fun_const_smul (hπ_diff.differentiable le_rfl).differentiableAt N, π.fderiv] + rw [fderiv_fun_const_smul (hπ_diff.differentiable (by simp)).differentiableAt N, π.fderiv] simp only [smul_smul, inv_mul_cancel₀ hN, one_div, smul_eq_mul, one_smul, ContinuousLinearMap.comp_smul] @@ -181,8 +181,8 @@ theorem fderiv_corrugated_map (hN : N ≠ 0) (hγ_diff : 𝒞 1 ↿γ) {f : E D (f + corrugation p.π N γ) x = p.update (D f x) (γ x (N * p.π x)) + corrugation.remainder p.π N γ x := by ext v - erw [fderiv_add (hf.differentiable le_rfl).differentiableAt - ((corrugation.contDiff _ N hγ_diff).differentiable le_rfl).differentiableAt] + erw [fderiv_add (hf.differentiable (by simp)).differentiableAt + ((corrugation.contDiff _ N hγ_diff).differentiable (by simp)).differentiableAt] simp_rw [ContinuousLinearMap.add_apply, corrugation.fderiv_apply _ N hN hγ_diff, hfγ, DualPair.update, ContinuousLinearMap.add_apply, p.π.comp_toSpanSingleton_apply, add_assoc] diff --git a/SphereEversion/Local/DualPair.lean b/SphereEversion/Local/DualPair.lean index 7ac983ac..808e7de9 100644 --- a/SphereEversion/Local/DualPair.lean +++ b/SphereEversion/Local/DualPair.lean @@ -65,7 +65,7 @@ attribute [local simp] ContinuousLinearMap.toSpanSingleton_apply theorem pi_ne_zero (p : DualPair E) : p.π ≠ 0 := fun H ↦ by simpa [H] using p.pairing -theorem ker_pi_ne_top (p : DualPair E) : ker p.π ≠ ⊤ := fun H ↦ by +theorem ker_pi_ne_top (p : DualPair E) : p.π.ker ≠ ⊤ := fun H ↦ by have : p.π.toLinearMap p.v = 1 := p.pairing simpa [LinearMap.ker_eq_top.mp H] @@ -84,10 +84,10 @@ def update (p : DualPair E) (φ : E →L[ℝ] F) (w : F) : E →L[ℝ] F := φ + (w - φ p.v) ⬝ p.π @[simp] -theorem update_ker_pi (p : DualPair E) (φ : E →L[ℝ] F) (w : F) {u} (hu : u ∈ ker p.π) : +theorem update_ker_pi (p : DualPair E) (φ : E →L[ℝ] F) (w : F) {u} (hu : u ∈ p.π.ker) : p.update φ w u = φ u := by rw [LinearMap.mem_ker] at hu - simp [update, hu] + simpa [update] using Or.inl hu @[simp] theorem update_v (p : DualPair E) (φ : E →L[ℝ] F) (w : F) : p.update φ w p.v = w := by @@ -105,21 +105,21 @@ theorem update_update (p : DualPair E) (φ : E →L[ℝ] F) (w w' : F) : add_sub_cancel, add_assoc, ← ContinuousLinearMap.add_comp, ← toSpanSingleton_add, sub_add_eq_add_sub, add_sub_cancel] -theorem inf_eq_bot (p : DualPair E) : ker p.π ⊓ p.spanV = ⊥ := bot_unique <| fun x hx ↦ by +theorem inf_eq_bot (p : DualPair E) : p.π.ker ⊓ p.spanV = ⊥ := bot_unique <| fun x hx ↦ by have : p.π x = 0 ∧ ∃ a : ℝ, a • p.v = x := by simpa [DualPair.spanV, Submodule.mem_span_singleton] using hx rcases this with ⟨H, t, rfl⟩ rw [p.π.map_smul, p.pairing, smul_eq_mul, mul_one] at H simp [H] -theorem sup_eq_top (p : DualPair E) : ker p.π ⊔ p.spanV = ⊤ := by +theorem sup_eq_top (p : DualPair E) : p.π.ker ⊔ p.spanV = ⊤ := by rw [Submodule.sup_eq_top_iff] intro x refine ⟨x - p.π x • p.v, ?_, p.π x • p.v, ?_, ?_⟩ <;> simp [DualPair.spanV, Submodule.mem_span_singleton, p.pairing] -theorem decomp (p : DualPair E) (e : E) : ∃ u ∈ ker p.π, ∃ t : ℝ, e = u + t • p.v := by - have : e ∈ ker p.π ⊔ p.spanV := by +theorem decomp (p : DualPair E) (e : E) : ∃ u ∈ p.π.ker, ∃ t : ℝ, e = u + t • p.v := by + have : e ∈ p.π.ker ⊔ p.spanV := by rw [p.sup_eq_top] exact Submodule.mem_top simp_rw [Submodule.mem_sup, DualPair.mem_spanV] at this @@ -127,7 +127,7 @@ theorem decomp (p : DualPair E) (e : E) : ∃ u ∈ ker p.π, ∃ t : ℝ, e = u exact ⟨u, hu, t, rfl⟩ -- useful with `DualPair.decomp` -theorem update_apply (p : DualPair E) (φ : E →L[ℝ] F) {w : F} {t : ℝ} {u} (hu : u ∈ ker p.π) : +theorem update_apply (p : DualPair E) (φ : E →L[ℝ] F) {w : F} {t : ℝ} {u} (hu : u ∈ p.π.ker) : p.update φ w (u + t • p.v) = φ u + t • w := by rw [map_add, map_smul, p.update_v, p.update_ker_pi _ _ hu] @@ -152,15 +152,12 @@ theorem map_update_comp_right (p : DualPair E) (ψ' : E →L[ℝ] F) (φ : E ≃ @[simp] theorem injective_update_iff (p : DualPair E) {φ : E →L[ℝ] F} (hφ : Injective φ) {w : F} : - Injective (p.update φ w) ↔ w ∉ (ker p.π).map φ := by + Injective (p.update φ w) ↔ w ∉ (p.π.ker).map (φ : E →ₛₗ[.id ℝ] F) := by constructor · rintro h ⟨u, hu, rfl⟩ have : p.update φ (φ u) p.v = φ u := p.update_v φ (φ u) - conv_rhs at this => rw [← p.update_ker_pi φ (φ u) hu] - rw [← h this] at hu - simp only [SetLike.mem_coe, LinearMap.mem_ker] at hu - rw [p.pairing] at hu - linarith + nth_rw 2 [← p.update_ker_pi φ (φ u) hu] at this + simp [← h this, p.pairing] at hu · intro hw refine (injective_iff_map_eq_zero (p.update φ w)).mpr fun x hx ↦ ?_ rcases p.decomp x with ⟨u, hu, t, rfl⟩ @@ -168,7 +165,7 @@ theorem injective_update_iff (p : DualPair E) {φ : E →L[ℝ] F} (hφ : Inject obtain rfl : t = 0 := by by_contra ht apply hw - refine ⟨-t⁻¹ • u, (ker p.π).smul_mem _ hu, ?_⟩ + refine ⟨-t⁻¹ • u, (p.π.ker).smul_mem _ hu, ?_⟩ rw [map_smul] have : -t⁻¹ • (φ u + t • w) + w = -t⁻¹ • (0 : F) + w := congr_arg (-t⁻¹ • · + w) hx rwa [smul_add, neg_smul, neg_smul, inv_smul_smul₀ ht, smul_zero, zero_add, diff --git a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Dual.lean b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Dual.lean index cf064031..965e58f6 100644 --- a/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Dual.lean +++ b/SphereEversion/ToMathlib/Analysis/InnerProductSpace/Dual.lean @@ -16,12 +16,9 @@ variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteS @[inherit_doc] local notation "pr[" x "]ᗮ" => projSpanOrthogonal x theorem orthogonal_span_toDual_symm (π : E →L[ℝ] ℝ) : - {.(InnerProductSpace.toDual ℝ E).symm π}ᗮ = ker π := by + {.(InnerProductSpace.toDual ℝ E).symm π}ᗮ = π.ker := by ext x - suffices (∀ a : ℝ, ⟪a • (toDual ℝ E).symm π, x⟫ = 0) ↔ π x = 0 by - simp only [orthogonal, mem_mk, LinearMap.mem_ker, ← toDual_symm_apply] - change (∀ (u : E), u ∈ span ℝ {(LinearIsometryEquiv.symm (toDual ℝ E)) π} → inner _ u x = 0) ↔ _ - simpa + suffices (∀ a : ℝ, ⟪a • (toDual ℝ E).symm π, x⟫ = 0) ↔ π x = 0 by simp refine ⟨fun h ↦ ?_, fun h _ ↦ ?_⟩ · simpa using h 1 · simp [inner_smul_left, h] From 624beb6029518b6f301f23fb72a2ab00c9898b85 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Tue, 13 Jan 2026 15:50:15 +0100 Subject: [PATCH 6/7] Fix remaining errors --- SphereEversion/Global/Immersion.lean | 3 ++- .../Global/ParametricityForFree.lean | 11 ++++----- SphereEversion/Local/HPrinciple.lean | 4 ++-- .../Local/ParametricHPrinciple.lean | 17 +++++++------ SphereEversion/Local/SphereEversion.lean | 24 +++++++++---------- 5 files changed, 29 insertions(+), 30 deletions(-) diff --git a/SphereEversion/Global/Immersion.lean b/SphereEversion/Global/Immersion.lean index 30c4c3ee..e92f1be3 100644 --- a/SphereEversion/Global/Immersion.lean +++ b/SphereEversion/Global/Immersion.lean @@ -72,7 +72,8 @@ 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 φ) : - (immersionRel I M I' M').slice ⟨(m, m'), φ⟩ p = ((ker p.π).map φ : Set <| TM' m')ᶜ := + (immersionRel I M I' M').slice ⟨(m, m'), φ⟩ p = + (((p.π.ker).map (φ : TM m →ₛₗ[.id ℝ] TM' m')): Set <| TM' m')ᶜ := Set.ext_iff.mpr fun _ ↦ p.injective_update_iff hφ variable [FiniteDimensional ℝ E] [FiniteDimensional ℝ E'] diff --git a/SphereEversion/Global/ParametricityForFree.lean b/SphereEversion/Global/ParametricityForFree.lean index eed94b4d..79c0b8e1 100644 --- a/SphereEversion/Global/ParametricityForFree.lean +++ b/SphereEversion/Global/ParametricityForFree.lean @@ -82,9 +82,9 @@ theorem relativize_slice {σ : OneJetBundle (IP.prod I) (P × M) I' M'} erw [ContinuousLinearMap.comp_apply, ContinuousLinearMap.inr_apply, ← ContinuousLinearMap.map_neg, neg_sub] obtain ⟨u, hu, t, rfl⟩ := q.decomp x - have hv : (id (0, (q.v : E)) : TangentSpace (IP.prod I) σ.proj.1) - p.v ∈ ker p.π := by + have hv : (id (0, (q.v : E)) : TangentSpace (IP.prod I) σ.proj.1) - p.v ∈ p.π.ker := by simp [LinearMap.mem_ker, map_sub, p.pairing, h2pq, q.pairing, sub_self] - have hup : ((0 : EP), u) ∈ ker p.π := (h2pq u).trans hu + have hup : ((0 : EP), u) ∈ p.π.ker := (h2pq u).trans hu erw [q.update_apply _ hu, ← Prod.zero_mk_add_zero_mk, map_add, p.update_ker_pi _ _ hup, ← Prod.smul_zero_mk, map_smul] conv_lhs => rw [← sub_add_cancel (0, q.v) p.v] @@ -203,7 +203,7 @@ theorem FamilyOneJetSec.curry_ϕ' (S : FamilyOneJetSec (IP.prod I) (P × M) I' M (x : M) : (S.curry p).ϕ x = (S p.1).ϕ (p.2, x) ∘L ContinuousLinearMap.inr ℝ EP E := by rw [S.curry_ϕ] congr 1 - refine (mdifferentiableAt_const.mfderiv_prod (contMDiff_id.mdifferentiableAt le_top)).trans ?_ + refine (mdifferentiableAt_const.mfderiv_prod mdifferentiableAt_id).trans ?_ rw [mfderiv_id, mfderiv_const] rfl @@ -216,9 +216,8 @@ theorem FamilyOneJetSec.isHolonomicAt_curry (S : FamilyOneJetSec (IP.prod I) (P (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).contMDiff_bs.mdifferentiableAt (mod_cast le_top)) - (mdifferentiableAt_const.prodMk (contMDiff_id.mdifferentiableAt le_top))).trans - ?_ + refine (mfderiv_comp x ((S t).contMDiff_bs.mdifferentiableAt (by simp)) + (mdifferentiableAt_const.prodMk mdifferentiableAt_id)).trans ?_ rw [id, hS] rfl diff --git a/SphereEversion/Local/HPrinciple.lean b/SphereEversion/Local/HPrinciple.lean index 387c639c..990acf68 100644 --- a/SphereEversion/Local/HPrinciple.lean +++ b/SphereEversion/Local/HPrinciple.lean @@ -89,7 +89,7 @@ together with a dual pair `p` and a subspace `E'` of the corresponding hyperplan structure StepLandscape extends Landscape E where E' : Submodule ℝ E p : DualPair E - hEp : E' ≤ ker p.π + hEp : E' ≤ p.π.ker variable {E} @@ -510,7 +510,7 @@ theorem RelLoc.FormalSol.improve (𝓕 : FormalSol R) (h_hol : ∀ᶠ x near L.C · apply (H.comp_le_0 _ _).mono · intro t ht rw [ht] - exact hH₀.self_of_nhdsSet 0 right_mem_Iic + exact hH₀.self_of_nhdsSet 0 self_mem_Iic -- t = 0 · apply (H.comp_ge_1 _ _).mono · intro t ht diff --git a/SphereEversion/Local/ParametricHPrinciple.lean b/SphereEversion/Local/ParametricHPrinciple.lean index 8af15367..d091bb62 100644 --- a/SphereEversion/Local/ParametricHPrinciple.lean +++ b/SphereEversion/Local/ParametricHPrinciple.lean @@ -78,9 +78,9 @@ theorem relativize_slice_loc {σ : OneJet (P × E) F} {p : DualPair (P × E)} (q simp_rw [ContinuousLinearMap.comp_apply, ContinuousLinearMap.inr_apply] rw [← ContinuousLinearMap.map_neg, neg_sub] obtain ⟨u, hu, t, rfl⟩ := q.decomp x - have hv : (0, q.v) - p.v ∈ ker p.π := by - rw [LinearMap.mem_ker, map_sub, p.pairing, h2pq, q.pairing, sub_self] - have hup : ((0 : P), u) ∈ ker p.π := (h2pq u).trans hu + have hv : (0, q.v) - p.v ∈ p.π.ker := by + simp [map_sub, p.pairing, h2pq, q.pairing, sub_self] + have hup : ((0 : P), u) ∈ p.π.ker := (h2pq u).trans hu rw [q.update_apply _ hu, ← Prod.zero_mk_add_zero_mk, map_add, p.update_ker_pi _ _ hup, ← Prod.smul_zero_mk, map_smul, vadd_eq_add] conv_lhs => { rw [← sub_add_cancel (0, q.v) p.v] } @@ -140,7 +140,7 @@ theorem FamilyJetSec.uncurry_φ' (S : FamilyJetSec E F P) (p : P × E) : S.φ p.1 p.2 ∘L ContinuousLinearMap.snd ℝ P E := by simp_rw [S.uncurry_φ, fderiv_snd, add_left_inj] refine (fderiv_comp p ((S.f_diff.comp (contDiff_id.prodMk contDiff_const)).differentiable - (mod_cast le_top) p.1) differentiableAt_fst).trans ?_ + (by simp) p.1) differentiableAt_fst).trans ?_ rw [fderiv_fst] rfl @@ -163,10 +163,9 @@ theorem FamilyJetSec.isHolonomicAt_uncurry (S : FamilyJetSec E F P) {p : P × E} simp_rw [JetSec.IsHolonomicAt, S.uncurry_φ] rw [show S.uncurry.f = fun x ↦ S.uncurry.f x from rfl, funext S.uncurry_f, show (fun x : P × E ↦ S.f x.1 x.2) = ↿S.f from rfl] - rw [fderiv_prod_eq_add (S.f_diff.differentiable (mod_cast le_top) _), fderiv_snd] + rw [fderiv_prod_eq_add (S.f_diff.differentiable (by simp) _), fderiv_snd] refine (add_right_inj _).trans ?_ - have := fderiv_comp p ((S p.1).f_diff.contDiffAt.differentiableAt (mod_cast le_top)) - differentiableAt_snd + have := fderiv_comp p ((S p.1).f_diff.contDiffAt.differentiableAt (by simp)) differentiableAt_snd rw [show D (fun z : P × E ↦ (↿S.f) (p.fst, z.snd)) p = _ from this, fderiv_snd, (show Surjective (ContinuousLinearMap.snd ℝ P E) from Prod.snd_surjective).clm_comp_injective.eq_iff] @@ -217,7 +216,7 @@ theorem FamilyJetSec.isHolonomicAt_curry (S : FamilyJetSec (P × E) F G) {t : G} (hS : (S t).IsHolonomicAt (s, x)) : (S.curry (t, s)).IsHolonomicAt x := by simp_rw [JetSec.IsHolonomicAt, S.curry_φ] at hS ⊢ rw [show (S.curry (t, s)).f = fun x ↦ (S.curry (t, s)).f x from rfl, funext (S.curry_f _)] - refine (fderiv_comp x ((S t).f_diff.contDiffAt.differentiableAt (mod_cast le_top)) + refine (fderiv_comp x ((S t).f_diff.contDiffAt.differentiableAt (by simp)) ((differentiableAt_const _).prodMk differentiableAt_id)).trans ?_ rw [_root_.id, hS] rfl @@ -287,7 +286,7 @@ theorem RelLoc.FamilyFormalSol.improve_htpy {ε : ℝ} (ε_pos : 0 < ε) (C : Se obtain ⟨𝓕, h₁, -, h₂, -, h₄, h₅⟩ := 𝓕₀.uncurry.improve_htpy' (R.isOpen_relativize h_op) (h_ample.relativize P) parametric_landscape ε_pos (h_hol.mono fun p hp ↦ 𝓕₀.isHolonomicAt_uncurry.mpr hp) - have h₁ : ∀ p, 𝓕 0 p = 𝓕₀.uncurry p := by intro p; rw [h₁.self_of_nhdsSet 0 right_mem_Iic]; rfl + have h₁ : ∀ p, 𝓕 0 p = 𝓕₀.uncurry p := by intro p; rw [h₁.self_of_nhdsSet 0 self_mem_Iic]; rfl refine ⟨𝓕.curry, ?_, ?_, ?_, ?_⟩ · intro s x; exact curry_eq_iff_eq_uncurry_loc (h₁ (s, x)) · refine h₂.mono ?_; rintro ⟨s, x⟩ hp t; exact curry_eq_iff_eq_uncurry_loc (hp t) diff --git a/SphereEversion/Local/SphereEversion.lean b/SphereEversion/Local/SphereEversion.lean index 66ed8d5c..e5b74ce0 100644 --- a/SphereEversion/Local/SphereEversion.lean +++ b/SphereEversion/Local/SphereEversion.lean @@ -178,14 +178,14 @@ theorem loc_immersion_rel_ample (n : ℕ) [Fact (dim E = n + 1)] (h : finrank clear h_mem let u : E := (InnerProductSpace.toDual ℝ E).symm p.π have u_ne : u ≠ 0 := EmbeddingLike.map_ne_zero_iff.mpr p.pi_ne_zero - by_cases H : ker p.π = (ℝ ∙ x)ᗮ + by_cases H : p.π.ker = (ℝ ∙ x)ᗮ · have key : ∀ w, EqOn (p.update φ w) φ (ℝ ∙ x)ᗮ := by intro w x rw [← H] exact p.update_ker_pi φ w exact ample_slice_of_forall _ p fun w _ ↦ hφ.congr (key w).symm obtain ⟨v', v'_in, hv', hπv'⟩ : - ∃ v' : E, v' ∈ (ℝ ∙ x)ᗮ ∧ ((ℝ ∙ x)ᗮ = ker p.π ⊓ (ℝ ∙ x)ᗮ ⊔ ℝ ∙ v') ∧ p.π v' = 1 := by + ∃ v' : E, v' ∈ (ℝ ∙ x)ᗮ ∧ ((ℝ ∙ x)ᗮ = p.π.ker ⊓ (ℝ ∙ x)ᗮ ⊔ ℝ ∙ v') ∧ p.π v' = 1 := by have ne_z : p.π (pr[x]ᗮ u) ≠ 0 := by rw [← toDual_symm_apply] change ¬⟪u, pr[x]ᗮ u⟫ = 0 @@ -204,25 +204,25 @@ theorem loc_immersion_rel_ample (n : ℕ) [Fact (dim E = n + 1)] (h : finrank v := v' pairing := hπv' } apply ample_slice_of_ample_slice (show p'.π = p.π from rfl) - suffices slice R p' (x, y, φ) = (map φ (ker p.π ⊓ (ℝ ∙ x)ᗮ) : Set F)ᶜ by + suffices slice R p' (x, y, φ) = (((p.π.ker ⊓ (ℝ ∙ x)ᗮ).map ((φ : E →ₛₗ[.id ℝ] F))) : Set F)ᶜ by rw [this] apply AmpleSet.of_one_lt_codim let Φ := φ.toLinearMap - suffices 2 ≤ dim (F ⧸ map Φ (ker p.π ⊓ (ℝ ∙ x)ᗮ)) by + suffices 2 ≤ dim (F ⧸ map Φ (p.π.ker ⊓ (ℝ ∙ x)ᗮ)) by rw [← finrank_eq_rank] exact_mod_cast this apply le_of_add_le_add_right - rw [Submodule.finrank_quotient_add_finrank (map Φ <| ker p.π ⊓ (ℝ ∙ x)ᗮ)] - have : dim (ker p.π ⊓ (ℝ ∙ x)ᗮ : Submodule ℝ E) + 1 = n := by - have eq := Submodule.finrank_sup_add_finrank_inf_eq (ker p.π ⊓ (ℝ ∙ x)ᗮ) (span ℝ {v'}) + rw [Submodule.finrank_quotient_add_finrank (map Φ <| p.π.ker ⊓ (ℝ ∙ x)ᗮ)] + have : dim (p.π.ker ⊓ (ℝ ∙ x)ᗮ : Submodule ℝ E) + 1 = n := by + have eq := Submodule.finrank_sup_add_finrank_inf_eq (p.π.ker ⊓ (ℝ ∙ x)ᗮ) (span ℝ {v'}) have eq₁ : dim (ℝ ∙ x)ᗮ = n := finrank_orthogonal_span_singleton x_ne - have eq₂ : ker p.π ⊓ (ℝ ∙ x)ᗮ ⊓ span ℝ {v'} = (⊥ : Submodule ℝ E) := by + have eq₂ : p.π.ker ⊓ (ℝ ∙ x)ᗮ ⊓ span ℝ {v'} = (⊥ : Submodule ℝ E) := by erw [inf_left_right_swap, inf_comm, ← inf_assoc, p'.inf_eq_bot, bot_inf_eq] have eq₃ : dim (span ℝ {v'}) = 1 := finrank_span_singleton p'.v_ne_zero rw [← hv', eq₁, eq₃, eq₂] at eq simpa only [finrank_bot] using eq.symm have : dim E = n + 1 := Fact.out - linarith [finrank_map_le Φ (ker p.π ⊓ (ℝ ∙ x)ᗮ)] + linarith [finrank_map_le Φ (p.π.ker ⊓ (ℝ ∙ x)ᗮ)] ext w rw [mem_slice_iff_of_not_mem hx y] rw [injOn_iff_injective] @@ -232,8 +232,9 @@ theorem loc_immersion_rel_ample (n : ℕ) [Fact (dim E = n + 1)] (h : finrank ext z simp only [p', j, DualPair.update, restrict_apply, ContinuousLinearMap.add_apply, p'', ContinuousLinearMap.coe_comp', coe_subtypeL', Submodule.coe_subtype, comp_apply] - have eq' : map (φ.comp j) (ker p''.π) = map φ (ker p.π ⊓ (ℝ ∙ x)ᗮ) := by - have : map (↑j) (ker p''.π) = ker p.π ⊓ (ℝ ∙ x)ᗮ := by + have eq' : (p''.π.ker).map (φ.comp j : _ →ₛₗ[.id ℝ] F) = + (p.π.ker ⊓ (ℝ ∙ x)ᗮ).map (φ : E →ₛₗ[.id ℝ] F) := by + have : (p''.π.ker).map (j : _ →ₛₗ[.id ℝ] _) = p.π.ker ⊓ (ℝ ∙ x)ᗮ := by ext z simp only [mem_map, LinearMap.mem_ker, mem_inf] constructor @@ -242,7 +243,6 @@ theorem loc_immersion_rel_ample (n : ℕ) [Fact (dim E = n + 1)] (h : finrank · rintro ⟨hz, z_in⟩ exact ⟨⟨z, z_in⟩, hz, rfl⟩ erw [← this, map_comp] - rfl rw [eq, p''.injective_update_iff, mem_compl_iff, eq'] · exact Iff.rfl rw [← show ((ℝ ∙ x)ᗮ : Set E).restrict φ = φ.comp j by ext; rfl] From 06ef932324e9ecc18a29d3c768ca39d9ef098c40 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Tue, 13 Jan 2026 16:12:08 +0100 Subject: [PATCH 7/7] Fix declarations, hopefully --- blueprint/src/global_convex_integration.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/blueprint/src/global_convex_integration.tex b/blueprint/src/global_convex_integration.tex index 75870b47..9f10e312 100644 --- a/blueprint/src/global_convex_integration.tex +++ b/blueprint/src/global_convex_integration.tex @@ -283,7 +283,7 @@ \subsection{Jets spaces} \begin{definition} \label{def:hom_bundle} \leanok -\lean{Bundle.ContinuousLinearMap} +\lean{Bundle.ContinuousLinearMap.vectorBundle} Let $E → B$ and $F → B$ be two vector bundles over some smooth manifold $B$. The bundle $\Hom(E, F) → B$ is the set of linear maps from $E_b$ to $F_b$ for some $b$ in $B$, with the obvious projection map.