Action At An Information Set Definition formalized
Agent Normal Form Definition staged
Agent Normal Form Of A Bayesian Game Definition staged
Antisymmetric Matrix Game Has Value Zero Theorem proved
Approximate Solution Definition staged
Approximate Solutions Are Reny Solutions Proposition staged
Aumann-Maschler Cav-u Theorem Theorem staged
Backward And Forward Induction Can Conflict Example staged
Backward Induction Value Definition formalized
Balanced Coalitional Game Definition staged
Balanced Collection Of Coalitions Definition staged
Bayesian Equilibrium Definition staged
Bayesian Equilibrium As Nash Equilibrium Theorem staged
Bayesian Game Definition staged
Bayesian Strategy Definition staged
Behavioral Equilibrium Definition staged
Belief System Definition staged
Best Response Definition admitted
Best Response Face Proposition staged
Best-Response Invariance Definition staged
Better Reply Secure Game Definition staged
Bewley-Kohlberg Asymptotic Value Theorem staged
Big Match Uniform Value Theorem staged
Blackwell B-Set Approachability Theorem staged
Bondareva-Shapley Theorem Theorem staged
Bracket Invariant For Admissible Sequences Lemma admitted
Calibrated Strategy Definition staged
Calibrated Strategy Exists Theorem staged
Canonical Correlation Device Definition staged
Cesàro Payoff Convergence From Robinson Lemma Lemma admitted
Chomp Strategy Stealing Theorem staged
Common Knowledge Can Filter Nash Equilibria Example staged
Compact Mixed Versus Finite-Support Minimax Proposition admitted
Completely Mixed Nash Is Subgame Perfect Theorem staged
Continuous Fictitious Play Closes The Duality Gap Proposition admitted
Convex Coalitional Game Definition staged
Convex Game Definition staged
Convex Game Nash Variational Characterization Proposition staged
Convex Games Have Nonempty Core Theorem staged
Core Of A Coalitional Game Definition staged
Core Payoffs Are Imputations Theorem staged
Correlated Best Response Need Not Be Independent Example staged
Correlated Equilibrium Definition staged
Correlated Equilibrium Exists In Finite Games Theorem staged
Correlated Equilibrium Set Is Convex And Compact Theorem staged
Correlated Strategy Definition staged
Cournot Duopoly Equilibrium From Supermodularity Proposition staged
Cournot Fishermen Equilibria Proposition staged
Degenerate Correlated Equilibrium Theorem staged
Derived Game Definition admitted
Determined Game Definition formalized
Deterministic Blackwell Sequence Theorem staged
Diagonal Matrix Game Value Proposition proved
Directional Derivative Of The Value Proposition admitted
Discounted Folk Theorem Theorem staged
Discounted Repeated Game Definition staged
Discounted Value Is the Unique Shapley Fixed Point Theorem staged
Discounted Value of a Zero-Sum Stochastic Game Definition staged
Dominant Strategy Profile is a Nash Equilibrium Theorem admitted
Dominated Strategy Definition staged
Duality Gap In A Matrix Game Definition formalized
ESS Replicator Lyapunov Function Theorem staged
ESS Uniform Invasion Barrier Proposition staged
Empirical Frequency Of Play Definition formalized
Entrant Incomplete Information Value Example Example staged
Epsilon Equilibrium Definition staged
Epsilon Perfect Equilibrium Definition staged
Epsilon Proper Equilibrium Definition staged
Epsilon-Optimal Strategy Definition formalized
Equilibrium Manifold Definition staged
Essential Equilibrium Component Definition staged
Euclidean Division Pasting In Robinson Induction Lemma admitted
Evaluation Game Equilibrium Definition staged
Evolutionarily Stable Strategy Definition staged
Existence Of Behavioral Equilibrium Theorem staged
Existence Of Perfect Equilibrium Theorem staged
Existence Of Proper Equilibrium Theorem staged
Existence Of Reny Solutions Theorem staged
Existence Of Sequential Equilibrium Theorem staged
Existence Of Subgame-Perfect Equilibrium With Perfect Recall Theorem staged
Existence of Optimal Mixed Strategies (Loomis Foundations) Theorem proved
Expected Payoff of a Matrix Game Definition formalized
Extensive Form Perfect Equilibrium Definition staged
Extensive Game With Imperfect Information Definition formalized
Extensive-Game Theorems Catalog Definition staged
External Regret Definition staged
Feasible And Individually Rational Payoffs Definition staged
Fictitious Play Definition formalized
Fictitious Play Convergence Theorem admitted
Finite Bayesian Equilibrium Exists Theorem staged
Finite Extensive Game With Perfect Information Definition formalized
Finite Game Catalog Definition staged
Finite Game-Tree Strategy Induces An Outcome Definition formalized
Finite Nash Equilibrium Computation Examples Example staged
Finite-Opponent Separation Minimax Proposition admitted
Finitely Repeated Folk Theorem Theorem staged
Finitely Repeated Game Definition staged
Fink Nash Existence in Stochastic Games Theorem staged
First-Order Nash Condition Theorem staged
Focal Point Definition staged
Folk Theorem (Baseline Statement) Theorem staged
Forward Induction Definition staged
Game Tree Definition formalized
General Mixed Minimax Theorem Theorem admitted
General Mixed Strategy Space Definition admitted
General Value Operator Definition admitted
General Value Operator Is Nonexpansive Proposition admitted
Generic Finite Odd Equilibria Theorem staged
Generic Uniqueness Of Subgame-Perfect Equilibrium Proposition staged
Hannan Set Definition staged
History And Subgame Definition formalized
Imputation Definition staged
Information Set Definition staged
Information Set Refinement And Equilibrium Proposition staged
Internal Regret Definition staged
Intersection Lemma Lemma admitted
Isbell Behavioral-To-Mixed Equivalence Theorem staged
Iterated Elimination Of Strictly Dominated Strategies Definition staged
Kakutani From Two-Player Nash Existence Theorem staged
Kohlberg Mertens Structure Theorem Theorem staged
Kuhn Existence Of Pure Subgame-Perfect Equilibrium (No-Chance) Theorem proved
Kuhn Existence Of Pure Subgame-Perfect Equilibrium (With Chance) Theorem staged
Kuhn Mixed-To-Behavioral Equivalence Theorem staged
Linear Extensive Game Definition staged
Local Characterization Of Behavioral Equilibrium Theorem staged
Marginal Contribution Definition staged
Markov Stationary Distribution as Zero-Sum Game Value Lemma admitted
Matching Pennies Example formalized
Matrix Game Definition formalized
Maximin and Minimax Values Definition formalized
Maximin is Bounded by Minimax Lemma proved
Mediated Game Definition staged
Mertens Stable Sets Definition staged
Mertens-Neyman Uniform Value Theorem staged
Mixed Behavioral And General Strategies Definition staged
Mixed Equilibrium In Compact Continuous Games Theorem staged
Mixed Extension Of A Matrix Game Definition formalized
Mixed Extension Of A Strategic Game Definition staged
Mixed Extension Pathology Example admitted
Mixed Nash Equilibrium Definition staged
Mixed Nash Equilibrium of a Matrix Game Theorem proved
Mixed Strategy Definition staged
Mixed Strategy Simplex Definition formalized
Monotone Decreasing Values Limit Proposition admitted
Monotone Family Assumption Counterexamples Example admitted
Monotone Smooth Game Definition staged
Monotonic Coalitional Game Definition staged
Nash Characterization And Uniqueness In Monotone Games Theorem staged
Nash Equilibria Are Rationalizable Proposition staged
Nash Equilibrium Definition admitted
Nash Equilibrium Induces Correlated Equilibrium Theorem staged
Nash Existence For Finite Games Theorem proved
Nash Existence In Better Reply Secure Games Theorem staged
Nash Existence In Compact Quasi-Concave Games Theorem staged
Nash Existence In Convex Games Theorem staged
Nash Existence In Supermodular Games Theorem staged
Nash Field Definition staged
Nash Payoff Uniqueness in Zero-Sum Games Theorem proved
Nash Payoffs Are Individually Rational Proposition staged
Nash Wardrop Equilibrium Definition staged
Nature In Extensive Games Definition staged
No External Regret Converges To Hannan Set Theorem staged
No Internal Regret Converges To Correlated Equilibrium Theorem staged
Noisy Duel With Multiple Bullets Theorem admitted
Noisy One-Bullet Duel Value Proposition admitted
Non-Player-Controlled Nonterminal State Definition formalized
Noncontractible Feasible Payoff Example Example staged
Normal And Extensive Perfection Can Differ Example staged
Normal Form Invariance Of Extensive Representations Proposition proved
Normal Form Reduction Definition formalized
Obedience Condition Theorem staged
One-Sided Compact Convex Minimax Proposition admitted
Optimal Pairs Are Exactly Saddle Points Theorem proved
Optimal Strategy Sets Definition formalized
Optimal Strategy Sets Are Polytopes Proposition proved
Payoff Negation in Zero-Sum Games Lemma proved
Payoff Vector Definition staged
Perfect Equilibrium Definition staged
Perfect Equilibrium And Undominated Equilibrium Proposition staged
Perfect Recall Definition staged
Perron-Frobenius For Positive Matrices Theorem proved
Player Guarantee Definition formalized
Poker Game Value Example Example staged
Population Game Definition staged
Positive Correlation Dynamics Definition staged
Potential Game Definition staged
Potential Is Lyapunov For Replicator Dynamics Theorem staged
Potential Maximizer Is Nash Theorem staged
Prisoner's Dilemma Example admitted
Proper And Perfect Equilibrium Examples Example staged
Proper Equilibrium Definition staged
Proper Equilibrium Induces Sequential Equilibrium Theorem staged
Prudent Strategy Definition staged
Pure Strategy With Imperfect Information Definition formalized
Quasi-Concave Game Definition staged
Quasi-Concavity And Semicontinuity Definition admitted
Rationalizable Set As Largest Best-Response Fixed Set Proposition staged
Rationalizable Strategy Definition staged
Reached Information Set Definition staged
Reached Subgame Nash Restriction Theorem staged
Recommendation Strategy Definition staged
Reny Solution Definition staged
Repeated Feasible Individually Rational Payoffs Definition staged
Repeated Game Definition staged
Repeated Game History Definition staged
Repeated Game Payoff Aggregation Definition staged
Repeated Game Strategy Definition staged
Repeated Game With Incomplete Information Definition staged
Repeated Game With Signals Definition staged
Replicator Dynamics Definition staged
Robinson Admissible Sequence Lemma Lemma admitted
Rubinstein Bargaining Subgame Perfect Equilibrium Theorem staged
Saddle Point Definition formalized
Semi-Algebraic Mixed Nash Set Proposition staged
Semi-Reduced Normal Form Definition formalized
Sequential Equilibrium Definition staged
Shapley Axioms Definition staged
Shapley Operator Definition staged
Shapley Operator Is a γ-Contraction Theorem staged
Shapley Uniqueness Theorem Theorem staged
Shapley Value Definition staged
Shapley Value Is Efficient Theorem staged
Shapley Value Lies In The Core Of A Convex Game Theorem staged
Silent One-Bullet Duel Has No Pure Value Proposition admitted
Silent Versus Noisy One-Bullet Duel Value Proposition admitted
Simple Game Definition staged
Simple Perfect-Information Game Definition formalized
Sion Boundary Counterexample Example admitted
Sion Minimax Theorem Theorem admitted
Sion-Wolfe Game Has No Mixed Value Example admitted
Smooth Game Definition staged
Solvable Game Definition staged
Solvable Games Have A Unique Nash Equilibrium Proposition staged
Stable Game Framework (Hofbauer–Sandholm) Theorem staged
Standard Repeated Game Definition staged
Stochastic Game Definition staged
Stochastic Game History Definition staged
Stochastic Matrix Has An Invariant Distribution Theorem proved
Strategic Game Definition admitted
Strategic Stability Definition staged
Strategy In A Perfect-Information Game Definition formalized
Strategy Profile Definition admitted
Strategy Profile And Induced Outcome Definition staged
Strict Dominance Definition admitted
Strict Domination And Never Best Response (via auxiliary zero-sum game) Proposition admitted
Strict Equilibrium Definition staged
Strict Equilibrium Is Proper Proposition staged
Strictly Competitive Perfect-Information Determinacy Theorem proved
Strictly Dominant Strategy Definition admitted
Strong Complementarity Theorem proved
Subgame Perfect Uniform Folk Theorem Theorem staged
Subgame Reduction For Non-Useful Indices Lemma admitted
Subgame-Perfect Equilibrium Implies Nash Equilibrium Proposition proved
Subgame-Perfect Equilibrium In Imperfect-Information Games Definition staged
Subgame-Perfect Equilibrium In Perfect-Information Games Definition formalized
Subroot And Subgame In Imperfect-Information Games Definition formalized
Superadditive Coalitional Game Definition staged
Supermodular Best Responses Are Lattices Proposition staged
Supermodular Game Definition staged
Support Complementarity Theorem proved
Support Of A Mixed Strategy Definition formalized
Symmetric Game Definition staged
Symmetric Mixed Equilibrium Theorem staged
Threat Point Definition staged
Three-By-Two Matrix Game Computation Example formalized
Three-Player Minimax Failure Example formalized
Three-Player Minority Game Equilibria Proposition staged
Transferable-Utility Coalitional Game Definition staged
Two-By-Two Value Formula Example formalized
Uniform Equilibrium Definition staged
Uniform Folk Theorem Theorem staged
Unilateral Deviation Definition admitted
Useful Window Bound For Admissible Sequences Lemma admitted
Value In Finite Zero-Sum Perfect-Information Games (No-Chance) Theorem proved
Value In Finite Zero-Sum Perfect-Information Games (With Chance) Theorem staged
Value Of A Zero-Sum Game Definition formalized
Value Operator Properties Proposition admitted
Von Neumann Minimax Theorem Theorem proved
Wardrop Variational Characterization Proposition staged
Weak Bayesian Perfect Equilibrium Definition staged
Weak Dominance Definition admitted
Weak Domination And Completely Mixed Tests (via auxiliary zero-sum game) Proposition admitted
Weakly Dominant Strategy Definition admitted
Zermelo Determinacy For Finite Perfect-Information Games Theorem proved
Zero-Sum Game Definition formalized

