All missions

Motivation

When indivisible goods are divided among $n$ agents without money, a standard way to say what each agent deserves is a share: a number $s(v,n)$ computed from the agent's own valuation $v$ alone, with the promise that she receives a bundle worth at least that much. The best-known share is the maximin share (MMS) of Budish (2011): the value an agent could guarantee by splitting the goods into $n$ bundles and receiving the worst one. A share is useful only if it is feasible, meaning that every profile of valuations admits an allocation giving each agent her share. The MMS is not feasible: Kurokawa, Procaccia and Wang (J. ACM 2018) built additive instances with three agents in which no allocation gives everyone her MMS.

This raises a natural question. Is there a single "best" feasible share, one that dominates every other feasible share? Babaioff and Feige (arXiv:2205.07519v1, 2022; Math. Oper. Res. 2025) observe that this fails for a trivial reason: shares tailored to one valuation each can be combined into an infeasible requirement. They therefore ask for less: a feasible share that dominates only the feasible shares that are also self-maximizing, so that a risk-averse agent who knows nothing about the allocation algorithm is best off reporting her true valuation. Their first main result, Theorem 1, shows that even this weaker "best" share does not exist for additive valuations or any larger class.

Setting

There are $m$ goods $M=\{0,\dots,m-1\}$ and $n\ge1$ agents. A valuation assigns a real value $v(S)$ to every bundle $S\subseteq M$; in the paper valuations are normalized ($v(\emptyset)=0$) and non-decreasing. A valuation is additive if $v(S)=\sum_{j\in S}w_j$ for item values $w_j\ge0$. An allocation is a map $A:M\to\{0,\dots,n-1\}$, and agent $i$ receives $A_i=A^{-1}(i)$.

A class $\mathcal C$ gives for each $m$ a set $\mathcal C_m$ of valuations on $m$ goods. A share for $\mathcal C$ is a function $s_{m,n}(v)$ that is realizable ($s_{m,n}(v)\le\max_S v(S)$) and name independent (renaming the goods does not change it) on $\mathcal C$. A bundle $S$ is acceptable for $v$ if $v(S)\ge s_{m,n}(v)$. The share is feasible for $\mathcal C$ if every profile $(v_0,\dots,v_{n-1})$ in $\mathcal C_m$ admits an allocation in which every agent's bundle is acceptable.

For a true valuation $v$ and a report $v'$, the implied guarantee is

