Challenge 17: Convergent sequences are bounded
Prove that if a sequence \(a_n\) is convergent, then \(a_n\) is bounded; that is, there exists an \(M ∈ ℝ\) such that for every \(n ∈ ℕ\), \(|a_n| ≤ M\).
To do so, complete the following Lean 4 theory:
import Mathlib.Data.Real.Basic import Mathlib.Tactic open Finset def SeqLim (a : ℕ → ℝ) (L : ℝ) : Prop := ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |a n - L| < ε def SeqConv (a : ℕ → ℝ) : Prop := ∃ L, SeqLim a L def SeqBdd (a : ℕ → ℝ) : Prop := ∃ M, ∀ n, |a n| ≤ M variable (a : ℕ → ℝ) example (ha : SeqConv a) : SeqBdd a := by sorry
1. Demostración en lenguaje natural
The proof is based on the following lemmas:
-
Lemma 1: If \(a_n\) converges to \(L\), then there exists a \(k \in \mathbb{N}\) such that for all \(n \geq k\), \(|a_{n}| < |L| + 1\).
-
Lemma 2: For every \(k \in \mathbb{N}\), there exists an \(M \in ℝ\) such that for all \(i < k\), \(|a_{i}| \leq M\).
Indeed, by the convergence of \(a_n\), there exists an \(L \in ℝ\) such that \(a_n\) converges to \(L\) and, by Lemma 1, there exists a \(k \in \mathbb{N}\) such that \[ ∀ n \geq k, |a_n| < |L| + 1 \tag{1} \] Moreover, by Lemma 2, there exists a \(C \in ℝ\) such that \[ ∀ i < k, |a_{i}| \leq C \tag{2} \] Let \[ M = \max(|L| + 1, C) \tag{3} \] Let us show that for every \(n \in \mathbb{N}\), \(|a_n| \leq M\). We will do so by distinguishing two cases.
Case 1: Suppose that \(n < k\). Then, \[ \begin{array}{llll} |a_n| &\leq C &&\text{[by (2)]} \\ &\leq M &&\text{[by (3)]} \end{array} \]
Case 2: Suppose that \(n \geq k\). Then, \[ \begin{array}{llll} |a_n| &\leq |L| + 1 &&\text{[by (1)]} \\ &\leq M &&\text{[by (3)]} \end{array} \]
It remains to prove the lemmas. To prove the first lemma, since \(a_n\) converges to \(L\), there exists a \(k \in \mathbb{N}\) such that \[ ∀ n \geq k, |a_n - L| < 1 \tag{4} \] Let us show that \(k\) satisfies the condition; that is, \[ ∀ n \geq k, |a_n| < |L| + 1 \] To do so, let \(n \in \mathbb{N}\) be such that \[ n \geq k \tag{5} \] Then, \[ \begin{array}{llll} |a_n| &= |L + (a_n - L)| \\ &\leq |L| + |a_n - L| &&\text{[by the triangle inequality]}\\ &< |L| + 1 &&\text{[by (4) and (5)]} \end{array} \]
To prove Lemma 2, let \[ M = \sum_{0 \leq i < k} |a_{i}| \tag{6} \] that is, \[ M = |a₀| + |a₁| + ... + |aₖ₋₁| \] Let us show that M is the bound we are looking for; that is, \[ \forall i < k, |a_{i}| \leq M \] To do so, let \(i \in \mathbb{N}\) be such that \[ i < k \tag{7} \] Then, since \[ \forall i \in \{0, 1, \dots, k-1\}, 0 \leq |a_{i}| \tag{8} \] and, by (7), \[ i \in \{0, 1, \dots, k-1\} \tag{9} \] we have \[ \begin{array}{llll} |a_{i}| &\leq \displaystyle \sum_{0 \leq i < k} |a_{i}| &&\text{[by (8) and (9)]}\\ &= M &&\text{[by (6)]} \end{array} \]
2. Proofs in Lean 4
import Mathlib.Data.Real.Basic import Mathlib.Tactic open Finset def SeqLim (a : ℕ → ℝ) (L : ℝ) : Prop := ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |a n - L| < ε def SeqConv (a : ℕ → ℝ) : Prop := ∃ L, SeqLim a L def SeqBdd (a : ℕ → ℝ) : Prop := ∃ M, ∀ n, |a n| ≤ M variable (a : ℕ → ℝ) -- Proofs of the 1st lemma -- ======================= -- Proof 1 -- ------- example (h : SeqLim a L) : ∃ k, ∀ n ≥ k, |a n| < |L| + 1 := by obtain ⟨k, hk⟩ := h 1 one_pos -- k : ℕ -- hk : ∀ n ≥ k, |a n - L| < 1 use k -- ⊢ ∀ n ≥ k, |a n| < |L| + 1 grind -- Proof 2 -- ------- example (h : SeqLim a L) : ∃ k, ∀ n ≥ k, |a n| < |L| + 1 := by obtain ⟨k, hk⟩ := h 1 one_pos -- k : ℕ -- hk : ∀ n ≥ k, |a n - L| < 1 use k -- ⊢ ∀ n ≥ k, |a n| < |L| + 1 intro n hn -- n : ℕ -- hn : n ≥ k -- ⊢ |a n| < |L| + 1 grind -- Proof 3 -- ------- example (h : SeqLim a L) : ∃ k, ∀ n ≥ k, |a n| < |L| + 1 := by obtain ⟨k, hk⟩ := h 1 one_pos -- k : ℕ -- hk : ∀ n ≥ k, |a n - L| < 1 exact ⟨k, fun _ _ => by grind⟩ -- Proof 4 -- ------- example (h : SeqLim a L) : ∃ k, ∀ n ≥ k, |a n| < |L| + 1 := (h 1 one_pos).imp fun _ _ _ _ => by grind -- Proof 5 -- ------- example (h : SeqLim a L) : ∃ k, ∀ n ≥ k, |a n| < |L| + 1 := by obtain ⟨k, hk⟩ := h 1 one_pos -- k : ℕ -- hk : ∀ n ≥ k, |a n - L| < 1 use k -- ⊢ ∀ n ≥ k, |a n| < |L| + 1 intro n hn -- n : ℕ -- hn : n ≥ k -- ⊢ |a n| < |L| + 1 calc |a n| = |L + (a n - L)| := by grind _ ≤ |L| + |a n - L| := by grind _ < |L| + 1 := by grind -- Proof 6 -- ------- example (h : SeqLim a L) : ∃ k, ∀ n ≥ k, |a n| < |L| + 1 := by obtain ⟨k, hk⟩ := h 1 one_pos -- k : ℕ -- hk : ∀ n ≥ k, |a n - L| < 1 use k -- ⊢ ∀ n ≥ k, |a n| < |L| + 1 intro n hn -- n : ℕ -- hn : n ≥ k -- ⊢ |a n| < |L| + 1 calc |a n| = |L + (a n - L)| := by congr ; ring _ ≤ |L| + |a n - L| := by simp only [abs_add_le] _ < |L| + 1 := add_lt_add_right (hk n hn) |L| -- Proof 7 -- ------- example (h : SeqLim a L) : ∃ k, ∀ n ≥ k, |a n| < |L| + 1 := by obtain ⟨k, hk⟩ := h 1 one_pos -- k : ℕ -- hk : ∀ n ≥ k, |a n - L| < 1 use k -- ⊢ ∀ n ≥ k, |a n| < |L| + 1 intro n hn -- n : ℕ -- hn : n ≥ k -- ⊢ |a n| < |L| + 1 calc |a n| = |L + (a n - L)| := congrArg abs (add_sub_cancel L (a n)).symm _ ≤ |L| + |a n - L| := abs_add_le L (a n - L) _ < |L| + 1 := add_lt_add_right (hk n hn) |L| -- Proof 8 -- ------- lemma L1 (h : SeqLim a L) : ∃ k, ∀ n ≥ k, |a n| < |L| + 1 := (h 1 one_pos).imp fun _k hk n hn => -- _k : ℕ -- hk : ∀ n ≥ _k, |a n - L| < 1 -- n : ℕ -- hn : n ≥ _k -- ⊢ |a n| < |L| + 1 calc |a n| = |L + (a n - L)| := congrArg abs (add_sub_cancel L (a n)).symm _ ≤ |L| + |a n - L| := abs_add_le L (a n - L) _ < |L| + 1 := add_lt_add_right (hk n hn) |L| -- Proofs of the 2nd lemma -- ======================= -- Proof 1 -- ------- example (k : ℕ) : ∃ M, ∀ i < k, |a i| ≤ M := by induction k with | zero => -- ⊢ ∃ M, ∀ i < 0, |a i| ≤ M use 1 -- ⊢ ∀ i < 0, |a i| ≤ 1 grind | succ k ih => -- k : ℕ -- ih : ∃ M, ∀ i < k, |a i| ≤ M -- ⊢ ∃ M, ∀ i < k + 1, |a i| ≤ M obtain ⟨M₁, hM₁⟩ := ih -- M₁ : ℝ -- hM₁ : ∀ i < k, |a i| ≤ M₁ set M := max M₁ |a k| use M -- ⊢ ∀ i < k + 1, |a i| ≤ M intro i hi -- i : ℕ -- hi : i < k + 1 -- ⊢ |a i| ≤ M rcases lt_or_ge i k with hi1 | hi2 · -- hi1 : i < k calc |a i| ≤ M₁ := by grind _ ≤ M := by grind · -- hi2 : k ≤ i have h1 : i = k := by grind calc |a i| = |a k| := by grind _ ≤ M := by grind -- Proof 2 -- ------- example (k : ℕ) : ∃ M, ∀ i < k, |a i| ≤ M := by induction k with | zero => -- ⊢ ∃ M, ∀ i < 0, |a i| ≤ M use 1 -- ⊢ ∀ i < 0, |a i| ≤ 1 grind | succ k ih => -- k : ℕ -- ih : ∃ M, ∀ i < k, |a i| ≤ M -- ⊢ ∃ M, ∀ i < k + 1, |a i| ≤ M obtain ⟨M₁, hM₁⟩ := ih -- M₁ : ℝ -- hM₁ : ∀ i < k, |a i| ≤ M₁ set M := max M₁ |a k| use M -- ⊢ ∀ i < k + 1, |a i| ≤ M intro i hi -- i : ℕ -- hi : i < k + 1 -- ⊢ |a i| ≤ M rcases lt_or_ge i k with hi1 | hi2 · -- hi1 : i < k calc |a i| ≤ M₁ := hM₁ i hi1 _ ≤ M := le_max_left _ _ · -- hi2 : k ≤ i have h1 : i = k := Nat.eq_of_le_of_lt_succ hi2 hi calc |a i| = |a k| := congrArg (|a ·|) h1 _ ≤ M := le_max_right _ _ -- Proof 3 -- ------- example (k : ℕ) : ∃ M, ∀ i < k, |a i| ≤ M := by set M := ∑ i ∈ range k, |a i| use M -- ⊢ ∀ i < k, |a i| ≤ M intro i hi -- i : ℕ -- hi : i < k -- ⊢ |a i| ≤ M have h1 : ∀ i ∈ range k, 0 ≤ |a i| := by grind grind [single_le_sum] -- Proof 4 -- ------- example (k : ℕ) : ∃ M, ∀ i < k, |a i| ≤ M := by set M := ∑ i ∈ range k, |a i| use M -- ⊢ ∀ i < k, |a i| ≤ M intro i hi -- i : ℕ -- hi : i < k -- ⊢ |a i| ≤ M have h1 : ∀ i ∈ range k, 0 ≤ |a i| := by intro j hj exact abs_nonneg (a j) exact single_le_sum h1 (mem_range.mpr hi) -- Proof 5 -- ------- example (k : ℕ) : ∃ M, ∀ i < k, |a i| ≤ M := by set M := ∑ i ∈ range k, |a i| use M -- ⊢ ∀ i < k, |a i| ≤ M intro i hi -- i : ℕ -- hi : i < k -- ⊢ |a i| ≤ M have h1 : ∀ i ∈ range k, 0 ≤ |a i| := fun j _ => abs_nonneg (a j) exact single_le_sum h1 (mem_range.mpr hi) -- Proof 6 -- ------- example (k : ℕ) : ∃ M, ∀ i < k, |a i| ≤ M := by set M := ∑ i ∈ range k, |a i| use M -- ⊢ ∀ i < k, |a i| ≤ M intro i hi -- i : ℕ -- hi : i < k -- ⊢ |a i| ≤ M exact single_le_sum (fun j _ => abs_nonneg (a j)) (mem_range.mpr hi) -- Proof 7 -- ------- example (k : ℕ) : ∃ M, ∀ i < k, |a i| ≤ M := by set M := ∑ i ∈ range k, |a i| use M -- ⊢ ∀ i < k, |a i| ≤ M exact fun i hi => single_le_sum (fun j _ => abs_nonneg (a j)) (mem_range.mpr hi) -- Proof 8 -- ------- lemma L2 (k : ℕ) : ∃ M, ∀ i < k, |a i| ≤ M := ⟨∑ i ∈ range k, |a i|, fun _ hi => single_le_sum (fun j _ => abs_nonneg (a j)) (mem_range.mpr hi)⟩ -- Proofs of the exercise -- ====================== example (ha : SeqConv a) : SeqBdd a := by obtain ⟨L, hL⟩ := ha -- L : ℝ -- hL : SeqLim a L obtain ⟨k, hk⟩ := L1 a hL -- k : ℕ -- hk : ∀ n ≥ k, |a n| < |L| + 1 obtain ⟨C, hC⟩ := L2 a k -- C : ℝ -- hC : ∀ i < k, |a i| ≤ C set M := max (|L| + 1) C with hM -- hM : M = max (|L| + 1) C use M -- ⊢ ∀ (n : ℕ), |a n| ≤ M intro n -- n : ℕ -- ⊢ |a n| ≤ M rcases lt_or_ge n k with hn1 | hn2 · -- hn1 : n < k calc |a n| ≤ C := hC n hn1 _ ≤ M := le_max_right _ C · -- hn2 : k ≤ n calc |a n| ≤ |L| + 1 := le_of_lt (hk n hn2) _ ≤ M := le_max_left (|L| + 1) _ -- Lemmas used -- =========== variable (n m : ℕ) variable (x y z : ℝ) variable (f : ℝ → ℝ) variable (s : Finset ℕ) #check (Nat.eq_of_le_of_lt_succ : n ≤ m → m < n + 1 → m = n) #check (abs_add_le x y : |x + y| ≤ |x| + |y|) #check (abs_nonneg x : 0 ≤ |x|) #check (add_lt_add_right : y < z → ∀ x, x + y < x + z) #check (add_sub_cancel x y : x + (y - x) = y) #check (congrArg f : x = y → f x = f y) #check (le_max_left x y : x ≤ max x y) #check (le_max_right x y : y ≤ max x y) #check (le_of_lt : x < y → x ≤ y) #check (mem_range : m ∈ range n ↔ m < n) #check (single_le_sum : (∀ i ∈ s, 0 ≤ a i) → ∀ i : ℕ, i ∈ s → a i ≤ ∑ x ∈ s, a x)
You can inspect, modify and run the code of these proofs interactively in Lean 4 Web.
3. Collaborative solutions
Have you found a proof that differs from the published ones? You can share it in the comments below by following these steps:
- Write your proof in live.lean-lang.org and check that it compiles without errors.
- Copy the code and post it in the comments of this entry, inside a Lean code block:
```lean -- your proof ```
Comments