# Limits of sequences

## Basic definitions

In this file, we introduce limits of sequences of real numbers.

We model a sequence $a₀, a₁, a₂, \dots$ of real numbers as a function from $ℕ := \{0,1,2,\dots\}$ to $ℝ$, sending $n$ to $a_n$. So in the below definition of the limit of a sequence, $a : ℕ → ℝ$ is the sequence.

Definition
A sequence $a$ converges to a real number $l$ if, for all positive $ε$, there is some $N$ such that, for every $n ≥ N$, $|a_n - l| < ε$.
definition is_limit (a : ℕ → ℝ) (l : ℝ) : Prop :=
∀ ε > 0, ∃ N, ∀ n ≥ N, | a n - l | < ε

Definition
A sequence converges if and only if it has a limit.
definition has_limit (a : ℕ → ℝ) : Prop := ∃ l : ℝ, is_limit a l


The difference between the above definition and the preceding one is that we don't specify the limit, we just claim that it exists.

## Basic lemmas

Lemma
The constant sequence with value $a$ converges to $a$.
lemma tendsto_const (a : ℝ) : is_limit (λ n, a) a :=

Proof
Let $ε$ be any positive real number.
  intros ε εpos,

a : ℝ
⊢ is_limit (λ (n : ℕ), a) a

a ε : ℝ,
εpos : ε > 0
⊢ ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |(λ (n : ℕ), a) n - a| < ε

We choose $N = 0$ in the definition of a limit,
  use 0,

a ε : ℝ,
εpos : ε > 0
⊢ ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |(λ (n : ℕ), a) n - a| < ε

a ε : ℝ,
εpos : ε > 0
⊢ ∀ (n : ℕ), n ≥ 0 → |(λ (n : ℕ), a) n - a| < ε

and observe that, for every $n ≥ N$, |a - a| < ε
  intros n _,

a ε : ℝ,
εpos : ε > 0
⊢ ∀ (n : ℕ), n ≥ 0 → |(λ (n : ℕ), a) n - a| < ε

a ε : ℝ,
εpos : ε > 0,
n : ℕ,
H : n ≥ 0
⊢ |(λ (n : ℕ), a) n - a| < ε

  simpa [sub_self] using εpos

a ε : ℝ,
εpos : ε > 0,
n : ℕ,
H : n ≥ 0
⊢ |(λ (n : ℕ), a) n - a| < ε

a ε : ℝ,
εpos : ε > 0,
n : ℕ,
H : n ≥ 0
⊢ |(λ (n : ℕ), a) n - a| < ε

QED.

We will need an easy reformulation of the limit definition

Lemma
A sequence $a_n$ converges to a number $l$ if and only if the sequence $a_n - l$ converges to zero.
lemma tendsto_iff_sub_tendsto_zero {a : ℕ → ℝ} {l : ℝ} :
is_limit (λ n, a n - l) 0 ↔ is_limit a l :=

Proof
We need to prove both implications, but both proofs are the same.
  split ;

a : ℕ → ℝ,
l : ℝ
⊢ is_limit (λ (n : ℕ), a n - l) 0 ↔ is_limit a l

a : ℕ → ℝ,
l : ℝ
⊢ is_limit (λ (n : ℕ), a n - l) 0 ↔ is_limit a l

We assume the premise, and consider any positive $ε$.
    intros h ε εpos,

a : ℕ → ℝ,
l : ℝ
⊢ is_limit (λ (n : ℕ), a n - l) 0 → is_limit a l

a : ℕ → ℝ,
l : ℝ,
h : is_limit (λ (n : ℕ), a n - l) 0,
ε : ℝ,
εpos : ε > 0
⊢ ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |a n - l| < ε

By the premise specialized to our $ε$, we get some $N$,
    rcases h ε εpos with ⟨N, H⟩,

a : ℕ → ℝ,
l : ℝ,
h : is_limit (λ (n : ℕ), a n - l) 0,
ε : ℝ,
εpos : ε > 0
⊢ ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |a n - l| < ε

a : ℕ → ℝ,
l : ℝ,
h : is_limit (λ (n : ℕ), a n - l) 0,
ε : ℝ,
εpos : ε > 0,
N : ℕ,
H : ∀ (n : ℕ), n ≥ N → |(λ (n : ℕ), a n - l) n - 0| < ε
⊢ ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |a n - l| < ε

and use that $N$ to prove the other condition
    use N,

a : ℕ → ℝ,
l : ℝ,
h : is_limit (λ (n : ℕ), a n - l) 0,
ε : ℝ,
εpos : ε > 0,
N : ℕ,
H : ∀ (n : ℕ), n ≥ N → |(λ (n : ℕ), a n - l) n - 0| < ε
⊢ ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |a n - l| < ε

