Lebesgue number lemma

Mathlib/Topology/UnitInterval.lean

@@ -20,7 +20,6 @@ We provide basic instances, as well as a custom tactic for discharging
 
 -/
 
-
 noncomputable section
 
 open Classical Topology Filter
@@ -73,6 +72,13 @@ instance hasOne : One I :=
   ⟨⟨1, by constructor <;> norm_num⟩⟩
 #align unit_interval.has_one unitInterval.hasOne
 
+instance : ZeroLEOneClass I := ⟨@zero_le_one ℝ _ _ _ _⟩
+
+instance : BoundedOrder I := Set.Icc.boundedOrder zero_le_one
+
+lemma univ_eq_Icc : (univ : Set I) = Icc 0 1 := by
+  ext ⟨t, t0, t1⟩; simp_rw [mem_univ, true_iff]; exact ⟨t0, t1⟩
+
 theorem coe_ne_zero {x : I} : (x : ℝ) ≠ 0 ↔ x ≠ 0 :=
   not_iff_not.mpr coe_eq_zero
 #align unit_interval.coe_ne_zero unitInterval.coe_ne_zero
@@ -129,6 +135,14 @@ theorem continuous_symm : Continuous σ :=
   (continuous_const.add continuous_induced_dom.neg).subtype_mk _
 #align unit_interval.continuous_symm unitInterval.continuous_symm
 
+lemma antitone_symm : Antitone σ := fun _ _ h ↦ sub_le_sub_left (α := ℝ) h _
+
+lemma bijective_symm : Function.Bijective σ :=
+  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩
+
+lemma half_le_symm_iff (t : I) : 1 / 2 ≤ (σ t : ℝ) ↔ (t : ℝ) ≤ 1 / 2 := by
+  rw [coe_symm_eq, le_sub_iff_add_le, add_comm, ←le_sub_iff_add_le, sub_half]
+
 instance : ConnectedSpace I :=
   Subtype.connectedSpace ⟨nonempty_Icc.mpr zero_le_one, isPreconnected_Icc⟩
 
@@ -177,6 +191,40 @@ theorem two_mul_sub_one_mem_iff {t : ℝ} : 2 * t - 1 ∈ I ↔ t ∈ Set.Icc (1
 
 end unitInterval
 
+/-- Any open cover of a closed interval in ℝ can be refined to
+  a finite partition into subintervals. -/
+lemma lebesgue_number_lemma_Icc {ι} {a b : ℝ} (h : a ≤ b) {c : ι → Set (Icc a b)}
+    (hc₁ : ∀ i, IsOpen (c i)) (hc₂ : univ ⊆ ⋃ i, c i) : ∃ t : ℕ → Icc a b, t 0 = a ∧
+      Monotone t ∧ (∀ n, ∃ i, Icc (t n) (t (n + 1)) ⊆ c i) ∧ ∃ n, ∀ m ≥ n, t m = b := by
+  obtain ⟨δ, δ_pos, ball_subset⟩ := lebesgue_number_lemma_of_metric isCompact_univ hc₁ hc₂
+  refine ⟨fun n ↦ projIcc a b h (n * (δ/2) + a), ?_, fun n m hnm ↦ ?_, fun n ↦ ?_, ?_⟩
+  · dsimp only; rw [Nat.cast_zero, zero_mul, zero_add, projIcc_left]
+  · apply monotone_projIcc
+    rw [add_le_add_iff_right, mul_le_mul_right (div_pos δ_pos zero_lt_two)]
+    exact_mod_cast hnm
+  · obtain ⟨i, hsub⟩ := ball_subset (projIcc a b h (n * (δ/2) + a)) trivial
+    refine ⟨i, fun x hx ↦ hsub ?_⟩
+    rw [Metric.mem_ball]
+    apply (abs_eq_self.mpr _).trans_lt
+    · apply (sub_le_sub_right _ _).trans_lt
+      on_goal 3 => exact hx.2
+      refine (max_sub_max_le_max _ _ _ _).trans_lt (max_lt (by rwa [sub_self]) ?_)
+      refine ((le_abs_self _).trans <| abs_min_sub_min_le_max _ _ _ _).trans_lt (max_lt ?_ ?_)
+      · rwa [sub_self, abs_zero]
+      · rw [add_sub_add_comm, sub_self, add_zero, ← sub_mul, Nat.cast_succ, add_sub_cancel',
+          one_mul, abs_lt]; constructor <;> linarith only [δ_pos]
+    · exact sub_nonneg_of_le hx.1
+  · refine ⟨Nat.ceil ((b-a)/(δ/2)), fun n hn ↦ ?_⟩
+    rw [coe_projIcc, min_eq_left_iff.mpr, max_eq_right h]
+    rwa [GE.ge, Nat.ceil_le, div_le_iff (div_pos δ_pos zero_lt_two), sub_le_iff_le_add] at hn
+
+/-- Any open cover of the unit interval can be refined to a finite partition into subintervals. -/
+lemma lebesgue_number_lemma_unitInterval {ι} {c : ι → Set unitInterval} (hc₁ : ∀ i, IsOpen (c i))
+    (hc₂ : univ ⊆ ⋃ i, c i) : ∃ t : ℕ → unitInterval, t 0 = 0 ∧ Monotone t ∧
+      (∀ n, ∃ i, Icc (t n) (t (n + 1)) ⊆ c i) ∧ ∃ n, ∀ m ≥ n, t m = 1 := by
+  simp_rw [← Subtype.coe_inj]
+  exact lebesgue_number_lemma_Icc zero_le_one hc₁ hc₂
+
 @[simp]
 theorem projIcc_eq_zero {x : ℝ} : projIcc (0 : ℝ) 1 zero_le_one x = 0 ↔ x ≤ 0 :=
   projIcc_eq_left zero_lt_one