The OR Formalization Drive

When is the auctioneer's revenue acceptable?

The Vickrey-Clarke-Groves auction is the textbook mechanism for selling several objects at once: bidders report valuations for bundles, the auctioneer computes the welfare-maximizing allocation, and each winner pays the externality it imposes on the others. Truthful bidding is a dominant strategy and the outcome is efficient. Yet Ausubel and Milgrom (2006) catalogued its practical defects: revenue can be zero when the objects are valuable, revenue can fall when bidders or bids are added, losing bidders can profit by colluding, and a bidder can profit from false identities. Chapter 15 of Snyder and Shen's Fundamentals of Supply Chain Theory (2019) reproduces those examples and then gives the cooperative-game answer to when they cannot occur: the VCG payoff vector should lie in the core, the set of outcomes no coalition of auctioneer and bidders can improve upon, and it does so for every set of participants exactly when the coalitional value function is bidder-submodular. This mission formalizes that characterization, Theorem 15.3, together with the lemma and theorem leading to it.

Setting

Players are the auctioneer $0$ and bidders $1, \dots, n$. A coalitional value function $V$ assigns to each coalition $T$ the value it can create by trading among themselves: $0$ if the auctioneer, who owns the objects, is not in $T$, and otherwise the optimal value of the auctioneer's allocation problem among the bidders of $T$, each bidder receiving at most one bundle and bundles disjoint (capValue). Two properties of $V$ are all the theory uses: coalitions without the auctioneer are worthless, and adding players never lowers the value (IsCoalitionalValue).

A payoff vector $\pi$ gives each player a payoff. It lies in the core of the game on a coalition $S \ni 0$ (InCore V S π) if the payoffs of $S$ sum to $V(S)$ and no sub-coalition $T \subseteq S$ is paid less than $V(T)$. The VCG payoff vector $\bar\pi(S)$ (vcgPayoff) pays each bidder $k$ its marginal contribution $V(S) - V(S \setminus k)$, which is its valuation minus its VCG payment, and the auctioneer the remainder. A core vector is bidder dominant (BidderDominant) if every bidder weakly prefers it to every other core vector. $V$ is bidder-submodular (BidderSubmodular) if each bidder's marginal contribution weakly decreases as the coalition grows.

Formalization targets

Goal: Theorem 15.3

For a coalitional value function $V$, the following are equivalent: (i) $V$ is bidder-submodular; (ii) for every coalition $S \ni 0$ the core equals $\Pi_S = \{\pi : \sum_{k \in S}\pi_k = V(S),\ 0 \le \pi_k \le \bar\pi_k(S)\ \forall k \in S \setminus 0\}$; (iii) for every coalition $S \ni 0$, $\bar\pi(S)$ lies in the core of $S$. This is vcg_core_characterization.

Supporting targets

That the combinatorial auction's $V$ is a coalitional value function; Lemma 15.1, the core is nonempty and each bidder's VCG payoff is the largest it receives at any core point; Theorem 15.2, the VCG vector is the bidder-dominant core point when it is in the core, and otherwise no bidder-dominant point exists and the auctioneer's VCG payoff is below every core payoff.

The English auction of Sect. 15.2, presented as a primal-dual interpretation of a linear program, and the combinatorial allocation problem of Sect. 15.3 carry no numbered results and are not targets.

Significance

Theorem 15.3 is the criterion an auction designer can check before running a VCG auction: when the bidders' valuations make $V$ bidder-submodular (for instance when objects are substitutes), the VCG outcome is a competitive outcome, its revenue meets the core benchmark, and none of the defects of Sect. 15.4.2 can arise; when they do not, Theorem 15.2 says the auctioneer's revenue is strictly below every competitive outcome. The result underlies the ascending package auctions proposed as VCG alternatives and the procurement auctions used in supply chains, such as the combinatorial reverse auctions of the chapter's case study.

None of these results has a machine-checked proof. The book proves all three. The formal treatment of the core and of marginal-contribution vectors is reusable for the cooperative-game models of cost allocation in supply chains.

Difficulty

The theorems are combinatorial statements about a function on finite sets, and the difficulty is entirely in the bookkeeping of coalitions. Lemma 15.1 needs the explicit core vector of its proof to be verified against every sub-coalition, which splits into cases on whether the sub-coalition contains the auctioneer and the distinguished bidder. The implication (i) $\Rightarrow$ (ii) telescopes marginal contributions along a chain of coalitions between a sub-coalition and $S$, and the chain has to be built and its sum computed. The implication (iii) $\Rightarrow$ (i) is the delicate one: a failure of submodularity is a pair of nested coalitions, and the proof needs to extract from it a single-element step at which a bidder's marginal contribution increases, then show the two-bidder sub-coalition blocks the VCG vector. The obvious idea, that submodularity can be checked only on single-element extensions, is correct but must itself be proved.

Formalization scope

Coalitions are finite sets of Fin (n+1) and payoff vectors are functions on all players; the core and $\Pi_S$ constrain only the players of $S$, so vectors differing outside $S$ are interchangeable. The core's budget equation sums over all players of the coalition, including the auctioneer, which is what the book's proofs use although its displayed definition sums over the bidders. The theorems take $V$ as any function with the two properties, and the auction's $V$ is shown to have them; the VCG vector is defined by the formulas (15.23) and (15.24) rather than through the payment rule, whose equivalence is the book's derivation. Bidder-submodularity is stated for $S \subseteq S'$ rather than proper inclusion, which changes nothing.

The definition module is shared by all five items. The single-item English auction as a primal-dual algorithm and the condition on individual preferences (substitutes) that implies bidder-submodularity are natural extensions on the same definitions.

Selected references

• L. V. Snyder and Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019, Chapter 15. https://doi.org/10.1002/9781119584445
• L. M. Ausubel and P. Milgrom, The lovely but lonely Vickrey auction, in Combinatorial Auctions, MIT Press, 2006. https://doi.org/10.7551/mitpress/9780262033428.003.0002
• S. de Vries and R. V. Vohra, Combinatorial auctions: a survey, INFORMS Journal on Computing 15(3), 2003. https://doi.org/10.1287/ijoc.15.3.284.16077
• W. Vickrey, Counterspeculation, auctions, and competitive sealed tenders, Journal of Finance 16(1), 1961. https://doi.org/10.1111/j.1540-6261.1961.tb02789.x

Motivation

A decision-maker has $n$ projects, each a Markov reward process, and at every decision time may advance exactly one of them; the others stay frozen. Which project to advance so as to maximize the expected total discounted reward? Posed as a dynamic program the problem has a state space that is the product of the $n$ state spaces, and the size of that product defeats every general method. The index theorem of Gittins and Jones (1974) says the dynamic program is solved exactly by an index policy: there is a real number $\nu(B, x)$, computable for each bandit process $B$ from its own data and its own current state $x$, such that always advancing a process of greatest index is optimal. Chapter 2 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., doi:10.1002/9780470980033), introduces the index, proves the theorem three times, and works out the properties of the index that the rest of the book, from jobs and superprocesses to restless bandits, is built on: which stopping time attains it, how it is computed, how it moves with the discount factor, and when it collapses to the myopic rule.

The index theorem itself is already on the platform, proved, as BanditAlgorithm.gittins_index_theorem in the Bandit Algorithms series (Lattimore and Szepesvári, Theorem 35.9). This mission cites it and formalizes what Chapter 2 establishes around it.

Setting

A bandit process $B$ (§2.3–2.4) is a Markov reward process on a countable state space $E$: transition probabilities $P(y \mid x)$, a bounded reward $r(x)$ received each time the continuation control is applied in state $x$, and a discount factor $a \in (0, 1)$; the freeze control leaves the state unchanged and yields nothing. The law of the process started at $x$ is $\mathbb{P}_x$ and $x(t)$ is its state at process time $t = 0, 1, 2, \dots$. A stopping time $\tau$ is a past-measurable rule for switching from continuation to freezing, taking values in $\{1, 2, \dots\} \cup \{\infty\}$. For such $\tau$, $R_\tau(B, x) = \mathbb{E}_x[\sum_{t < \tau} a^t r(x(t))]$ is the expected discounted reward and $W_\tau(B, x) = \mathbb{E}_x[\sum_{t < \tau} a^t]$ the expected discounted time; their ratio $\nu_\tau(B, x)$ (2.7) is the equivalent constant reward rate of that portion of $B$. The Gittins index is

$$\nu(B, x) = \sup_{\tau > 0} \frac{R_\tau(B, x)}{W_\tau(B, x)} \tag{2.6}$$

and, equivalently, the fair charge (2.5): the greatest rent $\lambda$ per period for which continuing $B$ for one or more periods, paying $\lambda$ each period, can be done without expected loss. A simple family of alternative bandit processes (SFABP) is $n$ such processes with a common discount factor, one of which is continued at each decision time; an index policy continues a process of greatest index. In the Lean development the single-arm model is the platform's (GittinsIndex): the chain law is built by the Ionescu–Tulcea construction, stopping times are adapted $\mathbb{N}\cup\{\infty\}$-valued maps on trajectories, and gittinsIndex P r a x is (2.6).

Formalization targets

Goal: Lemma 2.2, the optimal stopping set

The supremum in (2.6) is attained. For the initial state $\xi$, the attaining stopping rule may be taken to be "stop at the first time $t \ge 1$ at which the state lies in $\Sigma_0$" for any set $\Sigma_0$ with

$$\{x : \nu(B, x) < \nu(B, \xi)\} \subseteq \Sigma_0 \subseteq \{x : \nu(B, x) \le \nu(B, \xi)\},$$

and every such rule has $\nu_\tau(B, \xi) = \nu(B, \xi)$.

Milestones

Theorem 2.1 as a reference to the proved platform theorem; Eq. (2.5), the fair-charge characterization of the index; the restart-in-state formulation of §2.6.4 as the convergence of the Katehakis–Veinott value iteration; Theorem 2.3, monotonicity in the discount factor; Lemma 2.4, the interchange of two bandit portions; Propositions 2.5–2.8, the monotone-index cases in which the index is the immediate reward, or is attained only after the first step, or only at $\tau = \infty$.

