golf request: Topologist's sine curve

Stream: new members

[Vlad Tsyrklevich]

As an exercise, I wanted to try formalizing the topologist's sine curve (just the connectedness/path connectedness conditions, there is not currently a predicate for local connectedness in Mathlib) and I was surprised by how hard it was. In retrospect, I think the usual textbook proof leans heavily on the visual intuition and skips a lot of the boring details of moving between the image/preimage. Connectedness was easy, but path connectedness is what took some effort. Working with a Path constructed by choice and its input unitInterval being a subtype introduced some nitpicky inequalities that you don't think about in the informal version.

I realize it's a bit long, but I wondered if anyone had ideas on how to cut out some of the work I'm doing. In particular I wasn't sure if there was a better way of dealing with subtypes or if I could have been using non-metric parts of the Topology API to better effect.

To state the proof in words: I start by contradiction to get a path from the origin, find the supremum of the set of values for which the path is at the origin (zeroSup), then find a contradiction by showing that for any delta, there exists a value outside of the epsilon-ball at the supremum.

EDIT: One thing I considered is re-normalizing the path so that (path x).1 = x, but this seemed like it may be as much work as it saves.

import Mathlib.Analysis.Normed.Order.Lattice
import Mathlib.Data.Real.Pi.Bounds
import Mathlib.Data.Real.StarOrdered
import Mathlib.Geometry.Manifold.Instances.Real
import Mathlib.Order.CompletePartialOrder
import Mathlib.Tactic.Rify

