All missions

Why wholesale prices and targets

A wholesale price contract is the simplest agreement between a supplier and a retailer: the supplier names a unit price and the retailer chooses how much to buy. It is widely used and it is known to be inefficient when both firms maximize expected profit. The retailer bears all the demand risk and orders less than a centralized firm would, the double marginalization effect of Spengler (1950). The price-only model of Lariviere and Porteus (2001) is the standard reference for this game, and the survey of Cachon (2003) records the accepted conclusion that a wholesale price contract does not coordinate a supply chain.

That conclusion assumes risk-neutral firms. Many firms instead plan around targets. Brown and Sim (2009) proposed the CVaR-satisficing measure, which scores a random payoff by how robustly it reaches a target, and Chen, Long and Perakis (2015) applied it to the newsvendor. Chen and Tang (2021) ask what happens to the supply chain as a whole when the retailer is target-oriented. This mission formalizes their answer for the total supply-chain profit.

Setting

A supplier with marginal cost $c$ sells to a retailer at wholesale price $w$. The retailer sells at a fixed retail price $p$ and faces demand $D$ uniformly distributed on $[a,a+b]$, with $0<c<p$, $a\ge0$, $b>0$. Unsold units have no salvage value and unmet demand is lost. An order $y\ge0$ yields the random retailer profit

$$V(y;D)=p\min\{D,y\}-wy .$$

The extended CVaR of a random variable $V$ at level $\eta\in(-1,1)$ is a tail average: for $\eta\ge0$ the average of the worst $1-\eta$ of the distribution, and for $\eta<0$ the average of the best $1+\eta$. The CVaR-satisficing measure with target $\tau$ is

$$\rho_\tau(V)=\sup\{\eta\in(-1,1):\ \mathrm{CVaR}_\eta(V)\ge\tau\}$$

when that set is nonempty, and $-1$ otherwise.

The supplier is a Stackelberg leader and maximizes $(w-c)y$. A risk-neutral retailer answers $w$ with an order maximizing $\mathbb E[V(y;D)]$. A target-oriented retailer with target coefficient $\alpha^r$ answers with an order maximizing $\rho_{\tau^r}(V(y;D))$, where $\tau^r=\alpha^r(p-w)$. These are the settings "NN" and "NT". Write $\xi^c=(p-c)/p$ for the critical fractile. The total profit at a decision pair is $\Pi=(w-c)y+p\,\mathbb E[\min(D,y)]-wy$, and the centralized profit is $\Pi^c_{nn}(y)=p\,\mathbb E[\min(y,D)]-cy$, with maximum $\Pi^{c*}_{nn}$ over $y\ge0$.

Formalization targets

Goal: Proposition 8

For $\alpha^r\in\mathrm{Dom}=\{\alpha^r: 0<\alpha^r,\ a\le\alpha^r<a+b\}$, NN and NT outcomes exist, and there are thresholds $\bar\alpha^{r1}_I,\bar\alpha^{r2}_I$ such that

$$\Pi^*_{nt}\le\Pi^*_{nn}\ \text{ if }\ \alpha^r\le\bar\alpha^{r1}_I\ \text{ or }\ \alpha^r\ge\bar\alpha^{r2}_I,\qquad \Pi^*_{nt}\ge\Pi^*_{nn}\ \text{ if }\ \alpha^r\in(\bar\alpha^{r1}_I,\bar\alpha^{r2}_I);$$

$\Pi^*_{nt}$ is concave in $\alpha^r$ from $\bar\alpha^{r1}_I$ on and attains its maximum at $\alpha^r=b\xi^c+a$; and

$$\Pi^*_{nt}=\Pi^{c*}_{nn}\quad\text{at}\quad\alpha^r=b\xi^c+a .$$

The thresholds are existential, as printed, and one pair serves the first two parts. Every clause is part of the goal.

Milestones

In the order the paper's argument uses them:

1. the centralized solution for uniform demand (display after (8), p.11);
2. the NN solution (9)–(10) and footnote 6 (p.12);
3. the uniform clause of Lemma 1, the target-oriented retailer's order $y(w)$ (Online Appendix p.1);
4. Proposition 2, the NT decisions in the three target regimes (p.13);
5. the step $y^*_{nt}=y^1_{nt}\le y^*_{nn}$ for $\alpha^r\in[\alpha^{r1}_{nt},\alpha^{r2}_{nt})$ from the proof of Proposition 6 (Online Appendix p.6), which the proof of Proposition 8 cites.

Significance

