Formal Code Quality

Original model output, including both modified modules. Download patch

diff --git a/Mathlib/Analysis/Real/OfDigits.lean b/Mathlib/Analysis/Real/OfDigits.lean
index f206d72c68..88342f00e0 100644
--- a/Mathlib/Analysis/Real/OfDigits.lean
+++ b/Mathlib/Analysis/Real/OfDigits.lean
@@ -101,6 +101,34 @@ theorem abs_ofDigits_sub_ofDigits_le {b : ℕ} {x y : ℕ → Fin b} {n : ℕ}
     (ofDigits_nonneg _) (ofDigits_le_one _)
   simp
 
+theorem continuous_ofDigits {b : ℕ} :
+    Continuous (ofDigits : (ℕ → Fin b) → ℝ) := by
+  rw [continuous_iff_continuousAt]
+  intro x
+  change Filter.Tendsto ofDigits (nhds x) (nhds (ofDigits x))
+  rw [Metric.tendsto_nhds]
+  intro ε hε
+  obtain rfl | hb := (Nat.one_le_of_lt (b_pos x)).eq_or_lt
+  · filter_upwards [] with y
+    have hy : y = x := Subsingleton.elim y x
+    subst y
+    simp [hε]
+  have hpow : Filter.Tendsto (fun n : ℕ => ((b : ℝ) ^ n)⁻¹) Filter.atTop (nhds 0) := by
+    simpa [inv_pow] using
+      (tendsto_pow_atTop_nhds_zero_of_abs_lt_one (r := (b : ℝ)⁻¹) (by
+        rw [abs_of_nonneg]
+        · have hb' : (1 : ℝ) < b := by exact_mod_cast hb
+          exact (inv_lt_one₀ (by positivity)).2 hb'
+        positivity))
+  obtain ⟨n, hn⟩ := (Metric.tendsto_atTop.1 hpow ε hε)
+  have hnhds : (Set.Iio n).pi (fun i => {x i}) ∈ nhds x :=
+    set_pi_mem_nhds (Set.finite_Iio n) fun i hi => by
+      exact mem_nhds_iff.2 ⟨{x i}, subset_rfl, isOpen_discrete _, rfl⟩
+  filter_upwards [hnhds] with y hy
+  exact lt_of_le_of_lt (abs_ofDigits_sub_ofDigits_le (fun i hi => by
+    rw [Set.mem_pi] at hy
+    exact hy i hi) (n := n)) (by simpa using hn n le_rfl)
+
 /-- Converts a real number `x` from the interval `[0, 1)` into sequence of
 its digits in base `b`. -/
 noncomputable def digits (x : ℝ) (b : ℕ) [NeZero b] : ℕ → Fin b :=
diff --git a/Mathlib/Topology/Instances/CantorSet.lean b/Mathlib/Topology/Instances/CantorSet.lean
index a1a1324c55..4a53e15de8 100644
--- a/Mathlib/Topology/Instances/CantorSet.lean
+++ b/Mathlib/Topology/Instances/CantorSet.lean
@@ -312,4 +312,44 @@ theorem cantorSet_eq_zero_two_ofDigits :
   · rw [← ha.right]
     exact ofDigits_zero_two_sequence_mem_cantorSet ha.left
 
