If it's easier, this project lives on github at: https://github.com/dipplestix/lean_nash_eq
Status:
-
Listed the conditions for K fixed points and use the pris_dil_bounded and best_response_exists lemmas inside the NE lemma
-
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.