EconCSLib.GameTheory.StrategicGame.ZeroSum.Antisymmetric

For a square matrix B : I → I → ℝ with B = -Bᵀ (i.e. B i j = -B j i), the matrix game B has value 0 [MFoGT §2.8, Exercise 10(1)].

Equivalently, there exists x ∈ Δ(I) such that (Bx)_i ≤ 0 for every i.

Proof

By the minimax theorem the game has a value v. From B = -Bᵀ, every mixed z satisfies zᵀ B z = 0. Hence for the optimal xx: ∑ j, xx_j · Ej xx j = xxᵀ B xx = 0, but each Ej xx j ≥ value, so value ≤ 0. Symmetrically value ≥ 0.

def EconCSLib.StrategicGame.IsAntisymmetric {I : Type} (B : I → I → ℝ) : Prop

A square matrix is antisymmetric if B i j = -B j i for all i, j.

Equations

• EconCSLib.StrategicGame.IsAntisymmetric B = ∀ (i j : I), B i j = -B j i

theorem EconCSLib.StrategicGame.IsAntisymmetric.diag_zero {I : Type} [Fintype I] [Nonempty I] [DecidableEq I] {B : I → I → ℝ} (hB : IsAntisymmetric B) (i : I) : B i i = 0

An antisymmetric matrix has zero diagonal.

theorem EconCSLib.StrategicGame.IsAntisymmetric.quadform_zero {I : Type} [Fintype I] [Nonempty I] [DecidableEq I] {B : I → I → ℝ} (hB : IsAntisymmetric B) (z : I → ℝ) : ∑ i : I, ∑ j : I, z i * B i j * z j = 0

For any vector z, ∑_{i,j} z_i B_{ij} z_j = 0.

theorem EconCSLib.StrategicGame.MatrixGame.antisymmetric_value_zero {I : Type} [Fintype I] [Nonempty I] [DecidableEq I] {B : I → I → ℝ} (hB : IsAntisymmetric B) : { g := B }.value = 0

Antisymmetric matrix game has value 0 [MFoGT §2.8, Ex. 10(1)].

theorem EconCSLib.StrategicGame.MatrixGame.antisymmetric_exists_optimal_strategy {I : Type} [Fintype I] [Nonempty I] [DecidableEq I] {B : I → I → ℝ} (hB : IsAntisymmetric B) : ∃ (y : ↑(stdSimplex ℝ I)), ∀ (i : I), ∑ j : I, B i j * ↑y j ≤ 0

An antisymmetric matrix game admits an optimal column strategy y* with (B y*)_i ≤ 0 for every i.