Game Theory.Zero Sum

Theorem Antisymmetric Matrix Game Has Value Zero proved

Theorem Blackwell B-Set Approachability staged

Lemma Bracket Invariant For Admissible Sequences admitted

Definition Calibrated Strategy staged

Theorem Calibrated Strategy Exists staged

Lemma Cesàro Payoff Convergence From Robinson Lemma admitted

Proposition Compact Mixed Versus Finite-Support Minimax admitted

Proposition Continuous Fictitious Play Closes The Duality Gap admitted

Definition Derived Game admitted

Theorem Deterministic Blackwell Sequence staged

Proposition Diagonal Matrix Game Value proved

Proposition Directional Derivative Of The Value admitted

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

Theorem Existence of Optimal Mixed Strategies (Loomis Foundations) proved

Definition Expected Payoff of a Matrix Game formalized

Definition External Regret staged

Definition Fictitious Play formalized

Theorem Fictitious Play Convergence admitted

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

Definition Hannan Set staged

Definition Internal Regret staged

Lemma Intersection Lemma admitted

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

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 No External Regret Converges To Hannan Set staged

Theorem No Internal Regret Converges To Correlated Equilibrium staged

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

Lemma Payoff Negation in Zero-Sum Games proved

Theorem Perron-Frobenius For Positive Matrices proved

Definition Player Guarantee formalized

Definition Quasi-Concavity And Semicontinuity admitted

Lemma Robinson Admissible Sequence Lemma admitted

Definition Saddle Point formalized

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 Stochastic Matrix Has An Invariant Distribution proved

Proposition Strict Domination And Never Best Response (via auxiliary zero-sum game) admitted

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

Definition Value Of A Zero-Sum Game formalized

Proposition Value Operator Properties admitted

Theorem Von Neumann Minimax Theorem proved

Proposition Weak Domination And Completely Mixed Tests (via auxiliary zero-sum game) admitted

Definition Zero-Sum Game formalized