Operations Research

Motivation

The classical secretary problem asks how to select one valuable candidate when candidates arrive in random order and a decision must be made when each candidate appears. Many allocation settings have several goods of unequal quality instead of a single position. An employer may have roles of different desirability, or a seller may have placements with different visibility. In the weighted secretary problem, an agent's value is multiplied by the weight of the good assigned to that agent. The algorithm must decide irrevocably as agents arrive, while the benchmark sees every value before assigning goods. Babaioff, Dinitz, Gupta, Immorlica and Talwar study this model with arbitrary fixed agent values and a uniformly random arrival order, and give a constant competitive ratio independent of the number of agents and goods (authors' version, §§2–3).

The paper also studies time discounts and matroid constraints. This mission concerns its weighted-goods result, Theorem 3.4. The result combines an online allocation rule for several comparably valuable agents with the familiar one-choice secretary rule for an unusually valuable agent. These are distinct ways in which the sorted offline assignment can earn value; both are present even when the weights are fixed in advance. The weighted model matters because matching a valuable agent to an unsuitable good can lose value despite accepting the right agent.

Setting

There are $n$ agents $e\in U$, each with a nonnegative value $v(e)$, and $K$ goods indexed in decreasing order of nonnegative weight:

$$w(1)\ge w(2)\ge\cdots\ge w(K)\ge0.$$

An assignment $s$ gives each good to at most one agent, and each agent receives at most one good. A good may remain unassigned, represented by $\bot$ with $v(\bot)=0$. Its value is $\sum_{k=1}^K v(s(k))w(k)$. Agent values are arbitrary, not drawn independently from a distribution. The uncertainty is the arrival order $\pi$, chosen uniformly from all permutations; an agent's value becomes visible on arrival, and an allocation decision cannot be revised.

The offline optimum, $\mathrm{OPT}$, assigns the heaviest good to the highest-valued agent, the next good to the next agent, and so on. If $K>n$, the extra goods remain unassigned. A consistent tie break makes the ordering unique without changing the numerical value. This sorted assignment is defined directly; the mission does not replace it with an unconstrained variable said to be optimal.

The reservation algorithm draws a sample size $\tau\sim\mathrm{Binom}(n,1/2)$, observes the first $\tau$ agents without allocation, and retains the best $\min(K,\tau)$ sampled agents. Positive values are grouped into value classes $[2^{i-1},2^i)$ for integer $i$. A sampled agent in class $i$ reserves one good in that class's contiguous block, with higher classes receiving heavier blocks. A later agent receives the heaviest unassigned good reserved for its class when one is available. The classical secretary rule instead observes the first $\lfloor n/e\rfloor$ agents, then selects the first later arrival better than every predecessor; its winner receives good $1$.

Formalization targets

The mission's goal is the exact guarantee of Theorem 3.4 for Algorithm $A$, which runs the reservation algorithm with probability $8/(3e+8)$ and the classical rule with probability $3e/(3e+8)$:

$$\mathrm{OPT}\le(8+3e)\,\mathbb E[A].$$

Here the expectation covers the uniform arrival permutation, the independent binomial sample size used by the reservation branch, and the mixing coin. The multiplicative inequality expresses competitiveness even when an expected payoff is zero. It uses the explicit constant in the paper's proof rather than an instance-dependent or unspecified constant.

Four source results form the milestones. The classical secretary rule selects the maximum with probability at least $1/e$. Lemma 3.2 compares the starting indices $b_i$ and $o_i$ of class-$i$ blocks in the reservation and optimum assignments. Lemma 3.1 says that if the optimum assigns at least two agents from class $i$, the reservation rule assigns at least $u_i/4$ agents from that class in expectation. Lemma 3.3 converts this to expected value at least $\mathrm{OPT}_i/8$. The target retains the paper's class condition and both numerical fractions (authors' version, pp. 4–5).

Significance

Theorem 3.4 supplies a constant factor guarantee for irrevocable allocation when goods have different weights and agents arrive in random order. The factor does not grow with $n$ or $K$. It separates the effects of uncertain arrivals from the offline matching of high values to high weights, and it supplies a benchmark for later variants with more complicated feasibility constraints. The paper extends the reservation idea to additional combinatorial settings, including partition-matroid variants in Appendix C (authors' version, Appendix C).

The theorem is proved in the source paper, while the Lean statements in this mission are proof obligations. Formalizing them requires checking that the random-order model, sample distribution, tie convention and assignments jointly express the same algorithm. A complete development will also establish reusable finite-average facts for random permutations and binomial samples, and structural facts about sorted assignments and reserved blocks. Those pieces can support other secretary problems in the series; the mission's specific promise remains the weighted algorithm's exact bound.

Difficulty

A count of how many agents a class receives does not by itself control the weighted value of those goods. Goods have unequal weights, and the value of assigning the next good changes with its position in a block. A class whose offline optimum receives several agents can also lose all its sampled members from the allocation phase. Thus a direct comparison of expected class counts with expected class values is insufficient. The paper's separate count, block-position and value statements identify the claims a solver must establish; the final theorem must also account for classes represented only once in the offline assignment (authors' version, p. 5).

Formalization scope

Agents and goods are Fin n and Fin K; their indices start at zero in Lean, so paper time $t$ corresponds to Lean index $t-1$. An arrival permutation maps time to agent. Values and weights are real and explicitly nonnegative, and weights are antitone in the good index. The finite sums defining expectations are normalized by $n!$ for permutations and by $\binom n\tau/2^n$ for sample sizes. No measurability or integration convention is needed. For the goal, $K\ge1$ makes the heaviest good available; $K>n$ is allowed.

Equal values are ordered by smaller original agent index throughout the sorted optimum, the sample's top agents and the classical rule. The classical rule observes exactly $\lfloor n/e\rfloor$ arrivals, and zero-valued agents reserve no value-class goods. Positive values below one use negative integer class indices. The paper says only that class $i$ holds the values “between” $2^{i-1}$ and $2^i$ (p. 4, and again in Appendix C, p. 12); the mission fixes the half-open interval $[2^{i-1},2^i)$, so that the classes partition the positive reals (authors' version, pp. 4, 12). A reservation assignment is built from each post-sample agent's rank within its class, so a good is offered to at most one such agent. The theorem is about this concrete algorithm and the concrete sorted offline assignment; an arbitrary favorable policy or an optimum supplied as a hypothesis would not express the source result.

The development needs a finite assignment interface, a tie-aware rank order, value classes, the two online rules, and normalized finite expectations. The assignment and finite-average definitions are reusable. Contributions that prove the structural validity of the reservation assignment, the classical success guarantee, Lemmas 3.1–3.3, or the final combination all advance the stated target.

Selected references

• Moshe Babaioff, Michael Dinitz, Anupam Gupta, Nicole Immorlica and Kunal Talwar, Secretary Problems: Weights and Discounts, Proceedings of SODA 2009; authors' full version, proceedings DOI.

Motivation

A stochastic approximation algorithm is a recursion $x_{n+1}=x_n+\gamma_{n+1}\big(F(x_n)+U_{n+1}\big)$ with decreasing steps $\gamma_n$ and noise $U_n$. Stochastic gradient descent, the Robbins–Monro procedure, reinforcement-learning updates and learning dynamics in games all have this form. The ODE method compares such a recursion with the deterministic dynamics $\dot x=F(x)$. Benaïm's lecture notes (Séminaire de Probabilités XXXIII, 1999) do this in two steps. First, the limit set of the interpolated process is internally chain transitive for the semiflow of $F$ (Theorem 5.7, the subject of mission 1 of this series). Second, internally chain transitive sets are located using properties of the dynamics alone.

The most common tool in the second step is a Lyapounov function: a function that decreases strictly along every trajectory outside a set $\Lambda$ and is constant on $\Lambda$. Proposition 6.4 of the notes states exactly when such a function forces every internally chain transitive set into $\Lambda$. It is the step behind the convergence of stochastic gradient algorithms to critical points (Corollary 6.7) and behind convergence results for learning in potential games.

Timeline.

• Conley (Isolated Invariant Sets and the Morse Index, CBMS 38, 1978) introduced chain recurrence and the attractor–repeller description of it.
• Benaïm and Hirsch (J. Dyn. Diff. Eq. 8, 1996) identified limit sets of asymptotic pseudotrajectories with internally chain transitive sets.
• Benaïm (SIAM J. Control Optim. 34, 1996) developed the dynamical-systems approach to stochastic approximation built on these notions.
• Bowen (J. Differential Equations 18, 1975) characterized chain transitivity by the absence of proper attractors, the content of Proposition 5.3 of the notes.
• The 1999 notes state the Lyapounov criterion in the form used here, for semiflows on arbitrary metric spaces.

Setting

Let $(M,d)$ be a metric space, with no compactness or completeness assumed. A semiflow $\Phi$ on $M$ is a continuous map $\mathbb R_+\times M\to M$, $(t,x)\mapsto\Phi_t(x)$, with $\Phi_0=\mathrm{Id}$ and $\Phi_{t+s}=\Phi_t\circ\Phi_s$.

