EconCSLib.GameTheory.StrategicGame.ZeroSum.OptimalStrategySetPolytope

For a finite matrix game A, the sets of optimal mixed row and column strategies are nonempty polytopes in the ambient mixed-strategy space. We supply the four structural properties that together characterise an H-polytope (Mathlib does not yet ship a packaged IsPolytope):

• Nonempty, via the minimax theorem.
• Convex, via Mathlib's Convex.inter and the half-space form.
• Closed, via continuity of the defining linear functionals.
• Compact, as a closed subset of the compact standard simplex.

The deliverable is stated on the image of MatrixGame.optimalRowStrategies in I → ℝ (under the subtype value map), which is the natural ambient vector space for polytope vocabulary.

Main results

• MatrixGame.image_optimalRowStrategies_eq — H-representation: Subtype.val '' A.optimalRowStrategies = stdSimplex ℝ I ∩ ⋂ j, {f | A.value ≤ ∑ i, f i * A.g i j}.
• MatrixGame.optimalRowStrategies_image_isPolytope — bundles the convex / closed / compact / nonempty conclusion.
• Symmetric results for optimalColumnStrategies.

References

• [LRS] Laraki, Renault, Sorin, Mathematical Foundations of Game Theory, Proposition 2.4.1(a).

H-representation of the row-optimal set

def MatrixGame.optimalRowSet {I J : Type u} [Fintype I] [Fintype J] [Nonempty J] (A : MatrixGame I J ℝ) : Set (I → ℝ)

H-representation of the row-optimal strategy set in the ambient space I → ℝ: the standard simplex intersected with the finitely many half-spaces A.value ≤ ∑ i, f i * A.g i j, one per pure column j.

Equations

• A.optimalRowSet = stdSimplex ℝ I ∩ ⋂ (j : J), {f : I → ℝ | A.value ≤ ∑ i : I, f i * A.g i j}

def MatrixGame.optimalColumnSet {I J : Type u} [Fintype I] [Fintype J] [Nonempty J] (A : MatrixGame I J ℝ) : Set (J → ℝ)

H-representation of the column-optimal strategy set in the ambient space J → ℝ.

Equations

• A.optimalColumnSet = stdSimplex ℝ J ∩ ⋂ (i : I), {g : J → ℝ | ∑ j : J, g j * A.g i j ≤ A.value}

theorem MatrixGame.image_optimalRowStrategies_eq {I J : Type u} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] (A : MatrixGame I J ℝ) : Subtype.val '' A.optimalRowStrategies = A.optimalRowSet

The image of the row-optimal subtype set equals the H-representation polytope A.optimalRowSet.

Convex / closed / compact / nonempty

theorem MatrixGame.optimalRowSet_convex {I J : Type u} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] (A : MatrixGame I J ℝ) : Convex ℝ A.optimalRowSet

theorem MatrixGame.optimalRowSet_isClosed {I J : Type u} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] (A : MatrixGame I J ℝ) : IsClosed A.optimalRowSet

theorem MatrixGame.optimalRowSet_isCompact {I J : Type u} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] (A : MatrixGame I J ℝ) : IsCompact A.optimalRowSet

theorem MatrixGame.optimalRowSet_nonempty {I J : Type u} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] (A : MatrixGame I J ℝ) : A.optimalRowSet.Nonempty

theorem MatrixGame.optimalRowStrategies_image_isPolytope {I J : Type u} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] (A : MatrixGame I J ℝ) : Convex ℝ (Subtype.val '' A.optimalRowStrategies) ∧ IsClosed (Subtype.val '' A.optimalRowStrategies) ∧ IsCompact (Subtype.val '' A.optimalRowStrategies) ∧ (Subtype.val '' A.optimalRowStrategies).Nonempty

The row-optimal strategy set is a nonempty polytope: convex, closed, compact, and nonempty.

Column-side: dual statement

theorem MatrixGame.image_optimalColumnStrategies_eq {I J : Type u} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] (A : MatrixGame I J ℝ) : Subtype.val '' A.optimalColumnStrategies = A.optimalColumnSet

theorem MatrixGame.optimalColumnSet_convex {I J : Type u} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] (A : MatrixGame I J ℝ) : Convex ℝ A.optimalColumnSet

theorem MatrixGame.optimalColumnSet_isClosed {I J : Type u} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] (A : MatrixGame I J ℝ) : IsClosed A.optimalColumnSet

theorem MatrixGame.optimalColumnSet_isCompact {I J : Type u} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] (A : MatrixGame I J ℝ) : IsCompact A.optimalColumnSet

theorem MatrixGame.optimalColumnSet_nonempty {I J : Type u} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] (A : MatrixGame I J ℝ) : A.optimalColumnSet.Nonempty

theorem MatrixGame.optimalColumnStrategies_image_isPolytope {I J : Type u} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] (A : MatrixGame I J ℝ) : Convex ℝ (Subtype.val '' A.optimalColumnStrategies) ∧ IsClosed (Subtype.val '' A.optimalColumnStrategies) ∧ IsCompact (Subtype.val '' A.optimalColumnStrategies) ∧ (Subtype.val '' A.optimalColumnStrategies).Nonempty