supremum

Stream: new members

[Keeley Hoek]

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

[Chris Hughes]

No. Because nobody got round to writing one yet.

[Keeley Hoek]

Thanks!

[Keeley Hoek]

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]

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

[Chris Hughes]

You could prove that nat is a conditionally_complete_linear_order_bot first

[Kevin Buzzard]

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

[Chris Hughes]

Is there a galois insertion thing you can do here?

[James Arthur]

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]

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]

Maybe post more code?

[James Arthur]

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]

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]

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]

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

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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]

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]

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]

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]

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]

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]

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]

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]

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]

Yeah exactly. Let's establish that first.

[Kevin Buzzard]

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]

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]

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]

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

[Kevin Buzzard]

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

[James Arthur]

I probably just need has_Sup and is_Sup.

[Kevin Buzzard]

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]

Amazing. Thats useful.