Probability

Motivation

Many learning and risk-averse decision problems minimize a function of an expectation that is itself passed through another function: $F(x)=f(g(x))$ with $g(x)=\mathbb E[G(x,\xi)]$. Examples are mean–deviation risk measures, stochastic variational inequalities rewritten as minimization, and policy evaluation in reinforcement learning. Only noisy samples of $g$, of its Jacobian and of $\nabla f$ are available, and the plug-in estimate $\nabla g(x)^\top\nabla f(G)$ of $\nabla F(x)$ is biased because $f$ is nonlinear. Classical stochastic gradient analysis does not apply directly.

Timeline of sample complexities for smooth nonconvex two-level problems, measured by the number of samples needed to reach an $\varepsilon$-stationary point:

• 2017 — Wang, Fang and Liu (Math. Program.) introduce stochastic compositional gradient descent with two time scales; the unconstrained nonconvex rate is $O(\varepsilon^{-4})$ in their measure.
• 2017 — Wang, Liu and Fang (JMLR) accelerate it to $O(\varepsilon^{-2.25})$ for smooth unconstrained problems, still with two time scales.
• 2019–2020 — Ghadimi, Ruszczyński and Wang (arXiv:1812.01094, SIAM J. Optim. 2020) propose NASA, a single-time-scale method with one sample per iteration, and prove $O(\varepsilon^{-2})$ for constrained problems. This mission formalizes that result.

Setting

Problem (1.1) is

$$\min_{x\in X} F(x)=f(g(x)),$$

where $f:\mathbb R^m\to\mathbb R$ and $g:\mathbb R^n\to\mathbb R^m$ are continuously differentiable, $X\subseteq\mathbb R^n$ is closed and convex, and nothing is convex. Assumption 2 asks that $f$, $g$, $\nabla f$, $\nabla g$ be Lipschitz with constants $L_f,L_g,L_{\nabla f},L_{\nabla g}$; then $\nabla F$ is Lipschitz with $L_{\nabla F}=L_g^2L_{\nabla f}+L_fL_{\nabla g}$. $F^*$ is the infimum of $F$ over $X$.

For $\beta>0$ the subproblem solution is $\bar y(x,z,\beta)=\operatorname{argmin}_{y\in X}\{\langle z,y-x\rangle+\frac\beta2\|y-x\|^2\}=\Pi_X(x-z/\beta)$, with $\Pi_X$ the Euclidean projection. A pair $(x,z)$ is judged by the optimality measure

$$V(x,z)=\|\bar y(x,z,1)-x\|^2+\|z-\nabla F(x)\|^2,$$

which vanishes exactly when $z=\nabla F(x)$ and $-\nabla F(x)$ lies in the normal cone to $X$ at $x$.

The NASA method (Algorithm 1) keeps three sequences: iterates $x^k\in X$, gradient averages $z^k$ and value averages $u^k$. With parameters $a,b>0$, regularization $\beta>0$ and stepsizes $\tau_k\in(0,1/a]$:

$$x^{k+1}=x^k+\tau_k(\bar y(x^k,z^k,\beta)-x^k),\quad z^{k+1}=(1-a\tau_k)z^k+a\tau_k[J^{k+1}]^\top s^{k+1},\quad u^{k+1}=(1-b\tau_k)u^k+b\tau_kG^{k+1}.$$

Assumption 1 governs the oracle. Given $\mathcal F_k$, the outputs $G^{k+1}$, $J^{k+1}$ and $s^{k+1}$ are conditionally unbiased for $g(x^{k+1})$, $\nabla g(x^{k+1})$ and $\nabla f(u^k)$. Their second moments are bounded by $\sigma_G^2,\sigma_J^2,\sigma_s^2$, and $s^{k+1}$, $J^{k+1}$ are conditionally independent. The analysis rests on the merit function $W(x,z,u)=a(F(x)-F^*)-\eta(x,z)+\frac\gamma2\|g(x)-u\|^2$, where $\eta$ is the optimal value of the subproblem.

Formalization targets

Goal: Theorem 2(c), (3.37)

With $a=b=1$, $\beta=\big(\frac{(1+\alpha)^2}{\alpha}L_g^2+\frac\alpha4\big)L_{\nabla f}$ for some $\alpha>0$, $\tau_0=1$, $\tau_k=1/\sqrt N$ for $k\ge1$, $N\ge2$, and $R$ uniform on $\{1,\dots,N-1\}$:

$$\mathbb E[V(x^R,z^R)]\le\frac4{\sqrt N-1}\Big(\frac2{\alpha L_{\nabla f}}\big[\max(L_1,L_2)+\max(1,\beta^2)\big]\big[W(x^0,z^0,u^0)+\hat\sigma^2\big]+\sigma_J^2\sigma_s^2\Big).$$

The constants $L_1,L_2$ (3.32) and $\hat\sigma^2$ are explicit in the problem data. This is the paper's headline rate, and every other statement of the mission feeds it.

Milestones

1. Lemma 1: $\|\bar y(x,z,1)-x\|\le\max(1,\beta)\|\bar y(x,z,\beta)-x\|$.
2. Lemma 2: $\nabla F$ is $L_{\nabla F}$-Lipschitz.
3. Lemma 3: $\eta$ has an $L_{\nabla\eta}$-Lipschitz gradient in $(x,z)$.
4. (3.21): $\langle z,d\rangle+\beta\|d\|^2\le0$ for the subproblem step $d$.
5. Lemma 4: the pathwise descent inequality $c\sum\tau_k(\|d^k\|^2+\|g(x^k)-u^k\|^2)\le W(x^0,z^0,u^0)+\sum r^{k+1}$.
6. Proposition 1(a): moment bounds on $z^k$ and $d^k$.
7. Proposition 1(b): $\sum\mathbb E[r^{k+1}]\le\hat\sigma^2\sum\tau_k^2$.
8. (3.29): $V(x,z)\le\max(1,\beta^2)\|d\|^2+\|z-\nabla F(x)\|^2$.
9. Theorem 2(a): the weighted gradient-tracking error.
10. Theorem 2(b): the bound on $\mathbb E[V(x^R,z^R)]$ for general admissible stepsizes.

Significance

The result. Theorem 2(c) gives $\mathbb E[V(x^R,z^R)]\le\varepsilon$ after $O(\varepsilon^{-2})$ iterations with one oracle call each. That matches the complexity of stochastic gradient descent on single-level smooth nonconvex problems, so the nested structure costs only constants. The bound holds with constraints, and $z^R$ comes with a certified estimate of $\nabla F(x^R)$. The same merit-function technique underlies later single-time-scale methods for multi-level and conditional stochastic optimization.

Formalizing it. The result is proved on paper, not formalized. A machine-checked proof requires the whole chain, Lemma 4 through Theorem 2, to be stated with constants that the argument actually supports. Several printed constants do not meet that bar (see Formalization scope), so the formalization also certifies a corrected version of the theorem. The deterministic milestones (Lemmas 1–3, (3.21), (3.29)) are general facts about Euclidean projections and value functions of strongly convex subproblems, and other projected-gradient developments can reuse them.

Difficulty

The obvious approach fails. Analyzing $F(x^k)$ alone does not work because the step uses $z^k$, a biased and correlated estimate of $\nabla F(x^k)$, and its error does not vanish at a single time scale. The analysis instead tracks the coupled potential $W$. Each of its three terms needs a different tool: the descent lemma for $F$, the smoothness of the value function $\eta$ (Lemma 3, which needs differentiability of a parametric minimum), and a recursion for $u^k$. These pieces must combine under the single coupling condition (3.16). The probabilistic part is delicate as well. The cross terms vanish only in expectation, they require conditional independence of $J^{k+1}$ and $s^{k+1}$, and their integrability is not automatic. Theorem 2(a) adds a weighted unrolling of the $z$-recursion through the products $\Gamma_k$ and the summation condition (3.30).

Formalization scope