Game Theory.Cooperative Game

Balanced Coalitional Game Definition staged
Balanced Collection Of Coalitions Definition staged
Bondareva-Shapley Theorem Theorem staged
Convex Coalitional Game Definition staged
Convex Games Have Nonempty Core Theorem staged
Core Of A Coalitional Game Definition staged
Core Payoffs Are Imputations Theorem staged
Imputation Definition staged
Marginal Contribution Definition staged
Monotonic Coalitional Game Definition staged
Payoff Vector Definition staged
Shapley Axioms Definition staged
Shapley Uniqueness Theorem Theorem staged
Shapley Value Definition staged
Shapley Value Is Efficient Theorem staged
Shapley Value Lies In The Core Of A Convex Game Theorem staged
Simple Game Definition staged
Superadditive Coalitional Game Definition staged
Transferable-Utility Coalitional Game Definition staged

Game Theory.Cooperative Game.Classes

Convex Coalitional Game Definition staged
Convex Games Have Nonempty Core Theorem staged
Monotonic Coalitional Game Definition staged
Simple Game Definition staged
Superadditive Coalitional Game Definition staged

Game Theory.Cooperative Game.Core

Balanced Coalitional Game Definition staged
Balanced Collection Of Coalitions Definition staged
Core Of A Coalitional Game Definition staged
Core Payoffs Are Imputations Theorem staged
Imputation Definition staged
Marginal Contribution Definition staged
Payoff Vector Definition staged
Transferable-Utility Coalitional Game Definition staged

Game Theory.Cooperative Game.Shapley Value

Bondareva-Shapley Theorem Theorem staged
Shapley Axioms Definition staged
Shapley Uniqueness Theorem Theorem staged
Shapley Value Definition staged
Shapley Value Is Efficient Theorem staged
Shapley Value Lies In The Core Of A Convex Game Theorem staged

Game Theory.Extensive Game

Action At An Information Set Definition formalized
Agent Normal Form Definition staged
Backward And Forward Induction Can Conflict Example staged
Backward Induction Value Definition formalized
Behavioral Equilibrium Definition staged
Belief System Definition staged
Chomp Strategy Stealing Theorem staged
Completely Mixed Nash Is Subgame Perfect Theorem staged
Determined Game Definition formalized
Entrant Incomplete Information Value Example Example staged
Existence Of Behavioral Equilibrium Theorem staged
Existence Of Sequential Equilibrium Theorem staged
Existence Of Subgame-Perfect Equilibrium With Perfect Recall Theorem staged
Extensive Form Perfect Equilibrium Definition staged
Extensive Game With Imperfect Information Definition formalized
Extensive-Game Theorems Catalog Definition staged
Finite Extensive Game With Perfect Information Definition formalized
Finite Game-Tree Strategy Induces An Outcome Definition formalized
Forward Induction Definition staged
Game Tree Definition formalized
Generic Uniqueness Of Subgame-Perfect Equilibrium Proposition staged
History And Subgame Definition formalized
Information Set Definition staged
Information Set Refinement And Equilibrium Proposition staged
Isbell Behavioral-To-Mixed Equivalence Theorem staged
Kuhn Existence Of Pure Subgame-Perfect Equilibrium (No-Chance) Theorem proved
Kuhn Existence Of Pure Subgame-Perfect Equilibrium (With Chance) Theorem staged
Kuhn Mixed-To-Behavioral Equivalence Theorem staged
Linear Extensive Game Definition staged
Local Characterization Of Behavioral Equilibrium Theorem staged
Mertens Stable Sets Definition staged
Mixed Behavioral And General Strategies Definition staged
Nature In Extensive Games Definition staged
Non-Player-Controlled Nonterminal State Definition formalized
Normal And Extensive Perfection Can Differ Example staged
Normal Form Invariance Of Extensive Representations Proposition proved
Normal Form Reduction Definition formalized
Perfect Recall Definition staged
Poker Game Value Example Example staged
Proper Equilibrium Induces Sequential Equilibrium Theorem staged
Pure Strategy With Imperfect Information Definition formalized
Reached Information Set Definition staged
Reached Subgame Nash Restriction Theorem staged
Rubinstein Bargaining Subgame Perfect Equilibrium Theorem staged
Semi-Reduced Normal Form Definition formalized
Sequential Equilibrium Definition staged
Simple Perfect-Information Game Definition formalized
Strategic Stability Definition staged
Strategy In A Perfect-Information Game Definition formalized
Strategy Profile And Induced Outcome Definition staged
Strictly Competitive Perfect-Information Determinacy Theorem proved
Subgame-Perfect Equilibrium Implies Nash Equilibrium Proposition proved
Subgame-Perfect Equilibrium In Imperfect-Information Games Definition staged
Subgame-Perfect Equilibrium In Perfect-Information Games Definition formalized
Subroot And Subgame In Imperfect-Information Games Definition formalized
Value In Finite Zero-Sum Perfect-Information Games (No-Chance) Theorem proved
Value In Finite Zero-Sum Perfect-Information Games (With Chance) Theorem staged
Weak Bayesian Perfect Equilibrium Definition staged
Zermelo Determinacy For Finite Perfect-Information Games Theorem proved

Game Theory.Extensive Game.Core

Finite Game-Tree Strategy Induces An Outcome Definition formalized
Game Tree Definition formalized
History And Subgame Definition formalized
Nature In Extensive Games Definition staged
Non-Player-Controlled Nonterminal State Definition formalized
Strategy Profile And Induced Outcome Definition staged

Game Theory.Extensive Game.Examples

Backward And Forward Induction Can Conflict Example staged
Chomp Strategy Stealing Theorem staged
Entrant Incomplete Information Value Example Example staged
Normal And Extensive Perfection Can Differ Example staged
Poker Game Value Example Example staged
Rubinstein Bargaining Subgame Perfect Equilibrium Theorem staged

Game Theory.Extensive Game.Imperfect Information

Action At An Information Set Definition formalized
Behavioral Equilibrium Definition staged
Belief System Definition staged
Completely Mixed Nash Is Subgame Perfect Theorem staged
Existence Of Behavioral Equilibrium Theorem staged
Existence Of Subgame-Perfect Equilibrium With Perfect Recall Theorem staged
Extensive Game With Imperfect Information Definition formalized
Forward Induction Definition staged
Information Set Definition staged
Information Set Refinement And Equilibrium Proposition staged
Isbell Behavioral-To-Mixed Equivalence Theorem staged
Kuhn Mixed-To-Behavioral Equivalence Theorem staged
Linear Extensive Game Definition staged
Local Characterization Of Behavioral Equilibrium Theorem staged
Mertens Stable Sets Definition staged
Mixed Behavioral And General Strategies Definition staged
Perfect Recall Definition staged
Proper Equilibrium Induces Sequential Equilibrium Theorem staged
Pure Strategy With Imperfect Information Definition formalized
Reached Information Set Definition staged
Reached Subgame Nash Restriction Theorem staged
Sequential Equilibrium Definition staged
Strategic Stability Definition staged
Subgame-Perfect Equilibrium In Imperfect-Information Games Definition staged
Subroot And Subgame In Imperfect-Information Games Definition formalized
Weak Bayesian Perfect Equilibrium Definition staged