The result. Part 3 is the paper's contribution to the coordination literature: with a suitably chosen target, a wholesale price contract alone delivers the first-best supply-chain profit. Parts 1 and 2 locate it. Total profit rises above the risk-neutral level only on a middle band of targets, so both a modest and an overly ambitious retailer leave the chain no better off. The paper's other comparisons (Proposition 7 on the firms' individual profits, Propositions 9 to 17 on the other settings) are not part of this mission.

The formalization. The results are proved in the paper's Online Appendix. They have no machine-checked proof on this platform: the goal and the milestones are all new statements here. The mission adds to the platform an extended, two-sided CVaR, the Brown–Sim satisficing measure with its infeasible branch, and a price-only newsvendor Stackelberg game in which the leader's supremum need not be attained. Building these exposes three places where the printed statements need a correction or a precise reading, listed under Formalization scope.

Difficulty

The retailer's objective is not expected profit, so the classical critical-fractile calculation does not apply. Finding the order that maximizes the satisficing measure means working with tail averages of a law that has an atom, because every unit beyond realized demand is wasted and every order caps sales. The retailer's reaction then has two regimes with a kink, which depend on whether the optimal measure is positive or negative, and the supplier optimizes against that kinked reaction. The supplier's problem has three target regimes: in one the optimum sits at the kink, in one it has a radical closed form, and in one the supremum is not attained. The comparison in Proposition 8 has to hold across all of these regimes and across the two regimes of the risk-neutral benchmark.

Formalization scope

Representation. Demand is the law $(1/b)\cdot$Lebesgue measure restricted to $[a,a+b]$, and $V(y;D)$ is its push-forward. CVaR is defined from the quantile function $Q_V$ (the published RiskFunctionals_StochDominance_QuantileFunction) as the average of $Q_V$ over $(0,1-\eta]$, respectively $(-\eta,1]$. Best responses are defined as maximizers of (6) and (7) over $y\ge0$. None of the closed forms of the retailer's reaction or of the equilibria is a definition. Only the quantities $\alpha^{r1}_{nt},\alpha^{r2}_{nt},w^1_{nt},y^1_{nt}$ named by Proposition 2 are transcribed.

Conventions and corrections.

• Quantile averages. The paper's conditional expectations presuppose a unique $\eta$-quantile. $V(y;D)$ has an atom at $(p-w)y$, so that quantile does not exist in general, and the average form is used.
• The excluded endpoint. $\alpha^r=a+b$, which the paper's ranges include, is excluded. There every order has satisficing measure $-1$, every $y\ge0$ is a best response, and the NT outcome is undefined.
• Lemma 1 at $w=p$. The uniform clause is stated for $w\in[c,p)$. At $w=p$ the printed value $\alpha^r$ is wrong: the maximizers are exactly $[0,a]$, as the paper itself says on p.13.
• "$p-\epsilon$". The paper's "infinitely small" $\epsilon$ is read as a limit. An outcome is a limit of pairs $(w_n,y_n)$ with $w_n\in[c,p)$, $y_n$ a best response, and supplier profits tending to the supremum. Profits at an outcome are evaluated at the limit pair.
• Conditions on $b/a$ are written without division, for example $b\xi^c\le2a$, so that $a=0$ means $b/a=+\infty$.

Non-triviality. Outcome statements are quantified over all outcomes and also assert that outcomes exist, so they cannot hold vacuously.

Infrastructure. A complete development needs tail-average calculus for laws with one atom and the attainment and uniqueness analysis for the two retailer problems. The extended CVaR and satisficing measure are reusable beyond this mission. Contributions welcome: the general log-concave analogues of the milestones, and the paper's other settings as further statements.

Selected references

• J. J. Spengler, Vertical integration and antitrust policy, Journal of Political Economy 58(4), 1950, 347–352. https://doi.org/10.1086/256962
• M. A. Lariviere, E. L. Porteus, Selling to the newsvendor: An analysis of price-only contracts, Manufacturing & Service Operations Management 3(4), 2001, 293–305. https://doi.org/10.1287/msom.3.4.293.9971
• G. P. Cachon, Supply chain coordination with contracts, Handbooks in Operations Research and Management Science 11, 2003, 227–339. https://doi.org/10.1016/S0927-0507(03)11006-7
• D. B. Brown, M. Sim, Satisficing measures for analysis of risky positions, Management Science 55(1), 2009, 71–84. https://doi.org/10.1287/mnsc.1080.0929
• L. G. Chen, D. Z. Long, G. Perakis, The impact of a target on newsvendor decisions, Manufacturing & Service Operations Management 17(1), 2015, 78–86. https://doi.org/10.1287/msom.2014.0500
• L. G. Chen, Q. Tang, Supply chain performance with target-oriented firms, SSRN 3533746, version of July 6, 2021, with Online Appendix. https://ssrn.com/abstract=3533746

Motivation

Many resource allocation problems ask for a vector $x$ in a feasible set $C\subseteq\mathbb R^n$ that minimizes a symmetric convex cost: the variance of a load profile in energy scheduling, the makespan of a schedule, an egalitarian division of a joint gain. Different symmetric objectives usually have different minimizers, so the choice of objective matters. For one important class of feasible sets it does not: on the base polyhedron of a submodular function there is a single point that minimizes every separable convex objective at once, and even every Schur-convex objective. This "simultaneous optimization" property goes back to Fujishige's lexicographically optimal bases for $b=0$, and was established for scaled and shifted objectives by Schoot Uiterkamp, Gerards and Hurink (On a reduction for a class of resource allocation problems, INFORMS Journal on Computing, 2022).

The paper behind this mission, M. H. H. Schoot Uiterkamp, A characterization of simultaneous optimization, majorization, and (bi)submodular polyhedra (arXiv:2201.06596v2, 2023; later in Mathematics of Operations Research), asks the converse: which sets have this property for every scaling and every shift? Its answer, Theorem 5, is that among compact convex sets these are exactly the base polyhedra. The result explains why trade-offs between symmetric objectives are unavoidable in allocation problems whose feasible set is not a base polyhedron, and it yields a characterization of convex cooperative games through egalitarian solutions (Theorem 9 of the paper).

Setting

Let $N=\{1,\dots,n\}$ and $2^N$ its power set. For $x\in\mathbb R^n$ and $S\subseteq N$ write $x(S)=\sum_{i\in S}x_i$.

A set function $f:2^N\to\mathbb R$ is submodular if $f(\emptyset)=0$ and $f(A)+f(B)\ge f(A\cup B)+f(A\cap B)$ for all $A,B$. Its submodular polyhedron and base polyhedron are

$$P(f)=\{x\in\mathbb R^n: x(A)\le f(A)\ \forall A\in 2^N\},\qquad B(f)=\{x\in P(f): x(N)=f(N)\}.$$

For $x\in\mathbb R^n$ let $x^{\downarrow}$ be its non-increasing rearrangement. Then $x$ is majorized by $y$, $x\prec y$, if $\sum_{i\le k}x^{\downarrow}_i\le\sum_{i\le k}y^{\downarrow}_i$ for all $k$ and $x(N)=y(N)$. A function $\Phi:\mathbb R^n\to\mathbb R$ is Schur-convex if $x\prec y$ implies $\Phi(x)\le\Phi(y)$.

Fix a scaling vector $a\in\mathbb R^n_{>0}$ and a shift $b\in\mathbb R^n$. A vector $x$ is $(a,b)$-majorized by $y$, $x\prec_{(a,b)}y$, if $x(N)=y(N)$ and

$$\sum_{i\in N}a_i\,\phi\Big(\frac{x_i+b_i}{a_i}\Big)\le\sum_{i\in N}a_i\,\phi\Big(\frac{y_i+b_i}{a_i}\Big)$$

for every continuous convex $\phi:\mathbb R\to\mathbb R$. It is weakly $(a,b)$-supermajorized, $x\prec^{\uparrow}_{(a,b)}y$, if the same inequality holds for every non-increasing continuous convex $\phi$ (no sum condition). A point $x\in C$ is a least $(a,b)$-majorized element of $C$ if $x\prec_{(a,b)}y$ for all $y\in C$, and similarly for the weak version. For a set $C$ define $f_C(A)=\max_{x\in C}x(A)$.

Formalization targets

Goal: Theorem 5 (p.18)

For a compact convex $C\subseteq\mathbb R^n$ the following are equivalent:

1. $C$ has a least $(a,b)$-majorized element for every $a\in\mathbb R^n_{>0}$, $b\in\mathbb R^n$;
2. $C$ has a least $(1,b)$-majorized element for every $b\in\mathbb R^n$;
3. for every $b$ there is one $x^*\in C$ minimizing $\Phi(x+b)$ over $C$ for every continuous Schur-convex $\Phi$;
4. $f_C$ is submodular and $C=B(f_C)$.

All four statements and all six implications are part of the goal, for every $n$ and every compact convex $C$.

Milestones

• Lemma 2 (p.5): every extreme point $z$ of $B(f)$, $f$ submodular, is a greedy vector: for some permutation $\pi$, $z_{\pi(k)}=f(\{\pi(1),\dots,\pi(k)\})-f(\{\pi(1),\dots,\pi(k-1)\})$.
• Lemma 6 (p.7): $x\prec y$ iff $\Phi(x)\le\Phi(y)$ for all continuous Schur-convex $\Phi$, iff $\sum\phi(x_i)\le\sum\phi(y_i)$ for all continuous convex $\phi$, iff $x(N)=y(N)$ and $\sum\max(0,\alpha-x_i)\le\sum\max(0,\alpha-y_i)$ for all $\alpha$.
• Lemma 9 (p.10): for submodular $f$, $B(f)$ has a unique least $(a,b)$-majorized element for every $a\in\mathbb R^n_{>0}$, $b\in\mathbb R^n$; if moreover $f$ and $b$ are integral, every minimizer of $\sum_i\frac12(x_i+b_i)^2$ over $B^{\mathbb Z}(f)=B(f)\cap\mathbb Z^n$ is a least $(1,b)$-majorized element of $B^{\mathbb Z}(f)$.
• Lemma 14 (p.15): if a closed bounded $C$ has a least weakly $(1,b)$-supermajorized element for every $b$, then for every permutation $\pi$ some $x^*\in C$ maximizes all nested sums $\sum_{i\le k}x_{\pi(i)}$ over $C$.
• Lemma 15 (p.16): under that nested-sum condition on a closed bounded $C$, $f_C$ is submodular and $B(f_C)\subseteq\mathrm{co}(C)\subseteq P(f_C)$.

Significance

Theorem 5 turns an optimization property into a polyhedral one. A modeller who needs one allocation that is optimal for all symmetric convex objectives, after any shift by a fixed load $b$, knows exactly when this is possible: precisely when the feasible set is a base polyhedron. Outside that class there is a shift $b$ for which no single point minimizes all Schur-convex objectives of $x+b$, so trade-offs between such objectives cannot be avoided. The equivalence of statements 2 and 4 is also the content of the paper's characterization of convex transferable-utility games by the existence of egalitarian allocations for every shifted game.

The result is proved in the paper; nothing here is open. No part of it is formalized as far as the platform's catalog shows: majorization exists in published form (the definition reused here and Karamata's inequality, the direction (1) ⇒ (3) of Lemma 6), but there is no Lean statement about least majorized elements, the vertices of base polyhedra, or the converse characterization. A complete development would give machine-checked versions of the greedy description of base-polyhedron vertices, the classical characterizations of majorization, and the existence theorem for least $(a,b)$-majorized elements of base polyhedra, each reusable well beyond this paper.

