In auction theory and mechanism design, Border's theorem gives a necessary and sufficient condition for interim allocation rules (or reduced form auctions) to be implementable via an auction. It was first proven by Kim Border in 1991, expanding on work from Steven Matthews, Eric Maskin and John Riley. A similar version with different hypotheses was proven by Border in 2007. Preliminaries. Auctions. Auctions are a mechanism designed to allocate an indivisible good among formula_1 bidders with private valuation for the good – that is, when the auctioneer has incomplete information on the bidders' true valuation and each bidder knows only their own valuation. Formally, this uncertainty is represented by a family of probability spaces formula_2 for each bidder formula_3, in which each formula_4 represents a possible type (valuation) for bidder formula_5 to have, formula_6 denotes a σ-algebra on formula_7, and formula_8 a prior and common knowledge probability distribution on formula_7, which assigns the probability formula_10 that a bidder formula_5 is of type formula_12. Finally, we define formula_13 as the set of type profiles, and formula_14 the set of profiles formula_15. Bidders simultaneously report their valuation of the good, and an auction assigns a probability that they will receive it. In this setting, an auction is thus a function formula_16 satisfying, for every type profile formula_17 formula_18 where formula_19 is the formula_5-th component of formula_21. Intuitively, this only means that the probability that some bidder will receive the good is no greater than 1. Interim allocation rules (reduced form auctions). From the point of view of each bidder formula_5, every auction formula_23 induces some expected probability that they will win the good given their type, which we can compute as formula_24 where formula_25 is conditional probability of other bidders having profile type formula_26 given that bidder formula_5 is of type formula_12. We refer to such probabilites formula_29 as "interim allocation rules", as they give the probability of winning the auction in the "interim" period: after each player knowing their own type, but before the knowing the type of other bidders. The function formula_30 defined by formula_31 is often referred to as a "reduced form auction". Working with reduced form auctions is often much more analytically tractable for revenue maximization. Implementability. Taken on its own, an allocation rule formula_32 is called "implementable" if there exists an auction formula_33 such that formula_24 for every bidder formula_5 and type formula_4. Statement. Border proved two main versions of the theorem, with different restrictions on the auction environment. i.i.d environment. The auction environment is i.i.d if the probability spaces formula_37 are the same for every bidder formula_5, and types formula_12 are independent. In this case, one only needs to consider symmetric auctions, and thus formula_40 also becomes the same for every formula_5. Border's theorem in this setting thus states: Proposition: An interim allocation rule formula_42 is implementable by a symmetric auction if and only if for each measurable set of types formula_43, one has the inequality formula_44 Intuitively, the left-hand side represents the probability that the winner of the auction is of some type formula_45, and the right-hand side represents the probability that "there exists" some bidder with type formula_45. The fact that the inequality is necessary for implementability is intuitive; it being sufficient means that this inequality fully characterizes implementable auctions, and represents the strength of the theorem. Finite sets of types. If all the sets formula_7 are finite, the restriction to the i.i.d case can be dropped. In the more general environment developed above, Border thus proved: Proposition: An interim allocation rule formula_48 is implementable by an auction if and only if for each measurable sets of types formula_49, one has the inequality formula_50 The intuition of the i.i.d case remains: the left-hand side represents the probability that the winner of the auction is some bidder formula_5 with type formula_52, and the right-hand side represents the probability that "there exists" some bidder formula_5 with type formula_52. Once again, the strength of the result comes from it being sufficient to characterize implementable interim allocation rules.