Game Theory.Extensive Game.Normal Form

Agent Normal Form Definition staged
Existence Of Sequential Equilibrium Theorem staged
Extensive Form Perfect Equilibrium Definition staged
Normal Form Invariance Of Extensive Representations Proposition proved
Normal Form Reduction Definition formalized
Semi-Reduced Normal Form Definition formalized

Game Theory.Extensive Game.Perfect Information

Backward Induction Value Definition formalized
Determined Game Definition formalized
Extensive-Game Theorems Catalog Definition staged
Finite Extensive Game With Perfect Information Definition formalized
Finite Game-Tree Strategy Induces An Outcome Definition formalized
Generic Uniqueness Of Subgame-Perfect Equilibrium Proposition staged
Kuhn Existence Of Pure Subgame-Perfect Equilibrium (No-Chance) Theorem proved
Kuhn Existence Of Pure Subgame-Perfect Equilibrium (With Chance) Theorem staged
Simple Perfect-Information Game Definition formalized
Strategy In A Perfect-Information Game Definition formalized
Strictly Competitive Perfect-Information Determinacy Theorem proved
Subgame-Perfect Equilibrium Implies Nash Equilibrium Proposition proved
Subgame-Perfect Equilibrium In Perfect-Information Games Definition formalized
Value In Finite Zero-Sum Perfect-Information Games (No-Chance) Theorem proved
Value In Finite Zero-Sum Perfect-Information Games (With Chance) Theorem staged
Zermelo Determinacy For Finite Perfect-Information Games Theorem proved

Game Theory.Repeated Game

Aumann-Maschler Cav-u Theorem Theorem staged
Discounted Folk Theorem Theorem staged
Discounted Repeated Game Definition staged
Finitely Repeated Folk Theorem Theorem staged
Finitely Repeated Game Definition staged
Folk Theorem (Baseline Statement) Theorem staged
Repeated Feasible Individually Rational Payoffs Definition staged
Repeated Game Definition staged
Repeated Game History Definition staged
Repeated Game Payoff Aggregation Definition staged
Repeated Game Strategy Definition staged
Repeated Game With Incomplete Information Definition staged
Repeated Game With Signals Definition staged
Standard Repeated Game Definition staged
Subgame Perfect Uniform Folk Theorem Theorem staged
Uniform Equilibrium Definition staged
Uniform Folk Theorem Theorem staged

Game Theory.Repeated Game.Core

Discounted Repeated Game Definition staged
Finitely Repeated Game Definition staged
Repeated Feasible Individually Rational Payoffs Definition staged
Repeated Game Definition staged
Repeated Game History Definition staged
Repeated Game Payoff Aggregation Definition staged
Repeated Game Strategy Definition staged
Repeated Game With Signals Definition staged
Standard Repeated Game Definition staged
Uniform Equilibrium Definition staged

Game Theory.Repeated Game.Folk Theorem

Discounted Folk Theorem Theorem staged
Finitely Repeated Folk Theorem Theorem staged
Folk Theorem (Baseline Statement) Theorem staged
Subgame Perfect Uniform Folk Theorem Theorem staged
Uniform Folk Theorem Theorem staged

Game Theory.Repeated Game.Incomplete Info

Aumann-Maschler Cav-u Theorem Theorem staged
Repeated Game With Incomplete Information Definition staged

Game Theory.Stochastic Game

Bewley-Kohlberg Asymptotic Value Theorem staged
Big Match Uniform Value Theorem staged
Discounted Value Is the Unique Shapley Fixed Point Theorem staged
Discounted Value of a Zero-Sum Stochastic Game Definition staged
Fink Nash Existence in Stochastic Games Theorem staged
Mertens-Neyman Uniform Value Theorem staged
Shapley Operator Definition staged
Shapley Operator Is a γ-Contraction Theorem staged
Stochastic Game Definition staged
Stochastic Game History Definition staged

Game Theory.Stochastic Game.Asymptotic

Bewley-Kohlberg Asymptotic Value Theorem staged
Mertens-Neyman Uniform Value Theorem staged

Game Theory.Stochastic Game.Core

Big Match Uniform Value Theorem staged
Fink Nash Existence in Stochastic Games Theorem staged
Stochastic Game Definition staged
Stochastic Game History Definition staged

Game Theory.Stochastic Game.Value

Discounted Value Is the Unique Shapley Fixed Point Theorem staged
Discounted Value of a Zero-Sum Stochastic Game Definition staged
Shapley Operator Definition staged
Shapley Operator Is a γ-Contraction Theorem staged

Game Theory.Strategic Game

Agent Normal Form Of A Bayesian Game Definition staged
Approximate Solution Definition staged
Approximate Solutions Are Reny Solutions Proposition staged
Bayesian Equilibrium Definition staged
Bayesian Equilibrium As Nash Equilibrium Theorem staged
Bayesian Game Definition staged
Bayesian Strategy Definition staged
Best Response Definition admitted
Best Response Face Proposition staged
Best-Response Invariance Definition staged
Better Reply Secure Game Definition staged
Canonical Correlation Device Definition staged
Common Knowledge Can Filter Nash Equilibria Example staged
Convex Game Definition staged
Convex Game Nash Variational Characterization Proposition staged
Correlated Best Response Need Not Be Independent Example staged
Correlated Equilibrium Definition staged
Correlated Equilibrium Exists In Finite Games Theorem staged
Correlated Equilibrium Set Is Convex And Compact Theorem staged
Correlated Strategy Definition staged
Cournot Duopoly Equilibrium From Supermodularity Proposition staged
Cournot Fishermen Equilibria Proposition staged
Degenerate Correlated Equilibrium Theorem staged
Dominant Strategy Profile is a Nash Equilibrium Theorem admitted
Dominated Strategy Definition staged
ESS Replicator Lyapunov Function Theorem staged
ESS Uniform Invasion Barrier Proposition staged
Epsilon Equilibrium Definition staged
Epsilon Perfect Equilibrium Definition staged
Epsilon Proper Equilibrium Definition staged
Equilibrium Manifold Definition staged
Essential Equilibrium Component Definition staged
Evaluation Game Equilibrium Definition staged
Evolutionarily Stable Strategy Definition staged
Existence Of Perfect Equilibrium Theorem staged
Existence Of Proper Equilibrium Theorem staged
Existence Of Reny Solutions Theorem staged
Feasible And Individually Rational Payoffs Definition staged
Finite Bayesian Equilibrium Exists Theorem staged
Finite Game Catalog Definition staged
Finite Nash Equilibrium Computation Examples Example staged
First-Order Nash Condition Theorem staged
Focal Point Definition staged
Generic Finite Odd Equilibria Theorem staged
Iterated Elimination Of Strictly Dominated Strategies Definition staged
Kakutani From Two-Player Nash Existence Theorem staged
Kohlberg Mertens Structure Theorem Theorem staged
Mediated Game Definition staged
Mixed Equilibrium In Compact Continuous Games Theorem staged
Mixed Extension Of A Strategic Game Definition staged
Mixed Nash Equilibrium Definition staged
Mixed Strategy Definition staged
Monotone Smooth Game Definition staged
Nash Characterization And Uniqueness In Monotone Games Theorem staged
Nash Equilibria Are Rationalizable Proposition staged
Nash Equilibrium Definition admitted
Nash Equilibrium Induces Correlated Equilibrium Theorem staged
Nash Existence For Finite Games Theorem proved
Nash Existence In Better Reply Secure Games Theorem staged
Nash Existence In Compact Quasi-Concave Games Theorem staged
Nash Existence In Convex Games Theorem staged
Nash Existence In Supermodular Games Theorem staged
Nash Field Definition staged
Nash Payoffs Are Individually Rational Proposition staged
Nash Wardrop Equilibrium Definition staged
Noncontractible Feasible Payoff Example Example staged
Obedience Condition Theorem staged
Perfect Equilibrium Definition staged
Perfect Equilibrium And Undominated Equilibrium Proposition staged
Population Game Definition staged
Positive Correlation Dynamics Definition staged
Potential Game Definition staged
Potential Is Lyapunov For Replicator Dynamics Theorem staged
Potential Maximizer Is Nash Theorem staged
Prisoner's Dilemma Example admitted
Proper And Perfect Equilibrium Examples Example staged
Proper Equilibrium Definition staged
Prudent Strategy Definition staged
Quasi-Concave Game Definition staged
Rationalizable Set As Largest Best-Response Fixed Set Proposition staged
Rationalizable Strategy Definition staged
Recommendation Strategy Definition staged
Reny Solution Definition staged
Replicator Dynamics Definition staged
Semi-Algebraic Mixed Nash Set Proposition staged
Smooth Game Definition staged
Solvable Game Definition staged
Solvable Games Have A Unique Nash Equilibrium Proposition staged
Stable Game Framework (Hofbauer–Sandholm) Theorem staged
Strategic Game Definition admitted
Strategy Profile Definition admitted
Strict Dominance Definition admitted
Strict Equilibrium Definition staged
Strict Equilibrium Is Proper Proposition staged
Strictly Dominant Strategy Definition admitted
Supermodular Best Responses Are Lattices Proposition staged
Supermodular Game Definition staged
Symmetric Game Definition staged
Symmetric Mixed Equilibrium Theorem staged
Threat Point Definition staged
Three-Player Minority Game Equilibria Proposition staged
Unilateral Deviation Definition admitted
Wardrop Variational Characterization Proposition staged
Weak Dominance Definition admitted
Weakly Dominant Strategy Definition admitted

Game Theory.Strategic Game.Bayesian Correlated

