All missions

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

Motivation

A controller steers a diffusion and a stopper decides when the game ends. Such zero-sum games model, for example, a central bank that controls an exchange rate until a possible political veto, and the control of inflation (Hernandez-Hernandez, Simon, Zervos 2015, as cited in Bovo, De Angelis, Issoglio, p.3). When the controller may act singularly, in lumps and at any rate, the state jumps, and the natural equation is a variational inequality with two hard constraints at once: an obstacle and a bound on the gradient.

Timeline.

• Maitra and Sudderth (1996) introduced the gambler and the stopper in discrete time, with bounded payoffs.
• Karatzas and Sudderth (2001) treated one-dimensional diffusions with controlled coefficients.
• Karatzas and Zamfirescu (2008), Choukroun, Cosso and Pham (2015) and others treated classical controls, by martingale, viscosity and BSDE methods.
• Hernandez-Hernandez, Simon and Zervos (2015) treated a singular controller against a stopper in one dimension, by ordinary differential equations and a guess of the strategies.
• Bovo, De Angelis and Issoglio (arXiv:2203.06247v3, Mathematics of Operations Research, 2025) treated the multi-dimensional problem on an unbounded domain.

Setting

Fix $T>0$, $r\ge0$, $d\le d'$ and a stochastic basis with a $d'$-dimensional Brownian motion $W$. The state is

$$X_s=x+\int_0^s b(X_u)\,du+\int_0^s\sigma(X_u)\,dW_u+\int_{[0,s]}n_u\,d\nu_u,\qquad 0\le s\le T-t.$$

The control is a pair $(n,\nu)\in\mathcal A_t$: $n$ is a progressive unit vector, $\nu$ is adapted, non-decreasing and right-continuous with $\nu_{0-}=0$ and $\mathsf E[\nu_{T-t}^2]<\infty$. The stopper picks a stopping time $\tau\in\mathcal T_t$, $\tau\le T-t$. At $\tau$ the controller pays

$$J_{t,x}(n,\nu,\tau)=\mathsf E_x\Big[e^{-r\tau}g(t+\tau,X_\tau)+\int_0^\tau e^{-rs}h(t+s,X_s)\,ds+\int_{[0,\tau]}e^{-rs}f(t+s,X_s)\circ d\nu_s\Big].$$

The last integral charges a jump of $\nu$ by integrating $f$ along the segment the state travels. With $\mathcal L=\frac12\mathrm{tr}(\sigma\sigma^\top D^2)+\langle b,\nabla\rangle$, Problem A asks for $u\in W^{1,2,p}_{\ell oc}$, $p>d+2$, of quadratic growth with

$$u\ge g,\quad |\nabla u|_d\le f,\quad u(T,\cdot)=g(T,\cdot),$$

$\partial_tu+\mathcal Lu-ru=-h$ where both constraints are slack, $\ge-h$ a.e. where $u>g$, and $\le-h$ a.e. where $|\nabla u|_d<f$. The notation follows the Lean development: Data, Basis, payoff, lowerValue, upperValue, tauStar, IsProblemASolution.

Formalization targets

Goal: Theorem 3.3

$$\sup_{\tau}\inf_{(n,\nu)}J_{t,x}=\inf_{(n,\nu)}\sup_{\tau}J_{t,x}=:v(t,x)<\infty,$$

$v$ solves Problem A and dominates every solution, for every $p>d+2$, and for each control, with $\tau_*=\inf\{s\ge0\mid v(t+s,X_s)=g(t+s,X_s)\}\wedge(T-t)$,

$$v(t,x)=\inf_{(n,\nu)\in\mathcal A_t}J_{t,x}(n,\nu,\tau_*(n,\nu)).$$

Milestones

In proof order: well-posedness of the controlled equation; the penalised PDE on balls, Problem B (Propositions 4.1, 4.9, Lemma 4.5, Theorem 4.11); estimates independent of the ball (Propositions 5.1, 5.2); the penalised PDE on the whole space, Problem C (Theorem 5.3, Propositions 5.4, 5.5); estimates independent of the penalisation (Lemmas 5.6–5.8, Theorem 5.9); and existence for Problem A (Theorem 6.1).

Significance

The result. The theorem gives existence of a value without boundedness of the coefficients or payoffs and without uniform ellipticity, and it identifies the value with a solution of a variational inequality in a Sobolev class. The stopping rule is a best response against every control, and it is in feedback form. It reduces the game to a singular control problem with absorption on the contact set $\{v=g\}$, which is the route to the controller's optimal strategy. Uniqueness for Problem A and existence of an optimal control are open (Remark 3.5).

The formalization. The result is proved on paper. No machine-checked proof of it is known to the mission. The mission adds a singularly controlled multi-dimensional SDE with jumps at time zero, a controller-stopper game, and the parabolic Hölder and Sobolev classes $C^{j,k,\alpha}$, $C^{j,k,\alpha}_{\ell oc}$, $C^{j,k,\alpha}_{Loc}$, $W^{1,2,p}_{\ell oc}$.

Difficulty

The obvious argument is a verification theorem: apply Itô's formula to a solution of Problem A along the controlled state. It fails, because the maximal solution is only $W^{1,2,p}_{\ell oc}$ and its second derivatives are not defined along jump paths. The two constraints interact: a bound on $\nabla u$ must hold together with the obstacle, under the min-max structure of the problem, on an unbounded domain, and without bounded coefficients or uniform ellipticity. Swapping 'min' and 'max' in the variational inequality is itself equivalent in spirit to the equality of the upper and lower value. The analytic estimates known for gradient constraints alone do not supply the bounds that are needed.

Formalization scope

Payoffs and values lie in $[0,\infty]$: $f$ has polynomial growth and $\nu$ only a second moment, so $J$ can be $+\infty$, and the goal asserts that the value is finite. The value function is the toReal of the lower value. The infimum runs over triples $(n,\nu,X)$; the first milestone shows that every pair has exactly one state. The path of $\nu$ is extended by $0$ to negative times and $X$ by $x$, so a jump at time zero is covered. Derivatives are named witnesses, not fderiv. Bounded sets are replaced by the cylinders $[0,T]\times\bar B_R$. The statement quantifies over every basis and all data satisfying Assumptions 3.1 and 3.2. Functions are compared only on $[0,T]\times\mathbb R^d$.

A real-valued expectation would return $0$ at a non-integrable payoff and would trivialize the game; the statement rules this out by the lintegral payoff. Problem A carries the terminal condition and the growth bound, without which "maximal" would change meaning.

