|
| 1 | +/- |
| 2 | +Copyright (c) 2025 Daniele Bolla. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Daniele Bolla, David Loeffler |
| 5 | +-/ |
| 6 | +import Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse |
| 7 | +import Mathlib.Topology.Connected.PathConnected |
| 8 | + |
| 9 | +/-! |
| 10 | +# The "topologist's sine curve" is connected but not path-connected |
| 11 | +
|
| 12 | +We give an example of a closed subset `T` of `ℝ × ℝ` which is connected but not path-connected: the |
| 13 | +closure of the set `{ (x, sin x⁻¹) | x ∈ Ioi 0 }`. |
| 14 | +
|
| 15 | +## Main results |
| 16 | +
|
| 17 | +* `TopologistsSineCurve.isConnected_T`: the set `T` is connected. |
| 18 | +* `TopologistsSineCurve.not_isPathConnected_T`: the set `T` is not path-connected. |
| 19 | +
|
| 20 | +This formalization is part of the UniDistance Switzerland bachelor thesis of Daniele Bolla. A |
| 21 | +similar result has also been independently formalized by Vlad Tsyrklevich |
| 22 | +(https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/golf.20request.3A.20Topologist's.20sine.20curve). |
| 23 | +-/ |
| 24 | + |
| 25 | +open Topology Filter Set Real |
| 26 | + |
| 27 | +namespace TopologistsSineCurve |
| 28 | + |
| 29 | +/-- The topologist's sine curve, i.e. the graph of `y = sin (x⁻¹)` for `0 < x`. -/ |
| 30 | +def S : Set (ℝ × ℝ) := (fun x ↦ (x, sin x⁻¹)) '' Ioi 0 |
| 31 | + |
| 32 | +/-- The vertical line segment `{ (0, y) | -1 ≤ y ≤ 1 }`, which is the set of limit points of `S` |
| 33 | +not contained in `S` itself. -/ |
| 34 | +def Z : Set (ℝ × ℝ) := (fun y ↦ (0, y)) '' Icc (-1) 1 |
| 35 | + |
| 36 | +/-- The union of `S` and `Z` (which we will show is the closure of `S`). -/ |
| 37 | +def T : Set (ℝ × ℝ) := S ∪ Z |
| 38 | + |
| 39 | +/-- A sequence of `x`-values tending to 0 at which the sine curve has a given `y`-coordinate. -/ |
| 40 | +noncomputable def xSeq (y : ℝ) (k : ℕ) := 1 / (arcsin y + (k + 1) * (2 * π)) |
| 41 | + |
| 42 | +lemma xSeq_pos (y : ℝ) (k : ℕ) : 0 < xSeq y k := by |
| 43 | + rw [xSeq, one_div_pos] |
| 44 | + nlinarith [pi_pos, neg_pi_div_two_le_arcsin y] |
| 45 | + |
| 46 | +lemma sin_inv_xSeq {y : ℝ} (hy : y ∈ Icc (-1) 1) (k : ℕ) : sin (xSeq y k)⁻¹ = y := by |
| 47 | + simpa [xSeq, -Nat.cast_add, ← Nat.cast_succ] using sin_arcsin' hy |
| 48 | + |
| 49 | +lemma xSeq_tendsto (y : ℝ) : Tendsto (xSeq y) atTop (𝓝 0) := by |
| 50 | + refine .comp (g := fun k : ℝ ↦ 1 / (arcsin y + (k + 1) * (2 * π))) ?_ tendsto_natCast_atTop_atTop |
| 51 | + simp only [div_eq_mul_inv, show 𝓝 0 = 𝓝 (1 * (0 : ℝ)) by simp] |
| 52 | + refine (tendsto_inv_atTop_zero.comp <| tendsto_atTop_add_const_left _ _ ?_).const_mul _ |
| 53 | + exact (tendsto_atTop_add_const_right _ _ tendsto_id).atTop_mul_const (by positivity) |
| 54 | + |
| 55 | +/-! |
| 56 | +## `T` is closed |
| 57 | +-/ |
| 58 | +/-- The closure of the topologist's sine curve `S` is the set `T`. -/ |
| 59 | +lemma closure_S : closure S = T := by |
| 60 | + ext ⟨x, y⟩ |
| 61 | + -- Use sequential characterization of closure. |
| 62 | + simp only [mem_closure_iff_seq_limit, Prod.tendsto_iff] |
| 63 | + constructor |
| 64 | + · -- Show that if a sequence in `S` has a limit in `ℝ ^ 2`, the limit must be in `T`. |
| 65 | + rintro ⟨f, hf_mem, hf_lim⟩ |
| 66 | + have x_nonneg : 0 ≤ x := by |
| 67 | + refine isClosed_Ici.mem_of_tendsto hf_lim.1 (.of_forall fun n ↦ ?_) |
| 68 | + obtain ⟨y, hy⟩ := hf_mem n |
| 69 | + simpa [← hy.2] using le_of_lt hy.1 |
| 70 | + -- Case split on whether limit point `(x, y)` has `x = 0`. |
| 71 | + rcases x_nonneg.eq_or_lt with rfl | h |
| 72 | + · -- If the limit has `x = 0`, show `y`-coord must be in `[-1, 1]` using closedness |
| 73 | + right |
| 74 | + simp only [Z, mem_image, Prod.mk.injEq, true_and, exists_eq_right] |
| 75 | + refine isClosed_Icc.mem_of_tendsto hf_lim.2 (.of_forall fun n ↦ ?_) |
| 76 | + obtain ⟨y, hy⟩ := hf_mem n |
| 77 | + simpa only [Function.comp_apply, ← hy.2] using sin_mem_Icc .. |
| 78 | + · -- If the limit has `0 < x`, show `y`-coord must be `sin x⁻¹` using continuity |
| 79 | + refine .inl ⟨x, h, ?_⟩ |
| 80 | + simp only [Prod.mk.injEq, true_and] |
| 81 | + have : ContinuousAt (fun x ↦ sin x⁻¹) x := |
| 82 | + continuous_sin.continuousAt.comp <| continuousAt_inv₀ h.ne' |
| 83 | + refine tendsto_nhds_unique ?_ hf_lim.2 |
| 84 | + convert this.tendsto.comp hf_lim.1 with n |
| 85 | + obtain ⟨y, hy⟩ := hf_mem n |
| 86 | + simp [← hy.2] |
| 87 | + · -- Show that every `p ∈ T` is the limit of a sequence in `S`. |
| 88 | + rintro (hz | ⟨z, hz⟩) |
| 89 | + · -- Point is in `S`: use constant sequence |
| 90 | + exact ⟨_, fun _ ↦ hz, tendsto_const_nhds, tendsto_const_nhds⟩ |
| 91 | + · -- Point is in `Z`: use sequence from `xSeq` |
| 92 | + simp only [Prod.mk.injEq] at hz |
| 93 | + rcases hz with ⟨hz, ⟨rfl, rfl⟩⟩ |
| 94 | + refine ⟨fun n ↦ (xSeq z n, z), fun n ↦ ⟨_, xSeq_pos z n, ?_⟩, xSeq_tendsto z, |
| 95 | + tendsto_const_nhds⟩ |
| 96 | + simpa using sin_inv_xSeq hz n |
| 97 | + |
| 98 | +lemma isClosed_T : IsClosed T := by simpa only [← closure_S] using isClosed_closure |
| 99 | + |
| 100 | +/-! |
| 101 | +## `T` is connected |
| 102 | +-/ |
| 103 | +/-- `T` is connected, being the closure of the set `S` (which is obviously connected since it |
| 104 | +is a continuous image of the positive real line). -/ |
| 105 | +theorem isConnected_T : IsConnected T := by |
| 106 | + rw [← closure_S] |
| 107 | + refine (isConnected_Ioi.image _ <| continuousOn_id.prodMk ?_).closure |
| 108 | + exact continuous_sin.comp_continuousOn <| continuousOn_inv₀.mono fun _ hx ↦ hx.ne' |
| 109 | + |
| 110 | +/-! |
| 111 | +## `T` is not path-connected |
| 112 | +-/ |
| 113 | + |
| 114 | +lemma zero_mem_T : (0, 0) ∈ T := by |
| 115 | + refine .inr ⟨0, ⟨?_, ?_⟩, rfl⟩ <;> |
| 116 | + linarith |
| 117 | + |
| 118 | +/-- A point in the `body` of the topologist's sine curve. -/ |
| 119 | +noncomputable def w : ℝ × ℝ := (1, sin 1⁻¹) |
| 120 | + |
| 121 | +lemma w_mem_T : w ∈ T := .inl ⟨1, ⟨zero_lt_one' ℝ, rfl⟩⟩ |
| 122 | + |
| 123 | +private lemma norm_ge_abs_snd {a b : ℝ} : |b| ≤ ‖(a, b)‖ := by simp |
| 124 | + |
| 125 | +private lemma exists_unitInterval_gt {t₀ : unitInterval} (ht₀ : t₀ < 1) {δ : ℝ} (hδ : 0 < δ) : |
| 126 | + ∃ t₁, t₀ < t₁ ∧ dist t₀ t₁ < δ := by |
| 127 | + let s₀ := (t₀ : ℝ) -- t₀ is in unitInterval |
| 128 | + let s₁ := min (s₀ + δ / 2) 1 |
| 129 | + have h_s₀_delta_pos : 0 ≤ s₀ + δ / 2 := add_nonneg t₀.2.1 (by positivity) |
| 130 | + have hs₁ : 0 ≤ s₁ := le_min h_s₀_delta_pos zero_le_one |
| 131 | + have hs₁': s₁ ≤ 1 := min_le_right .. |
| 132 | + refine ⟨⟨s₁, hs₁, hs₁'⟩, lt_min ((lt_add_iff_pos_right _).mpr (half_pos hδ)) ht₀, ?_⟩ |
| 133 | + have h_le : s₁ ≤ s₀ + δ / 2 := min_le_left _ _ |
| 134 | + have h_ge : s₀ ≤ s₁ := le_min (by linarith) t₀.2.2 |
| 135 | + rw [Subtype.dist_eq, dist_comm, dist_eq, abs_of_nonneg (by linarith)] |
| 136 | + linarith |
| 137 | + |
| 138 | +private lemma mem_S_of_x_pos {p : ℝ × ℝ} (hx : 0 < p.1) (hT : p ∈ T) : p.2 = sin (p.1)⁻¹ := by |
| 139 | + obtain ⟨x, -, hx⟩ : p ∈ S := by |
| 140 | + cases hT with |
| 141 | + | inl hT => trivial |
| 142 | + | inr hZ => obtain ⟨y, ⟨-, rfl⟩⟩ := hZ; exact (lt_irrefl _ hx).elim |
| 143 | + simp [← hx] |
| 144 | + |
| 145 | +/-- For any `0 < a` and any `y ∈ Icc (-1) 1`, we can find `x ∈ Ioc a 0` with `sin x⁻¹ = y`. -/ |
| 146 | +lemma exists_mem_Ioc_of_y {y : ℝ} (hy : y ∈ Icc (-1) 1) {a : ℝ} (ha : 0 < a) : |
| 147 | + ∃ x ∈ Ioc 0 a, sin x⁻¹ = y := by |
| 148 | + obtain ⟨N, h_dist⟩ := (Metric.tendsto_nhds.mp (xSeq_tendsto y) (a / 2) (by positivity)).exists |
| 149 | + refine ⟨xSeq y N, ⟨xSeq_pos y N, ?_⟩, sin_inv_xSeq hy _⟩ |
| 150 | + rw [dist_eq, sub_zero, abs_of_pos (xSeq_pos _ N)] at h_dist |
| 151 | + linarith |
| 152 | + |
| 153 | +/-- The set `T` is not path-connected. -/ |
| 154 | +theorem not_isPathConnected_T : ¬ IsPathConnected T := by |
| 155 | + -- **Step 1**: |
| 156 | + -- Assume for contradiction we have a path from `z = (0, 0)` to `w = (1, sin 1)`. |
| 157 | + -- Let t₀ be the last time the path is on the y-axis. By continuity of the path, we |
| 158 | + -- can find a `δ > 0` such that for all `t ∈ [t₀, t₀ + δ]`, we have `‖p(t) - p(t₀)‖ < 1`. |
| 159 | + intro h_pathConn |
| 160 | + replace h_pathConn := h_pathConn.joinedIn (0, 0) zero_mem_T w w_mem_T |
| 161 | + let p := h_pathConn.somePath |
| 162 | + have xcoord_pathContinuous : Continuous fun t ↦ (p t).1 := continuous_fst.comp p.continuous |
| 163 | + let t₀ : unitInterval := sSup {t | (p t).1 = 0} |
| 164 | + have h_pt₀_x : (p t₀).1 = 0 := |
| 165 | + (isClosed_singleton.preimage xcoord_pathContinuous).sSup_mem ⟨0, by aesop⟩ |
| 166 | + obtain ⟨δ , hδ, ht⟩ : ∃ δ, 0 < δ ∧ ∀ t, dist t t₀ < δ → dist (p t) (p t₀) < 1 := |
| 167 | + Metric.eventually_nhds_iff.mp <| Metric.tendsto_nhds.mp (p.continuousAt t₀) _ one_pos |
| 168 | + -- **Step 2**: |
| 169 | + -- Choose a time t₁ in (t₀, t₀ + δ) and let `a = x(p(t₁))`. Using the fact that every |
| 170 | + -- connected subset of `ℝ` is an interval, we have `[0, a] ⊂ x(p([t0, t1]))`. |
| 171 | + obtain ⟨t₁, ht₁⟩ : ∃ t₁, t₀ < t₁ ∧ dist t₀ t₁ < δ := by |
| 172 | + refine exists_unitInterval_gt (lt_of_le_of_ne (unitInterval.le_one t₀) fun ht₀' ↦ ?_) hδ |
| 173 | + have w_x_path : (p 1).1 = 1 := by simp [w] |
| 174 | + have x_eq_zero : (p 1).1 = 0 := by rwa [ht₀'] at h_pt₀_x |
| 175 | + linarith |
| 176 | + let a := (p t₁).1 |
| 177 | + have ha : 0 < a := by |
| 178 | + obtain ⟨x, hxI, hx_eq⟩ : p t₁ ∈ S := by |
| 179 | + refine (h_pathConn.somePath_mem t₁).elim id fun ⟨y, hy⟩ ↦ ?_ |
| 180 | + have : (p t₁).1 = 0 := by simp only [p, ← hy.2] |
| 181 | + exact ((show t₁ ≤ t₀ from le_sSup this).not_gt ht₁.1).elim |
| 182 | + simpa only [a, ← hx_eq] using hxI |
| 183 | + have intervalAZeroSubOfT₀T₁Xcoord : Icc 0 a ⊆ (fun t ↦ (p t).1) '' Icc t₀ t₁ := |
| 184 | + (isPreconnected_Icc.image _ <| xcoord_pathContinuous.continuousOn).Icc_subset |
| 185 | + (show 0 ∈ (fun t ↦ (p t).1) '' Icc t₀ t₁ from ⟨t₀, ⟨le_rfl, ht₁.1.le⟩, ‹_›⟩) |
| 186 | + (show a ∈ (fun t ↦ (p t).1) '' Icc t₀ t₁ from ⟨t₁, ⟨ht₁.1.le, le_rfl⟩, rfl⟩) |
| 187 | + -- **Step 3**: For every `y ∈ [-1, 1]`, there exists a `t` with `p t = y` and `dist t₀ t < δ`. |
| 188 | + have exists_close {y : ℝ} (hy : y ∈ Icc (-1) 1) : ∃ t, dist t t₀ < δ ∧ (p t).2 = y := by |
| 189 | + -- first find a `t ∈ [t₀, t₁]` with this property |
| 190 | + obtain ⟨x, hx, hx'⟩ := exists_mem_Ioc_of_y hy ha |
| 191 | + obtain ⟨t, ht⟩ : ∃ t ∈ Icc t₀ t₁, (p t).1 = x := intervalAZeroSubOfT₀T₁Xcoord ⟨hx.1.le, hx.2⟩ |
| 192 | + have hp : (p t).2 = sin (p t).1⁻¹ := mem_S_of_x_pos (ht.2 ▸ hx.1) (h_pathConn.somePath_mem t) |
| 193 | + refine ⟨t, ?_, by rw [← hx', hp, ht.2]⟩ |
| 194 | + calc -- now show `t ∈ Icc t₀ t₁` implies `dist t t₀ < δ` |
| 195 | + dist t t₀ ≤ dist t₁ t₀ := dist_right_le_of_mem_uIcc (Icc_subset_uIcc' ht.1) |
| 196 | + _ = dist t₀ t₁ := by rw [dist_comm] |
| 197 | + _ < δ := ht₁.2 |
| 198 | + -- **Step 4**: |
| 199 | + -- Now the final contradiction: there are times within `δ` of `t₀` with `p t = 1`, and with |
| 200 | + -- `p t = -1`; but both must have distance `< 1` from `p t₀`, contradicting the triangle |
| 201 | + -- inequality. |
| 202 | + obtain ⟨x₁, hx₁, h_pathx₁⟩ : ∃ x₁, dist x₁ t₀ < δ ∧ (p x₁).2 = 1 := exists_close (by simp) |
| 203 | + obtain ⟨x₂, hx₂, h_pathx₂⟩ : ∃ x₂, dist x₂ t₀ < δ ∧ (p x₂).2 = -1 := exists_close (by simp) |
| 204 | + have : dist (p x₁) (p x₂) < 2 := by |
| 205 | + refine (dist_triangle_right _ _ (p t₀)).trans_lt ?_ |
| 206 | + exact (add_lt_add (ht _ hx₁) (ht _ hx₂)).trans_eq (by norm_num) |
| 207 | + have := norm_ge_abs_snd.trans_lt this |
| 208 | + rw [h_pathx₁, h_pathx₂, abs_of_nonneg (by norm_num)] at this |
| 209 | + linarith |
| 210 | + |
| 211 | +end TopologistsSineCurve |
0 commit comments