Why fixed design matters for quantile prediction

A conditional quantile describes a level of a response that is exceeded with a specified probability after its explanatory variables are fixed. Such predictions enter inventory decisions when demand depends on prices, promotions, or product characteristics. These explanatory variables may be designed or selected deliberately. Treating their historical values as independent draws from a common distribution can therefore misrepresent the statistical problem. Qi, Cao and Shen (2021) study conditional quantile prediction with deterministic explanatory variables and random innovations.

Their procedure first fits a linear regression and then constructs a distributionally robust prediction from its residuals. A Wasserstein ambiguity set contains probability laws within a specified transportation distance of the empirical residual law. Its usefulness depends on whether the relevant future-response law lies near that center. The concentration result in this mission addresses this question for the full distribution, before any particular quantile or loss is selected.

The regression and probability setting

Fix a finite dimension $p$, a deterministic sequence of feature vectors $x_i\in\mathbb R^p$, and a true coefficient $\beta_0\in\mathbb R^p$. The responses follow

$$Y_i=\beta_0^T x_i+\varepsilon_i.$$

The innovations are independent and identically distributed with a real Borel probability law $\mu$ of mean zero. They satisfy the light-tail assumption

$$A=\int e^{|u|^a}\,\mu(du)<\infty,\qquad a>1,\quad A>1.$$

Neither bounded support nor a density is required. The feature sequence is fixed before observing the innovations, and no separate intercept column is appended. The formal statements also allow a supplied constant feature column, a declared generalization of the source’s no-intercept model.

Let $X_N$ contain the first $N$ feature rows and let $G_N=X_N^T X_N$. The normalized Gram matrices $G_N/N$ converge to a finite nonsingular matrix. A sample size is admissible when it is positive and $G_N$ is nonsingular. At every such size, the ordinary least squares estimator is $\widehat\beta_N=G_N^{-1}X_N^TY$.