A complete development needs parabolic Schauder and $L^p$ theory, the Sobolev embedding, a Dynkin formula for $W^{1,2,p}$ functions, strong solutions with Hölder drift, Schaefer's fixed point theorem, and Itô's formula for càdlàg semimartingales. These are reusable beyond this mission, and contributions to any of them are welcome.

Selected references

• A. Bovo, T. De Angelis, E. Issoglio, Variational Inequalities on Unbounded Domains for Zero-Sum Singular Controller vs. Stopper Games, arXiv:2203.06247v3, 2023; Mathematics of Operations Research, 2025. https://arxiv.org/abs/2203.06247
• D. Hernandez-Hernandez, R.S. Simon, M. Zervos, A zero-sum game between a singular stochastic controller and a discretionary stopper, Ann. Appl. Probab. 25(1), 46–80, 2015.
• I. Karatzas, W.D. Sudderth, The controller-and-stopper game for a linear diffusion, Ann. Probab. 29(3), 1111–1127, 2001.
• I. Karatzas, I.-M. Zamfirescu, Martingale approach to stochastic differential games of control and stopping, Ann. Probab. 36(4), 1495–1527, 2008.
• A.P. Maitra, W.D. Sudderth, The gambler and the stopper, Lecture Notes-Monograph Series 30, 191–208, 1996.
• L.C. Evans, A second order elliptic equation with gradient constraint, Comm. Partial Differential Equations 4(5), 555–572, 1979.

Why compatibility affects delays

A service system can have enough capacity in total and still make one group of customers wait much longer than another. The distinction arises when servers can handle different customer classes. A flexible server may help several queues, while another server has only one eligible class. Which connections are present affects both how work is shared and how congestion is distributed. Afèche, Caldentey and Gupta study this design question for a bipartite matching queue. This mission concerns their exact heavy-traffic formula for class waiting times, rather than the paper's separate reward optimization and mixed-integer formulations. Source paper, §§2–4.

The regime keeps the individual servers, their rates, and their compatibility connections fixed. Only arrival rates increase toward the system's total capacity. Thus the question concerns congestion in one fixed system approaching saturation, not a limit in which more servers are added.

The queue and its component graph

There are $n>0$ customer classes and $m>0$ individual servers. A binary matrix $M$ records which server can serve which class. Class $i$ has an independent Poisson arrival stream of rate $\rho\widetilde\lambda_i$. Server $j$ has exponential service times with rate $\mu_j$, independent of customer class. All nominal arrival and service rates are strictly positive real numbers, and

$$\sum_i\widetilde\lambda_i=\sum_j\mu_j.$$

The load parameter satisfies $0<\rho<1$. Customers neither abandon nor encounter a finite waiting-room limit. Under first come first served, assign longest idle server, a completing server takes the oldest waiting customer it can serve. An arriving customer takes the compatible server that has been idle longest, if one exists; otherwise the customer waits. A matching is heavy-traffic admissible when this operational queue admits a stationary law at every load sufficiently close to one from below. These are the model and admissibility conventions of §2.

The residual graph is determined by a separate transportation problem at nominal load. A residual edge is an original compatible edge that carries positive flow in at least one feasible flow satisfying all nominal demands and filling all server capacities. Taking the union of these possible positive supports is essential: selecting one optimizer could incorrectly discard a connection. The connected components of this undirected bipartite graph are the complete-resource-pooling components, denoted $(\mathcal C_k,\mathcal S_k)$ for $1\le k\le K$. A component need not be a complete bipartite graph.

An original edge absent from the residual graph creates a directed arc from its customer component to its server component. The source establishes that this component graph is acyclic. A topological order lists every component once, putting the destination of each arc before its origin. This reverses the usual convention deliberately. Write $\mathcal T(M)$ for the collection of all such orders. Definitions 3–6.

Formalization targets

Let $W_i(\rho)$ be the actual stationary mean time until a class-$i$ arrival starts service. For an order $\sigma$, define

$$c_{\sigma,r}=\sum_{\ell=1}^r\mu_{\mathcal S_{\sigma(\ell)}},\qquad Q_\sigma=\prod_{r=1}^K c_{\sigma,r}^{-1},\qquad w_{\sigma,k}=\sum_{r=\sigma^{-1}(k)}^K c_{\sigma,r}^{-1}.$$

The goal is the full Theorem 1, p. 20: all class limits exist, and for every $i\in\mathcal C_k$,

$$\lim_{\rho\uparrow1}(1-\rho)W_i(\rho) =\sum_{\sigma\in\mathcal T(M)} \frac{Q_\sigma}{\sum_{\tau\in\mathcal T(M)}Q_\tau}\,w_{\sigma,k}.$$

Consequently, any two classes in the same component have the same finite scaled-mean limit. This does not assert equality of their means at a fixed load below one.

The nine supporting targets preserve Lemmas 1–6 and 8, Proposition 2, and the stationary product form in §4, equation (7). They cover attained max-flow saturation, acyclicity, all four printed component properties, the finite-load operational stationary law, both directions of the critical-prefix characterization, vanishing aggregate-state probabilities, the common internal-normalization limit, the exact normalized order masses, and the exact finite-load waiting-time identity. Lemma 8 precedes Lemma 5 in dependency order. Equation (7) retains the paper's attribution to Adan and Weiss (2014), Theorem 2.1.

What the result supplies

The formula assigns a limiting delay to each component using its total service capacity and position across the component graph's orders. It therefore connects a stochastic performance measure to a finite graph derived from feasible flows. Compatibility between different residual components matters even when its limiting flow is zero. The result also distinguishes equality within a component from differences between components. These are features of the source's waiting-time analysis, not assumptions of the formal model.

The Lean contribution is a precise statement of that connection with a concrete queue underneath it. The theorem declarations are open statements ending in sorry, not completed proofs. The definition layer supplies reusable event-clock and transportation objects, an operational FCFS-ALIS specialization, residual connectivity, observation events, and extended waiting means.

The main difficulty

Treating all capacity as one common server pool loses the compatibility restrictions. Treating distinct residual components as independent loses the effect of original connections between them. Neither simplification gives the full class-delay vector. The stationary state also remembers customer arrival order and idle-server order, so a vector of queue lengths alone does not determine the relevant transition rule. The source's product form and asymptotic formulas must concern this operational queue, rather than a probability distribution introduced solely to reproduce the desired answer.

Formalization scope

Lean uses zero-based finite indices for the classes and servers, while queue lengths remain unrestricted natural numbers. General Poisson event chains are defined separately from the queue. The queue is constructed through arrival and potential completion events; an idle server's completion event leaves the state unchanged. This constant-rate construction retains the independent exponential service mechanism. Initial idle ties have a specified ordering, and simultaneous subsequent events have probability zero.

