EconCSLib.Math.Minimax.SkewSymmetric

For a skew-symmetric matrix S : Fin N → Fin N → 𝕜 (S k l = - S l k) over a linearly ordered field, the symmetric matrix game on S has value 0: there is a mixed strategy z ∈ Δ with ∑ₖ zₖ Sₖₗ ≥ 0 for every column l.

This is the engine of the ordered-field minimax theorem (von Neumann symmetrisation): it is a pure feasibility statement, closed by the Theorem of the Alternative (EconCSLib.LinearAlgebra.theorem_of_alternative) — no LP optimum / attainment is needed. If the feasibility system had no solution, the Farkas certificate would yield w ≥ 0, w ≠ 0 with S w < 0 everywhere; but skew-symmetry forces wᵀ S w = 0, a contradiction.

theorem SkewSymmetric.optimal {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {N : ℕ} [NeZero N] (S : Fin N → Fin N → 𝕜) (hS : ∀ (k l : Fin N), S k l = -S l k) : ∃ (z : Fin N → 𝕜), (∀ (k : Fin N), 0 ≤ z k) ∧ ∑ k : Fin N, z k = 1 ∧ ∀ (l : Fin N), 0 ≤ ∑ k : Fin N, z k * S k l

Skew-symmetric optimal strategy. Every skew-symmetric game has a value-0 optimal mixed strategy.