EconCSLib.GameTheory.StrategicGame.ZeroSum.StochasticMatrix

Formalises [MFoGT Cor. 2.5.2]: every finite stochastic matrix has an invariant distribution. Proven via the matrix game with payoff B := A − I: its value is 0, and any row-optimal strategy x* is a left eigenvector of A (i.e. x* A = x*).

Main results

• IsStochasticMatrix — predicate for a row-stochastic matrix.
• uniformDist — uniform mixed strategy on a finite nonempty type.
• MatrixGame.exists_invariant_distribution — every stochastic matrix admits an invariant distribution.

Blueprint

• docs/knowledge/nodes/zero_sum/stochastic_matrix_invariant_distribution.md

structure EconCSLib.StrategicGame.IsStochasticMatrix {I : Type} [Fintype I] (A : I → I → ℝ) : Prop

A finite (row-)stochastic matrix: entries are non-negative and each row sums to 1.

• nonneg (i j : I) : 0 ≤ A i j
• rowSum (i : I) : ∑ j : I, A i j = 1

theorem EconCSLib.StrategicGame.IsStochasticMatrix.total_mass_preserved {I : Type} [Fintype I] [Nonempty I] [DecidableEq I] {A : I → I → ℝ} (hA : IsStochasticMatrix A) (x : I → ℝ) : ∑ j : I, ∑ i : I, x i * A i j = ∑ i : I, x i

The total mass after one application of a stochastic matrix to a probability vector equals the initial mass: ∑_j (xA)_j = ∑_i x_i.

noncomputable def EconCSLib.StrategicGame.uniformDist {I : Type} [Fintype I] [Nonempty I] : ↑(stdSimplex ℝ I)

Uniform mixed strategy on a finite nonempty index type.

Equations

• EconCSLib.StrategicGame.uniformDist = ⟨fun (x : I) => 1 / ↑(Fintype.card I), ⋯⟩

@[simp]

theorem EconCSLib.StrategicGame.uniformDist_val {I : Type} [Fintype I] [Nonempty I] [DecidableEq I] (i : I) : ↑uniformDist i = 1 / ↑(Fintype.card I)

The displacement matrix B = A − I

Value of the displacement game is zero

Main theorem: existence of an invariant distribution

theorem EconCSLib.StrategicGame.MatrixGame.exists_invariant_distribution {I : Type} [Fintype I] [Nonempty I] [DecidableEq I] (A : I → I → ℝ) (hA : IsStochasticMatrix A) : ∃ (x : ↑(stdSimplex ℝ I)), ∀ (j : I), ∑ i : I, ↑x i * A i j = ↑x j

Every finite stochastic matrix has an invariant distribution [MFoGT Cor. 2.5.2].