Points live in EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m). Jacobians are continuous linear maps with the operator norm, and $\nabla g(x)^\top$ is the adjoint. The projection is a function $P$ with the published predicate SpectralProjGrad.Shared.IsProjOnto X P, and $\bar y(x,z,\beta)=P(x-\beta^{-1}z)$. $\eta$ is the subproblem objective evaluated at $\bar y$, and Lemma 3 places $(x,z)$ in the $L^2$ product WithLp 2 (ℝⁿ × ℝⁿ). $F^*$ is sInf over $X$, and $F$ is assumed bounded below on $X$. The regularization $\beta_k\equiv\beta$ and the stepsizes are deterministic.

The randomness lives on a standard Borel probability space. Assumption 1 is stated with respect to any filtration to which $x^k,z^k,u^k$ are adapted, which includes the paper's natural filtration. It requires square-integrable oracle outputs, so that no conditional-expectation hypothesis is vacuous. Statements printed with conditional expectations on the left and constants on the right (Proposition 1, Theorem 2(a)) are stated in total expectation, which is what the proofs establish. Every conclusion about an expectation includes the integrability of the integrand, so a bound cannot hold because a non-integrable integral defaults to $0$. $\mathbb E[V(x^R,z^R)]$ is the $\tau$-weighted average of $\mathbb E[V(x^k,z^k)]$ over $k=1,\dots,N-1$ (3.34). Lemma 4 is deterministic: it holds along every path of the recursions, whatever the oracle outputs. The recursions tie $y^k$ to the projection and $z^k,u^k$ to the oracle outputs, so the goal cannot be satisfied by arbitrary sequences or by a vacuous oracle.

Corrections to printed constants, each stated in the item's Formalization Note:

• (3.18): the noise term of $r^{k+1}$ carries $\gamma b^2$, not $b^2$. The printed Lemma 4 has a counterexample.
• (3.26): $\hat\sigma^2$ uses $aL_{\nabla F}$, $\max(\sigma_J^2\sigma_s^2,\|z^0\|^2)/\beta^2$ (the $k=0$ term) and $\gamma b^2\sigma_G^2$.
• (3.33): the coefficient of $\max(1,\beta^2)\hat\sigma^2$ is $1/c$, not $a\bar c/c$. The two agree when $a\bar c=1$.
• (3.37): the denominator is $\alpha L_{\nabla f}$, not $\alpha L_{\nabla F}$, since the proof sets $c=\alpha L_{\nabla f}/4$. The proof also fixes $\gamma=\alpha L_{\nabla f}$ in $W$ and $\hat\sigma^2$.
• Proposition 1(a): the bound $\mathbb E\|z^k\|^2\le\sigma_J^2\sigma_s^2$ is false conditionally on $\mathcal F_{k-1}$ and is stated in expectation.
• Hypotheses the proofs use but the statements omit: $\tau_k\le1$, $b\tau_k\le1$, $a\beta\ge c$ and $\gamma b\ge2c$, $\tau_0=1/a$ (Theorem 2(a),(b)), $N\ge2$, and $L_{\nabla f}>0$.

The second claim (3.38) of Theorem 2(c) is excluded: its printed constant is smaller than what the proof gives. Theorem 3 (asymptotics) and the ASA variant of §4 are out of scope. Contributions are welcome at every milestone. Solvers will need Euclidean projection characterizations, differentiability of the squared distance to a convex set, conditional-independence product rules for conditional expectations, and Abel-type summation for the $\Gamma_k$ weights.

Selected references

• S. Ghadimi, A. Ruszczyński, M. Wang, A Single Time-Scale Stochastic Approximation Method for Nested Stochastic Optimization, arXiv:1812.01094v2, 2019; SIAM J. Optim. 30(1), 2020. https://arxiv.org/abs/1812.01094
• M. Wang, E. X. Fang, H. Liu, Stochastic compositional gradient descent: algorithms for minimizing compositions of expected-value functions, Math. Program. 161, 2017. https://doi.org/10.1007/s10107-016-1017-3
• M. Wang, J. Liu, E. X. Fang, Accelerating stochastic composition optimization, JMLR 18(105), 2017. https://jmlr.org/papers/v18/16-504.html
• S. Ghadimi, G. Lan, Stochastic first- and zeroth-order methods for nonconvex stochastic programming, SIAM J. Optim. 23(4), 2013. https://doi.org/10.1137/120880811
• A. Ruszczyński, Nonlinear Optimization, Princeton University Press, 2006.

Why trade credit terms matter

Most business-to-business sales are not paid in cash on delivery. The supplier lets the buyer pay later, which is trade credit, and often offers a discount for paying early. In the classic "2/10 net 30" the buyer gets 2% off for paying within 10 days and otherwise owes the full price in 30 days. Trade credit is a major source of short-term finance for firms. Empirical work documents both forms of contract: net terms, with one price and no discount, and two-part terms, with an early-payment discount. The discounts are large, and they vary a lot from one buyer to another (Petersen and Rajan 1997; Klapper, Laeven and Rajan 2012). The implied interest rate on a forgone discount is often far above a bank loan's. This raises two questions: why do cash-poor buyers use trade credit at all, and when should a supplier offer a discount?

Yang and Birge (Management Science 2018) answer this in a supplier–retailer model with a financially constrained retailer, who can finance inventory with a bank loan, with trade credit, or with both. Their answer is risk sharing. Trade credit is repaid out of realized sales, so the supplier bears part of the demand risk. She can therefore induce a larger order than a price-only contract does. The model builds on the selling-to-the-newsvendor model of Lariviere and Porteus (2001), and it complements the supplier-versus-bank analysis of Kouvelis and Zhao (2012). This mission formalizes the paper's main result on the structure of the optimal contract.

The model

A retailer buys a single good from a supplier at unit cost $c$ and sells it at unit price $p=1$. Demand is random with density $f$ on $[0,\infty)$. Its distribution function is $F(x)=\int_0^x f$, the complementary distribution function is $\bar F=1-F$, the failure rate is $h=f/\bar F$, and the generalized failure rate is $g(x)=x\,h(x)$. Demand has an increasing failure rate (IFR). The retailer has cash $K>0$.

The supplier offers a cash price $w_c$ and a credit price $w_t$, with $c\le w_c\le w_t\le 1$. The early-payment discount is $d_t=1-w_c/w_t$. If the retailer's cash does not cover his cash purchases, he borrows from a competitive bank. The bank loan is senior to trade credit. A bank and a supplier recovering a defaulted claim lose fractions $\alpha_b$ and $\alpha_t$ of what they recover, with $\alpha_b,\alpha_t\in[0,1]$.

Default is described by two thresholds. The bank-loan default threshold $\theta_b$ is the demand below which the bank is not repaid in full, and it equals the amount owed to the bank. The trade-credit default threshold $\theta_t\ge\theta_b$ is the demand below which the supplier is not repaid in full. The retailer uses a bank loan iff $\theta_b>0$, and uses trade credit iff $\theta_t>\theta_b$.

The paper shows (p. 13) that the supplier's problem can be written in the thresholds alone. Let

$$\hat F_b(x)=\bar F(x)[1-\alpha_b g(x)],\qquad C(\theta)=\frac{K+\int_0^\theta\hat F_b}{\hat F_b(\theta)}-\theta,$$ $$Q(\theta_b,\theta_t)=\min\{q\ge0:\ q\bar F(q)=[\theta_t+C(\theta_b)]\bar F(\theta_t)\}.$$

The retailer orders $Q$, the prices are $w_t=\bar F(Q)/\bar F(\theta_t)$ and $w_c=\hat F_b(\theta_b)w_t$, and the discount is $d_t=1-\hat F_b(\theta_b)$. The supplier's expected profit is

$$\Pi_s=K+\int_0^{\theta_t}\bar F(x)\,dx-c\,Q(\theta_b,\theta_t)-\Big[\alpha_b\int_0^{\theta_b}x\,dF(x)+\alpha_t\int_{\theta_b}^{\theta_t}(x-\theta_b)\,dF(x)\Big].$$

She maximizes $\Pi_s$ over a domain $\Theta$ of thresholds. A maximizer is an optimal trade credit contract. Net terms correspond to $\theta_b^*=0$, which is $d_t^*=0$. Two-part terms correspond to $\theta_b^*>0$.

