feat(Topology/Sion): the minimax theorem of von Neumann - Sion

[AntoineChambert-Loir]

Prove Sion.exists_isSaddlePointOn :
Let X and Y be convex subsets of topological vector spaces E and F,
X being moreover compact,
and let f : X × Y → ℝ be a function such that

• for all x, f(x, ⬝) is upper semicontinuous and quasiconcave
• for all y, f(⬝, y) is lower semicontinuous and quasiconvex
  Then inf_x sup_y f(x,y) = sup_y inf_x f(x,y).

The classical case of the theorem assumes that f is continuous,
f(x, ⬝) is concave, f(⬝, y) is convex.

As a particular case, one get the von Neumann theorem where
f is bilinear and E, F are finite dimensional.

We follow the proof of Komiya (1988).

Remark on implementation

• The essential part of the proof holds for a function
  f : X → Y → β, where β is a complete dense linear order.

• We have written part of it for just a dense linear order,

• On the other hand, if the theorem holds for such β,
  it must hold for any linear order, for the reason that
  any linear order embeds into a complete dense linear order.
  Although the Dedekind McNeille completion (docs#DedekindCut) furnishes a complete lattice,
  it is not dense in general, so that this result does not seem to be known to Mathlib yet.

• When β is ℝ, one can use Real.toEReal and one gets a proof for ℝ.

TODO

Give particular important cases (eg, bilinear maps in finite dimension).

Co-authored with @ADedecker

---

• depends on: [Merged by Bors] - feat(Analysis/Convex/Quasiconvex): properties of quasiconcave functions #31548
• depends on: [Merged by Bors] - feat(Order/SaddlePoint): define saddle points of a map #31547
• depends on: [Merged by Bors] - feat(Topology/Sublevel): sublevels in relation with semicontinuity and compactness #31558

[github-actions]

PR summary 6ef8cc2731

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Topology.Sion (new file)	1443

---

Declarations diff

+ DMCompletion.exists_isSaddlePointOn
+ clusterPt_principal_subtype_iff_frequently
+ coe_orderEmbedding
+ disjoint_sublevelLeft
+ exists_isSaddlePointOn
+ exists_isSaddlePointOn'
+ exists_lt_iInf_of_lt_iInf_of_finite
+ exists_lt_iInf_of_lt_iInf_of_sup
+ exists_saddlePointOn'
+ isClosed_setOf_sublevelLeft_subset
+ isClosed_sublevelLeft
+ isPreconnected_sublevelLeft
+ lowerSemicontinuousOn_of_forall_isMaxOn_and_mem
+ mem_sublevelLeft_iff
+ minimax
+ minimax'
+ monotone_sublevelLeft
+ nonempty_sublevelLeft
+ orderEmbedding
+ setOf_sublevelLeft_subset
+ sublevelLeft
+ sublevelLeft_subset_union
+ upperSemicontinuousOn_of_forall_isMinOn_and_mem

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[thorimur]

Thanks for this PR! :) Just to clarify, is this PR ready for review? If not, please comment WIP to mark it as a work in progress.

I will also unassign myself, as I was auto-assigned and it's not my field; hopefully the algorithm will assign a more appropriate reviewer. :)

[AntoineChambert-Loir]

I believe it is ready for review. There are a few -- private comments which indicate that maybe some definitions could be made private. The opinion of the reviewer will be valuable.

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[j-loreaux]

I'll be back to review this in more depth soon.

[j-loreaux]

Okay, I have now been through this fairly thoroughly. Aside from the comments below and the refactoring with DedekindCut, I think this is pretty much ready.

[j-loreaux]

I think this is no longer true, even if it was when you first made the PR. See DedekindCut.principalEmbedding

[AntoineChambert-Loir]

In fact, we need that the stuff be dense. I don't know whether it just suffices to take a product with [0;1] or if we need to fill open intervals within every pair (a,b) such that a<b and such that there are no elements inbetween.

[j-loreaux]

As indicated above, we have this now.

[j-loreaux]

I think this section can be simplified now.

[AntoineChambert-Loir]

As I wrote above, the Dedekind MacNeille completion is not exactly sufficient to complete the proof, because it creates a complete lattice, but not a dense one. Maybe this precise construction (together with lemmas on the Dedekind MacNeille completion) should be left to another PR. And then the final lemma about what happens when there exists such a dense completion would be replaced/deprecated.