Grace/Cumulus/GameTheory/NashEquilibrium.g17

Open in Workbench Download source

Imports

NashMap · FixedPoint.BrouwerSimplex

Declarations

Source

1-- Nash's theorem: a game is given by a block map assigning each pure2-- strategy to its player and, for each pure strategy i, a continuous function3-- V(i) on the cube giving the payoff to the owner of i when they switch to i4-- against the profile. At a fixed point of Nash's map no pure strategy pays5-- more than the owner's expected payoff, so the fixed point is an equilibrium6-- Part of Cumulus, the Grace17 mathematics library.7-- Copyright (c) 2026 Grant Passmore.8-- Released under the Apache License 2.0. See LICENSE in the repository root.9-- Authors: Grant Passmore1011module Grace.Cumulus.GameTheory.NashEquilibrium12import NashMap13import FixedPoint.BrouwerSimplex1415-- The deviation terms x(j)·(V(j)(x) − U) of a profile against a level U.16defgraph deviationTerms (n V x : Set) (U : Real) (j ∈ n) : ℝ := (x(j):R) * ((V(j)(x):R) + -U)17requires nNat : Nat(n)18requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)19requires hx : x ∈ unitCube(n)20proof21  have xj := unitCube.coordinate_real with hx, member22  have vj := CubeFunction.value with (CubeFunctionContinuous.function with (family with member)), hx23  have negative := realNegValue.real at U24  have difference := realAddValue.real at V(j)(x), -U25  exact realMulValue.real at x(j), (V(j)(x):R) + -U2627-- Summed over a block, the deviation terms are the block's payoff sum minus28-- U times the block's probability mass.29theorem deviationTerms.sum (n : Nat) (S V x : Set) (U : Real)30  requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)31  requires hx : x ∈ unitCube(n)32  shows realPartialSum(maskedPoint(n, S, deviationTerms(n, V, x, U)), n) = (realPartialSum(maskedPoint(n, S, assembledPoint(n, payoffFamily(n, V), x)), n):R) - U * (realPartialSum(maskedPoint(n, S, x), n):R)33proof34  have xFunction := unitCube.point with hx35  have functions := payoffFamily.functions with family36  have dFunction := deviationTerms.function at n, V, x, U with *37  have pFunction := assembledPoint.function with functions, hx38  have maskedD := maskedPoint.sequence at n, S, deviationTerms(n, V, x, U) with dFunction39  have maskedP := maskedPoint.sequence at n, S, assembledPoint(n, payoffFamily(n, V), x) with pFunction40  have maskedX := maskedPoint.sequence at n, S, x with xFunction41  have constantU := constantSequence.sequence at U42  have scaledX := mulSequence.sequence with constantU, maskedX43  have difference := subSequence.sequence with maskedP, scaledX44  have agree : ∀ k ∈ ℕ, k < n → maskedPoint(n, S, deviationTerms(n, V, x, U))(k) = subSequence(maskedPoint(n, S, assembledPoint(n, payoffFamily(n, V), x)), mulSequence(constantSequence(U), maskedPoint(n, S, x)))(k)45    intros k hk hkn46    have kNat : Nat(k) by typecheck47    have hkIn : k ∈ n by exact membership.of_Less with hkn48    have pReal := RealSequence.value at maskedPoint(n, S, assembledPoint(n, payoffFamily(n, V), x)), k with maskedP49    have xReal := RealSequence.value at maskedPoint(n, S, x), k with maskedX50    have uReal := RealSequence.value at constantSequence(U), k with constantU51    have uValue := constantSequence.value at U, k52    have scaledValue := mulSequence.value with constantU, maskedX, uReal, xReal53    have scaledReal := RealSequence.value at mulSequence(constantSequence(U), maskedPoint(n, S, x)), k with scaledX54    have differenceValue := subSequence.value with maskedP, scaledX, pReal, scaledReal55    rw [differenceValue, scaledValue, uValue]56    have alternatives : k ∈ S ∨ ¬k ∈ S by tauto57    cases alternatives with inBlock | outside58    . have dSame := maskedPoint.on_block with dFunction, hkIn, inBlock59      have pSame := maskedPoint.on_block with pFunction, hkIn, inBlock60      have xSame := maskedPoint.on_block with xFunction, hkIn, inBlock61      have dValue := deviationTerms.value at n, V, x, U, k with *62      have pValue := assembledPoint.value with functions, hx, hkIn63      have term := payoffFamily.term with family, hx, hkIn64      have xk := unitCube.coordinate_real with hx, hkIn65      have vk := CubeFunction.value with (CubeFunctionContinuous.function with (family with hkIn)), hx66      rw [dSame, pSame, xSame, dValue, pValue, term]67      ring68    . have dSame := maskedPoint.off_block with dFunction, hkIn, outside69      have pSame := maskedPoint.off_block with pFunction, hkIn, outside70      have xSame := maskedPoint.off_block with xFunction, hkIn, outside71      rw [dSame, pSame, xSame]72      ring73  have equal := realPartialSum.eq_prefix with maskedD, difference, agree74  have sub := realPartialSum.sub with maskedP, scaledX75  have scale := realPartialSum.scale with maskedX76  rw [equal, sub, scale]77  rfl7879-- Against the owner's own expected payoff, the deviation terms of a block sum80-- to zero on the product of simplices.81theorem deviationTerms.sum_zero (n : Nat) (m blk V x p : Set)82  requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)83  requires hx : x ∈ simplexProduct(n, m, blk)84  requires hp : p ∈ m85  shows realPartialSum(maskedPoint(n, blockSet(n, blk, p), deviationTerms(n, V, x, expectedPayoff(n, blk, V, p)(x))), n) = (0:R)86proof87  have xCube := simplexProduct.cube with hx88  have xFunction := unitCube.point with xCube89  have functions := payoffFamily.functions with family90  have pFunction := assembledPoint.function with functions, xCube91  have maskedP := maskedPoint.sequence at n, blockSet(n, blk, p), assembledPoint(n, payoffFamily(n, V), x) with pFunction92  have sumReal := realPartialSum.real with maskedP93  have payoffReal := expectedPayoff.real at n, blk, V, p, x with family, xCube94  have identity := deviationTerms.sum at n, blockSet(n, blk, p), V, x, expectedPayoff(n, blk, V, p)(x) with family, xCube95  have payoffValue := expectedPayoff.value at n, blk, V, p, x with family, xCube96  have sumOne := simplexProduct.block_sum with hx, hp97  have blockValue := blockSum.definition at n, blk, p98  have cubeValue := sumCube.value at n, blockSet(n, blk, p), x with xCube99  rw blockValue at cubeValue100  rw cubeValue at sumOne101  have one := realMulValue.one_right at expectedPayoff(n, blk, V, p)(x)102  rw [identity, sumOne, one, payoffValue]103  linarith104105-- At a fixed point of Nash's map, every gain is the coordinate times the106-- block's total gain.107theorem nashMap.fixed_gain (n : Nat) (blk V x i : Set)108  requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)109  requires hx : x ∈ unitCube(n)110  requires fixed : nashMap(n, blk, V)(x) = x111  requires hi : i ∈ n112  shows gain(n, blk, V, i)(x) = (x(i):R) * (totalGain(n, blk, V, blk(i))(x):R)113proof114  have coordinate := nashMap.coordinate at n, blk, V, x, i with family, hx, hi115  rw fixed at coordinate116  have xi := unitCube.coordinate_real with hx, hi117  have gainReal := gain.real at n, blk, V, i, x with family, hi, hx118  have scaleReal := denominator.real at n, blk, V, blk(i), x with family, hx119  have totalReal := totalGain.real at n, blk, V, blk(i), x with family, hx120  have scaleValue := denominator.value at n, blk, V, blk(i), x with family, hx121  have scaleAtLeastOne := denominator.at_least_one at n, blk, V, blk(i), x with family, hx122  have scaleNonzero : (denominator(n, blk, V, blk(i))(x):R) ≠ (0:R)123    intro zero124    rw zero at scaleAtLeastOne125    linarith126  have cancel := realInvValue.mul_right with scaleNonzero127  have key : ((x(i):R) + (gain(n, blk, V, i)(x):R)) * realInvValue((denominator(n, blk, V, blk(i))(x):R)) * (denominator(n, blk, V, blk(i))(x):R) = (x(i):R) + (gain(n, blk, V, i)(x):R)128    have rearrange : ((x(i):R) + (gain(n, blk, V, i)(x):R)) * realInvValue((denominator(n, blk, V, blk(i))(x):R)) * (denominator(n, blk, V, blk(i))(x):R) = ((x(i):R) + (gain(n, blk, V, i)(x):R)) * (realInvValue((denominator(n, blk, V, blk(i))(x):R)) * (denominator(n, blk, V, blk(i))(x):R))129      ring130    have commute := realMulValue.commutative at realInvValue(denominator(n, blk, V, blk(i))(x)), denominator(n, blk, V, blk(i))(x)131    have one := realMulValue.one_right at (x(i):R) + (gain(n, blk, V, i)(x):R)132    rwa [rearrange, commute, cancel]133  symm at coordinate134  rw [coordinate, scaleValue] at key135  have expand : (x(i):R) * ((1:R) + (totalGain(n, blk, V, blk(i))(x):R)) = (x(i):R) + (x(i):R) * (totalGain(n, blk, V, blk(i))(x):R)136    ring137  rw expand at key138  linarith139140-- Every block of a point of the product has a coordinate of positive mass.141theorem simplexProduct.positive_coordinate (n : Nat) (m blk x p : Set)142  requires hx : x ∈ simplexProduct(n, m, blk)143  requires hp : p ∈ m144  shows ∃ j ∈ n, j ∈ blockSet(n, blk, p) ∧ (0:R) < (x(j):R)145proof146  have xCube := simplexProduct.cube with hx147  have xFunction := unitCube.point with xCube148  have sumOne := simplexProduct.block_sum with hx, hp149  have blockValue := blockSum.definition at n, blk, p150  have cubeValue := sumCube.value at n, blockSet(n, blk, p), x with xCube151  rw blockValue at cubeValue152  rw cubeValue at sumOne153  have sequence := maskedPoint.sequence at n, blockSet(n, blk, p), x with xFunction154  by_contra none155  have terms : ∀ k ∈ n, maskedPoint(n, blockSet(n, blk, p), x)(k) = (0:R)156    intros k hk157    have alternatives : k ∈ blockSet(n, blk, p) ∨ ¬k ∈ blockSet(n, blk, p) by tauto158    cases alternatives with inBlock | outside159    . have same := maskedPoint.on_block with xFunction, hk, inBlock160      have interval := unitCube.coordinate with xCube, hk161      obtain ⟨kReal, lower, upper⟩ := closedInterval.membership.forward with interval162      have notPos : ¬(0:R) < (x(k):R)163        intro pos164        apply none165        witness k166        exact ⟨hk, ⟨inBlock, pos⟩⟩167      have le := realLe.of_not_less with notPos168      have zero : x(k) = (0:R) by exact realLe.antisymmetric with le, lower169      rwa same170    . exact maskedPoint.off_block with xFunction, hk, outside171  have vanish := realPartialSum.zero_terms with sequence172  have zeroSum := vanish with terms173  rw zeroSum at sumOne174  apply realZero.ne_one175  exact sumOne176177-- At a fixed point no block has positive total gain: a positive total gain178-- would make every deviation term nonnegative and the one at a coordinate of179-- positive mass strictly positive, yet the deviation terms sum to zero.180theorem nash.total_gain_zero (n : Nat) (m blk V x p : Set)181  requires blkFunction : blk : n → m182  requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)183  requires hx : x ∈ simplexProduct(n, m, blk)184  requires fixed : nashMap(n, blk, V)(x) = x185  requires hp : p ∈ m186  shows totalGain(n, blk, V, p)(x) = (0:R)187proof188  have xCube := simplexProduct.cube with hx189  have totalReal := totalGain.real at n, blk, V, p, x with family, xCube190  have totalNonneg := totalGain.nonnegative at n, blk, V, p, x with family, xCube191  have alternatives : (0:R) < (totalGain(n, blk, V, p)(x):R) ∨ ¬(0:R) < (totalGain(n, blk, V, p)(x):R) by tauto192  cases alternatives with positive | notPositive193  . exfalso194    have payoffReal := expectedPayoff.real at n, blk, V, p, x with family, xCube195    have dFunction := deviationTerms.function at n, V, x, expectedPayoff(n, blk, V, p)(x) with *196    have sequence := maskedPoint.sequence at n, blockSet(n, blk, p), deviationTerms(n, V, x, expectedPayoff(n, blk, V, p)(x)) with dFunction197    have sumZero := deviationTerms.sum_zero with family, hx, hp198    have termSign : ∀ j ∈ n, j ∈ blockSet(n, blk, p) → (0:R) ≤ (deviationTerms(n, V, x, expectedPayoff(n, blk, V, p)(x))(j):R) ∧ ((0:R) < (x(j):R) → (0:R) < (deviationTerms(n, V, x, expectedPayoff(n, blk, V, p)(x))(j):R))199      intros j hj inBlock200      have parts := blockSet.membership.forward with inBlock201      have block := parts.right202      have gainEq := nashMap.fixed_gain with family, xCube, fixed, hj203      rw block at gainEq204      have gainValue := gain.value at n, blk, V, j, x with family, hj, xCube205      rw block at gainValue206      have dValue := deviationTerms.value at n, V, x, expectedPayoff(n, blk, V, p)(x), j with *207      have dReal := FunctionBetween.apply_closed with dFunction, hj208      have xInterval := unitCube.coordinate with xCube, hj209      obtain ⟨xReal, xLower, xUpper⟩ := closedInterval.membership.forward with xInterval210      have vReal := CubeFunction.value with (CubeFunctionContinuous.function with (family with hj)), xCube211      have positiveCase : (0:R) < (x(j):R) → (0:R) < (deviationTerms(n, V, x, expectedPayoff(n, blk, V, p)(x))(j):R)212        intro xPos213        have gainPos : (0:R) < (gain(n, blk, V, j)(x):R)214          rw gainEq215          exact realMulValue.positive with xPos, positive216        rw gainValue at gainPos217        have differencePos : (0:R) < (V(j)(x):R) + -(expectedPayoff(n, blk, V, p)(x):R)218          have dAlternatives : (0:R) < (V(j)(x):R) + -(expectedPayoff(n, blk, V, p)(x):R) ∨ ¬(0:R) < (V(j)(x):R) + -(expectedPayoff(n, blk, V, p)(x):R) by tauto219          cases dAlternatives with dPos | dNotPos220          . exact dPos221          . have le := realLe.of_not_less with dNotPos222            have zero := realMax.of_le with le223            rw zero at gainPos224            exfalso225            linarith226        rw dValue227        exact realMulValue.positive with xPos, differencePos228      constructor229      . have xAlternatives : (0:R) < (x(j):R) ∨ ¬(0:R) < (x(j):R) by tauto230        cases xAlternatives with xPos | xNotPos231        . exact realLess.implies_le with (positiveCase with xPos)232        . have xLe := realLe.of_not_less with xNotPos233          have xZero : x(j) = (0:R) by exact realLe.antisymmetric with xLe, xLower234          have zero := realMulValue.zero_left at (V(j)(x):R) + -(expectedPayoff(n, blk, V, p)(x):R)235          rw [dValue, xZero, zero]236          exact realLe.reflexive237      . exact positiveCase238    obtain ⟨j, hj, inBlock, xPos⟩ := simplexProduct.positive_coordinate with hx, hp239    have signs := termSign with hj, inBlock240    have termPos := signs.right with xPos241    have nonnegative : ∀ k ∈ n, (0:R) ≤ (maskedPoint(n, blockSet(n, blk, p), deviationTerms(n, V, x, expectedPayoff(n, blk, V, p)(x)))(k):R)242      intros k hk243      have kAlternatives : k ∈ blockSet(n, blk, p) ∨ ¬k ∈ blockSet(n, blk, p) by tauto244      cases kAlternatives with kIn | kOut245      . have same := maskedPoint.on_block with dFunction, hk, kIn246        have kSigns := termSign with hk, kIn247        rw same248        exact kSigns.left249      . have same := maskedPoint.off_block with dFunction, hk, kOut250        rw same251        exact realLe.reflexive252    have bounds := realPartialSum.term_le_prefix with sequence253    have forAll := bounds with nonnegative254    have bound := forAll with hj255    have same := maskedPoint.on_block with dFunction, hj, inBlock256    rw [same, sumZero] at bound257    have termReal := FunctionBetween.apply_closed with dFunction, hj258    linarith259  . have le := realLe.of_not_less with notPositive260    exact realLe.antisymmetric with le, totalNonneg261262-- At a fixed point no pure strategy beats its owner's expected payoff.263theorem nash.no_gain (n : Nat) (m blk V x i : Set)264  requires blkFunction : blk : n → m265  requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)266  requires hx : x ∈ simplexProduct(n, m, blk)267  requires fixed : nashMap(n, blk, V)(x) = x268  requires hi : i ∈ n269  shows (V(i)(x):R) ≤ (expectedPayoff(n, blk, V, blk(i))(x):R)270proof271  have xCube := simplexProduct.cube with hx272  have block := FunctionBetween.apply_closed with blkFunction, hi273  have total := nash.total_gain_zero with blkFunction, family, hx, fixed, block274  have gainEq := nashMap.fixed_gain with family, xCube, fixed, hi275  rw total at gainEq276  have xi := unitCube.coordinate_real with xCube, hi277  have zero := realMulValue.zero_right at x(i)278  rw zero at gainEq279  have bound := gain.ge_difference at n, blk, V, i, x with family, hi, xCube280  rw gainEq at bound281  have vReal := CubeFunction.value with (CubeFunctionContinuous.function with (family with hi)), xCube282  have payoffReal := expectedPayoff.real at n, blk, V, blk(i), x with family, xCube283  linarith284285-- Nash's theorem.286theorem nash.equilibrium (n : Nat) (m blk V a : Set)287  requires blkFunction : blk : n → m288  requires ha : a ∈ simplexProduct(n, m, blk)289  requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)290  shows ∃ x ∈ simplexProduct(n, m, blk), ∀ i ∈ n, (V(i)(x):R) ≤ (expectedPayoff(n, blk, V, blk(i))(x):R)291proof292  have continuous := nashMap.continuous at n, blk, V with family293  have preserves := nashMap.preserves with blkFunction, family294  obtain ⟨x, hx, fixed⟩ := brouwer.simplexProduct_of_cube with blkFunction, ha, continuous, preserves295  witness x296  constructor297  . exact hx298  . intros i hi299    exact nash.no_gain with blkFunction, family, hx, fixed, hi300