Sion's Minimax

Stream: general

[Alex Meiburg]

Re: #announce > Sion's Minimax Theorem @ 💬

Currently it's proved for _real_ vector spaces and for functions to the reals, but this should generalize pretty readily to general vector spaces, and functions into any densely ordered conditionally complete linear order.

I'm going to be starting to clean this up and PR it soon

[Antoine Chambert-Loir]

Great job! although @ADedecker and myself unfortunatly also had one formalization on that repository https://github.com/AntoineChambert-Loir/Sion4 — which we wanted to upload to mathlib one day or another…

[Antoine Chambert-Loir]

Most of our proof works for a function valued in a dense complete linear order, but for one variant which requires the real numbers (to pass from conditionally complete to complete).

[Antoine Chambert-Loir]

On the other hand, one can observe that any linear order embeds in a complete dense linear order (mathlib doesn't seem to know that), so that this result implies the minimax theorem result for any linear order.

[Ruben Van de Velde]

(deleted)

[Alex Meiburg]

@Antoine Chambert-Loir : (replying here to avoid clutter in announce) Does Mathlib not know the fact you mention by taking WithTop (WithBot alpha)?

[Alex Meiburg]

Also, wow, I didn't realize another formalization existed already :sweat_smile: I had tried searching a few months ago but somehow failed find it. Is the main theorem done? (Sorry free?)

[Antoine Chambert-Loir]

Yes. We were willing to add the actual von Neumann theorem to the list, and Anatole has a PhD thesis to do, hence everything stalled.

[Antoine Chambert-Loir]

There are two things that we need to treat an arbitrary linear order: first densify it, by filling all holes by intervals [0;1], and then add a top and bottom element if needed (but only if needed) (rather add them first, so that it remains to fill the holes).

[Antoine Chambert-Loir]

By accident, I happened to PR #29976 tonight, with some basic results on semicontinuous functions part of which is needed.

[Alex Meiburg]

Ahhh, definitely some duplicate work there too - I have the same statements in my repo..

[Yijun Yuan]

Antoine Chambert-Loir said in #announce > Sion's Minimax Theorem :

any linear order embeds in a complete dense linear order

In my work on Hader-Narasimhan theory, I implemented the Dedekind-MacNeille completion DM(X) of any partially ordered set X (the minimal complete lattice containing a given partially ordered set), and showed that

1. If the order on X is linear, then the order on DM(X) is also linear.
2. The universal property of DM(X): any order embedding X→Y, with Y a complete lattice, factors through the canonical embedding X→DM(X).

What I do not formalize: The denseness of X in DM(X) (meet-dense, join-dense...)

I don't know if there is any overlap, or if my code is useful for you. @Antoine Chambert-Loir

Code: https://github.com/YijunYuan/HarderNarasimhan/blob/master/HarderNarasimhan/OrderTheory/DedekindMacNeilleCompletion.lean

[Notification Bot]

4 messages were moved here from #announce > Sion's Minimax Theorem by Mario Carneiro.

[Antoine Chambert-Loir]

@Yijun Yuan If I may, you should coordinate with the group of people who are simultaneously discussing the same thing on thath other channel #maths > Dedekind-MacNeille completion

[Antoine Chambert-Loir]

This is not exactly what I need, though: I want a dense complete linear order containing the initial linear order. (It won't be dense if the initial linear order has holes.)

[Aaron Liu]

Antoine Chambert-Loir said:

This is not exactly what I need, though: I want a dense complete linear order containing the initial linear order. (It won't be dense if the initial linear order has holes.)

You can lex it with the rationals to make it dense

[Aaron Liu]

Or I guess with the reals since it has to be complete

[Alex Meiburg]

I think those relevant facts aren't in Mathlib either
https://loogle.lean-lang.org/?q=ConditionallyCompleteLinearOrder%2C+Lex

[Aaron Liu]

no sorry the reals aren't complete either

[Aaron Liu]

just lex it with any nontrivial complete dense order

[Alex Meiburg]

Well that isn't in Mathlib either :sweat_smile:
My proof goes directly with a /conditionally/ complete order off the bat btw, so I don't need to embed in a complete order at the end

[Alex Meiburg]

One thing I want to poke at a bit more is exactly what the minimal requirements on boundedness are for it to go through in the conditional setting

[Anatole Dedecker]

Alex Meiburg said:

Also, wow, I didn't realize another formalization existed already :sweat_smile: I had tried searching a few months ago but somehow failed find it. Is the main theorem done? (Sorry free?)

I'm really sorry for all the duplicate work, this has been ready for a while and should have made its way into Mathlib if it were not for my complete inability to complete a project before starting the next one...

[Anatole Dedecker]

Alex Meiburg said:

One thing I want to poke at a bit more is exactly what the minimal requirements on boundedness are for it to go through in the conditional setting

Well you may be interested in the minimax statement in our repo, which assumes no kind of completeness but only that every inf and sup exists