Control Theory

Algorithmic Game Theory Operations Research Stochastic Systems·Captain: mikedeng1

Nonzero-Sum Stochastic Differential Games with Impulse Controls: A Verification Theorem with Applications 2: An Explicit Family of Nash Equilibria for the Linear Impulse GameResearch Paper

Motivation

Impulse control models an agent who acts on a random system through discrete interventions, each with a fixed cost: inventory replenishment, cash management, exchange-rate interventions by a central bank. With two agents whose objectives conflict, the problem becomes a nonzero-sum stochastic differential game with impulse controls. Before the work of Aïd, Basei, Callegaro, Campi and Vargiolu (Math. Oper. Res. 45(1), 2020; preprint arXiv:1605.00039), such games had no general verification theorem and few explicit equilibria; the paper supplies both. Its main application, formalized in this mission, is a game between two central banks with different targets for an exchange rate, a two-player version of the exchange-rate control models of Bertola, Runggaldier and Yasuda and of Cadenillas and Zapatero (references [10], [12] of the paper). The paper proves that this game has an explicit one-parameter family of Nash equilibria of threshold type, with closed-form payoffs.

Setting

The state is a real process. Without interventions it is $x+\sigma W_s$ , where $W$ is a standard real Brownian motion and $\sigma>0$ . Player 1 may shift it up by impulses $\delta\in Z_1=[0,\infty[$ , player 2 down by impulses $\delta\in Z_2=]-\infty,0]$ :

X_s=x+\sigma W_s+\sum_{k:\tau_{1,k}\le s}\delta_{1,k}+\sum_{k:\tau_{2,k}\le s}\delta_{2,k}.

Player 1 earns the running payoff $f_1(X_s)=X_s-s_1$ , player 2 earns $f_2(X_s)=s_2-X_s$ , with $s_1<s_2$ . An impulse $\delta$ costs its author $c+\lambda|\delta|$ and pays the opponent $\tilde c+\tilde\lambda|\delta|$ . Payoffs are discounted at rate $\rho>0$ . The standing assumptions are $c\ge\tilde c\ge0$ , $\lambda\ge\tilde\lambda\ge0$ , $(c,\lambda)\ne(\tilde c,\tilde\lambda)$ and $1-\lambda\rho>0$ .

A strategy of player $i$ is a pair $\varphi_i=(\mathcal C_i,\xi_i)$ : an open continuation region $\mathcal C_i\subseteq\mathbb R$ and a continuous impulse map $\xi_i:\mathbb R\to Z_i$ . Player $i$ intervenes when the state leaves $\mathcal C_i$ , applying the impulse $\xi_i(\text{state})$ ; player 1 has priority when both want to act. This rule defines the controlled process $X^{x;\varphi_1,\varphi_2}$ and the interventions $(\tau_{i,k},\delta_{i,k})$ inductively. Player $i$ 's payoff is

J^i(x;\varphi_1,\varphi_2)=\mathbb E_x\Big[\int_0^\infty e^{-\rho s}f_i(X_s)\,ds-\sum_{k}e^{-\rho\tau_{i,k}}(c+\lambda|\delta_{i,k}|)+\sum_{k}e^{-\rho\tau_{j,k}}(\tilde c+\tilde\lambda|\delta_{j,k}|)\Big].

A pair is $x$ -admissible, $(\varphi_1,\varphi_2)\in\Phi_x$ , when these random variables are integrable, $\sup_t|X_t|$ has all moments, and neither player's interventions accumulate in finite time. A Nash equilibrium is an admissible pair from which no player gains by deviating to any strategy that keeps the pair admissible.

The explicit objects are $\theta=\sqrt{2\rho/\sigma^2}$ , $\eta=(1-\lambda\rho)/\rho$ and

F(y)=2y+\theta c-\eta\log\frac{\eta+y}{\eta-y},\qquad 0<y<\eta .

From the zero $\xi$ of $F$ and a free parameter $\tilde s\in\mathbb R$ , the formulas (4.20)–(4.21) give thresholds $\bar x_1<\bar x_2$ , targets $x_1^*,x_2^*\in]\bar x_1,\bar x_2[$ , coefficients $A_{ij}$ , the functions $\varphi_i(y)=A_{i1}e^{\theta y}+A_{i2}e^{-\theta y}\pm(y-s_i)/\rho$ and the piecewise candidates $\tilde V_1,\tilde V_2$ of (4.6). These are linear outside $]\bar x_1,\bar x_2[$ and equal $\varphi_i$ inside.

Formalization targets

Goal: Proposition 4.7

For every $\tilde s\in\mathbb R$ and every initial state $x\in\mathbb R$ , the threshold strategies

\varphi_1^*=\big(]\bar x_1,+\infty[,\ y\mapsto\max(x_1^*-y,0)\big),\qquad \varphi_2^*=\big(]-\infty,\bar x_2[,\ y\mapsto\min(x_2^*-y,0)\big)

form an $x$ -admissible Nash equilibrium, and

J^1(x;\varphi_1^*,\varphi_2^*)=\tilde V_1(x),\qquad J^2(x;\varphi_1^*,\varphi_2^*)=\tilde V_2(x).

Milestones

(4.17). $F$ has a unique zero $\xi\in(0,\eta)$ .
Proposition 4.2. For every $\tilde s$ , the explicit 8-uple (4.20) satisfies the order conditions (4.7) and the optimality and pasting conditions (4.8)–(4.9). Moreover, $\varphi_2''$ changes sign exactly once in $]x_2^*,\bar x_2[$ .
Lemma 4.6. The impulses (4.23) maximise $\delta\mapsto\tilde V_i(x+\delta)-c-\lambda|\delta|$ , and the intervention operators satisfy (4.24): $\{\mathcal M_1\tilde V_1-\tilde V_1<0\}=]\bar x_1,\infty[$ and $\{\mathcal M_2\tilde V_2-\tilde V_2<0\}=]-\infty,\bar x_2[$ .
Condition (v). The equilibrium pair is $x$ -admissible for every $x$ . This includes the integrability (4.26) of the discounted intervention costs.

Milestones 1–3 are deterministic real analysis; milestone 4 and the goal are probabilistic.

Significance

The result gives explicit equilibria, with explicit thresholds and payoffs, for a nonzero-sum stochastic game with impulse controls. Such games rarely have closed-form solutions. The equilibria form a continuum indexed by $\tilde s$ : equilibrium payoffs are not unique, and every equilibrium in the family is a translate of a fixed interval policy. The explicit formulas also support the comparative statics of Section 4.4, where the continuation region widens as the fixed cost grows.

Proposition 4.7 is proved in the paper by applying its verification theorem (Theorem 3.3) to $\tilde V_1,\tilde V_2$ . The admissibility estimate (4.26) is written out only for initial states $x\in\{x_1^*,x_2^*\}$ ; the general case is said to be similar. As far as is known, none of these results has a machine-checked proof. A formal proof would check every regularity, pasting and admissibility condition. It would also yield a reusable pathwise construction of impulse-controlled Brownian motion.

Difficulty

The deterministic milestones need careful algebra with nested logarithms and square roots. Proving Lemma 4.6 requires the global shape of $\tilde V_i(y)\pm\lambda y$ , which needs the sign pattern of $\varphi_2''$ from Proposition 4.2, not only local conditions at the thresholds.

The goal is harder. The Nash inequality must hold against every admissible deviation: any open continuation region and any continuous impulse map, not only threshold strategies. Comparing payoffs therefore needs a verification argument, namely Itô's formula for a function that is $C^2$ only piecewise and $C^1$ across the thresholds, applied along a process with an unbounded number of jumps, plus a localisation that uses the moment condition (2.8). Admissibility needs a renewal-type bound on the discounted number of interventions, built from i.i.d. exit times of Brownian motion from an interval.

Formalization scope

The Lean development lives in the namespace ImpulseGames.LinearGame.

The constants and standing assumptions are a structure Model with the proposition Model.Standing. The added hypothesis $c>0$ appears in every statement that uses $\xi$ : with $c=0$ , which the standing assumptions allow, $F$ has no zero in $(0,\eta)$ and the family (4.20) does not exist.
The zero $\xi$ is a parameter, constrained by $\xi\in(0,\eta)$ and $F(\xi)=0$ . Milestone 1 shows that exactly one such $\xi$ exists.
The Brownian motion is Mathlib's IsBrownianReal W P on a probability space, with time in $\mathbb R_{\ge0}$ . Definition 2.2 is formalized pathwise: exit times $\inf\{s>\tilde\tau_{k-1}:\tilde X^{k-1}_s\notin\mathcal C_i\}$ in $[0,\infty]$ with $\inf\emptyset=\infty$ , the tie rule favouring player 1, and $e^{-\rho\cdot\infty}=0$ for the tail of each impulse control. No SDE or stochastic integral appears in any statement; the uncontrolled dynamics are $\zeta+\sigma(W_s-W_t)$ .
Payoffs are Bochner expectations. $\Phi_x$ requires every random variable of (2.7) to be integrable, so no deviation can obtain the default value $0$ of a non-integrable expectation. The moment condition (2.8) is stated with an extended-real supremum, and (2.9) is read almost surely.
The Nash condition quantifies over all strategies of Definition 2.1. A formalization that restricts deviations to threshold strategies would be a different, weaker theorem and is excluded. Likewise, the equilibrium payoffs $\tilde V_i$ are the explicit formulas (4.6), never defined as "the equilibrium value".

Two slips of the page are corrected. First, the paper's impulse maps $\xi_i^*(y)=x_i^*-y$ are not $Z_i$ -valued on all of $\mathbb R$ ; they are replaced by $\max(x_1^*-y,0)$ and $\min(x_2^*-y,0)$ , which agree with them wherever each player acts. Second, in Lemma 4.6 the maximiser (4.23) is not unique when $\lambda=\tilde\lambda$ , in the opponent's intervention region (all impulses tie there). The statement asserts maximality everywhere and uniqueness outside that region.

A complete development needs: elementary real analysis for milestones 1–3; a pathwise theory of piecewise-defined processes; an Itô formula for Brownian motion with $C^1$ , piecewise- $C^2$ functions; and exit-time estimates for Brownian motion. The last two are reusable well beyond this mission. Proofs of the deterministic milestones are welcome independently of the stochastic part.

Selected references

R. Aïd, M. Basei, G. Callegaro, L. Campi, T. Vargiolu, Nonzero-sum stochastic differential games with impulse controls: a verification theorem with applications, Mathematics of Operations Research 45(1), 2020. https://doi.org/10.1287/moor.2019.0989 (accepted manuscript: arXiv:1605.00039v4, https://arxiv.org/abs/1605.00039)
G. Bertola, W. J. Runggaldier, K. Yasuda, On classical and restricted impulse stochastic control for the exchange rate, Applied Mathematics and Optimization 74(2), 423–454, 2016.
A. Cadenillas, F. Zapatero, Classical and impulse stochastic control of the exchange rate using interest rates and reserves, Mathematical Finance 10(2), 141–156, 2000.
B. Øksendal, A. Sulem, Applied Stochastic Control of Jump Diffusions, 2nd ed., Springer, 2007.

9 thms2 active usersReviewed

Completed

Dynamic Programming Operations Research Optimization·Captain: mikedeng1

Stochastic Optimal Control: The Discrete-Time Case I: Finite-Horizon Abstract Dynamic Programming — the DP Algorithm Yields the N-Stage Optimal CostTextbook

Motivation

Dynamic programming (DP) solves sequential decision problems by backward recursion: compute the optimal cost of the last stage, then of the last two stages, and so on. For problems with finitely many states and controls and real-valued costs, the recursion obviously gives the optimal cost. Applications are rarely like that. Control spaces are continuous, costs can be unbounded or infinite, the criterion can be multiplicative (risk-sensitive exponential cost) or worst-case (minimax), and the set of policies is an infinite product of function spaces. In this setting the DP recursion can fail to produce the optimal cost.

Bertsekas and Shreve, Stochastic Optimal Control: The Discrete-Time Case (Academic Press 1978; Athena Scientific 1996), Part I, separates the order-theoretic content of DP from the measure theory. It works with an abstract monotone mapping $H$ that covers deterministic, stochastic, multiplicative-cost and minimax problems at once, following Bertsekas, Monotone mappings with application in dynamic programming, SIAM J. Control Optim. 15 (1977). Chapter 3 answers the finite-horizon questions: when does the DP algorithm give the $N$ -stage optimal cost, and when do optimal or nearly optimal policies exist? This mission is the first of a series formalizing the book. Later chapters (contraction models, monotone increase and decrease models, the Borel models of Part II) are built on the model fixed here.

Setting

Let $S$ (states) and $C$ (controls) be sets, and for each $x\in S$ let $U(x)\subseteq C$ be a nonempty control constraint set. Write $R^*=[-\infty,\infty]$ and let $F$ be the set of all functions $J:S\to R^*$ , ordered pointwise. A mapping $H:S\times C\times F\to R^*$ is given, subject to the Monotonicity Assumption: $J\le J'$ implies $H(x,u,J)\le H(x,u,J')$ for all $x\in S$ , $u\in U(x)$ .

A selector is a function $\mu:S\to C$ with $\mu(x)\in U(x)$ for all $x$ . A policy is a sequence $\pi=(\mu_0,\mu_1,\dots)$ of selectors. Define

T_\mu(J)(x)=H[x,\mu(x),J],\qquad T(J)(x)=\inf_{u\in U(x)}H(x,u,J),

and let $T^k$ be the $k$ -fold composition of $T$ . A terminal function $J_0\in F$ with $J_0(x)>-\infty$ for all $x$ is fixed. The $N$ -stage cost of $\pi$ and the $N$ -stage optimal cost are

J_{N,\pi}=(T_{\mu_0}T_{\mu_1}\cdots T_{\mu_{N-1}})(J_0),\qquad J^*_N(x)=\inf_{\pi}J_{N,\pi}(x).

A policy is uniformly $N$ -stage optimal if each tail $(\mu_i,\mu_{i+1},\dots)$ is $(N-i)$ -stage optimal, and $N$ -stage $\varepsilon$ -optimal if $J_{N,\pi}(x)\le J^*_N(x)+\varepsilon$ where $J^*_N(x)>-\infty$ and $J_{N,\pi}(x)\le-1/\varepsilon$ where $J^*_N(x)=-\infty$ .

The three conditions on $H$ used in the chapter are F.1 (continuity of $H$ along nonincreasing sequences $J_k$ with $H(x,u,J_1)<\infty$ ), F.2 (there is $\alpha>0$ with $H(x,u,J)\le H(x,u,J+r)\le H(x,u,J)+\alpha r$ for all $r>0$ ), and F.3 (a quantitative selection property with a constant $\beta>0$ ).

Formalization targets

Goal: Proposition 3.1

Under F.1, if $J_{k,\pi}(x)<\infty$ for all $x,\pi$ and $k=1,\dots,N$ ; or under F.2, if $J^*_k(x)>-\infty$ for all $x$ and $k=1,\dots,N$ :

J^*_N=T^N(J_0),

and under F.2, for every $\varepsilon>0$ there is $\pi_\varepsilon$ with $J^*_N\le J_{N,\pi_\varepsilon}\le J^*_N+\varepsilon$ .

Milestones

Proposition 3.3: $\pi^*$ is uniformly $N$ -stage optimal iff $(T_{\mu^*_k}T^{N-k-1})(J_0)=T^{N-k}(J_0)$ for $k<N$ . Needs monotonicity only.
Corollary 3.3.1: a uniformly $N$ -stage optimal policy exists iff every infimum $T^{k+1}(J_0)(x)=\inf_{u}H[x,u,T^k(J_0)]$ is attained, and then $J^*_N=T^N(J_0)$ .
Proposition 3.4: if $C$ is Hausdorff and every sublevel set $\{u\in U(x)\mid H[x,u,T^k(J_0)]\le\lambda\}$ is compact, then $J^*_N=T^N(J_0)$ and a uniformly $N$ -stage optimal policy exists.
Proposition 3.7: the minimax mapping $H(x,u,J)=\sup_{w\in W(x,u)}\{g+\alpha J[f]\}$ satisfies F.2 with constant $\alpha$ .
Proposition 3.6: the multiplicative mapping $H(x,u,J)=E\{g\,J[f]\mid x,u\}$ over a countable disturbance set satisfies F.1, and F.2 with constant $b$ when $0\le g\le b$ .
Proposition 3.2: under F.3 and the finiteness of $J_{k,\pi}$ , $J^*_N=T^N(J_0)$ and, for $\varepsilon_n\downarrow0$ , policies with $\{\varepsilon_n\}$ -dominated convergence to optimality exist.
Corollary 3.7.1(a): for minimax control with $J_0=0$ and $J^*_k>-\infty$ , the DP algorithm gives $J^*_N$ and $N$ -stage $\varepsilon$ -optimal policies exist.

Significance

The identity $J^*_N=T^N(J_0)$ says that an infimum over an infinite-dimensional policy space equals $N$ nested one-dimensional infima. Every numerical use of finite-horizon DP depends on it, and so do the infinite-horizon results of later chapters, which pass to the limit in $T^N(J_0)$ . Corollary 3.3.1 and Proposition 3.4 give the existence of optimal policies, and Propositions 3.6 and 3.7 verify the abstract hypotheses for two models outside standard expected additive cost.

These results are proved in the book; none of them is formalized. Mathlib has no abstract DP model, and the platform's finite-horizon results (Bertsekas, Dynamic Programming and Optimal Control, Prop. 1.3.1 and the minimax DP algorithm) assume finite disturbance and constraint sets and real costs. They are special cases, not this theory. The finite-horizon results of the 1977 paper (Lemma 3.1 here, on compact sublevel sets, and Corollary 3.1.1, the F.1′ case) are already posed on the platform and are not posed again.

Difficulty