• A set $A$ is invariant if $\Phi_t(A)=A$ for every $t\ge0$. For an invariant $\Lambda$, the restriction $\Phi|\Lambda$ is the semiflow $\Phi$ acting on $\Lambda$.
• For $\delta,T>0$, a $(\delta,T)$-pseudo-orbit from $a$ to $b$ is a list of points $y_0,\dots,y_k$ ($k\ge1$) and times $t_0,\dots,t_{k-1}\ge T$ with $d(y_0,a)<\delta$, $d(\Phi_{t_j}(y_j),y_{j+1})<\delta$ for $j<k$, and $y_k=b$.
• A set $L$ is internally chain transitive if it is nonempty, compact and invariant, and for all $a,b\in L$ and all $\delta,T>0$ there is a $(\delta,T)$-pseudo-orbit of $\Phi|L$, so with every $y_i\in L$, from $a$ to $b$.
• An attractor is a nonempty compact invariant set $A$ with a neighbourhood $W$ on which $\mathrm{dist}(\Phi_t x,A)\to0$ uniformly. Its basin is the set of points $x$ with $\mathrm{dist}(\Phi_t x,A)\to0$.
• Let $\Lambda\subset M$ be compact and invariant. A continuous $V:M\to\mathbb R$ is a Lyapounov function for $\Lambda$ if $t\mapsto V(\Phi_t(x))$ is constant for $x\in\Lambda$ and strictly decreasing for $x\notin\Lambda$.

Formalization targets

Goal: Proposition 6.4

Let $\Lambda$ be compact invariant and $V$ a Lyapounov function for $\Lambda$, and assume that $V(\Lambda)$ has empty interior in $\mathbb R$. Then for every internally chain transitive set $L$,

$$L\subset\Lambda\qquad\text{and}\qquad V|_L\ \text{is constant}.$$

Milestones

1. Lemma 5.2. If $U$ is open with compact closure and $\Phi_T(\overline U)\subset U$ for some $T>0$, there is an attractor $A\subset U$ whose basin contains $\overline U$.
2. Proposition 5.3. For nonempty $\Lambda$: internally chain transitive $\iff$ connected and internally chain recurrent $\iff$ compact invariant, and $\Phi|\Lambda$ has no proper attractor.
3. The claim of the proof of 6.4. For $L$ internally chain transitive and $v^*=\inf_L V$: $L\cap\Lambda\ne\emptyset$ and $v^*=\inf_{L\cap\Lambda}V$.
4. The sublevel step of the proof of 6.4. For every $c>v^*$ with $c\notin V(\Lambda)$, $V<c$ on all of $L$.

Significance

The result. Proposition 6.4 converts a statement about real numbers, that $V(\Lambda)$ has empty interior, into a statement about dynamics: the chain recurrent behaviour of $\Phi$ is confined to $\Lambda$. With Theorem 5.7 it gives the following. If $\Phi$ has such a Lyapounov function, then the limit set of any precompact asymptotic pseudotrajectory, in particular of a bounded stochastic approximation process, lies in $\Lambda$, and $V$ is constant on it. When $\Lambda$ is the set of equilibria and $V(\Lambda)$ is Lebesgue-null by Sard's theorem, this is the convergence of stochastic gradient algorithms to connected sets of critical points (Corollary 6.7). Remark 6.5 gives a flow on the circle with a strict Lyapounov function, where the circle itself is internally chain transitive. So the empty-interior hypothesis cannot be removed.

Formalizing it. The result is proved, in the notes and in the earlier literature. No machine-checked version of chain recurrence for semiflows on metric spaces, Conley's attractor lemma, or Bowen's characterization of chain transitive sets is known to us. The mission therefore adds the following:

• a formal definition layer for these notions on Mathlib's Flow;
• formal proofs of Lemma 5.2 and Proposition 5.3, which are reused across this series (missions 1 and 6);
• the Lyapounov criterion itself.

Difficulty

The obvious argument does not work. It runs: $V$ decreases along trajectories, so along an orbit in $L$ the value of $V$ must settle on $\Lambda$. But points of an internally chain transitive set are joined only by pseudo-orbits. At each of the $k$ jumps, $V$ may increase by an amount that is small but not controlled in number, so monotonicity of $V$ along true trajectories says nothing directly about $L$. Remark 6.5 shows that the conclusion is genuinely false without a condition on $V(\Lambda)$. The difficulty is therefore global: pseudo-orbits that climb back up $V$ through many small jumps must be excluded using information about the restricted semiflow $\Phi|L$ as a whole, not the monotonicity of $V$ along single trajectories. Milestones 1 and 2 are the general facts about chain transitive sets that this requires, and their own proofs involve compactness and uniform-continuity estimates over arbitrarily long pseudo-orbits.

Formalization scope

• Representation. $M$ is any MetricSpace, and the semiflow is Flow ℝ≥0 M.
• Invariance is equality $\Phi_t(A)=A$ for every $t$, not inclusion.
• Pseudo-orbits have at least one trajectory piece ($k\ge1$), times $\ge T$, an exact endpoint, and, in the internal notions, all their points in the set.
• Nonemptiness. Internally chain transitive and internally chain recurrent sets are nonempty by definition. Accordingly, Proposition 5.3 assumes $\Lambda\neq\emptyset$ and Lemma 5.2 assumes $U\neq\emptyset$.
• Lyapounov function. The predicate contains the standing assumptions of its definition: $\Lambda$ is compact and invariant, $V$ is continuous, $V(\Phi_t x)=V(x)$ on $\Lambda$, and $t\mapsto V(\Phi_t x)$ is strictly antitone off $\Lambda$.
• Empty interior is interior (V '' Λ) = ∅ in $\mathbb R$, not countability, finiteness or measure zero.
• Infima are stated with IsGLB, not a real sInf.

The following formalizations are trivializing and are excluded:

• chains with no jumps, under which every point is chain recurrent;
• invariance as inclusion;
• a non-strict decrease condition, under which constant functions are Lyapounov functions and the goal is false;
• chains of $\Phi$ that leave $L$, a strictly weaker notion;
• quantifying only over limit sets instead of every internally chain transitive set.

A complete development needs elementary facts about ω-limit sets of points of a compact invariant set: they are nonempty, compact and invariant. It also needs the attractor construction $A=\bigcap_{t\ge0}\overline{\bigcup_{s\ge t}\Phi_s(U)}$ and the open sets $\{y: x\hookrightarrow_{\delta,T}y\}$ used in Proposition 5.3. These are reusable for any work on Conley theory. Contributions of any of these lemmas, or of proofs of the milestones in any order, are welcome.

Selected references

• M. Benaïm, Dynamics of Stochastic Approximation Algorithms, Séminaire de Probabilités XXXIII, Lecture Notes in Mathematics 1709, Springer, 1999, pp. 1–68. https://doi.org/10.1007/BFb0096509
• M. Benaïm, M. W. Hirsch, Asymptotic pseudotrajectories and chain recurrent flows, with applications, J. Dynam. Differential Equations 8 (1996), 141–176. https://doi.org/10.1007/BF02218613
• M. Benaïm, A dynamical system approach to stochastic approximations, SIAM J. Control Optim. 34 (1996), 437–472. https://doi.org/10.1137/S0363012993253534
• C. Conley, Isolated Invariant Sets and the Morse Index, CBMS Regional Conference Series in Mathematics 38, AMS, 1978. https://doi.org/10.1090/cbms/038
• R. Bowen, ω-limit sets for Axiom A diffeomorphisms, J. Differential Equations 18 (1975), 333–339. https://doi.org/10.1016/0022-0396(75)90065-0

Motivation

Many estimation procedures in statistics, and most stochastic optimization models in operations research, have the same shape: a decision or parameter $x\in\mathbb R^n$ is chosen to minimize an expected loss $Ef(x)=\int f(x,\xi)\,P(d\xi)$ under a distribution $P$ that is not known. In practice $P$ is replaced by an estimate $P^\nu$ built from the information available at stage $\nu$ (an empirical measure, a smoothed or parametric fit, a Bayesian posterior), and the minimizer of the estimated problem is used in place of the true one. The basic question is whether this is justified: do the estimated solutions converge to a true solution, and the estimated optimal values to the true optimal value, as information accumulates?

For maximum likelihood this is Wald's consistency theorem (Wald 1949); Huber extended it to M-estimators under non-standard conditions (Huber 1967). Both settings are unconstrained, or constrained to an open set, and assume finite-valued criteria. Constrained least squares, $L^1$ and Huber regression with inequality constraints, variance-component models with Heywood cases, and two-stage stochastic programs with recourse all lead instead to criteria that take the value $+\infty$ off a closed feasible set and are only lower semicontinuous in $x$.

J. Dupačová and R. Wets (IIASA WP-86-41, 1986; journal version Ann. Statist. 16 (1988)) proved consistency in this generality by combining epi-convergence of functions with the theory of measurable multifunctions and normal integrands. This mission formalizes their §3.

Setting

$\Xi$ is a Polish space with its Borel $\sigma$-field and $P$ is a probability measure on it. The integrand is $f:\mathbb R^n\times\Xi\to(-\infty,\infty]$, and the true problem is to minimize

$$Ef(x)=\int_\Xi f(x,\xi)\,P(d\xi),$$

