Zulip Chat Archive

Stream: maths

Topic: convergent sequences are bounded


view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jan 18 2019 at 18:30):

[I'll just write the boilerplate now]

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Andrew Ashworth (Jan 18 2019 at 18:43):

Just proving Cauchy sequences were bounded led me to:

view this post on Zulip 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 _ _)
      (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₃))

view this post on Zulip 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? :-/

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jan 18 2019 at 18:47):

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

view this post on Zulip Kevin Buzzard (Jan 18 2019 at 18:48):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Jan 18 2019 at 18:49):

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

view this post on Zulip Mario Carneiro (Jan 18 2019 at 18:50):

just put 0 in the supremum

view this post on Zulip Kevin Buzzard (Jan 18 2019 at 18:50):

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

view this post on Zulip Mario Carneiro (Jan 18 2019 at 18:51):

not without using range

view this post on Zulip Kevin Buzzard (Jan 18 2019 at 18:51):

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

view this post on Zulip Kevin Buzzard (Jan 18 2019 at 18:51):

Can I avoid using map?

view this post on Zulip Kevin Buzzard (Jan 18 2019 at 18:51):

In python I can do quite fancy set comprehensions

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jan 18 2019 at 18:52):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jan 18 2019 at 18:52):

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

view this post on Zulip Kevin Buzzard (Jan 18 2019 at 18:54):

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

view this post on Zulip Mario Carneiro (Jan 18 2019 at 18:54):

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

view this post on Zulip Kevin Buzzard (Jan 18 2019 at 18:55):

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

view this post on Zulip Mario Carneiro (Jan 18 2019 at 18:55):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jan 18 2019 at 19:01):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jan 18 2019 at 19:01):

that's one way to do it

view this post on Zulip 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"

view this post on Zulip 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 :-)

view this post on Zulip 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"...

view this post on Zulip Mario Carneiro (Jan 18 2019 at 19:02):

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

view this post on Zulip Kevin Buzzard (Jan 18 2019 at 19:02):

The question even had 3n3^n in

view this post on Zulip Kevin Buzzard (Jan 18 2019 at 19:02):

which you can't even really define without induction

view this post on Zulip Mario Carneiro (Jan 18 2019 at 19:03):

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

view this post on Zulip Kevin Buzzard (Jan 18 2019 at 19:03):

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

view this post on Zulip Mario Carneiro (Jan 18 2019 at 19:03):

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

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip Mario Carneiro (Jan 18 2019 at 19:04):

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

view this post on Zulip Kevin Buzzard (Jan 18 2019 at 19:04):

:-)

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jan 18 2019 at 19:05):

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

view this post on Zulip Mario Carneiro (Jan 18 2019 at 19:06):

like finset.sup?

view this post on Zulip Mario Carneiro (Jan 18 2019 at 19:06):

Maybe all you need are nice notations for it

view this post on Zulip Kevin Buzzard (Jan 18 2019 at 19:06):

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

view this post on Zulip Kevin Buzzard (Jan 18 2019 at 19:07):

lattice.semilattice_sup_bot

view this post on Zulip Johan Commelin (Jan 18 2019 at 19:07):

Can't we have real.nnabs?

view this post on Zulip Kevin Buzzard (Jan 18 2019 at 19:07):

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

view this post on Zulip Mario Carneiro (Jan 18 2019 at 19:07):

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

view this post on Zulip Kevin Buzzard (Jan 18 2019 at 19:08):

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

view this post on Zulip Mario Carneiro (Jan 18 2019 at 19:08):

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

view this post on Zulip Kevin Buzzard (Jan 18 2019 at 19:08):

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

view this post on Zulip Mario Carneiro (Jan 18 2019 at 19:08):

but yes, you could do just that

view this post on Zulip Mario Carneiro (Jan 18 2019 at 19:08):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jan 18 2019 at 19:09):

This has been helpful, thanks.

view this post on Zulip Mario Carneiro (Jan 18 2019 at 19:09):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jan 18 2019 at 19:14):

that's what I mean you should do

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jan 18 2019 at 19:50):

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

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

I'm liking that.

view this post on Zulip Johan Commelin (Jan 18 2019 at 19:51):

You need more backticks :smiley:

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jan 18 2019 at 20:01):

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

view this post on Zulip Mario Carneiro (Jan 18 2019 at 20:02):

except that set is {0,1,2}

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jan 18 2019 at 20:03):

except that set is {0,1,2}

doh

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jan 18 2019 at 20:03):

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

view this post on Zulip Mario Carneiro (Jan 18 2019 at 20:04):

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

view this post on Zulip Patrick Massot (Jan 18 2019 at 20:05):

We need that new parser

view this post on Zulip Mario Carneiro (Jan 18 2019 at 20:05):

omg we could have something incredible


Last updated: May 12 2021 at 07:17 UTC