Skip to main content

Challenge 22: Subsequences with different limits imply non-convergence

Also available in:

Español

Prove that if a sequence has two subsequences with different limits, then the sequence is not convergent.

To do so, complete the following theory:

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

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

-- The sequence a is convergent
def SeqConv (a : ℕ → ℝ) : Prop :=
  ∃ L, SeqLim a L

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

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

variable {a b₁ b₂ : ℕ → ℝ}
variable {L L₁ L₂ : ℝ}

example
  (hb₁ : Subseq b₁ a)
  (hL₁ : SeqLim b₁ L₁)
  (hb₂ : Subseq b₂ a)
  (hL₂ : SeqLim b₂ L₂)
  (h : L₁ ≠ L₂)
  : ¬SeqConv a :=
by sorry

1. Proof in natural language

The proof will use two lemmas proved in previous challenges:

  • The lemma seqLim_of_subseq (Challenge 21): every subsequence of a convergent sequence converges to the same limit as the sequence.

  • The lemma seqLim_unique (Challenge 9): if a sequence aₙ converges to both \(L\) and \(M\), then \(L = M\).

To prove the challenge, suppose that the sequence a is convergent, with limit \(L\). Then, by the lemma seqLim_of_subseq, \(b_{1}\) converges to \(L\) and, by the lemma seqLim_unique, we have \[ L_{1} = L \] Similarly, \[ L_{2} = L \] Hence \(L_{1} = L_{2}\), which contradicts the hypothesis \(L_{1} ≠ L_{2}\).

2. Proofs in Lean 4

The proofs use the lemmas seqLim_of_subseq and seqLim_unique from previous challenges. To avoid repeating them in every challenge, the solutions below import them from the RetosLean4 project, which has to be cloned in order to run them. Those who prefer to try the code without installing anything can use the self-contained version, without imports, in Lean 4 Web.

import Mathlib.Tactic
import RetosLean4.Defs -- SeqLim, SeqConv, IsExtraction, Subseq
import RetosLean4.Reto_9 -- seqLim_unique
import RetosLean4.Reto_21 -- seqLim_of_subseq

variable {a b₁ b₂ : ℕ → ℝ}
variable {L L₁ L₂ M : ℝ}

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

example
  (hb₁ : Subseq b₁ a)
  (hL₁ : SeqLim b₁ L₁)
  (hb₂ : Subseq b₂ a)
  (hL₂ : SeqLim b₂ L₂)
  (h : L₁ ≠ L₂)
  : ¬SeqConv a :=
by
  intro h1
  -- h1 : SeqConv a
  -- ⊢ False
  obtain ⟨L, hL⟩ := h1
  -- L : ℝ
  -- hL : SeqLim a L
  apply h
  -- ⊢ L₁ = L₂
  have h2 : SeqLim b₁ L := seqLim_of_subseq hb₁ hL
  have h3 : SeqLim b₂ L := seqLim_of_subseq hb₂ hL
  calc L₁ = L  := seqLim_unique hL₁ h2
       _  = L₂ := seqLim_unique h3 hL₂

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

example
  (hb₁ : Subseq b₁ a)
  (hL₁ : SeqLim b₁ L₁)
  (hb₂ : Subseq b₂ a)
  (hL₂ : SeqLim b₂ L₂)
  (h : L₁ ≠ L₂)
  : ¬SeqConv a :=
by
  rintro ⟨L, hL⟩
  -- L : ℝ
  -- hL : SeqLim a L
  -- ⊢ False
  exact h (Eq.trans
           (seqLim_unique hL₁ (seqLim_of_subseq hb₁ hL))
           (seqLim_unique (seqLim_of_subseq hb₂ hL) hL₂))

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

theorem not_seqConv_of_subseq_seqLim_ne
  (hb₁ : Subseq b₁ a)
  (hL₁ : SeqLim b₁ L₁)
  (hb₂ : Subseq b₂ a)
  (hL₂ : SeqLim b₂ L₂)
  (h : L₁ ≠ L₂)
  : ¬SeqConv a :=
by
  rintro ⟨L, hL⟩
  -- L : ℝ
  -- hL : SeqLim a L
  -- ⊢ False
  exact h ((seqLim_unique hL₁ (seqLim_of_subseq hb₁ hL)).trans
           (seqLim_unique (seqLim_of_subseq hb₂ hL) hL₂))

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