All missions

Motivation

A postman, a snowplough or a street sweeper must traverse every street of a district and return to the depot. When some streets are one-way, the street network is a mixed graph: some edges are directed and must be traversed in a prescribed direction, the others are undirected and may be traversed either way. The first question about such a route is whether a closed route exists that traverses every street exactly once, an Euler tour of the mixed graph. When one exists, it is an optimal postman route; when none exists, the postman problem asks which streets to repeat.

J. Edmonds and E.L. Johnson treat this question in §6 of Matching, Euler tours and the Chinese postman (Mathematical Programming 5, 1973), the paper that solved the undirected Chinese postman problem by matching. Section 6 gives an algorithm that finds an Euler tour in any mixed graph that is connected, of even degree and symmetric, and §7 uses it for the mixed postman problem.

Timeline.

• 1736: Euler's condition for undirected graphs (even degrees, connectivity).
• 1951: T. van Aardenne-Ehrenfest and N.G. de Bruijn enumerate the Euler tours of a symmetric directed graph through spanning arborescences ("circuits and trees in oriented linear graphs"). Edmonds and Johnson cite this as the source of their arborescence rule.
• 1962: L.R. Ford and D.R. Fulkerson (Flows in Networks, §II.7) characterize, by a flow argument, when a mixed graph has an Euler tour without assuming symmetry.
• 1973: Edmonds and Johnson give the combined orientation and Rule algorithm of §6 for connected, even, symmetric mixed graphs, and the existence criterion of §7 for mixed postman tours.
• 1976: C.H. Papadimitriou shows the mixed postman problem NP-hard, so the polynomial-time picture of §6 does not extend to its optimization version.

Setting

A mixed graph $G$ has a finite set $N$ of nodes and a finite set $E$ of edges. Each edge $e$ meets two distinct nodes; several edges may meet the same pair of nodes. Some edges are directed: an edge directed away from node $i$ toward node $j$ must be traversed from $i$ to $j$. In Lean an edge has a tail, a head (distinct) and a Boolean directed; for an undirected edge the order of the two ends carries no meaning.

• The degree of a node is the total number of edges, regardless of direction, meeting it. $G$ is even if every degree is even.
• $\operatorname{out}(n)$ and $\operatorname{in}(n)$ count the directed edges directed away from and toward $n$. $G$ is symmetric if $\operatorname{out}(n)=\operatorname{in}(n)$ for every node $n$.
• $G$ is connected if it is connected when the directions on the edges are ignored.
• A mixed walk is a sequence $(n_1,e_1,n_2,\dots,e_l,n_{l+1})$ in which each directed $e_i$ goes from its tail $n_i$ to its head $n_{i+1}$ and each undirected $e_i$ meets $n_i$ and $n_{i+1}$. It is a tour if $n_{l+1}=n_1$, an Euler tour if it contains every edge exactly once, and a postman tour if it contains every edge at least once.
• An arborescence with root $r$ is a tree $T$ of directed edges in which every node $n\neq r$ of $T$ has precisely one edge of $T$ directed away from $n$. Following those edges from any node of $T$ leads to $r$. It is spanning if it contains every node.

Formalization targets

Goal: the mixed Euler tour theorem (§6, pp. 115–118)

If $G$ is connected, even and symmetric, then for every node $r$

$$\exists\ (r=n_1,e_1,\dots,e_l,n_{l+1}=r)\ \text{a mixed Euler tour of } G .$$

Milestones

1. Cut balance (p. 116). If $G$ is symmetric, every node set $S$ has as many directed edges leaving it as entering it.
2. Maximal arborescences span (pp. 115–116). Suppose the directed edges form a symmetric, connected spanning subgraph. Then an arborescence of directed edges to which no directed edge entering it from outside can be added contains every node.
3. The Rule (pp. 116–117). Suppose the directed edges form a symmetric connected spanning subgraph and the undirected edges have even degree. Fix a spanning arborescence with root $r$ and order the directed edges leaving each node $n\neq r$ so that the arborescence edge comes last. Then the following traversal from $r$ is an Euler tour: leave by the next unused undirected edge if there is one, otherwise by the next unused directed edge.
4. The assignment outcome (p. 118). If $G$ is connected, even and symmetric, directions can be assigned to some undirected edges so that the result is symmetric, its directed edges form a connected spanning subgraph, and the unassigned edges have even degree.
5. Mixed postman criterion (§7, p. 120). A connected mixed graph has a postman tour if and only if no nonempty proper node set $S$ has every boundary edge directed away from $S$.

Significance

The goal contains two classical theorems as special cases. With every edge undirected it is Euler's theorem for connected even multigraphs. With every edge directed it is the theorem that a connected balanced digraph is Eulerian. The milestones connect the two cases: an orientation reduces the mixed case to one the Rule can handle. The Rule itself is the van Aardenne-Ehrenfest–de Bruijn construction, which underlies the BEST theorem counting Euler tours. Milestone 5 decides whether the mixed postman problem has any feasible solution. The mixed postman problem is the standard model for routing on one-way street networks.

All results here are proved in the paper, so none is open. No Lean proof of any of them in this form is known. Mathlib's Eulerian walks are for simple graphs; it has no multigraph or mixed-graph Euler theorem, no directed Euler theorem and no arborescence-based traversal. The mission produces these, together with a reusable vocabulary of mixed multigraphs, walks that respect directions, and arborescences given by parent edges.

Difficulty

The obvious approach to the goal is to forget the directions and apply Euler's theorem. This fails because the tour it produces may traverse a directed edge backwards. Orienting all undirected edges at once also fails: an arbitrary orientation of the undirected edges need not keep every node balanced.

The difficult part of the Rule is showing that the greedy traversal does not get stuck before using every edge. It cannot stop at a node other than $r$ because of the degree conditions. The hard step is showing that no edge is left unused when it stops at $r$. The answer depends on the ordering condition: without the arborescence edge last at every node, the Rule can return to $r$ with edges still unused. The assignment step needs an invariant: the orientation must keep every node symmetric while it extends a spanning structure of directed edges.

Formalization scope

• Graphs. Nodes and edges are finite types (Fintype V, Fintype E). Parallel edges are allowed, including a directed and an undirected edge on the same pair. Loops are excluded (tail e ≠ head e), following the paper's standing setting of §2 (p. 91: edges meet two different nodes). Edges are a type, not a relation on nodes, so parallel edges stay distinct in every walk.
• Hypotheses as on p. 115. "Even" counts all edges, directed or undirected. "Symmetric" counts only directed edges. "Connected" ignores directions. Strong connectivity is not assumed. "Symmetric" does not mean that every node has even in-degree, and an Euler tour of the underlying undirected multigraph does not satisfy the goal: the tour must traverse each directed edge from its tail to its head.
• Walks are a node list and an edge list of length one less. The one-node walk is allowed, so the graph with one node and no edges satisfies the goal.
• Arborescences are given by an optional edge $a_n$ at each node, with an edge required for each non-root node of $W$; following those edges leads to $r$. A maximal arborescence is one where no directed edge enters $W$ from outside. The optional choice represents the root-only arborescence when the graph has no edges.
• The Rule is computed by a fuel-bounded traversal (at most $|E|$ steps) that keeps a global list of used edges. Its conclusion is that the computed sequences form a mixed Euler tour from $r$.
• The assignment is an existential statement over a second mixed graph $G'$ on the same edges, with the same unordered ends and every directed edge kept. The paper's algorithm (Steps 0–3) is not formalized.
• Postman criterion. "Proper subset" means nonempty and proper. Connectivity is assumed, as throughout §7, and the node set is nonempty (with no nodes there is no tour, while the criterion holds vacuously).
• Not formalized. The §7 evenness argument (p. 122) and the min-cost flow formulations are outside the scope.

Contributions are welcome at every level: proofs of the milestones, a direct proof of the goal, and general lemmas about mixed multigraph walks.

Selected references

• J. Edmonds and E.L. Johnson, Matching, Euler tours and the Chinese postman, Mathematical Programming 5 (1973) 88–124. https://doi.org/10.1007/BF01580113
• T. van Aardenne-Ehrenfest and N.G. de Bruijn, Circuits and trees in oriented linear graphs, Simon Stevin 28 (1951) 203–217.
• L.R. Ford and D.R. Fulkerson, Flows in Networks, Princeton University Press, 1962.
• C.H. Papadimitriou, On the complexity of edge traversing, Journal of the ACM 23 (1976) 544–554. https://doi.org/10.1145/321958.321974

Motivation

