Formalization of Sion's version of the von Neumann minimax theorem

Statements

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 ∈ X, f(x, ⬝) is upper semicontinuous and quasiconcave
• for all y ∈ Y, f(⬝, y) is lower semicontinuous and quasiconvex Then ⊓ x, ⊔ y, f (x, y) = ⊔ y, ⊓ 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][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 one can construct such an embedding using the Dedekind-Mac Neille completion, this result does not seem to be known to Mathlib.

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

TODO

• Spell out the particular case of von Neumann theorem.

• Use the Dedekind MacNeille completion of a linear order to simplify the statement of DMCompletion.exists_isSaddlePointOn.

References

• [vonNeumann-1928][Neumann, John von (1928). ”Zur Theorie der Gesellschaftsspiele”. Mathematische Annalen 100 (1): 295‑320]

• [Sion-1958][Sion, Maurice (1958). ”On general minimax theorems”. Pacific Journal of Mathematics 8 (1): 171‑76.]

• [Komiya-1988][Komiya, Hidetoshi (1988). “Elementary Proof for Sion’s Minimax Theorem”. Kodai Mathematical Journal 11 (1).]

theorem Sion.exists_lt_iInf_of_lt_iInf_of_sup {E : Type u_1} {F : Type u_2} {β : Type u_3} [LinearOrder β] {X : Set E} {Y : Set F} {f : E → F → β} [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] (ne_X : X.Nonempty) (kX : IsCompact X) (hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun (x : E) => f x y) X) (hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun (x : E) => f x y) [TopologicalSpace F] [AddCommGroup F] [Module ℝ F] (cY : Convex ℝ Y) (hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun (y : F) => f x y) Y) (hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun (y : F) => f x y) [DenselyOrdered β] [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] {y1 : F} (hy1 : y1 ∈ Y) {y2 : F} (hy2 : y2 ∈ Y) {t : β} (ht : ∀ x ∈ X, t < max (f x y1) (f x y2)) : ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0

theorem Sion.exists_lt_iInf_of_lt_iInf_of_finite {E : Type u_1} {F : Type u_2} {β : Type u_3} [LinearOrder β] {X : Set E} {Y : Set F} {f : E → F → β} [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] (ne_X : X.Nonempty) (kX : IsCompact X) (hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun (x : E) => f x y) X) (hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun (x : E) => f x y) [TopologicalSpace F] [AddCommGroup F] [Module ℝ F] (cY : Convex ℝ Y) (hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun (y : F) => f x y) Y) (hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun (y : F) => f x y) [DenselyOrdered β] [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] (cX : Convex ℝ X) {s : Set F} (hs : s.Finite) (hsY : s ⊆ Y) {t : β} (ht : ∀ x ∈ X, ∃ y ∈ s, t < f x y) : ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0

theorem Sion.minimax {E : Type u_1} {F : Type u_2} {β : Type u_3} [LinearOrder β] {X : Set E} {Y : Set F} {f : E → F → β} [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] (ne_X : X.Nonempty) (kX : IsCompact X) (hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun (x : E) => f x y) X) (hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun (x : E) => f x y) [TopologicalSpace F] [AddCommGroup F] [Module ℝ F] (cY : Convex ℝ Y) (hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun (y : F) => f x y) Y) (hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun (y : F) => f x y) [DenselyOrdered β] [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] (cX : Convex ℝ X) (sup_y : E → β) (hsup_y : ∀ x ∈ X, IsLUB {x_1 : β | ∃ y ∈ Y, f x y = x_1} (sup_y x)) (inf_sup : β) (hinf_sup : IsGLB {x : β | ∃ x_1 ∈ X, sup_y x_1 = x} inf_sup) (inf_x : F → β) (hinf_x : ∀ y ∈ Y, IsGLB {x : β | ∃ x_1 ∈ X, f x_1 y = x} (inf_x y)) (sup_inf : β) (hsup_inf : IsLUB {x : β | ∃ y ∈ Y, inf_x y = x} sup_inf) : inf_sup = sup_inf

A minimax theorem without completeness, using IsGLB and IsLUB.

