Math.Minimax

Theorem Antisymmetric Matrix Games Have Value proved

Lemma Base Case of Loomis Induction proved

Lemma Column-Drop Step of Loomis Induction proved

Lemma Common Guarantee Gives The Value proved

Proof plan Direct Induction Proof Of Loomis Theorem formalized

Lemma Existence of Loomis Optimisers proved

Definition Field-Generic Value Predicates formalized

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

Proof plan LP Duality Proof Of Minimax 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

Lemma Positive Aggregates xB and By proved

Lemma Row-Drop Step of Loomis Induction proved

Proposition Strong Complementarity proved

Theorem Ville Theorem admitted

Proof plan Ville Theorem By Discretization admitted

Lemma Weak Duality For Loomis Values proved

Theorem Zero-Sum Nash Equilibria As Saddle Points proved