A decision maker who must minimize an expected cost $\mathbb E^{\mathbb P}[h(x,\xi)]$ rarely knows the distribution $\mathbb P$ of the uncertain parameter $\xi$; usually only $N$ samples $\hat\xi_1,\dots,\hat\xi_N$ are available. Replacing $\mathbb P$ by the empirical distribution (sample average approximation) tends to produce decisions that perform poorly out of sample when $N$ is small. Distributionally robust optimization instead minimizes the worst expected cost over a set of distributions that are plausible given the data. Mohajerin Esfahani and Kuhn (arXiv:1505.05116v3, published in Mathematical Programming 171, 2018) take that set to be a ball in the Wasserstein metric around the empirical distribution. Such balls give finite-sample and asymptotic guarantees, but each evaluation of the robust objective is an optimization over infinitely many probability distributions. Section 4.1 of the paper shows that, for a large class of losses, this inner problem is a finite convex program. That result, Theorem 4.2, is the subject of this mission.

Timeline. Wasserstein ambiguity sets for portfolio selection were proposed by Pflug and Wozabal (2007); before this paper, robust problems over such sets were solved with global optimization algorithms (Pflug and Pichler 2014). Strong duality for conic linear and moment problems (Shapiro 2001) underlies the reduction. Mohajerin Esfahani and Kuhn (preprint 2015, journal 2018) proved the convex reduction for piecewise concave losses; Gao and Kleywegt (arXiv:1604.02199) and Blanchet and Murthy (arXiv:1604.01446) proved strong duality for general transport costs in 2016.

Setting

Let $E$ be a finite-dimensional real vector space with an arbitrary norm $\|\cdot\|$ (the paper's $\mathbb R^m$) and its Borel σ-algebra. Its dual norm is $\|z\|_* = \sup_{\|\xi\|\le 1}\langle z,\xi\rangle$, where $\langle z,\xi\rangle$ is the value of the linear functional $z$ at $\xi$. Let $\Xi\subseteq E$ be the support set and $\hat\xi_1,\dots,\hat\xi_N\in\Xi$ the samples, with empirical distribution $\widehat{\mathbb P}_N=\frac1N\sum_{i=1}^N\delta_{\hat\xi_i}$.

The 1-Wasserstein distance between two distributions is the least transport cost $\int\|\xi-\xi'\|\,\Pi(d\xi,d\xi')$ over all couplings $\Pi$ with the given marginals. The Wasserstein ball $\mathbb B_\varepsilon(\widehat{\mathbb P}_N)$ is the set of probability distributions on $\Xi$ within distance $\varepsilon\ge 0$ of $\widehat{\mathbb P}_N$.

The loss is a pointwise maximum $\ell(\xi)=\max_{k\le K}\ell_k(\xi)$ of measurable functions $\ell_k:E\to\overline{\mathbb R}=\mathbb R\cup\{\pm\infty\}$. Its expectation is $\mathbb E^{\mathbb Q}[\ell]=\mathbb E^{\mathbb Q}[\max\{\ell,0\}]+\mathbb E^{\mathbb Q}[\min\{\ell,0\}]$ with $\infty-\infty=\infty$. The worst-case expectation is

$$\sup_{\mathbb Q\in\mathbb B_\varepsilon(\widehat{\mathbb P}_N)}\mathbb E^{\mathbb Q}[\ell(\xi)].\tag{10}$$

The conjugate of $f:E\to\overline{\mathbb R}$ is $f^*(z)=\sup_\xi\langle z,\xi\rangle-f(\xi)$, the characteristic function $\chi_\Xi$ is $0$ on $\Xi$ and $+\infty$ off it, and the support function is $\sigma_\Xi(z)=\sup_{\xi\in\Xi}\langle z,\xi\rangle$. Assumption 4.1 requires $\Xi$ to be convex and closed, each $-\ell_k$ to be proper, convex and lower semicontinuous, and no $\ell_k$ to be identically $-\infty$ on $\Xi$.

Formalization targets

Goal: Theorem 4.2 (convex reduction)

Under Assumption 4.1, for every $\varepsilon\ge0$, (10) equals

$$\inf_{\lambda,s_i,z_{ik},\nu_{ik}}\ \lambda\varepsilon+\frac1N\sum_{i=1}^N s_i\quad\text{s.t.}\quad [-\ell_k]^*(z_{ik}-\nu_{ik})+\sigma_\Xi(\nu_{ik})-\langle z_{ik},\hat\xi_i\rangle\le s_i,\ \ \|z_{ik}\|_*\le\lambda\quad\forall i,k.\tag{11}$$

Milestones, in the order of the paper's proof

1. (12a)–(12c). Without any convexity, (10) is at most the value of (12c): $\inf\{\lambda\varepsilon+\frac1N\sum_i s_i:\ \sup_{\xi\in\Xi}(\ell(\xi)-\lambda\|\xi-\hat\xi_i\|)\le s_i,\ \lambda\ge0\}$.
2. Corollary 4.3. Without Assumption 4.1, (10) is at most the value of (12f), the program with constraints $[-\ell_k+\chi_\Xi]^*(z_{ik})-\langle z_{ik},\hat\xi_i\rangle\le s_i$ and $\|z_{ik}\|_*\le\lambda$.
3. (12a) is an equality for $\varepsilon>0$ under Assumption 4.1.
4. The case $\varepsilon=0$. (10) is the sample average $\frac1N\sum_i\ell(\hat\xi_i)$, the objective of (12b) converges to it as $\lambda\to\infty$, and (12a) is again an equality.
5. (12e) is an equality. For each constraint, $\sup_{\xi\in\Xi}(\ell_k(\xi)-\lambda\|\xi-\hat\xi_i\|)=\min_{\|z\|_*\le\lambda}\sup_{\xi\in\Xi}(\ell_k(\xi)-\langle z,\xi-\hat\xi_i\rangle)$.
6. (10) equals (12f) under Assumption 4.1.
7. (12f) equals (11) under Assumption 4.1, as optimal values.

Significance

Theorem 4.2 is what makes Wasserstein distributionally robust optimization computable. Once the worst-case expectation is a convex program in $(\lambda,s,z,\nu)$, minimizing over the decision $x$ becomes one larger convex program. Section 5 of the paper derives linear and conic programs from it for piecewise affine losses, uncertainty quantification and two-stage problems. Theorem 4.4 of the same paper (mission II of this series) builds worst-case distributions from the same program. Corollary 4.3 gives a conservative convex bound for losses that are not piecewise concave.

The result is proved on paper; no machine-checked proof of it is known. A formal development needs a working theory of extended-valued conjugates, support functions and inf-convolution in a normed space, Kantorovich-type couplings of an empirical measure, and a minimax theorem over a compact dual ball. Each of these is reusable well beyond this paper.

Difficulty

The weak inequality, (10) $\le$ (12f), is the elementary direction: integrate a pointwise bound against a near-optimal coupling. The difficulty lies in the two equalities. Equality in (12a) is strong duality for an infinite-dimensional moment problem whose loss may take the values $\pm\infty$ and may be unbounded on an unbounded $\Xi$. A Slater point exists only for $\varepsilon>0$, so $\varepsilon=0$ needs a separate limit argument. The equality (12f) $=$ (11) is subtle as well. The conjugate of $-\ell_k+\chi_\Xi$ is only the closure of the inf-convolution of $[-\ell_k]^*$ and $\sigma_\Xi$, so the two constraint sets differ and only the optimal values agree. The paper's sentence "cl$[f]\le 0$ iff $f\le0$" is false pointwise and cannot be formalized as written.

Formalization scope

• Space. $E$ is a finite-dimensional real normed space with its Borel σ-algebra. The pairing $\langle z,\xi\rangle$ is application of a continuous linear functional $z$, and $\|z\|_*$ is the operator norm. These choices keep the paper's arbitrary norm; §5 of the paper uses the 1- and ∞-norms.
• Extended reals. Values are in EReal. Mathlib's EReal has $\top+\bot=\bot$, whereas the paper has $\infty-\infty=\infty$, so the expectation treats an infinite positive part separately, and $[-\ell_k+\chi_\Xi]^*(z)$ is written as $\sup_{\xi\in\Xi}(\langle z,\xi\rangle+\ell_k(\xi))$, with no addition at all. The one EReal sum, $[-\ell_k]^*+\sigma_\Xi$ in (11), never meets $\top+\bot$ under Assumption 4.1.
• Programs. Each optimal value is an infimum over a feasibility predicate with real epigraph variables, so an infeasible program has value $+\infty$.
• Ball. The ball is the published WassersteinDRO.Duality.ambiguitySet with $p=1$ around empiricalDistribution. Its condition $\mathbb Q(\Xi^{\mathrm c})=0$ encodes $\mathbb Q\in\mathcal M(\Xi)$. The finite first moment is automatic at finite distance from $\widehat{\mathbb P}_N$.
• Standing assumptions. Every statement carries $N\ge1$, $K\ge1$, $\hat\xi_i\in\Xi$ (§2, p. 5) and measurability of each $\ell_k$ (p. 11). The radius condition is $\varepsilon\ge0$, or $\varepsilon>0$ in milestone 3.
• Assumption 4.1. Convexity of $-\ell_k$ is stated through its real epigraph, because ConvexOn cannot take an EReal codomain.
• Not trivializable. The statements cannot be made vacuous by an empty ball, because the samples lie in $\Xi$. They cannot be trivialized by a junk expectation either: the expectation is not guarded by integrability, so a distribution with infinite expected loss makes (10) infinite, exactly as in the paper.

