[Merged by Bors] - feat(Counterexamples): topologists' sine curve#25833
[Merged by Bors] - feat(Counterexamples): topologists' sine curve#25833loefflerd wants to merge 16 commits intoleanprover-community:masterfrom
Conversation
PR summary 2f145f4e8cImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
sgouezel
left a comment
There was a problem hiding this comment.
This looks great, thanks!
Co-authored-by: Sebastien Gouezel <sebastien.gouezel@univ-rennes1.fr>
|
Thanks Sebastien for the review! I have applied all the changes you suggested. |
Ruben-VandeVelde
left a comment
There was a problem hiding this comment.
Thanks, this all looks reasonable enough. Some small comments below
|
Jireh has thoughts he'll try to post soon |
|
Thanks Ruben for the review! I have made the changes you suggested, other than the issues with lemma naming. I have no particular attachment to the existing names, and I'm happy to rename them to something else if you have a suggestion; but since these lemmas aren't intended for re-use outside this particular context, and hence don't have particularly tidy or natural statements, it's harder to come up with especially snappy names for them. |
|
@j-loreaux I hear you have thoughts about this PR. Would you like to leave them here, and take care of reviewing this PR? |
There was a problem hiding this comment.
Sorry it has taken me a long time to get around to this. The generic nature of my thoughts are that I wanted some higher level machinery to prove all this. After playing around with it a bit, while it would be nice to have, I don't think I want to require it for merging this PR. My approach would involve almost a complete rewrite.
Nevertheless, let me describe my ideas, in case you are interested.
- The first bit concerns proving
closure S = T. It felt like this was too hard. After all the generic idea is: we only have to pay attention to what happens at𝓝[>] 0andatTop. In particulaar, this idea can be encapsulated in the following theorem, which is missing in Mathlib:
lemma closure_range_eq_range_union_setOf_mapClusterPt {X Y : Type*}
[TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {f : X → Y} (hf : Continuous f) :
closure (range f) = range f ∪ {y | MapClusterPt y (cocompact X) f} := by
refine subset_antisymm (fun y hy' ↦ ?_) ?_
· simp only [mem_union, mem_setOf_eq, or_iff_not_imp_right]
intro hy
have key : Disjoint (comap f (𝓝 y)) (cocompact X) := by
rw [disjoint_iff_inf_le]
calc
comap f (𝓝 y) ⊓ cocompact X
_ ≤ comap f (𝓝 y) ⊓ comap f (map f (cocompact X)) := by gcongr; exact le_comap_map
_ = comap f (𝓝 y ⊓ map f (cocompact X)) := by simp
_ = ⊥ := by convert comap_bot; simpa [MapClusterPt, ClusterPt] using hy
obtain ⟨k, hky, hk⟩ := disjoint_cocompact_right _ |>.mp key
rw [← le_principal_iff] at hky
have : (comap f (𝓝 y)).NeBot := by
rwa [comap_neBot_iff_frequently, ← mem_closure_iff_frequently]
obtain ⟨x, hxk, hx⟩ := hk hky
rw [ClusterPt] at hx
have h : Tendsto f (𝓝 x ⊓ comap f (𝓝 y)) (𝓝 y) :=
le_trans (by gcongr; exact inf_le_right) map_comap_le
exact ⟨x, tendsto_nhds_unique (hf.tendsto x |>.mono_left inf_le_left) h⟩
· refine union_subset subset_closure fun y hy ↦ ?_
rw [mem_closure_iff_clusterPt, ← map_top]
exact ClusterPt.mono hy (by simp)Of course, this concerns the range, not the image of a set, but you can recover the range by working with the subtype Iio 0 instead. From there you can pretty quickly get the intuition I had indicated:
/-!
## `T` is closed
-/
/-- The closure of the topologist's sine curve `S` is the set `T`. -/
lemma closure_S : closure S = T := by
rw [S]
have : (fun x ↦ (x, sin x⁻¹)) '' Ioi (0 : ℝ) =
range ((fun x ↦ (x, sin x⁻¹)) ∘ ((↑) : Ioi (0 : ℝ) → ℝ)) := by
simp [Set.range_comp, Ioi]
rw [this, closure_range_eq_range_union_setOf_mapClusterPt ?continuity, ← this, T, S]
case continuity => fun_prop (disch := aesop)
congr!
ext p
have : CompactIccSpace (Ioi (0 : ℝ)) := sorry -- we should have this
simp [mapClusterPt_comp]
simp [MapClusterPt, clusterPt_sup]
-- ⊢ ClusterPt p (map (fun x ↦ (x, sin x⁻¹)) (𝓝[>] 0)) ∨ ClusterPt p (map (fun x ↦ (x, sin x⁻¹)) atTop) ↔ p ∈ Z
sorryIn order to discharge this goal, it's helpful to have a few other things, one of which we're missing.
-- `ℝ` can probably be generalized a bit here,
-- of course there's an analogous one for `atBot`.
lemma _root_.Function.Periodic.map_atTop {α : Type*} {f : ℝ → α} {c : ℝ}
(hf : Function.Periodic f c) :
map f atTop = 𝓟 (Set.range f) := by
sorry
lemma _root_.Real.map_sin_atTop : map sin atTop = 𝓟 (Icc (-1) 1) := by
simpa using Real.sin_periodic.map_atTop
lemma _root_.Real.map_sin_inv_nhdsGT_zero :
map (fun x ↦ sin x⁻¹) (𝓝[>] 0) = 𝓟 (Icc (-1) 1) := by
simpa [← Function.comp_def, ← map_map] using Real.map_sin_atTop
lemma frequently_eq_of_mem_Icc (y : ℝ) (hy : y ∈ Icc (-1) 1) :
∃ᶠ x in 𝓝[>] 0, sin x⁻¹ = y := by
rw [← Filter.frequently_map (m := (fun x ↦ sin x⁻¹)) (P := (· = y)), map_sin_inv_nhdsGT_zero]
simp_allThis allows you to prove, using Filter.le_map_prod_fst_snd that if ClusterPt p (map (fun x ↦ (x, sin x⁻¹)) (𝓝[>] 0)), then ClusterPt p (𝓟 ({0} ×ˢ Icc (-1) 1), and since this set is closed, that means p ∈ Z. Similarly, you can show that ClusterPt p (map (fun x ↦ (x, sin x⁻¹)) atTop) is impossible because, if it were true then composing with Prod.fst would yield ClusterPt p.fst atTop, which is easily seen to be impossible.
So, if any of this interests you, you're welcome to try it out, but I won't require it. If you choose not to take this approach, you may merge.
bors d+
|
✌️ loefflerd can now approve this pull request. To approve and merge a pull request, simply reply with |
|
Dear Jireh: Many thanks for your comments on this PR. I do agree that this alternative approach would be somewhat slicker; and I will go over your message together with Daniele, once the next semester starts, and look into contributing some of the lemmas you've suggested to Mathlib and using them to shorten the proof. But since this PR has been open for several months now, I'd rather merge the PR as it stands and make optimisations later. (Did you have other comments, by the way? You wrote "1. The first bit concerns ..." but there doesn't seem to be a second bit.) bors r+ |
Define the "topologists' sine curve" in R^2, and show that its closure is connected but not path-connected. This formalization is part of the bachelor thesis of Daniele Bolla at UniDistance Switzerland. Co-authored-by: Daniele Bolla [daniele.bolla@stu.fernuni.ch](mailto:daniele.bolla@stu.fernuni.ch)
|
Pull request successfully merged into master. Build succeeded: |
* origin/master: (508 commits) feat(Logic/Basic): forall_and_index (leanprover-community#27737) feat(Algebra/intNorm): `x` divides `intNorm x` (leanprover-community#28021) feat(RingTheory/MvPolynomial/MonomialOrder): some lemmas about degree (leanprover-community#26000) chore: more elementary Motzkin polynomial proof (leanprover-community#28482) feat: e-seminormed monoid (leanprover-community#27385) feat(RingTheory): ` (⊥ : Ideal R) ^ n = ⊥` (leanprover-community#28171) fix(LinearAlgebra/Dimension/ErdosKaplansky): authorship (leanprover-community#28513) chore: golf entire `X_pow_eq_monomial` (leanprover-community#28504) feat(RingTheory): invertible modules and Picard group (leanprover-community#25337) chore: use delta `deriving` for leanprover-community#380 (leanprover-community#28498) feat: add bilinear maps for vector/matrix products (leanprover-community#28130) feat(Counterexamples): topologists' sine curve (leanprover-community#25833) feat(Analysis/Convex): doubly stochastic matrices have operator norm at most one (leanprover-community#28453) chore(Topology/Compactification): deprecate duplicate `ultrafilter_pure_injective` (leanprover-community#28436) feat: add `@[simp]` to `Multiset.cons_le_cons` and `Finset.insert_subset_insert` (leanprover-community#28285) feat: make `ring` work for semifields (leanprover-community#28494) feat: filtering lists and bounded quantifiers are primitive recursive (leanprover-community#26295) chore(Analysis/Analytic): split `Analytic.Basic` (leanprover-community#26270) refactor: tidy `mulVec` and `vecMul` lemmas about `•` (leanprover-community#28450) feat(Order/WellFounded): Acc and infinite descending chain (leanprover-community#28120) feat(NumberTheory/Padics): {Int,Rat}.padicValuation (leanprover-community#27667) chore(*): address a few timeout-related porting notes (leanprover-community#28483) feat(Algebra): toAlgebra_algebraMap (leanprover-community#28238) feat(Shrink): `IsCancelMul` instance (leanprover-community#28407) chore(Geometry): golf entire `chart_eq'` and `orthogonalProjection_orthogonalProjection` (leanprover-community#28485) feat: shifted geometric series and a `ProbabilityMeasure` version of `measure_iUnion_le` (leanprover-community#28087) chore(LinearAlgebra/PiTensorProduct): `rw` away use of `erw` in `lifts_zero` (leanprover-community#27554) feat(RingTheory): faithfully flat ring maps (leanprover-community#24530) chore(Geometry/RingedSpace): remove use of `erw` in `stalkSpecializes_stalkMap` (leanprover-community#27656) chore: add the Brownian motion project to downstream_repos.yml (leanprover-community#28459) feat(CategoryTheory/Sites/SheafOfTypes): composition of a sheaf with uliftFunctor is still a sheaf (leanprover-community#27816) feat(Valuation/DiscreteValuationRel): val relations with compatible valuations to Zm0 are IsDiscrete (leanprover-community#27213) chore(*): process a bunch of `aesop`-related porting notes (leanprover-community#28402) feat(CategoryTheory): abstract argument for the stability under transfinite compositions (leanprover-community#26030) chore: bump toolchain to v4.23.0-rc2 (leanprover-community#28454) chore(FieldTheory/Finite): fermat's little theorem in Nat form (leanprover-community#27962) feat(Combinatorics/SimpleGraph/Paths): add theorem `SimpleGraph.Walk.IsPath.concat` (leanprover-community#27582) feat(Slope): slope_pos_iff_of_le and related lemmas (leanprover-community#28039) feat: tactic analysis framework (leanprover-community#26683) chore(Data/EReal): deprecate `add_pos_of_nonneg_of_pos` and `add_ne_top_iff_of_ne_bot` (duplicates) (leanprover-community#28424) feat(MathlibTest/FieldSimp): add a few more tests (leanprover-community#28413) chore(RingTheory/HahnSeries): deprecate duplicate `orderTop_add_orderTop_le_orderTop_mul` (leanprover-community#28231) chore(AlgebraicGeometry/IdealSheaf): deprecate duplicate `AlgebraicGeometry.Scheme.IdealSheafData.Scheme.zeroLocus_radical` (leanprover-community#28202) feat(Algebra/Order): ArchimedeanClass ball (leanprover-community#27885) chore(Geometry/RingedSpace): remove use of `erw` in `isUnit_of_isUnit_germ` (leanprover-community#27660) feat(SkewMonoidAlgebra): coeff_mul lemmas (leanprover-community#27255) chore(LinearAlgebra): golf entire `isUnit_det` (leanprover-community#28438) chore(FieldTheory/IntermediateField): golf entire `coe_sum` and `coe_prod` (leanprover-community#28431) feat: separate linter error message for empty doc-strings (leanprover-community#27895) feat(RingTheory/PowerSeries/Binomial): add basic lemmas, golf (leanprover-community#27497) ...
…25833) Define the "topologists' sine curve" in R^2, and show that its closure is connected but not path-connected. This formalization is part of the bachelor thesis of Daniele Bolla at UniDistance Switzerland. Co-authored-by: Daniele Bolla [daniele.bolla@stu.fernuni.ch](mailto:daniele.bolla@stu.fernuni.ch)
…25833) Define the "topologists' sine curve" in R^2, and show that its closure is connected but not path-connected. This formalization is part of the bachelor thesis of Daniele Bolla at UniDistance Switzerland. Co-authored-by: Daniele Bolla [daniele.bolla@stu.fernuni.ch](mailto:daniele.bolla@stu.fernuni.ch)
Define the "topologists' sine curve" in R^2, and show that its closure is connected but not path-connected.
This formalization is part of the bachelor thesis of Daniele Bolla at UniDistance Switzerland.
Co-authored-by: Daniele Bolla daniele.bolla@stu.fernuni.ch