Skip to content

Latest commit

 

History

History
7 lines (5 loc) · 576 Bytes

README.md

File metadata and controls

7 lines (5 loc) · 576 Bytes

If it's easier, this project lives on github at: https://github.com/dipplestix/lean_nash_eq

Status:

  1. Listed the conditions for K fixed points and use the pris_dil_bounded and best_response_exists lemmas inside the NE lemma

  2. Started working on the same things, but for mixed strategies. Trying to make a simplex class and combine that with the set of strategies didn't work out for me, so I tried to implement the paper I referred to in the mixed_nash.lean file from coq to lean. Got through some of it, but unfortunately didn't have time to finish the full translation.