+/-- The ternary Cantor set is homeomorphic to the space of Boolean sequences. -/
+noncomputable def cantorSetHomeomorphNatBool : cantorSet ≃ₜ (ℕ → Bool) := by
+  let ternary (a : ℕ → Bool) : ℕ → Fin 3 := fun n => if a n then 2 else 0
+  let f : (ℕ → Bool) → cantorSet := fun a =>
+    ⟨ofDigits (ternary a), ofDigits_zero_two_sequence_mem_cantorSet (by
+      intro n
+      cases h : a n <;> simp [ternary, h])⟩
+  have hternary : Continuous ternary := by
+    apply continuous_pi
+    intro n
+    simpa [ternary, Function.comp_def] using
+      ((continuous_of_discreteTopology :
+          Continuous (fun z : Bool => if z then (2 : Fin 3) else 0)).comp (continuous_apply n))
+  have hf : Continuous f := by
+    apply Continuous.subtype_mk
+    exact (Real.continuous_ofDigits).comp hternary
+  have hinj : Function.Injective f := by
+    intro a b hab
+    apply funext
+    intro n
+    have h : ternary a = ternary b :=
+      ofDigits_zero_two_sequence_unique
+        (by intro n; cases h : a n <;> simp [ternary, h])
+        (by intro n; cases h : b n <;> simp [ternary, h])
+        (congrArg Subtype.val hab)
+    have := congrFun h n
+    cases ha : a n <;> cases hb : b n <;> simp [ternary, ha, hb] at this ⊢
+  have hsurj : Function.Surjective f := by
+    intro x
+    let a : ℕ → Bool := fun n => decide ((cantorToTernary x.1).get n = 2)
+    have ha : ternary a = (cantorToTernary x.1).get := by
+      funext n
+      have hn := cantorToTernary_ne_one (x := x.1) (n := n)
+      generalize hd : (cantorToTernary x.1).get n = d at hn ⊢
+      fin_cases d <;> simp [a, ternary, hd] at hn ⊢
+    refine ⟨a, ?_⟩
+    apply Subtype.ext
+    simpa [f, a, ha] using ofDigits_cantorToTernary x.2
+  exact ((hf.isClosedEmbedding hinj).toHomeomorphOfSurjective hsurj).symm
+
 end ternary02

Original model output, including both modified modules. Download patch

diff --git a/Mathlib/Analysis/Real/OfDigits.lean b/Mathlib/Analysis/Real/OfDigits.lean
index f206d72c68..03d3f34dc5 100644
--- a/Mathlib/Analysis/Real/OfDigits.lean
+++ b/Mathlib/Analysis/Real/OfDigits.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Vasilii Nesterov
 -/
 import Mathlib.Algebra.Order.Floor.Semifield
+import Mathlib.Analysis.Normed.Group.FunctionSeries
 import Mathlib.Analysis.SpecificLimits.Normed
 import Mathlib.Tactic.Rify
 
@@ -101,6 +102,35 @@ theorem abs_ofDigits_sub_ofDigits_le {b : ℕ} {x y : ℕ → Fin b} {n : ℕ}
     (ofDigits_nonneg _) (ofDigits_le_one _)
   simp
 
