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 this, 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₂)
  : ¬SucConvergente a :=
by sorry

1. Proof in natural language

The proof will use two lemmas proved in previous challenges:

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

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

For the proof of the challenge, suppose that the sequence a is convergent. Then, by the lemma seqLim_of_subseq, we have that \(b_{1}\) converges to \(L\) and, by the lemma seqLim_unique, we have that \[ L_{1} = L \] Similarly, we have that \[ L_{2} = L \] Therefore \(L_{1} = L_{2}\) in contradiction with the hypothesis \(L_{1} ≠ L_{2}\).

2. Proofs in Lean 4

The proof uses the lemmas seqLim_of_subseq and seqLim_unique from previous challenges. To avoid repeating them in each challenge, the following solutions import them from the RetosLean4 project, which must be cloned to run them. Those who prefer to test 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₂)
  : ¬SucConvergente 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₂)
  : ¬SucConvergente 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₂)
  : ¬SucConvergente 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 consult, modify and execute the code of these proofs interactively in Lean 4 Web.