Significance

Lemma 2.2 is the working form of the index: it turns the supremum over all stopping times into a specific rule, the first time the index falls below its starting value, and it is what the interchange proof of §2.7, the modified-forwards-induction policies of §2.6.6, the monotone-index propositions of §2.11 and the treatment of jobs in Chapter 3 all use. The fair-charge form (2.5) is the prevailing-charge proof of the theorem (Weber 1992) and the interpretation that carries over to superprocesses and restless bandits. The restart formulation is how indices are computed in practice (Katehakis and Veinott 1987), and Theorem 2.3 is the first of the comparative statics used throughout Chapters 7 and 8. Lemma 2.4 is the elementary inequality behind the original proof of Gittins and Jones.

Of these, only the index theorem has a machine-checked proof today. Formalizing the rest gives the platform the index as a usable object: a characterization of the optimal stopping rule, a convergent algorithm for it, and the monotonicity facts, all stated against the existing model so that every later mission of this series and every future use of the L&S model can build on them.

Difficulty

The obvious first move for Lemma 2.2, "take the stopping time that achieves the supremum", is what has to be proved: the supremum is over an uncountable family, and attainment comes from the optimal stopping problem with charge $\lambda = \nu(B, \xi)$, whose value function satisfies $\varphi(x) = \max\{0, r(x) - \lambda + a\mathbb{E}[\varphi(x(1)) \mid x(0) = x]\}$, together with the fact that its optimal stopping set is characterized by the strict and non-strict inequalities $\lambda > \nu(B, x)$ and $\lambda \ge \nu(B, x)$. That last step is the content: it identifies the local decision "stop or continue" with a comparison of indices, which is why any set between the two level sets works. On the platform's model this requires the dynamic-programming theory of discounted optimal stopping on a countable space (Theorem 2.10 of the book), the identification of fairChargeProfit with that value function, and the strong Markov property of markovChainMeasure at a trajectory stopping time. Theorem 2.3 needs randomized stopping times (a geometric kill) and the fact that they do not enlarge the supremum. The restart iteration is monotone and bounded but its operator is not a contraction in the restart value, so its limit has to be identified with the restart problem's value directly; that value is $\max(0, \nu/(1-a))$, not $\nu/(1-a)$, because restarting forever is free.

Formalization scope

The state space is a countable type with measurable singletons, so every subset is measurable; rewards are bounded; $a \in (0, 1)$. The chain law, stopping times, the discounted stopped sums and the index are the platform's, unchanged. Expectations are Bochner integrals; with bounded rewards they are finite and no total-function default value enters. IsPositiveStoppingTime fixes $\tau \ge 1$ everywhere, so $W_\tau \ge 1$ and the ratio (2.7) is a genuine quotient. The stopping rule of Lemma 2.2 is the hitting time from time $1$ of a set, with $\infty$ when the set is never hit. The fair-charge profit is a real supremum over the nonempty bounded family of positive stopping times, and (2.5) is stated with the outer supremum over $\{\lambda : \text{profit}(\lambda) \ge 0\}$, a nonempty set bounded above. The restart iteration is stated as a limit, with the value $\max(0, \nu(B, \xi)/(1-a))$: for a nonnegative index this is the book's $\nu/(1-a)$, and the maximum is forced by a one-state example with negative reward. The propositions' hypotheses are almost-sure events under $\mathbb{P}_x$, written as events of measure one.

Two trivializing readings are excluded: the index is never taken over all $\mathbb{N}\cup\{\infty\}$-valued maps but over adapted stopping times, and the stopping set of the goal is not restricted to the two extreme level sets. Contributions welcome: the optimal-stopping dynamic program on markovChainMeasure (value iteration, the strong Markov property at a stopping time), the equivalence of randomized and non-randomized stopping times for the supremum, and the monotone convergence of the restart iteration.

Selected references

• J. Gittins, K. Glazebrook, R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011, Chapter 2. doi:10.1002/9780470980033
• J. C. Gittins, D. M. Jones, A dynamic allocation index for the sequential design of experiments, in Progress in Statistics (Gani, ed.), North-Holland, 1974.
• R. Weber, On the Gittins index for multiarmed bandits, Annals of Applied Probability 2(4), 1992. doi:10.1214/aoap/1177005588
• M. N. Katehakis, A. F. Veinott, The multi-armed bandit problem: decomposition and computation, Mathematics of Operations Research 12(2), 1987. doi:10.1287/moor.12.2.262
• T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 35. doi:10.1017/9781108571401

Motivation

A recommendation system learns from the users it serves: the diner who tries a restaurant produces the review the next diner reads. Each user would rather exploit what is already known than explore for the benefit of those who come later, so a population of self-interested agents under-explores, and an alternative that looks bad on sparse early evidence may never be tried again even when it is the best. Chapter 11 of Slivkins, Introduction to Multi-Armed Bandits (arXiv:1904.07272), treats incentivized exploration: a principal who cannot force the agents but can recommend, and who, because it aggregates what earlier agents observed, knows more than any one of them. The question is whether recommendations alone can induce enough exploration to learn as fast as an ordinary bandit algorithm. The model is that of Kremer, Mansour and Perry (JPE 2014) and the results are those of Mansour, Slivkins and Syrgkanis (EC 2015, Operations Research 2020), specialized to two arms; the single-round problem is Bayesian persuasion in the sense of Kamenica and Gentzkow (AER 2011).

Setting

There are $K$ arms and $T$ rounds. A mean reward vector $\mu \in [0,1]^K$ is drawn from a known prior $P$, and each pull of arm $a$ yields a reward drawn from a known family $D_{\mu_a}$ with mean $\mu_a$. In round $t$ the principal recommends an arm $\mathrm{rec}_t$; agent $t$, who knows the prior, the family, the algorithm and the round but not the past, sees only $\mathrm{rec}_t$, chooses $a_t$, collects $r_t \sim D_{\mu_{a_t}}$ and leaves; the principal observes $(a_t, r_t)$. The chapter works with two arms, ordered so that the prior means satisfy $\mu^0_1 \ge \mu^0_2$, with a prior of finite support and finitely many reward values.

An algorithm is Bayesian incentive-compatible (BIC, Definition 11.4) if following its recommendation is in every agent's interest given what the agent knows: for every round $t$ and arms $a \ne a'$ with $\Pr[\mathrm{rec}_t = a, E_{t-1}] > 0$,

