Zulip Chat Archive

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

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

(and added segfault)

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

(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: Dec 20 2023 at 11:08 UTC