Zulip Chat Archive

Stream: maths

Topic: bounds


Kevin Buzzard (Nov 17 2018 at 11:23):

This is more of a funny story than anything else.

This week just gone at Imperial, we were looking at the real numbers and the completeness axiom in my class. Some of the students were involved in a (maths not Lean) project of constructing the real numbers as Dedekind cuts. The sheet started by defining totally ordered sets (the linear_order class in Lean) and the "least upper bound property" -- any non-empty bounded-above subset has a least upper bound. The sheet then remarked something I'd never realised -- there is no point defining also the "greatest lower bound property", because this follows from the least upper bound property. For the reals I had always imagined that this was proved by just considering {xxS}\{-x\,\mid\,x\in S\} but actually there is a direct proof which only uses total orders.

-- from order/bounds.lean

variables {α : Type*} [preorder α]
def upper_bounds (s : set α) : set α := { x | a  s, a  x }
def lower_bounds (s : set α) : set α := { x | a  s, x  a }
def is_least (s : set α) (a : α) : Prop := a  s  a  lower_bounds s
def is_greatest (s : set α) (a : α) : Prop := a  s  a  upper_bounds s
def is_lub (s : set α) : α  Prop := is_least (upper_bounds s)
def is_glb (s : set α) : α  Prop := is_greatest (lower_bounds s)

theorem warm_up (S : Type) [linear_order S] :
( E : set S, ( a, a  E)  ( b, b  upper_bounds E)   s : S, is_lub E s) 
( E : set S, ( a, a  E)  ( b, b  lower_bounds E)   s : S, is_glb E s) := sorry

Of course the proof requires a mathematical idea -- knowing any non-empty bounded-above set has a sup, and given a non-empty bounded-below set, we need to produce an inf without this involution which we have on the reals.

Kevin Buzzard (Nov 17 2018 at 11:26):

So I could see what the idea must be, and knocked up a tactic proof without too much trouble.

And then because the bounds definitions applied not just to linear_order but to preorder, Chris asked whether my proof also worked for partial orders or preorders. So the question became -- what do you actually need to assume about your order to prove this warm-up question? I'll post our conclusions later on today if nobody else fancies trying to figure this out :-)

Kevin Buzzard (Nov 17 2018 at 11:26):

No spoilers Kenny/Chris, if you're reading :-)

Johannes Hölzl (Nov 17 2018 at 11:58):

This is a standard construction at least for complete lattices, there often one defines the supremum or infimum and derives the other exterma. And these structures where the extrema only exists for non-empty bounded sets are called "conditionally complete lattices"

Kevin Buzzard (Nov 17 2018 at 13:54):

Right. So the question is: you might well know already that if, in a lattice, all non-empty bounded-above sets have a sup, then all non-empty bounded-below sets have an inf. This is a pleasant exercise. The question is whether you can get away with less than a lattice.

Mario Carneiro (Nov 17 2018 at 13:59):

if every set has a least upper bound, then it's already a lattice

Kevin Buzzard (Nov 17 2018 at 13:59):

I am only demanding on my order that every non-empty bounded above set has a least upper bound.

Mario Carneiro (Nov 17 2018 at 14:00):

then you get a conditionally complete lattice

Kevin Buzzard (Nov 17 2018 at 14:00):

but I need enough from my order to be able to deduce from this that every non-empty bounded-below set has a greatest lower bound.

Mario Carneiro (Nov 17 2018 at 14:01):

You might have to be careful about how you say bounded below, but the usual proof should go through

Kevin Buzzard (Nov 17 2018 at 14:01):

I explain exactly what I mean by all of these terms in the original post

Kevin Buzzard (Nov 17 2018 at 14:01):

The question is how much you can relax the typeclasses and still be able to fill in the sorry

Kevin Buzzard (Nov 17 2018 at 14:02):

e.g. can you prove

variables {α : Type*} [preorder α]
def upper_bounds (s : set α) : set α := { x | a  s, a  x }
def lower_bounds (s : set α) : set α := { x | a  s, x  a }
def is_least (s : set α) (a : α) : Prop := a  s  a  lower_bounds s
def is_greatest (s : set α) (a : α) : Prop := a  s  a  upper_bounds s
def is_lub (s : set α) : α  Prop := is_least (upper_bounds s)
def is_glb (s : set α) : α  Prop := is_greatest (lower_bounds s)

theorem warm_up (S : Type) [preorder S] :
( E : set S, ( a, a  E)  ( b, b  upper_bounds E)   s : S, is_lub E s) 
( E : set S, ( a, a  E)  ( b, b  lower_bounds E)   s : S, is_glb E s) := sorry

Mario Carneiro (Nov 17 2018 at 14:04):

I think so

Kevin Buzzard (Nov 17 2018 at 14:04):

so now begin dropping the axioms of a preorder