Welcome contributions are reusable lemmas on EReal-valued conjugates and support functions, the decomposition of a coupling with an empirical marginal into conditional distributions, the dual-norm identity $\max_{\|z\|_*\le\lambda}\langle z,v\rangle=\lambda\|v\|$, and a Sion-type minimax theorem.

Selected references

• P. Mohajerin Esfahani, D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric: performance guarantees and tractable reformulations, arXiv:1505.05116v3, 2017; Math. Program. 171 (2018) 115–166. https://arxiv.org/abs/1505.05116v3
• A. Shapiro, On duality theory of conic linear problems, in M. A. Goberna, M. A. López (eds.), Semi-Infinite Programming, Kluwer, 2001.
• R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 2010 (Theorem 11.23(a), p. 493).
• D. P. Bertsekas, Convex Optimization Theory, Athena Scientific, 2009 (Proposition 5.5.4).
• G. Ch. Pflug, A. Pichler, Multistage Stochastic Optimization, Springer, 2014.
• G. Ch. Pflug, D. Wozabal, Ambiguity in portfolio selection, Quantitative Finance 7 (2007) 435–442.
• R. Gao, A. J. Kleywegt, Distributionally robust stochastic optimization with Wasserstein distance, arXiv:1604.02199, 2016. https://arxiv.org/abs/1604.02199
• J. Blanchet, K. Murthy, Quantifying distributional model risk via optimal transport, arXiv:1604.01446, 2016. https://arxiv.org/abs/1604.01446

Motivation

A matching in a graph is a set of edges no two of which share a vertex. Finding a matching of maximum cardinality is one of the basic problems of combinatorial optimization: it models pairing tasks (workers to shifts, kidney donors to recipients, players to rounds), it is a subroutine of algorithms for the travelling salesman and Chinese postman problems, and it was the first problem shown to need more than linear programming over the obvious constraints to be solved exactly.

For bipartite graphs, König's theorem (1931) gives a min–max formula: the maximum size of a matching equals the minimum size of a set of vertices meeting every edge. In general graphs this fails already for a triangle, where a single edge is a maximum matching but two vertices are needed to meet all three edges. Jack Edmonds' paper Paths, trees, and flowers (1965) gave both a polynomial-time algorithm for maximum matching in general graphs, the blossom algorithm, and, as a by-product of its analysis, the correct min–max theorem for general graphs.

Timeline.

• 1891: Petersen uses alternating paths to prove the existence of factors in certain graphs.
• 1947: Tutte characterizes graphs with a perfect matching.
• 1957: Berge proves that a matching is maximum if and only if there is no augmenting path, and derives the deficiency formula now called the Tutte–Berge formula (Berge 1957).
• 1965: Edmonds shrinks odd circuits ("blossoms") to search for augmenting paths in polynomial time and proves the matching-duality theorem in terms of odd-set covers (Edmonds 1965); the companion paper on the matching polyhedron extends this to weighted matching.

Setting

A graph $G$ is a finite set of vertices and a finite set of edges, each edge meeting exactly two distinct vertices, its end-points. Several edges may join the same two vertices; this is needed because shrinking creates parallel edges. A matching $M$ is a set of edges no two of which meet the same vertex; a vertex is exposed if it meets no edge of $M$. "Maximum" refers to cardinality.

An odd set is a set $U$ of vertices with an odd number of elements. Its capacity is

$$\operatorname{cap}(U) = \begin{cases} 1 & |U| = 1,\\ k & |U| = 2k+1,\ k \ge 1.\end{cases}$$

A one-vertex set covers the edges meeting its vertex; a set of $2k+1 \ge 3$ vertices covers the edges with both end-points in it. An odd-set cover is a family $\mathcal S$ of odd sets such that every edge is covered by some member, and its capacity-sum is $\operatorname{cap}(\mathcal S) = \sum_{U \in \mathcal S} \operatorname{cap}(U)$.

The proof uses the following objects of §3–§4 of the paper. An alternating path is a simple path whose edges alternate between $M$ and the non-matching edges $\bar M$. An alternating tree is a tree whose vertices are split into inner and outer vertices, every edge joining an inner to an outer vertex and every inner vertex meeting exactly two tree edges; it is planted if $M$ restricted to the tree is a maximum matching of the tree whose one exposed vertex (the root) is exposed in $G$, and Hungarian if its outer vertices are adjacent only to its inner vertices. A blossom is an odd circuit on which $M$ is a maximum matching, leaving one vertex $b$ exposed; with a stem (an alternating path from an exposed vertex ending in a matching edge at $b$) it forms a flower. Shrinking a vertex set $U$ replaces it by a single vertex $U/U$, deletes the edges inside $U$ and keeps all other edges; $G/B$ and $M/B = M \cap (G/B)$ denote the result for a blossom $B$.

Formalization targets

Goal: the matching-duality theorem (5.6, p. 462)

$$\max\{|M| : M \text{ a matching of } G\} \;=\; \min\{\operatorname{cap}(\mathcal S) : \mathcal S \text{ an odd-set cover of } G\}.$$

It is stated as: there are a maximum matching $M$ and a minimum odd-set cover $\mathcal S$ with $|M| = \operatorname{cap}(\mathcal S)$.

Milestones (attack order)

1. Weak duality: $|M| \le \operatorname{cap}(\mathcal S)$ for every matching and odd-set cover.
2. 3.7 (Berge): $M$ is not maximum iff an alternating path joins two exposed vertices.
3. 4.1–4.2: maximum matchings of an alternating tree.
4. 4.14 and 4.15: the two directions of 4.12, in stronger form.
5. 4.12: for the blossom $B$ of a flower, $M$ is maximum in $G$ iff $M/B$ is maximum in $G/B$.
6. 4.17: removing a Hungarian tree preserves maximality.
7. 5.7: the theorem for graphs with at most one exposed vertex.
8. 5.8: the configuration produced by the algorithm on a maximum matching, and the odd sets $\mathcal S_J$ it yields, which reduce the theorem to a graph with one exposed vertex fewer.

Significance

The matching-duality theorem gives a certificate of optimality: a matching and an odd-set cover of equal size prove each other optimal, and the blossom algorithm produces both. It is equivalent to the Tutte–Berge formula $\nu(G) = \min_{X} \tfrac12\bigl(|V| + |X| - \operatorname{odd}(G - X)\bigr)$, it contains König's theorem as the case where all members of the cover are singletons, and it is the cardinality case of Edmonds' description of the matching polytope by odd-set constraints, which underlies weighted matching, $b$-matching and the polyhedral approach to combinatorial optimization.