Difficulty

The implication (4) ⇒ (1) is not proved in the paper: it is imported from earlier work of Schoot Uiterkamp, Gerards and Hurink (Lemma 9), so a complete formalization must also formalize that existence result for every scaling $a$ and shift $b$. The converse (2) ⇒ (4) is the paper's contribution and is where the obvious approach fails: knowing that one point minimizes all separable convex objectives says nothing directly about the facets of $C$. The route from the optimization property to the facet structure goes through points that maximize nested sums along every permutation (Lemma 14) and through the vertex description of base polyhedra (Lemma 2, used in Lemma 15); neither is a one-line consequence of the hypothesis. Lemma 6, although classical, needs a genuine argument for "Schur-convex optimality implies majorization", and the shift $b$ cannot be dropped: with $b=0$ only, statement 2 does not force $C$ to be a base polyhedron (for $n\ge 3$, a Euclidean disc in the hyperplane $x(N)=0$ has $0$ as a least $(1,0)$-majorized element).

Formalization scope

Vectors in $\mathbb R^n$ are Fin n → ℝ, indices are 0-based, $2^N$ is Finset (Fin n), permutations are Equiv.Perm (Fin n), and a nested sum $\sum_{i=1}^k x_{\pi(i)}$, $k\in N$, is the sum of x (π i) over i ≤ k for k : Fin n. Majorization is the published definition RetailVariety.Fashion.Majorized; submodularity includes $f(\emptyset)=0$; $P(f)$ and $B(f)$ are real polyhedra defined for every set function, with submodularity as a hypothesis. Continuous convex test functions are ConvexOn ℝ Set.univ φ together with Continuous φ. The maximum $\max_{x\in C}x(A)$ is sSup, which is the maximum for nonempty compact $C$; for $C=\emptyset$ every statement of Theorem 5 is false, so the equivalence holds without a nonemptiness hypothesis. Convexity is assumed in Theorem 5 only; Lemmas 14 and 15 assume closed and bounded sets, as in the paper.

Statement 3 quantifies $\forall b\ \exists x^*\ \forall\Phi$: a single minimizer for all objectives. The reversed order $\forall\Phi\ \exists x^*$ holds for every compact set and would trivialize the theorem. Likewise $(a,b)$-majorization keeps the equal-sum condition $x(N)=y(N)$; without it statement 4 would weaken to $B(f)\subseteq C\subseteq P(f)$.

Contributions are welcome at every level: proofs of the milestones, proof sketches that decompose Lemma 9 or Lemma 2 into smaller steps, and general infrastructure such as Krein–Milman-type representations of compact convex sets in Fin n → ℝ, already available on the platform.

Selected references

• M. H. H. Schoot Uiterkamp, A characterization of simultaneous optimization, majorization, and (bi)submodular polyhedra, arXiv:2201.06596v2, 2023; Mathematics of Operations Research, 2025. https://arxiv.org/abs/2201.06596v2
• M. H. H. Schoot Uiterkamp, M. E. T. Gerards, J. L. Hurink, On a reduction for a class of resource allocation problems, INFORMS Journal on Computing 34(3):1387–1402, 2022 (reference [42] of the paper: Condition 1 and Theorem 1; source of Lemma 9).
• S. Fujishige, N. Tomizawa, A note on submodular functions on distributive lattices, Journal of the Operations Research Society of Japan 26(4):309–318, 1983 (reference [25] of the paper; Theorem 3.4 is Lemma 2).
• S. Fujishige, Submodular Functions and Optimization, 2nd ed., Elsevier, Amsterdam, 2005 (reference [22] of the paper).
• A. W. Marshall, I. Olkin, B. C. Arnold, Inequalities: Theory of Majorization and Its Applications, 2nd ed., Springer, 2011. https://doi.org/10.1007/978-0-387-68276-1

Motivation

Financial products, insurance and many other goods are sold through advisors whose pay comes from the product providers. A large policy literature asks whether such advice is biased and how regulation should respond; a common answer is liability: make the advisor bear more of the cost of an unsuitable recommendation, through penalties, fiduciary duties or professional standards. Earlier models with linear commissions (Inderst and Ottaviani, 2012) predict that higher liability makes the advisor less responsive to commissions and so reduces the bias.

Honda, Inderst and Ottaviani (SSRN 4125013, published in Management Science, 2023, doi:10.1287/mnsc.2023.4750) observe that real compensation is nonlinear: volume bonuses are paid when an advisor reaches a sales target. With two customers and a bonus for a second sale, firms can respond to higher liability by changing the shape of pay, not only its level. The paper's Proposition 2 shows that, below a liability threshold, this response exactly offsets the liability: the bias of advice does not move at all.

Setting

Two firms $A$ and $B$ with common unit cost $c$ and common price $p$ sell only through one advisor. Two customers arrive one after the other. For each customer the advisor holds a posterior $q\in[0,1]$ that product $A$ suits; the posteriors are i.i.d. with a density $g$, continuous and positive on $[0,1]$, and c.d.f. $G(q)=\int_0^q g$. The distribution is symmetric, $G(q)=1-G(1-q)$, and has an increasing hazard rate $g(q)/[1-G(q)]$.

The advisor earns $w_h$ from a suitable sale and $w_l<w_h$ from an unsuitable one; the liability is $w=w_h-w_l>0$. Firm $n$ offers a commission $f_n$ and a bonus $b_n$: it pays $f_n$ for one sale and $2f_n+b_n$ for two. Limited liability makes payments non-negative, so a firm's strategy set is $X=\{(f,b): f\ge0,\ 2f+b\ge0\}$; a negative bonus is allowed.

The advisor recommends by cutoffs: after a first sale of $A$ she recommends $A$ to the second customer when $q_2\ge\bar q^A_2=\tfrac12-(f_A-f_B+b_A)/(2w)$, after a first sale of $B$ when $q_2\ge\bar q^B_2=\tfrac12-(f_A-f_B-b_B)/(2w)$, and to the first customer when $q_1\ge\bar q_1=\tfrac12-(f_A-f_B+Z^A-Z^B)/(2w)$, where $Z^A,Z^B$ are her expected continuation payoffs (all cutoffs clamped to $[0,1]$). With $\Pr(1)$ the probability of two different recommendations and $\Pr_n(2)$ the probability that $n$ is recommended twice, firm $n$'s expected sales and profit are

$$S_n=\Pr(1)+2\Pr_n(2),\qquad \pi_n=S_n(p-c-f_n)-\Pr_n(2)\,b_n .$$

A symmetric equilibrium compensation scheme is a scheme $(f,b)\in X$ such that both firms offering $(f,b)$ is a pure Nash equilibrium of the game in which each firm chooses a scheme in $X$ to maximize $\pi_n$.

Formalization targets

Goal: Proposition 2

Let $\bar q\in(0,1/2)$ solve $\bar q=\tfrac12-2G(\bar q)/g(\bar q)$ (15), and put

$$H(q)=\frac{G(q)}{g(q)}+\frac1{4g(1/2)[1-G(q)]^2+g(q)},\qquad w^*_f=\frac{p-c}{2H(\bar q)} .$$

For every $0<w<w^*_f$: every symmetric equilibrium scheme with $f>0$ and $0<b<w$ (advice to the second customer informative) is

$$f=p-c-2wH(\bar q),\qquad b=\frac{4G(\bar q)}{g(\bar q)}\,w ;$$

