Refactor Remark 1.3.10: move helper lemmas and simplify structure

- Move geometric series and floor helper lemmas (tsum_two_thirds_geometric, tsum_tail_bound, floor_two_mul_odd_ge, floor_two_mul_even_le, floor_two_mul_eq_of_mod_eq) before Remark_1_3_10 namespace
- Remove BinaryToTernaryProperties structure and binaryToTernaryFn definition (unused)
- Simplify DyadicRationals comment
- Clean up proof structure and organization

Author: aodecipher

analysis/Analysis/MeasureTheory/Section_1_3_2.lean

@@ -1781,9 +1781,8 @@ Both versions work for the theorem because:
 - Both map [0,1] into CantorSet ∪ {0}
 - Both give measurable f with f⁻¹(E) = F non-measurable
 -/
-namespace Remark_1_3_10
 
-/-- Dyadic rationals in [0,1]: numbers of the form k/2^n where k ≤ 2^n.
+/-- Dyadic rationals: numbers of the form k/2^n where k ≤ 2^n.
     These are exactly the real numbers with terminating binary expansions. -/
 def DyadicRationals : Set ℝ := {x : ℝ | ∃ (k n : ℕ), x = k / 2^n ∧ k ≤ 2^n}
 
@@ -1799,41 +1798,15 @@ lemma DyadicRationals.countable : DyadicRationals.Countable := by
   have hk_lt : k < 2^n + 1 := Nat.lt_succ_of_le hk_le
   exact ⟨⟨k, hk_lt⟩, hk.symm⟩
 
-/-- The properties required of the binary-to-ternary function for this construction.
-    The function maps [0,1] into the Cantor set C by converting binary digits to ternary.
-
-    Note: Unlike the textbook (which sets g(x) = 0 for dyadic rationals), our g is defined
-    uniformly for all x ∈ [0,1]. This makes g monotone on ALL of [0,1], not just on A. -/
-structure BinaryToTernaryProperties (g : ℝ → ℝ) : Prop where
-  nonneg : ∀ x, 0 ≤ g x
-  bounded : ∀ x, g x ≤ 1
-  zero_outside : ∀ x, x ∉ Set.Icc 0 1 → g x = 0  -- g(x) = 0 outside [0,1]
-  zero_at_zero : g 0 = 0  -- g(0) = 0 (binary 0.000... maps to ternary 0.000...)
-  zero_set_countable : (Set.Icc 0 1 ∩ {x | g x = 0}).Countable  -- {g = 0} ∩ [0,1] = {0}
-  monotone_on : MonotoneOn g (Set.Icc 0 1)  -- g is monotone on ALL of [0,1]
-  image_in_cantor : g '' (Set.Icc 0 1) ⊆ CantorSet ∪ {0}
-  injective_on_nonterminating : ∃ A : Set ℝ, A ⊆ Set.Icc 0 1 ∧
-    (Set.Icc 0 1 \ A).Countable ∧  -- A is co-countable in [0,1]
-    Set.InjOn g A ∧                 -- g is injective on A (hence bijective onto g(A) ⊆ C)
-    A ∩ DyadicRationals = ∅         -- A excludes dyadic rationals
-
-/-! ### Binary digit extraction and helper lemmas -/
-
 /-- Binary digit extraction: bⱼ(x) = ⌊2^j · x⌋ mod 2.
-    For x ∈ [0,1), this extracts the j-th binary digit (1-indexed).
+    For x ∈ [0,1), this extracts the j-th binary digit.
     Special case: x = 1 has all digits = 1 (1 = 0.111...₂).
     For x ∉ [0,1], all digits are 0. -/
 noncomputable def binaryDigit (x : ℝ) (j : ℕ) : ℕ :=
   if x ∈ Set.Ico (0:ℝ) 1 then ⌊(2:ℝ)^j * x⌋₊ % 2
   else if x = 1 then 1
   else 0
 
