return limit of convergent sequence

Stream: new members

[Dudu]

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]

You use classical.some

[Dudu]

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]

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]

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]

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]

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]

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

[Kevin Buzzard]

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]

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]

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]

@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]

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]

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]

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]

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

[Kevin Buzzard]

It's here: https://github.com/leanprover-community/tutorials

[Eduardo Freire]

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