Probability

Motivation

Many selection problems assign a value to each subset of a finite collection: the coverage supplied by chosen facilities, the influence reached by chosen seeds, or the value of a coalition. A submodular set function has diminishing returns in the precise sense that the combined value of two sets, counting their overlap once, does not exceed the sum of their separate values. When the function is also monotone, taking more elements never hurts. The unconstrained problem studied here permits nonmonotone functions, so both accepting and rejecting an element can matter. The question is what a single pass through the elements can guarantee when the function is available through value queries. Buchbinder et al., FOCS 2012

The randomized algorithm in this mission attains an expected one-half approximation for every nonnegative submodular function. The paper presents this as tight in the value-oracle setting: it recalls the earlier result of Feige, Mirrokni and Vondrák that a fixed improvement beyond one-half requires exponentially many queries. The contribution here is therefore both the guarantee and a short adaptive rule that attains it in a linear number of iterations. The local proposal follows the FOCS 2012 version of the paper; its theorem numbering differs from the later SIAM Journal on Computing article. Buchbinder et al., §I.A and Theorem I.2

Setting

Let $\mathcal N$ be a finite ground set, and let $f:2^{\mathcal N}\to\mathbb R_{\ge0}$ assign a nonnegative real value to every subset. The unconstrained submodular maximization problem asks for the largest value $f(S)$ among all $S\subseteq\mathcal N$. Write $OPT$ for that value when no confusion arises, and $O$ for a set attaining it. Submodularity means

$$f(A\cup B)+f(A\cap B)\le f(A)+f(B)\qquad(A,B\subseteq\mathcal N).$$

There is no monotonicity or normalization assumption: $f(\varnothing)$ and $f(\mathcal N)$ may both be positive. A value oracle returns $f(S)$ for a requested subset $S$. The paper's complexity claim counts such queries, assuming a query takes constant time. Buchbinder et al., §I and footnotes 1–2

Algorithm 2 visits the elements once in an arbitrary order $u_1,\ldots,u_n$. It keeps two sets, starting at $X_0=\varnothing$ and $Y_0=\mathcal N$. At step $i$, it measures the gain $a_i$ from adding $u_i$ to $X_{i-1}$ and the gain $b_i$ from removing $u_i$ from $Y_{i-1}$. It clips each gain at zero, giving $a'_i=\max(a_i,0)$ and $b'_i=\max(b_i,0)$. It adds $u_i$ to $X$ with probability $a'_i/(a'_i+b'_i)$ and otherwise removes it from $Y$. When both clipped gains vanish, the paper defines the add probability as one. After all elements have been processed, the two sets coincide, and the algorithm returns their common value. The state law is adaptive: its probability at step $i$ depends on the actual pair of sets produced by earlier choices. Buchbinder et al., Algorithm 2

Formalization targets

The main target is Theorem I.2 for this exact algorithm and for every enumeration of the ground set:

$$\max_{S\subseteq\mathcal N}f(S)\le 2\,\mathbb E[f(X_n)].$$

The milestone statements retain the paper's key local quantities. For a comparison optimum $O$, set $OPT_i=(O\cup X_i)\cap Y_i$. Lemma II.1 asserts $a_i+b_i\ge0$. The endpoint statement identifies $OPT_0=O$ and $OPT_n=X_n=Y_n$. Inequality (3) bounds the conditional loss in the positive-gain case; Lemma III.1 compares the expected change of $OPT_i$ with the expected combined change of $X_i$ and $Y_i$. The telescoped display keeps the initial endpoint values $f(\varnothing)$ and $f(\mathcal N)$ before using nonnegativity. Buchbinder et al., Lemmas II.1 and III.1, inequality (3), proof of Theorem I.2

A companion target is Theorem I.4 via its second proof. For two normalized monotone submodular utilities $f_1,f_2$, let $g(S)=f_1(S)+f_2(\mathcal N\setminus S)$. The maximum of $g$ is exactly the optimal welfare of a two-player partition. Algorithm 2 on $g$ is asked to satisfy

$$3\max_{S\subseteq\mathcal N}g(S)\le4\,\mathbb E[g(X_n)].$$

This is the paper's three-quarter guarantee in its welfare application. Buchbinder et al., Theorem I.4 and Proof (2)

Significance

The main theorem gives a specific randomized rule whose expected value is at least half the best subset value, even when accepting an element can lower the objective. It applies without restricting the cardinality or shape of the chosen subset. The welfare corollary shows that keeping the initial endpoint values in the analysis yields a stronger guarantee for the objective formed from two monotone players. Buchbinder et al., Theorems I.2 and I.4

This mission formalizes the statement of the algorithm, its intermediate state laws, its comparison set, and the paper's numbered proof targets. The algorithmic guarantee is proved in the source paper; the local Lean theorem files are open statements with sorry and do not yet give machine-checked proofs of these results. A completed development would supply a reusable formal model of an adaptive finite random process over pairs of subsets, as well as the specific submodular inequalities. The published Submodular and OPT definitions from the earlier Feige–Mirrokni–Vondrák formalization are reused here.

Difficulty

The two possible updates cannot be assessed independently. The probability of each choice depends on the current state, and the comparison set $OPT_i$ can gain or lose the processed element in a way that differs from the two algorithm sets. A bound on the expected value of $X_i$ alone does not control the movement of $OPT_i$. The proof must handle the clipped gains, including the case when both are zero, while preserving the exact joint law of $(X_i,Y_i)$. Buchbinder et al., proof of Lemma III.1

Formalization scope

The ground set is a finite Lean type; subsets are Finset X, and values are real numbers. An order is a list with no repeated elements that covers the type, including the empty type. The run is an explicit finite mass function on pairs of subsets after every prefix of the list. Expectation is a finite weighted sum, so it has no integrability exception. The transition clips the two real marginal gains and handles $0/0$ by assigning probability one to the add branch, exactly as Algorithm 2 specifies. The optimum is the published maximum over all subsets. No ratio divides by a possibly zero optimum.

The theorem fixes Algorithm 2 itself; an arbitrary process with nested sets or a process defined by its desired approximation property does not satisfy this scope. The Lean goal states the value bound and leaves the paper's linear-time claim outside the formal theorem. The algorithm uses four value evaluations per processed element in its printed rule; the Lean development represents those evaluations, not an implementation cost model. The statement that its two final sets coincide is a separate milestone.

The source's main-text decreasing-returns definition has an overbroad quantifier on the added element. This development uses the equivalent lattice inequality given in the paper's footnote, which permits nonmonotone functions. The proof of Lemma II.1 also has a set-index slip, and the proof of Theorem I.2 prints $F$ for $f$ in one display; neither slip is copied into a formal statement. The one-step inequality (3) is stated for any nested pair with the processed element in $Y\setminus X$, a generalization of the conditioned reachable states in the paper. Contributions proving the endpoint invariant, conditional inequality, one-step expected estimate, and final bound are all within scope.

Selected references

• Niv Buchbinder, Moran Feldman, Joseph Naor and Roy Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, Proceedings of the 53rd IEEE Symposium on Foundations of Computer Science, 2012. FOCS version used here.
• Niv Buchbinder, Moran Feldman, Joseph Naor and Roy Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, SIAM Journal on Computing 44(5), 2015. DOI: 10.1137/130929205. The cited statement indices above refer to the FOCS version.

Motivation

The conditional logit model is the workhorse of discrete choice analysis: it is used to forecast travel mode shares, to estimate demand for differentiated products, and, in operations research, as the multinomial logit (MNL) choice model behind assortment optimization and revenue management. Its selection probabilities have the form $P(x\mid s,B) = e^{v(s,x)}/\sum_{y\in B} e^{v(s,y)}$. Daniel McFadden's 1974 chapter Conditional Logit Analysis of Qualitative Choice Behavior gave the model two behavioural foundations, one of which is the subject of this mission: the logit form is a consequence of a single axiom on how choice probabilities change when the set of available alternatives changes.

