## Stream: maths

### Topic: convergent sequences are bounded

#### Kevin Buzzard (Jan 18 2019 at 18:23):

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 (Jan 18 2019 at 18:30):

[I'll just write the boilerplate now]

#### Kevin Buzzard (Jan 18 2019 at 18:37):

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 (Jan 18 2019 at 18:43):

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 (Jan 18 2019 at 18:43):

Just proving Cauchy sequences were bounded led me to:

#### Andrew Ashworth (Jan 18 2019 at 18:43):

-- 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 _ _)


#### Kevin Buzzard (Jan 18 2019 at 18:44):

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 (Jan 18 2019 at 18:45):

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 (Jan 18 2019 at 18:47):

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 (Jan 18 2019 at 18:48):

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

#### Mario Carneiro (Jan 18 2019 at 18:48):

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

#### Kevin Buzzard (Jan 18 2019 at 18:49):

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 (Jan 18 2019 at 18:49):

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

#### Mario Carneiro (Jan 18 2019 at 18:50):

just put 0 in the supremum

#### Kevin Buzzard (Jan 18 2019 at 18:50):

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

#### Mario Carneiro (Jan 18 2019 at 18:51):

not without using range

#### Kevin Buzzard (Jan 18 2019 at 18:51):

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

#### Kevin Buzzard (Jan 18 2019 at 18:51):

Can I avoid using map?

#### Kevin Buzzard (Jan 18 2019 at 18:51):

In python I can do quite fancy set comprehensions

#### Kevin Buzzard (Jan 18 2019 at 18:52):

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

#### Mario Carneiro (Jan 18 2019 at 18:52):

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

#### Andrew Ashworth (Jan 18 2019 at 18:52):

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 (Jan 18 2019 at 18:52):

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

#### Kevin Buzzard (Jan 18 2019 at 18:54):

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, then clearly $B=\max\{B_1,B_2\}$ works"

#### Mario Carneiro (Jan 18 2019 at 18:54):

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

#### Kevin Buzzard (Jan 18 2019 at 18:55):

Undergraduate mathematicians can fill in the proofs that there are only finitely many $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 (Jan 18 2019 at 18:55):

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

#### Kevin Buzzard (Jan 18 2019 at 18:56):

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 (Jan 18 2019 at 18:56):

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

#### Mario Carneiro (Jan 18 2019 at 18:59):

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 (Jan 18 2019 at 19:00):

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 (Jan 18 2019 at 19:00):

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 (Jan 18 2019 at 19:01):

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

#### Mario Carneiro (Jan 18 2019 at 19:01):

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

#### Kevin Buzzard (Jan 18 2019 at 19:01):

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

#### Mario Carneiro (Jan 18 2019 at 19:01):

that's one way to do it

#### Kevin Buzzard (Jan 18 2019 at 19:02):

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 (Jan 18 2019 at 19:02):

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 (Jan 18 2019 at 19:02):

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 (Jan 18 2019 at 19:02):

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

#### Kevin Buzzard (Jan 18 2019 at 19:02):

The question even had $3^n$ in

#### Kevin Buzzard (Jan 18 2019 at 19:02):

which you can't even really define without induction

#### Mario Carneiro (Jan 18 2019 at 19:03):

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

#### Kevin Buzzard (Jan 18 2019 at 19:03):

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

#### Mario Carneiro (Jan 18 2019 at 19:03):

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

#### Kevin Buzzard (Jan 18 2019 at 19:03):

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

#### Kevin Buzzard (Jan 18 2019 at 19:04):

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 (Jan 18 2019 at 19:04):

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

:-)

#### Kevin Buzzard (Jan 18 2019 at 19:05):

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 (Jan 18 2019 at 19:05):

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

#### Mario Carneiro (Jan 18 2019 at 19:06):

like finset.sup?

#### Mario Carneiro (Jan 18 2019 at 19:06):

Maybe all you need are nice notations for it

#### Kevin Buzzard (Jan 18 2019 at 19:06):

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

#### Kevin Buzzard (Jan 18 2019 at 19:07):

lattice.semilattice_sup_bot

#### Johan Commelin (Jan 18 2019 at 19:07):

Can't we have real.nnabs?

#### Kevin Buzzard (Jan 18 2019 at 19:07):

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

#### Mario Carneiro (Jan 18 2019 at 19:07):

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

#### Kevin Buzzard (Jan 18 2019 at 19:08):

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

#### Mario Carneiro (Jan 18 2019 at 19:08):

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

#### Kevin Buzzard (Jan 18 2019 at 19:08):

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

#### Mario Carneiro (Jan 18 2019 at 19:08):

but yes, you could do just that

#### Mario Carneiro (Jan 18 2019 at 19:08):

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

#### Kevin Buzzard (Jan 18 2019 at 19:09):

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

#### Mario Carneiro (Jan 18 2019 at 19:09):

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

#### Kevin Buzzard (Jan 18 2019 at 19:11):

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 (Jan 18 2019 at 19:14):

that's what I mean you should do

#### Kevin Buzzard (Jan 18 2019 at 19:15):

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

#### Kevin Buzzard (Jan 18 2019 at 19:50):

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

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


I'm liking that.

#### Johan Commelin (Jan 18 2019 at 19:51):

You need more backticks :smiley:

#### Patrick Massot (Jan 18 2019 at 20:00):

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 (Jan 18 2019 at 20:01):

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

#### Mario Carneiro (Jan 18 2019 at 20:02):

except that set is {0,1,2}

#### Kevin Buzzard (Jan 18 2019 at 20:02):

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

#### Kevin Buzzard (Jan 18 2019 at 20:03):

except that set is {0,1,2}

doh

#### Patrick Massot (Jan 18 2019 at 20:03):

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 (Jan 18 2019 at 20:03):

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


#### Mario Carneiro (Jan 18 2019 at 20:04):

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

#### Patrick Massot (Jan 18 2019 at 20:05):

We need that new parser

#### Mario Carneiro (Jan 18 2019 at 20:05):

omg we could have something incredible

Last updated: May 12 2021 at 07:17 UTC