Formalization targets

Goal: Proposition 3 (p. 15)

For every optimal contract $(\theta_b^*,\theta_t^*)$:

$$\theta_t^*>0\ \Longrightarrow\ \theta_b^*<\theta_t^*\qquad(\text{trade credit is always used}).$$

If $\alpha_t=0$, or if $K$ is sufficiently large, then $\theta_b^*=0$ and $d_t^*=0$ (net terms, no bank loan). If $\alpha_t>0$ and $K$ is sufficiently small, then

$$0<\theta_b^*<\theta_t^*,\qquad d_t^*>0\qquad(\text{two-part terms, both bank loan and trade credit}).$$

"Sufficiently large" and "sufficiently small" are existential thresholds on $K$ that depend on the data $(f,c,\alpha_b,\alpha_t)$, not on the contract.

Milestones

They are listed in the order the proof uses them:

1. Lemma C.4: $C$ is increasing, and convex when $\alpha_b=0$.
2. Corollary 3: $Q$ increases in $\theta_b$ and in $\theta_t$.
3. Lemma C.8: at $\alpha_b=0$, $\Pi_s$ is concave in $\theta_b$.
4. Lemma C.7: $Q$ increases in $\alpha_b$ and $K$.
5. Lemma C.9: $\Pi_s$ is concave in $\theta_t$.
6. Proposition 6, first sentence: $\Pi_s^*$ decreases in $\alpha_b$ and $\alpha_t$.

Significance

Proposition 3 is the paper's prediction about inventory financing portfolios. Once the supplier sets the terms, a retailer who needs external financing always uses trade credit. Early-payment discounts appear only when supplier default is costly and the retailer is cash-poor. A discount is then the supplier's way of moving part of the financing to the bank. The paper uses this to explain why discounts go to small, risky buyers, as observed by Klapper et al. (2012). The comparative statics of §5 (Propositions 4–6) are built on the same reduced problem.

The result is proved on paper but has not been formalized. The appendix lemmas it rests on (C.4, C.7, C.8, C.9) are stated without proof ("available upon request"). A machine-checked development would therefore settle whether these lemmas hold on the domain where the paper uses them. It would also produce a reusable library: IFR demand with failure rates, the bank-loan pricing kernel $\hat F_b$, and the implicit order quantity $Q$.

Difficulty

The order quantity $Q$ is defined implicitly, as the smaller root of a unimodal equation, and the paper's arguments differentiate through it with the implicit function theorem. Every derivative of $\Pi_s$ therefore involves $1/(\bar F(Q)[1-g(Q)])$, which blows up at the edge of $\Theta$ where $Q=g^{-1}(1)$. The density is only assumed continuous, so $\hat F_b$ and $C$ need not be differentiable when $\alpha_b>0$. Monotonicity and concavity have to be argued from the integral forms, or under a smoothness assumption the paper does not state.

The obvious argument for "sufficiently large $K$" also fails. It perturbs the optimum at $K$ just below $M^*=g^{-1}(1)\bar F(g^{-1}(1))$, but there the domain shrinks to a sliver near $\theta_t=0$, and the derivative of $\Pi_s$ in $\theta_t$ at $\theta_t=0$ can be negative. For exponential demand it tends to $-\infty$ as $K\to M^*$. The proof's claim that $\theta_t^*>0$ there is not part of the theorem. Part 1 for general $\alpha_b$ is reduced to $\alpha_b=0$ through Proposition 6, which requires comparing optima over domains that themselves depend on $\alpha_b$.

Formalization scope

All objects live in TradeCredit.Terms.Model.

Demand. Demand is a density $f:\mathbb R\to\mathbb R$ that is continuous on $[0,\infty)$, positive on $[0,\infty)$, zero on $(-\infty,0)$, integrable with total mass $1$, and has a weakly increasing failure rate on $[0,\infty)$. $F$ is the interval integral of $f$ from $0$. The normalizations are $p=1$ and $s=0$. The parameters satisfy $0<c<1$, $\alpha_b,\alpha_t\in[0,1]$ and $K>0$.

Domain. $\Theta$ is the printed set of Corollary 3 ($\theta_t\ge\theta_b\ge0$ and $[\theta_t+C(\theta_b)]\bar F(\theta_t)\le M^*$) plus two pinned constraints: $\theta_t\le Q(\theta_b,\theta_t)$ (that is, $w_t\le1$) and $c\le w_c$. These are the image under (11) of §3.1's $c\le w_c\le w_t\le 1$, which the printed $\Theta$ omits.

Statements. $Q$ is the infimum of the nonnegative roots. "The optimal contract" means every maximizer of $\Pi_s$ on $\Theta$. Existence of a maximizer is not asserted; the paper does not prove it. Monotonicity is weak, and concavity is Mathlib's ConcaveOn on the sections of $\Theta$. Proposition 6 is stated by comparing attained values with $\Pi_s^*=\sup_\Theta\Pi_s$.

Not in scope. The retailer's best response (Proposition 1) and the bijection between thresholds and contracts are not formalized. The goal is about the paper's own reduced problem. Lemma 1's first-order conditions are not a milestone: as printed they fail at a corner optimum $\theta_b^*=\theta_t^*=0$, and they need $C'$, which is not defined under a merely continuous density.

Ruling out trivialization. The large-$K$ clause quantifies over $K\in[\underline K,M^*)$ with $\underline K<M^*$. For $K\ge M^*$ the domain $\Theta$ has no point with $\theta_t>0$ and every "for every optimal contract" statement holds vacuously, so a large-$K$ clause that reached only those values would be empty.

Welcome contributions. Lemmas on IFR densities (positivity of $\bar F$, finiteness of the mean, monotonicity of $g$ and existence of $g^{-1}(1)$), the root structure of $q\bar F(q)$, and boundedness of $\Pi_s$ on $\Theta$ are reusable beyond this paper.

Source. The source PDF is the authors' accepted manuscript (LBS Research Online, eprint 801). All page numbers are the manuscript's.

Selected references

• S. A. Yang, J. R. Birge, Trade Credit, Risk Sharing, and Inventory Financing Portfolios, Management Science 64(8), 2018. https://doi.org/10.1287/mnsc.2017.2799
• M. A. Lariviere, E. L. Porteus, Selling to the Newsvendor: An Analysis of Price-Only Contracts, Manufacturing & Service Operations Management 3(4), 2001. https://doi.org/10.1287/msom.3.4.293.9971
• P. Kouvelis, W. Zhao, Financing the Newsvendor: Supplier vs. Bank, and the Structure of Optimal Trade Credit Contracts, Operations Research 60(3), 2012. https://doi.org/10.1287/opre.1120.1040
• M. A. Petersen, R. G. Rajan, Trade Credit: Theories and Evidence, Review of Financial Studies 10(3), 1997. https://doi.org/10.1093/rfs/10.3.661
• L. Klapper, L. Laeven, R. Rajan, Trade Credit Contracts, Review of Financial Studies 25(3), 2012. https://doi.org/10.1093/rfs/hhr122

Motivation

A firm launching a new experience good does not know how good the product is, and neither do its customers. Early buyers post reviews, and customers who wait learn from them: this is social learning (SL). Forward-looking customers anticipate this and may delay their purchase until reviews are available, which cuts into the firm's early sales. Papanastasiou and Savva (Management Science 2017) ask whether SL helps or hurts a monopolist facing such strategic consumers.

This mission formalizes their answer for responsive pricing, where the firm cannot commit to a second-period price and instead sets it after observing the reviews. Without learning, this is the classical price-skimming game of Besanko and Winston (1990), in which a firm without commitment power is hurt by consumer patience. With learning, two effects compete: reviews make the second-period market more informative (an informational effect the firm can exploit by repricing), and the option to learn makes waiting more attractive (a behavioral effect that hurts the firm).

Setting

A monopolist sells over two periods at unit cost $c\in[0,1)$ to a unit mass of consumers with preference types $x$ uniform on $[0,1]$. The mean quality is unknown, with prior $N(0,\sigma_p^2)$, and reviews are noisy with variance $\sigma_q^2$; the SL influence parameter is $\gamma=\sigma_p^2/\sigma_q^2\ge0$. Consumers discount second-period utility by $\delta_c\in[0,1]$; the firm does not discount.