$$\mathbb{E}[\mu_a - \mu_{a'} \mid \mathrm{rec}_t = a,\ E_{t-1}] \ge 0, \tag{11.1}$$

where $E_{t-1}$ is the event that all previous agents complied. A BIC algorithm is then an ordinary bandit algorithm whose recommendations are followed, and the run has the law of the Bayesian bandit of Chapter 3. Two contrasting policies frame the chapter. GREEDY reveals the history and lets agents exploit, $a_t \in \arg\max_a \mathbb{E}[\mu_a \mid H_t]$ (11.2); it is BIC and it fails. HiddenExploration (Algorithm 11.1) hides a little exploration in a lot of exploitation: on a signal $\mathrm{sig}$, with probability $\varepsilon$ it recommends a target arm $a_{\mathrm{trg}}(\mathrm{sig})$, otherwise the arm maximizing $\mathbb{E}[\mu_a \mid \mathrm{sig}]$, ties to arm 1. Its posterior gap is $G = \mathbb{E}[\mu_2 - \mu_1 \mid \mathrm{sig}]$. RepeatedHE (Algorithm 11.2) runs it round after round with an arbitrary bandit algorithm $\mathrm{ALG}$ as the target: $N_0$ initial rounds recommend arm 1; afterwards, with probability $\varepsilon$ the round is an exploration round in which $\mathrm{ALG}$ chooses (and is fed the reward), and otherwise the exploitation branch recommends $\min\arg\max_a \mathbb{E}[\mu_a \mid S_t]$, where $S_t$ is the data of all exploration rounds so far (11.10). The quantity that governs everything is $G_{1,n} = \mathbb{E}[\mu_2 - \mu_1 \mid S_{1,n}]$ (11.11), the posterior gap after $n$ samples of arm 1, and Property (11.12), that $\Pr[G_{1,n} > 0] > 0$ for some $n$: arm 2 can appear better after enough samples of arm 1.

Formalization targets

Goal: Theorem 11.15

RepeatedHE with exploration probability $\varepsilon > 0$ and $N_0$ initial samples of arm 1 is BIC as long as

$$\varepsilon < \tfrac13\,\mathbb{E}\big[G \cdot \mathbf 1\{G > 0\}\big], \qquad G = G_{N_0+1} = \mathbb{E}[\mu_2 - \mu_1 \mid S_{1,N_0}],$$

for any bandit algorithm $\mathrm{ALG}$ and any horizon. The threshold depends on the prior alone.

Milestones

Theorem 11.7 (GREEDY never chooses arm 2 with probability at least $\mu^0_1 - \mu^0_2$) and Corollary 11.8 (linear Bayesian regret of GREEDY under independent priors); Lemma 11.10 (HiddenExploration is BIC when $\varepsilon \le \frac13\mathbb{E}[G\mathbf 1\{G > 0\}]$) with Claim 11.12 (the arm-2 side of the constraint suffices); Corollary 11.14 (RepeatedHE is BIC under the round-by-round condition); Theorem 11.19 (without Property (11.12) no BIC algorithm ever plays arm 2, ties to arm 1).

Significance

The results say when exploration can be incentivized at all and how. Theorem 11.7 shows that revealing everything is not a solution: the greedy dynamics gets stuck on arm 1 with a probability that does not shrink with $T$, and Corollary 11.8 turns that into $\Omega(T)$ Bayesian regret. Theorem 11.15 shows that a recommendation-only principal can induce any amount of exploration it wants, with $\mathrm{ALG}$ arbitrary, at a per-round rate $\varepsilon$ fixed by the prior; Theorem 11.17 (stated with a proof sketch, and omitted here) then transfers $\mathrm{ALG}$'s regret to RepeatedHE up to the prior-dependent factors $N_0$ and $1/\varepsilon$, so $\tilde O(\sqrt T)$ regret is attainable subject to incentives. Theorem 11.19 closes the picture: Property (11.12) is necessary as well as sufficient. Together they characterize which priors admit incentivized exploration and give an algorithm that works for all of them.

Nothing of this is machine-checked. The mission adds to the Bayesian layer of mission III (prior, posterior by Bayes' rule, Bayesian regret) the BIC constraint on a joint law, GREEDY as a policy, the single-round HiddenExploration on an abstract finite signal, and the law of RepeatedHE; all of it is reusable for the $K$-arm and the "explore all explorable arms" extensions of the literature review.

Difficulty

Theorem 11.7 is a martingale argument: the posterior gap along the history is a Doob martingale, the first round in which arm 2 is chosen is a bounded stopping time, and optional stopping gives $\mathbb{E}[Z_\tau] = \mu^0_1 - \mu^0_2$; all of this has to be set up on the joint law of $(\mu, H_T)$ of mission III, where the posterior is defined by Bayes' rule and the identification with a conditional expectation is itself a theorem (posterior_eq_condProb). Lemma 11.10 is the heart of the chapter and is not a computation about $\mathrm{rec}$: it works with $F(E) = \mathbb{E}[G\mathbf 1_E]$, splits along the two branches, uses that the exploitation branch recommends arm 2 exactly when $G > 0$, and closes with $F(G > 0) + F(G < 0) = \mathbb{E}[\mu_2 - \mu_1] \le 0$; the only place where the analysis uses that both branches are functions of the signal is the step $\mathbb{E}[\mu_2 - \mu_1 \mid \mathrm{rec} = 2] = \mathbb{E}[G \mid \mathrm{rec} = 2]$, and a formalization has to make that step explicit. Theorem 11.15 requires seeing each later round of RepeatedHE as a HiddenExploration with signal $S_t$, where $\mathrm{ALG}$'s choice is a randomized function of $S_t$, and then the monotonicity of $\mathbb{E}[G_t\mathbf 1\{G_t > 0\}]$ in $t$, a two-line consequence of $S_{t+1}$ determining $S_t$ that presupposes the posterior given $S_t$ is the Bayes posterior of the exploration data alone, which is true because the exploration decisions do not depend on $\mu$ given that data. Corollary 11.8 needs the independence of the event "$\mu_1 < 1 - 2\alpha$ and arm 2 is never chosen" from $\mu_2$. Theorem 11.19 is an induction in which the inductive hypothesis is a probability-zero statement about all earlier rounds.

Formalization scope

Arms are Fin 2, the book's arm 1 being index 0; rounds are Fin T. The prior is a probability measure on mean vectors supported on a finite set $F \subseteq [0,1]^2$, with $\mu^0_1 \ge \mu^0_2$ as a hypothesis; the reward family is mission III's RewardFamily (finitely many values, mean $\nu$ for $\nu \in [0,1]$). BIC is defined on a joint law of $(\mu, \text{record})$ of the run in which every agent complies, with the recommendation of each round read off the record; the compliance event $E_{t-1}$ of (11.1) is the sure event of that law, which is the standard reading of "the agents believe all previous agents complied". For a bandit policy the law is mission III's jointMeasure. Conditional expectations are written as finite sums over $F$, so there are no integrals and no integrability side conditions; a posterior mean off the support is a junk $0$ that never enters a theorem. GREEDY allows arbitrary tie-breaking; HiddenExploration's exploitation branch breaks ties toward arm 1 as Algorithm 11.1 does; the tie convention of Theorem 11.19 is the strict form of BIC for arm 2. The law of RepeatedHE is an explicit finitely supported measure, $\mu$ and record weighted by the prior times the product of the round probabilities (initial rounds forced to arm 1, then the $\varepsilon$-coin, $\mathrm{ALG}$'s kernel on its own history, or the exploitation arm, then $D_{\mu_{a_t}}$); it is written this way because $\mathrm{ALG}$ is fed a history of variable length. Two conditions are stated exactly as printed: Lemma 11.10 with $\varepsilon \le \frac13\mathbb{E}[G\mathbf 1\{G > 0\}]$ (non-strict, checked at equality) and Theorem 11.15 with the strict inequality.

Trivializations are excluded: $\varepsilon > 0$ throughout; the BIC condition is asserted only where the recommendation has positive probability, and the sums in it are over the finite support, so an unsatisfiable hypothesis cannot hide in a measure-zero set. Welcome contributions: the optional-stopping argument on jointMeasure, the identification of explPostMean with the conditional expectation given the exploration data, the Bayes-rule algebra behind Lemma 11.10, and the counting lemmas on heRecords.

Selected references

• A. Slivkins, Introduction to Multi-Armed Bandits, Foundations and Trends in Machine Learning 12(1-2), 2019, Chapter 11. arXiv:1904.07272, doi:10.1561/2200000068
• I. Kremer, Y. Mansour, M. Perry, Implementing the "Wisdom of the Crowd", Journal of Political Economy 122(5), 2014. doi:10.1086/676597
• Y. Mansour, A. Slivkins, V. Syrgkanis, Bayesian Incentive-Compatible Bandit Exploration, Operations Research 68(4), 2020 (EC 2015). doi:10.1287/opre.2019.1919
• E. Kamenica, M. Gentzkow, Bayesian Persuasion, American Economic Review 101(6), 2011. doi:10.1257/aer.101.6.2590
• M. Sellke, A. Slivkins, The Price of Incentivizing Exploration: A Characterization via Thompson Sampling and Sample Complexity, Operations Research 71(5), 2023. doi:10.1287/opre.2022.2401

Motivation

Chapter 3 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., doi:10.1002/9780470980033), asks which of the assumptions behind the index theorem can be dropped and which cannot, using the simplest bandit processes there are: jobs, which pay a single reward when they complete. Along the way it settles three questions that matter on their own. When identical machines run in parallel, which schedule of deterministic jobs minimizes the total completion time (Baker's theorem), and what does the equal-ratio case look like (Theorem 3.3)? When an object is hidden in one of several boxes and each search costs money and may fail, in what order should the boxes be searched (Blackwell's search-index theorem, Theorem 3.6)? And when two bandit processes discount at different rates, is there still an index policy (Nash's Theorem 3.4)? The search theorem is the chapter's example of what the index machinery yields once undiscounted criteria are admitted through the limit $\gamma \downarrow 0$; the scheduling results are the source of the counterexamples that show a second machine breaks the index structure.

Setting

Jobs on parallel machines. There are $n$ jobs with service times $s_i > 0$ and weights $c_i$, and $m$ identical machines. A schedule assigns each job a machine and a position in that machine's processing order; each machine processes its jobs consecutively. The completion time $C_i$ of a job is the total service time of the jobs on its machine up to and including it; the flow time is $\sum_i C_i$ and the weighted flow time $\sum_i c_i C_i$. The load of a machine is the total service time assigned to it, and $\delta_j$ is its excess over the average $S/m$. The SPT list schedule sorts the jobs by increasing service time and deals them out cyclically to the machines. The level of a job is its position counted from the end of its machine's schedule.

The search problem (Problem 3). A stationary object is hidden in one of $n$ boxes, in box $i$ with probability $p_i$. A search of box $i$ costs $c_i$ and finds the object with probability $q_i$ if it is there. A search policy is a sequence of boxes; after $N_i$ unsuccessful searches of box $i$ the posterior probability that the object is there is proportional to $p_i(1-q_i)^{N_i}$, and the search index of the box is $p'_i q_i/c_i$, the current probability of finding the object per unit cost. The expected cost of a policy is $\sum_k c_{\sigma_k}\Pr[\text{not found by the first } k \text{ searches}]$.

Two discount factors. Bandit process $A$ (state space $S_A$, kernel $P_A$, reward $r_A$) discounts at rate $a$ and $B$ at rate $b$; a reward obtained at time $t$ is worth $a^t$ or $b^t$ times its face value according to which process produced it. The cross indices are $\nu_{AB}(x) = \sup_{\tau>0} \mathbb{E}\sum_{t<\tau} a^t r_A(x(t)) \big/ \mathbb{E}[1 - b^\tau]$ and $\nu_{BA}(y)$ with the roles exchanged: each is computed from one process's stopping times but with the other's discount factor in the denominator. The book prints the denominator as $\mathbb{E}\int_0^\tau b^t\,dt$ and compares $\nu_{AB}(x)$ with $\nu_{BA}(y)$ at every time; both are corrected here (see the Theorem 3.4 item), since the printed rule is not optimal. The family is the two-armed Markov bandit of the Bandit Algorithms model on the disjoint union $S_A \oplus S_B$.

Formalization targets

Goal: Theorem 3.6

For prior probabilities $p_i \ge 0$ summing to one, detection probabilities $0 < q_i \le 1$ and costs $c_i > 0$, a search policy is optimal if and only if at every step it searches a box of maximal current index $p'_i q_i / c_i$:

$$\text{optimal}(\sigma) \iff \forall k,\ \forall i:\ \frac{p_i (1-q_i)^{N_i(k)} q_i}{c_i} \le \frac{p_{\sigma_k}(1-q_{\sigma_k})^{N_{\sigma_k}(k)} q_{\sigma_k}}{c_{\sigma_k}}.$$

Milestones

Theorem 3.3, as the identity $\sum_i c_i C_i = \frac{\kappa}{2}\big(\sum_i s_i^2 + S^2/m + \sum_j \delta_j^2\big)$ when $c_i = \kappa s_i$; Theorem 3.4 in discrete time and corrected, that a policy selecting, at time $t$, $A$ when $a^t \nu_{AB}(x) > b^t \nu_{BA}(y)$ and $B$ when $a^t \nu_{AB}(x) < b^t \nu_{BA}(y)$ attains the supremum of the bandit-dependently discounted payoff; Theorem 3.7, that SPT minimizes the flow time on $m$ machines and that the optimal schedules are exactly those placing the $r$-th block of $m$ longest jobs at level $r$ from the end, for some order of the equal jobs.

Significance

Theorem 3.6 is the classical solution of the discrete search problem (Blackwell, reported by Matula 1964; Kadane 1969): the greedy rule in probability-per-cost is optimal, and every optimal policy is of that form. The book derives it from the index theorem through an auxiliary family of bandit processes (Problem 3A) and the undiscounted limit (Corollary 3.5), which is why it sits in this chapter; as a statement it is elementary and self-contained, and it is the template for the tax problems and Klimov's model of Chapter 4. Theorem 3.7 and Theorem 3.3 are the positive results about parallel machines that survive the loss of the index structure; Theorem 3.4 shows the index theorem's shape persisting under bandit-dependent discounting, with two twists: each index depends on the other process's discount factor, which is exactly why it does not extend to three processes, and the comparison at time $t$ weighs the indices by $a^t$ and $b^t$, so the rule is not stationary in the states. The printed statement misses the second twist and misnormalizes the first; two one-state bandits paying $0.18$ ($a = 0.9$) and $1$ ($b = 0.5$) are best played $B, B, B$ and then $A$ forever, which no stationary rule does.

None of these is machine-checked. Formalizing them gives the platform an optimality theorem for an infinite-horizon search process with an explicit index characterization in both directions, the standard parallel-machine flow-time results with a precise uniqueness clause, and a first statement on the Bandit Algorithms two-armed model with unequal discounting.

Difficulty

For Theorem 3.6 the obvious route, comparing two adjacent searches, gives only that interchanging a pair in the wrong index order lowers the cost; turning that into optimality over all infinite sequences needs that an optimal policy exists (costs are bounded below by zero and the index policy has finite cost), that a policy neglecting a box of positive prior has infinite cost, and that any first deviation from the index rule can be improved by moving a later search forward, which requires tracking how the not-found probability changes along the whole tail. The converse direction is the same interchange run backwards, and the tie case must be handled so that the equivalence is exact. Theorem 3.7's first part follows from writing the flow time as $\sum_i \ell_i s_i$ with $\ell_i$ the level and applying a rearrangement inequality over the multiset of levels, but the multiset of levels itself depends on how many jobs each machine gets, so balancing the machine counts is part of the argument; the uniqueness clause needs both that the multiset is forced and that the pairing of levels with service times is forced by strict monotonicity. Theorem 3.4 is the hardest: the book's proof changes the time scale of each process so that the two share a discount factor, which produces a semi-Markov family, and applies the index theorem there; in discrete time on the Markov model one needs either a discrete analogue of that argument or a direct prevailing-charge proof with two charge scales.

Formalization scope

Schedules are assignments of machines and positions with distinct positions on a machine, without idling; the flow-time quantities are finite sums over Fin n. The SPT schedule is defined by the ascending rank of a job (ties broken by index) and carries its own injectivity proof. The search cost is a series in $[0, \infty]$ of nonnegative terms, so no summability hypothesis is needed and "infinite cost" is literal; the index is stated unnormalized, $p_i(1-q_i)^{N_i} q_i/c_i$, which orders the boxes exactly as the posterior index does. The two-discount family uses the platform's MarkovBanditPolicy 2 (S_A ⊕ S_B) and markovBanditMeasure with the kernel that moves an $A$-state by $P_A$ and a $B$-state by $P_B$; the payoff is the round-by-round series $\sum_t (a^t \mathbb{E}[r\mathbf 1\{A_t = A\}] + b^t \mathbb{E}[r\mathbf 1\{A_t = B\}])$, absolutely summable for bounded rewards, and the policy condition is imposed at histories whose current states have the right types (all reachable histories do). Hypotheses: $m \ge 1$, service times positive; $p_i \ge 0$, $\sum p_i = 1$, $0 < q_i \le 1$, $c_i > 0$; countable state spaces, bounded rewards, $a, b \in (0,1)$.

Trivializing readings are excluded: the search "iff" is over all sequences, not a finite horizon; the uniqueness clause is stated in full, with ties resolved by any ranking of the equal jobs; the cross indices are suprema over positive stopping times (denominators at least one), and the two-discount rule weighs the indices by $a^t$, $b^t$. Welcome contributions: the rearrangement and level-count lemmas for schedules, the interchange lemma for the search cost, and a discrete prevailing-charge argument for Theorem 3.4.

Selected references

• J. Gittins, K. Glazebrook, R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011, Chapter 3. doi:10.1002/9780470980033
• D. W. Matula, A periodic optimal search, American Mathematical Monthly 71(1), 1964. doi:10.2307/2311300
• J. B. Kadane, Quiz show problems, Journal of Mathematical Analysis and Applications 27(3), 1969. doi:10.1016/0022-247X(69)90140-2
• K. R. Baker, Introduction to Sequencing and Scheduling, Wiley, 1974.
• P. Nash, A generalized bandit problem, Journal of the Royal Statistical Society B 42(2), 1980. doi:10.1111/j.2517-6161.1980.tb01119.x

Motivation

Chapter 5 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., doi:10.1002/9780470980033), presents the achievable region methodology of Tsoucas, Bertsimas and Niño-Mora, Glazebrook and Garbe, and Dacre, Glazebrook and Niño-Mora: instead of arguing about policies, one argues about the set of performance vectors they can produce. For a multi-armed bandit the natural performance of a policy is the vector of discounted numbers of times each state is continued; the expected return is linear in it; and the set of achievable performances turns out to be a polytope cut out by conservation laws, one inequality per subset of states, with equality exactly for the priority policies that put that subset last. Optimizing a linear objective over a polytope is a linear program, its dual is solved by an adaptive greedy algorithm, and the primal solution is the performance of a priority policy whose priorities are the algorithm's outputs, the Gittins indices. This gives yet another proof of the index theorem (Section 5.3) and, more importantly, a definition, generalized conservation laws (Section 5.4), of the class of systems for which the same argument works: branching bandits, multi-class queues, job scheduling with discounted rewards, systems with imposed priority classes. The chapter's main result, Theorem 5.5, is the statement that every such system is solved by an index policy.

Setting

There are $N$ job types $E = \{1, \dots, N\}$. A policy $\pi$ has a performance $x^\pi \in \mathbb{R}^N_+$, a vector of expectations; a permutation $\sigma$ of $E$ defines the permutation policy giving $\sigma_N$ highest and $\sigma_1$ lowest priority, and $S_k = \{\sigma_1, \dots, \sigma_k\}$ is the set of the $k$ lowest-priority types. The system satisfies GCL(1) if there are a base function $b : 2^E \to \mathbb{R}_+$ and a matrix $A = (A_i^S)$, positive on $S$ and zero off it, such that for every policy

$$\sum_{i \in S} A_i^S x_i^\pi \ge b(S) \quad (S \subseteq E), \qquad \sum_{i \in E} A_i^E x_i^\pi = b(E),$$

with equality in the first for every permutation policy whose $|S|$ lowest-priority types are $S$. GCL(2) reverses the inequality. The adaptive greedy algorithm $AG(A, r)$ picks $i_N$ maximizing $r_i/A_i^E$, sets $\bar y_E$ to the maximum, removes $i_N$, and repeats with the adjusted rewards $r_i - \sum_{j \ge k} A_i^{S_j}\bar y_{S_j}$ divided by $A_i^{S_{k-1}}$; its outputs are the order $i_1, \dots, i_N$, the dual variables $\bar y_{S_k}$ and the indices $\nu_{i_k} = \sum_{j \ge k} \bar y_{S_j}$.

For the SFABP of Section 5.3, $n$ identical bandit processes on $E$ with kernel $P$ and discount factor $a$ in the model of the Bandit Algorithms series, $x_i^\pi = \mathbb{E}^\pi \sum_t a^t I_i(t)$ is the discounted number of continuations of a bandit in state $i$, $A_i^S = \mathbb{E}[1 + a + \cdots + a^{T_i^S - 1}]$ is the discounted return time to $S$ from $i \in S$, and $b(S)$ is the minimal cost $\sum_{i \in S} A_i^S x_i^\pi$, namely $(1-a)^{-1}\mathbb{E}[a^\tau]$ with $\tau$ the number of continuations needed to bring every bandit into $S$.

Formalization targets

Goal: Theorem 5.5

For a GCL(1) system whose achievable region is convex, and any reward vector $r$: the achievable region is the polytope

$$P(A, b) = \Big\{x \in \mathbb{R}_+^N : \sum_{i \in S} A_i^S x_i \ge b(S),\ S \subset E,\ \sum_{i \in E} A_i^E x_i = b(E)\Big\};$$

its extreme points are performances of permutation policies; $AG(A, r)$ has an output; and for every output the permutation policy in the order it finds, the Gittins index policy, maximizes $\sum_i r_i x_i^\pi$ over all policies.

Milestones

Lemma 5.1 (the SFABP satisfies the conservation laws, with equality for policies giving priority to states outside $S$); the identification on p. 123 of the adaptive greedy indices of a SFABP with the Gittins indices, together with their monotonicity along the order found; Theorem 5.10, the GCL(2) counterpart of the goal for cost minimization.

Significance

Theorem 5.5 is the index theorem in its most general form of this kind: it says nothing about Markov chains, only that performances are expectations, objectives are linear and conservation laws hold, and it delivers both the optimal policy and the algorithm that computes its priorities in polynomial time in the number of job types. It is the theorem behind the index results for branching bandits and Klimov's multi-class queue and behind the suboptimality bounds of Sections 5.5 and 5.7, all of which are calculations on the polytope. Lemma 5.1 and the p. 123 identification are what tie the abstract theorem to the Gittins index: they show that the multi-armed bandit is a GCL(1) system and that the priorities the algorithm produces are the same indices as Chapters 2 to 4 define through stopping times.

None of these is machine-checked. Formalizing Theorem 5.5 puts an LP-duality index theorem on the platform in a form any system can instantiate by verifying its conservation laws; formalizing Lemma 5.1 relates the Bandit Algorithms run law to the single-chain return times, which is the first conservation law on that model; and the p. 123 theorem gives an algorithmic characterization of the Gittins index on finite chains, distinct from the restart and largest-remaining-index characterizations of Chapter 2.

Difficulty

The goal's optimality clause is weak LP duality once one shows that the greedy dual variables are nonpositive except $\bar y_E$ and satisfy the dual constraints with equality, which is a finite induction on the stages; the extreme-point clause needs that every vertex of a polyhedron is the unique maximizer of some linear functional, and the region clause that a compact convex set is the convex hull of its extreme points (Krein–Milman in finite dimension, or the polyhedral fact directly). None of this is in Mathlib in the required form. Lemma 5.1 is probabilistic: the lower bound requires the strong Markov property of the continued bandit under an arbitrary past-measurable policy, a pathwise accounting of the discounted periods paid for by each continuation from $S$, and the observation that at most $\tau$ slots can be spent on bandits that have never been in $S$; the equality for priority policies requires that these policies use exactly those slots first and then tile the future with return excursions, and the product form of $b(S)$ requires independence of the bandits' process-time trajectories under the run law, which is built decision time by decision time rather than as a product. The p. 123 theorem is the computation (5.13) to (5.14) combined with the optimal-stopping characterization of Chapter 2 for the stop sets $\{i_1, \dots, i_{k-2}\}$, which lie between $\{\nu < \nu(i_{k-1})\}$ and $\{\nu \le \nu(i_{k-1})\}$; ties make the induction delicate, and the statement is claimed for every tie-breaking.

Formalization scope

GCL(1) and GCL(2) systems are structures over an arbitrary policy type: performance, base function, matrix, permutation policies and the three laws are fields, so the theorems are statements about finite-dimensional data and the platform's proof needs no probability. The adaptive greedy algorithm is specified relationally, as the set of its possible outputs with arbitrary tie-breaking, and the conclusion holds for each of them; existence of an output is asserted separately. The optimality clause is stated as a comparison with every policy rather than as a real supremum. The hypothesis that the achievable region is convex is explicit: the book's argument from extreme points to the whole polytope uses randomization of policies, and without it the region of a system with only its permutation policies is finite. The SFABP items use $n$ identical bandits on Fin N in the Bandit Algorithms model, the coefficients $A_i^S$ through Mission I's stoppedTime at the return time, and $b(S)$ in the product form $(1-a)^{-1}\prod_{j : k_j \notin S}\mathbb{E}[a^{T^S_{k_j}}]$, which is the minimal cost the argument on p. 120 establishes; the book prints a sum, which is $0$ when all bandits start in $S$ where the minimal cost is $1/(1-a)$. Discount factors are in $(0, 1)$ throughout.

Trivializing readings are excluded: $A_i^S > 0$ for $i \in S$ is part of the structure and of Lemma 5.1's conclusion, the polytope equations are over all subsets, and the index clause quantifies over every greedy output. Welcome contributions: the nonpositivity and dual feasibility of the greedy variables, the vertex-exposure lemma for polyhedra, and the product decomposition of the run law of identical bandits.

Selected references

• J. Gittins, K. Glazebrook, R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011, Chapter 5. doi:10.1002/9780470980033
• D. Bertsimas, J. Niño-Mora, Conservation laws, extended polymatroids and multiarmed bandit problems; a polyhedral approach to indexable systems, Mathematics of Operations Research 21(2), 1996. doi:10.1287/moor.21.2.257
• P. Tsoucas, The region of achievable performance in a model of Klimov, IBM Research Report RC16543, 1991.
• E. G. Coffman, I. Mitrani, A characterization of waiting time performance realizable by single-server queues, Operations Research 28(3), 1980. doi:10.1287/opre.28.3.810
• K. D. Glazebrook, R. Garbe, Almost optimal policies for stochastic systems which almost satisfy conservation laws, Annals of Operations Research 92, 1999. doi:10.1023/A:1018992306696
• T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 35. doi:10.1017/9781108571401

Motivation

Every proof of the index theorem in Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., doi:10.1002/9780470980033), uses the fact that a bandit not being processed is frozen. Chapter 6 drops that: Whittle's restless bandits evolve under the passive action too, by a different law, and $m$ of $n$ must be active at every time. The problem is PSPACE-hard in general, so Whittle proposed a heuristic built from a Lagrangian relaxation: replace the hard constraint by a subsidy $W$ paid whenever a bandit is passive, solve the resulting single-bandit average-reward problem, and read off, for each state, the least subsidy $W(x)$ at which the passive action becomes optimal. When the set of states where passivity is optimal grows monotonically with $W$, the bandit is indexable and $W(x)$ is its Whittle index; the Whittle index policy activates the $m$ bandits of largest index. It reduces to the Gittins index policy when the passive action freezes, it is asymptotically optimal as $n$ grows under a fluid-stability condition (Weber and Weiss), and it has become the standard heuristic for sensor management, opportunistic channel access, maintenance and queueing control. The price is that indexability must be established model by model. Section 6.5 shows how easy this is when the single-bandit problem is solved by a monotone policy, on two bi-directional models: the spinning plates asset, which improves under investment and deteriorates when neglected, and the vigour bandit of Whittle's Ehrenfest project, which tires when worked and recovers when rested.

Setting

A restless bandit is a Markov decision process with two actions, active ($u = 1$) and passive ($u = 0$), each with its own transition kernel and reward. Under a deterministic stationary Markov policy $g$ with passive subsidy $W$ the reward in state $x$ is $r(x, g(x)) + W(1 - g(x))$, and the average reward from $x$ is the Cesàro limit of the expected rewards. The optimal average reward $g(W)$ is the supremum over such policies and initial states; a policy is optimal if it attains $g(W)$ from every initial state; $E_0(W)$ is the set of states in which some optimal policy is passive; the bandit is indexable if $E_0(W)$ is nondecreasing in $W$; and $W(x) = \inf\{W : x \in E_0(W)\}$.

The spinning plates asset lives on $\{1, \dots, k\}$: active moves $x \to x + 1$ at rate $\lambda(x)$, passive moves $x \to x - 1$ at rate $\mu(x)$, $\lambda(k) = \mu(1) = 0$, and $r(x)$ is earned under both actions, $r$ increasing. Uniformized so that rates are at most one, it is a discrete-time bandit whose kernels move with the rate's probability and otherwise stay. The monotone policy $(y)$ is passive exactly on $\{x \ge y\}$; under it the asset alternates between $y - 1$ and $y$, spending the fraction $\phi(y) = \lambda(y-1)/(\lambda(y-1) + \mu(y))$ of its time at $y$, so its average reward is $W\phi(y) + R(y)$ with $R(y) = r(y)\phi(y) + r(y-1)(1 - \phi(y))$, and $W^*(x) = (R(x+1) - R(x))/(\phi(x) - \phi(x+1))$. The vigour bandit is the mirror image: active moves down at rate $\nu(x)$ and earns $r(x)$, passive moves up at rate $\rho(x)$ and earns nothing, $\psi(y) = \nu(y)/(\nu(y) + \rho(y-1))$, and $W^{**}(x) = (r(x)(1 - \psi(x)) - r(x+1)(1 - \psi(x+1)))/(\psi(x+1) - \psi(x))$.

Formalization targets

Goal: Theorem 6.4

For the spinning plates asset: (i) if $\phi$ is strictly decreasing over the thresholds $1 \le y \le k + 1$, the asset is indexable; (ii) if additionally $W^*$ is strictly decreasing over the states, the Whittle index is

$$W(x) = W^*(x) = \frac{R(x+1) - R(x)}{\phi(x) - \phi(x+1)}, \qquad 1 \le x \le k.$$

Milestones

Eqs. (6.9)–(6.10): the monotone policy $(y)$ earns $W\phi(y) + R(y)$ from every initial state and $g(W) = \max_y [W\phi(y) + R(y)]$, because a monotone policy always achieves $g(W)$; Theorem 6.5, the same two statements for the vigour bandit with $\psi$ increasing and $W^{**}$ increasing.

Significance

Theorem 6.4 is the chapter's template for proving indexability: the single-bandit value $g(W)$ is the upper envelope of finitely many lines $W\phi(y) + R(y)$ whose slopes decrease in the threshold, so the optimal threshold moves monotonically with the subsidy and the hinge points of the envelope are the indices. The same argument gives Theorem 6.5, the admission-control indices of Section 6.7, and the marginal productivity indices of Niño-Mora; it is the reason Whittle indices are computable in closed form for bi-directional models. Its formalization establishes, on the platform, the first restless-bandit model with a proved index, and the general notions of passive set, indexability and Whittle index that every later restless-bandit statement will use.

None of this is machine-checked. The average-reward optimality notion is stated without the DP equation (6.6), through optimality from every initial state, which is what the equation's solution encodes on a finite state space and avoids the relative value function altogether.

Difficulty

The proof in the book is two paragraphs, but it stands on the reduction to monotone policies, which is only sketched: every deterministic stationary policy, from every initial state, drives the asset into an absorbing endpoint or a two-state cycle $\{z - 1, z\}$ whose average reward is that of the monotone policy $(z)$, so no policy beats the best monotone one and the passive set under an optimal-from-everywhere policy is exactly $\{x \ge x(W)\}$ for the smallest maximizing threshold. Formalizing this needs the average reward of a finite Markov chain as a limit determined by the stationary distribution of the recurrent class reached, for the two-point kernels of the model, and a case analysis of policies as $\{0,1\}$-strings. The envelope argument then needs that the smallest maximizer of $\max_y [W\phi(y) + R(y)]$ is nonincreasing in $W$ when $\phi$ is strictly decreasing, and that with $W^*$ strictly decreasing the maximizer is $\le x$ exactly when $W \ge W^*(x)$. Theorem 6.5 is the same with the roles of up and down exchanged. Nothing in Mathlib computes Cesàro limits of finite Markov chains.

Formalization scope

Restless bandits are the two-action DecisionProcesses of the superprocess module; average reward is a real limsup of Cesàro means of Bochner integrals over the chain law of the Bandit Algorithms model under the stationary kernel; the optimal average reward is a supremum over the finite type of deterministic stationary Markov policies and the finite state space, bounded by the reward bound. Both models are on Fin k with the book's states shifted down by one, kernels driftKernel p f that move to f x with probability p x, and the boundary conventions of $\phi$ and $\psi$ (the book's "convenient positive values") replaced by their values $1, 0$ and $0, 1$ at the two extreme thresholds; the model assumptions $\lambda(k) = \mu(1) = 0$, $\nu(1) = \rho(k) = 0$, rates in $[0, 1]$, and $r$ increasing and nonnegative are hypotheses. Theorem 6.5's "increasing" is read as strictly increasing, as in Theorem 6.4, since a nonstrict $\psi$ admits zero interior rates for which the monotone reduction fails. The milestone (6.9) requires $k \ge 1$ and positive interior rates, which Theorem 6.4's hypothesis (i) implies.

Trivializing readings are excluded: indexability is monotonicity of the passive set over all real subsidies, the passive set is defined through policies optimal from every initial state, and the index identity is for every state. Welcome contributions: the average reward of a two-state cycle, the reduction of an arbitrary $\{0,1\}$-policy to a monotone one, and the envelope lemma for lines with decreasing slopes.

Selected references

• J. Gittins, K. Glazebrook, R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011, Chapter 6. doi:10.1002/9780470980033
• P. Whittle, Restless bandits: activity allocation in a changing world, Journal of Applied Probability 25(A), 1988. doi:10.2307/3214163
• R. R. Weber, G. Weiss, On an index policy for restless bandits, Journal of Applied Probability 27(3), 1990. doi:10.2307/3214547
• K. D. Glazebrook, C. Kirkbride, D. Ruiz-Hernandez, Spinning plates and squad systems: policies for bi-directional restless bandits, Advances in Applied Probability 38(1), 2006. doi:10.1239/aap/1143936141
• J. Niño-Mora, Restless bandits, partial conservation laws and indexability, Advances in Applied Probability 33(1), 2001. doi:10.1017/S0001867800010661
• C. H. Papadimitriou, J. N. Tsitsiklis, The complexity of optimal queueing network control, Mathematics of Operations Research 24(2), 1999. doi:10.1287/moor.24.2.293

Motivation

The bandit processes that motivated the index theorem are sampling processes: an arm is a population from which one draws i.i.d. observations whose distribution has an unknown parameter, and each draw both earns something and teaches something. Chapter 7 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., doi:10.1002/9780470980033), develops the theory of such processes in the Bayesian setting: the state of the process is the current posterior for the parameter, continuing it samples the next value from the predictive distribution and moves to the new posterior. When the observations are themselves the rewards one has a reward process, the classical Bayesian multi-armed bandit; when the aim is to find as quickly as possible an individual whose measurement reaches a target $T$ (a compound active enough to warrant further testing, in the drug-screening problem from which the index theorem came) one has a target process, which is a job that completes when the target is reached. Two questions organize the chapter. When can the index be written down without any optimization, and when do symmetries of the model reduce the index to a function of fewer variables? The first is answered by the notion of a favourable prior (Section 7.3): if no run of observations below the target can raise the current probability of success, then the index is that probability, exactly, by Proposition 2.7. The second is answered by the invariance theorems of Section 7.4: a location parameter with a conjugate prior gives $\nu(\bar x, n) = \bar x + \nu(0, n)$, a scale parameter gives $\nu(\bar x, n) = \bar x\,\nu(1, n)$, and for target processes the target can be absorbed into the state, $\nu(\bar x, n, T) = \nu(\bar x - T, n, 0)$. These identities are what make the tables of Chapter 8 one-dimensional.

