Operations Research

Log-concave functions are the meeting point of convex analysis and probability: densities of Gaussian, exponential, uniform and Wishart distributions are all log-concave, and countless facts of applied probability flow from one structural theorem — integrating out variables preserves log-concavity. This mission builds the convex-analysis spine of Boyd & Vandenberghe's Convex Optimization (Chapters 2–3) — separation and supporting hyperplanes, dual cones, the first- and second-order differential characterizations of convexity, Fenchel conjugacy — and climbs to Prékopa's theorem via the Prékopa–Leindler inequality, a landmark of Brunn–Minkowski theory absent from Mathlib.

Value decomposition — approximating the value of a joint state by a sum of per-agent local values — is a staple of multi-agent dynamic programming and reinforcement learning, from index policies for restless bandits to modern MARL architectures, yet it is normally used without justification. Chen and Peng (arXiv:2506.02385) supply one. They show a multi-agent MDP admits an exact value decomposition precisely when its transition matrix is not entangled — a notion built in direct analogy with quantum entanglement — and then turn that qualitative characterisation into a quantitative one: a measure of Markov entanglement bounds the decomposition error in general. This mission formalizes that core theory. The goal is Theorem 6, the general N-agent bound in the occupancy-weighted norm; the milestones are the equivalence between separability and exact decomposition, the perturbation machinery that carries a one-step transition error into a value-function error, and the extensions to shared global state and shared rewards. The paper's restless-bandit application, which needs mean-field machinery of its own, is left to a second mission in the series.

How much flow can be sent from a source $s$ to a sink $t$ through a network with arc capacities $u_{ij}\in(0,\infty]$ — and what certifies that no more is possible? This mission formalizes §7.4-7.5 of Bertsimas & Tsitsiklis. The circulation calculus of §7.4 supplies the two structural tools: the flow decomposition theorem (Lemma 7.1 — every nonzero nonnegative circulation is a positive combination $\mathbf{f}=\sum_i a_i\mathbf{f}^i$ of simple circulations with only forward arcs, with integer $a_i$ when $\mathbf{f}$ is integer) and the optimality criterion for the minimum cost network flow problem (Theorem 7.6 — a feasible flow is optimal if and only if there is no unsaturated cycle with negative cost). Section 7.5 then formulates the maximum flow problem ($\max b_s$ s.t. $\mathbf{A}\mathbf{f}=\mathbf{b}$, $b_t=-b_s$, $b_i=0$ for $i\ne s,t$, $0\le\mathbf{f}\le\mathbf{u}$), defines augmenting paths (Definition 7.2: $f_{ij}<u_{ij}$ on forward arcs, $f_{ij}>0$ on backward arcs) and the Ford–Fulkerson algorithm, and proves integer invariance and finite termination for integer capacities (Theorem 7.8). The goal is Theorem 7.10:

(a) if the Ford–Fulkerson algorithm terminates because no augmenting path can be found, the current flow is optimal;

(b) the value of the maximum flow equals the minimum cut capacity

— the archetypal combinatorial min-max theorem, which the book notes can also be read as LP duality (pp. 311-312).

Sometimes reward during learning is irrelevant — a pharmaceutical company running phase-II trials only cares about identifying the best treatment, as quickly and as reliably as possible. Chapter 33 of Lattimore–Szepesvári formalizes fixed-confidence best-arm identification: a policy together with a stopping time $\tau$ and a recommendation must be sound (wrong with probability at most $\delta$) while minimizing $\mathbb{E}[\tau]$. The information-theoretic complexity is $c^*(\nu)^{-1} = \sup_{\alpha\in\mathcal{P}_{k-1}} \inf_{\nu'\in\mathcal{E}_{alt}(\nu)} \sum_i \alpha_i D(\nu_i, \nu_i')$: every sound strategy needs $\mathbb{E}[\tau] \ge c^*(\nu)\log\frac{1}{4\delta}$, and the Track-and-Stop algorithm — the goal theorem — achieves $\lim_{\delta\to 0} \mathbb{E}[\tau]/\log(1/\delta) = c^*(\nu)$ exactly. The mission also covers the fixed-budget counterpart, sequential halving.

When rewards are binary — a click or no click, a cure or no cure — the subgaussian machinery of Missions I–III is not tight: the variance of a Bernoulli arm degrades near the boundary of $[0,1]$, and the correct exponential rate is governed by the binary relative entropy $d(p,q) = p\log\frac{p}{q} + (1-p)\log\frac{1-p}{1-q}$ rather than a squared distance. Chapter 10 of Lattimore–Szepesvári develops Chernoff's tail bound in its information-theoretic form and the KL-UCB algorithm, whose upper confidence bounds are level sets of $d$. The goal theorem shows KL-UCB attains

— asymptotic optimality with exactly the constant demanded by the lower bound of Mission VII, strictly improving subgaussian UCB on every Bernoulli instance.