If a set $B\subseteq[0,1]$ of types buys in period 1, its mass $|B|$ is the mass of reviews, and the posterior mean $q_u$, seen from period 1, has the pre-posterior law $N\big(0,\sigma_p^2\,\tfrac{|B|\gamma}{|B|\gamma+1}\big)$ (Lemma 1 and Definition 1 of the paper). In period 2 the remaining types value the product at $x+q_u$.

Under responsive pricing the firm sets $p_1$; consumers decide whether to buy now or wait; reviews realize $q_u$; the firm sets $p_2=s(q_u)$ to maximize the second-period profit

$$\pi_2(p_2)=(p_2-c)\,\big|\{x\in[0,1]\setminus B:\ x+q_u\ge p_2\}\big|.$$

An equilibrium after $p_1$ is a measurable buyer set $B$ and a measurable rule $s$ that is optimal at every $q_u$, such that every type in $B$ weakly prefers $x-p_1$ to the discounted expected value $\delta_c\,\mathbb E[(x+q_u-s(q_u))^+]$ of waiting, and every type outside $B$ weakly prefers waiting. The firm's expected profit is $\pi_r=(p_1-c)|B|+\mathbb E[\pi_2(s(q_u))]$, and $\pi_r^*$ is its supremum over all $p_1$ and all equilibria. The benchmark "absence of SL" ($\gamma\to0$ in the paper) is the same model at $\gamma=0$, where $q_u=0$ with certainty.

Formalization targets

Goal: Proposition 6

$$\gamma>0\ \Longrightarrow\ \exists\,\Delta_{lr}\in(0,1],\ \Delta_{hr}\in[0,1):\quad \delta_c\le\Delta_{lr}\ \text{or}\ \delta_c\ge\Delta_{hr}\ \Longrightarrow\ \pi_r^*\big|_{\gamma}>\pi_r^*\big|_{\gamma=0}.$$

The thresholds are left unspecified; the statement asserts only that SL raises the optimal profit near both ends of the patience range.

Milestones

1. Lemma 3: the second-period price $p_2^*(q_u,\bar x)$ of (6) is optimal when $[0,\bar x)$ remains.
2. (5): without SL, the first-period buyers are the types $x\ge\chi(p_1)=\frac{2p_1-c\delta_c}{2-\delta_c}$.
3. Proposition 4: the benchmark optimum $p_1^*=\frac{2c+\delta_c^2(1-c)+4(1-\delta_c)}{6-4\delta_c}$, $p_2^*=\frac{\chi(p_1^*)+c}{2}$, and monotonicity in $\delta_c$.
4. Lemma 4: with SL, the first-period threshold $\zeta(p_1)$ solves the implicit equation (7).
5. (8): the expected profit as a function of the threshold (with a corrected integrand).
6. Proposition 5: adoption inertia is never optimal; the on-path second-period price.
7. Example 3: the endpoint $\delta_c=0$.
8. Continuity of $\pi_r^*$ in $\delta_c\in[0,1]$ (proof of Proposition 6).

Significance

The result shows that the benefit of reviews to a firm that reprices dynamically, previously established for non-strategic consumers, survives when consumers strategically wait for information. It is one half of the paper's comparison between commitment and responsiveness: under SL the firm's flexibility to react to reviews becomes valuable, which reverses the classical ranking of pre-announced over responsive pricing.

The paper proves the result on paper only. This mission produces a machine-checked model of a two-period game with a continuum of consumers, Bayesian learning and subgame-perfect pricing, and machine-checked versions of the equilibrium characterizations. The paper's numerical evidence that the result holds for all $\delta_c$ is not part of the goal.

Difficulty

The first-period threshold is defined implicitly: in (7) the law of $q_u$ has a variance that depends on the threshold itself, and the second-period price inside the integral is a piecewise function of both. Existence, uniqueness and the comparison with the benchmark all go through this fixed-point equation.

The endpoint $\delta_c=1$ relies on Proposition 5(i), that inducing adoption inertia is strictly suboptimal. At $\delta_c=1$ the alternative price used in the printed proof yields exactly the inertia profit, so this endpoint is not settled by the page's witness. Passing from the two endpoints to the thresholds requires continuity of an optimal value taken over an unbounded price set and over implicitly defined equilibria; the paper cites the Maximum Theorem, whose hypotheses must be established.

Formalization scope

Everything lives in namespace SLPricing.Resp. The model file is shared, verbatim, with the two other missions of this series. Conventions:

• Standing assumptions: $\sigma_p>0$, $\gamma\ge0$, $\delta_c\in[0,1]$, $c\in[0,1)$; firm discount factor $1$; pure strategies.
• Best responses are weak, so buyer sets are unique only up to null sets.
• The second-period rule must be optimal at every realization and measurable. In the exit region $q_u\le c-\bar x$ every optimal price sells nothing; (6)'s value $c$ is a convention there.
• Optimal values are suprema in EReal over all real prices and all their equilibria, so neither an empty nor an unbounded family produces a junk value. Defining $\pi_r^*$ as the profit at a closed-form price, or the benchmark by dropping the second period, would make the goal circular; the formalization does neither.
• The thresholds are in the half-open intervals of the page; closed intervals would make the goal trivial.

Hypotheses added or restricted relative to the page, each disclosed in its item:

• (5) assumes $p_1\ge c$ (the printed formula is wrong below cost) and states uniqueness for $\delta_c<1$ (at $\delta_c=1$ non-threshold equilibria exist).
• Proposition 4 states uniqueness only for $\delta_c<1$ (at $\delta_c=1$ every $p_1\ge(1+c)/2$ is optimal).
• Lemma 4 assumes $p_1\ge0$; its monotonicity sentence is not posed.
• Lemma 3's uniqueness assumes $\bar x>0$ and $q_u>c-\bar x$.
• (8) is stated with last integrand $\zeta(q_u-c)$; the page prints $\zeta q_u$, which contradicts the proof of Lemma 3.

Contributions welcome: Gaussian integral estimates for (7), the second-period optimization of Lemma 3, a witness against inertia at $\delta_c=1$, and a continuity argument for optimal values over parametrized equilibria, which is reusable for the series' other missions.

Selected references

• Y. Papanastasiou, N. Savva, Dynamic Pricing in the Presence of Social Learning and Strategic Consumers, Management Science 63(4):919–939, 2017. https://doi.org/10.1287/mnsc.2015.2378 (cited from the accepted manuscript MS-14-00028.R2, 2016)
• D. Besanko, W. L. Winston, Optimal Price Skimming by a Monopolist Facing Rational Consumers, Management Science 36(5):555–567, 1990. https://doi.org/10.1287/mnsc.36.5.555
• Y. Aviv, A. Pazgal, Optimal Pricing of Seasonal Products in the Presence of Forward-Looking Consumers, Manufacturing & Service Operations Management 10(3):339–359, 2008. https://doi.org/10.1287/msom.1070.0183
• R. K. Sundaram, A First Course in Optimization Theory, Cambridge University Press, 1996. https://doi.org/10.1017/CBO9780511804526

Motivation

The stochastic linear quadratic (LQ) optimal control problem asks to steer a linear stochastic differential equation by a control so as to minimize a quadratic cost. It is the basic model of stochastic control: Wonham studied it in 1968 (Wonham 1968), and it is the model on which feedback design, mean-field control and LQ differential games are built (Yong–Zhou 1999).

Classically the cost weights are assumed nonnegative and the control weight $R$ uniformly positive definite, the standard conditions (1.4). Under them the Riccati equation has a unique solution and the optimal control is a linear state feedback. A stochastic problem can however be well posed when $R$ is indefinite, because the diffusion term also penalizes the control.

Timeline:

• 1998: Chen, Li and Zhou observe that a stochastic LQ problem can be solvable with an indefinite $R$ (SIAM J. Control Optim. 36).
• 2002: Ait Rami, Moore and Zhou introduce a generalized Riccati equation with a pseudoinverse and algebraic constraints (SIAM J. Control Optim. 40).
• 2014: Sun and Yong prove that closed-loop solvability is equivalent to the existence of a regular solution of that Riccati equation (SIAM J. Control Optim. 52).
• 2016: Sun, Li and Yong characterize strongly regular solvability by the uniform convexity of the cost functional (SIAM J. Control Optim. 54, Theorem 4.5). This mission is that theorem.

Setting

A probability space $(\Omega,\mathcal F,\mathbb P)$ carries a standard one-dimensional Brownian motion $W$. Its natural filtration, augmented by the $\mathbb P$-null sets, is $\mathbb F$. Fix a horizon $T>0$ and deterministic coefficients $A,C\in\mathbb R^{n\times n}$, $B,D\in\mathbb R^{n\times m}$, weights $Q\in\mathbb S^n$, $S\in\mathbb R^{m\times n}$, $R\in\mathbb S^m$ (functions of time) and $G\in\mathbb S^n$. The admissible controls $\mathcal U[t,T]$ are the $\mathbb F$-progressively measurable processes $u$ with $\mathbb E\int_t^T|u|^2ds<\infty$. The state from the initial pair $(t,x)$ solves

$$dX=(AX+Bu+b)\,ds+(CX+Du+\sigma)\,dW,\qquad X(t)=x,$$

and the cost is

$$J(t,x;u)=\mathbb E\Big\{\langle GX(T),X(T)\rangle+2\langle g,X(T)\rangle+\int_t^T\big[\langle QX,X\rangle+2\langle SX,u\rangle+\langle Ru,u\rangle+2\langle q,X\rangle+2\langle\rho,u\rangle\big]ds\Big\}.$$

Standing assumptions (H1)–(H2): $A\in L^1$, $B,C\in L^2$, $D\in L^\infty$, $Q\in L^1$, $S\in L^2$, $R\in L^\infty$ on $(0,T)$, and square-integrability of the random terms $b,\sigma,q,\rho,g$. No sign condition is imposed on $G$, $Q$ or $R$. The homogeneous problem (SLQ)$^0$ sets $b,\sigma,g,q,\rho=0$; its cost is $J^0$.

The map $u\mapsto J^0(0,0;u)$ is uniformly convex if, for some $\lambda>0$,

$$J^0(0,0;u)\ \ge\ \lambda\,\mathbb E\int_0^T|u(s)|^2ds\qquad\forall u\in\mathcal U[0,T].\qquad(4.2)$$

With $\Sigma_P=R+D^\top PD$ and $K_P=B^\top P+D^\top PC+S$, the Riccati equation is

$$\dot P+PA+A^\top P+C^\top PC+Q-K_P^\top\Sigma_P^\dagger K_P=0,\qquad P(T)=G,\qquad(4.6)$$

with $\dagger$ the Moore–Penrose pseudoinverse. A solution $P\in C([0,T];\mathbb S^n)$ is strongly regular if $\Sigma_P\ge\lambda I$ a.e. for some $\lambda>0$ (4.10).

Formalization targets

Goal: Theorem 4.5

$$\exists\lambda>0:\ J^0(0,0;u)\ge\lambda\,\mathbb E\!\int_0^T\!|u|^2ds\ \ \forall u\in\mathcal U[0,T]\iff(4.6)\text{ admits a strongly regular solution.}$$

The goal fixes no constant: the $\lambda$ on each side is existential.

Milestones

1. Lemma 2.2: the cost of a feedback control $\Theta X+u$, written through the solution of a Lyapunov equation.
2. Lemma 2.3: $u\mapsto u-\Theta X^{(u)}$ is bounded below, $\mathbb E\int|u-\Theta X^{(u)}|^2\ge\gamma\,\mathbb E\int|u|^2$.
3. Proposition 4.1: uniform convexity gives unique open-loop solvability and $V^0(t,x)\ge\alpha|x|^2$.
4. Proposition 4.4: every Lyapunov solution satisfies $R+D^\top PD\ge\lambda I$ and $P\ge\alpha I$, with the same $\lambda,\alpha$.
5. (4.20) and the monotonicity $P_1\ge P_i\ge P_{i+1}\ge\alpha I$ of the iteration (4.18)–(4.19).
6. Uniform convergence of the iteration to a strongly regular solution.
7. The completion of squares $J^0(0,0;u)=\mathbb E\int\langle\Sigma_P(u-\Theta X^{(u)}),u-\Theta X^{(u)}\rangle ds$.

Companion items: Remark 4.6 (the same $\lambda$ bounds $\Sigma_P$), the well-posedness of the state equation and the cost (Sun–Yong 2014, Proposition 2.1), and Proposition 3.5 (the standard conditions (1.4) imply uniform convexity).

Significance

Theorem 4.5 gives a checkable sufficient condition for the classical structure of LQ control: under (4.2) the Riccati equation has a solution whose gain matrix $R+D^\top PD$ is uniformly positive definite, so the optimal control is a state feedback with an invertible gain. It covers indefinite weights, and Proposition 3.5 shows that it contains the classical case (1.4). Combined with Sun–Yong's equivalence it yields Corollary 4.7, the feedback representation of the open-loop optimal control, which later missions of this series use.

The results are proved in the paper. As far as is known they have no machine-checked proof. Formalizing them requires stochastic calculus for controlled SDEs (Itô's formula for quadratic forms of a state process) linked to matrix ODE theory. The definitions this mission fixes (the LQ problem, the Riccati and Lyapunov equations with a pseudoinverse) can be reused by the other missions of the series and by any stochastic LQ formalization.

Difficulty

The direction (ii) ⇒ (i) is a completion of squares followed by Lemma 2.3. Lemma 2.3 is not obvious: it asserts a bounded inverse for an operator defined through an SDE.

The direction (i) ⇒ (ii) is the hard one. The obvious approach would solve (4.6) directly, but (4.6) is nonlinear and its coefficient $\Sigma_P^\dagger$ may be singular. No sign condition gives a priori bounds. The paper instead builds a policy-iteration sequence of linear Lyapunov equations. The difficulty is to show that every iterate keeps $R+D^\top P_iD\ge\lambda I$, so that the next gain is defined, and stays bounded below. These bounds come from the cost functional (Proposition 4.4), not from the matrix equation. Uniform convergence of the iterates then needs integrable estimates under the weak integrability of (H1).

Formalization scope

• Basis. The paper's $(\Omega,\mathcal F,\mathbb P,W)$ is a probability measure with a standard Brownian motion IsStdBrownian (Mathlib's IsBrownianReal per coordinate, published module Peng1990.SMP.Stochastic). $\mathbb F$ is augmentedFiltration (published ReflectedBSDE.Existence.Setting).
• State and cost. The state from $(t,x)$ is an Itô solution from time $0$ whose coefficients are switched on at $t$, with continuous paths and $\mathbb E\sup|X|^2<\infty$. $J$ is evaluated along a chosen solution, which is unique; the item state_wellposed poses existence, uniqueness and integrability of the cost. Expectations are Bochner integrals, and $|u|^2$ is the Euclidean $u\cdot u$.
• Integrability and values. $L^p$ conditions on matrix functions are entrywise. The diffusion coefficients $C,D$ are taken Borel measurable on $[0,\infty)$ (a measurable representative of their class), so that the Itô integrand $CX+Du+\sigma$ of (1.1) is progressively measurable. $V$ is an EReal infimum over admissible controls.
• Matrix ODEs. The Riccati and Lyapunov equations are in integral form: continuous symmetric $P$, an integrable right-hand side, and $P(t)=G+\int_t^TF(s,P(s))ds$. The pseudoinverse is the published HarmonicGames.Decomposition.pinv. Where the paper prints $(\cdot)^{-1}$ ((4.19), p. 2290) Lean's matrix inverse is used; it is invertible there by $R+D^\top PD\ge\lambda I$.
• The iteration. The sequence of milestones 5–6 is given by hypotheses: $P_0$ solves (4.18) and $P_{i+1}$ the Lyapunov equation of $\Theta_i$. Lyapunov solutions are unique, so this is the paper's sequence.
• Constants. $\lambda$ and $\alpha$ in Proposition 4.4 and Remark 4.6 are the constants of (4.2) and (4.1), passed as parameters.