That axiom is Luce's choice axiom, which McFadden calls Independence of Irrelevant Alternatives (IIA): the relative odds of choosing one alternative over another do not depend on which other alternatives are present. Luce (1959) introduced it; McFadden (1974, §I) showed how, together with positivity and a mild condition on which alternative sets can occur, it yields the conditional logit form with a "utility indicator" $v(s,x)$ shared by all alternative sets.

Timeline. Luce, Individual Choice Behavior (1959): the choice axiom and its ratio-scale representation. McFadden (1974, pp. 109–110): the derivation in the econometric setting with measured attributes $s$, the binary-odds identities (5)–(10), and footnote 3, which removes an extra axiom (Axiom 3) by a universal benchmark alternative. McFadden (1974, pp. 111–112): the companion random-utility characterization by extreme-value shocks, treated in mission 2 of this series.

Setting

Let $X$ be the universe of objects of choice and $S$ the universe of vectors of measured attributes of decision-makers. An alternative set is a finite set $B\subseteq X$; a designated family of finite sets is the family of possible alternative sets. The selection probability $P(x\mid s,B)$ is the probability that an individual drawn at random from the population, with attributes $s$ and facing $B$, chooses $x\in B$. For every $s$ and possible $B$, $x\mapsto P(x\mid s,B)$ is a probability vector on $B$. Whenever $x\neq y$ belong to a possible set, the pair $\{x,y\}$ is possible too, so binary choices are defined.

• Axiom 1 (IIA). For all possible $B$, all $s$ and all $x,y\in B$: $P(x\mid s,\{x,y\})P(y\mid s,B) = P(y\mid s,\{x,y\})P(x\mid s,B)$.
• Axiom 2 (Positivity). $P(x\mid s,B)>0$ for all possible $B$, all $s$, all $x\in B$.
• Binary probabilities. $p_{xy}=P(x\mid s,\{x,y\})$ for $x\neq y$, and $p_{xx}=\tfrac12$ by definition.
• The function $V$. $V(s,x,z)=\log(p_{xz}/p_{zx})$.
• Universal benchmark. An alternative $z$ such that $B\cup\{z\}$ is possible whenever $B$ is.

In Lean these are IsSelectionProb, PairsPossible, Axiom1, Axiom2, binProb, altSetV and IsUniversalBenchmark in the namespace McFadden1974.IIA.

Formalization targets

Goal: footnote 3 with Equation (12)

Under Axioms 1 and 2 and a universal benchmark $z$, with $v(s,x)=V(s,x,z)$, for every $s$, every possible $B$ (containing $z$ or not) and every $x\in B$:

$$P(x\mid s,B) = \frac{e^{v(s,x)}}{\sum_{y\in B} e^{v(s,y)}}.$$

The function $v$ is the same for all alternative sets; this is what distinguishes the goal from Equation (10).

Milestones, in the paper's order

1. Equation (5): for $x\neq y$ in $B$ with $P(x\mid s,B)>0$, Axiom 1 gives $P(x\mid s,\{x,y\})>0$ and $\dfrac{P(y\mid s,\{x,y\})}{P(x\mid s,\{x,y\})}=\dfrac{P(y\mid s,B)}{P(x\mid s,B)}$.
2. Equations (6)–(7): $P(y\mid s,B)=\dfrac{p_{yx}}{p_{xy}}P(x\mid s,B)$ and $1=\Big(\sum_{y\in B}\dfrac{p_{yx}}{p_{xy}}\Big)P(x\mid s,B)$.
3. Equation (8): $P(x\mid s,B)=1\big/\sum_{y\in B}(p_{yx}/p_{xy})$.
4. Equation (9): $\dfrac{p_{yx}}{p_{xy}}=\dfrac{p_{yz}/p_{zy}}{p_{xz}/p_{zx}}$ for $x,y,z$ in a possible set.
5. Equation (10): for a benchmark $z\in B$, $P(x\mid s,B)=e^{V(s,x,z)}\big/\sum_{y\in B}e^{V(s,y,z)}$.

Significance

The result. The goal identifies a testable axiom on choice probabilities, IIA, with a parametric functional form, the conditional logit model. It is what licenses the econometric specification $v(s,x)=\theta'z(s,x)$ estimated in the rest of McFadden's chapter, and it is the reason the MNL model is the default in assortment and pricing problems in operations research. It also makes the model's limitations precise: any population whose choices violate IIA (the auto/red-bus/blue-bus example on p. 113 of the chapter) cannot be logit.

Formalizing it. The result is classical and proved on paper. No machine-checked statement of it exists on the platform, which has the logit form only as a definition (soft-max, MNL revenue) and IIA only in Arrow's social-choice sense, a different axiom about preference aggregation. This mission produces a formal statement of the derivation with every standing assumption explicit, including two the paper leaves implicit: that selection probabilities are normalized on binary sets, and that binary subsets of possible sets are possible.

Difficulty

The algebra is elementary; the difficulty is bookkeeping of where each axiom may be applied. Axioms 1 and 2 are assumed only on possible alternative sets. Equation (10) needs the benchmark to lie in the alternative set, and the naive argument "pick $z\in B$ as benchmark" produces a function $V(s,x,z)$ that depends on the set through the choice of $z$. The goal requires a single $v$ for all sets, including sets that do not contain $z$, where neither Equation (10) nor the axioms on $B$ alone say anything about $z$. A second subtlety is the diagonal: $\{x,x\}=\{x\}$, so $p_{xx}$ is set to $\tfrac12$ by definition rather than read off a singleton choice.

Formalization scope

Alternatives form a type X with decidable equality, alternative sets are Finset X, possible sets are a Set (Finset X), and selection probabilities are a real-valued function P : S → Finset X → X → ℝ. Only values P s B x with x ∈ B and B possible are constrained; no statement depends on the others. binProb sets the diagonal to 1/2. altSetV uses Real.log, which is 0 on non-positive arguments; under Axiom 2 on the binary sets its argument is always positive where it is used.

The probability-vector hypothesis on every possible set, binary sets included, is part of every statement: without it the zero function satisfies Axiom 1 vacuously and Equations (7)–(8) fail. The goal is stated with the explicit $v(s,x)=V(s,x,z)$, never as "for each $B$ there is a $v$", which would only restate (10).

Nothing beyond Mathlib's finite sums, Real.exp and Real.log is needed. Proofs of the milestones and of the goal are welcome, as is a formal statement of the auto/bus example or of the converse (logit selection probabilities satisfy Axioms 1 and 2).

Selected references

• D. McFadden, Conditional logit analysis of qualitative choice behavior, in P. Zarembka (ed.), Frontiers in Econometrics, Academic Press, New York, 1974, pp. 105–142. https://eml.berkeley.edu/reprints/mcfadden/zarembka.pdf
• R. D. Luce, Individual Choice Behavior: A Theoretical Analysis, Wiley, New York, 1959. https://doi.org/10.1037/14396-000

Why protection levels and their inputs matter

An airline sells the seats of one flight leg in several fare classes at different prices. Low-fare passengers usually book first, so the airline must decide how many seats to keep back, or protect, for later high-fare passengers. Peter Belobaba's 1987 MIT dissertation introduced the expected marginal seat revenue (EMSR) rule for this decision, and EMSR-type rules became a standard of airline revenue management practice (Talluri and van Ryzin 2004). A protection level is computed from a demand forecast, and forecasts are uncertain. Section 6.2 of the dissertation asks how the protection level moves when its inputs move: the mean of forecast demand, its standard deviation, and the ratio of the two fares. That question decides where forecasting effort pays off, and this mission formalizes the answers the dissertation gives for Gaussian demand.

