## Stream: maths

### Topic: minimum of finite set

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

#### Chris Hughes (May 23 2018 at 19:45):

finset.sup defined, or at least used in multivariate_polynomial

#### Chris Hughes (May 23 2018 at 19:46):

Only defined for semilattice_sup_bot

#### Patrick Massot (May 23 2018 at 19:48):

That's unexpected

Thanks

#### Patrick Massot (May 23 2018 at 19:49):

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

Why not?

#### Chris Hughes (May 23 2018 at 19:49):

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

#### Patrick Massot (May 23 2018 at 19:50):

failed to synthesize type class instance for ⊢ semilattice_sup_bot ℝ

#### Patrick Massot (May 23 2018 at 19:50):

It means I need to learn

#### Patrick Massot (May 23 2018 at 19:50):

what is a semilattice_sup_bot

#### Chris Hughes (May 23 2018 at 19:50):

reals aren't a semilattice sup bot

#### Chris Hughes (May 23 2018 at 19:50):

It needs a least element of the type.

#### Kenny Lau (May 23 2018 at 19:50):

ennreal is

#### Kenny Lau (May 23 2018 at 19:50):

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

#### Patrick Massot (May 23 2018 at 19:54):

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

in my norms.lean

#### Johan Commelin (May 23 2018 at 19:55):

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

#### Johan Commelin (May 23 2018 at 19:55):

Like that it is a comm_semiring, and its topology

#### Patrick Massot (May 23 2018 at 19:56):

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

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

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

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

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

#### Patrick Massot (May 23 2018 at 20:02):

I was not able to import it in any way

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

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

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

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

#### Patrick Massot (May 23 2018 at 20:24):

(with products of two types only)

(no)

#### Kevin Buzzard (May 23 2018 at 20:26):

(assertion violation)

#### Patrick Massot (May 23 2018 at 20:27):

The version up at github has no assertion violation

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

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

#### Kevin Buzzard (May 23 2018 at 21:01):

"more canonical" :-)

#### Kevin Buzzard (May 23 2018 at 21:01):

We didn't formalise canonical yet

#### Kevin Buzzard (May 23 2018 at 21:01):

let alone make it a partial order

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

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

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

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

#### Simon Hudon (May 23 2018 at 23:34):

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

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

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

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

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

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

#### Sean Leather (May 24 2018 at 06:06):

lemma le_maxi_of_forall {b : β} (hb : ∀a∈s, 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


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

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

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

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

#### Mario Carneiro (May 24 2018 at 06:26):

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

#### Mario Carneiro (May 24 2018 at 06:27):

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

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

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

#### Patrick Massot (May 28 2018 at 09:48):

I don't understand how nnreal could help here

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

#### Patrick Massot (May 28 2018 at 09:52):

Oh yes, I don't want more crazy substraction

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