Ruling out trivial forms. Uniform convexity is not defined through the operator $M_2(0)$ of (3.8), and strong regularity includes the integral Riccati equation. A formalization that drops the Riccati equation, or reads uniform convexity off a matrix condition, is a different theorem. No positivity of $G$, $Q$ or $R$ is assumed anywhere except in Proposition 3.5, whose hypothesis (1.4) is exactly that.

Contributions welcome: Itô's formula for $\langle P(s)X(s),X(s)\rangle$ with a $C^1$ (or absolutely continuous) matrix $P$; existence and uniqueness for linear SDEs with $L^1/L^2$ coefficients; existence and uniqueness for linear matrix ODEs; the Penrose identities for pinv.

Selected references

• J. Sun, X. Li, J. Yong, Open-Loop and Closed-Loop Solvabilities for Stochastic Linear Quadratic Optimal Control Problems, SIAM J. Control Optim. 54 (2016), 2274–2308. https://doi.org/10.1137/15M103532X
• J. Sun, J. Yong, Linear Quadratic Stochastic Differential Games: Open-Loop and Closed-Loop Saddle Points, SIAM J. Control Optim. 52 (2014), 4082–4121. https://doi.org/10.1137/140953642
• M. Ait Rami, J. B. Moore, X. Y. Zhou, Indefinite Stochastic Linear Quadratic Control and Generalized Differential Riccati Equation, SIAM J. Control Optim. 40 (2002), 1296–1311. https://doi.org/10.1137/S0363012900371083
• S. Chen, X. Li, X. Y. Zhou, Stochastic Linear Quadratic Regulators with Indefinite Control Weight Costs, SIAM J. Control Optim. 36 (1998), 1685–1702. https://doi.org/10.1137/S0363012996310478
• W. M. Wonham, On a Matrix Riccati Equation of Stochastic Control, SIAM J. Control 6 (1968), 681–697. https://doi.org/10.1137/0306044
• J. Yong, X. Y. Zhou, Stochastic Controls: Hamiltonian Systems and HJB Equations, Springer, 1999. https://doi.org/10.1007/978-1-4612-1466-3

Why open-loop and closed-loop solvability must be told apart

In a stochastic linear–quadratic (LQ) optimal control problem a controller steers a linear stochastic differential equation and pays a quadratic cost. When the cost weights are allowed to be indefinite — as in mean–variance portfolio selection, where the control weight is zero — the problem can still be well posed, and two different notions of solution appear. An open-loop optimal control is a process chosen for one given initial pair $(t,x)$. A closed-loop optimal strategy is a feedback law $u=\Theta X+v$ that is optimal for every initial state at once. A closed-loop optimal strategy yields an open-loop optimal control for each initial state; the converse is the question.

Timeline. Chen, Li and Zhou (1998, doi:10.1137/S0363012996310478) started the theory of indefinite stochastic LQ control. Ait Rami, Moore and Zhou (2002, doi:10.1137/S0363012900371083) introduced the generalized Riccati equation with a Moore–Penrose pseudoinverse and stated that, for Problem (SLQ)$^0$ with continuous coefficients and $S=0$, a continuous open-loop optimal control exists at every initial pair if and only if the Riccati equation has a solution satisfying a range condition and a sign condition. Sun and Yong (2014, doi:10.1137/140953642) characterized closed-loop solvability by regular solutions of that Riccati equation. Sun, Li and Yong (2016, doi:10.1137/15M103532X) showed by two explicit examples that the 2002 equivalence fails in both directions, and that open-loop solvability is strictly weaker than closed-loop solvability. This mission formalizes those examples.

Setting

Let $W$ be a standard one-dimensional Brownian motion on a probability space $(\Omega,\mathcal F,\mathbb P)$ and $\mathbb F$ its augmented natural filtration. For $(t,x)\in[0,T)\times\mathbb R^n$ and a control $u$ in the space $\mathcal U[t,T]$ of $\mathbb F$-progressively measurable $\mathbb R^m$-valued processes with $\mathbb E\int_t^T|u|^2ds<\infty$, the state equation is

$$dX=(AX+Bu+b)\,ds+(CX+Du+\sigma)\,dW,\qquad X(t)=x,$$

and the cost $J(t,x;u)$ is the expectation of $\langle GX(T),X(T)\rangle+2\langle g,X(T)\rangle$ plus the time integral of a quadratic form in $(X,u)$ with weights $Q,S,R$ and linear terms $q,\rho$. Problem (SLQ)$^0$ is the case $b=\sigma=g=q=\rho=0$, with cost $J^0$ and value function $V^0(t,x)=\inf_{u\in\mathcal U[t,T]}J^0(t,x;u)$.

The Riccati equation (4.6) is

$$\dot P+PA+A^\top P+C^\top PC+Q-(PB+C^\top PD+S^\top)(R+D^\top PD)^\dagger(B^\top P+D^\top PC+S)=0,\qquad P(T)=G,$$

where $M^\dagger$ is the Moore–Penrose pseudoinverse. A solution is regular if (4.7) $\mathcal R(B^\top P+D^\top PC+S)\subseteq\mathcal R(R+D^\top PD)$ a.e., (4.8) $(R+D^\top PD)^\dagger(B^\top P+D^\top PC+S)\in L^2$, and (4.9) $R+D^\top PD\ge 0$ a.e.

Example 7.1 is Problem (SLQ)$^0$ with $n=1$, $m=2$, $T=1$:

$$dX=[u_1+u_2]\,ds+[u_1-u_2]\,dW,\qquad J^0(t,x;u)=\mathbb E\,X(1)^2,$$

that is, $A=C=Q=0$, $B=(1,1)$, $D=(1,-1)$, $G=1$, $S=0$, $R=0$.

Formalization targets

Goal: Example 7.1

For every $(t,x)\in[0,1)\times\mathbb R$,

$$u^*_{(t,x)}(s)=-\Big(\frac{x}{2-2t},\frac{x}{2-2t}\Big)^\top\ \text{is open-loop optimal},\qquad V^0(t,x)=0,$$

while $V^0(1,x)=x^2$, and for every $t\in[0,1)$ the problem is not closed-loop solvable on $[t,1]$.

Milestones

1. (7.3): the Riccati equation has the unique solution $P\equiv1$, and it violates (4.7).
2. Theorem 4.3 for (SLQ)$^0$: closed-loop solvability on $[t,T]$ is equivalent to the existence of a regular solution on $[t,T]$.
3. (7.5)–(7.6): with $R$ replaced by $R+\varepsilon I$ the Riccati equation has the strongly regular solution $P_\varepsilon(t)=\varepsilon/(\varepsilon+2-2t)$.
4. (7.7): $P_\varepsilon(t)\to 0$ for $t<1$ and $P_\varepsilon(1)=1$.
5. (7.9)–(7.10): the closed-loop state and control of the regularized problem, $u_\varepsilon=-\big(\frac{x}{\varepsilon+2-2t},\frac{x}{\varepsilon+2-2t}\big)^\top$.
6. $u_\varepsilon\to u^*_{(t,x)}$ in $L^2$ as $\varepsilon\to0$.

Companion: Example 7.2

For $dX=u\,ds$ and $J=X(1)^2+\int_t^1s^2u^2ds$, the Riccati equation (7.12) has the unique solution $P(t)=t$, which satisfies (4.7) and (4.9), yet no open-loop optimal control exists at $(0,x)$, $x\neq0$.

Significance

The result. Example 7.1 refutes the necessity half of the Ait Rami–Moore–Zhou criterion: a continuous open-loop optimal control exists at every initial pair, but the Riccati equation has no regular solution. Example 7.2 refutes the sufficiency half. Together they show that the Riccati equation with conditions (4.7) and (4.9) characterizes neither notion, and that open-loop solvability is strictly weaker than closed-loop solvability; Example 7.1 also exhibits a finite value function that is discontinuous in time. These facts are why the paper develops separate characterizations of open-loop solvability (through the regularized Riccati solutions $P_\varepsilon$) instead of the Riccati equation itself.

