Grace/Cumulus/GameTheory/NashMap.g17

Open in Workbench Download source

Imports

FixedPoint.WeightedSums · FixedPoint.BlockSimplex

Declarations

Source

1-- Nash's map on mixed strategy profiles: each player's expected payoff is the2-- block sum of x(i)·V(i)(x) over their pure strategies, the gain of a pure3-- strategy is the positive part of its payoff above the expected payoff, and4-- every coordinate is shifted by its gain and renormalised by the block's5-- total gain, giving a continuous self-map of the product of simplices6-- 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.NashMap12import FixedPoint.WeightedSums13import FixedPoint.BlockSimplex1415-- The payoff terms x(i)·V(i)(x), as a family of cube functions.16defgraph payoffFamily (n V : Set) (i ∈ n) : functionSpace(unitCube(n), ℝ) := mulCube(n, coordinateCube(n, i), V(i))17requires nNat : Nat(n)18requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)19proof20  have coordinate := coordinateCube.continuous at n, i with member21  have continuous := mulCube.continuous with coordinate, (family with member)22  have function := CubeFunctionContinuous.function with continuous23  have between : mulCube(n, coordinateCube(n, i), V(i)) : unitCube(n) → ℝ24    exact CubeFunction.function with function25  exact functionSpace.mem_iff.backward with between2627theorem payoffFamily.continuous (n : Nat) (V : Set)28  requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)29  shows ∀ i ∈ n, CubeFunctionContinuous(payoffFamily(n, V)(i), n)30proof31  intros i hi32  have same := payoffFamily.value at n, V, i with *33  have coordinate := coordinateCube.continuous with hi34  rw same35  exact mulCube.continuous with coordinate, (family with hi)3637theorem payoffFamily.functions (n : Nat) (V : Set)38  requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)39  shows ∀ i ∈ n, CubeFunction(payoffFamily(n, V)(i), n)40proof41  intros i hi42  have continuous := payoffFamily.continuous with family43  exact CubeFunctionContinuous.function with (continuous with hi)4445theorem payoffFamily.term (n : Nat) (V x i : Set)46  requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)47  requires hx : x ∈ unitCube(n)48  requires hi : i ∈ n49  shows payoffFamily(n, V)(i)(x) = (x(i):R) * (V(i)(x):R)50proof51  have same := payoffFamily.value at n, V, i with *52  have coordinate := coordinateCube.continuous with hi53  have coordinateFunction := CubeFunctionContinuous.function with coordinate54  have componentFunction := CubeFunctionContinuous.function with (family with hi)55  have product := mulCube.value with coordinateFunction, componentFunction, hx56  have coordinateValue := coordinateCube.value with hi, hx57  rw [same, product, coordinateValue]58  rfl5960-- The expected payoff of the player who owns block p.61def expectedPayoff (n blk V p : Set) : Set := weightedSum(n, blockSet(n, blk, p), payoffFamily(n, V))6263theorem expectedPayoff.definition (n blk V p : Set)64  shows expectedPayoff(n, blk, V, p) = weightedSum(n, blockSet(n, blk, p), payoffFamily(n, V))65proof66  unfold expectedPayoff67  rfl6869theorem expectedPayoff.continuous (n : Nat) (blk V p : Set)70  requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)71  shows CubeFunctionContinuous(expectedPayoff(n, blk, V, p), n)72proof73  have terms := payoffFamily.continuous with family74  have same := expectedPayoff.definition at n, blk, V, p75  rw same76  exact weightedSum.continuous with terms7778theorem expectedPayoff.function (n : Nat) (blk V p : Set)79  requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)80  shows CubeFunction(expectedPayoff(n, blk, V, p), n)81proof82  exact CubeFunctionContinuous.function with (expectedPayoff.continuous at n, blk, V, p with family)8384theorem expectedPayoff.real (n : Nat) (blk V p x : Set)85  requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)86  requires hx : x ∈ unitCube(n)87  shows expectedPayoff(n, blk, V, p)(x) ∈ ℝ88proof89  exact CubeFunction.value with (expectedPayoff.function at n, blk, V, p with family), hx9091theorem expectedPayoff.value (n : Nat) (blk V p x : Set)92  requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)93  requires hx : x ∈ unitCube(n)94  shows expectedPayoff(n, blk, V, p)(x) = realPartialSum(maskedPoint(n, blockSet(n, blk, p), assembledPoint(n, payoffFamily(n, V), x)), n)95proof96  have functions := payoffFamily.functions with family97  have same := expectedPayoff.definition at n, blk, V, p98  rw same99  exact weightedSum.value with functions, hx100101-- The gain of pure strategy i: its payoff above the owner's expected payoff,102-- or zero.103def gain (n blk V i : Set) : Set :=104  maxCube(n, constantFunction(unitCube(n), ℝ, (0:R)), addCube(n, V(i), negCube(n, expectedPayoff(n, blk, V, blk(i)))))105106theorem gain.definition (n blk V i : Set)107  shows gain(n, blk, V, i) = maxCube(n, constantFunction(unitCube(n), ℝ, (0:R)), addCube(n, V(i), negCube(n, expectedPayoff(n, blk, V, blk(i)))))108proof109  unfold gain110  rfl111112theorem gain.continuous (n : Nat) (blk V i : Set)113  requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)114  requires hi : i ∈ n115  shows CubeFunctionContinuous(gain(n, blk, V, i), n)116proof117  have zeroIn : (0:R) ∈ ℝ by typecheck118  have zero := constantCube.continuous with zeroIn119  have payoff := expectedPayoff.continuous at n, blk, V, blk(i) with family120  have negative := negCube.continuous with payoff121  have difference := addCube.continuous with (family with hi), negative122  have same := gain.definition at n, blk, V, i123  rw same124  exact maxCube.continuous with zero, difference125126theorem gain.function (n : Nat) (blk V i : Set)127  requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)128  requires hi : i ∈ n129  shows CubeFunction(gain(n, blk, V, i), n)130proof131  exact CubeFunctionContinuous.function with (gain.continuous at n, blk, V, i with family, hi)132133theorem gain.real (n : Nat) (blk V i x : Set)134  requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)135  requires hi : i ∈ n136  requires hx : x ∈ unitCube(n)137  shows gain(n, blk, V, i)(x) ∈ ℝ138proof139  exact CubeFunction.value with (gain.function at n, blk, V, i with family, hi), hx140141theorem gain.value (n : Nat) (blk V i x : Set)142  requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)143  requires hi : i ∈ n144  requires hx : x ∈ unitCube(n)145  shows gain(n, blk, V, i)(x) = realMax((0:R), (V(i)(x):R) + -(expectedPayoff(n, blk, V, blk(i))(x):R))146proof147  have zeroIn : (0:R) ∈ ℝ by typecheck148  have zero := constantCube.continuous with zeroIn149  have payoff := expectedPayoff.continuous at n, blk, V, blk(i) with family150  have negative := negCube.continuous with payoff151  have difference := addCube.continuous with (family with hi), negative152  have zeroFunction := CubeFunctionContinuous.function with zero153  have componentFunction := CubeFunctionContinuous.function with (family with hi)154  have payoffFunction := CubeFunctionContinuous.function with payoff155  have negativeFunction := CubeFunctionContinuous.function with negative156  have differenceFunction := CubeFunctionContinuous.function with difference157  have same := gain.definition at n, blk, V, i158  have maxValue := maxCube.value with zeroFunction, differenceFunction, hx159  have zeroValue := constantFunction.apply at unitCube(n), ℝ, x, (0:R) with hx160  have differenceValue := addCube.value with componentFunction, negativeFunction, hx161  have negativeValue := negCube.value with payoffFunction, hx162  rw [same, maxValue, zeroValue, differenceValue, negativeValue]163  rfl164165theorem gain.nonnegative (n : Nat) (blk V i x : Set)166  requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)167  requires hi : i ∈ n168  requires hx : x ∈ unitCube(n)169  shows (0:R) ≤ (gain(n, blk, V, i)(x):R)170proof171  have value := gain.value at n, blk, V, i, x with family, hi, hx172  have componentReal := CubeFunction.value with (CubeFunctionContinuous.function with (family with hi)), hx173  have payoffReal := expectedPayoff.real at n, blk, V, blk(i), x with family, hx174  rw value175  exact realMax.ge_left176177theorem gain.ge_difference (n : Nat) (blk V i x : Set)178  requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)179  requires hi : i ∈ n180  requires hx : x ∈ unitCube(n)181  shows (V(i)(x):R) + -(expectedPayoff(n, blk, V, blk(i))(x):R) ≤ (gain(n, blk, V, i)(x):R)182proof183  have value := gain.value at n, blk, V, i, x with family, hi, hx184  have componentReal := CubeFunction.value with (CubeFunctionContinuous.function with (family with hi)), hx185  have payoffReal := expectedPayoff.real at n, blk, V, blk(i), x with family, hx186  rw value187  exact realMax.ge_right188189-- The gains as a family, and each block's total gain.190defgraph gainFamily (n blk V : Set) (i ∈ n) : functionSpace(unitCube(n), ℝ) := gain(n, blk, V, i)191requires nNat : Nat(n)192requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)193proof194  have function := gain.function at n, blk, V, i with family, member195  have between : gain(n, blk, V, i) : unitCube(n) → ℝ by exact CubeFunction.function with function196  exact functionSpace.mem_iff.backward with between197198theorem gainFamily.term (n : Nat) (blk V i : Set)199  requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)200  requires hi : i ∈ n201  shows gainFamily(n, blk, V)(i) = gain(n, blk, V, i)202proof203  exact gainFamily.value at n, blk, V, i with *204205theorem gainFamily.continuous (n : Nat) (blk V : Set)206  requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)207  shows ∀ i ∈ n, CubeFunctionContinuous(gainFamily(n, blk, V)(i), n)208proof209  intros i hi210  have same := gainFamily.term at n, blk, V, i with family, hi211  rw same212  exact gain.continuous with family, hi213214theorem gainFamily.functions (n : Nat) (blk V : Set)215  requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)216  shows ∀ i ∈ n, CubeFunction(gainFamily(n, blk, V)(i), n)217proof218  intros i hi219  have continuous := gainFamily.continuous at n, blk, V with family220  exact CubeFunctionContinuous.function with (continuous with hi)221222theorem gainFamily.nonnegative (n : Nat) (blk V x : Set)223  requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)224  requires hx : x ∈ unitCube(n)225  shows ∀ i ∈ n, (0:R) ≤ (gainFamily(n, blk, V)(i)(x):R)226proof227  intros i hi228  have same := gainFamily.term at n, blk, V, i with family, hi229  rw same230  exact gain.nonnegative with family, hi, hx231232def totalGain (n blk V p : Set) : Set := weightedSum(n, blockSet(n, blk, p), gainFamily(n, blk, V))233234theorem totalGain.definition (n blk V p : Set)235  shows totalGain(n, blk, V, p) = weightedSum(n, blockSet(n, blk, p), gainFamily(n, blk, V))236proof237  unfold totalGain238  rfl239240theorem totalGain.continuous (n : Nat) (blk V p : Set)241  requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)242  shows CubeFunctionContinuous(totalGain(n, blk, V, p), n)243proof244  have terms := gainFamily.continuous at n, blk, V with family245  have same := totalGain.definition at n, blk, V, p246  rw same247  exact weightedSum.continuous with terms248249theorem totalGain.function (n : Nat) (blk V p : Set)250  requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)251  shows CubeFunction(totalGain(n, blk, V, p), n)252proof253  exact CubeFunctionContinuous.function with (totalGain.continuous at n, blk, V, p with family)254255theorem totalGain.real (n : Nat) (blk V p x : Set)256  requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)257  requires hx : x ∈ unitCube(n)258  shows totalGain(n, blk, V, p)(x) ∈ ℝ259proof260  exact CubeFunction.value with (totalGain.function at n, blk, V, p with family), hx261262theorem totalGain.value (n : Nat) (blk V p x : Set)263  requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)264  requires hx : x ∈ unitCube(n)265  shows totalGain(n, blk, V, p)(x) = realPartialSum(maskedPoint(n, blockSet(n, blk, p), assembledPoint(n, gainFamily(n, blk, V), x)), n)266proof267  have functions := gainFamily.functions at n, blk, V with family268  have same := totalGain.definition at n, blk, V, p269  rw same270  exact weightedSum.value with functions, hx271272theorem totalGain.nonnegative (n : Nat) (blk V p x : Set)273  requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)274  requires hx : x ∈ unitCube(n)275  shows (0:R) ≤ (totalGain(n, blk, V, p)(x):R)276proof277  have functions := gainFamily.functions at n, blk, V with family278  have nonnegative := gainFamily.nonnegative at n, blk, V, x with family, hx279  have same := totalGain.definition at n, blk, V, p280  rw same281  exact weightedSum.nonnegative with functions, hx, nonnegative282283theorem totalGain.ge_gain (n : Nat) (blk V x i : Set)284  requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)285  requires hx : x ∈ unitCube(n)286  requires hi : i ∈ n287  shows (gain(n, blk, V, i)(x):R) ≤ (totalGain(n, blk, V, blk(i))(x):R)288proof289  have functions := gainFamily.functions at n, blk, V with family290  have nonnegative := gainFamily.nonnegative at n, blk, V, x with family, hx291  have inBlock := blockSet.own at n, blk, i with hi292  have same := totalGain.definition at n, blk, V, blk(i)293  have term := gainFamily.term at n, blk, V, i with family, hi294  have bound := weightedSum.ge_term with functions, hx, nonnegative, hi, inBlock295  rw term at bound296  rwa same297298-- One plus the total gain, the renormalising denominator of a block.299def denominator (n blk V p : Set) : Set := addCube(n, constantFunction(unitCube(n), ℝ, (1:R)), totalGain(n, blk, V, p))300301theorem denominator.definition (n blk V p : Set)302  shows denominator(n, blk, V, p) = addCube(n, constantFunction(unitCube(n), ℝ, (1:R)), totalGain(n, blk, V, p))303proof304  unfold denominator305  rfl306307theorem denominator.continuous (n : Nat) (blk V p : Set)308  requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)309  shows CubeFunctionContinuous(denominator(n, blk, V, p), n)310proof311  have oneIn : (1:R) ∈ ℝ by typecheck312  have one := constantCube.continuous with oneIn313  have total := totalGain.continuous at n, blk, V, p with family314  have same := denominator.definition at n, blk, V, p315  rw same316  exact addCube.continuous with one, total317318theorem denominator.value (n : Nat) (blk V p x : Set)319  requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)320  requires hx : x ∈ unitCube(n)321  shows denominator(n, blk, V, p)(x) = (1:R) + (totalGain(n, blk, V, p)(x):R)322proof323  have oneIn : (1:R) ∈ ℝ by typecheck324  have one := constantCube.continuous with oneIn325  have oneFunction := CubeFunctionContinuous.function with one326  have totalFunction := totalGain.function at n, blk, V, p with family327  have same := denominator.definition at n, blk, V, p328  have sum := addCube.value with oneFunction, totalFunction, hx329  have oneValue := constantFunction.apply at unitCube(n), ℝ, x, (1:R) with hx330  rw [same, sum, oneValue]331  rfl332333theorem denominator.real (n : Nat) (blk V p x : Set)334  requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)335  requires hx : x ∈ unitCube(n)336  shows denominator(n, blk, V, p)(x) ∈ ℝ337proof338  exact CubeFunction.value with (CubeFunctionContinuous.function with (denominator.continuous at n, blk, V, p with family)), hx339340theorem denominator.at_least_one (n : Nat) (blk V p x : Set)341  requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)342  requires hx : x ∈ unitCube(n)343  shows (1:R) ≤ (denominator(n, blk, V, p)(x):R)344proof345  have value := denominator.value at n, blk, V, p, x with family, hx346  have total := totalGain.nonnegative at n, blk, V, p, x with family, hx347  have totalReal := totalGain.real at n, blk, V, p, x with family, hx348  rw value349  linarith350351-- Coordinate i of Nash's map.352def nashCoordinate (n blk V i : Set) : Set :=353  mulCube(n, addCube(n, coordinateCube(n, i), gain(n, blk, V, i)), invCube(n, denominator(n, blk, V, blk(i))))354355theorem nashCoordinate.definition (n blk V i : Set)356  shows nashCoordinate(n, blk, V, i) = mulCube(n, addCube(n, coordinateCube(n, i), gain(n, blk, V, i)), invCube(n, denominator(n, blk, V, blk(i))))357proof358  unfold nashCoordinate359  rfl360361theorem nashCoordinate.continuous (n : Nat) (blk V i : Set)362  requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)363  requires hi : i ∈ n364  shows CubeFunctionContinuous(nashCoordinate(n, blk, V, i), n)365proof366  have coordinate := coordinateCube.continuous with hi367  have gainContinuous := gain.continuous at n, blk, V, i with family, hi368  have numerator := addCube.continuous with coordinate, gainContinuous369  have scale := denominator.continuous at n, blk, V, blk(i) with family370  have atLeastOne : ∀ x ∈ unitCube(n), (1:R) ≤ (denominator(n, blk, V, blk(i))(x):R)371    intros x hx372    exact denominator.at_least_one with family, hx373  have inverse := invCube.continuous with scale, atLeastOne374  have same := nashCoordinate.definition at n, blk, V, i375  rw same376  exact mulCube.continuous with numerator, inverse377378theorem nashCoordinate.value (n : Nat) (blk V i x : Set)379  requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)380  requires hi : i ∈ n381  requires hx : x ∈ unitCube(n)382  shows nashCoordinate(n, blk, V, i)(x) = ((x(i):R) + (gain(n, blk, V, i)(x):R)) * realInvValue((denominator(n, blk, V, blk(i))(x):R))383proof384  have coordinate := coordinateCube.continuous with hi385  have gainContinuous := gain.continuous at n, blk, V, i with family, hi386  have numerator := addCube.continuous with coordinate, gainContinuous387  have scale := denominator.continuous at n, blk, V, blk(i) with family388  have atLeastOne : ∀ y ∈ unitCube(n), (1:R) ≤ (denominator(n, blk, V, blk(i))(y):R)389    intros y hy390    exact denominator.at_least_one with family, hy391  have inverse := invCube.continuous with scale, atLeastOne392  have coordinateFunction := CubeFunctionContinuous.function with coordinate393  have gainFunction := CubeFunctionContinuous.function with gainContinuous394  have numeratorFunction := CubeFunctionContinuous.function with numerator395  have scaleFunction := CubeFunctionContinuous.function with scale396  have inverseFunction := CubeFunctionContinuous.function with inverse397  have same := nashCoordinate.definition at n, blk, V, i398  have product := mulCube.value with numeratorFunction, inverseFunction, hx399  have sum := addCube.value with coordinateFunction, gainFunction, hx400  have coordinateValue := coordinateCube.value with hi, hx401  have inverseValue := invCube.value with scaleFunction, hx402  rw [same, product, sum, coordinateValue, inverseValue]403  rfl404405theorem nashCoordinate.bounds (n : Nat) (blk V i x : Set)406  requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)407  requires hi : i ∈ n408  requires hx : x ∈ unitCube(n)409  shows (0:R) ≤ (nashCoordinate(n, blk, V, i)(x):R) ∧ (nashCoordinate(n, blk, V, i)(x):R) ≤ (1:R)410proof411  have value := nashCoordinate.value at n, blk, V, i, x with family, hi, hx412  have xInterval := unitCube.coordinate with hx, hi413  obtain ⟨xReal, xLower, xUpper⟩ := closedInterval.membership.forward with xInterval414  have gainReal := gain.real at n, blk, V, i, x with family, hi, hx415  have gainNonneg := gain.nonnegative at n, blk, V, i, x with family, hi, hx416  have gainLe := totalGain.ge_gain at n, blk, V, x, i with family, hx, hi417  have totalReal := totalGain.real at n, blk, V, blk(i), x with family, hx418  have scaleReal := denominator.real at n, blk, V, blk(i), x with family, hx419  have scaleValue := denominator.value at n, blk, V, blk(i), x with family, hx420  have scaleAtLeastOne := denominator.at_least_one at n, blk, V, blk(i), x with family, hx421  obtain ⟨inversePositive, inverseLe⟩ := realInvValue.le_one with scaleAtLeastOne422  have inverseNonneg := realLess.implies_le with inversePositive423  have numeratorNonneg : (0:R) ≤ (x(i):R) + (gain(n, blk, V, i)(x):R) by linarith424  have scaleNonzero : (denominator(n, blk, V, blk(i))(x):R) ≠ (0:R)425    intro zero426    rw zero at scaleAtLeastOne427    linarith428  have cancel := realInvValue.mul_right with scaleNonzero429  have numeratorLe : (x(i):R) + (gain(n, blk, V, i)(x):R) ≤ (denominator(n, blk, V, blk(i))(x):R)430    rw scaleValue431    linarith432  have scaled := realLe.mul_right_of_nonnegative with numeratorLe, inverseNonneg433  rw cancel at scaled434  rw value435  constructor436  . exact realMulValue.nonnegative with numeratorNonneg, inverseNonneg437  . exact scaled438439-- The family of Nash coordinates and the assembled map.440defgraph nashFamily (n blk V : Set) (i ∈ n) : functionSpace(unitCube(n), ℝ) := nashCoordinate(n, blk, V, i)441requires nNat : Nat(n)442requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)443proof444  have continuous := nashCoordinate.continuous at n, blk, V, i with family, member445  have function := CubeFunctionContinuous.function with continuous446  have between : nashCoordinate(n, blk, V, i) : unitCube(n) → ℝ447    exact CubeFunction.function with function448  exact functionSpace.mem_iff.backward with between449450theorem nashFamily.coordinate (n : Nat) (blk V i : Set)451  requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)452  requires hi : i ∈ n453  shows nashFamily(n, blk, V)(i) = nashCoordinate(n, blk, V, i)454proof455  exact nashFamily.value at n, blk, V, i with *456457theorem nashFamily.continuous (n : Nat) (blk V : Set)458  requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)459  shows ∀ i ∈ n, CubeFunctionContinuous(nashFamily(n, blk, V)(i), n)460proof461  intros i hi462  have same := nashFamily.coordinate at n, blk, V, i with family, hi463  rw same464  exact nashCoordinate.continuous with family, hi465466theorem nashFamily.functions (n : Nat) (blk V : Set)467  requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)468  shows ∀ i ∈ n, CubeFunction(nashFamily(n, blk, V)(i), n)469proof470  intros i hi471  have continuous := nashFamily.continuous at n, blk, V with family472  exact CubeFunctionContinuous.function with (continuous with hi)473474theorem nashFamily.bounds (n : Nat) (blk V : Set)475  requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)476  shows ∀ i ∈ n, ∀ x ∈ unitCube(n), (0:R) ≤ (nashFamily(n, blk, V)(i)(x):R) ∧ (nashFamily(n, blk, V)(i)(x):R) ≤ (1:R)477proof478  intros i hi x hx479  have same := nashFamily.coordinate at n, blk, V, i with family, hi480  rw same481  exact nashCoordinate.bounds with family, hi, hx482483def nashMap (n blk V : Set) : Set := assembledMap(n, nashFamily(n, blk, V))484485theorem nashMap.definition (n blk V : Set)486  shows nashMap(n, blk, V) = assembledMap(n, nashFamily(n, blk, V))487proof488  unfold nashMap489  rfl490491theorem nashMap.continuous (n : Nat) (blk V : Set)492  requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)493  shows CubeContinuous(nashMap(n, blk, V), n)494proof495  have continuous := nashFamily.continuous at n, blk, V with family496  have bounds := nashFamily.bounds at n, blk, V with family497  have same := nashMap.definition at n, blk, V498  rw same499  exact assembledMap.continuous with continuous, bounds500501theorem nashMap.in_cube (n : Nat) (blk V x : Set)502  requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)503  requires hx : x ∈ unitCube(n)504  shows nashMap(n, blk, V)(x) ∈ unitCube(n)505proof506  have continuous := nashMap.continuous at n, blk, V with family507  have map := continuous.left508  have function := CubeMap.function with map509  exact FunctionBetween.apply_closed with function, hx510511theorem nashMap.coordinate (n : Nat) (blk V x i : Set)512  requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)513  requires hx : x ∈ unitCube(n)514  requires hi : i ∈ n515  shows nashMap(n, blk, V)(x)(i) = ((x(i):R) + (gain(n, blk, V, i)(x):R)) * realInvValue((denominator(n, blk, V, blk(i))(x):R))516proof517  have functions := nashFamily.functions at n, blk, V with family518  have bounds := nashFamily.bounds at n, blk, V with family519  have same := nashMap.definition at n, blk, V520  have assembled := assembledMap.coordinate with functions, bounds, hx, hi521  have coordinate := nashFamily.coordinate at n, blk, V, i with family, hi522  rw [same, assembled, coordinate]523  exact nashCoordinate.value with family, hi, hx524525-- Nash's map keeps every block sum equal to one.526theorem nashMap.block_sum (n : Nat) (m blk V x p : Set)527  requires blkFunction : blk : n → m528  requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)529  requires hx : x ∈ simplexProduct(n, m, blk)530  requires hp : p ∈ m531  shows blockSum(n, blk, p)(nashMap(n, blk, V)(x)) = (1:R)532proof533  have xCube := simplexProduct.cube with hx534  have sumOne := simplexProduct.block_sum with hx, hp535  have image := nashMap.in_cube at n, blk, V, x with family, xCube536  have functions := gainFamily.functions at n, blk, V with family537  have gains := assembledPoint.function with functions, xCube538  have shifted : ∀ j ∈ n, j ∈ blockSet(n, blk, p) → nashMap(n, blk, V)(x)(j) = ((x(j):R) + (assembledPoint(n, gainFamily(n, blk, V), x)(j):R)) * realInvValue((denominator(n, blk, V, p)(x):R))539    intros j hj inBlock540    have parts := blockSet.membership.forward with inBlock541    have block := parts.right542    have value := nashMap.coordinate at n, blk, V, x, j with family, xCube, hj543    have gainValue := assembledPoint.value with functions, xCube, hj544    have term := gainFamily.term at n, blk, V, j with family, hj545    rw block at value546    rwa [gainValue, term]547  have sumSame := blockSum.definition at n, blk, p548  have scaleReal := denominator.real at n, blk, V, p, x with family, xCube549  have inverseReal := realInvValue.real at denominator(n, blk, V, p)(x)550  have affine := sumCube.scaled_sum with xCube, image, gains, shifted551  rw sumSame at affine552  have totalValue := totalGain.value at n, blk, V, p, x with family, xCube553  have scaleValue := denominator.value at n, blk, V, p, x with family, xCube554  have scaleAtLeastOne := denominator.at_least_one at n, blk, V, p, x with family, xCube555  have scaleNonzero : (denominator(n, blk, V, p)(x):R) ≠ (0:R)556    intro zero557    rw zero at scaleAtLeastOne558    linarith559  have cancel := realInvValue.mul_right with scaleNonzero560  have numerator : (1:R) + (realPartialSum(maskedPoint(n, blockSet(n, blk, p), assembledPoint(n, gainFamily(n, blk, V), x)), n):R) = denominator(n, blk, V, p)(x)561    rw [scaleValue, totalValue]562    rfl563  rwa [affine, sumOne, numerator]564565theorem nashMap.preserves (n : Nat) (m blk V : Set)566  requires blkFunction : blk : n → m567  requires family : ∀ i ∈ n, CubeFunctionContinuous(V(i), n)568  shows ∀ x ∈ simplexProduct(n, m, blk), nashMap(n, blk, V)(x) ∈ simplexProduct(n, m, blk)569proof570  intros x hx571  have xCube := simplexProduct.cube with hx572  apply simplexProduct.membership.backward573  constructor574  . exact nashMap.in_cube with family, xCube575  . intros p hp576    exact nashMap.block_sum with blkFunction, family, hx, hp577