Grace/Cumulus/GameTheory/Polymatrix.g17

Open in Workbench Download source

Imports

NashDeviation · PureProfile

Declarations

Source

1-- Polymatrix games: the payoff to the owner of pure strategy i is the sum,2-- over the pure strategies j of the other players, of the opponent's3-- probability of j times a table entry T(i)(j). Two-player bimatrix games are4-- the case of two blocks. Every polymatrix game has a Nash equilibrium5-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.GameTheory.Polymatrix11import NashDeviation12import PureProfile1314-- The terms a(j)·x(j) of a row of the table, as a family of cube functions.15defgraph rowFamily (n a : Set) (j ∈ n) : functionSpace(unitCube(n), ℝ) := mulCube(n, constantFunction(unitCube(n), ℝ, a(j)), coordinateCube(n, j))16requires nNat : Nat(n)17requires aFunction : a : n → ℝ18proof19  have aj := FunctionBetween.apply_closed with aFunction, member20  have constant := constantCube.continuous at n, a(j) with aj21  have coordinate := coordinateCube.continuous at n, j with member22  have continuous := mulCube.continuous with constant, coordinate23  have function := CubeFunctionContinuous.function with continuous24  have between : mulCube(n, constantFunction(unitCube(n), ℝ, a(j)), coordinateCube(n, j)) : unitCube(n) → ℝ25    exact CubeFunction.function with function26  exact functionSpace.mem_iff.backward with between2728theorem rowFamily.continuous (n : Nat) (a : Set)29  requires aFunction : a : n → ℝ30  shows ∀ j ∈ n, CubeFunctionContinuous(rowFamily(n, a)(j), n)31proof32  intros j hj33  have same := rowFamily.value at n, a, j with *34  have aj := FunctionBetween.apply_closed with aFunction, hj35  have constant := constantCube.continuous with aj36  have coordinate := coordinateCube.continuous with hj37  rw same38  exact mulCube.continuous with constant, coordinate3940theorem rowFamily.functions (n : Nat) (a : Set)41  requires aFunction : a : n → ℝ42  shows ∀ j ∈ n, CubeFunction(rowFamily(n, a)(j), n)43proof44  intros j hj45  have continuous := rowFamily.continuous with aFunction46  exact CubeFunctionContinuous.function with (continuous with hj)4748theorem rowFamily.term (n : Nat) (a x j : Set)49  requires aFunction : a : n → ℝ50  requires hx : x ∈ unitCube(n)51  requires hj : j ∈ n52  shows rowFamily(n, a)(j)(x) = (a(j):R) * (x(j):R)53proof54  have same := rowFamily.value at n, a, j with *55  have aj := FunctionBetween.apply_closed with aFunction, hj56  have constant := constantCube.continuous with aj57  have coordinate := coordinateCube.continuous with hj58  have constantFunction2 := CubeFunctionContinuous.function with constant59  have coordinateFunction := CubeFunctionContinuous.function with coordinate60  have product := mulCube.value with constantFunction2, coordinateFunction, hx61  have constantValue := constantFunction.apply with hx, aj62  have coordinateValue := coordinateCube.value with hj, hx63  rw [same, product, constantValue, coordinateValue]64  rfl6566-- The payoff to the owner of i against the other players' mixtures.67def polymatrixPayoff (n blk T i : Set) : Set :=68  weightedSum(n, n ∖ blockSet(n, blk, blk(i)), rowFamily(n, T(i)))6970theorem polymatrixPayoff.definition (n blk T i : Set)71  shows polymatrixPayoff(n, blk, T, i) = weightedSum(n, n ∖ blockSet(n, blk, blk(i)), rowFamily(n, T(i)))72proof73  unfold polymatrixPayoff74  rfl7576theorem polymatrixPayoff.row (n T i : Set)77  requires table : T : n → functionSpace(n, ℝ)78  requires hi : i ∈ n79  shows T(i) : n → ℝ80proof81  have inSpace := FunctionBetween.apply_closed with table, hi82  exact functionSpace.mem_iff.forward with inSpace8384theorem polymatrixPayoff.continuous (n : Nat) (blk T i : Set)85  requires table : T : n → functionSpace(n, ℝ)86  requires hi : i ∈ n87  shows CubeFunctionContinuous(polymatrixPayoff(n, blk, T, i), n)88proof89  have row := polymatrixPayoff.row with table, hi90  have terms := rowFamily.continuous with row91  have same := polymatrixPayoff.definition at n, blk, T, i92  rw same93  exact weightedSum.continuous with terms9495-- The payoff of i only depends on the coordinates outside i's own block.96theorem polymatrixPayoff.independent (n : Nat) (blk T i x z : Set)97  requires table : T : n → functionSpace(n, ℝ)98  requires hi : i ∈ n99  requires hx : x ∈ unitCube(n)100  requires hz : z ∈ unitCube(n)101  requires agree : ∀ j ∈ n, blk(j) ≠ blk(i) → z(j) = x(j)102  shows polymatrixPayoff(n, blk, T, i)(z) = polymatrixPayoff(n, blk, T, i)(x)103proof104  have row := polymatrixPayoff.row with table, hi105  have functions := rowFamily.functions with row106  have same := polymatrixPayoff.definition at n, blk, T, i107  have zValue := weightedSum.value at n, n ∖ blockSet(n, blk, blk(i)), rowFamily(n, T(i)), z with functions, hz108  have xValue := weightedSum.value at n, n ∖ blockSet(n, blk, blk(i)), rowFamily(n, T(i)), x with functions, hx109  have zPoints := assembledPoint.function with functions, hz110  have xPoints := assembledPoint.function with functions, hx111  have maskedZ := maskedPoint.sequence at n, n ∖ blockSet(n, blk, blk(i)), assembledPoint(n, rowFamily(n, T(i)), z) with zPoints112  have maskedX := maskedPoint.sequence at n, n ∖ blockSet(n, blk, blk(i)), assembledPoint(n, rowFamily(n, T(i)), x) with xPoints113  have termsAgree : ∀ k ∈ ℕ, k < n → maskedPoint(n, n ∖ blockSet(n, blk, blk(i)), assembledPoint(n, rowFamily(n, T(i)), z))(k) = maskedPoint(n, n ∖ blockSet(n, blk, blk(i)), assembledPoint(n, rowFamily(n, T(i)), x))(k)114    intros k hk hkn115    have hkIn : k ∈ n by exact membership.of_Less with hkn116    have alternatives : k ∈ n ∖ blockSet(n, blk, blk(i)) ∨ ¬k ∈ n ∖ blockSet(n, blk, blk(i)) by tauto117    cases alternatives with outsideBlock | insideBlock118    . have zSame := maskedPoint.on_block with zPoints, hkIn, outsideBlock119      have xSame := maskedPoint.on_block with xPoints, hkIn, outsideBlock120      have zPoint := assembledPoint.value with functions, hz, hkIn121      have xPoint := assembledPoint.value with functions, hx, hkIn122      have zTerm := rowFamily.term with row, hz, hkIn123      have xTerm := rowFamily.term with row, hx, hkIn124      have parts := difference.membership.forward with outsideBlock125      have notOwn : blk(k) ≠ blk(i)126        intro own127        apply parts.right128        apply blockSet.membership.backward129        exact ⟨hkIn, own⟩130      have coordinate := agree with hkIn, notOwn131      rw [zSame, xSame, zPoint, xPoint, zTerm, xTerm, coordinate]132      rfl133    . have zSame := maskedPoint.off_block with zPoints, hkIn, insideBlock134      have xSame := maskedPoint.off_block with xPoints, hkIn, insideBlock135      rw [zSame, xSame]136      rfl137  have equal := realPartialSum.eq_prefix with maskedZ, maskedX, termsAgree138  rwa [same, zValue, xValue]139140-- The family of all payoff functions of the game.141defgraph polymatrixPayoffs (n blk T : Set) (i ∈ n) : functionSpace(unitCube(n), ℝ) := polymatrixPayoff(n, blk, T, i)142requires nNat : Nat(n)143requires table : T : n → functionSpace(n, ℝ)144proof145  have continuous := polymatrixPayoff.continuous at n, blk, T, i with table, member146  have function := CubeFunctionContinuous.function with continuous147  have between : polymatrixPayoff(n, blk, T, i) : unitCube(n) → ℝ148    exact CubeFunction.function with function149  exact functionSpace.mem_iff.backward with between150151theorem polymatrixPayoffs.continuous (n : Nat) (blk T : Set)152  requires table : T : n → functionSpace(n, ℝ)153  shows ∀ i ∈ n, CubeFunctionContinuous(polymatrixPayoffs(n, blk, T)(i), n)154proof155  intros i hi156  have same := polymatrixPayoffs.value at n, blk, T, i with *157  rw same158  exact polymatrixPayoff.continuous with table, hi159160-- Every polymatrix game has a Nash equilibrium: a profile x such that no161-- player improves their expected payoff by changing their own mixture.162theorem polymatrix.equilibrium (n : Nat) (m blk T rep : Set)163  requires blkFunction : blk : n → m164  requires repFunction : rep : m → n165  requires section : ∀ q ∈ m, blk(rep(q)) = q166  requires table : T : n → functionSpace(n, ℝ)167  shows ∃ x ∈ simplexProduct(n, m, blk), ∀ p ∈ m, ∀ z ∈ simplexProduct(n, m, blk), (∀ j ∈ n, blk(j) ≠ p → z(j) = x(j)) → (expectedPayoff(n, blk, polymatrixPayoffs(n, blk, T), p)(z):R) ≤ (expectedPayoff(n, blk, polymatrixPayoffs(n, blk, T), p)(x):R)168proof169  have anchor := pureProfile.in_product with blkFunction, repFunction, section170  have family := polymatrixPayoffs.continuous at n, blk, T with table171  obtain ⟨x, equilibrium⟩ := nash.exists_equilibrium with blkFunction, anchor, family172  have hx := Equilibrium.profile with equilibrium173  have xCube := simplexProduct.cube with hx174  witness x175  constructor176  . exact hx177  . intros p hp z hz agree178    have zCube := simplexProduct.cube with hz179    have independent : ∀ i ∈ n, blk(i) = p → polymatrixPayoffs(n, blk, T)(i)(z) = polymatrixPayoffs(n, blk, T)(i)(x)180      intros i hi own181      have same := polymatrixPayoffs.value at n, blk, T, i with *182      have agreeI : ∀ j ∈ n, blk(j) ≠ blk(i) → z(j) = x(j)183        intros j hj notOwn184        rw own at notOwn185        exact agree with hj, notOwn186      rw same187      exact polymatrixPayoff.independent with table, hi, xCube, zCube, agreeI188    exact nash.no_deviation with blkFunction, family, equilibrium, hz, hp, independent189