Formalizing it. The examples are proved in the paper by appeal to its Theorems 5.3 and 6.2 and to Theorem 4.3 from Sun–Yong (2014). Nothing in this chain is machine-checked anywhere. A formal proof of the goal must verify the explicit optimal control against the canonical stochastic state equation, compute the value function, and rule out every closed-loop strategy; it can use Theorem 4.3 (posed here as a milestone) or a direct argument. The definitions built here (the stochastic LQ problem, the pseudoinverse Riccati equation, regularity) are shared with the other missions of this series.

Difficulty

Open-loop optimality looks immediate because $J^0=\mathbb EX(1)^2\ge0$, but it requires showing that the state driven by $u^*$ hits $0$ at time $1$, which means identifying the solution of the stochastic state equation for this control. The value at $t=1$ requires the degenerate interval $[1,1]$ to be handled inside the same SDE framework. The hard part is the negative claim: it quantifies over all feedback pairs $(\Theta,v)$ with $\Theta\in L^2$, and must show that no such pair drives every initial state to $0$ at time $1$. The paper reduces this to Theorem 4.3, whose proof (in Sun–Yong 2014) is a substantial piece of stochastic LQ theory; checking that $P\equiv 1$ fails the range condition is the easy end of that chain.

Formalization scope

Time is $\mathbb R_{\ge0}$, vectors are Fin k → ℝ, inner products are dot products, and $|u|^2=u\cdot u$. The Brownian motion is the published Peng1990.SMP.IsStdBrownian, the filtration the published augmented filtration, the SDE solution concept the published Peng1990.SMP.SolvesSDE, and the pseudoinverse the published HarmonicGames.Decomposition.pinv.

• The state from $(t,x)$ is an SDE from time $0$ with coefficients switched on at $t$, with a.s. continuous paths and $\mathbb E\sup|X|^2<\infty$; the cost uses a chosen solution, unique by [23, Proposition 2.1].
• Value functions are infima in the extended reals over admissible controls.
• The Riccati equation is in integral form on $[t_0,T]$; regularity is (4.7)–(4.9) on $[t_0,T]$.
• A closed-loop optimal strategy on $[t,T]$ requires $\Theta\in L^2(t,T)$, $v\in\mathcal U[t,T]$, and, for every initial state, a solution of the closed-loop system that is no worse than any admissible control.
• Theorem 4.3 is stated on $[t,T]$ (the paper states it on $[0,T]$ and applies it on $[t,1]$).
• The goal places no hypotheses on the probability space beyond the Brownian motion.

Proving only that $P\equiv1$ violates (4.7) does not settle the goal: the goal is about solvability of the control problem itself, and "not closed-loop solvable on any $[t,1]$" is stated for every $t<1$, not as the failure on some interval.

Contributions are welcome on any milestone, on the well-posedness of linear SDEs in this framework, and on the pseudoinverse identities (Penrose equations, the pseudoinverse of a scaled symmetric matrix) that the Riccati computations need.

Selected references

• J. Sun, X. Li, J. Yong, Open-loop and closed-loop solvabilities for stochastic linear quadratic optimal control problems, SIAM J. Control Optim. 54(5) (2016) 2274–2308. doi:10.1137/15M103532X
• M. Ait Rami, J. B. Moore, X. Y. Zhou, Indefinite stochastic linear quadratic control and generalized differential Riccati equation, SIAM J. Control Optim. 40 (2002) 1296–1311. doi:10.1137/S0363012900371083
• J. Sun, J. Yong, Linear quadratic stochastic differential games: open-loop and closed-loop saddle points, SIAM J. Control Optim. 52 (2014) 4082–4121. doi:10.1137/140953642
• S. Chen, X. Li, X. Y. Zhou, Stochastic linear quadratic regulators with indefinite control weight costs, SIAM J. Control Optim. 36 (1998) 1685–1702. doi:10.1137/S0363012996310478

Motivation

Linear–quadratic (LQ) optimal control is the basic test case of stochastic control: a linear stochastic differential equation, a quadratic cost, and an optimal control that one expects to be a linear feedback of the state computed from a Riccati equation. In the indefinite stochastic case the weighting matrices $G$, $Q$, $R$ carry no sign condition. The cost can then be convex without being uniformly convex, an optimal control may fail to exist although the value is finite, and the Riccati equation may have no solution of the kind the classical theory needs.

Sun, Li and Yong (SIAM J. Control Optim. 54 (2016) 2274–2308) separate finiteness, convexity, open-loop solvability and closed-loop solvability for this problem. This mission covers their Section 6. Under uniform convexity the optimal control is the Riccati feedback of Corollary 4.7. Section 6 removes uniform convexity: it regularizes the control weight $R$ to $R+\varepsilon I$, takes the Riccati feedback control $u_\varepsilon$ of each regularized problem, and shows that open-loop solvability of the original problem is exactly the convergence of $u_\varepsilon$ along some sequence $\varepsilon_k\to0$.

Timeline. Chen, Li and Zhou (SIAM J. Control Optim. 36 (1998)) introduced indefinite stochastic LQ problems. Ait Rami, Moore and Zhou (SIAM J. Control Optim. 40 (2002)) introduced the generalized Riccati equation with a pseudoinverse. Sun and Yong (SIAM J. Control Optim. 52 (2014)) characterized closed-loop solvability by regular solutions of that equation. In 2016 Sun, Li and Yong characterized uniform convexity by strongly regular solutions and open-loop solvability by the regularized feedback sequence treated here.

Setting

Fix a horizon $T>0$ and a probability space carrying a one-dimensional standard Brownian motion $W$, with $\mathbb F$ the augmented natural filtration of $W$. For an initial pair $(t,x)\in[0,T)\times\mathbb R^n$ and an admissible control $u\in\mathcal U[t,T]$, an $\mathbb F$-progressively measurable $\mathbb R^m$-valued process with $\mathbb E\int_t^T|u|^2ds<\infty$, the state solves

$$dX=(AX+Bu+b)\,ds+(CX+Du+\sigma)\,dW,\qquad X(t)=x .$$

The cost is

$$J(t,x;u)=\mathbb E\Big[\langle GX(T),X(T)\rangle+2\langle g,X(T)\rangle+\int_t^T\big(\langle QX,X\rangle+2\langle SX,u\rangle+\langle Ru,u\rangle+2\langle q,X\rangle+2\langle\rho,u\rangle\big)ds\Big].$$

The coefficients $A,B,C,D,Q,S,R$ and $G$ are deterministic, $b,\sigma,q,\rho,g$ are random, and the integrability conditions are (H1)–(H2). The value function is $V(t,x)=\inf_uJ(t,x;u)\in[-\infty,\infty)$. A control $u^*$ is open-loop optimal at $(t,x)$ if $J(t,x;u^*)\le J(t,x;u)$ for every $u\in\mathcal U[t,T]$. Problem (SLQ)$^0$ is the case $b,\sigma,g,q,\rho=0$, with cost $J^0$.

For $\varepsilon>0$ let $P_\varepsilon$ be the strongly regular solution of the Riccati equation (5.7),

$$\dot P_\varepsilon+P_\varepsilon A+A^\top P_\varepsilon+C^\top P_\varepsilon C+Q-K_\varepsilon^\top\Sigma_\varepsilon^{-1}K_\varepsilon=0,\qquad P_\varepsilon(T)=G,$$

where $\Sigma_\varepsilon=R+\varepsilon I+D^\top P_\varepsilon D\ge\lambda I$ for some $\lambda>0$ and $K_\varepsilon=B^\top P_\varepsilon+D^\top P_\varepsilon C+S$. Let $(\eta_\varepsilon,\zeta_\varepsilon)$ be the adapted solution of the linear backward equation (4.11) for these data, and put

$$\Theta_\varepsilon=-\Sigma_\varepsilon^{-1}K_\varepsilon,\qquad v_\varepsilon=-\Sigma_\varepsilon^{-1}\big(B^\top\eta_\varepsilon+D^\top\zeta_\varepsilon+D^\top P_\varepsilon\sigma+\rho\big).$$