This is the third mission in a series on the dissertation. The first treats marginal allocation among distinct fare classes, and the second the two-class nested protection level in the discrete model, including its revenue optimality. This mission takes the continuous Gaussian model of Chapter 6 on its own terms.

Setting

Let $r$ be the number of requests for a fare class, a real random variable with law $\mu$. For a seat level $S \in \mathbb R$ the tail probability is

$$\bar P(S) = P[r \ge S],$$

and for the fare $f$ of the class the expected marginal seat revenue is $\mathrm{EMSR}(S) = \bar P(S)\cdot f$ (Eqs. (6.1)–(6.2)).

There are two classes: class 1 with fare $f_1$ and class 2 with fare $f_2$, where $0 < f_2 < f_1$. Requests for class 1 are Gaussian with estimated mean $\bar r$ and estimated standard deviation $\hat\sigma > 0$, written $r_1 \sim N(\bar r, \hat\sigma^2)$. A real number $S$ is an EMSR protection level for class 1 against class 2 when

$$\bar P_1(S) = P[r_1 \ge S] = \frac{f_2}{f_1} \qquad \text{(Eq. (6.10))}.$$

The standardized level $Z$ is the value "which has a probability of $f_2/f_1$ of being exceeded" by a standard normal variable:

$$P[N(0,1) \ge Z] = \frac{f_2}{f_1}.$$

In the Lean development these are tailProb, emsr, gaussianLaw rbar σ, stdNormal, IsProtectionLevel rbar σ f₁ f₂ S and IsStdNormalLevel f₁ f₂ Z, all in the namespace SeatInventory.Gaussian.

Formalization targets

Goal: the Gaussian protection level and its sensitivity to $\hat\sigma$

For $\hat\sigma > 0$ and $0 < f_2 < f_1$:

1. Eq. (6.10) has exactly one solution $S$, and the standard normal equation has exactly one solution $Z$;
2. they satisfy

$$S = \bar r + Z\hat\sigma \qquad \text{(Eq. (6.12))};$$

