Grace/Cumulus/GameTheory/PureProfile.g17

Open in Workbench Download source

Imports

FixedPoint.BlockSimplex

Declarations

Source

1-- Pure strategy profiles: choosing one pure strategy per player gives a2-- point of the product of simplices, the anchor Nash's theorem needs3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.GameTheory.PureProfile9import FixedPoint.BlockSimplex1011-- The sequence that is one at r and zero elsewhere.12defgraph pointMass (r : Set) (i ∈ ℕ) : ℝ := (realNat(indicator({r}, i)):R)13proof14  have natural := indicator.natural at {r}, i15  exact realNat.real at indicator({r}, i)1617theorem pointMass.sequence (r : Set)18  shows RealSequence(pointMass(r))19proof20  exact pointMass.function at r2122theorem realPartialSum.pointMass_outside (r : Set) (m : Nat)23  shows ¬r ∈ m → realPartialSum(pointMass(r), m) = (0:R)24proof25  induction m26  | zero =>27    intro outside28    exact realPartialSum.zero at pointMass(r)29  | succ(j) using ih =>30    intro outside31    have jNat : Nat(j) by typecheck32    have jIn := nat.omega.forward with jNat33    have notInJ : ¬r ∈ j34      intro inJ35      apply outside36      apply bootstrap.succ.membership.backward37      left38      exact inJ39    have notEqual : r ≠ j40      intro equal41      apply outside42      rw equal43      exact bootstrap.succ.self at j44    have previous := ih with notInJ45    have massValue := pointMass.value at r, j46    have other := indicator.singleton_other at r, j with notEqual47    have step := realPartialSum.succ at pointMass(r), j48    have sequence := pointMass.sequence at r49    have termReal := RealSequence.value at pointMass(r), j with sequence50    have termZero : pointMass(r)(j) = (0:R)51      rw [massValue, other]52      exact realNat.zero53    rw step54    linarith5556theorem realPartialSum.pointMass_below (r : Set) (m : Nat)57  shows r ∈ m → realPartialSum(pointMass(r), m) = (1:R)58proof59  induction m60  | zero =>61    intro below62    exfalso63    rw nat.zero at below64    simpa using below65  | succ(j) using ih =>66    intro below67    have jNat : Nat(j) by typecheck68    have jIn := nat.omega.forward with jNat69    have massValue := pointMass.value at r, j70    have step := realPartialSum.succ at pointMass(r), j71    have sequence := pointMass.sequence at r72    have sumReal := realPartialSum.real at pointMass(r), j with sequence73    have termReal := RealSequence.value at pointMass(r), j with sequence74    have split := bootstrap.succ.membership.forward with below75    cases split with inJ | same76    . have previous := ih with inJ77      have notEqual : r ≠ j78        intro equal79        rw equal at inJ80        have irreflexive := membership.irreflexive at j81        exact irreflexive with inJ82      have other := indicator.singleton_other at r, j with notEqual83      have termZero : pointMass(r)(j) = (0:R)84        rw [massValue, other]85        exact realNat.zero86      rw step87      linarith88    . have notInJ : ¬r ∈ j89        intro inJ90        rw same at inJ91        have irreflexive := membership.irreflexive at j92        exact irreflexive with inJ93      have outside := realPartialSum.pointMass_outside at r, j94      have previous := outside with notInJ95      have termOne : pointMass(r)(j) = (1:R)96        rw [massValue, same]97        have self := indicator.singleton_self at j98        rw self99        exact realNat.one100      rw step101      linarith102103-- The profile that plays the strategies in R with probability one.104defgraph pureProfile (n R : Set) (i ∈ n) : ℝ := (realNat(indicator(R, i)):R)105requires nNat : Nat(n)106proof107  have natural := indicator.natural at R, i108  exact realNat.real at indicator(R, i)109110theorem pureProfile.in_cube (n : Nat) (R : Set)111  shows pureProfile(n, R) ∈ unitCube(n)112proof113  have function := pureProfile.function at n, R with *114  have zeroIn : (0:R) ∈ ℝ by typecheck115  have oneIn : (1:R) ∈ ℝ by typecheck116  apply unitCube.membership.backward117  constructor118  . exact functionSpace.mem_iff.backward with function119  . intros i hi120    have value := pureProfile.value at n, R, i with *121    apply closedInterval.membership.backward122    rw value123    have alternatives : i ∈ R ∨ ¬i ∈ R by tauto124    cases alternatives with inR | outside125    . have one := indicator.member with inR126      rw [one, realNat.one]127      have oneLe : (1:R) ≤ (1:R) by linarith128      have zeroLe : (0:R) ≤ (1:R) by linarith129      exact ⟨oneIn, ⟨zeroLe, oneLe⟩⟩130    . have zero := indicator.absent with outside131      rw [zero, realNat.zero]132      have zeroLe : (0:R) ≤ (0:R) by linarith133      have zeroLeOne : (0:R) ≤ (1:R) by linarith134      exact ⟨zeroIn, ⟨zeroLe, zeroLeOne⟩⟩135136-- With one representative strategy per player, the masked terms of a block137-- form the point mass at that player's representative.138theorem pureProfile.masked (n : Nat) (m blk rep p i : Set)139  requires blkFunction : blk : n → m140  requires repFunction : rep : m → n141  requires section : ∀ q ∈ m, blk(rep(q)) = q142  requires hp : p ∈ m143  requires hi : i ∈ n144  shows maskedPoint(n, blockSet(n, blk, p), pureProfile(n, functionImage(rep, m, n)))(i) = pointMass(rep(p))(i)145proof146  have aFunction := pureProfile.function at n, functionImage(rep, m, n) with *147  have iNat := natural.member at n with hi148  have iIn := nat.omega.forward with iNat149  have massValue := pointMass.value at rep(p), i150  have alternatives : i = rep(p) ∨ i ≠ rep(p) by tauto151  cases alternatives with same | different152  . have inBlock : i ∈ blockSet(n, blk, p)153      apply blockSet.membership.backward154      constructor155      . exact hi156      . rw same157        exact section with hp158    have onBlock := maskedPoint.on_block with aFunction, hi, inBlock159    have value := pureProfile.value at n, functionImage(rep, m, n), i with *160    have inImage : i ∈ functionImage(rep, m, n)161      apply functionImage.membership.backward162      constructor163      . exact hi164      . witness p165        exact ⟨hp, same⟩166    have one := indicator.member with inImage167    rw [onBlock, value, one, massValue, same]168    have self := indicator.singleton_self at rep(p)169    rw self170    rfl171  . have differentReversed : rep(p) ≠ i172      intro equal173      apply different174      rw equal175      rfl176    have other := indicator.singleton_other with differentReversed177    have massZero : pointMass(rep(p))(i) = (0:R)178      rw [massValue, other]179      exact realNat.zero180    rw massZero181    have blockAlternatives : i ∈ blockSet(n, blk, p) ∨ ¬i ∈ blockSet(n, blk, p) by tauto182    cases blockAlternatives with inBlock | outside183    . have onBlock := maskedPoint.on_block with aFunction, hi, inBlock184      have value := pureProfile.value at n, functionImage(rep, m, n), i with *185      have notImage : ¬i ∈ functionImage(rep, m, n)186        intro inImage187        have parts := functionImage.membership.forward with inImage188        obtain ⟨q, hq, equal⟩ := parts.right189        have blockParts := blockSet.membership.forward with inBlock190        have blockI := blockParts.right191        have sectionQ := section with hq192        rw [equal, sectionQ] at blockI193        apply different194        rw [equal, blockI]195        rfl196      have zero := indicator.absent with notImage197      rw [onBlock, value, zero]198      exact realNat.zero199    . exact maskedPoint.off_block with aFunction, hi, outside200201theorem pureProfile.in_product (n : Nat) (m blk rep : Set)202  requires blkFunction : blk : n → m203  requires repFunction : rep : m → n204  requires section : ∀ q ∈ m, blk(rep(q)) = q205  shows pureProfile(n, functionImage(rep, m, n)) ∈ simplexProduct(n, m, blk)206proof207  have aCube := pureProfile.in_cube at n, functionImage(rep, m, n)208  apply simplexProduct.membership.backward209  constructor210  . exact aCube211  . intros p hp212    have aFunction := unitCube.point with aCube213    have sequence := maskedPoint.sequence at n, blockSet(n, blk, p), pureProfile(n, functionImage(rep, m, n)) with aFunction214    have mass := pointMass.sequence at rep(p)215    have agree : ∀ k ∈ ℕ, k < n → maskedPoint(n, blockSet(n, blk, p), pureProfile(n, functionImage(rep, m, n)))(k) = pointMass(rep(p))(k)216      intros k hk hkn217      have hkIn : k ∈ n by exact membership.of_Less with hkn218      exact pureProfile.masked with blkFunction, repFunction, section, hp, hkIn219    have equal := realPartialSum.eq_prefix with sequence, mass, agree220    have repIn := FunctionBetween.apply_closed with repFunction, hp221    have one := realPartialSum.pointMass_below at rep(p), n222    have blockValue := blockSum.definition at n, blk, p223    have cubeValue := sumCube.value at n, blockSet(n, blk, p), pureProfile(n, functionImage(rep, m, n)) with aCube224    rw blockValue at cubeValue225    rw [cubeValue, equal]226    exact one with repIn227