this scheme is an equilibrium whenever each firm's profit satisfies first-order sufficiency against it; both components are positive; the cutoffs there are $(\bar q_1,\bar q^A_2,\bar q^B_2)=(1/2,\bar q,1-\bar q)$, independent of $w$; and $f$ is strictly decreasing and $b$ strictly increasing in $w$.

Milestones

Lemma 1 (the cutoff rule is the advisor's optimal policy), Lemma 5 ($\bar q_1=\bar q^A_2+\int_{\bar q^A_2}^{\bar q^B_2}G$), Claim (32) (sales stay constant along $df=-\tfrac12db$), the derivative values (36)–(37), Lemma 2 (the bonus (14)), Lemma 3 (the cutoff equation (15) has one solution in $(0,1/2)$) and Lemma 4 (the commission (16)).

Significance

The result separates two policy instruments. Liability alone cannot reduce the bias of advice while firms pay both commissions and bonuses: firms raise the bonus, cut the commission, and the advisor's recommendations stay exactly as biased as before, while total expected compensation $f+b/2$ rises. Liability bites only above $w^*_f$, where commissions hit zero. This is the paper's case for regulating bonus payments directly rather than relying on liability.

The result is proved in the paper; nothing here is open. No part of it is formalized anywhere. The mission produces a machine-checked version of the model (advisor cutoffs with continuation payoffs, sales probabilities, the compensation game on the limited-liability strategy set) and of the equilibrium characterization. Moderation found that the paper's uniqueness claim needs the restriction $b<w$: for the uniform distribution, $p-c=1$ and $w=1/5$, the scheme $(f,b)=(3/5,3/5)$ is a symmetric equilibrium in which both firms lock in the second customer, so the statements carry $b<w$ as a declared correction.

Difficulty

The derivative computations (Claim (32), (36), (37)) are calculus at a point where all cutoffs are interior, after Lemma 5 rewrites $\bar q_1$ through an integration by parts that uses symmetry of $G$. Two steps go beyond them. First, uniqueness: the first-order conditions apply when $0<b<w$, the class the statements quantify over. When $b\ge w$ both second-customer cutoffs sit at a corner and each firm locks in the second customer; such symmetric equilibria do exist (the uniform example above), which is why the corrected statements exclude them. Second, existence: the paper assumes strict quasiconcavity of profits, which taken literally fails for every distribution, since profit is affine where one firm wins both sales. The formal statement therefore conditions existence on first-order sufficiency against the candidate scheme: every own scheme with interior cutoffs at which both own partial derivatives vanish is a best response. The restriction to interior cutoffs is needed, since where a firm never sells its profit is identically zero and every point is critical.

Formalization scope

A scheme is a pair $(f,b)\in\mathbb R^2$. The constant $w_l$ is dropped from all advisor payoffs, since it cancels from every comparison. Cutoffs are clamped to $[0,1]$ (footnote 19 for $\bar q^A_2$; the same convention for $\bar q^B_2$ and $\bar q_1$). The hazard rate is required to be weakly increasing on $[0,1)$, where it is defined. Prices are given (§4); the customer-side assumption (1) is not imposed, and the results hold for all real $p,c$.

The equilibrium is the Nash condition on the profits, built on the published two-player definition CompetingChains.Cournot.IsPureNash; the closed forms (14)–(16) are conclusions, never definitions. A definition of the equilibrium by its formulas, or of the cutoffs by $1/2\mp b/(2w)$, would make the goal arithmetic and is ruled out. The uniqueness clause ranges over all symmetric equilibria with $f>0$ and $0<b<w$ (a declared correction); first-order sufficiency is a hypothesis of the existence clause only.

Needed infrastructure: interval integrals with variable limits and the fundamental theorem of calculus, derivatives of clamped expressions at interior points, and the intermediate value theorem for (15). Proofs of the milestones and of first-order sufficiency for concrete distributions such as the uniform one are all welcome.

Selected references

• J. Honda, R. Inderst, M. Ottaviani, When Liability is Not Enough: Regulating Bonus Payments in Markets With Advice, SSRN working paper 4125013, May 2022. https://ssrn.com/abstract=4125013 — published in Management Science, 2023, https://doi.org/10.1287/mnsc.2023.4750
• R. Inderst, M. Ottaviani, Competition through Commissions and Kickbacks, American Economic Review 102(2), 780–809, 2012. https://doi.org/10.1257/aer.102.2.780
• R. Inderst, M. Ottaviani, Misselling through Agents, American Economic Review 99(3), 883–908, 2009. https://doi.org/10.1257/aer.99.3.883

Motivation

The supremum of a Lévy process over a finite horizon, and the time at which it is attained, enter the prices of lookback and barrier options, ruin probabilities in insurance, and the workload of queues and storage systems. Their law is explicit only in special cases, so in practice they are computed by Monte Carlo simulation. The classical method, the random walk approximation on a grid of mesh $T/n$, has a strong error that decays only polynomially in $n$ (Asmussen–Glynn–Pitman 1995; Dia–Lamberton 2011).

González Cázares, Mijatović and Uribe Bravo (arXiv:1810.11039v3) introduced the stick-breaking approximation (SBA). It rests on the description by Pitman and Uribe Bravo (2012) of the concave majorant of a Lévy process: the faces of the majorant, taken in size-biased order, have the law of a uniform stick-breaking of $[0,T]$ paired with the increments of an independent copy of the process. The approximation needs only $n+1$ samples of increments of $X$, and the paper shows that its error decays geometrically in $n$.

Setting

A Lévy process $X=(X_t)_{t\ge0}$ is a real process with $X_0=0$, independent and stationary increments and right-continuous paths with left limits. Its law is determined by its generating triplet $(\sigma^2,\nu,b)$: a Gaussian coefficient $\sigma\ge0$, a Lévy measure $\nu$ on $\mathbb R$ with $\nu(\{0\})=0$ and $\int\min\{1,x^2\}\nu(dx)<\infty$, and a drift $b$, through $\mathbb E[e^{iuX_t}]=e^{-t\Psi(u)}$ with the cutoff $\mathbb 1_{\{|x|<1\}}$. $X$ is compound Poisson with drift when $\sigma=0$ and $\nu(\mathbb R)<\infty$; the paper excludes this case, which is equivalent to $\mathbb P(X_t=x)=0$ for all $x$ and $t>0$ (Assumption 2).

Fix $T>0$. Write $\overline X_t=\sup_{s\le t}X_s$ for the running supremum and $\tau_t=\inf\{s\in[0,t]:\overline X_s=\overline X_t\}$ for the first time it is reached. The target is $\chi=(X_T,\overline X_T,\tau_T)$.

The stick-breaking process on $[0,T]$ is $L_0=T$, $\ell_n=V_nL_{n-1}$, $L_n=L_{n-1}-\ell_n$, with $(V_n)$ i.i.d. uniform on $(0,1)$. A stick-breaking coupling is a triple $(X,\ell,Y)$ in which $Y$ has the law of $X$, $Y$ is independent of $\ell$, and almost surely

$$\chi=\sum_{k=1}^\infty\Big(Y_{L_{k-1}}-Y_{L_k},\ (Y_{L_{k-1}}-Y_{L_k})^+,\ \ell_k\mathbb 1_{\{Y_{L_{k-1}}-Y_{L_k}>0\}}\Big).\tag{1.1}$$

The SBA $\chi_n$ (1.2) keeps the first $n$ summands and adds $(Y_{L_n},Y^+_{L_n},L_n\mathbb 1_{\{Y_{L_n}>0\}})$. Its errors are $\Delta_n$, $\delta_n$ (the partial-sum errors of the supremum and of its time, (1.3)) and $\Delta^{SB}_n=\Delta_n-Y^+_{L_n}$, $\delta^{SB}_n=\delta_n-L_n\mathbb 1_{\{Y_{L_n}>0\}}$.

The rate is built from four indices. The Blumenthal–Getoor index is $\beta=\inf\{p>0:I^p_0<\infty\}$ with $I^p_0=\int_{(-1,1)}|x|^p\nu(dx)$. With a free parameter $\delta$, the paper sets $\beta_+=\beta+\delta\mathbb 1_{\{I^\beta_0=\infty\}}$ (4.6). The index $\alpha$ (4.21) is $2$ if $\sigma\ne0$, $1$ if $\sigma=0$, the jumps have finite variation and the natural drift $b_0=b-\int_{(-1,1)}x\nu(dx)$ is nonzero, and $\beta$ otherwise. Then $\alpha_+=\alpha+(\beta_+-\beta)\mathbb 1_{\{\alpha=\beta\}}$ and

$$\eta_p=1+\mathbb 1_{\{p>\alpha\}}+\frac p{\alpha_+}\mathbb 1_{\{p\le\alpha\}}.\tag{4.22}$$

The large-jump moments are $I^p_+=\int_{[1,\infty)}x^p\nu(dx)$ and $I^p_-=\int_{(-\infty,-1]}|x|^p\nu(dx)$.

A correction. As printed, (4.6) gives $\beta_+=0$ for Brownian motion ($\beta=0$, $I^0_0<\infty$), and then the explicit constants of (4.12), (4.13) and (4.23) contain $p/0$. The mission sets $\beta_+=\beta+\delta$ also when $\beta=0$. The change affects no instance where the printed formulas are defined, and it never changes $\alpha_+$ or $\eta_p$. Every statement quantifies over every admissible $\delta$: $\delta\in(0,2-\beta)$, with $\beta+\delta<1$ when $\beta<1$, whenever $I^\beta_0=\infty$ or $\beta=0$. This is the stronger of the two readings of "pick $\delta$".

Formalization targets

Goal: Theorem 2 with (4.24)

For every stick-breaking coupling with $X$ not compound Poisson with drift and every $p\ge1$:

$$\max\big\{\mathbb E|\delta^{SB}_n|^p,\ \mathbb E\delta_n^p\big\}\le T^p(1+p)^{-n}\qquad(n\ge1),$$

$\eta_p\in[3/2,2]$, and

$$\mathbb E[\Delta_n^p]\le C_p(X)\,T^{\eta_p-1}\eta_p^{-n}\ \ (I^p_+<\infty),\qquad \mathbb E[(\Delta^{SB}_n)^p]\le C^*_p(X)\,T^{\eta_p-1}\eta_p^{-n}\ \ (\min\{I^p_+,I^p_-\}<\infty),$$

with $C_p(X)$, $C^*_p(X)$ explicit in $(\sigma^2,\nu,b)$ (4.23). The goal also contains the $\mathcal O(\eta_p^{-n})$ form for every admissible $\delta$. The explicit form carries the restriction $\alpha<p\Rightarrow\alpha_+<p$ on $\delta$, which the paper's proof imposes.

Milestones

In proof order: the equivalence of Assumption 2 with "not compound Poisson with drift"; existence of the coupling; (1.1) in law on any horizon; Theorem 1 (the error of the SBA given $L_n$ has the law of the supremum of $Y$ over $[0,L_n]$, with monotone a.s. bounds); $\mathbb E[L_n^p]=T^p(1+p)^{-n}$; Lemma 1 (bounds on $\nu$); Lemma 2 (explicit small-time moments $\mathbb E[\overline X_t^p]\le m^p_X(t)$); Corollary 3 ($\mathbb E[\overline X_t^p]\le C_p(X)t^{\eta_p-1}$); Lemma 3 (a bound $Ct^q$ gives $CT^q(1+q)^{-n}$).

Significance

The theorem is the reason the SBA is useful. Geometric decay means that $\mathcal O(\log(1/\epsilon))$ sticks suffice for accuracy $\epsilon$. In the paper this gives multilevel Monte Carlo and unbiased estimators of optimal complexity for Lipschitz and barrier-type functionals of $\chi$, and a central limit theorem for the Monte Carlo estimator. The rate $\eta_p\ge3/2$, for $p\ge1$, holds for every Lévy process that is not compound Poisson with drift, including infinite-variation and heavy-tailed ones.

The result is proved in the paper. It has no machine-checked proof, and to the platform's knowledge no Lean formalization of stick-breaking, concave majorants or small-time moment bounds for general Lévy processes exists. A full formalization would check the constants of (4.13) and (4.23), which no reader has machine-verified. It would also expose the boundary case $\beta=0$ that the printed (4.6) mishandles.

Difficulty

The analytic part, Lemmas 1–2 and Corollary 3, needs the Lévy–Itô decomposition at a truncation level $\kappa=(t/T)^{1/\beta_+}$ that depends on time. Each component is then bounded separately: Doob's inequality for the small-jump martingale, a Poisson-moment bound with Stirling numbers for the large jumps, and the reflection principle for the Brownian part. The constants must be tracked exactly.

The probabilistic part rests on two results that are not in Mathlib: the law of the faces of the concave majorant (Pitman–Uribe Bravo), and a transfer theorem that realises the coupling on an extension of the probability space. A natural first idea is to bound $\Delta_n$ by a random-walk discretisation error. This fails, because the SBA uses no grid. The decay comes from $L_n$ being a product of $n$ independent uniform factors, and that structure is visible only through Theorem 1.

Formalization scope

Time is $\mathbb R_{\ge0}$. Lévy processes are SingCtrlLevy.Barrier.IsLevyWith, a published definition whose paths are càdlàg and start at $0$ for every $\omega$. Its triplet uses the cutoff $\mathbb 1_{\{|x|<1\}}$. The coupling is a predicate IsSBCoupling listing the properties the proofs use: same triplet, i.i.d. uniform $V$, independence of $Y$ and $V$, and (1.1) almost surely. Its non-vacuity is a milestone. "Conditionally on $L_n$" is equality of joint laws with $L_n$. Expectations are lintegrals, and the Lévy-measure moments are extended reals. Every constant that uses toReal comes with a finiteness hypothesis, so an infinite moment is never silently read as $0$. Sticks are indexed from $0$, and $n\ge1$ as in the paper. The goal fixes no $\delta$ and contains no free rate or constant: $\eta_p$, $C_p(X)$ and $C^*_p(X)$ are the paper's formulas.

A complete development needs the Lévy–Itô decomposition, Doob's maximal inequality in continuous time, the reflection principle for Brownian motion, the concave majorant of a càdlàg path, and size-biased sampling. All of these are reusable well beyond this mission. Contributions to any of them, and proofs of the self-contained milestones (Lemma 1 and the moment identity for $L_n$), are welcome.

Selected references

• J. I. González Cázares, A. Mijatović, G. Uribe Bravo, Geometrically Convergent Simulation of the Extrema of Lévy Processes, arXiv:1810.11039v3, 2021. https://arxiv.org/abs/1810.11039v3
• J. Pitman, G. Uribe Bravo, The convex minorant of a Lévy process, Annals of Probability 40(4), 1636–1674, 2012. https://mathscinet.ams.org/mathscinet-getitem?mr=2978134
• K. Sato, Lévy Processes and Infinitely Divisible Distributions, Cambridge Studies in Advanced Mathematics 68, Cambridge University Press, revised ed., 2013. https://mathscinet.ams.org/mathscinet-getitem?mr=3185174
• O. Kallenberg, Foundations of Modern Probability, Springer, 2nd ed., 2002. https://mathscinet.ams.org/mathscinet-getitem?mr=1876169
• S. Asmussen, P. Glynn, J. Pitman, Discretization error in simulation of one-dimensional reflecting Brownian motion, Annals of Applied Probability 5(4), 875–896, 1995. https://mathscinet.ams.org/mathscinet-getitem?mr=1384357
• E. H. A. Dia, D. Lamberton, Connecting discrete and continuous lookback or hindsight options in exponential Lévy models, Advances in Applied Probability 43(4), 1136–1165, 2011. https://mathscinet.ams.org/mathscinet-getitem?mr=2867949

Motivation

Classical Feynman–Kac theorems connect a parabolic equation with fixed boundary data to the expectation of a functional of a diffusion stopped at the boundary. Several models in finance and physics do not fit this frame, because the terminal and boundary values depend on the solution in the interior. Dai, Kou and Yang (SSRN 3541591, later in Mathematics of Operations Research, doi:10.1287/moor.2020.1061) treat this class. Their motivating examples are the pricing of dual-purpose funds, whose value at a reset date feeds back into the contract, the regenerative processes of inventory control, and the entropy of a one-dimensional thermoelastic body, where Day (1982) derived a parabolic equation with nonlocal boundary conditions.

Nonlocal parabolic problems have an analytic literature: Friedman (1986) and Pao (1995, 1998) on nonlocal boundary conditions, Chabrowski (1984) on nonlocal initial conditions, Lieberman (1999) on time-periodic problems. The process side goes back to Grigorescu and Kang (2013), who study diffusions that jump from the boundary, with a nondegenerate transition probability that the clock process here does not have.

Setting

Let $\mathcal O\subset\mathbb R^d$, $d\ge1$, be a bounded smooth domain, $T>0$, $Q=[0,T)\times\mathcal O$, $\bar Q=[0,T]\times\bar{\mathcal O}$, and let the parabolic boundary be $\partial_pQ=(\{T\}\times\bar{\mathcal O})\cup([0,T)\times\partial\mathcal O)$. With continuous coefficients $b,\sigma$, Lipschitz and of linear growth, $a=\sigma\sigma^{\mathsf T}$ uniformly elliptic on $Q$, a rate $r>0$, and $f$ Hölder on $\bar Q$, set

$$\mathcal LW=\tfrac12\sum_{i,j}a_{ij}\,\partial_{x_ix_j}W+\sum_ib_i\,\partial_{x_i}W-rW.$$

For each $(t,x)\in\partial_pQ$ let $\nu_{t,x}$ be a positive Borel measure on $Q$ of mass $\bar\nu(t,x)\le1$ with $\nu_{t,x}((t,T)\times\mathcal O)=0$. The nonlocal problem is

$$-\partial_tW-\mathcal LW=f\ \text{ in }Q,\qquad W=h+\mathcal BW\ \text{ on }\partial_pQ,\qquad \mathcal BW(t,x)=\iint_QW(s,z)\,\nu_{t,x}(ds,dz).$$

The data $h$ and $\nu$ may be discontinuous on a small set $D\subset\partial_pQ$, which covers finitely many time slices of the lateral boundary and a null part of the terminal slice.

The underlying process is a clock $v$ and a diffusion $X$ in $Q$. On hitting $\partial_pQ$ at $\xi$, the pair jumps to a point of $Q$ with law $\tilde\nu_\xi=\nu_\xi/\bar\nu(\xi)$ and the mass $Y$ is multiplied by $\bar\nu(\xi)$. The clock can only jump backwards. $\theta_i$ is the $i$-th hitting time.

Formalization targets

Goal: Theorem 3.1

$$W(t,x)=E_t^x\Big[\int_t^\infty e^{-r(s-t)}Y_{s-}f(v_{s-},X_{s-})\,ds+\sum_{\theta_i\ge t}e^{-r(\theta_i-t)}Y_{\theta_i-}h(v_{\theta_i-},X_{\theta_i-})\Big]\quad\text{on }\bar Q,$$

for the unique bounded solution $W\in C^{1,2}(Q)\cap C(\bar Q\setminus D)$. The statement asserts existence, uniqueness and the representation at every point of $\bar Q$, boundary included.

Milestones

In proof order: the construction of the process (§2.2); non-explosion, Lemma 2.3; geometric decay, (A.2); the bound on the value functions, Proposition 2.4; the local Feynman–Kac theorem with discontinuous data, Proposition A.1; the identification of the iterates $W_{i+1}$, solving the problem with data $h+\mathcal BW_i$, with finite-horizon value functions, Lemma A.2; uniform convergence, Lemma A.3; the limit is a solution, Proposition A.4; and the finite-step representation of every bounded solution, (A.16).

Significance

The theorem gives existence and uniqueness for nonlocal parabolic problems with discontinuous dependence on the parameter, a setting more general than Chabrowski (1984), and it gives a representation of the solution by a cash-flow expectation. The paper uses it to obtain a pricing equation for dual-purpose funds, a regenerative interpretation of band controls, and a particle interpretation of thermoelastic entropy. The iteration behind the existence proof is also a numerical scheme.

The result is proved, in print, and not formalized anywhere to our knowledge. The platform's FeynmanKac series treats one-dimensional problems on the whole line with terminal data, given a solution. This mission adds statements on a bounded domain in general dimension, with discontinuous boundary data, and a process with random redistribution from the boundary.

Difficulty

A Dirichlet argument cannot start, because the boundary data depends on the solution and inherits its unknown regularity. A contraction argument is unavailable since $\bar\nu$ may equal $1$, so the operator $W\mapsto\mathcal BW$ has norm $1$. Discontinuous data rule out the classical Feynman–Kac theorem directly. Non-explosion cannot be read off from the process being strong Markov with a nondegenerate kernel, because the clock is degenerate: $\theta_i\to\infty$ needs an argument that rules out rapid alternation between terminal and lateral hits, through Assumption 2.2. Interior Schauder estimates, parabolic regularity up to the slice $t=0$, Itô's formula, and the strong Markov property of a process built on random intervals are each substantial in Lean.

Formalization scope

The domain is a set in EuclideanSpace ℝ (Fin d) with a global $C^\infty$ defining function. Functions take the pair $(t,x)$. Jump measures are FiniteMeasure on the subtype $Q$, so the weak topology is the one on $Q$ and mass cannot escape to $\partial Q$. $Q$ contains $t=0$, and the time derivative there is one-sided. The boundary equation holds on all of $\partial_pQ$, including $D$. The bound on $h$ is $|h|\le K_hT$, implied by the paper's $|h(s,x)|\le K_hs$. It is the form the proofs use.

The process is given through Realization: a filtered probability space under the usual assumptions, independent Brownian motions, stopping times, and cycles in $Q$ ending at a left limit in $\partial_pQ$. Non-explosion is not assumed. Stochastic integrals are the published EntropyMFG.Enhanced.HasItoIntegral.

The representation cannot hold trivially. The goal asserts that a realization exists at every point, that the time integral exists and the series converges, and that the payoff is integrable, so neither a vacuous quantifier nor a default integral value can satisfy it.

A full development needs a multidimensional Itô formula for these integrals, strong solutions of Lipschitz SDEs, the strong Markov property, parabolic Schauder estimates, and classical solvability of the Dirichlet problem. These are reusable far beyond this mission, and contributions to any of them are welcome. Proposition A.1 and the construction in §2.2 are natural separate entry points.

Selected references

• M. Dai, S. Kou, C. Yang, A Stochastic Representation for Nonlocal Parabolic PDEs with Applications, SSRN 3541591. https://ssrn.com/abstract=3541591
• M. Dai, S. Kou, C. Yang, same title, Mathematics of Operations Research. https://doi.org/10.1287/moor.2020.1061

The remaining entries are cited as in the paper's bibliography.

• J. Chabrowski, On nonlocal problems for parabolic equations, Nagoya Mathematical Journal 93, 109–131, 1984.
• J. Chabrowski, On the nonlocal problem with a functional for parabolic equation, Funkcialaj Ekvacioj 27(1), 101–123, 1984.
• W. A. Day, Extensions of a property of the heat equation to linear thermoelasticity and other theories, Quarterly of Applied Mathematics 40(3), 319–330, 1982.
• A. Friedman, Monotonic decay of solutions of parabolic equations with nonlocal boundary conditions, Quarterly of Applied Mathematics 44(3), 401–407, 1986.
• A. Friedman, Stochastic Differential Equations and Applications, Courier Corporation, 2012.
• A. Friedman, Partial Differential Equations of Parabolic Type, Courier Dover Publications, 2013.
• I. Grigorescu, M. Kang, Markov processes with redistribution, Markov Processes and Related Fields 19(3), 497–520, 2013.
• G. M. Lieberman, Time-periodic solutions of linear parabolic differential equations, Communications in Partial Differential Equations 24(3–4), 631–663, 1999.
• C. V. Pao, Reaction diffusion equations with nonlocal boundary and nonlocal initial conditions, Journal of Mathematical Analysis and Applications 195(3), 702–718, 1995.
• C. V. Pao, Asymptotic behavior of solutions of reaction-diffusion equations with nonlocal boundary conditions, Journal of Computational and Applied Mathematics 88(1), 225–238, 1998.

Why exact training can be computationally difficult

Training a classifier asks for parameters that fit observed examples. Even when the data can be classified perfectly, the task of finding suitable parameters can have substantial computational cost. The question here concerns exact training: deciding whether any parameter choice makes zero mistakes on the entire supplied data set. It concerns computation on given data, rather than the number of examples needed to predict unseen observations.

Blum and Rivest study a particularly small threshold network: two hidden nodes followed by one output node. The number of computational nodes stays fixed at three, while the number of input coordinates varies. Their headline theorem says that exact training of this architecture is NP-complete even when every input coordinate is Boolean (Blum and Rivest, 1992, §§1–3). The mission formalizes that theorem and its positive-quadrant prerequisite from the published paper.

The network and its training data

A linear threshold node takes real inputs $z_0,\ldots,z_{k-1}$, multiplies them by real weights $w_0,\ldots,w_{k-1}$, and compares their sum with a real threshold $t$. Its output is

$$H_{w,t}(z)= \begin{cases} +1,&\sum_{i=0}^{k-1}w_i z_i>t,\\ -1,&\sum_{i=0}^{k-1}w_i z_i\le t. \end{cases}$$

In particular, equality produces the negative output. The network has two such hidden nodes $h_0,h_1$, each receiving every coordinate of $x\in\{0,1\}^n$. Its output is

$$f_N(x)=H_{u,t_3}\bigl(h_0(x),h_1(x)\bigr).$$

The output node receives numerical values −1 and +1. All hidden weights, both hidden thresholds, both output weights and the output threshold can be chosen independently as arbitrary real numbers. There are no further nodes or connections. This is the topology in Figure 1 and the threshold convention of §2 (source, p. 119).

A training instance consists of a dimension $n$ and finitely many examples $(x,y)$, where $x\in\{0,1\}^n$ and $y\in\{-1,+1\}$. It is trainable when some network parameter choice satisfies $f_N(x)=y$ on every example. The question includes data that cannot be fitted. It imposes no distribution on the examples and no tolerance for misclassification.

Formalization targets

Let $L_{\mathrm{training}}$ be the language of explicitly encoded trainable instances. One language includes all input dimensions and all finite training sets. The goal is Theorem 1, printed p. 119:

$$\operatorname{NPComplete}(L_{\mathrm{training}}).$$

Here NP-completeness includes both a polynomially checkable finite certificate for every yes-instance and polynomial-time many-one reductions from every problem in NP. The existence of a certificate is part of the conclusion; real network parameters remain unrestricted in the definition of a yes-instance.

The single milestone is Theorem 2, printed p. 120. A positive quadrant is an intersection of two real threshold regions that contains all positive examples and none of the negative examples. Write $L_{\mathrm{quadrant},C}$ for its feasibility language restricted to at most $Cn$ example rows. The milestone is

$$\exists C\in\mathbb N,\qquad C>0\ \land\ \operatorname{NPComplete}(L_{\mathrm{quadrant},C}).$$

The constant is chosen once for the entire language. This expresses the unspecified $O(n)$ example bound in the problem definition of §3.1. Both targets retain the full NP-completeness conclusions of the paper (source, Theorems 1–2).

What the result establishes

The headline result locates a worst-case computational obstruction in an architecture with only three threshold nodes. Under $\mathrm P\ne\mathrm{NP}$, an algorithm cannot decide exact trainability on every such finite Boolean data set in polynomial time. The result does not say that every training instance is hard, nor does it assert an exponential lower bound. It separates a general guarantee on exact training from the performance a method might achieve on particular data (source, §§1 and 7).

The formal development supplies a concrete interface between real-valued network feasibility and finite-string computational complexity. The reusable threshold node, explicit network evaluation and input language make the numerical conventions visible. The present items are checked declarations of the paper's targets; their proofs remain to be supplied. Completing them requires establishing both the certificate and hardness components under the same definitions.

Why the formal proof requires care

Labels constrain only the final output. They do not specify the outputs of the hidden nodes. Consequently, choosing the hidden classifications is part of the training problem. In addition, the output node is itself trainable: a difficulty result for the fixed-AND auxiliary model does not by itself establish difficulty for the full model, whose feasible class is larger (source, §§3.1–3.3).

There is also a distinction between real parameters and finite witnesses. Merely existentially quantifying real weights does not give an NP verifier. The proof must connect feasibility to finite certificates and account for their bit lengths. Finally, the linear example bound in the quadrant problem has to hold with a constant independent of each instance. These obligations remain in the targets rather than becoming assumed hypotheses.

Formalization scope and conventions

Coordinates use Fin n; labels use Bool, with true denoting +1. A separate conversion interprets Boolean input coordinates as 0 or 1, so the two numerical roles cannot be confused. Training examples form finite lists. Listing each source pair once represents a finite training set; reordering or repeating an identical pair does not affect exact agreement. Conflicting labels on one input are infeasible. Empty data and zero-dimensional inputs are included.

The alphabet has five symbols. An instance starts with $n$ dimension ticks and a header terminator, followed by explicit rows. Each row contains $n$ coordinate bits, a label bit and a row terminator. For $m$ rows the length is $n+1+m(n+2)$, linear in the explicit dimension-and-row representation. Empty data have only their dimension header. A string outside the encoder's range is rejected. The quadrant budget counts listed rows; at dimension zero its budget permits only empty data.

The two quadrant cuts may be parallel, coincident or constant. Choosing their orientations and perturbing thresholds on a finite sample expresses the selected quadrant using strict positive regions; no margin or general-position assumption is imposed. The full training goal keeps all three nodes trainable and includes no weight bounds or assumed reduction.

The development imports the published CookPvsNP_defs model of Turing machines, polynomial time, finite witnesses and many-one reductions. Thresholds form their own definition module, and the paper-specific network builds on them. Contributions to finite-certificate theory and complexity reductions can use these interfaces. Independent Theorems 3–8 concern different networks or approximation questions and are outside this mission's dependency scope.

Selected references

• A. L. Blum and R. L. Rivest, Training a 3-Node Neural Network is NP-Complete, Neural Networks 5 (1992), 117–127. Published article. All numbering and pagination in this mission refer to this version.

Why robustness must be judged after optimization

Value-at-Risk (VaR) and Expected Shortfall are the two risk measures used in banking and insurance regulation. Their robustness has traditionally been studied as a property of the functional alone, applied to one fixed position. In that setting Cont, Deguest and Scandolo (2010) found VaR more robust than coherent risk measures, while later work such as Embrechts, Wang and Wang (2015) put that comparison into a different perspective.

A regulatory risk measure is not applied to a fixed position, however: positions are optimized against it. Embrechts, Schied and Wang therefore ask whether the optimized position keeps its value when the model it was optimized for is slightly wrong. Their main result, formalized here, is that for a broad class of budget-constrained problems VaR fails this test. The authors read this as an instance of Goodhart's law: when a measure becomes a target, it ceases to be a good measure.

Setting

Let $(\Omega,\mathcal F,\mathbb P)$ be a probability space, $n\ge1$, and let $X$ be an $n$-dimensional random vector with law $\mu_X$, called the best-of-knowledge model. Fix measurable functions $v:\mathbb R^n\to\mathbb R\cup\{-\infty\}$ and $w:\mathbb R^n\to\mathbb R$, a measurable price density $\gamma:\mathbb R^n\to(0,\infty)$, and $x_0\in\mathbb R$. The admissible set is

$$\mathcal G=\{g\text{ measurable}:v\le g\le w,\ \mathbb E[g(X)\gamma(X)]\ge x_0\}.$$

For an objective functional $\rho$, the functional optimization problem (8) is to minimize $\rho(g(X))$ over $g\in\mathcal G$. Write $\rho(X;\mathcal G)=\inf\{\rho(g(X)):g\in\mathcal G\}$ for its value, and $\mathcal G_X(\rho)=\{g\in\mathcal G:\rho(g(X))=\rho(X;\mathcal G)\}$ for its set of optimizers, which may be empty.

The objective is $\rho=\mathrm{VaR}_p$ for $p\in(0,1)$, where $\mathrm{VaR}_p(Y)=\inf\{x\in\mathbb R:\mathbb P(Y\le x)\ge p\}$.

Model uncertainty is a pseudo-metric space $(\mathcal Z,\pi)$ of $n$-random vectors containing $X$. Three kinds of metric occur: the $L^\infty$-metric $\pi^\infty_n(Y,Z)=\operatorname{ess\,sup}|Y-Z|$, the $L^q$-metric $\pi^q_n(Y,Z)=\|Y-Z\|_q$, and the pseudo-metric $\pi^W_n(Y,Z)$, the Prokhorov distance of the laws of $Y$ and $Z$.

Definition 1. $\rho$ is compatible with $(\mathcal G,\mathcal Z,\pi)$ if it maps $\{g(Z):Z\in\mathcal Z,g\in\mathcal G\}$ to $\mathbb R\cup\{+\infty\}$ and $\rho(g(Y))=\rho(g(Z))$ whenever $\pi(Y,Z)=0$.

Definition 2. A compatible $\rho$ is robust against optimization at $X$ for $(\mathcal G,\mathcal Z,\pi)$ if there is $g_X\in\mathcal G_X(\rho)$ such that $Y\mapsto\rho(g_X(Y))$ is $\pi$-continuous at $Y=X$.

Assumption G. $\mathbb E[\gamma(X)]<\infty$ and $\mathcal G\ne\emptyset$; $\mu_X$ has a positive density on its support, which is a convex subset of $\mathbb R^n$; and $(\mathcal Z,\pi)$ is $(L^0_n,\pi^W_n)$ or $(L^q_n,\pi^q_n)$ with $q\in[1,\infty]$.

Assumption V. $\operatorname{ess\,sup}(v)<\rho(X;\mathcal G)<\rho(w(X))$, and $\gamma$ is bounded from above.

Formalization targets

Goal: Theorem 1

For $p\in(0,1)$, under Assumptions G and V,

$$\rho=\mathrm{VaR}_p\text{ is not robust against optimization at }X\text{ for }(\mathcal G,\mathcal Z,\pi).$$

The statement fixes no constant. It covers every $n\ge1$, every $p$, every $q\in[1,\infty]$ and the weak pseudo-metric. The Lean statement also asserts that $\mathrm{VaR}_p$ is compatible, so that the failure is one of continuity.

Milestones

The steps of the proof in Appendix A.2, in order:

1. (A.1): every optimizer satisfies $\mathbb E_X[\gamma g_X]=x_0$.
2. (A.2): $\mathrm{VaR}_p(g_X(X))=\operatorname{ess\,sup}(g_X\,|\,A^c)$ for a $p$-tail event $A$ of $g_X$.
3. $g_X\mathbb 1_A=w\mathbb 1_A$.
4. If the quantile function of $g_X(X)$ is continuous at $p$, then $\mu_X(A'\setminus A)\in(0,1-p]$ for a $p$-tail event $A'$ of $w$.
5. The quantile function of $g_X(X)$ jumps at $p$.
6. A Borel set of mass $1-p$ can be given strictly more mass by a map of displacement at most $\varepsilon$.
7. Uniform $\varepsilon$-perturbations of $X$ are $\varepsilon$-close to $X$ in every metric of Assumption G.
8. $\mathrm{VaR}_p(g_X(Z))$ stays above the jump along such perturbations.

Significance

The theorem gives a negative answer for the risk measure most used in practice. Near the optimized position, an arbitrarily small misspecification changes the realized VaR by a fixed amount, even in the $L^\infty$-metric. Convex risk measures, by contrast, are shown to be robust in the same framework in later sections of the paper, so the result separates the two regulatory measures in a way that functional-level robustness does not.

The theorem is proved in the paper; to the knowledge of this mission it has no machine-checked proof. The mission adds a checked version with explicit conventions for the extended-value budget, for tail events and for the Prokhorov metric. Definition 2 and the admissible set are stated for general objective functionals, so the later results of the paper can be stated on the same definitions.

Difficulty

The obvious route is to exhibit the optimizer. In general there is no explicit form: $n$, $v$, $w$ and $\gamma$ are arbitrary, and an optimizer need not be unique or exist. The non-robustness must be derived from optimality alone, for every optimizer, from the bare first-order information in the budget constraint. The second obstacle is that a quantile discontinuity of $g_X(X)$ does not by itself give a discontinuity along perturbations of $X$: $g_X$ is an uncontrolled Borel function, and the perturbation has to exploit the geometry of $\mu_X$ for a Borel set with no regularity.

Formalization scope

The space $\mathbb R^n$ is EuclideanSpace ℝ (Fin n) with 0 < n. For $n=0$ the claim is false, so the hypothesis is essential. Functions $g$ are Borel, and the bounds $v\le g\le w$ are pointwise on all of $\mathbb R^n$. The budget $\mathbb E[g(X)\gamma(X)]$ is the extended-value expectation in EReal: $+\infty$ is feasible and an undefined difference is infeasible, which is the reading under which the printed proof goes through. Objectives and $\rho(X;\mathcal G)$ are EReal-valued. Distances are ℝ≥0∞-valued: levyProkhorovEDist of the laws, and eLpNorm, with $q=\infty$ included. The density clause is mutual absolute continuity of $\mu_X$ and Lebesgue measure on a convex set. The bound on $\gamma$ is $\mu_X$-a.e.

RobustAgainstOptimization does not bundle compatibility; otherwise "not robust" could hold because of incompatibility alone. The proof's normalization $\mathbb E[\gamma(X)]=1$ is not a hypothesis anywhere.

VaR and tail events are reused from the published definitions of ESAxioms.Characterization. A complete development needs quantile calculus for VaR on measurable random variables, the existence of tail events for measures with a density (the general statement, ESAxioms.Characterization.lemma_A3, is open on the platform and is not posed again here), and the bound of the Prokhorov distance by a uniform distance. Those parts are reusable beyond this mission, and contributions to them are welcome, as are direct proofs of any milestone.

Selected references

• P. Embrechts, A. Schied, R. Wang, Robustness in the Optimization of Risk Measures, arXiv:1809.09268v3, 2021. https://arxiv.org/abs/1809.09268
• R. Cont, R. Deguest, G. Scandolo, Robustness and sensitivity analysis of risk measurement procedures, Quantitative Finance 10(6), 593–606, 2010. https://doi.org/10.1080/14697681003685597
• P. Embrechts, B. Wang, R. Wang, Aggregation-robustness and model uncertainty of regulatory risk measures, Finance and Stochastics 19(4), 763–790, 2015. https://doi.org/10.1007/s00780-015-0273-z
• R. Wang, R. Zitikis, An axiomatic foundation for the Expected Shortfall, Management Science, 2021. https://doi.org/10.1287/mnsc.2020.3617