+/-- Interpreting a sequence of digits as a real number is continuous. -/
+theorem continuous_ofDigits (b : ℕ) : Continuous (ofDigits : (ℕ → Fin b) → ℝ) := by
+  rcases b with _ | b
+  · letI : IsEmpty (ℕ → Fin 0) := ⟨fun x ↦ Fin.elim0 (x 0)⟩
+    rw [continuous_def]
+    intro s hs
+    convert isOpen_empty
+    exact Set.eq_empty_iff_forall_notMem.mpr fun x _ ↦ isEmptyElim x
+  · rcases b with _ | b
+    · convert (continuous_const : Continuous fun _ : ℕ → Fin 1 ↦ (0 : ℝ)) using 1
+      funext x
+      simp [ofDigits, ofDigitsTerm]
+    change Continuous fun x : ℕ → Fin (b + 2) ↦ ∑' n, ofDigitsTerm x n
+    apply continuous_tsum (u := fun n ↦ (b + 1 : ℝ) * ((b + 2 : ℝ) ^ (n + 1))⁻¹)
+    · intro n
+      unfold ofDigitsTerm
+      fun_prop
+    · simp_rw [pow_succ', mul_inv, ← inv_pow, ← mul_assoc]
+      exact Summable.mul_left _ <| summable_geometric_of_lt_one (by positivity) (by
+        apply (inv_lt_one₀ (by positivity)).mpr
+        have : 0 ≤ (b : ℝ) := by positivity
+        linarith)
+    · intro n x
+      rw [Real.norm_eq_abs, abs_of_nonneg ofDigitsTerm_nonneg]
+      have h := ofDigitsTerm_le (digits := x) (n := n)
+      norm_num [Nat.cast_add, Nat.cast_ofNat] at h ⊢
+      convert h using 1
+      ring
+
 /-- Converts a real number `x` from the interval `[0, 1)` into sequence of
 its digits in base `b`. -/
 noncomputable def digits (x : ℝ) (b : ℕ) [NeZero b] : ℕ → Fin b :=
diff --git a/Mathlib/Topology/Instances/CantorSet.lean b/Mathlib/Topology/Instances/CantorSet.lean
index a1a1324c55..d5f35045aa 100644
--- a/Mathlib/Topology/Instances/CantorSet.lean
+++ b/Mathlib/Topology/Instances/CantorSet.lean
@@ -29,6 +29,8 @@ This file defines the Cantor ternary set and proves a few properties.
 * `ofDigits_zero_two_sequence_mem_cantorSet`: any such sequence corresponds to a number
   in the Cantor set.
 * `ofDigits_zero_two_sequence_unique`: such a representation is unique.
+* `cantorSetHomeomorph`: the ternary Cantor set is homeomorphic to the space of infinite
+  Boolean sequences.
 -/
 
 /-- The order `n` pre-Cantor set, defined starting from `[0, 1]` and successively removing the
@@ -312,4 +314,41 @@ theorem cantorSet_eq_zero_two_ofDigits :
   · rw [← ha.right]
     exact ofDigits_zero_two_sequence_mem_cantorSet ha.left
 
+/-- The ternary Cantor set is homeomorphic to the space of infinite Boolean sequences. -/
+noncomputable def cantorSetHomeomorph : cantorSet ≃ₜ (ℕ → Bool) := by
+  let ternary : (ℕ → Bool) → ℕ → Fin 3 := fun a n ↦ if a n then 2 else 0
+  have ternary_ne_one (a : ℕ → Bool) (n : ℕ) : ternary a n ≠ 1 := by
+    simp only [ternary]
+    split <;> simp_all
+  let toCantor : (ℕ → Bool) → cantorSet := fun a ↦
+    ⟨ofDigits (ternary a), ofDigits_zero_two_sequence_mem_cantorSet (ternary_ne_one a)⟩
+  let toBinary : cantorSet → ℕ → Bool := fun x ↦ (cantorToBinary x).get
+  have toCantor_toBinary (x : cantorSet) : toCantor (toBinary x) = x := by
+    apply Subtype.ext
+    change ofDigits (ternary (toBinary x)) = x
+    rw [show ternary (toBinary x) = (cantorToTernary x).get by
+      funext n
+      simp [ternary, toBinary, cantorToTernary, Stream'.get_map]]
+    exact ofDigits_cantorToTernary x.property
+  have toBinary_toCantor (a : ℕ → Bool) : toBinary (toCantor a) = a := by
+    have hternary : (cantorToTernary (toCantor a)).get = ternary a :=
+      ofDigits_zero_two_sequence_unique (fun _ ↦ cantorToTernary_ne_one)
+        (ternary_ne_one a) (by
+          rw [ofDigits_cantorToTernary (toCantor a).property])
+    funext n
+    have hn := congrFun hternary n
+    simp only [cantorToTernary, Stream'.get_map, ternary] at hn
+    grind
+  let e : (ℕ → Bool) ≃ cantorSet :=
+    { toFun := toCantor
+      invFun := toBinary
+      left_inv := toBinary_toCantor
+      right_inv := toCantor_toBinary }
+  have he : Continuous e := by
+    apply Continuous.subtype_mk
+    exact (Real.continuous_ofDigits 3).comp <| continuous_pi fun n ↦ by
+      exact (continuous_of_discreteTopology : Continuous fun b : Bool ↦
+        if b then (2 : Fin 3) else 0).comp (continuous_apply n)
+  exact (e.toHomeomorphOfContinuousClosed he he.isClosedMap).symm
+
 end ternary02