Math

Theorem Antisymmetric Matrix Games Have Value proved

Lemma Base Case of Loomis Induction proved

Theorem Brouwer Fixed Point Theorem staged

Theorem Brouwer Fixed Point Theorem For A Simplex proved

Lemma Column-Drop Step of Loomis Induction proved

Lemma Common Guarantee Gives The Value proved

Lemma Continuity on the Real Standard Simplex proved

Definition Convex Combination of Simplex Points formalized

Proof plan Direct Induction Proof Of Loomis Theorem formalized

Lemma Existence of Loomis Optimisers proved

Theorem Farkas Lemma proved

Definition Field-Generic Value Predicates formalized

Lemma Fixed Point Theorem For Retracts Of A Simplex staged

Lemma Fourier-Motzkin Elimination Step proved

Lemma Iterated Weighted Sums Commute proved

Theorem Kakutani Fixed Point Theorem staged

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

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

Theorem Ordered-Field Minimax Statement formalized

Definition Player-1 LP Formulation of a Matrix Game admitted

Definition Player-2 LP Formulation of a Matrix Game admitted

Definition Point Mass on the Standard Simplex formalized

Lemma Pointwise Bounds Are Simplex Bounds proved

Lemma Positive Aggregates xB and By proved

Lemma Row-Drop Step of Loomis Induction proved

Lemma Scarf Combinatorial Lemma (Colorful Room Existence) proved

Proposition Strong Complementarity proved

Theorem Strong Complementarity For Linear Programming proved

Theorem Strong Duality For Linear Programming proved

Lemma Sup-Inf Choice Function Identity staged

Theorem Tarski Fixed Point Theorem For Compact Euclidean Lattices staged

Theorem Theorem Of The Alternative proved

Theorem Ville Theorem admitted

Proof plan Ville Theorem By Discretization admitted

Lemma Weak Duality For Loomis Values proved

Definition Weighted Sum over the Standard Simplex formalized

Proof plan Zero-Sum Linear Programming Bridge admitted

Theorem Zero-Sum Nash Equilibria As Saddle Points proved