Stationarity uses a published countable-state invariant probability-vector definition, supported on states reachable from empty queues. A tagged arrival is inserted into equilibrium and followed until service starts. Its expected wait is a nonnegative hitting-time tail sum in $[0,\infty]$; finiteness is a conclusion before conversion to a real value. Neither the product form nor the waiting-time formula defines this mean. Compressed observations include zero busy servers and omit in-service customers from waiting counts. All limits run through real loads in $(0,1)$ toward one.

The printed empty-subset clause of Lemma 3(ii) is retained even though it asserts $0>0$ in a one-server example. A separate source finding records that counterexample. Another finding records the omitted all-idle mass in the finite-load normalization step of Lemma 5's proof; its limiting statement remains unchanged. These findings do not replace the source targets. Contributions may supply proofs, disproof of the printed false milestone, or auxiliary results establishing a valid proof route to the unchanged main theorem.

Selected references

• Philipp Afèche, René Caldentey and Varun Gupta, On the Optimal Design of a Bipartite Matching Queueing System, Operations Research, catalog year 2021. DOI. Citations here use the acquired 59-page artifact dated November 3, 2019, with SSRN 3345302 footers. Printed and PDF page numbers coincide. The metadata citation basis remains published; journal pagination and numbering from other versions are not substituted.

Motivation

Periodic-review inventory control with a fixed ordering cost is a basic model of operations management: every order costs $K>0$ regardless of its size, so a firm orders in batches and the optimal policy is an $(s,S)$ policy rather than a base-stock level (Scarf 1960; Zheng 1991). In practice the demand distribution is unknown and, when unmet demand is lost, only sales are observed (censored demand). Earlier learning algorithms for censored inventory systems (Huh and Rusmevichientong 2009; Huh, Levi, Rusmevichientong and Orlin 2011) rely on the convexity of the base-stock cost, which fixed costs destroy.

Yuan, Luo and Shi (2021) give the first learning algorithm for this setting with a regret guarantee. The algorithm combines first-order steps (stochastic gradient descent on the order-up-to level) with zeroth-order, bandit-like elimination over a grid of reorder gaps, and it shares censored sales across all candidate policies by simulation.

Setting

A firm reviews inventory in periods $t=1,2,\dots$. In period $t$ it sees the beginning inventory $x_t\ge0$, orders up to $y_t\in[x_t,\beta]$, where $\beta\ge0$ is the warehouse capacity, faces demand $d_t$, sells $\min(d_t,y_t)$ and carries $x_{t+1}=(y_t-d_t)^+$. Costs are a fixed cost $K>0$ per positive order, a unit cost $c\ge0$, a unit holding cost $h>0$ and a lost-sales penalty $p>c$. The pseudo cost of a period is

$$\tilde C_t=K\mathbf 1(y_t>x_t)+c(y_t-x_t)+h(y_t-d_t)^+-p\min(y_t,d_t),$$

the period cost minus $p\,d_t$, a term no policy affects. Assumption 1: the demands $D_t$ are i.i.d., nonnegative, with a density bounded by $\rho>0$. No moment of $D$ is assumed.

A $(\delta,S)$ policy orders up to $S$ whenever $x_t\le S-\delta$; the gap $\delta=S-s$ replaces the usual $s$. One cycle started at $S$ lasts $L(\delta)=\min\{k\ge1:D_1+\dots+D_k\ge\delta\}$ periods and has pseudo cost $G(\delta,S)$ (newsvendor pseudo costs plus the reorder at its end). The objective is the long-run average pseudo cost $V(\delta,S)=\mathbb E[G(\delta,S)]/\mathbb E[L(\delta)]$, with $V^*(\delta)=\min_{S\in[\delta,\beta]}V(\delta,S)$ and $V^*=\min_{0\le\delta\le S\le\beta}V(\delta,S)$.

The $(\delta,S)$ learning algorithm fixes a grid $\delta_j=j\beta/J$, targets $S^n_j$ and an active set $\mathcal A^n\subseteq\{1,\dots,J\}$. In epoch $n$ it runs the active policy with the largest target, $j^n=\arg\max_{j\in\mathcal A^n}S^n_j$, at level $S^n=\max(x^n,S^n_{j^n})$ until the epoch's sales exceed $\bar\delta^n=\max_{j\in\mathcal A^n}\delta_j$, completes the current cycle, simulates one cycle of every active policy from those sales, updates each target by a projected stochastic-gradient step $S^{n+1}_j=\mathrm{Proj}_{[\delta_j,\beta]}(S^n_j-\eta^n\tilde\nabla^n_j)$, and removes the gaps whose empirical average pseudo cost $\hat V^n_j=\hat G^n_j/\hat L^n_j$ exceeds the best by more than $\Delta^n$. The regret over $N$ epochs is

$$R_N=\mathbb E\Bigl[\sum_{t=1}^{T_N}\tilde C_t\Bigr]-V^*\,\mathbb E[T_N],$$

with $T_N$ the last period of epoch $N$.

Formalization targets

Goal: Theorem 3

With $J=\lfloor\sqrt N\rfloor$, $\eta^n=\beta/(\xi\sqrt n)$ and $\Delta^n=2\theta\log(8N^2)/\sqrt n$, where $\xi,\theta$ are the explicit constants (18)–(19),

$$\exists C\ \ \forall N\ge2\ \ \forall S^1:\qquad R_N\le C\log N\sqrt N .$$

The constant depends on the instance, not on $N$ or on the initial targets.

Milestones

The structural facts: $|\tilde C_t|\le\gamma$ (Lemma 1); $\mathbb E[L(\delta)]$ is $6\rho$-Lipschitz (Lemma 2) and $\mathbb E[L(\beta)]\le1+6\rho\beta$ (Corollary 1); $V(\delta,\cdot)$ is convex and uniformly Lipschitz, $\tilde\nabla$ is an unbiased gradient of $\mathbb E[G]$, and $V^*(\cdot)$ is Lipschitz (Theorem 2). The reduction (23), $R_N\le2(1+6\rho\beta)\mathbb E[\sum_n(V(\delta^n,S^n)-V^*)]+c\beta+K$. The four losses of the decomposition (25): discretization (Proposition 1), pruning (Proposition 2, $O(\log N\sqrt N)$), inventory carry-over (Proposition 3) and SGD (Proposition 4), the last three $O(\sqrt N)$. The tools: an exponential tail gives sub-exponential parameters (Lemma 6), the cycle quantities are sub-exponential (Lemma 3, corrected), a high-probability bound for sub-exponential projected SGD (Theorem 5, corrected), the estimation bound $|\hat V^n_j-V^*_j|\le\theta\log(8/\kappa)/\sqrt n$ (Lemma 4, corrected), and a capped-queue bound (Lemma 5).