The theorem has been proved since 1965, with several independent proofs (via Tutte's theorem, via the Gallai–Edmonds decomposition, via linear programming). Mathlib contains Tutte's perfect-matching theorem for simple graphs, but neither the Tutte–Berge formula nor odd-set covers, alternating trees, blossom shrinking or Berge's augmenting-path theorem in a multigraph setting. This mission produces a machine-checked version of Edmonds' statement together with the lemmas of his algorithmic proof (4.12, 4.14, 4.15, 4.17), which are the correctness core of the blossom algorithm.

Difficulty

Weak duality and Berge's theorem are elementary. The difficulty is the strong direction. The obvious argument, a search for augmenting paths from an exposed vertex, fails because an alternating search tree in a non-bipartite graph can close an odd circuit, after which a vertex is reachable both by an even and by an odd alternating path; a naive search either misses augmenting paths or must back-track exponentially. The proof therefore has to work in shrunken graphs, whose vertices are nested sets of original vertices, and transfer maximality and covers back through every shrinking (4.12–4.15). Keeping track of nested blossoms, of the identity of edges under shrinking and of the parity bookkeeping of 5.8 is the main formal burden.

Formalization scope

• Graphs are the published EdmondsMatching65.Polyhedron.Graph V E (a map from edges to unordered pairs of distinct vertices) with finite V, E; parallel edges are allowed and loops are not. Matchings are Finset E. Maximum and minimum are by cardinality, stated with explicit comparisons rather than sSup/sInf.
• A family of odd sets is a Finset (Finset V); repeating a member only adds capacity, so this does not change the minimum. The capacity of a singleton is $1$, not $(1-1)/2$.
• Paths and circuits are lists of vertices and edges; subgraphs are vertex and edge sets; a matching of a subgraph is a matching of $G$ using only its edges.
• Shrinking is contraction along a partition of the vertices: the vertex type of $G/\mathcal P$ is the set of parts, the edge type is the set of edges not inside a part. Nested blossom shrinking is encoded by an inductive predicate of blossom sets (the complete expansions of pseudovertices), not by a tower of quotient types. Statements that shrink a set other than a circuit assume its induced subgraph connected, the standing assumption of 4.9.
• 5.7 is stated as the existence of a cover: the page's explicit families fail for the two-vertex graph with one edge and for the one-vertex graph, where the claim still holds.
• 5.8 is stated through the configuration the algorithm outputs (blossom sets, a planted Hungarian tree in $G'$, pseudovertices outer), not through the algorithm as a procedure.
• A trivializing formalization is excluded: the goal asserts the equality of the maximum and the minimum, not weak duality and not the separate existence of an optimal matching and an optimal cover.

Reusable beyond this mission: the multigraph shrinking construction, blossom sets, alternating and Hungarian trees, and Berge's theorem in the multigraph setting; these are shared with the companion mission on the invariance of the dual (Gallai–Edmonds). Proofs of any milestone, and alternative proofs of the goal (e.g. through Mathlib's Tutte theorem), are welcome.

Selected references

• J. Edmonds, Paths, trees, and flowers, Canadian Journal of Mathematics 17 (1965), 449–467. https://doi.org/10.4153/CJM-1965-045-4
• C. Berge, Two theorems in graph theory, Proceedings of the National Academy of Sciences USA 43 (1957), 842–844. https://doi.org/10.1073/pnas.43.9.842
• W. T. Tutte, The factorization of linear graphs, Journal of the London Mathematical Society 22 (1947), 107–111. https://doi.org/10.1112/jlms/s1-22.2.107
• J. Edmonds, Maximum matching and a polyhedron with 0,1-vertices, Journal of Research of the National Bureau of Standards 69B (1965), 125–130. https://doi.org/10.6028/jres.069B.013
• L. Lovász and M. D. Plummer, Matching Theory, North-Holland, 1986. https://doi.org/10.1090/chel/367

Motivation

Stochastic dual dynamic programming (SDDP), introduced by Pereira and Pinto in 1991, is the standard method for multistage stochastic linear programs with many stages, such as hydro-thermal scheduling and long-term energy planning. It approximates each stage's expected future cost from below by the maximum of finitely many linear functions (cuts), built from LP dual solutions at sampled states, and alternates a forward simulation pass with a backward cut-generation pass. Practitioners stop the method when a simulated upper bound is close to the lower bound $C^k_1$. Whether this procedure converges at all is the question of this mission.

Timeline:

• 1991: Pereira and Pinto publish SDDP, with no convergence proof.
• 1999: Chen and Powell prove almost-sure convergence for CUPPS; Linowsky and Philpott (2005) extend the argument to SDDP, AND and ReSa. Both proofs rely on an unstated independence assumption between sampled outcomes and convergent subsequences of iterates.
• 2008: Philpott and Guan (Oper. Res. Lett. 36(4), 450–455) give a proof based on the finiteness of the set of distinct cut coefficients, for a class they call DOASA (Dynamic Outer Approximation Sampling Algorithms).
• Later work (Shapiro 2011; Girardeau, Leclère and Philpott 2015) extends convergence to convex nonlinear and continuous settings.

Setting

There are $T\ge2$ stages. Stage $t$ has a decision $x_t\ge0$ in $\mathbb R^{n_t}$, costs $c_t$, a matrix $A_t$ and, for $t\le T-1$, a matrix $B_t$ coupling $x_t$ to the next stage. At stage $1$ the constraint is $A_1x_1=b_1$. For $2\le t\le T$ the right-hand side is random: $A_tx_t=\omega_t-B_{t-1}x_{t-1}$, where $\omega_t$ takes values $\omega_{t1},\dots,\omega_{tq_t}$ with probabilities $p_{ti}>0$, independently across stages. The expected cost-to-go is defined backwards from $\mathcal Q_{T+1}\equiv0$:

$$Q_t(x_{t-1},\omega_{ti})=\min\{c_t^\top x_t+\mathcal Q_{t+1}(x_t):A_tx_t=\omega_{ti}-B_{t-1}x_{t-1},\ x_t\ge0\},\qquad \mathcal Q_t=\sum_i p_{ti}Q_t(\cdot,\omega_{ti}),$$

and $Q_1=\min\{c_1^\top x_1+\mathcal Q_2(x_1):A_1x_1=b_1,x_1\ge0\}$ is the problem [LP1]. Assumption (A4) says every stage problem met along the way has a nonempty, bounded feasible region.

The approximate problem [AP$_t^k$] replaces $\mathcal Q_{t+1}$ by $\max_j\{\alpha_{t+1,j}-(\beta^j_{t+1})^\top x_t\}$ over the cuts generated before iteration $k$; its value is $C^k_t$. A scenario fixes one outcome per stage $2,\dots,T-1$. Each DOASA iteration (i) samples one forward scenario $\omega^k$ and solves [AP$_t^k$] along it, giving states $x^k_t$; (ii) for $t=T,\dots,2$ runs the Cut Calculation Algorithm (CCA): it solves [AP$_t^k$] at $x^k_{t-1}$ for the outcomes in a backward sample $\Omega^k_t$, stores optimal extreme-point dual solutions $(\pi,\rho)$ in a collection $\mathcal D_t$, picks for every outcome the best stored dual, and averages them into a new cut on $\theta_t$. DOASA-N instead traverses a fixed list of $N$ scenarios in every iteration.

Formalization targets

Goal: Theorem 4 under the joint sampling property J

If, with probability 1, every scenario prefix is followed by the forward pass jointly with each outcome being in the backward sample infinitely often (property J), then with probability 1 every DOASA run has an iteration $K$ after which the cuts no longer change, the policy $\bar x$ they induce is optimal for [LP1], and

$$C^K_1=Q_1 .$$

Milestones

• Monotonicity (p. 4): $C^{k+1}_t\ge C^k_t$ and $C^{k+1}_1\ge C^k_1$.
• Lower bound (p. 4): every cut is valid, so $C^k_t\le Q_t$ and $C^k_1\le Q_1$.
• Lemma 1 (p. 6): the set $\mathcal G^k_t$ of distinct generated cuts is bounded in size and eventually constant.
• Lemma 2 (p. 10): DOASA-N stops changing after finitely many iterations, with $\lim_kC^k_1\le Q_1$.
• Lemma 3 (p. 10): DOASA-N over all scenarios, with backward sampling infinitely often per scenario, converges almost surely to an optimal policy.

Significance

The theorem justifies SDDP, AND, ReSa and CUPPS as exact methods: on a finite scenario tree, sampling-based cutting-plane schemes reach an optimal policy and a tight lower bound after finitely many iterations, almost surely. The finiteness argument (Lemma 1) is the template for later finite-convergence proofs of SDDP variants.

The paper's proofs are informal. No part of this development is machine-checked, and the printed statement of Theorem 4 is false (see below), so a formal proof also settles exactly which sampling hypothesis is enough. The finite-cut lemma and the cut-validity milestone are reusable for any Benders-type multistage method.

Difficulty

The obvious argument goes: cut sets stabilize (Lemma 1), and every scenario and every outcome is sampled infinitely often, so the limiting cuts must be exact. The last step fails. A cut at a state is exact only if, for every outcome, a dual that is optimal at that state has been collected. Sampling the forward scenario and the backward outcomes infinitely often, but separately, does not ensure this. Lemma 1 itself is also delicate: the dual vectors $\rho$ grow in dimension with $k$, so the collection of extreme-point duals can be infinite even though the cut coefficients take finitely many values. The algorithm's choices (extreme-point duals, ties among best duals) must be handled for every run, not for a convenient one.

Formalization scope

Stages are numbered $1,\dots,T$ with variable dimensions per stage. B t is the paper's $B_t$, the matrix multiplying $x_t$ in stage $t+1$. Value functions are real infima, used only on reachable states. Iterations are numbered from $0$ in Lean. Explicit choices, each recorded in the item statements:

• The J correction. The paper states Theorem 4 under FPSP and BPSP. These do not suffice. In a three-stage instance whose last-stage backward sample is $\{c\}$ after forward outcome $a$ and $\{d\}$ after $b$, alternating, both properties hold but the cuts stabilize at a suboptimal policy with $C^k_1$ below $Q_1$. The goal is stated under J, which implies FPSP and BPSP and holds for the schemes the paper names. Lemma 3's BPSP is read per scenario of DOASA-N.
• Initial cut. The paper's trivial cut $\theta_{t+1}\ge-\infty$ makes [AP$_t^1$] unbounded; it is replaced by a finite cut $\theta_{t+1}\ge L_t$ assumed valid on reachable states. Stage $T$ uses the exact cut $\theta_{T+1}\ge0$.
• (A4) is required on reachable states only.
• The LP solver is a deterministic oracle on cut sets returning optimal solutions of [AP$_t$], so repeated cuts do not change forward solutions.
• Duals. Collected duals are optimal extreme points of the dual region; best duals are chosen with arbitrary tie-breaks. No cut is added while the dual collection is empty. Dual multipliers $\rho$ are sequences padded with zeros.
• Runs are relations covering DOASA and DOASA-N (batched forward scenarios). The conclusions hold for every run consistent with the samples, inside the almost-sure quantifier.

A trivializing encoding, in which cuts are arbitrary valid hyperplanes, duals are taken for all outcomes, or the sampling hypotheses directly assume exactness of the cuts, is ruled out: the run relation transcribes CCA steps 1–3 as printed.

A complete development needs LP weak and strong duality (published on the platform as LinearOptimization.lp_weak_duality and LinearOptimization.lp_strong_duality, in their own encoding), finiteness of the set of extreme points of a polyhedron, and the almost-sure intersection of finitely many events (Mathlib). Contributions to any milestone, to the proof that J holds for independent sampling, and to the counterexample showing FPSP and BPSP are insufficient are welcome.

Selected references

• A. B. Philpott, Z. Guan, On the convergence of stochastic dual dynamic programming and related methods, Oper. Res. Lett. 36(4) (2008) 450–455. https://doi.org/10.1016/j.orl.2008.01.013 (cited from the authors' manuscript v24, 2008-02-25)
• M. V. F. Pereira, L. M. V. G. Pinto, Multi-stage stochastic optimization applied to energy planning, Math. Program. 52 (1991) 359–375. https://doi.org/10.1007/BF01582895
• Z.-L. Chen, W. B. Powell, Convergent cutting-plane and partial-sampling algorithm for multistage stochastic linear programs with recourse, J. Optim. Theory Appl. 102 (1999) 497–524. https://doi.org/10.1023/A:1022641805263
• A. Shapiro, Analysis of stochastic dual dynamic programming method, European J. Oper. Res. 209 (2011) 63–72. https://doi.org/10.1016/j.ejor.2010.08.007
• P. Girardeau, V. Leclère, A. B. Philpott, On the convergence of decomposition methods for multistage stochastic convex programs, Math. Oper. Res. 40(1) (2015) 130–145. https://doi.org/10.1287/moor.2014.0664

Motivation

The number of successes in many rare trials is approximately Poisson. For independent trials the quality of that approximation was quantified by Le Cam in 1960: if $X_1,\dots,X_n$ are independent Bernoulli variables with $P(X_i=1)=p_i$, $W=\sum_i X_i$ and $\lambda=\sum_i p_i$, the total variation distance between the law of $W$ and the Poisson law with mean $\lambda$ is bounded by a constant multiple of $\sum_i p_i^2$, and by a constant multiple of $\lambda^{-1}\sum_i p_i^2$ when $\lambda\ge 1$. Many applications have dependent trials: occurrences of a pattern in a sequence, exceedances of a high level by a stationary process, failures in a system with local interactions. L. H. Y. Chen's 1975 paper extended Charles Stein's method of normal approximation to the Poisson case and obtained explicit bounds for dependent trials. The approach became known as the Stein–Chen method, and is now the standard tool for Poisson approximation of dependent counts.

Timeline.

• 1960. Le Cam proves the independent-trial bounds (0.1)–(0.3) of Chen's introduction.
• 1964. Kerstan extends them to independent nonnegative integer variables and improves the constant in (0.3).
• 1970. Stein introduces his method of normal approximation for dependent variables.
• 1975. Chen (Ann. Probab. 3) adapts it to Poisson approximation. He proves Theorems 4.1–4.4 for sequences satisfying Ibragimov's mixing condition, the $m$-dependent case, and a second-order expansion for independent trials.

This mission formalizes the order-$\lambda^{-1}$ bound of that paper, Theorem 4.2.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space and let $X_1,\dots,X_n$ be Bernoulli trials: random variables with values in $\{0,1\}$ and $p_i=P(X_i=1)$. Following the paper, set $X_i\equiv0$ for $i\le0$ and $i\ge n+1$. Put

$$W=\sum_{i=1}^nX_i,\qquad \lambda=\sum_{i=1}^np_i .$$

For a bounded real function $h$ on the nonnegative integers, the Poisson expectation is

$$\mathcal P_\lambda h=e^{-\lambda}\sum_{k=0}^\infty h(k)\frac{\lambda^k}{k!},$$

the mean of $h$ under the Poisson law with parameter $\lambda$. The quantity of interest is $|Eh(W)-\mathcal P_\lambda h|$ for all $h$ with $|h|\le1$. Its supremum over such $h$ is twice the total variation distance between the law of $W$ and the Poisson law.

Dependence is measured by Ibragimov's mixing condition (4.1). Let $\mathcal M_{a,b}=\sigma(X_i:a\le i\le b)$. There must be a non-increasing sequence $\varphi(k)\downarrow0$ such that for all $j,k\ge1$ and every event $B\in\mathcal M_{j+k,\infty}$,

$$|P(B\mid\mathcal M_{1j})-P(B)|\le\varphi(k)\quad\text{almost surely}.$$

A sequence is $m$-dependent when $(X_1,\dots,X_r)$ and $(X_{r+k},\dots)$ are independent for all $k>m$. It then satisfies (4.1) with $\varphi(k)=0$ for $k>m$.

The proof works with the partial sums $V^{(i)}=\sum_{|k-i|>m}X_k$, $V^{(i,j)}=\sum_{|k-i|>m,|k-j|>m}X_k$, $Y_{ij}=V^{(i)}+\sum_{k=i-m}^jX_k$ and $Y'_{ij}=V^{(i)}+\sum_{k=i-m,k\ne i}^jX_k$. It also uses the Stein solution $S_\lambda h$, the solution for $w\ge1$ of $wf(w)-\lambda f(w+1)=h(w)-\mathcal P_\lambda h$.

Formalization targets

Goal: Theorem 4.2, (4.13)

For every $m=0,1,2,\dots$ and every $h$ with $|h|\le1$,

$$|Eh(W)-\mathcal P_\lambda h|\le2\lambda^{-1}\bigl[8m+5+4(n\varphi(m+1))^{1/2}\bigr]\Bigl[\operatorname{Var}(W)-\lambda+2(2m+1)\sum_{i=1}^np_i^2\Bigr]+32\bigl[6m+3+(n\varphi(m+1))^{1/2}\bigr]n\varphi(m+1).$$

The bound involves only the law of $W$ through $\operatorname{Var}(W)$, the success probabilities, the window $m$ and the mixing rate. The window $m$ is free, so the statement covers every trade-off between local dependence and mixing.

Consequences (companion items)

• Theorem 4.3, (4.21). For $m$-dependent trials, $|Eh(W)-\mathcal P_\lambda h|\le2(8m+5)\lambda^{-1}\bigl[\sum\sum_{i\ne j}\operatorname{Cov}(X_i,X_j)+(4m+1)\sum p_i^2\bigr]$.
• Corollary 4.1, (4.23). For independent trials, $|Eh(W)-\mathcal P_\lambda h|\le10\lambda^{-1}\sum p_i^2$. This improves Le Cam's (0.3).
• Theorem 4.4. For identically distributed trials with $\varphi(m)=e^{-\alpha m}$, there are bounds (4.24) and (4.25) whose constants depend only on $\alpha$.

Milestones

The milestones follow the paper's proof:

• the basic identity (2.2), the Stein solution (2.5) and the expansion (2.6);
• the bounds on $S_\lambda h$: Lemmas 3.1–3.3, (3.6) and Lemma 3.5;
• the mixing inequalities, Lemmas 4.1–4.3 and 4.6;
• the variance bound, Lemma 4.4;
• the four displays (4.14) and (4.16)–(4.19) of the proof of Theorem 4.2;
• Cauchy–Schwarz (4.10) and Lemma 4.5.

Significance

Theorem 4.2 gives an error of order $\lambda^{-1}$ times the excess variance $\operatorname{Var}(W)-\lambda+O(m\sum p_i^2)$, plus a mixing remainder. When the trials are nearly uncorrelated, $\operatorname{Var}(W)\approx\lambda$ and the bound is small even though $\lambda$ is large. This is the regime where the companion Theorem 4.1, which carries a factor $\min(\lambda^{-1/2},1)$, is weaker. The independent case recovers Le Cam's order $\lambda^{-1}\sum p_i^2$ with constant 10. The $m$-dependent case gives explicit Poisson limit theorems for scan statistics and pattern counts.

All results of the paper are proved there, and the proofs are elementary apart from the measure theory of Lemma 4.1. To our knowledge none of them has a machine-checked proof. Mathlib has the Poisson distribution and conditional expectation, but no Stein–Chen bound and no mixing inequality of Ibragimov's type. A formal proof would give the first checked quantitative Poisson approximation for dependent trials. It would also give reusable covariance inequalities for $\varphi$-mixing sequences (Lemmas 4.2 and 4.3).

Difficulty

Most of the work is bookkeeping, and it is heavy. Identity (2.2) needs a telescoping over windows $[i-m,j]$ whose ends can fall outside $[1,n]$. (4.15)–(4.18) need $|Y'_{i,j-1}+1-\lambda|$ to be compared with $|V^{(i,j)}-EV^{(i,j)}|$ with explicit constants.

The genuinely probabilistic step is the decoupling of Lemma 4.2. Condition (4.1) controls conditional probabilities of events. Lemma 4.2 needs a bound on conditional expectations of functions of a whole random vector. Passing from one to the other requires a regular conditional distribution that is uniformly close to the unconditional law on a set of full measure (Lemma 4.1). The naive route, applying (4.1) to each level set of a simple function, loses a factor that grows with the number of levels and does not give the constant $2\|f\|$.

The bound (4.16) applies Lemma 4.4 to a subsequence of the trials. This uses the fact that dropping variables preserves (4.1) with the same $\varphi$, because $\varphi$ is non-increasing.

Formalization scope

• Trials. The trials are a map $X:\mathbb N\to\Omega\to\mathbb N$ that is measurable, vanishes at index $0$ and above $n$, and is at most $1$ almost surely. The constant padding adds nothing to any $\sigma$-algebra, so (4.1), $m$-dependence and independence of the padded sequence are those of $X_1,\dots,X_n$.
• Probabilities and moments. $p_i$ is defined as $P(X_i=1)$, not taken as a parameter. $\operatorname{Var}$ and $\operatorname{Cov}$ are Mathlib's. All integrands are almost surely bounded, so no integrability hypotheses are needed.
• Norms. Sup norms are replaced by bounds $M$ with $|h|\le M$. $\|S_\lambda h\|$ ranges over $w\ge1$.
• Mixing condition. In (4.1) the conditional probability is the conditional expectation of the indicator, and lags are $k\ge1$.
• Added hypotheses. The §3 lemmas and (2.6), (4.14) assume $\lambda>0$, because they divide by $\lambda$. The goal and the companions do not assume it: at $\lambda=0$ all $p_i$ vanish, $W=0$ almost surely, and both sides are $0$ under Lean's convention $0^{-1}=0$.
• Lemmas 4.2 and 4.3. They are stated for an arbitrary measurable real sequence satisfying (4.1), as on the page. The independent copy $Z'$ is expressed through the law of $Z$.
• Theorem 4.4. Its constants are quantified before the probability space, $n$ and the trials. This is what "depend only on $\alpha$" means.

A trivializing formalization is ruled out. Measurability of the trials is part of the definition, because otherwise conditional expectations in (4.1) collapse to $0$. The goal mentions only $W$, $\lambda$, $p_i$, $\operatorname{Var}(W)$, $\varphi$, $m$ and $h$. It does not mention $S_\lambda h$ or any milestone quantity.

A complete development needs the Stein solution and its bounds, a Bernoulli-sum calculus over integer windows, regular conditional distributions on standard Borel spaces, and the mixing covariance inequalities. The last two are reusable beyond this mission. Contributions to any milestone are welcome, as are alternative proofs of Lemma 4.2 through Mathlib's condDistrib.

Selected references

• L. H. Y. Chen, Poisson approximation for dependent trials, Annals of Probability 3(3):534–545, 1975. https://doi.org/10.1214/aop/1176996359
• L. Le Cam, An approximation theorem for the Poisson binomial distribution, Pacific Journal of Mathematics 10(4):1181–1197, 1960. https://doi.org/10.2140/pjm.1960.10.1181
• C. Stein, A bound for the error in the normal approximation to the distribution of a sum of dependent random variables, Proc. Sixth Berkeley Symp. Math. Statist. Probab. 2:583–602, 1972. https://projecteuclid.org/euclid.bsmsp/1200514239
• I. A. Ibragimov, Some limit theorems for stationary processes, Theory of Probability and its Applications 7(4):349–382, 1962. https://doi.org/10.1137/1107036
• A. D. Barbour, L. Holst, S. Janson, Poisson Approximation, Oxford University Press, 1992. ISBN 978-0-19-852235-9

Motivation

Sampling uniformly from a bounded region can be difficult when direct transformation of a familiar random variable is unavailable and rejection sampling spends most of its trials outside the region. Robert L. Smith studied procedures that move within the region: from the current point, choose a direction, form the line set through that point inside the region, and choose the next point uniformly on that line set. The resulting sequence is a homogeneous Markov chain. The Random Directions Algorithm, later commonly called hit-and-run, is a central instance of this construction. Smith's 1984 paper establishes conditions under which the chain approaches the uniform distribution even when its initial point is fixed rather than sampled uniformly (Smith 1984, pp. 1298–1301).

For simulation, the initial point is usually chosen because it is known to be feasible. The question is therefore whether the distribution after many moves forgets that particular choice. A stationary distribution alone does not answer this: stationarity describes what happens if the chain already starts with that distribution. Smith's Theorem 2 gives the stronger, pointwise starting-state statement for the class of symmetric mixing algorithms satisfying his two regularity assumptions (Smith 1984, p. 1301).

Setting

Let $S$ be the state region and $V$ its finite, nonzero content measure. In Smith's geometric setting, $S$ is a bounded $k$-dimensional measurable region in $\mathbb R^n$, and $V$ is $k$-dimensional content; at $k=0$, content is counting measure. A Markov transition kernel $P$ assigns to every current point $x\in S$ a probability $P(x,A)$ of entering a measurable set $A\subseteq S$ on the next move. For the associated chain $(X_0,X_1,\ldots)$, the $m$-step transition probability is $P^m(x,A)=\mathbb P(X_m\in A\mid X_0=x)$.

The uniform law is $\lambda(A)=V(A)/V(S)$. Smith's Assumption (a) gives a measurable transition density $f(y\mid x)$ relative to $V$:

$$P(x,A)=\int_A f(y\mid x)\,V(dy).$$

For a symmetric mixing algorithm, the paper states that this density satisfies $f(y\mid x)=f(x\mid y)$ for all $x,y\in S$. Assumption (b) says $f(y\mid x)>0$ for all such pairs. These are pointwise conditions, including states of zero $V$-measure. A nonempty measurable set $A$ is closed if $P(x,A)=1$ for every $x\in A$. The chain is indecomposable in the paper's sense when it has no two disjoint closed sets (Smith 1984, pp. 1299–1300).

Formalization targets

Stationarity and indecomposability

Lemma 1 asserts that $\lambda$ is stationary: $\lambda(A)=\int_S P(x,A)\,\lambda(dx)$ for every measurable $A$. Lemma 2 excludes two disjoint closed sets. Both are direct prerequisites of the goal. Smith's Theorem 1 also establishes uniqueness of the stationary distribution and almost-sure convergence of empirical visit frequencies under a stationary start; it is described in the source, but its trajectory-level formalization is outside this proposal (Smith 1984, p. 1300).

Convergence from every starting point

The mission goal is Smith's Theorem 2. For every $x\in S$ and every measurable $A\subseteq S$,

$$\lim_{m\to\infty}P^m(x,A)=\lambda(A).$$

This is the paper's explicit meaning of strongly mixing. The milestone list also records the proof's stated nonperiodicity condition: for every $n\ge2$, the $n$-step transition law has no two disjoint closed sets. It is a target in its own right because it concerns all higher-step kernels, not only the one-step chain (Smith 1984, p. 1301).

Significance

Theorem 2 makes the uniform law the limiting distribution of the sample at time $m$, for any fixed feasible initial point. The paper's Theorem 1 supplies a different guarantee about long-run empirical frequencies under a stationary start, although it is not a target of this proposal. Smith later specializes the framework to the Random Directions Algorithm and gives a quantitative rate under additional geometric conditions; that rate is the subject of the companion mission (Smith 1984, pp. 1303–1304).

These results are proved in the paper but the declarations in this proposal are theorem statements with sorry, not machine-checked proofs. A completed formalization would turn the paper's measure-theoretic claims into reusable statements about general measurable state spaces and kernels. The normalized content law, the density interface, and closed-set predicate can be reused when studying other Monte Carlo kernels with the same hypotheses.

Difficulty

The main obstacle is the jump from stationary behavior to convergence from every starting point. Symmetry identifies the candidate stationary law, and strict positivity limits how the chain can split into closed parts, but neither sentence by itself establishes the claimed limit of $P^m(x,A)$. The distinction matters especially at starting points in $V$-null sets: an almost-everywhere starting-state result would leave out precisely the universal claim in Theorem 2. The paper appeals to a general-state Markov-chain convergence result for this step (Smith 1984, p. 1301).

Formalization scope

Lean uses a measurable type $\alpha$ as the whole region $S$, a finite measure $V$ with $V(S)\ne0$, a Markov kernel $P$, and an extended-nonnegative density $f:\alpha\to\alpha\to\mathbb R_{\ge0}^{\infty}$. The density is jointly measurable and is linked to $P$ by the integral identity above; symmetry is pointwise, and positivity is added only for Lemma 2 and Theorems 1–2. This abstract representation retains the hypotheses those results use without fixing a particular Euclidean dimension. It covers the counting-content case as well as continuous content, although it does not construct the geometric direction-and-chord algorithm. The Random Directions kernel belongs to the companion mission.

The uniform law is normalized by $V(S)$. Finiteness and nonzero total content prevent a meaningless inverse or an empty probability space. The $m$-step law is the published MarkovChainCLT.iterKernel. Theorem 2 quantifies over every $x$, rather than $\lambda$-almost every $x$, and uses setwise convergence on each measurable $A$. No invariance, uniqueness, minorization, or convergence premise is added to the goal. Detaching $f$ from $P$ would empty out the substantive assertion. Formal contributions can target the density-to-invariance argument, the closed-set conditions, and the general-state convergence theorem needed for the goal. The paper's separate pathwise Theorem 1 remains an appropriate later extension.

Selected references

• Robert L. Smith, Efficient Monte Carlo Procedures for Generating Points Uniformly Distributed over Bounded Regions, Operations Research 32(6), 1296–1308, 1984. DOI: 10.1287/opre.32.6.1296.

Motivation

A seller with one indivisible object must decide whether to keep it or transfer it to one of several bidders whose values she does not observe. The allocation and the payment rule affect what bidders choose to report. Myerson's 1981 paper identifies a revenue-maximizing rule when bidders' private value estimates are independent, their densities are positive, and their valuations may be revised after learning other bidders' information. It covers value distributions for which the usual virtual-value rule is not monotone, by replacing each bidder's virtual value with an ironed priority level.

The question matters to auction design because a pointwise revenue-maximizing assignment can reward a bidder for understating a value. The seller must maximize expected utility subject to both incentive compatibility and each bidder's ability to decline participation. The paper's main theorem gives a specific allocation and payment pair that meets those constraints and attains the maximum. The result is proved in the source; this mission asks for a machine-checked formalization of it.

Setting

There is a finite nonempty set $N$ of bidders and one seller. Bidder $i$ has a value estimate $t_i$ in a finite interval $[a_i,b_i]$, where $a_i<b_i$; endpoints may be negative and may differ between bidders. The continuous density $f_i$ is strictly positive on that interval and has total integral one. The bidders' estimates are independent, so a profile $t=(t_i)_{i\in N}$ has density $f(t)=\prod_i f_i(t_i)$ on $T=\prod_i[a_i,b_i]$. Write $F_i(s)=\int_{a_i}^{s}f_i(u)\,du$ for the distribution function. The seller's known value for keeping the object is $t_0$.

A revision effect $e_j(t_j)$ describes the change in everyone else's valuation after bidder $j$'s estimate becomes known. Bidder $i$'s revised value is $v_i(t)=t_i+\sum_{j\ne i}e_j(t_j)$, while the seller's is $v_0(t)=t_0+\sum_j e_j(t_j)$. A direct mechanism assigns each profile an allocation probability $p_i(t)$ and expected payment $x_i(t)$ for each bidder. Payments may be negative and need not vanish when a bidder loses. Its feasibility conditions say that allocation probabilities are nonnegative and sum to at most one, each bidder's interim expected utility is nonnegative at every possible value, and truthful reporting yields at least as much interim utility as any other report. The seller maximizes her expected utility over all feasible mechanisms.

The virtual value is $c_i(s)=s-e_i(s)-(1-F_i(s))/f_i(s)$. In the general case it need not increase with $s$. Myerson transforms $c_i$ through the quantile $q=F_i(s)$: $h_i(q)=c_i(F_i^{-1}(q))$, $H_i(q)=\int_0^q h_i(r)\,dr$, and $G_i$ is the convex envelope of $H_i$ on $[0,1]$. The slope $g_i$ of $G_i$, extended across kinks, gives the ironed priority $\bar c_i(s)=g_i(F_i(s))$. At profile $t$, the winning set $M(t)$ contains exactly those bidders whose priority is maximal and at least $t_0$.

Formalization targets

The goal is Myerson's §6 theorem. The proposed rule shares the object equally among bidders in $M(t)$, or keeps it when $M(t)$ is empty, and charges each bidder the envelope payment:

$$\bar p_i(t)=\begin{cases}|M(t)|^{-1},&i\in M(t),\\0,&i\notin M(t),\end{cases} \qquad \bar x_i(t)=\bar p_i(t)v_i(t)-\int_{a_i}^{t_i}\bar p_i(t_{-i},s)\,ds.$$

The target asserts that $(\bar p,\bar x)$ is feasible and that every feasible $(p,x)$ has seller utility no greater than that of $(\bar p,\bar x)$. The milestone list follows the paper's reduction: Lemma 2 characterizes feasible direct mechanisms by a monotone interim allocation rule and an envelope identity; equation (4.12) rewrites seller utility using virtual values; Lemma 3 turns maximization of virtual surplus into optimality. Equations (6.9)–(6.13) compare virtual and ironed priorities and establish the optimality and monotonicity of the proposed allocation.

Significance

The theorem specifies both who receives the object and how payments are computed, including irregular distributions and bidder-specific supports. The ironed priorities preserve incentives while retaining the seller's maximal expected utility. Equation (4.12) also gives the revenue-equivalence consequence: once the allocation rule and each lowest-type interim utility are fixed, expected seller utility is fixed.

A formal proof would connect several reusable results: product distributions with bidder-specific densities, interim incentive constraints, an envelope characterization, virtual-surplus accounting, and one-dimensional convex ironing. The source theorem and milestones are currently statements to be proved in this development, not existing machine-checked results. Related Börgers auction statements on Prove2Me use a common nonnegative support, at least two bidders, zero revision effects, and zero seller value; they do not provide this general theorem.

Difficulty

Maximizing virtual surplus at each profile is straightforward only if each bidder's virtual value rises with her report. When it falls, the resulting win probability can also fall, violating the incentive constraint. Replacing virtual values by slopes of a convex envelope restores monotonicity, but then the proof must account exactly for the difference between the original and ironed objectives, including flat portions of the envelope. Payments must satisfy the interim envelope identity for every type, while the seller's objective includes both transfers and her value for retaining the object.

Formalization scope

The Lean model uses a finite nonempty bidder type, real-valued reports and payments, one object, independent continuous positive densities normalized on each finite support, and continuous revision effects. The latter regularity is implicit in the paper's assertion that $c_i$ is continuous. No mean-zero condition on revision effects is imposed: the paper explicitly says its equation (2.9) is unnecessary. One bidder, negative support endpoints, unequal supports, and arbitrary seller value remain allowed.

The profile law is Lebesgue measure restricted to $T$ and weighted by the product density. Integrating a function after replacing coordinate $i$ represents the $T_{-i}$ integral, because bidder $i$'s marginal density has mass one. Mechanisms are total functions, but allocation and incentive conditions quantify over supported profiles and reports. Feasibility explicitly requires integrability of allocations, payments, and their report sections so no undefined Bochner expectation can acquire Lean's default value zero. The convex envelope is the two-point infimum of equation (6.3); its defining set is nonempty and bounded below on $[0,1]$. The slope uses the right derivative below quantile one and the left derivative at one. The theorem requires feasibility of the proposed pair as well as its utility bound, ruling out an empty or unconstrained maximization claim.

The Stieltjes expressions in (6.9), (6.12), and (6.13) are combined into equivalent ordinary-integral comparisons over the profile law. A complete proof needs the one-dimensional envelope theorem, product-measure integration and Fubini results, differentiation of the convex envelope, and a careful endpoint treatment. The definitions of interim utilities and ironing can be reused for related auction models; contributions that establish these analytic components or the listed source lemmas are in scope.

Selected references

• Roger B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1):58–73, 1981. DOI: 10.1287/moor.6.1.58.