The obvious argument interchanges the infimum over policies with the composition of operators: $\inf_\pi T_{\mu_0}(\cdots)=T(\inf_{\pi'}\cdots)$ . The inequality $T^N(J_0)\le J^*_N$ follows from monotonicity alone. The reverse inequality is the content. Taking a near-minimizing selector at each stage requires either passing a limit inside $H$ (F.1) or bounding how errors at later stages propagate through $H$ (F.2, F.3). Both steps break at infinite values. With $J^*_k(x)=-\infty$ there may be no $\varepsilon$ -optimal policy at all (Counterexample 4 of the book). Without F.1 or F.2 the identity itself fails (Counterexamples 1–3). A proof must therefore track separately the states where the optimal cost is $-\infty$ , which is why F.3 and the definition of $\varepsilon$ -optimality have two cases.

Formalization scope

The model is a structure Model S C with fields U, U_nonempty, H : S → C → (S → EReal) → EReal and the monotonicity proof. Policies are ℕ → Selector, with selectors as a subtype of S → C. $T^N$ is m.T^[N], and $(T_{\mu_0}\cdots T_{\mu_{N-1}})(J)$ is a recursion that applies $T_{\mu_{N-1}}$ first. All values lie in EReal. The book's convention $\infty-\infty=\infty$ never arises in Propositions 3.1–3.4, which only add real numbers to extended reals. The minimax and multiplicative mappings implement it explicitly (badd, and an expectation that returns $+\infty$ when the positive part diverges). Every theorem assumes $J_0>-\infty$ and $N\ge1$ . Assumptions F.1–F.3 are predicates on the model. F.2 is also available with a named constant (F2With) so that Propositions 3.6 and 3.7 can carry the book's constants $b$ and $\alpha$ .

$J^*_N$ is defined as an infimum over policies of the composed operators, never through $T$ , so the goal is not true by definition. A formalization in which $J_{N,\pi}$ already contains an infimum over controls would make Proposition 3.1 hold by rfl, and this one rules that out.

Proving the goal needs elementary EReal order arithmetic, iterated infima over subtypes, and pointwise selection of near-minimizers via choice. Proposition 3.6 additionally needs monotone and dominated convergence for countable sums in ℝ≥0∞. The model and operator definitions are reusable by the later missions of the series (contraction, monotone increase and decrease models). Proofs of any milestone, and reusable EReal lemmas about shifting by real constants, are welcome.

Selected references

D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press 1978; Athena Scientific 1996, Chapters 2–3. https://web.mit.edu/dimitrib/www/soc.html
D. P. Bertsekas, Monotone mappings with application in dynamic programming, SIAM J. Control Optim. 15(3) (1977) 438–464. https://doi.org/10.1137/0315031
D. P. Bertsekas, Dynamic Programming and Stochastic Control, Academic Press 1976.
D. P. Bertsekas, Abstract Dynamic Programming, 3rd ed., Athena Scientific 2022. https://web.mit.edu/dimitrib/www/abstractdp_MIT.html

12 thms2 active usersReviewed

Mechanism Design Operations Research Stochastic Systems·Captain: mikedeng1

Optimal Electricity Demand Response Contracting with Responsiveness Incentives 2: The Producer's First-Best Value in Closed FormResearch Paper

Motivation

Electricity demand response asks consumers to lower their consumption during price events, when generation is expensive or scarce. Field trials such as the Low Carbon London experiment showed that consumers do react to price signals, but that the reaction is erratic: the average consumption falls while its variability stays high, and a producer that has to follow the load curve in real time pays for that variability. Aïd, Possamaï and Touzi (arXiv:1810.09063; Math. Oper. Res. 2022, doi:10.1287/moor.2021.1201) model this as a continuous-time principal–agent problem in which the consumer (the agent) controls both the level and the volatility of consumption, and the producer (the principal) designs a payment that rewards both.

The paper compares two benchmarks. In the second best, the producer observes only the consumption path and the consumer responds optimally to the contract; this is the subject of the companion mission of this series. In the first best, the producer dictates both the contract and the consumer's effort, subject only to the consumer's participation. The first best is the reference point against which the cost of moral hazard, the information rent, is measured. This mission formalizes the first-best value in closed form, Proposition 3.1 (i) of the paper.

The methodology follows the continuous-time principal–agent literature: Holmström and Milgrom (1987) for exponential utilities and linear contracts, Sannikov (2008) for the dynamic-programming view of the agent's continuation value, and Cvitanić, Possamaï and Touzi (2018) for contracts indexed on both the output and its quadratic variation.

Setting

Fix integers $N,d\ge0$ (usages for the mean effort and for the volatility effort), cost parameters $\mu\in(0,\infty)^N$ , $\lambda\in(0,\infty)^d$ , nominal volatilities $\sigma\in(0,\infty)^d$ , effort bounds $A_{\max}>0$ and $0<\varepsilon\le1$ , risk aversions $r,p>0$ , a marginal volatility cost $h>0$ , slopes $\kappa,\theta\in\mathbb R$ , a horizon $T>0$ , an initial consumption $X_0\in\mathbb R$ and a reservation utility $R_0<0$ .

The consumer chooses a mean effort $\alpha$ with values in $A=\prod_i[0,\mu_iA_{\max}]$ and a responsiveness effort $\beta$ with values in $B=[\varepsilon,1]^d$ , at cost

c(\alpha,\beta)=c_1(\alpha)+\tfrac12c_2(\beta),\qquad c_1(a)=\tfrac12\sum_i\frac{a_i^2}{\mu_i},\qquad c_2(b)=\sum_j\frac{\sigma_j^2}{\lambda_j}\big(b_j^{-1}-1\big).

The consumption $X$ follows $X_t=X_0-\int_0^t\alpha_s\cdot\mathbf 1\,ds+\int_0^t\sigma(\beta_s)\cdot dW_s$ with $\sigma(b)=(\sigma_1\sqrt{b_1},\dots,\sigma_d\sqrt{b_d})$ , in the weak sense: $X$ is the canonical process on $C([0,T],\mathbb R)$ , and an admissible pair $(\nu,\mathbb P)$ is a progressively measurable control $\nu=(\alpha,\beta)$ with a probability measure under which $X$ starts at $X_0$ and solves the associated martingale problem.

The consumer values consumption by $f(x)=\kappa x$ and the producer bears the generation cost $g(x)=\theta x$ ; write $\delta=\kappa-\theta$ . For a payment $\xi$ made at time $T$ , the consumer's and the producer's criteria are

J_A=\mathbb E^{\mathbb P}\Big[-e^{-r\left(\xi+\int_0^T(\kappa X_s-c(\nu_s))ds\right)}\Big],\qquad J_P=\mathbb E^{\mathbb P}\Big[-e^{-p\left(-\xi-\int_0^T\theta X_sds-\frac h2\langle X\rangle_T\right)}\Big].

A contract is an $\mathcal F_T$ -measurable $\xi$ with uniform exponential moments (2.5). The first-best value is

V^{FB}=\sup\big\{J_P(\xi,\nu,\mathbb P):\ \xi\text{ a contract},\ (\nu,\mathbb P)\text{ admissible},\ J_A(\xi,\nu,\mathbb P)\ge R_0\big\}.

The consumer's Hamiltonians are $H_m(z)=-\inf_{a\in A}\{a\cdot\mathbf 1\,z+c_1(a)\}$ and $H_v(\gamma)=-\frac12\inf_{b\in B}\{c_2(b)-\gamma|\sigma(b)|^2\}$ . Finally $\rho=\frac{rp}{r+p}$ , $L_0=-\frac1r\log(-R_0)$ , $U(x)=-e^{-px}$ , $\bar\mu=\sum_i\mu_i$ and $x^-=\max(0,-x)$ .

Formalization targets

Goal: Proposition 3.1 (i)

Assume $\delta^-T\le A_{\max}$ . Then

V^{FB}=U\big(\bar v(0,X_0)-L_0\big),\quad \bar v(0,X_0)=\delta TX_0+\int_0^T\Big(\tfrac12\bar\mu(\delta^-)^2(T-t)^2+H_v\big(-h-\rho\delta^2(T-t)^2\big)\Big)dt.

Milestones

Proposition 2.1. The best responses $\hat a(z)$ , $\hat b(\gamma)$ attain the infima defining $H_m$ , $H_v$ , and these Hamiltonians have explicit closed forms.
(A.5). The auxiliary value $\bar V=\sup_{(\nu,\mathbb P)}\mathbb E^{\mathbb P}\big[-e^{-\rho(\int_0^T(\delta X_t-c(\nu_t))dt-\frac h2\langle X\rangle_T)}\big]$ is finite and negative, and $V^{FB}=R_0(\bar V/R_0)^{1+p/r}$ .
Proposition A.3 (i), with the explicit solution of p. 28.

\bar V=-e^{-\rho\left(\delta TX_0+\int_0^T\bar m(t)dt\right)},\qquad \bar m(t)=H_m(\delta(T-t))+H_v\big(-h-\rho\delta^2(T-t)^2\big).

Significance

The closed form shows how the first-best value depends on each parameter: on the energy value discrepancy $\delta$ through the mean-effort term, on the volatility cost $h$ and the effective risk aversion $\rho$ through the volatility Hamiltonian, and on the reservation utility only through the shift by $L_0$ . It is one half of the paper's information rent (Proposition 3.4), the gap between the first- and second-best values, and it is the benchmark against which the calibrated contracts of the paper's Section 4 are judged.

The result is proved in the paper, partly by appeal to standard stochastic control arguments. To our knowledge it has no machine-checked proof. A formal proof requires a verification theorem for an exponential-utility control problem in the weak formulation, and a risk-sharing argument with a pathwise quadratic-variation term in the contract; both are reusable beyond this paper.

Difficulty

The deterministic parts, Proposition 2.1 and the algebra that turns (A.5) and the value of $\bar V$ into the goal, are calculus. The difficulty lies in the two stochastic steps. In (A.5), the producer's optimal payment for a given effort depends on $\langle X\rangle_T$ ; it must be realised as a measurable function of the path that is a contract in the sense of (2.5), uniformly over all admissible laws, and the participation constraint must be shown to bind. In Proposition A.3 (i), the upper bound on $\bar V$ must hold for every progressively measurable, path-dependent control, not only for Markov feedback controls; the paper invokes "standard stochastic control theory", which has to be made precise for controls of the volatility under a martingale-problem formulation, where no Brownian motion is given in advance.

Formalization scope

The canonical space is $C([0,T],\mathbb R)$ with the coordinate σ-algebra and the canonical filtration; processes are indexed by $[0,T]$ . Admissible pairs are given by a martingale problem: $X_0=X_0$ almost surely, and both $X_t-X_0+\int_0^t\alpha_s\cdot\mathbf 1\,ds$ and its square minus $\int_0^t|\sigma(\beta_s)|^2ds$ are martingales. In the criteria, $\langle X\rangle_T$ is replaced by its almost-sure value $\int_0^T|\sigma(\beta_s)|^2ds$ ; a contract remains any $\mathcal F_T$ -measurable function of the path. Expectations of utilities are negated lower Lebesgue integrals of exponentials in $[-\infty,0]$ , and every value is an extended-real supremum with $\sup\emptyset=-\infty$ . $B$ is read as $[\varepsilon,1]^d$ , with indices in Fin N and Fin d.

The Hamiltonians are defined by their infima, never by their closed forms, so that Proposition 2.1 is not true by definition, and the first-best value is a supremum over the model's own objects, not a variable pinned by hypotheses. Three hypotheses are added to the page: $\varepsilon\le1$ (so $B\ne\emptyset$ ), $R_0<0$ (so $L_0$ is defined), and, for the goal only, $\delta^-T\le A_{\max}$ , without which the printed $\frac12\bar\mu(\delta^-)^2(T-t)^2$ exceeds $H_m(\delta(T-t))$ and contradicts the paper's own proof. Misprints corrected and disclosed in the items: the closed form of $H_m$ in Proposition 2.1 is false for $z^->A_{\max}$ and is replaced by $\bar\mu(m z^--m^2/2)$ with $m=z^-\wedge A_{\max}$ ; the index range of $\hat b$ is $j=1,\dots,d$ ; on p. 28, $\int_0^t\bar m$ is $\int_t^T\bar m$ and "(A.11)" is (A.6).

The parts (ii)–(iii) of Proposition 3.1, the optimal efforts and the optimal contract, are not stated. Contributions welcome: a verification theorem for controlled martingale problems with bounded coefficients, exponential moment bounds uniform over admissible laws, and a pathwise quadratic variation on the canonical space.

Selected references

R. Aïd, D. Possamaï, N. Touzi, Optimal electricity demand response contracting with responsiveness incentives, arXiv:1810.09063v3, 2019; Math. Oper. Res. 2022. https://arxiv.org/abs/1810.09063
J. Cvitanić, D. Possamaï, N. Touzi, Dynamic programming approach to principal–agent problems, Finance Stoch. 22, 2018. https://arxiv.org/abs/1510.07111
B. Holmström, P. Milgrom, Aggregation and linearity in the provision of intertemporal incentives, Econometrica 55, 1987. https://doi.org/10.2307/1913238
Y. Sannikov, A continuous-time version of the principal–agent problem, Rev. Econ. Stud. 75, 2008. https://doi.org/10.1111/j.1467-937X.2007.00463.x
I. Karatzas, S. Shreve, Brownian Motion and Stochastic Calculus, Springer, 1991, §5.4 (martingale problems and weak solutions). https://doi.org/10.1007/978-1-4612-0949-2

7 thms2 active usersReviewed

Mechanism Design Operations Research Stochastic Systems·Captain: mikedeng1

Optimal Electricity Demand Response Contracting with Responsiveness Incentives 1: The Producer's Second-Best Value in Closed FormResearch Paper

Motivation

Demand response asks electricity consumers to lower or smooth their consumption when generation is expensive, in exchange for payments. Field trials such as Low Carbon London showed two effects of such incentives: consumers reduce their average consumption, and the variability of their response depends on how much effort they put into it. A producer who cannot observe the consumer's individual usages, only the aggregate consumption path, faces a moral hazard problem: the payment can depend only on what is observed.

Aïd, Possamaï and Touzi (arXiv:1810.09063v3, 2019; Math. Oper. Res. 2022) cast this as a continuous-time principal–agent problem in which the consumer controls both the drift and the volatility of his consumption, and the producer pays for reductions in both. The volatility channel is what makes the problem new: the classical Holmström–Milgrom model (Econometrica 1987) controls only the drift. The paper uses the general reduction of Cvitanić, Possamaï and Touzi (Finance Stoch. 2018) to optimal contracts with volatility control, and obtains the producer's value in closed form up to a scalar minimisation. This mission formalizes that closed form.

Setting

Fix integers $N,d\ge0$ , cost parameters $\mu\in(0,\infty)^N$ and $\lambda\in(0,\infty)^d$ , nominal volatilities $\sigma\in(0,\infty)^d$ , effort bounds $A_{\max}>0$ and $\varepsilon\in(0,1]$ , risk aversions $r,p>0$ , a marginal cost of volatility $h>0$ , marginal energy value $\kappa$ and cost $\theta$ with $\delta:=\kappa-\theta$ , a horizon $T>0$ , an initial consumption $X_0$ and a reservation utility $R_0<0$ . Write $\bar\mu:=\sum_i\mu_i$ and $x^-:=\max(0,-x)$ .

Consumption. $X$ is the canonical process on $\Omega=C([0,T],\mathbb R)$ with its natural filtration $\mathbb F$ . A control $\nu=(\alpha,\beta)$ is progressively measurable, with $\alpha_t\in A:=\prod_i[0,\mu_iA_{\max}]$ (effort to reduce consumption) and $\beta_t\in B:=[\varepsilon,1]^d$ (effort to reduce volatility). Under $\nu$ the consumption follows, in the weak sense,

X_t=X_0-\int_0^t\alpha_s\cdot\mathbf 1\,ds+\int_0^t\sigma(\beta_s)\cdot dW_s,\qquad |\sigma(b)|^2=\sum_j\sigma_j^2b_j .

Effort costs $c(\nu)=c_1(\alpha)+\frac12c_2(\beta)$ per unit time, with $c_1(a)=\frac12\sum_ia_i^2/\mu_i$ and $c_2(b)=\sum_j\frac{\sigma_j^2}{\lambda_j}(b_j^{-1}-1)$ .

Criteria. For a payment $\xi$ at time $T$ , the consumer's criterion is $J_A=\mathbb E[-e^{-r(\xi+\int_0^T(\kappa X_s-c(\nu_s))ds)}]$ and the producer's is $J_P=\mathbb E[U(-\xi-\int_0^T\theta X_sds-\frac h2\langle X\rangle_T)]$ with $U(x)=-e^{-px}$ . Contracts $\mathcal C$ are the $\mathcal F_T$ -measurable $\xi$ with exponential moments of order $m>1$ uniformly over the consumer's responses (2.5). The consumer's value is $V_A(\xi)=\sup J_A$ , and $\mathcal P^\star(\xi)$ is the set of his optimal responses.

Second best. The producer offers $\xi$ , the consumer responds optimally, ties are broken in the producer's favour, and participation requires $V_A(\xi)\ge R_0$ :

V^{SB}:=\sup_{\xi\in\mathcal C,\ V_A(\xi)\ge R_0}\ \sup_{\mathcal P^\star(\xi)}J_P(\xi,\cdot),\qquad\sup\emptyset=-\infty .

Hamiltonians. $H_m(z)=-\inf_{a\in A}\{a\cdot\mathbf 1\,z+c_1(a)\}$ and $H_v(\gamma)=-\frac12\inf_{b\in B}\{c_2(b)-\gamma|\sigma(b)|^2\}$ .

Formalization targets

Goal: Proposition 3.2 (i)

Assume $\delta^-T\le A_{\max}$ . With $q_t(z)=h+rz^2+p(z-\delta(T-t))^2$ , $L_0=-\frac1r\log(-R_0)$ ,

m_{SB}(t)=\frac12\bar\mu\delta^2(T-t)^2-\frac12\inf_{z\in\mathbb R}\Big\{\bar\mu\big(z^-+\delta(T-t)\big)^2-2H_v\big(-q_t(z)\big)\Big\},

V^{SB}=U\big(v(0,X_0)-L_0\big),\qquad v(0,X_0)=\delta TX_0+\int_0^Tm_{SB}(s)\,ds .

Milestones

Proposition 2.1. The consumer's best responses $\hat a_i(z)=\mu_i(z^-\wedge A_{\max})$ and $\hat b_j(\gamma)=(1\wedge(\lambda_j\gamma^-)^{-1/2})\vee\varepsilon$ attain the infima defining $H_m$ and $H_v$ , and

H_m(z)=\bar\mu\big(m z^--\tfrac{m^2}2\big),\ m=z^-\wedge A_{\max};\qquad H_v(\gamma)=-\tfrac12\big(\hat c_2(\gamma)-\gamma|\hat\sigma(\gamma)|^2\big).

Lemma A.1. With $f_0(q,\gamma)=q|\hat\sigma(\gamma)|^2+\hat c_2(\gamma)$ , $F_0(q):=\inf_{\gamma\le0}f_0(q,\gamma)=f_0(q,-q)=-2H_v(-q)$ , and $F_0$ is non-decreasing.
Proposition A.4 (ii). A minimiser of $z\mapsto F_0(h-k+rz^2+p(z-y)^2)+\bar\mu(z^-+y)^2$ is $\frac p{r+p}y$ when $y\ge0$ , and lies in $[y,\frac p{r+p}y]$ when $y\le0$ .

A companion statement, Corollary 3.1 (i), gives the explicit off-peak payment rates $z_{SB}(t)=\frac p{r+p}\delta(T-t)$ and $\gamma_{SB}(t)=-h-\frac{rp}{r+p}\delta^2(T-t)^2$ when $\delta\ge0$ .

Significance

The closed form reduces an infinite-dimensional contracting problem, a supremum over all path-dependent payments and all consumer responses, to a deterministic one-dimensional minimisation at each time. It is the basis of the paper's comparisons: with the first-best value it measures the cost of moral hazard, and its minimiser gives the price of energy and of responsiveness that the optimal contract charges, which the paper calibrates on Low Carbon London data.

The result is proved on paper. No part of it is machine-checked. A complete formalization would give a checked instance of a continuous-time principal–agent theorem with volatility control. It would also fix, in exact terms, the conventions the paper leaves implicit (weak solutions, the effort cap), and the printed misprints that this mission corrects.

Difficulty

The deterministic milestones are calculus on boxes. The goal is not. The upper bound $V^{SB}\le U(v(0,X_0)-L_0)$ must hold for every $\mathcal F_T$ -measurable contract, not only for contracts of a convenient form. The step that fails in a direct attempt is the representation of an arbitrary contract: one needs that every $\xi\in\mathcal C$ inducing an optimal response can be written as $Y_T^{y_0,Z,\Gamma}$ , an integral against $dX$ and $d\langle X\rangle$ driven by the consumer's continuation certainty equivalent. This is the main theorem of Cvitanić–Possamaï–Touzi (2018) and rests on second-order backward SDEs; it has no counterpart in Mathlib. Restricting the supremum to linear or representable contracts at the outset would assume exactly that theorem. The lower bound needs, for the candidate contract, existence of the consumer's optimal response as a weak solution and a verification argument for the producer's HJB equation.

Formalization scope

All objects live in the namespace DemandResponse.SecondBest, and all hypotheses are fields of a structure Params. Conventions:

Weak formulation. An admissible pair $(\nu,\mathbb P)$ is a control and a probability measure on $C([0,T],\mathbb R)$ with $X_0=X_0$ a.s., under which $X_t-X_0+\int_0^t\alpha_s\cdot\mathbf 1\,ds$ and its square minus $\int_0^t|\sigma(\beta_s)|^2ds$ are $\mathbb F$ -martingales. This is the martingale problem equivalent to weak solutions of (2.1); the paper deliberately leaves weak solutions informal (footnote 2). The pair, not the law alone, is the admissible object, because the cost depends on $\nu$ .
Quadratic variation. $\langle X\rangle_T$ in $J_P$ is its almost-sure value $\int_0^T|\sigma(\beta_s)|^2ds$ .
Values. Expected utilities are negated lower Lebesgue integrals, in $[-\infty,0]$ ; all suprema are in the extended reals, so the empty supremum is $-\infty$ , as on p. 9.
Hamiltonians are defined by their infima, not by the closed forms of Proposition 2.1.
Indices are Fin N, Fin d; $N=0$ , $d=0$ are allowed. $\hat b_j(\gamma)=1$ when $\lambda_j\gamma^-\le1$ (the paper's $0^{-1/2}=+\infty$ ).
Added hypotheses. $\varepsilon\le1$ ( $B\neq\emptyset$ ), $R_0<0$ ( $\log(-R_0)$ defined), and for the goal $\delta^-T\le A_{\max}$ . The paper's closed form is computed with the effort cap removed (" $\eta_A\to0$ as $A\nearrow\infty$ ", p. 30), and with the capped effort of the model it is correct exactly under this hypothesis.
Corrected misprints. $-2H_m(-q(z))$ in $m_{SB}$ is read as $-2H_v(-q(z))$ ; with $H_m$ the infimum is $-\infty$ . The printed $H_m(z)=\frac12\bar\mu(z^-\wedge A_{\max})^2$ is false for $z^->A_{\max}$ and is corrected. " $j=1,\dots,N$ " for $\hat b$ means $j=1,\dots,d$ . In Proposition A.4 (ii) the open interval becomes closed, and "for large $A$ " is read as $\eta_A\equiv0$ .

The goal is an equality of extended reals between $V^{SB}$ , defined from the model, and an explicit real number. A formalization that defines $V^{SB}$ over a restricted class of contracts, or with a real-valued supremum that returns $0$ on unbounded sets, would trivialize or change it and is not the goal.

Needed infrastructure: continuous-time martingales on the canonical path space (Mathlib has Martingale and progressive measurability), existence of weak solutions with bounded coefficients, a representation theorem for contracts (Cvitanić–Possamaï–Touzi), and a verification theorem for the producer's HJB equation. The weak-formulation layer and the contract representation are reusable for any continuous-time principal–agent model with drift and volatility control. Contributions of any of these pieces, and proofs of the deterministic milestones, are welcome.

Selected references

R. Aïd, D. Possamaï, N. Touzi, Optimal Electricity Demand Response Contracting with Responsiveness Incentives, arXiv:1810.09063v3, 2019; Mathematics of Operations Research 47 (2022). https://arxiv.org/abs/1810.09063v3
J. Cvitanić, D. Possamaï, N. Touzi, Dynamic programming approach to principal–agent problems, Finance and Stochastics 22 (2018) 1–37. https://doi.org/10.1007/s00780-017-0344-4
B. Holmström, P. Milgrom, Aggregation and Linearity in the Provision of Intertemporal Incentives, Econometrica 55 (1987) 303–328. https://doi.org/10.2307/1913238
Y. Sannikov, A Continuous-Time Version of the Principal–Agent Problem, Review of Economic Studies 75 (2008) 957–984. https://doi.org/10.1111/j.1467-937X.2008.00486.x
I. Karatzas, S. Shreve, Brownian Motion and Stochastic Calculus, 2nd ed., Springer 1991, §5.4 (martingale problem and weak solutions). https://doi.org/10.1007/978-1-4612-0949-2

7 thms2 active usersReviewed

Completed

Dynamic Programming Linear algebra Markov Chain+2·Captain: mikedeng1

Bellman's Dynamic Programming IX: Markovian Decision Processes and the Maximal Perron RootTextbook

Motivation

Chapter XI of Richard Bellman's Dynamic Programming (Princeton University Press, 1957; DOI 10.2307/j.ctv1nxcw0f) studies decision processes whose state is a vector of nonnegative quantities, for example the probabilities that a system is in each of $N$ states, or the stocks of $N$ commodities, and whose transitions are linear maps chosen stage by stage by a controller. Maximizing a linear functional of the state at every stage leads to the nonlinear difference equation

x_i(n+1) = \max_q \sum_{j=1}^N a_{ij}(q)\, x_j(n), \qquad x_i(0) = c_i,

and, in the limit of small time steps, to differential equations of the form $dx/dt = \max_q [A(q,t)x + b(q,t)]$ and, when two opposing controllers act, $dx/dt = \max_p \min_q[\dots]$ .

These equations are the multiplicative counterpart of the additive Bellman equation. Their growth rate is the natural object for controlled population models, controlled Markov chains observed through their unnormalized state vectors, and economic growth models with a choice of technology. Bellman announced the discrete results in "A Markovian decision process" (J. Math. Mech. 6, 1957) the same year as the book, and R. A. Howard's Dynamic Programming and Markov Processes (MIT Press, 1960) developed policy iteration for the related average-reward problem. The central discrete result of the chapter, Theorem 2, is an early instance of what is now called nonlinear Perron–Frobenius theory (Lemmens and Nussbaum, 2012).

Setting

Fix $N \ge 1$ . Row $i$ of the matrix carries its own control $q_i$ , ranging over a set $S_i$ ; the joint control is $q = (q_1, \dots, q_N)$ in $S = S_1 \times \dots \times S_N$ , and $A(q) = (a_{ij}(q_i))$ . Bellman insists on this row-wise structure (§ 3): "the set of q's for each row is distinct from the corresponding set for any other row ... so that there is no interaction between the various maximizations". The maximum of a vector over $q$ is then taken row by row.

The Perron root $\varphi(q)$ is the characteristic root of $A(q)$ of largest absolute value, the spectral radius of $A(q)$ as a complex matrix. The conditions (10.3) of the chapter are:

for every $y$ and every row the maximum of $\sum_j a_{ij}(q_i) y_j$ over $S_i$ is attained;
$0 < a_{ij}(q) \le m < \infty$ on $S$ ;
$\varphi$ attains its maximum on $S$ .

For the continuous processes, $\|x\| = \sum_i |x_i|$ and $\|A\| = \sum_{i,j}|a_{ij}|$ , and a solution of $dx/dt = F(t,x)$ , $x(0)=c$ , on $[0,T]$ is a continuous $x$ with $x(t) = c + \int_0^t F(s, x(s))\,ds$ , which is the book's "satisfying the equation almost everywhere". The successive approximations are $x_0 = c$ , $x_{n+1}(t) = c + \int_0^t F(s, x_n(s))\,ds$ .

Formalization targets

Goal: Chapter XI, Theorem 2

Under (10.3) there is exactly one $\lambda > 0$ for which

\lambda y_i = \max_q \sum_{j=1}^N a_{ij}(q)\, y_j, \qquad i = 1,\dots,N,

has a solution with all $y_i > 0$ . That solution is unique up to a positive factor, and

\lambda = \max_{q \in S} \varphi(q).

Milestones

§ 4, Lemma. For row-wise maximized operators $T_1(x) = \max_q[b_1(q,t) + \int_0^t A(q,s)x\,ds]$ and $T_2(y)$ likewise, $\|T_1(x) - T_2(y)\| \le \max_q[\|b_1 - b_2\| + \int_0^t \|A(q,s)\|\,\|x-y\|\,ds]$ .
Theorem 1. If $\|A(q,t)\|, \|b(q,t)\| \le f(t)$ with $f$ locally integrable and the maximum is attained, then $dx/dt = \max_q[A(q,t)x + b(q,t)]$ , $x(0) = c$ , has a unique solution, the uniform limit of the successive approximations.
Theorem 3 (corrected). If moreover $\varphi$ has a unique maximizer on $S$ and $c \ge 0$ , $c \ne 0$ , then the recurrence satisfies $x_i(n) \sim a\,y_i\,\lambda^n$ with $a = a(c) > 0$ .
Theorem 4. The same well-posedness for $dx/dt = \max_p\min_q[A(p,q,t)x + b(p,q,t)] = \min_q\max_p[\dots]$ on $[0,T]$ .
Theorem 5. If $(Bp,q) \ge d > 0$ on probability vectors, the solution of $du/dt = \max_p\min_q[(Ap,q) - (Bp,q)u]$ satisfies

\lim_{t\to\infty} u(t) = \max_p \min_q \frac{(Ap,q)}{(Bp,q)} = \min_q \max_p \frac{(Ap,q)}{(Bp,q)} .

Significance

Theorem 2 identifies the optimal long-run growth rate of a controlled multiplicative process with the largest Perron root among the admissible matrices, and shows that the optimal process has a single positive stationary direction. Theorem 3 turns this into the asymptotics of the value iteration $x(n+1) = \max_q A(q)x(n)$ : after normalization by $\lambda^n$ the iterates converge to a multiple of the eigenvector. Theorems 1 and 4 are the existence and uniqueness results that justify defining continuous-time controlled processes and differential games by these equations. Theorem 5 recovers the min-max theorem for ratios of bilinear forms (Chapter X) as the long-run limit of a scalar differential game.

The results are classical, and none of them is formalized. Mathlib has the spectral radius and irreducible matrices but no Perron–Frobenius theorem and no Brouwer fixed point theorem; the platform has a statement of the Perron theorem for a single positive matrix (ClassicalGaps.perron_positive_matrix). A formal proof of the goal therefore also produces a reusable monotone, positively homogeneous eigenvector theorem on the positive orthant.

Difficulty

The map $y \mapsto \max_q A(q)y$ is not linear, so the linear-algebra proof of the Perron theorem through the characteristic polynomial does not apply. Existence of a positive eigenvector needs a fixed point argument for a nonlinear map of the simplex (Bellman uses Brouwer's theorem). The identification $\lambda = \max_q \varphi(q)$ must connect the nonlinear eigenvalue with the spectra of the individual matrices, which requires the Perron theory of each $A(q)$ , including the fact that the Perron root dominates every complex eigenvalue in modulus. For Theorem 3, the iterates may switch controls infinitely often when $S$ is infinite, so an argument that the optimal control is eventually constant does not settle convergence. For Theorems 1 and 4, the right-hand side is only measurable in $t$ and Lipschitz in $x$ with an integrable constant, so the classical Picard–Lindelöf theorem with a continuous right-hand side does not apply directly.

Formalization scope

Everything lives in the namespace BellmanDP.Markovian. Vectors are Fin N → ℝ and matrices are Matrix (Fin N) (Fin N) ℝ. Row $i$ 's control type is Q i with admissible set S i, and the joint admissible set is Set.pi Set.univ S. The Perron root is (spectralRadius ℂ (A.map (algebraMap ℝ ℂ))).toReal, the largest modulus of a complex eigenvalue; it is not defined as a positive eigenvalue with a positive eigenvector, which would make the Perron–Frobenius content of the goal definitional. The maximized eigen-equation is stated with IsGreatest, so the maxima are attained. The goal and Theorem 3 assume $N \ge 1$ ; for $N = 0$ every $\lambda$ would qualify.

Conventions and repairs:

Theorem 3 prints "a unique q for which the maximum value of q is assumed". A control has no maximum value; the proof uses " $q^*$ ... the value of $q$ for which $\lambda = \varphi(q^*)$ ", so the hypothesis is uniqueness of the maximizer of $\varphi$ . For $c = 0$ the iterates vanish and $x_i(n) \sim a y_i\lambda^n$ fails, so $c \ne 0$ is assumed (the proof takes $c > 0$ "without loss of generality"). The asymptotic is stated as $x_i(n)/\lambda^n \to a y_i$ with $a > 0$ .
Theorems 1 and 4: the book's controls are functions of $t$ with the maximum outside the integral; since the maximization is pointwise (§ 4), the statements use pointwise sets and the integral of the pointwise maximum. Measurability of $t \mapsto F(t,x)$ is not stated in the book and is assumed. In Theorem 4 the max-min is taken row by row, and (2a) is encoded as the existence of a saddle point in each row.
§ 4 Lemma: " $\le \max_q[\dots]$ " is stated as " $\le [\dots]$ at some admissible joint $q$ ".
Theorem 5: the right-hand side is the max-min form; the equality of the two ratio values is part of the conclusion.

Degenerate readings are ruled out: the maxima are attained or taken over nonempty compact sets, never Lean's junk sSup of an unbounded set, and the Perron root is spectral rather than defined through the conclusion. Contributions welcome: a proof of the single-matrix Perron theorem in the form needed here, a Brouwer or Kakutani fixed point theorem for the simplex, and a Carathéodory existence theorem for $dx/dt = F(t,x)$ with an integrable Lipschitz constant, each reusable well beyond this mission.

Selected references

R. Bellman, Dynamic Programming, Princeton University Press, 1957; Princeton Landmarks in Mathematics ed., 2010, Chapter XI. https://doi.org/10.2307/j.ctv1nxcw0f
R. Bellman, "A Markovian decision process", Journal of Mathematics and Mechanics 6 (1957), 679–684.
R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
O. Perron, "Zur Theorie der Matrices", Mathematische Annalen 64 (1907), 248–263. https://doi.org/10.1007/BF01449896
B. Lemmens and R. Nussbaum, Nonlinear Perron–Frobenius Theory, Cambridge University Press, 2012. https://doi.org/10.1017/CBO9781139026079

9 thms2 active usersReviewed

Calculus of Variations Dynamic Programming Numerical Analysis+2·Captain: mikedeng1

Bellman's Dynamic Programming VII: Convergence of Discrete Approximations in the Calculus of VariationsTextbook

Motivation

Chapter IX of Richard Bellman's Dynamic Programming (Princeton University Press, 1957; Princeton Landmarks edition 2010, DOI 10.2307/j.ctv1nxcw0f) recasts problems of the calculus of variations with constraints as dynamic programming processes. A variational problem with an inequality constraint on the control, such as $0 \le y \le x$ , is awkward for the classical Euler–Lagrange theory: the optimal control switches between the constraint boundary and the interior, and the number and location of the switches are unknown in advance. Bellman's proposal is to replace the continuous problem by a discrete-time one and to solve that by the recurrence relations of dynamic programming, a procedure he describes as the more reliable computational one "in cases treated to date" (§ 11, p. 260).

That proposal is sound only if the discrete values converge to the continuous value as the time step goes to zero. Chapter IX states one such convergence result, Theorem 2 of § 12, and proves it through an Euler-scheme error estimate. The same chapter works through an example (§§ 10–11) whose discrete version is described by Theorem 1. Both are the subject of this mission. The convergence of time-discretized dynamic programming to the continuous value function has since become a standard topic of numerical optimal control (for example the semi-Lagrangian schemes analysed by Capuzzo-Dolcetta and Falcone), and Bellman's § 12 is an early rigorous instance of it.

Setting

A state $x(t) \ge 0$ evolves on a horizon $[0, T]$ under a control $y(t)$ with $0 \le y \le x$ , a running reward $F(x, y)$ and dynamics

\frac{dx}{dt} = G(x, y), \qquad x(0) = c .

Writing $y = \varphi x$ with a fractional control $0 \le \varphi \le 1$ turns $F$ and $G$ into $\tilde F(x, \varphi) = F(x, \varphi x)$ and $\tilde G(x, \varphi) = G(x, \varphi x)$ (phiForm). The continuous value is

f(c, T) = \sup_{\varphi} \int_0^T \tilde F(x(t), \varphi(t))\, dt,

over measurable $\varphi$ with values in $[0, 1]$ , where $x$ solves $x(t) = c + \int_0^t \tilde G(x(s), \varphi(s))\,ds$ on $[0, T]$ (IsTrajectory, contValue).

For $n = 1, 2, \dots$ the discrete problem uses step $1/n$ and $N = \lfloor Tn \rfloor$ steps (horizonSteps): for $\varphi_0, \dots, \varphi_N \in [0, 1]$ ,

x_0 = c, \quad x_{k+1} = x_k + \frac{\tilde G(x_k, \varphi_k)}{n}, \qquad J_N(\{\varphi_k\}, n) = \sum_{k=0}^{N} \frac{\tilde F(x_k, \varphi_k)}{n},

and $f(c, T, n) = \max J_N$ (eulerTraj, discretePayoff, discreteValue). A discrete control defines the step control $\varphi(t) = \varphi_k$ on $k/n \le t < (k+1)/n$ (stepControl).

The example of §§ 10–11 has a gain function $b$ with $b(0) = 0$ , $b'(0) = \infty$ , $b' > 0$ , $b'(y) \to 0$ as $y \to \infty$ , $b'' < 0$ (IsGainFunction; $b(y) = y^{1/2}$ is one), and value functions (uSeq)

u_0(c) = c, \qquad u_{N+1}(c) = \max_{0 \le v \le c}\,\bigl[c - v + u_N(c + b(v))\bigr].

Formalization targets

Goal: Chapter IX, Theorem 2 (corrected)

Assume (11): (a) $F$ and $G$ have continuous second partial derivatives; (b) $px \le G(x, y) \le qx + r$ for $x > 0$ , $0 \le y \le x$ ; (c) $G_y > 0$ throughout that region, or $G_y < 0$ throughout. Then for all $c \ge 0$ , $T > 0$ , the set of continuous payoffs is nonempty and bounded above, and

\lim_{n \to \infty} f(c, T, n) = f(c, T).

Milestones

Chapter IX, Theorem 1: the structure of $u_N$ . There are $v_N(c)$ and thresholds $c_N$ with $v_N$ decreasing in $c$ , $v_{N+1} > v_N$ , $c_N$ the unique fixed point of $v_N$ with $c_{N+1} > c_N$ , $u_N(c) = u_{N-1}(c + b(c))$ for $c \le c_N$ , $u_N(c) = c - v_N(c) + u_{N-1}(c + b(v_N(c)))$ for $c \ge c_N$ , and $u_N' \ge u_{N-1}'$ .
§ 12, Lemma (corrected): for $G$ Lipschitz on $[m, M] \times [0, 1]$ , the Euler states with a step control are within $\kappa / n$ of the exact solution on $[0, T]$ .
Eq. (12.13): $|J(\varphi) - J_N(\{\varphi_k\}, n)| \le B'/n$ for step controls.
Eq. (12.14): $f(c, T, n) \le f(c, T) + B'/n$ for all $n \ge 1$ .
Eq. (12.17): $f(c, T) \le \liminf_{n \to \infty} f(c, T, n)$ .

Milestones 3–5 are stated for $c > 0$ , as in the book's proof ("Given $c > 0$ and $T > 0$ "); the goal is stated for $c \ge 0$ , as in the theorem.

Significance

Theorem 2 says that the value of a constrained continuous-time control problem can be computed, to any accuracy, by the finite recurrence of dynamic programming on a time grid. Its upper half (12.14) gives a rate: the discrete value never exceeds the continuous one by more than $B'/n$ . The lower half (12.17) needs no rate and holds because measurable controls are approximated by step controls. Theorem 1 is a discrete counterpart of the transition curve computed in § 10: below the threshold $c_N$ the whole state is invested, above it an interior amount, and the thresholds increase with the number of remaining stages.

As far as the mission's author could establish, none of these results has a machine-checked proof. The Euler error estimate is classical and has a Gronwall-type proof; Mathlib contains Gronwall's inequality (Analysis/ODE/Gronwall) and Picard–Lindelöf for continuous right-hand sides, but no convergence theory for the value of discretized control problems. The book leaves the proof of Theorem 1 to the reader.

Difficulty

The upper bound (12.14) follows from the Lemma once the continuous and the discrete trajectories are known to stay in a common bounded strip $m \le x \le M$ ; that uniform bound is what assumption (11b) provides and must be established first. The lower bound is where the obvious argument fails: an arbitrary measurable control is not a step control on the grid $k/n$ , and passing to a step control changes the trajectory, so the payoff must be shown continuous under almost-everywhere convergence of controls. This uses the trajectory's dependence on the control in $L^1$ , not only on the initial value. Solutions exist in the Carathéodory sense only, so the integral form of the equation is required. For Theorem 1 the induction must carry concavity of $u_N$ and a strict comparison of marginal values across $N$ , and $u_N$ is not differentiable at $c = 0$ , where $b'(0) = \infty$ .

Formalization scope

States, controls and rewards are real; $F, G, b : \mathbb R \to \mathbb R$ (or $\mathbb R \to \mathbb R \to \mathbb R$ ), with the hypotheses imposed where the book imposes them. The conventions:

Misprint in (12.5). The print sets $N = [T/n]$ while using the step $1/n$ in (12.6) and the intervals $k/n \le t < (k+1)/n$ in the Lemma. Under the literal reading the discrete horizon $N/n$ tends to $0$ and Theorem 2 is false: for $F \equiv 1$ , $G(x, y) = y$ (which satisfies (11) with $p = 0$ , $q = 1$ , $r = 0$ , $G_y = 1$ ) and $T = 1$ , $f(c, 1) = 1$ but $f(c, 1, n) = 1/n$ for $n \ge 2$ . The mission uses $N = \lfloor Tn \rfloor$ and keeps the book's sum $\sum_{k=0}^{N}$ ; the range " $k = 0, \dots, n - 1$ " in (12.6) is read as $k = 0, \dots, N - 1$ .
Lemma. Its range " $0 \le t \le N$ " is read as $0 \le t \le T$ . The bounds $m \le x \le M$ are required of the solution $x(t)$ as well as of the sequence $x_k$ , since a Lipschitz condition on the strip says nothing about $G$ outside it; the proof of Theorem 2 supplies both bounds. The constant may depend on $m$ , $M$ and the Lipschitz constant.
Assumptions (11) are on the original $F(x, y)$ , $G(x, y)$ , with (11a) read as $C^2$ on $\mathbb R^2$ ; the problem is posed through $y = \varphi x$ .
"Max" over measurable controls is a supremum (the proof picks $\varepsilon$ -optimal controls). The goal asserts that the set of payoffs is nonempty and bounded above, so the Lean supremum cannot take its default value $0$ . Trajectories satisfy the integral equation with integrable right-hand side, and the reward is required integrable, so the Bochner integral's default $0$ cannot enter either.
Theorem 1. (5a) is read as non-strict monotonicity: for $N = 1$ the interior optimum solves $b'(v) = 1$ and is constant in $c$ . $v_N(c) \ge 0$ is required for $c \ge c_N$ , so that $v_N(c)$ is a feasible choice. (5f) presupposes differentiability and is stated where both derivatives exist.

A trivializing formalization is ruled out: the discrete and continuous values are defined from $F$ and $G$ by the book's recursions and integrals, not assumed as hypotheses, and the corrected step count is not a free parameter.

Needed infrastructure: Carathéodory existence and uniqueness for Lipschitz right-hand sides with measurable controls, Gronwall estimates for the Euler scheme, and approximation of measurable controls by step functions. All three are reusable beyond this mission, and contributions of any of them are welcome.

Selected references

R. Bellman, Dynamic Programming, Princeton University Press, 1957; Princeton Landmarks in Mathematics edition, 2010. Chapter IX, §§ 10–12, pp. 256–263. DOI 10.2307/j.ctv1nxcw0f
I. Capuzzo-Dolcetta, On a discrete approximation of the Hamilton–Jacobi equation of dynamic programming, Applied Mathematics and Optimization 10 (1983) 367–377. DOI 10.1007/BF01448394
M. Bardi and I. Capuzzo-Dolcetta, Optimal Control and Viscosity Solutions of Hamilton–Jacobi–Bellman Equations, Birkhäuser, 1997. DOI 10.1007/978-0-8176-4755-1

8 thms2 active usersReviewed

Completed

Dynamic Programming Operations Research Optimization+1·Captain: mikedeng1

Bellman's Dynamic Programming VI: Optimal Policies for the Continuous Gold-Mining ProcessTextbook

Motivation

Chapter II of Richard Bellman's Dynamic Programming (Princeton University Press, 1957) solves a discrete gold-mining process: a single machine can be used in one of two mines, each use extracts a fixed fraction of the gold remaining in that mine, and each use carries a fixed risk of destroying the machine. Maximizing the expected total gold leads to an index rule: work the mine whose ratio of expected yield to risk is larger. Chapter VIII, A Continuous Stochastic Decision Process, passes to continuous time. Decisions are taken at every instant, and effort may be divided between the mines. The optimal policy is characterized by first-order conditions on switching functions, the objects of Pontryagin's later maximum principle.

It is also an early continuous-time index policy of the kind later central to bandit theory. Chapter VIII treats two mines, then a third decision that works both mines at once.

Setting

Mine A holds $x_0 \ge 0$ units of gold and mine B holds $y_0 \ge 0$ . At time $t$ a proportion $\varphi_1(t) \in [0,1]$ of the machine's effort goes to A and $\varphi_2(t) = 1 - \varphi_1(t)$ to B (Eq. (7.3)). With $x(t), y(t)$ the gold remaining, $p(t)$ the probability that the machine still works and $f(t)$ the expected gold mined, the process is defined by Eq. (7.2):

\frac{dx}{dt} = -\varphi_1 r_1 x,\qquad \frac{dy}{dt} = -\varphi_2 r_2 y,\qquad \frac{dp}{dt} = -p\,(\varphi_1 q_1 + \varphi_2 q_2),\qquad \frac{df}{dt} = p\,(\varphi_1 r_1 x + \varphi_2 r_2 y),

with $x(0) = x_0$ , $y(0) = y_0$ , $p(0) = 1$ , $f(0) = 0$ . The mining rates $r_1, r_2$ and the failure rates $q_1, q_2$ are positive. The objective is the expected total gold $f(\infty) = \int_0^\infty f'(t)\,dt$ .

In the three-choice problem (§ 12) a third decision $C$ removes gold from A at rate $r_3$ and from B at rate $r_4$ , and fails at rate $q_3$ . A control is a triple $\varphi_1, \varphi_2, \varphi_3 \ge 0$ with $\varphi_1 + \varphi_2 + \varphi_3 = 1$ (Eq. (12.2)). For a horizon $T$ , the switching functions $K_1, K_2, K_3$ of Eq. (12.5) are computed along a control. For instance,

K_1(t) = -q_1\int_t^T f'(s)\,ds + r_1\,p(T)\,x(T) - r_1\int_t^T p'(s)\,x(s)\,ds.

They measure the first-order gain from shifting effort towards each decision at time $t$ . The linear forms

C_1 = q_1 r_2 y - q_2 r_1 x,\qquad C_2 = q_1 r_4 y - (q_3 r_1 - q_1 r_3)x,\qquad C_3 = (q_3 r_2 - q_2 r_4) y - q_2 r_3 x

and the quantity $D = q_1 r_2 r_3 + q_2 r_1 r_4 - q_3 r_1 r_2$ (Eqs. (13.2)–(13.3)) organize the analysis.

Formalization targets

Goal: Chapter VIII, Theorem 1

For the two-choice process, the maximum of $f(\infty)$ is attained by the policy

\varphi_1 = 1 \text{ for } q_1 r_2 y < q_2 r_1 x,\qquad \varphi_2 = 1 \text{ for } q_1 r_2 y > q_2 r_1 x,\qquad \varphi_1 = \tfrac{r_2}{r_1+r_2},\ \varphi_2 = \tfrac{r_1}{r_1+r_2} \text{ for } q_1 r_2 y = q_2 r_1 x.

The formal statement asserts that some admissible control follows this rule along its own trajectory, and that every such control maximizes $f(\infty)$ over all measurable controls with values in $[0,1]$ .

Milestones

Eq. (10.1): $f_A(\infty) = r_1 x_0/(q_1 + r_1)$ and $f_B(\infty) = r_2 y_0/(q_2 + r_2)$ for the pure policies.
Lemmas 1–3 (§ 13): for a control that maximizes $f(T)$ , almost everywhere, $K_i > K_j$ forces $\varphi_i = 1$ or $\varphi_j = 0$ ; a strictly largest $K_i$ forces $\varphi_i = 1$ ; a strictly beaten $K_i$ forces $\varphi_i = 0$ .
Lemma 4 (§ 14): if $C_2 = 0$ and $C_3 = 0$ lie in the positive quadrant and $D \ne 0$ , no optimal control mixes $A$ , $B$ and $C$ on an interval.
Lemma 5 (§ 14): a mixture of exactly two decisions on an interval keeps the state on $C_1 = 0$ , $C_2 = 0$ or $C_3 = 0$ respectively, with the proportions that hold $y/x$ fixed.
§ 15, Eq. (1) (corrected): $f_C(\infty) = r_3 x_0/(q_3 + r_3) + r_4 y_0/(q_3 + r_4)$ .
"Theorem 8" (§ 16, the chapter's third theorem): if $D < 0$ (with $r_3 > r_4$ and $x_0, y_0 > 0$ ), the three-choice problem is solved by the two-choice rule of Theorem 1, and every optimal control has $\varphi_3 = 0$ almost everywhere.

Significance

Theorem 1 gives a closed-form optimal feedback policy for a continuous-time stochastic scheduling problem. The policy depends only on the slope $y/x$ , and on the line $q_1 r_2 y = q_2 r_1 x$ it is a mixed (chattering) policy: the discrete optimum becomes a mixture in the continuous limit. Lemmas 1–5 are a hand-made maximum principle for controls that enter linearly, read almost everywhere. "Theorem 8" says exactly when a composite decision is useless: $D < 0$ means that $C$ removes gold at a higher failure cost than an equivalent mixture of $A$ and $B$ .

On the formal side, none of these results is formalized anywhere. Mathlib has no theory of controlled differential equations or of necessary conditions for optimal control. The platform's maximum principles (BertsekasDP.pontryagin_minimum_principle, VectorSpaceOpt.pontryagin_minimum_principle) assume smooth dynamics and a finite horizon with differentiable costs. They do not cover this process, with measurable controls and an improper-integral objective. A formal proof of Theorem 1 would be a complete optimality proof for a continuous-time index policy with chattering controls. The book's argument for Theorem 1 is partly informal; a complete proof, by that route or another, is the target.

Difficulty

The optimization is over an infinite-dimensional set of measurable controls on an infinite horizon, and the objective is not concave in the control. The first-order conditions of §§ 8–9 are necessary, not sufficient, so they do not by themselves prove that the rule is optimal. The book's argument combines them with qualitative facts (the rule is used thereafter once used above the line, and $B$ is preferred near the $y$ -axis). Making this rigorous requires comparing an arbitrary control with the rule, not just perturbing near an optimum. It is also not known in advance that an optimal control exists, so arguments of the form "let $\varphi$ be optimal" need an existence step or a direct comparison. For the lemmas, the switching functions must be shown absolutely continuous, with the derivative formulas (13.1) holding almost everywhere, before "equal on an interval" can be turned into " $C_k = 0$ on the interval".

Formalization scope

Process by closed forms. No differential equations are formalized. With $\Phi_i(t) = \int_0^t \varphi_i$ , the definitions are $x = x_0 e^{-r_1\Phi_1 - r_3\Phi_3}$ , $y = y_0 e^{-r_2\Phi_2 - r_4\Phi_3}$ , $p = e^{-\sum_i q_i\Phi_i}$ , $f(T) = \int_0^T f'$ . These are the unique absolutely continuous solutions of (7.2) and (12.1). The two-choice process is the three-choice one with $\varphi_3 = 0$ .
Controls are open-loop and measurable, with $\varphi_i \ge 0$ and $\sum_i \varphi_i = 1$ . Decisions are indexed 0, 1, 2 for $A, B, C$ .
$f(\infty)$ is a lower Lebesgue integral with values in $[0,\infty]$ . It has no junk value, and optimality is compared in $[0,\infty]$ .
Theorem 1's feedback rule is encoded as a predicate on open-loop controls: the rule holds along the control's own trajectory for almost every $t \ge 0$ . The goal also asserts that such a control exists, which rules out the trivializing reading in which no control satisfies the rule and the optimality claim is vacuous.
Horizon of Lemmas 1–5. § 12 considers only $T = \infty$ , but the variation (12.4) and the switching functions (12.5) are written for a general $T$ . Each lemma is formalized for both: every finite horizon $T$ , with $K_i$ built from that horizon, and $T = \infty$ , with $K_i$ given by (12.5) at $T = \infty$ (boundary term $0$ ).
Implicit ranges. All rates $q_1, q_2, q_3, r_1, \dots, r_4$ are taken positive, and $x_0, y_0 \ge 0$ . Lemmas 4–5 and "Theorem 8" take $x_0, y_0 > 0$ , the open quadrant the book analyses. Lemma 4 carries the book's assumption that $C_2 = 0$ and $C_3 = 0$ lie in the positive quadrant ( $q_1 r_3 < q_3 r_1$ , $q_2 r_4 < q_3 r_2$ ). "Theorem 8" carries the standing assumption $r_3 > r_4$ of § 15.
Misprint corrected. The value of the pure $C$ -policy in the proof of Lemma 6 (§ 15, Eq. (1), p. 237) is printed $r_3 x_0/(q_2 + r_3) + r_4 y_0/(q_3 + r_4)$ . The first denominator must be $q_3 + r_3$ : for $x_0 = 1$ , $y_0 = 0$ , $q_2 = 1$ , $q_3 = 2$ , $r_3 = 1$ the process yields $1/3$ , not $1/2$ . The corrected identity is stated.
Numbering. The third theorem of the chapter is printed "Theorem 8" and is cited that way.
Left out. Theorem 2 ( $D > 0$ ) specifies its solution only through Fig. 7 and an unspecified line $L$ . Lemmas 6–8, 11 and the two Lemmas 12 describe regions of figures. The finite-horizon analysis of § 11 has no numbered result, and neither does the nonlinear utility of § 18.

Useful infrastructure: the derivative formulas (13.1) for the $K_i$ , a first-variation lemma for $f(T)$ under bounded perturbations of a measurable control, and a comparison principle for deteriorating projects. The last is reusable for other continuous-time index policies. Proofs of any milestone, and alternative arguments for Theorem 1, are welcome.

Selected references

R. Bellman, Dynamic Programming, Princeton University Press, 1957; Princeton Landmarks in Mathematics edition, 2010. Chapter VIII, pp. 222–244. https://doi.org/10.2307/j.ctv1nxcw0f
L. S. Pontryagin, V. G. Boltyanskii, R. V. Gamkrelidze, E. F. Mishchenko, The Mathematical Theory of Optimal Processes, Interscience, 1962.
J. C. Gittins, Bandit processes and dynamic allocation indices, Journal of the Royal Statistical Society B 41 (1979), 148–177. https://doi.org/10.1111/j.2517-6161.1979.tb01068.x

11 thms2 active usersReviewed

Analysis Partial Differential Equations·Captain: mikedeng1

Stability and Instability Results of the Wave Equation with a Delay Term in the Boundary or Internal Feedbacks IV: Arbitrarily Small Destabilizing Delays for Internal DampingResearch Paper

Motivation

Feedback laws in engineering are applied with a lag: sensors, actuators and communication channels introduce a time delay $\tau$ between the measurement of a state and the control that reacts to it. For finite-dimensional systems small delays are usually harmless. For distributed systems such as the wave equation they need not be: Datko, Lagnese and Polis (SIAM J. Control Optim. 24, 1986) and Datko (SIAM J. Control Optim. 26, 1988) showed, for one-dimensional examples, that an arbitrarily small delay in a stabilizing feedback can destroy stability. The question matters to anyone who designs boundary or internal controllers for vibrating structures and wants to know whether a stabilizing law is robust to delay.

Nicaise and Pignotti (SIAM J. Control Optim. 45 (2006)) study the wave equation on a bounded domain of $\mathbb R^n$ with a damping term that combines an instantaneous and a delayed velocity feedback, with coefficients $\mu_1$ and $\mu_2$ . They show that the system is exponentially stable when $\mu_2 < \mu_1$ (Theorems 1.1 and 1.3), and that when $\mu_2 \ge \mu_1$ stability can fail (Theorems 1.2 and 1.4). This mission is Theorem 1.4, the internal-damping instability result, in the case the paper proves.

1986–1988: Datko, Lagnese and Polis; Datko — destabilization by small delays in one-dimensional boundary-damped wave equations.
2006: Nicaise and Pignotti — the multi-dimensional dichotomy $\mu_2 < \mu_1$ (stability) versus $\mu_2 \ge \mu_1$ (instability for some delays), for boundary and internal feedback.

Setting

Let $n \ge 1$ and let $\Omega \subset \mathbb R^n$ be a bounded open set with boundary $\Gamma$ of class $C^2$ , split as $\Gamma = \Gamma_D \cup \Gamma_N$ with $\overline{\Gamma_D} \cap \overline{\Gamma_N} = \emptyset$ and $\Gamma_D \neq \emptyset$ . Write $\nu$ for the outer unit normal and $\partial u/\partial\nu$ for the normal derivative. Let $\mu_1 > 0$ , $\mu_2 > 0$ and let $\tau > 0$ be the delay. With damping coefficient $a \equiv 1$ the problem is

u_{tt}(x,t) - \Delta u(x,t) + \mu_1 u_t(x,t) + \mu_2 u_t(x,t-\tau) = 0 \quad \text{in } \Omega \times (0,\infty),

u = 0 \ \text{ on } \Gamma_D \times (0,\infty), \qquad \frac{\partial u}{\partial\nu} = 0 \ \text{ on } \Gamma_N \times (0,\infty),

with initial data $u(\cdot,0) = u_0$ , $u_t(\cdot,0) = u_1$ and a history $u_t = g_0$ on $\Omega \times (-\tau, 0)$ . The standard energy of a solution is

\mathcal E(t) = \frac12 \int_\Omega \big\{ |u_t(x,t)|^2 + |\nabla u(x,t)|^2 \big\}\,dx .

The condition $\mu_2 < \mu_1$ is the paper's assumption (1.8). The paper's problem (1.12)–(1.16) carries a general coefficient $a \in L^\infty(\Omega)$ with $a \ge 0$ and $a > a_0 > 0$ near $\Gamma_N$ ; $a \equiv 1$ is one such coefficient.

Formalization targets

Goal: Theorem 1.4 for $a \equiv 1$

If (1.8) fails, i.e. $0 < \mu_1 \le \mu_2$ , then

\forall \varepsilon > 0\ \exists \tau \in (0,\varepsilon)\ \exists u \text{ solving the problem with delay } \tau:\ \ \mathcal E(t) \not\to 0 \ (t \to \infty),

and the same holds with " $\tau \in (0,\varepsilon)$ " replaced by " $\tau > M$ ", for every $M$ . The goal asserts only non-decay, not a rate of growth or the value of the energy, so it survives any sharpening of the examples.

Milestones

(5.21)–(5.23): if $\varphi$ is an eigenfunction of the mixed Dirichlet–Neumann Laplacian, $\Delta\varphi = -\Lambda^2\varphi$ , and $\lambda \in \mathbb C$ solves $\lambda^2 + (\mu_1 + \mu_2 e^{-\lambda\tau})\lambda = -\Lambda^2$ , then $e^{\lambda t}\varphi(x)$ is a solution.
(5.24)–(5.25): with $\lambda = \alpha + i\beta$ and $\beta\tau = (2l+1)\pi$ , that equation is equivalent to $\alpha^2 + \beta^2 = \Lambda^2$ , $\mu_2 e^{-\alpha\tau} = 2\alpha + \mu_1$ .
Case (a), $\mu_1 = \mu_2$ : the system forces $\alpha = 0$ and $\beta^2 = \Lambda^2$ .
Case (b), $\mu_2 > \mu_1$ , (5.26)–(5.27): for every $\Lambda > 0$ and $l$ there is $\alpha \in (0, (\mu_2-\mu_1)/2)$ with $\tau(\alpha) = \alpha^{-1}\ln(\mu_2/(\mu_1+2\alpha)) > 0$ solving the system.
Energy of separated solutions (p. 1584): $\mathcal E(t) = e^{2\,\mathrm{Re}(\lambda)t}\,\mathcal E(0)$ with $\mathcal E(0) > 0$ .
Delay bounds (p. 1585, corrected): $(2l+1)\pi/\Lambda < \tau < (2l+1)\pi/\sqrt{\Lambda^2 - (\mu_2-\mu_1)^2/4}$ , the second when $\Lambda^2 > (\mu_2-\mu_1)^2/4$ .

Significance

The result shows that the stability threshold $\mu_2 < \mu_1$ of Theorem 1.3 is sharp in the sense that matters for design: at or beyond the threshold there is no delay margin, since delays as small as desired already produce solutions whose energy does not decay. Together with Theorem 1.3 it gives a complete dichotomy in the coefficients $(\mu_1,\mu_2)$ for the internally damped wave equation with delay, in any dimension, and it identifies the mechanism (roots of the characteristic equation on or to the right of the imaginary axis) that later work on delayed stabilization has had to avoid.

The result is proved in the paper; to the best of current knowledge it has not been machine-checked. The mission's product is a formal proof of the $a \equiv 1$ case together with its algebraic core: the reduction of the transcendental characteristic equation, the analysis of both cases, and the two-sided bounds on the delays. The spectral input it needs, an unbounded sequence of eigenvalues of the mixed Dirichlet–Neumann Laplacian with regular eigenfunctions, is reusable well beyond this paper.

Difficulty

The scalar part is elementary. The difficulty is the spectral input. The small delays come from $\tau_{n,l} \approx (2l+1)\pi/\Lambda_n$ with $\Lambda_n \to \infty$ , so the proof needs infinitely many eigenvalues $\Lambda_n^2 \to \infty$ of the Laplacian with mixed Dirichlet–Neumann conditions on a $C^2$ domain, with eigenfunctions that are $C^2$ inside and $C^1$ up to the boundary. This requires compactness of the embedding $H^1_{\Gamma_D}(\Omega) \hookrightarrow L^2(\Omega)$ , the spectral theorem for compact self-adjoint operators, and elliptic regularity for a mixed problem, none of which is available in Mathlib for domains in $\mathbb R^n$ . A single eigenpair gives only the large delays (letting $l \to \infty$ ); it does not give the small ones.

A second point: the paper's own bound $(2l+1)^2\pi^2/\tau_{n,l}^2 \le \Lambda_n^2$ bounds $\tau_{n,l}$ only from below, so it does not by itself give $\tau_{n,l} \to 0$ ; the upper bound of milestone 6 is needed.

Formalization scope

Space: $\mathbb R^n$ is EuclideanSpace ℝ (Fin n) with $n \ge 1$ . The $C^2$ boundary is given by a global $C^2$ defining function $\psi$ ( $\Omega = \{\psi < 0\}$ , $\partial\Omega = \{\psi = 0\}$ , $\nabla\psi \ne 0$ on $\partial\Omega$ ); $\nu = \nabla\psi/|\nabla\psi|$ ; the surface measure is pinned by the Gauss–Green formula for all $C^1$ fields.
Solutions are complex valued functions $u(x,t)$ defined for all $t \in \mathbb R$ , $C^2$ on $\Omega \times \mathbb R$ and $C^1$ on $\overline\Omega \times \mathbb R$ ; the equation and boundary conditions hold for $t > 0$ ; initial data and history are the traces of $u$ . The Neumann condition uses the derivative within $\overline\Omega$ . $|\nabla u|^2$ is the sum of the squared moduli of the partial derivatives.
Corrected scope: Theorem 1.4 is printed for a general $a$ satisfying (1.17)–(1.18); §5.2 proves it only for $a \equiv 1$ , which is what is stated.
Corrected slips: (5.22) prints $\Delta\varphi = -\mu^2\varphi$ for $-\Lambda^2\varphi$ ; p. 1584 prints $e^{\alpha+i\beta}\varphi(x)$ for $e^{(\alpha+i\beta)t}\varphi(x)$ ; the p. 1585 bound is supplemented by the upper bound of milestone 6. Milestone texts are quoted verbatim, including the slips.
The standing hypotheses (1.6)–(1.7) and the constant $\xi$ of (1.10) are not used by §5.2 and are omitted, which strengthens the statements.
A trivializing formalization is ruled out: the goal's conclusion $\mathcal E \not\to 0$ excludes $u \equiv 0$ , the energy integrand is continuous on the compact $\overline\Omega$ so the integral is genuine, and the normal derivative is taken within $\overline\Omega$ so the Neumann condition is not satisfied by a junk value.
No statement assumes the existence of eigenvalues; supplying the spectral theory of the mixed Laplacian is part of the goal. Contributions welcome: the spectral theorem for the mixed Dirichlet–Neumann Laplacian on a bounded $C^2$ domain, boundary regularity of its eigenfunctions, and the energy identity for separated solutions.

Selected references

S. Nicaise, C. Pignotti, Stability and instability results of the wave equation with a delay term in the boundary or internal feedbacks, SIAM J. Control Optim. 45(5):1561–1585, 2006. https://doi.org/10.1137/060648891
R. Datko, Not all feedback stabilized hyperbolic systems are robust with respect to small time delays in their feedbacks, SIAM J. Control Optim. 26:697–713, 1988.
R. Datko, J. Lagnese, M. P. Polis, An example on the effect of time delays in boundary feedback stabilization of wave equations, SIAM J. Control Optim. 24:152–156, 1986.
P. Grisvard, Elliptic Problems in Nonsmooth Domains, Pitman, 1985 (regularity of mixed boundary value problems).

10 thms2 active usersReviewed

Analysis Partial Differential Equations·Captain: mikedeng1

Stability and Instability Results of the Wave Equation with a Delay Term in the Boundary or Internal Feedbacks III: Destabilizing Delays for Boundary FeedbackResearch Paper

Motivation

Boundary feedback stabilization of the wave equation asks whether a damping term placed on part of the boundary drives the energy of every solution to zero. Without delay the answer is classical: the feedback $\partial u/\partial\nu = -\mu_1 u_t$ on a part $\Gamma_N$ of the boundary gives exponential energy decay under geometric conditions (Chen, Lagnese, Lasiecka–Triggiani, Komornik–Zuazua). In practice a feedback is applied with a lag, and a small lag can destroy stability. Datko, Lagnese and Polis (doi:10.1137/0324007) and Datko (doi:10.1137/0326040) showed, in one space dimension, that a purely delayed boundary feedback destabilizes the system for arbitrarily small delays.

Nicaise and Pignotti (doi:10.1137/060648891) study a feedback made of an instantaneous part and a delayed part, with weights $\mu_1$ and $\mu_2$ , in any space dimension. Their Theorem 1.1 gives exponential decay when $\mu_2 < \mu_1$ . This mission formalizes the converse, Theorem 1.2: when $\mu_2 \ge \mu_1$ , some delays admit solutions whose energy does not decay at all.

Timeline.

1986: Datko, Lagnese and Polis, a one-dimensional wave equation whose delayed boundary feedback is unstable.
1988: Datko, instability under arbitrarily small delays for a class of hyperbolic systems.
2006: Xu, Yung and Li (doi:10.1051/cocv:2006021), one space dimension, by spectral analysis: stability for $\mu_2 < \mu_1$ , instability for $\mu_2 > \mu_1$ , possible instabilities for $\mu_1 = \mu_2$ .
2006: Nicaise and Pignotti, the same dichotomy in any dimension $n$ , with explicit destabilizing delays built from eigenfunctions (§5.1).

Setting

Let $n \ge 1$ and let $\Omega \subset \mathbb R^n$ be a bounded open set with boundary $\Gamma$ of class $C^2$ . The boundary is split as $\Gamma = \Gamma_D \cup \Gamma_N$ , with $\overline{\Gamma_D} \cap \overline{\Gamma_N} = \emptyset$ and $\Gamma_D \neq \emptyset$ . Write $\nu$ for the outer unit normal and $d\Gamma$ for the surface measure. Together these data form a mixed domain (MixedDomain n in Lean).

Fix $\mu_1, \mu_2 > 0$ and a delay $\tau > 0$ . The problem (1.1)–(1.3) is

\begin{cases} u_{tt}(x,t) - \Delta u(x,t) = 0 & \text{in } \Omega \times (0,+\infty),\\ u(x,t) = 0 & \text{on } \Gamma_D \times (0,+\infty),\\ \dfrac{\partial u}{\partial\nu}(x,t) = -\mu_1 u_t(x,t) - \mu_2 u_t(x,t-\tau) & \text{on } \Gamma_N \times (0,+\infty), \end{cases}

with initial data $u(\cdot,0)$ , $u_t(\cdot,0)$ and a history $u_t$ on $\Gamma_N \times (-\tau,0)$ (1.4)–(1.5). The standard energy of a solution is (3.7)

\mathcal E(t) = \frac12\int_\Omega \big(|u_t(x,t)|^2 + |\nabla u(x,t)|^2\big)\,dx .

Condition (1.8) of the paper is $\mu_2 < \mu_1$ . This mission concerns the complementary case $\mu_2 \ge \mu_1$ .

For real functions $w$ on $\Omega$ , (5.11) defines $q_0(w) = \int_{\Gamma_N} |w|^2\,d\Gamma$ and $q_1(w) = \int_\Omega |\nabla w|^2\,dx$ .

Formalization targets

Goal: Theorem 1.2 (p. 1563)

If $\mu_2 \ge \mu_1$ , there exist delays $0 < \tau_0 < \tau_1 < \cdots$ and, for each $k$ , a classical solution $u_k$ of (1.1)–(1.3) with delay $\tau_k$ and a constant $c_k > 0$ such that

\mathcal E_k(t) = c_k \qquad \text{for all } t \ge 0 .

The statement fixes no formula for the delays and no value of the energy. It asserts only the existence of infinitely many delays for which the energy does not decay.

Milestones

(5.1)–(5.2), pp. 1579–1580. If $\lambda \in \mathbb C$ and $\varphi$ solves $-\Delta\varphi + \lambda^2\varphi = 0$ in $\Omega$ , $\varphi = 0$ on $\Gamma_D$ and $\partial\varphi/\partial\nu = -(\mu_1 + \mu_2 e^{-\lambda\tau})\lambda\varphi$ on $\Gamma_N$ , then $u = e^{\lambda t}\varphi$ solves (1.1)–(1.3).
(5.5)–(5.7), pp. 1580 and 1582. For $b > 0$ , $l \in \mathbb N$ and $b\tau = \arccos(-\mu_1/\mu_2) + 2l\pi$ :

\cos(b\tau) = -\mu_1/\mu_2,\qquad \mu_2\sin(b\tau) = \sqrt{\mu_2^2-\mu_1^2},\qquad (\mu_1 + \mu_2e^{-ib\tau})\,ib = b\sqrt{\mu_2^2-\mu_1^2}.

Case (a), $\mu_1 = \mu_2$ , p. 1581. For a normalized mixed Dirichlet–Neumann eigenfunction $\varphi$ with $-\Delta\varphi = b^2\varphi$ and $\tau = (2l+1)\pi/b$ , the function $u = e^{ibt}\varphi$ is a solution and

\int_\Omega(|\nabla u|^2 + |u_t|^2)\,dx = 2b^2 \quad (t \ge 0).

Case (b), $\mu_2 > \mu_1$ , pp. 1581–1582. A normalized minimizer $\varphi$ of $s\,q_0(w) + \sqrt{s^2q_0(w)^2 + 4q_1(w)}$ , where $s = \sqrt{\mu_2^2-\mu_1^2}$ , solves the variational problem (5.7) with $2b$ equal to the minimum value.

Significance

The result. Theorem 1.2 shows that the threshold $\mu_2 < \mu_1$ of Theorem 1.1 is sharp in the following sense: once the delayed weight reaches the instantaneous one, no geometric assumption restores asymptotic stability for every delay. Together, Theorems 1.1 and 1.2 separate robust from non-robust boundary feedbacks by a single inequality between the two gains. The explicit delays of case (a), $\tau_{n,l} = (2l+1)\pi/b_n$ , become arbitrarily small or large. So even an arbitrarily short lag in an equally weighted feedback can remove decay.

The formalization. The paper proves the result. It has not been formalized, and Mathlib has no wave equation on domains, no mixed eigenvalue problems and no Sobolev spaces on domains. This mission produces:

a machine-checked statement of the instability half of the paper's dichotomy;
the reduction to a spectral problem as separate, checkable steps;
a precise record of what the paper leaves implicit. In case (b) the existence of the minimizer is assumed ("if the minimum … is attained"), and in case (a) the existence of Dirichlet–Neumann eigenfunctions is quoted.

Difficulty

Milestones 1 and 2 are calculus and trigonometry. The difficulty sits in producing $\varphi$ . The goal needs a nonzero function $\varphi$ that is $C^2$ in $\Omega$ and $C^1$ up to the boundary and solves an eigenvalue problem with mixed Dirichlet and Neumann (case (a)) or Dirichlet and Robin-type (case (b)) boundary conditions. Existence requires compactness of $H^1_{\Gamma_D}(\Omega) \hookrightarrow L^2(\Omega)$ and of the trace into $L^2(\Gamma_N)$ , followed by elliptic regularity up to a $C^2$ boundary. None of these is in Mathlib.

A shortcut does not work: in case (b) the frequency $b$ enters the boundary condition, so $\varphi$ is not an eigenfunction of a fixed self-adjoint operator. The page instead minimizes a non-quadratic functional, and its first-variation computation (5.18)–(5.19) needs care: the functional is not 2-homogeneous, so the normalization by $1 + \varepsilon^2\|v\|^2$ does not literally give $g(\varepsilon) \ge g(0)$ , although the first-order condition is right.

Taking real parts does not give a real-valued solution with constant energy: in case (b) the energy of $\cos(bt)\varphi$ oscillates.

Formalization scope

Solutions are complex-valued, $u : \mathbb R^n \times \mathbb R \to \mathbb C$ , as the page's $e^{\lambda t}\varphi$ with $\lambda \in \mathbb C$ are. $|u_t|^2$ and $|\nabla u|^2 = \sum_i |\partial_i u|^2$ are squared moduli.
Classical solutions. A solution is $C^2$ on $\Omega \times \mathbb R$ and $C^1$ on $\overline\Omega \times \mathbb R$ . It solves the equations for $t > 0$ , and its values at $t \le 0$ are the initial data and history. The normal derivative is the derivative within $\overline\Omega$ applied to $\nu$ . $C^2$ regularity up to the boundary is not required, because eigenfunctions of mixed problems generally lack it.
The domain. The $C^2$ boundary is given by a global defining function $\psi$ with $\Omega = \{\psi < 0\}$ . The surface measure is pinned down by the Gauss–Green formula for all $C^1$ vector fields, which determines it uniquely.
Dropped hypotheses. The geometric hypotheses (1.6)–(1.7) and the parameter $\xi$ of (1.10) are not used in §5.1 and are omitted. This strengthens the statements.
Sobolev spaces. $H^1_{\Gamma_D}(\Omega)$ is replaced in milestone 4 by the class of real functions that are $C^2$ in $\Omega$ , $C^1$ on $\overline\Omega$ and zero on $\Gamma_D$ , both as the minimization class and as the test class.
Non-triviality. The goal requires the constant energy to be positive and the delays to be strictly increasing. Without positivity, the zero solution would satisfy "constant energy". Without strict monotonicity, one delay repeated would count as a sequence.

A complete development needs the following:

Green's first identity on $C^2$ domains for functions that are $C^1$ up to the boundary;
existence and regularity of eigenfunctions of the Laplacian with mixed boundary conditions;
in case (b), existence of the minimizer (Rellich compactness and the trace theorem).

These pieces are reusable well beyond this mission. Contributions of any of them, or of an alternative route to a $\varphi$ with the required properties, are welcome.

Selected references

S. Nicaise, C. Pignotti, Stability and instability results of the wave equation with a delay term in the boundary or internal feedbacks, SIAM J. Control Optim. 45(5):1561–1585, 2006. https://doi.org/10.1137/060648891
R. Datko, J. Lagnese, M. P. Polis, An example on the effect of time delays in boundary feedback stabilization of wave equations, SIAM J. Control Optim. 24:152–156, 1986. https://doi.org/10.1137/0324007
R. Datko, Not all feedback stabilized hyperbolic systems are robust with respect to small time delays in their feedbacks, SIAM J. Control Optim. 26:697–713, 1988. https://doi.org/10.1137/0326040
G. Q. Xu, S. P. Yung, L. K. Li, Stabilization of wave systems with input delay in the boundary control, ESAIM Control Optim. Calc. Var. 12:770–785, 2006. https://doi.org/10.1051/cocv:2006021

7 thms2 active usersReviewed

Dynamical Systems Linear algebra·Captain: mikedeng1

Stabilization for a Perturbed Chain of Integrators in Prescribed Time I: Prescribed-Time Estimates for the Linear Time-Varying FeedbackResearch Paper

Motivation

Many control tasks have to settle at a given deadline, not merely eventually. Examples are missile guidance, where the interception time is fixed in advance, and rendezvous or consensus manoeuvres that must finish by a scheduled instant. Prescribed-time stabilization asks for a feedback that brings the state of a system to the origin at a time $T>0$ chosen by the designer, independently of the initial condition, and keeps this property under disturbances. It is stronger than finite-time stabilization, where the settling time depends on the initial state, and stronger than fixed-time stabilization, where it is only bounded uniformly.

Song, Wang, Holloway and Krstić (Automatica 2017) obtained prescribed-time regulation of normal-form systems with feedback gains that grow without bound as $t\to T$ . The computations required explicit time derivatives of the gain function. Chitour, Ushirobira and Bouhemou (SIAM J. Control Optim. 2020) recast this construction as time-varying homogeneity: a time-dependent dilation of the state combined with a change of time turns the prescribed-time problem into a standard exponential-stabilization problem on an infinite horizon. The analysis then reduces to linear matrix inequalities. This mission formalizes the linear-feedback part of that paper (§3.1, pp. 1026–1030).

Timeline:

2010: Chitour and Sigalotti (SIAM J. Control Optim. 48) prove a Lyapunov LMI for $J_n - b e_n K^T$ , uniform over a bounded range $\underline b\le b\le\bar b$ .
2017: Song, Wang, Holloway and Krstić give prescribed-time regulation with a time-varying feedback.
2020: Chitour, Ushirobira and Bouhemou remove the upper bound $\bar b$ (Proposition 10) and derive the prescribed-time estimate by time-varying homogeneity (Corollary 14).

Setting

Fix a positive integer $n$ and a prescribed time $T>0$ . Let $(e_i)_{1\le i\le n}$ be the canonical basis of $\mathbb R^n$ , and let $J_n$ be the $n$ -th Jordan block, $J_n e_i = e_{i-1}$ with $e_0=0$ . The perturbed chain of integrators is

\dot x(t) = J_n x(t) + \big(d(t) + b(t)u(t)\big) e_n, \qquad t\in[0,T),

with state $x(t)\in\mathbb R^n$ and control $u(t)\in\mathbb R$ . Here $d$ is a measurable matched disturbance, and $b$ is an uncertain control gain with $b(t)\ge\underline b>0$ and no upper bound.

With weights $r_i = n-i+1$ , the dilation is $D^{\mathbf r}_\mu = \operatorname{diag}(\mu^{r_1},\dots,\mu^{r_n})$ and $D_{\mathbf r} = \operatorname{diag}(r_1,\dots,r_n)$ . An admissible weight is a continuous function $a\ge0$ on $[0,T]$ with $\int_t^T a>0$ for $t<T$ . It defines

\lambda(t) = \frac{1}{\int_t^T a(\xi)\,d\xi},\qquad s(t) = \int_0^t\lambda(\xi)\,d\xi,\qquad 0\le t<T.

The parameter $\lambda$ blows up at $T$ , and $s$ maps $[0,T)$ onto $[0,\infty)$ . In the coordinates $y = D^{\mathbf r}_{\lambda(t)}x$ and the time $s$ , the system becomes

y' = \big(a D_{\mathbf r} + J_n\big)y + (b u + d)e_n .

The feedback studied is $u = -K^T D^{\mathbf r}_\eta y$ , that is $u(t) = -K^T D^{\mathbf r}_{\eta\lambda(t)}x(t)$ in the original variables, where $K\in\mathbb R^n$ and $\eta\ge1$ .

Formalization targets

Goal: Corollary 14 (corrected)

There is a rate $\mu>0$ depending only on $n$ and $\underline b$ such that, for every $T$ and admissible $a$ , there are $K$ and $C>0$ with

|x_i(t)| \le \frac{1}{(\eta\lambda(t))^{n-i+1}}\Big(C\eta\max(1,\eta^{n-1})e^{-\mu\eta s(t)}\|x(0)\| + C\max_{r\in[0,t]}|d(r)|\Big)

for every $\eta\ge1$ , every $b\ge\underline b$ , every disturbance $d$ , every closed-loop solution, every $t\in[0,T)$ and every $1\le i\le n$ . Since $\lambda(t)\to\infty$ , every coordinate reaches $0$ at the prescribed time $T$ .

Milestones

§3 (10): $\dot\lambda = a\lambda^2$ , $\lambda$ is nondecreasing and tends to $\infty$ at $T$ , and $s$ is an increasing $C^1$ bijection $[0,T)\to[0,\infty)$ .
§3 (7)–(11): the transformed dynamics.
Proposition 10: $\exists\rho,S,K$ such that $(J_n - be_nK^T)^TS + S(J_n-be_nK^T)\preceq-\rho\,\mathrm{Id}$ for all $b\ge\underline b$ .
Proposition 11: the same LMI with $aD_{\mathbf r}$ added, uniformly in $|a|\le C_0$ .
Proposition 12 (corrected): the ISS estimate (17) in the time $s$ .
Proposition 13: the $\eta$ -scaled LMI (20).

Significance

Corollary 14 says that a linear feedback with a time-varying gain drives the chain of integrators to the origin at the designer's deadline $T$ . The guarantee holds for every control gain $b\ge\underline b$ , however large, and gives an explicit input-to-state bound for the matched disturbance. The weight $a$ is free, so the blow-up profile of the gain can be chosen, for example to converge faster than polynomially. Proposition 10 removes the upper bound on $b$ from the classical LMI, and is of independent use for high-gain and persistently excited systems.

On formalization: the results are proved on paper; no formalization of them is known. The mission produces checked statements of the LMIs, the time change, and the prescribed-time estimate. Two printed estimates are false as stated, (17) and (23), and the mission states corrected versions (see Formalization scope). Formal proofs would certify the corrected constants.

Difficulty

The obvious approach is to take a Lyapunov function for the constant-coefficient closed loop and differentiate it along trajectories. This fails for two reasons. First, $b$ ranges over an unbounded interval, so no compactness argument yields a common Lyapunov matrix, and a single $S$ and $K$ must work for all $b\ge\underline b$ at once. Second, the transformed system carries the time-varying term $a(s)D_{\mathbf r}$ , and in the original time the feedback gain $\lambda(t)$ is unbounded. Estimates must survive both the rescaling by $D^{\mathbf r}_{\eta\lambda(t)}$ and the change of time. Constants that look harmless in the new time, such as the condition number of $S$ and the value $\lambda(0)$ , reappear in the original variables, and dropping them makes the printed estimates false.

Formalization scope

Lean representation: vectors of $\mathbb R^n$ are Fin n → ℝ, and coordinate i : Fin n is the paper's index i.val + 1, so $r_i$ = n - i.val. Matrices are Matrix (Fin n) (Fin n) ℝ, and $e_nK^T$ is vecMulVec (eN n) K. Matrix inequalities use the Loewner order (open scoped MatrixOrder), and "real symmetric positive definite" is PosDef. The norm $\|\cdot\|$ is Euclidean, written out as eucNorm. Solutions are Carathéodory solutions in integral form: for every $t$ in the interval, the right-hand side is integrable on $[0,t]$ and the integral identity holds. This matches the paper's measurable $b$ and $d$ . The standing assumptions are $n\ge1$ (§3), $T>0$ , $a$ continuous and nonnegative on $[0,T]$ with $\int_t^Ta>0$ on $[0,T)$ , and $b\ge\underline b>0$ . No upper bound on $b$ is assumed anywhere. $\max|d|$ is replaced by an arbitrary bound $D$ of $|d|$ on the interval.

Corrected statements, with milestone texts kept verbatim:

(17) as printed has no constant on the transient term and fails for $n\ge2$ : with $a\equiv1$ and $y(0)=e_1$ , $|y_1|$ first increases. Proposition 12 is stated with $C_S$ on that term.
(23) as printed fails at $t=0$ whenever $\int_0^Ta<1$ . The goal is stated with a constant $C$ on the transient term, and $K$ and $C$ may depend on $T$ and $a$ . The rate $\mu$ and the disturbance gain $C_S$ depend only on $n$ and $\underline b$ , as on the page.
Proposition 13's undefined $\mu_*$ is the $\rho$ of its statement.
" $\lambda$ increasing" is read as nondecreasing.
Corollary 14's " $t\ge0$ " is read as $t\in[0,T)$ .

Trivializing encodings are ruled out as follows. The integrability clause of IsIntegralSolution prevents a non-integrable right-hand side from integrating to $0$ . Every constant is quantified before the objects it must not depend on: the rate $\mu$ before $T$ and $a$ , $K$ before $\eta$ , and $\rho,S,K$ before $b$ . No statement weakens the estimates to mere convergence.

Needed infrastructure: Lyapunov estimates for absolutely continuous solutions, Loewner-order congruence, and interval-integral calculus for the time change. The LMI lemmas and the integral-form solution predicate are reusable in other control missions. Proofs of any milestone are welcome, and so are sharper constants.

Selected references

Y. Chitour, R. Ushirobira, H. Bouhemou, Stabilization for a Perturbed Chain of Integrators in Prescribed Time, SIAM J. Control Optim. 58(2):1022–1048, 2020. https://doi.org/10.1137/19M1285937
Y. Song, Y. Wang, J. Holloway, M. Krstić, Time-varying feedback for regulation of normal-form nonlinear systems in prescribed finite time, Automatica 83:243–251, 2017. https://doi.org/10.1016/j.automatica.2017.06.008
Y. Chitour, M. Sigalotti, On the stabilization of persistently excited linear systems, SIAM J. Control Optim. 48:4032–4055, 2010. https://doi.org/10.1137/080737812

10 thms2 active usersReviewed

Completed

Operations Research Theoretical Computer Science·Captain: mikedeng1

Supervisory Control of a Class of Discrete Event Processes II: Every Reduced, Trim Supervisor Is the Quotient of a Supervisor Built on a Recognizer for Its Closed-Loop LanguageResearch Paper

Motivation

Supervisory control theory, introduced by Ramadge and Wonham (SIAM J. Control Optim. 25(1), 1987), models a manufacturing cell, a communication protocol or a resource-sharing system as an automaton whose transitions are events, some of which an external controller may disable. A controller, the supervisor, is itself an automaton that watches the event sequence and, in each of its states, decides which controllable events are currently allowed. The framework is the standard model for logical (untimed) control of discrete event systems and is the subject of textbooks such as Cassandras and Lafortune (Springer, 2008) and Wonham and Cai (Springer, 2019).

A practical concern is supervisor size. The synthesis procedure of the paper (§9) produces a supervisor whose automaton records exactly as much of the past as the desired closed-loop language requires, but there are many other supervisors realising the same behaviour. The paper's second main result, the quotient structure theorem (Theorem 10.1, p. 223), explains how they are related: any supervisor with two natural economy properties is obtained from a canonical one, built on a recognizer of the closed-loop language, by lumping states. This is the structural starting point of the later literature on supervisor reduction.

Setting

A generator is $\mathcal G = (Q, \Sigma, \delta, q_0, Q_m)$ : a state set $Q$ , a finite alphabet $\Sigma$ of events, a partial transition function $\delta : \Sigma \times Q \to Q$ , an initial state $q_0$ and marker states $Q_m \subseteq Q$ . Extending $\delta$ to strings gives the generated language $L(\mathcal G)$ (strings along which $\delta$ is defined from $q_0$ ) and the marked language $L_m(\mathcal G)$ (those that end in $Q_m$ ). The closure $\bar K$ of a language $K$ is its set of prefixes. Throughout, $\mathcal G$ is trim: $L(\mathcal G) = \bar L_m(\mathcal G)$ . A recognizer for a language $K$ is an accessible generator whose marked language is $K$ .

A subset $\Sigma_c \subseteq \Sigma$ of events is controllable. A supervisor is $\mathcal S = (S, \phi)$ where $S = (X, \Sigma, \xi, x_0, X_m)$ is an accessible deterministic automaton with possibly infinite state set and $\phi : X \to \{0,1\}^{\Sigma_c}$ is a state feedback map; events outside $\Sigma_c$ are always enabled. The closed loop $\mathcal S/\mathcal G$ runs $S$ and $\mathcal G$ in lockstep and allows $\sigma$ from $(x, q)$ iff $\xi(\sigma, x)$ and $\delta(\sigma, q)$ are defined and $\phi(x)(\sigma) = 1$ . Its languages are $L(\mathcal S/\mathcal G)$ , $L_m(\mathcal S/\mathcal G)$ (marker set $X_m \times Q_m$ ) and $L_c(\mathcal S/\mathcal G) = L(\mathcal S/\mathcal G) \cap L_m(\mathcal G)$ .

$\mathcal S$ is complete if $S$ never refuses an event that the plant can execute and $\phi$ enables: $s \in L(\mathcal S/\mathcal G)$ , $s\sigma \in L(\mathcal G)$ and $\phi(\xi(s, x_0))(\sigma) = 1$ imply $s\sigma \in L(\mathcal S/\mathcal G)$ . It is proper if it is complete and $\bar L_m(\mathcal S/\mathcal G) = \bar L_c(\mathcal S/\mathcal G) = L(\mathcal S/\mathcal G)$ .

A projection $\pi : \mathcal S \to \hat{\mathcal S}$ is a surjection $X \to \hat X$ with $\pi(x_0) = \hat x_0$ , $X_m = \pi^{-1}(\hat X_m)$ , $\hat\xi(\sigma, \pi(x)) = \pi(\xi(\sigma, x))$ wherever $\xi(\sigma, x)$ is defined, and $\hat\phi \circ \pi = \phi$ .

For a language $K$ , strings $s, s'$ are $\bar K$ -equivalent if $st \in \bar K \iff s't \in \bar K$ for all $t$ . The automaton $S$ is $\bar K$ -reduced if $\bar K$ -equivalent strings of $\bar K$ lead to the same state, and $\bar K$ -trim if every state is reached by a string of $\bar K$ .

Formalization targets

Goal: Theorem 10.1 (quotient structure theorem)

Let $\mathcal S = (S, \phi)$ be complete, $K_1 := L_m(\mathcal S/\mathcal G)$ , $K_3 := L(\mathcal S/\mathcal G)$ , with $S$ $K_3$ -reduced and $K_3$ -trim, and let $\hat S^0 = (X^0, \Sigma, \xi^0, x^0_0, X^0)$ be a trim recognizer for $K_3$ . Then there are $X^0_m \subseteq X^0$ and $\phi^0$ such that $\mathcal S^0 = ((X^0, \Sigma, \xi^0, x^0_0, X^0_m), \phi^0)$ satisfies

\mathcal S^0 \text{ complete},\quad L_m(\mathcal S^0/\mathcal G) = K_1,\quad L(\mathcal S^0/\mathcal G) = K_3,\quad \exists\, \pi : \mathcal S^0 \to \mathcal S,\quad \mathcal S \text{ proper} \Rightarrow \mathcal S^0 \text{ proper}.

Milestones

Proposition 8.1 (p. 219): for complete $\mathcal S$ and a projection $\pi : \mathcal S \to \hat{\mathcal S}$ , (i) $\pi$ is unique; (ii) $(L_m, L_c, L)(\mathcal S/\mathcal G) = (L_m, L_c, L)(\hat{\mathcal S}/\mathcal G)$ ; (iii) $\hat{\mathcal S}$ is complete; (iv) nonblocking, nonrejecting and proper transfer in both directions.

The displayed steps of the proof of Theorem 10.1 (pp. 223–224): $\pi(\xi^0(s, x^0_0)) := \xi(s, x_0)$ is well defined on $X^0$ ; it is a projection once $X^0_m := \pi^{-1}(X_m)$ and $\phi^0 := \phi \circ \pi$ ; $L(\mathcal S^0/\mathcal G) = K_3$ follows from two enablement conditions; $\mathcal S^0$ is complete; and $L_m(\mathcal S^0/\mathcal G) = K_1$ .

Significance

Theorem 10.1 says that the reduction properties the synthesis procedure of §9 guarantees are exactly what makes a supervisor a quotient of the canonical supervisor on a recognizer of $K_3$ . Combined with Proposition 8.1, which shows that a projection preserves every closed-loop language, completeness and properness, it identifies supervisors with the same behaviour up to state lumping. This is the basis on which supervisor reduction and the comparison of supervisor realisations rest.

The result is proved in the paper. What this mission produces is a machine-checked version of the model (generators with partial transitions, supervisors with infinite state sets, the closed loop, completeness and properness) and of the two results above. No formalization of Ramadge–Wonham supervisory control was found on Prove2Me at the time of drafting; the definitions of this mission are reusable by any later mission on the theory, including the synthesis results of the first mission of the series.

Difficulty

The mathematics is elementary; the difficulty is bookkeeping with partial functions. Every step compares runs of three automata (the plant, $S$ and the recognizer) that may be undefined at different strings, and a proof must track at each string which of them is defined. The tempting shortcut of treating the projection condition as full commutation, $\hat\xi(\sigma, \pi(x)) = \pi(\xi(\sigma, x))$ for all $\sigma, x$ , is not available: the page asks for it only where $\xi(\sigma, x)$ is defined, and Proposition 8.1 (ii) holds only because completeness of $\mathcal S$ compensates for transitions that $\hat\xi$ has and $\xi$ lacks. Likewise, the map $\pi$ of Theorem 10.1 is defined through arbitrary representatives, and its well-definedness uses both that $\hat S^0$ recognizes $K_3$ with all states marked and that $S$ is $K_3$ -reduced.

Formalization scope

The alphabet is a Lean type α with [Fintype α] (the page's $\Sigma$ , which is Lean syntax); strings are List α, $s\sigma$ is s ++ [σ]. A generator is a structure with its own state type in Type and a partial transition δ : α → Q → Option Q; its extended transition is the left fold. The feedback map has type X → Ec → Bool, and " $\sigma$ enabled at $x$ " means $\sigma \notin \Sigma_c$ or $\phi(x)(\sigma) = 1$ ; the page's $\phi : X \to \{0,1\}^\Sigma$ is the same object under this extension. The closed loop is run from $(x_0, q_0)$ without forming its accessible part, which changes none of its languages. Existential statements over supervisors quantify over state types in Type.

Standing assumptions that are hypotheses of every theorem: $\Sigma$ finite; $\mathcal G$ trim, stated as 𝒢.L = pre 𝒢.Lm; every supervisor automaton accessible. Theorem 10.1 and its proof steps also assume $\mathcal S$ complete, $S$ $K_3$ -reduced and $K_3$ -trim, and a trim recognizer $R$ for $K_3$ with all states marked, and $\mathcal S^0$ is built on that given $R$ rather than on a recognizer chosen by the prover. The conclusion names $K_1$ and $K_3$ as the languages of $\mathcal S$ , not as free variables. A projection predicate that drops $\pi(x_0) = \hat x_0$ , surjectivity or the marker equation would make the goal's clause (ii) trivially satisfiable by a constant map; the sanity check shipped with the mission rules this out on the primitive plant of §2.3.

Contributions welcome: proofs of the milestones, lemmas relating the fold-based extended transition to concatenation, and a reusable library for closed-loop runs.

Selected references

P. J. Ramadge and W. M. Wonham, Supervisory Control of a Class of Discrete Event Processes, SIAM J. Control Optim. 25(1):206–230, 1987. https://doi.org/10.1137/0325013
C. G. Cassandras and S. Lafortune, Introduction to Discrete Event Systems, 2nd ed., Springer, 2008. https://doi.org/10.1007/978-0-387-68612-7
W. M. Wonham and K. Cai, Supervisory Control of Discrete-Event Systems, Springer, 2019. https://doi.org/10.1007/978-3-319-77452-7

15 thms2 active usersReviewed

Completed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Robust Solutions to Uncertain Semidefinite Programs II: An SDP Inner Approximation of the Robust Feasible Set under Structured PerturbationsResearch Paper

Motivation

A semidefinite program (SDP) minimizes a linear objective $c^Tx$ subject to a linear matrix inequality $F(x) = F_0 + \sum_{i=1}^m x_i F_i \succeq 0$ . In engineering applications the coefficient matrices are rarely known exactly: they come from measurements, from a model of a physical plant, or from a finite-precision implementation. El Ghaoui, Oustry and Lebret (SIAM J. Optim. 9(1), 1998) asked for solutions that remain feasible for every admissible value of the uncertain data, and showed how to compute such robust solutions by semidefinite programming. The paper appeared alongside Ben-Tal and Nemirovski's robust convex programming (Math. Oper. Res. 23(4), 1998) and is one of the two founding treatments of robust SDP.

When the uncertainty has structure (a block-diagonal perturbation, repeated scalar parameters, a symmetric matrix), the exact robust problem is NP-hard (El Ghaoui and Lebret, SIAM J. Matrix Anal. Appl. 18, 1997). This is the same obstacle that robust control meets in computing the structured singular value, and the remedy the paper uses, scaling matrices that commute with the perturbation structure, goes back to that literature (Doyle, IEE Proc. D 129, 1982; Fan, Tits and Doyle, IEEE Trans. Automat. Control 36, 1991). This mission formalizes the resulting tractable conservative approximation, Theorem 3.2 of the paper, together with the lemma it rests on and an application to integer feasibility problems.

Setting

Fix natural numbers $m, n, p, q$ . The decision variable is $x \in \mathbb{R}^m$ . The nominal data are affine maps

F(x) = F_0 + \sum_{i=1}^m x_i F_i \in \mathbb{R}^{n\times n}, \qquad R(x) = R_0 + \sum_{i=1}^m x_i R_i \in \mathbb{R}^{q\times n},

with every $F_i$ symmetric, and fixed matrices $L \in \mathbb{R}^{n\times p}$ , $D \in \mathbb{R}^{q\times p}$ . A perturbation is a matrix $\Delta \in \mathbb{R}^{p\times q}$ , and the perturbed constraint matrix is the linear-fractional representation (LFR)

\mathbf{F}(x,\Delta) = F(x) + L\Delta(I - D\Delta)^{-1}R(x) + R(x)^T(I - \Delta^TD^T)^{-1}\Delta^TL^T,

which is defined when $\det(I - D\Delta) \neq 0$ . The perturbation ranges over a linear subspace $\mathcal{D} \subseteq \mathbb{R}^{p\times q}$ , which encodes the structure, and is bounded by a level $\rho > 0$ in the spectral norm $\|\Delta\|$ (the largest singular value). The robust feasible set is

\mathcal{X}_\rho = \{x : \text{for every } \Delta \in \mathcal{D} \text{ with } \|\Delta\| \le \rho,\ \det(I - D\Delta) \neq 0 \text{ and } \mathbf{F}(x,\Delta) \succeq 0\},

and the robust SDP (RSDP) is to minimize $c^Tx$ over $\mathcal{X}_\rho$ .

The scaling set of $\mathcal{D}$ is the linear subspace

\mathcal{B} = \{(S,T,G) \in \mathbb{R}^{p\times p}\times\mathbb{R}^{q\times q}\times\mathbb{R}^{p\times q} : S\Delta = \Delta T,\ G\Delta^T = -\Delta G^T \text{ for every } \Delta \in \mathcal{D}\}.

Formalization targets

Goal: Theorem 3.2 (p. 37), as an inclusion of feasible sets

For every $x$ : if some $(S,T,G) \in \mathcal{B}$ has $S \succ 0$ , $T \succ 0$ and

\begin{bmatrix} F(x) - LSL^T & R(x)^T - LSD^T + LG \\ R(x) - DSL^T + G^TL^T & \rho^{-2}T - DSD^T + DG + G^TD^T\end{bmatrix} \succ 0,

then $x \in \mathcal{X}_\rho$ , and in fact $\mathbf{F}(x,\Delta) \succ 0$ for every $\Delta \in \mathcal{D}$ with $\|\Delta\| \le \rho$ . A companion item states the consequence for optimal values: the SDP value is an upper bound on the RSDP value, with both infima taken in the extended reals.

Milestones

Lemma 3.2 (p. 37): the same implication for constant $F$ , $R$ and $\rho = 1$ , with the matrix (13).
The full-perturbation case (p. 37): for $\mathcal{D} = \mathbb{R}^{p\times q}$ and $p, q \ge 1$ , $\mathcal{B}$ consists exactly of the triples $(\tau I_p, \tau I_q, 0)$ , with $\tau \ge 0$ when $S \succeq 0$ .
Theorem 5.6 (p. 48): if $F_i = 2L_iR_i$ with $r_i = \operatorname{rank} F_i$ , and $x_{\mathrm{feas}}$ satisfies, for some $\lambda \ge 0$ and block-diagonal $S = S^T$ , $G = -G^T$ ,

\begin{bmatrix} F(x_{\mathrm{feas}}) - \lambda I - LSL^T & \tfrac12R^T + LG \\ \tfrac12R - GL^T & S\end{bmatrix} \succ 0,

then every integer vector closest to $x_{\mathrm{feas}}$ in the maximum norm satisfies $F(z) \succeq 0$ .

Significance

The result. Theorem 3.2 replaces an NP-hard semi-infinite constraint, one matrix inequality for each admissible perturbation, by a single linear matrix inequality in the enlarged variable $(x, S, T, G)$ . Every point it certifies is robustly feasible, so its optimal value is a certified upper bound on the robust optimum and its optimizer is a usable robust solution. In the full case the scalings collapse to one multiplier $\tau$ (milestone 2), which connects the bound to the exact reformulation of Section 3.1 of the paper. Theorem 5.6 shows the same machinery at work on a combinatorial problem: robustness against perturbations of size $1/2$ in each coordinate of $x$ turns an SDP-feasible point into an integer solution by rounding.

Formalizing it. The results are proved in the paper (Lemma 3.2 with the proof deferred to [16]); none of them has a machine-checked proof that this mission is aware of, and the platform has no linear-fractional or structured-perturbation results. The formalization also settles the exact form of the certificate: as printed, the matrix (13) and the LMI of Theorem 3.2 contain products that are dimensionally undefined, and this mission states the condition the proof actually yields (see the scope section).

Difficulty

The inequality to be proved is a statement about infinitely many perturbations, and $\mathbf{F}(x,\Delta)$ depends on $\Delta$ through a matrix inverse. The natural first step, eliminating $\Delta$ by an exact S-procedure as in the full case, is not available: with a structured $\mathcal{D}$ the set of pairs of vectors linked by some $\Delta \in \mathcal{D}$ is not described by one quadratic inequality, and losslessness fails. The scalings in $\mathcal{B}$ give several valid quadratic inequalities instead, and one must show that their combination controls every $\Delta$ in the norm ball, including the well-posedness claim $\det(I - D\Delta) \neq 0$ , which is part of the conclusion rather than an assumption. The commutation condition $S\Delta = \Delta T$ must be turned into an inequality for $\|\Delta\| \le 1$ , which requires more than the definition of the spectral norm. For Theorem 5.6 the block-diagonal perturbation family and the rescaling between $\rho = 1/2$ and the stated matrix must be matched to the general lemma.

Formalization scope

Matrices are Matrix (Fin a) (Fin b) ℝ; $\succ 0$ and $\succeq 0$ are Matrix.PosDef and Matrix.PosSemidef (both include symmetry); block matrices are Matrix.fromBlocks on Fin n ⊕ Fin q. The norm of a perturbation is the $\ell^2$ operator norm (open scoped Matrix.Norms.L2Operator), i.e. the largest singular value; the maximum norm in Theorem 5.6 is Mathlib's sup norm on Fin m → ℝ. $\mathcal{D}$ is a Submodule. Affine maps are given by coefficient families indexed by Fin (m+1). Mathlib's matrix inverse is $0$ at a singular matrix, so every statement pairs the LFR with $\det(I - D\Delta) \neq 0$ . The standing assumption $\rho > 0$ of Section 3 is a hypothesis.

Readings and corrections of the printed statements:

(13) as printed is dimensionally inconsistent; we state the condition the proof yields, which coincides with the printed one when $G$ is square and skew-symmetric and $\mathcal{D}$ consists of symmetric matrices. Concretely, (11) prints $G \in \mathbb{R}^{q\times p}$ with $G\Delta = -\Delta^TG^T$ and (13) prints the blocks $R - DSL - GL^T$ and $T - GD^T + DG - DSD^T$ ; the mission uses $G \in \mathbb{R}^{p\times q}$ with $G\Delta^T = -\Delta G^T$ and the blocks $R - DSL^T + G^TL^T$ and $T - DSD^T + DG + G^TD^T$ . The same correction applies to the LMI of Theorem 3.2 (with $\rho^{-2}T$ ). Theorem 5.6 is stated as printed.
"An upper bound on the RSDP (4) and a corresponding solution $x$ can be computed by solving the SDP" is read as the inclusion of the SDP's feasible projection in $\mathcal{X}_\rho$ , for every $x$ ; the goal states it with the strict conclusion $\mathbf{F}(x,\Delta) \succ 0$ as well. The value form is a separate item.
In the full-perturbation remark, "for some $\tau \ge 0$ " is stated under $S \succeq 0$ , and "We then recover the exact results of section 3.1" is not formalized.
In Theorem 5.6, $\mathcal{S}$ 's index range " $i = 1,\dots,n$ " is read as $i = 1,\dots,m$ ; the hypothesis $r_i = \operatorname{rank}F_i$ is kept.

Trivializing formalizations are ruled out: $(0,0,0) \in \mathcal{B}$ always, so the hypotheses $S \succ 0$ and $T \succ 0$ are kept outside $\mathcal{B}$ ; $\mathcal{D}$ is a subspace, not an arbitrary set; and the norm is the spectral norm, not Mathlib's default entrywise norm.

A complete development needs the square root of a positive definite matrix and its commutation with $S$ and $T$ , the spectral-norm characterization $\Delta\Delta^T \preceq \|\Delta\|^2 I$ , Schur-complement and congruence facts for block matrices, and a linear-fractional identity relating $(I - D\Delta)^{-1}$ to an auxiliary vector. These are reusable well beyond this mission; contributions of any of them, and of the value and rounding corollaries, are welcome.

Selected references

L. El Ghaoui, F. Oustry, H. Lebret, Robust Solutions to Uncertain Semidefinite Programs, SIAM J. Optim. 9(1):33–52, 1998. https://doi.org/10.1137/S1052623496305717
L. El Ghaoui, H. Lebret, Robust solutions to least-squares problems with uncertain data, SIAM J. Matrix Anal. Appl. 18:1035–1064, 1997. https://doi.org/10.1137/S0895479896298130
M. K. H. Fan, A. L. Tits, J. C. Doyle, Robustness in the presence of mixed parametric uncertainty and unmodeled dynamics, IEEE Trans. Automat. Control 36:25–38, 1991. https://doi.org/10.1109/9.62265
J. C. Doyle, Analysis of feedback systems with structured uncertainties, IEE Proc. D 129(6):242–250, 1982. https://doi.org/10.1049/ip-d.1982.0053
A. Ben-Tal, A. Nemirovski, Robust convex optimization, Math. Oper. Res. 23(4):769–805, 1998. https://doi.org/10.1287/moor.23.4.769
S. Boyd, L. El Ghaoui, E. Feron, V. Balakrishnan, Linear Matrix Inequalities in System and Control Theory, SIAM, 1994. https://doi.org/10.1137/1.9781611970777

5 thms2 active usersReviewed

Operations Research Optimization·Captain: mikedeng1

Optimizing Static Linear Feedback: Gradient Method I: The Gradient Method Converges to a Stationary Point, and Linearly to the Optimal Gain under State FeedbackResearch Paper

Motivation

The linear-quadratic regulator (LQR) is the basic problem of optimal control: steer a linear system $\dot x = Ax + Bu$ so as to minimize an integrated quadratic cost. When the full state is measured and the gain may be chosen freely, the optimal feedback is given by the algebraic Riccati equation (Kalman, 1960). In many applications only an output $y = Cx$ is measured, and the controller is restricted to a static feedback $u = -Ky$ . For this output-feedback problem no Riccati-type characterization exists; the design problem is a non-convex optimization over the gain matrix $K$ .

Direct optimization of the gain by gradient descent, known in the control literature since Levine and Athans (1970) and revived in reinforcement learning as policy gradient (Fazel, Ge, Kakade and Mesbahi, 2018, arXiv:1801.05039), is therefore of interest both to control engineers and to the learning community. Fatkhullin and Polyak (arXiv:2004.09875, SIAM J. Control Optim. 2021) give a self-contained analysis of the continuous-time problem: the cost is coercive on the set of stabilizing gains, smooth on sublevel sets, and, for state feedback, satisfies a gradient-domination (Łežanski–Polyak–Łojasiewicz) inequality. From these they derive convergence guarantees for the gradient method.

Setting

Fix real matrices $A\in\mathbb R^{n\times n}$ , $B\in\mathbb R^{n\times m}$ , $C\in\mathbb R^{r\times n}$ and weights $Q\in\mathbb R^{n\times n}$ , $R\in\mathbb R^{m\times m}$ , and an initial-state covariance $\Sigma\in\mathbb R^{n\times n}$ . A gain is a matrix $K\in\mathbb R^{m\times r}$ , and the closed-loop matrix is $A_K = A - BKC$ . A square matrix is Hurwitz if all its complex eigenvalues have negative real part. The set of stabilizing gains is

\mathcal S = \{K\in\mathbb R^{m\times r} : A_K \text{ is Hurwitz}\}.

For $K\in\mathcal S$ let $X(K)$ be the unique solution of the Lyapunov equation

A_K^\top X + XA_K + C^\top K^\top RKC + Q = 0,

and define the cost $f(K)=\mathrm{Tr}\big(X(K)\Sigma\big)$ , the expected integrated quadratic cost of the closed loop from a random initial state with covariance $\Sigma$ . With $Y(K)$ the solution of $A_KY+YA_K^\top+\Sigma=0$ , the gradient of $f$ in the Frobenius inner product is

\nabla f(K)=2\big(RKC-B^\top X(K)\big)Y(K)C^\top .

A known stabilizing gain $K_0\in\mathcal S$ is given, and $\mathcal S_0=\{K\in\mathcal S: f(K)\le f(K_0)\}$ is its sublevel set. The standing assumptions are $Q,R,\Sigma\succ0$ , $\operatorname{rank}C=r$ and $B\neq0$ . State feedback (SLQR) is the case $C=I$ .

The gradient method with step sizes $\gamma_j$ is

K_{j+1}=K_j-\gamma_j\nabla f(K_j),\qquad j\ge0 .

A number $L>0$ is a smoothness constant if $\|\nabla f(K)-\nabla f(K')\|_F\le L\|K-K'\|_F$ for all $K,K'\in\mathcal S_0$ .

Formalization targets

Goal: Theorem 4.2 for state feedback

For $C=I$ , an optimal gain $K_*\in\mathcal S$ , and any smoothness constant $L$ :

if $0<\gamma_j\le 2/L$ for all $j$ , then every $K_j\in\mathcal S_0$ and

f(K_{j+1})\le f(K_j)-\gamma_j\Big(1-\frac{L\gamma_j}{2}\Big)\|\nabla f(K_j)\|_F^2 ;

if $0<\varepsilon_1\le\gamma_j\le 2/L-\varepsilon_2$ with $\varepsilon_2>0$ , then $\nabla f(K_j)\to0$ ,

\min_{0\le j\le k}\|\nabla f(K_j)\|_F^2\le\frac{f(K_0)}{c_1k}\quad(k\ge1),\qquad c_1=\frac{\varepsilon_1\varepsilon_2L}{2},

and there are $c\ge0$ , $0\le q<1$ with $\|K_j-K_*\|_F\le c\,q^j$ .

Milestones

In attack order:

Appendix A lemmas. Trace duality of dual Lyapunov equations (Lemma A.1), the trace sandwich (Lemma A.4), and eigenvalue lower bounds for Lyapunov solutions (Lemma A.5).
Coercivity and existence. Coercivity of $f$ with the lower bounds (3.1)–(3.2) (Lemma 3.8), boundedness of $\mathcal S_0$ (Corollary 3.9), and existence of a minimizer (Corollary 3.10).
Smoothness. The gradient formula (Lemma 3.11) and existence of a smoothness constant on $\mathcal S_0$ (Theorem 3.15, qualitative form).
Gradient domination for state feedback. Lemmas C.2, C.3 and C.1, and the LPL inequality with the explicit constant (3.11):

\tfrac12\|\nabla f(K)\|_F^2\ge\mu\big(f(K)-f(K_*)\big),\qquad K\in\mathcal S_0 \qquad\text{(Theorem 3.17)}.

Theorem 4.2 for output feedback. Descent and stationarity, parts 1 and 2 without the linear rate, for general $C$ .

Significance

The theorem shows that a plain first-order method, started from any stabilizing gain, never destabilizes the closed loop and decreases the cost monotonically, for output feedback as well as state feedback. For state feedback it converges globally and linearly to the optimal gain. The cost is non-convex, and its domain $\mathcal S$ is open, possibly non-convex and unbounded, so this does not follow from convex optimization theory. It is the continuous-time counterpart of the policy-gradient guarantees of Fazel et al. for discrete-time LQR, and it underlies model-free and data-driven variants of gain tuning.

The result is proved in the paper, but it has not been formalized. The formalization adds three things. It makes the invariance argument (the iterates stay in $\mathcal S_0$ ) explicit, and the paper describes that argument as the non-trivial part. It corrects the statements where the printed text is wrong (see below). It also produces a reusable library of Lyapunov-equation facts. Mathlib has no Lyapunov equation, no LQR cost and no Hurwitz stability theory, and the platform has no continuous-time LQR material. The nearest platform items treat discrete-time Riccati iteration (BertsekasDP.riccati_convergence_stability) and Polyak–Łojasiewicz rates on a whole normed space (ShiOptRates.pl_rate). Neither applies to a function defined only on a non-convex open subset.

Difficulty

The standard descent-lemma argument assumes $f$ is defined and $L$ -smooth on the whole space. Here $f$ is defined only on $\mathcal S$ , and it is not smooth on all of $\mathcal S$ : it blows up at the boundary. A gradient step from a point of $\mathcal S_0$ could in principle jump out of $\mathcal S$ , where the Lyapunov equation has no meaningful solution. The smoothness bound is available only inside $\mathcal S_0$ , so the argument must show that the whole segment from $K_j$ to $K_{j+1}$ stays in $\mathcal S_0$ before the descent inequality can be used on it. That requires coercivity, compactness of $\mathcal S_0$ and an exit-time argument. For the linear rate, gradient domination has to be established on $\mathcal S_0$ with constants controlled by $f(K_0)$ , and passing from function values to distances to $K_*$ needs that minimizer's structure. Gradient domination fails for output feedback (the paper's Example 3.4 has two disconnected components with different minima), so the linear rate is stated only for $C=I$ .

Formalization scope

Matrices are Matrix (Fin p) (Fin q) ℝ. Hurwitz means every element of the complex spectrum has negative real part. $X(K)$ , $Y(K)$ are "the unique solution of the Lyapunov equation, $0$ if there is none or several"; this junk value is never used, because every statement evaluates $f$ and $\nabla f$ only at gains proved or assumed to lie in $\mathcal S$ . The iterates' membership in $\mathcal S_0$ is a conclusion of the goal, never a hypothesis; assuming it would delete the theorem's content. $\nabla f$ is defined by the formula (3.3), and Lemma 3.11 is the theorem that it is the gradient. $\|\cdot\|_F$ is $\sqrt{\sum M_{ij}^2}$ , $\|\cdot\|$ is the spectral (operator) norm, and $\lambda_1,\lambda_n$ are the minimum and maximum eigenvalue of a symmetric matrix. State feedback is the instance $r=n$ , $C=1$ . In (4.6) the Frobenius norm replaces the paper's spectral norm, which is equivalent because $c$ is existential. The minimum over $0\le j\le k$ requires $k\ge1$ .

Deviations from the printed text, each recorded in the item's Formalization Note:

The smoothness constant. The explicit $L$ of (3.8) is false as printed (for $n=m=1$ , $A=0$ , $B=100$ , $Q=100$ , $R=10^{-3}$ , $\Sigma=0.1$ , $K_0=10^{-6}$ , one has $f''(K_0)=2L$ ). The goal therefore takes $L$ as any Lipschitz constant of $\nabla f$ on $\mathcal S_0$ , which is the paper's definition of $L$ -smoothness (§3.6) and all that its proof uses. Theorem 3.15 enters only as "some such $L>0$ exists".
Lemma C.1. It is stated with $\lambda_1^2(\Sigma)$ in the denominator, as its proof concludes and as (3.11) requires.
Lemma A.5. It is stated for $A^\top X+XA+Q=0$ ; the printed $-Q$ admits no positive definite solution.
The gain space. $\mathcal S\subseteq\mathbb R^{m\times r}$ , where p. 3 prints $\mathbb R^{m\times n}$ .

Not stated: Theorem 4.3 and Algorithm 4.1, Lemma 3.6, Lemmas 3.12–3.14, Corollary 3.16 and the explicit constant (3.8). Welcome contributions include a Lyapunov-equation library (existence, uniqueness, integral representation, positivity), continuity of the spectrum, and the exit-time argument, which is reusable for any descent method on a sublevel set of an open domain.

Selected references

I. Fatkhullin, B. Polyak, Optimizing Static Linear Feedback: Gradient Method, SIAM J. Control Optim. 59(5), 2021; preprint arXiv:2004.09875v2. https://arxiv.org/abs/2004.09875
M. Fazel, R. Ge, S. Kakade, M. Mesbahi, Global Convergence of Policy Gradient Methods for the Linear Quadratic Regulator, ICML 2018. https://arxiv.org/abs/1801.05039
W. Levine, M. Athans, On the determination of the optimal constant output feedback gains for linear multivariable systems, IEEE Trans. Automat. Control 15(1), 1970. https://doi.org/10.1109/TAC.1970.1099363
H. Karimi, J. Nutini, M. Schmidt, Linear Convergence of Gradient and Proximal-Gradient Methods Under the Polyak–Łojasiewicz Condition, ECML PKDD 2016. https://arxiv.org/abs/1608.04636
R. E. Kalman, Contributions to the theory of optimal control, Bol. Soc. Mat. Mexicana 5, 1960.

16 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: naimengye

Stochastic Networks VII: Internet Congestion Control and the Primal AlgorithmTextbook

Motivation

When a file is transferred over the Internet, no part of the network decides how fast it should go. The machines inside the network forward packets; when a resource is heavily loaded it drops or marks one; the destination reports that to the source; and the source slows down, then gradually speeds up again until the next signal. This end-to-end cycle of increase and decrease is TCP, and it is the mechanism by which the Internet discovers available capacity and divides it among competing flows.

Chapter 7 of Frank Kelly and Elena Yudovina's Stochastic Networks (Cambridge University Press, 2014) asks what such a scheme converges to. The answer is the chapter's organizing idea: the decentralized dynamics solve a global optimization problem that no participant can see. Each source knows only its own rate and the congestion signals it receives; no machine anywhere holds the link-route incidence matrix; and yet the flow rates converge to the unique maximizer of a concave network utility, and that maximizer is the proportionally fair allocation. This is the same phenomenon as the electrical network of Chapter 4, now with the local rule chosen so that the global objective is the one we want.

Setting

A network has $J$ resources and $R$ routes, with link-route incidence matrix $A$ : $A_{jr}=1$ when route $r$ uses resource $j$ . Route $r$ carries a time-varying flow rate $x_r(t)>0$ , and the load on resource $j$ is $\sum_{s:j\in s}x_s(t)$ .

Each resource $j$ generates congestion signals at rate

\mu_j(t)=p_j\Bigl(\sum_{s:j\in s}x_s(t)\Bigr),

where $p_j$ is non-negative, continuous, increasing and not identically zero — one may read $p_j(y)$ as the probability that a packet is dropped or marked at resource $j$ under load $y$ . The primal algorithm is the response of the sources:

\frac{d}{dt}x_r(t)=\kappa_r\Bigl(w_r-x_r(t)\sum_{j\in r}\mu_j(t)\Bigr), \qquad r\in\mathcal{R}, \tag{7.5}

with $w_r,\kappa_r>0$ : a steady increase proportional to the weight $w_r$ , and a decrease proportional to the stream of congestion signals received. Both sums are local — over the resources on route $r$ , and over the routes through resource $j$ — so nothing in the network needs to know $A$ .

The network problem $\mathrm{network}(A,C;w)$ of section 7.1 is to maximize $\sum_r w_r\log x_r$ over $x\ge0$ with $Ax\le C$ , and a feasible $x$ is weighted proportionally fair when every feasible $y$ satisfies $\sum_r w_r (y_r-x_r)/x_r\le0$ .

Formalization targets

Goal — Theorem 7.6, global stability of the primal algorithm

U(x)=\sum_{r}w_r\log x_r-\sum_{j}\int_0^{\sum_{s:j\in s}x_s}p_j(y)\,dy

is a Lyapunov function for (7.5): the unique maximizer $\bar x$ of $U$ over the positive orthant is an equilibrium point, and every trajectory of the primal algorithm converges to it.

The goal asserts both halves of the book's last sentence: that $\bar x$ maximizes $U$ , and that the trajectory converges to it. It fixes no rate of convergence and no basin restriction beyond starting in the interior, which is what "global" means here.

Supporting levels

Proposition 7.4, that solving $\mathrm{network}(A,C;w)$ and being weighted proportionally fair are the same condition; strict concavity of $U$ on the positive orthant; the partial derivative $\partial U/\partial x_r=w_r/x_r-\sum_{j\in r}p_j(\cdot)$ that identifies the maximizer; the equivalence between a stationary point of $U$ and an equilibrium of (7.5); and the Lyapunov identity (7.7),

\frac{d}{dt}U(x(t))=\sum_r\frac{\kappa_r}{x_r(t)}\Bigl(w_r-x_r(t)\sum_{j\in r}p_j(\cdot)\Bigr)^2\ \ge 0 .

Significance

The result itself. Theorem 7.6 is the statement that a decentralized rule solves a centralized problem. Its practical content is that the choice of $p_j$ and $w_r$ determines what is optimized, so a protocol designer who wants a particular notion of fairness can get it by choosing the local rule accordingly — the $\alpha$ -fair family of Chapter 8 is exactly this dial. Its theoretical content is the identification of the limit: because $U$ 's first term is $\sum_r w_r\log x_r$ , the limit is the weighted proportionally fair allocation, which by Proposition 7.4 is the solution of the network problem and, by Remark 7.5, also the Nash bargaining solution and a market-clearing equilibrium. Three quite different notions of "the right allocation" coincide, and a simple end-to-end feedback rule finds it.

Formalizing it. Nothing here is open; the model and the theorem are from Kelly, Maulloo and Tan (1998). What the mission produces is a machine-checked congestion-control model — the network problem, proportional fairness, the primal dynamics and the Lyapunov function — and a statement of the convergence result in a form later work can cite. Mathlib has no network utility maximization and no congestion control.

Difficulty

The Lyapunov identity is a chain-rule computation and is not the hard part, and neither is $\frac{d}{dt}U\ge0$ . The gap the book flags explicitly is between " $U$ increases along trajectories" and " $x(t)\to\bar x$ ": a strictly increasing Lyapunov function does not by itself force convergence, because the derivative could decay fast enough for the system to stall short of the maximum. The book closes it with a compactness argument — the trajectory is trapped in $\{x: U(x)\ge U(x(0))\}$ , which is compact, and on the complement of an $\epsilon$ -ball around $\bar x$ within that set the derivative (7.7) is continuous and therefore bounded away from zero, so only finite time can be spent there. Reproducing that argument is the substance of the goal, and it needs the compactness of the sublevel set, which comes from strict concavity and the growth of $-\int_0^{y}p_j$ .

A second difficulty is one of representation rather than mathematics. The primal algorithm is an ODE, and a formal statement must say what a trajectory is. Here a trajectory is given as a differentiable function satisfying (7.5) pointwise, with positivity assumed rather than derived; deriving positivity from the dynamics is a separate (true, and welcome) result.

Formalization scope

Resources and routes are indexed by finite types and the incidence matrix is real-valued with entries constrained to $0$ or $1$ , matching the book and the convention of mission IV of this series, whose linkFlow is reused here. Flow vectors live in the positive orthant, stated as ∀ r, 0 < x r: the utility contains $\log x_r$ , which has no meaning at $x_r=0$ , and the book's own maximum is interior to the positive orthant.

The network problem's objective is maximized over the intersection of the feasible set with the positive orthant rather than over $x\ge0$ , since $\log 0$ is not a real number; the fairness condition, by contrast, is quantified over all feasible $y$ including boundary points, exactly as the book states it, and the inequality $\sum_r w_r(y_r-x_r)/x_r\le0$ is meaningful there.

A trajectory is a function of real time satisfying the derivative condition at each $t\ge0$ , and staying in the positive orthant is a hypothesis. The equilibrium $\bar x$ is given by its stationarity condition $w_r=\bar x_r\sum_{j\in r}p_j(\cdot)$ rather than by an existence claim, so the goal is about the trajectory rather than about solving the fixed-point equation; that the stationary point is the maximizer is the first conjunct of the conclusion, so nothing is assumed about it that is not also proved.

The goal cannot be satisfied vacuously: the hypotheses are jointly satisfiable — for instance one resource, one route, $p(y)=y$ , $w=\kappa=1$ , $\bar x=1$ — and the conclusion is a genuine limit.

Contributions welcome beyond the listed items: that the positive orthant is invariant under (7.5); uniqueness and existence of the max-min fair allocation; Theorem 7.2 on problem decomposition into user and network problems; Theorem 7.8, the corresponding global stability result for the TCP-like system of section 7.4; and the dual algorithm of section 7.6.

Selected references

Frank Kelly and Elena Yudovina, Stochastic Networks, Cambridge University Press, 2014, Chapter 7 (pp. 151–185); Proposition 7.4, Theorem 7.6, equations (7.4)–(7.7). DOI 10.1017/cbo9781139565363
F. P. Kelly, A. K. Maulloo and D. K. H. Tan, Rate control for communication networks: shadow prices, proportional fairness and stability, Journal of the Operational Research Society 49 (1998), 237–252. DOI 10.1057/palgrave.jors.2600523
F. P. Kelly, Charging and rate control for elastic traffic, European Transactions on Telecommunications 8 (1997), 33–37. DOI 10.1002/ett.4460080106
J. F. Nash, The bargaining problem, Econometrica 18 (1950), 155–162. DOI 10.2307/1907266
S. H. Low and D. E. Lapsley, Optimization flow control I: basic algorithm and convergence, IEEE/ACM Transactions on Networking 7 (1999), 861–874. DOI 10.1109/90.811451

8 thms2 active usersReviewed

Completed

Functional Analysis·Captain: olivier

Fading Memory and Approximation of Nonlinear Operators (Boyd & Chua, 1985)Research Paper

Motivation

A recurrent network, a nonlinear filter, a physical transducer: all are operators carrying an input signal to an output signal. Approximating such an operator — not a function on $\mathbb{R}^n$ , but a map between signal spaces — is the question behind every claim that a recurrent architecture is "universal".

In 1985 Boyd and Chua gave the answer that still underpins the field. They isolated fading memory as the exact continuity notion required, and proved that a time-invariant operator with fading memory can be approximated by a finite Volterra series — uniformly over an infinite time horizon and over a noncompact set of signals. Both italicised words mark the break with what was available before: the classical Volterra approximation theorems hold only on a finite interval $[0,T]$ and only on a compact set of inputs, which rules out most signals of engineering interest.

This is the result reservoir computing inherits. Every modern universality theorem for echo state networks, state-affine systems, or linear-dynamics-plus-polynomial-readout architectures proceeds by showing the architecture realises enough of these operators, then invokes Boyd–Chua. Formalising it turns the foundation of those arguments into machine-checked mathematics.

Timeline.

1958 — Volterra series are the standard tool for weakly nonlinear systems, but the available approximation theorems are confined to a finite interval and a compact input set.
1985 — Boyd and Chua identify fading memory and remove both restrictions. Theorem 1 is the continuous-time statement; Theorems 3 and 4 are its discrete-time counterparts.
2001 — Jaeger introduces echo state networks; the echo state property is the well-posedness half of the same picture.
2018 — Grigoryeva and Ortega prove universality for reservoir computers by reducing to Boyd–Chua.

Setting

Following the convention of the published ReservoirESN definitions, the index counts steps into the past: $u_k$ (discrete) or $u(t)$ (continuous) is the value of the signal $k$ steps, or $t$ units of time, before the present. A sequence or function is therefore the complete history of a signal up to now. Under this convention every operator below is causal.

A weighting is a map $w$ decreasing to zero with values in $(0,1]$ , and the weighted norm is $\lVert u \rVert_w = \sup_{t \ge 0} \lvert u(t)\rvert\, w(t)$ — the distant past is discounted.

An operator $N$ is time-invariant when its value at any instant is its present-time value applied to the shifted history, $(Nu)(r) = \big(N(\sigma^r u)\big)(0)$ with $(\sigma^r u)(t) = u(t+r)$ . It has fading memory on a set $K$ when its present-time functional $u \mapsto (Nu)(0)$ is $\lVert\cdot\rVert_w$ -continuous on $K$ . The quantifier order is taken verbatim from the source: $\delta$ may depend on the input $u$ as well as on $\varepsilon$ , so this is pointwise continuity — formally weaker than the uniform version ReservoirESN.FunctionalFMP already on the platform.

In continuous time the admissible inputs are the bounded, slew-limited signals

K = \{\, u \;:\; \lvert u(t)\rvert \le M_1,\quad \lvert u(s)-u(t)\rvert \le M_2\,\lvert s-t\rvert \,\},

and the approximating functionals are the convolutions $G_g u = \int_0^\infty g(t)\,u(t)\,dt$ with $\int_0^\infty \lvert g\rvert/w < \infty$ .

Goal — Theorem 1

Let $\varepsilon > 0$ and let $N$ be any time-invariant operator with fading memory on $K$ . Then there are finitely many admissible kernels $g_1,\dots,g_m$ and a polynomial $p : \mathbb{R}^m \to \mathbb{R}$ such that

\sup_{u \in K}\ \sup_{r \ge 0}\ \Big\lvert (Nu)(r) - p\big(G_{g_1}\sigma^r u,\ \dots,\ G_{g_m}\sigma^r u\big) \Big\rvert \ \le\ \varepsilon.

That is: a bank of linear filters followed by a polynomial readout — the architecture of Fig. 3 of the paper, and, recognisably, the architecture of a reservoir computer. The goal is stated in this form rather than as an explicit Volterra kernel expansion; expanding a polynomial in convolutions into Volterra kernels is a purely algebraic restatement, and formalising Volterra kernels would add bookkeeping without adding mathematical content. The approximation is uniform over all of $K$ at once and over all time at once, and $K$ is not compact in the sup norm — the whole point of fading memory is that it makes $K$ behave as though it were.

Milestones

The decomposition follows the paper: the discrete-time chain first (Section VI and Appendix A2), then the two continuous-time lemmas the goal rests on (Section IV and Appendix A1).

1 — Damping, and compactness of the discrete ball. On the $\ell^\infty$ ball, closeness over a finite horizon already forces closeness in weighted norm; consequently the weighted topology and the product topology coincide there, and the ball is compact by Tychonoff. This is the discrete analogue of Lemma A1, and the only place where $w \to 0$ is used.

2 — Theorem 4, the discrete NLMA approximation. Fading memory becomes topological continuity on that compact ball; the delay functionals $u \mapsto u_k$ separate points; Stone–Weierstrass then yields a nonlinear moving average — a polynomial read from a finite window, $(\widehat{N}u)_k = p(u_k,\dots,u_{k+m-1})$ — approximating $N$ uniformly. Boyd and Chua note this implies Theorem 3, the discrete finite-Volterra statement.

3 — Lemma 1: compactness in continuous time. The bounded slew-limited set is compact for the weighted norm. The source proves it by Arzelà–Ascoli on each interval $[-n,0]$ followed by a diagonal extraction; the slew limit is exactly the equicontinuity that makes this work, and it is required here — the discrete case needs no analogue, as the paper remarks.

4 — Lemma 2: the convolution functionals separate points. Admissible kernels give $\lVert\cdot\rVert_w$ -continuous functionals, and they separate: for $u \neq v$ the kernel $g_0(t) = (u(t)-v(t))\,w(t)\,e^{-t}$ is admissible and $G_{g_0}u - G_{g_0}v = \int_0^\infty (u-v)^2 w\, e^{-t} > 0$ .

Goal. Stone–Weierstrass on the compact set of milestone 3 with the separating family of milestone 4, then time-invariance to transport the estimate to every instant.

What is already available

The companion missions on reservoir computing have published, machine-checked, the definitions reused here — UnifBdd, WeightedBound, IsWeighting, FunctionalFMP — along with WeightedCompact.unifBdd_tendsto_subseq, a weighted sequential-compactness result for the discrete ball. Solvers can build on those rather than restate them.

Why this is not routine

Mathlib has Stone–Weierstrass in the form needed (ContinuousMap.subalgebra_topologicalClosure_eq_top_of_separatesPoints, which asks only for CompactSpace), and it has Arzelà–Ascoli in an abstract uniform-space form. What it has nothing about is fading memory, weighted norms on signal spaces, Volterra series, Laguerre systems, or moving-average operators. The work is the bridge: turning a weighted-norm continuity hypothesis into a topological statement Mathlib's Stone–Weierstrass will accept, extracting a genuine MvPolynomial from an abstract density result, and — for the goal — assembling a compactness proof in continuous time from Mathlib's Ascoli machinery.

Two modelling points are load-bearing and stated plainly rather than buried. The discrete ball must be taken in scalar (or finite-dimensional) signals: for infinite-dimensional values it is not compact and the theorem fails. And in continuous time the slew limit cannot be dropped: without equicontinuity the set is not compact in any topology that makes the convolution functionals continuous.

Source

S. Boyd and L. O. Chua, Fading memory and the problem of approximating nonlinear operators with Volterra series, IEEE Transactions on Circuits and Systems, vol. CAS-32, no. 11, pp. 1150–1161, November 1985.

6 thms2 active usersReviewed

Analysis Dynamic Programming Operations Research·Captain: mikedeng1

Wait Time Based Pricing for Queues with Customer-Chosen Service Times: The Delay Differential Optimality Equations Have a Decreasing Concave SolutionResearch Paper

Motivation

Service systems such as public fast-charging stations for electric vehicles let each customer choose how long to be served. Lin, Shang and Sun (SSRN 3709573, 2020; later in Management Science, doi:10.1287/mnsc.2022.4474) study a firm that announces to every arriving customer the current wait time $w$ (the work already in the queue) and a price rate $p$ per unit of service time. The customer then decides whether to join and, if so, how long a service to buy. Queue pricing usually conditions on the queue length with random service times (Low 1974; Paschalidis and Tsitsiklis 2000; Kim and Randhawa 2018). Here the state is the wait time, and it moves deterministically between arrivals.

The firm maximizes long-run average revenue or social welfare. The optimality condition the paper derives is not an ordinary differential equation but a delay differential equation (DDE) that looks ahead: the value at $w$ depends on the value at $w + \mathtt t(p) > w$ . This mission formalizes the paper's existence theorem for that equation.

Setting

A model has a usage utility $U$ , a waiting cost $c$ , a Poisson arrival rate $\lambda > 0$ and a maximum service time $C > 0$ , under Assumption 1 (p. 7):

$U(t) \ge 0$ , $U(0) = 0$ , $0 \le U'(t) \le U'(0)$ and $U''(t) < 0$ on $[0, C]$ ;
$\frac{d^2}{dt^2}[U'(t)t] < 0$ on $[0, C]$ ;
$c(0) = 0$ , $c'(w) > 0$ and $c''(w) \ge 0$ for $w \ge 0$ .

At price $p \in [0, U'(0)]$ a joining customer chooses the service time $\mathtt t(p) = \min\{(U')^{-1}(p), C\}$ (5). They join when $U(\mathtt t(p)) - p\,\mathtt t(p) - c(w) \ge 0$ . Three thresholds follow:

$\bar w$ solves $U(C) = c(\bar w)$ ; above it nobody joins.
$\Gamma(w)$ , for $w \in [0, \bar w]$ , is the highest price at which a customer still joins (Proposition 2).
$\hat w$ and $L(w)$ (Proposition 1) describe when the marginal price $U'(t)$ still attracts a customer.

The per-customer value is $\mathbf v(p) - \alpha c(w)$ , with $\mathbf v(p) = p\,\mathtt t(p)$ , $\alpha = 0$ for revenue and $\mathbf v(p) = U(\mathtt t(p))$ , $\alpha = 1$ for welfare (Lemma 1).

The optimality equations (12)–(15) ask for a constant $\mathsf g$ (the average rate) and a relative value function $V$ with

\mathsf g = -V'(w) + \lambda \max\Big\{\max_{p \in [0, \Gamma(w)]} \big[\mathbf v(p) - \alpha c(w) + V(w + \mathtt t(p)) - V(w)\big],\ 0\Big\}, \quad w \in (0, \bar w],

\mathsf g = \lambda \max\Big\{\max_{p \in [0, \Gamma(0)]} \big[\mathbf v(p) + V(\mathtt t(p)) - V(0)\big],\ 0\Big\}, \qquad \mathsf g = -V'(w) \ (w > \bar w), \qquad V(\bar w) = 0.

Algorithm 1 (p. 14) is a backward explicit-Euler shooting scheme. For a guess $g \ge 0$ and $N$ grid cells on $[0, \bar w]$ , it starts from $V^g_N(w) = -(w - \bar w)g$ for $w \ge \bar w$ . It then builds a piecewise-linear $V^g_N$ cell by cell from right to left. On the cell ending at $x$ the slope is $-g + K^g_N(x)$ , where the slope adjustment $K^g_N(x)$ is $\lambda$ times the positive part of the inner maximum at $x$ . The shooting value is $g_N = \min\{g \ge 0 : g \ge K^g_N(0)\}$ (23). Finally $\bar g = \lim_j g_{2^j}$ (24) and $V^{\bar g}(w) = \lim_j V^{\bar g}_{2^j}(w)$ (Proposition 6).

Formalization targets

Goal: Theorem 1 (p. 17)

\bar g = \lim_{j\to\infty} g_{2^j} \ \text{exists},\quad V^{\bar g}_{2^j}(w) \to V^{\bar g}(w)\ (w \ge 0),\quad (\bar g, V^{\bar g}) \text{ solves (12)–(15)},\quad V^{\bar g} \text{ is nonincreasing and concave on } [0, \bar w + C].

Milestones

The milestones follow the paper's proof in order:

Thresholds and the value function (Propositions 1–3, pp. 8–11): uniqueness of $\hat w$ and $\bar w$ , the characterization (8) of $\Gamma$ , $\Gamma(0) = U'(0)$ with $\Gamma$ decreasing, and the bounds (V1)–(V2) on $\mathbf v$ .
The finite- $N$ scheme (Proposition 4, Lemmas 2, 3, 5): $V^g_N$ is concave and $K^g_N$ is nonincreasing; $K$ increases when the grid is refined and decreases in $g$ ; and $K^{U'(0)}_N \equiv 0$ .
The limits (Proposition 5, Lemma 6, Proposition 6): $g_{2^j}$ increases to $\bar g \le U'(0)$ , the $V^{\bar g}_{2^j}$ are uniformly $\bar g$ -Lipschitz, and they converge uniformly to a concave, nonincreasing, Lipschitz $V^{\bar g}$ .
The equations in the limit (Lemma 7, Propositions 7–8): $K^{\bar g}_{2^j}(0) \to \bar g$ ; the boundary condition (13); differentiability of $V^{\bar g}$ on $[0, \bar w]$ and the DDE (12).

Significance

Theorem 1 is the existence half of the paper's verification argument. Its Theorem 2 then shows that the constructed $\bar g$ equals the optimal long-run average rate over all predictable price processes. Its Theorem 3 reads the structure of the optimal price and service-time policies off $V^{\bar g}$ . Without a solution of (12)–(15) neither result has an object to talk about. The construction also gives a convergent numerical method (Algorithm 1) for a class of look-ahead DDEs that standard ODE theory does not cover.

The proofs are written out in the paper's Appendix B, except Lemma 12, an internal step of Proposition 8 whose proof the authors leave out. None of it is machine-checked. A complete formalization would check every step of the shooting argument and supply the omitted lemma. It would also yield a reusable framework: Euler-type schemes for delay equations whose delay points forward, monotone in the grid and in a scalar parameter.

Difficulty

The obvious approach, Cauchy–Lipschitz, fails: (12) is not an initial-value problem. $V'(w)$ depends on $V$ on $[w, w + C]$ , so the equation must be integrated backwards from $\bar w$ , and then the value $\mathsf g$ is unknown. The shooting scheme fixes $g$ , integrates backwards, and tunes $g$ so that the boundary condition (13) at $w = 0$ holds in the limit. For fixed $g$ the approximations need not converge as $N \to \infty$ (the slope at $0$ can diverge), so $g$ and $N$ must be coupled through $g_N$ .

The hard step is Proposition 8. Each $V^{\bar g}_{2^j}$ has kinks at every grid point, yet the limit has to be differentiable. One has to show that the left and right derivatives of the concave limit coincide and equal the right-hand side of (12), which requires passing a maximum over a $w$ -dependent price set to the limit.

Formalization scope

All declarations live in the namespace WaitTimePricing.Existence, and only Mathlib is imported. Conventions:

$U, c : \mathbb R \to \mathbb R$ are $C^3$ and $C^2$ on $\mathbb R$ , a disclosed strengthening of "three/two times differentiable". Assumption 1's inequalities are imposed exactly on $[0, C]$ and $[0, \infty)$ . $\lambda > 0$ and $C > 0$ are added; the paper uses them without stating them.
$\mathtt t(p) = \sup\{t \in [0, C] : p \le U'(t)\}$ , meaningful for $p \in [0, U'(0)]$ . $\hat w$ , $L(w)$ , $\bar w$ and $\Gamma(w)$ are defined by their characterizing sets, not by closed forms. Propositions 1–2 are theorems about these sets.
The objective is one of Lemma 1's two cases. The paper's remark that any $\mathbf v$ satisfying (V1)–(V2) would do is not formalized, because it silently needs continuity of $\mathbf v$ .
Every "max" in (12), (13), (19) and (22) is a real supremum over $[0, \Gamma(w)]$ . For the continuous $V$ used here this set is nonempty and bounded, and the supremum is attained.
$V'$ is never a default-valued derivative. (12) and (14) assert that $V$ has the prescribed derivative, two-sided for $w \in (0, \bar w]$ and $w > \bar w$ ; Proposition 8 states the case $w = 0$ with a right derivative.
Algorithm 1 is a recursion over the passes of its loop, with $N \ge 1$ . The initialization (16) is extended from $[\bar w, \bar w + C]$ to $[\bar w, \infty)$ so that (14) can hold as printed on $(\bar w, \infty)$ . Only values on $[0, \bar w + C]$ enter the loop, so the construction is unchanged.
$\bar g$ and $V^{\bar g}$ are defined as limits that take a default value when the limit does not exist. Propositions 5–6 and the goal assert the convergence.
"Decreasing" is nonincreasing everywhere (including $\Gamma$ , Proposition 2(iii)), the reading the proofs establish.

Trivializations ruled out. The goal names the paper's $\bar g$ and $V^{\bar g}$ together with their convergence, not an arbitrary solution and not default values of undefined limits. It cannot be met at a kink through a default-valued derivative. Its inner maxima cannot vanish through an empty or unbounded set. $\Gamma$ and $\mathtt t$ are not closed forms that would make (8) true by definition. The weaker statement "some $(\mathsf g, V)$ solves (12)–(15)" is not the goal.

Contributions are welcome at every milestone. Reusable pieces include monotonicity of a max-operator under backward induction, Dini-type uniform convergence of monotone sequences of equi-Lipschitz concave functions, and the differentiability of a concave limit of piecewise-linear functions. Theorem 2 (optimality over predictable controls) and Theorem 3 (policy structure) are outside this mission. Theorem 3 appears to fail as printed when $\bar g > U'(C)$ .

Selected references

C.-A. Lin, K. Shang, P. Sun, Wait Time Based Pricing for Queues with Customer-Chosen Service Times, SSRN 3709573, version of October 12, 2020. https://ssrn.com/abstract=3709573 (journal version: Management Science, https://doi.org/10.1287/mnsc.2022.4474)
D. W. Low, Optimal dynamic pricing policies for an M/M/s queue, Operations Research 22(3), 1974. https://doi.org/10.1287/opre.22.3.545
I. C. Paschalidis, J. N. Tsitsiklis, Congestion-dependent pricing of network services, IEEE/ACM Transactions on Networking 8(2), 2000. https://doi.org/10.1109/90.842140
J. Kim, R. S. Randhawa, The value of dynamic pricing in large queueing systems, Operations Research 66(2), 2018. https://doi.org/10.1287/opre.2017.1668
D. P. Bertsekas, Dynamic Programming and Optimal Control, 2nd ed., Athena Scientific, 2000. http://www.athenasc.com/dpbook.html

19 thms1 active userReviewed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

An Approximate Analysis of Dynamic Pricing, Outsourcing, and Scheduling Policies for a Multiclass Make-to-Stock Queue in the Heavy Traffic Regime: The Two-Barrier Drift-Rate Control Policy Is OptimalResearch Paper

Motivation

A manufacturer that makes several products to stock for price-sensitive customers controls three levers at once: the prices it posts, which shape demand; outsourcing, which clears a large backlog at a cost; and scheduling, which decides which product the single server makes next. Ata and Barjesteh (Operations Research 71(1), 2023) study this multiclass make-to-stock queue in the heavy-traffic regime, where the queue is nearly saturated and the system is approximated by a Brownian control problem. The approximation collapses to a one-dimensional problem in the workload, the total amount of work in the system. Its solution is a two-barrier policy whose state-dependent drift translates back into a dynamic pricing rule, an outsourcing threshold and a scheduling priority (§7 of the paper).

The one-dimensional problem belongs to the family of drift-rate control problems for Brownian motion under a long-run average cost criterion (Ata, Harrison and Shepp, Ann. Appl. Probab. 2005; Rubino and Ata, Oper. Res. 2009). Problems of this kind are solved by a Bellman equation with free boundaries and a verification argument; the present paper adds two-sided singular control (outsourcing at the bottom, idling at the top) to a quadratic drift cost and a piecewise linear state cost.

Setting

There are $K\ge1$ products with mean production times $m_k>0$ and holding, backorder and outsourcing cost rates $h_k,b_k,r_k>0$ . A symmetric positive definite matrix $H$ describes the curvature of the revenue rate. Write $a=m'H^{-1}m$ and

h^\star=\min_k\frac{h_k}{m_k},\qquad b^\star=\min_k\frac{b_k}{m_k},\qquad \kappa=\min_k\frac{r_k}{m_k}.

The drift cost and the effective holding cost are

c(x)=\min\{\zeta'H\zeta:\ m'\zeta=x\},\qquad h(w)=h^\star w\ (w\ge0),\quad h(w)=-b^\star w\ (w<0).

Let $B$ be a Brownian motion with drift $\mu\ge0$ and variance $\sigma^2>0$ , started at $0$ , with respect to a filtration $\mathbb F$ . An admissible control consists of a progressively measurable drift rate $\theta$ and nondecreasing, right-continuous, adapted processes $L$ (effective outsourcing) and $U$ (idleness) with $L(0)=U(0)=0$ . The workload is

W(t)=B(t)-\int_0^t\theta(s)\,ds-U(t)+L(t),

and admissibility also requires $\mathbb E|W(t)|/t\to0$ . The equivalent workload formulation (EWF) is to minimize

\limsup_{t\to\infty}\frac1t\,\mathbb E\Big[\int_0^tc(\theta(s))\,ds+\int_0^th(W(s))\,ds+\kappa L(t)\Big]. \tag{29}

A barrier policy with barriers $l<u$ keeps $W$ in $[l,u]$ , increases $L$ only when $W=l$ and $U$ only when $W=u$ .

For $\gamma\ge0$ put $l_\gamma=-\frac1{b^\star}(\gamma+\mu\kappa+\frac a4\kappa^2)$ and $u_\gamma=\gamma/h^\star$ . Let $v^-_\gamma$ solve the Riccati equation

v'=\frac a{2\sigma^2}(v^2-\kappa^2)-\frac{2\mu}{\sigma^2}(v+\kappa)+\frac{2(h(l_\gamma)-h(w))}{\sigma^2}\ \text{on }[l_\gamma,0],\qquad v(l_\gamma)=-\kappa,

and $v^+_\gamma$ solve $v'=\frac a{2\sigma^2}v^2-\frac{2\mu}{\sigma^2}v+\frac{2(h(u_\gamma)-h(w))}{\sigma^2}$ on $[0,u_\gamma]$ with $v(u_\gamma)=0$ . The paper's $\gamma^\star$ is the unique $\gamma$ with $v^-_{\gamma}(0)=v^+_{\gamma}(0)$ ; $v$ pastes $v^-_{\gamma^\star}$ and $v^+_{\gamma^\star}$ at $0$ , and the candidate drift is $\theta(w)=\frac a2v(w)$ .

Formalization targets

Goal: Theorem 1

For every filtered probability space carrying such a Brownian motion,

\lim_{t\to\infty}\frac{J_{\text{cand}}(t)}t=\gamma^\star\quad\text{for every barrier policy at }(l_{\gamma^\star},u_{\gamma^\star})\text{ with drift }\theta(W),\qquad \limsup_{t\to\infty}\frac{J(t)}t\ge\gamma^\star\ \text{for every admissible control},

where $J$ is the expected cumulative cost in (29). The constant $\gamma^\star$ is the paper's construction, not a parameter.

Milestones

Lemma 1 and Lemma 2: the closed forms $c(x)=x^2/a$ and its conjugate $\varphi(y)=\frac a4y^2$ , maximized at $\psi(y)=\frac a2y$ .
Proposition 2: a barrier policy whose $(\gamma,f)$ solves the ODE (35)–(36) has long-run average cost $\gamma$ .
Lemma 3: any solution of the Riccati-form Bellman equation (43)–(45) has $\gamma>0$ , $l=l_\gamma<0$ , $u=u_\gamma>0$ .
Lemmas 18–20 and Corollary 6: sign and monotonicity of the Riccati solutions.
§6.3 well-posedness, Lemma 4(i)–(ii), Corollary 1: uniqueness of $v^\pm_\gamma$ , their monotone dependence on $\gamma$ , and the unique crossing $\gamma^\star$ .
Proposition 3 and Corollary 2: $(l_{\gamma^\star},u_{\gamma^\star},\gamma^\star,v)$ is the unique solution of (43)–(45), and $f=\int v$ solves the Bellman equation (37)–(39), uniquely up to a constant.

Significance

The theorem identifies an explicit optimal policy for a two-sided singular drift-control problem: two barriers and a strictly increasing, non-positive drift, all determined by a scalar root $\gamma^\star$ of a monotone equation. In the paper it drives the proposed pricing, outsourcing and scheduling policy (§7) and its asymptotic analysis; the Riccati structure is what makes $\gamma^\star$ computable by line search.

The result is proved in the paper; none of it has been machine-checked. Formalizing it gives a checked verification theorem for an average-cost Brownian control problem with singular controls, and checked statements of the Riccati comparison lemmas on which it rests. Several printed statements of the paper are corrected here (see the scope section), so the formal versions are the first fully precise ones.

Difficulty

The optimality half of Theorem 1 is a verification argument: apply Itô's formula to $f(W(t))$ for an arbitrary admissible control with jumps in $L$ and $U$ , use the Bellman inequality pointwise, and control $\mathbb E f(W(t))/t$ with the growth condition (32). Mathlib does not yet have Itô's formula for continuous semimartingales with finite-variation, possibly discontinuous parts, and the candidate's average cost (Proposition 2) needs the same tool plus the fact that a reflected diffusion spends zero time at the barriers.

The deterministic half is not routine either. The obvious reading of the paper, solving each Riccati problem for every $\gamma\ge0$ and passing $\gamma\to\infty$ , fails: the solutions blow up in finite time, so $v^\pm_\gamma$ exist only for $\gamma$ in a bounded initial interval, and the crossing argument must be run on that interval. The comparison arguments of Lemmas 18–20 also need second derivatives of solutions whose right-hand side has a kink at $w=0$ .

Formalization scope

Time is indexed by $\mathbb R$ and only $t\ge0$ matters. The Brownian motion is defined locally (drift, variance, start at $0$ , independence of increments from the filtration). Expected costs are computed in $[0,\infty]$ , so a control with infinite cost counts as $+\infty$ . The integrals in (34) are Lebesgue–Stieltjes integrals against the paths of $L$ and $U$ , jumps included. Derivatives at the barriers are one-sided; $C^1$ and $C^2$ up to the boundary are ContDiffOn on the closed interval. Minima and maxima (in $c$ , (37), (40)) are stated as attained.

Standing assumptions added to every statement, all implicit in the paper: $K\ge1$ ; $m_k,h_k,b_k,r_k>0$ ; $H$ symmetric positive definite; $\mu\ge0$ , $\sigma>0$ ; $B$ starts at $0$ ; $L,U$ right-continuous; $\theta$ progressively measurable with locally integrable paths; $l<u$ in the Bellman equations.

Corrected statements. Lemmas 18–20 are printed for solutions on $[0,\infty)$ , which do not exist; they are posed on every bounded interval where a solution exists. The §6.3 claim that $v^\pm_\gamma$ exist for every $\gamma\ge0$ is replaced by uniqueness, solvability at $\gamma=0$ and order-connectedness of the solvability sets. Lemma 4's limits as $\gamma\to\infty$ become unboundedness on those sets. Theorem 1's comparison class is every admissible control, which the paper's proof treats, and which contains the stationary Markov policies to which §6 restricts attention.

Not posed. The existence of the reflected diffusion realizing the candidate policy is presupposed by the paper and not claimed: the first half of the goal quantifies over all barrier policies with the given data. The second half is a statement about every admissible control and is not vacuous.

$\gamma^\star$ , $v$ , $f$ and $\theta$ are built from the Riccati solutions by choice, exactly as the paper constructs them; taking them as hypotheses-constrained parameters, or defining $c$ by its closed form, would trivialize the goal and is ruled out. Contributions are welcome on the Riccati lemmas (pure real analysis, reusable for other drift-control problems), on Itô's formula for semimartingales with finite-variation parts, and on Skorokhod-type existence of reflected diffusions.

Selected references

B. Ata and N. Barjesteh, An Approximate Analysis of Dynamic Pricing, Outsourcing, and Scheduling Policies for a Multiclass Make-to-Stock Queue in the Heavy Traffic Regime, Operations Research 71(1):341–357, 2023. https://doi.org/10.1287/opre.2022.2361 (accepted manuscript: https://ssrn.com/abstract=3464763)
B. Ata, J. M. Harrison and L. A. Shepp, Drift rate control of a Brownian processing system, Annals of Applied Probability 15(2):1145–1160, 2005. https://doi.org/10.1214/105051604000000855
M. Rubino and B. Ata, Dynamic control of a make-to-order, parallel-server system with cancellations, Operations Research 57(1):94–108, 2009. https://doi.org/10.1287/opre.1080.0532
J. M. Harrison, Brownian Models of Performance and Control, Cambridge University Press, 2013. https://doi.org/10.1017/CBO9781139087698

18 thms1 active userReviewed

Dynamic Programming Operations Research Stochastic Systems·Captain: mikedeng1

A Dynamic Model for Managing Volunteer Engagement I: The Bellman Equation of the Drift-Rate Control Problem Has a SolutionResearch Paper

Motivation

Non-profit organizations depend on volunteers whose availability they cannot schedule. They can only influence it, through recruiting drives, reminders and recognition events. Ata, Tongarlak, Lee and Field (arXiv:2312.02920) model a food-recovery non-profit's volunteer pool as a queueing network. Repeat volunteers rest between shifts, one-time volunteers arrive at random, and all signed-up volunteers wait on one sign-up list, from which they may abandon. The organization pays for engagement activities that speed up volunteers' return, and it is penalized when tasks go uncovered because the list is empty.

In heavy traffic the problem reduces to a one-dimensional drift-rate control problem. A workload process $W \ge 0$ behaves like a reflected Ornstein–Uhlenbeck process whose drift $\theta(t)$ the controller chooses from an interval $A = [\theta_0, \theta_L]$ at cost $c(\theta(t))$ , plus a penalty $p$ per unit of idleness at $W = 0$ . The analytic core of the paper is the Bellman equation of this problem: a first-order ordinary differential equation on $[0,\infty)$ with an unknown constant. Its solution yields the optimal long-run average cost and a nested threshold policy for when to run each engagement activity.

Setting

There are $L \ge 1$ engagement activities. The data are a lowest drift $\theta_0 < 0$ , drift increments $\eta_1, \dots, \eta_L > 0$ , per-unit-drift costs $0 < c_1 < c_2 < \dots < c_L < p$ , an idleness cost rate $p > 0$ , a mean-reversion rate $\kappa > 0$ and a volatility $\sigma > 0$ . The breakpoints are

\theta_l = \theta_0 + \sum_{i=1}^{l} \eta_i, \qquad l = 0, 1, \dots, L,

and $A = [\theta_0, \theta_L]$ . The engagement cost $c : A \to \mathbb{R}_+$ is piecewise linear and convex: $c(\theta_0) = 0$ , with slope $c_l$ on $(\theta_{l-1}, \theta_l]$ , so that $c(x) = \sum_{i=1}^{l-1} c_i \eta_i + c_l (x - \theta_{l-1})$ for $\theta_{l-1} < x \le \theta_l$ . Its convex conjugate is

\phi(y) = \sup_{x \in A} \{ y x - c(x) \}, \qquad y \in \mathbb{R}.

The Bellman equation (68)–(69) asks for a constant $\beta > 0$ and a continuously differentiable function $v$ on $[0,\infty)$ such that

\beta = \tfrac12 \sigma^2 v'(x) + x\kappa\,(p - v(x)) - \phi(p - v(x)), \qquad x \ge 0,

with $v(0) = 0$ , $v$ strictly increasing, and $\lim_{x\to\infty} v(x) = p$ .

The milestones use the shooting objects of the paper's Online Supplement §F:

the lower bound $\underline\beta = -\inf\{\phi(y) : y \le p\}$ ;
the initial value problem IVP( $\beta$ ): the same equation with only the condition $v(0) = 0$ ; its solution is $v_\beta$ ;
the set $\mathcal I$ of $\beta > \underline\beta$ for which $v_\beta$ is increasing;
the set $\mathcal D$ of $\beta > \underline\beta$ for which $v_\beta$ is nondecreasing on $(0, x_\beta)$ and nonincreasing on $(x_\beta, \infty)$ for some $x_\beta$ ;
the constant $\beta^* = \inf \mathcal I$ .

Formalization targets

Goal: Theorem 1 (p. 21)

\exists\, \beta > 0,\ \exists\, v \in C^1[0,\infty):\quad \beta = \tfrac12\sigma^2 v' + x\kappa(p - v) - \phi(p - v)\ \ (x \ge 0),\quad v(0) = 0,\quad v \uparrow,\quad v(x) \to p.

The goal asserts existence only. It does not identify $\beta$ with $\inf\mathcal I$ , and it does not claim uniqueness.

Milestones (Online Supplement §F, in attack order)

$\underline\beta > 0$ (OS p. 13).
Lemma 3: $\phi$ is Lipschitz with constant $\max_{0\le k\le L} |\theta_k|$ .
Lemma 4: IVP( $\beta$ ) has a unique $C^1$ solution on $[0,\infty)$ for $\beta > \underline\beta$ .
Lemma 6: $v_\beta(x)$ is strictly increasing in $\beta$ for $x > 0$ and continuous in $\beta$ .
Corollary 2: $v_\beta$ has no flat pieces.
Lemmas 10, 12, 15, 16: descriptions of $\mathcal D$ . Membership in $\mathcal D$ is equivalent to $v_\beta' < 0$ somewhere, to $v_\beta < 0$ somewhere, and to $v_\beta \to -\infty$ . $\mathcal D$ is closed downward.
Lemmas 13, 14: $\mathcal I, \mathcal D \ne \emptyset$ , and a characterization of the solutions in $\mathcal I$ that overshoot $p$ .
Lemmas 17, 18, 20: $\beta^* > \underline\beta$ , $\beta^* \in \mathcal I$ with $v_{\beta^*}$ bounded, and $v_{\beta^*}(x) \to p$ .
Corollary 4: $(\beta^*, v_{\beta^*})$ solves (68)–(69).

Significance

The Bellman equation is what makes the paper's policy computable. Theorem 1 provides the constant $\beta^*$ , which the paper's Theorem 2 identifies as the optimal long-run average cost of the workload problem. It also provides the increasing function $v$ , whose level sets $\tau_l = v^{-1}(p - c_l)$ are the thresholds of the optimal nested policy: engagement activity $l$ is used when the workload is below $\tau_l$ . The companion mission (II) gives $v$ in closed form between consecutive thresholds. Both results presuppose the existence proved here.

The paper proves Theorem 1 in its Online Supplement, partly by citation: Lemma 4 is called standard and its proof is omitted. As far as is known, none of these statements has a machine-checked proof. A formalization would also settle two points that the printed argument leaves loose. The lower bound $\underline\beta$ is written as an infimum over all of $\mathbb{R}$ , which is $-\infty$ when $\theta_L < 0$ . And one step in the proof of Lemma 9 claims that a set of positive measure contains an interval, which is false; the formal chain avoids this step by posing Corollary 2 directly.

Difficulty

The equation is first order but nonlinear through $\phi$ , and it is posed on an unbounded interval with a boundary condition at infinity. A local existence theorem does not suffice: the right-hand side has linear growth with a coefficient that grows with $x$ , so global existence on $[0,\infty)$ and monotone, continuous dependence on $\beta$ must be established separately.

The main difficulty is the shooting step. For a fixed $\beta$ the initial value problem has a solution, but it generally fails the condition $v(x) \to p$ : either it eventually turns down and tends to $-\infty$ , or it crosses $p$ and grows without bound. The proof must show the following:

the parameter range splits cleanly into these two behaviours, with no third behaviour such as a plateau or a limit strictly between $0$ and $p$ ;
both behaviours occur;
at the infimum $\beta^*$ of the increasing regime, the solution is increasing and bounded and converges exactly to $p$ .

Continuity in $\beta$ alone does not give the last point: it needs a separate argument at infinity.

Formalization scope

Everything is stated for one fixed parameter set satisfying an explicit predicate Standing: $L \ge 1$ , $\theta_0 < 0$ , $\eta_l > 0$ , $0 < c_1 < \dots < c_L < p$ , $p, \kappa, \sigma > 0$ . These are disclosed additions. The paper never restates them for the abstract control problem, but they follow from its queueing primitives ((24), (43), (50), p. 18). No hypothesis $\theta_L \ge 0$ is made.

Conventions:

$\eta$ and $c$ are sequences indexed by $\mathbb{N}$ and used at $1, \dots, L$ .
The cost is (52) written as one sum. It agrees with (52) on $A$ , and its values off $A$ are never used.
$\phi$ is the real supremum over the compact interval $A$ (attained). It is never defined by its closed form.
$\underline\beta$ is $-\inf\{\phi(y) : y \le p\}$ . This is the reading the paper's proofs use, and it agrees with the printed $-\inf_{y \in \mathbb{R}} \phi(y)$ whenever $\theta_L \ge 0$ .
"Continuously differentiable on $[0,\infty)$ " is a pair $(v, v')$ : $v'$ is continuous on $[0,\infty)$ and is the derivative of $v$ within $[0,\infty)$ at every point (one-sided at $0$ ).
"Increasing" means strictly increasing.
$\beta^* = \inf \mathcal I$ is a real infimum. Lemmas 13, 17 and 18 make it meaningful; no property of $\mathcal I$ is assumed.

Trivializing formalizations are ruled out. The solution $v_\beta$ is never chosen: every lemma quantifies over all solutions of IVP( $\beta$ ). The goal quantifies $\beta$ and $v$ existentially and requires all of (69), including the limit $p$ and strict monotonicity.

The source is the arXiv preprint v2, including its Online Supplement. The queueing network (§2) and the Brownian control problem (§3) motivate the equation but are not part of any formal statement.

A complete development needs:

global existence, uniqueness and comparison for scalar Lipschitz ODEs on $[0,\infty)$ (Mathlib's IsPicardLindelof and Gronwall bounds are the starting point);
the elementary theory of the conjugate of a piecewise linear convex function.

Both are reusable beyond this mission. Proofs of individual milestones are welcome in any order. Lemmas 3, 4 and 6 are independent of the shooting lemmas.

Selected references

B. Ata, M. H. Tongarlak, D. Lee, J. Field, A Dynamic Model for Managing Volunteer Engagement, arXiv:2312.02920v2, 2023 (Operations Research, 2024). https://arxiv.org/abs/2312.02920
B. Ata, J. M. Harrison, L. A. Shepp, Drift rate control of a Brownian processing system, Annals of Applied Probability 15(2), 1145–1160, 2005 (cited in the paper for the conjugate's minimal maximizer).
H. B. Keller, Numerical Methods for Two-Point Boundary-Value Problems, Dover, 2018 (cited for Lemma 4).

17 thms1 active userReviewed

Dynamic Programming Operations Research Probability·Captain: mikedeng1

A Dynamic Model for Managing Volunteer Engagement II: The Bellman Solution in Closed Form Between Consecutive Engagement ThresholdsResearch Paper

Motivation

Non-profit organizations such as food banks run on volunteer labour. Volunteers sign up for shifts, wait on a sign-up list, work, rest, and may or may not return; the organization can spend money on engagement activities (reminders, recognition events, recruitment drives) that raise the rate at which volunteers come back or arrive. Spending too little leaves shifts unstaffed; spending too much wastes a scarce budget. Ata, Tongarlak, Lee and Field (arXiv:2312.02920, Operations Research, 2024) model this as a multiclass queueing network, pass to a heavy-traffic limit, and obtain a one-dimensional drift-rate control problem: a reflected diffusion for the scaled workload whose drift is chosen, at a cost, from an interval of feasible drifts. The optimal policy they derive is a nested threshold policy: as the workload falls below successive thresholds $\tau_1>\tau_2>\dots>\tau_L$ , one more engagement activity is switched on.

To compute that policy one needs the thresholds, and the paper obtains them from a closed-form description of the solution of the Bellman equation between consecutive thresholds. That closed form, Proposition 3 of the paper, is the goal of this mission. A companion mission formalizes Theorem 1, the existence of a solution of the same Bellman equation.

Setting

There are $L\ge1$ engagement activities. The data are a lowest drift $\theta_0<0$ , drift increments $\eta_1,\dots,\eta_L>0$ , per-unit-drift costs $0<c_1<c_2<\dots<c_L<p$ , an idleness cost rate $p$ , a mean-reversion rate $\kappa>0$ and a volatility $\sigma>0$ . The breakpoints are

\theta_l=\theta_0+\sum_{i=1}^{l}\eta_i,\qquad l=0,\dots,L,

and the feasible drifts form the interval $A=[\theta_0,\theta_L]$ . The engagement cost $c:A\to\mathbb R_+$ is the convex, increasing, piecewise linear function with $c(\theta_0)=0$ and slope $c_l$ on $(\theta_{l-1},\theta_l]$ :

c(x)=\sum_{i=1}^{l-1}c_i\eta_i+c_l(x-\theta_{l-1}),\qquad \theta_{l-1}<x\le\theta_l .

Its convex conjugate is

\phi(y)=\sup_{x\in A}\{yx-c(x)\},\qquad y\in\mathbb R .

The Bellman equation of the drift-rate control problem asks for a constant $\beta>0$ and a continuously differentiable function $v$ on $[0,\infty)$ with

\beta=\tfrac12\sigma^2v'(x)+x\kappa\,\big(p-v(x)\big)-\phi\big(p-v(x)\big),\qquad x\ge0,

such that $v(0)=0$ , $v$ is strictly increasing, and $v(x)\to p$ as $x\to\infty$ . Here $\beta$ is the optimal long-run average cost and $v=g'$ is the derivative of the transformed relative value function $g$ of the paper's §4 (p. 20).

Put $\hat c_l=c_l$ for $l=1,\dots,L$ and $\hat c_{L+1}=p$ . Since $v$ is strictly increasing from $0$ towards $p$ , each level $p-\hat c_l\in(0,p)$ is attained exactly once; the thresholds are

\tau_l=v^{-1}(p-\hat c_l),\quad l=1,\dots,L,\qquad \tau_{L+1}=0,\qquad \tau_0=\infty .

With $\Phi$ the standard normal cumulative distribution function, the paper defines for $l=1,\dots,L+1$

u_l(x)=p-\hat c_l\exp\Big\{\tfrac{-2\theta_{l-1}(x-\tau_l)+\kappa(x^2-\tau_l^2)}{\sigma^2}\Big\}+\tfrac{2(\beta-c(\theta_{l-1}))\sqrt\pi}{\sigma\sqrt\kappa}\exp\Big\{\tfrac{(\kappa x-\theta_{l-1})^2}{\kappa\sigma^2}\Big\}\Big[\Phi\Big(\tfrac{\kappa x-\theta_{l-1}}{\sigma\sqrt{\kappa/2}}\Big)-\Phi\Big(\tfrac{\kappa\tau_l-\theta_{l-1}}{\sigma\sqrt{\kappa/2}}\Big)\Big].

Formalization targets

Goal: Proposition 3 (p. 25)

For every solution $(\beta,v)$ of the Bellman equation and every $l=1,\dots,L+1$ ,

v(x)=u_l(x)\qquad\text{for all }x\in[\tau_l,\tau_{l-1}).

The statement fixes nothing beyond the model: it holds for any solution, with the thresholds defined from that solution.

Milestones

(E9), Online Supplement p. 13: the conjugate is piecewise linear,

\phi(y)=\theta_0y\ (y\le c_1),\qquad \phi(y)=\theta_{m-1}y-c(\theta_{m-1})\ (c_{m-1}<y\le c_m),\qquad \phi(y)=\theta_Ly-c(\theta_L)\ (y>c_L).

Lemma 2(i), (D1), Online Supplement p. 9: for $\kappa,\sigma>0$ ,

\int_\tau^x e^{(2\theta z-\kappa z^2)/\sigma^2}\,dz=\frac{\sigma\sqrt\pi}{\sqrt\kappa}e^{\theta^2/(\kappa\sigma^2)}\Big[\Phi\Big(\tfrac{x-\theta/\kappa}{\sigma/\sqrt{2\kappa}}\Big)-\Phi\Big(\tfrac{\tau-\theta/\kappa}{\sigma/\sqrt{2\kappa}}\Big)\Big].

Lemma 2(ii), (D2), Online Supplement p. 9: the companion formula for $\int_\tau^x z\,e^{(2\theta z-\kappa z^2)/\sigma^2}dz$ .

Significance

The result. Proposition 3 turns the nested threshold policy into something computable. Evaluating $u_l$ at the right end of its interval and inverting gives $\tau_{l-1}$ from $\tau_l$ , so the thresholds $\tau_L,\tau_{L-1},\dots,\tau_1$ follow by a one-dimensional recursion once $\beta$ is known. The paper's simulation study of a food bank (§5) uses these thresholds to set engagement policy. The result also shows that the value-function derivative, although defined through a nonlinear equation involving a supremum, is an explicit combination of Gaussian-type functions on each threshold interval.

Formalizing it. The result is proved in the paper (Online Supplement §D); no machine-checked version of it, of the conjugate formula (E9), or of the truncated Gaussian integrals (D1)–(D2) is known to exist. A formal proof checks the transcription of a long explicit formula with many constants, which is exactly where printed closed forms tend to go wrong, and produces reusable pieces: the conjugate of a convex piecewise linear function and two interval-integral identities for the normal cdf.

Difficulty

The Bellman equation is nonlinear in $v$ through $\phi(p-v)$ . The obvious approach, solving it directly, fails because $\phi$ has no single formula. What makes it tractable is that on $[\tau_l,\tau_{l-1})$ the argument $p-v(x)$ stays in one linearity interval of $\phi$ ; this is a property of the solution, derived from its monotonicity and the definition of the thresholds, not a hypothesis. A complete proof must therefore combine the piecewise description of a supremum, a uniqueness argument for a linear first-order equation on a half-open interval (with the one-sided derivative at the left end and, for $l=1$ , an unbounded interval), and the evaluation of Gaussian integrals over finite intervals in terms of the normal cdf, matching every constant of the printed formula. The two expressions for the $\Phi$ arguments, $(\kappa x-\theta)/(\sigma\sqrt{\kappa/2})$ in $u_l$ and $(x-\theta/\kappa)/(\sigma/\sqrt{2\kappa})$ in (D1)–(D2), are equal, but the identification must be made.

Formalization scope

All objects live in the namespace VolunteerEngage.Thresholds, Lean 4 with Mathlib.

The parameters form a structure Model; $\eta$ and $c$ are $\mathbb N$ -indexed sequences of which the indices $1,\dots,L$ are used. The standing assumptions ( $L\ge1$ , $\theta_0<0$ , $\eta_l>0$ , $0<c_1<\dots<c_L<p$ , $p>0$ , $\kappa>0$ , $\sigma>0$ ) form the predicate Standing, a hypothesis of every model-level theorem. The paper states them in the model's derivation ((15), (24), (42), (43), (50), p. 18) rather than for the abstract control problem.
The cost (52) is written as one sum, equal to (52) on $A$ ; values off $A$ are never used. $\phi$ is the supremum (66) over $A$ , never its closed form, so (E9) is a genuine statement.
A solution of the Bellman equation includes $\beta>0$ and a pair $(v,v')$ with $v'$ continuous on $[0,\infty)$ and the one-sided derivative of $v$ within $[0,\infty)$ at every point. "Increasing" is strict.
The thresholds enter the goal as a sequence $\tau$ with $\tau_{L+1}=0$ and, for $l\le L$ , $\tau_l\ge0$ and $v(\tau_l)=p-\hat c_l$ ; strict monotonicity makes this the definition $\tau_l=v^{-1}(p-\hat c_l)$ , so the proposition's clause " $\tau_l=v^{-1}(p-\hat c_l)$ ", which restates that definition, is not posed separately. $\tau_0=\infty$ is encoded by dropping the upper bound for $l=1$ .
The goal is stated for every solution $(\beta,v)$ ; $\beta>0$ is part of the solution predicate, as on p. 21. It is not vacuous: the companion mission's goal (Theorem 1) asserts that a solution exists. A formalization that assumed the closed form of $\phi$ , that $p-v$ stays in one linearity interval, or that took $u_l$ as the definition of $v$ would make the goal trivial and is ruled out.
$\Phi$ is the published definition Cohen2019.Robust.Phi, which is Mathlib's cdf (gaussianReal 0 1). Integrals in (D1)–(D2) are oriented interval integrals of continuous functions.

The source is the arXiv preprint v2 including its Online Supplement. The queueing network (§2) and the Brownian control problem (§3) motivate the Bellman equation but are not part of any formal statement; the optimality of the threshold policy (Theorem 2) is not formalized here. Proofs of any milestone, of the goal, and general lemmas on conjugates of piecewise linear functions or on Gaussian integrals over intervals are welcome.

Selected references

B. Ata, M. H. Tongarlak, D. Lee, J. Field, A Dynamic Model for Managing Volunteer Engagement, arXiv:2312.02920v2, 2023; Operations Research, 2024. https://arxiv.org/abs/2312.02920

6 thms1 active userReviewed

Analysis Economics Operations Research·Captain: mikedeng1

Punish Underperformance with Suspension: Optimal Dynamic Contracts in the Presence of Switching Cost IV: Low Switching Cost, Control-Band Value Functions Meet the Optimality ConditionsResearch Paper

Motivation

Many service relationships are dynamic contracts in which the principal cannot observe the agent's effort, only its noisy consequences. Cao, Sun and Tian (Management Science, 2024) study such a relationship when the principal can suspend the agent and must pay a fixed switching cost to restart work. Suspension is a punishment that does not end the relationship, and it is used in practice for platform workers, contractors and franchisees. The paper shows that, when the switching cost and the revenue are low, the optimal contract has a control-band structure: the agent's promised utility is kept inside an interval, the agent is suspended when it falls below the lower end, and work resumes at the upper end. Two-threshold policies of this kind are standard in optimal switching problems with switching costs (Duckworth and Zervos, 2001; Vath and Pham, 2007), whose verification arguments the paper compares with its own.

This mission is the fourth of a series formalizing the analytic core of the paper. It covers the low-switching-cost region (Area III of the paper's Figure 2).

Setting

A Poisson process of arrivals brings revenue $R$ each. The base arrival rate is $\underline\mu\ge0$ ; if the agent works, at cost $b>0$ per unit of time, the rate becomes $\mu>\underline\mu$ . Write $\Delta\mu=\mu-\underline\mu$ . The principal's cost rate while the agent works is $c\ge b$ , restarting work costs $K>0$ , and the principal and the agent discount at rates $0<r\le\rho$ . Assumption 1 is $R\Delta\mu>c$ . The constants are

\beta=\frac b{\Delta\mu},\quad \bar w=\frac{\beta\mu}\rho,\quad \underline v=\frac{\underline\mu R}r,\quad \bar V=\frac{R\mu-c-(\rho-r)\bar w}r,\quad \bar V(w)=\frac{R\mu-c-(\rho-r)w}r .

The promised utility $w\ge0$ is the state. For a function $f$ on $\mathbb R_+$ with left derivative $f'$ , the paper's operators are

(\mathcal A_If)(w)=(\mu+r)f(w)-\mu f(w+\beta)+\rho(\bar w-w)f'(w)-(\mu R-c)+(\rho-r)w,

(\mathcal A_\emptyset f)(w)=rf(w)-\rho wf'(w)+(\rho-r)w-R\underline\mu,

for the working state $I$ and the suspended state $\emptyset$ . A pair $(V_I,V_\emptyset)$ satisfies the optimality condition (20)–(22) if $\mathcal A_IV_I\ge0$ , $\mathcal A_\emptyset V_\emptyset\ge0$ , $0\le V_I-V_\emptyset\le K$ and $V_I(0),V_\emptyset(0)\ge\underline v$ .

Two families of functions enter. In the suspended state, $V_c(w)=\underline v+w+c\,w^{r/\rho}$ (24) solves $\mathcal A_\emptyset V=0$ with $V(0)=\underline v$ . In the working state, for $\tilde w<\bar w$ , $V_{\tilde w}$ is the $C^1$ solution of the delay differential equation (25), in which $V(w)$ is coupled to the look-ahead value $V((w+\beta)\wedge\tilde w)$ , with $V_{\tilde w}=\bar V(\tilde w)$ beyond $\tilde w$ ; $\mathcal V_{\tilde w}$ is its concavification (Lemma 2), linear below a threshold $\check w(\tilde w)$ . Lemma 3's $\hat{\mathrm w}$ is the unique $\tilde w$ with $\mathcal V_{\tilde w}(0)=\underline v$ under Condition 1.

The parameter regions are Condition 1 ( $\mu\ge\rho-r$ or $R<\hat R$ ), Condition 2 (its negation) and Condition 3: Condition 1 and $K<\bar K_1$ , or Condition 2 and $K<\underline K$ , with $\hat R$ (28), $\bar K_1$ (K1) and $\underline K$ (33) explicit thresholds.

The paper uses three different hats: Definition 1's payment threshold $\hat w$ , Lemma 3's upright $\hat{\mathrm w}$ , and Proposition 6's bold $\hat{\mathbf w}$ , the upper end of the control band.

Formalization targets

Goal: Proposition 7, first claim

Under Condition 3 there are parameters $(\mathsf c,\hat{\mathbf w},\bar\vartheta,\underline\vartheta)$ satisfying Proposition 6 such that

V_I(w)=\begin{cases}V_{\mathsf c}(w),&w<\underline\vartheta\\ \mathcal V_{\hat{\mathbf w}}(w),&w\ge\underline\vartheta\end{cases},\qquad V_\emptyset(w)=\begin{cases}V_{\mathsf c}(w),&w<\bar\vartheta\\ \mathcal V_{\hat{\mathbf w}}(w)-K,&w\ge\bar\vartheta\end{cases}\qquad(46)

satisfy (20)–(22).

Proposition 6

Under Condition 3 there is $(\mathsf c,\hat{\mathbf w},\bar\vartheta,\underline\vartheta)$ with $\mathsf c>0$ , $\underline\vartheta<\bar\vartheta<\hat{\mathbf w}$ and value matching and smooth pasting at both thresholds:

\mathcal V_{\hat{\mathbf w}}(\underline\vartheta)=V_{\mathsf c}(\underline\vartheta),\quad \mathcal V_{\hat{\mathbf w}}'(\underline\vartheta)=V_{\mathsf c}'(\underline\vartheta),\quad \mathcal V_{\hat{\mathbf w}}(\bar\vartheta)=V_{\mathsf c}(\bar\vartheta)+K,\quad \mathcal V_{\hat{\mathbf w}}'(\bar\vartheta)=V_{\mathsf c}'(\bar\vartheta)>1 .

Milestones

Lemma EC.4 (the first step of the EC.3.9 construction), Proposition 6, and the two hardest parts of (20) at the constructed tuple: Lemma EC.12 ( $\mathcal A_\emptyset V_\emptyset\ge0$ on $[\bar\vartheta,\hat{\mathbf w})$ ) and Lemma EC.13 ( $\mathcal A_IV_I\ge0$ below $\underline\vartheta$ ). The other steps of the construction are posed as further statements of the mission without milestone status: Lemma EC.7 (the root of $\psi=K$ under Condition 1), Lemma EC.8 and Lemma EC.11 (the Condition 2 counterparts of EC.4 and EC.7).

Significance

Proposition 7 is the analytic certificate behind the paper's Theorem 5: combined with the verification Theorem 1, it shows that the control-band contract is optimal in the low-cost region, and that the principal's value is $V_\emptyset(w)-w$ . Without it the third case of the paper's main Theorem 2 is unproved. The construction of Proposition 6 also gives a computable description of the band, which the paper uses for its numerical illustrations.

The results are proved in the paper's e-companion; none of them has a machine-checked proof. This mission states the analytic part as Lean targets. The delay-ODE layer (existence, uniqueness and shape of $V_{\tilde w}$ ) is shared with the first mission of the series, and Proposition 7's proof depends on it. The stochastic contract model, the verification theorem and the optimality Theorems 1–5 are not formalized in this series.

Difficulty

Each piece of (20)–(22) is a one-variable inequality, but the functions are not explicit. $\mathcal V_{\hat{\mathbf w}}$ is defined through a delay equation, and the band's endpoints are defined implicitly through four nested steps: matching at $\underline\theta$ , a range bound $\underline\theta^0$ , an upper threshold $\bar\theta(\underline\theta)$ and a root of a gap function $\psi$ . The natural argument, convexity or concavity of $\mathcal A_IV_I$ on the suspension region, fails: on $[0,\underline\vartheta)$ the function $\mathcal A_IV_I$ mixes $V_{\mathsf c}$ with the look-ahead value $V_I(w+\beta)$ and is not convex (p. 28), so the convexity arguments of the switching literature do not apply. The paper's proof of this single inequality occupies EC.3.12, with eight auxiliary lemmas.

Formalization scope

Functions are ℝ → ℝ and every statement quantifies over $w\ge0$ . The standing assumptions are $0\le\underline\mu<\mu$ , $0<b\le c$ , $K>0$ , $0<r\le\rho$ and Assumption 1; $\underline\mu\ge0$ and $b>0$ are disclosed additions. Conventions:

$f'$ in $\mathcal A_I,\mathcal A_\emptyset$ is the left derivative; derivatives of $V_{\tilde w}$ , $\mathcal V_{\tilde w}$ are taken within $\mathbb R_+$ .
(20) is posed for $w>0$ : at $0$ the left derivative does not exist and $V_{\mathsf c}'(0^+)=+\infty$ .
$V_{\tilde w}$ is a solution of (25)–(26) chosen when one exists; $\check w$ , $\hat{\mathrm w}$ , $\bar K_1$ , $\underline\theta^0$ , $\bar\theta$ are infima or suprema of sets the paper describes; $\tilde w(\underline\theta)$ , $C(\underline\theta)$ are chosen matching pairs.
"Increasing/decreasing" is strict.
$\underline K$ (33) uses the corrected bracket $((\rho-\mu)/\rho)\beta$ in place of the printed $(r/\rho)\beta$ ; the printed form contradicts the proof's (EC.69).
Proposition 6's " $\hat{\mathbf w}<\hat{\mathrm w}$ " is read as $\hat{\mathbf w}<\bar w$ in the Condition 2 case, where $\hat{\mathrm w}$ does not exist; $0<\underline\vartheta$ is stated.
The goal is existential over Proposition 6 tuples. Lemmas EC.12 and EC.13 are stated at the tuple constructed in EC.3.9, in both cases of Condition 3; EC.13 is posed on $(0,\underline\vartheta)$ .
Lemma EC.11's second limit is printed at $0$ ; it is stated at $\breve{\underline\theta}$ , as the proof computes it.

The tuple is never defined by the property that (46) satisfies (20)–(22); the construction definitions are Steps 1–4 of EC.3.9 only, and the goal requires all of Proposition 6's conclusions. The second claim of Proposition 7, (48) on the contract's utility, is out of scope.

A complete development needs existence, uniqueness and regularity for the linear delay equation (25) (reusable for other delay problems), implicit-function arguments for $\tilde w(\underline\theta)$ , and the sign analysis of EC.3.12. Proofs of single milestones, and of the delay-ODE lemmas of the series' first mission, are welcome.

Selected references

P. Cao, P. Sun, F. Tian, Punish Underperformance with Suspension: Optimal Dynamic Contracts in the Presence of Switching Cost, Management Science, 2024. https://doi.org/10.1287/mnsc.2023.4845
K. Duckworth, M. Zervos, A model for investment decisions with switching costs, Annals of Applied Probability 11(1), 2001. https://doi.org/10.1214/aoap/998926992
V. L. Vath, H. Pham, Explicit solution to an optimal switching problem in the two-regime case, SIAM Journal on Control and Optimization 46(2), 2007. https://doi.org/10.1137/050638783

9 thms1 active userReviewed

Analysis Economics Operations Research·Captain: mikedeng1

Punish Underperformance with Suspension: Optimal Dynamic Contracts in the Presence of Switching Cost I: Condition 1, High Switching Cost, Not-Hiring Value Functions Meet the Optimality ConditionsResearch Paper

Motivation

Many service relationships let a firm pause an agent instead of firing them: a sales representative who brings in no customers for a while is suspended, a contractor is laid off for a season and recalled. Pausing is not free. Every restart carries a switching cost $K$ (re-training, re-establishing a territory, setting up the work environment), so a principal who suspends too readily pays for it. Cao, Sun and Tian (Management Science, 2024) study the optimal dynamic contract for this trade-off in continuous time, building on the Poisson-arrival moral-hazard model of Sun and Tian (2018). Their main result (Theorem 2) splits the parameter space into three regimes: never hire, hire and keep the agent working forever, and a control-band contract with suspension episodes of fixed length. This mission covers the first regime under the paper's Condition 1.

Setting

A principal earns a revenue $R$ per arrival of a Poisson process. Without effort the arrival rate is $\underline\mu\ge0$ ; an agent who works, at private cost $b>0$ per unit time, raises it to $\mu>\underline\mu$ . Write $\Delta\mu=\mu-\underline\mu$ . The principal's cost rate while the agent works is $c\ge b$ , every start of work costs $K>0$ , and the principal and the agent discount at rates $0<r\le\rho$ . Assumption 1 is $R\Delta\mu>c$ . The derived constants are

\beta=\frac{b}{\Delta\mu},\qquad \bar w=\frac{\beta\mu}{\rho},\qquad \underline v=\frac{\underline\mu R}{r},\qquad \bar V(w)=\frac{R\mu-c-(\rho-r)w}{r}.

The state of a contract is the agent's promised utility $w\ge0$ . The paper's verification theorem reduces optimality to a pair of functions: $V_I$ for the working state and $V_\emptyset$ for the suspended state. For a function $f$ on $\mathbb R_+$ , with $f'$ its left derivative, the operators are

(\mathcal A_If)(w)=(\mu+r)f(w)-\mu f(w+\beta)+\rho(\bar w-w)f'(w)-(\mu R-c)+(\rho-r)w,

(\mathcal A_\emptyset f)(w)=rf(w)-\rho wf'(w)+(\rho-r)w-R\underline\mu,

and $(V_I,V_\emptyset)$ satisfies the optimality condition (20)–(22) if $\mathcal A_IV_I\ge0$ , $\mathcal A_\emptyset V_\emptyset\ge0$ , $0\le V_I-V_\emptyset\le K$ on $\mathbb R_+$ , and $V_I(0)\ge\underline v$ , $V_\emptyset(0)\ge\underline v$ .

The working-state candidate is built from the delay differential equation (25): for $\tilde w\in[0,\bar w)$ , $V_{\tilde w}$ is the $C^1$ function on $[0,\tilde w]$ with

(\mu+r)V(w)-\mu V\big((w+\beta)\wedge\tilde w\big)+\rho(\bar w-w)V'(w)-(\mu R-c)+(\rho-r)w=0,

and $V(w)=\bar V(\tilde w)$ for $w\ge\tilde w$ . $V_{\tilde w}$ may be convex near $0$ ; $\check w(\tilde w)$ is the point up to which $V_{\tilde w}''>0$ , and the concavification $\mathcal V_{\tilde w}$ replaces $V_{\tilde w}$ on $[0,\check w(\tilde w))$ by its tangent line at $\check w(\tilde w)$ . Condition 1 is " $\mu\ge\rho-r$ or $R<\hat R$ " with

\hat R=\Big[\frac cb+\frac{(\rho-r)\mu}{\Delta\mu(\rho-r-\mu)}\cdot\frac{\rho-\mu}{\rho}\Big]\beta.

Under it there is a unique $\hat{\mathrm w}\in[0,\bar w)$ with $\mathcal V_{\hat{\mathrm w}}(0)=\underline v$ (Lemma 3). Three hats occur in the paper: $\hat w$ of Definition 1 (a payment threshold), $\hat{\mathrm w}$ of Lemma 3 (used here), and $\hat{\mathbf w}$ of Proposition 6 (not used here). For $K<\bar V(\hat{\mathrm w})-\underline v$ , Lemma 4 gives a tangent pair $(\bar\theta^K,m^K)$ : the line $m^Kw+\underline v$ touches $\mathcal V_{\hat{\mathrm w}}-K$ at $\bar\theta^K$ . Finally $\bar K_1=\inf\{K\in(0,\bar V(\hat{\mathrm w})-\underline v]\mid m^K<1\}$ (K1).

Formalization targets

Goal: Proposition 3 (p. 22)

Under Condition 1 and $\bar K_1\le K\le\bar V(\hat{\mathrm w})-\underline v$ , for the pair $(\bar\theta^K,m^K)$ of (29),

V_I=\mathcal V_{\hat{\mathrm w}},\qquad V_\emptyset(w)=\begin{cases}m^Kw+\underline v,&w\le\bar\theta^K,\\ \mathcal V_{\hat{\mathrm w}}(w)-K,&w>\bar\theta^K,\end{cases}

satisfy (20)–(22).

Milestones

Lemma EC.2: existence and uniqueness of $V_{\tilde w}$ , $\tilde w\in[0,\bar w)$ .
Lemma EC.2(iii)–(iv): $V_{\tilde w}$ increasing; $V_{\tilde w}$ decreasing and $V_{\tilde w}'$ increasing in $\tilde w$ .
Lemma 2(i): the sign pattern of $V_{\tilde w}''$ around $\check w(\tilde w)$ , and $\check w(\tilde w)\le(1-r/\rho)\beta$ .
Lemma 2(ii)–(iii): $\mathcal V_{\tilde w}$ increasing and concave; comparison in $\tilde w$ .
Lemma 3: $\hat{\mathrm w}$ exists and is unique; $\mathcal V_{\hat{\mathrm w}}'(0)>1$ when $\check w(\hat{\mathrm w})>0$ .
Proposition 2: for $K\ge\bar V(\hat{\mathrm w})-\underline v$ , $(\mathcal V_{\hat{\mathrm w}},\underline v)$ satisfies (20)–(22).
Lemma 4: tangent pairs exist; $\bar\theta^K$ increases and $m^K$ decreases in $K$ ; $\bar\theta^K\to\check w(\hat{\mathrm w})$ as $K\downarrow0$ .

Significance

Propositions 2 and 3 are the analytic certificates behind Theorem 2(i): combined with the verification theorem (Theorem 1), they show that under Condition 1 and $K\ge\bar K_1$ the principal's utility from any incentive-compatible contract promising $w$ is at most $V_\emptyset(w)-w\le\underline v$ , so never hiring the agent is optimal, and $\bar K_1$ is exactly the switching-cost threshold of that regime. The same objects ( $V_{\tilde w}$ , $\mathcal V_{\hat{\mathrm w}}$ , the tangent pairs) reappear in the low-cost control-band regime (Propositions 6–7), so a formal development of the delay ODE and its concavification is reused there.

The paper proves all these results; none is formalized. The mission formalizes the deterministic half of the guess-and-verify argument. The stochastic contract model (point processes, promise keeping, incentive compatibility), Theorem 1 and the optimality theorems are outside its scope.

Difficulty

The obvious approach, verifying (20)–(22) by direct computation, works for the linear pieces but not for $\mathcal V_{\hat{\mathrm w}}$ , which has no closed form: (25) is a delay equation solved backwards from $\tilde w$ in steps of length $\beta$ , and the closed form (EC.52) of the paper holds only on the last step $[(\tilde w-\beta)^+,\tilde w]$ . Every property of $\mathcal V_{\hat{\mathrm w}}$ used in the goal (monotonicity, the single change of convexity, the comparison in $\tilde w$ that makes $\hat{\mathrm w}$ unique) has to be extracted from the equation itself, across the kinks of $w\mapsto(w+\beta)\wedge\tilde w$ . On the second branch of $V_\emptyset$ , $\mathcal A_\emptyset V_\emptyset\ge0$ is not a pointwise identity either: it requires $m^K\le1$ , which is where $K\ge\bar K_1$ enters.

Formalization scope

Parameters form a structure with real fields; the standing assumptions $0\le\underline\mu<\mu$ , $0<b\le c$ , $K>0$ , $0<r\le\rho$ , $R\Delta\mu>c$ are a hypothesis of every theorem. $\underline\mu\ge0$ and $b>0$ are disclosed additions (a rate and a cost).
Functions are ℝ → ℝ; every statement quantifies over $w\ge0$ only. In $\mathcal A_I,\mathcal A_\emptyset$ , $f'$ is the left derivative (derivWithin f (Set.Iic w) w, the paper's p. 15 convention); in statements about $V_{\tilde w}$ and $\mathcal V_{\tilde w}$ , derivatives are taken within $\mathbb R_+$ ; in (25), within $[0,\tilde w]$ .
(20) is required for $w>0$ : at $w=0$ a left derivative of a function on $\mathbb R_+$ does not exist. (21) and (22) are as printed.
$V_{\tilde w}$ is a chosen solution of (25)–(26) (Lemma EC.2 is the milestone that makes this meaningful); $\check w(\tilde w)$ is a supremum defined through the sign of $V''$ , and $\hat{\mathrm w}$ an infimum; $\bar K_1$ is an infimum. None is defined by the property a theorem asserts about it.
The goal holds for every pair satisfying (29); the pair is unique, and at $K=\bar V(\hat{\mathrm w})-\underline v$ it is $(\hat{\mathrm w},0)$ . The second branch of (30) is extended beyond $\hat{\mathrm w}$ , as the paper's proof uses.
"Increasing/decreasing" mean strictly. The contract-utility claim $U(\underline\Gamma)=\underline v$ of Proposition 2 is not stated.
Ruled out: weakening (20)–(22) (dropping the upper bound $K$ in (21), or (22)), or defining $V_{\tilde w}$ by its closed form (EC.52), which is valid only near $\tilde w$ .

Needed infrastructure: existence and uniqueness for linear ODEs with a terminal condition, extended step by step across a delay; one-sided derivatives of piecewise functions; concavity from sign conditions on second derivatives. Proofs of the milestones, and reusable lemmas about delay equations of this form, are welcome.

Selected references

P. Cao, P. Sun, F. Tian, Punish Underperformance with Suspension: Optimal Dynamic Contracts in the Presence of Switching Cost, Management Science, 2024. https://doi.org/10.1287/mnsc.2023.4845 (cited from the authors' manuscript with e-companion).
P. Sun, F. Tian, Optimal Contract to Induce Continued Effort, Management Science 64(9), 2018. https://doi.org/10.1287/mnsc.2017.2795

11 thms1 active userReviewed

Analysis Economics Operations Research·Captain: mikedeng1

Punish Underperformance with Suspension: Optimal Dynamic Contracts in the Presence of Switching Cost III: Condition 2, Medium Switching Cost, Always-Work Value Functions Meet the Optimality ConditionsResearch Paper

Motivation

Many service relationships pay an agent per unit of output whose arrival is random: a salesperson closing deals, a call-centre worker resolving tickets, a contractor delivering jobs. When effort is unobservable, the classical tool for keeping an agent motivated is the threat of termination after poor performance. In practice firms often use a milder punishment, suspension: the agent is sent home for a while and later called back. Restarting work is not free, and each restart costs the firm a fixed switching cost.

P. Cao, P. Sun and F. Tian, Punish Underperformance with Suspension: Optimal Dynamic Contracts in the Presence of Switching Cost (Management Science, 2024), characterise the optimal dynamic contract in this setting. The optimal contract depends on the size of the switching cost: when it is large the firm should not hire, when it is moderate the firm should keep the agent working forever, and when it is small the firm uses a control-band contract with suspension episodes. Their proof is "guess and verify": a stochastic verification theorem (their Theorem 1) turns any pair of functions satisfying a system of quasi-variational inequalities into an upper bound on the principal's value, and Propositions 2–7 exhibit such pairs in each parameter region.

This mission formalizes the certificate for the medium-switching-cost region under Condition 2 (Area II of the paper's Figure 2), where the agent is never suspended.

Setting

The principal faces a Poisson stream of arrivals, each worth revenue $R$ . Without effort the arrival rate is $\underline\mu\ge0$ ; an agent who exerts effort, at cost $b>0$ per unit time, raises it to $\mu>\underline\mu$ . Write $\Delta\mu=\mu-\underline\mu$ . The principal's total cost rate while the agent works is $c\ge b$ , every start of work costs a switching cost $K>0$ , and the principal and agent discount at rates $0<r\le\rho$ . Assumption 1 is $R\Delta\mu>c$ .

The paper's derived constants are

\beta=\frac{b}{\Delta\mu},\quad \bar w=\frac{\beta\mu}{\rho},\quad \underline v=\frac{\underline\mu R}{r},\quad \bar V=\frac{R\mu-c-(\rho-r)\bar w}{r},\quad \bar K_2=\bar V-\underline v-\bar w,

together with the revenue thresholds $\hat R$ (28) and $\bar R$ (34) and the switching-cost threshold $\underline K$ (33). Condition 2 is $\mu<\rho-r$ and $R\ge\hat R$ : the agent is much more impatient than the principal and revenue is high.

The state variable is the agent's promised utility $w\ge0$ . Two operators act on functions $f$ of $w$ , where $f'$ is the left derivative:

(\mathcal A_I f)(w)=(\mu+r)f(w)-\mu f(w+\beta)+\rho(\bar w-w)f'(w)-(\mu R-c)+(\rho-r)w,

(\mathcal A_\emptyset f)(w)=rf(w)-\rho wf'(w)+(\rho-r)w-R\underline\mu.

The first is a delay-differential operator for the working state, the second a first-order operator for the suspended state. A pair $(V_I,V_\emptyset)$ satisfies the optimality condition (20)–(22) when $\mathcal A_IV_I\ge0$ , $\mathcal A_\emptyset V_\emptyset\ge0$ , $0\le V_I-V_\emptyset\le K$ and $V_I(0),V_\emptyset(0)\ge\underline v$ .

The suspended-state equation $\mathcal A_\emptyset V=0$ with $V(0)=\underline v$ is solved by $V_c(w)=\underline v+w+c\,w^{r/\rho}$ (24). In the region of this mission the paper builds

V_\emptyset(w)=\begin{cases}V_{c_K}(w),&w\le\bar w,\\ \bar V-K,&w>\bar w,\end{cases}\qquad V_I(w)=\begin{cases}V_{c_K}(w),&w\le\underline\theta_K,\\ \bar V+m_K(w-\bar w),&\underline\theta_K<w\le\bar w,\\ \bar V,&w>\bar w,\end{cases}

from parameters $(c_K,m_K,\underline\theta_K)$ chosen so that $V_{c_K}$ pastes smoothly onto the line at $\underline\theta_K$ and ends at $\bar V-K$ at $\bar w$ .

Formalization targets

Goal: Proposition 5 (first claim)

Under Condition 2 and $K\in[\underline K,\bar K_2)$ , for every triple $(c_K,m_K,\underline\theta_K)$ with $\underline\theta_K\in(0,\bar w)$ , $c_K>0$ , $m_K\in[\frac{\rho-r}{\rho-r-\mu},\frac{\bar V-\underline v}{\bar w})$ and

V_{c_K}(\underline\theta_K)=\bar V+m_K(\underline\theta_K-\bar w),\qquad V'_{c_K}(\underline\theta_K)=m_K,\qquad V_{c_K}(\bar w)=\bar V-K,

the functions $V_I,V_\emptyset$ above satisfy (20)–(22).

Milestones

(EC.67): explicit $C^1(\underline\theta)$ and $m(\underline\theta)$ solve the value-matching and smooth-pasting equations at any $\underline\theta\in(0,\bar w]$ .
Lemma EC.3: $\psi_1(\underline\theta)=\bar V-\underline v-\bar w-C^1(\underline\theta)\bar w^{r/\rho}$ is continuous and strictly decreasing on $[0,\bar w]$ , so $\psi_1=K$ has a unique root $\underline\theta_K\in(0,\bar w)$ for $K\in(0,\bar K_2)$ ; the root decreases in $K$ and tends to $\bar w$ as $K\downarrow0$ .
Lemma 5: for every $K\in[\underline K,\bar K_2)$ the triple exists, and $c_K$ , $m_K$ , $\underline\theta_K$ are monotone in $K$ .

Lemma 5 guarantees that the goal is not vacuous.

Significance

Proposition 5 is the analytic half of the paper's Theorem 4: combined with the verification theorem, it shows that in Area II the principal's optimal value is attained by a contract that pays the agent $\beta$ per arrival and never suspends. The threshold $\underline K$ separates this region from the control-band region of Proposition 7, so the explicit formula for $\underline K$ is the boundary of the phase diagram.

The result is proved in the paper. No machine-checked version exists. A formal proof checks a delicate sign argument near $w=0$ , where $V_{c_K}$ has infinite slope, and it checks the threshold $\underline K$ , whose printed formula contains an error (see Formalization scope). The paper's companion identity (41), $U(\bar\Gamma)=\bar V-\bar w-K=V_\emptyset(\bar w)-\bar w$ , is about the utility of a contract and is not part of this mission; its deterministic half is immediate from (39).

Difficulty

The cases $w\in[\underline\theta_K,\bar w]$ and $w>\bar w$ are algebraic. The difficulty is $w\in(0,\underline\theta_K)$ : there $V_I$ is the curve $V_{c_K}$ , and $w+\beta$ lands beyond $\bar w$ (Condition 2 gives $\beta>\bar w$ ), so $\mathcal A_IV_I$ couples the curve with the constant $\bar V$ . Positivity there needs more than the sign of the smooth-pasting slope: it uses the lower bound on $m_K$ in (35), which is exactly where the threshold $\underline K$ enters. A direct sign check at $\underline\theta_K$ alone does not cover the interval. The existence lemma requires monotonicity of $\psi_1$ , whose expression mixes powers $\underline\theta^{r/\rho-1}$ with a linear factor.

Formalization scope

All functions are ℝ → ℝ and every quantifier ranges over $w\ge0$ ; powers are Real.rpow. The standing assumptions $0\le\underline\mu<\mu$ , $0<b\le c$ , $K>0$ , $0<r\le\rho$ , $R\Delta\mu>c$ are one hypothesis Standing; $\underline\mu\ge0$ and $b>0$ are read off the model and stated explicitly. The left derivative is derivWithin f (Set.Iic w) w, following the paper's convention on p. 15. Condition (20) is posed for $w>0$ only: at $w=0$ the right derivative of $V_{c_K}$ is $+\infty$ , so the paper's (20) there is an extended-real statement and Lean's junk derivative would make it false. (21) and (22) are posed as printed.

The threshold $\underline K$ of (33) is corrected: the printed bracket contains $\frac r\rho\beta$ , but the paper's own proof identifies $\underline K$ with $\check K_2$ of (EC.69), which gives $\frac{\rho-\mu}{\rho}\beta$ . With the printed term Lemma 5 fails (for $r=0.2,\rho=1.2,b=c=1,R=5,\mu=0.9,\underline\mu=0.1$ , the printed value is $-0.069$ , the corrected one $7.2533$ ). Equation (36) is printed with a free $w$ that should read $\underline\theta_K$ . The range $\underline\theta_K\in(0,\bar w)$ , given by the proof, is stated.

The goal quantifies over all triples satisfying Lemma 5's conclusions; such a triple is unique, so this is the paper's claim, and Lemma 5 rules out a vacuous goal. Dropping the bound $K$ in (21), the condition (22), or the lower bound on $m_K$ would trivialize or change the statement.

The development needs the derivative of $w\mapsto w^{r/\rho}$ , sign analysis of explicit real functions, and the intermediate value theorem. The Setting file is shared with the other missions of this series and will be consolidated. Proofs of the milestones in any order are welcome; (EC.67) is a self-contained calculus exercise.

Selected references

P. Cao, P. Sun, F. Tian, Punish Underperformance with Suspension: Optimal Dynamic Contracts in the Presence of Switching Cost, Management Science, 2024. https://doi.org/10.1287/mnsc.2023.4845 (cited from the authors' manuscript and e-companion: §4.2 pp. 24–26, EC.3.7–EC.3.8 pp. ec32–ec34).
Y. Sannikov, A Continuous-Time Version of the Principal-Agent Problem, Review of Economic Studies 75(3), 2008. https://doi.org/10.1111/j.1467-937X.2008.00486.x
B. Biais, T. Mariotti, J.-C. Rochet, S. Villeneuve, Large Risks, Limited Liability, and Dynamic Moral Hazard, Econometrica 78(1), 2010. https://doi.org/10.3982/ECTA7261

6 thms1 active userReviewed

Analysis Economics Operations Research·Captain: mikedeng1

Punish Underperformance with Suspension: Optimal Dynamic Contracts in the Presence of Switching Cost II: Condition 2, High Switching Cost, Not-Hiring Value Functions Meet the Optimality ConditionsResearch Paper

Motivation

Firms that outsource work to an agent whose effort they cannot observe often punish poor performance by suspending the relationship for a while, even though restarting costs money: a new set-up, re-training, re-mobilisation. Cao, Sun and Tian (Management Science, 2024) study this trade-off in a continuous-time principal–agent model with Poisson arrivals and a fixed switching cost paid every time work (re)starts. They characterise the optimal dynamic contract in three regimes: never hire the agent, hire and keep the agent working forever, or a control-band contract with suspension episodes of fixed length. The model extends the Poisson-arrival contracting framework of Sun and Tian (2018) by adding the switching cost.

The proof follows a guess-and-verify pattern. A stochastic verification theorem (Theorem 1 of the paper) turns any pair of functions satisfying a system of quasi-variational inequalities into an upper bound on the principal's value. Propositions 2–7 then supply such a pair in each parameter region. This mission covers one region: the agent is much more impatient than the principal (Condition 2) and the switching cost is high.

Setting

A principal earns revenue $R$ per arrival of a Poisson process. Without the agent's effort the arrival rate is $\underline\mu\ge0$ ; with effort it is $\mu>\underline\mu$ , and effort costs the agent $b>0$ per unit of time. While the agent works, the principal's total cost rate is $c\ge b$ . Each time work starts or restarts, the principal pays a switching cost $K>0$ . The principal discounts at rate $r$ and the agent at rate $\rho$ , with $0<r\le\rho$ . Write $\Delta\mu=\mu-\underline\mu$ . Assumption 1 is $R\Delta\mu>c$ .

The derived constants are

\beta=\frac{b}{\Delta\mu},\qquad \bar w=\frac{\beta\mu}{\rho},\qquad \underline v=\frac{\underline\mu R}{r},\qquad \bar V=\frac{R\mu-c-(\rho-r)\bar w}{r},\qquad \bar K_2=\bar V-\underline v-\bar w .

The variable $w\ge0$ is the agent's promised utility. The revenue threshold is

\hat R=\Big[\frac cb+\frac{(\rho-r)\mu}{\Delta\mu(\rho-r-\mu)}\cdot\frac{\rho-\mu}{\rho}\Big]\beta .

Condition 2 is: $\mu<\rho-r$ and $R\ge\hat R$ .

For a function $f$ on $\mathbb R_+$ with left derivative $f'$ , the working-state operator and the suspension-state operator are

(\mathcal A_I f)(w)=(\mu+r)f(w)-\mu f(w+\beta)+\rho(\bar w-w)f'(w)-(\mu R-c)+(\rho-r)w,

(\mathcal A_\emptyset f)(w)=rf(w)-\rho wf'(w)+(\rho-r)w-R\underline\mu .

The first is a delay-differential operator: it evaluates $f$ at $w+\beta$ . A pair $(V_I,V_\emptyset)$ satisfies the optimality condition (20)–(22) if

(\mathcal A_IV_I)(w)\ge0,\quad(\mathcal A_\emptyset V_\emptyset)(w)\ge0,\qquad 0\le V_I(w)-V_\emptyset(w)\le K,\qquad V_I(0)\ge\underline v,\ V_\emptyset(0)\ge\underline v .

Formalization targets

Goal: Proposition 4

Under Condition 2, let $V_I$ be the line from $\underline v$ at $w=0$ to $\bar V$ at $w=\bar w$ , and let $V_I$ be constant $\bar V$ beyond $\bar w$ (display (31)). Then

K>\bar V-\underline v\ \Longrightarrow\ (V_I,\ V_\emptyset\equiv\underline v)\ \text{satisfies (20)–(22)},

\bar K_2<K\le\bar V-\underline v\ \Longrightarrow\ (V_I,\ V_\emptyset)\ \text{satisfies (20)–(22)},

where in the second case $V_\emptyset$ is the line from $\underline v$ to $\bar V-K$ on $[0,\bar w]$ , constant $\bar V-K$ beyond (display (32)).

Milestones

Lemma EC.2(vi), second claim: if $\rho>r+\mu$ , then $\bar V-\frac{\rho-r}{\rho-r-\mu}\bar w\ge\underline v$ if and only if $R\ge\hat R$ .
Proposition 4, first part: the case $K>\bar V-\underline v$ .
Proposition 4, second part: the case $\bar K_2<K\le\bar V-\underline v$ .

Significance

Through the paper's verification theorem, Proposition 4 yields the "not hiring" half of the main Theorem 2 in the Condition 2 regime. If $K\ge\bar K_2$ , the principal's value is at most $\underline v$ , so it is optimal never to engage the agent (Theorem 3). The threshold $\bar K_2=\bar V-\underline v-\bar w$ is the switching cost above which the value of hiring, net of the set-up cost and of the agent's promised rent, falls below the outside value. Together with the companion missions of this series (Condition 1 with high cost, Condition 2 with medium cost, and the low-cost control-band regime), this result completes the partition of the parameter space behind Theorem 2.

The result is proved in the paper and has no machine-checked proof yet. This mission states the analytic certificate of the guess-and-verify argument, not the contract-optimality theorem. The contribution it asks for is a formal proof that these explicit functions satisfy the quasi-variational inequalities, including the left-derivative behaviour at the kink $w=\bar w$ and the algebra that links Condition 2 to the sign of $\mathcal A_IV_I$ .

Difficulty

The functions are piecewise linear, so the difficulty is not analytic depth but bookkeeping that is easy to get wrong:

The operator $\mathcal A_I$ is non-local. It evaluates $V_I$ at $w+\beta$ , and which branch of (31) applies there depends on how $\bar w$ compares with $\beta$ , which Condition 2 settles.
At the kink $w=\bar w$ the functions are not differentiable, so the left-derivative convention must be used explicitly.
The sign of $\mathcal A_IV_I$ on $[0,\bar w]$ reduces to an inequality between $\bar V$ , $\underline v$ and $\bar w$ , and showing that this inequality is the revenue condition $R\ge\hat R$ requires unfolding (8)–(10) and (28).

The naive check, that $\mathcal A_IV_I$ vanishes or is positive because $V_I$ is "close to" a solution of the delay equation, does not work: $V_I$ is not a solution of (25), and the inequality is strict in general.

Formalization scope

All parameters are real numbers in one structure Params. Its predicate Standing collects the paper's standing assumptions: $0\le\underline\mu<\mu$ , $0<b\le c$ , $K>0$ , $0<r\le\rho$ and $R\Delta\mu>c$ . Two of these are added to the page and disclosed: $\underline\mu\ge0$ , since it is an arrival rate, and $b>0$ , since (31)–(32) divide by $\bar w=\beta\mu/\rho$ .

Functions are ℝ → ℝ, and every condition is quantified over $w\ge0$ only. The derivative in $\mathcal A_I$ and $\mathcal A_\emptyset$ is the left derivative derivWithin f (Set.Iic w) w, as the paper prescribes on p. 15. Inequality (20) is required for $w>0$ : on $\mathbb R_+$ the left derivative at $0$ does not exist. Inequalities (21) and (22) are required exactly as printed. "Satisfy the optimality condition (20)–(22)" means exactly these three conditions; the paper's Theorem 1 additionally asks for monotonicity and concavity, but Proposition 4 does not claim them and they are not added.

The threshold $\hat R$ is the printed formula. Its denominator $\rho-r-\mu$ is positive under Condition 2, so Lean's convention $x/0=0$ never applies there.

None of the conditions is weakened: (21) keeps both bounds, (22) is kept, and the operators are not pre-simplified with the closed form of $\bar V$ . A formal proof therefore has to carry out the sign computation itself. The stochastic contract model (Poisson point processes, promise keeping, incentive compatibility), the verification Theorem 1 and the optimality Theorems 2–3 are not formalized.

Two hat symbols elsewhere in the paper are distinct objects from those used here: $\hat{\mathrm w}$ of Lemma 3 and the bold $\hat{\mathbf w}$ of Proposition 6. Neither appears in this mission. Proofs of the milestones, and proofs of the goal that use them, are welcome.

Selected references

P. Cao, P. Sun, F. Tian, Punish Underperformance with Suspension: Optimal Dynamic Contracts in the Presence of Switching Cost, Management Science, 2024. https://doi.org/10.1287/mnsc.2023.4845
P. Sun, F. Tian, Optimal Contract to Induce Continued Effort, Management Science 64(9), 4193–4217, 2018. https://doi.org/10.1287/mnsc.2017.2795

5 thms1 active userReviewed

Economics Partial Differential Equations Probability·Captain: mikedeng1

A Dynamic Principal Agent Problem with One-sided Commitment: The Principal's Value Function Is the Minimal Continuous Viscosity Solution of the Type-Indexed HJB SystemResearch Paper

Motivation

In a principal–agent problem with moral hazard, a principal (an employer) pays an agent whose effort she cannot observe; she sees only an output process whose drift the effort controls. Continuous-time versions of the problem, starting with Holmström–Milgrom (1987) and Sannikov (2008), are solved by turning the agent's continuation utility into a state variable and writing a Hamilton–Jacobi–Bellman (HJB) equation for the principal's value.

Most of this literature assumes two-sided commitment: the agent cannot leave. In labour markets the agent can quit whenever an outside offer beats his continuation utility, and the principal must then hire someone else. Zhang and Zhu (arXiv:2208.06473; Mathematics of Operations Research, 2025) study this one-sided commitment: the principal is committed to the contract, the agent is free to quit at a stopping time of his choice, and after each quitting the principal pays a cost and hires a new agent, possibly of another type. The principal's value then depends on every future hire, and the paper characterises it by a coupled system of HJB equations.

Setting

Fix a horizon $T>0$ and a payment cap $C_0>0$ . A standard Brownian motion $B$ on $(\Omega,\mathcal F,\mathbb P)$ is the output. Agents have types $\theta\in\Theta$ . An agent of type $\theta$ receiving a payment rate $\eta\le C_0$ and exerting effort $\alpha$ has running utility $f(\theta;s,\eta)$ and running cost $h(\theta;s,\alpha)$ ; $f$ is increasing and concave in $\eta$ , $h$ is convex in $\alpha$ (Assumption 2.2). Effort shifts the drift of $B$ through the Girsanov measure $\mathbb P^\alpha$ (weak formulation). The agent's optimal effort against a sensitivity process $Z$ is $\alpha=I^h(\theta;\cdot,Z)$ , the inverse of $\partial_\alpha h$ , and $\mathbb E^{\theta,Z}$ denotes expectation under the corresponding measure.

A contract started at time $t$ is described in forward form by $(\eta,Z)$ : the agent's continuation utility is

\mathcal X^{\theta;t,x,\eta,Z}_s=x-\int_t^s\big[f(\theta;r,\eta_r)+H(\theta;r,Z_r)\big]dr+\int_t^sZ_r\,dB_r,

with $H(\theta;s,z)=\sup_\alpha[\alpha z-h(\theta;s,\alpha)]$ and the constraint $\mathcal X_T=0$ . The agent's utility is capped by the upper barrier $\overline L^\theta_t=\int_t^Tf(\theta;s,C_0)\,ds$ . He quits at the first time $\mathcal X$ reaches the lower barrier $\underline L^\theta_t=R^\theta_t-c^\theta_t$ , where $R^\theta$ is his market value and $c^\theta\ge1/\Lambda_0$ his quitting cost (Assumptions 2.7, 3.1). The relevant domain is

D_\theta=\{(t,x):0\le t<T,\ \underline L^\theta_t<x\le\overline L^\theta_t\}.

When the $i$ -th agent quits at $\tau_i<T$ , the principal pays $c^P_{\tau_i}$ and hires an agent of type $\zeta_{\tau_i}$ at utility $R^{\zeta_{\tau_i}}_{\tau_i}$ (the quitting sequence (5.8)). The principal's value is

u_\infty(\theta;t,x)=\sup_{(\eta,Z,\zeta)}\mathbb E^{\zeta,Z}\Big[\int_t^T\big[I^h(\zeta_s;s,Z_s)-\eta_s\big]ds-\sum_{i\ge1}c^P_{\tau_i}\mathbf 1_{\{\tau_i<T\}}\Big],

and the value of the best new hire at time $t$ is $\overline u_\infty(t)=\sup_\theta u_\infty(\theta;t,R^\theta_t)-c^P_t$ .

Formalization targets

Goal: Theorem 6.3

The family $\{u_\infty(\theta;\cdot,\cdot)\}_{\theta\in\Theta}$ is the minimal continuous viscosity solution of

\partial_tu+\sup_{\eta\le C_0,\ z\in\mathbb R}\Big[\tfrac12|z|^2\partial_{xx}u-\big[f(\theta;t,\eta)+\tilde H(\theta;t,z)\big]\partial_xu+I^h(\theta;t,z)-\eta\Big]=0\quad\text{on }D_\theta,\ \theta\in\Theta,

with boundary conditions

u(\theta;t,\overline L^\theta_t)=-C_0(T-t),\qquad u(\theta;T-,x)=0,\qquad u(\theta;t,\underline L^\theta_t+)\ge\sup_{\theta'}u(\theta';t,R^{\theta'}_t)-c^P_t.

The last condition couples the equations for different types. The goal also asserts that the value sets in (6.1) are nonempty and bounded above, so that $u_\infty$ is a genuine real-valued function.

Milestones

Lemma 3.4: explicit contracts with $\int_t^T[C_0-\eta_s]ds\le\delta$ under which the agent never quits.
Lemma 2.5 (2.20): a priori estimates for admissible contracts.
Proposition 2.8 and Lemma 3.6: the self-enforcing value $V^P_0$ and the new-hire value $\overline u_0$ are uniformly continuous with modulus $C\sqrt\rho$ .
Theorem 4.5: with at most one quitting, $u_1$ is the minimal continuous viscosity solution of the same equation with boundary datum $\overline u_0$ .
Proposition 5.4: a non-recursive representation of $u_n$ (at most $n$ quittings).
Proposition 6.1: $\mathbb P^{\zeta,Z}(\tau_n<T)\le C/n$ , and $|u_n-u_\infty|\le C/n$ .
Proposition 6.2: monotonicity and uniform continuity of $u_\infty$ , regularity of $\overline u_\infty$ , and the boundary conditions.
(6.7): the dynamic programming principle for $u_\infty$ .

Significance

The theorem identifies the principal's value under one-sided commitment as a PDE object, which makes it computable and comparable with other contracting regimes. Along the way the paper shows that the principal sees only finitely many quittings (Proposition 6.1) and that tolerating more quittings never lowers her value, so contracts that prevent quitting altogether (self-enforcing contracts) are in general suboptimal. The coupling through $\overline u_\infty$ turns the problem into an infinite system of HJB equations indexed by agent types, a structure that also appears in switching and re-hiring problems.

The result is proved in the paper; none of it is formalized. A formalization would add to the platform a continuous-time moral-hazard model in the weak formulation, hitting-time stopping driven by an Itô integral, a quitting sequence with random restarts and type switching, and a viscosity-solution notion for a fully nonlinear HJB equation on a time-dependent domain. The paper's own proof leaves several steps to the reader (the dynamic programming principle, the viscosity property, comparison for a truncated equation), so a complete development would also supply these.

Difficulty

The obvious route is "dynamic programming principle, then viscosity property, then comparison". Each step is harder here than in a textbook control problem. The control $z$ is unbounded, so the Hamiltonian can be $+\infty$ and the viscosity property must be derived without a finite Hamiltonian. The process is stopped at a hitting time of a moving barrier and restarted at a random level with a new type, so the dynamic programming principle must handle restarts. Minimality cannot come from a standard comparison principle, because the boundary datum at $\underline L^\theta$ depends on the competitor itself and no growth condition is imposed on competitors; the paper argues through approximation by $u_n$ and Theorem 4.5 instead.

Formalization scope

All objects are defined in the namespace DynPrincipalAgent.HJB. Process time is $\mathbb R_{\ge0}$ ; deterministic data are functions of real time. The Itô integral is the published Peng1990.SMP.IsItoIntegral, with a continuous version required wherever hitting times read paths. Controls started at $t$ are progressively measurable for the filtration $\mathbb F^t$ of $B_s-B_t$ . Value functions are real suprema of value sets that record an expectation only when it is genuine (integrable payoffs, almost surely integrable drifts and running rewards, summable quitting costs); these conditions hold for every admissible control.

Pinned readings, all disclosed in the items: viscosity solutions are the standard Crandall–Ishii–Lions notion with $C^2$ test functions on $\mathbb R^2$ , tested on the interior of $D_\theta$ , with the supremum in the HJB operator never formed; the boundary condition at $\underline L^\theta$ requires a real right limit compared against every $u(\theta';t,R^{\theta'}_t)-c^P_t$ ; $\Theta$ carries a σ-algebra and $f$ , $h$ , $\partial_\alpha h$ are jointly measurable; Assumption 2.7 (ii) is read as $|R^\theta_s-R^\theta_{s'}|\le\rho(|s-s'|)$ ; a modulus of continuity is nondecreasing, vanishes at $0^+$ and satisfies $\rho(\delta)\ge\delta$ ; generic constants depend only on $(T,C_0,\Lambda_0,\Lambda_1)$ and are fixed before the model; $H$ and $\tilde H$ take the closed forms of (2.11)–(2.12). The agent's BSDE and reflected BSDE (Propositions 2.3, 3.2), §7's standard contracts and the economic interpretation of $R^\theta$ , $c^\theta$ , $c^P$ are out of scope.

A formalization in which a value function equals a junk value (an empty or unbounded real supremum, a Bochner integral of a non-integrable payoff, a hitting time of an empty set) or in which the viscosity notion is vacuous does not count: the goal states that the value sets are nonempty and bounded, and the definitions avoid junk by construction. Competitors in the minimality clause satisfy exactly the printed boundary conditions, with no added growth bound.

Reusable infrastructure: Girsanov measures for BMO drifts, forward utility processes, hitting times of continuous semimartingales, and viscosity solutions of HJB equations on non-cylindrical domains. Contributions on any milestone, and on general lemmas such as the dynamic programming principle for controlled diffusions stopped at hitting times, are welcome.

Selected references

J. Zhang, Z. Zhu, A Dynamic Principal Agent Problem with One-sided Commitment, Mathematics of Operations Research, 2025. Preprint arXiv:2208.06473v3. https://arxiv.org/abs/2208.06473
Y. Sannikov, A Continuous-Time Version of the Principal–Agent Problem, Review of Economic Studies 75 (2008). https://doi.org/10.1111/j.1467-937X.2008.00486.x
B. Holmström, P. Milgrom, Aggregation and Linearity in the Provision of Intertemporal Incentives, Econometrica 55 (1987). https://doi.org/10.2307/1913238
M. G. Crandall, H. Ishii, P.-L. Lions, User's guide to viscosity solutions of second order partial differential equations, Bull. AMS 27 (1992). https://doi.org/10.1090/S0273-0979-1992-00266-5

17 thms1 active userReviewed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Comparison Between Mean-Variance and Monotone Mean-Variance Preferences Under Jump Diffusion and Stochastic Factor Model: Optimal MMV and MV Utilities Coincide If and Only If Assumption 1 HoldsResearch Paper

Motivation

Mean-variance (MV) preferences, $U_\theta(X)=\mathbb E[X]-\frac\theta2\mathrm{Var}(X)$ , are the standard objective of portfolio selection since Markowitz. They are not monotone: an investor can prefer a terminal wealth $X$ to a wealth $X'\ge X$ that is larger in every state, because the extra upside raises the variance. Monotone mean-variance (MMV) preferences (Maccheroni, Marinacci, Rustichini and Taboga, 2009) repair this. They are the largest monotone preferences that agree with MV preferences on the domain of monotonicity $\mathcal G_\theta=\{f\in\mathcal L^2:f-\mathbb E[f]\le1/\theta\}$ .

A natural question is when switching from MV to MMV changes the optimal investment. In continuous-time markets driven only by Brownian motions, the optimal strategies under the two preferences coincide (Trybuła and Zawisza, 2019, for a stochastic factor model; Strub and Li, 2020, for continuous semimartingale markets), and whether this persists with jumps was left open by Trybuła and Zawisza. Li, Liang and Pang study a market whose risky asset also jumps and whose coefficients depend on a stochastic factor. They show that the two problems agree if and only if a pathwise condition on the jumps, Assumption 1, holds.

Setting

On a probability space $(\Omega,\mathcal F,\mathbb P)$ live two independent Brownian motions $W^1,W^2$ and an independent Poisson random measure $N(\mathrm ds,\mathrm dp)$ with finite Lévy measure $\nu$ and compensated measure $\tilde N$ . The filtration $\{\mathcal F_t\}$ is generated by $W^1,W^2,N$ . A stochastic factor follows

\mathrm dZ_s=a(Z_s)\,\mathrm ds+b(Z_s)(\rho_W\,\mathrm dW^1_s+\bar\rho_W\,\mathrm dW^2_s),\qquad Z_t=z,

with $\rho_W^2+\bar\rho_W^2=1$ . Investing the amount $\pi_s$ in the risky asset gives the (discounted) wealth

\mathrm dX^\pi_s=\pi_s(\mu(Z_s)-r)\,\mathrm ds+\pi_s\sigma(Z_s)\,\mathrm dW^1_s+\pi_s\int_{\mathbb R}\gamma(Z_s,p)\,\tilde N(\mathrm ds,\mathrm dp),\qquad X_t=x,

on $[t,T]$ , with $\gamma>-1$ . Write $\Sigma(z)=\sigma(z)^2+\int\gamma(z,p)^2\nu(\mathrm dp)$ and $\lambda(z)=(\mu(z)-r)^2/\Sigma(z)$ .

The MMV preference is

V_\theta(X)=\inf_{\mathbb Q}\Big\{\mathbb E^{\mathbb Q}[X]+\frac1{2\theta}\Big(\mathbb E^{\mathbb P}\Big[\Big(\frac{\mathrm d\mathbb Q}{\mathrm d\mathbb P}\Big)^2\Big]-1\Big)\Big\}.

The infimum runs either over the Doléans-Dade measures $\mathcal Q^t$ or over all of $\mathcal Q_0=\{\mathbb Q\ll\mathbb P:\mathbb E[(\mathrm d\mathbb Q/\mathrm d\mathbb P)^2]<\infty\}$ . A measure in $\mathcal Q^t$ has density $\mathcal E_T$ , where $\mathcal E$ is the stochastic exponential of $\int\eta_1\mathrm dW^1+\int\eta_2\mathrm dW^2+\int\!\int\phi\,\mathrm d\tilde N$ with $\mathcal E_T\ge0$ , $\mathbb E[\mathcal E_T]=1$ and $\mathcal E_T\in L^2$ .

The optimal utilities from $(x,z,t)$ are suprema over the admissible strategies of the paper's Definitions 2 and 3: predictable $\pi$ whose wealth has $\mathbb E[\sup_s|X^\pi_s|^2]<\infty$ , under $\mathbb P$ for MV and under every $\mathbb Q\in\mathcal Q^t$ for MMV. Both solutions are expressed through the solution $G=-e^F$ of the nonlinear parabolic PDE (20),

G_t+\alpha(z)G_z+\tfrac12b(z)^2G_{zz}-\beta(z)b(z)^2\frac{G_z^2}{G}+\lambda(z)G=0,\qquad G(z,T)=-1.

Through $\zeta(z,s)=-(\mu(z)-r-\sigma(z)b(z)\rho_WG_z/G)/\Sigma(z)$ it also enters Assumption 1. Let $\tau$ be the first jump time after $t$ at which $\zeta(Z_s,s)\gamma(Z_s,\Delta L_s)=-1$ . Assumption 1 requires $\zeta\gamma\ge-1$ at every jump in $(t,T]$ up to time $\tau$ .

Formalization targets

Goal: Theorem 9

\sup_{\pi\in\mathcal B_{x,z,t}}U_\theta(X^\pi_T)=\sup_{\pi\in\mathcal A_{x,1/(2\theta),z,t}}V_\theta(X^\pi_T)\iff\text{Assumption 1 holds at }(z,t).

The same holds when $V_\theta$ ranges over $\mathcal Q_0$ instead of $\mathcal Q^t$ .

Milestones

Theorem 3 links the market player's density process to the wealth: $2Y_sG(Z_s,s)=X^{\pi^*}_s-x+2yG(z,t)$ .
Theorem 4 solves the MMV problem: the value is $V(x,y,z,t)=-x+G(z,t)y$ , with an explicit saddle point.
Theorem 6 solves the auxiliary quadratic problem: $U_D(x,z,t)=-(x-D)^2/G(z,t)$ .
Theorem 7 gives the Lagrange multiplier and the optimal target.
(39) gives the optimal MV strategy.
The moment identities $\mathbb E[R_T]=\mathbb E[R_T^2]=H(z,t)=-1/G(z,t)$ .
Theorem 8: under Assumption 1 the optimal strategies coincide.
Lemma 4: the optimal MV wealth lies in $\mathcal G_\theta$ if and only if Assumption 1 holds.
(44)–(45): the mean and variance of the optimal wealth.

Significance

The result separates the two preferences by an observable property of the market. The Brownian theory gives agreement for free. With jumps the MV-optimal wealth can leave $\mathcal G_\theta$ , and that happens exactly when a jump of size $\zeta\gamma<-1$ can occur before the first jump with $\zeta\gamma=-1$ . In that case MMV and MV investors hold different portfolios. The paper's §5.4 examines in market data whether Assumption 1 is reasonable. The explicit closed forms (the value $-x+G(z,t)y$ , the variance $-(G(z,t)+1)/\theta^2$ of the optimal wealth, the efficient frontier) are what applied work uses.

The result is proved on paper, in an arXiv preprint later published in Mathematics of Operations Research (2025). None of it is machine-checked. A formal proof would check the verification arguments for a stochastic differential game with jumps, a Feynman–Kac representation with a jump density, and the comparison with Maccheroni et al.'s monotone hull. The paper's own proofs are brief at several of these steps. The underlying infrastructure (Itô calculus with Poisson jumps, Doléans-Dade exponentials, verification theorems) would be reusable for most of continuous-time portfolio theory.

Difficulty

The obvious argument would show $U_\theta=V_\theta$ along the optimal wealth and conclude. Lemma 4 shows this argument breaks: the optimal MV wealth need not lie in $\mathcal G_\theta$ . Remark 7 also notes that membership in $\mathcal G_\theta$ alone does not identify the optimal values; both optimal strategies must be found and compared.

Finding them needs a verification theorem for a two-player stochastic differential game with jumps (Theorems 1 and 4). That in turn needs Itô's formula for jump diffusions and martingale properties of Doléans-Dade exponentials that may vanish (Lemma 2, Mémin's criterion). Identifying the two strategies needs the moment identities $\mathbb E[R_T]=\mathbb E[R_T^2]=H$ , which come from a Feynman–Kac argument with a jump-driven density (Lemma 3). The converse direction needs a stopping argument at the first "bad" jump. None of this exists in Mathlib, which has Brownian motion but no stochastic integral and no Poisson process.

Formalization scope

Time is $[0,\infty)$ ; every process lives on $[t,T]$ with $t<T$ , and $\int_t^s$ is a difference of integral processes whose integrands vanish before $t$ .
Brownian integrals are the $L^2$ Itô integrals of Peng1990.SMP.Stochastic. The admissible classes $\mathcal A$ , $\mathcal B$ , $\mathcal M^t$ therefore contain only strategies whose Brownian integrands are in $L^2$ ; all strategies used in the paper qualify.
The Poisson random measure is JacodTodorov10.LLN.IsFPoisson with $\nu$ finite and $\nu(\{0\})=0$ . The compensated integral is the pathwise sum over atoms minus the compensator integral.
The filtration is the natural (uncompleted) filtration of $(W^1,W^2,N)$ .
Processes are adapted with càdlàg paths; $X_{s-}$ is Mathlib's Function.leftLim. Feedback strategies come with an existence claim, never as bare assumptions.
All optimal values are infima/suprema in EReal over the full admissible classes. Measures in $\mathcal Q_0$ are probability measures.
$\mathcal M^t$ is defined by the defining equation (5) of the stochastic exponential. The printed formula (4) has $\Delta X$ where $\Delta M$ is meant and is not used.
Proposition 1 is not formalized: its hypotheses do not deliver a classical solution. $G$ is a hypothesis: $G=-e^F$ with $F$ bounded, $C^{2,1}$ with bounded derivatives, solving (20). The Conditions of Proposition 1 are kept as printed. $\Sigma,\lambda,\beta>0$ is a standing hypothesis (implicit on p. 12).
Assumption 1 uses $\tau$ in $[0,\infty]$ ( $\inf\emptyset=\infty$ ), and "a.s." holds simultaneously for all $s\in(t,T]$ .
Printed slips: (37) evaluates $G_z/G$ at $(Z_s,t)$ ; it is read at $(Z_s,s)$ . Lemma 4's "Equation (1)" means (20)/(21).
Divisions by $1-\mathbb E[R_T]$ and $\mathrm{Var}[R_T]$ carry the hypotheses $\mathbb E[R_T]\neq1$ , $\mathrm{Var}[R_T]>0$ .

A formalization that replaces either optimal utility by a closed form or by the utility of one fixed strategy is out of scope: it assumes Theorems 4 and 7 and empties the goal. So is one that removes the jumps, freezes the factor, or replaces Assumption 1 by a sufficient condition such as $\gamma\ge0$ ; each of these makes the "only if" vacuous or false. Contributions that build general infrastructure (an Itô formula for jump diffusions, Doléans-Dade exponentials, a Feynman–Kac theorem) are especially welcome.

Selected references

B. Li, Z. Liang, L. Pang, Comparison Between Mean-Variance and Monotone Mean-Variance Preferences Under Jump Diffusion and Stochastic Factor Model, arXiv:2211.14473v2, 2023. https://arxiv.org/abs/2211.14473
F. Maccheroni, M. Marinacci, A. Rustichini, M. Taboga, Portfolio selection with monotone mean-variance preferences, Mathematical Finance 19(3):487–521, 2009. https://doi.org/10.1111/j.1467-9965.2009.00376.x
J. Trybuła, D. Zawisza, Continuous-time portfolio choice under monotone mean-variance preferences—stochastic factor case, Mathematics of Operations Research 44(3):966–987, 2019 (cited as [Trybuła and Zawisza 2019] in arXiv:2211.14473v2).
M. S. Strub, D. Li, A note on monotone mean–variance preferences for continuous processes, Operations Research Letters 48(4):397–400, 2020 (cited as [Strub and Li 2020] in arXiv:2211.14473v2).
P. Protter, Stochastic Integration and Differential Equations, 2nd ed., Springer, 2005, ISBN 978-3-662-10061-5.

15 thms1 active userReviewed

Missions

Nonzero-Sum Stochastic Differential Games with Impulse Controls: A Verification Theorem with Applications 2: An Explicit Family of Nash Equilibria for the Linear Impulse GameResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 4.7

Milestones

Significance

Difficulty

Formalization scope

Selected references

Stochastic Optimal Control: The Discrete-Time Case I: Finite-Horizon Abstract Dynamic Programming — the DP Algorithm Yields the N-Stage Optimal CostTextbook

Motivation

Setting

Formalization targets

Goal: Proposition 3.1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Optimal Electricity Demand Response Contracting with Responsiveness Incentives 2: The Producer's First-Best Value in Closed FormResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 3.1 (i)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Optimal Electricity Demand Response Contracting with Responsiveness Incentives 1: The Producer's Second-Best Value in Closed FormResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 3.2 (i)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Bellman's Dynamic Programming IX: Markovian Decision Processes and the Maximal Perron RootTextbook

Motivation

Setting

Formalization targets

Goal: Chapter XI, Theorem 2

Milestones

Significance

Difficulty

Formalization scope

Selected references

Bellman's Dynamic Programming VII: Convergence of Discrete Approximations in the Calculus of VariationsTextbook

Motivation

Setting

Formalization targets

Goal: Chapter IX, Theorem 2 (corrected)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Bellman's Dynamic Programming VI: Optimal Policies for the Continuous Gold-Mining ProcessTextbook

Motivation

Setting

Formalization targets

Goal: Chapter VIII, Theorem 1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Stability and Instability Results of the Wave Equation with a Delay Term in the Boundary or Internal Feedbacks IV: Arbitrarily Small Destabilizing Delays for Internal DampingResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1.4 for a≡1a \equiv 1a≡1

Milestones

Significance

Difficulty

Goal: Theorem 1.4 for $a \equiv 1$