-/-- The binary-to-ternary function: g(x) = ∑_{j≥1} 2·bⱼ(x)·3^{-j} for x ∈ [0,1], else 0. -/
-noncomputable def binaryToTernaryFn (x : ℝ) : ℝ :=
-  if x ∈ Set.Icc (0:ℝ) 1 then
-    ∑' j : ℕ, (2 * binaryDigit x (j + 1) : ℝ) * (1/3:ℝ)^(j + 1)
-  else 0
-
 /-- Binary digits are in {0, 1}. -/
 lemma binaryDigit_le_one (x : ℝ) (j : ℕ) : binaryDigit x j ≤ 1 := by
   simp only [binaryDigit]
@@ -1850,6 +1823,127 @@ lemma binaryDigit_zero (j : ℕ) : binaryDigit 0 j = 0 := by
 lemma binaryDigit_one (j : ℕ) : binaryDigit 1 j = 1 := by
   simp only [binaryDigit, Set.mem_Ico, lt_self_iff_false, and_false, ↓reduceIte]
 
+/-- The full sum ∑_{j≥0} 2·(1/3)^{j+1} = 1. -/
+lemma tsum_two_thirds_geometric : ∑' j : ℕ, (2:ℝ) * (1/3:ℝ)^(j + 1) = 1 := by
+  have h1 : ∑' j : ℕ, (1/3:ℝ)^j = (1 - 1/3)⁻¹ :=
+    tsum_geometric_of_lt_one (by norm_num) (by norm_num)
+  calc ∑' j : ℕ, (2:ℝ) * (1/3:ℝ)^(j + 1)
+      = ∑' j : ℕ, (2/3:ℝ) * (1/3:ℝ)^j := by congr 1; ext j; ring
+    _ = (2/3) * ∑' j : ℕ, (1/3:ℝ)^j := by rw [tsum_mul_left]
+    _ = (2/3) * (1 - 1/3)⁻¹ := by rw [h1]
+    _ = 1 := by norm_num
+
+/-- The tail sum bound: ∑_{j≥k} 2·(1/3)^{j+1} = (1/3)^k. -/
+lemma tsum_tail_bound (k : ℕ) :
+    ∑' j : ℕ, (2:ℝ) * (1/3:ℝ)^(k + j + 1) = (1/3:ℝ)^k := by
+  have h1 : ∑' j : ℕ, (1/3:ℝ)^j = (1 - 1/3)⁻¹ :=
+    tsum_geometric_of_lt_one (by norm_num) (by norm_num)
+  calc ∑' j : ℕ, (2:ℝ) * (1/3:ℝ)^(k + j + 1)
+      = ∑' j : ℕ, (2:ℝ) * ((1/3:ℝ)^(k+1) * (1/3:ℝ)^j) := by
+        congr 1; ext j; rw [← pow_add]; ring_nf
+    _ = (2:ℝ) * (1/3:ℝ)^(k+1) * ∑' j : ℕ, (1/3:ℝ)^j := by
+        rw [← tsum_mul_left]; congr 1; ext j; ring
+    _ = (2:ℝ) * (1/3:ℝ)^(k+1) * (1 - 1/3)⁻¹ := by rw [h1]
+    _ = (1/3:ℝ)^k := by field_simp; ring
+
+/-- Helper: if ⌊2z⌋₊ % 2 = 1 then ⌊2z⌋₊ ≥ 2⌊z⌋₊ + 1 -/
+lemma floor_two_mul_odd_ge {z : ℝ} (hz : 0 ≤ z) (hodd : ⌊2 * z⌋₊ % 2 = 1) :
+    ⌊2 * z⌋₊ ≥ 2 * ⌊z⌋₊ + 1 := by
+  have h_decomp : ⌊2 * z⌋₊ = 2 * (⌊2 * z⌋₊ / 2) + ⌊2 * z⌋₊ % 2 := (Nat.div_add_mod _ _).symm
+  rw [hodd] at h_decomp
+  have h_div : ⌊2 * z⌋₊ / 2 ≥ ⌊z⌋₊ := by
+    have h1 : (2 * ⌊z⌋₊ : ℕ) ≤ ⌊2 * z⌋₊ := by
+      have hfloor := Nat.floor_le hz
+      apply Nat.le_floor
+      simp only [Nat.cast_mul, Nat.cast_ofNat]
+      linarith
+    rw [mul_comm] at h1
+    exact (Nat.le_div_iff_mul_le (by norm_num : 0 < 2)).mpr h1
+  omega
+
+/-- Helper: if ⌊2z⌋₊ % 2 = 0 then ⌊2z⌋₊ ≤ 2⌊z⌋₊ -/
+lemma floor_two_mul_even_le {z : ℝ} (hz : 0 ≤ z) (heven : ⌊2 * z⌋₊ % 2 = 0) :
+    ⌊2 * z⌋₊ ≤ 2 * ⌊z⌋₊ := by
+  have h_decomp : ⌊2 * z⌋₊ = 2 * (⌊2 * z⌋₊ / 2) + ⌊2 * z⌋₊ % 2 := (Nat.div_add_mod _ _).symm
+  rw [heven, add_zero] at h_decomp
+  have h_div : ⌊2 * z⌋₊ / 2 ≤ ⌊z⌋₊ := by
+    have h1 : ⌊2 * z⌋₊ < 2 * (⌊z⌋₊ + 1) := by
+      have := Nat.lt_floor_add_one z
+      have h2 : 2 * z < 2 * (⌊z⌋₊ + 1) := by linarith
+      have h3 : (⌊2 * z⌋₊ : ℝ) ≤ 2 * z := Nat.floor_le (mul_nonneg (by norm_num) hz)
+      have h4 : (⌊2 * z⌋₊ : ℝ) < 2 * (↑⌊z⌋₊ + 1) := lt_of_le_of_lt h3 h2
+      have h5 : (⌊2 * z⌋₊ : ℝ) < 2 * ⌊z⌋₊ + 2 := by linarith
+      exact_mod_cast h5
+    omega
+  omega
+
+/-- Helper: equal mod 2 and equal ⌊z⌋ implies equal ⌊2z⌋ -/
+lemma floor_two_mul_eq_of_mod_eq {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y)
+    (h_floor : ⌊x⌋₊ = ⌊y⌋₊) (h_mod : ⌊2 * x⌋₊ % 2 = ⌊2 * y⌋₊ % 2) :
+    ⌊2 * x⌋₊ = ⌊2 * y⌋₊ := by
+  by_cases hxodd : ⌊2 * x⌋₊ % 2 = 1
+  · have hyodd := h_mod ▸ hxodd
+    have hx_ge := floor_two_mul_odd_ge hx hxodd
+    have hy_ge := floor_two_mul_odd_ge hy hyodd
+    have hx_lt : ⌊2 * x⌋₊ < 2 * ⌊x⌋₊ + 2 := by
+      have := Nat.lt_floor_add_one x
+      have h2 : 2 * x < 2 * (⌊x⌋₊ + 1) := by linarith
+      have h3 : (⌊2 * x⌋₊ : ℝ) ≤ 2 * x := Nat.floor_le (mul_nonneg (by norm_num) hx)
+      have h4 : (⌊2 * x⌋₊ : ℝ) < 2 * ⌊x⌋₊ + 2 := by linarith
+      exact_mod_cast h4
+    have hy_lt : ⌊2 * y⌋₊ < 2 * ⌊y⌋₊ + 2 := by
+      have := Nat.lt_floor_add_one y
+      have h2 : 2 * y < 2 * (⌊y⌋₊ + 1) := by linarith
+      have h3 : (⌊2 * y⌋₊ : ℝ) ≤ 2 * y := Nat.floor_le (mul_nonneg (by norm_num) hy)
+      have h4 : (⌊2 * y⌋₊ : ℝ) < 2 * ⌊y⌋₊ + 2 := by linarith
+      exact_mod_cast h4
+    omega
+  · have hxeven : ⌊2 * x⌋₊ % 2 = 0 := Nat.mod_two_eq_zero_or_one (⌊2 * x⌋₊) |>.resolve_right hxodd
+    have hyeven := h_mod ▸ hxeven
+    have hx_le := floor_two_mul_even_le hx hxeven
+    have hy_le := floor_two_mul_even_le hy hyeven
+    have hx_ge : ⌊2 * x⌋₊ ≥ 2 * ⌊x⌋₊ := by
+      have h1 : (2 * ⌊x⌋₊ : ℕ) ≤ ⌊2 * x⌋₊ := by
+        have hfloor := Nat.floor_le hx
+        apply Nat.le_floor
+        simp only [Nat.cast_mul, Nat.cast_ofNat]
+        linarith
+      exact h1
+    have hy_ge : ⌊2 * y⌋₊ ≥ 2 * ⌊y⌋₊ := by
+      have h1 : (2 * ⌊y⌋₊ : ℕ) ≤ ⌊2 * y⌋₊ := by
+        have hfloor := Nat.floor_le hy
+        apply Nat.le_floor
+        simp only [Nat.cast_mul, Nat.cast_ofNat]
+        linarith
+      exact h1
+    omega
+
+namespace Remark_1_3_10
+
+/-- The properties required of the binary-to-ternary function for this construction.
+    The function maps [0,1] into the Cantor set C by converting binary digits to ternary.
+
+    Note: Unlike the textbook (which sets g(x) = 0 for dyadic rationals), our g is defined
+    uniformly for all x ∈ [0,1]. This makes g monotone on ALL of [0,1], not just on A. -/
+structure BinaryToTernaryProperties (g : ℝ → ℝ) : Prop where
+  nonneg : ∀ x, 0 ≤ g x
+  bounded : ∀ x, g x ≤ 1
+  zero_outside : ∀ x, x ∉ Set.Icc 0 1 → g x = 0  -- g(x) = 0 outside [0,1]
+  zero_at_zero : g 0 = 0  -- g(0) = 0 (binary 0.000... maps to ternary 0.000...)
+  zero_set_countable : (Set.Icc 0 1 ∩ {x | g x = 0}).Countable  -- {g = 0} ∩ [0,1] = {0}
+  monotone_on : MonotoneOn g (Set.Icc 0 1)  -- g is monotone on ALL of [0,1]
+  image_in_cantor : g '' (Set.Icc 0 1) ⊆ CantorSet ∪ {0}
+  injective_on_nonterminating : ∃ A : Set ℝ, A ⊆ Set.Icc 0 1 ∧
+    (Set.Icc 0 1 \ A).Countable ∧  -- A is co-countable in [0,1]
+    Set.InjOn g A ∧                 -- g is injective on A (hence bijective onto g(A) ⊆ C)
+    A ∩ DyadicRationals = ∅         -- A excludes dyadic rationals
+
+/-- The binary-to-ternary function: g(x) = ∑_{j≥1} 2·bⱼ(x)·3^{-j} for x ∈ [0,1], else 0. -/
+noncomputable def binaryToTernaryFn (x : ℝ) : ℝ :=
+  if x ∈ Set.Icc (0:ℝ) 1 then
+    ∑' j : ℕ, (2 * binaryDigit x (j + 1) : ℝ) * (1/3:ℝ)^(j + 1)
+  else 0
+
 /-- The series ∑ 2·bⱼ(x)·3^{-j} is summable for any x. -/
 lemma binaryToTernary_summable (x : ℝ) :
     Summable (fun j => (2 * binaryDigit x (j + 1) : ℝ) * (1/3:ℝ)^(j + 1)) := by