Setting

A sampling model consists of a likelihood $f(\cdot \mid \theta)$, a family of priors $\pi(\cdot \mid p)$ on the parameter indexed by the parameters $p$ of a conjugate family, and the Bayes update $p \mapsto p_x$ of those parameters after observing $x$; the family is conjugate if the posterior of $\pi(\cdot \mid p)$ given $X = x$ is $\pi(\cdot \mid p_x)$. The predictive distribution is $f(\cdot \mid p) = \int f(\cdot \mid \theta)\pi(d\theta \mid p)$. The reward process moves from $p$ to $p_x$ with $x \sim f(\cdot \mid p)$ and earns $r(p) = \int x f(x \mid p)dx$. The target process with target $T$ moves to the completion state $C$ if $x \ge T$ and to $p_x$ otherwise, earning the current probability of success $r(p) = f([T, \infty) \mid p)$, and $0$ in $C$. A state $p$ is favourable if $r(p_{x_1 \cdots x_m}) \le r(p)$ for every finite sequence of observations $x_i < T$. For the invariance theorems the parameters are $(\bar x, n)$ with the update $((n\bar x + x)/(n+1), n+1)$; $\mu$ is a location parameter of the likelihood if $f(\cdot \mid \mu + c)$ is $f(\cdot \mid \mu)$ shifted by $c$, and $\bar x$ is a location parameter of the prior family if $\pi(\cdot \mid \bar x + c, n)$ is $\pi(\cdot \mid \bar x, n)$ shifted by $c$; scale parameters are defined with $x \mapsto bx$, $b > 0$. The Gittins index is that of the Bandit Algorithms model on these chains.