a : ℕ → ℝ,
l : ℝ,
h : is_limit (λ (n : ℕ), a n - l) 0,
ε : ℝ,
εpos : ε > 0,
N : ℕ,
H : ∀ (n : ℕ), n ≥ N → |(λ (n : ℕ), a n - l) n - 0| < ε
⊢ ∀ (n : ℕ), n ≥ N → |a n - l| < ε

which is immediate.
    intros n hn,

a : ℕ → ℝ,
l : ℝ,
h : is_limit (λ (n : ℕ), a n - l) 0,
ε : ℝ,
εpos : ε > 0,
N : ℕ,
H : ∀ (n : ℕ), n ≥ N → |(λ (n : ℕ), a n - l) n - 0| < ε
⊢ ∀ (n : ℕ), n ≥ N → |a n - l| < ε

a : ℕ → ℝ,
l : ℝ,
h : is_limit (λ (n : ℕ), a n - l) 0,
ε : ℝ,
εpos : ε > 0,
N : ℕ,
H : ∀ (n : ℕ), n ≥ N → |(λ (n : ℕ), a n - l) n - 0| < ε,
n : ℕ,
hn : n ≥ N
⊢ |a n - l| < ε

    simpa using H n hn }

a : ℕ → ℝ,
l : ℝ,
h : is_limit (λ (n : ℕ), a n - l) 0,
ε : ℝ,
εpos : ε > 0,
N : ℕ,
H : ∀ (n : ℕ), n ≥ N → |(λ (n : ℕ), a n - l) n - 0| < ε,
n : ℕ,
hn : n ≥ N
⊢ |a n - l| < ε

no goals

QED.

In the definition of a limit, the final ε can be replaced by a constant multiple of ε. We could assume this constant is positive but we don't want to deal with this when applying the lemma.

Lemma
Let $a$ be a sequence. In order to prove that $a$ converges to some limit $l$, it is sufficient to find some number $K$ such that, for all $ε > 0$, there is some $N$ such that, for all $n ≥ N$, $|a_n - l| < Kε$.
lemma tendsto_of_mul_eps (a : ℕ → ℝ) (l : ℝ) (K : ℝ)
(h : ∀ ε > 0, ∃ N, ∀ n ≥ N, | a n - l | < K*ε) : is_limit a l :=

Proof
Let $ε$ be any positive number.
  intros ε εpos,

a : ℕ → ℝ,
l K : ℝ,
h : ∀ (ε : ℝ), ε > 0 → (∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |a n - l| < K * ε)
⊢ is_limit a l

a : ℕ → ℝ,
l K : ℝ,
h : ∀ (ε : ℝ), ε > 0 → (∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |a n - l| < K * ε),
ε : ℝ,
εpos : ε > 0
⊢ ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |a n - l| < ε

$K$ is either non positive or positive
  cases le_or_gt K 0 with Knonpos Kpos,

a : ℕ → ℝ,
l K : ℝ,
h : ∀ (ε : ℝ), ε > 0 → (∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |a n - l| < K * ε),
ε : ℝ,
εpos : ε > 0
⊢ ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |a n - l| < ε

2 goals
case or.inl
a : ℕ → ℝ,
l K : ℝ,
h : ∀ (ε : ℝ), ε > 0 → (∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |a n - l| < K * ε),
ε : ℝ,
εpos : ε > 0,
Knonpos : K ≤ 0
⊢ ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |a n - l| < ε

case or.inr
a : ℕ → ℝ,
l K : ℝ,
h : ∀ (ε : ℝ), ε > 0 → (∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |a n - l| < K * ε),
ε : ℝ,
εpos : ε > 0,
Kpos : K > 0
⊢ ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |a n - l| < ε

If $K$ is non positive then our assumed bound quicklygives a contradiction.
    exfalso,

case or.inl
a : ℕ → ℝ,
l K : ℝ,
h : ∀ (ε : ℝ), ε > 0 → (∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |a n - l| < K * ε),
ε : ℝ,
εpos : ε > 0,
Knonpos : K ≤ 0
⊢ ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |a n - l| < ε

a : ℕ → ℝ,
l K : ℝ,
h : ∀ (ε : ℝ), ε > 0 → (∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |a n - l| < K * ε),
ε : ℝ,
εpos : ε > 0,
Knonpos : K ≤ 0
⊢ false

Indeed we can apply our assumption to $ε = 1$ to get $N$ such thatfor all $n ≥ N$, $|a n - l| < K * 1$
    rcases h 1 (by linarith) with ⟨N, H⟩,

a : ℕ → ℝ,
l K : ℝ,
h : ∀ (ε : ℝ), ε > 0 → (∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |a n - l| < K * ε),
ε : ℝ,
εpos : ε > 0,
Knonpos : K ≤ 0
⊢ false