@@ -1866,16 +1960,6 @@ lemma binaryToTernary_summable (x : ℝ) :
   · have h : Summable (fun j : ℕ => (1/3:ℝ)^j) := summable_geometric_of_lt_one (by norm_num) (by norm_num)
     exact (h.mul_left 2).comp_injective (fun _ _ h => Nat.succ_injective h)
 
-/-- The full sum ∑_{j≥0} 2·(1/3)^{j+1} = 1. -/
-lemma tsum_two_thirds_geometric : ∑' j : ℕ, (2:ℝ) * (1/3:ℝ)^(j + 1) = 1 := by
-  have h1 : ∑' j : ℕ, (1/3:ℝ)^j = (1 - 1/3)⁻¹ :=
-    tsum_geometric_of_lt_one (by norm_num) (by norm_num)
-  calc ∑' j : ℕ, (2:ℝ) * (1/3:ℝ)^(j + 1)
-      = ∑' j : ℕ, (2/3:ℝ) * (1/3:ℝ)^j := by congr 1; ext j; ring
-    _ = (2/3) * ∑' j : ℕ, (1/3:ℝ)^j := by rw [tsum_mul_left]
-    _ = (2/3) * (1 - 1/3)⁻¹ := by rw [h1]
-    _ = 1 := by norm_num
-
 /-! ### Helper lemmas for monotonicity proof -/
 
 /-- For x ∈ (0, 1), there exists a position where the binary digit is 1. -/