Formalization targets

Goal: Theorem 7.9 (in the form of Corollary 7.10)

If $\mu$ is a location parameter of a reward process with a conjugate prior family in which $\bar x$ is a location parameter and the parameters update as the sample mean and count, then for every $n > 0$

$$r(\bar x + c, n) = r(\bar x, n) + c \quad\text{and}\quad \nu(\bar x, n) = \bar x + \nu(0, n),$$

under the standing assumptions that the observations have a mean and the discounted rewards of the chain are integrable.

Milestones

Proposition 7.4 (favourable state: $\nu = r$); Example 7.5 (Bernoulli target process, $\nu(\alpha, \beta) = \alpha/(\alpha + \beta)$); Example 7.6 (normal target process with known variance, $\nu(\bar x, n) = \Phi(\bar x (1 + n^{-1})^{-1/2})$ for $\bar x \ge 0$); Theorem 7.11 (scale parameter: $\nu(\bar x, n) = \bar x\,\nu(1, n)$); Theorem 7.17 (target process with a location parameter: $\nu(\bar x, n, T) = \nu(\bar x - T, n, 0)$).

Significance

Theorem 7.9 and its companions are the reason the Gittins index of the normal reward process is tabulated as a function of $n$ alone and that of the exponential process as a function of $n$ and one ratio; every computational method of Chapter 8 starts by reducing the state space with them. Proposition 7.4 is the source of every closed-form index in the book: it identifies the states in which sampling for information is worthless, so that the index collapses to the immediate expected reward, and Examples 7.5 and 7.6 show that for the Bernoulli target process this is every state and for the normal target process every state with a nonnegative posterior mean. The formalization gives the platform its first Bayesian sampling-process model, in which the state is a posterior and conjugacy is stated through the posterior kernel of the likelihood, and its first index identities on unbounded-reward chains, which is where the integrability assumptions of the Bandit Algorithms model do real work.