Motivation

The number of successes in many rare, roughly independent trials is approximately Poisson. This law of small numbers is used for counts of rare events in reliability, insurance, epidemiology, queueing and random combinatorics. A quantitative version says how large the error is. For independent Bernoulli trials with success probabilities $p_1,\dots,p_n$ and $\lambda=\sum p_i$, Le Cam (1960) showed that the error in total variation is of order $\sum p_i^2$. When all $p_i$ are small this tends to zero, but it does not say what the leading part of the error is.

L. H. Y. Chen's 1975 paper (Ann. Probab. 3, 534–545) adapted Charles Stein's method for normal approximation to the Poisson case. The result is now called the Stein–Chen method. The paper's §2–§4 give first-order error bounds for dependent (mixing) trials. Its §5, "A refinement", goes one order further for independent trials. It identifies the first-order correction explicitly and shows that what remains is of order $\lambda^{-1}\sum p_i^3$. Kerstan (1964) had obtained a similar expansion by a different method. Chen's version comes from iterating the basic identity of the Stein–Chen method. This mission formalizes §5.

Timeline:

• 1953: Prohorov bounds the distance between the binomial and the Poisson law.
• 1960: Le Cam proves the $\sum p_i^2$ bound for independent, non-identical trials. Hodges and Le Cam give a short proof.
• 1964: Kerstan gives a refinement of the Prohorov–Le Cam bounds.
• 1975: Chen introduces the Stein–Chen method. It gives first-order bounds under Ibragimov's mixing condition and the second-order expansion (Theorem 5.1) for independent trials.