-- #22684
/-- If a function is continuous on the union of two sets, it is continuous on both of them. -/
theorem continuousOn_of_union {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
    {s t : Set X} {f : X → Y} (h : ContinuousOn f (s ∪ t)) :
    ContinuousOn f s ∧ ContinuousOn f t :=
  ⟨fun x hx ↦ continuousWithinAt_union.mp (h x (Set.mem_union_left t hx)) |>.1,
   fun x hx ↦ continuousWithinAt_union.mp (h x (Set.mem_union_right s hx)) |>.2⟩

noncomputable abbrev fn (x : ℝ) : ℝ × ℝ := ⟨id x, Real.sin x⁻¹⟩
abbrev fn_domain := Set.Ioi (0 : ℝ)
def curve := fn '' fn_domain ∪ {(0, 0)}

private lemma sine_diverges (x y : ℝ) (hx : x > 0) (hy : -1 ≤ y ∧ y ≤ 1) :
    ∃ z : ℝ, (0 < z ∧ z < x) ∧ Real.sin z⁻¹ = y := by
  obtain ⟨n, hn⟩ := exists_nat_gt x⁻¹
  use (Real.arcsin y + (n * (2 * Real.pi)))⁻¹
  constructor
  · have := Real.monotone_arcsin hy.1
    simp only [Real.arcsin_neg, Real.arcsin_one] at this
    have : 1 ≤ (n : ℝ) := by
      have : 0 < n := by rify; linarith [inv_pos_of_pos hx]
      exact Nat.one_le_cast.mpr this
    constructor
    · apply inv_pos.mpr
      have : Real.pi < n * (2 * Real.pi) := by nlinarith [Real.pi_gt_d2]
      linarith [Real.pi_gt_d2]
    · have : x⁻¹ < Real.arcsin y + n * (2 * Real.pi) := by nlinarith [Real.pi_gt_d2]
      exact inv_lt_of_inv_lt₀ hx this
  · simp [Real.sin_arcsin' hy]

theorem connected : IsConnected curve := by
  have range : IsConnected (fn '' fn_domain) :=
    have : ContinuousOn (fun x => Real.sin x⁻¹) (Set.Ioi 0) := by
      have h₁ : ContinuousOn (fun x => Real.sin x⁻¹) {0}ᶜ :=
        ContinuousOn.comp' Real.continuousOn_sin continuousOn_inv₀ (Set.mapsTo'.mpr fun _ x => x)
      rw [Eq.symm Set.Iio_union_Ioi] at h₁
      exact continuousOn_of_union h₁ |>.2
    have : ContinuousOn fn fn_domain :=
      ContinuousOn.prod continuousOn_id this
    IsConnected.image isConnected_Ioi fn this
  have : curve ⊆ closure (fn '' fn_domain) := by
    have : 0 ∈ closure (fn '' fn_domain) := by
      apply mem_closure_iff.mpr
      intro s hopen hmem
      obtain ⟨ε, hε, hball⟩ := Metric.isOpen_iff.mp hopen 0 hmem
      obtain ⟨x, hx₁, hx₂⟩ := sine_diverges ε 0 hε (by simp)
      have : (x, 0) ∈ s := by
        have : (x, 0) ∈ Metric.ball (0 : ℝ × ℝ) ε := by
          simp only [Prod.mk_zero_zero, Metric.mem_ball, dist_zero_right, Prod.norm_mk,
            Real.norm_eq_abs, norm_zero, abs_nonneg, sup_of_le_left, abs_lt]
          constructor <;> linarith
        exact hball this
      use ⟨x, Real.sin x⁻¹⟩
      simp [hx₁, hx₂, this]
    apply Set.union_subset subset_closure
    simp [this]
  exact IsConnected.subset_closure range Set.subset_union_left this

theorem not_path_connected : ¬IsPathConnected curve := by
  by_contra hpath
  have : JoinedIn curve 0 (1, Real.sin 1) := by
    have h₁ : 0 ∈ curve := by simp [curve]
    have h₂ : (1, Real.sin 1) ∈ curve := by simp [curve]
    exact IsPathConnected.joinedIn hpath 0 h₁ (1, Real.sin 1) h₂
  obtain ⟨path, path_mem⟩ := this
  let zero : Set (ℝ × ℝ) := {0} ×ˢ Set.univ
  let zero_preimage := path ⁻¹' zero
  have : Fact ((0 : ℝ) ≤ 1) := Fact.Manifold.instLeReal
  let zeroSup := sSup zero_preimage
  have zeroSup_mem : zeroSup ∈ zero_preimage := by
    have h₁ : IsClosed zero_preimage :=
      IsClosed.preimage path.continuous (IsClosed.prod isClosed_singleton isClosed_univ)
    have : zero_preimage.Nonempty := by use 0; simp [zero_preimage, zero]
    exact IsClosed.sSup_mem this h₁
  have path₁_zeroSup : (Prod.fst ∘ path) zeroSup = 0 := by
    have (x : unitInterval) (hx : x ∈ zero_preimage) : (Prod.fst ∘ path) x = 0 := by
      simp only [Prod.mk_zero_zero, Set.singleton_prod, Set.image_univ, Set.mem_preimage,
        Set.mem_range, zero_preimage, zero] at hx
      obtain ⟨y, hy⟩ := hx
      simp [← hy]
    exact this zeroSup zeroSup_mem
  have path_zeroSup : path zeroSup = 0 := by
    have := path_mem zeroSup
    simp only [id_eq, Prod.mk_zero_zero, Set.Icc_self, Set.union_singleton, Set.mem_insert_iff,
      Set.mem_image, curve, path₁_zeroSup] at this
    rcases this with h | ⟨y, ⟨hy₁, hy₂⟩⟩
    · exact h
    · exfalso
      have := (Prod.ext_iff.mp hy₂).1
      have : (path zeroSup).1 ≠ 0 := by rw [← this]; exact Ne.symm (ne_of_lt hy₁)
      contradiction
  obtain ⟨δ, hδ₁, hδ₂⟩ := Metric.continuous_iff.mp path.continuous zeroSup 1 Real.zero_lt_one
  let zeroSup_plus_δ : unitInterval :=
    if h: zeroSup + (δ/2) ≤ 1 then
      have : zeroSup + (δ/2) ∈ unitInterval := by
        simp only [Set.mem_Icc, h, and_true]
        have : (zeroSup : ℝ) ≥ 0 := unitInterval.nonneg'
        linarith
      ⟨zeroSup + (δ/2), this⟩
    else 1
  have zeroSup_lt : zeroSup < zeroSup_plus_δ := by
    dsimp [zeroSup_plus_δ]
    split
    · change zeroSup < zeroSup + δ/2
      linarith
    · have : zeroSup ≠ 1 := by
        have : 1 ∉ zero_preimage := by simp [zero_preimage, zero]
        exact ne_of_mem_of_not_mem zeroSup_mem this
      exact unitInterval.lt_one_iff_ne_one.mpr this
  let pt := path zeroSup_plus_δ
  have pt₁_gt_zero : 0 < pt.1 := by
    have path_gt_zeroSup (x : unitInterval) (hx : x > zeroSup) : 0 < (path x).1 := by
      have : ∀ p ∈ curve, p.1 ≥ 0 := by
        simp only [id_eq, Prod.mk_zero_zero, Set.Icc_self, Set.union_singleton, Set.mem_insert_iff,
          Set.mem_image, Set.mem_Ioi, forall_eq_or_imp, Prod.fst_zero, le_refl, forall_exists_index,
          and_imp, forall_apply_eq_imp_iff₂, true_and, curve]
        intros
        linarith
      have h₁ : (path x).1 ≥ 0 := this (path x) (path_mem x)
      have h₂ : (path x).1 ≠ 0 := by
        by_contra h
        have : x ∈ zero_preimage := by simp [zero_preimage, zero, ← h]
        have : ¬(x > zeroSup) := not_lt_of_ge (CompleteLattice.le_sSup zero_preimage x this)
        contradiction
      exact lt_of_le_of_ne h₁ (Ne.symm h₂)
    exact path_gt_zeroSup zeroSup_plus_δ zeroSup_lt
  obtain ⟨x, hx₁, hx₂⟩ := sine_diverges pt.1 1 pt₁_gt_zero (by simp)
  have : x ∈ (Prod.fst ∘ path) '' (Set.Ioo zeroSup zeroSup_plus_δ) := by
    have h₁ : Set.Ioo (0 : ℝ) pt.1 ⊆ (Prod.fst ∘ path) '' (Set.Ioo zeroSup zeroSup_plus_δ) := by
      have hp : (Prod.fst ∘ path) zeroSup_plus_δ = pt.1 := rfl
      have : ContinuousOn (Prod.fst ∘ path) (Set.Icc zeroSup zeroSup_plus_δ) :=
        Continuous.continuousOn (Continuous.comp continuous_fst path.continuous)
      have := intermediate_value_Ioo (le_of_lt zeroSup_lt) this
      rwa [path₁_zeroSup, hp] at this
    have h₂ : x ∈ Set.Ioo 0 pt.1 := by rwa [Set.mem_Ioo]
    exact h₁ h₂
  obtain ⟨xinv, hxinv₁, hxinv₂⟩ := this
  have dist_xinv : dist xinv zeroSup < δ := by
    have : dist zeroSup_plus_δ zeroSup < δ := by
      dsimp [zeroSup_plus_δ]
      split
      · change dist (zeroSup + δ / 2) (zeroSup) < δ
        simp [abs_of_nonneg, le_of_lt, hδ₁]
      · simp only [dist, Set.Icc.coe_one, unitInterval.one_minus_nonneg zeroSup, abs_of_nonneg]
        linarith
    have : dist xinv zeroSup ≤ dist zeroSup_plus_δ zeroSup := by
      simp [dist, abs_of_nonneg, le_of_lt, Set.mem_Ioo.mp hxinv₁, zeroSup_lt]
    linarith
  have path_xinv : path xinv = ⟨x, 1⟩ := by
    simp only [Prod.mk_zero_zero, Function.comp_apply] at hxinv₂
    apply Prod.ext hxinv₂
    have := path_mem xinv
    simp only [Prod.mk_zero_zero, Set.Icc_self, Set.union_singleton, Set.mem_insert_iff,
      Set.mem_image, curve] at this
    rcases this with h | ⟨y, ⟨hy₁, hy₂⟩⟩
    · exfalso
      have : (path xinv).1 = 0 := (Prod.ext_iff.mp h).1
      linarith
    · have := Prod.ext_iff.mp hy₂
      simp only [id_eq, hxinv₂] at this
      simp [← hx₂, ← this.2, this.1]
  specialize hδ₂ xinv dist_xinv
  simp [path_zeroSup, path_xinv] at hδ₂

[Michael Rothgang]

(There is docs#LocallyConnectedSpace, but no notion of locally connected sets. This would be a welcome addition, though!)

[Michael Rothgang]

Would you like to PR this definition to mathlib - after it has been golfed? (To the Counterexamples directory, for instance.)

[Vlad Tsyrklevich]

I thought about it, it's a well-known example, but given the amount of fiddly manipulation required I wasn't sure if it's a good candidate. If others think it'd make a good candidate I'd be happy to

[Michael Rothgang]

In any case, here are some ideas for golfing/stylistic comments:

• you can use dot notation to make your code more concise
  For example, IsConnected.image isConnected_Ioi fn this can equivalently be written as
  isConnected_Ioi.image fn this: Lean knows that isConnected_Ioi is type IsConnected ...,
  and deduces that you mean to apply the lemma IsConnected.image.

• you can inline some very short haves: combined with the previous point,

    have : ContinuousOn fn fn_domain :=
      ContinuousOn.prod continuousOn_id this
    IsConnected.image isConnected_Ioi fn this

could become isConnected_Ioi.image fn (continuousOn_id.prod this).

• your proofs have a lot of have's: often, it makes sense to promote them to individual lemmas
  (Mathlib code has a lot more lemmas than you'd see in a textbook or paper.)

[Vlad Tsyrklevich]

Thanks for the feedback! Originally I thought, there's no way I can split this up more, the logic is too intertwined, but that was clearly wrong. I did manage to split it up more so the proof of non-path-connectedness is now actually fairly short, now the path-renormalization is the ugliest bit, but still, I feel like I've learned more about how to work with mathlib in all of it this. I'll post the current state in case anyone cares to offer more feedback.

import Mathlib.Analysis.Normed.Order.Lattice
import Mathlib.Data.Real.Pi.Bounds
import Mathlib.Data.Real.StarOrdered
import Mathlib.Geometry.Manifold.Instances.Real
import Mathlib.Order.CompletePartialOrder
import Mathlib.Tactic.Rify

-- #22684
/-- If a function is continuous on the union of two sets, it is continuous on both of them. -/
theorem continuousOn_of_union {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
    {s t : Set X} {f : X → Y} (h : ContinuousOn f (s ∪ t)) :
    ContinuousOn f s ∧ ContinuousOn f t :=
  ⟨fun x hx ↦ continuousWithinAt_union.mp (h x (Set.mem_union_left t hx)) |>.1,
   fun x hx ↦ continuousWithinAt_union.mp (h x (Set.mem_union_right s hx)) |>.2⟩

noncomputable abbrev fn (x : ℝ) : ℝ × ℝ := ⟨x, Real.sin x⁻¹⟩
abbrev fn_domain := Set.Ioi (0 : ℝ)
abbrev curve := fn '' fn_domain ∪ {0}

private lemma sine_diverges (x y : ℝ) (hx : x > 0) (hy : -1 ≤ y ∧ y ≤ 1) :
    ∃ z : ℝ, (0 < z ∧ z < x) ∧ Real.sin z⁻¹ = y := by
  obtain ⟨n, hn⟩ := exists_nat_gt x⁻¹
  use (Real.arcsin y + (n * (2 * Real.pi)))⁻¹
  constructor
  · have := Real.monotone_arcsin hy.1
    simp only [Real.arcsin_neg, Real.arcsin_one] at this
    have : 1 ≤ (n : ℝ) := by
      have : 0 < n := by rify; linarith [inv_pos_of_pos hx]
      exact Nat.one_le_cast.mpr this
    constructor
    · apply inv_pos.mpr
      nlinarith [Real.pi_gt_d2]
    · have : x⁻¹ < Real.arcsin y + n * (2 * Real.pi) := by nlinarith [Real.pi_gt_d2]
      exact inv_lt_of_inv_lt₀ hx this
  · simp [Real.sin_arcsin' hy]

theorem connected : IsConnected curve := by
  have range : IsConnected (fn '' fn_domain) := by
    apply isConnected_Ioi.image fn <| continuousOn_id.prod _
    apply ContinuousOn.mono
    · exact Real.continuousOn_sin.comp' continuousOn_inv₀ (Set.mapsTo'.mpr fun _ x ↦ x)
    · simp
  have : curve ⊆ closure (fn '' fn_domain) := by
    refine Set.union_subset subset_closure <| Set.singleton_subset_iff.mpr <| mem_closure_iff.mpr ?_
    intro s hopen hmem
    obtain ⟨ε, hε, hball⟩ := Metric.isOpen_iff.mp hopen 0 hmem
    obtain ⟨x, hx₁, hx₂⟩ := sine_diverges ε 0 hε (by simp)
    use ⟨x, Real.sin x⁻¹⟩
    have : (x, 0) ∈ s := by
      apply hball
      simp [abs_lt, hx₁, show -ε < x by linarith]
    simp [hx₂, hx₁, this]
  exact IsConnected.subset_closure range Set.subset_union_left this

lemma renormalize_path2 {X : Type*} [TopologicalSpace X] [T1Space X] {x y : X} {F : Set X}
    (joined : JoinedIn F x y) (h : x ≠ y) : ∃ p : Path x y, (∀ i, p i ∈ F) ∧ ∀ i > 0, p i ≠ x := by
  haveI : Fact ((0 : ℝ) ≤ 1) := Fact.Manifold.instLeReal -- TODO
  obtain ⟨path, path_mem⟩ := joined
  let preimage := path ⁻¹' {x}
  let xSup := sSup preimage
  have xSup_mem : xSup ∈ preimage := by
    have : preimage.Nonempty := by use 0; simp [preimage]
    exact IsClosed.sSup_mem this <| IsClosed.preimage path.continuous isClosed_singleton
  have path_xSup_eq : path xSup = x := by
    simpa only [Set.mem_preimage, Set.mem_singleton_iff, preimage] using xSup_mem
  let δ : ℝ := 1 - xSup
  have lt_δ : 0 < δ :=
    have : xSup < 1 := by
      refine unitInterval.lt_one_iff_ne_one.mpr ?_
      by_contra hh
      simp [Ne.symm h, hh] at path_xSup_eq
    sub_pos.mpr this
  have (i : unitInterval) : (xSup : ℝ) + (i : ℝ) * δ ∈ unitInterval := by
    have : δ * (i : ℝ) ≤ 1 - xSup := mul_le_iff_le_one_right lt_δ |>.mpr <| unitInterval.le_one i
    have : 0 ≤ (xSup : ℝ) := unitInterval.nonneg'
    have : 0 ≤ (i : ℝ) := unitInterval.nonneg'
    constructor
    · positivity
    · linarith
  let newPath : Path x y := {
    toFun := fun i ↦ path ⟨xSup + i * δ, this i⟩
    continuous_toFun := by
      refine path.continuous.comp' <| Continuous.subtype_mk ?_ this
      exact continuous_const.add <| continuous_subtype_val.mul continuous_const
    source' := by simp [path_xSup_eq]
    target' := by simp [δ]
  }
  use newPath
  constructor
  · simp [newPath, path_mem]
  · intro i hi
    have : (i : ℝ) * δ > 0 := mul_pos hi lt_δ
    have : xSup + (i : ℝ) * δ > xSup := by linarith
    have h (y : unitInterval) (h : y > xSup) : path y ≠ x := by
      by_contra hcontra
      have : y ∈ preimage := by simp [preimage, hcontra]
      have : ¬ sSup preimage < y:= by simp [le_sSup this]
      simp [xSup] at h
      contradiction
    exact h _ this

lemma path_intermediate_value {x y : ℝ × ℝ} {i₁ i₂ : unitInterval} {p p₁ p₂ : ℝ} (path : Path x y)
    (hi : i₁ < i₂) (hp₁ : (path i₁).1 = p₁) (hp₂ : (path i₂).1 = p₂) (hp : p₁ < p ∧ p < p₂) :
    ∃ i, (i₁ < i ∧ i < i₂) ∧ (path i).1 = p := by
  haveI : Fact ((0 : ℝ) ≤ 1) := Fact.Manifold.instLeReal -- TODO
  have h₁ : Set.Ioo p₁ p₂ ⊆ (Prod.fst ∘ path) '' (Set.Ioo i₁ i₂) := by
    have :=
      intermediate_value_Ioo (le_of_lt hi) <| continuous_fst.comp path.continuous |>.continuousOn
    simpa [hp₁, hp₂] using this
  have h₂ : p ∈ Set.Ioo p₁ p₂ := by rwa [Set.mem_Ioo]
  exact h₁ h₂

lemma curve_point_gt_zero {x : ℝ × ℝ} (h₁ : x ∈ curve) (h₂ : x.1 > 0) :
    x = (x.1, Real.sin (x.1)⁻¹) := by
  simp only [Prod.mk_zero_zero, Set.Icc_self, Set.union_singleton, Set.mem_insert_iff,
    Set.mem_image, curve] at h₁
  rcases h₁ with h | ⟨y, ⟨hy₁, hy₂⟩⟩
  · exfalso
    have : x.1 = 0 := (Prod.ext_iff.mp h).1
    linarith
  · have := Prod.ext_iff.mp hy₂
    simp only [id_eq] at this
    apply Prod.ext <;> simp [← this.2, this.1]

theorem not_path_connected : ¬IsPathConnected curve := by
  haveI : Fact ((0 : ℝ) ≤ 1) := Fact.Manifold.instLeReal -- TODO
  by_contra hpconn
  have := hpconn.joinedIn 0 (by simp) (1, Real.sin 1) (by simp)
  obtain ⟨path, path_mem, hpath⟩ := renormalize_path2 this (by simp [Prod.ext_iff])
  obtain ⟨δ, hδ₁, hδ₂⟩ := Metric.continuous_iff.mp path.continuous 0 1 Real.zero_lt_one
  let δstep : unitInterval := ⟨δ/2 ⊓ 1, by simp; linarith⟩
  have δstep_gt : 0 < δstep := by simp [δstep, Subtype.mk_lt_mk.mpr, hδ₁]
  let pt := path δstep
  have pt₁_gt_zero : 0 < pt.1 :=
    have path_gt (y : unitInterval) (hy : y > 0) : 0 < (path y).1 := by
      have : ∀ p ∈ curve, p = 0 ∨ 0 < p.1 := by simp_all
      rcases this (path y) (path_mem _) with h | h
      · exact False.elim (hpath y hy h)
      · exact h
    path_gt δstep δstep_gt
  obtain ⟨x, hx₁, hx₂⟩ := sine_diverges pt.1 1 pt₁_gt_zero (by simp)
  obtain ⟨xinv, hxinv₁, hxinv₂⟩ := path_intermediate_value path δstep_gt (by simp) rfl hx₁
  have dist_xinv : dist xinv 0 < δ := by
    have : ↑xinv < δ := lt_trans (Set.mem_Ioo.mp hxinv₁).2 (by simp [δstep, hδ₁])
    simp [dist, abs_of_nonneg, le_of_lt, Set.mem_Ioo.mp hxinv₁, this]
  have path_xinv := curve_point_gt_zero (path_mem xinv) (by simp [hxinv₂, hx₁])
  rw [hxinv₂, hx₂] at path_xinv
  specialize hδ₂ xinv dist_xinv
  simp [path_xinv, hxinv₂] at hδ₂

[Jireh Loreaux]

I would probably rephrase sine_diverges into something like this:

open Filter Real

example (y : ℝ) (hy₁ : -1 ≤ y) (hy₂ : y ≤ 1) : ∃ᶠ x in atTop, sin x = y := sorry

Then you get the the related result that you want, namely

open Filter Real Topology

example (y : ℝ) (hy₁ : -1 ≤ y) (hy₂ : y ≤ 1) : ∃ᶠ x in 𝓝[>] 0, sin x⁻¹ = y := sorry

by using docs#Filter.frequently_map and docs#inv_atTop₀.

In fact, the first result generalizes to any periodic function on ℝ (and can probably be generalized even further to other domains like ordered additive commutatve monoids where Tendsto (fun n : ℕ ↦ n • c) atTop atTop where c is the period of the function, and if you get this, then you can even multiplicativize the result).

open Filter

lemma Function.Periodic.frequently_atTop_real_eq : {β : Type*} {f : ℝ → β}
    {c : ℝ} (hf : f.Periodic c) (hc : c ≠ 0) {y : β} (hy : y ∈ Set.Range f) :
    ∃ᶠ x in atTop, f x = y :=
  sorry