None of this is machine-checked. The invariance theorems are stated in the proper-prior form of the corollaries, with the model's symmetry as hypotheses, so that they apply to any conjugate family with the stated structure rather than to a particular density.

Difficulty

The invariance theorems require showing that the chain of parameters from the shifted (scaled) state is the image of the chain from the original state under the shift (scaling) of trajectories, which is an equivariance of the Ionescu–Tulcea construction with respect to a measurable bijection commuting with the kernel; that stopping times are carried to stopping times; that the discounted reward of a stopping time shifts by $c$ times the discounted time; and that the supremum of a nonempty bounded set of reals shifts and scales accordingly. Boundedness of the set of ratios is where the integrability assumption enters. Proposition 7.4 is the chain-level statement that all rewards along every trajectory from a favourable state are at most $r(p)$, which needs an induction on the trajectory law of the target chain, followed by the argument of Proposition 2.7. Example 7.6 needs the monotonicity of $\bar x_m (1 + 1/(n+m))^{-1/2}$ in the observations below the target, a small inequality, plus the Gaussian probability of a half-line as the current probability of success; Example 7.5 needs only that $\alpha/(\alpha + \beta + m)$ decreases.

Formalization scope

The sampling model is a structure with Markov likelihood and prior kernels and a jointly measurable update; the predictive distribution is the kernel composition; conjugacy is an almost-everywhere identity between Mathlib's posterior of the likelihood with respect to the prior and the prior at the updated parameters, and is carried as a hypothesis of the invariance theorems and of Proposition 7.4 so that their subject is the Bayesian process. For the parameters $(\bar x, n)$ it is required on $n > 0$ only (IsConjugateOn): a proper prior has $n > 0$, and conjugacy at every $(\bar x, n) \in \mathbb{R}^2$ is impossible with a location parameter, since at $n = -1$ the update divides by zero and sends every observation to one state, which made the first draft's location theorems vacuous. The chains are built with Kernel.map of product kernels, so their measurability is structural, and the target process lives on P ⊕ Unit with the completion state absorbing. The book's improper priors are replaced by proper conjugate families with the location or scale structure of Corollaries 7.10 and 7.12, as those corollaries do; the discrete-time correction factor of Section 2.8 is not applied since it cancels in every identity stated. The two examples are built directly from a uniform or Gaussian seed with the transition probabilities the book computes (the beta and normal posterior computations of Exercise 7.1 are not formalized). Hypotheses: $a \in (0, 1)$; integrable observations and L&S Assumption 35.6 for the reward processes; $n > 0$ for the invariance theorems and $\bar x > 0$ for the scale theorem; $\alpha, \beta > 0$; $\bar x \ge 0$ and $n > 0$ for the normal example.

Trivializing readings are excluded: the indices are the genuine suprema of the Bandit Algorithms definition with integrable rewards, the update rule is the book's and not a free parameter, and the favourability condition ranges over all finite observation sequences. Welcome contributions: the equivariance of the trajectory measure under a state bijection commuting with the kernel, the transport of stopping times, and the reward bound along the target chain from a favourable state.

Selected references

• J. Gittins, K. Glazebrook, R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011, Chapter 7. doi:10.1002/9780470980033
• J. C. Gittins, D. M. Jones, A dynamic allocation index for the sequential design of experiments, in Progress in Statistics (J. Gani, ed.), North-Holland, 1974.
• D. M. Jones, Search Procedures for Industrial Chemical Research, PhD thesis, University of Wales, 1975.
• H. Raiffa, R. Schlaifer, Applied Statistical Decision Theory, Harvard University Press, 1961.
• T. S. Ferguson, Mathematical Statistics: A Decision Theoretic Approach, Academic Press, 1967.
• T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapters 34–35. doi:10.1017/9781108571401

