Zulip Chat Archive

Stream: new members

Topic: supremum


view this post on Zulip Keeley Hoek (Jun 12 2019 at 09:49):

Is there a has_Sup instance for enat? If not, why not?

view this post on Zulip Chris Hughes (Jun 12 2019 at 09:52):

No. Because nobody got round to writing one yet.

view this post on Zulip Keeley Hoek (Jun 12 2019 at 09:53):

Thanks!

view this post on Zulip Keeley Hoek (Jun 12 2019 at 09:55):

Is there any machinery which already handles given some finite upper bound of nats finding a minimal witness? (something to do with lattices? Sorry, I don't know anything about them)

view this post on Zulip Chris Hughes (Jun 12 2019 at 09:56):

nat.find and nat.find_greatest will help. You should write a complete_linear_order instance.

view this post on Zulip Chris Hughes (Jun 12 2019 at 09:59):

You could prove that nat is a conditionally_complete_linear_order_bot first

view this post on Zulip Kevin Buzzard (Jun 12 2019 at 10:12):

You should write a transfer tactic which just transports everything on nat to enat ;-)

view this post on Zulip Chris Hughes (Jun 12 2019 at 10:12):

Is there a galois insertion thing you can do here?

view this post on Zulip James Arthur (Sep 25 2020 at 11:57):

Why is supremum defined as such in mathlib?

( x, x  S)  ( x  S,  y  S, y  x)

is there a quirk with lean that means that this would still work for a set S=(0,1)S = (0, 1) or S={x:x<2} S = \{ x : x < 2 \} ? I'm a tad confused why this works.

Probably I should explain I'm trying to define supremum and infimum standalone as part of a project to formalise the Exeter Analysis course.

view this post on Zulip Kevin Buzzard (Sep 25 2020 at 12:00):

That is just the true-false statement that S has a top element. I don't really understand what the question is but suspect it might be a misunderstanding on your part rather than a quirk in Lean

view this post on Zulip Kevin Buzzard (Sep 25 2020 at 12:01):

Maybe post more code?

view this post on Zulip James Arthur (Sep 25 2020 at 12:01):

I stole that bit of code from this, which is part of data.real.basic

lemma Sup_def (S : set ) :
  Sup S = if h : ( x, x  S)  ( x,  y  S, y  x)
    then classical.some (exists_sup S h.1 h.2) else 0 := rfl

view this post on Zulip James Arthur (Sep 25 2020 at 12:11):

What I can't get my head around is that I'd define supremum as this:

def anal.sup (T : set ) := ( x  T,  y  T, y  x)  ( t  ,  y  T, y  t, x  t)

Although, it's a bit of a mess and doesn't compile, it feels closer to what we are given in our notes.

"Similarly, if there exists an a ∈ R such that a ≤ x x ∈ S, then S is bounded below and a is a lower bound of S. If α is a lower bound of S, but no number is greater than α is, then α is called the infimum of S"

view this post on Zulip Reid Barton (Sep 25 2020 at 12:12):

James Arthur said:

( x, x  S)  ( x  S,  y  S, y  x)

This is not the definition of the sup. It's the condition under which a subset of the reals has a sup (nonempty and bounded above).

view this post on Zulip Kevin Buzzard (Sep 25 2020 at 12:13):

Aah, you didn't even quote it correctly! x doesn't have to be in S in the second clause

view this post on Zulip Kevin Buzzard (Sep 25 2020 at 12:14):

James I still don't understand the question. The lemma says that if S is any set at all, then if S is non-empty and bounded then the Lean function Sup will indeed return the supremum of S, and if it isn't then it will return a junk value.

view this post on Zulip James Arthur (Sep 25 2020 at 12:14):

Reid Barton said:

James Arthur said:

( x, x  S)  ( x  S,  y  S, y  x)

This is not the definition of the sup. It's the condition under which a subset of the reals has a sup (nonempty and bounded above).

Ah, that makes a lot more sense.

view this post on Zulip Reid Barton (Sep 25 2020 at 12:14):

There is a more general notion is_lub defined in order.bounds.

view this post on Zulip Kevin Buzzard (Sep 25 2020 at 12:15):

Note also that Sup is a total function, like division, so 1/0 = junk value (=0) and Sup(all the reals) = junk value too.

view this post on Zulip Kevin Buzzard (Sep 25 2020 at 12:16):

def anal.sup (T : set ) := ( x  T,  y  T, y  x)  ( t  ,  y  T, y  t, x  t)

Does this compile? The second clause looks wrong.

view this post on Zulip James Arthur (Sep 25 2020 at 12:17):

