Challenge 20: If aₙ → L and M is an upper bound of aₙ, then L ≤ M
Prove that if the sequence \(a_{n}\) converges to \(L\) and \(M\) is an upper bound of \(a_{n}\) (that is, \(a_{n} ≤ M\) for all \(n\)), then \(L ≤ M\).
To do this, complete the following Lean 4 theory:
import Mathlib.Data.Real.Basic import Mathlib.Tactic def SeqLim (a : ℕ → ℝ) (L : ℝ) : Prop := ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |a n - L| < ε def IsUB (a : ℕ → ℝ) (M : ℝ) : Prop := ∀ n, a n ≤ M variable {a : ℕ → ℝ} variable {L M : ℝ} example (ha : SeqLim a L) (hM : IsUB a M) : L ≤ M := by sorry
1. Proof in natural language
We prove it by contradiction. Suppose that \[ L > M \tag{1} \] and we will reach the contradiction \(M < M\).
From (1), we have \[ L - M > 0 \] and, using this quantity in the convergence of \(a_n\), we obtain a \(k\) such that \[ ∀ n ≥ k, |a_n - L| < L - M \tag{2} \] In particular, for \(n = k\) (which satisfies \(k ≥ k\)), from (2) we obtain \[ |a_k - L| < L - M \tag{3} \] Moreover, \[ L - a_k ≤ |a_k - L| \tag{4} \] since \[ \begin{array}{ll} L - a_k &= -(a_k - L) \\ &≤ |a_k - L| \end{array} \] Finally, \[ \begin{array}{llll} M &= L - (L - M) \\ &< L - |a_k - L| &&\text{[by (3)]} \\ &≤ L - (L - a_k) &&\text{[by (4)]} \\ &= a_k \\ &≤ M &&\text{[because \(M\) is an upper bound of \(a_n\)]} \\ \end{array} \] Therefore, \(M < M\).
2. Proofs in Lean 4
import Mathlib.Data.Real.Basic import Mathlib.Tactic def SeqLim (a : ℕ → ℝ) (L : ℝ) : Prop := ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |a n - L| < ε def IsUB (a : ℕ → ℝ) (M : ℝ) : Prop := ∀ n, a n ≤ M variable {a : ℕ → ℝ} variable {L M : ℝ} -- Proof 1 -- ======= example (ha : SeqLim a L) (hM : IsUB a M) : L ≤ M := by by_contra hL -- hL : ¬L ≤ M -- ⊢ False apply lt_irrefl M -- ⊢ M < M obtain ⟨k, hk⟩ := ha (L - M) (by grind) -- k : ℕ -- hk : ∀ n ≥ k, |a n - L| < L - M calc M < a k := by grind _ ≤ M := hM k -- Proof 2 -- ======= example (ha : SeqLim a L) (hM : IsUB a M) : L ≤ M := by by_contra hL -- hL : ¬L ≤ M -- ⊢ False apply lt_irrefl M -- ⊢ M < M have h1 : L > M := not_le.mp hL have h2 : L - M > 0 := sub_pos.mpr h1 obtain ⟨k, hk⟩ := ha (L - M) h2 -- k : ℕ -- hk : ∀ n ≥ k, |a n - L| < L - M calc M = L - (L - M) := by grind _ < L - |a k - L| := by grind _ ≤ L - (L - a k) := by grind _ = a k := by grind _ ≤ M := hM k -- Proof 3 -- ======= example (ha : SeqLim a L) (hM : IsUB a M) : L ≤ M := by by_contra hL -- hL : ¬L ≤ M -- ⊢ False apply lt_irrefl M -- ⊢ M < M have h1 : L - M > 0 := sub_pos.mpr (not_le.mp hL) obtain ⟨k, hk⟩ := ha (L - M) h1 -- k : ℕ -- hk : ∀ n ≥ k, |a n - L| < L - M have h2 : |a k - L| < L - M := hk k (le_refl k) have h3 : L - a k ≤ |a k - L| := by calc L - a k = -(a k - L) := by ring _ ≤ |a k - L| := neg_le_abs (a k - L) calc M = L - (L - M) := by ring _ < L - |a k - L| := sub_lt_sub_left h2 L _ ≤ L - (L - a k) := by gcongr _ = a k := by ring _ ≤ M := hM k -- Proof 4 -- ======= example (ha : SeqLim a L) (hM : IsUB a M) : L ≤ M := by by_contra hL -- hL : ¬L ≤ M -- ⊢ False apply lt_irrefl M -- ⊢ M < M obtain ⟨k, hk⟩ := ha (L - M) (sub_pos.mpr (not_le.mp hL)) -- k : ℕ -- hk : ∀ n ≥ k, |a n - L| < L - M have h1 : |a k - L| < L - M := hk k (le_refl k) have h2 : L - a k ≤ |a k - L| := by calc L - a k = -(a k - L) := (neg_sub (a k) L).symm _ ≤ |a k - L| := neg_le_abs (a k - L) calc M = L - (L - M) := (sub_sub_self L M).symm _ < L - |a k - L| := sub_lt_sub_left h1 L _ ≤ L - (L - a k) := sub_le_sub_left h2 L _ = a k := sub_sub_self L (a k) _ ≤ M := hM k -- Lemmas used -- ============ variable (x y : ℝ) #check (le_refl x : x ≤ x) #check (lt_irrefl x : ¬x < x) #check (neg_le_abs x : -x ≤ |x|) #check (neg_sub x y : -(x - y) = y - x) #check (not_le : ¬x ≤ y ↔ y < x) #check (sub_le_sub_left : x ≤ y → ∀ z, z - y ≤ z - x) #check (sub_lt_sub_left : x < y → ∀ z, z - y < z - x) #check (sub_pos : 0 < x - y ↔ y < x) #check (sub_sub_self x y : x - (x - y) = y)
You can consult, modify and execute the code of these proofs interactively in Lean 4 Web.