Zulip Chat Archive

Stream: maths

Topic: minimum of finite set


view this post on Zulip Patrick Massot (May 23 2018 at 19:43):

with sup you don't need to use iget. max is the better name but I think sup has the better behaviour.

What is this sup you are talking about?

view this post on Zulip Chris Hughes (May 23 2018 at 19:45):

finset.sup defined, or at least used in multivariate_polynomial

view this post on Zulip Chris Hughes (May 23 2018 at 19:46):

Only defined for semilattice_sup_bot

view this post on Zulip Patrick Massot (May 23 2018 at 19:48):

That's unexpected

view this post on Zulip Patrick Massot (May 23 2018 at 19:48):

Thanks

view this post on Zulip Patrick Massot (May 23 2018 at 19:49):

I still can't use it though. I'll try harder

view this post on Zulip Chris Hughes (May 23 2018 at 19:49):

Why not?

view this post on Zulip Chris Hughes (May 23 2018 at 19:49):

It takes the sup of the image of a given function.

view this post on Zulip Patrick Massot (May 23 2018 at 19:50):

failed to synthesize type class instance for ⊢ semilattice_sup_bot ℝ

view this post on Zulip Patrick Massot (May 23 2018 at 19:50):

It means I need to learn

view this post on Zulip Patrick Massot (May 23 2018 at 19:50):

what is a semilattice_sup_bot

view this post on Zulip Chris Hughes (May 23 2018 at 19:50):

reals aren't a semilattice sup bot

view this post on Zulip Chris Hughes (May 23 2018 at 19:50):

It needs a least element of the type.

view this post on Zulip Kenny Lau (May 23 2018 at 19:50):

ennreal is

view this post on Zulip Kenny Lau (May 23 2018 at 19:50):

the nonnegative (in your case, positif) reals also is

view this post on Zulip Patrick Massot (May 23 2018 at 19:54):

Using the type of nonnegative real would probably mess up lots of things

view this post on Zulip Patrick Massot (May 23 2018 at 19:54):

in my norms.lean

view this post on Zulip Johan Commelin (May 23 2018 at 19:55):

Incidentally, I just defined some stuff on nonnegative reals this week...

view this post on Zulip Johan Commelin (May 23 2018 at 19:55):

Like that it is a comm_semiring, and its topology

view this post on Zulip Patrick Massot (May 23 2018 at 19:56):

Nooo! I don't want to do topological commutative semi-ring theory!

view this post on Zulip Johan Commelin (May 23 2018 at 19:58):

Well, it is very useful for defining the standard simplices. Because it takes care of the condition that all the coordinates are positive

view this post on Zulip Andrew Ashworth (May 23 2018 at 19:59):

is this part of your bigop project? I am dying to have useable matrices and summations in Lean, maybe I will take a look

view this post on Zulip Patrick Massot (May 23 2018 at 20:01):

No, I'm back to calculus while I wait for omega/cooper to be usable, just in case it makes using nat possible

view this post on Zulip Andrew Ashworth (May 23 2018 at 20:02):

well, studying cooper was also on my recreational to-do list, so i'll have to get on it

view this post on Zulip Patrick Massot (May 23 2018 at 20:02):

I was not able to import it in any way

view this post on Zulip Patrick Massot (May 23 2018 at 20:21):

@Johannes Hölzl The point of my questions about max is to try to get a norm on ℝ^n. But this goes through the dreaded definition of Lean metric spaces. Could you get me started by doing

instance metric_space.fintype_function {α : Type*} [metric_space α] {β : Type*} [fintype β]
: metric_space (β  α)

(using the max distance between images) I think I could manage from there.

view this post on Zulip Johannes Hölzl (May 23 2018 at 20:22):

Do you want to use the max distance in general, or just because we don't have sqrt yet?

view this post on Zulip Patrick Massot (May 23 2018 at 20:23):

We started using max on products a long time ago. It's partly for lack of square root tooling, but I also don't see why square root would be better

view this post on Zulip Patrick Massot (May 23 2018 at 20:23):

The current state of this story is https://github.com/PatrickMassot/lean-differential-topology/blob/master/src/norms.lean

view this post on Zulip Patrick Massot (May 23 2018 at 20:24):

(with products of two types only)

view this post on Zulip Kevin Buzzard (May 23 2018 at 20:26):

(and added segfault)

view this post on Zulip Kevin Buzzard (May 23 2018 at 20:26):

(no)

view this post on Zulip Kevin Buzzard (May 23 2018 at 20:26):

(assertion violation)

view this post on Zulip Patrick Massot (May 23 2018 at 20:27):

The version up at github has no assertion violation

view this post on Zulip Patrick Massot (May 23 2018 at 20:28):

And I was linking to this only so that Johannes could see my definition of normed group

view this post on Zulip Johannes Hölzl (May 23 2018 at 20:42):

For me somehow the Euclidean distance (l_2-norm) as the canonical distance. But yeah, we can first start with the max-distance. That's one advantage of uniform spaces: the produce construction is more canonical :-)

view this post on Zulip Kevin Buzzard (May 23 2018 at 21:01):

"more canonical" :-)

view this post on Zulip Kevin Buzzard (May 23 2018 at 21:01):

We didn't formalise canonical yet

view this post on Zulip Kevin Buzzard (May 23 2018 at 21:01):

let alone make it a partial order

view this post on Zulip Johannes Hölzl (May 23 2018 at 22:04):

@Patrick Massot https://gist.github.com/johoelzl/2ea9c95fb3a4773c8da5f63384906105 here is the metric space for finite function.
@Simon Hudon I think I will change max to my version of maxi. How would you do these kind of proofs?

view this post on Zulip Mario Carneiro (May 23 2018 at 22:09):