Motivation

The free energy principle (FEP) proposes that a self-organizing system — a brain, an organism, an agent — persists by minimizing one quantity: the variational free energy of its sensory states under an internal generative model. Introduced by Karl Friston as a principle of brain function [Friston 2006] and stated in its unified form [Friston 2010], the principle makes a precise mathematical claim at its core: whatever internal state estimate the system holds, the free energy of incoming data is never below the data's surprisal (negative log marginal likelihood), and the excess is exactly the Kullback–Leibler divergence between the system's recognition density and the Bayesian posterior implied by the model. Active inference extends the same functional from perception to action and planning [Friston et al. 2017], and the same bound is known in machine learning as the evidence lower bound (ELBO) of variational inference [Parr et al. 2022].

Timeline of the mathematical content this mission formalizes:

• 2006 — Friston, A free energy principle for the brain (J. Physiol. Paris 100): the bound stated for perception as variational inference on a generative model.
• 2010 — Friston, The free-energy principle: a unified brain theory? (Nat. Rev. Neurosci. 11, 127–138): free energy as an upper bound on surprisal, presented as the core of a unified account.
• 2017 — Friston, FitzGerald, Rigoli, Schwartenbeck, Pezzulo, Active inference: a process theory (Neural Comput. 29(1), 1–49): the same functional drives policy selection through expected free energy.
• 2022 — Parr, Pezzulo, Friston, Active Inference (MIT Press): textbook treatment; the posterior-form identity $F = D_{\mathrm{KL}}(Q\,\|\,P(s|o)) - \log P(o)$ as the central equation.
• 2026 — fep_formal (Active Inference Institute): a machine-checked Lean 4 catalogue of 155 Free Energy Principle topics, compiled with zero proof holes against a pinned Mathlib. This mission transcribes the catalogue's core-free-energy chain — topic fep-002 and the foundation module active_inference — onto the platform, turning the first link of the FEP development into solvable community infrastructure.

Setting

Everything is finite, and laws are normalized real mass functions.

A finite law on a finite type $\alpha$ is a function $p : \alpha \to \mathbb{R}$ with $p(x) \ge 0$ for every $x$ and $\sum_x p(x) = 1$. A finite kernel from $\alpha$ to $\beta$ assigns to each $x \in \alpha$ a normalized row over $\beta$. The mission's definitions Def_fep_finite_laws and Def_fep_finite_information package these carriers with entropy, cross-entropy, and the KL divergence

$$D_{\mathrm{KL}}(p\,\|\,q) \;=\; \sum_{x} q(x)\cdot \mathrm{klFun}\!\left(\frac{p(x)}{q(x)}\right), \qquad \mathrm{klFun}(x) = x\log x + 1 - x,$$

a totalized real-valued divergence that is finite even at zero-mass atoms (the convention $0 \cdot \log 0 = 0$ via Real.negMulLog) and nonnegative on normalized laws.

A finite generative model for active inference (definition Def_fep_generative_model) over finite types $\mathsf{Policy}, \mathsf{State}, \mathsf{Outcome}$ consists of: an initial state law $P(s)$; a policy-conditioned transition kernel; a state-to-outcome likelihood kernel; a preference law over outcomes; and a policy prior. Under a policy $\pi$ the model predicts the state law $P(s \mid \pi)$ and the outcome law $P(o \mid \pi)$. A recognition density is any finite law $Q$ over states — the system's internal estimate. At an outcome $o$ with positive predicted mass, the Bayesian posterior $P(\cdot \mid o, \pi)$ is the exact finite Bayes rule. The outcome surprisal is $-\log P(o \mid \pi)$, and the posterior-form variational free energy of a recognition density $Q$ is

$$F[Q, o, \pi] \;=\; D_{\mathrm{KL}}\big(Q \,\|\, P(\cdot \mid o, \pi)\big) \;-\; \log P(o \mid \pi).$$

Formalization targets

Goal: the variational free-energy bound

For every generative model, every policy $\pi$, every outcome $o$ with $P(o\mid\pi) > 0$, and every recognition density $Q$:

$$-\log P(o \mid \pi) \;\le\; F[Q, o, \pi].$$

The recognition density $Q$ is universally quantified — the bound holds for whatever state estimate the system happens to carry.

Exactness, uniqueness, and the ELBO form

Three companions pin down the equality case, ordered weakest to strongest alongside the milestone list:

• Exactness — the Bayesian posterior attains the bound:

$$F\big[P(\cdot \mid o, \pi),\, o,\, \pi\big] = -\log P(o \mid \pi).$$

• Uniqueness — equality characterizes the posterior, with no full-support assumption:

$$F[Q, o, \pi] = -\log P(o \mid \pi) \iff Q = P(\cdot \mid o, \pi).$$

• ELBO form — negating both sides:

$$-F[Q, o, \pi] \;\le\; \log P(o \mid \pi).$$

Measure-theoretic core

Independently of the finite model, in Mathlib's nonnegative extended reals $\mathbb{R}_{\ge0} \cup \{\infty\}$, with $q$, $p$ measures on any measurable space and $s \in \mathbb{R}_{\ge0} \cup \{\infty\}$:

$$s \;\le\; s + D_{\mathrm{KL}}(q \,\|\, p),$$

the unconditional shape of the bound (topic fep-002 of the source catalogue), with the divergence taken as $\infty$ when the log-likelihood ratio is not integrable.

Significance

The result itself. This inequality is the load-bearing step of the FEP: it converts "minimize free energy" into "move recognition toward the posterior," and it is the exact statement whose continuous, dynamic, and policy-selecting extensions (expected free energy, Markov blankets, non-equilibrium thermodynamics) form the rest of the FEP literature. Without it, the principle's variational step has no mathematical content.

Formalizing it. The mathematics here is classical — Gibbs' inequality — and the source development already proves every row with no proof holes. What the mission adds is faithful, reusable infrastructure: the definitions are published as platform nodes in the shared namespace FreeEnergyPrinciple, so later missions in this programme (expected free energy and policy selection, Markov blankets, Gaussian and continuous-time variants, already proved in the source repository) can import them instead of re-deriving the substrate. Status honesty: all eight items below are formalized and machine-checked locally against the platform environment; each is an open problem on the platform only in the sense that no proof has yet been submitted to it.

Difficulty

The bound itself is a one-line consequence of KL nonnegativity — the naive idea "prove it by simp on the KL sum" is essentially right, and the source proofs are correspondingly short. The actual difficulty is boundary precision, where plausible renderings go silently wrong:

• The positivity premise $P(o \mid \pi) > 0$ is not decoration: the Bayesian posterior is defined only where the evidence has positive mass, and hiding that in a totalized division would change the statement.
• The uniqueness characterization is not a formality: at zero-mass reference atoms the logarithmic cross-entropy identity degenerates, and the proof needs the normalization lemma $D_{\mathrm{KL}}(p\,\|\,q) = 0 \leftrightarrow p = q$, which forces the recognition law's mass to zero wherever the posterior's is zero. A solver who proves the bound but states equality with a full-support hypothesis has proved something different from the source.
• The measure-theoretic core is deliberately unconditional; adding finiteness side conditions to it would weaken the source's point that $\mathbb{R}_{\ge0} \cup \{\infty\}$ absorbs the degenerate cases.

A vacuous formalization — quantifying over a single distinguished recognition law, or taking "posterior" as an arbitrary variable — would trivialize the goal; the targets below rule this out by fixing the exact finite Bayes rule and universally quantifying $Q$.

Formalization scope

Committed conventions of this mission's Lean development:

• All model carriers are finite types (Fintype); laws are $\mathbb{R}$-valued normalized mass functions; kernels are normalized rows. No measure-theoretic machinery below the finite substrate except for the measure-theoretic core milestone.
• KL is the totalized real-valued finite divergence $D_{\mathrm{KL}}(p\,\|\,q) = \sum_x q(x)\cdot \mathrm{klFun}(p(x)/q(x))$; entropy uses Real.negMulLog, so $0 \cdot \log 0 = 0$ exactly, not by exception-handling.
• The posterior is the exact finite Bayes rule FiniteKernel.posterior, taken at the explicit hypothesis $0 < P(o \mid \pi)$.
• One mission-wide namespace FreeEnergyPrinciple; definitions live in the published definition files Def_fep_finite_laws, Def_fep_finite_information, Def_fep_generative_model, and every theorem item imports them. A Free Energy Principle II mission (expected free energy) is expected to reuse the same namespace and definitions.
• The measure-theoretic core uses Mathlib's InformationTheory.klDiv in ℝ≥0∞ with no finiteness hypotheses.
• Contributions welcome: alternative measure-theoretic renderings of the core bound, the Gaussian instantiation of the same identity, and ports of the source repository's subsequent rows (Bayesian model reduction, expected free energy) onto these definitions.

Selected references

• K. Friston, A free energy principle for the brain, Journal of Physiology (Paris) 100 (2006) 70–87. https://doi.org/10.1016/j.jphysparis.2006.10.001
• K. Friston, The free-energy principle: a unified brain theory?, Nature Reviews Neuroscience 11 (2010) 127–138. https://doi.org/10.1038/nrn2787
• K. Friston, T. FitzGerald, F. Rigoli, P. Schwartenbeck, G. Pezzulo, Active inference: a process theory, Neural Computation 29 (2017) 1–49. https://doi.org/10.1162/neco_a_00912
• T. Parr, G. Pezzulo, K. J. Friston, Active Inference: The Free Energy Principle in Mind, Brain, and Behavior, MIT Press (2022). https://mitpress.mit.edu/9780262045354/active-inference/
• D. A. Friedman, fep_formal: Towards Lean 4 Formalization of the Free Energy Principle (v1.2.0), Active Inference Institute (2026), the formal source of truth for this mission. https://github.com/ActiveInferenceInstitute/fep_formal
• D. A. Friedman, Towards Lean 4 Formalization of the Free Energy Principle: AI-Driven Theorem Sketching and Verification for Active Inference and Bayesian Mechanics, Active Inference Journal (2026). https://doi.org/10.5281/zenodo.19699233