Significance

Theorem 3 gives an $O(\log T\sqrt T)$ regret, since $N\le T_N$. The repeated newsvendor problem already has an $\Omega(\sqrt T)$ lower bound (Zhang, Chao and Shi 2020, as cited on p.17 of the source), so the rate is optimal up to the logarithm. It is the first nonparametric learning guarantee for inventory systems with fixed costs, and Theorem 5 is a high-probability bound for SGD with sub-exponential gradients that the paper offers as of independent interest.

No part of the paper has a machine-checked proof. A formalization would also settle the statement layer, which the paper leaves informal in several places. Lemma 3 is false as printed: it needs $h\le p$, $p<\gamma$ and $\gamma\ge1$, which its proof uses, and the mission states it with them. Theorem 5 is false as printed in two ways: its hypotheses must cover the last iterate $i=n$, and its term $2b\log(1/\delta)/n$ fails for large $\beta$, because the proof treats the pairing with $z_i-z^*$ as $(\beta\nu,b)$- rather than $(\beta\nu,\beta b)$-sub-exponential; the mission states it with $2\max(1,\beta)b$. Its proof also bounds $\sum_i\eta_i\|\tilde\nabla_i\|^2$ almost surely from a second-moment bound, a gap with no known counterexample. Lemma 4 is false as printed for small $\beta$, where the fixed step sizes keep the iterates jumping between the endpoints; it is stated with Lemma 3's hypotheses. The goal itself is stated as printed, for every instance satisfying Assumption 1. Because the paper's route goes through Lemmas 3 and 4, it covers only $h\le p<\gamma$, $\gamma\ge1$, so the remaining instances need another argument, which can use the factor $\log N$ in $\Delta^n$.

Difficulty

The obvious argument treats each epoch as a fresh renewal cycle of a fixed policy and runs SGD and elimination on i.i.d. samples. That fails in three places. First, the implemented policy changes from epoch to epoch and depends on the past through the carried-over inventory, so the epoch costs are neither i.i.d. nor exactly renewal; the reduction (23) has to use the structure of complete cycles and bounded epoch lengths. Second, the simulated cycles are built from censored sales of a different policy, and their validity rests on the leader having the largest target and the epoch's sales exceeding every active gap. Third, the analytic inputs are not routine: the Lipschitz bound for the renewal function of a walk with a bounded density (Lemma 2) is a new argument, and the concentration steps need explicit sub-exponential constants for unbounded cycle quantities.

Formalization scope

Everything is pathwise on the demand path $t\mapsto D_t(\omega)$, with 0-based periods. The parameters are bundled with their ranges in Params. Assumption 1 is IsDemandProcess: measurability, iIndepFun, IdentDistrib, and the law of $D_0$ bounded by $\rho\cdot$Lebesgue on $[0,\infty)$. Hitting times and epoch ends are infima on $\mathbb N$, which are junk only on a null set. $V$ is a ratio of Bochner integrals, and $V^*(\delta)$, $V^*$ are infima over the feasible sets, which are nonempty and bounded since $|V|\le\gamma$. The algorithm algState is the paper's Algorithm 1 literally: the first period of an epoch orders up to $S^n$, the while-loop runs on sales, the current cycle is completed, the simulation uses sales, and ties in the argmax go to the smallest index. Sub-exponentiality is the published HighDimStat.TailBounds.IsSubExponential.

The goal is not trivialized by junk integrals: it concludes that the total pseudo cost and $T_N$ are integrable. The constant $C$ precedes $N$ and the initialization, the parameters are the paper's explicit formulas, and no hypothesis beyond Assumption 1 and the cost ranges is added.

A complete development needs renewal theory for walks with bounded densities, differentiation under the integral for piecewise-linear cycle costs, Azuma–Bernstein inequalities for sub-exponential martingale differences, and the analysis of the algorithm's epochs. Lemmas 2, 5, 6 and Theorem 5 are reusable beyond this mission. Contributions to any milestone, or a proof of the goal for instances outside $h\le p<\gamma$, $\gamma\ge1$, are welcome.

Selected references

• H. Yuan, Q. Luo, C. Shi, Marrying Stochastic Gradient Descent with Bandits: Learning Algorithms for Inventory Systems with Fixed Costs, Management Science, 2021. https://doi.org/10.1287/mnsc.2020.3799 (accepted manuscript: https://ssrn.com/abstract=3329611)
• Y.-S. Zheng, A simple proof for optimality of (s, S) policies in infinite-horizon inventory systems, Journal of Applied Probability 28(4):802–810, 1991.
• H. Scarf, The optimality of (S, s) policies in the dynamic inventory problem, Mathematical Methods in the Social Sciences, Stanford University Press, 1960.
• W. T. Huh, P. Rusmevichientong, A nonparametric asymptotic analysis of inventory planning with censored demand, Mathematics of Operations Research 34(1):103–123, 2009.
• W. T. Huh, R. Levi, P. Rusmevichientong, J. B. Orlin, Adaptive data-driven inventory control with censored demand based on Kaplan-Meier estimator, Operations Research 59(4):929–941, 2011.
• H. Zhang, X. Chao, C. Shi, Closing the gap: A learning algorithm for lost-sales inventory systems with lead times, Management Science, 2020.
• M. J. Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint, Cambridge University Press, 2019.

Bibliographic data of the cited works are taken from the source's reference list (pp.45–47).

Motivation

Fund managers, traders and employees with performance pay are judged period by period: a bonus, a fee or a loss of reputation follows each quarterly or annual review, not the value of the portfolio at some distant terminal date. Behavioral finance adds that such outcomes are felt as gains and losses relative to a reference point, with loss aversion and risk seeking over losses (Tversky and Kahneman, 1992). Tse and Zheng (SSRN 3971852, version of June 20, 2023; published in Operations Research, doi:10.1287/opre.2021.0780) solve the resulting continuous-time portfolio problem in closed form over an infinite horizon. Finite-horizon non-concave utility maximization is classical (Berkelaar, Kouwenberg and Post, 2004; Reichlin, 2013; Bichuch and Sturm, 2014); with infinitely many evaluation dates and a path-dependent reward, neither the HJB approach nor plain martingale duality applies directly, and this paper combines the two.