Setting

Let $X_1,\dots,X_n$ be independent random variables on a probability space, each taking only the values $0$ and $1$, with success probabilities $p_i=P(X_i=1)$. Put

$$W=\sum_{i=1}^nX_i,\qquad\lambda=\sum_{i=1}^np_i,\qquad W^{(i)}=\sum_{k\ne i}X_k,\qquad\lambda^{(i)}=\sum_{j\ne i}p_j .$$

For a bounded real function $h$ on the nonnegative integers, the Poisson expectation is

$$\mathscr P_\lambda h=e^{-\lambda}\sum_{k=0}^\infty h(k)\frac{\lambda^k}{k!},$$

the mean of $h$ under the Poisson law with parameter $\lambda$. The Stein equation is $wf(w)-\lambda f(w+1)=h(w)-\mathscr P_\lambda h$. For $w\ge1$ its solution is

$$S_\lambda h(w)=-(w-1)!\,\lambda^{-w}\sum_{k=0}^{w-1}\bigl[h(k)-\mathscr P_\lambda h\bigr]\frac{\lambda^k}{k!}.$$

Write $\Delta f(w)=f(w+1)-f(w)$ and $Lf(w)=f(w+1)$. Chen's second-order operator is

$$U_\lambda h(w)=\Delta S_\lambda h(w+1)=S_\lambda h(w+2)-S_\lambda h(w+1),\qquad w\ge0 .$$