with the convention that $Ef(x)=+\infty$ whenever $\xi\mapsto f(x,\xi)$ is not bounded above by a summable function. The effective domain of a function $h:\mathbb R^n\to[-\infty,\infty]$ is $\operatorname{dom}h=\{x: h(x)<\infty\}$, and $\operatorname{argmin}h=\{x: h(x)=\inf h\}$.

Information arrives on a probability space $(Z,\mathcal F,\mu)$ with an increasing sequence of $\sigma$-fields $\mathcal F^1\subseteq\mathcal F^2\subseteq\dots\subseteq\mathcal F$. Each sample $\zeta\in Z$ yields probability measures $P^\nu(\cdot,\zeta)$ on $\Xi$, and $\zeta\mapsto P^\nu(A,\zeta)$ is $\mathcal F^\nu$-measurable for every Borel $A$: the estimate at stage $\nu$ uses only stage-$\nu$ information. The estimated problem minimizes

$$E^\nu f(x,\zeta)=\int_\Xi f(x,\xi)\,P^\nu(d\xi,\zeta).$$

A sequence $g^\nu$ epi-converges to $g$ if, at every $x$, $\liminf g^\nu(x^\nu)\ge g(x)$ along every sequence $x^\nu\to x$, and $\limsup g^\nu(x^\nu)\le g(x)$ along some sequence $x^\nu\to x$.

The standing hypotheses are Assumption 3.4: $\operatorname{dom}f=S\times\Xi$ with $S$ closed and nonempty; $f(x,\cdot)$ is continuous for $x\in S$; $f(\cdot,\xi)$ is lower semicontinuous; and $f$ is locally lower Lipschitz on $S$ with a bounded continuous modulus $\beta(\xi)$. Assumption 3.5 asks that, for $\mu$-almost every $\zeta$, $P^\nu(\cdot,\zeta)$ converge in distribution to $P$, that $|f(x,\cdot)|$ be uniformly tight along $P=P^0,P^1,\dots$ for each $x\in S$, and that $\int\inf_x f(x,\xi)\,P^\nu(d\xi,\zeta)>-\infty$ for all $\nu$.

Formalization targets

Goal: Theorem 3.9, "In particular" (pp. 21–22)

Let $D\subseteq\mathbb R^n$ be compact, suppose $(\operatorname{argmin}E^\nu f)\cap D\neq\emptyset$ $\mu$-a.s. for every $\nu$, and suppose $\{x^*\}=\operatorname{argmin}Ef\cap D$. Then there are $\mathcal F^\nu$-measurable selections $x^\nu$ of $\operatorname{argmin}E^\nu f$ with

$$x^\nu(\zeta)\to x^*\quad\text{and}\quad \inf E^\nu f(\cdot,\zeta)\to\inf Ef\qquad\text{for }\mu\text{-almost every }\zeta .$$

The goal does not assume that $Ef$ has a unique global minimizer, and it does not assume convexity.

Milestones

In attack order:

• Proposition 3.3: epi-convergence gives $\limsup(\inf g^\nu)\le\inf g$, limits of minimizers are minimizers, and the minimum is attained in the closure of a bounded $D$.
• Lemma 3.6: almost surely, $Ef$ and every $E^\nu f$ are proper and l.s.c., with domain $S$.
• Theorem 3.7: almost surely, $E^\nu f$ epi-converges and converges pointwise to $Ef$.
• Theorem 3.8: almost surely, the epigraphs of $E^\nu f$ are closed, and they depend $\mathcal F^\nu$-measurably on $\zeta$.
• Theorem 3.9:
  • (3.14) $\limsup(\inf E^\nu f)\le\inf Ef$ a.s.;
  • (i) cluster points of estimated minimizers minimize $Ef$;
  • (ii) $\zeta\mapsto\operatorname{argmin}E^\nu f(\cdot,\zeta)$ is closed-valued and $\mathcal F^\nu$-measurable.
• Proposition 3.1: the measurable selection theorem.

Significance

The result separates two things: the statistical input, which is only convergence in distribution of $P^\nu$ plus a tightness condition, and the variational output, which is convergence of optimal values and solutions. It therefore applies to any estimator $P^\nu$ that converges weakly almost surely: empirical measures, kernel estimates, parametric fits. It also covers constrained and nonsmooth problems: the feasible set enters through $f=+\infty$ off $S$, and only lower semicontinuity in $x$ is required. Asymptotic distribution results for constrained estimators, such as the second part of the same paper and the subsequent literature on sample average approximation, start from this consistency.

The theorem is proved on paper. To the best of current knowledge none of it is machine-checked. Mathlib has weak convergence of probability measures, lower semicontinuity and extended-real integrals. It does not have epi-convergence, Effros-measurable multifunctions, normal integrands or the Kuratowski–Ryll-Nardzewski selection theorem. A formal proof produces these as reusable components. It also has to supply the details that the paper's proof of Theorem 3.8 leaves as a sketch.

Difficulty

Pointwise convergence $E^\nu f(x)\to Ef(x)$ is not enough to move minimizers to the limit, and uniform convergence fails because $f$ is $+\infty$ off $S$ and need not be bounded. Epi-convergence is the right notion. Proving it needs a liminf inequality along moving points $x^\nu\to x$ under moving measures $P^\nu$. That combines Fatou's lemma, the lower Lipschitz bound and the tightness condition, and the integrands are extended-real-valued, so care is needed.

The second difficulty is measurability. The exceptional null set lies in $\mathcal F$ but not in $\mathcal F^\nu$, so "$\mathcal F^\nu$-measurable" has to be understood on a full-measure set in the trace $\sigma$-field. The paper's argument for Theorem 3.8 appeals to continuity of $P\mapsto\operatorname{epi}E_Pf$ in the epi-topology, and it remarks itself that Theorem 3.7 gives this only along sequences satisfying Assumption 3.5. A solver will have to rebuild this step, for example through the normal-integrand structure of $E^\nu f$.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n) with its Euclidean norm.
• $\Xi$ is a Polish space with its Borel $\sigma$-algebra. This is exactly a closed subset of a Polish space with the relative Borel field.
• $f$ is EReal-valued. Every expectation is the mission's expect: $+\infty$ when $\int f^+=\infty$, and $\int f^+-\int f^-$ otherwise, both computed as Lebesgue integrals of $[0,\infty]$-valued functions. A Bochner integral, which would assign $0$ to non-integrable functions, is never used for $Ef$ or $E^\nu f$.
• The sample index is shifted: Lean's Pν k and 𝔽 k are the paper's $P^{k+1}$ and $\mathcal F^{k+1}$, and $P=P^0$ is a separate argument.
• Infima, $\liminf$ and $\limsup$ are taken in $[-\infty,\infty]$.
• Measurability on the full-measure set $Z_0$ uses the trace $\sigma$-field.
• The selections in the goal are total, $\mathcal F^\nu$-measurable maps $Z\to\mathbb R^n$ that select almost surely. This is equivalent to the paper's maps $Z_0\to\mathbb R^n$.
• "Random l.s.c. function" in Theorem 3.8 is encoded by the equivalent conditions (3.4i)–(3.4ii): nonempty, closed and measurable epigraphs.
• Lower Lipschitz (3.10) is written additively.
• The hypothesis that $\Xi$ is the support of $P$ is omitted. It is unused in §3, and omitting it strengthens every statement.
• Nothing beyond the page is assumed: no convexity, no compact $S$, no bounded $f$, no unique minimizer, no i.i.d. sampling, no empirical $P^\nu$, no completeness of $\mu$ or $\mathcal F^\nu$.

The hypotheses are not vacuous. A sorry-free check verifies all of them, including those of the goal, for $f(x,\xi)=\|x\|^2$ with Dirac measures. Defining the expectation through a Bochner integral, or dropping $S\neq\emptyset$ (which makes every $\operatorname{argmin}$ all of $\mathbb R^n$), would trivialize or change the statements; the definitions above rule both out.

Contributions are welcome on any milestone. Proposition 3.1 (Kuratowski–Ryll-Nardzewski for $\mathbb R^m$-valued multifunctions) and Proposition 3.3 (deterministic epi-convergence facts) are independent of the probabilistic setting and reusable beyond this mission.

Selected references

• J. Dupačová, R. Wets, Asymptotic Behavior of Statistical Estimators and Optimal Solutions for Stochastic Optimization Problems, IIASA Working Paper WP-86-41, 1986. https://pure.iiasa.ac.at/id/eprint/2818/ — journal version: Ann. Statist. 16(4), 1517–1549, 1988. https://doi.org/10.1214/aos/1176351052
• A. Wald, Note on the consistency of the maximum likelihood estimate, Ann. Math. Statist. 20, 595–601, 1949. https://doi.org/10.1214/aoms/1177729938
• P. J. Huber, The behavior of maximum likelihood estimates under nonstandard conditions, Proc. Fifth Berkeley Symp. Math. Statist. Probab. 1, 221–233, 1967. https://projecteuclid.org/euclid.bsmsp/1200512988
• R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998 (Ch. 7 epi-convergence; Ch. 14 measurable multifunctions and normal integrands). https://doi.org/10.1007/978-3-642-02431-3

Motivation