Agent Normal Form Of A Bayesian Game Definition staged
Bayesian Equilibrium Definition staged
Bayesian Equilibrium As Nash Equilibrium Theorem staged
Bayesian Game Definition staged
Bayesian Strategy Definition staged
Best Response Face Proposition staged
Canonical Correlation Device Definition staged
Correlated Best Response Need Not Be Independent Example staged
Correlated Equilibrium Definition staged
Correlated Equilibrium Exists In Finite Games Theorem staged
Correlated Equilibrium Set Is Convex And Compact Theorem staged
Correlated Strategy Definition staged
Degenerate Correlated Equilibrium Theorem staged
Finite Bayesian Equilibrium Exists Theorem staged
Mediated Game Definition staged
Nash Equilibrium Induces Correlated Equilibrium Theorem staged
Obedience Condition Theorem staged
Recommendation Strategy Definition staged

Game Theory.Strategic Game.Continuous

Convex Game Definition staged
Convex Game Nash Variational Characterization Proposition staged
Cournot Duopoly Equilibrium From Supermodularity Proposition staged
Cournot Fishermen Equilibria Proposition staged
Evaluation Game Equilibrium Definition staged
Feasible And Individually Rational Payoffs Definition staged
First-Order Nash Condition Theorem staged
Focal Point Definition staged
Mixed Equilibrium In Compact Continuous Games Theorem staged
Monotone Smooth Game Definition staged
Nash Characterization And Uniqueness In Monotone Games Theorem staged
Nash Existence In Compact Quasi-Concave Games Theorem staged
Nash Existence In Convex Games Theorem staged
Nash Existence In Supermodular Games Theorem staged
Noncontractible Feasible Payoff Example Example staged
Prudent Strategy Definition staged
Quasi-Concave Game Definition staged
Smooth Game Definition staged
Supermodular Best Responses Are Lattices Proposition staged
Supermodular Game Definition staged
Threat Point Definition staged
Three-Player Minority Game Equilibria Proposition staged

Game Theory.Strategic Game.Core

Best Response Definition admitted
Best-Response Invariance Definition staged
Finite Game Catalog Definition staged
Mixed Extension Of A Strategic Game Definition staged
Mixed Strategy Definition staged
Prisoner's Dilemma Example admitted
Strategic Game Definition admitted
Strategy Profile Definition admitted
Symmetric Game Definition staged
Unilateral Deviation Definition admitted

Game Theory.Strategic Game.Dominance

Dominated Strategy Definition staged
Iterated Elimination Of Strictly Dominated Strategies Definition staged
Nash Equilibria Are Rationalizable Proposition staged
Rationalizable Set As Largest Best-Response Fixed Set Proposition staged
Rationalizable Strategy Definition staged
Solvable Game Definition staged
Solvable Games Have A Unique Nash Equilibrium Proposition staged
Strict Dominance Definition admitted
Strictly Dominant Strategy Definition admitted
Weak Dominance Definition admitted
Weakly Dominant Strategy Definition admitted

Game Theory.Strategic Game.Dynamics

ESS Replicator Lyapunov Function Theorem staged
ESS Uniform Invasion Barrier Proposition staged
Evolutionarily Stable Strategy Definition staged
Nash Field Definition staged
Nash Wardrop Equilibrium Definition staged
Population Game Definition staged
Positive Correlation Dynamics Definition staged
Potential Game Definition staged
Potential Is Lyapunov For Replicator Dynamics Theorem staged
Potential Maximizer Is Nash Theorem staged
Replicator Dynamics Definition staged
Stable Game Framework (Hofbauer–Sandholm) Theorem staged
Wardrop Variational Characterization Proposition staged

Game Theory.Strategic Game.Equilibrium

Common Knowledge Can Filter Nash Equilibria Example staged
Dominant Strategy Profile is a Nash Equilibrium Theorem admitted
Epsilon Equilibrium Definition staged
Finite Nash Equilibrium Computation Examples Example staged
Kakutani From Two-Player Nash Existence Theorem staged
Mixed Nash Equilibrium Definition staged
Nash Equilibrium Definition admitted
Nash Existence For Finite Games Theorem proved
Nash Payoffs Are Individually Rational Proposition staged
Semi-Algebraic Mixed Nash Set Proposition staged
Strict Equilibrium Definition staged
Symmetric Mixed Equilibrium Theorem staged

Game Theory.Strategic Game.Refinements

Approximate Solution Definition staged
Approximate Solutions Are Reny Solutions Proposition staged
Better Reply Secure Game Definition staged
Epsilon Perfect Equilibrium Definition staged
Epsilon Proper Equilibrium Definition staged
Equilibrium Manifold Definition staged
Essential Equilibrium Component Definition staged
Existence Of Perfect Equilibrium Theorem staged
Existence Of Proper Equilibrium Theorem staged
Existence Of Reny Solutions Theorem staged
Generic Finite Odd Equilibria Theorem staged
Kohlberg Mertens Structure Theorem Theorem staged
Nash Existence In Better Reply Secure Games Theorem staged
Perfect Equilibrium Definition staged
Perfect Equilibrium And Undominated Equilibrium Proposition staged
Proper And Perfect Equilibrium Examples Example staged
Proper Equilibrium Definition staged
Reny Solution Definition staged
Strict Equilibrium Is Proper Proposition staged

Game Theory.Zero Sum

Antisymmetric Matrix Game Has Value Zero Theorem proved
Blackwell B-Set Approachability Theorem staged
Bracket Invariant For Admissible Sequences Lemma admitted
Calibrated Strategy Definition staged
Calibrated Strategy Exists Theorem staged
Cesàro Payoff Convergence From Robinson Lemma Lemma admitted
Compact Mixed Versus Finite-Support Minimax Proposition admitted
Continuous Fictitious Play Closes The Duality Gap Proposition admitted
Derived Game Definition admitted
Deterministic Blackwell Sequence Theorem staged
Diagonal Matrix Game Value Proposition proved
Directional Derivative Of The Value Proposition admitted
Duality Gap In A Matrix Game Definition formalized
Empirical Frequency Of Play Definition formalized
Epsilon-Optimal Strategy Definition formalized
Euclidean Division Pasting In Robinson Induction Lemma admitted
Existence of Optimal Mixed Strategies (Loomis Foundations) Theorem proved
Expected Payoff of a Matrix Game Definition formalized
External Regret Definition staged
Fictitious Play Definition formalized
Fictitious Play Convergence Theorem admitted
Finite-Opponent Separation Minimax Proposition admitted
General Mixed Minimax Theorem Theorem admitted
General Mixed Strategy Space Definition admitted
General Value Operator Definition admitted
General Value Operator Is Nonexpansive Proposition admitted
Hannan Set Definition staged
Internal Regret Definition staged
Intersection Lemma Lemma admitted
Markov Stationary Distribution as Zero-Sum Game Value Lemma admitted
Matching Pennies Example formalized
Matrix Game Definition formalized
Maximin and Minimax Values Definition formalized
Maximin is Bounded by Minimax Lemma proved
Mixed Extension Of A Matrix Game Definition formalized
Mixed Extension Pathology Example admitted
Mixed Nash Equilibrium of a Matrix Game Theorem proved
Mixed Strategy Simplex Definition formalized
Monotone Decreasing Values Limit Proposition admitted
Monotone Family Assumption Counterexamples Example admitted
Nash Payoff Uniqueness in Zero-Sum Games Theorem proved
No External Regret Converges To Hannan Set Theorem staged
No Internal Regret Converges To Correlated Equilibrium Theorem staged
Noisy Duel With Multiple Bullets Theorem admitted
Noisy One-Bullet Duel Value Proposition admitted
One-Sided Compact Convex Minimax Proposition admitted
Optimal Pairs Are Exactly Saddle Points Theorem proved
Optimal Strategy Sets Definition formalized
Optimal Strategy Sets Are Polytopes Proposition proved
Payoff Negation in Zero-Sum Games Lemma proved
Perron-Frobenius For Positive Matrices Theorem proved
Player Guarantee Definition formalized
Quasi-Concavity And Semicontinuity Definition admitted
Robinson Admissible Sequence Lemma Lemma admitted
Saddle Point Definition formalized
Silent One-Bullet Duel Has No Pure Value Proposition admitted
Silent Versus Noisy One-Bullet Duel Value Proposition admitted
Sion Boundary Counterexample Example admitted
Sion Minimax Theorem Theorem admitted
Sion-Wolfe Game Has No Mixed Value Example admitted
Stochastic Matrix Has An Invariant Distribution Theorem proved
Strict Domination And Never Best Response (via auxiliary zero-sum game) Proposition admitted
Strong Complementarity Theorem proved
Subgame Reduction For Non-Useful Indices Lemma admitted
Support Complementarity Theorem proved
Support Of A Mixed Strategy Definition formalized
Three-By-Two Matrix Game Computation Example formalized
Three-Player Minimax Failure Example formalized
Two-By-Two Value Formula Example formalized
Useful Window Bound For Admissible Sequences Lemma admitted
Value Of A Zero-Sum Game Definition formalized
Value Operator Properties Proposition admitted
Von Neumann Minimax Theorem Theorem proved
Weak Domination And Completely Mixed Tests (via auxiliary zero-sum game) Proposition admitted
Zero-Sum Game Definition formalized

Game Theory.Zero Sum.Applications

Blackwell B-Set Approachability Theorem staged
Deterministic Blackwell Sequence Theorem staged
Markov Stationary Distribution as Zero-Sum Game Value Lemma admitted
Perron-Frobenius For Positive Matrices Theorem proved
Stochastic Matrix Has An Invariant Distribution Theorem proved
Strict Domination And Never Best Response (via auxiliary zero-sum game) Proposition admitted
Weak Domination And Completely Mixed Tests (via auxiliary zero-sum game) Proposition admitted

Game Theory.Zero Sum.Continuous

Compact Mixed Versus Finite-Support Minimax Proposition admitted
Finite-Opponent Separation Minimax Proposition admitted
General Mixed Minimax Theorem Theorem admitted
General Mixed Strategy Space Definition admitted
Intersection Lemma Lemma admitted
Mixed Extension Pathology Example admitted
Monotone Decreasing Values Limit Proposition admitted
Monotone Family Assumption Counterexamples Example admitted
One-Sided Compact Convex Minimax Proposition admitted
Quasi-Concavity And Semicontinuity Definition admitted
Sion Boundary Counterexample Example admitted
Sion Minimax Theorem Theorem admitted
Sion-Wolfe Game Has No Mixed Value Example admitted

Game Theory.Zero Sum.Core