Setting

A Brownian motion $B$ lives on $(\Omega,\mathcal F,P)$ with its augmented natural filtration $(\mathcal F_t)_{t\ge0}$. The market has a stock $S_t=S_0\exp((\mu-\sigma^2/2)t+\sigma B_t)$, $\sigma>0$, and a bond $D_t=e^{rt}$. With the Sharpe ratio $\theta=(\mu-r)/\sigma\neq0$, the pricing kernel is $Z_t=\exp(-\theta B_t-(r+\theta^2/2)t)$.

An admissible portfolio $X\in\mathcal A_0(x)$, $x>0$, is the value $X_t=\varphi^{(S)}_tS_t+\varphi^{(D)}_tD_t$ of predictable holdings with

$$X_t=x+\int_0^t\varphi^{(S)}_u\,dS_u+\int_0^t\varphi^{(D)}_u\,dD_u\ \ge0\qquad\text{for all }t\ge0 .$$

The portfolio is evaluated at $T_i=i\tau$, $\tau>0$. The performance of period $i$ is $X_{T_i}-\gamma X_{T_{i-1}}$, with target $\gamma\ge0$, and is valued by the S-shaped utility

$$U(x)=x^\alpha\ (x\ge0),\qquad U(x)=-k|x|^\alpha\ (x<0),\qquad \alpha\in(0,1),\ k\ge0 .$$

The agent solves

$$V(x)=\sup_{X\in\mathcal A_0(x)}E\Big[\sum_{i=1}^\infty e^{-\beta T_i}U(X_{T_i}-\gamma X_{T_{i-1}})\Big]\qquad(4)$$

with $\beta>0$ and the standing Assumption 1: $\beta>h:=r\alpha+\alpha\theta^2/(2(1-\alpha))$.

For $a\in\mathbb R$ let $G_a(y)=U(y-\gamma)+ay^\alpha$, $y\ge0$, and define the one-period auxiliary problem

$$F(a)=\sup\{E[G_a(Y)]:\ Y\ge0\ \mathcal F_\tau\text{-measurable},\ E[Z_\tau Y]\le1\},\qquad \Phi(a)=e^{-\beta\tau}F(a).$$

$\bar G_a$ is the smallest concave majorant of $G_a$ on $[0,\infty)$, and $y^*_a(q)$ is a maximizer of $y\mapsto\bar G_a(y)-qy$ over $y\ge0$, $q>0$. Put $\kappa=(k^{1/(1-\alpha)}+1)^{1-\alpha}$.

Formalization targets

Goal: Theorem 1 (pp.13–14)

$\Phi$ has a unique fixed point $A^*$, and $V(x)=A^*x^\alpha$ for every $x>0$. For every maximizer selection $y^*_{A^*}$ there is $\lambda^*>0$ (in Cases 1, 2a, 2b the unique root of $E[Z_\tau y^*_{A^*}(\lambda Z_\tau)]=1$) and an optimal $X^*\in\mathcal A_0(x)$ with

$$X^*_{T_0}=x,\qquad X^*_{T_i}=X^*_{T_{i-1}}\,y^*_{A^*}\big(\lambda^*Z_{T_i}/Z_{T_{i-1}}\big),\quad i\ge1 .$$

For constants $0<c_1<1<c_2$, $c_3>1$, the support of the period return is $(0,c_1\gamma)\cup(c_2\gamma,\infty)$ if $A^*>0$; $\{0\}\cup(c_3\gamma,\infty)$ if $-1\le A^*\le0$; $\{0\}\cup(c_3\gamma,\gamma/(1-|A^*|^{-1/(1-\alpha)}))$ if $-\kappa<A^*<-1$; $\{0\}$ if $A^*\le-\kappa$. All $\gamma\ge0$ and $k\ge0$ are covered.

Milestones, in proof order

Lemma 1 (shape of $G_a$); Lemma 2 ($\bar G_a$); the static Merton value $\sup_{Y\in L_{0,\tau}(1)}E[Y^\alpha]=e^{h\tau}$; Proposition 3 (the optimizer of (14)); Proposition 4 ($\Phi$ is a contraction with constant $e^{-(\beta-h)\tau}$); Lemma 3 (bounds on $\Phi$ and $A^*$); the dynamic Merton value $x^\alpha e^{hT}$; summability and Fubini for (4); $ZX$ is a supermartingale; the conditional problem (26) and the supermartingale (27); the upper bound $V(x)\le A^*x^\alpha$; stationarity of the multiplier; replication of budget-feasible sequences; the martingale $\hat M$ and attainment; exclusion of Case 4 at $A^*$.

Significance

The theorem reduces an infinite-horizon, path-dependent, non-concave control problem to a scalar fixed point $A^*$, and makes the optimal policy explicit: each period's gross return is an i.i.d. function of the pricing-kernel increment. The four support regimes are the paper's economic content: a strictly solvent portfolio when $A^*>0$, a positive probability of total loss in Cases 2a and 2b, and immediate liquidation in Case 3. These drive the paper's results on how evaluation frequency and target level moderate or amplify risk taking (Propositions 2 and 5, Corollary 2, which build on Theorem 1).

The result is proved in the paper; nothing in it has a machine-checked proof. Formalizing it requires a nonnegative self-financing wealth model over the published local Itô integral, a non-concave static utility maximization by concavification and Legendre duality, the finite-horizon Merton value with power utility, a Banach fixed-point argument for $\Phi$, and a discrete-time verification across evaluation dates.

Difficulty

The natural route is dynamic programming: guess $V(x)=A^*x^\alpha$ and verify the Bellman equation (10). It fails as a proof because the HJB equation (8) has a periodic boundary condition involving the unknown value itself, and $V$ is not concave. The hard steps are stochastic: the supermartingale property of deflated wealth needs an Itô product rule for the local integral; replication needs the martingale representation theorem for the Brownian filtration and, when the budget does not bind, a "doubling down" strategy that destroys wealth while staying nonnegative. On the deterministic side, Lemma 2 and Proposition 3 require existence and uniqueness of the tangency points $c_1,c_2,c_3$ in four regimes.

Formalization scope

Time is $[0,\infty)$ (ℝ≥0), $T_i=i\tau$. The filtration is a hypothesis: it equals the augmented natural filtration of $B$. The Itô integral is EthierKurtz.HasBrownianItoIntegral, which asks for pathwise square integrability; under the augmented filtration this changes no value process beyond null sets. $V$ and $F$ are suprema in the extended reals; budgets $E[Z_\tau Y]\le1$ are Lebesgue integrals of nonnegative functions, so infinite-cost payoffs are infeasible. The objective is a Bochner integral of a tsum, genuine for every admissible portfolio by the summability milestone.

