convergent sequences are bounded

Stream: maths

[Kevin Buzzard]

How do I prove that a convergent sequence is bounded in Lean, in a way which is comprehensible to undergraduates? Say a_n tends to L. Setting epsilon=1 I know that for n>=N I have |a_n|<=|L|+1 by the triangle inequality. Now I need to let B be the max of |l|+1 and |a_n| for n<N (and then |a_n|<=B for all n). Mathematicians would say this was "trivial" so ideally I'd like to use as much automation as possible.

[Kevin Buzzard]

[I'll just write the boilerplate now]

[Kevin Buzzard]

import data.real.basic
import tactic.linarith

noncomputable theory
local attribute [instance, priority 0] classical.prop_decidable

local notation `|` x `|` := abs x

definition is_limit (a : ℕ → ℝ) (l : ℝ) : Prop :=
∀ ε > 0, ∃ N, ∀ n ≥ N, | a n - l | < ε

definition is_bounded (a : ℕ → ℝ) : Prop := ∃ B : ℝ, ∀ n, |a n| ≤ B

theorem convergent_implies_bounded (a : ℕ → ℝ) : (∃ l, is_limit a l) → is_bounded a := sorry

I am a bit scared that my proof looks intimidating.

I was just watching Patrick proving that all epis were split in the category of sets and I thought it was going to be horrible but he just used this "choose" tactic and it was wonderful. I'm now wondering whether I can pull off something equally slick looking with this.

[Andrew Ashworth]

A slick proof would be interesting. I tried doing a bit of basic analysis in Lean a long time ago, my proofs took me forever to write.

[Andrew Ashworth]

Just proving Cauchy sequences were bounded led me to:

[Andrew Ashworth]

-- Lemma 5.1.15 (Cauchy sequences are bounded).
example : ∃ r, ∀ i, abv (f i) < r :=
let ⟨i, h⟩ := cauchy f zero_lt_one in
let R := (finset.range (i+1)).sum (λ j, abv (f j)) in
have h₁ : ∀ j ≤ i, abv (f j) ≤ R, from
  λ j ij, show (λ j, abv (f j)) j ≤ R, from
  finset.single_le_sum
    (λ k hk, is_absolute_value.abv_nonneg abv (f k))
    (by rwa [finset.mem_range, nat.lt_succ_iff]),
exists.intro (R + 1) (λ j, or.elim (lt_or_le j i)
  (λ h₂,
    let h₃ := le_of_lt h₂ in
    lt_of_le_of_lt (h₁ j h₃) (lt_add_one R))
  (λ ij,
    let h₃ := lt_of_le_of_lt (is_absolute_value.abv_add abv _ _)
      (add_lt_add_of_le_of_lt (h₁ _ (le_refl i)) (h j ij)) in
    by rw [add_sub, add_comm] at h₃; simpa using h₃))

[Kevin Buzzard]

finset.max spits out a term of type option alpha. How come the one time I _want_ it to spit out zero (on the basis that forall x in X, x <= finset.max X would still be true when X is empty) it uses the option trick? :-/

[Kevin Buzzard]

Yeah, that code looks really intimidating. Obviously Lean code can become intimidating after a certain level, but I was hoping I had not got to that point yet, I'm trying to show the undergraduates how to use this thing.

[Kevin Buzzard]

How close can I get to $X:=\max\{|a_n|\,|\,n\leq N\}$ plus a theorem saying $n\leq N\implies |a_n|\leq X$?

[Kevin Buzzard]

I would like to avoid list.map list.range etc etc if possible.

[Mario Carneiro]

you could use the real supremum of the set, that's pretty direct although you have less library assistance

[Kevin Buzzard]

I now realise that I want to take the sup in the set of non-negative reals, which exists even for the empty set. Do we have this trick in Lean?

[Kevin Buzzard]

eew but then I'd have to redefine |x| to take values in nnreal

[Mario Carneiro]

just put 0 in the supremum

[Kevin Buzzard]

Can I even make the set in a way that looks close to $\{|a_n|\,|\,n\leq N\}$?

[Mario Carneiro]

not without using range

[Kevin Buzzard]

I feel like my choice of notation might be about to bite me as well :-)

[Kevin Buzzard]

Can I avoid using map?

[Kevin Buzzard]

In python I can do quite fancy set comprehensions

[Kevin Buzzard]

I've just realised that I don't even know if I can do them in Lean

[Mario Carneiro]

lol, Simon will show you how to do fancy set comprehensions using do notation

[Andrew Ashworth]

Are these lemmas actually trivial? Iirc, when I was following along these textbook proofs, each one required at least a paragraph of explanation

[Mario Carneiro]

I agree actually, I've never seen this be a 0 line proof

[Kevin Buzzard]

The fact that $|a_n|\leq B_1$ for $n\geq N$ implies that $a_n$ is bounded would be presented in a maths class like this: "let $B_2$ be the max of $|a_n|$ for $n<N$, then clearly $B=\max\{B_1,B_2\}$ works"

[Mario Carneiro]

I have written this exact proof in mathlib somewhere, maybe you can make something of it

[Kevin Buzzard]

Undergraduate mathematicians can fill in the proofs that there are only finitely many $n<N$, that the max exists, and that $|a_n|\leq B$ for all $n$, and they would be deemed sufficiently trivial as to be not worth mentioning.

[Mario Carneiro]