Every lower bound in bandit theory rests on one question: how hard is it to tell two probability measures apart from a sample? The answer is quantified by the relative entropy $D(P,Q)$, and the sharpest elementary tool is the Bretagnolle–Huber inequality: for any event $A$, $P(A) + Q(A^c) \ge \frac{1}{2}\exp(-D(P,Q))$ — no test can distinguish $P$ from $Q$ with total error probability below $\frac{1}{2}e^{-D(P,Q)}$. This mission formalizes Chapter 14 of Lattimore–Szepesvári: the Bretagnolle–Huber inequality (the goal theorem, proved via Le Cam's inequality $\int p \wedge q \ge \frac{1}{2}(\int\sqrt{pq})^2$), Pinsker's inequality $\delta(P,Q) \le \sqrt{D(P,Q)/2}$, and the closed-form divergences between Gaussians and Bernoullis. These half-page inequalities power every impossibility result in Missions VII, XI and beyond.

Why the two-item periodic JRP is hard

The joint replenishment problem (JRP) is the multi-item extension of the economic order quantity (EOQ) model. Each item is reordered periodically and pays its own ordering and holding costs, and a joint ordering cost is shared by items ordered at the same time. Before this work no hardness result was known for the periodic JRP (p. 10), even though no exact polynomial-time algorithm was known either (Schulz and Telha, arXiv:2007.09045; Operations Research, 2024, as Integer Factorization: Why Two-Item Joint Replenishment Is Hard).

The paper explains this through number theory. In the periodic JRP the joint cost is incurred every $\gcd(q_1, q_2)$ periods, so the objective contains a greatest common divisor of the decision variables. The paper's Theorem 2 states that, assuming the Riemann hypothesis, the two-item periodic JRP is NP-hard under randomized reductions. The proof composes two reductions:

• Shor's reduction from Partition to RangeDivisor ("does $M$ have a divisor in $[L, U]$?"), given in the paper's appendix and based on Shor (2011); this is where the Riemann hypothesis enters;
• a reduction from RangeDivisor to the two-item periodic JRP, whose correctness is Lemma 3 (pp. 13–14).

This mission formalizes Lemma 3. Mission 4 of this series formalizes the Partition half; missions 1 and 2 formalize the integer-factorization reductions behind Theorem 1.

Setting

A period is a positive integer $q$. An item with ordering cost $K$ and holding cost $H$ costs

per unit time. The two-item periodic JRP (objective (3), p. 10) minimizes, over $q_1, q_2 \in \mathbb{Z}_+$,

As a decision problem (p. 13), it asks whether some $(q_1, q_2)$ has cost at most a threshold $z$.

An instance of RangeDivisor (p. 12) is a triple of integers $M \ge U \ge L > 0$ satisfying

it is a yes-instance when $M$ has a divisor $q$ with $L \le q \le U$.

Given such a triple, the instance $\mathrm{JRP}_{M,U,L}$ sets

and the threshold is $z_{M,L,U} = L + U + 2M^2(M+1)$, where $2M^2(M+1) = \mathrm{EOQ}_{K_2,H_2}(M)$. Once item 2 is fixed at $q_2 = M$, item 1 solves problem (5):

In Lean these objects are JRPHard.Aperiodic.eoq, JRPHard.Periodic.periodicCost, JRPHard.Periodic.coefK2, JRPHard.Periodic.coefH2 (shared with missions 1 and 2), and IsRangeDivisorInstance, HasDivisorIn, coefK0, rangeCost, threshold, obj5 and fConv in the namespace JRPHard.RangeDiv.

Formalization targets

Goal: Lemma 3

For every RangeDivisor instance $(M, L, U)$,

Milestones (the steps of the proof, pp. 14–15)

1. Item 2 is pinned: every plan with $q_2 \ne M$ costs more than $z_{M,L,U}$.
2. $f(q) = LU/q + q$ is a lower bound on problem (5)'s objective, $f(L) = f(U) = L + U$, and $f$ is minimized at $\sqrt{LU}$.
3. $\gcd(q, M) \ne q \Rightarrow \gcd(q, M) \le q/2$.
4. If $\gcd(q, M) \ne q$, the objective of (5) at $q$ is at least $2\sqrt{2LU} > L + U$.
5. A divisor $q \in [L, U]$ of $M$ has objective at most $L + U$.
6. A period with objective at most $L + U$ divides $M$ and lies in $[L, U]$.

Significance

Lemma 3 is the step that carries hardness from number theory to inventory theory. With Shor's result it shows that, under the Riemann hypothesis, no polynomial-time exact algorithm for the two-item periodic JRP exists unless NP problems can be solved in randomized polynomial time. The paper concludes (p. 15) that no algorithm for the two-item problem may be simultaneously exact and polynomial on all inputs, so some concession, such as heuristics, must be made.

The result is proved in the paper; it has not been machine-checked. The mission produces a checked statement of the reduction's correctness with every coefficient explicit, and it corrects two imprecisions in the printed lemma (the threshold and the unspecified "sufficiently large" coefficients of item 2; see below). The objects (eoq, periodicCost) are the same ones used in mission 2 of this series.

Difficulty

Each step is elementary, but the statement mixes integer and real reasoning. The objective of (5) is not monotone or convex in $q$: its value jumps between $LU/q + q$ at divisors of $M$ and at least $2LU/q + q$ elsewhere. The argument must show that the gap between these two curves exceeds the window around $L + U$, and this is exactly what RangeDivisor's condition $L + U < 2\sqrt{2LU}$ provides. Without that condition a non-divisor can be cheaper than $L + U$ (for $L = 1$, $U = 100$, $M = 7$, the period $q = 14$ has objective $100/7 + 14 < 101$). The pinning of $q_2 = M$ also has to beat the slack $M + 2\sqrt{LU}$ against $L + U$, which is where $M \ge U$ is used.

Formalization scope

This mission formalizes the correctness of the reduction behind Theorem 2 (its JRP half, Lemma 3); polynomial running time is not formalized. Theorem 2 itself, Shor's NP-completeness of RangeDivisor under randomized reductions, and "one can construct in polynomial time" are not stated. What remains of the polynomial-time claim is the explicit coefficients and the bound $K_0, K_2, H_2 \le 2M^4$ (bit length at most $4\log_2 M + 2$).

Conventions:

• periods are natural numbers, and every quantified period is assumed positive (Lean's $K/0 = 0$ and $\gcd(0, M) = M$ would otherwise create spurious cheap plans);
• costs are real numbers; $L$, $U$, $M$ and the coefficients are natural numbers cast to $\mathbb{R}$;
• RangeDivisor's condition is stated with Real.sqrt exactly as printed;
• "the optimal value is at most $z$" is the decision form "some plan has cost at most $z$" (p. 13); the minimum is attained, so the two agree.

Two disclosed departures from the printed lemma:

• The threshold. The page writes "the optimal value of $\mathrm{JRP}_{M,U,L} \le L + U$". The two-item cost also contains item 2's term $2M^2(M+1)$, so the literal comparison never holds and would make the lemma false. The threshold is $z_{M,L,U} = L + U + 2M^2(M+1)$, the $z_{M,L,U}$ announced in §3.1.
• The item-2 coefficients. The page chooses "sufficiently large values of $K_2$ and $H_2$, as in … Lemma 2". The statement fixes Lemma 2's values $K_2 = M^3(M+1)$, $H_2 = M(M+1)$ rather than quantifying existentially, which would let any instance satisfy the lemma.

A formalization that drops the positivity of periods, states the threshold as $L + U$ on the full two-item cost, or leaves $K_2, H_2$ existential does not capture Lemma 3 and is ruled out.

No library beyond Mathlib (Nat.gcd, Real.sqrt) is needed. Proofs of the milestones, and alternative proofs of the goal, are welcome.

Selected references

• A. S. Schulz and C. Telha, Integer factorization and Riemann's hypothesis: Why two-item joint replenishment is hard, arXiv:2007.09045v1, 2020; published as Integer Factorization: Why Two-Item Joint Replenishment Is Hard, Operations Research, 2024. https://arxiv.org/abs/2007.09045
• P. W. Shor, An NP-complete variant of factoring, Theoretical Computer Science Stack Exchange, 2011 (version 2011-03-01, as cited by the paper). https://cstheory.stackexchange.com/q/4785
• S. Arora and B. Barak, Computational Complexity: A Modern Approach, Cambridge University Press, 2009. https://doi.org/10.1017/CBO9780511804090

Motivation

Fake accounts (purchased followers, likes and engagement) are a large part of influencer marketing on social media, and platforms say they invest in detecting and removing them. Huang and Liu (Management Science 71(10), 2025) model this market as a signaling game. An influencer of unknown quality buys fake followers to look popular, consumers decide whether to follow, an advertiser pays for the real followers it expects, and the platform, which takes a share of the advertising revenue, chooses how much antifake effort to spend. A practical question for regulators and platform designers follows: does a platform that maximizes profit have any reason to fight fake accounts? This mission formalizes the paper's answer for the purely profit-driven platform: it does not.

The model draws on the signaling literature, in particular the undefeated equilibrium refinement of Mailath, Okuno-Fujiwara and Postlewaite (1993), and is close to the welfare analysis of social-learning manipulation in Chen and Papanastasiou (Management Science 67(11), 2021).

Setting

An influencer is of type $H$ (probability $\rho\in(0,1)$) or $L$, with content quality $q_H>q_L>0$, and $E[q]=\rho q_H+(1-\rho)q_L$. A fraction $l\in(0,1)$ of consumers (social media literacy) are informed and know the type. The platform picks an effort $d\ge0$. With technology level $\tau\in[0,1)$ and base price $p_0$, a fake account costs $p_f=p_0+d/(1-\tau)$ (1), and following costs a consumer $c=c_0+c_1(1-\tau)d$ (2), with $c_0,c_1\ge0$.

Informed followers of a $t$-type number $n^t_{in}=l(1-c/q_t)$ (8). Uninformed consumers see the early follower count $n_2^t$ and follow in number $n^t_{un}=(1-l)(1-c/E[q\mid n_2^t])$ (9). The real followers are $n^t_{r,ia}=n^t_{in}+n^t_{un}$ (10). An uninformed advertiser expects $E[n_{r,ua}]=\Pr(H\mid n)n^H_{r,ia}+\Pr(L\mid n)n^L_{r,ia}$ (11). From the $t$-type's side, the advertiser pays for $E[n^t_r]=l\,n^t_{r,ia}+(1-l)E[n_{r,ua}]$ real followers (12). Under a pooling equilibrium both types show the same count and the posterior is $\rho$. Under a separating equilibrium (costly or natural) the posterior is $1$ at the $H$-type's count and $0$ at the $L$-type's.

With advertising revenue $\mu>0$ per real consumer and platform share $\lambda_p$, the platform's profit under equilibrium type $r$ is (6)

where $E[n_r]$ averages (12) over the type. Two thresholds, $d_1=(1-\tau)(\eta_1-p_0)$ (13) and $d_2=(1-\tau)(\eta_2-p_0)$ (16), with $\eta_1=\lambda_i\mu(1-l)\big[q_H(E[q]-q_L)/(lE[q](q_H-q_L))+\rho\big]$ and $\eta_2=\frac1l\lambda_i\mu(1-l^2)$, select the equilibrium (Proposition 1). If $d_1>0$ and $d\le d_1$ the equilibrium is pooling. Otherwise it is costly separating for $d\le d_2$ and naturally separating beyond. The equilibrium profit is $\pi_p(d)=\pi^{r(d)}_p(d)$.

Formalization targets

Goal: Proposition 4(a)

A purely profit-driven platform ($w=0$ in the objective $\Pi_p=(1-w)\pi_p+wU$ of (3)) optimally chooses zero antifake effort, and zero is the unique optimum.

Milestones

1. (18): $d_1<d_2$.
2. Lemma 7: each $\pi^{pool}_p,\pi^{csep}_p,\pi^{nsep}_p$ strictly decreases in $d\ge0$.
3. The concavity comparison after Lemma 8: for $c>0$, $\rho\,n_{un}(q_H)+(1-\rho)\,n_{un}(q_L)<n_{un}(E[q])$.
4. Advertising revenue is higher under pooling: $E[n^{csep}_r](d)\le E[n^{pool}_r](d)$, strictly if $c>0$.
5. Lemma 8(a): if $d_1\le0$, $\pi^{csep}_p(0)>\pi^{nsep}_p(d_2)$ (under Assumption 3, $p_0<\eta_2$).
6. Lemma 8(b)(1): if $d_1>0$, $\pi^{pool}_p(0)>\pi^{csep}_p(d_1)$.
7. Lemma 8(b)(2): if $d_1>0$, $\pi^{csep}_p(d_1)>\pi^{nsep}_p(d_2)$.

Significance

Proposition 4(a) separates two motives for antifake effort. Effort harms a profit-maximizing platform twice: it raises the consumers' following cost, which lowers participation and revenue, and it costs $\frac{\gamma}{2}d^2$. Pooling, in which low-quality influencers successfully mimic high-quality ones, also earns more revenue than separation, because uninformed consumers follow an average influencer more readily than the average of the two types. So any antifake effort a platform makes must come from its concern for consumer welfare (Proposition 4(b)), not from advertising profit. That is the paper's argument for external pressure or regulation.

The result is proved in the paper's Online Appendix. This mission formalizes the main-text claims behind it: the threshold ordering, Lemma 7, the concavity argument and Lemma 8, together with the goal. To our knowledge none of these has a machine-checked proof. The definitions of the follower and profit model are reusable for the companion mission on the influencer's defensive purchasing (Proposition 3).

Difficulty

The obvious argument is "effort only costs, so choose zero". It is incomplete, because effort changes which equilibrium is played, and the equilibrium profit $\pi_p$ is discontinuous at $d_1$ and $d_2$. Comparing profits across regimes needs two facts. First, pooling revenue dominates separating revenue at the same effort, a strict-convexity (Jensen) inequality for $x\mapsto 1/x$ applied to the uninformed followers through (11)–(12). Second, the thresholds are ordered, $d_1<d_2$, which uses the explicit $\eta_1,\eta_2$. The bookkeeping of (10)–(12), where the advertiser's expectation is nested inside the type-average, has to be unfolded exactly. The boundary case $d_1=0$ falls under Proposition 1(a), so zero effort then induces costly separation, not pooling.

Formalization scope

Parameters form a Lean structure with ASCII field names (mu, lamI, lamP, rho, l, qH, qL, c0, c1, tau, p0, gamma). A Standing predicate records the ranges: $\mu>0$; $\lambda_i,\lambda_p>0$ with $\lambda_i+\lambda_p<1$; $\rho,l\in(0,1)$; $0<q_L<q_H$; $c_0,c_1\ge0$; $\tau\in[0,1)$; $\gamma>0$. $p_0$ is unconstrained, and Assumption 3 ($p_0<\eta_2$) is a separate hypothesis, used only in Lemma 8(a). The model's expectations are the closed forms (8)–(12); no probability space is built. Follower formulas are untruncated, as in the paper. Assumptions 1–2 depend on $d$, are never stated for a range of $d$, and are not needed, so they are not imposed.

The equilibrium regime map is Proposition 1 taken as a definition: the belief systems, the undefeated refinement and the proofs of Lemmas 1–4 are in the Online Appendix, which this mission does not use. The regime test is "$d_1>0$ and $d\le d_1$" for pooling, which matches Proposition 1(a) at $d_1=0$. Lemma 7 is stated on all of $d\ge0$, a superset of each regime's range. The two separating profits are the same function, because real followers depend only on the information revealed. The concavity milestone assumes $c>0$, without which both sides are equal.

The goal is about the equilibrium profit computed from (6) and (8)–(12). It is not about abstract regime profits with Lemmas 7–8 as hypotheses, and pooling revenue is not defined by substituting $E[q]$ into a single-type formula, which would hide the Jensen step. Consumer welfare $U$ is not formalized: its formula is not in the main text, so Proposition 4(b) and Table 3 are out of scope. Contributions welcome: proofs of the milestones and the goal, and a formalization of the signaling game behind Proposition 1.

Selected references

• Z. Huang and D. Liu, Economics of Social Media Fake Accounts, Management Science 71(10):8865–8883, 2025. https://doi.org/10.1287/mnsc.2022.02616
• G. J. Mailath, M. Okuno-Fujiwara and A. Postlewaite, Belief-Based Refinements in Signalling Games, Journal of Economic Theory 60(2):241–276, 1993. https://doi.org/10.1006/jeth.1993.1022
• L. Chen and Y. Papanastasiou, Seeding the Herd: Pricing and Welfare Effects of Social Learning Manipulation, Management Science 67(11):6734–6750, 2021.

Motivation

Many stochastic optimization models contain an expected-value constraint

where $\xi$ is a random object with unknown law $P_0$, $x$ is a decision and $h$ is a known loss. When $P_0$ is known only through an i.i.d. sample $\xi_1,\dots,\xi_n$, data-driven distributionally robust optimization (DRO) replaces $E_0$ by the worst case over a ball of distributions around the data. H. Lam, Recovering Best Statistical Guarantees via the Empirical Divergence-Based Distributionally Robust Optimization (arXiv:1605.09349v1, 2016; Operations Research 67(4), 2019), studies a ball of reweightings of the sample itself, measured by the Burg entropy, and links its radius to empirical likelihood (Owen 2001).

Lam's Theorem 2 shows that, for a fixed decision $x$, the minimum and maximum of $E_w[h(x;\xi)]$ over this ball bracket $Z_0(x)$ with probability tending to $1-\alpha$ when the radius is $\chi^2_{1,1-\alpha}/(2n)$. Theorem 3, the goal of this mission, complements it: the two bounds also converge almost surely to $Z_0(x)$. A confidence statement says the robust bounds are rarely wrong; consistency says they are eventually tight, so that the robust constraint does not stay conservative as data accumulate.

This mission is the second of a three-mission series on the pointwise theory of the paper (1: coverage, Theorem 2; 3: reduction to a Burg ball on a finite support, Proposition 1).

Setting

Let $\xi_1,\xi_2,\dots$ be i.i.d. random elements of a measurable space $\Xi$ with law $P_0$. Fix a decision $x\in\mathbb R^m$ and write $Z_0(x)=E_0[h(x;\xi)]$.

The Burg generator is $\phi(t)=-\log t+t-1$ for $t>0$ and $\phi(t)=+\infty$ for $t\le0$. The empirical Burg-entropy divergence ball of radius $\eta$ is the set of weight vectors

On the simplex, $-\frac1n\sum_i\log(nw_i)=\frac1n\sum_i\phi(nw_i)$, the $\phi$-divergence of $w$ from the uniform weights.

Let $0<\alpha<1$ and let $q=\chi^2_{1,1-\alpha}$ be the $(1-\alpha)$-quantile of the $\chi^2_1$ distribution. The lower and upper empirical DRO values are

The proof works with the centred observations $\tilde h_i=h(x;\xi_i)-Z_0(x)$.

Formalization targets

Goal: Theorem 3 (p. 12)

Under the conditions of Theorem 2 ($0<\mathrm{Var}_0(h(x;\xi))<\infty$, $Z_0(x)$ finite),

Milestones (the steps of the printed proof, at a single decision)

1. Lemma 3 (p. 38, Owen's Lemma 11.2): for i.i.d. $Y_i$ with $EY_i^2<\infty$, $\max_{1\le i\le n}|Y_i|=o(n^{1/2})$ a.s.
2. (75)–(76) (p. 33): the Lagrangian dual

with the printed conventions at $\lambda=0$ and for arguments outside the domain of the logarithm. 3. The elementary inequality (p. 34): $-\log(1-t)\le t+2t^2$ for $|t|\le1/2$. 4. (77) (p. 34): if $\max_i|\tilde h_i|\le\lambda/2$ with $\lambda>0$, then

5. The uniform-weight lower bound (p. 34): $\overline Z_n(x)-Z_0(x)\ge\frac1n\sum_i\tilde h_i$.

Milestones 2, 4 and 5 are deterministic statements about an arbitrary data vector; only Lemma 3 and the goal are probabilistic.

Significance

The result. Theorem 3 shows that the empirical DRO with the $\chi^2_1$ calibration is a consistent estimator of the constraint function at every fixed decision, not only a confidence bound. Together with Theorem 2 it places the empirical Burg-ball DRO on the same footing as the classical normal-approximation confidence interval: correct asymptotic coverage and shrinkage to the truth. The deterministic bounds (76)–(77) are also reusable on their own: they control the worst-case reweighting of any finite sample by its first two empirical moments.

Formalizing it. The theorem is proved in the paper; no machine-checked proof is known. The mission asks for a formal proof of the printed argument, specialized to one decision. A closely related open target exists on the platform: GenEmpLik.Expansion.lemma_1 (Duchi, Glynn and Namkoong) states the expansion of the robust mean, sample mean plus $\sqrt{\rho s_n^2/n}+o(n^{-1/2})$, for a smooth generator class under stationary ergodic data. Combined with the strong law it would give the upper half of Theorem 3, but it is a different statement with different hypotheses and is itself unproved, so it is not used as a milestone here.

Difficulty

The tempting argument, "the ball shrinks to the empirical distribution and the empirical mean converges", does not close by itself: $h(x;\xi)$ is only square integrable, not bounded, and the maximizing weight shifts mass towards the largest observations, so the gap $\overline Z_n(x)-\frac1n\sum_ih(x;\xi_i)$ has to be controlled against the extremes of the sample rather than by the size of the ball alone. The printed proof routes this through the convex dual (76). That step needs a constraint qualification, the conjugate of the Burg generator with its boundary conventions (an infinite value outside the domain of the logarithm, and the degenerate multiplier $\lambda=0$), and a choice of multiplier that dominates every centred observation while still letting all three terms of (77) vanish. The almost-sure statement then combines Lemma 3 with two strong laws on one event of full probability.

Formalization scope

• Data. The sample $\xi_1,\dots,\xi_n$ is ξ 0, …, ξ (n-1): a sequence of measurable maps that is independent (iIndepFun) and identically distributed (IdentDistrib with ξ 0). $Z_0(x)$ is the Bochner integral of h x ∘ ξ 0, and the moment conditions are MemLp (h x ∘ ξ 0) 2 (finite mean and variance) together with positive variance, which makes the integral the true mean.
• Decision. The paper's $x\in\Theta\subset\mathbb R^m$ is an arbitrary point of EuclideanSpace ℝ (Fin m); $\Theta$ plays no role in a pointwise statement and is dropped.
• Quantile. $q$ is pinned by $\mathcal N(0,1)\{y:y^2\le q\}=1-\alpha$, which determines it uniquely. The radius $q/(2n)$ is passed as $\rho=q/2$ to the published GenEmpLik.Expansion.robustMean, whose ball has radius $\rho/n$.
• Values. $\overline Z_n$ is robustMean burg (q/2); $\underline Z_n$ is robustLower burg (q/2) from the frozen shared EmpiricalDRO.Coverage.Setting module, a real infimum over the same published ball (PhiDivRobust.Counterpart.probUncertaintySet). For $n\ge1$ the value sets are nonempty and bounded, so the real sSup/sInf are the attained maximum and minimum.
• Divergence. burg is valued in EReal with $+\infty$ for $t\le0$, so a zero weight is excluded from the ball by an infinite divergence and never by a junk value of Real.log. The dual summand dualTerm is EReal-valued with the printed conventions: $+\infty$ for $t\ge\lambda>0$; $0$ or $+\infty$ at $\lambda=0$.
• Generalizations, disclosed. The deterministic milestones hold for every data vector; (76) is stated for every $q>0$ (the Slater point needs $q>0$), (77) for every $\lambda>0$ satisfying the hypothesis, and the uniform-weight bound for every radius $\rho\ge0$. In the goal, positive variance and the value of $\alpha$ are kept as printed although the conclusion does not need them.
• Ruled out. Junk logarithms at zero weights, a junk sSup/sInf of an empty value set, a free radius detached from the $\chi^2_1$ quantile, and a dropped variance condition are all excluded by the encoding above. The paper's printed (75) writes $\overline Z_n(x)$ where its radius $q_n/(2n)$ makes it $\overline Z^*_n(x)$; at a single decision the two coincide.
• Not posed. The paper's headline result, Theorem 4 (uniform coverage over $\Theta$ with a $\chi^2$-process quantile $q_n$), and the uniform statements Theorems 5–7 need Donsker and Glivenko–Cantelli classes, weak convergence in $\ell^\infty(\Theta)$ and conditional quantiles of Gaussian-process suprema, none of which has library support yet; they are left out.
• Reuse. Lemma 3 for nonnegative variables is the proved platform theorem NumStochOpt.ListScheduling.lemma_8_1_i_max_over_sqrt_ae, included as a reference. Mathlib's ProbabilityTheory.strong_law_ae supplies the laws of large numbers. Contributions welcome: the duality (76) for general $\phi$-divergence balls, and the deterministic bound (77).

Selected references

• H. Lam, Recovering Best Statistical Guarantees via the Empirical Divergence-Based Distributionally Robust Optimization, arXiv:1605.09349v1, 2016; Operations Research 67(4), 2019. https://arxiv.org/abs/1605.09349v1 , https://doi.org/10.1287/opre.2018.1786
• A. B. Owen, Empirical Likelihood, Chapman & Hall/CRC, 2001. https://doi.org/10.1201/9781420036152
• A. Ben-Tal, D. den Hertog, A. De Waegenaere, B. Melenberg, G. Rennen, Robust solutions of optimization problems affected by uncertain probabilities, Management Science 59(2), 2013. https://doi.org/10.1287/mnsc.1120.1641
• J. C. Duchi, P. W. Glynn, H. Namkoong, Statistics of robust optimization: a generalized empirical likelihood approach, Mathematics of Operations Research 46(3), 2021. https://arxiv.org/abs/1610.03425

Motivation

Comparing histograms is a basic operation in statistics, computer vision and machine learning: a bag of image descriptors, a word-frequency vector, a discretized density. When the bins carry a geometry (colors that are close to one another, words with related meanings), a comparison that ignores the geometry, such as an $\ell^p$ norm between the histogram vectors, treats a small shift of mass to a neighboring bin as severely as a shift to a distant bin. Optimal transport compares two histograms by the cheapest way to move one onto the other, with costs read off a ground distance between bins. Rubner, Tomasi and Guibas introduced it to image retrieval as the earth mover's distance (Rubner et al. 2000), and it has since been used for document classification (Kusner et al. 2015) and as a training loss (Frogner et al. 2015).

These uses rely on the transport cost being a distance, so that nearest-neighbor search, clustering and the geometry of the space of histograms behave as expected. This mission formalizes the statement that it is one: Proposition 2.2 of Peyré and Cuturi, Computational Optimal Transport (2019), the discrete form of the classical fact that the $p$-Wasserstein distance is a metric (Villani 2003, Theorem 7.3).

Setting

Fix $n\ge1$ and write $[\![n]\!]=\{1,\dots,n\}$. The probability simplex is

its elements are histograms. For $a,b\in\Sigma_n$ the set of couplings (2.10) is

the nonnegative matrices with row sums $a$ and column sums $b$; $P_{i,j}$ is the mass sent from bin $i$ to bin $j$. For a cost matrix $C$, the Kantorovich problem (2.11) is

A matrix $D\in\mathbb R^{n\times n}_+$ is a distance on $[\![n]\!]$ if it is symmetric, $D_{i,j}=0$ exactly when $i=j$, and $D_{i,k}\le D_{i,j}+D_{j,k}$ for all $i,j,k$. For $p\ge1$, write $D^p=(D_{i,j}^p)_{i,j}$ for the entrywise power. The $p$-Wasserstein distance (2.17) is

In the Lean development these are couplings a b, frob C P, otCost C a b, powCost D p and W D p a b in the namespace CompOT.Metric.

Formalization targets

Goal: Proposition 2.2 (p. 377)

For a distance matrix $D$ and $p\ge1$, for all $a,b,c\in\Sigma_n$,

Milestones, from the book's proof (pp. 377–379)

1. $\mathrm{diag}(a)$ is an optimal coupling in $U(a,a)$ for $D^p$ and $\mathrm W_p(a,a)=0$.
2. If $a\ne b$, every $P\in U(a,b)$ has $P_{i,j}\ne0$ for some $i\ne j$.
3. If $a\ne b$, then $\mathrm W_p(a,b)>0$.
4. $\mathrm W_p(a,b)=\mathrm W_p(b,a)$.
5. Gluing. With $\tilde b_j=b_j$ if $b_j>0$ and $\tilde b_j=1$ otherwise, for $P\in U(a,b)$ and $Q\in U(b,c)$,

6. Minkowski chain. For the same $P,Q,S$,

The case $p=1$ of the goal's attainment and triangle inequality is already proved on the platform, in another encoding (couplings as functions on $V\times V$ for a finite metric space $V$): MarkovMixing.transport_metric, included here as a reference item. The goal for general $p\ge1$ is new.

Significance

The result. Proposition 2.2 makes $(\Sigma_n,\mathrm W_p)$ a metric space whose metric depends on the ground distance $D$. This is what entitles later chapters of the book to speak of Wasserstein barycenters, geodesics and Lipschitz properties of the transport cost, and it underlies the use of $\mathrm W_p$ as a loss or a retrieval distance. Remark 2.15 of the same page records that for $0<p\le1$ it is $\mathrm W_p^p$, not $\mathrm W_p$, that is a distance, so the restriction $p\ge1$ is substantive.

Formalizing it. The result is classical and fully proved in the book; it has not been machine-checked for general $p$ in this discrete matrix form. The platform's $p=1$ result uses a different encoding of couplings, so this mission supplies the matrix-form transportation polytope $U(a,b)$, the cost $L_C$ and $\mathrm W_p$ shared with the other missions of this series, plus a discrete gluing lemma and a Minkowski step stated for arbitrary couplings, which are reusable in any finite transport argument.

Difficulty

Symmetry and definiteness are short once the minimum in $L_{D^p}$ is known to be attained, which needs compactness of $U(a,b)$; strict positivity for $a\ne b$ fails for an infimum that is not attained. The triangle inequality is the substantial part. The direct idea of composing the two transport plans as $PQ$ does not give a coupling: the composition must be renormalized by the middle histogram $b$, and $b$ may have zero entries, on which a naive $1/b_j$ is undefined. The renormalized matrix must then be shown to have the right marginals, which uses that $P_{i,j}=0$ wherever $b_j=0$. The final step needs Minkowski's inequality for weighted $\ell^p$ sums together with the triangle inequality of $D$ and the monotonicity of $t\mapsto t^p$; for $p<1$ it fails.

Formalization scope

Indices $[\![n]\!]$ are Fin n (0-based). Histograms are Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, and $\Sigma_n$ is Mathlib's stdSimplex ℝ (Fin n); histograms may have zero entries. $L_C(a,b)$ is a real infimum over the subtype $U(a,b)$, and every theorem assumes the histograms lie in $\Sigma_n$, where $U(a,b)$ is nonempty (it contains $ab^{\top}$) and compact. That attainment is part of what a solver proves; it is not a hypothesis. The exponent $p$ is a real number with $p\ge1$, and all powers are real powers. The book's "positive" is read as $\mathrm W_p\ge0$; strict positivity is the clause $\mathrm W_p(a,b)=0\iff a=b$. The hypotheses of the goal are exactly those of the page: $D_{i,j}\ge0$, (i)–(iii), and $p\ge1$. The milestones carry the same setting, and milestones 5 and 6 are stated for all couplings instead of only optimal ones, since the proof does not use optimality there.

A trivializing formalization is ruled out: without the simplex hypotheses $U(a,b)$ can be empty and the real infimum would be $0$, making "$\mathrm W_p(a,b)=0$" true for unrelated histograms; and the four claims are stated about $\mathrm W_p$ itself, not about the glued coupling or about a minimum over a set assumed nonempty.

Needed infrastructure: compactness and nonemptiness of $U(a,b)$ and attainment of $L_C$; transposition of couplings; the gluing construction; Minkowski's inequality for finite weighted sums (Mathlib has Real.Lp_add_le and its weighted variants). Proofs of any milestone are welcome, as are reusable lemmas on $U(a,b)$.

Selected references

• G. Peyré and M. Cuturi, Computational Optimal Transport, Foundations and Trends in Machine Learning 11(5–6):355–607, 2019. https://doi.org/10.1561/2200000073 (Proposition 2.2, p. 377).
• C. Villani, Topics in Optimal Transportation, Graduate Studies in Mathematics 58, AMS, 2003. https://doi.org/10.1090/gsm/058
• Y. Rubner, C. Tomasi and L. J. Guibas, The Earth Mover's Distance as a Metric for Image Retrieval, International Journal of Computer Vision 40(2):99–121, 2000. https://doi.org/10.1023/A:1026543900054
• M. Kusner, Y. Sun, N. Kolkin and K. Weinberger, From Word Embeddings to Document Distances, ICML 2015. https://proceedings.mlr.press/v37/kusnerb15.html
• C. Frogner, C. Zhang, H. Mobahi, M. Araya-Polo and T. Poggio, Learning with a Wasserstein Loss, NeurIPS 2015. https://arxiv.org/abs/1506.05439
• D. A. Levin, Y. Peres and E. L. Wilmer, Markov Chains and Mixing Times, AMS, 2009, Lemma 14.3 (the $p=1$ case on the platform). https://doi.org/10.1090/mbk/058

Why discrete Kantorovich duality

Optimal transport between two histograms is a linear program: move mass $a_i$ out of each source bin $i$ and deliver mass $b_j$ to each target bin $j$ at unit cost $C_{i,j}$, as cheaply as possible. Its dual replaces the transport plan by a pair of price vectors and is the basis of most of the computational methods in G. Peyré and M. Cuturi's Computational Optimal Transport (Foundations and Trends in Machine Learning, 2019, doi:10.1561/2200000073): the dual ascent and Hungarian methods, the auction algorithm, the semi-discrete solvers of Chapter 5, and the dual reading of Sinkhorn's algorithm in Chapter 4. The book states the duality as Proposition 2.4 and derives it from linear programming strong duality (Bertsimas and Tsitsiklis, Introduction to Linear Optimization, 1997, Theorem 4.4). Remark 2.21 gives it an economic reading: a vendor sets a collection price $f_i$ at each warehouse and a delivery price $g_j$ at each factory, and the best price the vendor can charge while staying below every shipping cost equals the optimal transport cost.

This is the third mission in a series on the book. It covers §2.5 (Dual Problem, pp. 382–385) and §3.1–3.3 (Kantorovich Linear Programs, C-Transforms, Complementary Slackness, pp. 400–405).

Setting

Indices run over $\llbracket n\rrbracket=\{1,\dots,n\}$ and $\llbracket m\rrbracket$. A histogram is a vector in the probability simplex $\Sigma_n=\{a\in\mathbb R^n_+ : \sum_i a_i = 1\}$. Fix $a\in\Sigma_n$, $b\in\Sigma_m$ and a cost matrix $C\in\mathbb R^{n\times m}$; no sign or metric condition is imposed on $C$.

• The couplings (2.10) are $\mathbf U(a,b)=\{P\in\mathbb R_+^{n\times m}: P\mathbb 1_m=a,\ P^{\mathsf T}\mathbb 1_n=b\}$.
• The Kantorovich problem (2.11) is $L_C(a,b)=\min_{P\in\mathbf U(a,b)}\langle C,P\rangle$, with $\langle C,P\rangle=\sum_{i,j}C_{i,j}P_{i,j}$.
• The admissible dual variables (2.21) are $\mathbf R(C)=\{(f,g)\in\mathbb R^n\times\mathbb R^m : f_i+g_j\le C_{i,j}\ \forall i,j\}$, written $f\oplus g\le C$.
• The $C$-transform of $f\in\mathbb R^n$ is $(f^C)_j=\min_i C_{i,j}-f_i$, and the $\bar C$-transform of $g\in\mathbb R^m$ is $(g^{\bar C})_i=\min_j C_{i,j}-g_j$ (§3.2).
• $P$ and $(f,g)$ are complementary w.r.t. $C$ (Definition 3.1) if $C_{i,j}=f_i+g_j$ whenever $P_{i,j}>0$.

In Lean these are couplings, frob, IsOptimalCoupling, dualFeasible, dualObj, IsDualOptimal, cTransform, cbarTransform and Complementary in the namespace CompOT.Duality.

Formalization targets

Goal: Proposition 2.4 (p. 382)

Stated with both extrema attained: there are an optimal coupling $P$ and a dual optimal pair $(f,g)$ with $\langle C,P\rangle=\langle f,a\rangle+\langle g,b\rangle$.

Milestones

1. Weak duality (Remark 2.21, p. 385): $\langle C,P\rangle\ge\sum_{i,j}P_{i,j}(f_i+g_j)=\langle f,a\rangle+\langle g,b\rangle$ for $P\in\mathbf U(a,b)$ and $(f,g)\in\mathbf R(C)$.
2. The $C$-transform is the best second potential (§3.2, p. 403): $(f,f^C)\in\mathbf R(C)$, and $g\le f^C$ whenever $(f,g)\in\mathbf R(C)$.
3. Semi-dual inequality (§3.2, p. 403): $\langle f,a\rangle+\langle g,b\rangle\le\langle f,a\rangle+\langle f^C,b\rangle$ for $(f,g)\in\mathbf R(C)$.
4. Proposition 3.1 (pp. 403–404): $f\le f'\Rightarrow f^C\ge f'^C$; $f^{C\bar C}\ge f$ and $g^{\bar CC}\ge g$; $f^{C\bar CC}=f^C$.
5. Proposition 3.3 (p. 405): complementary feasible solutions are primal and dual optimal.
6. Proposition 3.2 (p. 404): for optimal $P^\star$ and $(f^\star,g^\star)$, $P^\star_{i,j}(C_{i,j}-f^\star_i-g^\star_j)=0$ for all $(i,j)$.
7. The semi-dual (3.5) (p. 403): $L_C(a,b)=\max_{f\in\mathbb R^n}\langle f,a\rangle+\langle f^C,b\rangle$.

Milestones 6 and 7 are consequences of the goal; milestones 1 and 5 do not need it.

Significance

Proposition 2.4 is the finite-dimensional form of Kantorovich duality. It turns the optimal cost into a maximum over price vectors, so that any admissible pair of prices certifies a lower bound on $L_C(a,b)$ and an optimal pair certifies optimality of a plan through complementary slackness (Propositions 3.2 and 3.3). The $C$-transform reduces the dual to a concave maximization in one vector (3.5), which is the form used for semi-discrete transport and for stochastic dual methods; Proposition 3.1 shows that alternating $C$- and $\bar C$-transforms stalls after one round.

All of these results are classical and proved in the book or by direct reference to linear programming. General-form LP strong duality, weak duality and complementary slackness are already machine-checked on the platform (LinearOptimization.lp_strong_duality and its siblings, from the Bertsimas–Tsitsiklis series); measure-theoretic weak Kantorovich duality is also on the platform with integrability hypotheses. What this mission adds is the book's own discrete statements in the book's notation, as a base that later missions of the series (dual ascent, auction, entropic duality) can cite, with the $C$-transform calculus of §3.2 formalized for real-valued finite costs.

Difficulty

Weak duality, the $C$-transform facts and Proposition 3.3 are finite computations with sums and minima. The content of the mission is the equality in Proposition 2.4 together with attainment of both the minimum and the maximum. Attainment of the minimum needs compactness and nonemptiness of $\mathbf U(a,b)$; attainment of the maximum is not a compactness argument, since $\mathbf R(C)$ is unbounded (it is invariant under $(f,g)\mapsto(f+t,g-t)$). Reducing Proposition 2.4 to the general LP statement requires an explicit translation of $\mathbf U(a,b)$ and $\mathbf R(C)$ into the general-form primal–dual pair, including the sign conventions of equality-constrained primal variables and free dual variables. The Lagrangian argument on p. 382–383 exchanges a min and a max without justification beyond "always possible for linear programs", so it does not yield a proof by itself.

Formalization scope

Indices are 0-based (Fin n, Fin m); matrices are Matrix (Fin n) (Fin m) ℝ; all quantities are real. Histograms are encoded as a ∈ stdSimplex ℝ (Fin n), the book's standing convention for $(a,b)$, and every statement involving $a$ or $b$ carries it; this also forces $n,m\ge1$. Zero entries in $a$ and $b$ are allowed. Optimality of a plan and of a dual pair are predicates quantifying over the whole feasible set, never real ⨅/⨆, so no junk value from an empty or unbounded set can enter. The $C$-transforms are real infima over a finite index set; statements that use them without histograms assume $n\ge1$ (and $m\ge1$ where the $\bar C$-transform appears), because Lean's infimum over an empty index is $0$.

The goal cannot be satisfied trivially: it asserts existence of a plan that is optimal against every coupling and a pair that is optimal against every admissible pair, with equal values; dropping either optimality clause, or the equal-mass hypotheses, changes the theorem.

Two printed slips are corrected and disclosed in the item notes: Proposition 3.2 prints $C_{i,j}-f^\star_i+g^\star_j$ where its proof uses $C_{i,j}-f^\star_i-g^\star_j$, and Propositions 3.2 and 3.3 refer to the primal and dual as "(2.24)" and "(2.11)", meaning the discrete primal (2.11) and dual (2.20).

Useful infrastructure: the platform's general-form LP strong duality (included as a reference item), Mathlib's stdSimplex and finite infima. Contributions welcome: proofs of each milestone, a direct proof of Proposition 2.4 by reduction to the LP theorem, and alternative proofs of the goal.

Selected references

• G. Peyré and M. Cuturi, Computational Optimal Transport, Foundations and Trends in Machine Learning 11(5–6):355–607, 2019. https://doi.org/10.1561/2200000073
• D. Bertsimas and J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997 (Theorem 4.4, strong duality).
• L. Kantorovich, On the transfer of masses, Doklady Akademii Nauk SSSR 37:199–201, 1942 (English translation: J. Math. Sci. 133:1381–1382, 2006). https://doi.org/10.1007/s10958-006-0049-2

Inventory control when demand follows the state of the world

Single-item inventory theory asks how much stock to order each period when the order carries a fixed cost $K$ on top of a per-unit cost and demand is random. With independent, identically distributed demand, Scarf (1960) showed that the optimal finite-horizon policy has the $(s,S)$ form: when the stock falls below the reorder point $s$, order up to the level $S$; otherwise order nothing. His proof introduced $K$-convexity.

In practice demand is rarely i.i.d. It depends on economic conditions, seasons, or the stage of a product's life cycle, which change over time and carry over from one period to the next. Song and Zipkin (1993) modeled this by letting a Markov chain of "world states" modulate the demand distribution. Sethi and Cheng (1997) treat a general discrete-time model of this kind. The demand density, the cost parameters and the surplus cost all depend on the period and on the current demand state. They prove that a state-dependent $(s,S)$ policy is optimal over a finite horizon. They require no growth condition on the backlog cost, and they allow $s$ and $S$ to be $-\infty$.

Timeline:

• 1960: Scarf proves $(s,S)$ optimality for i.i.d. demand using $K$-convexity, assuming a backlog cost that grows faster than the unit ordering cost.
• 1966: Veinott gives an alternative proof under different assumptions.
• 1993: Song and Zipkin treat a continuous-time model with Markov-modulated Poisson demand and linear costs, assuming $p > \alpha c^i$.
• 1997: Sethi and Cheng prove the discrete-time result studied here, with general convex surplus costs.

Setting

There are $L$ demand states $I$ and periods $0, 1, \dots, N$. The state $i_k$ in period $k$ follows a Markov chain with transition matrix $P = (p_{ij})$. Given $i_k = i$, the demand $\xi_k \ge 0$ has density $\varphi_{i,k}$, with mean at most $M$. At the start of period $k$ an order $u_k \ge 0$ is placed and arrives at once. Then demand is subtracted, and unmet demand is backlogged:

Ordering costs $c_k(i,u) = K^i_k\delta(u) + c^i_k u$, with $\delta(u) = 1$ for $u > 0$ and $0$ otherwise, and $K^i_k, c^i_k \ge 0$. A surplus $x$ costs $f_k(i,x)$, a convex, nonnegative function with $f_k(i,0) = 0$ and $f_k(i,x) \le C(1+|x|)$.