A perfect graph is one whose coloring problem has a particularly sharp answer on every induced subgraph: the fewest colors needed is exactly the size of its largest clique. This makes a local obstruction, a clique, certify the optimum number of colors throughout the graph. Claude Berge proposed in 1961 that perfection could be recognized by the absence of two kinds of induced odd cycles, one in the graph and one in its complement. The equivalence became known as the strong perfect graph conjecture. Chudnovsky, Robertson, Seymour, and Thomas proved it in their 2006 paper, which also proves a structural decomposition of the graphs under study. The paper connects this question to graph coloring, Shannon capacity, and linear and integer programming. Chudnovsky et al., pp. 51–54

The earlier complement theorem was proved by Lovász in 1972 and appears as Theorem 1.1 in the paper. The strong conjecture remained unresolved for roughly four decades; the authors' Theorem 1.2 settles it. Their proof places a second result, Theorem 1.3, beside the equivalence: a graph with no forbidden odd hole or antihole must either belong to a basic class or admit one of several specified decompositions. The graph classes and decompositions are therefore part of the statement of the route to the main result, not merely vocabulary for a proof. Chudnovsky et al., pp. 52–56

Setting

All graphs here are finite and simple. The complement $\overline G$ has the same vertices as $G$, and two distinct vertices are adjacent in $\overline G$ exactly when they are not adjacent in $G$. For a vertex set $X$, the notation $G|X$ means the induced subgraph on $X$. A clique is a set of pairwise adjacent vertices. Its largest possible size in a graph $H$ is $\omega(H)$, and $\chi(H)$ is the minimum number of colors in a proper vertex coloring of $H$.

A hole is an induced cycle of length at least four. An antihole of $G$ is a hole in $\overline G$. A graph is Berge if every hole and antihole has even length. Thus a perfect graph requires $\chi(G|X)=\omega(G|X)$ for every $X\subseteq V(G)$, while a Berge graph satisfies a restriction on induced cycles in both $G$ and $\overline G$. “Induced” matters: a cycle with a chord is not a hole. Chudnovsky et al., pp. 51–52

For the structural milestones, a basic graph is a bipartite graph, the complement of one, a line graph of a bipartite graph, the complement of such a line graph, or a double split graph. The latter consists of paired vertices $a_i,b_i$ and $c_j,d_j$ with the within-pair and between-pair adjacencies specified on pp. 52–53. A proper 2-join partitions the vertices into two sides with two prescribed complete cross-edge blocks, connected-component conditions on both sides, and a special odd-path condition. A proper homogeneous pair is a pair of vertex sets whose outside vertices split into four nonempty adjacency classes. A balanced skew partition has one side disconnected and the other disconnected in the complement, together with parity restrictions on induced paths and antipaths. Chudnovsky et al., pp. 52–54

Formalization targets

Theorem 1.2: perfection and the Berge property

The goal is the exact equivalence for every finite simple graph:

$$G\text{ is perfect}\quad\Longleftrightarrow\quad G\text{ is Berge}.$$

No order bound, chosen graph class, or decomposition hypothesis is attached to the goal. Chudnovsky et al., p. 52, 1.2

Structural and reduction milestones

Theorem 1.1 says that $G$ perfect implies $\overline G$ perfect. Theorem 1.5 says that a minimum imperfect graph, a Berge nonperfect graph with the smallest vertex count among all such graphs, cannot admit a balanced skew partition. Theorem 13.5 says that a recalcitrant graph—a Berge graph with the listed line-graph, double-split, 2-join, homogeneous-pair, and balanced-skew outcomes absent—has $G$ or $\overline G$ bipartite. Theorem 1.3 states the decomposition conclusion:

$$G\text{ Berge}\Longrightarrow G\text{ basic}\ \lor\ G\text{ or }\overline G\text{ has a proper 2-join}\ \lor\ G\text{ has a proper homogeneous pair}\ \lor\ G\text{ has a balanced skew partition}.$$

The milestone order records the two reduction results, the later structural capstone, and the decomposition statement it yields. The paper's other section results that establish 13.5 are posed in the remaining missions of this series. Chudnovsky et al., pp. 52, 54–55, 154

Significance

Theorem 1.2 gives a forbidden-induced-subgraph characterization of perfect graphs. Its cycle condition is intrinsic to the graph and its complement; its coloring condition quantifies over every induced subgraph. Together with Theorem 1.3, it ties a numerical property of colorings to explicit graph structures and separations. The complement theorem and the exclusion of decompositions for a minimum imperfect graph explain why the structural alternatives have the strength needed for the equivalence. Chudnovsky et al., pp. 52–56

The mathematical theorem was proved in the cited paper. This mission poses its statements in Lean and seeks machine-checked proofs; the draft theorem declarations are open targets. The definition layer is useful beyond this mission: induced holes, Berge graphs, perfection, balanced skew partitions, and the decomposition predicates can support the later missions without changing what each source statement means. No machine-checked proof of these draft targets is claimed here.

Difficulty

The forward implication can be tested on induced odd cycles, but that observation does not settle the converse. Excluding odd holes and antiholes does not give an immediate coloring of an arbitrary induced subgraph. The paper instead establishes a detailed account of what a Berge graph can look like when it is not in a basic class. The delicate point in turning this account into Theorem 1.2 is that each decomposition outcome must be incompatible with a minimum imperfect graph. Ordinary skew partitions are too broad for that role; the balanced parity conditions are part of the statement. The structural conclusion 13.5 collects restrictions established across many later sections, so formalizing its prerequisites is a substantial graph-theoretic task. Chudnovsky et al., pp. 52–56, 154

Formalization scope

Lean uses SimpleGraph V with finite vertices, decidable vertex equality, and the Mathlib complement, induced subgraph, chromatic number, clique number, bipartiteness, and line graph. A hole is a list in cyclic order whose adjacency relation agrees exactly with the cycle edges; a path is likewise listed in one orientation with exactly its consecutive edges. Antiholes and antipaths use the complement graph. The empty vertex set is connected, matching p. 54. The double split partition is encoded by an equivalence from the four indexed parts to the whole vertex type, making disjointness and coverage explicit. A minimum imperfect graph is globally minimal by vertex count, among all finite Berge graphs.

No hypothesis beyond the paper's finite, simple graph convention is added to the goal or numbered milestones. In particular, “Berge” includes holes in both $G$ and $\overline G$; “perfect” ranges over every induced subgraph; and the complement occurs only in those decomposition outcomes where the paper places it. A non-induced cycle or a missing complement condition would make the formal target different. The definitions and Lean proofs of the graph classes, their boundary cases, and the structural milestones are welcome contributions. Later missions pose the paper's intervening numbered results rather than duplicating them here.

Selected references

• Maria Chudnovsky, Neil Robertson, Paul Seymour, and Robin Thomas, The strong perfect graph theorem, Annals of Mathematics 164 (2006), 51–229. DOI 10.4007/annals.2006.164.51.

Motivation

Open networks of single-server queues with general interarrival and service distributions are the standard model of job shops, communication networks and service systems. Outside the product-form (Jackson) case their queue-length distributions are not known in closed form. When every station is close to saturation, a heavy-traffic limit replaces the network by a diffusion process. Martin I. Reiman's paper Open Queueing Networks in Heavy Traffic (Mathematics of Operations Research 9(3), 1984) proves such a limit for the vector of queue lengths of a general open network. The limit is a reflected Brownian motion on the nonnegative orthant. That process has since become the default diffusion approximation for open networks, and it is the starting point of later work on its stationary distribution and on control of networks in heavy traffic.

Timeline:

• Iglehart and Whitt (1970a,b) proved heavy-traffic limits for a single multiple-server station and for acyclic networks, in which no customer visits a station twice.
• Harrison (1973, 1978) treated tandem queues; the 1978 paper introduced reflected Brownian motion on the nonnegative orthant as the diffusion limit.
• Harrison and Reiman (1981a, Ann. Probab. 9:302–308) constructed reflected Brownian motion on the orthant through a continuous reflection mapping. That paper is the source of Lemma 1 here.