@@ -1931,78 +2015,6 @@ lemma binaryDigit_partial_sum_lt (x : ℝ) (n : ℕ) :
         apply div_lt_div_of_pos_right h1 h2n_pos
     _ = (⌊(2:ℝ)^n * x⌋₊ : ℝ) / (2:ℝ)^n + (1:ℝ) / (2:ℝ)^n := by ring
 
-/-- Helper: if ⌊2z⌋₊ % 2 = 1 then ⌊2z⌋₊ ≥ 2⌊z⌋₊ + 1 -/
-lemma floor_two_mul_odd_ge {z : ℝ} (hz : 0 ≤ z) (hodd : ⌊2 * z⌋₊ % 2 = 1) :
-    ⌊2 * z⌋₊ ≥ 2 * ⌊z⌋₊ + 1 := by
-  have h_decomp : ⌊2 * z⌋₊ = 2 * (⌊2 * z⌋₊ / 2) + ⌊2 * z⌋₊ % 2 := (Nat.div_add_mod _ _).symm
-  rw [hodd] at h_decomp
-  have h_div : ⌊2 * z⌋₊ / 2 ≥ ⌊z⌋₊ := by
-    have h1 : (2 * ⌊z⌋₊ : ℕ) ≤ ⌊2 * z⌋₊ := by
-      have hfloor := Nat.floor_le hz
-      apply Nat.le_floor
-      simp only [Nat.cast_mul, Nat.cast_ofNat]
-      linarith
-    rw [mul_comm] at h1
-    exact (Nat.le_div_iff_mul_le (by norm_num : 0 < 2)).mpr h1
-  omega
-
-/-- Helper: if ⌊2z⌋₊ % 2 = 0 then ⌊2z⌋₊ ≤ 2⌊z⌋₊ -/
-lemma floor_two_mul_even_le {z : ℝ} (hz : 0 ≤ z) (heven : ⌊2 * z⌋₊ % 2 = 0) :
-    ⌊2 * z⌋₊ ≤ 2 * ⌊z⌋₊ := by
-  have h_decomp : ⌊2 * z⌋₊ = 2 * (⌊2 * z⌋₊ / 2) + ⌊2 * z⌋₊ % 2 := (Nat.div_add_mod _ _).symm
-  rw [heven, add_zero] at h_decomp
-  have h_div : ⌊2 * z⌋₊ / 2 ≤ ⌊z⌋₊ := by
-    have h1 : ⌊2 * z⌋₊ < 2 * (⌊z⌋₊ + 1) := by
-      have := Nat.lt_floor_add_one z
-      have h2 : 2 * z < 2 * (⌊z⌋₊ + 1) := by linarith
-      have h3 : (⌊2 * z⌋₊ : ℝ) ≤ 2 * z := Nat.floor_le (mul_nonneg (by norm_num) hz)
-      have h4 : (⌊2 * z⌋₊ : ℝ) < 2 * (↑⌊z⌋₊ + 1) := lt_of_le_of_lt h3 h2
-      have h5 : (⌊2 * z⌋₊ : ℝ) < 2 * ⌊z⌋₊ + 2 := by linarith
-      exact_mod_cast h5
-    omega
-  omega
-
-/-- Helper: equal mod 2 and equal ⌊z⌋ implies equal ⌊2z⌋ -/
-lemma floor_two_mul_eq_of_mod_eq {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y)
-    (h_floor : ⌊x⌋₊ = ⌊y⌋₊) (h_mod : ⌊2 * x⌋₊ % 2 = ⌊2 * y⌋₊ % 2) :
-    ⌊2 * x⌋₊ = ⌊2 * y⌋₊ := by
-  by_cases hxodd : ⌊2 * x⌋₊ % 2 = 1
-  ·
-    have hyodd := h_mod ▸ hxodd
-    have hx_ge := floor_two_mul_odd_ge hx hxodd
-    have hy_ge := floor_two_mul_odd_ge hy hyodd
-    have hx_lt : ⌊2 * x⌋₊ < 2 * ⌊x⌋₊ + 2 := by
-      have := Nat.lt_floor_add_one x
-      have h2 : 2 * x < 2 * (⌊x⌋₊ + 1) := by linarith
-      have h3 : (⌊2 * x⌋₊ : ℝ) ≤ 2 * x := Nat.floor_le (mul_nonneg (by norm_num) hx)
-      have h4 : (⌊2 * x⌋₊ : ℝ) < 2 * ⌊x⌋₊ + 2 := by linarith
-      exact_mod_cast h4
-    have hy_lt : ⌊2 * y⌋₊ < 2 * ⌊y⌋₊ + 2 := by
-      have := Nat.lt_floor_add_one y
-      have h2 : 2 * y < 2 * (⌊y⌋₊ + 1) := by linarith
-      have h3 : (⌊2 * y⌋₊ : ℝ) ≤ 2 * y := Nat.floor_le (mul_nonneg (by norm_num) hy)
-      have h4 : (⌊2 * y⌋₊ : ℝ) < 2 * ⌊y⌋₊ + 2 := by linarith
-      exact_mod_cast h4
-    rw [h_floor] at hx_ge hx_lt
-    omega
-  ·
-    have hxeven : ⌊2 * x⌋₊ % 2 = 0 := by omega
-    have hyeven := h_mod ▸ hxeven
-    have hx_le := floor_two_mul_even_le hx hxeven
-    have hy_le := floor_two_mul_even_le hy hyeven
-    have hx_ge : 2 * ⌊x⌋₊ ≤ ⌊2 * x⌋₊ := by
-      have hfl := Nat.floor_le hx
-      apply Nat.le_floor
-      simp only [Nat.cast_mul, Nat.cast_ofNat]
-      linarith
-    have hy_ge : 2 * ⌊y⌋₊ ≤ ⌊2 * y⌋₊ := by
-      have hfl := Nat.floor_le hy
-      apply Nat.le_floor
-      simp only [Nat.cast_mul, Nat.cast_ofNat]
-      linarith
-    rw [h_floor] at hx_le hx_ge
-    omega
-
 /-- Key lemma: if bₖ(x) = 1, then x ≥ ⌊2^k * x⌋₊ / 2^k + 2^{-(k+1)} -/
 lemma binaryDigit_one_implies_lower_bound {x : ℝ} (hx : x ∈ Set.Ico (0:ℝ) 1) (k : ℕ)
     (hbk : binaryDigit x (k + 1) = 1) :
