## Stream: new members

### Topic: supremum

#### Keeley Hoek (Jun 12 2019 at 09:49):

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

#### Chris Hughes (Jun 12 2019 at 09:52):

No. Because nobody got round to writing one yet.

Thanks!

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

#### Chris Hughes (Jun 12 2019 at 09:56):

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

#### Chris Hughes (Jun 12 2019 at 09:59):

You could prove that nat is a conditionally_complete_linear_order_bot first

#### Kevin Buzzard (Jun 12 2019 at 10:12):

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

#### Chris Hughes (Jun 12 2019 at 10:12):

Is there a galois insertion thing you can do here?

#### 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)$ or $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.

#### 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

#### Kevin Buzzard (Sep 25 2020 at 12:01):

Maybe post more code?

#### 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


#### 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"

#### 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).

#### 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

#### 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.

#### 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.

#### Reid Barton (Sep 25 2020 at 12:14):

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

#### 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.

#### 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.

#### 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.

#### 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

#### 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).

#### 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.

#### 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.

#### 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.

#### 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?

#### Kevin Buzzard (Sep 25 2020 at 12:47):

Yeah exactly. Let's establish that first.

#### 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

#### 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.

#### 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

#### 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

#### Kevin Buzzard (Sep 25 2020 at 14:17):

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

#### James Arthur (Sep 25 2020 at 14:38):

I probably just need has_Sup and is_Sup.

#### 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.

#### James Arthur (Sep 25 2020 at 14:47):

Amazing. Thats useful.

Last updated: May 17 2021 at 22:15 UTC