Antisymmetric Matrix Game Has Value Zero Theorem proved
Duality Gap In A Matrix Game Definition formalized
Epsilon-Optimal Strategy Definition formalized
Expected Payoff of a Matrix Game Definition formalized
Matrix Game Definition formalized
Mixed Extension Of A Matrix Game Definition formalized
Mixed Nash Equilibrium of a Matrix Game Theorem proved
Mixed Strategy Simplex Definition formalized
Optimal Pairs Are Exactly Saddle Points Theorem proved
Optimal Strategy Sets Definition formalized
Optimal Strategy Sets Are Polytopes Proposition proved
Payoff Negation in Zero-Sum Games Lemma proved
Player Guarantee Definition formalized
Saddle Point Definition formalized
Strong Complementarity Theorem proved
Support Complementarity Theorem proved
Support Of A Mixed Strategy Definition formalized
Value Of A Zero-Sum Game Definition formalized
Zero-Sum Game Definition formalized

Game Theory.Zero Sum.Examples

Diagonal Matrix Game Value Proposition proved
Matching Pennies Example formalized
Noisy Duel With Multiple Bullets Theorem admitted
Noisy One-Bullet Duel Value Proposition admitted
Silent One-Bullet Duel Has No Pure Value Proposition admitted
Silent Versus Noisy One-Bullet Duel Value Proposition admitted
Three-By-Two Matrix Game Computation Example formalized
Three-Player Minimax Failure Example formalized
Two-By-Two Value Formula Example formalized

Game Theory.Zero Sum.Learning

Bracket Invariant For Admissible Sequences Lemma admitted
Calibrated Strategy Definition staged
Calibrated Strategy Exists Theorem staged
Cesàro Payoff Convergence From Robinson Lemma Lemma admitted
Continuous Fictitious Play Closes The Duality Gap Proposition admitted
Empirical Frequency Of Play Definition formalized
Euclidean Division Pasting In Robinson Induction Lemma admitted
External Regret Definition staged
Fictitious Play Definition formalized
Fictitious Play Convergence Theorem admitted
Hannan Set Definition staged
Internal Regret Definition staged
No External Regret Converges To Hannan Set Theorem staged
No Internal Regret Converges To Correlated Equilibrium Theorem staged
Robinson Admissible Sequence Lemma Lemma admitted
Subgame Reduction For Non-Useful Indices Lemma admitted
Useful Window Bound For Admissible Sequences Lemma admitted

Game Theory.Zero Sum.Minimax

Existence of Optimal Mixed Strategies (Loomis Foundations) Theorem proved
Maximin and Minimax Values Definition formalized
Maximin is Bounded by Minimax Lemma proved
Nash Payoff Uniqueness in Zero-Sum Games Theorem proved
Von Neumann Minimax Theorem Theorem proved

Game Theory.Zero Sum.Operators

Derived Game Definition admitted
Directional Derivative Of The Value Proposition admitted
General Value Operator Definition admitted
General Value Operator Is Nonexpansive Proposition admitted
Value Operator Properties Proposition admitted

Market Design

Gale-Shapley Deferred Acceptance Algorithm Definition formalized
Gale-Shapley Theorem (Existence of Stable Matching) Theorem proved
Lattice Structure of Stable Matchings (Conway-Knuth) Theorem proved
Matching (Partial Bijection) Definition formalized
Matching Market (One-to-One) Definition formalized
Proposing-Side Optimal Stable Matching Theorem proved
Rural Hospitals Theorem Theorem proved
Stability (Individual Rationality + No Blocking Pair) Definition formalized
Strategy-Proofness of Gale-Shapley for the Proposing Side (Roth 1982) Theorem staged

Market Design.Matching

Gale-Shapley Deferred Acceptance Algorithm Definition formalized
Gale-Shapley Theorem (Existence of Stable Matching) Theorem proved
Lattice Structure of Stable Matchings (Conway-Knuth) Theorem proved
Matching (Partial Bijection) Definition formalized
Matching Market (One-to-One) Definition formalized
Proposing-Side Optimal Stable Matching Theorem proved
Rural Hospitals Theorem Theorem proved
Stability (Individual Rationality + No Blocking Pair) Definition formalized
Strategy-Proofness of Gale-Shapley for the Proposing Side (Roth 1982) Theorem staged

Market Design.Matching.One To One

Gale-Shapley Deferred Acceptance Algorithm Definition formalized
Gale-Shapley Theorem (Existence of Stable Matching) Theorem proved
Lattice Structure of Stable Matchings (Conway-Knuth) Theorem proved
Matching (Partial Bijection) Definition formalized
Matching Market (One-to-One) Definition formalized
Proposing-Side Optimal Stable Matching Theorem proved
Rural Hospitals Theorem Theorem proved
Stability (Individual Rationality + No Blocking Pair) Definition formalized
Strategy-Proofness of Gale-Shapley for the Proposing Side (Roth 1982) Theorem staged

Math

Antisymmetric Matrix Games Have Value Theorem proved
Base Case of Loomis Induction Lemma proved
Brouwer Fixed Point Theorem Theorem staged
Brouwer Fixed Point Theorem For A Simplex Theorem proved
Column-Drop Step of Loomis Induction Lemma proved
Common Guarantee Gives The Value Lemma proved
Continuity on the Real Standard Simplex Lemma proved
Convex Combination of Simplex Points Definition formalized
Direct Induction Proof Of Loomis Theorem Proof plan formalized
Existence of Loomis Optimisers Lemma proved
Farkas Lemma Theorem proved
Field-Generic Value Predicates Definition formalized
Fixed Point Theorem For Retracts Of A Simplex Lemma staged
Fourier-Motzkin Elimination Step Lemma proved
Iterated Weighted Sums Commute Lemma proved
Kakutani Fixed Point Theorem Theorem staged
Kakutani Fixed-Point Proof of the Minimax Theorem Proof plan admitted
LP Duality Proof Of Minimax Proof plan admitted
LP Optimum ↔ Game-Theoretic Optimal Strategy Theorem admitted
Loomis Theorem (Positive B) Theorem proved
Minimax From Antisymmetric Games Proof plan admitted
Minimax From Deterministic Approachability Proof plan admitted
Minimax via the All-Ones Specialization of Loomis Proof plan formalized
Ordered-Field Minimax Statement Theorem formalized
Player-1 LP Formulation of a Matrix Game Definition admitted
Player-2 LP Formulation of a Matrix Game Definition admitted
Point Mass on the Standard Simplex Definition formalized
Pointwise Bounds Are Simplex Bounds Lemma proved
Positive Aggregates xB and By Lemma proved
Row-Drop Step of Loomis Induction Lemma proved
Scarf Combinatorial Lemma (Colorful Room Existence) Lemma proved
Strong Complementarity Proposition proved
Strong Complementarity For Linear Programming Theorem proved
Strong Duality For Linear Programming Theorem proved
Sup-Inf Choice Function Identity Lemma staged
Tarski Fixed Point Theorem For Compact Euclidean Lattices Theorem staged
Theorem Of The Alternative Theorem proved
Ville Theorem Theorem admitted
Ville Theorem By Discretization Proof plan admitted
Weak Duality For Loomis Values Lemma proved
Weighted Sum over the Standard Simplex Definition formalized
Zero-Sum Linear Programming Bridge Proof plan admitted
Zero-Sum Nash Equilibria As Saddle Points Theorem proved

Math.Fixed Point

Brouwer Fixed Point Theorem Theorem staged
Brouwer Fixed Point Theorem For A Simplex Theorem proved
Fixed Point Theorem For Retracts Of A Simplex Lemma staged
Kakutani Fixed Point Theorem Theorem staged
Scarf Combinatorial Lemma (Colorful Room Existence) Lemma proved

Math.Lattice

Tarski Fixed Point Theorem For Compact Euclidean Lattices Theorem staged

Math.Linear Algebra

Farkas Lemma Theorem proved
Fourier-Motzkin Elimination Step Lemma proved
Theorem Of The Alternative Theorem proved

Math.Linear Algebra.Alternatives

Farkas Lemma Theorem proved
Fourier-Motzkin Elimination Step Lemma proved
Theorem Of The Alternative Theorem proved

Math.Linear Programming

LP Optimum ↔ Game-Theoretic Optimal Strategy Theorem admitted
Player-1 LP Formulation of a Matrix Game Definition admitted
Player-2 LP Formulation of a Matrix Game Definition admitted
Strong Complementarity For Linear Programming Theorem proved
Strong Duality For Linear Programming Theorem proved
Zero-Sum Linear Programming Bridge Proof plan admitted

Math.Linear Programming.Duality

Strong Complementarity For Linear Programming Theorem proved
Strong Duality For Linear Programming Theorem proved

Math.Linear Programming.Minimax Bridge

LP Optimum ↔ Game-Theoretic Optimal Strategy Theorem admitted
Player-1 LP Formulation of a Matrix Game Definition admitted
Player-2 LP Formulation of a Matrix Game Definition admitted
Zero-Sum Linear Programming Bridge Proof plan admitted

Math.Minimax

Antisymmetric Matrix Games Have Value Theorem proved
Base Case of Loomis Induction Lemma proved
Column-Drop Step of Loomis Induction Lemma proved
Common Guarantee Gives The Value Lemma proved
Direct Induction Proof Of Loomis Theorem Proof plan formalized
Existence of Loomis Optimisers Lemma proved
Field-Generic Value Predicates Definition formalized
Kakutani Fixed-Point Proof of the Minimax Theorem Proof plan admitted
LP Duality Proof Of Minimax Proof plan admitted
Loomis Theorem (Positive B) Theorem proved
Minimax From Antisymmetric Games Proof plan admitted
Minimax From Deterministic Approachability Proof plan admitted
Minimax via the All-Ones Specialization of Loomis Proof plan formalized
Ordered-Field Minimax Statement Theorem formalized
Positive Aggregates xB and By Lemma proved
Row-Drop Step of Loomis Induction Lemma proved
Strong Complementarity Proposition proved
Ville Theorem Theorem admitted
Ville Theorem By Discretization Proof plan admitted
Weak Duality For Loomis Values Lemma proved
Zero-Sum Nash Equilibria As Saddle Points Theorem proved

Math.Order

Sup-Inf Choice Function Identity Lemma staged

Math.Simplex

Continuity on the Real Standard Simplex Lemma proved
Convex Combination of Simplex Points Definition formalized
Iterated Weighted Sums Commute Lemma proved
Point Mass on the Standard Simplex Definition formalized
Pointwise Bounds Are Simplex Bounds Lemma proved
Weighted Sum over the Standard Simplex Definition formalized

Mechanism Design