theorem Sion.exists_isSaddlePointOn' {E : Type u_1} {F : Type u_2} {β : Type u_3} [LinearOrder β] {X : Set E} {Y : Set F} {f : E → F → β} [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] (ne_X : X.Nonempty) (kX : IsCompact X) (hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun (x : E) => f x y) X) (hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun (x : E) => f x y) [TopologicalSpace F] [AddCommGroup F] [Module ℝ F] (cY : Convex ℝ Y) (kY : IsCompact Y) (hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun (y : F) => f x y) Y) (hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun (y : F) => f x y) [DenselyOrdered β] [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] (cX : Convex ℝ X) (ne_Y : Y.Nonempty) : ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b

The Sion-von Neumann minimax theorem (saddle point form)

theorem Sion.minimax' {E : Type u_1} {F : Type u_2} {β : Type u_3} [CompleteLinearOrder β] [DenselyOrdered β] {X : Set E} {Y : Set F} {f : E → F → β} [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] (ne_X : X.Nonempty) (cX : Convex ℝ X) (kX : IsCompact X) (hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun (x : E) => f x y) X) (hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun (x : E) => f x y) [TopologicalSpace F] [AddCommGroup F] [Module ℝ F] [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] (cY : Convex ℝ Y) (hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun (y : F) => f x y) Y) (hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun (y : F) => f x y) : ⨅ x ∈ X, ⨆ y ∈ Y, f x y = ⨆ y ∈ Y, ⨅ x ∈ X, f x y

A minimax theorem in inf-sup form, for complete linear orders.

theorem Sion.exists_saddlePointOn' {E : Type u_1} {F : Type u_2} {β : Type u_3} [CompleteLinearOrder β] [DenselyOrdered β] {X : Set E} {Y : Set F} {f : E → F → β} [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] (ne_X : X.Nonempty) (cX : Convex ℝ X) (kX : IsCompact X) (hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun (x : E) => f x y) X) (hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun (x : E) => f x y) [TopologicalSpace F] [AddCommGroup F] [Module ℝ F] [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] (cY : Convex ℝ Y) (ne_Y : Y.Nonempty) (kY : IsCompact Y) (hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun (y : F) => f x y) Y) (hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun (y : F) => f x y) : ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b

The Sion-von Neumann minimax theorem (saddle point form), case of complete linear orders.

theorem Sion.DMCompletion.exists_isSaddlePointOn {E : Type u_1} {F : Type u_2} {β : Type u_3} [LinearOrder β] {X : Set E} {Y : Set F} {f : E → F → β} [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] (ne_X : X.Nonempty) (cX : Convex ℝ X) (kX : IsCompact X) (hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun (x : E) => f x y) X) (hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun (x : E) => f x y) [TopologicalSpace F] [AddCommGroup F] [Module ℝ F] [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] (cY : Convex ℝ Y) (ne_Y : Y.Nonempty) (kY : IsCompact Y) (hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun (y : F) => f x y) Y) (hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun (y : F) => f x y) [TopologicalSpace β] [OrderTopology β] {γ : Type u_5} [CompleteLinearOrder γ] [DenselyOrdered γ] [TopologicalSpace γ] [OrderTopology γ] {ι : β ↪o γ} (hι : Continuous ⇑ι) : ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b

The minimax theorem, in the saddle point form, when β is given a Dedekind-MacNeille completion ι : β ↪o γ

theorem Sion.exists_isSaddlePointOn {E : Type u_1} {F : Type u_2} {X : Set E} {Y : Set F} {f : E → F → ℝ} [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] (ne_X : X.Nonempty) (cX : Convex ℝ X) (kX : IsCompact X) (hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun (x : E) => f x y) X) (hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun (x : E) => f x y) [TopologicalSpace F] [AddCommGroup F] [Module ℝ F] [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] (cY : Convex ℝ Y) (ne_Y : Y.Nonempty) (kY : IsCompact Y) (hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun (y : F) => f x y) Y) (hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun (y : F) => f x y) : ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b

The minimax theorem, in the saddle point form