Saddle points of a map

• IsSaddlePointOn. Let f : E × F → β be a map, where β is preordered. A pair (a,b) in E × F is a saddle point of f on X × Y if f a y ≤ f x b for all x ∈ X and all y in Y.

• isSaddlePointOn_iff: if β is a complete linear order, then (a, b) ∈ X × Y is a saddle point on X × Y iff ⨆ y ∈ Y, f a y = ⨅ x ∈ X, f x b = f a b.

theorem iSup₂_iInf₂_le_iInf₂_iSup₂ {E : Type u_1} {F : Type u_2} {β : Type u_3} (X : Set E) (Y : Set F) (f : E → F → β) [CompleteLinearOrder β] : ⨆ y ∈ Y, ⨅ x ∈ X, f x y ≤ ⨅ x ∈ X, ⨆ y ∈ Y, f x y

The trivial minimax inequality

def IsSaddlePointOn {E : Type u_1} {F : Type u_2} {β : Type u_3} (X : Set E) (Y : Set F) (f : E → F → β) [Preorder β] (a : E) (b : F) : Prop

The pair (a, b) is a saddle point of f on X × Y if f a y ≤ f x b for all x ∈ X and all y in Y.

Note: we do not require that a ∈ X and b ∈ Y.

theorem IsSaddlePointOn.swap_left {E : Type u_1} {F : Type u_2} {β : Type u_3} {X : Set E} {Y : Set F} {f : E → F → β} [Preorder β] {a a' : E} {b b' : F} (ha' : a' ∈ X) (hb : b ∈ Y) (h : IsSaddlePointOn X Y f a b) (h' : IsSaddlePointOn X Y f a' b') : IsSaddlePointOn X Y f a b'

theorem IsSaddlePointOn.swap_right {E : Type u_1} {F : Type u_2} {β : Type u_3} {X : Set E} {Y : Set F} {f : E → F → β} [Preorder β] {a a' : E} {b b' : F} (ha : a ∈ X) (hb' : b' ∈ Y) (h : IsSaddlePointOn X Y f a b) (h' : IsSaddlePointOn X Y f a' b') : IsSaddlePointOn X Y f a' b

theorem isSaddlePointOn_iff {E : Type u_1} {F : Type u_2} {β : Type u_3} {X : Set E} {Y : Set F} {f : E → F → β} [CompleteLinearOrder β] {a : E} (ha : a ∈ X) {b : F} (hb : b ∈ Y) : IsSaddlePointOn X Y f a b ↔ ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b

theorem isSaddlePointOn_iff' {E : Type u_1} {F : Type u_2} {β : Type u_3} {X : Set E} {Y : Set F} {f : E → F → β} [CompleteLinearOrder β] {a : E} (ha : a ∈ X) {b : F} (hb : b ∈ Y) : IsSaddlePointOn X Y f a b ↔ ⨆ y ∈ Y, f a y ≤ ⨅ x ∈ X, f x b

theorem isSaddlePointOn_value {E : Type u_1} {F : Type u_2} {β : Type u_3} {X : Set E} {Y : Set F} {f : E → F → β} [CompleteLinearOrder β] {a : E} (ha : a ∈ X) {b : F} (hb : b ∈ Y) (h : IsSaddlePointOn X Y f a b) : ⨅ x ∈ X, ⨆ y ∈ Y, f x y = f a b ∧ ⨆ y ∈ Y, ⨅ x ∈ X, f x y = f a b

Minimax formulation of saddle points