Keyword: zero-sum

Theorem Antisymmetric Matrix Game Has Value Zero proved

Theorem Antisymmetric Matrix Games Have Value proved

Theorem Aumann-Maschler Cav-u Theorem staged

Lemma Base Case of Loomis Induction proved

Theorem Bewley-Kohlberg Asymptotic Value staged

Theorem Big Match Uniform Value staged

Lemma Bracket Invariant For Admissible Sequences admitted

Lemma Cesàro Payoff Convergence From Robinson Lemma admitted

Lemma Column-Drop Step of Loomis Induction proved

Lemma Common Guarantee Gives The Value proved

Proposition Compact Mixed Versus Finite-Support Minimax admitted

Proposition Continuous Fictitious Play Closes The Duality Gap admitted

Definition Derived Game admitted

Proposition Diagonal Matrix Game Value proved

Proof plan Direct Induction Proof Of Loomis Theorem formalized

Proposition Directional Derivative Of The Value admitted

Theorem Discounted Value Is the Unique Shapley Fixed Point staged

Definition Discounted Value of a Zero-Sum Stochastic Game staged

Definition Duality Gap In A Matrix Game formalized

Definition Empirical Frequency Of Play formalized

Definition Epsilon-Optimal Strategy formalized

Lemma Euclidean Division Pasting In Robinson Induction admitted

Lemma Existence of Loomis Optimisers proved

Theorem Existence of Optimal Mixed Strategies (Loomis Foundations) proved

Definition Expected Payoff of a Matrix Game formalized

Definition Fictitious Play formalized

Theorem Fictitious Play Convergence admitted

Definition Field-Generic Value Predicates formalized

Proposition Finite-Opponent Separation Minimax admitted

Theorem General Mixed Minimax Theorem admitted

Definition General Mixed Strategy Space admitted

Definition General Value Operator admitted

Proposition General Value Operator Is Nonexpansive admitted

Lemma Intersection Lemma admitted

Proof plan Kakutani Fixed-Point Proof of the Minimax Theorem admitted

Proof plan LP Duality Proof Of Minimax admitted

Theorem LP Optimum ↔ Game-Theoretic Optimal Strategy admitted

Theorem Loomis Theorem (Positive B) proved

Lemma Markov Stationary Distribution as Zero-Sum Game Value admitted

Example Matching Pennies formalized

Definition Matrix Game formalized

Definition Maximin and Minimax Values formalized

Lemma Maximin is Bounded by Minimax proved

Theorem Mertens-Neyman Uniform Value staged

Proof plan Minimax From Antisymmetric Games admitted

Proof plan Minimax From Deterministic Approachability admitted

Proof plan Minimax via the All-Ones Specialization of Loomis formalized

Definition Mixed Extension Of A Matrix Game formalized

Example Mixed Extension Pathology admitted

Theorem Mixed Nash Equilibrium of a Matrix Game proved

Definition Mixed Strategy Simplex formalized

Proposition Monotone Decreasing Values Limit admitted

Example Monotone Family Assumption Counterexamples admitted

Theorem Nash Payoff Uniqueness in Zero-Sum Games proved

Theorem Noisy Duel With Multiple Bullets admitted

Proposition Noisy One-Bullet Duel Value admitted

Proposition One-Sided Compact Convex Minimax admitted

Theorem Optimal Pairs Are Exactly Saddle Points proved

Definition Optimal Strategy Sets formalized

Proposition Optimal Strategy Sets Are Polytopes proved

Theorem Ordered-Field Minimax Statement formalized

Lemma Payoff Negation in Zero-Sum Games proved

Theorem Perron-Frobenius For Positive Matrices proved

Definition Player Guarantee formalized

Definition Player-1 LP Formulation of a Matrix Game admitted

Definition Player-2 LP Formulation of a Matrix Game admitted

Example Poker Game Value Example staged

Lemma Positive Aggregates xB and By proved

Definition Quasi-Concavity And Semicontinuity admitted

Lemma Robinson Admissible Sequence Lemma admitted

Lemma Row-Drop Step of Loomis Induction proved

Definition Saddle Point formalized

Definition Shapley Operator staged

Theorem Shapley Operator Is a γ-Contraction staged

Proposition Silent One-Bullet Duel Has No Pure Value admitted

Proposition Silent Versus Noisy One-Bullet Duel Value admitted

Example Sion Boundary Counterexample admitted

Theorem Sion Minimax Theorem admitted

Example Sion-Wolfe Game Has No Mixed Value admitted

Theorem Stable Game Framework (Hofbauer–Sandholm) staged

Theorem Stochastic Matrix Has An Invariant Distribution proved

Theorem Strictly Competitive Perfect-Information Determinacy proved

Proposition Strong Complementarity proved

Theorem Strong Complementarity proved

Lemma Subgame Reduction For Non-Useful Indices admitted

Theorem Support Complementarity proved

Definition Support Of A Mixed Strategy formalized

Example Three-By-Two Matrix Game Computation formalized

Example Three-Player Minimax Failure formalized

Example Two-By-Two Value Formula formalized

Lemma Useful Window Bound For Admissible Sequences admitted

Theorem Value In Finite Zero-Sum Perfect-Information Games (No-Chance) proved

Theorem Value In Finite Zero-Sum Perfect-Information Games (With Chance) staged

Definition Value Of A Zero-Sum Game formalized

Proposition Value Operator Properties admitted

Theorem Ville Theorem admitted

Proof plan Ville Theorem By Discretization admitted

Theorem Von Neumann Minimax Theorem proved

Lemma Weak Duality For Loomis Values proved

Definition Zero-Sum Game formalized

Proof plan Zero-Sum Linear Programming Bridge admitted

Theorem Zero-Sum Nash Equilibria As Saddle Points proved