Probability

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

Motivation

Linear–quadratic (LQ) optimal control is the basic test case of stochastic control: a linear stochastic differential equation, a quadratic cost, and a value function that one expects to be a quadratic form in the initial state. In the indefinite stochastic case the weighting matrices $G$, $Q$, $R$ carry no sign condition, and the classical picture breaks down. Without a sign condition the infimum of the cost can be $-\infty$. Before one can ask whether an optimal control exists, one has to ask whether the problem is finite, i.e. whether its value function stays above $-\infty$.

Sun, Li and Yong (SIAM J. Control Optim. 54 (2016) 2274–2308) separate the notions of finiteness, convexity, open-loop and closed-loop solvability for this problem. This mission covers their Section 5. Section 5 characterizes finiteness of the homogeneous problem by a family of regularized Riccati equations, and Example 5.2 shows that convexity of the cost alone is not enough.

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 finiteness by the limit of the regularized solutions 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, and $b,\sigma,q,\rho,g$ are random; the integrability conditions are (H1)–(H2). The value function is $V(t,x)=\inf_{u}J(t,x;u)\in[-\infty,\infty)$. Problem (SLQ)$^0$ is the case $b,\sigma,g,q,\rho=0$; its cost and value are $J^0$ and $V^0$. The problem is finite at $t$ if $V(t,x)>-\infty$ for all $x$, and finite if this holds for every $t\in[0,T]$.

Write $\Sigma_\varepsilon(P)=R+\varepsilon I+D^\top PD$ and $K(P)=B^\top P+D^\top PC+S$. The regularized Riccati equation (5.7) is

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

A solution is strongly regular if $\Sigma_\varepsilon(P_\varepsilon)\ge\lambda I$ a.e. for some $\lambda>0$. Further, $M_0$ solves the Lyapunov equation (3.2), $\dot M_0+M_0A+A^\top M_0+C^\top M_0C+Q=0$, $M_0(T)=G$, and $\Phi_A$ solves $\dot\Phi_A=A\Phi_A$, $\Phi_A(0)=I$. The comparison function is

$$N(t)=[\Phi_A(t)^\top]^{-1}\Big\{P(0)-\int_0^t\Phi_A^\top(C^\top M_0C+Q)\Phi_A\,ds\Big\}\Phi_A(t)^{-1}.$$

Formalization targets

Goal: Theorem 5.3

Assume (H1)–(H2) and (5.6): $J^0(0,0;u)\ge0$ for all $u\in\mathcal U[0,T]$. For every $\varepsilon>0$, let $P_\varepsilon$ be the strongly regular solution of (5.7). Then

$$\text{(SLQ)}^0\ \text{is finite}\iff\exists\beta\in\mathbb R\ \ \forall\varepsilon>0:\ P_\varepsilon(0)\ge\beta I .$$

In this case $P(t)=\lim_{\varepsilon\downarrow0}P_\varepsilon(t)$ exists for every $t\in[0,T]$, and

$$V^0(t,x)=\langle P(t)x,x\rangle,\qquad R+D^\top PD\ge0\ \text{a.e.},\qquad N(t)\le P(t)\le M_0(t).$$

In particular, finiteness at $t=0$ implies finiteness.

Milestones

1. Proposition 5.1: (i) ⇒ (ii) ⇒ (iii) ⇒ (iv) and (v) ⇒ (ii). The statements relate finiteness of (SLQ) and (SLQ)$^0$, a quadratic $V^0$, convexity of $J$, and $\mathcal P[t,T]\ne\emptyset$.
2. Remark 4.8: under uniform convexity, $V^0(t,x)=\langle P(t)x,x\rangle$ with $P$ the strongly regular solution.
3. (5.8): $R+\varepsilon I+D^\top P_\varepsilon D\ge\varepsilon I$ a.e.
4. (5.13): $P_{\varepsilon_2}(t)\ge P_{\varepsilon_1}(t)\ge P(t)$ for $\varepsilon_2>\varepsilon_1>0$, and the limit $\bar P(t)=\lim_{\varepsilon\downarrow0}P_\varepsilon(t)$ exists with $\bar P(t)\ge P(t)$.
5. (5.16): $P_\varepsilon(t)\le M_0(t)$.
6. (5.15) and (5.17): $P(0)\le P_\varepsilon(0)$, and $J^0(t,x;u)\ge\langle N(t)x,x\rangle$.