Kevin Buzzard (Nov 17 2018 at 14:05):

and how far can you get?

Mario Carneiro (Nov 17 2018 at 14:05):

if you take E := lower_bounds E then it's nonempty, and an element of E is an upper bound for lower_bounds E

Kevin Buzzard (Nov 17 2018 at 14:05):

right. And which axioms for a preorder do you use in this proof?

Mario Carneiro (Nov 17 2018 at 14:06):

if a in E and b in lower_bounds E then b <= a so a is an upper bound of lower_bounds E

Mario Carneiro (Nov 17 2018 at 14:06):

it uses nothing

Kevin Buzzard (Nov 17 2018 at 14:07):

variables {α : Type*} [has_le α]
def upper_bounds (s : set α) : set α := { x | a  s, a  x }
def lower_bounds (s : set α) : set α := { x | a  s, x  a }
def is_least (s : set α) (a : α) : Prop := a  s  a  lower_bounds s
def is_greatest (s : set α) (a : α) : Prop := a  s  a  upper_bounds s
def is_lub (s : set α) : α  Prop := is_least (upper_bounds s)
def is_glb (s : set α) : α  Prop := is_greatest (lower_bounds s)

theorem warm_up (S : Type) [has_le S] :
( E : set S, ( a, a  E)  ( b, b  upper_bounds E)   s : S, is_lub E s) 
( E : set S, ( a, a  E)  ( b, b  lower_bounds E)   s : S, is_glb E s) :=
λ H E ⟨⟨a, haE, b, hbuE⟩⟩,
let s, hs1, hs2 := H (lower_bounds E) ⟨⟨b, hbuE, a, λ s hs, hs a haE⟩⟩ in
s, λ t htE, hs2 t (λ z hzLE, hzLE t htE), hs1

Kevin Buzzard (Nov 17 2018 at 14:07):

punchline achieved

Mario Carneiro (Nov 17 2018 at 14:07):

it could be any relation

Kevin Buzzard (Nov 17 2018 at 14:07):

This made me wonder why preorder was assumed in bounds.lean

Mario Carneiro (Nov 17 2018 at 14:08):

because preorder is our weakest "lawful" order class

Kevin Buzzard (Nov 17 2018 at 14:08):

surely has_le is weaker?

Kevin Buzzard (Nov 17 2018 at 14:08):

It's surely an order class

Kevin Buzzard (Nov 17 2018 at 14:08):

because of the notation

Kevin Buzzard (Nov 17 2018 at 14:09):

you yourself know that has_add and has_mul are two completely different classes

Kevin Buzzard (Nov 17 2018 at 14:09):

that's why you had to define groups twice

Mario Carneiro (Nov 17 2018 at 14:10):

if it's not a preorder, you probably shouldn't be using <=

Mario Carneiro (Nov 17 2018 at 14:11):

plus all the terminology there doesn't really make sense without some transitivity

Kevin Buzzard (Nov 17 2018 at 14:29):

I am surprised that this is your attitude. I think the notation implies a "way of thinking" about the structure, but why can't I define the "upper bounds" of a set with has_le to be the obvious things? I thought that this was the mathlib philosophy -- you define things in the max generality that they parse, and for these definitions like upper_bounds we need nothing more than the predicate.

Kevin Buzzard (Nov 17 2018 at 14:29):

Octonians aren't associative, and yet people still use * to multiply them

Mario Carneiro (Nov 17 2018 at 14:32):

octonions aren't completely lawless though

Mario Carneiro (Nov 17 2018 at 14:33):

If we cared about them we would define loops or power-associative monoids or whatever

Mario Carneiro (Nov 17 2018 at 14:35):

I think it helps to be at least a little application-driven here. If it's only ever used on preorders then why the suprious generalization?

Mario Carneiro (Nov 17 2018 at 14:35):

note also that typeclass inference is a bit longer for lower classes, although this is probably a small effect

Mario Carneiro (Nov 17 2018 at 14:36):

I would recommend using pure notation classes only in lawless situations like meta programming

Kevin Buzzard (Nov 17 2018 at 14:49):

Oh that's an interesting comment. So there is a place for the has_lt typeclass beyond just a notational trick?

Kevin Buzzard (Nov 17 2018 at 14:49):

It's just in lawless metaland :-)

Kevin Buzzard (Mar 17 2019 at 17:10):

I think it helps to be at least a little application-driven here. If it's only ever used on preorders then why the suprious generalization?

In #789 I PR'ed monoid_equiv and Chris suggested I change it to mul_equiv. I want linear_ordered_comm_group_equiv but should this be extending le_equiv or preorder_equiv? Note the conversation above.

Kevin Buzzard (Mar 17 2019 at 17:11):

@Mario Carneiro . I just seem to be getting conflicting ideas about this one.


Last updated: Dec 20 2023 at 11:08 UTC