From 47f408c937044db054cb77f088622ad067236629 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Sat, 17 Oct 2026 11:26:53 +0200 Subject: [PATCH 1/3] wip: bump to current mathlib --- still a handful of broken proofs --- SphereEversion/Global/LocalisationData.lean | 4 +- SphereEversion/Global/SmoothEmbedding.lean | 2 +- SphereEversion/Local/SphereEversion.lean | 2 +- SphereEversion/Loops/Basic.lean | 46 +++++++++++++------ SphereEversion/Loops/Exists.lean | 3 +- SphereEversion/Loops/Reparametrization.lean | 4 +- .../ToMathlib/Analysis/Convex/Basic.lean | 2 +- SphereEversion/ToMathlib/ExistsOfConvex.lean | 6 ++- lake-manifest.json | 22 ++++----- lakefile.toml | 1 - lean-toolchain | 2 +- 11 files changed, 58 insertions(+), 36 deletions(-) diff --git a/SphereEversion/Global/LocalisationData.lean b/SphereEversion/Global/LocalisationData.lean index 4208c2db..bb6d91bf 100644 --- a/SphereEversion/Global/LocalisationData.lean +++ b/SphereEversion/Global/LocalisationData.lean @@ -50,8 +50,8 @@ omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] in theorem iUnion_succ' {β : Type*} (s : ld.ι → Set β) (i : IndexType ld.N) : (⋃ j ≤ i, s j) = (⋃ j < i, s j) ∪ s i := by simp only [(fun _ ↦ le_iff_lt_or_eq : ∀ j, j ≤ i ↔ j < i ∨ j = i)] - erw [biUnion_union, biUnion_singleton] - rfl + sorry /-erw [biUnion_union, biUnion_singleton] + rfl-/ open Filter diff --git a/SphereEversion/Global/SmoothEmbedding.lean b/SphereEversion/Global/SmoothEmbedding.lean index 25f6564e..db854c5b 100644 --- a/SphereEversion/Global/SmoothEmbedding.lean +++ b/SphereEversion/Global/SmoothEmbedding.lean @@ -415,7 +415,7 @@ theorem nice_update_of_eq_outside_compact_aux {K : Set X} (g : X → Y) φ.update ψ f g m = f m := by by_cases hm' : m ∈ range φ · obtain ⟨x, rfl⟩ := hm' - replace hm : x ∉ K := by contrapose! hm; exact mem_image_of_mem φ hm + replace hm : x ∉ K := by contrapose hm; exact mem_image_of_mem φ hm simp [hg x hm] · exact ite_eq_right hm' diff --git a/SphereEversion/Local/SphereEversion.lean b/SphereEversion/Local/SphereEversion.lean index daf49543..65aa98eb 100644 --- a/SphereEversion/Local/SphereEversion.lean +++ b/SphereEversion/Local/SphereEversion.lean @@ -194,7 +194,7 @@ theorem loc_immersion_rel_ample (n : ℕ) [Fact (dim E = n + 1)] (h : finrank rw [← toDual_symm_apply] change ¬⟪u, pr[x]ᗮ u⟫ = 0 rw [inner_projection_self_eq_zero_iff.not] - contrapose! H + contrapose H rw [orthogonal_orthogonal] at H rw [← orthogonal_span_toDual_symm, spanOrthogonal, spanLine, span_singleton_eq_span_singleton_of_ne u_ne H] diff --git a/SphereEversion/Loops/Basic.lean b/SphereEversion/Loops/Basic.lean index d9a708cb..e6bf7819 100644 --- a/SphereEversion/Loops/Basic.lean +++ b/SphereEversion/Loops/Basic.lean @@ -382,22 +382,42 @@ theorem ContDiff.partial_loop {γ : E → Loop F} {n : ℕ∞} (hγ_diff : 𝒞 variable [FiniteDimensional ℝ F] + + +#click_suggestions set_option backward.isDefEq.respectTransparency.types false in theorem Loop.support_diff {γ : E → Loop F} : Loop.support (Loop.diff γ) ⊆ Loop.support γ := by unfold Loop.support - erw [closure_compl, closure_compl] - rw [compl_subset_compl] - intro x hx - rw [mem_interior_iff_mem_nhds] at * - rcases mem_nhds_iff.mp hx with ⟨U, hU, U_op, hxU⟩ - apply Filter.mem_of_superset (U_op.mem_nhds hxU) fun y hy ↦ ?_ - have Hy : ∀ t, (fun z ↦ γ z t) =ᶠ[𝓝 y] fun z ↦ (γ z).average := - fun t ↦ Filter.mem_of_superset (U_op.mem_nhds hy) - (fun z hz ↦ Loop.isConst_iff_forall_avg.mp (hU hz) t) - have : ∀ t : ℝ, Loop.diff γ y t = D (fun z : E ↦ (γ z).average) y := fun t ↦ (Hy t).fderiv_eq - intro t s - simp only [this] - + gcongr + intro hx + sorry + -- have Hy : ∀ t, (fun z ↦ γ z t) =ᶠ[𝓝 y] fun z ↦ (γ z).average := + -- fun t ↦ Filter.mem_of_superset (U_op.mem_nhds hy) + -- (fun z hz ↦ Loop.isConst_iff_forall_avg.mp (hU hz) t) + -- have (y) : ∀ t : ℝ, Loop.diff γ y t = D (fun z : E ↦ (γ z).average) y := fun t ↦ (Hy t).fderiv_eq + -- intro y s + -- trans 0 + -- sorry + -- sorry + -- --suffices ∀() + -- --intro s t + -- unfold IsConst at hx ⊢ + --change closure {x | (diff γ x).IsConst}ᶜ ⊆ closure {x | (γ x).IsConst}ᶜ + --rw [Set.compl_def] + --rw [closure_compl] + + --, closure_compl] + --rw [compl_subset_compl] + --intro x hx + --rw [mem_interior_iff_mem_nhds] at * + -- rcases mem_nhds_iff.mp hx with ⟨U, hU, U_op, hxU⟩ + -- --apply Filter.mem_of_superset (U_op.mem_nhds hxU) fun y hy ↦ ?_ + -- have Hy : ∀ t, (fun z ↦ γ z t) =ᶠ[𝓝 y] fun z ↦ (γ z).average := + -- fun t ↦ Filter.mem_of_superset (U_op.mem_nhds hy) + -- (fun z hz ↦ Loop.isConst_iff_forall_avg.mp (hU hz) t) + -- have : ∀ t : ℝ, Loop.diff γ y t = D (fun z : E ↦ (γ z).average) y := fun t ↦ (Hy t).fderiv_eq + -- intro t s + -- simp only [this] variable [FiniteDimensional ℝ E] diff --git a/SphereEversion/Loops/Exists.lean b/SphereEversion/Loops/Exists.lean index 3afcadd8..e737848a 100644 --- a/SphereEversion/Loops/Exists.lean +++ b/SphereEversion/Loops/Exists.lean @@ -169,11 +169,12 @@ theorem exist_loops_aux2 [FiniteDimensional ℝ E] (hK : IsCompact K) (hΩ_op : in Lean 3. -/ apply hU.mem_nhdsSet.mpr + sorry /- proof was refine (union_subset_union fun (x : E × ℝ × ℝ) (hx : x.2.1 ≤ 5⁻¹) ↦ lt_of_le_of_lt hx (by norm_num)) ?_ refine union_subset_union (fun (x : E × ℝ × ℝ) (hx : fract x.2.2 ≤ 5⁻¹) ↦ lt_of_le_of_lt hx (by norm_num)) ?_ - exact fun x hx ↦ lt_of_lt_of_le (by norm_num : (3 / 4 : ℝ) < 4 / 5) hx + exact fun x hx ↦ lt_of_lt_of_le (by norm_num : (3 / 4 : ℝ) < 4 / 5) hx -/ have h2γ₄ : EqOn γ₄ (fun x ↦ b x.1) U := by rintro ⟨x, t, s⟩ hxts simp_rw [h0γ₄, γ₃, Loop.reparam_apply] diff --git a/SphereEversion/Loops/Reparametrization.lean b/SphereEversion/Loops/Reparametrization.lean index 8e5cae62..1a643036 100644 --- a/SphereEversion/Loops/Reparametrization.lean +++ b/SphereEversion/Loops/Reparametrization.lean @@ -275,7 +275,7 @@ theorem contDiffOn_localCenteringDensity : fun x ↦ (x, x) change ContDiffOn ℝ ∞ ((w ∘ z) ∘ Prod.fst) (γ.localCenteringDensityNhd x ×ˢ (univ : Set ℝ)) rw [prod_univ] - refine ContDiffOn.comp ?_ contDiff_fst.contDiffOn Subset.rfl + sorry /-refine ContDiffOn.comp ?_ contDiff_fst.contDiffOn ?_--(by simp)--Subset.rfl have h₁ := contDiff_barycentric ι ℝ F (Fintype.card_fin _) (n := ∞) have h₂ : 𝒞 ∞ (eval i : (ι → ℝ) → ℝ) := contDiff_apply _ _ i refine (h₂.comp_contDiffOn h₁).comp ?_ ?_ @@ -284,7 +284,7 @@ theorem contDiffOn_localCenteringDensity : refine γ.smooth_surrounded.contDiffOn.prodMap (ContDiff.contDiffOn ?_) exact γ.approxSurroundingPointsAt_smooth x _ · intro y hy - simp [z, γ.approxSurroundingPointsAt_mem_affineBases x y hy] + simp [z, γ.approxSurroundingPointsAt_mem_affineBases x y hy] -/ · exact contDiff_deltaMollifier.comp contDiff_snd variable [FiniteDimensional ℝ E] in diff --git a/SphereEversion/ToMathlib/Analysis/Convex/Basic.lean b/SphereEversion/ToMathlib/Analysis/Convex/Basic.lean index 169de34d..eff2c90a 100644 --- a/SphereEversion/ToMathlib/Analysis/Convex/Basic.lean +++ b/SphereEversion/ToMathlib/Analysis/Convex/Basic.lean @@ -158,7 +158,7 @@ theorem ReallyConvex.preimageₛₗ (f : E →ₛₗ[σ.toRingHom] E') {s : Set apply hs.finsum_mem · intro i; rw [← map_zero σ]; apply σ.monotone'; apply hw · rw [← map_finsum _ h4w, h3w, map_one] - · intro i hi; apply h2w; rw [mem_support] at hi ⊢; contrapose! hi; rw [hi, map_zero] + · intro i hi; apply h2w; rw [mem_support] at hi ⊢; contrapose hi; rw [hi, map_zero] theorem ReallyConvex.preimage [IsOrderedRing 𝕜] (f : E →ₗ[𝕜] E₂) {s : Set E₂} (hs : ReallyConvex 𝕜 s) : diff --git a/SphereEversion/ToMathlib/ExistsOfConvex.lean b/SphereEversion/ToMathlib/ExistsOfConvex.lean index 048904de..77e2accf 100644 --- a/SphereEversion/ToMathlib/ExistsOfConvex.lean +++ b/SphereEversion/ToMathlib/ExistsOfConvex.lean @@ -76,6 +76,7 @@ theorem exists_contMDiff_of_convex {P : M → F → Prop} (hP : ∀ x, Convex ∃ f : M → F, CMDiff n f ∧ ∀ x, P x (f x) := by let PP : (Σ x : M, Germ (𝓝 x) F) → Prop := fun p ↦ p.2.ContMDiffAt I n ∧ P p.1 p.2.value have hPP : ∀ x : M, ReallyConvex (smoothGerm I x) {φ | PP ⟨x, φ⟩} := fun x ↦ by + sorry /- was: apply ReallyConvex.inter · apply reallyConvex_contMDiffAt let v : Germ (𝓝 x) F →ₛₗ[smoothGerm.valueRingHom I x] F := Filter.Germ.valueₛₗ I x @@ -83,7 +84,7 @@ theorem exists_contMDiff_of_convex {P : M → F → Prop} (hP : ∀ x, Convex dsimp only [← smoothGerm.valueOrderRingHom_toRingHom] at v apply ReallyConvex.preimageₛₗ rw [reallyConvex_iff_convex] - apply hP + apply hP -/ have hPP' : ∀ x, ∃ f : M → F, ∀ᶠ x' in 𝓝 x, PP ⟨x', f⟩ := fun x ↦ by rcases hP' x with ⟨U, U_in, f, hf, hf'⟩ use f @@ -140,6 +141,7 @@ theorem exists_contMDiff_of_convex₂ {P : M₁ → (M₂ → F) → Prop} [Sigm let PP : (Σ x : M₁, Germ (𝓝 x) (M₂ → F)) → Prop := fun p ↦ p.2.ContMDiffAtProd I₁ I₂ n ∧ P p.1 p.2.value have hPP : ∀ x : M₁, ReallyConvex (smoothGerm I₁ x) {φ | PP ⟨x, φ⟩} := fun x ↦ by + sorry /- was: apply ReallyConvex.inter · apply reallyConvex_contMDiffAtProd let v : Germ (𝓝 x) (M₂ → F) →ₛₗ[smoothGerm.valueRingHom I₁ x] M₂ → F := Filter.Germ.valueₛₗ I₁ x @@ -147,7 +149,7 @@ theorem exists_contMDiff_of_convex₂ {P : M₁ → (M₂ → F) → Prop} [Sigm dsimp only [← smoothGerm.valueOrderRingHom_toRingHom] at v apply ReallyConvex.preimageₛₗ rw [reallyConvex_iff_convex] - apply hP + apply hP -/ have hPP' : ∀ x, ∃ f : M₁ → M₂ → F, ∀ᶠ x' in 𝓝 x, PP ⟨x', f⟩ := fun x ↦ by rcases hP' x with ⟨U, U_in, f, hf, hf'⟩ use f diff --git a/lake-manifest.json b/lake-manifest.json index d313c2f8..b796c5db 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,17 +15,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "56a005855ea17e0b0958f73ec801ae140b0a1679", + "rev": "fbc1661a327737928fe9d69b74f7deaa09eecfbc", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.35.0", + "inputRev": "master", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "dfa4f38190d07c37e315953e08b90fe2d95b3c24", + "rev": "c2d7840c65673533e15b499f25beecdc6227f7d8", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d6b4c7be5be75ec4917c873ac50c756dc1436372", + "rev": "9d39f9bb0c30aa2f6200808805ff16e6ce950890", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a41f0e9a4dea23188ea9cc1c41ac9f8bbafe0b93", + "rev": "b3cc36c295aa5e3e3c0197b09a6556298e710447", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "df72b022e558978a1c50264cfc4d7fec86fa8e04", + "rev": "17137fad38a2cc782ff00b323a13c3a991d085ab", "name": "proofwidgets", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "4a174c490d8707121c4a9290800489f105d85e07", + "rev": "cbdde3aa2665915fb286c48bcd4cdf885c629511", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "dce0ad79c486cb1fb504af04f953c3466b0c6db8", + "rev": "6d26f8bb4b2bb78f929ad160feac508866821316", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "66e469188fe07963e5cf666c7d4433f45b8131c5", + "rev": "4453b52d2468f4c346a8711d728c0742e7483c9b", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -95,10 +95,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "c24fe6078c630e89b489bffe59b3e20ac30d12c8", + "rev": "34d2efffcb6dc8d5f3537cf6a7f88bfaa999ec49", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.35.0", + "inputRev": "v4.36.0-rc1", "inherited": true, "configFile": "lakefile.toml"}], "name": "SphereEversion", diff --git a/lakefile.toml b/lakefile.toml index aba60259..830f03c6 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -11,7 +11,6 @@ weak.linter.style.header = false [[require]] name = "mathlib" scope = "leanprover-community" -rev = "v4.35.0" [[require]] name = "checkdecls" diff --git a/lean-toolchain b/lean-toolchain index d87704ef..d0cf8c52 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.35.0 \ No newline at end of file +leanprover/lean4:v4.36.0-rc1 \ No newline at end of file From ee949e48420601ebe166fd39d68f066203749c1a Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Wed, 21 Oct 2026 12:01:03 +0200 Subject: [PATCH 2/3] wip: bump to current mathlib --- SphereEversion/Global/LocalisationData.lean | 3 +-- SphereEversion/Loops/Exists.lean | 13 +++++++------ SphereEversion/Loops/Reparametrization.lean | 6 ++++-- SphereEversion/ToMathlib/ExistsOfConvex.lean | 14 ++++++-------- SphereEversion/ToMathlib/SmoothBarycentric.lean | 6 +++--- lake-manifest.json | 10 +++++----- 6 files changed, 26 insertions(+), 26 deletions(-) diff --git a/SphereEversion/Global/LocalisationData.lean b/SphereEversion/Global/LocalisationData.lean index bb6d91bf..96f9d2b1 100644 --- a/SphereEversion/Global/LocalisationData.lean +++ b/SphereEversion/Global/LocalisationData.lean @@ -50,8 +50,7 @@ omit [IsManifold I ∞ M] [IsManifold I' ∞ M'] in theorem iUnion_succ' {β : Type*} (s : ld.ι → Set β) (i : IndexType ld.N) : (⋃ j ≤ i, s j) = (⋃ j < i, s j) ∪ s i := by simp only [(fun _ ↦ le_iff_lt_or_eq : ∀ j, j ≤ i ↔ j < i ∨ j = i)] - sorry /-erw [biUnion_union, biUnion_singleton] - rfl-/ + simp_rw [iUnion_or, iUnion_union_distrib, iUnion_iUnion_eq_left] open Filter diff --git a/SphereEversion/Loops/Exists.lean b/SphereEversion/Loops/Exists.lean index e737848a..96497abd 100644 --- a/SphereEversion/Loops/Exists.lean +++ b/SphereEversion/Loops/Exists.lean @@ -169,12 +169,13 @@ theorem exist_loops_aux2 [FiniteDimensional ℝ E] (hK : IsCompact K) (hΩ_op : in Lean 3. -/ apply hU.mem_nhdsSet.mpr - sorry /- proof was - refine (union_subset_union fun (x : E × ℝ × ℝ) - (hx : x.2.1 ≤ 5⁻¹) ↦ lt_of_le_of_lt hx (by norm_num)) ?_ - refine union_subset_union (fun (x : E × ℝ × ℝ) - (hx : fract x.2.2 ≤ 5⁻¹) ↦ lt_of_le_of_lt hx (by norm_num)) ?_ - exact fun x hx ↦ lt_of_lt_of_le (by norm_num : (3 / 4 : ℝ) < 4 / 5) hx -/ + apply union_subset_union (fun x hx ↦ lt_of_le_of_lt hx (by norm_num)) + --rw [preimage_union, preimage_union] + apply union_subset_union (fun x hx ↦ lt_of_le_of_lt hx (by norm_num : (3 / 4 : ℝ) < 4 / 5)) + apply le_of_eq + ext x + simp + sorry have h2γ₄ : EqOn γ₄ (fun x ↦ b x.1) U := by rintro ⟨x, t, s⟩ hxts simp_rw [h0γ₄, γ₃, Loop.reparam_apply] diff --git a/SphereEversion/Loops/Reparametrization.lean b/SphereEversion/Loops/Reparametrization.lean index 1a643036..9f3a1227 100644 --- a/SphereEversion/Loops/Reparametrization.lean +++ b/SphereEversion/Loops/Reparametrization.lean @@ -275,7 +275,9 @@ theorem contDiffOn_localCenteringDensity : fun x ↦ (x, x) change ContDiffOn ℝ ∞ ((w ∘ z) ∘ Prod.fst) (γ.localCenteringDensityNhd x ×ˢ (univ : Set ℝ)) rw [prod_univ] - sorry /-refine ContDiffOn.comp ?_ contDiff_fst.contDiffOn ?_--(by simp)--Subset.rfl + -- TODO: what's the right set to use? + apply ContDiffOn.comp ?_ contDiff_fst.contDiffOn (t := γ.localCenteringDensityNhd x) (by sorry) + --refine ContDiffOn.comp ?_ contDiff_fst.contDiffOn ?_--(by simp)--Subset.rfl have h₁ := contDiff_barycentric ι ℝ F (Fintype.card_fin _) (n := ∞) have h₂ : 𝒞 ∞ (eval i : (ι → ℝ) → ℝ) := contDiff_apply _ _ i refine (h₂.comp_contDiffOn h₁).comp ?_ ?_ @@ -284,7 +286,7 @@ theorem contDiffOn_localCenteringDensity : refine γ.smooth_surrounded.contDiffOn.prodMap (ContDiff.contDiffOn ?_) exact γ.approxSurroundingPointsAt_smooth x _ · intro y hy - simp [z, γ.approxSurroundingPointsAt_mem_affineBases x y hy] -/ + simp [z, γ.approxSurroundingPointsAt_mem_affineBases x y hy] · exact contDiff_deltaMollifier.comp contDiff_snd variable [FiniteDimensional ℝ E] in diff --git a/SphereEversion/ToMathlib/ExistsOfConvex.lean b/SphereEversion/ToMathlib/ExistsOfConvex.lean index 77e2accf..31b63f9c 100644 --- a/SphereEversion/ToMathlib/ExistsOfConvex.lean +++ b/SphereEversion/ToMathlib/ExistsOfConvex.lean @@ -76,15 +76,14 @@ theorem exists_contMDiff_of_convex {P : M → F → Prop} (hP : ∀ x, Convex ∃ f : M → F, CMDiff n f ∧ ∀ x, P x (f x) := by let PP : (Σ x : M, Germ (𝓝 x) F) → Prop := fun p ↦ p.2.ContMDiffAt I n ∧ P p.1 p.2.value have hPP : ∀ x : M, ReallyConvex (smoothGerm I x) {φ | PP ⟨x, φ⟩} := fun x ↦ by - sorry /- was: - apply ReallyConvex.inter - · apply reallyConvex_contMDiffAt + rw [ofPred_and] + apply (reallyConvex_contMDiffAt ..).inter let v : Germ (𝓝 x) F →ₛₗ[smoothGerm.valueRingHom I x] F := Filter.Germ.valueₛₗ I x change ReallyConvex (smoothGerm I x) (v ⁻¹' {y | P x y}) dsimp only [← smoothGerm.valueOrderRingHom_toRingHom] at v apply ReallyConvex.preimageₛₗ rw [reallyConvex_iff_convex] - apply hP -/ + apply hP have hPP' : ∀ x, ∃ f : M → F, ∀ᶠ x' in 𝓝 x, PP ⟨x', f⟩ := fun x ↦ by rcases hP' x with ⟨U, U_in, f, hf, hf'⟩ use f @@ -141,15 +140,14 @@ theorem exists_contMDiff_of_convex₂ {P : M₁ → (M₂ → F) → Prop} [Sigm let PP : (Σ x : M₁, Germ (𝓝 x) (M₂ → F)) → Prop := fun p ↦ p.2.ContMDiffAtProd I₁ I₂ n ∧ P p.1 p.2.value have hPP : ∀ x : M₁, ReallyConvex (smoothGerm I₁ x) {φ | PP ⟨x, φ⟩} := fun x ↦ by - sorry /- was: - apply ReallyConvex.inter - · apply reallyConvex_contMDiffAtProd + rw [ofPred_and] + apply (reallyConvex_contMDiffAtProd ..).inter let v : Germ (𝓝 x) (M₂ → F) →ₛₗ[smoothGerm.valueRingHom I₁ x] M₂ → F := Filter.Germ.valueₛₗ I₁ x change ReallyConvex (smoothGerm I₁ x) (v ⁻¹' {y | P x y}) dsimp only [← smoothGerm.valueOrderRingHom_toRingHom] at v apply ReallyConvex.preimageₛₗ rw [reallyConvex_iff_convex] - apply hP -/ + apply hP have hPP' : ∀ x, ∃ f : M₁ → M₂ → F, ∀ᶠ x' in 𝓝 x, PP ⟨x', f⟩ := fun x ↦ by rcases hP' x with ⟨U, U_in, f, hf, hf'⟩ use f diff --git a/SphereEversion/ToMathlib/SmoothBarycentric.lean b/SphereEversion/ToMathlib/SmoothBarycentric.lean index e1765d31..935a3ca4 100644 --- a/SphereEversion/ToMathlib/SmoothBarycentric.lean +++ b/SphereEversion/ToMathlib/SmoothBarycentric.lean @@ -136,7 +136,7 @@ theorem contDiff_barycentric [DecidablePred (· ∈ affineBases ι 𝕜 F)] [Fin simp only [Matrix.cramer_transpose_apply] have hcont : ContDiff 𝕜 n fun x : ι → F ↦ b.toMatrix x := contDiff_pi.mpr fun j ↦ contDiff_pi.mpr fun j' ↦ - ((smooth_barycentric_coord b j').of_le le_top).comp (contDiff_apply 𝕜 _ j) + ((contDiff_barycentric_coord b j').of_le le_top).comp (contDiff_apply 𝕜 _ j) have h_snd : ContDiff 𝕜 n fun x : F × (ι → F) ↦ b.toMatrix x.snd := hcont.comp contDiff_snd apply ContDiffOn.mul · apply ((Matrix.contDiff_det ι 𝕜 n).comp h_snd).contDiffOn.inv @@ -150,8 +150,8 @@ theorem contDiff_barycentric [DecidablePred (· ∈ affineBases ι 𝕜 F)] [Fin simp only [AffineBasis.toMatrix_apply, AffineBasis.coords_apply] by_cases hij : j = i · simp only [hij, ite_true] - exact (smooth_barycentric_coord b j').fst'.of_le le_top + exact (contDiff_barycentric_coord b j').fst'.of_le le_top · simp only [hij, ite_false] - exact ((smooth_barycentric_coord b j').of_le le_top).comp (contDiff_pi.mp contDiff_snd j) + exact ((contDiff_barycentric_coord b j').of_le le_top).comp (contDiff_pi.mp contDiff_snd j) end contDiff_barycentric diff --git a/lake-manifest.json b/lake-manifest.json index b796c5db..7405e78a 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "fbc1661a327737928fe9d69b74f7deaa09eecfbc", + "rev": "b575e0bbdec41cf856f3f53ee0d30f83820c645b", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "b3cc36c295aa5e3e3c0197b09a6556298e710447", + "rev": "19a8e822bfeace1ae4e090045aad81e0c930e6cf", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "17137fad38a2cc782ff00b323a13c3a991d085ab", + "rev": "ff78fbc75a9bffb4ef08f8c290e268d120cd27d7", "name": "proofwidgets", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "cbdde3aa2665915fb286c48bcd4cdf885c629511", + "rev": "29c64c56cc38211d39b306db2df11701e3d3de11", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "4453b52d2468f4c346a8711d728c0742e7483c9b", + "rev": "8e746d768c73b716c7d4bc07bd8e73f2a75bdb60", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", From f58027cec3f3eb78119c6db2d5ae534936a976a6 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Wed, 21 Oct 2026 12:28:11 +0200 Subject: [PATCH 3/3] Revert "wip trying" This reverts commit f774a654997612994ff544b04721281eb82c07f3. --- SphereEversion/Loops/Exists.lean | 13 ++++++------- SphereEversion/Loops/Reparametrization.lean | 6 ++---- 2 files changed, 8 insertions(+), 11 deletions(-) diff --git a/SphereEversion/Loops/Exists.lean b/SphereEversion/Loops/Exists.lean index 96497abd..e737848a 100644 --- a/SphereEversion/Loops/Exists.lean +++ b/SphereEversion/Loops/Exists.lean @@ -169,13 +169,12 @@ theorem exist_loops_aux2 [FiniteDimensional ℝ E] (hK : IsCompact K) (hΩ_op : in Lean 3. -/ apply hU.mem_nhdsSet.mpr - apply union_subset_union (fun x hx ↦ lt_of_le_of_lt hx (by norm_num)) - --rw [preimage_union, preimage_union] - apply union_subset_union (fun x hx ↦ lt_of_le_of_lt hx (by norm_num : (3 / 4 : ℝ) < 4 / 5)) - apply le_of_eq - ext x - simp - sorry + sorry /- proof was + refine (union_subset_union fun (x : E × ℝ × ℝ) + (hx : x.2.1 ≤ 5⁻¹) ↦ lt_of_le_of_lt hx (by norm_num)) ?_ + refine union_subset_union (fun (x : E × ℝ × ℝ) + (hx : fract x.2.2 ≤ 5⁻¹) ↦ lt_of_le_of_lt hx (by norm_num)) ?_ + exact fun x hx ↦ lt_of_lt_of_le (by norm_num : (3 / 4 : ℝ) < 4 / 5) hx -/ have h2γ₄ : EqOn γ₄ (fun x ↦ b x.1) U := by rintro ⟨x, t, s⟩ hxts simp_rw [h0γ₄, γ₃, Loop.reparam_apply] diff --git a/SphereEversion/Loops/Reparametrization.lean b/SphereEversion/Loops/Reparametrization.lean index 9f3a1227..1a643036 100644 --- a/SphereEversion/Loops/Reparametrization.lean +++ b/SphereEversion/Loops/Reparametrization.lean @@ -275,9 +275,7 @@ theorem contDiffOn_localCenteringDensity : fun x ↦ (x, x) change ContDiffOn ℝ ∞ ((w ∘ z) ∘ Prod.fst) (γ.localCenteringDensityNhd x ×ˢ (univ : Set ℝ)) rw [prod_univ] - -- TODO: what's the right set to use? - apply ContDiffOn.comp ?_ contDiff_fst.contDiffOn (t := γ.localCenteringDensityNhd x) (by sorry) - --refine ContDiffOn.comp ?_ contDiff_fst.contDiffOn ?_--(by simp)--Subset.rfl + sorry /-refine ContDiffOn.comp ?_ contDiff_fst.contDiffOn ?_--(by simp)--Subset.rfl have h₁ := contDiff_barycentric ι ℝ F (Fintype.card_fin _) (n := ∞) have h₂ : 𝒞 ∞ (eval i : (ι → ℝ) → ℝ) := contDiff_apply _ _ i refine (h₂.comp_contDiffOn h₁).comp ?_ ?_ @@ -286,7 +284,7 @@ theorem contDiffOn_localCenteringDensity : refine γ.smooth_surrounded.contDiffOn.prodMap (ContDiff.contDiffOn ?_) exact γ.approxSurroundingPointsAt_smooth x _ · intro y hy - simp [z, γ.approxSurroundingPointsAt_mem_affineBases x y hy] + simp [z, γ.approxSurroundingPointsAt_mem_affineBases x y hy] -/ · exact contDiff_deltaMollifier.comp contDiff_snd variable [FiniteDimensional ℝ E] in