Companions

Theorem 5.6 states the converse of Remark 4.8. Theorem 5.7 gives six equivalent conditions when $D=0$ and $R\gg0$. Example 5.2 is a problem whose cost is convex but which is not finite. Corollary 5.4 gives a Lyapunov-type sufficient condition for finiteness.

Significance

The result. Theorem 5.3 turns finiteness, a statement about an infimum over an infinite-dimensional space of controls, into a lower bound on a one-parameter family of matrices. Each matrix in the family solves a well-posed Riccati equation. The theorem also says that the value function of a finite homogeneous problem is a quadratic form whose matrix is the monotone limit of $P_\varepsilon$. It shows that this limit satisfies the regularity condition (5.10) and sits between two explicit bounds. Section 6 of the paper builds on the same regularization to construct minimizing sequences. Theorem 5.7 shows that in the case $D=0$, $R\gg0$, finiteness already forces unique closed-loop solvability.

Formalizing it. The result has been proved on paper since 2016; nothing in this mission is open mathematics. As far as is known, no part of indefinite stochastic LQ theory has been machine-checked, and Lean/Mathlib has no stochastic LQ problem, no matrix Riccati equation and no fundamental-matrix theory for time-varying linear ODEs. The mission produces faithful statements of the theorem, its proof steps and its companions on top of a reusable problem layer, as targets for complete formal proofs.

Difficulty