3. $Z < 0$ if $f_2/f_1 > 1/2$, $Z > 0$ if $f_2/f_1 < 1/2$, $Z = 0$ if $f_2/f_1 = 1/2$ (Eq. (6.14)), and $S = \bar r$ in the last case;
4. if $\hat\sigma' > \hat\sigma$ and $S'$ solves (6.10) for $N(\bar r, \hat\sigma'^2)$, then $S' < S$, $S' > S$ or $S' = S$ according as $f_2/f_1$ is above, below or equal to $1/2$.

The goal states no numerical constant and no particular fare ratio; it fixes only the shape of the dependence.

Milestones, in attack order

• Eq. (6.1)–(6.2): for any request law, $\bar P$ and $\mathrm{EMSR}$ are non-increasing in $S$.
• Eq. (6.10): the Gaussian protection level exists and is unique.
• Eq. (6.11)–(6.12): $S = \bar r + Z\hat\sigma$.
• p. 154: with $\hat\sigma$ and the fares fixed, replacing $\bar r$ by $\bar r + c$ replaces $S$ by $S + c$.
• Eq. (6.14): the sign of $Z$, and $S = \bar r$ at fare ratio $1/2$ for every $\hat\sigma$.
• p. 154: the effect of $\hat\sigma$ on $S$ (part 4 of the goal on its own).
• p. 157: $Z$ and $S$ decrease strictly as the fare ratio $f_2/f_1$ increases.

The dissertation's constant-coefficient-of-variation form, Eq. (6.13), $S = \bar r(1 + Zk)$ with $k = \hat\sigma/\bar r$, follows from (6.12) by substitution and is not stated separately.

Significance

The result gives every Gaussian protection level as a closed form in one standard normal quantile. From it come the three sensitivities that Sect. 6.2 uses to argue for better forecasts. The protection level moves one-for-one with mean demand. The standard deviation moves it in a direction fixed only by whether the discount fare is above or below half the full fare. A higher fare ratio always lowers it. The dissertation uses these facts, and its Figures 6.1 and 6.2, to argue that reducing the estimated standard deviation of demand narrows the range of protection levels a forecast can produce. The same quantile structure is behind Littlewood's rule and the newsvendor critical fractile, so the statements here are the Gaussian specialization of a pattern that recurs throughout revenue management and inventory theory.

All the statements are classical and easy to believe. None of them, to our knowledge, has a machine-checked proof. Mathlib provides the Gaussian law and its affine images, but no standard normal quantile and no statement that a Gaussian tail is a strictly decreasing bijection onto $(0,1)$. Formalizing this mission produces both, in a form that can be used again wherever a normal critical fractile appears.

Difficulty

Most of the work is in the existence and uniqueness of the two tail solutions. The tail $S \mapsto P[r_1 \ge S]$ must be shown continuous, strictly decreasing, and to take every value in $(0,1)$. Strictness needs the Gaussian density to be positive everywhere, and existence needs a limit argument at both ends. Monotonicity alone, which holds for every law (Eqs. (6.1)–(6.2)), gives neither, because a general law can have flat stretches and jumps in its tail. The relation $S = \bar r + Z\hat\sigma$ then requires transporting the tail of $N(\bar r,\hat\sigma^2)$ to that of $N(0,1)$ through the affine map $x \mapsto (x - \bar r)/\hat\sigma$, and the sign of $Z$ requires the symmetry of $N(0,1)$, namely $P[N(0,1) \ge 0] = 1/2$. Once uniqueness is available, each sensitivity statement follows from these facts. The tempting shortcut of reading $S = \bar r + Z\hat\sigma$ as a definition is ruled out below.

Formalization scope

• Continuous seats. Protection levels and $Z$ are real numbers, as in the dissertation's own Gaussian example ($Z = -0.675$ at fare ratio $0.75$). This differs from the first two missions of the series, which count seats in $\mathbb N$. For a continuous law $P[r \ge S] = P[r > S]$, so the two definitions of $\bar P$ the dissertation uses (Eq. (5.2) and Eq. (6.2)) coincide here.
• Gaussian law. $N(\bar r, \hat\sigma^2)$ is Mathlib's gaussianReal rbar (σ^2), parameterised by the variance. Every theorem assumes $\hat\sigma > 0$; at $\hat\sigma = 0$ the law is a Dirac mass and (6.10) has no solution.
• Fares. $0 < f_2 < f_1$, so $f_2/f_1 \in (0,1)$. This is the dissertation's "$f_2 < f_1$" together with positive fares.
• Relational sensitivity. The sensitivity statements compare any two solutions of (6.10) under the two input values. Together with uniqueness, this is the same as monotonicity of the solution map. No function is defined by a choice operator.
• Tail as a real number. $\bar P(S)$ is the measure of $[S,\infty)$ as a real number. The law is a probability measure, so nothing is truncated.
• No trivialization. $S$ is defined only by the tail equation (6.10) for $N(\bar r, \hat\sigma^2)$, and $Z$ only by the tail equation for $N(0,1)$. Neither is defined by the formula $S = \bar r + Z\hat\sigma$, which would make Eq. (6.12) true by definition.
• Not covered. The revenue optimality of the level defined by (6.10) belongs to the second mission. The multi-class EMSR rules (5.19)–(5.29) are not optimal for three or more classes and are not stated. The empirical analysis of Sect. 6.1 is out of scope.

Useful infrastructure, all reusable: the strict monotonicity, continuity and range of Gaussian tails; the standard normal quantile; and tail transport under affine maps. Contributions of these as separate lemmas are welcome.

Selected references

• P. P. Belobaba, Air Travel Demand and Airline Seat Inventory Management, PhD thesis, MIT Flight Transportation Laboratory Report R87-7, 1987. (no DOI; the source PDF of this mission).
• P. P. Belobaba, Application of a probabilistic decision model to airline seat inventory control, Operations Research 37(2):183–197, 1989. https://doi.org/10.1287/opre.37.2.183
• K. Littlewood, Forecasting and control of passenger bookings, AGIFORS Symposium Proceedings 12, 1972; reprinted in Journal of Revenue and Pricing Management 4:111–123, 2005. https://doi.org/10.1057/palgrave.rpm.5170134
• K. T. Talluri and G. J. van Ryzin, The Theory and Practice of Revenue Management, Springer, 2004. https://doi.org/10.1007/b139000

Motivation

In the classical secretary problem a decision maker sees $n$ candidates in a uniformly random order and must accept or reject each one on arrival, irrevocably, aiming to accept a valuable one. Its online, random-order structure models hiring, selling an item to sequentially arriving buyers, and posting prices in online markets. Babaioff, Dinitz, Gupta, Immorlica and Talwar (SODA 2009) study the discounted secretary problem, where the reward of a selection depends on when it is made: a candidate accepted late is worth less (or more) by a time-dependent factor, as with a seller whose revenue decays with time, or a firm that loses value the longer a position stays empty.

Timeline of the setting:

• Dynkin (1963) introduced the classical problem; the rule "observe a $1/e$ fraction, then accept the first record" selects the best candidate with probability tending to $1/e$.
• Rasmussen and Pliska (1975/76) and Mahdian, McAfee and Pennock (2008, personal communication cited by the paper) studied secretary problems with specific "well-behaved" discount functions such as $d(t)=\beta^t$.
• Babaioff et al. (2009) treat an arbitrary discount function $d$. Without prior knowledge, no algorithm is better than $\Omega(\log n/\log\log n)$-competitive (their Theorem 4.3), and $O(\log n)$ is achievable (Theorem 4.4). If the algorithm knows a good estimate $Z$ of the expected offline optimum, a single threshold rule recovers a constant fraction (Theorem 4.7, headlined as Theorem 1.2). This mission formalizes that last result.

Setting

There are $n\ge1$ elements, indexed by $\mathrm{Fin}\,n$. Element $e$ has a value $v(e)\ge0$, and each time $t\in\{1,\dots,n\}$ has a discount $d(t)\ge0$. The elements arrive in a uniformly random order $\pi$, a bijection from times to elements: element $\pi(t)$ arrives at time $t$. Selecting the element that arrives at time $i$ earns $d(i)\,v(\pi(i))$, and an algorithm selects at most one element.

The offline optimum on the order $\pi$ is $\mathrm{OPT}(\pi)=\max_{i=1}^n d(i)\,v(\pi(i))$. It is a random variable, and the benchmark is its expectation

$$\mathbf E[\mathrm{OPT}]=\sum_{\pi\in S_n}\frac1{n!}\max_{i=1}^n\{d(i)\,v(\pi(i))\}.$$

For a real parameter $Z$, algorithm $\mathcal A$ selects the first time $j$ at which $d(j)\,v(\pi(j))\ge Z/2$ and earns that product; if no time qualifies, it selects nothing and earns $0$. It knows $Z$ and $d$, sees the values one at a time, and never sees the future of $\pi$. Its expected value is $\mathbf E[\mathcal A]=\sum_{\pi\in S_n}\frac1{n!}\,\mathcal A(\pi)$.

The proof uses three derived objects:

• the accepting permutations $S_{acc}=\{\pi:\max_i d(i)v(\pi(i))\ge Z/2\}$, on which $\mathcal A$ selects something;
• their contribution $L=\sum_{\pi\in S_{acc}}\frac1{n!}\max_i d(i)v(\pi(i))$ to $\mathbf E[\mathrm{OPT}]$;
• for a time $i$ and an element $j$, the set $G_{ij}$ of orders on which $\mathcal A$ selects $j$ at time $i$. These are the orders with $\pi(i)=j$ and $d(k)v(\pi(k))<Z/2$ for every $k<i$.

Formalization targets

Goal: Theorem 4.7

For every $n\ge1$, all discounts $d\ge0$, all values $v\ge0$ and every real $Z$,

$$Z\le\mathbf E[\mathrm{OPT}]\ \Longrightarrow\ \mathbf E[\mathcal A]\ \ge\ \frac Z4.$$

Taking $Z=\mathbf E[\mathrm{OPT}]$ gives $\mathbf E[\mathrm{OPT}]\le4\,\mathbf E[\mathcal A]$, a $4$-competitive algorithm when the expected optimum is known.

Milestones (in the order of the paper's proof, p. 8)

1. Eq. (4.1). If $Z\le\mathbf E[\mathrm{OPT}]$ then $L\ge Z/2$.
2. Eq. (4.3). If $Z\le\mathbf E[\mathrm{OPT}]$ then

$$\sum_{i=1}^n\sum_{j:\,d(i)v(j)\ge Z/2}\frac1n\,d(i)v(j)\ \ge\ \frac Z2.$$

3. Eq. (4.4). $\displaystyle\mathbf E[\mathcal A]=\sum_{i=1}^n\sum_{j:\,d(i)v(j)\ge Z/2}d(i)v(j)\,\frac{|G_{ij}|}{|S_n|}$.
4. Claim 4.8. For every $i,j$ with $d(i)v(j)\ge Z/2$, $n|G_{ij}|\ge|S_n\setminus S_{acc}|$; and if $2|S_{acc}|\le n!$ then $2n|G_{ij}|\ge n!$.

Significance

The result. The discounted problem separates sharply by information: a logarithmic gap is unavoidable without prior knowledge, while knowledge of the single number $\mathbf E[\mathrm{OPT}]$, or of any lower estimate $Z$ of it, closes the gap to a constant. The algorithm is a fixed posted threshold, so read as a mechanism it is a posted price, which is truthful for single-parameter agents (§1). The paper also notes that when all values are known, $\mathbf E[\mathrm{OPT}]$ can be estimated by sampling (its Lemma A.1), which yields a constant-competitive algorithm in that setting. The companion lower bound (Theorem 4.6) shows that even complete knowledge of the values does not give a ratio better than $\sqrt2$.

Formalizing it. The result is proved on paper; no machine-checked proof is known. The formalization yields a checked version of the paper's counting argument on permutations (Claim 4.8) and of the tie-breaking step behind Eq. (4.3), and reusable finite random-order bookkeeping: expectations over $S_n$ as averages, threshold stopping rules, and the decomposition of an online algorithm's value by the time and element it selects.

Difficulty

The obvious argument fails when $\mathcal A$ rarely selects. $\mathcal A$ earns at least $Z/2$ whenever it selects anything, so $\mathbf E[\mathcal A]\ge\frac Z2\Pr[\mathcal A\text{ selects}]$. That settles the case $\Pr[\mathcal A\text{ selects}]\ge1/2$ and nothing else: the probability of selecting can be tiny while $\mathbf E[\mathrm{OPT}]$ is still large, because the optimum may be concentrated on a few orders with a large product. In that case the bound must come from comparing the algorithm with the optimum pair by pair: every time–element pair $(i,j)$ with $d(i)v(j)\ge Z/2$ must be realized by $\mathcal A$ on a positive fraction of the orders.

Two points need care in a formal proof:

• Eq. (4.2) rewrites $L$ as a sum over pairs weighted by the conditional probability that $d(i)v(j)$ is the highest product. It relies on a consistent tie-breaking rule, which the paper leaves implicit.
• Claim 4.8 is a counting argument on $S_n$. A map from the rejecting orders into $G_{ij}$ swaps element $j$ into position $i$, and must be shown to be at most $n$-to-$1$ and to land in $G_{ij}$.

Neither (4.2) nor the map appears in the statements, so solvers may replace either with any argument they like.

Formalization scope

• Types. Times and elements are Fin n; the paper's time $t$ is the index $t-1$. An order is π : Equiv.Perm (Fin n), read as time ↦ element, as on p. 3. The instance [NeZero n] encodes $n\ge1$, so the maximum over times is a genuine maximum (Finset.sup').
• Expectations. Expectations over the uniform order are finite averages $\frac1{n!}\sum_\pi$. No measure theory is used.
• Values and constants. Values, discounts and $Z$ are real numbers, and the hypotheses $d\ge0$, $v\ge0$ are explicit. The constant $1/4$ is the paper's. The bound is stated multiplicatively, $Z/4\le\mathbf E[\mathcal A]$, never as a ratio.
• Thresholds and ties. Every threshold is non-strict ($\ge Z/2$), exactly as on pp. 7–8. $\mathcal A$ selects the first qualifying time, so it needs no tie-breaking. The tie-breaking remark at Eq. (4.2) concerns only the paper's intermediate identity (4.2), which is not a milestone.
• Claim 4.8. Both inequalities are stated with cleared denominators. The second carries the proof's case hypothesis $2|S_{acc}|\le n!$, which the paper uses in the same place ("at most half the permutations are in $S_{acc}$").
• What is not this theorem. $\mathcal A$ is the online threshold rule with threshold $Z/2$ applied to $\pi$ as it unfolds. An algorithm that inspects the whole order, or that chooses its threshold after seeing the values, would make the bound trivial and is not this theorem.
• Contributions welcome. Proofs of each milestone, including the counting argument of Claim 4.8. Lemmas on averages over Equiv.Perm (Fin n) and on first-hitting times are reusable beyond this mission.

Selected references

• M. Babaioff, M. Dinitz, A. Gupta, N. Immorlica, K. Talwar, Secretary Problems: Weights and Discounts, Proceedings of the 20th ACM-SIAM Symposium on Discrete Algorithms (SODA), 2009.
• E. B. Dynkin, Optimal choice of the stopping moment of a Markov process, Doklady Akademii Nauk SSSR 150:238–240, 1963.
• W. T. Rasmussen, S. R. Pliska, Choosing the maximum from a sequence with a discount function, Applied Mathematics and Optimization 2(3):279–289, 1975/76.
• M. Mahdian, P. McAfee, D. Pennock, The secretary problem with durable employment, personal communication, 2008 (cited as [MMP08]).
• M. Babaioff, N. Immorlica, R. Kleinberg, Matroids, secretary problems, and online mechanisms, SODA 2007, pp. 434–443.

Motivation

A correlated equilibrium is the equilibrium notion that arises when the players of a game take their actions on the advice of a common randomizing device, each player seeing only his own recommendation. It was introduced by Aumann in 1974 (Aumann 1974). Aumann's 1987 paper (Aumann 1987) gives the simple, finite form of the definition used today (Definition 2.1) and shows that the notion is what Bayesian rationality with a common prior predicts. On the way it records, as Proposition 2.3, the fact that makes correlated equilibrium tractable in practice: for a finite two-person game, the distributions over action pairs that come from correlated equilibria are exactly the solutions of an explicit finite system of linear inequalities.

That characterization is the starting point of the computational theory of correlated equilibria. Because the set is a polyhedron, an optimal correlated equilibrium can be found by linear programming, and no-swap-regret learning dynamics converge to this set (Foster and Vohra 1997; Hart and Mas-Colell 2000). In each of these works the linear-inequality description is taken as the definition; the paper's Proposition 2.3 is the bridge back to the strategic definition.

Setting

Player 1 has a finite set $S^1$ of actions and player 2 a finite set $S^2$. For $j \in S^1$ and $k \in S^2$, $h^1_{jk}$ and $h^2_{jk}$ are the two players' payoffs at the action pair $(j,k)$.

A correlated strategy pair is a pair of functions $f^1 : \Gamma \to S^1$, $f^2 : \Gamma \to S^2$ on a finite probability space $(\Gamma, \mu)$: a finite set $\Gamma$ with nonnegative weights $\mu(\gamma)$ summing to $1$. Chance draws $\gamma$ and suggests the action $f^i(\gamma)$ to player $i$. The pair is a correlated equilibrium (Definition 2.1, condition (2.2)) if no player gains by a deviation that depends only on his own suggestion: for every $\varphi : S^1 \to S^1$,

$$\mathbb E\, h^1(\varphi(f^1), f^2) \le \mathbb E\, h^1(f^1, f^2),$$

and the analogous inequality holds for player 2 and every $\psi : S^2 \to S^2$.

A distribution is a family $(p_{jk})_{j \in S^1, k \in S^2}$ with $p_{jk} \ge 0$ and $\sum_j \sum_k p_{jk} = 1$. The distribution of a correlated strategy pair assigns to $(j,k)$ the probability $\mu\{f^1 = j,\ f^2 = k\}$. A correlated equilibrium distribution (c.e.d.) is the distribution of some correlated equilibrium on some finite probability space.

In the Lean development these are IsDistribution p, IsProbVec μ, IsCE h₁ h₂ μ f₁ f₂, distr μ f₁ f₂ and IsCED h₁ h₂ p, with h₁ j k $= h^1_{jk}$ and p j k $= p_{jk}$.

Formalization targets

Goal: Proposition 2.3

For every distribution $(p_{jk})$: $(p_{jk})$ is a correlated equilibrium distribution if and only if

$$\sum_k \big(h^1_{jk} - h^1_{qk}\big)\, p_{jk} \ge 0 \quad \text{for all } j, q \in S^1, \tag{2.4}$$ $$\sum_j \big(h^2_{jk} - h^2_{jr}\big)\, p_{jk} \ge 0 \quad \text{for all } k, r \in S^2. \tag{2.5}$$

Milestones

1. Identification with distributions (Sect. 2, p. 4). A correlated strategy pair is a correlated equilibrium if and only if its distribution $p$ satisfies $\sum_j\sum_k p_{jk} h^1_{\varphi(j)k} \le \sum_j\sum_k p_{jk} h^1_{jk}$ for all $\varphi$, and the analogous condition for player 2.
2. Conditioning on possible suggestions (proof of Prop. 2.3, p. 6). For a distribution, player 1's condition holds if and only if $H^1(q \mid j) \le H^1(j \mid j)$ for every suggestion $j$ of positive probability and every $q$, where $H^1(q\mid j) = \sum_k h^1_{qk} p_{jk} / \sum_k p_{jk}$; likewise for player 2.
3. Player 1 gives (2.4): player 1's condition on $p$ is equivalent to (2.4).
4. Player 2 gives (2.5): player 2's condition on $p$ is equivalent to (2.5).

A further statement, not a milestone, records the paper's example on p. 5: in the game of chicken (Figure 4) the distribution of Figure 5 is a c.e.d. with expected payoff $(5,5)$.

Significance

The result. Proposition 2.3 turns an existential statement — there is some probability space and some correlated strategy pair that is an equilibrium and has distribution $p$ — into finitely many linear inequalities on $p$ alone. Consequently the set of c.e.d.'s is a compact convex polyhedron, membership is decidable by evaluating $|S^1|^2 + |S^2|^2$ linear forms, and optimizing a linear objective over it is a linear program. The paper states the two-person case and remarks that "the principle, however, is no different in the general case".

Formalizing it. The proposition is classical and its proof is short; to our knowledge it has no machine-checked proof. The platform already has the linear-inequality (swap) form of correlated equilibrium for two-player games on Fin m × Fin n (Foster–Vohra 1997 missions) and Aumann's 1974 randomizing-structure model, but no statement that connects the strategic definition over arbitrary finite probability spaces with the linear system. This mission supplies that connection, so that results proved about the polyhedron apply to equilibria in Aumann's sense and conversely.

Difficulty

The mathematics is elementary; the care is in the statement. Two points need attention. First, the direction from the inequalities to a c.e.d. requires constructing a probability space and a correlated strategy pair whose distribution is the given $p$; the c.e.d. notion quantifies over probability spaces, not over distributions. Second, the paper's argument divides by the probability $\sum_k p_{jk}$ of a suggestion, which may be zero; the conditional formulation (milestone 2) holds only over possible suggestions, while (2.4) and (2.5) quantify over all actions and hold trivially at impossible ones. Deviations must be functions of the player's own suggestion: restricting to constant deviations gives coarse correlated equilibrium, which (2.4)–(2.5) do not characterize, and allowing arbitrary functions of $\gamma$ gives a stronger notion.

Formalization scope

Two players with finite action types S₁ S₂ : Type* (Fintype, DecidableEq); payoffs h₁ h₂ : S₁ → S₂ → ℝ; distributions p : S₁ → S₂ → ℝ with the sign and sum conditions as an explicit hypothesis of every statement about distributions. Finite probability spaces are finite types Γ : Type with a probability vector μ : Γ → ℝ; deviations are compositions φ ∘ f₁ with φ : S₁ → S₁. The conditional payoffs $H^1$, $H^2$ use Lean's x / 0 = 0 and are only ever used at possible suggestions. Empty action sets admit no distribution, so the statements are then vacuous, exactly as in the paper.

A trivializing formalization is ruled out: "c.e.d." is the existential notion over finite probability spaces with a genuine probability vector and an equilibrium in the sense of Definition 2.1, not the inequalities themselves or the swap form on $p$.

No infrastructure beyond finite sums and Finset.filter is needed. Contributions welcome: proofs of the milestones, and the $n$-player generalization the paper alludes to.

Selected references

• R. J. Aumann, Correlated Equilibrium as an Expression of Bayesian Rationality, Econometrica 55 (1987), 1–18. https://doi.org/10.2307/1911154
• R. J. Aumann, Subjectivity and Correlation in Randomized Strategies, Journal of Mathematical Economics 1 (1974), 67–96. https://doi.org/10.1016/0304-4068(74)90037-8
• D. P. Foster and R. V. Vohra, Calibrated Learning and Correlated Equilibrium, Games and Economic Behavior 21 (1997), 40–55. https://doi.org/10.1006/game.1997.0595
• S. Hart and A. Mas-Colell, A Simple Adaptive Procedure Leading to Correlated Equilibrium, Econometrica 68 (2000), 1127–1150. https://doi.org/10.1111/1468-0262.00153

Motivation

Control problems for queueing systems (admission control, service rate control, routing to parallel servers) are naturally modelled as Markov decision chains whose state is a vector of queue lengths. The state space is therefore denumerably infinite, and the performance measure of interest is usually the long-run average cost per slot. For such models the existence theory of average cost optimal stationary policies is well developed (Chapter 7 of Sennott's book), but existence gives no algorithm: an optimal policy is a function on an infinite set, and value iteration cannot be run on an infinite state space.

The approximating sequence method answers this by replacing the infinite model $\Delta$ with a sequence of finite models $\Delta_N$ on truncated state spaces $S_N$, solving the average cost optimality equation in each, and passing to the limit. Chapter 8 of L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems (Wiley, 1999) gives a set of conditions, the (AC) assumptions, under which this limit procedure provably produces the minimum average cost and an average cost optimal policy of $\Delta$.

Timeline. The approximating sequence method for the average cost criterion and the (AC) assumptions were introduced in Sennott (1997a), with further results in Sennott (1997b) (bibliographic notes, p. 194). The book collects these results, adds the four step verification template (Proposition 8.2.1), the finite-set augmentation route based on the (BOR) assumptions (Proposition 8.2.3), and the weakening (WAC) of Section 8.7, which Chapter 9 uses.

Setting

An MDC $\Delta$ has a countable state space $S$, a finite nonempty action set $A_i$ in each state $i$, a finite cost $C(i,a)\ge0$, and transition probabilities $P_{ij}(a)$. A general policy $\theta$ chooses actions at random using the whole past history. Its average cost is

$$J_\theta(i)=\limsup_{n\to\infty}\frac1n\sum_{t=0}^{n-1}E_\theta[C(X_t,A_t)\mid X_0=i],$$

and the minimum average cost is $J(i)=\inf_\theta J_\theta(i)\in[0,\infty]$. A policy is average cost optimal if $J_\theta\equiv J$.

An approximating sequence $(\Delta_N)_{N\ge N_0}$ consists of finite sets $S_N$ increasing to $S$ and MDCs $\Delta_N$ on $S_N$ with the same actions and costs and with transition probabilities $P_{ij}(a;N)$ on $S_N$ converging to $P_{ij}(a)$. Write $v^N_n$ and $V^N_\alpha$ for the $n$-horizon and discounted value functions of $\Delta_N$.

The (AC) assumptions are:

• (AC1) there are finite constants $J^N$ and finite functions $r^N$ on $S_N$ with

$$J^N+r^N(i)=\min_a\Big\{C(i,a)+\sum_{j\in S_N}P_{ij}(a;N)\,r^N(j)\Big\},\qquad i\in S_N; \tag{8.1}$$

• (AC2) $\limsup_N r^N(i)<\infty$;
• (AC3) $\liminf_N r^N(i)\ge -Q$ for a constant $Q\ge0$;
• (AC4) $J^*:=\limsup_N J^N<\infty$ and $J^*\le J(i)$ for all $i$.

The (WAC) assumptions of Section 8.7 allow $Q$ to depend on the state, at the price of integrability conditions along every stationary policy.

Formalization targets

Goal: Theorem 8.1.1

Under (AC), the limit $\lim_{N\to\infty}J^N$ exists and

$$J(i)=\lim_{N\to\infty}J^N\qquad\text{for all } i\in S,$$

and every limit point $e^*$ of stationary policies $e^N$ realizing the minimum in (8.1) is average cost optimal for $\Delta$. The statement fixes no constants; it asserts the shape of the conclusion for any model satisfying (AC).

Milestones

• Proposition 8.2.1 (the four step template): unichain and aperiodicity of the finite models, an $x$ standard policy at which the approximating sequence is conforming, a comparison of $v^N_n$ (or $V^N_\alpha$) with $v_n$ (or $V_\alpha$), and a lower bound on $v^N_n - v^N_n(x)$ together imply that the value iteration limits

$$r^N(i)=\lim_{n\to\infty}\big(v^N_n(i)-v^N_n(x)\big)$$

exist and satisfy (AC).

• Corollary 8.2.2: on $S=\{0,1,2,\dots\}$ with $S_N=\{0,\dots,N\}$ and excess probability sent to $N$, monotonicity of $v^N_n$, $v_n$ and of the first passage moments of a $0$ standard policy suffices.
• Proposition 8.2.3: an augmentation type approximating sequence that sends excess probability to a finite set of cheap states satisfies the template.
• Proposition 8.5.1: in the single-server queue with Bernoulli($p$) arrivals and constant service rate $a>p$,

$$J_{d(a)}=\frac{Hp(1-p)}{a-p}+\frac{pC(a)}{a}.$$

• Proposition 8.7.1: the conclusions of Theorem 8.1.1 hold under (WAC).

Significance

The result itself. Theorem 8.1.1 is what turns the existence theory of Chapter 7 into a computation. It certifies that the minimum average costs of the truncations converge to the minimum average cost of the infinite model, that this cost is constant, and that the policies produced by value iteration on $\Delta_N$ converge, along subsequences, to an optimal policy for $\Delta$. Propositions 8.2.1–8.2.3 reduce (AC) to properties that can be checked model by model; Section 8.3 checks them for queues with reject option, service rate control, and routing to parallel queues. Proposition 8.7.1 is the version used in Chapter 9 for models whose relative values are not uniformly bounded below. Proposition 8.5.1 gives the closed-form open-loop benchmark used in the numerical study of Section 8.5.

Formalizing it. All results are proved in the book; none has a machine-checked proof. A formalization would give the first verified convergence theorem for truncations of denumerable-state average cost MDPs, and would make the approximating sequence method usable as a certified reduction from infinite to finite models. The template results (8.2.1–8.2.3) additionally require a formal treatment of conformity of approximating Markov chains (Appendix C.4–C.5), which is of independent use.

Difficulty

The naive argument takes limits in (8.1) along $N$: the minimum over $a$ and the finite sums pass to the limit only in the inequality direction, and only after a Fatou-type lemma for sums against the converging distributions $P_{ij}(a;N)$ with integrands $r^N$ that are neither bounded nor monotone. The lower bound $-Q$ in (AC3) is exactly what makes this possible; without it the limit inequality can fail. The limit inequality then produces only an average cost optimality inequality, and turning it into optimality of the limit policy requires a separate argument that a function bounded below and satisfying the inequality yields an upper bound on the average cost. Existence of $\lim_N J^N$ is not given: (AC4) controls only the limit superior, and the limit must be identified through every subsequence. For the template results, the difficulty is in the Markov chain side: the convergence of first passage times and costs of the truncated chains, which fails for general approximating sequences (Examples C.4.4, C.4.7).

Formalization scope

The Lean development is in the namespace SennottDP.AvgASM. The state space is any countable type; action sets are Finsets, assumed nonempty; costs are finite and nonnegative (ℝ≥0); transition probabilities are ℝ≥0∞-valued, with each row a probability distribution for admissible actions. All value functions and average costs take values in $[0,\infty]$ (ℝ≥0∞), and every infimum over policies ranges over the full class of history-dependent randomized policies. The $J^N$ and $r^N$ of (AC1) are real; the limits superior and inferior over $N$ in (AC2)–(AC4) and (WAC) are taken in EReal, so an unbounded sequence cannot produce a junk finite value. The equality $J(i)=\lim_N J^N$ is stated in EReal, which also asserts that $J(i)$ is finite. Quantities of $\Delta_N$ at states outside $S_N$ are junk values that affect only finitely many $N$ for each state.

A trivializing formalization is ruled out: $J^N$ and $r^N$ are the witnesses of (AC1), not free variables, the policies $e^N$ must realize the minimum in (8.1) for those witnesses, and the minimum average cost $J$ is an infimum over all policies, so the goal cannot be satisfied by choosing $J^*$ or the limit policy.

A complete development needs: the induced process law of a general policy; the average cost optimality inequality argument (Lemma 7.2.1); the finite-state average cost results of Chapter 6 (Propositions 6.4.1, 6.5.1, 6.6.3); a Fatou lemma for converging distributions (Proposition A.2.5); limit points of policy sequences (Proposition B.5); and, for the template results, the theory of $z$ standard chains and conformity (Appendix C.2–C.5). The Markov chain layer and the approximating sequence definitions are reusable beyond this mission. Contributions of any of these intermediate results as separate theorems are welcome.

Selected references

• L. I. Sennott, Stochastic Dynamic Programming and the Control of Queueing Systems, Wiley Series in Probability and Statistics, John Wiley & Sons, 1999. https://doi.org/10.1002/9780470317037
• L. I. Sennott, "The computation of average optimal policies in denumerable state Markov decision chains", Advances in Applied Probability 29 (1997), 114–137 (cited as Sennott (1997a) in the book).
• L. I. Sennott, "On computing average cost optimal policies with application to routing to parallel queues", ZOR — Mathematical Methods of Operations Research 45 (1997), 45–62 (cited as Sennott (1997b) in the book).

Motivation

A Markov chain Monte Carlo sampler is often assembled from simpler parts. A practitioner who has several proposal mechanisms $Q_1, Q_2, \dots$ for a Metropolis–Hastings sampler can combine them in two ways. Either each $Q_i$ drives its own Metropolis–Hastings kernel $P_i$ and the sampler picks kernel $P_i$ with probability $\beta_i$ at each step, or the mixture $Q = \sum_i \beta_i Q_i$ is used as a single proposal inside one Metropolis–Hastings kernel. Both samplers leave the target $\pi$ invariant, so the choice is about efficiency.

Section 4 of Tierney (1998) settles the comparison: when both samplers use the maximal acceptance probability, the second never does worse in terms of asymptotic variances of sample-path averages. The statement that carries this is Proposition 5, an ordering of kernels in Peskun's off-diagonal order; the variance comparison then follows from Theorem 4 of the same paper, the general-state-space extension of Peskun (1973).

Timeline. Peskun (1973) introduced off-diagonal domination for finite state spaces and showed that the Metropolis–Hastings acceptance probability is maximal in that order. A version of Proposition 5 for discrete chains appears in the appendix of Tierney (1991) and in the rejoinder of Besag, Green, Higdon and Mengersen (1995). Tierney (1998) states and proves it for general state spaces, using the measure-theoretic description of Metropolis–Hastings kernels from §2 of the same paper.

Setting

Let $(E, \mathcal E)$ be a measurable space and $\pi$ a probability measure on it, the target. A proposal kernel $Q(x, dy)$ is a Markov kernel on $E$. Given a measurable acceptance probability $\alpha : E \times E \to [0,1]$, the Metropolis–Hastings kernel is

$$P(x, dy) = Q(x, dy)\,\alpha(x, y) + \delta_x(dy) \int \bigl(1 - \alpha(x, u)\bigr)\, Q(x, du),$$

where $\delta_x$ is the point mass at $x$ (mhKernel Q α).

Put $\mu(dx, dy) = \pi(dx) Q(x, dy)$ and $\mu^T(dx, dy) = \mu(dy, dx)$. With $\nu = \mu + \mu^T$ and $h = d\mu/d\nu$ (canonDensity), let

$$R = \{(x, y) : h(x, y) > 0,\ h(y, x) > 0\},\qquad r(x, y) = h(x, y)/h(y, x) \text{ on } R,\quad r = 1 \text{ on } R^c$$

(canonR, canonRatio). The set $R$ is symmetric, $\mu$ and $\mu^T$ are mutually absolutely continuous on $R$ and mutually singular off it (Proposition 1 of the paper). The Metropolis–Hastings acceptance probability is

$$\alpha_{MH}(x, y) = \min\{1, r(y, x)\} \text{ if } (x, y) \in R, \qquad \alpha_{MH}(x, y) = 0 \text{ otherwise}$$

(alphaMH π Q), and the kernel with $\alpha = \alpha_{MH}$ is the maximal Metropolis–Hastings kernel for $Q$ (maxMHKernel π Q).

For kernels $P_1, P_2$ on $E$, $P_1$ dominates $P_2$ off the diagonal, $P_1 \succeq P_2$ (OffDiagDominates π P₁ P₂), if for $\pi$-almost every $x$, $P_1(x, A \setminus \{x\}) \ge P_2(x, A \setminus \{x\})$ for all $A \in \mathcal E$. For a countable family of kernels $K_i$ and weights $\beta_i \ge 0$, the mixture $\sum_i \beta_i K_i$ is the kernel $x \mapsto \sum_i \beta_i K_i(x, \cdot)$ (mixKernel β K).

Formalization targets

Goal: Proposition 5

Let $Q_i$ be a finite or countable family of proposal kernels and $\beta_i \ge 0$ with $\sum_i \beta_i = 1$. Let $P_i$ be the maximal Metropolis–Hastings kernel for $Q_i$ and $P$ the maximal Metropolis–Hastings kernel for $Q = \sum_i \beta_i Q_i$. Then

$$P \succeq \sum_i \beta_i P_i .$$

Both sides use maximal kernels: $P$ uses $\alpha_{MH}$ of the mixture proposal, each $P_i$ its own $\alpha^{(i)}_{MH}$, and the same weights $\beta_i$ form both mixtures.

Milestones

1. The construction in the proof of Proposition 1 (p. 2) yields a set $R$ and ratio $r$ with the properties of Proposition 1 for $\mu = \pi \otimes Q$.
2. $\alpha_{MH}$ satisfies conditions (i) and (ii) of Theorem 2 (p. 3): $\alpha_{MH} = 0$ $\mu$-a.e. on $R^c$, and $\alpha_{MH}(x, y) r(x, y) = \alpha_{MH}(y, x)$ $\mu$-a.e. on $R$.
3. The maximal kernel satisfies detailed balance, $\pi(dx) P(x, dy) = \pi(dy) P(y, dx)$.
4. For any symmetric $\sigma$-finite $\nu$ dominating $\mu$, with $h = d\mu/d\nu$:

$$\pi(dx) Q(x, dy)\, \alpha_{MH}(x, y) = \min\{h(y, x), h(x, y)\}\, \nu(dx, dy).$$

5. As measures on $E \times E$:

$$\pi(dx) Q(x, dy)\, \alpha_{MH}(x, y) \ge \sum_i \beta_i\, \pi(dx) Q_i(x, dy)\, \alpha^{(i)}_{MH}(x, y).$$

A companion item states the maximality of $\alpha_{MH}$ (§3, p. 7): every measurable acceptance probability $\alpha$ whose kernel is reversible satisfies $\alpha \le \alpha_{MH}$ $\mu$-a.e., so the maximal kernel dominates every reversible Metropolis–Hastings kernel with the same proposal.

Significance

The result. Proposition 5, combined with Theorem 4 of the paper (off-diagonal domination orders asymptotic variances of reversible kernels), shows that for every function $f$ with finite variance the asymptotic variance of $\frac1n \sum_{k} f(X_k)$ under the mixture-proposal sampler is at most that under the mixture of samplers. Per-iteration cost can be higher for the mixture proposal, since $\alpha_{MH}$ then needs the densities of all components; Proposition 5 isolates the statistical side of that trade-off. The maximality companion states the fact behind the name "maximal kernel": $\alpha_{MH}$ is the largest acceptance probability that keeps a Metropolis–Hastings kernel reversible.

Formalizing it. The paper's proof is a computation of about six lines with Radon–Nikodym densities. A formal version must make explicit what the computation leaves implicit: that $\alpha_{MH}$, defined from one dominating measure, has the same density form for every symmetric dominating measure; that the measure inequality on $E \times E$ passes to the kernel-level statement with one null set for all $A$; and that the mixture proposal and the mixture of kernels are handled as countable sums of kernels. As of September 2026 neither Mathlib nor this platform has a machine-checked version of Proposition 5, of the maximality of $\alpha_{MH}$, or of reversibility of the Metropolis–Hastings kernel on a general state space; only finite-state Metropolis chains have been formalized on the platform.

Difficulty

The obvious argument works pointwise with densities: write every kernel as a density against a common reference measure and compare $\min\{\cdot, \cdot\}$ of sums with sums of minima. On a general state space there is no common reference measure given in advance, and $\alpha_{MH}$ is only defined up to $\mu$-null sets, through a Radon–Nikodym derivative with respect to $\mu + \mu^T$, a measure that differs for $Q$ and for each $Q_i$. The step that needs care is relating these different versions: the densities $h_i$ of the $\mu_i$ against a common symmetric $\nu$, the density of $\mu = \sum_i \beta_i \mu_i$, and the transpose densities $h(y, x)$, which are densities of $\mu^T$ only because $\nu$ is symmetric.

The second difficulty is the passage from measures to kernels. The inequality between measures on $E \times E$ gives, for each fixed $A$, the kernel inequality for $\pi$-almost every $x$, with a null set that depends on $A$. The order $\succeq$ requires one null set for all $A$, and the diagonal must be removed, which needs the diagonal to be measurable.

Formalization scope

The formalization is in Lean 4 with Mathlib, in the namespace TierneyMH.Mixture. The state space is a type E with a σ-algebra; π is a probability measure; proposal kernels are Markov kernels Kernel E E. Acceptance probabilities and densities take values in $[0, \infty]$ (ℝ≥0∞); a general $\alpha$ is assumed measurable with $\alpha \le 1$. $\mu$ is π ⊗ₘ Q, $\mu^T$ its image under Prod.swap, detailed balance is Kernel.IsReversible. Mixtures are indexed by a countable type ("a sequence", which includes finite families), with weights in ℝ≥0 and HasSum β 1.

Added hypotheses, both labelled in the statements: singletons are measurable (implicit in the paper's $A \setminus \{x\}$ and $\delta_x$), on the goal and the maximality companion; and, on the goal only, the σ-algebra of $E$ is countably generated. The second is an addition to the paper: it is what makes the exceptional null set in $\succeq$ uniform over $A$ in the passage from the measure inequality to the kernels. It is not assumed in the measure-level milestones.

$\alpha_{MH}$ is one fixed version, built from Mathlib's rnDeriv exactly as in the proof of Proposition 1 (with $\nu = \mu + \mu^T$, not an arbitrary dominating measure), and all statements are insensitive to the version. The ratio $r$ is set to 1 on the null subset of $R$ where $h$ is infinite, so that $0 < r < \infty$ and $r(x, y) = 1/r(y, x)$ hold everywhere, as Proposition 1 asks.

Trivializations ruled out: $\alpha_{MH}$ is the indicator of $R$ times $\min\{1, r(y, x)\}$, never an arbitrary acceptance function or a single $\alpha$ shared by all components; $\succeq$ compares $A \setminus \{x\}$, not $A$ (on $A$ the rejection masses differ and the comparison is false); and the conclusion is about the Metropolis–Hastings kernels themselves, not about the measure identity alone. All hypotheses are satisfiable, for instance on $E$ = Bool with $\pi$ uniform, two proposals $Q_1 = \pi$ and $Q_2 = \delta_x$ and weights $(1/2, 1/2)$.

Needed infrastructure, reusable for other Metropolis–Hastings results: Radon–Nikodym calculus for product measures and their transposes, countable sums of kernels, and a monotone-class argument over a countable generating family. The Metropolis–Hastings kernel, $R$, $r$ and off-diagonal domination are defined identically in the companion missions I (detailed balance, Theorem 2) and II (Peskun ordering, Theorem 4) of this series. Proofs of milestones in any order, and proofs of the goal from the milestones, are welcome.

Selected references

• L. Tierney, A Note on Metropolis–Hastings Kernels for General State Spaces, The Annals of Applied Probability 8(1), 1998, 1–9. https://doi.org/10.1214/aoap/1027961031
• P. H. Peskun, Optimum Monte Carlo sampling using Markov chains, Biometrika 60(3), 1973, 607–612. https://doi.org/10.1093/biomet/60.3.607
• J. Besag, P. Green, D. Higdon, K. Mengersen, Bayesian computation and stochastic systems (with discussion), Statistical Science 10(1), 1995, 3–66. https://doi.org/10.1214/ss/1177010123
• W. K. Hastings, Monte Carlo sampling methods using Markov chains and their applications, Biometrika 57(1), 1970, 97–109. https://doi.org/10.1093/biomet/57.1.97
• N. Metropolis, A. W. Rosenbluth, M. N. Rosenbluth, A. H. Teller, E. Teller, Equations of state calculations by fast computing machines, J. Chemical Physics 21, 1953, 1087–1091. https://doi.org/10.1063/1.1699114