For any coefficient $\beta$, let $\widehat P_N(\beta)$ be the uniform empirical law of the residuals $Y_i-\beta^T x_i$. At the true coefficient, this is the empirical innovation law. At the fitted coefficient, it is the surrogate residual distribution. Fix a deterministic prediction vector $c\in\mathbb R^p$. Conditional on the realized training innovations $\omega$, define $P_{\varepsilon'}(\omega)$ as the pushforward of $\mu$ by $u\mapsto u+(\beta_0-\widehat\beta_N(\omega))^Tc$. Thus it describes an independent future innovation shifted by the fitted prediction error. It is not averaged over training realizations.

Formalization targets

The goal is the complete Theorem 2 of Qi, Cao and Shen, supplied PDF/printed page 17. For every $\eta\in(0,1)$, there exists a deterministic nonnegative radius sequence $r_N\to0$ such that, at every admissible sample size,

$$\mu^{\otimes N}\left\{\omega:W_1\big(P_{\varepsilon'}(\omega),\widehat P_N(\widehat\beta_N(\omega))\big)\ge r_N\right\}\le\eta.$$

The radius can depend on the deterministic design, the law, the prediction vector and the confidence level, but never on the observed training vector. Both convergence and the closed upper-tail bound belong to the goal.

Seven milestones follow the dependency order of the source proof. Lemma 5 is represented by the existing, more general Fournier–Guillin empirical concentration theorem, specialized to dimension and transport power one. The new statements preserve Lemma 1's unrestricted dual representation, Lemma 4's variance bound

$$\sigma^2\le (2(A-1))^{1/a},$$

and both conclusions of Lemma 3:

$$0\le H_{ii}\le1,\qquad \operatorname{trace}(H)=\sum_iH_{ii}=p,$$

where $H=X(X^TX)^{-1}X^T$. Lemma 6 compares empirical innovations with fitted residuals at radius $\sqrt{p\kappa/N}/\eta$. Lemma 8 states $W_1(\mu,\mu(\cdot-t))=|t|$ for arbitrary translated real probability laws. Lemma 7 compares the innovation law with the training-conditioned shifted law at radius $\sqrt{\kappa c^TG_N^{-1}c/\eta}$. Both radius-convergence clauses are retained, and $\kappa$ may be any finite variance upper bound as allowed after Lemma 4.

What the concentration statement supplies

The result provides shrinking distributional uncertainty sets for regression residuals fitted on fixed-design data. In the source, this supports the finite-sample loss guarantee and the later consistency analysis. Those downstream claims, the independent tractable reformulation, and the random-design comparison are outside this mission; the selected goal concerns concentration alone. See Qi, Cao and Shen, Sections 4–6.

The formalization supplies concrete definitions of the responses, fitted residual law and training-conditioned target. It reuses published coupling-based Wasserstein and empirical-measure definitions. The existing Fournier–Guillin concentration statement is Open, rather than an already verified proof of the needed tail estimate. The seven new theorem declarations are likewise statement targets, not completed proofs.

Why the residual law needs separate analysis

Ordinary empirical concentration applies to independent samples from one law. Fitted residuals use a coefficient estimated from the same observations, so their coordinates are generally dependent and need not have identical distributions. Furthermore, the target law changes with the realized training sample through the prediction error at $c$. Replacing either law with an unconditional mixture changes the theorem. The fixed-design setting and the distinction between these two random laws are central to the statement in Section 5.2.

Source defects also require explicit treatment. Lemma 7's printed closed-tail assertion fails at $c=0$, because its radius is zero. Lemma 1's unrestricted supremum can include undefined signed integrals. The proof of Lemma 8 uses densities for laws that may be atomic. The proof of Lemma 7 also uses the variance of an absolute error in an uncentered tail bound; a two-sample Rademacher calculation disproves that intermediate inequality. These claims are preserved at their printed strength, with evidence recorded separately; no corrected theorem replaces a source milestone.

Formalization scope and conventions

Real coordinate vectors use finite function types, with indices shifted from one-based paper notation to zero-based finite indices. Dimensions are natural numbers; the source does not explicitly exclude zero, whose additional zero-radius issue in Lemma 6 is recorded separately. Training samples have exactly the finite product law $\mu^{\otimes N}$. The finite-sample bounds quantify over all positive full-rank prefixes, so no condition requires a rank-$p$ matrix with fewer than $p$ rows.

Transport costs and nonnegative moments use extended nonnegative reals. Infinite integrals remain infinite. The light-tail parameter $A$ equals the actual finite exponential moment. Lemma 1 has explicit signed-integral definedness in its conclusion, exposing indeterminate expressions without restricting its probability laws. Translation is a measurable pushforward, including for atomic and infinite-first-moment laws.

Definitions do not assume concentration, an OLS error estimate, or the claimed leverage bounds. The goal does not substitute independent residuals, discrete noise, a fixed coefficient estimate, or sample-dependent radii. Further work can supply proofs or disproofs of the exact targets while retaining these conventions.

Selected references

• Meng Qi, Ying Cao and Zuo-Jun (Max) Shen, Distributionally Robust Conditional Quantile Prediction with Fixed Design, Management Science, 2021. DOI. Citations here use the supplied 36-page artifact, whose PDF and printed page numbers coincide; its SSRN footer differs from the catalog's published-basis label.
• Nicolas Fournier and Arnaud Guillin, On the rate of convergence in Wasserstein distance of the empirical measure, Probability Theory and Related Fields 162, 707–738, 2015. Author preprint.

Motivation

A planner who commits resources before learning their eventual returns can evaluate a decision by how much better another decision would have performed after those returns became known. This absolute regret criterion compares against the best feasible hindsight decision under the same realization of uncertainty. It differs from protecting only the lowest possible profit: the benchmark changes with the realized scenario. Production and transportation decisions provide one application when shipment costs are revealed after production has been chosen. Poursoltani and Delage, supplied pp. 1–4 and 19–20, investigate how two-stage regret models relate to adjustable robust optimization.

The selected claim is their objective-uncertainty absolute-regret reformulation, Proposition 2. Its statement includes both equivalence of optimization problems and transfer of the assumptions used by robust optimization methods. The literal printed statement has a counterexample, described below. Retaining that statement makes the distinction between the displayed model and the proof's intended model explicit.

Setting

A first-stage decision is a real vector $x\in\mathbb R^{n_x}$ selected from $X=\{x:Wx\le v\}$. An uncertain vector $\zeta\in\mathbb R^{n_\zeta}$ ranges over $U=\{\zeta:P\zeta\le q\}$. After its observation, a recourse decision $y\in\mathbb R^{n_y}$ must satisfy $Ax+By\le\psi$. All inequalities are componentwise. Matrices $W,P,A,B$ have respectively $r,s,m,m$ rows and the appropriate decision-space columns; their right-hand sides are $v,q,\psi$. A deterministic vector $c$ prices the first-stage decision, while an affine function $d(\zeta)=D\zeta+d$ prices recourse. Thus realized profit is $c^Tx+d(\zeta)^Ty$. No probability distribution is specified. This is the model of §3.2, equations (8)–(10), supplied p. 7.

Let $Y(x)$ denote the recourse feasible set. The optimal recourse profit is $h(x,\zeta)=\sup_{y\in Y(x)}[c^Tx+d(\zeta)^Ty]$. Hindsight profit also optimizes over the first-stage decision. When profits can be unbounded, subtracting two optimized profits can be ambiguous. The source therefore specifies the nested convention

$$R(x)=\sup_{\zeta\in U}\sup_{\bar x\in X}\sup_{\bar y\in Y(\bar x)}\inf_{y\in Y(x)}[c^T(\bar x-x)+d(\zeta)^T(\bar y-y)].$$

The worst-case absolute regret value is $R^*=\inf_{x\in X}R(x)$. Each bracket is a real number before optimization. Under the source's uniform upper bound on profits, this agrees with the usual hindsight-minus-achieved-profit definition. The source's separate interpretation of an unbounded-below value as zero reported regret does not change the raw objective used here; see §4, supplied p. 8.

Formalization targets

The transformed scenario is $u=(\zeta,\rho)$, with $\rho\in\mathbb R^m$. Its uncertainty set is exactly the printed equation (17):

$$U'=\{(\zeta,\rho):P\zeta\le q,\ B^T\rho=D\zeta+d\}.$$

A policy assigns real vectors $(\lambda(u),\gamma(u))\in\mathbb R^m\times\mathbb R^r$ to every lifted scenario. Feasibility requires, for every $u\in U'$,

$$\lambda(u),\gamma(u)\ge0,\quad A^T\lambda(u)+W^T\gamma(u)=c,\quad B^T\lambda(u)=D\zeta+d.$$

For a fixed $x$, let $V(x)$ be the supremum over feasible policies of

$$\inf_{(\zeta,\rho)\in U'}[c^Tx+(\psi-Ax)^T\rho-\psi^T\lambda(u)-v^T\gamma(u)],$$

and put $V^*=\sup_{x\in X}V(x)$. These are the block constraints and objective of equation (16), supplied pp. 9–10.

Assumption 1 requires a feasible triple with $x\in X$ and $\zeta\in U$; polyhedrality is part of the construction. Assumption 2 requires recourse for every $x\in X$ and every $\zeta\in U$. Under these base hypotheses, the target asserts

$$R^*=-V^*,\qquad \operatorname{argmin}_{x\in X}R(x)=\operatorname{argmax}_{x\in X}V(x).$$

It also explicitly states $R(x)=-V(x)$ for each feasible $x$, the stronger fixed-decision comparison used in Appendix F.3. No optimizer existence is asserted. Assumption 3 requires some scenario of bounded recourse for each $x$; Assumption 4 requires a lower bound on worst-case profit for each $x$; Assumption 5 is a uniform upper bound on all profits. The remaining clauses are

$$(A3\wedge A5)\Rightarrow(A1'\wedge A2'\wedge A3'),\qquad(A3\wedge A5\wedge A4)\Rightarrow A4'.$$

Primed assumptions are evaluated using the transformed pointwise recourse problem. One shared milestone references the already proved general LP-duality theorem for the source's two displayed dependencies: Appendix F.3, equation (31), p. 32, followed by Appendix F.1, equation (27), p. 30. The primary milestone quotation is equation (31); both complete quotations are retained in the ordered, separately paginated source occurrences. Equation (31) identifies hindsight profit with the infimum of $\psi^T\lambda+v^T\gamma$ over $\lambda,\gamma\ge0$ satisfying $A^T\lambda+W^T\gamma=c$ and $B^T\lambda=d(\zeta)$. Equation (27) identifies $h(x,\zeta)$ with the infimum of $c^Tx+(\psi-Ax)^T\rho$ over $B^T\rho=d(\zeta)$ and $\rho\ge0$. The nonnegative multiplier in this latter duality identity must be distinguished from the unrestricted multiplier in printed (17).

Significance

An exact equivalence would allow regret models to inherit methods and assumption checks developed for two-stage robust models. The conditional clauses matter because feasibility, bounded recourse at one scenario, and a lower bound across all scenarios are different requirements. Omitting any of them changes what can be concluded about the transformed problem. This is the role claimed for Proposition 2 in the paper's discussion, supplied p. 10.

The formalization distinguishes an already proved LP-duality substrate from the new regret claim. In particular, it exposes a source defect: printed $U'$ has no constraint $\rho\ge0$. Take $n_x=n_y=n_\zeta=1$, $m=r=s=2$, $W=P=(1,-1)^T$, $v=q=0$, $A=D=0$, $B=(1,-1)^T$, $\psi=(1,0)^T$, and $c=d=0$. Then $X=U=\{0\}$, $Y(0)=[0,1]$, and all original profits and regrets vanish. All five assumptions hold. Yet $U'$ admits $\rho=(t,t)$ for every real $t$. Feasible transformed recourse has $\lambda=(a,a)$ with $a\ge0$, giving objective $t-a$. Consequently $V^*=-\infty$ while $R^*=0$, and Assumption $4'$ fails. This concerns the literal equation (17); the source proof's different domain is not substituted for it.

Difficulty

The main obstacle is mathematical validity of the printed reformulation, rather than finding a proof tactic. An uncertainty-domain constraint cannot be recovered from an unrelated recourse constraint: the nonnegativity of $\lambda$ does not constrain $\rho$. The counterexample survives bounded original feasible sets and uniformly zero profits. A second source finding records a sign typo in the third WCARM display row on p. 32. Neither finding justifies silently changing the selected target.

Formalization scope

Finite coordinate spaces are represented by functions from Fin n to the reals. These are continuous decision and scenario spaces, not finite scenario lists. Product spaces represent concatenated vectors; equalities replace paired opposite inequalities. General LP feasibility is reused from ModernConvex_LPDuality_LinearProgram. The local definitions supply only the objective-uncertainty data, nested regret, and printed lifted policy model.

All extrema use EReal, with empty infimum $+\infty$ and empty supremum $-\infty$. The original and transformed objectives are independently constructed. No equivalence, duality result, attainment, compactness, finite scenario restriction, or affine-policy restriction is bundled into the model. No measurable-policy requirement is imposed. First-stage optimality concerns the optimized policy envelope and does not assert that a policy attaining it exists. The assumption-transfer clauses retain their original quantifier order. Relative regret, affine-policy exactness, and the paper's independent companion results are outside this mission.

Selected references

• Mehran Poursoltani and Erick Delage, Adjustable Robust Optimization Reformulations of Two-Stage Worst-Case Regret Minimization Problems, Operations Research (2022), DOI: 10.1287/opre.2021.2159. Citations use the supplied PDF dated July 10, 2020: Proposition 2, pp. 9–10; setup pp. 4–8; Appendix F.3, pp. 31–32; Appendix F.1, p. 30. Printed and PDF page numbers coincide. Final-journal version equivalence remains unverified; the supplied artifact is pinned by SHA256 05e610bd6a7b83731fccc04bebecd4961bde105cac69a0f951bf0da1cc2f1a95.

Learning values through interaction

Q-learning maintains estimates of the reward obtainable from each state and action. This makes it a natural method when an agent can interact with an environment but cannot ask a simulator for arbitrary transitions. The central question is whether these local value updates can support a quantitative guarantee on the reward lost during exploration. Jin, Allen-Zhu, Bubeck and Jordan study this question for finite episodic problems and give the UCB-Bernstein regret claim formalized here (arXiv:1807.03765v1, Sections 1–3). The target concerns this tabular setting, rather than function approximation or a limit of infinitely many learning steps.

A finite episodic decision problem

A Markov decision process has a finite nonempty state set of size $S$, a finite nonempty action set of size $A$, and a positive episode length $H$. At stage $h$, taking action $a$ in state $x$ gives a deterministic reward $r_h(x,a)\in[0,1]$ and a successor drawn from the probability row $P_h(\cdot\mid x,a)$. The rows may differ at every stage. At the beginning of each of $K$ episodes, an adversary chooses the initial state using the completed history; randomized choices are allowed. Write $T=KH$ for the total number of decisions.

A Markov policy selects one action at each stage and state. Its value $V_h^\pi(x)$ is the expected remaining reward from that point. The optimal value $V_h^\star(x)$ is obtained by finite backward maximization, and both values are zero after the last decision. These conventions are those of Section 2. The pseudo-regret compares the optimal value with that of the policy actually selected for each episode:

$$R_K=\sum_{k=1}^K\bigl[V_1^\star(x_1^k)-V_1^{\pi_k}(x_1^k)\bigr].$$

Although each value is an expectation, this sum is random because the learned policies and starting states depend on the observed history.

The algorithm initializes every Q entry to $H$. At a visit to a state-action-stage triple, it updates that entry using the observed successor value, the reward and an exploration bonus. The learning rate at visit number $t$ is $\alpha_t=(H+1)/(H+t)$. Its clipped value estimate is $V_h(x)=\min\{H,\max_a Q_h(x,a)\}$. Actions maximize the Q entry; every maximizer tie selection is admitted.

Formalization targets

The goal is the full restatement of Theorem 2, page 15. There are universal positive constants $c_1,c_2,C$ such that, for every instance and every $p\in(0,1)$, the bonus specification (C.1)–(C.3), using $\iota=\log(SAT/p)$, gives

$$\Pr\!\left\{R_K\le C\left(\sqrt{H^3SAT\iota}+\sqrt{H^9S^3A^3}\,\iota^2\right)\right\}\ge1-p.$$

Both terms are included for every positive $H,K$. The constants precede all instance parameters and adaptive rules. The target is a probability bound for the constructed algorithm, not an assumption about a favorable event.

The milestones are Lemma 4.1 and Lemmas C.1–C.7 from the same pinned source. Lemma 4.1 supplies the learning-rate weight properties through an existing Open statement. C.1 states the exact Q-error recursion. C.2 states the printed coarse bound, and C.7 states the weighted value-error estimate. C.3 compares optimal-value variance and historical empirical variance. C.4 states both optimism and the fine upper bound simultaneously. C.5 bounds the cumulative conditional variance of the played policies. C.6 compares empirical variance with that played-policy variance. The distinct probability levels $1-p/K$, $1-2p$ and $1-4p$ remain explicit.

What the target establishes

The claimed leading term grows like the square root of interaction length, with explicit dependence on the horizon and state/action counts. The second term records the finite-time cost that the headline asymptotic notation can hide. The paper compares this guarantee with its Hoeffding bonus and with model-based methods in Section 3. Those other algorithms are not substituted for the specified process.

This development provides concrete definitions and open statements for checking the claimed result. It does not assert completed Lean proofs. It also keeps source claims separate from source findings: the printed unrelated-pair quantification in C.2 and the printed error terms in C.6 remain visible. Recorded discrepancies identify mathematical obligations for a proof or disproof, rather than silently changing the target.

Adaptive estimates and exact conventions

The empirical variance uses next-stage values evaluated when each earlier visit occurred. These values change as learning proceeds, so they are not samples of one fixed value function. Policy choices, visit counts and initial states also depend on history. Replacing this sequence with independent samples from a frozen policy would change the problem. The finite-horizon propagation of these changing estimates and the distinction between optimal, estimated and played-policy values are central difficulties in Appendix C.

The source also contains a discrepancy between its variance equation and the algorithm pseudocode, a false universal-pair bound, a conflicting proof identity, and a missing logarithm in an intermediate estimate. A small-logarithm edge case affects the weighted-error claim as printed. These findings are documented separately; no corrected theorem replaces a mission target.

Formalization scope

States, actions, stages and episodes use finite index types, with positive cardinalities. The general nonstationary MDP is reused from the published library. A specialization identifies its state-dependent action types with the common action set and converts cost to reward by negation. Transition entries remain arbitrary real probabilities. Policy and optimal values are computed by backward recursion over a nonempty finite action maximum.

Historical observation lists represent the count and raw first and second accumulators. This preserves every update and historical observation; the representation makes no storage-complexity claim. The finite-history law multiplies actual start, policy and transition kernels. Randomized policy tie selection includes deterministic choices as point masses. No concentration or optimism conclusion is built into the probability law.

For the algorithm, $\beta_0=0$ and the first visit has $b_1=\beta_1/2$. The mathematical specification follows (C.1)–(C.3), which Theorem 2 explicitly invokes. Singular analytical concentration radii at zero visits are interpreted as infinite; the corresponding assertions are nonrestrictive there. C.1 and C.4 retain their actual initialization conclusions. The source's two different definitions of the symbol $\delta$ are kept distinct. The reusable model, values and process interfaces support future proof work without requiring a guessed numerical constant or a restricted class of starting states.

Selected references

• Chi Jin, Zeyuan Allen-Zhu, Sebastien Bubeck and Michael I. Jordan, Is Q-learning Provably Efficient?, preprint, 2018. arXiv:1807.03765v1, Sections 2–4 and Appendices B–C. All source numbering in this mission refers to this version.

Why uncertain demand matters for inventory pooling

A retailer with stock at several locations can serve a customer from a nearby location when local inventory runs out. This flexibility reduces shortages, but shipping and unused inventory still cost money. Evaluating the benefit requires a joint demand distribution: high demand at one location is easier to absorb when demand elsewhere is low. In practice, a retailer may know means, variances and correlations more reliably than a complete distribution. Distribution-free inventory pooling asks what cost can be guaranteed using only that moment information.

Govindarajan, Sinha and Uichanco study this question for a multilocation newsvendor with shipment decisions made after demand is observed. The selected result is their two-location bound, together with its conditional attainment claim and the two results used in its derivation. The reference is the held version of Distribution-Free Inventory Risk Pooling in a Multilocation Newsvendor, specifically Theorem 1 on printed page 15. The mathematical task includes checking whether that claim holds on its entire stated domain.

Shipments, costs and moment information

There are inventory nodes with stock $y_i$ and customer locations with realized demands $d_j$. A feasible flow consists of shipment quantities $z_{ij}\ge0$ satisfying

$$\sum_jz_{ij}\le y_i,\qquad \sum_iz_{ij}\le d_j.$$

The holding cost per leftover unit is $h>0$, the penalty per unmet unit is $p>0$, and shipping from node $i$ to location $j$ costs $s_{ij}>0$. Their total cost is

$$J(y,d,z)=h\sum_i(y_i-\sum_jz_{ij})+p\sum_j(d_j-\sum_iz_{ij})+\sum_{i,j}s_{ij}z_{ij}.$$

The recourse cost $C(y,d)$ is the infimum over these feasible flows, as in equation (2). An infeasible instance has value $+\infty$.

For two locations, shipping locally costs $s_0$ and shipping across locations costs $s$, with $p+h>s>s_0>0$. The moment ambiguity set $\mathcal F$ consists of all Borel probability laws on $\mathbb R^2$ with finite second moments, means $m_i$, standard deviations $\sigma_i$, and cross covariance $\rho\sigma_1\sigma_2$, where $-1\le\rho\le1$. No independence, density or nonnegative support is required in this set. At zero standard deviation, $\rho$ is interpreted as a covariance parameter. This unrestricted set is distinct from the nonnegative-support class used in the paper's original inventory optimization problem.

Formalization targets

The first milestone, Lemma 1, concerns any finite nested fulfillment hierarchy, rather than just two locations. Each level partitions the locations into nonempty clusters, successive levels merge clusters, and costs increase non-strictly toward the root. The root cost is at most $p+h$. With $E_\ell$ denoting aggregation over level-$\ell$ clusters and $\eta_\ell$ the parent-minus-child cost increments, the physical-domain identity is

$$C(y,d)=h e^\top(y-d)+s_0^\top d+\sum_{\ell=0}^{L-1}\eta_\ell^\top(E_\ell d-E_\ell y)^+.$$

At the root, the increment is $p+h-s_{L-1}$. This result retains nonnegative inventories and demands, arbitrary finite hierarchy depth, and equal-cost boundaries.

For the second milestone, Proposition 1, define $a=m_1-y_1$, $b=m_2-y_2$, $A=a^2+\sigma_1^2$, $B=b^2+\sigma_2^2$, $T=ab+\rho\sigma_1\sigma_2$, and

$$\Phi(y;\nu)=\sqrt{\frac{A+B+(\nu-1)T}{\nu+1}}.$$

For every $\zeta>0$, real inventory pair $y$, and $f\in\mathcal F$, the asserted bound is

$$\mathbb E_f[(d_1-y_1)^++(d_2-y_2)^++\zeta(d_1+d_2-y_1-y_2)^+] \le\frac{\zeta+1}{2}(a+b)+(\zeta+1)\Phi\left(y;\frac{3\zeta+1}{\zeta+1}\right).$$

The bound is attained by a law with at most six points whenever Condition 1 holds. That condition is the explicit nonempty interval $[\max(0,\alpha_1,\alpha_5),\min(\alpha_2,\alpha_3,\alpha_4)]$; all five source coefficients are defined in the accompanying Bounds item.

The goal, Theorem 1, retains both the exact cost bound and actual conditional attainment:

$$\sup_{f\in\mathcal F}\mathbb E_f[C(y,d)]\le s_0(m_1+m_2)-\frac{p-h-s_0}{2}(y_1+y_2-m_1-m_2) +(p+h-s_0)\Phi\left(y;\frac{3(p+h-s)+s-s_0}{p+h-s_0}\right).$$

If Condition 1 holds with $\zeta=(p+h-s)/(s-s_0)$, some $f^*\in\mathcal F$ with at most six support points has expected cost equal to this right side. These are exactly equations (5), (9) and (10) of the held source.

What resolving the statements establishes

A valid sharp moment bound would quantify how marginal uncertainty and dependence interact with inventory sharing. Attainment matters: it identifies an admissible demand law realizing the bound, rather than merely a numerical ceiling. The hierarchy identity also separates a shipment optimization problem from its aggregate shortages and can serve other inventory models.

There is, however, a concrete domain issue in the printed goal. Equation (2) forbids negative shipment quantities, while Theorem 1 quantifies over laws allowing negative demand. Negative demand makes its column constraint infeasible. For example, with $h=1,p=3,s_0=1,s=2$, inventories and means $(1,1)$, and independent demands uniform on $\{-1,3\}$, the expectation of the literal recourse cost is infinite. The printed bound is the finite value $2+3\sqrt{12/5}$. The formal target preserves this claim, and the source counterexample is recorded separately. Compilation of the declarations is not a proof of the paper's results.

Mathematical difficulties and domain boundaries

The bivariate shortage terms share random coordinates, so bounding each term separately loses their joint moment structure. Conditional attainment also requires genuine nonnegative probabilities satisfying all moment equations simultaneously. The endpoints $\rho=\pm1$ remain included even though an intermediate appendix derivation uses strict inequalities.

A separate issue is the transition from the physical recourse problem to unrestricted laws. The hierarchy identity is a statement on nonnegative realizations. Extending its positive-part expression to the whole plane does not redefine the original flow problem automatically. This distinction is material to the printed goal, rather than a technical obstacle to hide with an additional finiteness assumption.

Formalization scope and conventions

The definitions separate transportation recourse, nested partitions, moment parameters, and analytic bounds. Probability laws reuse the published RobustMeanCov_Projection_MeanCovClass, whose finite second moments prevent default-valued real integrals. Finite indices start at zero. Hierarchy clusters are finite sets, and aggregation is a finite sum. The one-location, one-level boundary is allowed.

Recourse and its expectation take nonnegative extended values; comparisons with finite expressions occur in EReal without discarding the right side's sign. The shortage loss has a real integral because the moment conditions ensure integrability. Six-point laws use six nonnegative weights summing to one, allowing zero weights and coincident atoms. The displayed condition requires $\Phi>0$ only within its attainment antecedent. No theorem assumes the desired inequality, an optimizer, or tightness. The selected scope excludes inventory minimization, the general-network semidefinite approximation, and empirical performance claims.

Selected references

• Govindarajan, A., Sinha, A. and Uichanco, J. Distribution-Free Inventory Risk Pooling in a Multilocation Newsvendor. Management Science, DOI record dated 2020. DOI. Numbering follows the held PDF: Lemma 1, p. 10; Proposition 1 and Theorem 1, p. 15; proofs ec3–ec11. Catalog citation basis is published; the held artifact carries “Submitted to Management Science” and SSRN 3315439 markings. No final volume or page metadata is asserted.

Financing reliability across supply-chain tiers

A manufacturer can have ample cash while an upstream supplier lacks the funds needed to make production reliable. Financing that supplier through an intermediary changes both the cost of credit and the incentives to invest. Information is also uneven: a firm may know its immediate supplier's working capital without knowing the capital of a more distant supplier. Dong, Qiu and Xu study how visibility and direct financing change these incentives in a three-tier supply chain (2022, Sections 3–6). Their central claim is that a direct financing channel can support voluntary blockchain adoption by both suppliers while improving all three firms' profits.

The mathematical question concerns the contracts and investments in this economic model. Blockchain supplies visibility of upstream working capital and execution of contingent contracts. The model does not describe a consensus algorithm or make claims about cryptographic security.

Players, cash flows, and voluntary participation

The three risk-neutral players are a manufacturer, an immediate supplier, and an upstream supplier. Demand, production capacity, and the retail price are normalized to one. Upstream production cost and the risk-free interest rate are zero. The immediate supplier pays procurement price $v$ and can obtain emergency supply at cost $e$, with $0<v<e<1$. An investment $y\ge0$ succeeds with probability $P(y)\in[0,1)$, where $P$ is increasing and concave. The two suppliers have working capital $\theta_1$ and $\theta_2$.

An advance-payment contract specifies a wholesale price and an interest rate. The upstream supplier can self-finance or borrow the advance $(y-\theta_2)^+$. Its terminal cash reflects limited liability. The immediate supplier can finance this advance using its own capital, competitive bank borrowing, or manufacturer finance. Bank repayment is capped by available assets and its expected repayment equals principal. The source also allows joint bank and manufacturer finance. The immediate supplier chooses manufacturer finance on a tie and uses emergency supply exactly when its wholesale price is at least $e$.

The traditional equilibrium has limited visibility. The manufacturer knows $\theta_1$ but only a probability distribution of $\theta_2$ on $[0,c)$, where $c$ is the source's unconstrained maximizer of $vP(y)-y$. Its contract maximizes expected profit under that distribution, anticipating the suppliers' actual responses. The full working-capital region is the source's rectangle $W=[0,\theta_1^{\max}]\times[0,c)$, with its auxiliary bank-finance optimizers and total-capital constraint.

Under delegate financing, blockchain reveals $\theta_2$, but finance still passes through the immediate supplier. Under direct financing, the manufacturer lends to the upstream supplier and offers the immediate supplier a wholesale price. Both mechanisms preserve the traditional menu. Adoption requires a strictly higher realized profit, and the manufacturer's optimization also requires its own strict improvement. These comparisons use the traditional outcome at the realized capital profile, not its ex ante average (Sections 5–6).

Formalization targets

The goal is the complete printed Theorem 3, including existence of an attained optimal direct menu. Write its price, rate, and implemented investment as $\check w^1$, $\check r_m^2$, and $\check y$. There is a nonincreasing emergency-cost threshold $\bar{\check e}(\theta_2)$, independent of $\theta_1$ and $e$, such that

$$\check r_m^{2*}\le r_s^*,\qquad \check w^{1*}=\begin{cases} \bar{\check w}^{1}(\theta_1,\theta_2)\le w^*,& e>\bar{\check e}(\theta_2),\\ e,& e\le\bar{\check e}(\theta_2). \end{cases}$$

The threshold is no larger than the delegate-financing emergency threshold, both suppliers always adopt, and

$$\check\pi_i>\pi_i^*\quad(i=0,1,2),\qquad \check y^*\ge y^*.$$

The nine supporting targets are Lemma 1, Lemmas EC.3 and EC.4, Proposition 1, Theorem 1, Lemma EC.1, Proposition EC.1, Lemma EC.2, and Theorem 2. They cover investment implementation, financing choices and comparative statics, the traditional optimum, the delegate rate and transition regions, and voluntary-adoption thresholds. Every numbered result retains its clauses, including uniqueness and the source's distinct endpoint conventions. Theorems 4–5 and the mandatory-adoption extension are outside this mission.

What the formalization establishes

The source attributes universal voluntary adoption to the direct financing channel, beyond the more limited adoption region under delegate financing (Theorem 3, supplied manuscript p. 23). Its contract characterization also compares financing rates, wholesale prices, emergency-sourcing thresholds, and reliability investment. A statement about adoption alone would omit much of that claim.

The formalization makes the sequence of optimization problems explicit. It distinguishes initial capital from incremental profit, preserves an arbitrary capital prior, and represents every stated optimum by an actual maximizing contract with implemented supplier responses. The statements have been typechecked as open goals; they are not machine-checked proofs of the economic conclusions. Source proof gaps are recorded separately, and the printed targets remain available for proof or disproof.

Mathematical difficulties and source findings

Optimizing a manufacturer's contract requires anticipating the supplier's financing decision and the upstream investment response. Cash flows change at both loan-default boundaries and the emergency-sourcing threshold. The traditional objective is an expectation, while the blockchain objectives are profile-specific optimizations constrained by three participation comparisons.

Strict participation also creates an attainment issue. The direct-financing proof identifies a wholesale price at a supplier's participation boundary, although the model requires strict improvement. A limiting price is not automatically an attained optimum. The Section 4.1 claim that the unconstrained optimum is always an interior first-order root also needs an assumption: for $v=1/2$ and $P(y)=1-e^{-y}$, the optimum is zero and $vP′(0)=1/2$. In addition, the displayed system (EC.13) contains $-P(y)>0$, incompatible with a nonnegative success probability. The mission retains the printed theorem and records these proof findings in its source audit; it does not turn either problem into a new assumption or substitute weak participation (Appendix A, ec7–ec8).

Formalization scope and conventions

All prices, capital, and investments remain real. Priors are Borel probability measures with mass one on $[0,c)$; no density, finite support, or special reliability formula is imposed. The expectation predicate includes integrability. Derivative equations carry derivative-existence conditions, and the implementing-rate formula is certified at a nonzero denominator. Optimal response functions are existential data with explicit optimality certificates, never choices silently returned from empty maximizing sets.

The generic sequential-game best-response interface is reused from a published definition. Every boundary bank response used in the capital and contract domains has an explicit optimality certificate, including $\theta_2=c$. Supplier response lemmas cover all $w\ge\underline w$ and retain the full nonnegative interest-rate domain. The paper-specific layers supply reliability and supplier cash flows, competitive lending, traditional equilibrium, voluntary delegate financing, and direct financing. Joint-financing deviations follow the source's invoice-netting payment sequence. A tagged no-offer alternative represents an infinite manufacturer AP rate; it induces bank finance without multiplying by infinity. Rejection retains the traditional outcome. Emergency supply is used at equality $w=e$, and manufacturer finance wins a supplier financing tie.

The low-price participation boundary is an equality of profits, kept distinct from strict feasibility. “Increasing” and “decreasing” are read weakly where the source does not print a strict comparison. The Table 3 loan symbols are read consistently with its single direct-advance caption. Each theorem's metadata lists these conventions and any notation readings. Useful subsequent contributions include proofs, disproofs, and separately identified corrected variants; a corrected variant cannot replace the printed mission target.

Selected references

• Dong, L., Qiu, Y., and Xu, F. Blockchain-Enabled Deep-Tier Supply Chain Finance. Manufacturing & Service Operations Management, forthcoming manuscript dated May 2022, cited as published under the supplied artifact's metadata. DOI: 10.1287/msom.2022.1123. Source numbering: printed/PDF pp. 7–23; appendix ec1–ec11 corresponds to PDF pp. 31–41.

Information before a platform release

A platform release can attract both customers and developers. A customer's valuation depends on the number of other customers and the available applications, while a developer values access to customers. Before adoption, those numbers are expectations. Announcing features can influence these expectations, but communicating information costs money and also changes competition between platforms. Chellappa and Mukherjee study this interaction through formal, informal, and absent preannouncements in a two-firm market. The target here is their first proposition, concerning strong taste preferences when agents use one platform and existing customers remain loyal. Chellappa and Mukherjee (2020)

The distinction between announcement choice and subsequent pricing matters. Prices computed under an assumed pair of announcements do not by themselves determine whether either firm would prefer a different announcement. The claim concerns a complete sequence of strategic choices, including choices following announcements that do not occur in the proposed equilibrium.

Agents, announcements, and adoption

The Hotelling market consists of firms 0 and 1 at the endpoints of a unit interval. New users and new developers form two separate uniform populations, each of mass one. Their locations describe tastes. An agent at location $x$ loses utility $tx$ at firm 0 and $t(1-x)$ at firm 1, where $t>0$ measures taste strength. Each side also has an old population of mass one, split equally between the firms. These installed bases remain loyal and adopt the new version. New agents choose exactly one platform. Source §§2–2.4

The firms have a common intrinsic value $\theta>0$. Users benefit from other users with coefficient $\alpha>0$ and from developers with coefficient $\beta>0$. Developers benefit from users with the same cross-side coefficient $\beta$, without a same-side developer term. First, each firm simultaneously chooses formal announcement $F$, informal announcement $I$, or no announcement $N$. Formal announcement costs $c>0$ and fully informs both sides. Informal announcement costs $kc$, where $0<k\le1$, and attenuates new-market expectations by $\mu$ for users and $\delta$ for developers, with $0<\mu\le\delta<1$. No announcement costs zero and contributes no expectations beyond the installed base.

Write $(a_i,b_i,C_i)$ for these multipliers and cost: $(1,1,c)$ under $F$, $(\mu,\delta,kc)$ under $I$, and $(0,0,0)$ under $N$. Firms next choose user prices $p_i$ and developer fees $l_i$. For new demands $n_u^i,n_d^i$, the values before transport are

$$V_u^i=\theta+\alpha(1/2+a_i n_u^i)+\beta(1/2+a_i n_d^i)-p_i,$$ $$V_d^i=\theta+\beta(1/2+b_i n_u^i)-l_i.$$

Announcements continue to determine expectations during pricing. Fulfilled expectations require that the demands appearing in these values agree with utility-maximizing adoption. The markets are fully covered, individual utility is nonnegative, and tariffs are nonnegative. Each firm's objective includes revenue from installed and new customers:

$$\Pi_i=p_i(1/2+n_u^i)+l_i(1/2+n_d^i)-C_i.$$

Formal preannouncement under strong preferences

The target preserves Proposition 1's tariffs and its open interval, including every numerical coefficient. The source's maintained formal-candidate economic conditions are explicit:

$$t>\alpha,\quad t(t-\alpha)>\beta^2,\quad t>\alpha+\beta,\quad t>\beta,$$ $$4t\ge c+2\alpha+4\beta,\quad 5t\le2\theta+6\alpha+6\beta,\quad 5t\le2\theta+6\beta.$$

Under these conditions and

$$\frac{2\theta+\beta(1+4\mu+\delta)}5<t<\frac{2\theta+6\beta}5,$$

the asserted outcome of symmetric pure subgame-perfect Nash equilibrium is

$$s_0=s_1=F,\qquad p_i^*=2(t-\alpha-\beta),\qquad l_i^*=2(t-\beta).$$

The goal includes existence of such an equilibrium system and the characterization of every symmetric pure equilibrium outcome. Existence includes a consistent selection of fulfilled-expectation allocations and pricing continuations after every announcement pair. This reads the paper's categorical language within its stated focus on symmetric pure equilibria. There are no supporting numbered milestones: the shared proof of Propositions 1–3 introduces no earlier numbered result on which Proposition 1 depends. Proposition 1, p. 26; Appendix A, pp. 45–48

What the result would establish

The result associates a precise range of consumer preferences with the firms' information choices and both components of their tariffs. Its strategic content includes the incentive to announce formally even when changing the announcement changes subsequent competition. The target is therefore useful for understanding when information provision can be sustained alongside price competition in this model.

The formal development provides explicit definitions of allocation, expectations, unilateral deviations, and continuation play. These definitions distinguish maintained economic conditions from conclusions about optimal behavior. The goal is a statement awaiting a checked proof or disproof; the local compilation of its declaration is not a proof of the economic result. The generic Nash interface is reused from an existing definition, while the source-specific information and market conventions are supplied here.

Continuations and the source's proof gap

The central difficulty is that unilateral announcement changes lead to asymmetric subgames. At $(F,F)$, a firm's switch to $I$ or $N$ leads to $(I,F)$ or $(N,F)$, rather than to a diagonal profile. Appendix equation (A2) compares symmetric-profile profits instead. Furthermore, the printed symmetric candidate profits give $\pi_{NN}-\pi_{FF}=2\alpha+4\beta+c>0$, inconsistent with the strict opposite comparison in that equation. This is a documented gap in the printed argument, not a claimed feasible unilateral deviation: the symmetric $NN$ candidate can fail participation. Appendix A, pp. 46–47

The formal target retains Proposition 1 despite this finding. A separate recorded typo concerns informal information multipliers appearing in a display labeled formal utility. The model uses the primitive utilities and the subsequent consistent participation inequalities. No proof gap is inserted as an assumption.

Formalization scope and conventions

All economic parameters, tariffs, and market cutoffs are real. The two firms and three modes are finite; the agent populations and tariff spaces remain continuous. A cutoff represents an interval's uniform mass, with weak utility comparisons at boundary allocations. The isolated indifferent agent has zero mass. No derived interior demand formula is evaluated as a negative customer population.

The covered-market reading requires a demand selection to choose a feasible allocation at every tariff profile that admits one. Every unilateral feasible joint tariff change is compared under that same selection. Nonnegative profit is an equilibrium requirement, not a filter on deviations. Both firms' price plans are specified after all nine histories, and no history is removed because its symmetric candidate is infeasible. Symmetric strategies exchange firm labels and announcement histories; unilateral deviations remain unrestricted.

The definition files separate a general covered Hotelling split, the paper's primitives, its feasible-market relation, and its two-stage equilibrium system. They build on real arithmetic and the published generic pure Nash predicate. The printed outcome is a separate predicate and never the definition of equilibrium. Contributions may establish or refute the full claim under these declared conventions; replacing it by first-order conditions or a conditional price calculation would change the target.

Selected references

• Ramnath K. Chellappa and Rajiv Mukherjee, Platform Preannouncement Strategies: The Strategic Role of Information in Two-Sided Markets Competition, Management Science, 2020. DOI: 10.1287/mnsc.2020.3606. Citations use the held 55-page artifact: printed and PDF pages coincide. The recorded citation basis is published; the artifact carries SSRN 2705238 footers. Proposition 1 is on p. 26 and equation (A5) on p. 47.

Incentives for an interacting population

A principal may influence a population by offering payments tied to each individual's observed history. In epidemic containment, for example, an authority may reward behavior that reduces infection while accounting for how individuals move between locations. The principal must anticipate both each individual's response and the population distribution produced by those responses. Carmona and Wang formulate this problem with finitely many individual states and an infinite population, and identify an equivalence between optimal contracting and a stochastic control problem. This mission formalizes that general equivalence, their first main result, rather than the later linear-quadratic specialization. Held source, introduction and §3.

States, controls, payments, and equilibria

An individual occupies one of $m$ states during a continuous interval $[0,T]$. The canonical path space consists of right-continuous paths with left limits, with no jump at the terminal time. The observable information at time $t$ is the history of the state process $X$ up to that time. Under a reference probability law $P$, every transition between distinct states has rate one, and the initial state has a prescribed distribution $p^\circ$.

The individual's control is any predictable process taking values in a compact set $A\subseteq\mathbb R^l$. The transition rates $q(t,i,j,a,p)$ depend on time, current and next states, the chosen action, and the distribution $p$ of the population. Assumption 2.1 gives zero row sums, a uniform upper bound on positive off-diagonal rates, and Lipschitz dependence on action and population distribution. It does not require rates to be uniformly bounded away from zero. The controlled law $Q^{\alpha,p}$ is constructed from its explicit density relative to $P$. §2.2.

A contract comprises a predictable running payment $r$ and a measurable terminal payment $\xi$ with $\xi\in L^2(P)$. Both may depend on the entire observed history. The agent incurs running cost $c$ and receives utility $u(r)$ and $U(\xi)$. Its expected cost is

$$J_{r,\xi}(\alpha,p)=E^{Q^{\alpha,p}}\left[\int_0^T(c(t,X_t,\alpha_t,p(t))-u(r_t))dt-U(\xi)\right].$$

A Nash equilibrium is an admissible best response $\alpha$ against the prescribed flow $p$, together with consistency: $p_i(t)=Q^{\alpha,p}(X_t=e_i)$ at every time. Let $\mathcal N(r,\xi)$ denote these equilibria and $\mathcal C$ the contracts admitting at least one. The principal pays running cost $c_0(t,p(t))+r_t$ and terminal cost $C_0(p(T))+\xi$. Its inner optimization favors the principal among equilibria meeting a reservation threshold $\kappa$. §§2.3–2.6.

Formalization targets

The Hamiltonian $H_i(t,z,a,p,R)$ is the running cost minus the reward argument plus $\sum_{j\ne i}(z_j-z_i)(q(t,i,j,a,p)-1)$. Assumption 3.1 requires its unique action minimizer $\hat a_i(t,z,p)$ to be measurable and uniformly Lipschitz in $z$ for the state seminorm. Write $\hat H$ for the minimized Hamiltonian.

The three milestones preserve all clauses of the source. Lemma 3.3 gives one positive constant for the two seminorm Lipschitz bounds on $\hat H$ and $\hat a$. Lemma 3.4 states existence and uniqueness for both the frozen-control and optimized backward equations, their expected-cost identities, and attainment by the feedback control. Theorem 3.6 gives both directions of the correspondence between Nash equilibria and solutions of the mean-field backward system. Its converse identifies controls almost everywhere for $dP\otimes dt$ and flows almost everywhere for $dt$. §§3.1–3.2.

The goal is Theorem 3.7:

$$\forall\kappa\in\mathbb R,\qquad \widetilde V(\kappa)=V(\kappa).$$

Here $V$ is the original two-level contracting infimum. The forward McKean–Vlasov value $\widetilde V$ optimizes over predictable payments, the printed class of adapted left-continuous $Z$, and random initial values $Y_0$ measurable at time zero with $E^P[Y_0]\le\kappa$. The forward dynamics give a terminal value $Y_T$, and the principal's terminal payment in its objective is $U^{-1}(-Y_T)$. The equality includes the assertion that both values are defined. §3.3, equations (30)–(34) and Theorem 3.7.

What the equivalence would establish

The result replaces an optimization over contracts and induced equilibria with an optimization over controls in forward mean-field dynamics. It preserves the principal's value rather than merely producing a feasible contract or a one-sided bound. The source presents this equivalence as the foundation for its later specialized calculations.

The formalization supplies explicit, separately inspectable definitions of contracts, costs, equilibrium, solution classes, and the two infima. The theorem declarations are statements awaiting proof or disproof; they are not machine-checked proofs of the paper's claims. Recording exact domains also makes possible failures of the printed claims visible. In particular, the held source does not ensure that the inverse utility in (34) is defined at every admitted terminal value.

Mathematical difficulties and source findings

The two optimization problems have different variables and admissibility conditions. Establishing equality must account for arbitrary history-dependent contracts and every allowed forward input, as well as the precise equivalence relation for backward solutions. A constant vector added to $Z$ is invisible to the state seminorm, so literal uniqueness of its coordinates would be incorrect.

The source also has a substantive domain issue: with $U(x)=\exp(x)$, zero running rewards and costs, unit rates, and $Y_0=1$, the forward trajectory $Y_t=1$ requires $U^{-1}(-1)$, which does not exist. Moreover, the forward class printed on p. 8 uses the first power of the seminorm, whereas the backward class uses its square. Neither issue is repaired by adding assumptions to the target. Two typographical readings are disclosed separately: the payment index in (20)–(21) and the extra hat in (15). The local findings retain numerical evidence and the printed claims. PDF pp. 6–9.

Formalization scope

States use Fin m, with a simplex inhabitant excluding zero states while retaining one state and boundary initial distributions. The action set remains an arbitrary compact subset of Euclidean space. Time remains continuous, and the population remains infinite. Published canonical-path, reference-law, density, seminorm, and finite-jump-integral primitives are reused. The paper-specific model does not inherit the stronger assumptions of the publication supplying those primitives.

Costs and infima use extended reals. Empty infima equal positive infinity, and unbounded-below infima may equal negative infinity. Signed integrals are partial: nonmeasurability and infinity minus infinity do not receive a default numerical value. Inverse utilities require a unique preimage. Every printed forward control must have a solution-derived, selection-independent cost; no subset of conveniently solvable controls replaces the domain. The original value checks costs at the contracts and equilibria indexed by (11), including all competing controls in each best-response test. The feedback control has a fixed zero extension after $T$, making global predictability depend only on the stated time interval. The goal contains no assumed equilibrium correspondence or equality of cost sets.

Selected references

• René Carmona and Peiqi Wang, Finite-State Contract Theory with a Principal and a Field of Agents, held artifact arXiv:1808.07942v1, 23 August 2018. All result indices and pages in this mission refer to this artifact; PDF pages equal printed pages.
• Catalog publication: René Carmona and Peiqi Wang, same title, Management Science (2021), DOI 10.1287/mnsc.2020.3760. The catalog records citation basis published, but the held PDF is the explicitly identified arXiv version, not the journal typesetting.

This mission formalizes P. Haim-Kislev and Y. Ostrover, A counterexample to Viterbo's conjecture, Ann. of Math. (2) 203 (2026) 603–622, doi:10.4007/annals.2026.203.2.5 (arXiv:2405.16513v3, whose page numbers are used).

Motivation

Viterbo's volume–capacity conjecture (2000) asserted that among convex domains of given volume in $\mathbb R^{2n}$ the Euclidean ball has the largest symplectic capacity: $c(K)^n \le n!\,\mathrm{Vol}(K)$ for every symplectic capacity $c$. It had been confirmed near the ball, for many symmetric classes, and up to a universal constant, and its restriction to Lagrangian products $K \times K^\circ$ of centrally symmetric bodies is equivalent to Mahler's conjecture. Haim-Kislev and Ostrover disproved it with an explicit example in $\mathbb R^4$: the product of a regular pentagon and its rotation by $90°$, whose Ekeland–Hofer–Zehnder capacity is computed through Minkowski billiards.

Setting

• Phase space $\mathbb R^{2n} = \mathbb R^n_q \times \mathbb R^n_p$, with symplectic embeddings, balls and the Gromov width from the published bundle SymmetricPolar.
• A convex domain is a bounded convex set with nonempty interior; a symplectic capacity is Definition 1.1 (monotone, conformal, normalized on the unit ball and cylinder).
• The Ekeland–Hofer–Zehnder capacity $c_{\rm EHZ}$ is the least action of a generalized closed characteristic on the boundary (p. 10): an absolutely continuous loop whose velocity lies, at almost every time, in $J$ applied to the normal cone; the systolic ratio is $\mathrm{Sys}(A) = c_{\rm EHZ}(A)^n/(n!\,\mathrm{Vol}(A))$.
• Minkowski billiards (Definition 2.1), the support function $h_T$, the $T^\circ$-length of a polygon, and $\mathcal P(K)$, the polygons that cannot be translated into the interior of $K$.
• The definitions are in the bundle Viterbo.

Target

Theorem 1.3 (p. 3): Viterbo's conjecture fails for every $n \ge 2$.

Significance

The result settles a 25-year-old conjecture at the centre of quantitative symplectic geometry, and with it the strong Viterbo conjecture that all normalized capacities agree on convex domains. It reopens the questions of which classes do satisfy the inequality (centrally symmetric domains, Question 1, whose affirmative answer would imply Mahler's conjecture) and of the largest possible systolic ratio. It also gives convex domains with systolic ratio $1$ that are not symplectomorphic to the ball, contrary to a conjecture in Viterbo's paper (Remark 1.8). OpenAI's symplectic and convex-geometric results already on prove2.me (the symmetric Mahler inequality, the Gromov width of $K \times K^\circ$, non-squeezing) sit next to these statements.

Difficulty

The counterexample itself is concrete. By Theorem 2.2 (Artstein-Avidan–Ostrover, Rudolf), $c_{\rm EHZ}(K \times T)$ is the least $T^\circ$-length of a polygon with at most three vertices that cannot be translated into the interior of the pentagon, a piecewise-linear minimization that the paper settles by a case analysis; the area of a regular pentagon then gives $\mathrm{Sys} = (\sqrt5+3)/5 > 1$. In $\mathbb R^{2n}$ for $n \ge 3$ the counterexample is the 2-product of $K \times T$ with a ball of the same capacity, whose systolic ratio is the product of the two; a polytope version uses iterated $(1, \infty)$-products of $K$ and $T$ instead. The hard inputs are cited: the billiard characterization of $c_{\rm EHZ}$ for non-smooth Lagrangian products, the product formula for systolic ratios in higher dimensions, and the identification of $c_{\rm EHZ}$ with a capacity in the sense of Definition 1.1 (Hofer–Zehnder theory), which turns the computed counterexample into the statement about all capacities. These are stated as external milestones.

Formalization scope

The milestones are Proposition 1.4 and its minimization, the case $n = 2$ of the proof of Theorem 1.3, the $c_{\rm EHZ}$ form of Theorem 1.3, Theorem 2.2, the cited product formulas, the facts used about capacities ($c_G$ and $c_Z$ are capacities, Viterbo holds for $c_G$, $c_{\rm EHZ}$ is a capacity on convex domains, the ball's capacity), the polytope counterexamples and the maximal systolic ratio of §1.1(ii), the failure of the strong conjecture, Remark 1.8, Question 1 as an Open statement, and the equivalence with Mahler's conjecture cited on p. 3. Left out: the other results cited as context in the introduction (local results near the ball, special classes, the universal bound, $c_{\rm EHZ} = c_Z$ in dimension 4, Mahler's conjecture in dimension three); the coincidence on convex domains of the Hofer–Zehnder, first Ekeland–Hofer and symplectic homology capacities, and the closed-Reeb-orbit form of $c_{\rm EHZ}$ (each needs its own construction, and the paper uses only that $c_{\rm EHZ}$ is a capacity); Remarks 1.6 and 1.7, Question 3, and the description of the generic Reeb dynamics in §3.1.

Selected references

• P. Haim-Kislev and Y. Ostrover, A counterexample to Viterbo's conjecture, Ann. of Math. 203 (2026) 603–622, https://doi.org/10.4007/annals.2026.203.2.5.
• C. Viterbo, Metric and isoperimetric problems in symplectic geometry, J. Amer. Math. Soc. 13 (2000) 411–431, https://doi.org/10.1090/S0894-0347-00-00328-3.
• S. Artstein-Avidan and Y. Ostrover, Bounds for Minkowski billiard trajectories in convex bodies, IMRN 2014, 165–193, https://doi.org/10.1093/imrn/rns216.
• D. Rudolf, The Minkowski billiard characterization of the EHZ-capacity of convex Lagrangian products, J. Dynam. Differential Equations 36 (2024) 2773–2791, https://doi.org/10.1007/s10884-022-10228-0.
• S. Artstein-Avidan, R. Karasev and Y. Ostrover, From symplectic measurements to the Mahler conjecture, Duke Math. J. 163 (2014) 2003–2022, https://doi.org/10.1215/00127094-2794999.
• P. Haim-Kislev and Y. Ostrover, Remarks on symplectic capacities of p-products, Internat. J. Math. 34 (2023) 2350021, https://doi.org/10.1142/S0129167X23500210.

Decisions made before and after uncertainty

In a two-stage robust optimization problem, a decision maker commits to some variables before observing uncertain data and chooses the remaining variables after observing it. Requiring every decision to be fixed at the outset can lose the benefit of this information. Allowing an arbitrary response, however, can produce a problem with infinitely many decision variables and constraints. The survey by Bertsimas, Brown and Caramanis, §4, discusses this tension and describes affine decision rules as one approach to it.

An affine decision rule prescribes a constant response plus a linear adjustment to the observed uncertainty. It is specified by finitely many coefficients, even when the observations range over a continuum. This mission concerns the survey's explicit semidefinite approximation for these rules when uncertainty affects both the initial decisions' constraint coefficients and the recourse matrix. The target is the quantitative containment in its Theorem 7, with Theorem 6 providing the supporting approximation assertion. This is a selected survey result attributed there to reference [10], rather than an assertion that the survey identifies it as an original headline contribution.

Data, rules, and uncertainty sets

Let $m$ be the number of constraints, $n_1$ the number of first-stage variables, $n_2$ the number of second-stage variables, and $L$ the number of uncertainty coordinates. All variables are real. Given matrices $A_j^{(0)},A_j^{(1)},\ldots,A_j^{(L)}$ with $m$ rows and $n_j$ columns, set

$$A_j(u)=A_j^{(0)}+\sum_{l=1}^L u_l A_j^{(l)},\qquad j=1,2.$$

The first-stage cost is $c^Tx_1$, where $c\in\mathbb R^{n_1}$. Feasibility requires $A_1(u)x_1+A_2(u)x_2(u)\le b$ componentwise, for every admitted uncertainty vector $u$, with $b\in\mathbb R^m$ fixed. The entire vector $u$ is revealed before the second-stage action.

The affinely adjustable robust counterpart, or AARC, restricts the action to $x_2(u)=Qu+q$. The decision is therefore the full tuple $\chi=(x_1,q,Q)$. Write $q^{(0)}=q$ and let $q^{(l)}$ be column $l$ of $Q$. All these coefficients are fixed before observation. In particular, $Q$ cannot be selected separately for each uncertainty realization.

Let $S_1,\ldots,S_K$ be symmetric positive semidefinite $L\times L$ matrices, with $K\ge1$. For a positive radius $\rho$, define the ellipsoidal uncertainty intersection

$$U_\rho=\{u\in\mathbb R^L:\ u^T(\rho^{-2}S_k)u\le1\text{ for every }k\}.$$

Individual matrices may be singular or zero. Neither boundedness of the intersection nor strict positive definiteness is imposed. The original feasible set is

$$X_\rho=\{\chi:\ A_1(u)x_1+A_2(u)(Qu+q)\le b\text{ for every }u\in U_\rho\}.$$

The printed construction preceding (4.13) defines

$$\alpha_i=-[A_1^{(0)}x_1+A_2^{(0)}q^{(0)}-b]_i,$$ $$\beta_i^{(l)}=-\tfrac12[A_1^{(l)}x_1+A_2^{(0)}q^{(l)}-b]_i,$$ $$\Gamma_i^{(l,k)}=-\tfrac12[A_2^{(k)}q^{(l)}+A_2^{(l)}q^{(k)}]_i.$$

These formulas are retained literally. A semidefinite certificate assigns a nonnegative multiplier vector $\lambda^{(i)}\in\mathbb R^K$ to each row and requires

$$M_i=\begin{bmatrix} \Gamma_i+\rho^{-2}\sum_k\lambda_k^{(i)}S_k&\beta_i\\ \beta_i^T&\alpha_i-\sum_k\lambda_k^{(i)} \end{bmatrix}\succeq0.$$

Here $M_i\succeq0$ means that $M_i$ is symmetric and its quadratic form is nonnegative on every real vector. The approximate set $X_\rho^{\mathrm{approx}}$ contains exactly those full tuples admitting these certificates. The SDP minimizes the same cost $c^Tx_1$.

Formalization targets

Theorem 6, as an inner-approximation assertion, states that every feasible certificate yields an original robustly feasible policy with the same objective. Its formal target retains the explicit finite program (4.14), including all row multipliers.

For $r=\sum_k\operatorname{rank}_{\mathbb R}(S_k)>0$, define

$$\gamma=\sqrt{2\ln(6r)}.$$

The goal is the complete Theorem 7, printed page 26 in the held artifact:

$$X_{\gamma\rho}\subseteq X_\rho^{\mathrm{approx}}\subseteq X_\rho.$$

The same data and ellipsoid matrices occur in all three sets. Only the uncertainty radius changes on the left. No optimizer is part of this claim, and neither containment is omitted. The factor is the exact printed factor, including the constants 2 and 6.

What the containment would provide

The right inclusion is a safety assertion: a policy admitted by the finite SDP satisfies every original constraint at the chosen radius. The left inclusion measures conservativeness: a policy robust to the larger uncertainty set would already admit an SDP certificate at the smaller radius. Thus the comparison relates a finite certificate to the original continuum of constraints while retaining the full response rule. It does not compare affine policies with unrestricted adaptive policies.

The formalization supplies independently constructed feasible sets, an explicit block certificate, and a precise statement of the rank-dependent comparison. These definitions separate the reusable two-stage model and uncertainty geometry from the coefficients printed in this source. The survey states the result without a proof in this section. The local theorem declarations are proof targets, not machine-checked proofs of the asserted containments.

Mathematical and source difficulties

When the recourse matrix depends on uncertainty, substitution of an affine rule produces quadratic terms in $u$. The fixed-recourse linear reduction therefore does not describe this setting. An intersection of ellipsoids also differs from the single-ellipsoid case. Neither simplifying restriction is made here.

There is a substantive source issue: the printed $\beta$ formula differs from the linear term in the expansion immediately above it. The recorded scalar counterexample I1 satisfies the ellipsoidal assumptions and admits a zero PSD certificate, yet violates the original constraint. It therefore contradicts the printed safety assertion and the right inclusion with these coefficients. The mission preserves that literal assertion for assessment, including disproof; it does not replace it with a corrected theorem or assume the disputed residual identity.

Formalization scope and conventions

Finite coordinates use Fin, with zero-based indices. Matrices and real positive semidefiniteness use Mathlib. Real matrix ranks are natural numbers coerced to reals inside the natural logarithm. Positive radius and positive total rank in Theorem 7 exclude undefined inputs in the displayed formulas; positive total rank already forces a nonempty matrix family and uncertainty dimension. Theorem 6 has no rank restriction. Empty decision-coordinate sets use their ordinary finite-dimensional conventions.

The original AARC is evaluated directly from the two uncertain matrices and the affine policy. Its definition never depends on the certificate. The SDP eliminates only its multipliers, preserving every coefficient of $\chi$. There are $m$ PSD blocks of order $L+1$ and $n_1+(L+1)n_2+mK$ scalar decision variables. No attainment, compactness, fixed recourse, integrality, or sampled-uncertainty assumption is introduced. The general affine-rule evaluation reuses a published definition; its unrelated lot-sizing constraints are not imposed.

Selected references

• Dimitris Bertsimas, David B. Brown and Constantine Caramanis, Theory and Applications of Robust Optimization, arXiv:1010.5445v1, §§4.2–4.3.1, Theorems 6–7. The formalization cites the supplied 50-page artifact bearing this stamp, SHA-256 25714e004b9b868fcb48997d3364800e379cd1be5f8b027ca6f50ee08f25ae50. It also bears an inconsistent “Revised version: November 26, 2024” line. Its printed pages 25–26 are PDF pages 26–27. The journal metadata identifies SIAM Review (2011), DOI 10.1137/080734510, but that journal artifact and its numbering were not independently verified. No journal pagination is used here.

Perishable Inventory Theory: A Review: Convex costs and age-sensitive optimal ordering

Motivation

Perishability makes inventory age matter. Two warehouses with the same total stock can face different expiration risks and choose different replenishments. Nahmias’ 1982 review collects structural results for these decisions and contrasts fixed shelf lives with random lifetimes and proportional decay.

Setting

The central model has iid nonnegative demand with a density, zero delivery lag, FIFO service, proportional procurement costs, and a fixed lifetime of m periods. The state records stock in each of the m−1 remaining-life categories and any outstanding backlog. Lost sales and full backordering are separate cases. Expected holding and shortage costs are convex. Fries charges current expiration; Nahmias charges the expected eventual expiration of the order placed now. The terminal condition is either zero or the stated salvage/emergency-purchase value.

Target

The goal states convexity of both actual Bellman objectives in the nonnegative real order quantity and existence of an optimal selector. Its age derivatives obey −1 ≤ yₙ⁽¹⁾ ≤ ⋯ ≤ yₙ⁽ᵐ⁻¹⁾ < 0 in the positive ordering region, for n ≥ m in Fries’ accounting and n ≥ 1 in Nahmias’ accounting. With salvage, the ordering region is total stock x < x̄. The post-order stock satisfies yₙ(0) ≤ x+yₙ(𝐱) ≤ x̄, with equality at the lower bound for negative net stock. The comparison with nonperishable ordering and its dependence on starting stocks are included. The backorder threshold uses the displayed quantile; the lost-sales threshold comes from its associated nonperishable objective.

Significance

The goal expresses why total stock alone cannot describe optimal replenishment: newer inventory has a larger marginal effect on the order quantity. The review’s accounting models describe the same physical inventory but charge expiration at different times. Their correspondence is one of the milestones.

Difficulty

A formal statement must keep physical expiration separate from expected charges, distinguish demand from backlog, preserve the whole age vector, and handle minimizers and demand distributions without artificial grids or finite-state restrictions. Continuous-review policies and stationary laws require their own operational models.

Formalization scope

This is one survey mission with a goal, ten definition modules and twenty-four independent literature-result milestones. The milestones cover fixed-life EOQ, newsvendor separation, two-period and general-lifetime expiration identities, sensitivity and ordering regions, the two accounting conventions, continuous-review ordering and cycle costs, stationary base-stock processes, FIFO issuance, fixed replenishment, warehouse allocation, exponential survival, deterministic decay, myopic policies and stationary density equations. They are not presented as a proof dependency chain.

Orders and stock quantities are real except for the single-unit Poisson model. Expectations and optimization use extended values where required; theorems assert attainment rather than assuming their own conclusions. Published newsvendor and Poisson definitions are reused. Every mathematical encoding or reading is listed on its item. Printed claims are retained even where explicit counterexamples have been recorded in the companion insights; corrected variants are not mission items.

References

Steven Nahmias, “Perishable Inventory Theory: A Review,” Operations Research 30(4), 680–708 (1982), DOI:10.1287/opre.30.4.680. The central results are reported in §1.2.a(ii), pp. 685–687, with attribution to Fries [1975], Nahmias [1975a, 1977a], and Nahmias and Pierskalla [1975]. Each milestone cites the review’s own page and identifies the original work it reports. The mission uses the published review as its sole citation basis.

Motivation

A pure entangled state of two parties can be converted reversibly, in the limit of many copies, into singlets: $N$ copies of $\psi_{AB}$ yield about $N\,S(\rho_A)$ singlets and can be recovered from them (Bennett, Bernstein, Popescu, Schumacher 1996). For bipartite pure states the singlet is therefore the only kind of entanglement. For three or more parties the question is whether every pure state is, asymptotically and reversibly, equivalent to a collection of two-party singlets, or whether genuinely multiparty kinds of entanglement exist.

The three-party GHZ state $\tfrac{1}{\sqrt2}(|000\rangle + |111\rangle)$ is the natural test case. Its one-party entropies can be matched by one singlet per pair for every two GHZ states, and a single GHZ state can be turned into a singlet between any chosen pair. Linden, Popescu, Schumacher and Westmoreland (arXiv:quant-ph/9912039, 1999) answered the question with a quantitative constraint on all local protocols, eq. (22), which this mission formalizes.

Timeline.

• 1996: Bennett, Bernstein, Popescu and Schumacher show reversible concentration of bipartite pure-state entanglement into singlets.
• 1997–1998: Vedral, Plenio and coauthors define the relative entropy of entanglement $E_r$ and show that it does not increase on average under local operations and classical communication (Vedral–Plenio 1998).
• 1999: Bennett, Popescu, Rohrlich, Smolin and Thapliyal show that the four-party GHZ state cannot be converted reversibly into singlets, using one- and two-party entropies; the three-party case remains open (arXiv:quant-ph/9908073).
• 1999: Linden, Popescu, Schumacher and Westmoreland prove (22) and deduce that the three-party GHZ state is not reversibly equivalent to singlets.

Setting

Alice, Bob and Claire hold finite-dimensional systems $\mathbb C^A$, $\mathbb C^B$, $\mathbb C^C$; each system includes all copies of the initial state and all ancillas, so the dimensions never change. The joint state is a unit vector $\psi\in\mathbb C^A\otimes\mathbb C^B\otimes\mathbb C^C$.

A local step is one party applying a finite family of operators $K_1,\dots,K_n$ on their own system with $\sum_k K_k^\dagger K_k = I$. Outcome $k$ occurs with probability $p_k=\|\varphi_k\|^2$, where $\varphi_k$ is $K_k$ applied to that party's factor of $\psi$, and the state becomes the pure state $\varphi_k/\|\varphi_k\|$. A measurement with spectral projectors $P_k$, and a unitary $U$, are local steps. A local protocol is a finite tree of such steps: after each outcome is broadcast, the next step (by any party) may depend on all outcomes so far. Each final branch is a pure state with a probability, and $\langle f\rangle_{\text{final}}$ denotes the probability-weighted average of a quantity $f$ over the final branches.

For a pure state $\psi$ let $\rho^{BC}=\operatorname{Tr}_A|\psi\rangle\langle\psi|$ and $\rho^A=\operatorname{Tr}_{BC}|\psi\rangle\langle\psi|$. The relative entropy is $S(\rho\|\sigma)=\operatorname{Tr}\rho\ln\rho-\operatorname{Tr}\rho\ln\sigma$ (eq. (9)), equal to $+\infty$ unless $\operatorname{supp}\rho\subseteq\operatorname{supp}\sigma$. The relative entropy of entanglement of Bob and Claire is

$$E_r(\rho^{BC})=\min_{\sigma\ \text{separable}} S(\rho^{BC}\|\sigma),$$

the minimum over finite convex combinations of product states $\sigma^B\otimes\sigma^C$ (eq. (11)). $S(A)=-\operatorname{Tr}\rho^A\ln\rho^A$ is Alice's entropy, her entanglement with Bob and Claire. All logarithms are natural.

Formalization targets

Goal: eq. (22)

For every finite-dimensional $A,B,C$, every initial unit vector $\psi$ and every local protocol,

$$\langle E_r(BC)\rangle_{\text{final}}-E_r(BC)_{\text{initial}}\;\le\;S(A)_{\text{initial}}-\langle S(A)\rangle_{\text{final}}.$$

Milestones, in the order of the paper's argument

• (8) After Alice measures, $\rho^{BC}=\sum_k p_k\rho^{BC}_k$.
• (10) Donald's identity: $\sum_k p_kS(\rho_k\|\sigma)=\sum_kp_kS(\rho_k\|\rho)+S(\rho\|\sigma)$ for $\rho=\sum_kp_k\rho_k$.
• (13) For one measurement by Alice, $\sum_kp_kE_r(\rho^{BC}_k)-E_r(\rho^{BC})\le\sum_kp_kS(\rho^{BC}_k\|\rho^{BC})=S(\rho^{BC})-\sum_kp_kS(\rho^{BC}_k)=S(\rho^A)-\sum_kp_kS(\rho^A_k)$.
• (14) Local unitaries leave $E_r(\rho^{BC})$ and $S(\rho^A)$ unchanged.
• (15) The bound for Alice's whole round: measurement, broadcast, outcome-dependent unitaries by all three parties.
• (17)–(18) A measurement by Bob (or Claire) leaves $\rho^A$ unchanged on average, so $S(\rho^A)\ge\sum_kp_kS(\rho^A_k)$.
• (21) $E_r(\rho^{BC})\ge\sum_kp_kE_r(\tilde\rho^{BC}_k)$ for a local measurement by Bob or Claire followed by local unitaries.
• After (21) The bound (15) holds for a step by any party.

Significance

The inequality says that the bipartite entanglement of Bob and Claire, measured by $E_r$, can grow on average only by consuming Alice's entanglement with them. In a reversible protocol both directions satisfy the bound and average entropies cannot change, so the average $E_r$ of every pair is conserved. Since $E_r$ of the Bob–Claire marginal of a GHZ state is $0$ while a Bob–Claire singlet has $E_r=\ln 2$, GHZ states cannot be converted reversibly into singlets, even asymptotically: three-party pure-state entanglement is not all of singlet type. The same argument, with the parties grouped into three, shows that genuine $n$-party entanglement exists for every $n$. Conservation of the one-party entropies and of the pairwise $E_r$ also fixes how many GHZ states and singlets can be extracted from a state when reversible extraction is possible (eq. (23)).

The result is proved in the paper, apart from the monotonicity (21), which the paper quotes from Vedral and Plenio. No machine-checked proof of (22), of the LOCC monotonicity of $E_r$, or of Donald's identity in this form is known to exist. Formalizing the mission produces a finite-dimensional model of pure-branch LOCC protocols, a library form of $E_r$ with its basic properties, and the monotonicity theorem (21), which is used throughout entanglement theory.

Difficulty

Most steps are finite-dimensional linear algebra: the no-signalling identities (8) and (17), Donald's identity, the equality of the entropies of the two marginals of a pure state (Schmidt decomposition), and concavity of the von Neumann entropy. Two points carry the weight.

The first is (21). It does not follow from (13): Bob's measurement changes $\rho^{BC}$ itself, and the argument needs the monotonicity of the relative entropy under the quantum channel $\rho\mapsto\bigoplus_k(K_k\otimes I)\rho(K_k\otimes I)^\dagger$, that is, the data-processing inequality, whose known proofs go through strong subadditivity or Lieb's concavity theorem. The choice of separable comparison state for each branch, $\sigma_k\propto(K_k\otimes I)\sigma(K_k\otimes I)^\dagger$, must also be shown separable.

The second is bookkeeping with infinite values. Relative entropies are $+\infty$ off support, and the printed identities subtract such quantities; the statements are therefore in additive form, and every proof must track supports and zero-probability branches. The final induction over the protocol tree has to scale the bound for a branch by the branch's probability.

Formalization scope

• The local systems are arbitrary finite index types A, B, C (B, C nonempty); the joint index type is A × (B × C), Alice first. QAlgorithms.traceLeft traces out Alice, QAlgorithms.traceRight traces out Bob and Claire.
• Local steps are complete families of square matrices (IsKrausFamily), which contain the paper's projective measurements and unitaries. Every branch is kept and no subsystem is discarded, as on p.2 of the paper.
• Protocol is an inductive finite tree with one step constructor per party; Protocol.IsLocal requires every step to be complete; Protocol.avg computes $\langle f\rangle_{\text{final}}$ on unnormalized branch vectors, weighting the normalized leaf state by its squared norm.
• relEntropy takes values in ℝ≥0∞ and is ⊤ off support; relEntEnt is the infimum over QAlgorithms.Entanglement.IsSeparableDensity; the entropy is the published natural-log Information100.P56.entropy. All inequalities are stated in ℝ≥0∞ in additive form, ⟨E_r⟩_f + ⟨S(A)⟩_f ≤ E_r,i + S(A)_i, which is equivalent because every term is finite.
• The goal has no hypothesis about $E_r$: its LOCC monotonicity is milestone (21), not an assumption. Without Protocol.IsLocal or without ‖ψ‖ = 1 the statement would be false; both are hypotheses.

Contributions are welcome on each milestone; the monotonicity of the relative entropy under channels and the separability-preservation lemmas are reusable well beyond this mission.

Selected references

• N. Linden, S. Popescu, B. Schumacher, M. Westmoreland, Reversibility of local transformations of multiparticle entanglement, arXiv:quant-ph/9912039v1, 1999. https://arxiv.org/abs/quant-ph/9912039
• C. H. Bennett, H. J. Bernstein, S. Popescu, B. Schumacher, Concentrating partial entanglement by local operations, Phys. Rev. A 53, 1996. https://arxiv.org/abs/quant-ph/9511030
• C. H. Bennett, S. Popescu, D. Rohrlich, J. A. Smolin, A. V. Thapliyal, Exact and asymptotic measures of multipartite pure state entanglement, Phys. Rev. A 63, 012307, 2000. https://arxiv.org/abs/quant-ph/9908073
• V. Vedral, M. B. Plenio, Entanglement measures and purification procedures, Phys. Rev. A 57, 1619, 1998. https://arxiv.org/abs/quant-ph/9707035
• M. Ohya, D. Petz, Quantum Entropy and Its Use, Springer, 1993 (the paper's reference for Donald's identity (10)). https://doi.org/10.1007/978-3-642-57997-4

Motivation

Cryptographic protocols are usually proved secure by showing that what an adversary sees in the real protocol is indistinguishable from what it would see in an ideal one, typically with a distinguishing advantage that decays exponentially in a security parameter. Classically there are several ways to measure how distinguishable two probability distributions are: the probability of guessing wrong, the total variation (Kolmogorov) distance, the Bhattacharyya overlap, and the mutual information between the source label and the sample. For quantum protocols, such as quantum key distribution, the adversary holds quantum states and may choose any measurement, so each classical measure has a quantum counterpart obtained by optimising over measurements.

Fuchs and van de Graaf (arXiv:quant-ph/9712042) collected these four measures for pairs of density matrices and proved inequalities between them. The inequality $1 - F \le \tfrac12\|\rho_0-\rho_1\|_1 \le \sqrt{1-F^2}$ between trace distance and fidelity, now called the Fuchs–van de Graaf inequality, is one of the most used tools of quantum information theory. The paper's main result, Theorem 1, contains it together with two-sided bounds on the quantum Shannon distinguishability, which has no closed formula.

Setting

Fix equal prior probabilities $\pi_0 = \pi_1 = \tfrac12$. For probability distributions $p_0, p_1$ on a finite set $\mathcal X$:

• probability of error $\mathrm{PE}(p_0,p_1) = \tfrac12\sum_x \min\{p_0(x),p_1(x)\}$;
• Kolmogorov distance $K(p_0,p_1) = \tfrac12\sum_x |p_0(x)-p_1(x)|$;
• Bhattacharyya coefficient $B(p_0,p_1) = \sum_x \sqrt{p_0(x)p_1(x)}$;
• Shannon distinguishability $\mathrm{SD}(p_0,p_1) = I(T;X) = H(p) - \tfrac12 H(p_0) - \tfrac12 H(p_1)$, where $T$ is a fair coin, $X\sim p_T$, $p = \tfrac12(p_0+p_1)$ and $H$ is the Shannon entropy in bits.

$H_2(x) = -x\log_2 x - (1-x)\log_2(1-x)$ is the binary entropy.

A density matrix is an $N\times N$ complex positive semidefinite matrix of trace one, $N$ finite. A POVM $E = \langle E_1,\dots,E_m\rangle$ is a finite family of positive semidefinite matrices summing to the identity; the number $m$ of outcomes is arbitrary. Measuring $\rho$ with $E$ gives the distribution $p(E)(x) = \mathrm{Tr}(\rho E_x)$. For two states $\rho_0,\rho_1$ the quantum measures are

$$\mathrm{PE}(\rho_0,\rho_1) = \inf_{E} \mathrm{PE}(p_0(E),p_1(E)),\quad K(\rho_0,\rho_1) = \sup_{E} K(\cdot),\quad B(\rho_0,\rho_1) = \inf_{E} B(\cdot),\quad \mathrm{SD}(\rho_0,\rho_1) = \sup_{E} \mathrm{SD}(\cdot),$$

each over all POVMs. Finally $\mathrm{Tr}|\rho_0-\rho_1|$ is the trace norm of the difference.

Formalization targets

Goal: Theorem 1 (p.17)

For all density matrices $\rho_0,\rho_1$ of any finite size, the quantum versions of the three relations of Proposition 5 hold,

$$1-B \le K \le \sqrt{1-B^2},\qquad 1 - H_2(\mathrm{PE}) \le \mathrm{SD} \le 1 - 2\,\mathrm{PE},\qquad 1 - B \le \mathrm{SD} \le 1 - H_2\Big(\tfrac12 - \tfrac12\sqrt{1-B^2}\Big),$$

and so do their trace-norm forms

$$1 - B \le \tfrac12\mathrm{Tr}|\rho_0-\rho_1| \le \sqrt{1-B^2},\qquad 1 - H_2\big(\tfrac12 - \tfrac14\mathrm{Tr}|\rho_0-\rho_1|\big) \le \mathrm{SD} \le \tfrac12\mathrm{Tr}|\rho_0-\rho_1| .$$

The printed (45) and (48) have $\sqrt{1-B}$ in place of $\sqrt{1-B^2}$; the paper's proof (eq. (72)) has the square, and the printed form fails for $\rho_0 = |0\rangle\langle 0|$, $\rho_1 = |{+}\rangle\langle{+}|$. The goal states the corrected form.

Milestones

1. Proposition 2: $\mathrm{PE}(p_0,p_1) = \tfrac12 - \tfrac12 K(p_0,p_1)$.
2. Eq. (82): $2\min\{x,1-x\} \le H_2(x) \le 2\sqrt{x(1-x)}$ on $[0,1]$.
3. Convexity of $r\mapsto H_2(\tfrac12-\tfrac12\sqrt{1-r^2})$ on $[-1,1]$.
4. Proposition 5, eqs. (43), (44), (45) (the last corrected), for classical distributions.
5. Proposition 1 (Helstrom): $\mathrm{PE}(\rho_0,\rho_1) = \tfrac12 - \tfrac14\sum_j|\lambda_j| = \tfrac12 - \tfrac14\mathrm{Tr}|\rho_0-\rho_1|$, with $\lambda_j$ the eigenvalues of $\rho_0-\rho_1$.
6. Proposition 3: $K(\rho_0,\rho_1) = \tfrac12\sum_j|\lambda_j| = \tfrac12\mathrm{Tr}|\rho_0-\rho_1|$.

Significance

The trace-norm/Bhattacharyya inequality (46) is the standard bridge between trace distance and fidelity, used in continuity bounds, in the analysis of approximate state preparation, and throughout quantum cryptography. Because the quantum $B$ equals the fidelity $\mathrm{Tr}\sqrt{\sqrt{\rho_0}\rho_1\sqrt{\rho_0}}$ (Fuchs–Caves, cited in the paper and not part of this mission), (46) is the usual Fuchs–van de Graaf inequality once that identity is available. The bounds (47)–(48) are the only general handle on the accessible information of two equiprobable states, and the paper uses them to show that exponential indistinguishability is the same notion whichever of the four measures is used (Theorem 2).

The results are classical and proved in the paper. What this mission adds is a machine-checked development: the four measures defined as optimisations over all POVMs (any number of outcomes, not only projective or two-outcome measurements), Helstrom's theorem in that generality, and the full set of six two-sided inequalities. On Prove2Me a related upper half of (46) is proved with the root fidelity in place of $B$ (QAlgorithms.Papers.Independent.Claimed50.P12.lemmaB_1), a Jensen–Shannon versus total variation bound is proved in nats (OAI.EntropyRateDimension.FiniteEntropy.js_le_tv), and Helstrom's formula restricted to two-outcome measurements is an open goal (QAlgorithms.Papers.Independent.Bridge50.P44.helstrom_equal_prior). None of these states Theorem 1 or uses the POVM-optimised $B$.

Difficulty

The classical inequalities are elementary except for two points: the left half of (44) is the binary Fano inequality, and the right half of (45) needs the convexity of $H_2(\tfrac12 - \tfrac12\sqrt{1-r^2})$, a one-variable fact whose derivative computation degenerates at the endpoints where $\sqrt{1-r^2}$ has infinite slope.

On the quantum side the paper's argument picks optimal measurements $E^*_B$, $E^*_K$. With infima and suprema those may not be available a priori, so each step must go through approximating sequences of POVMs, and the left halves of (44) and (47) additionally need continuity and monotonicity of $H_2$ on $[0,\tfrac12]$. Proposition 1 needs both directions: a lower bound on the error of every POVM, including ones with more outcomes than the dimension, and the Helstrom projective measurement attaining it. The trace norm is defined as $\mathrm{Tr}\sqrt{\Gamma^\dagger\Gamma}$, so relating it to the eigenvalues of the Hermitian $\Gamma = \rho_0-\rho_1$ needs the spectral theorem.

Formalization scope

Density matrices are Matrix n n ℂ over an arbitrary finite index type n satisfying WildeQIT.IsDensityOperator (positive semidefinite, trace one). The trace norm is WildeQIT.traceNorm and the binary entropy is WildeQIT.binaryEntropy (bits), both published definitions reused here. Classical distributions are functions on a finite type with IsProbDist. POVMs are families E : Fin m → Matrix n n ℂ for every m : ℕ. Probabilities are real parts of traces. Each quantum measure is the real sInf or sSup of the set of its values at all POVMs. That set is nonempty (the one-outcome POVM) and bounded on the relevant side, so no junk value of an empty or unbounded optimisation can enter. The paper's min/max is read as inf/sup, following its own remark on p.10. Shannon distinguishability is defined through the expansion $H(p) - \tfrac12H(p_0) - \tfrac12H(p_1)$, which avoids the $0/0$ of the form $1 - \sum_x p(x)H_2(r_0(x))$.

A trivializing formalization is ruled out explicitly: replacing $B(\rho_0,\rho_1)$ by the fidelity formula, restricting to two-outcome or projective measurements, or taking an infimum over an empty family of POVMs would each state a different theorem.

Proofs of any milestone are welcome, as are reusable lemmas: nonnegativity of $\mathrm{Tr}(\rho E)$, outcome distributions as probability distributions, the binary Fano inequality, and the spectral form of the trace norm of a Hermitian matrix.

Selected references

• C. A. Fuchs and J. van de Graaf, Cryptographic Distinguishability Measures for Quantum Mechanical States, IEEE Trans. Inf. Theory 45(4), 1999; preprint arXiv:quant-ph/9712042v2, 1998. https://arxiv.org/abs/quant-ph/9712042
• C. W. Helstrom, Quantum Detection and Estimation Theory, Academic Press, 1976. https://doi.org/10.1016/S0076-5392(08)60247-7
• C. A. Fuchs and C. M. Caves, Mathematical techniques for quantum communication theory, Open Syst. Inf. Dyn. 3, 345–356, 1995. https://arxiv.org/abs/quant-ph/9604001
• T. M. Cover and J. A. Thomas, Elements of Information Theory, Wiley, 1991 (Fano's inequality). https://doi.org/10.1002/0471200611