Suppose that the sequence \(c_n\) is an interleaving of the sequences \(a_n\) and \(b_n\); that is, that \[ (c_0, c_1, c_2, \dots) = (a_0, b_0, a_1, b_1, a_2, b_2, \dots) \]

Prove that if \(c_n\) converges to \(L\), then \(a_n\) and \(b_n\) converge to \(L\).

To do so, complete the following theory

import Mathlib.Tactic

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

example
  (hc : ∀ n, c n = if Even n
                   then a (n / 2)
                   else b ((n - 1) / 2))
  (hL : SeqLim c L)
  : SeqLim a L ∧ SeqLim b L :=
by sorry

Read more…

Using Challenge 22 (which states that if a sequence has two subsequences that converge to different limits, then the sequence is not convergent), prove that the sequence defined by 1, -1, 1, -1, ... is not convergent.

To do so, complete the following theory:

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 : ℕ → ℝ}

example
  (ha : ∀ n, a n = (-1)^n)
  : ¬SeqConv a :=
by sorry

Read more…

Prove that the constant sequence \(a_{n} = L\) converges to \(L\).

To do so, complete the following theory:

import Mathlib.Tactic

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

variable {a : ℕ → ℝ}
variable {L : ℝ}

example
  (h : ∀ n, a n = L)
  : SeqLim a L :=
by sorry

Read more…

Introduction

Who it is for. This guide is aimed at teachers who want to introduce Lean 4 to mathematics students who are used to writing proofs on paper but have no previous programming experience. No prior knowledge of computer science is required.

Philosophy of the course.

1. Lean is a proof notebook that talks back. You write an argument and the computer tells you, step by step, what is missing. It is presented as a patient interlocutor, not as a programming language.
2. Mathematics first, syntax later. Each topic starts from a proof the student already knows how to do on paper and translates it into Lean.
3. No installation at the beginning. The first three sessions can be done in the browser. Local installation comes when the student already wants to carry on alone.
4. You learn by reading the proof state. The central skill is not memorizing tactics, but reading the goals window (the infoview) the way one reads a blackboard.
5. Making mistakes is cheap. The red error is information, not a failure.

Structure. Eight topics of about 2 hours each (theory and practice mixed). Each topic has two parts: the content (what the student sees) and the teaching tips (notes for the teacher with key ideas, typical mistakes, ...).

Convention. All the examples start with import Mathlib.Tactic, Lean's library of tactics. The code blocks can be pasted as they are into the editor.

Read more…

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

Read more…

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

Read more…

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 so, 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

Read more…

Prove that convergent sequences are Cauchy sequences

To do so, complete the following Lean 4 theory:

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

variable {u : ℕ → ℝ}

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

def SeqConv (u : ℕ → ℝ) :=
  ∃ a, SeqLim u a

def IsCauchy (u : ℕ → ℝ) :=
  ∀ ε > 0, ∃ k, ∀ p ≥ k, ∀ q ≥ k, |u p - u q| < ε

example
  (h : SeqConv u)
  : IsCauchy u :=
by sorry

Read more…

Prove that if the sequence \(aₙ\) converges to \(L\) and \(bₙ\) converges to \(M\), then \(aₙbₙ\) converges to \(LM\).

To do so, 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| < ε

variable {a b c : ℕ → ℝ}
variable {L M : ℝ}

example
  (ha : SeqLim a L)
  (hb : SeqLim b M)
  (hc : ∀ n, c n = a n * b n)
  : SeqLim c (L * M) :=
by sorry

Read more…