Three readings are fixed. "Support is $S$" means: the variable lies in $S$ almost surely and every point of $S$ is charged; the literal topological support is closed and would make the table false. "The optimal portfolio is given by (16)" means existence of an optimizer of that form; uniqueness fails at $A^*=-\kappa$. $y^*_{A^*}$ is any maximizer selection of $\bar G_{A^*}(y)-qy$, as on p.38; Proposition 3's explicit function is one.

Three milestones are corrected minimally, each with a counterexample in its item: Lemma 2, Case 1 has $1/(1+(k/a)^{1/(2-\alpha)})\le1$ (equality at $k=0$); Lemma 2 and Proposition 3, Case 2, exclude $(a,k)=(-1,0)$, where (22) has no root; Proposition 3 assumes $\gamma>0$ in Cases 1 and 2, as their constants are undefined at $\gamma=0$ (Cases 3 and 4 keep $\gamma\ge0$). The goal is unaffected: $k=0$ forces $A^*\ge0$, and at $\gamma=0$ only Case 1 occurs.

Reusable beyond this mission: the admissible-wealth model over the Itô relation, the smallest concave majorant, the Merton values, and the replication milestone. Contributions to any milestone, and to general lemmas such as the Itô product rule for EthierKurtz.HasBrownianItoIntegral or Brownian martingale representation, are welcome.

Selected references

• A. S. L. Tse, H. Zheng, Portfolio Selection, Periodic Evaluations and Risk Taking, SSRN Working Paper 3971852, version of June 20, 2023. https://ssrn.com/abstract=3971852 (published: Operations Research, 2023, https://doi.org/10.1287/opre.2021.0780).
• A. Tversky, D. Kahneman, Advances in prospect theory: cumulative representation of uncertainty, Journal of Risk and Uncertainty 5(4):297–323, 1992. https://doi.org/10.1007/BF00122574
• A. B. Berkelaar, R. Kouwenberg, T. Post, Optimal portfolio choice under loss aversion, Review of Economics and Statistics 86(4):973–987, 2004.
• C. Reichlin, Utility maximization with a given pricing measure when the utility is not necessarily concave, Mathematics and Financial Economics 7(4):531–556, 2013.
• M. Bichuch, S. Sturm, Portfolio optimization under convex incentive schemes, Finance and Stochastics 18(4):873–915, 2014.
• D. Duffie, Dynamic Asset Pricing Theory, 3rd ed., Princeton University Press, 2001.

Motivation

Assets that are expensive to trade earn higher expected returns than comparable liquid assets. Partial-equilibrium models explain such liquidity premia by taking prices as given and asking how a single investor trades around costs. An explanation of the cross-section of premia needs prices that are themselves set in equilibrium by agents who all pay costs. Muhle-Karbe, Shi and Yang (arXiv:2011.13625v1; Mathematics of Operations Research, 2023) build such a model with $N$ mean-variance agents, $K$ risky assets and quadratic trading costs, and show that an equilibrium exists for any numbers of agents and assets.

Timeline. For one risky asset and two agents, Herdegen, Muhle-Karbe and Possamaï (reference [21] of the paper, Finance and Stochastics) reduced the equilibrium to a fully coupled FBSDE and obtained existence only when the risk aversions are sufficiently similar, via Picard iteration; the reduced Riccati system there has four coupled equations. Models that penalize squared inventories instead of fluctuations lead to linear FBSDEs and are solvable in general ([6, 33] of the paper). The present paper (2020) reduces the problem to two matrix Riccati equations and proves their global solvability without smallness conditions.

Setting

A filtered probability space $(\Omega,\mathcal F,(\mathcal F_t)_{t\in[0,T]},P)$ with horizon $T>0$ carries a $D$-dimensional Brownian motion $W$. There are $N\ge2$ agents with risk aversions $\gamma^n>0$; agent $N$ is the most risk-averse, $\gamma^N=\max_n\gamma^n$ (3.2). Agent $n$ receives the endowment $d\zeta^n_t=(\xi^n_t)^\top dW_t$, and the aggregate endowment is zero. There are $K\le D$ risky assets with supply $s\in\mathbb R^K$ and prices $dS_t=\mu_t\,dt+\sigma_t\,dW_t$, $S_T=\mathfrak S$ (2.2), where the drift $\mu$ and the volatility $\sigma$ are to be found.

Agent $n$ starts from $\varphi^n_{0-}$ (with $\sum_n\varphi^n_{0-}=s$), trades at rate $\dot\varphi\in\mathbb H^4(\mathbb R^K)$, holds $\varphi_t=\varphi^n_{0-}+\int_0^t\dot\varphi_u\,du$ and maximizes

$$J^n_T(\dot\varphi)=\mathbb E\Big[\int_0^T\Big(\varphi_t^\top\mu_t-\frac{\gamma^n}2\|\sigma_t^\top\varphi_t+\xi^n_t\|^2-\frac12\dot\varphi_t^\top\Lambda\dot\varphi_t\Big)dt\Big],\qquad(4.1)$$

with a symmetric positive definite cost matrix $\Lambda$. A Radner equilibrium with transaction costs is a price process for which every agent has an optimal rate and the positions sum to $s$ at all times. The risk-aversion matrix is $\Gamma=\mathrm{diag}\{\gamma^1,\dots,\gamma^{N-1}\}-\frac1N\mathbb 1_{N-1}\mathbb 1_{N-1}^\top\mathrm{diag}\{\gamma^n-\gamma^N\}$ (4.7), and $c_n=\bar\gamma(1/\gamma^n-1/\gamma^N)$ with $\bar\gamma=(\sum_n1/\gamma^n)^{-1}$.

Under Assumption 3.2 ($\mathfrak S=\alpha W_T+\beta T$, $\operatorname{rank}\alpha=\operatorname{rank}\alpha\alpha^\top=K$) and Assumption 4.3 ($\xi^n_t=\xi^nW_t$), the equilibrium is built from the matrix Riccati system

$$F'=\Gamma\otimes\sigma_H\sigma_H^\top-F(I_{N-1}\otimes\Lambda^{-1})F,\quad H'=(\Gamma\otimes\sigma_H)\xi-F(I_{N-1}\otimes\Lambda^{-1})H,\quad F(0)=H(0)=0,\qquad(4.8)$$

with $\sigma_H=\alpha+(c\otimes I_K)^\top H$, and from the fundamental matrix $\Phi$ of (4.9).