The naive argument fails at the interchange of the limit $\varepsilon\to0$ with the infimum over controls. Monotonicity in $\varepsilon$ gives a limit $\bar P(t)\ge P(t)$ directly. The reverse inequality needs near-optimal controls whose $L^2$ norm may blow up, so it has to be organized carefully. The sufficiency direction needs more than the bound at $t=0$. Finiteness at later times is recovered through the comparison function $N(t)$, which combines the fundamental matrix $\Phi_A$ with the Lyapunov solution $M_0$. Example 5.2 rules out the tempting shortcut: under (5.6) the cost is convex, yet $V^0(0,x)=-\infty$ for all $x\ne0$. Every step also rests on stochastic calculus (Itô's formula for $\langle PX,X\rangle$, well-posedness of the state equation) and on the representation of the value through the Riccati equation (Theorems 4.3 and 4.5, cited here).

Formalization scope

The problem layer is shared by the four missions of this series: SLQSolv.Finite.Setting and SLQSolv.Finite.Riccati. It builds on the published Itô-calculus and SDE layer Peng1990.SMP.Stochastic, the augmented Brownian filtration of ReflectedBSDE.Existence.Setting, and the Moore–Penrose pseudoinverse HarmonicGames.Decomposition.pinv. The layer commits to these conventions:

• time is ℝ≥0, vectors are Fin k → ℝ, and $|u|^2$ is the dot product $u\cdot u$;
• the state from $(t,x)$ is an SDE solution from time 0 with coefficients switched on at $t$, with continuous paths and a finite second moment of the supremum; the cost uses this (unique) solution;
• $V$ and $V^0$ take values in EReal, so $V=-\infty$ is ⊥ and finiteness is ⊥ < V;
• matrix ODEs (Riccati, Lyapunov, (5.12)) are in integral form on $[t_0,T]$; the Riccati equation uses the pseudoinverse, which equals the printed inverse on strongly regular solutions;
• matrix inequalities are Loewner inequalities (PosSemidef of the difference), and $L^p$ conditions on matrix coefficients are entrywise;
• "bounded from below" means one scalar $\beta$ with $P_\varepsilon(0)\ge\beta I$ for all $\varepsilon>0$; the limit is $\varepsilon\downarrow0$;
• $P_\varepsilon$, $M_0$, $\Phi_A$ are hypotheses pinned by their defining equations, each with a unique solution; the limit $P$ is a conclusion, not a hypothesis.

A formalization in which "bounded from below" allows $\beta$ to depend on $\varepsilon$, or in which finiteness is checked on $J^0$ at a fixed control rather than on $V^0$, would trivialize the theorem and is excluded.

A complete development needs several pieces, all reusable beyond this mission:

• Itô's formula for quadratic forms of linear SDEs;
• existence and uniqueness for linear SDEs with $L^p$ coefficients;
• existence, uniqueness and invertibility for time-varying linear matrix ODEs;
• continuity of the pseudoinverse on uniformly positive matrices;
• the strongly regular solvability theorem (Theorem 4.5, the goal of mission 1 of this series).

Contributions to any of them are welcome.

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
• J. Yong, X. Y. Zhou, Stochastic Controls: Hamiltonian Systems and HJB Equations, Springer, 1999. https://doi.org/10.1007/978-1-4612-1466-3

Motivation

Online reviews let consumers learn about a new product from the experience of earlier buyers. For a firm selling to strategic consumers, who time their purchases, this social learning (SL) cuts two ways. Reviews reveal quality, which can raise second-period demand; but a consumer who expects reviews also has a new reason to wait, and every consumer who waits writes no review. Papanastasiou and Savva (Management Science 63(4), 2017) build a two-period model in which both forces are endogenous and ask whether a monopolist that commits to its prices in advance is better or worse off when consumers learn from one another.

The benchmark without learning is the classical intertemporal pricing problem with strategic consumers (Landsberger and Meilijson, 1985), whose optimal pre-announced plan is a decreasing price path. This mission formalizes the paper's answer for pre-announced pricing: its Proposition 3.

Setting

A unit mass of consumers has preference types $x$ uniform on $[0,1]$. A product of unknown mean quality $\hat q$ is sold over two periods. Buying in period $t$ gives type $x$ the utility $\delta_c^{t-1}(x+q-p_t)$, where $\delta_c\in[0,1]$ is the consumers' discount factor and $q$ the perceived quality. The firm has unit cost $c\in[0,1)$ and does not discount.

Everyone shares the prior $\hat q\sim N(0,\sigma_p^2)$. Individual quality perceptions are $N(\hat q,\sigma_q^2)$, and $\gamma=\sigma_p^2/\sigma_q^2$ is the SL influence parameter. If a mass $n_1$ buys in period 1 and posts reviews, the posterior mean is $q_u=\tfrac{n_1\gamma}{n_1\gamma+1}R$, where $R$ is the average rating. Seen from period 1, $q_u$ is random, with the pre-posterior law

$$q_u\sim N\!\left(0,\ \sigma_p^2\,\frac{n_1\gamma}{n_1\gamma+1}\right).$$

Under pre-announced pricing the firm commits to a plan $\{p_1,p_2\}$. Consumers then play a purchasing game. A set $B\subseteq[0,1]$ of early buyers is an equilibrium if every type in $B$ weakly prefers buying now, $x-p_1\ge 0$ and $x-p_1\ge\delta_c\,\mathbb E[(x+q_u-p_2)^+]$, and every other type weakly prefers to wait. Here $q_u$ has the pre-posterior law for $n_1=|B|$. In period 2 the remaining types buy iff $x+q_u\ge p_2$. The firm's expected profit is

$$\pi_p(p_1,p_2;B)=(p_1-c)\,|B|+(p_2-c)\,\mathbb E\big[\,|\{x\in[0,1]\setminus B:\ x+q_u\ge p_2\}|\,\big],$$

and the optimal pre-announced profit $\pi_p^*$ is its supremum over all plans and all their equilibria. Absence of SL is the same model at $\gamma=0$, where $q_u\equiv 0$.

Formalization targets

Goal: Proposition 3

For $\gamma>0$ there are thresholds $\Delta_{lp}(\gamma)\in(0,1]$ and $\Delta_{hp}(\gamma)\in[0,1)$ such that

$$\delta_c\le\Delta_{lp}(\gamma)\ \text{ or }\ \delta_c\ge\Delta_{hp}(\gamma)\quad\Longrightarrow\quad \pi_p^*\big|_{\gamma}>\pi_p^*\big|_{\gamma=0}.$$

Milestones

1. Lemma 1: the pre-posterior law above.
2. Display (2): without SL, the buyer set is $[\tau(p_1,p_2),1]$ for an explicit threshold $\tau$.
3. Proposition 1: without SL, $\pi^*=(1-c)^2/(\delta_c+3)$, attained at $p_1^*=\tfrac{c(1+\delta_c)+2}{\delta_c+3}$ and $p_2^*=\tfrac{2c+\delta_c+1}{\delta_c+3}$.
4. Lemma 2: with SL, the buyer set is $[\theta,1]$, where $\theta$ solves the implicit equation (3), or $\theta=1$ under adoption inertia. A companion item states that $\theta$ is monotone in $\gamma,p_1,\delta_c,p_2$.
5. Lemma 5: waiting is worth strictly more when more consumers buy early.
6. Proposition 2: adoption inertia is never optimal, and patient consumers face an increasing optimal price path.
7. Examples 1 and 2: with myopic consumers, SL raises the optimal second-period price and the optimal profit.
8. $\pi_p^*$ is continuous in $\delta_c\in[0,1]$.

Significance

Proposition 3 says that social learning helps the firm at both ends of the patience range. For myopic consumers this is the informational effect alone. For patient consumers it holds even though learning makes them strictly more inclined to wait (Lemma 2) and the committed price cannot react to the reviews. The paper's numerical experiments found no intermediate $\delta_c$ at which learning hurts, but the theorem asserts only the two ends. The result underlies the managerial conclusions of the paper: firms gain from encouraging reviews even when consumers are strategic.

The result is proved in the paper; nothing in the model has been machine-checked before. A formal proof would check the equilibrium analysis of a continuum purchasing game with an endogenous information externality. Its intermediate results also serve the paper's two other missions: responsive pricing, and the comparison of responsive with pre-announced pricing. These are the Normal convex-order monotonicity (Lemma 5), the implicit threshold equation (Lemma 2), the no-SL benchmark (Proposition 1) and a Maximum-Theorem continuity statement.

Difficulty

The equilibrium threshold $\theta$ solves an equation whose Normal kernel has a variance that depends on $\theta$ itself. Existence, uniqueness and monotonicity are not closed-form computations.

The endpoint $\delta_c=1$ is the delicate one. There learning makes waiting most attractive, and the strict gain over the no-SL optimum $(1-c)^2/4$ must come from a plan that still induces a positive mass of early buyers.

Continuity of $\pi_p^*$ in $\delta_c$ is a Maximum-Theorem argument for a supremum over an unbounded set of prices whose objective passes through an implicit equilibrium. Compactness of the relevant price set has to be established, not assumed.

Formalization scope

Every statement is taken over the standing assumptions $\sigma_p>0$, $\gamma\ge 0$, $\delta_c\in[0,1]$, $c\in[0,1)$, with firm discount factor $1$ and pure strategies. Further conventions:

• Absence of SL is the same model at $\gamma=0$. There the pre-posterior law is the point mass at $0$, which is the paper's limit $\gamma\to 0$.
• Best responses are weak. Equilibrium buyer sets are therefore unique only up to Lebesgue-null sets. The degenerate plan $p_1=p_2$ at $\delta_c=1$ without SL, where every type is indifferent, is excluded from the uniqueness claim of (2).
• Optimal values are suprema in the extended reals over all real plans and all purchasing equilibria. They are never real suprema with junk values, never the profit at a closed-form price, and never restricted to threshold equilibria. "Optimal plan" means a plan one of whose equilibria attains the supremum.
• Proposition 3's thresholds are stated with the strict bounds $\Delta_{lp}>0$ and $\Delta_{hp}<1$. With closed bounds the claim would follow from the cases $\delta_c=0$ and $\delta_c=1$ alone.
• Added hypotheses, each disclosed in its item:
  • $p_1\in[0,1]$ in Lemma 2 and its monotonicity item, and $p_1\ge 0$ in (2);
  • $\delta_c>0$ in Lemma 5;
  • $p_1<1$ in Example 1 (at $p_1=1$ nobody buys early, so the example's strict inequality fails there), and $c<p_1$ for its no-SL uniqueness part;
  • $\delta_c<1$ for uniqueness in Proposition 1;
  • $n_1>0$ in Lemma 1;
  • existence of an optimal plan, asserted together with Proposition 2(ii);
  • monotonicity of $\theta$ is weak.
• Not posed:
  • Lemma 2(ii) is built into the second-period demand.
  • The "unique equilibrium" clauses of Propositions 1 and 2 are the items for (2) and Lemma 2.
  • The fixed-price variant of Proposition 3 (pp. 17–18) is false at $\delta_c=1$.

The witness used in the printed proof of Proposition 2(i) does not settle the case $\delta_c=1$.

A complete development needs Gaussian expectations of hinge functions and their monotonicity in the variance (strict convex order), an implicit-equation argument for the threshold, and a version of Berge's Maximum Theorem. The Gaussian lemmas and the no-SL benchmark are reusable across the series. Contributions to any milestone are welcome.

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)
• M. Landsberger, I. Meilijson, Intertemporal price discrimination and sales strategy under incomplete information, RAND Journal of Economics 16(3):424–430, 1985. https://doi.org/10.2307/2555568
• G. P. Cachon, R. Swinney, Purchasing, Pricing, and Quick Response in the Presence of Strategic Consumers, Management Science 55(3):497–511, 2009. https://doi.org/10.1287/mnsc.1080.0948
• A. Müller, D. Stoyan, Comparison Methods for Stochastic Models and Risks, Wiley, 2002. https://doi.org/10.1002/9780470317167
• R. K. Sundaram, A First Course in Optimization Theory, Cambridge University Press, 1996. https://doi.org/10.1017/CBO9780511804526

Motivation

Liouville quantum gravity describes random surfaces whose area measure is formally $e^{\gamma h(z)}dz$, where $h$ is a Gaussian free field (GFF). Schramm–Loewner evolution (SLE$_\kappa$) describes random fractal curves that arise as scaling limits of interfaces in critical lattice models. Sheffield's paper Conformal weldings of random surfaces: SLE and the quantum gravity zipper (arXiv:1012.4797, Ann. Probab. 44 (2016), DOI 10.1214/15-AOP1055) shows that the two theories fit together: SLE curves are the interfaces obtained by conformally welding independent quantum surfaces along their boundaries.

The starting point of that program is a coupling between the reverse Loewner flow and the free boundary GFF (Theorem 1.2 of the paper): zipping up the upper half-plane by a reverse SLE$_\kappa$ map, and changing coordinates by the rule of Liouville quantum gravity, does not change the law of the field. This mission formalizes that theorem and the calculations of §4.1 that prove it.

Timeline. Couplings of forward SLE with the GFF go back to Schramm–Sheffield for $\kappa=4$ (arXiv:1008.2447) and to Dubédat for general $\kappa$ (arXiv:0712.3018). The reverse coupling with the free boundary GFF and the factor $Q\log|f_T'|$ is Sheffield's (2010 preprint, published 2016); it underlies the later mating-of-trees theory of Duplantier–Miller–Sheffield (arXiv:1409.7055).

Setting

Let $\mathbb H=\{z\in\mathbb C:\operatorname{Im}z>0\}$. A test function is a smooth, compactly supported real function $\rho$ with support in $\mathbb H$; it has mean zero if $\int_{\mathbb H}\rho(z)\,dz=0$. For a function $F$ write $(F,\rho)=\int F\rho\,dz$.

The free boundary Green's function is $G(y,z)=-\log|y-z|-\log|y-\bar z|$, and the energy of two test functions is

$$E(\rho_1,\rho_2)=\int_{\mathbb H}\int_{\mathbb H}\rho_1(y)\,G(y,z)\,\rho_2(z)\,dy\,dz .$$

A free boundary GFF $\tilde h$ is a random modulo-additive-constant distribution: for every family of mean-zero test functions $\rho_1,\dots,\rho_n$, the vector $((\tilde h,\rho_j))_j$ is a centred Gaussian vector with covariance $(E(\rho_i,\rho_j))_{i,j}$. Pairings with test functions of nonzero mean are not defined.

Fix $\kappa>0$ and a standard Brownian motion $B$, and put $W_t=\sqrt\kappa B_t$. The reverse Loewner flow is $f_t(z)=g_t(z)-W_t$, where for each $z\in\mathbb H$

$$\partial_t g_t(z)=\frac{-2}{g_t(z)-W_t},\qquad g_0(z)=z ,$$

the pathwise form of $df_t(z)=\frac{-2}{f_t(z)}dt-\sqrt\kappa\,dB_t$. Write $f_t'=\partial_zf_t$ and

$$Q=\frac{2}{\sqrt\kappa}+\frac{\sqrt\kappa}{2},\qquad \mathfrak h_0(z)=\frac{2}{\sqrt\kappa}\log|z|,\qquad \mathfrak h_t(z)=\mathfrak h_0(f_t(z))+Q\log|f_t'(z)| .$$

The fraktur $\mathfrak h_t$ are deterministic functionals of the flow. Finally $G_t(y,z)=G(f_t(y),f_t(z))$, $E_t(\rho_1,\rho_2)=\iint\rho_1(y)G_t(y,z)\rho_2(z)\,dy\,dz$, and $C_t(z)=-\log\operatorname{Im}f_t(z)-\log|f_t'(z)|$.

Formalization targets

Goal: Theorem 1.2

For every $T>0$, with $\tilde h$ independent of $B$,

$$\mathfrak h_0+\tilde h\ \overset{d}{=}\ \mathfrak h_T+\tilde h\circ f_T\qquad\text{(modulo additive constants),}$$

that is, the pairing vectors with every finite family of mean-zero test functions have the same law. Here $(\tilde h\circ f_T,\rho)=(\tilde h,|(f_T^{-1})'|^2\rho\circ f_T^{-1})$.

Milestones (in the order the proof uses them)

1. The reverse-flow table on p. 44: $\frac{d}{dt}f_t'(z)=2f_t'(z)/f_t(z)^2$.
2. The table on p. 47: $\frac{d}{dt}G_t(y,z)=-\operatorname{Re}\frac{2}{f_t(y)}\operatorname{Re}\frac{2}{f_t(z)}$.
3. $\operatorname{Im}f_t(z)$ is strictly increasing in $t$.
4. $|\partial_tC_t(z)|$ is bounded uniformly for $z$ in a compact subset of $\mathbb H$ and all $t$.
5. For fixed $z$, $\mathfrak h_t(z)$ is a martingale.
6. For mean-zero $\rho$, $(\mathfrak h_t,\rho)$ is a martingale.
7. For fixed $x\neq y$, $\mathfrak h_t(x)\mathfrak h_t(y)+G_t(x,y)$ is a martingale.
8. (4.2): $(\mathfrak h_t,\rho_1)(\mathfrak h_t,\rho_2)+E_t(\rho_1,\rho_2)$ is a martingale.
9. The one-dimensional law: mixing $\mathcal N((\mathfrak h_T,\rho),E_T(\rho))$ over $B$ gives $\mathcal N((\mathfrak h_0,\rho),E(\rho,\rho))$.
10. Proposition 3.1: a random modulo-constant distribution whose mean-zero pairings are $\mathcal N(0,E(\rho,\rho))$ is the free boundary GFF.

Significance

The result. Theorem 1.2 says that the free boundary quantum surface $(\mathbb H,\mathfrak h_0+\tilde h)$ is invariant in law under zipping up by an independent reverse SLE$_\kappa$ for a fixed time. It is the stationarity statement behind the quantum gravity zipper: Theorems 1.3–1.4 and 1.8 of the paper (the welding of boundary arcs of equal quantum length, treated in the companion mission) start from it, and the subsequent theory of quantum wedges, quantum cones and mating of trees uses it as a basic tool. It also gives an alternate way to sample the field: first sample $B$ (hence the curve), then sample an independent GFF, and form $\mathfrak h_T+\tilde h\circ f_T$.

Formalizing it. The theorem is proved in the literature, and the paper itself regards several steps as standard (Proposition 3.1 is cited to [She07]). No part of it has a machine-checked proof. A complete development would give Lean its first Gaussian free field, its first reverse Loewner flow, and martingale statements for SLE functionals; the deterministic Loewner calculus of milestones 1–4 is useful independently of the probabilistic part.

Difficulty

The time derivatives in milestones 1–3 are routine once the flow is known to be holomorphic in $z$, and milestone 4 follows from them. The obstacle is upgrading local martingales to martingales and exchanging the stochastic dynamics with integration in $z$. Itô's formula gives that $\mathfrak h_t(z)$ is a continuous local martingale; that it is a true martingale needs the bound of milestone 4, which shows that it is a Brownian motion run for a time at most a constant times $t$. Passing from points to $(\mathfrak h_t,\rho)$ and to (4.2) needs integrability of $\mathfrak h_t(z)$ uniformly on the support of $\rho$ and a Fubini argument. Mathlib has neither Itô calculus nor quadratic variation, so these steps need either a stochastic-calculus library or a direct argument. The final step (milestones 9–10) needs the Cramér–Wold device for an infinite-dimensional Gaussian field and the change of variables $E(\rho^{f_T})=E_T(\rho)$.

Formalization scope

• $\mathbb H$ is the open set $\{0<\operatorname{Im}z\}$ of $\mathbb C$ as a real normed space; test functions are Mathlib's 𝓓(ℍ, ℝ); integrals are Bochner integrals for Lebesgue measure on $\mathbb C$ and $\mathbb C\times\mathbb C$.
• The free boundary GFF is a predicate on a map $\Omega\to$ (test functions $\to\mathbb R$): measurable pairings, and multivariateGaussian 0 (E(ρ_i,ρ_j)) laws for every mean-zero family. Every statement pairs only with mean-zero test functions.
• The Green's function carries no factor $1/(2\pi)$ (the Dirichlet inner product carries $(2\pi)^{-1}$).
• The reverse Loewner flow is pathwise: an ODE in $t$ for $g_t=f_t+W_t$, required for every $z\in\mathbb H$ and $t\ge0$. Time is $\mathbb R_{\ge0}$. The deterministic milestones are stated for every continuous driving function.
• $B$ is Mathlib's IsBrownianReal, taken with every path continuous and every coordinate measurable; martingales are with respect to its natural filtration and hold for all $t\ge0$.
• The goal is stated through the conditional law given $B$: the $P$-mixture of $\mathcal N\big(((\mathfrak h_T,\rho_j))_j,(E_T(\rho_i,\rho_j))\big)$ equals the law of $((\mathfrak h_0,\rho_j)+(\tilde h,\rho_j))_j$, with $\tilde h$ on its own probability space. The mixture is a lower Lebesgue integral of set probabilities.
• A trivializing formalization would define $E_t$ with the forward Green's function, mix over a measure other than the law of $B$, or let the GFF predicate fix only one-dimensional laws; none of these is used, and Proposition 3.1 is stated separately.
• Welcome contributions: a Loewner-ODE library (existence, uniqueness, holomorphy in $z$), Gaussian free field infrastructure, and martingale arguments without Itô calculus.

Selected references

• S. Sheffield, Conformal weldings of random surfaces: SLE and the quantum gravity zipper, Ann. Probab. 44(5) (2016), 3474–3545. arXiv:1012.4797, DOI 10.1214/15-AOP1055
• S. Sheffield, Gaussian free fields for mathematicians, Probab. Theory Related Fields 139 (2007), 521–541. arXiv:math/0312099
• O. Schramm, S. Sheffield, A contour line of the continuum Gaussian free field, Probab. Theory Related Fields 157 (2013), 47–80. arXiv:1008.2447
• J. Dubédat, SLE and the free field: partition functions and couplings, J. Amer. Math. Soc. 22 (2009), 995–1054. arXiv:0712.3018
• B. Duplantier, S. Sheffield, Liouville quantum gravity and KPZ, Invent. Math. 185 (2011), 333–393. arXiv:0808.1560
• B. Duplantier, J. Miller, S. Sheffield, Liouville quantum gravity as a mating of trees, Astérisque 427 (2021). arXiv:1409.7055