With $X_\varepsilon$ the solution of the closed-loop system $dX_\varepsilon=[(A+B\Theta_\varepsilon)X_\varepsilon+Bv_\varepsilon+b]ds+[(C+D\Theta_\varepsilon)X_\varepsilon+Dv_\varepsilon+\sigma]dW$, $X_\varepsilon(t)=x$, the regularized feedback sequence is

$$u_\varepsilon=\Theta_\varepsilon X_\varepsilon+v_\varepsilon,\qquad\varepsilon>0 .$$

$\mathcal U[t,T]=L^2_{\mathbb F}(t,T;\mathbb R^m)$ is a Hilbert space with inner product $\mathbb E\int_t^T\langle u,v\rangle ds$; weak and strong convergence of controls refer to it.

Formalization targets

Goal: Theorem 6.2

Assume (H1)–(H2) and that $u\mapsto J^0(0,0;u)$ is convex. For $(t,x)\in[0,T)\times\mathbb R^n$ the following are equivalent:

$$\text{(SLQ) is open-loop solvable at }(t,x)\iff\exists\,\varepsilon_k\downarrow0:\ u_{\varepsilon_k}\rightharpoonup u^*\iff\exists\,\varepsilon_k\downarrow0:\ u_{\varepsilon_k}\to u^*\text{ in }\mathcal U[t,T],$$

and every weak or strong limit of such a subsequence is an open-loop optimal control at $(t,x)$. The goal assumes convexity, not uniform convexity, and no finiteness.

Milestones

1. Corollary 3.4: convexity of $J(t,x;\cdot)$ or $J^0(t,x;\cdot)$ at one $x$, at every $x$, and $J^0(t,0;u)\ge0$ on $\mathcal U[t,T]$ are equivalent.
2. The zero extension (4.3): $J^0(t,0;u)=J^0(0,0;0I_{[0,t)}\oplus u)$.
3. Corollary 4.7: under uniform convexity, the Riccati feedback control (4.28) is the unique open-loop optimal control.
4. Theorem 6.1: if the problem is finite, $\lim_{\varepsilon\to0^+}J(t,x;u_\varepsilon)=V(t,x)$.
5. Lemma 6.3: in a Hilbert space the norm is weakly lower semicontinuous, and strong convergence is weak convergence plus convergence of norms.
6. (6.7): $\mathbb E\int_t^T|u_\varepsilon|^2ds\le(V_\varepsilon-V)/\varepsilon\le\mathbb E\int_t^T|v^*|^2ds$ for any optimal $v^*$.
7. Weak lower semicontinuity of $u\mapsto J(t,x;u)$.

Two further statements follow the goal: open-loop solvability is equivalent to $\sup_{\varepsilon>0}\mathbb E\int_t^T|u_\varepsilon|^2ds<\infty$ (p. 2303), and Proposition 6.4: if $\sup_{\varepsilon>0}\int_0^T|\Theta_\varepsilon|^2ds<\infty$, the Riccati equation (4.6) has a regular solution and Problem (SLQ)$^0$ is closed-loop solvable.

Significance

Theorem 6.1 gives a minimizing sequence computed from Riccati and backward equations whenever the problem is finite. Theorem 6.2 turns it into a test for open-loop solvability that needs no uniform convexity and no regular solution of the original Riccati equation. When an optimal control exists, it is recovered as the limit of feedback controls. Proposition 6.4 converts a bound on the gains $\Theta_\varepsilon$ into closed-loop solvability of the homogeneous problem. Section 7 of the paper shows that open-loop solvability does not imply closed-loop solvability, so a criterion phrased directly in open-loop terms is needed.

All of these results are proved in the paper. None of them, nor the solution theory of stochastic LQ problems they rest on, had a machine-checked proof on Prove2Me or in Mathlib as of October 2026. A formal development needs the well-posedness of linear SDEs and BSDEs with integrable coefficients, the Riccati theory of Section 4, and the Hilbert-space structure of the space of admissible controls. Those parts are reusable for any stochastic LQ problem.

Difficulty

The obvious approach takes any minimizing sequence and extracts a weakly convergent subsequence. That fails without uniform convexity: a minimizing sequence need not be bounded, and boundedness is exactly what open-loop solvability provides in (6.7). The converse direction needs the limit of the regularized costs to identify the value, which requires both the minimizing property of $u_\varepsilon$ (Theorem 6.1) and weak lower semicontinuity of $J$. That in turn rests on convexity being transported from $J^0(0,0;\cdot)$ to $J(t,x;\cdot)$ through Corollary 3.4 and the zero extension. Upgrading weak to strong convergence uses the norm bound (6.7) with the limit itself as the optimal control. Every step depends on Corollary 4.7, the Riccati representation of the optimal control of the regularized problem, whose proof requires the theory of Section 4.

Formalization scope

The probability basis is a probability space with a one-dimensional standard Brownian motion and its augmented natural filtration. Vectors are Fin k → ℝ and matrices Matrix (Fin k) (Fin l) ℝ. Time is ℝ≥0, and $|u|^2$ is the Euclidean dot product u ⬝ᵥ u. (H1)–(H2) are standing assumptions, with entrywise $L^p$ conditions on the matrix coefficients. The state from $(t,x)$ is a strong solution of the published SDE notion Peng1990.SMP.SolvesSDE whose coefficients are switched on at $t$; it has a.s. continuous paths and $\mathbb E\sup|X|^2<\infty$. The cost is evaluated along a chosen solution, which is unique. $V$ is an infimum in the extended reals. Limits in $\varepsilon$ are taken as $\varepsilon\to0^+$. "A subsequence" is a sequence $\varepsilon_k>0$ with $\varepsilon_k\to0$, and the limit control is required to be admissible. The backward equations use the published Peng1990.SMP.SolvesBSDE, and the pseudoinverse in (4.6) and (4.11) is the published HarmonicGames.Decomposition.pinv.

Theorem 6.1 prints the term $-\Theta_\varepsilon^\top\rho$ in its backward equation. The equation (4.11) that its proof uses through Corollary 4.7 has $+\Theta_\varepsilon^\top\rho$, and the formalization uses (4.11). Corollary 3.4 is stated without its item (vi), which involves an operator $M_2(t)$ that the paper quotes from another source.

The families $P_\varepsilon$, $(\eta_\varepsilon,\zeta_\varepsilon)$ and $X_\varepsilon$ are hypotheses pinned by their equations for every $\varepsilon>0$. The sequence $u_\varepsilon$ is therefore the Riccati feedback sequence (6.2), never an arbitrary minimizing sequence or an arbitrary family of $\varepsilon$-optimal controls; with such a family the implication (ii) ⇒ (i) would be a different theorem.

Contributions are welcome at every level: the solution theory of linear SDEs and BSDEs, Itô's formula for quadratic forms, Riccati and Lyapunov equations in integral form, weak compactness in $L^2_{\mathbb F}$, and the milestones themselves.

Selected references

• J. Sun, X. Li, J. Yong, Open-loop and closed-loop solvabilities for stochastic linear quadratic optimal control problems, SIAM J. Control Optim. 54(5) (2016) 2274–2308. https://doi.org/10.1137/15M103532X
• J. Sun, J. Yong, Linear quadratic stochastic differential games: open-loop and closed-loop saddle points, SIAM J. Control Optim. 52(6) (2014) 4082–4121. https://doi.org/10.1137/140953642
• S. Chen, X. Li, X. Y. Zhou, Stochastic linear quadratic regulators with indefinite control weight costs, SIAM J. Control Optim. 36(5) (1998) 1685–1702. https://doi.org/10.1137/S0363012996310478
• M. Ait Rami, J. B. Moore, X. Y. Zhou, Indefinite stochastic linear quadratic control and generalized differential Riccati equation, SIAM J. Control Optim. 40(4) (2002) 1296–1311. https://doi.org/10.1137/S0363012900371083
• S. Peng, A general stochastic maximum principle for optimal control problems, SIAM J. Control Optim. 28(4) (1990) 966–979. https://doi.org/10.1137/0328054