Formalization targets

Goal: Theorem 4.5

For the solution $(F,H)$ of (4.8) on $[0,T]$ and $\Phi$ of (4.9), the explicit tuple (4.11)–(4.14) solves the FBSDE of Lemma 4.2, and

$$S=\bar S+\mathcal Y-(c\otimes\Lambda)^\top\dot\varphi\ \text{ is a Radner equilibrium with transaction costs,}$$

with $\bar S$ the frictionless Bachelier price of Proposition 3.3. The Lean goal asserts that (4.8) and (4.9) are solvable, that $\Phi(t)$ is invertible, that the tuple lies in $\mathbb H^4\times\mathbb H^4\times\mathbb H^2\times\mathcal S^2\times\mathbb H^4$ and satisfies the three dynamics, and that every agent's rate is optimal against all $\mathbb H^4$ rates and the market clears.

Milestones

• Lemma 4.2: a solution of the FBSDE gives optimal, market-clearing rates.
• Lemma 7.1: $\Gamma$ is positive definite and all its eigenvalues are real and positive.
• Lemmas 7.4–7.6 and Corollaries 7.7–7.8: Kronecker positivity, positivity of generators of linear matrix ODEs, $F\succeq0$, and $\|\Phi_F(r)\Phi_F^{-1}(\tau)\|_{op}\le1$.
• (7.13): $\|\alpha+(c\otimes I_K)^\top H(\tau)\|_{op}\le\|\alpha\|\exp(\|c\|\|\Lambda\|^{1/2}\|\Lambda^{-1}\|^{1/2}\|\Gamma\|\|\xi\|\tau)$.
• Lemma 4.4: (4.8) has a unique global solution with $F\succeq0$.
• (7.17)–(7.19): algebraic identities for $\Gamma$ and $c$.

Significance

Theorem 4.5 gives an equilibrium with transaction costs in closed form up to the solution of a matrix ODE, for arbitrary numbers of agents and assets and without any smallness assumption. It is the basis of the paper's small-cost expansions of liquidity premia (Theorem 5.1) and of its calibration to data. Lemma 4.4 is of independent interest as a global well-posedness result for a non-symmetric matrix Riccati system.

The paper's results are proved on paper; none of them has a machine-checked proof. A formalization adds a checked chain from the stochastic model to the explicit equilibrium, including the sufficiency of the first-order conditions for (4.1), which the paper leaves to "the above discussion".

Difficulty

The obvious route to (4.8) is Picard–Lindelöf plus a comparison argument. Picard–Lindelöf gives only a local solution, and comparison principles for matrix Riccati equations need symmetric, ordered coefficients: here $\Gamma$ and $F$ are not symmetric, so the standard Riccati theory does not apply. Global existence comes from showing that $F$ stays positive semidefinite in the non-symmetric sense (Lemmas 7.1, 7.4, 7.5), which makes a fundamental matrix a contraction (Corollary 7.8) and yields a Gronwall bound (7.13) that excludes blow-up. Mathlib has no blow-up alternative for ODEs and no Liouville formula. On the stochastic side, the candidate involves a pathwise integral of $W$ and its membership in the $\mathbb H^p$ spaces needs Gaussian moment bounds; optimality needs concavity of (4.1) and a true-martingale argument.

Formalization scope

Agents are Fin (M + 1) ($N=M+1\ge2$, agent $N$ is Fin.last M); stacked vectors are indexed by Fin M × Fin K, block first, matching Mathlib's kroneckerMap. "Positive (semi)definite" means $b^\top Ab>0$ ($\ge0$) without symmetry, as in footnotes 10 and 19; using Mathlib's PosDef would make Lemma 7.1 false. $\|\cdot\|$ is the Frobenius norm and $\|\cdot\|_{op}$ the $\ell^2$ operator norm, both explicit functions. Matrix ODEs are entrywise derivatives within the interval. $\Lambda^{1/2}$ is a parameter $R$ with $R^\top=R\succ0$, $R^2=\Lambda$. Time is $\mathbb R_{\ge0}$ truncated to $[0,T]$; the filtration is arbitrary; the Itô integral is the published Peng1990.SMP.IsItoIntegral. Admissible rates are exactly $\mathbb H^4$, and the objective is integrable for every admissible rate, so Lean's junk value never decides optimality. The goal asserts existence of $F,H,\Phi$ and invertibility of $\Phi$, so it is not vacuous and Lean's total inverse cannot trivialize $\Psi$.

Two printed slips are corrected: Lemma 4.4's $c_n>0$ is false when some $\gamma^n=\gamma^N$ and is stated as $c_n\ge0$; the first entry of (7.18) is $\gamma^N-\gamma^1$. Readings: $\beta\in\mathbb R^K$ (printed $\mathbb R^D$); Lemma 7.1's eigenvalues are all real and positive; Lemma 4.2 assumes the price drift lies in $\mathbb H^2$. Lemmas 7.5–7.6, Corollaries 7.7–7.8 and (7.13) are stated on any initial interval rather than the maximal one.

Needed infrastructure, reusable beyond this mission: linear matrix ODEs (existence, invertibility of fundamental matrices), ODE continuation, Kronecker products and non-symmetric positivity, Itô integrals of deterministic integrands against Brownian motion and the product rule for them. Proofs of any milestone are welcome, as are intermediate lemmas such as (7.10)–(7.12).

Selected references