We can make imax (I usually use the i as a prefix) as an alternative to max defined for inhabited sets if you like. If it is defined as max.iget then we get all the theorems for free

view this post on Zulip Mario Carneiro (May 23 2018 at 22:10):

I want to make finset.max a special case of finset.sup by defining a with_bot A := option A type which extends the order with none <= some a

view this post on Zulip Johannes Hölzl (May 23 2018 at 22:58):

I still don't see cases where the current max has advantages, or how to do proofs properly. Using with_bot, could we just use sup instead of the current max, and use sup + iget as max?

view this post on Zulip Simon Hudon (May 23 2018 at 23:34):

@Johannes Hölzl Sorry, I haven't been following. Which proofs do you mean?

view this post on Zulip Mario Carneiro (May 24 2018 at 04:27):

Using with_bot, sup over with_bot would be the same as max is currently (in particular, it would return an option), and then you could postprocess the result with iget if that makes sense in your application. I like the way max works at the moment because it lets you work relationally with max, i.e. "x is the max of s" rather than a term "max of s" which may or may not actually be a max of s

view this post on Zulip Sean Leather (May 24 2018 at 05:55):

def maxi [decidable_linear_order β] [inhabited β] (s : finset α) (f : α  β) : β := (s.image f).max.iget

lemma maxi_empty : ( : finset α).maxi f = default β

I don't understand how maxi_empty is useful.

view this post on Zulip Johannes Hölzl (May 24 2018 at 05:55):

@Simon Hudon the proofs in https://gist.github.com/johoelzl/2ea9c95fb3a4773c8da5f63384906105 Its a little bit of a special case (we are working essentially in R >= 0) and we explicitly want s = empty -> max s = 0. Without adding my own rules for maxi (a.k.a. imax) I would need a lot of annoying case distinctions (ala finset.univ = empty)

view this post on Zulip Johannes Hölzl (May 24 2018 at 05:59):

At least at the beginning maxi_empty is helpful: the following rules have a special condition to compare to the default when s = empty, which can be resolved using by simp * at *.

view this post on Zulip Sean Leather (May 24 2018 at 06:03):

I see: (hd : s = ∅ → b ≤ default β) is what you mean. So with an option result, you don't need that? But you still think using inhabited is better?

view this post on Zulip Sean Leather (May 24 2018 at 06:06):

lemma le_maxi_of_forall {b : β} (hb : as, b  f a) (hd : s =   b  default β) : b  s.maxi f

looks a lot like

theorem le_max_of_mem {a b : α} {s : finset α} (h : a  b) : a  s  a  max b s

view this post on Zulip Sean Leather (May 24 2018 at 06:08):

BTW, I'm really just trying to wrap my head around the use of inhabited and why it's better. I'm not trying to claim mine is universally better or anything. Since I haven't tried to implement it or use it myself, I don't have an intuition for it.

view this post on Zulip Johannes Hölzl (May 24 2018 at 06:15):

le_maxi_of_forall is slightly different, as it is about a lower bound. Either s is empty, than you compare it to the default: handling the case where s is empty, or where the default value is well defined. In your le_max_of_mem case you show that an element is a lower bound, also there is no difference between non-empty s and b being well defined.

view this post on Zulip Sean Leather (May 24 2018 at 06:21):

Right. But they both deal with a “default,” whether that be b in le_max_of_mem or default β in le_maxi_of_forall. That's the similarity I see.

view this post on Zulip Mario Carneiro (May 24 2018 at 06:26):

I'm not a fan of these inhabited solutions because default is (supposed to be) a completely arbitrary element with no semantic value. It's not supposed to be compared to stuff because in a given structure you have no idea what it could be. If it happens to work out in some type, that should be treated as coincidence and should not be relied on.

view this post on Zulip Mario Carneiro (May 24 2018 at 06:26):

which is why I find the hypothesis s = ∅ → b ≤ default β very strange

view this post on Zulip Mario Carneiro (May 24 2018 at 06:27):

if you care about having a particular fallback value, there is get_or_else for that

view this post on Zulip Patrick Massot (May 28 2018 at 09:37):

@Mario Carneiro and @Johannes Hölzl did you decide something about this max debate? Can I use https://gist.github.com/johoelzl/2ea9c95fb3a4773c8da5f63384906105 or is it already outdated with respect to current mathlib?

view this post on Zulip Johannes Hölzl (May 28 2018 at 09:46):

I'm not sure yet. I didn't try to write the proof only using the option variant of max. @Sean Leather did you use max already?
But we have a new possibility now: use nnreal to define dist and norm (or maybe nndist). Then we can use sup and don't need to worry about the empty case. It should still easily embed into real.

view this post on Zulip Patrick Massot (May 28 2018 at 09:48):

I don't understand how nnreal could help here

view this post on Zulip Sebastien Gouezel (May 28 2018 at 09:51):

Please, please, please don't use nnreals for dist and norm! I tried to do something like that for Gromov hyperbolic space (except that I needed distances taking the value infinity, so I used ennreal). And then I had to start everything over again using ereal once I was deep enough in the theory, when I had to do serious computations and inequalities, as the fact that subtraction on ennreal (or nnreal, or nat) is truncating things makes everything a total mess -- I think Patrick has been bitten by this quite a few times, right?

view this post on Zulip Patrick Massot (May 28 2018 at 09:52):

Oh yes, I don't want more crazy substraction

view this post on Zulip Sean Leather (May 28 2018 at 10:54):

I'm not sure yet. I didn't try to write the proof only using the option variant of max. @Sean Leather did you use max already?

@Johannes Hölzl No, I haven't started using the max in mathlib.


Last updated: May 18 2021 at 06:15 UTC