Documentation

EconCSLib.Math.Minimax.Minimax

EconCSLib.Math.Minimax.Minimax #

Finite two-player zero-sum minimax over any linearly ordered field [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜], with NO compactness and NO LP-optimum-attainment lemma. The route is von Neumann symmetrisation: embed the game A (after a positivity shift) into the skew-symmetric matrix S on I ⊕ J ⊕ Unit; SkewSymmetric.optimal (Theorem of the Alternative) gives a value-0 optimal z = (p, q, λ); reading off the blocks and normalising by ∑ p yields the optimal mixed strategies and the value.

source
theorem Minimax.skew_optimal {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {K : Type u_2} [Fintype K] [DecidableEq K] [Nonempty K] (S : K → K → 𝕜) (hS : ∀ (k l : K), S k l = -S l k) :
∃ (z : K → 𝕜), (∀ (k : K), 0 ≤ z k) ∧ ∑ k : K, z k = 1 ∧ ∀ (l : K), 0 ≤ ∑ k : K, z k * S k l

SkewSymmetric.optimal transported to an arbitrary nonempty finite index.

source
def Minimax.symMat {𝕜 : Type u_1} [Field 𝕜] {I : Type u_2} {J : Type u_3} (A : I → J → 𝕜) :
I ⊕ J ⊕ Unit → I ⊕ J ⊕ Unit → 𝕜

The skew-symmetric symmetrisation of a game A on I ⊕ J ⊕ Unit.

Equations
Instances For
    source
    theorem Minimax.symMat_skew {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} {J : Type u_3} [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] [Nonempty I] [Nonempty J] (A : I → J → 𝕜) (k l : I ⊕ J ⊕ Unit) :
    symMat A k l = -symMat A l k
    source
    theorem Minimax.minimax_pos {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} {J : Type u_3} [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] [Nonempty I] [Nonempty J] (A : I → J → 𝕜) (hA : ∀ (i : I) (j : J), 0 < A i j) :
    ∃ (x : I → 𝕜) (y : J → 𝕜) (v : 𝕜), (∀ (i : I), 0 ≤ x i) ∧ ∑ i : I, x i = 1 ∧ (∀ (j : J), 0 ≤ y j) ∧ ∑ j : J, y j = 1 ∧ (∀ (j : J), v ≤ ∑ i : I, x i * A i j) ∧ ∀ (i : I), ∑ j : J, A i j * y j ≤ v

    Minimax for a strictly positive game.

    source
    theorem Minimax.minimax {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {I : Type u_2} {J : Type u_3} [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] [Nonempty I] [Nonempty J] (A : I → J → 𝕜) :
    ∃ (x : I → 𝕜) (y : J → 𝕜) (v : 𝕜), (∀ (i : I), 0 ≤ x i) ∧ ∑ i : I, x i = 1 ∧ (∀ (j : J), 0 ≤ y j) ∧ ∑ j : J, y j = 1 ∧ (∀ (j : J), v ≤ ∑ i : I, x i * A i j) ∧ ∀ (i : I), ∑ j : J, A i j * y j ≤ v

    Ordered-field von Neumann minimax. Every finite two-player zero-sum game over a linearly ordered field has a value and optimal mixed strategies.