@@ -2117,19 +2129,6 @@ lemma binaryDigit_first_diff {x y : ℝ} (hx : x ∈ Set.Ico (0:ℝ) 1) (hy : y
     rw [h_floor_eq] at hx_lb
     linarith
 
-/-- The tail sum bound: ∑_{j≥k} 2·(1/3)^{j+1} = (1/3)^k. -/
-lemma tsum_tail_bound (k : ℕ) :
-    ∑' j : ℕ, (2:ℝ) * (1/3:ℝ)^(k + j + 1) = (1/3:ℝ)^k := by
-  have h1 : ∑' j : ℕ, (1/3:ℝ)^j = (1 - 1/3)⁻¹ :=
-    tsum_geometric_of_lt_one (by norm_num) (by norm_num)
-  calc ∑' j : ℕ, (2:ℝ) * (1/3:ℝ)^(k + j + 1)
-      = ∑' j : ℕ, (2:ℝ) * ((1/3:ℝ)^(k+1) * (1/3:ℝ)^j) := by
-        congr 1; ext j; rw [← pow_add]; ring_nf
-    _ = (2:ℝ) * (1/3:ℝ)^(k+1) * ∑' j : ℕ, (1/3:ℝ)^j := by
-        rw [← tsum_mul_left]; congr 1; ext j; ring
-    _ = (2:ℝ) * (1/3:ℝ)^(k+1) * (1 - 1/3)⁻¹ := by rw [h1]
-    _ = (1/3:ℝ)^k := by field_simp; ring
-
 /-- Monotonicity: if digits agree up to k and bₖ(x) < bₖ(y), then g(x) < g(y). -/
 lemma binaryToTernary_lt_of_digit_lt {x y : ℝ}
     (hx : x ∈ Set.Icc (0:ℝ) 1) (hy : y ∈ Set.Icc (0:ℝ) 1) (k : ℕ)