For another parameter $b>0$, $S_bU_\lambda h$ and $U_bU_\lambda h$ apply the Stein solution and the operator with parameter $b$ to the function $U_\lambda h$.

In Lean: poissonExp, stein, delta, shiftL, stU, prob, lam, lamExcept, W, Wi, all in the namespace PoissonDepTrials.SecondOrder.

Formalization targets

Goal: Theorem 5.1, (5.7)

If $X_1,\dots,X_n$ are independent, $n\ge2$ and $\bar p=\max_ip_i\le\lambda/2$, then for every $h$ with $|h|\le1$,

$$\Bigl|Eh(W)-\mathscr P_\lambda h+\Bigl(\sum_{i=1}^np_i^2\Bigr)\mathscr P_\lambda U_\lambda h\Bigr|\le\bigl(24+96\sqrt2\bigr)\lambda^{-1}\sum_{i=1}^np_i^3 .$$

The paper writes the constant as "an absolute constant $C$ not greater than $24+96(2)^{1/2}$". The formal goal fixes $C$ at that value, which is the same statement.

Milestones

In order: the Stein solution (2.3)/(2.5); the difference identity (3.6); Lemmas 3.1, 3.2, 3.3 and 3.5 (bounds on $S_\lambda h$ and $\Delta S_\lambda h$); the first-order identity (5.8) $Eh(W)=\mathscr P_\lambda h-\sum_ip_i^2EU_\lambda h(W^{(i)})$; Lemmas 5.1 and 5.2 (dependence of Poisson expectations on the parameter); Lemmas 5.3–5.5 (bounds on $\mathscr P_b|L^mU_\lambda h|$, $S_bU_\lambda h$ and $U_bU_\lambda h$); the bound (5.9),

