From 196b142b945e0d9b96e20a6761986851fbc8e6da Mon Sep 17 00:00:00 2001 From: Eric Date: Wed, 23 Oct 2024 16:41:28 -0700 Subject: [PATCH] Prove Exercise 3.1.5 with help --- OrderedSemigroups/Convergence.lean | 147 +++++++++++++++++++++++++++++ 1 file changed, 147 insertions(+) create mode 100644 OrderedSemigroups/Convergence.lean diff --git a/OrderedSemigroups/Convergence.lean b/OrderedSemigroups/Convergence.lean new file mode 100644 index 0000000..d6b165b --- /dev/null +++ b/OrderedSemigroups/Convergence.lean @@ -0,0 +1,147 @@ +import Mathlib.Analysis.Normed.Order.Lattice + +open Filter + +lemma arch_nat {e C : ℝ} (C_pos : C > 0) (e_pos : e > 0) : ∃n : ℕ+, 1 / n < e/(2*C) := by + have eC_pos : e / (2 * C) > 0 := div_pos e_pos (mul_pos zero_lt_two C_pos) + obtain ⟨n, hn⟩ := exists_nat_one_div_lt eC_pos + use ⟨n + 1, by omega⟩ + field_simp + exact hn + +-- Exercise 3.1.5 https://arxiv.org/pdf/1408.5805 +-- Formalized with the help of Tomas Ortega +lemma sequence_convergence + (a : ℕ → ℝ) -- sequence indexed by integers + (C : ℝ) -- the constant from the bound + (h_bound : ∀ m n : ℕ, |a (m + n) - a m - a n| ≤ C) : + ∃! θ : ℝ, -- exists unique θ + -- conclusion: θ is the limit of a_n/n at +∞ + (Filter.Tendsto (fun n ↦ a n / (n : ℝ)) Filter.atTop (nhds θ)) := by + -- let I_n be the interval [(a_n - C)/n, (a_n + C)/n] + let I (n : ℕ) := {x | |(a n) / n - x| ≤ C / n} -- this definition probably needs n > 1 + -- check that I_{m*n} ⊆ I_n for all m, n (we'll do natural, I think it is needed) + have h (m n : ℕ) (mpos : m > 0): |a (m * n) - m * a n| ≤ (m - 1) * C := by + -- induction from starting point m = 1 + induction' m, mpos using Nat.le_induction with m hm hI + · rw [Nat.succ_eq_add_one, zero_add, Nat.cast_one, one_mul, one_mul, sub_self, sub_self, abs_zero, zero_mul] -- base case m = 1 + · field_simp -- simplify the goal and casting + calc + |a ((m + 1) * n) - (m + 1) * a n| = |(a ((m + 1) * n) - a (m * n) - a n) + (a (m * n) - m * a n)| := by ring_nf + _ ≤ |a ((m + 1) * n) - a (m * n) - a n| + |a (m * n) - m * a n| := abs_add_le _ _ + _ = |a (m * n + n) - a (m * n) - a n| + |a (m * n) - m * a n| := by ring_nf + _ ≤ C + (m - 1) * C := add_le_add (h_bound (m * n) n) hI + _ = m * C := by ring_nf + + have h_I (m n : ℕ) (mpos : 0 < m) : I (m * n) ⊆ I n := by + -- m can be 1 or greater + have hm : m = 1 ∨ m > 1 := by exact LE.le.eq_or_gt mpos + obtain hm | hm := hm + · rw [hm, one_mul] -- m = 1 + · intro x hx -- m > 1 + have h' : |a (n) - a (m * n) / m| ≤ (m - 1) * C / m := calc + |a (n) - a (m * n) / m| = 1 / m * |m * a n - a (m * n)| := by field_simp; rw [abs_div]; field_simp; ring_nf + _ = 1 / ↑m * |a (m * n) - m * a n| := by rw [<-abs_neg]; ring_nf + _ ≤ 1 / ↑m * ((m - 1) * C) := mul_le_mul_of_nonneg_left (h m n mpos) (by positivity) + _ ≤ (m - 1) * C / m := by field_simp + + calc + |a n / ↑n - x| = |(a n / ↑n - a (m * n) / (m * n)) + (a (m * n) / (m * n) - x)| := by simp only [sub_add_sub_cancel] + _ ≤ |a n / ↑n - a (m * n) / (m * n)| + |a (m * n) / (m * n) - x| := abs_add_le _ _ + _ ≤ |a n / ↑n - a (m * n) / (m * n)| + C / ↑(m * n) := by rw [add_le_add_iff_left, <-Nat.cast_mul]; exact hx + _ = |a n / n - (a (m * n) / m) / n| + C / ↑(m * n) := by field_simp + _ = |(a n - a (m * n) / m) / n| + C / ↑(m * n) := by ring_nf + _ ≤ |a n - a (m * n) / ↑m| / |↑n| + C / ↑(m * n) := by rw [abs_div] + _ ≤ (m - 1) * C / m / n + C / ↑(m * n) := by rw [Nat.abs_cast, add_le_add_iff_right]; exact div_le_div_of_nonneg_right h' (Nat.cast_nonneg' n) + _ ≤ ((m - 1) * C + C) / (m * n) := by field_simp + _ ≤ (m * C) / (m * n) := by exact div_le_div_of_nonneg_right (by linarith) (by simp [mpos]) + _ ≤ C / ↑n := by ring_nf; field_simp + + have : C ≥ 0 := by + have pos := abs_nonneg (a (2 + 1) - a 2 - a 1) + have := h 2 1 (by simp) + exact Preorder.le_trans 0 |a (2 + 1) - a 2 - a 1| C pos (h_bound 2 1) + + -- I n is nonempty + have h_I_nonempty (n : ℕ) : ∃ x, x ∈ I n := by + -- n can be zero or positive + use (a n) / n + dsimp [I] + rw [sub_self, abs_zero] + obtain rfl | npos := Nat.eq_zero_or_pos n + · rw [CharP.cast_eq_zero, div_zero] + · positivity + + let h_Icc (n : ℕ) := Set.Icc ((a n) / n - C / n) ((a n) / n + C / n) + + have h_I_Icc (n : ℕ) : I n = h_Icc n := by + ext x + exact ⟨fun x => Set.mem_Icc_iff_abs_le.mp x, fun x => Set.mem_Icc_iff_abs_le.2 x⟩ + + -- let J be the intersection of all I_n for n in N + let J := ⋂ n ∈ (Set.univ : Set ℕ+), I n + -- J is nonempty + have h_J_nonempty : ∃ x, x ∈ J := by + dsimp [J] + apply IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed + · simp [Directed] + intro x y + use (x*y) + constructor + · rw [mul_comm x y] + exact h_I y x (by simp [x.property]) + · exact h_I x y (by simp [x.property]) + · simp [Set.Nonempty, h_I_nonempty] + · simp [h_I_Icc, isCompact_Icc] + exact fun i => isCompact_Icc + · simp [h_I_Icc] + exact fun i => isClosed_Icc + -- Let x be the element in the intersection of all the I_n + obtain ⟨x, hx⟩ := h_J_nonempty + -- then x is what the sequence (a n)/n converges to + use x + simp + have : (Filter.Tendsto (fun n ↦ a n / (n : ℝ)) Filter.atTop (nhds x)) := by + by_cases h : C = 0 + -- the case where C = 0 implies that the whole sequence is constant and equal to x + · subst_vars + simp_all [h_Icc, J, I] + have (n : ℕ+) : (a n) / (n : ℝ) = x := by + have := hx n + exact this.symm + rw [Metric.tendsto_atTop] + intro e pos_e + use 1 + intro n n_ge_1 + simp [dist] + have := this ⟨n, by omega⟩ + simp at this + simpa [this] + · have C_pos : C > 0 := lt_of_le_of_ne this fun a => h (id (Eq.symm a)) + rw [Metric.tendsto_atTop] + intro e he + simp [dist] + simp [J, I] at hx + obtain ⟨N, hN⟩ := arch_nat C_pos he + use N + intro n N_le_n + have zero_lt_n : n > 0 := Nat.lt_of_lt_of_le N.property N_le_n + have x_in_interval := hx ⟨n, zero_lt_n ⟩ + simp at x_in_interval + have N_le_n : (N : ℝ) ≤ n := Nat.cast_le.mpr N_le_n + have zero_lt_N : 0 < (N : ℝ) := Nat.cast_pos'.mpr N.property + have : 1 / (N : ℝ) ≥ 1 / (n : ℝ) := by + exact one_div_le_one_div_of_le (α := ℝ) zero_lt_N N_le_n + calc |(a n) / (n : ℝ) - x| + _ ≤ C / (n : ℝ) := x_in_interval + _ = C * (n : ℝ)⁻¹ := by field_simp + _ ≤ C * (N : ℝ)⁻¹ := by simp_all + _ < C * (e / (2*C)) := by simp_all + _ = e / 2 := by + field_simp + rw [mul_comm 2 C, ←mul_assoc e C 2, mul_comm e C] + _ < e := by simp_all + constructor + · trivial + · intro y hy + exact tendsto_nhds_unique hy this