Motivation

The bilinear program

$$\min_{(x,y)} \; c^T x + x^T A y + d^T y \quad \text{subject to} \quad x \in X,\ y \in Y,$$

with $X \subseteq \mathbb{R}^p$ and $Y \subseteq \mathbb{R}^q$ polyhedra, is one of the recurring nonconvex problems of mathematical programming. It arises from constrained bimatrix games (Mangasarian 1964), dynamic Markovian assignment, multicommodity network flow and certain dynamic production problems (Konno 1971, 1976). Its classical structural fact is that, because the constraints on $x$ and on $y$ are separate and the objective is linear in each block, an optimal solution can be found at an extreme point of $X \times Y$ (Falk 1973, doi:10.1007/BF01580119). Vertex-enumeration, extreme-point ranking and cutting-plane methods for the problem rest on that fact.

Al-Khayyal and Falk (Math. Oper. Res. 8(2), 1983) consider the jointly constrained version, in which the feasible region is an arbitrary set $S$ of pairs $(x, y)$, so that constraints may couple $x$ and $y$. They observe that the extreme-point property is then lost, and replace it with a weaker structural fact that survives: a minimum is attained on the boundary of the feasible region. This mission formalizes that result, Theorem 1 of the paper, together with the two examples on p. 274 that delimit it.

Setting

Write points of $\mathbb{R}^p \times \mathbb{R}^q$ as $(x, y)$, and let $S \subseteq \mathbb{R}^p \times \mathbb{R}^q$ be a nonempty compact set. No convexity of $S$ is assumed. Let $\varphi : \mathbb{R}^p \times \mathbb{R}^q \to \mathbb{R}$ be continuous on $S$.

The function $\varphi$ is biconcave over $S$ (Lean: BiconcaveOn S φ) when both partial functions are concave wherever they live inside $S$: for every fixed $y$, the map $x \mapsto \varphi(x, y)$ is concave on every convex set $C$ with $C \times \{y\} \subseteq S$; and for every fixed $x$, the map $y \mapsto \varphi(x, y)$ is concave on every convex set $D$ with $\{x\} \times D \subseteq S$. Equivalently, $\varphi$ is concave along every segment of $S$ that is parallel to the $x$-block or to the $y$-block. A bilinear objective $f(x) + x^T y + g(y)$ with $f$ and $g$ concave is biconcave; joint concavity of $\varphi$ is not required.

The boundary $\partial S$ is the topological frontier of $S$ in $\mathbb{R}^p \times \mathbb{R}^q$: the closure of $S$ minus its interior. A solution of $\min\{\varphi(x,y) : (x,y) \in S\}$ is a point $z \in S$ with $\varphi(z) \le \varphi(w)$ for all $w \in S$ (Lean: IsMinOn φ S z). The Euclidean distance on the product (Lean: eucDist) is $d\big((x,y),(x',y')\big) = \sqrt{\|x-x'\|^2 + \|y-y'\|^2}$.

Formalization targets

Goal: Theorem 1 (p. 274)

If $S \subseteq \mathbb{R}^p \times \mathbb{R}^q$ ($p + q \ge 1$) is nonempty and compact, and $\varphi$ is continuous on $S$ and biconcave over $S$, then

$$\exists\, z^* \in \partial S \quad \text{with} \quad \varphi(z^*) = \min\{\varphi(x, y) : (x, y) \in S\}.$$

The conclusion is existence of a boundary minimizer. It does not assert that every minimizer lies on $\partial S$ (a constant $\varphi$ is a counterexample to that).

Milestones

1. Proof of Theorem 1, p. 274. If $(\bar x, \bar y) \in \operatorname{int} S$ and $(x^*, y^*) \in \partial S$ is a nearest boundary point in Euclidean distance $d^*$, then the closed Euclidean ball of radius $d^*$ about $(\bar x, \bar y)$ lies in $S$, and with $(s,t) = 2(\bar x, \bar y) - (x^*, y^*)$ the points $(s,t)$, $(x^*, t)$ and $(s, y^*)$ are feasible.
2. Proof of Theorem 1, p. 275, first display. For $\varphi$ biconcave over $S$ and segments $[x^*, s] \times \{\tfrac12 y^* + \tfrac12 t\}$, $\{x^*\} \times [y^*, t]$, $\{s\} \times [y^*, t]$ inside $S$,

$$\varphi\big(\tfrac12(x^*,y^*) + \tfrac12(s,t)\big) \ge \tfrac12\varphi(x^*, \tfrac12y^*+\tfrac12t) + \tfrac12\varphi(s, \tfrac12y^*+\tfrac12t) \ge \tfrac14\big[\varphi(x^*,y^*)+\varphi(x^*,t)+\varphi(s,y^*)+\varphi(s,t)\big].$$

3. Example, p. 274. The program $\min\{-x + xy - y : -6x + 8y \le 3,\ 3x - y \le 3,\ 0 \le x, y \le 5\}$ has the solution $(7/6, 1/2)$, which is not an extreme point of the feasible region, and no extreme point is a solution.
4. Example, p. 274. $\min\{xy : -1 \le x \le 2,\ -2 \le y \le 3\}$ has local solutions at $(-1, 3)$ and $(2, -2)$, the first of which is not global.

Significance

Theorem 1 is the structural statement that separates jointly constrained bilinear and biconcave programs from their separably constrained special case. It says where a global search may restrict attention, namely to $\partial S$, and example 3 shows that this cannot be sharpened to extreme points once the constraints couple the blocks. Example 4 records that such problems have proper local minima, so a local method alone does not solve them; this motivates the branch-and-bound algorithm of the same paper, which is the subject of the companion mission.

The result is proved in the paper; this mission produces its machine-checked statement and proof. Mathlib contains the Bauer-type principle for jointly concave functions on compact convex sets, but no statement of this kind for biconcave functions on nonconvex sets, and no formalization of Theorem 1 is known. The two examples are small but exact computations, and they certify that the definitions admit the intended instances.

Difficulty

The first idea is to apply the concave-minimization principle: a concave function on a compact convex set attains its minimum at an extreme point. It does not apply. $S$ need not be convex, so it has no useful extreme-point structure, and $\varphi$ is concave only along segments parallel to one block, so it is not concave along the segment from an interior point to a boundary point in a general direction. Example 3 shows that the conclusion "extreme point" is actually false here.

What remains is local geometry around an interior minimizer: one must find points of $S$ around it at which biconcavity can be applied in both blocks, and control their membership in $S$ without convexity. The feasibility of the mixed points $(x^*, t)$ and $(s, y^*)$, which the paper uses without comment, is where the choice of the Euclidean distance matters, and it is recorded as a separate milestone.

Formalization scope

• Points are pairs in EuclideanSpace ℝ (Fin p) × EuclideanSpace ℝ (Fin q). The boundary is Mathlib's frontier in this product; it does not depend on the norm. Only milestone 1 refers to a distance, and it uses eucDist, the Euclidean distance written out, because Mathlib's default metric on a product is the maximum of the block distances.
• The theorem is the "more general context" of p. 274, independent of the paper's Problem 𝒫: the standing assumptions (a)–(c) of p. 274 (convex $f$, $g$; closed convex $S$; a box $\Omega$) do not enter.
• Hypotheses of the goal: IsCompact S, S.Nonempty, ContinuousOn φ S (continuity only on $S$), and BiconcaveOn S φ. One hypothesis is added: $0 < p + q$. For $p = q = 0$ the space is a point, whose only nonempty subset has empty frontier, so the conclusion fails; the paper works in positive dimension throughout.
• Biconcavity is read over $S$: concavity on every convex subset of each section of $S$. Assuming instead concavity of each partial function on the whole space would be a stronger hypothesis and a weaker theorem.
• Trivializing formalizations ruled out: the statement assumes neither joint concavity of $\varphi$ nor convexity of $S$ (either would reduce it to the Bauer principle), and it covers sets with nonempty interior; the case of empty interior, where $\partial S = S$, is included but is not the only case.
• Corrected misprint (milestone 3): the paper prints the solution of example 3 as $(7/16, 1/2)$. That point has objective value $-23/32$, while the feasible vertex $(1,0)$ has value $-1$. On the edge $3x - y = 3$ the objective equals $3x^2 - 7x + 3$, minimized at $x = 7/6$, value $-13/12$, the global minimum. The Lean states the corrected point $(7/6, 1/2)$; the milestone text is kept verbatim.
• In milestone 4, "local solution" is IsLocalMinOn relative to the box, and non-globality of $(-1, 3)$ records the paper's word "proper".
• Infrastructure needed: nearest boundary points of compact sets (Mathlib has IsCompact.exists_mem_frontier_infDist_compl_eq_dist, stated for the ambient metric), the fact that a closed ball about an interior point whose radius is the distance to the frontier lies in the set, and concavity on segments. A lemma that works for an arbitrary norm on the product would be reusable. Contributions of alternative proofs are welcome.

Selected references

• Faiz A. Al-Khayyal and James E. Falk, Jointly Constrained Biconvex Programming, Mathematics of Operations Research 8(2):273–286, 1983. https://doi.org/10.1287/moor.8.2.273
• James E. Falk, A Linear Max-Min Problem, Mathematical Programming 5:169–188, 1973. https://doi.org/10.1007/BF01580119
• Hiroshi Konno, A Cutting Plane Algorithm for Solving Bilinear Programs, Mathematical Programming 11:14–27, 1976. https://doi.org/10.1007/BF01580367
• Olvi L. Mangasarian, Equilibrium Points of Bimatrix Games, Journal of the Society for Industrial and Applied Mathematics 12(4):778–780, 1964. https://doi.org/10.1137/0112064
• Heinz Bauer, Minimalstellen von Funktionen und Extremalpunkte, Archiv der Mathematik 9:389–393, 1958. https://doi.org/10.1007/BF01900582