• J. Muhle-Karbe, X. Shi, C. Yang, An Equilibrium Model for the Cross-Section of Liquidity Premia, arXiv:2011.13625v1, 2020; Mathematics of Operations Research, 2023. https://arxiv.org/abs/2011.13625v1
• M. Herdegen, J. Muhle-Karbe, D. Possamaï, Equilibrium Asset Pricing with Transaction Costs, Finance and Stochastics (forthcoming in 2020 per the paper's reference [21]).
• S. Peng, A General Stochastic Maximum Principle for Optimal Control Problems, SIAM J. Control Optim. 28(4), 1990 (source of the published Itô-integral definitions Peng1990_SMP_Stochastic reused here).

A firm that controls what the public learns

A firm whose revenue follows the public's belief about a hidden value, such as the quality of a product, can shape that belief by sending information. It chooses how much to send, and it can bias what it sends. Advertising, propaganda and sell-side research share this structure. Keppo, Kim and Zhang formulate it as an infinite-horizon Markov decision process on the public's beliefs and solve it in closed form. The model sits next to Bayesian persuasion (Kamenica and Gentzkow 2011) and to costly lying (Kartik 2009). It differs from them in having no game: the public keeps a fixed, naive updating rule, and the firm solves a control problem against it. Explicit solutions of Bayesian dynamic programs are rare, and they are rarer still when the action is a change of measure.

The manipulation problem

The public treats a parameter $\theta$ as random, with normal belief $N(\mu,s)$. In each period the firm picks a dissemination quantity $q\ge0$, at cost $c_tq$, with cost rate $c_t=c_1\eta^{t-1}$. The public would then see a Gaussian signal with drift $\theta$ over a horizon $q$, and its posterior mean $\mu^q$ would have law $N(\mu,\sigma^2_{\mu^q})$ with $\sigma^2_{\mu^q}=s^2q/(1+sq)$.

The firm also picks a distortion rule: any law $G\ll N(\mu,\sigma^2_{\mu^q})$ with finite mean. The new posterior mean is drawn from $G$, and the firm pays $\gamma D(G\|N(\mu,\sigma^2_{\mu^q}))$, a multiple of the relative entropy. The public still updates its variance to $s/(1+sq)$, whatever $G$ is. The firm receives the posterior mean each period.

A policy makes these choices as a function of the whole history of posterior means, and the value is

$$V(\mu,s,c)=\sup_M\ \sum_{t\ge1}\alpha^{t-1}\,E\bigl[\mu_t-c_tq_t-\gamma D_t\bigr],\qquad\alpha\in[0,1).$$

Formalization targets

Goal: the optimal policy

With $\bar\eta=\min(\eta,1)$, let $s_{TH}(c)=\sqrt{2\gamma c(1-\alpha)(1-\alpha\bar\eta)}$. The goal is Theorem 2 of the paper together with the optimal quantity of Theorem 1. For all $\alpha\in[0,1)$, $\gamma>0$, $\eta\ge0$:

$$V(\mu,s,c)=\frac{\mu}{1-\alpha}+G(s,c),$$

with $G$ the explicit function (18). This value solves the Bellman equation (10). For $c>0$ the unique maximizer of (10) is

$$q^*(s,c)=\Bigl(\frac1{s_{TH}(c)}-\frac1s\Bigr)^+,\qquad G^*=N\Bigl(\mu+\frac{(s-s_{TH}(c))^+}{(1-\alpha)\gamma},\ (s-s_{TH}(c))^+\Bigr).$$

For $c_1,\eta>0$ the Markov policy built from these attains $V$.

Milestones

The milestones follow the proof: the Gaussian update (Lemma EC.2); uniqueness of the Bellman solution (Lemma 1); the variational formula (Lemma 2) and its Gaussian case; the reduction of (10) to (13) (Corollary 1); the finite-stage decomposition and bound; separability (Lemma EC.3); the derivative properties (Lemma 3); monotonicity in $\eta$ (Proposition 1(d)); and Theorem 1.

What the theorem gives

The result is a complete description of optimal manipulation. The firm is silent until the variance exceeds a threshold, and it then brings the variance down to exactly that threshold. Among all distortions it chooses a pure shift of the mean. Everything downstream in the paper, namely the time path of beliefs, the comparative statics and the social-learning extension, reads off these formulas.

Formalizing it adds three things. The result is proved on paper and, as far as the platform shows, not formalized. The mission gives the platform a closed-form infinite-horizon control problem whose action is a change of measure, with history-dependent policies on the Ionescu-Tulcea measure. It also repairs the argument: several printed statements are false as they stand. Lemma 1 asserts a unique solution on bounded functions, which contain none. Lemma 2 needs an integrability condition for attainment. Lemma 3 asserts a second derivative that does not exist at the thresholds. The corrected statements are recorded item by item, with counterexamples.

Where the difficulty lies

The obvious argument is contraction on bounded functions followed by a verification, and it fails at the first step: every solution contains the unbounded term $\mu/(1-\alpha)$, so the space of the printed proof is empty of solutions, and uniqueness needs a weighted class in which $v+c$ is excluded.

The second obstacle is the upper bound over policies. A policy may depend on the whole history and may send the expected mean to $-\infty$, so a transversality argument is not available. The bound has to go through the finite-stage problems by conditioning on the Ionescu-Tulcea measure.

The third is the verification of (18), a piecewise function whose pieces are indexed by the dissemination time. Its derivative is continuous across thresholds but its second derivative is not. For $c=0$ or $\eta=0$ the supremum in (8) is not attained, so the lower bound there needs near-optimal policies.

Formalization scope

Lean represents states and quantities in ℝ≥0. A distortion is encoded by the distorted law G, with the conditions G ≪ baseLaw μ s q and y integrable; (4) is exactly this bijection. The cost is Mathlib's klDiv. A Policy is a sequence of measurable quantity rules and Markov kernels on histories of posterior means, with the law of the belief process given by Kernel.traj. Periods are indexed from $0$, so period $t=n+1$ has cost rate $c_1\eta^n$. The total profit is a limsup of partial sums in EReal, with costs in ℝ≥0∞, so an infinite cost is never free. Real suprema are stated with IsLUB.

The sup in V ranges over all history-dependent policies and all distortions, not Markov ones or Gaussian shifts, so the theorem cannot be obtained by restricting to the form of its answer. klDiv is never converted to a real at an infinite value. The value $\eta>1$ is covered through $\bar\eta$, while the cost rate keeps the true $\eta$.

A complete development needs Gaussian conjugacy, the Gibbs variational identity with its uniqueness clause, the Gaussian tilt, and finite-horizon conditioning on Kernel.traj. The conjugacy, the tilt and the conditioning lemmas are reusable beyond this mission. Proofs of any milestone are welcome, and so are direct proofs of the goal that avoid Lemma 3, whose role in the paper's argument the verification of (18) can replace.

Selected references

• J. Keppo, M. J. Kim, X. Zhang, Learning Manipulation Through Information Dissemination, SSRN manuscript 3465030, PDF of 2021-09-04. https://ssrn.com/abstract=3465030
• P. Dupuis, R. S. Ellis, A Weak Convergence Approach to the Theory of Large Deviations, Wiley, 1997. https://doi.org/10.1002/9781118165904
• E. Kamenica, M. Gentzkow, Bayesian Persuasion, American Economic Review 101(6), 2011. https://doi.org/10.1257/aer.101.6.2590
• N. Kartik, Strategic Communication with Lying Costs, Review of Economic Studies 76(4), 2009. https://doi.org/10.1111/j.1467-937X.2009.00559.x
• D. P. Bertsekas, S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Athena Scientific, 1996. https://web.mit.edu/dimitrib/www/soc.html