All-Pay Auction Symmetric Equilibrium Theorem staged
Auction Comparisons Under Risk Aversion Theorem staged
Basic Auction Formats Definition formalized
Bayesian Mechanisms Definition formalized
Bayesian Selling Problem (IPV) Definition staged
Bayesian Single-Item Auction Framework Definition formalized
Bayesian Single-Item Auction Interim Quantities And IC Definition formalized
Bid-Profile Supports Definition formalized
Binary Knapsack Allocations Definition formalized
DSIC Predicate Definition formalized
Direct Mechanism Interface Definition formalized
Dutch ≡ First-Price Strategic Equivalence Theorem staged
English ≡ Second-Price IPV Equivalence Theorem staged
Entry Fees And Reserve Prices In IPV Auctions Theorem staged
Ex-Ante Equilibrium Predicates Definition formalized
Ex-Ante Expected Utility (Bayesian Mechanisms) Definition formalized
Ex-Ante Revelation Principle Interface Theorem proved
Ex-Post Individual Rationality Predicate Definition formalized
First-Price Fails DSIC Theorem proved
First-Price Mechanism Definition formalized
Induced Strategic Game Definition formalized
Knapsack Auction Environment Definition formalized
Knapsack Relaxations And Dynamic Programming Theorem proved
Mechanisms With Transfers Definition formalized
Multiple-Parameter Transfer Layer Definition formalized
Myerson Monotonicity Characterization Theorem proved
Myerson Optimal Auction Legacy Plan Proof plan staged
Myerson Payment Construction (withMyersonPayment) Definition formalized
Myerson Payment Envelope Lemmas Lemma proved
Myerson Payment Formula Definition formalized
Myerson Reserve-Price Characterisation Theorem staged
No Deterministic Constant Competitive Ratio Theorem proved
Online Single-Item (Posted-Price) Auction Definition formalized
Ordered-Bid Utilities Definition formalized
Regular Myerson Optimal Single-Item Auction Theorem proved
Reserve Second-Price Mechanism Definition formalized
Reserve Second-Price Truth-Telling Is Dominant Theorem proved
Revenue Equivalence Theorem Theorem staged
Sample-Then-Threshold Rule Is 1/4-Competitive Theorem proved
Second-Price (Vickrey) Mechanism Definition formalized
Single-Parameter Transfer Layer Definition formalized
Strict Value Comparison Breaks the Competitive Guarantee Example proved
Symmetric IPV First-Price Equilibrium Theorem staged
Truthful Bidding Is Dominant in the Online Auction Theorem proved
Truthfulness From DSIC Theorem proved
VCG Payment Identity Theorem proved
VCG Social Welfare Definition formalized
VCG Truthfulness And Individual Rationality Theorem proved
VCG Welfare And Payments Definition formalized
VCG Welfare Without Agent i Definition formalized
Vickrey Truth-Telling Is Dominant Theorem proved
Virtual Values and Regularity Definition formalized
Virtual-Surplus-Maximizing Allocation Definition formalized
Weak Value Comparison Degrades to 1/n on the Needle Profile Example proved
Welfare-Maximizing Knapsack Mechanism Theorem proved

Mechanism Design.Auction

All-Pay Auction Symmetric Equilibrium Theorem staged
Auction Comparisons Under Risk Aversion Theorem staged
Basic Auction Formats Definition formalized
Bayesian Single-Item Auction Framework Definition formalized
Bayesian Single-Item Auction Interim Quantities And IC Definition formalized
Bid-Profile Supports Definition formalized
Binary Knapsack Allocations Definition formalized
Dutch ≡ First-Price Strategic Equivalence Theorem staged
English ≡ Second-Price IPV Equivalence Theorem staged
Entry Fees And Reserve Prices In IPV Auctions Theorem staged
First-Price Fails DSIC Theorem proved
First-Price Mechanism Definition formalized
Knapsack Auction Environment Definition formalized
Knapsack Relaxations And Dynamic Programming Theorem proved
No Deterministic Constant Competitive Ratio Theorem proved
Online Single-Item (Posted-Price) Auction Definition formalized
Ordered-Bid Utilities Definition formalized
Regular Myerson Optimal Single-Item Auction Theorem proved
Reserve Second-Price Mechanism Definition formalized
Reserve Second-Price Truth-Telling Is Dominant Theorem proved
Sample-Then-Threshold Rule Is 1/4-Competitive Theorem proved
Second-Price (Vickrey) Mechanism Definition formalized
Strict Value Comparison Breaks the Competitive Guarantee Example proved
Symmetric IPV First-Price Equilibrium Theorem staged
Truthful Bidding Is Dominant in the Online Auction Theorem proved
Vickrey Truth-Telling Is Dominant Theorem proved
Virtual Values and Regularity Definition formalized
Virtual-Surplus-Maximizing Allocation Definition formalized
Weak Value Comparison Degrades to 1/n on the Needle Profile Example proved
Welfare-Maximizing Knapsack Mechanism Theorem proved

Mechanism Design.Auction.Basic

Basic Auction Formats Definition formalized
Bid-Profile Supports Definition formalized
First-Price Fails DSIC Theorem proved
First-Price Mechanism Definition formalized
Ordered-Bid Utilities Definition formalized
Reserve Second-Price Mechanism Definition formalized
Reserve Second-Price Truth-Telling Is Dominant Theorem proved
Second-Price (Vickrey) Mechanism Definition formalized
Vickrey Truth-Telling Is Dominant Theorem proved

Mechanism Design.Auction.Bayesian

All-Pay Auction Symmetric Equilibrium Theorem staged
Auction Comparisons Under Risk Aversion Theorem staged
Bayesian Single-Item Auction Framework Definition formalized
Bayesian Single-Item Auction Interim Quantities And IC Definition formalized
Dutch ≡ First-Price Strategic Equivalence Theorem staged
English ≡ Second-Price IPV Equivalence Theorem staged
Entry Fees And Reserve Prices In IPV Auctions Theorem staged
Regular Myerson Optimal Single-Item Auction Theorem proved
Symmetric IPV First-Price Equilibrium Theorem staged
Virtual Values and Regularity Definition formalized
Virtual-Surplus-Maximizing Allocation Definition formalized

Mechanism Design.Auction.Knapsack

Binary Knapsack Allocations Definition formalized
Knapsack Auction Environment Definition formalized
Knapsack Relaxations And Dynamic Programming Theorem proved
Welfare-Maximizing Knapsack Mechanism Theorem proved

Mechanism Design.Auction.Online

No Deterministic Constant Competitive Ratio Theorem proved
Online Single-Item (Posted-Price) Auction Definition formalized
Sample-Then-Threshold Rule Is 1/4-Competitive Theorem proved
Strict Value Comparison Breaks the Competitive Guarantee Example proved
Truthful Bidding Is Dominant in the Online Auction Theorem proved
Weak Value Comparison Degrades to 1/n on the Needle Profile Example proved

Mechanism Design.Basic

DSIC Predicate Definition formalized
Direct Mechanism Interface Definition formalized
Ex-Post Individual Rationality Predicate Definition formalized
Induced Strategic Game Definition formalized
Truthfulness From DSIC Theorem proved

Mechanism Design.Bayesian

Bayesian Mechanisms Definition formalized
Bayesian Selling Problem (IPV) Definition staged
Ex-Ante Equilibrium Predicates Definition formalized
Ex-Ante Expected Utility (Bayesian Mechanisms) Definition formalized
Ex-Ante Revelation Principle Interface Theorem proved

Mechanism Design.Myerson

Myerson Monotonicity Characterization Theorem proved
Myerson Optimal Auction Legacy Plan Proof plan staged
Myerson Payment Construction (withMyersonPayment) Definition formalized
Myerson Payment Envelope Lemmas Lemma proved
Myerson Payment Formula Definition formalized
Myerson Reserve-Price Characterisation Theorem staged
Regular Myerson Optimal Single-Item Auction Theorem proved
Revenue Equivalence Theorem Theorem staged
Virtual Values and Regularity Definition formalized
Virtual-Surplus-Maximizing Allocation Definition formalized

Mechanism Design.Transfer

Mechanisms With Transfers Definition formalized
Multiple-Parameter Transfer Layer Definition formalized
Single-Parameter Transfer Layer Definition formalized

Mechanism Design.Vcg

VCG Payment Identity Theorem proved
VCG Social Welfare Definition formalized
VCG Truthfulness And Individual Rationality Theorem proved
VCG Welfare And Payments Definition formalized
VCG Welfare Without Agent i Definition formalized

Social Choice