I want to define the supremum of a set of real numbers. There's problems with junk values, but I should be able to deal with them if I define the extended reals. My question was basically how do I define supremum because my version doesn't compile. I thought if I could work out how mathlib did it, I could rejig it into my code.

view this post on Zulip James Arthur (Sep 25 2020 at 12:17):

Kevin Buzzard said:

def anal.sup (T : set ) := ( x  T,  y  T, y  x)  ( t  ,  y  T, y  t, x  t)

Does this compile? The second clause looks wrong.

It is wrong and doesn't compile

view this post on Zulip Kevin Buzzard (Sep 25 2020 at 12:18):

James Arthur said:

I want to define the supremum of a set of real numbers. There's problems with junk values, but I should be able to deal with them if I define the extended reals. My question was basically how do I define supremum because my version doesn't compile. I thought if I could work out how mathlib did it, I could rejig it into my code.

You need to think hard about exactly the type of the term you want to define. Currently Lean has Sup which returns the sup of a set of reals if this sup exists, and returns 0 otherwise. You don't necessarily need to look at mathlib to see its internal design decisions, if you can write the maths then you can write it in Lean (perhaps after asking for hints first).

view this post on Zulip Kevin Buzzard (Sep 25 2020 at 12:19):

But things like "I should be able to deal with them if I use extended reals" indicate to me that you still haven't actually decided what the source and target of the function you want to define is. So you should decide that first -- by which I mean make a precise decision which you understand can't be changed later -- this is a design decision which you will have to make as the designer.

view this post on Zulip James Arthur (Sep 25 2020 at 12:31):

I know I want the code to be easy to read, preferably by my coursemates with help from lots of comments. I don't quite know how to define sup and inf, but I wanted it to be one definition for each, just with the two conditions that are given in the notes, while importing the reals from mathlib. We proved that the rationals aren't complete using it, which would be nice to prove using my sup and inf.

view this post on Zulip Kevin Buzzard (Sep 25 2020 at 12:43):

I'm sure that we'll be able to get you some easy-to-read code, you don't need to use the inbuilt Sup, you will be able to use the inbuilt theorem that if you have a non-empty bounded set of reals then it has a real Sup and if I'd had more time to work on the real number game over the summer then perhaps I would have been able to show you how we did it there. But right now you are going to have to define what the source and target of your Sup function are going to be, and this is your own decision. One you've decided, I'm sure we can help you make it.

I once made a square root function (before mathlib had square roots) and I decided that I wanted the input to be a non-negative real, so I asked for two inputs -- a real, and a proof that it was non-negative. This worked fine, however it was sometimes a pain to use because I got sick of supplying proofs that e.g. 37 was non-negative. This is why mathlib has this Sup function, which does not always return the sup (in fact it fails to return the sup precisely when the sup doesn't exist) but it is easier to use.

view this post on Zulip James Arthur (Sep 25 2020 at 12:46):

So I need to decide what goes into my sup and what comes out? Is that what you mean by source and target?

view this post on Zulip Kevin Buzzard (Sep 25 2020 at 12:47):

Yeah exactly. Let's establish that first.

view this post on Zulip Kevin Buzzard (Sep 25 2020 at 12:47):

Here are some half-baked thoughts about formalising Imperial's analysis course by the way: https://github.com/ImperialCollegeLondon/M1P1-lean/tree/master/src . You might find them useful

view this post on Zulip James Arthur (Sep 25 2020 at 12:55):

Thankyou.

I'd be happy if it had an input of a set of reals and outputted the supremum, if it exists, or zero.

view this post on Zulip Kevin Buzzard (Sep 25 2020 at 14:14):

So this is exactly what Sup does. Why don't you write the predicate first? That's a good way to start I guess. Write a function which takes a set S of reals and a real number x, and outputs the statement that x is a sup of S. That could be called is_Sup or something. Note that it will almost certainly be in lean already but you might want to write your own anyway, especially if this is for teaching purposes

view this post on Zulip Kevin Buzzard (Sep 25 2020 at 14:17):

In fact it seems to me that you could probably go a long way with just has_Sup and is_Sup

view this post on Zulip Kevin Buzzard (Sep 25 2020 at 14:17):

Isn't this all you need in a basic analysis course?

view this post on Zulip James Arthur (Sep 25 2020 at 14:38):

I probably just need has_Sup and is_Sup.

view this post on Zulip Kevin Buzzard (Sep 25 2020 at 14:43):

So then you don't need to get involved in weird functions which return 0 if a set doesn't have a sup.

view this post on Zulip James Arthur (Sep 25 2020 at 14:47):

Amazing. Thats useful.


Last updated: May 17 2021 at 22:15 UTC