a : ℕ → ℝ,
l K : ℝ,
h : ∀ (ε : ℝ), ε > 0 → (∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |a n - l| < K * ε),
ε : ℝ,
εpos : ε > 0,
Knonpos : K ≤ 0,
N : ℕ,
H : ∀ (n : ℕ), n ≥ N → |a n - l| < K * 1
⊢ false

in particular this holds when $n = N$
    specialize H N (by linarith),

a : ℕ → ℝ,
l K : ℝ,
h : ∀ (ε : ℝ), ε > 0 → (∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |a n - l| < K * ε),
ε : ℝ,
εpos : ε > 0,
Knonpos : K ≤ 0,
N : ℕ,
H : ∀ (n : ℕ), n ≥ N → |a n - l| < K * 1
⊢ false

a : ℕ → ℝ,
l K : ℝ,
h : ∀ (ε : ℝ), ε > 0 → (∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |a n - l| < K * ε),
ε : ℝ,
εpos : ε > 0,
Knonpos : K ≤ 0,
N : ℕ,
H : |a N - l| < K * 1
⊢ false

but $|a N - l| ≥ 0$ so we get a contradiction.
    have : |a N - l| ≥ 0, from abs_nonneg _,

a : ℕ → ℝ,
l K : ℝ,
h : ∀ (ε : ℝ), ε > 0 → (∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |a n - l| < K * ε),
ε : ℝ,
εpos : ε > 0,
Knonpos : K ≤ 0,
N : ℕ,
H : |a N - l| < K * 1
⊢ false

a : ℕ → ℝ,
l K : ℝ,
h : ∀ (ε : ℝ), ε > 0 → (∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |a n - l| < K * ε),
ε : ℝ,
εpos : ε > 0,
Knonpos : K ≤ 0,
N : ℕ,
H : |a N - l| < K * 1,
this : |a N - l| ≥ 0
⊢ false

    linarith },

a : ℕ → ℝ,
l K : ℝ,
h : ∀ (ε : ℝ), ε > 0 → (∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |a n - l| < K * ε),
ε : ℝ,
εpos : ε > 0,
Knonpos : K ≤ 0,
N : ℕ,
H : |a N - l| < K * 1,
this : |a N - l| ≥ 0
⊢ false

case or.inr
a : ℕ → ℝ,
l K : ℝ,
h : ∀ (ε : ℝ), ε > 0 → (∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |a n - l| < K * ε),
ε : ℝ,
εpos : ε > 0,
Kpos : K > 0
⊢ ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |a n - l| < ε

Now assume $K$ is positive. Our assumption gives $N$ such that,for all $n ≥ N$, $|a n - l| < K * (ε / K)$
    rcases h (ε/K) (div_pos εpos Kpos) with ⟨N, H⟩,

case or.inr
a : ℕ → ℝ,
l K : ℝ,
h : ∀ (ε : ℝ), ε > 0 → (∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |a n - l| < K * ε),
ε : ℝ,
εpos : ε > 0,
Kpos : K > 0
⊢ ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |a n - l| < ε

a : ℕ → ℝ,
l K : ℝ,
h : ∀ (ε : ℝ), ε > 0 → (∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |a n - l| < K * ε),
ε : ℝ,
εpos : ε > 0,
Kpos : K > 0,
N : ℕ,
H : ∀ (n : ℕ), n ≥ N → |a n - l| < K * (ε / K)
⊢ ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |a n - l| < ε

we can simplify that $K (ε / K)$ and we are done.
    rw mul_div_cancel' _ (ne_of_gt Kpos) at H,

a : ℕ → ℝ,
l K : ℝ,
h : ∀ (ε : ℝ), ε > 0 → (∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |a n - l| < K * ε),
ε : ℝ,
εpos : ε > 0,
Kpos : K > 0,
N : ℕ,
H : ∀ (n : ℕ), n ≥ N → |a n - l| < K * (ε / K)
⊢ ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |a n - l| < ε

a : ℕ → ℝ,
l K : ℝ,
h : ∀ (ε : ℝ), ε > 0 → (∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |a n - l| < K * ε),
ε : ℝ,
εpos : ε > 0,
Kpos : K > 0,
N : ℕ,
H : ∀ (n : ℕ), n ≥ N → |a n - l| < ε
⊢ ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |a n - l| < ε

    tauto }

a : ℕ → ℝ,
l K : ℝ,
h : ∀ (ε : ℝ), ε > 0 → (∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |a n - l| < K * ε),
ε : ℝ,
εpos : ε > 0,
Kpos : K > 0,
N : ℕ,
H : ∀ (n : ℕ), n ≥ N → |a n - l| < ε
⊢ ∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |a n - l| < ε

no goals

QED.