Acyclic Envy Graph Has a Source Theorem staged
Additive Valuation Definition formalized
Allocation Definition formalized
Arrow's Impossibility Theorem Theorem staged
Arrow's Theorem via Decisive Coalitions Theorem staged
Basic Welfare Lemmas Lemma staged
Best-Good Selection Definition formalized
Borda Score and Borda Rule Definition formalized
Bundle Rotation Definition formalized
CDF of a Non-Atomic Finite Measure on ℝ Is Continuous Lemma staged
Cake Valuation Definition formalized
Cardinal Fair-Division Instance Definition formalized
Cardinal-Instance Fairness and Welfare Wrappers Definition formalized
Chooser Is Always Envy-Free Theorem staged
Coalition Contraction — Splitting a Decisive Coalition Theorem staged
Condorcet Paradox Theorem staged
Condorcet Winner Definition formalized
Cut-and-Choose Allocation and Fair Cut Point Definition formalized
Cut-and-Choose Is Envy-Free at a Fair Cut Theorem staged
Cut-and-Choose Output Is a Complete Partition Theorem staged
Cutter Does Not Envy at a Fair Cut Theorem staged
Decidable Fairness Checkers Theorem staged
Decisive Coalition and Dictator Definition formalized
Decisive Coalition for an Ordered Pair Definition formalized
Dictatorial Social Choice Function Definition formalized
Dictatorial Social Welfare Function Definition formalized
Divisible Allocation Definition formalized
Divisible Cardinal Instance Definition formalized
Divisible Envy-Free, Proportional, Equitable Predicates Definition formalized
Divisible Measure Instance Definition formalized
Divisible Ordinal Instance Definition formalized
Dubins–Spanier Inductive Step Lemma staged
Dubins–Spanier Proportional Existence Theorem staged
Dubins–Spanier as a Rule on Measure Instances Theorem staged
EF + Proportional Existence (Stromquist Corollary) Theorem staged
EF Impossibility — Two Agents, One Good Theorem staged
EF ⇒ EFX (Monotone Valuations) Theorem staged
EF ⇒ PROP (Additive Valuations, Complete Allocations) Theorem staged
EF ⇒ Proportional (Measure Valuations) Theorem staged
EF1 — Envy-Free Up to One Good Definition formalized
EFX Existence — 2 Agents, 2 Goods Theorem staged
EFX Existence — Two Agents, Any Finite Good Set Theorem staged
EFX from No-Envy + Monotonicity Theorem staged
EFX from a Singleton-Bundle Sufficient Condition Lemma staged
EFX — Envy-Free Up to Any Good Definition formalized
EFX ⇒ EF1 Theorem staged
Egalitarian (Maximin) Welfare Definition formalized
Egalitarian Welfare Lower-Bounds Utilitarian Welfare Lemma staged
Eliminate All Envy Cycles Definition formalized
Envy Cycle Definition formalized
Envy Relation and Sources Definition formalized
Envy-Cycle Elimination Algorithm Definition formalized
Envy-Cycle Elimination Produces EF1 Theorem staged
Envy-Free Allocation Definition formalized
Envy-Free Existence (Stromquist, n Agents) Theorem staged
Equitable Allocation Definition formalized
Fair Assignment from a Common KKM Point Lemma staged
Fair Cut Point Exists Theorem staged
Fair Division Instance Definition formalized
Fair Division Solution Concept and Rule Definition formalized
Field Expansion — Decisive on One Pair Implies Decisive Everywhere Theorem staged
Gibbard–Satterthwaite Theorem Theorem staged
Grand Coalition Is Decisive under Unanimity Theorem staged
IIA on Strict Preference Lemma staged
IVT — Cut Point Exists for Non-Atomic Measures on [0,1] Lemma staged
Independence of Irrelevant Alternatives Definition formalized
Indivisible Additive Instance Definition formalized
Indivisible Allocation Definition formalized
Indivisible Cardinal Instance Definition formalized
Indivisible Egalitarian (Maximin) Welfare Definition formalized
Indivisible Envy-Free Definition formalized
Indivisible Equitable Definition formalized
Indivisible Ordinal Instance Definition formalized
Indivisible Pareto Optimal Definition formalized
Indivisible Proportional Definition formalized
Indivisible Utilitarian Welfare Definition formalized
Indivisible Valuation Definition formalized
IsMaxminShare ↔ IsAlphaMMS 1 Theorem staged
MMS Value — Basic Bounds Lemma staged
Maximin Share (MMS) Allocation Definition formalized
Maximin Share Value Definition formalized
Measure Valuation Definition formalized
Measure-Instance EF ↔ Real-Valued Cardinal EF Theorem staged
Measure-Instance Existence Wrappers Theorem staged
Minimal Decisive Coalition Has Size One Theorem staged
Monotonic Social Choice Function Definition formalized
Muller–Satterthwaite Theorem Theorem staged
Non-Atomicity Is Preserved by Subtype.val Pushforward Lemma staged
Normalized Measure Valuation ↔ Probability Measure Lemma staged
PROP ⇒ MMS (Additive Valuations, Complete Allocations) Theorem staged
PROP ⇒ α-MMS (Additive Valuations) Theorem staged
Pairwise Majority Comparison Definition formalized
Pareto Optimal Allocation Definition formalized
Pareto-Domination Count Termination Measure Definition formalized
Piece-Value Function Is Continuous on the Division Simplex Lemma staged
Plurality Score and Plurality Rule Definition formalized
Preference Profile Definition formalized
Preference Relation Definition formalized
Proportional Allocation Definition formalized
Proportional Existence on [0,1] (n Agents) Theorem staged
Round-Robin Allocation Definition formalized
Round-Robin Is EF1 Theorem staged
Round-Robin Output Is a Complete Partition Theorem staged
Share Instance (No-Externality Model) Definition formalized
Social Choice Function Definition formalized
Social Choice Instance Definition formalized
Social Welfare Function Definition formalized
Solution Concept, Rule, and Correspondence Definition formalized
Strategy-Proof Social Choice Function Definition formalized
Strategy-Proof ⇒ Monotonic Theorem staged
Strict Preference Definition formalized
Stromquist Agent-Preference Union U(i) Definition formalized
Stromquist Pieces from the Division Simplex Definition formalized
Stromquist Preference Sets A(i, j) Definition formalized
Stromquist Shifted-Cell Approximation Definition staged
Stromquist Unique-Preference Sets B(i, j) Definition formalized
Stromquist — Unusual Case (Shifted-Cell Limit) Theorem staged
Stromquist — Usual Case (U Covers the Simplex) Theorem staged
Two-Agent EF Existence via Cut-and-Choose Theorem staged
Unanimity (Pareto Axiom) Definition formalized
Utilitarian Welfare and Utilitarian Optimality Definition formalized
Utility Represents Share Preference Definition formalized
Weakly Decisive Coalition Definition formalized
α-MMS Allocation Definition formalized
α-MMS — Monotonicity and Endpoint Lemmas Theorem staged

Social Choice.Fair Division

Acyclic Envy Graph Has a Source Theorem staged
Additive Valuation Definition formalized
Allocation Definition formalized
Basic Welfare Lemmas Lemma staged
Best-Good Selection Definition formalized
Bundle Rotation Definition formalized
CDF of a Non-Atomic Finite Measure on ℝ Is Continuous Lemma staged
Cake Valuation Definition formalized
Cardinal Fair-Division Instance Definition formalized
Cardinal-Instance Fairness and Welfare Wrappers Definition formalized
Chooser Is Always Envy-Free Theorem staged
Cut-and-Choose Allocation and Fair Cut Point Definition formalized
Cut-and-Choose Is Envy-Free at a Fair Cut Theorem staged
Cut-and-Choose Output Is a Complete Partition Theorem staged
Cutter Does Not Envy at a Fair Cut Theorem staged
Decidable Fairness Checkers Theorem staged
Divisible Allocation Definition formalized
Divisible Cardinal Instance Definition formalized
Divisible Envy-Free, Proportional, Equitable Predicates Definition formalized
Divisible Measure Instance Definition formalized
Divisible Ordinal Instance Definition formalized
Dubins–Spanier Inductive Step Lemma staged
Dubins–Spanier Proportional Existence Theorem staged
Dubins–Spanier as a Rule on Measure Instances Theorem staged
EF + Proportional Existence (Stromquist Corollary) Theorem staged
EF Impossibility — Two Agents, One Good Theorem staged
EF ⇒ EFX (Monotone Valuations) Theorem staged
EF ⇒ PROP (Additive Valuations, Complete Allocations) Theorem staged
EF ⇒ Proportional (Measure Valuations) Theorem staged
EF1 — Envy-Free Up to One Good Definition formalized
EFX Existence — 2 Agents, 2 Goods Theorem staged
EFX Existence — Two Agents, Any Finite Good Set Theorem staged
EFX from No-Envy + Monotonicity Theorem staged
EFX from a Singleton-Bundle Sufficient Condition Lemma staged
EFX — Envy-Free Up to Any Good Definition formalized
EFX ⇒ EF1 Theorem staged
Egalitarian (Maximin) Welfare Definition formalized
Egalitarian Welfare Lower-Bounds Utilitarian Welfare Lemma staged
Eliminate All Envy Cycles Definition formalized
Envy Cycle Definition formalized
Envy Relation and Sources Definition formalized
Envy-Cycle Elimination Algorithm Definition formalized
Envy-Cycle Elimination Produces EF1 Theorem staged
Envy-Free Allocation Definition formalized
Envy-Free Existence (Stromquist, n Agents) Theorem staged
Equitable Allocation Definition formalized
Fair Assignment from a Common KKM Point Lemma staged
Fair Cut Point Exists Theorem staged
Fair Division Instance Definition formalized
Fair Division Solution Concept and Rule Definition formalized
IVT — Cut Point Exists for Non-Atomic Measures on [0,1] Lemma staged
Indivisible Additive Instance Definition formalized
Indivisible Allocation Definition formalized
Indivisible Cardinal Instance Definition formalized
Indivisible Egalitarian (Maximin) Welfare Definition formalized
Indivisible Envy-Free Definition formalized
Indivisible Equitable Definition formalized
Indivisible Ordinal Instance Definition formalized
Indivisible Pareto Optimal Definition formalized
Indivisible Proportional Definition formalized
Indivisible Utilitarian Welfare Definition formalized
Indivisible Valuation Definition formalized
IsMaxminShare ↔ IsAlphaMMS 1 Theorem staged
MMS Value — Basic Bounds Lemma staged
Maximin Share (MMS) Allocation Definition formalized
Maximin Share Value Definition formalized
Measure Valuation Definition formalized
Measure-Instance EF ↔ Real-Valued Cardinal EF Theorem staged
Measure-Instance Existence Wrappers Theorem staged
Non-Atomicity Is Preserved by Subtype.val Pushforward Lemma staged
Normalized Measure Valuation ↔ Probability Measure Lemma staged
PROP ⇒ MMS (Additive Valuations, Complete Allocations) Theorem staged
PROP ⇒ α-MMS (Additive Valuations) Theorem staged
Pareto Optimal Allocation Definition formalized
Pareto-Domination Count Termination Measure Definition formalized
Piece-Value Function Is Continuous on the Division Simplex Lemma staged
Proportional Allocation Definition formalized
Proportional Existence on [0,1] (n Agents) Theorem staged
Round-Robin Allocation Definition formalized
Round-Robin Is EF1 Theorem staged
Round-Robin Output Is a Complete Partition Theorem staged
Share Instance (No-Externality Model) Definition formalized
Stromquist Agent-Preference Union U(i) Definition formalized
Stromquist Pieces from the Division Simplex Definition formalized
Stromquist Preference Sets A(i, j) Definition formalized
Stromquist Shifted-Cell Approximation Definition staged
Stromquist Unique-Preference Sets B(i, j) Definition formalized
Stromquist — Unusual Case (Shifted-Cell Limit) Theorem staged
Stromquist — Usual Case (U Covers the Simplex) Theorem staged
Two-Agent EF Existence via Cut-and-Choose Theorem staged
Utilitarian Welfare and Utilitarian Optimality Definition formalized
Utility Represents Share Preference Definition formalized
α-MMS Allocation Definition formalized
α-MMS — Monotonicity and Endpoint Lemmas Theorem staged

Social Choice.Fair Division.Core

