## Stream: new members

### Topic: return limit of convergent sequence

#### Dudu (Dec 05 2021 at 19:33):

Hello,

How can I write a function that takes as input a convergent sequence and outputs its limit? I've tried this:

import tactic
import data.real.basic

noncomputable

def d : ℝ → ℝ → ℝ := λ(a b : ℝ), |a-b|

def seq_has_lim (a : ℕ → ℝ) (L : ℝ) :=
∀(ε : ℝ)(hε : ε > 0),∃(N : ℕ),∀(n : ℕ)(hn: n ≥ N),
d (a n) L < ε

def convergent_seqs :=
{a : ℕ → ℝ | ∃(L : ℝ), seq_has_lim a L}

def lim_of_seq : convergent_seqs →  ℝ :=
begin
intro a,
cases a with a ha,
change ∃(L : ℝ), seq_has_lim a L at ha,
cases ha with L hL,
exact L,
end


This does not work since the cases tactic requires that the goal is of type Prop (if I understood it correctly...). Also, from what I've managed to find here, apparently it is not a good idea to use tactics in a definition. I imagine I need to use the fact that limits are unique somewhere, but I don't see how.

#### Kevin Buzzard (Dec 05 2021 at 19:42):

You use classical.some

#### Dudu (Dec 05 2021 at 20:27):

Oh, thank you. But still, when doing something like this informally we normally first show that limits are unique so that our function is well defined. Here we didn't use that fact. Is the way to go here to just define the function

def lim_of_seq : convergent_seqs →  ℝ :=
begin
intro a,
cases a with a ha,
change ∃(L : ℝ), seq_has_lim a L at ha,
exact classical.some ha,
end


and then show that any function in convergent_seqs → ℝ that assigns a sequence to its limit must be equal to lim_of_seq?

#### Kevin Buzzard (Dec 05 2021 at 20:28):

The way to think about classical.some is that Lean chooses once and for all an element of every nonempty type. You have an assertion that some limit exists, so the type of limits is nonempty, so the function returns the term of that type which it chose when you switched Lean on.

#### Kevin Buzzard (Dec 05 2021 at 20:30):

noncomputable def lim_of_seq : convergent_seqs →  ℝ :=
λ a, classical.some (a.2)

lemma lim_of_seq.is_limit (s : convergent_seqs) :
seq_has_lim s.1 (lim_of_seq s) := classical.some_spec s.2


#### Kevin Buzzard (Dec 05 2021 at 20:31):

This is just a style issue -- there's no need to use tactic mode to make the definition, and the moment you make the definition you should make the key API for the definition, namely the assertion that the definition returns something which satisfies the definition of the limit.

#### Kevin Buzzard (Dec 05 2021 at 20:33):

The thing with mathematical content is

lemma lim_of_seq.limit_unique (s : convergent_seqs) (L : ℝ) :
seq_has_lim s.1 L → L = lim_of_seq s :=
begin
sorry
end


#### Dudu (Dec 05 2021 at 20:40):

I see, this cleared things up a lot. Thank you!

#### Kevin Buzzard (Dec 05 2021 at 20:45):

In Lean the idiomatic thing to do is, perhaps surprisingly, not even make the subtype of convergent sequences, but define the limit of an arbitrary sequence! If it converges, define the limit to be something it converges to, and if it doesn't converge then just define the limit to be 37. Then you don't have to worry about all this s.1 stuff.

#### Kevin Buzzard (Dec 05 2021 at 20:55):

Maybe this is a little more idiomatic:

import tactic
import data.real.basic

noncomputable

def d : ℝ → ℝ → ℝ := λ(a b : ℝ), |a-b|

def is_lim (a : ℕ → ℝ) (L : ℝ) :=
∀ ε > 0, ∃ N, ∀ n ≥ N, d (a n) L < ε

-- def convergent_seqs :=
-- {a : ℕ → ℝ | ∃(L : ℝ), seq_has_lim a L}

def seq_has_lim (a : ℕ → ℝ) : Prop := ∃ L, is_lim a L

open_locale classical

noncomputable def lim_of_seq (a : ℕ → ℝ) : ℝ :=
if h : seq_has_lim a then classical.some h else 37

lemma lim_of_seq.is_limit (a : ℕ → ℝ) (ha : seq_has_lim a) :
is_lim a (lim_of_seq a) :=
begin
unfold lim_of_seq,
rw dif_pos ha,
exact classical.some_spec ha
end

lemma lim_of_seq.limit_unique (a : ℕ → ℝ) (ha : seq_has_lim a) (M : ℝ) :
is_lim a M → M = lim_of_seq a :=
begin
sorry
end


But there's nothing wrong with your way, especially if you're just experimenting.

#### Patrick Massot (Dec 05 2021 at 20:56):

For the record, all this is already in mathlib, see docs#lim. When I started using Lean, I thought that would be a very useful and common definition. It turns out I was completely wrong, and this is barely used.

#### Dudu (Dec 05 2021 at 21:04):

@Kevin Buzzard Wow, this approach really is surprising, but after some thought I think I see why it makes sense, I appreciate the suggestion :)

#### Kevin Buzzard (Dec 05 2021 at 21:07):

The problem is when you start doing things like "limit of sum is sum of limits" -- you want to just add the sequences and talk about the limit of the sum, but if you can't even talk about the limit before you've proved it converges then it makes things much more convoluted. If you want to understand what I'm talking about, keep working the way you're doing!

Another approach is not to even define this "limit of a sequence" function _at all_, and just prove things like seq_has_lim a L -> seq_has_lim b M -> seq_has_lim (a + b) (L + M). This works fine.

#### Kevin Buzzard (Dec 05 2021 at 21:08):

That was the approach I took in my course earlier this year: https://github.com/ImperialCollegeLondon/formalising-mathematics/blob/master/src/week_3/Part_A_limits.lean

#### Eduardo Freire (Dec 05 2021 at 21:26):

I did try proving one lemma using the my first approach and realized that it would be a bit annoying, I'll definitely use that last approach from now on.

Also, this course looks great, I can't believe I didn't find it before!

#### Patrick Massot (Dec 05 2021 at 21:31):

Did you do the tutorials project first? It's full of limits of sequences.

#### Eduardo Freire (Dec 05 2021 at 21:34):

I did, but it didn't include this function that takes a sequence and returns its limit and I initially thought that that would be a better way to do things

Last updated: Dec 20 2023 at 11:08 UTC