$$\Bigl|Eh(W)-\mathscr P_\lambda h+\Bigl(\sum p_i^2\Bigr)\mathscr P_\lambda U_\lambda h\Bigr|\le24\lambda^{-1}\sum_ip_i^3+96\lambda^{-1}\sum_i\sum_{j\ne i}\frac{p_i^2p_j^2}{\lambda^{(i)}};$$

and the closing inequality $\lambda^{-1}\sum_ip_i^2\sum_{j\ne i}p_j^2/\lambda^{(i)}\le\sqrt2\,\lambda^{-1}\sum_ip_i^3$.

Significance

The theorem gives an explicit first correction to the Poisson approximation of a Poisson-binomial law, with a remainder of the next order. When all $p_i$ equal $p$, the first-order error $\sum p_i^2=\lambda p$ is replaced by the remainder $\lambda^{-1}\sum p_i^3=p^2$, which is smaller by the factor $\lambda$. The correction term is a functional of the Poisson law alone, $-(\sum p_i^2)\mathscr P_\lambda U_\lambda h$. It can be evaluated without knowing the distribution of $W$. The method of proof applies the basic identity twice. The paper notes that further iteration gives expansions to any order.

On the formal side, Mathlib has the Poisson distribution but no Stein–Chen machinery and no quantitative Poisson approximation. The theorem has, as far as is known, no machine-checked proof. This mission produces the Stein solution and its standard bounds (Lemmas 3.1–3.5), which are reusable by any Stein–Chen argument. It also produces the parameter-perturbation estimates of Lemmas 5.1–5.2 and a complete second-order expansion. Missions 1 and 2 of this series formalize the first-order bounds of §4 under a mixing condition. They share the Stein-solution layer.

Difficulty

The first-order bound needs only that $\Delta S_\lambda h$ is uniformly small (Lemma 3.4). A second-order bound needs more. After the first application of the identity, the error $\sum p_i^2EU_\lambda h(W^{(i)})$ has to be expanded again. That requires control of the iterated operator $U_bU_\lambda h$ with a different parameter $b=\lambda^{(i)}$, because $W^{(i)}$ is approximately Poisson with mean $\lambda^{(i)}$, not $\lambda$. The bound on $U_bU_\lambda h$ (Lemma 5.5) grows linearly in $|w-\lambda|$. Applying the uniform bounds of §3 throughout loses a factor $\lambda^{1/2}$ and produces an error of order $\lambda^{-1/2}\sum p_i^3$ instead of $\lambda^{-1}\sum p_i^3$. The linear growth has to be paired with the variance of $W^{(i,j)}$. The averaging over pairs $(i,j)$ in the final step uses the condition $\bar p\le\lambda/2$, which keeps every $\lambda^{(i)}$ comparable to $\lambda$.

Formalization scope

Conventions committed to in Lean:

• The trials are a sequence X : ℕ → Ω → ℕ. Each $X_i$ is measurable with values in $\{0,1\}$ almost surely. $X_i\equiv0$ for $i=0$ and $i>n$, which is the paper's own padding convention (p. 535). Independence is iIndepFun (fun i => X i) P over all of ℕ. Because the padding variables are constants, this is equivalent to independence of $X_1,\dots,X_n$.
• $p_i$ is defined from $X$, not taken as a parameter.
• $\|h\|$ is replaced by an arbitrary bound $M$ with $|h(k)|\le M$ for all $k$. The norm of $S_\lambda h$ is taken over its domain $w\ge1$.
• $\bar p\le\lambda/2$ is written as $p_i\le\lambda/2$ for every $i\in\{1,\dots,n\}$.
• The goal assumes neither $\lambda>0$ nor integrability. Every function involved is bounded, so every expectation and Poisson sum is genuine. At $\lambda=0$ both sides of (5.7) vanish.

Hypotheses added relative to the page, each disclosed in the item's Formalization Note:

• $\lambda>0$ in the §3 and §5 lemmas, in (5.8) and in (5.9). These divide by $\lambda$, by $b$ or by $\lambda^{(i)}$.
• $b>0$ in Lemmas 5.3–5.5, which is the standing range of §5.
• Boundedness of $f$ in Lemma 5.2. The lemma is only applied to bounded functions.

The random indices $I,J$ that the paper introduces to shorten notation in (5.8)–(5.9) are not formalized. The same quantities are written as finite sums over indices.

Ruled out: the second-order term must be the operator $U_\lambda h=\Delta S_\lambda h(\cdot+1)$ built from the Stein solution exactly as on p. 543. A free function, or $U_\lambda h$ evaluated at the junk value $S_\lambda h(0)$, would empty the theorem.

Welcome contributions include:

• the Stein-solution bounds of §3, which are reusable well beyond this paper;
• Poisson-sum manipulations (Lemmas 5.1–5.2);
• the independence bookkeeping that turns (2.6) into (5.8).

Selected references

• L. H. Y. Chen, Poisson approximation for dependent trials, Ann. Probab. 3(3):534–545, 1975. https://doi.org/10.1214/aop/1176996359
• L. Le Cam, An approximation theorem for the Poisson binomial distribution, Pacific J. Math. 10:1181–1197, 1960. https://doi.org/10.2140/pjm.1960.10.1181
• J. L. Hodges and L. Le Cam, The Poisson approximation to the Poisson binomial distribution, Ann. Math. Statist. 31:737–740, 1960. https://doi.org/10.1214/aoms/1177705799
• J. Kerstan, Verallgemeinerung eines Satzes von Prochorow und Le Cam, Z. Wahrscheinlichkeitstheorie verw. Gebiete 2:173–179, 1964. https://doi.org/10.1007/BF00533419
• C. Stein, A bound for the error in the normal approximation to the distribution of a sum of dependent random variables, Proc. Sixth Berkeley Symp. Math. Statist. Prob. 2, 1972. https://projecteuclid.org/euclid.bsmsp/1200514239