Allocation Definition formalized
Basic Welfare Lemmas Lemma staged
Cardinal Fair-Division Instance Definition formalized
Cardinal-Instance Fairness and Welfare Wrappers Definition formalized
Egalitarian (Maximin) Welfare Definition formalized
Egalitarian Welfare Lower-Bounds Utilitarian Welfare Lemma staged
Envy-Free Allocation Definition formalized
Equitable Allocation Definition formalized
Fair Division Instance Definition formalized
Fair Division Solution Concept and Rule Definition formalized
Pareto Optimal Allocation Definition formalized
Proportional Allocation Definition formalized
Share Instance (No-Externality Model) Definition formalized
Utilitarian Welfare and Utilitarian Optimality Definition formalized
Utility Represents Share Preference Definition formalized

Social Choice.Fair Division.Divisible

CDF of a Non-Atomic Finite Measure on ℝ Is Continuous Lemma staged
Cake Valuation Definition formalized
Chooser Is Always Envy-Free Theorem staged
Cut-and-Choose Allocation and Fair Cut Point Definition formalized
Cut-and-Choose Is Envy-Free at a Fair Cut Theorem staged
Cut-and-Choose Output Is a Complete Partition Theorem staged
Cutter Does Not Envy at a Fair Cut Theorem staged
Divisible Allocation Definition formalized
Divisible Cardinal Instance Definition formalized
Divisible Envy-Free, Proportional, Equitable Predicates Definition formalized
Divisible Measure Instance Definition formalized
Divisible Ordinal Instance Definition formalized
Dubins–Spanier Inductive Step Lemma staged
Dubins–Spanier Proportional Existence Theorem staged
Dubins–Spanier as a Rule on Measure Instances Theorem staged
EF + Proportional Existence (Stromquist Corollary) Theorem staged
EF ⇒ Proportional (Measure Valuations) Theorem staged
Envy-Free Existence (Stromquist, n Agents) Theorem staged
Fair Assignment from a Common KKM Point Lemma staged
Fair Cut Point Exists Theorem staged
IVT — Cut Point Exists for Non-Atomic Measures on [0,1] Lemma staged
Measure Valuation Definition formalized
Measure-Instance EF ↔ Real-Valued Cardinal EF Theorem staged
Measure-Instance Existence Wrappers Theorem staged
Non-Atomicity Is Preserved by Subtype.val Pushforward Lemma staged
Normalized Measure Valuation ↔ Probability Measure Lemma staged
Piece-Value Function Is Continuous on the Division Simplex Lemma staged
Proportional Existence on [0,1] (n Agents) Theorem staged
Stromquist Agent-Preference Union U(i) Definition formalized
Stromquist Pieces from the Division Simplex Definition formalized
Stromquist Preference Sets A(i, j) Definition formalized
Stromquist Shifted-Cell Approximation Definition staged
Stromquist Unique-Preference Sets B(i, j) Definition formalized
Stromquist — Unusual Case (Shifted-Cell Limit) Theorem staged
Stromquist — Usual Case (U Covers the Simplex) Theorem staged
Two-Agent EF Existence via Cut-and-Choose Theorem staged

Social Choice.Fair Division.Divisible.Cut And Choose

Chooser Is Always Envy-Free Theorem staged
Cut-and-Choose Allocation and Fair Cut Point Definition formalized
Cut-and-Choose Is Envy-Free at a Fair Cut Theorem staged
Cut-and-Choose Output Is a Complete Partition Theorem staged
Cutter Does Not Envy at a Fair Cut Theorem staged
Fair Cut Point Exists Theorem staged
Two-Agent EF Existence via Cut-and-Choose Theorem staged

Social Choice.Fair Division.Divisible.Dubins Spanier

Dubins–Spanier Inductive Step Lemma staged
Dubins–Spanier Proportional Existence Theorem staged
Dubins–Spanier as a Rule on Measure Instances Theorem staged
IVT — Cut Point Exists for Non-Atomic Measures on [0,1] Lemma staged

Social Choice.Fair Division.Divisible.Stromquist

Envy-Free Existence (Stromquist, n Agents) Theorem staged
Fair Assignment from a Common KKM Point Lemma staged
Piece-Value Function Is Continuous on the Division Simplex Lemma staged
Stromquist Agent-Preference Union U(i) Definition formalized
Stromquist Pieces from the Division Simplex Definition formalized
Stromquist Preference Sets A(i, j) Definition formalized
Stromquist Shifted-Cell Approximation Definition staged
Stromquist Unique-Preference Sets B(i, j) Definition formalized
Stromquist — Unusual Case (Shifted-Cell Limit) Theorem staged
Stromquist — Usual Case (U Covers the Simplex) Theorem staged

Social Choice.Fair Division.Indivisible

Acyclic Envy Graph Has a Source Theorem staged
Additive Valuation Definition formalized
Best-Good Selection Definition formalized
Bundle Rotation Definition formalized
Decidable Fairness Checkers Theorem staged
EF Impossibility — Two Agents, One Good Theorem staged
EF ⇒ EFX (Monotone Valuations) Theorem staged
EF ⇒ PROP (Additive Valuations, Complete Allocations) Theorem staged
EF1 — Envy-Free Up to One Good Definition formalized
EFX Existence — 2 Agents, 2 Goods Theorem staged
EFX Existence — Two Agents, Any Finite Good Set Theorem staged
EFX from No-Envy + Monotonicity Theorem staged
EFX from a Singleton-Bundle Sufficient Condition Lemma staged
EFX — Envy-Free Up to Any Good Definition formalized
EFX ⇒ EF1 Theorem staged
Eliminate All Envy Cycles Definition formalized
Envy Cycle Definition formalized
Envy Relation and Sources Definition formalized
Envy-Cycle Elimination Algorithm Definition formalized
Envy-Cycle Elimination Produces EF1 Theorem staged
Indivisible Additive Instance Definition formalized
Indivisible Allocation Definition formalized
Indivisible Cardinal Instance Definition formalized
Indivisible Egalitarian (Maximin) Welfare Definition formalized
Indivisible Envy-Free Definition formalized
Indivisible Equitable Definition formalized
Indivisible Ordinal Instance Definition formalized
Indivisible Pareto Optimal Definition formalized
Indivisible Proportional Definition formalized
Indivisible Utilitarian Welfare Definition formalized
Indivisible Valuation Definition formalized
IsMaxminShare ↔ IsAlphaMMS 1 Theorem staged
MMS Value — Basic Bounds Lemma staged
Maximin Share (MMS) Allocation Definition formalized
Maximin Share Value Definition formalized
PROP ⇒ MMS (Additive Valuations, Complete Allocations) Theorem staged
PROP ⇒ α-MMS (Additive Valuations) Theorem staged
Pareto-Domination Count Termination Measure Definition formalized
Round-Robin Allocation Definition formalized
Round-Robin Is EF1 Theorem staged
Round-Robin Output Is a Complete Partition Theorem staged
α-MMS Allocation Definition formalized
α-MMS — Monotonicity and Endpoint Lemmas Theorem staged

Social Choice.Fair Division.Indivisible.Algorithms

Acyclic Envy Graph Has a Source Theorem staged
Best-Good Selection Definition formalized
Bundle Rotation Definition formalized
Eliminate All Envy Cycles Definition formalized
Envy Cycle Definition formalized
Envy Relation and Sources Definition formalized
Envy-Cycle Elimination Algorithm Definition formalized
Envy-Cycle Elimination Produces EF1 Theorem staged
Pareto-Domination Count Termination Measure Definition formalized
Round-Robin Allocation Definition formalized
Round-Robin Is EF1 Theorem staged
Round-Robin Output Is a Complete Partition Theorem staged

Social Choice.Fair Division.Indivisible.Mms

IsMaxminShare ↔ IsAlphaMMS 1 Theorem staged
MMS Value — Basic Bounds Lemma staged
Maximin Share (MMS) Allocation Definition formalized
Maximin Share Value Definition formalized
PROP ⇒ MMS (Additive Valuations, Complete Allocations) Theorem staged
PROP ⇒ α-MMS (Additive Valuations) Theorem staged
α-MMS Allocation Definition formalized
α-MMS — Monotonicity and Endpoint Lemmas Theorem staged

Social Choice.Voting

Arrow's Impossibility Theorem Theorem staged
Arrow's Theorem via Decisive Coalitions Theorem staged
Borda Score and Borda Rule Definition formalized
Coalition Contraction — Splitting a Decisive Coalition Theorem staged
Condorcet Paradox Theorem staged
Condorcet Winner Definition formalized
Decisive Coalition and Dictator Definition formalized
Decisive Coalition for an Ordered Pair Definition formalized
Dictatorial Social Choice Function Definition formalized
Dictatorial Social Welfare Function Definition formalized
Field Expansion — Decisive on One Pair Implies Decisive Everywhere Theorem staged
Gibbard–Satterthwaite Theorem Theorem staged
Grand Coalition Is Decisive under Unanimity Theorem staged
IIA on Strict Preference Lemma staged
Independence of Irrelevant Alternatives Definition formalized
Minimal Decisive Coalition Has Size One Theorem staged
Monotonic Social Choice Function Definition formalized
Muller–Satterthwaite Theorem Theorem staged
Pairwise Majority Comparison Definition formalized
Plurality Score and Plurality Rule Definition formalized
Social Choice Function Definition formalized
Social Welfare Function Definition formalized
Strategy-Proof Social Choice Function Definition formalized
Strategy-Proof ⇒ Monotonic Theorem staged
Unanimity (Pareto Axiom) Definition formalized
Weakly Decisive Coalition Definition formalized

Social Choice.Voting.Arrow

Arrow's Impossibility Theorem Theorem staged
Arrow's Theorem via Decisive Coalitions Theorem staged
Coalition Contraction — Splitting a Decisive Coalition Theorem staged
Decisive Coalition and Dictator Definition formalized
Decisive Coalition for an Ordered Pair Definition formalized
Field Expansion — Decisive on One Pair Implies Decisive Everywhere Theorem staged
Grand Coalition Is Decisive under Unanimity Theorem staged
IIA on Strict Preference Lemma staged
Minimal Decisive Coalition Has Size One Theorem staged
Weakly Decisive Coalition Definition formalized

Social Choice.Voting.Gibbard Satterthwaite

Gibbard–Satterthwaite Theorem Theorem staged
Muller–Satterthwaite Theorem Theorem staged
Strategy-Proof ⇒ Monotonic Theorem staged

Social Choice.Voting.Rules

Borda Score and Borda Rule Definition formalized
Condorcet Paradox Theorem staged
Condorcet Winner Definition formalized
Pairwise Majority Comparison Definition formalized
Plurality Score and Plurality Rule Definition formalized