Grace/Cumulus/GameTheory/NashDeviation.g17

Open in Workbench Download source

Imports

NashEquilibrium

Declarations

Source

1-- Equilibria as a predicate, and the deviation reading of Nash's condition:2-- when the payoffs of a player's pure strategies do not depend on that3-- player's own mixture, no change of their mixture improves their expected4-- payoff at an 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.NashDeviation11import NashEquilibrium1213-- A profile in the product where no pure strategy beats its owner's14-- expected payoff.15predicate Equilibrium (n m blk V x : Set) :=16  x ∈ simplexProduct(n, m, blk) ∧ ∀ i ∈ n, (V(i)(x):R) ≤ (expectedPayoff(n, blk, V, blk(i))(x):R)1718theorem Equilibrium.profile (n m blk V x : Set)19  requires equilibrium : Equilibrium(n, m, blk, V, x)20  shows x ∈ simplexProduct(n, m, blk)21proof22  exact equilibrium.left2324theorem Equilibrium.pure (n m blk V x i : Set)25  requires equilibrium : Equilibrium(n, m, blk, V, x)26  requires hi : i ∈ n27  shows (V(i)(x):R) ≤ (expectedPayoff(n, blk, V, blk(i))(x):R)28proof29  exact equilibrium.right with hi3031theorem nash.exists_equilibrium (n : Nat) (m blk V a : Set)32  requires blkFunction : blk : n → m33  requires ha : a ∈ simplexProduct(n, m, blk)34  requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)35  shows ∃ x, Equilibrium(n, m, blk, V, x)36proof37  obtain ⟨x, hx, pure⟩ := nash.equilibrium with blkFunction, ha, family38  witness x39  exact ⟨hx, pure⟩4041-- If z agrees with the equilibrium x except on player p's block, and the42-- payoffs of p's pure strategies are the same at z and at x, then p's43-- expected payoff at z is at most their expected payoff at x.44theorem nash.no_deviation (n : Nat) (m blk V x z p : Set)45  requires blkFunction : blk : n → m46  requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)47  requires equilibrium : Equilibrium(n, m, blk, V, x)48  requires hz : z ∈ simplexProduct(n, m, blk)49  requires hp : p ∈ m50  requires independent : ∀ i ∈ n, blk(i) = p → V(i)(z) = V(i)(x)51  shows (expectedPayoff(n, blk, V, p)(z):R) ≤ (expectedPayoff(n, blk, V, p)(x):R)52proof53  have hx := Equilibrium.profile with equilibrium54  have xCube := simplexProduct.cube with hx55  have zCube := simplexProduct.cube with hz56  have zFunction := unitCube.point with zCube57  have functions := payoffFamily.functions with family58  have payoffs := assembledPoint.function with functions, zCube59  have maskedP := maskedPoint.sequence at n, blockSet(n, blk, p), assembledPoint(n, payoffFamily(n, V), z) with payoffs60  have maskedZ := maskedPoint.sequence at n, blockSet(n, blk, p), z with zFunction61  have payoffReal := expectedPayoff.real at n, blk, V, p, x with family, xCube62  have constantU := constantSequence.sequence at expectedPayoff(n, blk, V, p)(x)63  have scaledZ := mulSequence.sequence with constantU, maskedZ64  have bounded : ∀ k ∈ ℕ, k < n → (maskedPoint(n, blockSet(n, blk, p), assembledPoint(n, payoffFamily(n, V), z))(k):R) ≤ (mulSequence(constantSequence(expectedPayoff(n, blk, V, p)(x)), maskedPoint(n, blockSet(n, blk, p), z))(k):R)65    intros k hk hkn66    have kNat : Nat(k) by typecheck67    have hkIn : k ∈ n by exact membership.of_Less with hkn68    have zReal := RealSequence.value at maskedPoint(n, blockSet(n, blk, p), z), k with maskedZ69    have uReal := RealSequence.value at constantSequence(expectedPayoff(n, blk, V, p)(x)), k with constantU70    have uValue := constantSequence.value at expectedPayoff(n, blk, V, p)(x), k71    have scaledValue := mulSequence.value with constantU, maskedZ, uReal, zReal72    rw [scaledValue, uValue]73    have alternatives : k ∈ blockSet(n, blk, p) ∨ ¬k ∈ blockSet(n, blk, p) by tauto74    cases alternatives with inBlock | outside75    . have parts := blockSet.membership.forward with inBlock76      have block := parts.right77      have pSame := maskedPoint.on_block with payoffs, hkIn, inBlock78      have zSame := maskedPoint.on_block with zFunction, hkIn, inBlock79      have pValue := assembledPoint.value with functions, zCube, hkIn80      have term := payoffFamily.term with family, zCube, hkIn81      have same := independent with hkIn, block82      have pure := Equilibrium.pure with equilibrium, hkIn83      rw block at pure84      have zInterval := unitCube.coordinate with zCube, hkIn85      obtain ⟨zkReal, zLower, zUpper⟩ := closedInterval.membership.forward with zInterval86      have vReal := CubeFunction.value with (CubeFunctionContinuous.function with (family with hkIn)), xCube87      have step := realLe.mul_left_of_nonnegative with pure, zLower88      have commute := realMulValue.commutative at z(k), expectedPayoff(n, blk, V, p)(x)89      rw commute at step90      rwa [pSame, zSame, pValue, term, same]91    . have pSame := maskedPoint.off_block with payoffs, hkIn, outside92      have zSame := maskedPoint.off_block with zFunction, hkIn, outside93      have zero := realMulValue.zero_right at expectedPayoff(n, blk, V, p)(x)94      rw [pSame, zSame, zero]95      exact realLe.reflexive96  have monotone := realPartialSum.monotone_prefix with maskedP, scaledZ, bounded97  have scale := realPartialSum.scale at maskedPoint(n, blockSet(n, blk, p), z), n, expectedPayoff(n, blk, V, p)(x) with maskedZ98  have zValue := expectedPayoff.value at n, blk, V, p, z with family, zCube99  have sumOne := simplexProduct.block_sum with hz, hp100  have blockValue := blockSum.definition at n, blk, p101  have cubeValue := sumCube.value at n, blockSet(n, blk, p), z with zCube102  rw blockValue at cubeValue103  rw cubeValue at sumOne104  have one := realMulValue.one_right at expectedPayoff(n, blk, V, p)(x)105  rw [scale, sumOne, one] at monotone106  rwa zValue107