$$\hat s_v(v')=\min_{\{S:\ v'(S)\ge s_{m,n}(v')\}} v(S),$$

and the share guarantee is $\hat s(v,n)=\hat s_v(v)$. The share is self-maximizing for $\mathcal C$ if $\hat s(v,n)\ge\hat s_v(v')$ for all $v,v'\in\mathcal C_m$. A share $s$ dominates $s'$ on $\mathcal C$ if $s_{m,n}(v)\ge s'_{m,n}(v)$ for all $m$, $n\ge1$ and $v\in\mathcal C_m$. A feasible share is SM-dominant if it dominates every feasible self-maximizing share.

The proof uses picking-order shares. A picking order is $\omega:\{1,\dots,m\}\to[n]$; $x_k$ is the most that agent $k$ can ensure when she picks at the steps $\omega_j=k$ and an adversary makes all other picks to minimize her value. The $\omega$-Picking-Order share is $\min_k x_k$.

Formalization targets

Goal: Theorem 1 (p.14)

For every class $\mathcal C$ that contains all additive valuations,

$$\neg\,\exists s:\ s\text{ is a share for }\mathcal C,\ \text{feasible for }\mathcal C,\ \text{and dominates every feasible self-maximizing share for }\mathcal C,$$

and hence no SM-dominant feasible share for $\mathcal C$ exists. The dominating share need not be self-maximizing, and no computational bound is imposed.

Milestones

1. (§4.1, p.15) The $\omega$-Picking-Order share is the value of a bundle, so it equals its share guarantee.
2. (§4.1, p.15) It is a share in the sense of Definition 2.
3. (Lemma 14, p.34) It is self-maximizing for every class.
4. (Lemma 15, p.34) It is feasible for every class.
5. (Lemma 16, p.35) For an additive $v$, some picking order has share exactly $\mathrm{MMS}_n(v)$.
6. ([KPW18], p.16) Some additive three-agent instance has no allocation giving every agent her MMS.

Significance

Theorem 1 says that, for additive valuations and every larger class (submodular, subadditive, general monotone), no notion of "the fair share" can be both always achievable and at least as generous as every truthful achievable share. The paper responds by studying approximate domination and proving positive results (Theorem 3: for additive valuations, a feasible, self-maximizing, polynomial-time computable share that is $\tfrac{2n}{3n-1}$-dominating). The negative result is what makes these approximations the right target.

The theorem is proved on paper; it has no machine-checked proof. A formal development needs the picking game for arbitrary (non-additive) valuations, the incentive argument of Lemma 14, the greedy analysis of Lemma 16, and an explicit additive instance without MMS allocations. That last item, the Kurokawa–Procaccia–Wang counterexample, is cited by the paper and has not been formalized here either; a verified instance would be reusable by any fair-division development.

Difficulty

The definitions are elementary, but the statement quantifies over shares for an arbitrary class, so the self-maximizing and feasibility properties of picking-order shares must be proved for every valuation, not just additive ones. For general valuations the agent's best strategy is not greedy, and Lemma 14 rests on comparing strategies of a finite game rather than on a formula. The final step needs an explicit instance in which the MMS is infeasible: such instances are delicate (carefully balanced item values for three agents) and checking that no allocation works requires examining all $3^m$ allocations together with the three maximin values. The tempting shortcut of fixing the class to additive valuations is not the theorem: the shares to be dominated must be self-maximizing and feasible on the whole class.

Formalization scope

Goods are Fin m, bundles Finset (Fin m), valuations Finset (Fin m) → ℝ, a class is C : (m : ℕ) → Set (Finset (Fin m) → ℝ), and a share is s : (m n : ℕ) → (Finset (Fin m) → ℝ) → ℝ. Allocations are maps Fin m → Fin n. Every property quantifies over all $m$ and all $n\ge1$; at $n=0$ no allocation of a nonempty set of goods exists, which would make feasibility impossible and the theorem vacuous, so $n=0$ is excluded. Guarantees are minima in WithTop ℝ, which is the real minimum whenever the share is realizable. The picking game value is defined by backward induction (FairShares.gameVal). The MMS is the published LittleCharity.MMS.mms v n Finset.univ. The goal allows the class to contain arbitrary real set functions beyond the additive valuations; this implies the paper's statement for classes of valuations over goods.

The polynomial-time clauses of Proposition 5 and Lemma 15, Theorem 2 (every feasible share is dominated by a feasible self-maximizing one) and the approximation results of §6 are outside this mission. Proofs of any milestone, a reusable development of perfect-information picking games, and a verified MMS-infeasible instance are all welcome.

Selected references

• M. Babaioff, U. Feige, Fair Shares: Feasibility, Domination and Incentives, arXiv:2205.07519v1, 2022; Math. Oper. Res., 2025. https://arxiv.org/abs/2205.07519v1
• D. Kurokawa, A. D. Procaccia, J. Wang, Fair Enough: Guaranteeing Approximate Maximin Shares, J. ACM 65(2):8, 2018. https://doi.org/10.1145/3140756
• E. Budish, The Combinatorial Assignment Problem: Approximate Competitive Equilibrium from Equal Incomes, J. Political Economy 119(6), 2011. https://doi.org/10.1086/664613

Why indefinite, partially observed mean-field games

Mean-field games model a large population of agents in which each agent's dynamics and cost depend on the others only through population averages. In the linear-quadratic (LQ) case the agents' states follow linear stochastic differential equations and costs are quadratic, so the equilibrium can be computed from Riccati equations. A standard way to use the limit is to solve a single-agent limiting problem against a fixed mean-field trajectory, close the loop with a consistency condition, and then prove that the resulting decentralized strategies are an $\varepsilon$-Nash equilibrium of the finite game with $\varepsilon\to0$ as $N\to\infty$ (Huang, Caines and Malhamé, 2007, doi:10.1109/TAC.2007.904450).

Two features make the problem of T. Chen, T. Nie and Z. Wu (arXiv:2508.01568v1) harder than the classical setting. First, agents do not see their own state; they see a noisy, controlled private observation and a public observation of a common noise. Second, the cost weights may be indefinite: no sign is imposed on the state weight $Q$, the control weight $R$ or the terminal weight $L_T$. Indefinite weights arise in mean-variance portfolio selection, where the control weight is zero (§6 of the paper). Indefinite stochastic LQ control without partial observation goes back to Chen, Li and Zhou (1998, doi:10.1137/S0363012996310478); uniform convexity of the cost as the standing condition is the approach of Sun, Li and Yong (2016, doi:10.1137/15M103532X).

Setting

Fix a horizon $T$, a state dimension $n$, a control dimension $m$, and a noise dimension $d$. On a probability space carry a one-dimensional common noise $W^0$ and, for each agent $1\le i\le N$, two independent $d$-dimensional noises $W^i,\bar W^i$. Agent $i$'s state $x^i\in\mathbb R^n$ solves

$$dx^i=\{Ax^i+Bu^i+\bar Ax^{(N)}+\bar Bu^{(N)}+b\}dt+\sigma dW^i+\{Dx^i+Fu^i+\bar Dx^{(N)}+\bar Fu^{(N)}+\bar b\}dW^0+\bar\sigma d\bar W^i,\qquad x^i_0=x,$$

where $x^{(N)}$ and $u^{(N)}$ are the population averages of states and controls. Agent $i$ observes $dy^i=\{Gx^i+Hu^i+\bar Gx^{(N)}+\bar Hu^{(N)}+\tilde b\}dt+\tilde\sigma d\bar W^i$ and the public process $d\theta=(I\theta+\check b)dt+\check\sigma dW^0$. Its cost $\mathcal J_i(u^i,u^{-i})$ is a quadratic functional of $x^i-\alpha_kx^{(N)}$ and $u^i-\beta_ku^{(N)}$ with weights $Q,R,S,q,r,L_T,l_T$. The coefficients are bounded deterministic functions (Assumptions (H1)–(H2)). Admissible centralized strategies $\mathscr U^i_c$ are square-integrable controls adapted to the observations.

The limiting problem (MFD) replaces $(x^{(N)},u^{(N)})$ by a mean-field pair $(x^0,u^0)$ adapted to the common observation. It is solved over decentralized strategies $\mathscr U^i_d$, adapted to agent $i$'s own limiting observation. A relaxed compensator is a symmetric absolutely continuous $P$ such that the weights $Q^P=Q+\dot P+PA+A^\top P+D^\top PD$, $S^P=S+PB+D^\top PF$, $R^P=R+F^\top PF$, $L_T-P_T$ satisfy the classical positivity condition (PD). Equivalently, $P$ satisfies the matrix inequalities of Condition (RC).

Formalization targets

Goal: Theorem 5.11

Assume (H1)–(H2), that a relaxed compensator exists, and that the Riccati equation (35) has a unique solution. Then there are $C>0$ and $N_0$ such that for every $N\ge N_0$ and every profile $\bar u$ of decentralized strategies (optimal for (MFD) with the consistent pair $(x^0,u^0)$), each $\bar u^i\in\mathscr U^i_c$ and

$$\mathcal J_i(\bar u^i,\bar u^{-i})\le\mathcal J_i(u^i,\bar u^{-i})+\frac{C}{\sqrt N}\qquad\text{for all }u^i\in\mathscr U^i_c.$$

Milestones

The limiting problem: backward separation (Lemma 4.2), reduction of the admissible class (Lemma 4.3), and the maximum principle (Proposition 4.4). Relaxed compensators: the identity $J_i=J^P_i+\tfrac12\langle P_0x,x\rangle$ (Lemma 4.7), Schur's complement (Lemma 4.8), (PD) ⇔ (RC) (Proposition 4.10), unique solvability of the Hamiltonian system (Proposition 4.11), the Riccati feedback (Theorem 4.12), and the equivalence of compensator, Riccati solvability and uniform convexity (Lemma 4.14). The approximation estimates: Lemmas 5.2–5.5, 5.8–5.10, and the a-priori bound (44) on profitable deviations.

Significance

The result says that a population of agents who cannot observe their states and face indefinite costs can still use strategies computed from one representative problem and lose only $O(1/\sqrt N)$ against any unilateral deviation. The relaxed compensator gives a coefficient-level certificate: Condition (RC) is a system of inequalities, not a Riccati equation, and by Lemma 4.14 it is equivalent to the uniform convexity that other indefinite mean-field works assume outright.

The paper proves these results on paper; none of them has a machine-checked proof. A formal proof would also produce reusable infrastructure absent from Mathlib: Itô's formula for quadratic functionals of linear SDEs, filtering identities under observation filtrations, and indefinite Riccati theory.

Difficulty

The standard $\varepsilon$-Nash argument bounds the cost gap uniformly over deviations with bounded $\mathbb E\int|u^i|^2$. With positive weights that bound comes for free, because a profitable deviation has bounded cost and the cost is coercive. With indefinite weights the cost is not coercive, so the a-priori bound (44) must be derived. The paper passes to the compensated cost $\mathcal J^P_i$ and uses the uniform convexity of $J^P_i$ together with $N$-dependent approximation errors. In addition, the observation filtrations depend on the controls, so the admissible sets are defined through the control-free observations (backward separation). The conditional law of large numbers under common noise requires conditional independence given $W^0$.

Formalization scope

Time is $\mathbb R_{\ge0}$ with only $[0,T]$ read. Vectors are Fin n → ℝ and matrices Matrix (Fin n) (Fin m) ℝ. One standard Brownian motion of dimension $1+2Nd$ carries $W^0,W^i,\bar W^i$, and its natural filtration is the full information $\mathcal F$. SDEs and BSDEs are strong solutions in the sense of the published Peng1990_SMP_Stochastic definitions. Statements quantify over all solution processes. Observation σ-algebras are augmented by null sets. Riccati and ODE solutions are absolutely continuous and satisfy their equations almost everywhere. The decentralized profile is characterized by optimality in (MFD) and the consistency condition $x^0=\mathbb E[\bar X^i|\mathcal F^\theta]$, $u^0=\mathbb E[\bar u^i|\mathcal F^\theta]$, not by the feedback formula.

Several printed formulas are corrected, each recorded on its item: the observation (11), the transpose in (18), $M^P$ in (23), $\bar\Sigma$, the diffusion in (39), and three abbreviations of $\mathcal J^P_i$ (p.17). Costs are Bochner integrals, finite for every admissible control.

A trivializing encoding is ruled out: the goal quantifies over every probability space and every profile, with $C$ and $N_0$ chosen first, and its hypotheses are satisfiable (a verification file exhibits coefficients satisfying (H1)–(H2) with $P\equiv0$ a relaxed compensator). Contributions toward Itô's formula for $\langle P_tX_t,X_t\rangle$, monotone FBSDE solvability, and conditional LLN rates are reusable beyond this mission.

Selected references

• T. Chen, T. Nie, Z. Wu, Indefinite Linear-Quadratic Partially Observed Mean-Field Game, arXiv:2508.01568v1, 2025. https://arxiv.org/abs/2508.01568
• M. Huang, P. E. Caines, R. P. Malhamé, Large-population cost-coupled LQG problems with nonuniform agents: individual-mass behavior and decentralized ε-Nash equilibria, IEEE Trans. Autom. Control 52(9), 2007. https://doi.org/10.1109/TAC.2007.904450
• S. Chen, X. Li, X. Y. Zhou, Stochastic linear quadratic regulators with indefinite control weight costs, SIAM J. Control Optim. 36(5), 1998. https://doi.org/10.1137/S0363012996310478
• J. Sun, X. Li, J. Yong, Open-loop and closed-loop solvabilities for stochastic linear quadratic optimal control problems, SIAM J. Control Optim. 54(5), 2016. https://doi.org/10.1137/15M103532X
• S. Peng, A general stochastic maximum principle for optimal control problems, SIAM J. Control Optim. 28(4), 1990. https://doi.org/10.1137/0328054

Motivation

When a seller has several different indivisible objects and buyers value bundles additively, the simplest selling procedure is to run one sealed-bid second-price auction per object. The New Zealand government sold cellular management rights tenders this way in 1990 (Remark 3 of Basu–Mukherjee, citing Mueller). Basu and Mukherjee ask which normative axioms single this procedure out among all strategy-proof direct mechanisms when buyers want more than one object (no unit demand). Their answer is an equivalence between an ethical axiom, anonymity in welfare, and efficiency, for strategy-proof mechanisms that never leave an object unsold.

The single-object version of this question is classical: Holmström (1979) showed that efficient strategy-proof mechanisms on smoothly connected domains are Groves mechanisms. The multi-object additive setting with strategy-proofness alone admits a much larger class of mechanisms, which is what makes the characterization informative.

Setting

There are buyers $N=\{1,\dots,n\}$ and objects $M=\{1,\dots,m\}$. Buyer $i$ has a valuation $v_i^k>0$ for each object $k$; a profile $v$ is the $n\times m$ matrix of these values, and $\mathcal V$ is the set of positive profiles. A direct mechanism $\mu=(d,p)$ maps every profile to a decision matrix $d(v)\in\{0,1\}^{n\times m}$ ($d_i^k(v)=1$ iff $i$ is sold $k$; each object to at most one buyer) and prices $p_i(v)\ge 0$. Buyer $i$ with true valuation $x$ gets quasilinear utility $u(\mu_i(v);x)=d_i(v)^\top x-p_i(v)$.

Every mechanism is regular: (i) a buyer who wins nothing pays nothing; (ii) a small change of $v_i^k$ alone never changes $i$'s decisions on the other objects. The axioms are:

• SP: truthful reporting maximizes each buyer's utility whatever the others report;
• AS (agent sovereignty): each buyer can win or lose each object by changing its own report for that object;
• AN (anonymity in welfare): for every permutation $\pi$ of buyers, $u(\mu_i(v);v_i)=u(\mu_{\pi i}(\pi v);v_i)$ with $(\pi v)_t=v_{\pi^{-1}(t)}$;
• EFF: $d(v)$ maximizes $\sum_i d_i^\top v_i$ over all decision matrices;
• no wastage: every object is sold at every profile.

The Lean development names these IsRegular, SP, AS, AN, EFF, SellsAll, on top of the general direct mechanism MechanismDesign.VCG.DirectMechanism.

Formalization targets

Goal: Theorem 4

For every regular, strategy-proof, agent-sovereign mechanism that sells all objects at all profiles,

$$\mu \text{ satisfies AN} \iff \mu \text{ satisfies EFF}.$$

The goal is stated for all $n,m$ and without the paper's continuity hypothesis.

Milestones

1. The price sandwich (4.2): for SP mechanisms, $v_i^\top\Delta d_i\le \Delta p_i\le v_i'^\top\Delta d_i$; equal bundles have equal prices.
2. Theorem 1: with one buyer, SP and AS hold iff the mechanism posts a positive price $T^k$ per object.
3. Theorem 2: SP and AS hold iff there are positive thresholds $T_i^k(v_{-i})$ with $d_i^k=1$ above, $0$ below, and $p_i=\sum_{k\text{ won}}T_i^k$.
4. Footnote 22: truthful utility is $\sum_k (v_i^k-T_i^k(v_{-i}))^+\ge 0$.
5. Proposition 2 (corrected): under AN, $T_{\pi i}^k((\pi v)_{-\pi i})=T_i^k(v_{-i})$.
6. Proposition 1 (corrected, $n\ge2$): under AN, a winner of a column of equal bids $x$ has threshold $x$.
7. Necessity: under AN and no wastage, $T_i^k(v_{-i})=\max_{j\ne i}v_j^k$.
8. Holmström step: EFF in $\Gamma_{M,N}$ forces Definition 7's Pivotal payments.
9. Pivotal utility is $\sum_{k\text{ won}}(v_i^k-\max_{j\ne i}v_j^k)$, and the Pivotal mechanism is anonymous.
10. The Pivotal mechanism with the least-index tie-break is regular, SP, AS, continuous, efficient, anonymous and sells everything ($n\ge2$).

Significance

Theorem 4 gives an axiomatic justification for selling heterogeneous objects by separate second-price auctions: among strategy-proof, agent-sovereign, no-wastage mechanisms, treating buyers anonymously in welfare is the same as allocating efficiently, and by Holmström's theorem the only such mechanism is the Pivotal (Clarke) mechanism. Theorem 2 is a reusable characterization of strategy-proof multi-object mechanisms with additive valuations as threshold (personalized posted-price) mechanisms.

The result is proved on paper; no machine-checked proof of it or of Theorem 2 is known. A formal development also settles several points of the printed text: the literal Definition 4 (continuity) is satisfied by no mechanism in $\Gamma_{M,N}$, Proposition 2 and Theorem 3 fail as printed (a two-buyer counterexample is recorded in the milestones), Proposition 1 needs $n\ge 2$, and Theorem 4 holds without continuity, which answers the paper's question on p.25 about the independence of continuity in the negative.

Difficulty

The obvious route through the paper's appendix goes via Theorem 3 ("continuous mechanisms have thresholds depending only on column $k$"), which is false; any proof must instead work with thresholds that may a priori depend on all of $v_{-i}$. The step from strategy-proofness to thresholds (Theorem 2) is the technical core: it needs regularity (ii) to decouple the objects (without it, a single buyer facing a bundle discount is SP and AS but has no threshold form), monotonicity from the price sandwich, and a squeeze of prices across each threshold. The anonymity argument then has to extract equality of threshold vectors from equality of the piecewise-linear utilities $\sum_k (x_k-a_k)^+$, and the no-wastage hypothesis has to be used together with feasibility to pin the thresholds from both sides.

Formalization scope

Buyers are Fin n, objects Fin m (paper index = Lean index + 1). Decisions are Bool; a decision matrix is feasible when each column has at most one true (the paper's "column sums to 1" is read as $\le 1$, which coincides with it under no wastage). Profiles are Fin n → Fin m → ℝ and positivity is a hypothesis (PosProfile) in every axiom rather than a subtype; values of a mechanism at non-positive profiles are irrelevant. Thresholds are functions of the whole profile that ignore row $i$. $\pi v$ is fun t => v (π.symm t). The highest competing bid is a real supremum over $j\ne i$, used only with $n\ge 2$. Continuity (used only in milestone 10) is read as indifference at the price the mechanism charges for the flipped bundle.

A trivializing formalization is ruled out: the goal's hypothesis set is shown inhabited by milestone 10 (the Pivotal mechanism), and the axioms are stated over feasible decisions, so the lower bound on thresholds cannot be bypassed by selling an object twice.

The development needs only finite sums, permutations of Fin n, and elementary real analysis (connectedness of $(0,\infty)$ for regularity (ii), limits for continuity). Theorem 2 and the anonymity-of-thresholds lemma are reusable for other multi-object mechanism-design missions. Proofs of any milestone, and alternative proofs of the goal that bypass milestones, are welcome.

Selected references

• R. Basu, C. Mukherjee, Strategyproof multidimensional mechanism design without unit demand, IIM Calcutta Working Paper Series WPS No 875, April 2022. Published as Strategy-Proof Multidimensional Mechanism Design, Mathematics of Operations Research, 2024. https://doi.org/10.1287/moor.2022.0324
• B. Holmström, Groves' scheme on restricted domains, Econometrica 47(5), 1137–1144, 1979. https://doi.org/10.2307/1911954
• E. H. Clarke, Multipart pricing of public goods, Public Choice 11, 17–33, 1971. https://doi.org/10.1007/BF01726210
• W. Vickrey, Counterspeculation, auctions, and competitive sealed tenders, Journal of Finance 16(1), 8–37, 1961. https://doi.org/10.1111/j.1540-6261.1961.tb02789.x

Motivation

Hotels, airlines and retailers increasingly let customers pay with loyalty points from a third-party program: a consumer either pays the cash price $p$ or redeems a fixed number $q$ of points, and for every reward sale the seller receives a reimbursement $R$ from the point issuer. A seller with limited inventory and a finite selling season must then set its cash price knowing that some customers will switch from cash to points and that others, priced out in cash, will still buy with points. Chung, Ahn and Chun (MSOM 2022; working paper SSRN 3426903) embed this consumer choice in the classical finite-horizon dynamic pricing model of Gallego and van Ryzin (Management Science 1994) and ask how accepting points changes the optimal price. Their answer, Proposition 1, is that the optimal price is pulled strictly toward the reimbursement rate.

Setting

A seller holds $y$ units with $t$ periods to go. In each period at most one consumer arrives, with probability $\lambda\in(0,1)$. The consumer has a reservation price $V$ with distribution $F$ and density $f$, and a perceived point value $\Theta\ge0$ with distribution $G$ and density $g$; $q$ points are worth $\theta q$ to her. With probability $\bar\beta\in[0,1]$ she holds at least $q$ points (a reward consumer) and chooses the best of $v-p$, $v-\theta q$ and $0$; otherwise (probability $\beta=1-\bar\beta$) she chooses the better of $v-p$ and $0$. The three attributes are independent. Write $\bar F=1-F$, $\bar G=1-G$ and

$$I(p)=\int_0^{p/q}\bar F(qx)\,dG(x),$$

the probability that a reward consumer buys with points.

The seller's value function satisfies $V_0(y)=0$, $V_t(0)=0$ and, for $t,y\ge1$, the optimality equations (1)

$$V_t(y)=\max_{p\ge0}J_t(p,y),$$ $$\begin{aligned}J_t(p,y)={}&\lambda\bar\beta\Big[\bar F(p)\bar G(p/q)\big(p+V_{t-1}(y-1)\big)+I(p)\big(R+V_{t-1}(y-1)\big)+\big(1-\bar F(p)\bar G(p/q)-I(p)\big)V_{t-1}(y)\Big]\\&+\lambda\beta\Big[\bar F(p)\big(p+V_{t-1}(y-1)\big)+F(p)V_{t-1}(y)\Big]+(1-\lambda)V_{t-1}(y).\end{aligned}$$

The marginal value of inventory is $\Delta_t(y)=V_t(y)-V_t(y-1)$. An optimal price $p^*_t(y)$ maximizes $J_t(\cdot,y)$ over $p\ge0$. The one-period blackout price $p^c_t(y)$ maximizes, over all real $p$, the objective of (3),

$$J^c_t(p,y)=\lambda\bar F(p)\big(p+V_{t-1}(y-1)\big)+\big(1-\lambda\bar F(p)\big)V_{t-1}(y),$$

the price the seller would charge if points were refused in period $t$ only, with the same continuation values.

Theorem 1 of the paper assumes A1 ($F$ and $G$ have an increasing failure rate), A2 (the hazard of $V$ dominates the hazard of the point worth $q\Theta$) and A3 (the ratio of the hazard of $V$ to the hazard of the point channel, $\frac{f(p)/\bar F(p)}{(\bar\beta g(p/q)/q)/(1-\bar\beta G(p/q))}$, is non-decreasing).

Formalization targets

Goal: Proposition 1 (corrected)

Under A1–A3, regular densities and $\bar\beta>0$, for $t,y\ge1$ with $\bar F(\Delta_{t-1}(y))>0$: both maximizers exist, and for every optimal price $p^*$ and every blackout price $p^c$ with $g(p^c/q)>0$,

$$p^c<R\ \Longrightarrow\ p^c<p^*<R\quad(\text{when }\bar\beta<1\text{ or }\bar F(R)>0),\qquad R<p^c\ \Longrightarrow\ R<p^*<p^c.$$

Milestones

1. Eq. (2): $J_t(p,y)=\lambda\bar\beta\big[\bar F(p)\bar G(p/q)(p-\Delta)+I(p)(R-\Delta)\big]+\lambda\beta\bar F(p)(p-\Delta)+V_{t-1}(y)$ with $\Delta=\Delta_{t-1}(y)$.
2. Eq. (7): the derivative of $J_t(\cdot,y)$ and its factored form $\lambda(1-\bar\beta G(p/q))\bar F(p)\big[1-\tfrac{f(p)}{\bar F(p)}(p-\Delta)-\tfrac{\bar\beta g(p/q)/q}{1-\bar\beta G(p/q)}(p-R)\big]$.
3. Theorem 1 (corrected): when $\bar\beta<1$ or $\bar F(R)>0$, a unique optimal price, positive and satisfying the first-order condition.
4. Eq. (22) (corrected): the blackout problem has a unique maximizer $p^c>\Delta$, with $1-\tfrac{f(p^c)}{\bar F(p^c)}(p^c-\Delta)=0$.

Significance

Proposition 1 refutes the intuition that adding a sales channel must raise the price: accepting points raises the optimal price when the reimbursement exceeds the blackout price and lowers it otherwise, and never past $R$. The paper's comparative statics in inventory and time (Corollary 2) and in the reward fraction and reimbursement (Proposition 2) are derived from it. Theorem 1 is a unimodality result for a revenue function in which cash and point purchases are imperfect substitutes; it extends the classical fact that an increasing failure rate makes a single-channel revenue unimodal (Ziya, Ayhan and Foley, Operations Research 2004; Lariviere, Operations Research 2006).

The results are proved in the paper; none is formalized. A complete development would give a machine-checked unimodality theorem for a two-channel pricing objective with a Stieltjes-integral term, which no library currently contains.

Checking the statements against the model turned up three necessary corrections, all stated in the Lean.

• $\bar F(\Delta_{t-1}(y))>0$ is needed by Theorem 1, (22) and Proposition 1. With $F=U[0,1]$, $G=U[0,2]$, $q=1$, $\bar\beta=1$, $\lambda=1/2$, $R=10$ and $(t,y)=(2,1)$, every printed assumption holds and $\Delta_1(1)\approx1.26$, so every $p\ge1$ maximizes both $J_2(\cdot,1)$ and (3).
• $\bar\beta>0$ and $g(p^c/q)>0$ are needed by Proposition 1. With $F=U[0,2]$, $G=3+\mathrm{Gamma}(3,1)$, $q=1$, $\bar\beta=0.7$, $\lambda=1/2$, $R=1.5$ and $t=y=1$, no consumer ever redeems, so $p^*=p^c=1<R$.
• $\bar\beta<1$ or $\bar F(R)>0$ is needed by Theorem 1 and by case (a) of Proposition 1. With $F=U[0,100]$, $G=U[0,10]$, $q=10$, $\bar\beta=1$, $\lambda=1/2$, $R=250$ and $t=y=1$, every assumption above holds. But $J_1(\cdot,1)$ increases up to the top of $F$'s support and is constant beyond it, so every $p\ge100$ is optimal (including $p^*=300>R$), while $p^c=50$. When every consumer is a reward consumer and $R$ exceeds every reservation price, pricing out all cash buyers can be optimal.

A2 is printed as $f(p)/\bar F(p)\ge g(p/q)/\bar G(p/q)$. It is read with the hazard of $q\Theta$, $g(p/q)/(q\bar G(p/q))$. The proof of Theorem 1 replaces $f/\bar F$ by exactly this quantity, and Corollary 1 speaks of the "$q$ point-worth distribution". The paper's own Figure 2 instance ($F=U[0,100]$, $G=U[0,10]$, $q=10$) violates the printed form and satisfies the read form with equality.

Difficulty

The revenue $J_t(\cdot,y)$ is a sum of three terms, each unimodal in $p$ under A1, but the sum can be bimodal (the paper's Appendix B), so unimodality of the summands does not settle Theorem 1. The printed proof of Theorem 1 first restricts attention to prices $p\ge\Delta_{t-1}(y)$, arguing that a lower price would make the value function decrease in $t$. Nothing in the model gives $V_t(y)\ge V_{t-1}(y)$: reward sales cannot be refused, and when $R<\Delta_{t-1}(y)$ they lose value. The case $p<\Delta_{t-1}(y)$ is therefore open in the printed argument. The statement is kept at full strength: an extensive numerical search over exponential, uniform, truncated-normal, Weibull and Gamma instances found no counterexample. The domain of prices is unbounded, so the existence of a maximizer is not automatic either.

Formalization scope

All declarations live in the namespace PointRedemption. The model is a structure Params holding $\lambda$ (lam), $q>0$, $\bar\beta\in[0,1]$ (βbar), $R\ge0$, and the laws μV, μΘ as probability measures with nonnegative densities f, g (via volume.withDensity), with $\Theta\ge0$. $\bar F$, $\bar G$ and the IFR property are the published LariviereIGFR.Char.survival and IsIFR. $I(p)$ is the integral of $\bar F(qx)$ against μΘ over $[0,p/q]$. $V_t(y)$ is the supremum over $[0,\infty)$ in (1), and $t$ counts periods to go with no horizon. Optimal and blackout prices are quantified maximizers (IsMaxOn on $[0,\infty)$ and on $\mathbb R$), never closed forms or roots of a first-order condition. Defining $p^c$ by (22) or $p^*$ by (21) would make the goal an algebraic manipulation, and the goal includes the existence of both maximizers, so it cannot hold vacuously. A2 includes $\bar G(p/q)>0$ and A3 is read where its ratio is a finite positive real, so Lean's $x/0=0$ cannot satisfy them where the paper's quantities are infinite. The densities are assumed differentiable at the prices in play, as the paper's use of $f'$ and $g'$ requires.

Needed infrastructure includes the following:

• the fundamental theorem of calculus for a cdf at a point of continuity of the density;
• differentiation of a parametric Stieltjes integral;
• the exponential tail of an IFR law, which bounds $p\bar F(p)$;
• the monotonicity of $V_t(y)$ in $y$, which gives $\Delta_{t-1}(y)\ge0$;
• a sign analysis of the derivative (7).

The IFR facts are reusable beyond this mission. Proofs of any milestone are welcome, as are counterexamples to the printed restriction $p\ge\Delta_{t-1}(y)$.

Selected references

• H. Chung, H.-S. Ahn, S. Y. Chun, Dynamic Pricing with Point Redemption, Manufacturing & Service Operations Management, 2022. https://doi.org/10.1287/msom.2021.1067 (working paper: KAIST WP KCB-WP-2019-013, https://ssrn.com/abstract=3426903)
• G. Gallego, G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8), 1994. https://doi.org/10.1287/mnsc.40.8.999
• S. Ziya, H. Ayhan, R. D. Foley, Relationships among three assumptions in revenue management, Operations Research 52(5), 2004. https://doi.org/10.1287/opre.1040.0134
• M. A. Lariviere, A Note on Probability Distributions with Increasing Generalized Failure Rates, Operations Research 54(3), 2006. https://doi.org/10.1287/opre.1060.0282

Motivation

The newsvendor problem is the basic model of ordering under uncertain demand: a quantity $y$ is ordered before the demand $z$ is seen, and the cost $\Psi(y,z) = h(y-z)^+ + b(z-y)^+$ charges $h$ per unsold unit and $b$ per unit short. In practice the order can depend on observed features $x$ (weather, prices, store characteristics), so the decision is a policy $f$ mapping features to orders. Learning such a policy from data is a standard problem in data-driven operations management (Ban and Rudin 2019).

Minimizing the empirical cost over all policies is degenerate: it only fixes $f$ on the observed feature values $\hat x_k$ and leaves it arbitrary elsewhere. Zhang, Yang and Gao instead minimize the worst-case expected cost over a Wasserstein ball of distributions around the empirical distribution. This is an infinite-dimensional, adjustable distributionally robust problem: the inner adversary chooses a distribution, the outer decision maker a whole function. Their Theorem 1 (Zhang, Yang and Gao) solves it in closed form.

Setting

The data are $K \ge 1$ distinct feature values $\hat x_1,\dots,\hat x_K$ in a feature space $\mathcal X$ with distance $\|x-x'\|$, and for each $k$ a list of $n_k \ge 1$ demand observations $\hat z_{k1},\dots,\hat z_{kn_k} \in \mathcal Z = \mathbb R_+$, with $n = \sum_k n_k$. The empirical distribution is $\widehat{\mathbb P} = \frac1n\sum_{k,i}\delta_{(\hat x_k,\hat z_{ki})}$, and $\widehat{\mathcal X} = \{\hat x_k\}$ is the set of observed features. Throughout, $b > 0$ and $0 \le h \le b$.

The type-1 Wasserstein distance between distributions on $\mathcal X \times \mathcal Z$ is

$$\mathcal W(\mathbb P,\mathbb Q) = \inf_{\gamma\in\Gamma(\mathbb P,\mathbb Q)} \mathbb E_\gamma\big[\|\tilde X - X\| + |\tilde Z - Z|\big],$$

the infimum over couplings $\gamma$ of $\mathbb P$ and $\mathbb Q$. With radius $\rho \ge 0$, the robust problem is

$$v_P = \inf_{f\in\mathcal F}\ \sup\Big\{\mathbb E_{\mathbb P}[\Psi(f(X),Z)] : \mathbb P\in\mathcal P_1(\mathcal X\times\mathcal Z),\ \mathcal W(\mathbb P,\widehat{\mathbb P})\le\rho\Big\}, \tag{P}$$

where $\mathcal F$ is the set of all measurable policies $\mathcal X \to \mathcal Z$ and $\mathcal P_1$ the distributions with finite first moment. The in-sample problem $(\widehat{\mathrm P})$, with value $v_{\widehat P}$, is the same problem with $\mathcal X$ replaced by $\widehat{\mathcal X}$: a minimization over vectors $(\hat f(\hat x_k))_k \in \mathbb R_+^K$.

Given an in-sample policy $\hat f$, the Shapley extension is $f(x) = \min_j\max_k A_{jk}(x)$, where $A_{kk}(x) = \hat f(\hat x_k)$ and, for $j\ne k$, $A_{jk}(x)$ is the inverse-distance interpolation

$$A_{jk}(x) = \frac{\|x-\hat x_k\|}{\|x-\hat x_j\|+\|x-\hat x_k\|}\hat f(\hat x_j) + \frac{\|x-\hat x_j\|}{\|x-\hat x_j\|+\|x-\hat x_k\|}\hat f(\hat x_k).$$

Formalization targets

Goal: Theorem 1

$$v_P = v_{\widehat P},\qquad (\widehat{\mathrm P}) \text{ attains its minimum},$$

and for every minimizer $\hat f^*$ of $(\widehat{\mathrm P})$ its Shapley extension satisfies $\min_j\max_k A_{jk}(x) = \max_k\min_j A_{jk}(x)$ for all $x$, is measurable and nonnegative, and attains $v_P$. Every $\rho \ge 0$ is covered, including $\rho = 0$.

Milestones

• Lemma 1 (p.8): the extension (i) interpolates $\hat f$, (iii) stays between $\min\hat f$ and $\max\hat f$, (iv) has Lipschitz constant at most the discrete Lipschitz constant of the data, and (ii) satisfies $\Phi(f(x)) - \|x-\hat x_k\| \le \max_j\{\Phi(\hat f(\hat x_j)) - \|\hat x_j-\hat x_k\|\}$ for every convex $\Phi$, eq. (5).
• Lemma EC.2 with its two ingredients: a $2\times2$ matrix without saddle point is diagonally dominant, and Shapley's theorem that a matrix whose $2\times2$ submatrices all have saddle points has one.
• Lemma EC.1 (strong duality $v_P^f = v_D^f$ for each policy, stated for $\rho>0$; see below) and the in-sample duality $(\widehat{\mathrm P}) = (\widehat{\mathrm D})$, which holds for all $\rho\ge0$.
• The three steps of the proof of Theorem 1 on p.ec4 (the cases $\lambda>0$ and $\lambda=0$, and $v_D = v_{\widehat D}$).
• (EC.2) and Lemma EC.3 from Appendix B, which give attainment of $(\widehat{\mathrm P})$.

Significance

Theorem 1 reduces an optimization over all measurable functions on $\mathcal X$ to a finite-dimensional robust problem in $K$ variables, followed by an explicit formula. The optimal policy is defined everywhere, Lipschitz, bounded by the in-sample orders, and computable from pairwise distances. In the paper the in-sample problem is further shown to be a Lipschitz-regularized empirical problem and a linear program (Propositions 1 and 2), and the extension leads to generalization bounds (Proposition 3). Closed-form optimal decision rules for adjustable distributionally robust problems over unrestricted policy classes are rare; the usual approach restricts to affine or otherwise parametric rules.

The result is proved in the paper; this mission formalizes it. As far as is known, none of the ingredients (the Shapley extension, its saddle point, the finite-support Wasserstein duality for this loss) has a machine-checked proof. Shapley's $2\times2$ saddle-point theorem and finite-support Wasserstein duality are general tools that other missions can reuse.

Difficulty

The natural first idea is to extend $\hat f^*$ by any Lipschitz extension (McShane–Whitney, nearest neighbour). This does not give optimality: what is needed is property (5) for every convex $\Phi$ simultaneously, a convexity-aware comparison with every observed point, and the Shapley extension is built so that each pairwise interpolation $A_{jk}$ satisfies it. The second obstacle is that the minimax formula only defines a policy once the saddle point exists; this needs Shapley's combinatorial theorem (Shapley 1964) plus a sign argument on four products of inequalities.

On the duality side, the strong duality of Lemma EC.1 must hold for every measurable policy, including discontinuous ones, so arguments that rely on upper semicontinuity of the loss do not apply directly. Attainment of $(\widehat{\mathrm P})$ is not automatic either: the feasible set $\mathbb R_+^K$ is unbounded, and compactness comes from the truncation of Lemma EC.3.

Formalization scope

The feature space is a second-countable metric space with its Borel σ-algebra (the paper's subset of $(\mathbb R^d,\|\cdot\|)$ is one). Demands live in ℝ≥0. Policies are functions X → ℝ that are measurable and nonnegative. The in-sample feature set is indexed by Fin K through the injective map $k\mapsto\hat x_k$, and an in-sample policy is a vector y : Fin K → ℝ with y ≥ 0. All optimal values are in ℝ≥0∞. The Wasserstein cost is the sum $\|x-x'\|+|z-z'|$, written out explicitly, because Lean's default metric on a product is the maximum. The worst case is a supremum over every probability measure with finite first moment in the ball, and $v_P$ is an infimum over all measurable nonnegative policies. Restricting either to finitely supported measures or to Lipschitz policies would make Theorem 1 a different statement. The diagonal $A_{kk} := \hat f(\hat x_k)$ follows Lemma 1 (S); the single formula of Theorem 1 is $0/0$ there.

Lemma EC.1 as printed allows $\rho = 0$, where it fails: for $f(x)=x^2$ on $\mathcal X=\mathbb R$ with one observation at the origin, the primal value is $0$ and the dual value is $+\infty$. The milestone therefore assumes $\rho>0$. The goal keeps $\rho\ge0$, since its proof needs only weak duality on $\mathcal X$ and the in-sample duality, which holds at $\rho = 0$.

A complete development needs: the newsvendor cost and its convexity, couplings and transport costs (the coupling set is the published WassersteinDRO.StrongDuality.couplings), finite-support Wasserstein duality (Gao and Kleywegt, Mohajerin Esfahani and Kuhn), the Shapley matrix and its saddle point, and a compactness argument in $\mathbb R^K\times\mathbb R$. Contributions are welcome at every milestone; Shapley's theorem and the duality lemmas are the most reusable.

Selected references

• L. Zhang, J. Yang, R. Gao, Optimal Robust Policy for Feature-Based Newsvendor, author manuscript (2022); published in Management Science (2024). https://doi.org/10.1287/mnsc.2023.4810
• L. S. Shapley, Some topics in two-person games, in Advances in Game Theory, Annals of Mathematics Studies 52, Princeton University Press, 1964. https://doi.org/10.1515/9781400882014
• R. Gao, A. Kleywegt, Distributionally robust stochastic optimization with Wasserstein distance, Mathematics of Operations Research, 2023. https://doi.org/10.1287/moor.2022.1275
• P. Mohajerin Esfahani, D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric, Mathematical Programming, 2018. https://doi.org/10.1007/s10107-017-1172-1
• J. Blanchet, K. Murthy, Quantifying distributional model risk via optimal transport, Mathematics of Operations Research, 2019. https://doi.org/10.1287/moor.2018.0936
• G.-Y. Ban, C. Rudin, The big data newsvendor: practical insights from machine learning, Operations Research, 2019. https://doi.org/10.1287/opre.2018.1757

Repair facilities and the value of emergency repairs

A firm that maintains capital goods (aircraft, medical scanners, lithography machines) keeps spare parts and runs a repair shop. When a part fails, it is replaced from stock if possible. Otherwise a machine waits, and the firm pays a backorder cost. The firm must choose how many spares of each part type to hold, which failed part to repair next, and when to pay for an outside emergency repair. Özkan and van Houtum study this joint control problem in the heavy-traffic regime of a closed repairable-parts network (SSRN 3784144; published later in Operations Research). This mission works from the SSRN copy.

The limiting problem is solved exactly, and the answer is a decision rule: emergency repairs are worth using exactly when the least backorder saving per unit of repair time exceeds the least emergency cost per unit of repair time.

Setting

There are $n\ge1$ part types (SKUs), with repair rates $\mu_i>0$, limiting breakdown rates $\lambda_i>0$, costs $b_i,c_i,h_i>0$, a drift $\theta\le0$ and a variance $\Sigma>0$. Let $X$ be a Brownian motion with drift $0$ and variance $\Sigma$, started at $0$. An inventory vector $S\in\mathbb R^n_+$ is fixed.

The equivalent workload formulation (EWF) chooses a workload $W\ge0$, an idleness process $I$, an emergency repair process $E$, and an allocation $a(t)\in\mathcal A(W(t))$, where

$$\mathcal A(w)=\Big\{q\in\mathbb R^n_+:\sum_i q_i/\mu_i=w\Big\},$$

subject to

$$W(t)=X(t)+\theta t-\sum_i\frac{\lambda_i}{\mu_i}\int_0^t(a_i(s)-S_i)^+\,ds+I(t)-E(t).$$

The processes $I$ and $E$ start at $0$, are nondecreasing, càdlàg and adapted. Write $b_j\mu_j/\lambda_j=\min_i b_i\mu_i/\lambda_i$ and $c_k\mu_k=\min_i c_i\mu_i$. The objective is

$$\limsup_{t\to\infty}\ \sum_i h_iS_i+\frac1t\,\mathbf E\Big[\sum_i b_i\int_0^t(a_i(s)-S_i)^+\,ds+c_k\mu_kE(t)\Big].$$

The candidate solution comes from the Bellman system (13): find $(f,B,\gamma)$ with $f\in C^2$, $B>0$, $\gamma\ge0$ such that

$$\tfrac12\Sigma f''(w)+\theta f'(w)+\min_{q\in\mathcal A(w)}\sum_i\Big(b_i-\frac{\lambda_i}{\mu_i}f'(w)\Big)(q_i-S_i)^+=\gamma\quad\text{on }[0,B],$$

with $\ge\gamma$ for $w>B$, $0\le f'\le c_k\mu_k$ on $\mathbb R_+$, $f'(0)=0$ and $f'(B)=c_k\mu_k$.

The barrier policy reflects the workload at $0$ and at $B$ and allocates by $q^*$, which backorders only one SKU, $\kappa(w)\in\arg\min_i\{b_i\mu_i-\lambda_if'(w)\}$, above total inventory.

Formalization targets

Goal: Theorem 2

Suppose $b_j\mu_j/\lambda_j>c_k\mu_k$. Then (13) has a solution, and for each solution a barrier policy with upper barrier $B$ exists, and

$$\lim_{t\to\infty}\frac1t\,\mathbf E\Big[\sum_i b_i\int_0^t(a_i(s)-S_i)^+\,ds+c_k\mu_kE(t)\Big]=\gamma$$

under it, while every EWF-feasible solution with the same $S$ has objective at least $\sum_ih_iS_i+\gamma$.

Milestones

• The allocation problem: Lemma 1.
• The initial value problem for $f'$: Lemmas A.3.1, A.3.2, A.3.3, A.3.6, A.3.8, A.3.9.
• The Bellman system: Lemma 2 Part ii.
• The regulators: Lemmas A.4.3 and 4.
• The verification argument: (A.58), (A.45)–(A.47), (A.62), (A.63).

Significance

Theorem 2 identifies an explicit optimal policy and its cost for a singular ergodic control problem with a state-dependent drift. The cost is computed by a one-dimensional free-boundary problem, which is what makes the inventory optimization of the paper's §5 tractable.

The result is proved in the paper; no machine-checked proof of it is known to this mission. Formalizing it adds a verification theorem for ergodic singular control with jump controls, a reflected equation with discontinuous monotone drift, and a global analysis of a piecewise linear ODE. These are the recurring pieces of Brownian control problems in operations research. The only other instance on the platform is AtaBarjesteh23.Workload, for a different workload formulation, and its goals are still open.

The formalization also corrects the source. Printed Lemma 4 claims a regulator solution for every càdlàg input, and that is false when $q^*$ makes the drift jump (see Difficulty). The mission states the corrected lemma and the barrier policy almost surely.

Difficulty

The obvious existence argument for the barrier policy fails. The drift $\beta(w)=\sum_i(\lambda_i/\mu_i)(q_i^*(w)-S_i)^+$ jumps upward wherever $\kappa$ changes. The paper patches the regulator over the intervals between jumps. On a path that approaches a jump point $w_0$ from below with slope strictly between the two one-sided values of $\beta$, the workload can neither cross $w_0$ nor stay there. So no solution exists for that path, and existence holds only for almost every Brownian path, where the noise prevents this. Pathwise uniqueness is still true because $\beta$ is nondecreasing on $[0,B]$.

The second difficulty is the competitor class. Feasible solutions need not be Markov, work-conserving or continuous, and $E$ may jump. Expected workload may even grow linearly. Itô's formula alone therefore does not give the lower bound: the jumps of $E$ and $I$ and the growth of $\mathbf E[W(t)]$ need separate treatment.

Formalization scope

Time is indexed by $\mathbb R$, and only $t\ge0$ is constrained. The SKU set is Fin n with $n\ge1$. Costs are computed in $\mathbb R_{\ge0}\cup\{\infty\}$ with lower integrals, so an infinite expectation is $\infty$. The measures $d\ell$ and $du$ are Lebesgue–Stieltjes measures of the path extended by $0$ to negative times. Feasibility requires progressive measurability of the allocation and integrable paths, and it holds for every $\omega$. The filtration satisfies the usual conditions, as in the paper. The published definition AtaBarjesteh23.Workload.IsDriftBM is the Brownian motion.

The allocation $q^*$ is fixed: the fill of OA A.2 when no SKU is backordered, and the largest-$\lambda$ tie-break otherwise. That is the right-continuous choice named on OA p.26. Regulators are stated for $b\le B$, where $f'$ is strictly increasing.

A trivial reading is excluded in three ways. The goal asserts existence of the Bellman solution and of the barrier policy, so it is not conditional on either. The lower bound ranges over all feasible solutions. A path with non-integrable allocation is not feasible, so it cannot gain a junk drift of $0$.

The development needs an Itô formula for processes with finite-variation jump parts, a reflection map on $\mathbb D$, and global ODE comparison arguments. Each is reusable beyond this mission. Contributions to any of them are welcome, and so is a pathwise treatment of the regulator with monotone discontinuous drift.

Selected references

• E. Özkan, G.-J. van Houtum, Joint Inventory and Scheduling Control in a Repair Facility, SSRN 3784144 (2023). https://ssrn.com/abstract=3784144
• E. Özkan, G.-J. van Houtum, Joint Inventory and Scheduling Control in a Repair Facility, Operations Research (2023). https://doi.org/10.1287/opre.2023.2459
• J. M. Harrison, Brownian Models of Performance and Control, Cambridge University Press, 2013. https://doi.org/10.1017/CBO9781139087698
• W. Whitt, Stochastic-Process Limits, Springer, 2002. https://doi.org/10.1007/b97479
• A. Ju. Veretennikov, On strong solutions and explicit formulas for solutions of stochastic integral equations, Math. USSR-Sb. 39 (1981). https://doi.org/10.1070/SM1981v039n03ABEH001518

Motivation

A chance constrained program minimizes a cost while requiring a random constraint to hold with high probability. It models decisions under uncertainty in energy systems, finance, and process and water-quality engineering. Replacing the probability by an empirical frequency over $N$ samples gives the sample average approximation, whose constraint counts the violated samples. This counting function is a 0/1 loss: it is discontinuous, and the resulting problem is NP-hard. The usual remedies are mixed-integer reformulations, or smooth and convex surrogates that change the problem.

Zhou, Pan, Xiu and Li (arXiv:2210.11889v5) work on the 0/1 constraint directly. They compute the projection onto the constraint set, define a stationarity condition from it, and rewrite that condition as a system of equations. A semismooth Newton method, SNSCO, then solves the system. This mission formalizes the local analysis of SNSCO.

Setting

Let $f:\mathbb R^K\to\mathbb R$ and $G:\mathbb R^K\to\mathbb R^{M\times N}$ be continuously differentiable, let $\Omega\subseteq\mathbb R^K$ be nonempty, closed and convex, and let $s\ge 1$ be an integer. For a matrix $Z$, the quantity $\|Z\|_0^+$ counts the columns of $Z$ with a positive entry. The problem (SCO) is

$$\min_{x\in\Omega} f(x)\quad\text{subject to}\quad \|G(x)\|_0^+\le s.$$

With $G(x)=(g(x,\xi_1),\dots,g(x,\xi_N))$ and $s=\lceil\alpha N\rceil$ this is the sample average approximation.

Write $\mathcal S:=\{Z:\|Z\|_0^+\le s\}$. The set $\Pi_{\mathcal S}(Z)$ of nearest points of $\mathcal S$ has a closed form. It is described by a family $\mathbb T(Z;s)$ of column sets, which records the choices of $s$ columns of largest positive part. A point $x^*$ with multiplier $W^*$ is $\tau$-stationary if

$$x^*=\Pi_\Omega\bigl(x^*-\tau[\nabla f(x^*)+\textstyle\sum W^*_{mn}\nabla G_{mn}(x^*)]\bigr),\qquad Z^*\in\Pi_{\mathcal S}(Z^*+\tau W^*),$$

where $Z^*=G(x^*)$. Put $w=(x;\mathrm{vec}(W))$ and $\Lambda=G(x)+\tau W$. For an index set $\mathcal V$, the map $F(w;\mathcal V)$ collects a projected-gradient residual $\varphi(w;\mathcal V)$, the entries of $G(x)$ on $\mathcal V$, and the entries of $W$ off $\mathcal V$. Stationarity becomes $F(w^*;\mathcal V_*)=0$, where $\mathcal V_*$ is the set of zero entries of $Z^*$ in columns of zero maximum.

SNSCO does not know $\mathcal V_*$. At $w^\ell$ it selects $T_\ell\in\mathbb T(\Lambda^\ell;s)$ and $\mathcal V_\ell:=U_{T_\ell}=\{(m,n):n\in T_\ell,\ \Lambda^\ell_{mn}\ge0\}$, takes an element $H^\ell$ of the Clarke generalized Jacobian of $\varphi(\cdot;\mathcal V_\ell)$, and solves a Newton system with a regularization block $-\mu_\ell I$. A backtracking test on $\|G\|_0^+\le(\gamma+1)s$ fixes the step size.

Formalization targets

Goal: Theorem 5

Let $x^*$ be $\tau$-stationary with $0<\tau<\tau_*$, let Assumption 2 hold, and let $\gamma\ge|\Gamma_0^*|/s$. Then there is $\eta>0$ such that every run of SNSCO with $\|w^0-w^*\|<\eta$ takes full Newton steps and satisfies

$$w^\ell\to w^*,\qquad \|w^{\ell+1}-w^*\|=o(\|w^\ell-w^*\|).$$

Under strong semismoothness of $\varphi(\cdot;\mathcal V_*)$ and of $G_{mn}$, $(m,n)\in\mathcal V_*$, the bound improves to

$$\|w^{\ell+1}-w^*\|\le C\|w^\ell-w^*\|^2 .$$

Both clauses hold for every selection of $T_\ell$ and $H^\ell$, with $\eta$ and $C$ chosen before the run.

Milestones

In proof order: the sign of $Z^\downarrow_s$ (9); the closed form of $\Pi_{\mathcal S}$ (Proposition 1); column-wise complementarity (24); the fixed-point inclusion (Proposition 2); the stationary equations (Theorem 4); identification of the active set (Lemma 2); semismoothness of $F(\cdot;\mathcal V)$ (Lemma 3); uniform regularity of the Newton matrix (Lemma 4); and the superlinear and quadratic one-step estimates, (85) and the last display of p.22.

Significance

The theorem gives a local rate for an algorithm that attacks the 0/1 constraint itself, with no surrogate and no integer variables. The projection and the stationary equations are reusable for any problem with a column-counting constraint, including support vector machines and one-bit compressed sensing, which the paper notes as special cases.

The paper proves the result, and this mission adds the machine-checked proof. Two corrections are also recorded in the statements. The sentence of Theorem 5 omits $\tau<\tau_*$, without which it is false at $\tau=\tau_*$. Lemmas 3 and 4 hold only for those $\mathcal V\subseteq\mathcal V_*$ with $W^*_{\overline{\mathcal V}}=0$. As far as known, no result with a varying index set is formalized: the proved nonsmooth Newton theorems on the platform (Qi and Sun 1993 and Qi 1993) fix one system.

Difficulty

The standard Newton argument bounds $F(w^\ell)-F(w^*)-H^\ell(w^\ell-w^*)$ for one fixed map $F$. Here the map $F(\cdot;U_{T_\ell})$ changes with the iterate, so that argument does not apply directly. It needs $F(w^*;U_{T_\ell})=0$ for whichever set the iterate selects, although $U_{T_\ell}$ need not equal $\mathcal V_*$. This identification is where $\tau<\tau_*$ enters. Semismoothness is assumed only for $\varphi(\cdot;\mathcal V_*)$ and must transfer to each $\varphi(\cdot;\mathcal V)$, which involves a Clarke Jacobian of a composition with a non-surjective linear map. The chain rule available there is weaker than the usual inclusion.

Formalization scope

Points live in EuclideanSpace ℝ (Fin K) and matrices in Matrix (Fin M) (Fin N) ℝ, with [NeZero M] so that columns have a maximum. The variable $w$ lives in the Euclidean space on Fin K ⊕ (Fin M × Fin N), and $F$ and $\nabla F_\mu$ are written on that index type, so no block permutation appears. The Clarke Jacobian is the platform's NonsmoothNewton.Shared.clarkeJac. Semismoothness is the paper's (10)–(11), not Qi and Sun's limit form. $\Pi_\Omega$ is a function chosen by Classical.epsilon, and $\Pi_{\mathcal S}$ is a set. The hypothesis $\tau<\tau_*$ is BelowTauStar, with no division and with $\tau_*=+\infty$ when $\|Z^*\|_0^+<s$ or $W^*_{:\Gamma_0^*}=0$. A run has no stopping test, and it is a predicate on sequences, so every selection is covered.

The goal must not be restated for the one-step map, with Lemma 2's conclusion assumed, or for fixed $\mathcal V=\mathcal V_*$. A verification file shows that the run predicate and Assumption 2 are satisfiable on a concrete instance.

Needed infrastructure: the Clarke Jacobian of a Lipschitz map on Euclidean space (nonemptiness, local boundedness and closedness, partly available on the platform) and its behaviour under composition with a linear map. The results on $\Pi_{\mathcal S}$ are elementary and self-contained. Contributions of general lemmas on Clarke Jacobians are welcome.

Selected references

• S. Zhou, L. Pan, N. Xiu, G. Y. Li, A 0/1 Constrained Optimization Solving Sample Average Approximation for Chance Constrained Programming, arXiv:2210.11889v5, 2026. https://arxiv.org/abs/2210.11889v5
• L. Qi, J. Sun, A nonsmooth version of Newton's method, Mathematical Programming 58, 1993. https://doi.org/10.1007/BF01581275
• L. Qi, Convergence analysis of some algorithms for solving nonsmooth equations, Mathematics of Operations Research 18, 1993. https://doi.org/10.1287/moor.18.1.227
• F. H. Clarke, Optimization and Nonsmooth Analysis, SIAM Classics in Applied Mathematics 5, 1990. https://doi.org/10.1137/1.9781611971309