https://github.com/leanprover/mathlib/blob/master/src/topology/metric_space/basic.lean#L531-L545

[Kevin Buzzard]

One reason it's hard for all this Lean stuff to catch up with normal maths is that normal maths goes at what Lean people would think of as breakneck speed, with all sorts of side goals never dealt with. They're dealt with using the undergraduate tactic.

[Mario Carneiro]

It looks like I used finset.range and finset.sup, with nndist to stay in the nnreals

[Mario Carneiro]

I guess I would say that in lean we write things in a particular way to prove side goals by type correctness when possible

[Kevin Buzzard]

that's because you poor guys have to prove these goals :-) We just say they're obvious and hence not worth the time!

[Mario Carneiro]

when you say "the max of |a_n| for n<N" there is a proof obligation that the set is bounded above, and has a max. When it's a finset this is obvious

[Kevin Buzzard]

You guys would probably point out that you need to prove it by induction or something :-)

[Mario Carneiro]

because if I said "the max of |a_n| for n>N" it wouldn't be true

[Kevin Buzzard]

We don't even notice that we're using induction. We're even using recursion to define the max, I should think.

[Mario Carneiro]

that's one way to do it

[Kevin Buzzard]

There was a question on my M1F example sheet of the form "(i) Prove [blah] by induction (ii) now prove that I'm wasting your time and prove it directly without using induction"

[Kevin Buzzard]

and when I came to formalise it I realised that there was no way in hell that it was going to be proved without using induction :-)

[Andrew Ashworth]

Actually, I did have to prove that every finite sequence was bounded using induction, this was from Tao's UG analysis book "Analysis 1"...

[Mario Carneiro]

If you prove this theorem by induction you can avoid any contact with finite suprema

[Kevin Buzzard]

The question even had $3^n$ in

[Kevin Buzzard]

which you can't even really define without induction

[Mario Carneiro]

well, exp(n*log 3) is not inductive

[Kevin Buzzard]

heh, it's not nat-valued either :-)

[Mario Carneiro]

of course it is, when the input is a natural number so is the output

[Kevin Buzzard]

and I'd better check with Chris that he didn't use nat.rec anywhere in his definition of exp

[Kevin Buzzard]

of course it is, when the input is a natural number so is the output

No! The output is a real number in the image of some coercion map, right? That's what you guys think anyway!

[Mario Carneiro]

if you think it's not that's DTT lying to you

[Kevin Buzzard]

:-)

[Kevin Buzzard]

I'm going to have to spend some time thinking about this. I don't think these problems are unsolvable. Patrick proved that if f was surjective then it had a one-sided inverse using some simple choose tactic and it looked really good. Last year I proved this without that tactic to my UGs and it looked really horrible.

[Kevin Buzzard]

Sometimes it's just a case of hiding all the true horror behind some simple interface.

[Mario Carneiro]

like finset.sup?

[Mario Carneiro]

Maybe all you need are nice notations for it

[Kevin Buzzard]

finset.sup wants some semilattice_bot thing, and the reals aren't one of those

[Kevin Buzzard]

lattice.semilattice_sup_bot

[Johan Commelin]

Can't we have real.nnabs?

[Kevin Buzzard]

Yes. But of course that will cause problems somewhere else.

[Mario Carneiro]

finset.max I think doesn't care, but it returns an option

[Kevin Buzzard]

How come finset.max returns an option but 1 / 0 doesn't?

[Mario Carneiro]

because it's on a generic type, there is no zero element

[Kevin Buzzard]

Is there a variant which returns default alpha if there's no elements?

[Mario Carneiro]

but yes, you could do just that

[Mario Carneiro]

I think there was one written at some point, not sure where it's gone

[Kevin Buzzard]

Maybe I'll write a little library with variants of these things which work better for me.

[Kevin Buzzard]

This has been helpful, thanks.

[Mario Carneiro]

you can define it as (finset.max s).iget

[Kevin Buzzard]

It looks intimidating. I think that for my current purposes I just want to write some of my own functions which I'll hide in an import.

[Mario Carneiro]

that's what I mean you should do

[Kevin Buzzard]

Oh I see. Of course. I have the weekend to do it, hopefully I will have it right by Tuesday.

[Kevin Buzzard]

local notation `[0..` n `]` := finset.range n

#check [0..3] -- finset ℕ

I'm liking that.

[Johan Commelin]

You need more backticks :smiley:

[Patrick Massot]

I was just watching Patrick proving that all epis were split in the category of sets and I thought it was going to be horrible but he just used this "choose" tactic and it was wonderful. I'm now wondering whether I can pull off something equally slick looking with this.

This tactic was written specifically for this talk

[Kevin Buzzard]

I know Johan, but I was between tube stations when this became clear :-)

[Mario Carneiro]

except that set is {0,1,2}

[Kevin Buzzard]

Yes Patrick I remember you talking about it here. It seemed to work very well in practice.

[Kevin Buzzard]

except that set is {0,1,2}

doh

[Patrick Massot]

I mean I think it's useful to give talk and lectures where we want proofs to look nice. Because it pushes us to improve our tool

[Kevin Buzzard]

local notation `[0..` n `]` := finset.range (n + 1)

[Mario Carneiro]

yeah but now how are you going to denote {|a_n| : n < N}?

[Patrick Massot]

We need that new parser

[Mario Carneiro]

omg we could have something incredible