(These attributions follow Reiman's own account, pp. 441–442 of the 1984 paper.)

• Reiman (1984) proved the limit for general open networks with Markovian routing (Theorem 1). The paper also proves a limit for sojourn times along fixed routes (Theorem 2).

Setting

There are $K$ single-server stations and a nonempty set $\mathcal J\subseteq\{1,\dots,K\}$ of stations that receive customers from outside. The primitives are mutually independent sequences of IID random variables: interarrival times $u_k^i>0$ ($k\in\mathcal J$), service times $v_k^i>0$, and routing indicators $\phi_k^i\in\{0,1,\dots,K\}$. When the $i$th customer served at station $k$ finishes, it moves to station $\phi_k^i$, or leaves if $\phi_k^i=0$. The parameters are the service rates $\mu_k=(E v_k^1)^{-1}$, the service-time variances $s_k=\operatorname{var} v_k^1$, the arrival rates $\lambda_k=(E u_k^1)^{-1}$ (with $\lambda_k=0$ for $k\notin\mathcal J$), and the interarrival variances $a_k=\operatorname{var} u_k^1$. The routing matrix $P=(p_{kj})$, $p_{kj}=P\{\phi_k^1=j\}$, has spectral radius strictly less than one, so every customer eventually leaves.

Let $A_k(t)$ be the number of exogenous arrivals to station $k$ by time $t$, and $S_k(t)$ the number of service completions at $k$ in $t$ units of busy time. Let $\hat S_k(t)=\sum_{i\le S_k(t)}e_{\phi_k^i}-S_k(t)e_k$, with $e_0=0$. The queue length $Q(t)\in\mathbb Z_+^K$ and the busy time $B(t)$ are the unique solution of

$$Q(t)=A(t)+\sum_{k=1}^K\hat S_k(B_k(t)),\qquad B_k(t)=\int_0^t1_{\{Q_k(s)>0\}}\,ds,\qquad B(0)=0 .$$

A sequence of such networks, indexed by $n$, shares $K$, $\mathcal J$ and $P$. Its parameters $\mu(n),s(n),\lambda(n),a(n)$ converge to finite limits $\mu,s,\lambda,a$. With $\nu(n)=\lambda(n)+\mu(n)P$, the heavy-traffic condition is

$$c_k(n)=\sqrt n\,(\nu_k(n)-\mu_k(n))\to c_k .$$

Moments of order $2+\epsilon$ of the interarrival and service times are bounded uniformly in $n$. The scaled queue length is $Z^n(t)=n^{-1/2}Q^n(nt)$, $0\le t\le1$.

Formalization targets

Goal: Theorem 1

Let $\xi$ be a Brownian motion with drift $c$ and covariance matrix $\mathcal A$, where

$$\mathcal A_{ii}=\lambda_i^3a_i+\mu_i^3s_i(1-2p_{ii})+\sum_j\mu_jp_{ji}(1-p_{ji}+p_{ji}\mu_j^2s_j),$$ $$\mathcal A_{ij}=-\Big[\mu_i^3s_ip_{ij}+\mu_j^3s_jp_{ji}+\sum_k\mu_kp_{ki}p_{kj}(1-\mu_k^2s_k)\Big]\quad(i\ne j).$$

Let $Z=\phi(\xi)$ be its reflection with reflection matrix $I-P$. Then

$$Z^n\Rightarrow Z\quad\text{in } D[0,1]\text{ (Skorohod topology)}.$$

The goal fixes no constants beyond the parameters' limits. It is stated for every network sequence satisfying (20)–(26).

Milestones

The milestones follow the paper's proof, in order:

• the existence and uniqueness claim for (1)–(3);
• the representation $Q=\tilde X+Y(I-P)$ (Eq. (13));
• the least-element map $f$ (Proposition 1);
• the reflection mapping $\phi$ (Lemma 1) and $f=\phi$ on continuous paths (Proposition 2);
• the netput limit $\zeta^n\Rightarrow\zeta$ (Proposition 3);
• stochastic boundedness of $Z^n$ (Lemma 6);
• vanishing scaled idleness $n^{-1}I^n_k(n)\to0$ (Proposition 4);
• the centred limit $\tilde\zeta^n\Rightarrow\zeta$ (Proposition 5).

Significance

Theorem 1 justifies the diffusion approximation of a heavily loaded open network. Writing $Q^n(t)\approx\sqrt n\,Z(t/n)$ reduces questions about the network to questions about one reflected Brownian motion, whose data are explicit functions of the first two moments of the primitives and of the routing matrix. The same limit, with Lemma 2, gives the paper's Theorem 2 on sojourn times. It is the model case for the multiclass heavy-traffic theory that followed.

The result has been proved since 1984. No machine-checked version exists. The mission's contributions would be:

• a formal statement of the network, of its Harrison representation, and of weak convergence in $D$;
• a formal proof of the reflection-mapping facts (Proposition 1, Lemma 1, Proposition 2), which are deterministic and reusable;
• eventually, a formal proof of the full limit theorem.

Difficulty

The obvious route applies a functional central limit theorem to $Q^n$ directly. That fails because $Q^n$ is not a sum of independent terms: each station serves only while its queue is nonempty, so the service process is evaluated at the random busy time $B_k(t)$, which depends on the whole network. The proof therefore has to separate the netput process, which obeys a central limit theorem, from the regulator $Y$. It then has to show that the random time change $B^n_k(nt)/n$ converges to the identity, i.e. that idleness vanishes on the diffusion scale. Weak convergence must also be transported through a reflection map that is defined on all of $D$ but is known to be continuous only at continuous paths.

Formalization scope

The Lean development uses the following conventions:

• Stations are Fin K, vectors are row vectors Fin K → ℝ, and a row vector times a matrix is Matrix.vecMul.
• A routing indicator lives in Fin (K+1), with 0 meaning "leaves" and j.succ meaning station $j$.
• The primitives are mutually independent (iIndep of their σ-algebras), IID within each sequence, everywhere positive and square integrable.
• "Spectral radius $<1$" is stated as $P^m\to0$.
• $(Q^n,B^n)$ is any pair solving (1)–(3) almost surely, with measurable paths so that (2) is a Lebesgue integral.
• The networks are indexed by ℕ; (25)–(26) are imposed for $n\ge1$, (22) and (26) over $k\in\mathcal J$, and $\mathcal J$ is the same for all $n$.
• Brownian motion with drift $c$ and covariance $\mathcal A$ lives on $[0,\infty)$. It is defined by continuity, $\xi(0)=0$, independent increments, and the Gaussian characteristic function of increments.
• $Z$ is the reflection of $\xi$ in the sense of (14)–(17).
• Weak convergence in $D$ is stated in Skorohod-representation form: a coupling with almost-sure J$_1$ convergence on $[0,1]$. This form accommodates a separate probability space for each $n$.

Added hypotheses, each implicit on the page:

1. The existence item assumes $U_k(l),V_k(l)\to\infty$ at the sample point; without it the maxima defining $A_k(t)$ and $S_k(t)$ need not exist.
2. Solutions of (1)–(3) have measurable paths.

No positivity hypothesis on the limits $\mu_k$ is added: (25) and (26) bound the means of the service and interarrival times, so the limits are positive.

The statement is not to be weakened. Ruled out are:

• convergence of finite-dimensional distributions only;
• a single network without the index $n$;
• uniform convergence used in place of the Skorohod topology without the coupling;
• a Brownian motion that is not required to have independent Gaussian increments.

Each of these is a different theorem.

Useful contributions, all reusable beyond this mission:

• the deterministic reflection-map results;
• Donsker-type theorems for renewal counting processes in $D$;
• the random time-change lemma (Billingsley);
• the continuous mapping theorem in coupling form.

Selected references

• M. I. Reiman, Open Queueing Networks in Heavy Traffic, Mathematics of Operations Research 9(3):441–458, 1984. https://doi.org/10.1287/moor.9.3.441
• J. M. Harrison and M. I. Reiman, Reflected Brownian Motion on an Orthant, Annals of Probability 9:302–308, 1981 (cited in Reiman 1984 as [6]).
• J. M. Harrison, The Diffusion Approximation for Tandem Queues in Heavy Traffic, Advances in Applied Probability 10:886–905, 1978 (Reiman 1984, [5]).
• J. M. Harrison, The Heavy Traffic Approximation for Single Server Queues in Series, Journal of Applied Probability 10:613–629, 1973 (Reiman 1984, [4]).
• D. L. Iglehart and W. Whitt, Multiple Channel Queues in Heavy Traffic, I and II: Sequences, Networks, and Batches, Advances in Applied Probability 2:150–177 and 355–364, 1970 (Reiman 1984, [8], [9]).
• P. Billingsley, Convergence of Probability Measures, Wiley, New York, 1968 (Reiman 1984, [1]).

Motivation

A hotel sells rooms of several types, in limited numbers, to guests who each want one room. The revenue-optimal way to sell is known only in special cases: for buyers with several private values, optimal mechanisms can be randomized, involve lotteries, and lack a closed form (Manelli–Vincent 2007; Chawla, Hartline, Kleinberg 2007). In practice sellers post prices. The question is how much revenue posting prices gives up.

Chawla, Hartline, Malec and Sivan (arXiv:0907.2435v2, STOC 2010) answer it for a broad class of single- and multi-parameter problems. For unit-demand buyers of multiple copies of multiple items they show that a menu of posted prices, offered to the buyers in whatever order they arrive, earns at least $1/6.75$ of the revenue of any deterministic truthful mechanism (Theorem 14). This mission formalizes that result together with the two steps it is built from: a reduction from the multi-parameter problem to a single-parameter one with "copies" of each buyer (Lemma 3, Theorem 4), and an order-oblivious pricing for the intersection of two partition matroids (Theorem 13).

Setting

Single-parameter problem (BSMD). Finitely many agents $i$ have independent private values $v_i \sim F_i$, each with a density on a bounded interval. A seller may serve any set in a downward-closed set system $\mathcal J$. A deterministic mechanism $M$ maps reported values $v$ to a served set $M(v) \in \mathcal J$ and payments $\pi_i(v)$; it is truthful if reporting the true value is a dominant strategy and no agent ends with negative utility. Its expected revenue is $\mathcal R^M = \mathbb E_v[\sum_i \pi_i(v)]$. For prices $p$, agent $i$ desires service if $p_i \le v_i$, and $\mathcal S_v$ is the class of maximal feasible sets of desiring agents. The order-oblivious revenue is

$$\mathcal R^{\mathrm{obl}}_{\mathbf p} = \mathbb E_{v}\Big[\min_{S \in \mathcal S_v} \sum_{i \in S} p_i\Big],$$

a lower bound on the revenue of posting the prices $p$ to the agents in an adversarial order.

Multi-parameter unit-demand problem (BMUMD). There are $m$ buyers and a finite set $J$ of services, partitioned into the groups $J_i$ of services targeted at buyer $i$. Buyer $i$ has value $v_j$ for each $j \in J_i$, all values independent with $v_j \sim F_j$, and the set system $\mathcal J \subseteq 2^J$ is unit-demand: $|S \cap J_i| \le 1$ for feasible $S$. A mechanism $\mathcal A$ is truthful if no buyer gains by misreporting its whole vector $(v_j)_{j \in J_i}$, and individually rational if a buyer receiving $j$ pays at most $v_j$ and a buyer receiving nothing pays $0$.

Copies. The instance $\mathcal I^{\mathrm{copies}}$ replaces each buyer $i$ by $|J_i|$ single-parameter agents, one per service $j \in J_i$ with value $v_j$, under the same $\mathcal J$.

Price menus. Given prices $(p_j)$ and an arrival order $\sigma$, the price-menu mechanism approaches the buyers in order; buyer $i$ is offered the services of $J_i$ that can still be feasibly allocated, at prices $p_j$, and buys a utility-maximizing one if some has $p_j \le v_j$.

Multiple copies of items. With items $K$ and $\mathrm{cap}(k)$ copies of item $k$, services are pairs $(i,k)$ and a set of services is feasible if it gives each buyer at most one item and uses at most $\mathrm{cap}(k)$ copies of $k$: the intersection of two partition matroids.

Formalization targets

Goal: Theorem 14

For regular distributions there are prices $p$ such that, for every arrival order $\sigma$, the price-menu mechanism $\mathcal P_\sigma$ is truthful and

$$\mathcal R^{\mathcal A} \le \tfrac{27}{4}\,\mathcal R^{\mathcal P_\sigma}$$

for every individually rational, truthful deterministic mechanism $\mathcal A$.

Milestones

• Truthful BMUMD mechanisms are weakly monotone (p. 13), and the allocation of $\mathcal A^{\mathrm{copies}}$ is monotone in each $v_j$ (p. 13).
• Lemma 3: $\mathcal R^{\mathcal A} \le \mathcal R^{\mathcal A'}$ for some truthful $\mathcal A'$ on $\mathcal I^{\mathrm{copies}}$.
• The price-menu mechanism allocates a maximal feasible set of services (p. 14).
• Theorem 4: if $\mathcal R^{M'} \le \alpha\,\mathcal R^{\mathrm{obl}}_{\mathbf p}$ for every truthful $M'$ on $\mathcal I^{\mathrm{copies}}$, then $\mathcal R^{\mathcal A} \le \alpha\,\mathcal R^{\mathcal P_\sigma}$ for every $\sigma$ and every truthful IR $\mathcal A$.
• Lemma 2 (regular part): $\mathcal R^M \le \sum_i p^M_i q^M_i$, with $q^M_i$ the probability that $M$ serves $i$ and $F_i(p^M_i) = 1 - q^M_i$.
• Theorem 19 (existence form): a revenue-optimal truthful mechanism exists.
• The claim $c_i \ge 4/9$ of App. D.4: under $\sum_{i' \in P} q_{i'} \le \mathrm{cap}(P)/3$ in every part, with probability at least $4/9$ neither part of $i$ is full without $i$.
• Theorem 13: for two partition matroids there are prices with $\mathcal R^M \le \tfrac{27}{4}\,\mathcal R^{\mathrm{obl}}_{\mathbf p}$ for every truthful $M$.

Significance

The result shows that for unit-demand buyers, a seller loses at most a constant factor by replacing the optimal, possibly opaque, truthful mechanism with a menu of prices that does not depend on the order in which buyers arrive. The reduction of Theorem 4 is generic: any order-oblivious pricing for the single-parameter instance with copies, under any unit-demand constraint, transfers to the multi-parameter instance with the same factor. Theorem 13 supplies one such pricing for the intersection of two partition matroids, which is exactly the shape of the multi-unit, multi-item constraint.

All results here are proved in the paper and none is formalized elsewhere; the platform has Myerson's single-unit optimal auction and weak monotonicity in an abstract quasilinear model (Börgers), but no posted-price approximation, no copies reduction, and no order-oblivious revenue. The formal development adds a machine-checked account of the reduction (in particular that the price-menu mechanism is truthful and allocates a maximal feasible set for every order), a precise version of the probabilistic claim behind the constant $6.75$, and reusable definitions of order-oblivious revenue and of multi-parameter truthfulness with the paper's individual rationality.

Difficulty

Lemma 3 needs more than the observation that the copies instance has more competition: one must build a truthful single-parameter mechanism with at least the same revenue. The allocation is copied, but the payments must be threshold payments of the copies mechanism, and showing they dominate the original payments uses both weak monotonicity and the paper's individual rationality, through the taxation principle.

Theorem 13 compares order-oblivious revenue with Myerson's revenue through the bound of Lemma 2, at prices built from Myerson's service probabilities scaled by $1/3$. The step that is easy to get wrong is the probability that an agent is considered: the events "part $P_1$ is not full" and "part $P_2$ is not full" depend on overlapping agents, so the product bound $(2/3)(2/3)$ does not follow from Markov's inequality alone; it holds because both events are decreasing in the set of desiring agents (Harris' inequality). The comparison must also be uniform: one set of prices must serve against every truthful mechanism, which requires an optimal mechanism to exist.

Formalization scope

• Distributions (P1): each $F_j$ has a measurable density, strictly positive on a bounded interval $[\underline v_j, \overline v_j] \subseteq [0, \infty)$, with no mass outside. Values are independent (product prior).
• Regularity (P2): the virtual value $\phi(v) = v - (1 - F(v))/f(v)$ is non-decreasing on the support. It is assumed in Lemma 2, Theorem 19, Theorem 13 and the goal. Theorem 14 does not state it, but its proof goes through Theorem 13, which the paper proves for regular distributions; the non-regular extension (App. E, randomized prices) is out of scope, as is the second paragraph of Lemma 2.
• Mechanisms (P3): deterministic; dominant-strategy truthful with misreports in the support (a buyer misreports all coordinates of $J_i$ at once); single-parameter IR is ex-post nonnegative utility; multi-parameter IR is the paper's ($\pi_i \le v_j$ if served $j$, $\pi_i = 0$ if unserved); allocation events and payments measurable, payments integrable.
• Benchmarks (P4): Myerson's mechanism is not constructed. "Approximates $\mathcal R^{\mathcal M}$" is stated against every truthful mechanism, and Lemma 3 and Theorem 19 in existence form.
• Price menus: ties between utility-maximizing services are broken by a fixed enumeration of $J$; a service of utility $0$ is bought. Theorem 4 assumes $\alpha \ge 0$.
• Dropped: the last sentence of Theorem 14 (polynomial-time computability of the prices) has no cost model here.
• Constant: $6.75$ is written $27/4$ everywhere.
• Not trivializable: the prices in Theorem 13 and the goal are chosen before the mechanism, and the benchmark includes every truthful mechanism, so a degenerate price vector cannot meet the bound; $\mathcal R^{\mathrm{obl}}_{\mathbf p}$ is a genuine minimum over a nonempty finite class.

Needed infrastructure, reusable beyond this mission: Myerson's characterization of truthful single-parameter mechanisms and the revenue–virtual-surplus identity for densities on intervals, Harris' inequality for product measures, and the taxation principle for deterministic multi-parameter mechanisms. Contributions on any of these are welcome.

Selected references

• S. Chawla, J. D. Hartline, D. Malec, B. Sivan, Multi-parameter Mechanism Design and Sequential Posted Pricing, STOC 2010; arXiv:0907.2435v2, 2010. https://arxiv.org/abs/0907.2435
• R. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 1981. https://doi.org/10.1287/moor.6.1.58
• S. Chawla, J. D. Hartline, R. Kleinberg, Algorithmic Pricing via Virtual Valuations, EC 2007. https://arxiv.org/abs/0711.3203
• A. M. Manelli, D. R. Vincent, Multidimensional mechanism design: Revenue maximization and the multiple-good monopoly, Journal of Economic Theory 137(1), 2007. https://doi.org/10.1016/j.jet.2006.12.007
• T. E. Harris, A lower bound for the critical probability in a certain percolation process, Proc. Cambridge Philos. Soc. 56, 1960. https://doi.org/10.1017/S0305004100034241

Motivation

Long-running projects such as construction, plant engineering or software development involve payments to and from the contractor at many points in time: disbursements when activities are carried out, progress payments when milestones are reached. When the planning horizon is long, money received later is worth less, and the natural financial objective is the net present value of all cash flows. Scheduling a project to maximize its net present value subject to minimum and maximum time lags was studied by Russell (1970) and Grinold (1972), and the problem is the prototype of a nonregular objective: delaying an activity can be profitable, because disbursements lose value when they are postponed.

This mission follows Chapter 3 of Neumann, Schwindt and Zimmermann, Project Scheduling with Time Windows and Scarce Resources (2nd ed., Springer 2003). The book shows that the net present value objective belongs to the class of binary-monotone objective functions (§3.3.5), and it uses this in §3.9.1 to give a combinatorial optimality criterion for the resource-free problem: a vertex schedule is optimal exactly when the subprojects cut off by the arcs of a spanning tree have net present values of the right sign (Proposition 3.9.2). That criterion drives the book's parametric analysis of the net present value as a function of the discount rate and the deadline.

Setting

A project consists of activities $V=\{0,1,\dots,n+1\}$, $n\ge1$, where $0$ is the project beginning and $n+1$ the project completion. Activity $i$ has an integer duration $p_i$, with $p_0=p_{n+1}=0$ and $p_i>0$ otherwise. Temporal constraints are the arcs of a project network $N=\langle V,E;\delta\rangle$: an arc $\langle i,j\rangle$ with integer weight $\delta_{ij}$ requires $S_j-S_i\ge\delta_{ij}$ for the start times $S_i$. A maximum project duration $\bar d$ is the arc $\langle n+1,0\rangle$ with weight $-\bar d$. The time-feasible region is

$$\mathcal S_T=\{S\in\mathbb R^{n+2}_{\ge0}\mid S_0=0,\ S_j-S_i\ge\delta_{ij}\ (\langle i,j\rangle\in E)\}.$$

Let $0<\beta\le1$ be the discount rate ($\beta=1/(1+I)$ for an interest rate $I$) and $c_i^F\in\mathbb R$ the cash flow of activity $i$, paid at its completion time $C_i=S_i+p_i$. The problem (3.9.1) is

$$\text{minimize } f(S)=-\sum_{i\in V}c_i^F\beta^{S_i+p_i}\quad\text{subject to } S\in\mathcal S_T,$$

and a minimizer is a time-optimal schedule. A vertex of $\mathcal S_T$ is an extreme point. A spanning tree $G=\langle V,E^G\rangle$ is associated with $S$ if $E^G\subseteq E$, $E^G$ has $n+1$ arcs and a connected underlying undirected graph, and $S$ is the unique solution of $S_0=0$, $S_j-S_i=\delta_{ij}$ for $\langle i,j\rangle\in E^G$. Deleting a tree arc $\langle i,j\rangle$ splits $G$ into two subtrees; $V_{ij}$ is the node set of the one not containing $0$. The arc is forward if the tree path from $0$ passes it from $i$ to $j$ and backward otherwise, and

$$npv^{ij}(S)=\sum_{h\in V_{ij}}c_h^F\beta^{S_h+p_h}$$

is the net present value of the subproject $V_{ij}$. Finally, $f$ is binary-monotone if it is monotone on every line $\{S+\lambda z\ge0\mid\lambda\in\mathbb R\}$ with direction $z\in\{0,1\}^{n+2}$ (Definition 3.3.2).

Formalization targets

Goal: Proposition 3.9.2, pinned reading

Assume every node is reached from $0$ by a path of nonnegative length (the standing convention of §1.2) and let $S$ be a vertex of $\mathcal S_T$.

$$\text{(sufficiency)}\quad G \text{ associated with } S,\ \ npv^{ij}(S)\ge0 \text{ on forward arcs},\ npv^{ij}(S)\le0 \text{ on backward arcs}\ \Longrightarrow\ S \text{ time-optimal};$$ $$\text{(necessity, } \beta<1)\quad S \text{ time-optimal}\ \Longrightarrow\ \exists\, G \text{ associated with } S \text{ satisfying the sign conditions}.$$

The book states "if and only if … for each arc of the corresponding spanning tree", where the corresponding tree is chosen using optimality. The two directions above are the reading that makes the statement well defined: sufficiency for every associated tree, necessity for some associated tree.

Milestones

1. §3.3.5: the net present value objective is binary-monotone and sum-separable.
2. §3.9.1: if $\mathcal S_T$ is nonempty and bounded, some vertex of $\mathcal S_T$ is time-optimal.
3. Proposition 3.2.16: every vertex of $\mathcal S_T$ has an associated spanning tree, an outtree rooted at $0$ if the vertex is a minimal point.
4. Proposition 3.5.4: a directed forest with at least one node has a source with at most one successor or a sink with exactly one predecessor.

Significance

Proposition 3.9.2 turns a nonconvex continuous optimization problem into a finite check on a spanning tree. Read as an economic statement, it says that at an optimal schedule no subproject with positive net present value can be started earlier and no subproject with negative net present value can be postponed. The book builds on it the parametric procedure of §3.9.1, which tracks the optimal tree as the discount rate or the deadline varies (Propositions 3.9.3 and 3.9.4), and the steepest descent method of §3.5.2 terminates exactly when the criterion holds.

The results are proved in the book, partly by reference to network optimization (Ahuja et al., 1993) and to Schwindt and Zimmermann (2001, 2002). None of them is formalized on the platform or, as far as is known, anywhere else. A formal proof would give the first machine-checked optimality certificate for a nonregular project scheduling objective, and the spanning-tree description of vertices (Proposition 3.2.16) is shared with Mission VI of this series.

Difficulty

The objective $f$ is neither convex nor concave when cash flows of both signs occur, so local optimality at a vertex does not imply global optimality by a convexity argument, and a first-order check along the edges of $\mathcal S_T$ is not obviously enough. The criterion is also not a statement about one tree: a degenerate vertex, where more than $n+1$ temporal constraints are binding, has several associated trees, and the sign conditions may hold on some and fail on others. Necessity therefore requires producing a suitable tree, not checking a given one. Finally, the combinatorial objects (the subtree $V_{ij}$, forward and backward orientation relative to the root) have to be connected to the geometry of $\mathcal S_T$ through Proposition 3.2.16, whose proof in the book is a citation.

Formalization scope

Activities are Fin (n + 2) with 0 the project beginning and Fin.last (n+1) the project completion; start times are real; durations are natural numbers and arc weights integers. The deadline is a structure field together with the backward arc $\langle n+1,0\rangle$ of weight $-\bar d$. $\beta^x$ is Real.rpow, and every statement assumes $0<\beta\le1$ as the book does (p. 203). Vertices are Set.extremePoints ℝ. A spanning tree is a Finset of $n+1$ arcs whose SimpleGraph.fromRel is connected; $V_{ij}$ is the set of nodes not reachable from $0$ once the arc is deleted.

Three readings are committed and disclosed in the item statements. Necessity is stated only for $\beta<1$: at $\beta=1$ the objective is constant, every schedule is optimal, and the sign conditions can fail on every tree. The standing convention of §1.2 (a path of nonnegative length from $0$ to every node) is a hypothesis of Proposition 3.2.16 and of the goal; without it a vertex can be fixed by $S_i\ge0$ rather than by arcs of $N$, and necessity fails. The existence of an optimal vertex assumes $\mathcal S_T$ nonempty and bounded, which the book asserts in §3.1. Chapter 3's resource constraints do not occur in this mission, which concerns $PS\infty|temp,\bar d|f$ only.

The goal cannot be discharged by choosing the tree freely: associated trees must consist of arcs of $N$ that are binding at $S$ and determine $S$ uniquely, and sufficiency must hold for every such tree. Contributions welcome beyond the milestones: a proof of Proposition 3.2.16 reusable by Mission VI, and a general lemma relating binding spanning trees of difference constraints to extreme points.

Selected references

• K. Neumann, C. Schwindt, J. Zimmermann, Project Scheduling with Time Windows and Scarce Resources, 2nd ed., Springer, 2003, §3.1 (p. 203), §3.3.5 (pp. 224–225), §3.5.2 (p. 252), §3.9.1 (pp. 333–334). https://doi.org/10.1007/978-3-540-24800-2
• A. H. Russell, "Cash flows in networks", Management Science 16 (1970), 357–373. https://doi.org/10.1287/mnsc.16.5.357
• R. C. Grinold, "The payment scheduling problem", Naval Research Logistics Quarterly 19 (1972), 123–136.
• C. Schwindt, J. Zimmermann, "A steepest ascent approach to maximizing the net present value of projects", Mathematical Methods of Operations Research 53 (2001), 435–450.
• C. Schwindt, J. Zimmermann, "Parametrische Optimierung als Instrument zur Bewertung von Investitionsprojekten", Zeitschrift für Betriebswirtschaft 72 (2002), 593–617.
• R. K. Ahuja, T. L. Magnanti, J. B. Orlin, Network Flows, Prentice Hall, 1993.
• C. Berge, Graphs and Hypergraphs, North-Holland, Amsterdam, 1976.

Motivation

The classical Lagrange multiplier rule and its inequality-constrained form, the Karush–Kuhn–Tucker (KKT) conditions, are necessary conditions satisfied at a minimizer of a constrained problem. In finite dimensions, a continuous function bounded below on a closed bounded feasible set attains its minimum, so the rule describes an actual point. In an infinite-dimensional Banach space this fails: closed bounded sets are not compact, minimizing sequences need not converge, and a smooth function bounded below on a smooth constraint set can have no minimizer at all. The multiplier rule then has nothing to describe.

Ekeland's 1974 paper On the Variational Principle (DOI) introduced a principle (its Theorem 1.1) that replaces "a minimizer exists" with "near every almost-minimizer there is a point that strictly minimizes a slightly perturbed function". Section 3 of the paper uses this to prove that, for a problem with finitely many smooth equality and inequality constraints satisfying a linear-independence regularity condition, nearly optimal feasible points satisfy the KKT conditions up to a small error, with no compactness and no existence of a minimizer. This is the first appearance of what is now called an approximate or asymptotic KKT condition, a notion central to the convergence theory of nonlinear programming algorithms.

Setting

Let $V$ be a real Banach space with dual $V^*$ (continuous linear functionals) and dual norm $\|x^*\|_*=\sup_{\|h\|\le1}\langle x^*,h\rangle$. Let $F:V\to\mathbb R$ be Fréchet-differentiable, with derivative $F'(v)\in V^*$, and let $G_1,\dots,G_m:V\to\mathbb R$ be $C^1$ (continuously Fréchet-differentiable). Fix $0\le p\le m$ and consider

$$\inf F(v)\quad\text{subject to}\quad G_i(v)=0\ (1\le i\le p),\qquad G_i(v)\ge0\ (p+1\le i\le m). \tag{3.1}$$

The feasible set is $\mathcal C=\{v\in V : G_i(v)=0 \text{ for } i\le p,\ G_i(v)\ge0 \text{ for } i>p\}$ (3.2). At $v\in\mathcal C$ the saturated constraints are $I(v)=\{i : G_i(v)=0\}$ (3.3). The regularity assumption (3.4) is: for every $v\in\mathcal C$, the derivatives $G_i'(v)$, $i\in I(v)$, are linearly independent in $V^*$.

In the Lean development these are EkelandVP.Constraints.feasibleSet p G and EkelandVP.Constraints.IsRegular p G, with constraints indexed by Fin m.

Formalization targets

Goal: Theorem 3.1 (p. 330)

Assume (3.4), $\mathcal C\ne\emptyset$, and that $F$ is bounded below on $\mathcal C$ (3.5). Then for every $\varepsilon>0$ there are $v_\varepsilon\in\mathcal C$ and $\lambda_1,\dots,\lambda_m\in\mathbb R$ with

$$F(v_\varepsilon)\le\inf_{\mathcal C}F+\varepsilon^2,\qquad \lambda_i\ge0\ (i>p),\qquad \lambda_i=0 \text{ if } G_i(v_\varepsilon)\ne0,$$ $$\Big\|F'(v_\varepsilon)-\sum_{i=1}^m\lambda_iG_i'(v_\varepsilon)\Big\|_*\le\varepsilon.$$

Milestones, in the order of the paper's proof

1. (3.8)–(3.12): a feasible $v$ with $F(v)\le\inf_{\mathcal C}F+\varepsilon^2$ and $F(w)\ge F(v)-\varepsilon\|w-v\|$ for all $w\in\mathcal C$ (the variational principle applied to $F$ restricted to $\mathcal C$; no regularity needed).
2. (3.16): at a regular feasible point $v$, every $h$ with $\langle G_i'(v),h\rangle=0$ ($i\le p$) and $\langle G_i'(v),h\rangle\ge0$ ($i>p$, $i\in I(v)$) is the initial velocity of a $C^1$ curve $u:[0,\tau]\to\mathcal C$ with $u(0)=v$.
3. Lemma 3.2: at a point with the property of milestone 1, $\langle F'(v),h\rangle\ge-\varepsilon\|h\|$ for every such $h$.
4. Lemma 3.3: an $\varepsilon$-Farkas–Minkowski lemma in $V^*$: if $\langle w^*,h\rangle\ge-\varepsilon\|h\|$ whenever $\langle u_i^*,h\rangle=0$ and $\langle v_j^*,h\rangle\ge0$, then $\|w^*-\sum\lambda_iu_i^*-\sum\mu_jv_j^*\|_*\le\varepsilon$ for some $\lambda_i\in\mathbb R$ and $\mu_j\ge0$.

An additional item states Corollary 3.4 (p. 333), the one-constraint case: if $G(v)=0\Rightarrow G'(v)\ne0$, $\{G=0\}\neq\emptyset$ and $F$ is bounded below on $\{G=0\}$, then for every $\varepsilon>0$ there are $v_\varepsilon$ with $G(v_\varepsilon)=0$ and $\lambda_\varepsilon\in\mathbb R$ with $\|F'(v_\varepsilon)-\lambda_\varepsilon G'(v_\varepsilon)\|_*\le\varepsilon$.

Significance

The result. Theorem 3.1 is an existence theorem for approximate KKT points that needs neither compactness nor attainment of the infimum. It shows that every bounded-below problem with regular constraints has a sequence of feasible points whose objective values converge to the infimum and along which the KKT residual tends to zero. This is the property that later work calls approximate KKT or asymptotic KKT (AKKT) and uses as a stopping criterion and as a sequential optimality condition for nonlinear programming. Corollary 3.4 is the corresponding nonlinear eigenvalue statement: on a regular level set, $F'$ is approximately proportional to $G'$ at almost-minimizing points.

Formalizing it. The result is classical and proved in the paper; to our knowledge no machine-checked version exists. Mathlib has the Fréchet derivative, the implicit function theorem for strictly differentiable maps, Banach–Alaoglu and the Hahn–Banach separation theorems, but no Ekeland principle in this form, no Lyusternik-type tangent-curve theorem for mixed equality–inequality constraints, and no Farkas lemma in a dual Banach space. Each milestone is a reusable piece of nonlinear optimization theory in Banach spaces.

Difficulty

The obvious argument, "take a minimizer and apply the Lagrange multiplier rule", fails at the first step because no minimizer need exist. The variational principle supplies a point $v_\varepsilon$ that minimizes $F+\varepsilon\|\cdot-v_\varepsilon\|$ on $\mathcal C$, but that function is not differentiable at $v_\varepsilon$, so the multiplier rule cannot be applied to it directly either. Two further gaps remain. Linearized feasible directions (those satisfying the derivative conditions on the active constraints) need not be directions along which one can actually move inside $\mathcal C$; closing this gap requires the regularity assumption and completeness of $V$, and must keep the active inequality constraints nonnegative, not just the equalities. And the resulting first-order inequality, which holds only up to $\varepsilon\|h\|$, must be turned into an approximate multiplier representation in $V^*$, an infinite-dimensional dual space in which the usual finite-dimensional Farkas lemma does not apply as stated.

Formalization scope

• $V$ is a real Banach space: [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V]. $V^*$ is V →L[ℝ] ℝ with the operator norm; $F'(v)$ is fderiv ℝ F v.
• Constraints are one family G : Fin m → V → ℝ, 0-based: the paper's constraint $i$ is Lean index $i-1$, an equality constraint iff its index is $<p$. p ≤ m is assumed in the goal.
• $C^1$ is ContDiff ℝ 1; $F$ is Differentiable ℝ F (Fréchet-differentiable everywhere).
• No infimum over $\mathcal C$ is formed: "bounded below" is BddBelow (F '' 𝒞) and "$F(v)\le\inf_{\mathcal C}F+\varepsilon^2$" is "$F(v)\le F(w)+\varepsilon^2$ for all $w\in\mathcal C$". A real infimum over an empty or unbounded set would be a junk value.
• Added hypotheses, disclosed in each item: $\mathcal C\ne\emptyset$ (goal and milestone 1) and $\{G=0\}\ne\emptyset$ (Corollary 3.4). Without them the paper's hypotheses hold vacuously ($\inf\emptyset=+\infty$) while the conclusion asks for a feasible point.
• Lemma 3.3 is stated with $\le\varepsilon$. The paper prints $<\varepsilon$ in (3.20), which fails for $V=\mathbb R$, no constraints and $w^*=\varepsilon\,\mathrm{id}$; its proof gives $\le$, and Theorem 3.1 uses $\le$.
• Lemma 3.2 and milestone 2 assume the linear independence (3.4) only at the point $v$ under consideration, and Lemma 3.2 is stated for any feasible $v$ with property (3.12); this is exactly what the paper's proof uses.
• Regularity is a linear independence of the indexed family $(G_i'(v))_{i\in I(v)}$, so a repeated saturated constraint violates it; the constraint qualification cannot be trivialized by collapsing duplicates.

Contributions welcome: a general Ekeland principle with the strict-minimizer conclusion, a Lyusternik–Graves tangent-curve theorem for $C^1$ maps with surjective derivative onto $\mathbb R^k$, and a closedness result for finitely generated cones in $V^*$.

Selected references

• I. Ekeland, On the Variational Principle, J. Math. Anal. Appl. 47 (1974) 324–353. https://doi.org/10.1016/0022-247X(74)90025-0
• I. Ekeland, Nonconvex minimization problems, Bull. Amer. Math. Soc. (N.S.) 1 (1979) 443–474. https://doi.org/10.1090/S0273-0979-1979-14595-6
• R. Andreani, G. Haeser, J. M. Martínez, On sequential optimality conditions for smooth constrained optimization, Optimization 60 (2011) 627–641. https://doi.org/10.1080/02331930903578700