Skip to main content

Challenge 21: Subsequences have the same limit as the sequence

Also available in:

Español

A subsequence is obtained by applying an extraction function to the original sequence; that is, a strictly increasing function \(φ : ℕ \to ℕ\). For example, the subsequence \[ u_{0}, u_{2}, u_{4}, u_{6}, \dots \] is obtained with the extraction function \(\varphi\) defined by \(\varphi(n) = 2n\).

The previous definitions are formalized in Lean 4 as:

-- φ is an extraction function.
def IsExtraction (φ : ℕ → ℕ) :=
  StrictMono φ

-- v is a subsequence of u.
def Subseq (v u : ℕ → ℝ) :=
  ∃ φ, IsExtraction φ ∧ v = u ∘ φ

-- a is the limit of u.
def SeqLim (u : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |u n - a| < ε

Prove that every subsequence of a convergent sequence converges to the same limit as the sequence.

To do so, complete the following Lean 4 theory:

import Mathlib.Data.Real.Basic

variable {u v : ℕ → ℝ}
variable {a : ℝ}

def IsExtraction (φ : ℕ → ℕ):=
  StrictMono φ

def Subseq (v u : ℕ → ℝ) :=
  ∃ φ, IsExtraction φ ∧ v = u ∘ φ

def SeqLim (u : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |u n - a| < ε

example
  (hv : Subseq v u)
  (ha : SeqLim u a)
  : SeqLim v a :=
by sorry

1. Proof in natural language

We will use the following lemma: If \(\varphi\) is an extraction function, then \[ \forall n, n \leq \varphi(n) \]

Since \(v\) is a subsequence of \(u\), there exists an extraction function \(\varphi\) such that \[ v = u ∘ \varphi \tag{1} \]

We have to prove that for every \(\varepsilon > 0\), there exists a \(k \in \mathbb{N}\) such that \[ \forall n \geq k, |v(n) - a| < \varepsilon \tag{2} \]

Since \(a\) is the limit of \(u\), there exists a \(k \in \mathbb{N}\) such that \[ \forall n \geq k, |u(n) - a| < \varepsilon \tag{3} \]

Let us show that \(k\) satisfies (2). To do so, let \(n \geq k\). Then, \[ \varphi(n) \geq k \tag{4} \] since \[ \begin{array}{llll} \varphi(n) &\geq n &&\text{[by the Lemma]} \\ &\geq k \\ \end{array} \] Hence, \[ \begin{array}{llll} |v(n) - a| &= |(u ∘ \varphi)(n) - a| &&\text{[by (1)]} \\ &= |u(\varphi(n)) - a| \\ &< \varepsilon &&\text{[by (3) and (4)]} \end{array} \]

2. Proofs in Lean 4

import Mathlib.Data.Real.Basic

variable {u v : ℕ → ℝ}
variable {a : ℝ}

-- φ is an extraction function.
def IsExtraction (φ : ℕ → ℕ):=
  StrictMono φ

-- v is a subsequence of u.
def Subseq (v u : ℕ → ℝ) :=
  ∃ φ, IsExtraction φ ∧ v = u ∘ φ

-- a is the limit of u.
def SeqLim (u : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ k : ℕ, ∀ n ≥ k, |u n - a| < ε

-- Proof 1
-- =======

example
  (hv : Subseq v u)
  (ha : SeqLim u a)
  : SeqLim v a :=
by
  obtain ⟨φ, hφ, hφ'⟩ := hv
  -- φ : ℕ → ℕ
  -- hφ : IsExtraction φ
  -- hφ' : v = u ∘ φ
  intros ε hε
  -- ε : ℝ
  -- hε : ε > 0
  -- ⊢ ∃ k, ∀ n ≥ k, |v n - a| < ε
  obtain ⟨k, hk⟩ := ha ε hε
  -- k : ℕ
  -- hk : ∀ n ≥ k, |u n - a| < ε
  use k
  -- ⊢ ∀ n ≥ k, |v n - a| < ε
  intros n hn
  -- n : ℕ
  -- hn : n ≥ k
  -- ⊢ |v n - a| < ε
  have h1 : φ n ≥ k :=
    calc φ n
         ≥ n := StrictMono.le_apply hφ
       _ ≥ k := hn
  calc |v n - a|
       = |(u ∘ φ ) n  - a| := by rw [hφ']
     _ = |u (φ n) - a|     := rfl
     _ < ε                 := hk (φ n) h1

-- Proof 2
-- =======

example
  (hv : Subseq v u)
  (ha : SeqLim u a)
  : SeqLim v a :=
by
  obtain ⟨φ, hφ, rfl⟩ := hv
  -- φ : ℕ → ℕ
  -- hφ : IsExtraction φ
  -- ⊢ SeqLim (u ∘ φ) a
  intros ε hε
  -- ε : ℝ
  -- hε : ε > 0
  -- ⊢ ∃ k, ∀ n ≥ k, |(u ∘ φ) n - a| < ε
  obtain ⟨k, hk⟩ := ha ε hε
  -- k : ℕ
  -- hk : ∀ n ≥ k, |u n - a| < ε
  use k
  -- ⊢ ∀ n ≥ k, |(u ∘ φ) n - a| < ε
  intros n hn
  -- n : ℕ
  -- hn : n ≥ k
  -- ⊢ |(u ∘ φ) n - a| < ε
  have h1 : φ n ≥ k :=
    calc φ n
         ≥ n := hφ.le_apply
       _ ≥ k := hn
  calc |(u ∘ φ) n  - a|
     _ = |u (φ n) - a|     := rfl
     _ < ε                 := hk (φ n) h1

-- Proof 3
-- =======

example
  (hv : Subseq v u)
  (ha : SeqLim u a)
  : SeqLim v a :=
by
  obtain ⟨φ, hφ, rfl⟩ := hv
  -- φ : ℕ → ℕ
  -- hφ : IsExtraction φ
  -- ⊢ SeqLim (u ∘ φ) a
  intros ε hε
  -- ε : ℝ
  -- hε : ε > 0
  -- ⊢ ∃ k, ∀ n ≥ k, |(u ∘ φ) n - a| < ε
  obtain ⟨k, hk⟩ := ha ε hε
  -- k : ℕ
  -- hk : ∀ n ≥ k, |u n - a| < ε
  use k
  -- ⊢ ∀ n ≥ k, |(u ∘ φ) n - a| < ε
  intros n hn
  -- n : ℕ
  -- hn : n ≥ k
  -- ⊢ |(u ∘ φ) n - a| < ε
  apply hk
  -- ⊢ φ n ≥ k
  apply le_trans hn
  -- ⊢ n ≤ φ n
  exact hφ.le_apply

-- Proof 4
-- =======

example
  (hv : Subseq v u)
  (ha : SeqLim u a)
  : SeqLim v a :=
by
  obtain ⟨φ, hφ, rfl⟩ := hv
  -- φ : ℕ → ℕ
  -- hφ : IsExtraction φ
  -- ⊢ SeqLim (u ∘ φ) a
  intros ε hε
  -- ε : ℝ
  -- hε : ε > 0
  -- ⊢ ∃ k, ∀ n ≥ k, |(u ∘ φ) n - a| < ε
  obtain ⟨k, hk⟩ := ha ε hε
  -- k : ℕ
  -- hk : ∀ n ≥ k, |u n - a| < ε
  exact ⟨k, fun n hn ↦ hk (φ n) (le_trans hn hφ.le_apply)⟩

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