Control Theory

Motivation

Transient stability asks whether a power grid, after a large disturbance such as a fault or a line trip, returns to synchronous operation in which all generators rotate at a common frequency. The classical approach builds energy functions for the swing equations and estimates regions of attraction numerically; it gives no closed-form test relating synchronization to the network's parameters, and it handles transfer conductances (losses) only when they are "sufficiently small" without saying how small.

Dörfler and Bullo (arXiv:0910.5673v4; SIAM J. Control Optim. 50(3), 2012) observe that, for strongly overdamped generators, the network-reduced swing equations behave like a first-order non-uniform Kuramoto model, and they give purely algebraic conditions under which this model synchronizes. The same model is a generalization of the classical Kuramoto model of coupled oscillators, studied in physics, neuroscience and control, with heterogeneous time constants, asymmetric effective coupling and phase shifts. This mission formalizes the first of the paper's two synchronization conditions, Theorem V.3, which is also statements 1)–2) of the paper's main result, Theorem III.2.

Setting

There are $n \ge 2$ oscillators with phases $\theta_1, \dots, \theta_n$. Each has a time constant $D_i > 0$ and a natural frequency $\omega_i \in \mathbb R$; each pair has a coupling weight $P_{ij} \ge 0$ and a phase shift $\varphi_{ij} \in [0, \pi/2[$, with $P_{ii} = \varphi_{ii} = 0$. The non-uniform Kuramoto model is

$$D_i\,\dot\theta_i = \omega_i - \sum_{j=1}^n P_{ij}\sin(\theta_i - \theta_j + \varphi_{ij}), \qquad i = 1, \dots, n. \tag{8}$$

The phases live on the torus. For an arc length $\gamma \in [0, \pi]$, the set $\Delta(\gamma)$ consists of configurations whose phases all lie in the interior of some arc of length $\gamma$, and $\bar\Delta(\gamma)$ is its closure (with the synchronized configurations). A set is positively invariant if every solution starting in it stays in it. A solution achieves exponential frequency synchronization if all frequencies $\dot\theta_i(t)$ converge exponentially fast to a common value $\dot\theta_\infty$.

The condition of the theorem compares two numbers built from the parameters, with $\varphi_{\max} = \max_{i,j}\varphi_{ij}$:

$$\Gamma_{\min} := n\min_{i\neq j}\Big\{\frac{P_{ij}}{D_i}\cos\varphi_{ij}\Big\},\qquad \Gamma_{\mathrm{critical}} := \frac{1}{\cos\varphi_{\max}}\Big(\max_{i\neq j}\Big|\frac{\omega_i}{D_i}-\frac{\omega_j}{D_j}\Big| + 2\max_i\sum_{j=1}^n\frac{P_{ij}}{D_i}\sin\varphi_{ij}\Big).$$

$\Gamma_{\min}$ is the weakest lossless coupling of an oscillator to the network; $\Gamma_{\mathrm{critical}}$ measures the spread of natural frequencies and the losses. When $\Gamma_{\min} > \Gamma_{\mathrm{critical}}$, put $c = \cos(\varphi_{\max})\Gamma_{\mathrm{critical}}/\Gamma_{\min}$, $\gamma_{\min} = \arcsin c \in [0, \pi/2-\varphi_{\max}[$ and $\gamma_{\max} = \pi - \arcsin c \in\, ]\pi/2, \pi]$.

Formalization targets

Goal: Theorem V.3 (Synchronization condition I), corrected

If $P = P^T$ is complete ($P_{ij} > 0$ for $i \ne j$) and

$$\Gamma_{\min} > \Gamma_{\mathrm{critical}}, \tag{26}$$

then (1) $\bar\Delta(\gamma)$ is positively invariant for every $\gamma \in [\gamma_{\min}, \gamma_{\max}]$, and every solution starting in $\Delta(\gamma_{\max})$ eventually stays in $\bar\Delta(\gamma)$ for each $\gamma \in\, ]\gamma_{\min}, \gamma_{\max}]$; (2) every solution starting in $\Delta(\gamma_{\max})$ achieves exponential frequency synchronization to some $\dot\theta_\infty$, and $\dot\theta_\infty \in [\dot\theta_{\min}(0), \dot\theta_{\max}(0)]$ when the solution starts in $\Delta(\pi/2 - \varphi_{\max})$.

Milestones

The milestones follow the paper's proof. Theorem V.1 is a frequency-synchronization theorem for phase-cohesive oscillators under a globally reachable node, with the explicit rate

$$\lambda_{fe} = \lambda_2(L(P_{ij}))\cos(\gamma)\cos(\angle(D\mathbf 1, \mathbf 1))^2/D_{\max}$$

when $\varphi \equiv 0$ and $P = P^T$. Its supporting steps are the frequency dynamics (20) and a dihedral-angle bound. The phase-cohesiveness argument of Theorem V.3 is split into a trigonometric lower bound, a pointwise bound on the growth rate of the arc containing all phases, the characterization of $[\gamma_{\min}, \gamma_{\max}]$ by inequality (30), positive invariance, and the entry into $\bar\Delta(\pi/2 - \varphi_{\max})$.

Significance

The theorem turns synchronization of a heterogeneous, lossy oscillator network into one inequality among explicit parameters. For the classical Kuramoto model it specializes to $K > \omega_{\max} - \omega_{\min}$ (Remark V.4), which improved the sufficient conditions known at the time. For power networks it gives, through Theorem III.2, a computable sufficient condition for transient stability when generator inertia is small relative to damping.

To our knowledge none of these results has a machine-checked proof. The development needs ODE comparison arguments for a non-smooth Lyapunov function (the arc length) and an exponential convergence theorem for time-varying consensus. Both are general tools that are not in Mathlib and would be reusable for other consensus and synchronization results. The mission also records two clauses of the printed theorem that are false as stated, with counterexamples, and states the corrected theorem.

Difficulty

The arc length $V(\theta) = \max_{i,j}(\theta_i - \theta_j)$ is only Lipschitz, so its decrease along solutions must be argued through Dini derivatives and a comparison lemma rather than by differentiation. Positive invariance at the boundary $\gamma = \gamma_{\min}$ holds with a non-strict inequality, so a naive "strictly decreasing at the boundary" argument does not apply there. Frequency synchronization rests on a contraction property of linear consensus with time-varying, state-dependent weights. The weights are positive only after the phases have entered $\bar\Delta(\pi/2 - \varphi_{\max})$. Before that the frequency range can expand, which is why the range clause of the printed theorem fails for initial arcs longer than $\pi/2 - \varphi_{\max}$.

Formalization scope

Phases are represented by real lifts $\theta : \mathrm{Fin}\,n \to \mathbb R$. $\bar\Delta(\gamma)$ means that all pairwise differences of the lift are at most $\gamma$, and $\Delta(\gamma)$ that they are strictly less than $\gamma$. Conclusions are stated for the same continuous lift, which is at least as strong as membership on the torus. A solution is a map $\theta : \mathbb R \to \mathbb R^n$ with derivative (one-sided at $0$) equal to the right-hand side of (8) for all $t \ge 0$. Every statement quantifies over all such solutions. $\dot\theta$ always denotes the vector field along the solution. Minima and maxima over $i \ne j$ are over ordered pairs, and $n \ge 2$ is assumed so that they exist. The conventions $P_{ii} = \varphi_{ii} = 0$ are explicit hypotheses. $\gamma_{\min}$ and $\gamma_{\max}$ are defined by $\arcsin$, and a milestone certifies that they are the unique solutions in the printed ranges. $\lambda_2$ is the second-smallest eigenvalue of the symmetric Laplacian.

The source is the arXiv preprint v4 of the SICON article, cited with its own page and theorem numbers. Three corrections relative to the printed text are made and disclosed in the items:

• "each trajectory starting in $\Delta(\gamma_{\max})$ reaches $\bar\Delta(\gamma_{\min})$" holds only asymptotically ($n = 2$, $\varphi \equiv 0$, $D \equiv 1$, $P_{12} = 1$, $\omega = (1, 0)$: the phase difference tends to the equilibrium $\pi/6 = \gamma_{\min}$ without reaching it). It is stated for every $\gamma > \gamma_{\min}$.
• the frequency range $[\dot\theta_{\min}(0), \dot\theta_{\max}(0)]$ fails for some initial conditions in $\Delta(\gamma_{\max})$ ($n = 2$, $D \equiv 1$, $\omega \equiv 0$, $P_{12} = 1$, $\varphi_{12} = \varphi_{21} = 1/2$, $\theta(0) = (2.4, 0)$). It is stated for initial conditions in $\Delta(\pi/2 - \varphi_{\max})$, while exponential synchronization is stated for all of $\Delta(\gamma_{\max})$.
• the rate (19) is printed with a leading minus sign but is used as a positive decay rate. The positive rate is stated.

No statement is trivially satisfiable. The solution predicate holds for actual solutions (for example the synchronous solution), condition (26) is satisfiable (take $\omega \equiv 0$ and $\varphi \equiv 0$), the exponential rate is required to be strictly positive, and $\gamma_{\min}, \gamma_{\max}$ are specific numbers rather than existential witnesses.

Contributions are welcome on all milestones. The trigonometric bound, the dihedral-angle bound and the $\gamma_{\min}/\gamma_{\max}$ characterization are elementary. The comparison lemma for Dini derivatives and the consensus contraction theorem are reusable infrastructure.

Selected references

• F. Dörfler, F. Bullo, Synchronization and Transient Stability in Power Networks and Nonuniform Kuramoto Oscillators, SIAM J. Control Optim. 50(3), 2012; preprint arXiv:0910.5673v4. https://arxiv.org/abs/0910.5673v4 — DOI: https://doi.org/10.1137/110851584
• L. Moreau, Stability of continuous-time distributed consensus algorithms, 43rd IEEE CDC, 2004 (the contraction theorem cited as [53, Theorem 1]). https://arxiv.org/abs/math/0409010
• Y. Kuramoto, Self-entrainment of a population of coupled non-linear oscillators, Int. Symp. on Mathematical Problems in Theoretical Physics, Lecture Notes in Physics 39, 1975. https://doi.org/10.1007/BFb0013365
• H.-D. Chiang, F. F. Wu, P. P. Varaiya, Foundations of direct methods for power system transient stability analysis, IEEE Trans. Circuits Syst. 34(2), 1987. https://doi.org/10.1109/TCS.1987.1086115

Motivation

An investor who trades continuously in a market driven by Brownian motion, and who may only hold portfolios in a prescribed set, wants to maximize the expected utility of terminal wealth. With power utility $U_\gamma(x)=\frac1\gamma x^\gamma$, $\gamma\in(0,1)$, this is the constant-relative-risk-aversion problem that goes back to Merton (Merton 1971). When there are fewer stocks than sources of noise the market is incomplete, and when portfolio proportions are restricted (no short sales, bounded positions, a fixed allocation) the problem is constrained.

For convex constraints, duality methods settle the problem (Cvitanić–Karatzas 1992; Kramkov–Schachermayer 1999). They do not apply when the constraint set is closed but not convex, as for integer-lot or "all-or-nothing" restrictions. Hu, Imkeller and Müller (2005, arXiv:math/0508448) treat that case by a martingale optimality principle: they build a process that is a supermartingale for every admissible strategy and a martingale for one, and obtain it from a backward stochastic differential equation (BSDE) with a driver that grows quadratically in $z$. The existence theory for such equations is due to Kobylanski (2000).

This mission formalizes the power-utility result, Theorem 14 of the paper. A companion mission treats the exponential-utility result, Theorem 7.

Setting

Fix a horizon $T>0$ and a probability space $(\Omega,\mathcal F,P)$ carrying an $m$-dimensional Brownian motion $W$; $\mathbb F$ is the augmentation of its natural filtration. $|\cdot|$ is the Euclidean norm, and $\lambda$ is Lebesgue measure on $[0,T]$.

Market. There is a bond with zero interest and $d\le m$ stocks with prices $dS^i_t/S^i_t=b^i_t\,dt+\sigma^i_t\,dW_t$. The rates $b_t\in\mathbb R^d$ and the volatility $\sigma_t\in\mathbb R^{d\times m}$ are predictable and uniformly bounded, and $KI_d\ge\sigma_t\sigma_t^{\mathrm{tr}}\ge\varepsilon I_d$ for constants $K>\varepsilon>0$. The market price of risk is $\theta_t=\sigma_t^{\mathrm{tr}}(\sigma_t\sigma_t^{\mathrm{tr}})^{-1}b_t\in\mathbb R^m$.

Constraints. A closed set $\tilde C\subseteq\mathbb R^{1\times d}$ of row vectors constrains the proportions $\tilde\rho_t$ of wealth held in the stocks. In the variable $\rho_t=\tilde\rho_t\sigma_t\in\mathbb R^{1\times m}$ the constraint reads $\rho_t\in C_t(\omega)=\tilde C\sigma_t(\omega)$. For a closed $C\subseteq\mathbb R^m$, $\operatorname{dist}_C(a)=\min_{b\in C}|a-b|$, and $\Pi_C(a)=\{b\in C:|a-b|=\operatorname{dist}_C(a)\}$ is the (possibly multi-valued) projection.

Wealth and admissible strategies. From initial capital $x>0$ the wealth (11) is

$$X^{(\rho)}_t=x\exp\Big(\int_0^t\rho_s\,dW_s+\int_0^t\rho_s\theta_s\,ds-\tfrac12\int_0^t|\rho_s|^2\,ds\Big).$$

The admissible class $\tilde{\mathcal A}$ (Definition 13) consists of predictable $\rho$ with $\rho_t\in C_t$ for $\lambda\otimes P$-a.e. $(t,\omega)$ and $\int_0^T|\rho_s|^2\,ds<\infty$ a.s. The value is (12), $\bar V(x)=\sup_{\rho\in\tilde{\mathcal A}}E[U_\gamma(X^{(\rho)}_T)]$.

The BSDE. $\mathcal H^\infty(\mathbb R)$ is the class of predictable, $\lambda\otimes P$-a.e. bounded processes and $\mathcal H^2(\mathbb R^m)$ that of predictable $Z$ with $E\int_0^T|Z_t|^2\,dt<\infty$. The BSDE (15) is

$$Y_t=0-\int_t^TZ_s\,dW_s-\int_t^Tf(s,Z_s)\,ds,\qquad f(t,z)=\frac{\gamma(1-\gamma)}2\operatorname{dist}^2\Big(\frac{z+\theta_t}{1-\gamma},C_t\Big)-\frac{\gamma|z+\theta_t|^2}{2(1-\gamma)}-\frac12|z|^2 .$$

A BMO martingale $\int_0^\cdot\xi\,dW$ is one with $\sup_\tau\|E[\int_\tau^T|\xi_s|^2ds\mid\mathcal F_\tau]\|_\infty<\infty$ over stopping times $\tau\le T$ (equation (2)).

Formalization targets

Goal: Theorem 14

(15) has a unique solution $(Y,Z)\in\mathcal H^\infty(\mathbb R)\times\mathcal H^2(\mathbb R^m)$, and for $x>0$

$$\bar V(x)=\frac1\gamma\,x^\gamma\exp(Y_0),$$

attained by some $\rho^*\in\tilde{\mathcal A}$ with

$$\rho^*_t\in\Pi_{C_t(\omega)}\Big(\frac1{1-\gamma}(Z_t+\theta_t)\Big).\qquad(16)$$

The page prints $V(x)=x^\gamma\exp(Y_0)$; its proof measures utility by $x^\gamma$, so the value of (12) with $U_\gamma=\frac1\gamma x^\gamma$ carries the factor $\frac1\gamma$ (see Formalization scope).

Milestones

1. (14), p. 17: for $\rho\in C$, $\gamma\rho\theta-\frac12\gamma|\rho|^2+f(z)\le-\frac12|\gamma\rho+z|^2$, with equality on $\Pi_C\big(\frac{z+\theta}{1-\gamma}\big)$.
2. (H1), p. 18: $|f(t,z)|\le c_0+c_1|z|^2$.
3. Existence and 4. uniqueness for (15), p. 18.
4. Lemma 17, p. 20: $\int Z\,dW$ and $\int\rho^*dW$ are BMO martingales.
5. Optimality of $\rho^*$, p. 18: $\rho^*\in\tilde{\mathcal A}$ and $E[(X^{(\rho^*)}_T)^\gamma]=x^\gamma\exp(Y_0)$.
6. Comparison, p. 18: $E[(X^{(\rho)}_T)^\gamma]\le x^\gamma\exp(Y_0)$ for every $\rho\in\tilde{\mathcal A}$.

Significance

The theorem gives the value of a constrained power-utility problem in closed form through one scalar, $Y_0$, of a BSDE, and identifies an optimal strategy as a measurable selection of a projection onto the constraint set. Convexity of the constraint is not needed; when $\tilde C$ is a convex cone the result recovers the strategy obtained by other methods (Remark 16 of the paper). The same scheme handles exponential and logarithmic utility in the paper's other sections, and the dynamic programming principle of Proposition 15 follows from it.

The result is proved in the paper. As far as the platform's records show, none of it is formalized: there is no quadratic BSDE, no BMO martingale and no continuous-time utility-maximization statement on the platform. A complete formalization would add an existence and uniqueness theory for BSDEs with quadratic growth, the BMO criterion for stochastic exponentials, and a verification theorem for constrained portfolio problems, each reusable well beyond this paper.

Difficulty

The verification argument is short on paper; its inputs are not. Existence for (15) rests on Kobylanski's existence theorem for drivers of quadratic growth, which is not in Mathlib; the Lipschitz theory does not cover a driver growing like $|z|^2$. Uniqueness needs a comparison principle for such drivers. Lemma 17 and the martingale property of $\tilde R^{(\rho^*)}$ need the theory of BMO martingales and of their stochastic exponentials, also absent. The comparison milestone concerns processes that are only local supermartingales. A naive attempt that treats $\tilde R^{(\rho)}$ as a martingale for every admissible $\rho$ fails: for a general $\rho\in\tilde{\mathcal A}$, which is only locally square integrable, it is merely a local supermartingale.

Formalization scope

All declarations live in HuImkellerMuller.Power. Time is ℝ≥0; vectors of $\mathbb R^{1\times m}$ are EuclideanSpace ℝ (Fin m), with products $z\theta$ as inner products; $\tilde C$ is a Set (Fin d → ℝ). The Brownian motion, the augmented filtration, the measure $\lambda\otimes P$ and the Itô-integral operator I are reused from published definitions (EthierKurtz_IsStandardBrownian, CvitanicKaratzas92_Optimality_Market). The wealth is constructed from I, $\rho$ and $\theta$; $\theta$ is computed from $b$ and $\sigma$.

Conventions and disclosed readings:

• The factor $\frac1\gamma$. The goal states $\bar V(x)=\frac1\gamma x^\gamma\exp(Y_0)$ for (12) with $U_\gamma$; milestones 6–7 state $E[(X_T)^\gamma]$ against $x^\gamma\exp(Y_0)$, as the proof does.
• Added hypothesis $\tilde C\neq\emptyset$ (needed for (4) and for $\Pi_{C_t}\neq\emptyset$).
• Strategies are written in $\rho=\tilde\rho\sigma\in\mathbb R^m$ (Definition 13 says "$d$-dimensional"); §3's "$\bar C_2\subseteq\mathbb R^d$" and $\tilde C$ are one closed set.
• (16) and the constraint hold $\lambda\otimes P$-a.e.; "$\rho^*$ given by (16)" means any predictable selection.
• $Y_0$ is a.s. constant; the value identity holds for $P$-a.e. $\omega$.
• Uniqueness means $Y^1_t=Y^2_t$ a.s. for every $t$ and $Z^1=Z^2$ $\lambda\otimes P$-a.e.
• Expectations of nonnegative quantities are lower integrals in $[0,\infty]$; the value is a supremum in $[0,\infty]$.
• Ellipticity holds for $P$-a.e. $\omega$ and every $t\le T$; boundedness of $b$, $\sigma$ holds everywhere.

The value is a supremum of lower integrals, never of Bochner integrals: a Bochner expectation of a non-integrable $U_\gamma(X_T)$ is $0$ and would make the supremum meaningless. The goal asserts existence of a solution of (15) and does not take one as a hypothesis, so it cannot hold vacuously.

Contributions welcome: a theory of BSDEs with quadratic growth (Kobylanski), BMO martingales and Kazamaki's criterion, measurable selection of metric projections, and proofs of the deterministic milestone (14) and the growth bound (H1).

Selected references

• Y. Hu, P. Imkeller, M. Müller, Utility maximization in incomplete markets, Ann. Appl. Probab. 15(3), 2005, 1691–1712. https://doi.org/10.1214/105051605000000188 (arXiv:math/0508448v1, https://arxiv.org/abs/math/0508448)
• M. Kobylanski, Backward stochastic differential equations and partial differential equations with quadratic growth, Ann. Probab. 28(2), 2000, 558–602. https://doi.org/10.1214/aop/1019160253
• N. Kazamaki, Continuous Exponential Martingales and BMO, Lecture Notes in Math. 1579, Springer, 1994. https://doi.org/10.1007/BFb0073585
• J. Cvitanić, I. Karatzas, Convex duality in constrained portfolio optimization, Ann. Appl. Probab. 2(4), 1992, 767–818. https://doi.org/10.1214/aoap/1177005576
• D. Kramkov, W. Schachermayer, The asymptotic elasticity of utility functions and optimal investment in incomplete markets, Ann. Appl. Probab. 9(3), 1999, 904–950. https://doi.org/10.1214/aoap/1029962818
• R. C. Merton, Optimum consumption and portfolio rules in a continuous-time model, J. Econom. Theory 3, 1971, 373–413. https://doi.org/10.1016/0022-0531(71)90038-X

Motivation

An investor who trades in a market with fewer stocks than sources of randomness cannot hedge every risk: the market is incomplete. If the investor also faces a liability $F$ due at the horizon $T$ and has to respect trading constraints (no short sales, limits on positions in certain stocks, a ban on trading some assets altogether), the question of how to trade optimally becomes a constrained stochastic control problem. With exponential utility $U(x)=-\exp(-\alpha x)$, its value function gives the investor's utility indifference price of $F$, a standard pricing rule in incomplete markets.

Earlier treatments needed convexity. Cvitanić and Karatzas (Ann. Appl. Probab. 2 (1992)) proved existence and uniqueness for utility maximization in a Brownian filtration with convex constraints, by convex duality. Delbaen, Grandits, Rheinländer, Samperi, Schweizer and Stricker (Math. Finance 12 (2002)) related exponential utility maximization to the martingale measure of minimal relative entropy. El Karoui and Rouge (Math. Finance 10 (2000)) computed the value function and optimal strategy for exponential utility by backward stochastic differential equations (BSDEs), for strategies confined to a convex cone; Sekine (preprint, 2002) obtained the same BSDE from the Cvitanić–Karatzas duality. Hu, Imkeller and Müller (Ann. Appl. Probab. 15 (2005)) gave a direct BSDE solution that works for closed, possibly nonconvex constraint sets, with a bounded liability. The tool is a BSDE whose driver grows quadratically in the control variable, whose solvability rests on Kobylanski's existence theorem for quadratic BSDEs (Ann. Probab. 28 (2000)).

Setting

Fix $T>0$ and an $m$-dimensional Brownian motion $W$ on a probability space $(\Omega,\mathcal F,P)$, and let $\mathbb F=(\mathcal F_t)$ be the $P$-augmentation of the filtration generated by $W$. There are $d\le m$ stocks with prices $dS^i_t/S^i_t=b^i_t\,dt+\sigma^i_t\,dW_t$; the drift $b$ and the $d\times m$ volatility matrix $\sigma$ are predictable and uniformly bounded, and $KI_d\ge\sigma\sigma^{\mathrm{tr}}\ge\varepsilon I_d$ for constants $K>\varepsilon>0$. The market price of risk is $\theta_t=\sigma^{\mathrm{tr}}_t(\sigma_t\sigma^{\mathrm{tr}}_t)^{-1}b_t\in\mathbb R^m$.

A strategy is an $\mathbb R^{1\times m}$-valued predictable process $p_t=\pi_t\sigma_t$, where $\pi_t$ is the vector of amounts held in the stocks. Its wealth from initial capital $x$ is

$$X^{(p)}_t=x+\int_0^tp_u\,(dW_u+\theta_u\,du).$$

The constraint is a closed set $\tilde C\subseteq\mathbb R^{1\times d}$, not necessarily convex; in terms of $p$ it reads $p_t\in C_t:=\tilde C\sigma_t$. A strategy is admissible, $p\in\mathcal A$, when $E\int_0^T|p_t|^2dt<\infty$, $p_t\in C_t$ for $\lambda\otimes P$-a.e. $(t,\omega)$, and $\{\exp(-\alpha X^{(p)}_\tau):\tau\le T\text{ a stopping time}\}$ is uniformly integrable. The value function is

$$V(x)=\sup_{p\in\mathcal A}E\Big[-\exp\Big(-\alpha\big(X^{(p)}_T-F\big)\Big)\Big],$$

with $\alpha>0$ and a bounded $\mathcal F_T$-measurable liability $F$. For a closed set $C$, $\operatorname{dist}_C(a)=\min_{b\in C}|a-b|$ and $\Pi_C(a)=\{b\in C:|a-b|=\operatorname{dist}_C(a)\}$ is the set of nearest points.

Formalization targets

Goal: Theorem 7

Let $f(t,z)=-\frac\alpha2\operatorname{dist}^2\big(z+\frac1\alpha\theta_t,C_t\big)+z\theta_t+\frac1{2\alpha}|\theta_t|^2$. The BSDE

$$Y_t=F-\int_t^TZ_s\,dW_s-\int_t^Tf(s,Z_s)\,ds,\qquad t\in[0,T],$$

has a unique solution $(Y,Z)\in\mathcal H^\infty(\mathbb R)\times\mathcal H^2(\mathbb R^m)$, the value function is

$$V(x)=-\exp\big(-\alpha(x-Y_0)\big),$$

and there is an optimal strategy $p^*\in\mathcal A$ with $p^*_t\in\Pi_{C_t}\big(Z_t+\frac1\alpha\theta_t\big)$.

Milestones

In the order of the proof: the bound (4) on $C_t$ and its closedness; the measurable selection Lemma 11 (a), (b); the identity on p. 8 that dictates $f$; the growth bound (9) and the local Lipschitz estimate of $f$; existence and uniqueness for (7); the BMO property of Lemma 12; admissibility and optimality of any predictable selection $p^*$; and the comparison $E[-\exp(-\alpha(X^{(p)}_T-F))]\le-\exp(-\alpha(x-Y_0))$ for every $p\in\mathcal A$.

Significance

The theorem reduces a constrained, nonconvex control problem to a single quadratic BSDE: the value is read off the initial value $Y_0$, and the optimal strategy is a pointwise nearest-point selection from the constraint set. It requires neither convexity nor duality, and it exhibits non-uniqueness of the optimal strategy when $\Pi_{C_t}$ has several points. It is the starting point of the quadratic-BSDE approach to utility maximization, indifference pricing and related equilibrium problems.

The result is proved in the paper; nothing in it is open. As far as is known, none of it is formalized: Mathlib has no stochastic integral against Brownian motion, no BSDE theory and no BMO martingales. A complete development would be the first machine-checked solution of a continuous-time portfolio optimization problem by BSDE methods, and its intermediate results (measurable selection of nearest points, the BMO bound for quadratic BSDEs, the verification argument) are reusable.

Difficulty

The deterministic steps (the identity behind the choice of $f$, the growth and Lipschitz bounds) are short. The hard steps are elsewhere. Existence rests on Kobylanski's theorem for BSDEs with quadratic growth, whose proof is a monotone approximation argument with exponential transforms; the Lipschitz theory of Pardoux–Peng does not apply. Uniqueness and the optimality of $p^*$ need the BMO property of $\int Z\,dW$ and a Girsanov change of measure with a stochastic exponential of a BMO martingale. The selection Lemma 11 (b) cannot use a projection map because $\tilde C$ is not convex; a measurable choice from a possibly multivalued nearest-point set is required. Finally the verification argument is a localization: $R^{(p)}$ is only a local supermartingale, and passing to the limit uses the uniform integrability built into admissibility.

Formalization scope

Time is $\mathbb R_{\ge0}$ with $T>0$; row vectors of $\mathbb R^{1\times m}$ are EuclideanSpace ℝ (Fin m) (so $|\cdot|$ is Euclidean) and products such as $z\theta$ are inner products. The Brownian motion is the published EthierKurtz.IsStandardBrownian; the filtration and the stochastic integral come from the published module CvitanicKaratzas92_Optimality_Market (IsAugmentedBrownianFiltration, lebP for $\lambda\otimes P$, and an Itô-integral operator I). Predictability is measurability for Mathlib's Filtration.predictable. The market price of risk $\theta$ and the wealth $X^{(p)}$ are computed from the data, not assumed.

Expectations of $-\exp(\cdot)$ are minus lower integrals in $[0,\infty]$, and $V(x)$ is an extended real: a Bochner expectation would assign the junk value $0$ to non-integrable strategies and make them optimal, which is the trivializing formalization to avoid. Existence and uniqueness of the BSDE solution are part of the goal, not hypotheses, and the optimal strategy is a predictable selection of the nearest-point set, not of a choice function.

Disclosed readings: $\tilde C\neq\emptyset$ is assumed (otherwise $\mathcal A=\emptyset$); constraints and (8) are read $\lambda\otimes P$-a.e.; ellipticity holds for $P$-a.e. $\omega$ and all $t\le T$; $Y_0$ is a.s. constant and the value identity holds a.s.; uniqueness is in $Y_t$ a.s. for each $t$ and $Z$ $\lambda\otimes P$-a.e.; "$p^*$ given by Lemma 11" is read as any predictable selection; Lemma 11 (b) assumes full rank of $\sigma_t(\omega)$. The equivalence of the $\pi$- and $p$-formulations (Remark 5), the dynamic principle (Proposition 9) and Remarks 2–10 are out of scope.

Needed infrastructure: Itô calculus for continuous semimartingales, stochastic exponentials, BMO martingales and Kazamaki's criterion, Girsanov's theorem, quadratic BSDEs, and measurable selection. Contributions to any of these are welcome; they serve the companion power-utility mission (Theorem 14) as well.

Selected references

• Y. Hu, P. Imkeller, M. Müller, Utility maximization in incomplete markets, Ann. Appl. Probab. 15(3), 1691–1712, 2005. https://doi.org/10.1214/105051605000000188 (arXiv: https://arxiv.org/abs/math/0508448)
• M. Kobylanski, Backward stochastic differential equations and partial differential equations with quadratic growth, Ann. Probab. 28(2), 558–602, 2000. https://doi.org/10.1214/aop/1019160253
• J. Cvitanić, I. Karatzas, Convex duality in constrained portfolio optimization, Ann. Appl. Probab. 2(4), 767–818, 1992. https://doi.org/10.1214/aoap/1177005576
• E. Pardoux, S. Peng, Adapted solution of a backward stochastic differential equation, Systems Control Lett. 14(1), 55–61, 1990. https://doi.org/10.1016/0167-6911(90)90082-6
• N. El Karoui, R. Rouge, Pricing via utility maximization and entropy, Math. Finance 10(2), 259–276, 2000. https://doi.org/10.1111/1467-9965.00093
• F. Delbaen, P. Grandits, T. Rheinländer, D. Samperi, M. Schweizer, C. Stricker, Exponential hedging and entropic penalties, Math. Finance 12(2), 99–123, 2002. https://doi.org/10.1111/1467-9965.02001
• N. Kazamaki, Continuous Exponential Martingales and BMO, Lecture Notes in Math. 1579, Springer, 1994. https://doi.org/10.1007/BFb0073585

Motivation

An insurance company whose surplus falls below zero is ruined. The probability of ruin is the classical measure of solvency risk in actuarial mathematics. A company can lower it in two ways: it can invest part of its surplus in a risky asset, and it can pass part of each claim to a reinsurer in exchange for part of the premium. Which mix of investment and reinsurance minimises the probability of ruin is a stochastic control problem. It is studied in risk theory and in applied probability, and it is a model case for control problems with jumps.

Hipp and Plum (2000) solved the problem with investment alone. They wrote down the Hamilton–Jacobi–Bellman (HJB) equation and showed that it has a smooth solution. H. Schmidli (2002) added proportional reinsurance. He proved a verification theorem (his Theorem 1) and an existence theorem (his Theorem 2) for the combined problem. This mission formalizes the existence theorem and the analytic statements it rests on.

Setting

Claims arrive as a Poisson process with rate $\lambda>0$. The claim sizes $Y$ are independent with distribution function $G$, where $G(0)=0$ and $G$ is continuous. The insurer collects premiums at rate $c>0$. A risky asset follows a geometric Brownian motion with drift $\mu>0$ and volatility $\sigma>0$. Under proportional reinsurance with retention level $b\in[0,1]$, the insurer pays the fraction $bY$ of each claim and pays the reinsurer a premium at rate $c(b)$. The function $c(b)$ is decreasing and continuous, $c(1)=0$, $\liminf_{b\uparrow1}c(b)/(1-b)>0$, and there is $\underline b>0$ with $c(b)>c$ for $b<\underline b$ and $c(b)\le c$ for $b\ge\underline b$. In particular, full reinsurance costs more than the premium income.

Write $f$ for an unnormalised survival probability, with $f(u)=0$ for $u<0$. The HJB equation (1) of the problem is

$$\sup_{b\in[0,1]}\sup_{A\ge0}\Big[\tfrac12\sigma^2A^2f''(u)+\big(c-c(b)+\mu A\big)f'(u)+\lambda\big(\mathbb E[f(u-bY)]-f(u)\big)\Big]=0 ,$$

where $A$ is the amount invested. Eliminating $A$ and substituting $g=f'$ turns (1) into the integral equation (5):

$$g(u)=\frac{1}{\dfrac{\mu^2}{2\sigma^2}\displaystyle\int_0^u\frac{dx}{D_g(x)}+\dfrac{c}{\lambda}},$$ $$D_g(x)=\inf_{b\in[0,1]}\Big[\lambda\Big(1-G(x/b)+\int_0^x\big(1-G((x-z)/b)\big)g(z)\,dz\Big)-\big(c-c(b)\big)g(x)\Big].$$

Condition (6) at $u$ is $D_g(u)>0$. In Lean, ReinsPremium, ClaimLaw, tail, den ($=D_g$), SolvesEq5On, H and SolvesHJB (equation (1)) live in the shared module SchmidliRuin.Verif.Setting; HasBoundedDensity, Cond6, SolvesEq3At and SolvesHJBAtZero live in SchmidliRuin.Exist.Setting.

Formalization targets

Goal: Theorem 2 (p. 900)

If $G$ has a bounded density, then

$$\exists!\ g:[0,\infty)\to\mathbb R\ \text{strictly decreasing, solving (5) on }[0,\infty).$$

Lean states this as two conjuncts: existence, and equality on $[0,\infty)$ of any two strictly decreasing solutions.

Milestones, in attack order

1. Lemma 3 (p. 894). For a solution $f$ of (3) on $[0,\eta)$, the optimal retention is $b^*(u)=1$ for small $u$: it is optimal not to reinsure small capital.
2. Lemma 4 (p. 898). Under a bounded density, (5) has a solution on some $[0,\varepsilon)$, with $g(u)=\lambda/c-\alpha\sqrt u+o(\sqrt u)$ and $\alpha=\lambda\mu/(\sigma c^{3/2})$.
3. Condition (6) near $0$ (pp. 898–899): such a local solution satisfies $D_g(u)>0$ for small $u>0$.
4. Lemma 5 (p. 899). A decreasing solution on $[0,u_0)$ with (6) on $(0,u_0)$ extends to $[0,u_0]$, and (6) holds at $u_0$.
5. Continuation (proof of Theorem 2, p. 901). A solution with (6) on $(0,u_0]$ continues to $[0,u_0+\eta)$ with (6).
6. Theorem 1, second sentence (p. 896). For a decreasing solution $g$ of (5), $f(x)=1+\int_0^xg$ is a strictly increasing solution of (1), twice continuously differentiable on $(0,\infty)$.
7. Theorem 1, last sentence (p. 896). There is at most one strictly increasing, twice continuously differentiable solution of (1) with $f(0)=1$.

Significance

The existence theorem completes the dynamic-programming solution of the problem. By the verification theorem, $f=1+\int_0^\cdot g$ divided by $f(\infty)$ is the maximal survival probability $\delta(u)$. The maximisers of the HJB equation define the optimal feedback strategy: the investment $A^*(u)=-\mu f'(u)/(\sigma^2f''(u))$ and the retention level $b^*(u)$. Without Theorem 2 the verification theorem would be a statement about a function that might not exist. Equation (5) is also the basis of the paper's numerical scheme (§5), which iterates (5) to compute $\delta$ and the optimal strategies.

Theorem 2 has a published proof. As far as is known, none of the results above has a machine-checked proof, and nothing on Prove2Me states them. The work is to formalize the published argument. This takes the local existence result of Hipp and Plum, which the paper cites rather than reproves, and a continuation argument for a nonlinear Volterra-type equation whose kernel is an infimum over a control parameter. Milestones 6 and 7 are the purely analytic content of the verification theorem that the uniqueness part of Theorem 2 uses. The paper derives milestone 7 stochastically, and an analytic proof is equally welcome.

Difficulty

The denominator $D_g(x)$ vanishes at $x=0$: $D_g(0)=\lambda-c\,g(0)=0$, because $g(0)=\lambda/c$. The integral in (5) is therefore improper at the origin. A Picard iteration started from a constant does not work, because it does not control $\int_0^u dx/D_g(x)$. One needs the exact square-root rate $D_g(x)\asymp\sqrt x$, and Lemma 4 obtains it only through Lemma 3 (no reinsurance near $0$) and the Hipp–Plum analysis of the reinsurance-free equation. Lemma 4's proof in the paper is a two-line citation, so a solver must formalize that local existence result.

The second difficulty is continuation. A solution can be continued as long as condition (6) holds, and Lemma 5 has to exclude that (6) degenerates at a finite endpoint. There the infimum over $b$ interacts with the vanishing of $g$. The paper's argument uses a Gronwall estimate and the shape of $c(b)$ around $\underline b$, and the minimiser $b$ in $D_g$ need not be unique or continuous.

Formalization scope

• Model data. $c,\lambda,\mu,\sigma$ are real parameters, all strictly positive. The claim law is a probability measure $\nu$ on $\mathbb R$, with $G=$ cdf ν, $\nu((-\infty,0])=0$ and $G$ continuous. "Bounded density" means $\nu$ has a measurable density with values in $[0,C]$. $\mathbb E[h(u-bY)]$ is $\int h(u-by)\,d\nu(y)$.

• Premium. $c(b)$ is a real function, used on $[0,1]$. The condition $\liminf_{b\uparrow1}c(b)/(1-b)>0$ is the lower bound $c(b)\ge\kappa(1-b)$ near $1$, which is equivalent. A real-valued $c$ excludes the case $c(0)=\infty$ that the paper allows when $\mathbb E[Y]<\infty$.

• Conventions.

  • $1-G(x/b)$ at $b=0$ is $\mathbb P[0\cdot Y>x]=0$; it is computed by tail, never by Lean's $x/0=0$.
  • "$g$ solves (5) at $u$" includes that the integral exists: $g$ is integrable on $[0,u]$, $D_g\ne0$ on $(0,u)$, and $1/D_g$ is integrable on $[0,u]$.
  • Every supremum of the paper is a least upper bound (IsLUB … 0). Lean's sSup would return $0$ on an unbounded family, for example when $f''\ge0$, and that would make "$f$ solves (1)" true by accident.
  • Uniqueness is equality on $[0,\infty)$. The values of $g$ off $[0,\infty)$ are free, so a unique-existence quantifier over $\mathbb R\to\mathbb R$ would be false.
  • "Twice continuously differentiable" is read on $(0,\infty)$, since $f''(0+)=-\infty$ (p. 895). At $u=0$, (1) and (3) are taken in the boundary form $\sup_b[(c-c(b))f'(0)+\lambda(\mathbb E f(-bY)-f(0))]=0$, with the right derivative $f'(0)$.
  • $\lambda$ and $c$ are general. §4 sets $\lambda=c=1$ by a change of units.

• Trivialising readings ruled out.

  • Encoding (5) with an unguarded $1/D_g$ would let a function with a vanishing denominator "solve" (5).
  • Dropping the boundary equation at $u=0$ from Lemma 3 makes it false: a premium flat near $b=0$ admits local solutions with $b^*\equiv0$.

• Infrastructure needed.

  • existence of the minimiser in $D_g$ and continuity of $D_g$ in $x$;
  • a local existence theorem for singular integral equations in the style of Hipp–Plum;
  • Gronwall's inequality (Mathlib has versions);
  • Banach's fixed-point theorem (ContractingWith).

  The continuation and closure lemmas (milestones 3–5) are reusable for other HJB equations of risk theory with a jump term. Contributions that state and prove intermediate claims of the paper's proofs are welcome as sub-results.

Selected references

• H. Schmidli, On minimizing the ruin probability by investment and reinsurance, Ann. Appl. Probab. 12(3), 890–907, 2002. https://doi.org/10.1214/aoap/1031863173
• C. Hipp and M. Plum, Optimal investment for insurers, Insurance Math. Econom. 27(2), 215–228, 2000. https://doi.org/10.1016/S0167-6687(00)00049-4
• H. Schmidli, Optimal proportional reinsurance policies in a dynamic setting, Scand. Actuar. J. 2001(1), 55–68, 2001. https://doi.org/10.1080/034612301750077338
• S. N. Ethier and T. G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986. https://doi.org/10.1002/9780470316658

Motivation

Optimal control problems with pointwise bounds on the control, such as

$$\min_u \tfrac12\|y - z\|_{L^2}^2 + \tfrac{\beta}{2}\|u\|_{L^2}^2 \quad\text{subject to } -\Delta y = u \text{ in } \Omega,\ y = 0 \text{ on } \partial\Omega,\ u \le \psi,$$

reduce, after eliminating the state, to a quadratic program in $L^2(\Omega)$ with a pointwise upper bound. The primal-dual active set strategy solves such problems by guessing the set where the bound is active, solving one linear system on that guess, and updating the guess from the new primal and dual values. It is used routinely in PDE-constrained optimization because each iteration costs one linear solve and, in practice, very few iterations are needed.

Hintermüller, Ito and Kunisch (SIAM J. Optim. 13 (2002) 865–888; authors' version hal-01660511) showed that this strategy is a semismooth Newton method for a nonsmooth reformulation of the optimality system, built on the notion of slant differentiability of Chen, Nashed and Qi (SIAM J. Numer. Anal. 38 (2000) 1200–1216). In finite dimension this gives local superlinear convergence (missions I–IV of this series). This mission concerns the paper's function-space result, Theorem 4.1: in $L^2(\Omega)$, under a norm gap on the operator, the method still converges locally superlinearly. Ulbrich (SIAM J. Optim. 13 (2003) 805–841) developed a related semismooth Newton theory for superposition operators in function spaces, which also requires a norm gap.

Setting

Let $(\Omega, \mu)$ be a finite measure space (the paper takes a bounded domain $\Omega \subset \mathbb{R}^n$ with Lebesgue measure) and $L^p = L^p(\Omega)$ the real Lebesgue spaces, with inner product $(\cdot,\cdot)$ on $L^2$. The paper writes $A$ for an operator and calligraphic $\mathcal{A}$, $\mathcal{I}$ for active and inactive sets.

Slant differentiability (Definition 1). For Banach spaces $X$, $Z$, a map $F : X \to Z$ is slantly differentiable in an open set $U$ if there is $G : U \to \mathcal{L}(X, Z)$, a slanting function, with

$$\lim_{h\to 0}\frac{1}{\|h\|}\,\|F(x+h) - F(x) - G(x+h)h\| = 0 \qquad (x \in U). \tag{A}$$

For $\delta \in \mathbb{R}$, the candidate slanting function of the pointwise max is $G_m(y)(x) = 1$ if $y(x) > 0$, $0$ if $y(x) < 0$, $\delta$ if $y(x) = 0$ (4.1).

The problem. Given $f, \psi \in L^2$ and a self-adjoint $A \in \mathcal{L}(L^2)$ with

$$(Ay, y) \ge \gamma\|y\|^2 \quad (\gamma > 0), \tag{H1}$$

minimize $\tfrac12(y, Ay) - (f, y)$ subject to $y \le \psi$. The solution $y^*$ and its multiplier $\lambda^*$ are the unique solution of

$$Ay^* + \lambda^* = f, \qquad \lambda^* - \max(0, \lambda^* + c(y^* - \psi)) = 0 \ \text{a.e.}, \tag{4.2}$$

for any fixed $c > 0$. The norm gap hypothesis is

$$A = C + \beta I, \qquad C \in \mathcal{L}(L^2, L^q),\quad \beta > 0,\quad q > 2. \tag{H2}$$

The algorithm. From $(y^0, \lambda^0) \in L^2 \times L^2$, set $\mathcal{A}_k = \{x : \lambda^k(x) + c(y^k(x) - \psi(x)) > 0\}$, $\mathcal{I}_k = \Omega\setminus\mathcal{A}_k$, and solve

$$Ay^{k+1} + \lambda^{k+1} = f, \qquad y^{k+1} = \psi \text{ on } \mathcal{A}_k, \qquad \lambda^{k+1} = 0 \text{ on } \mathcal{I}_k.$$

A sequence obeying this rule for every $k$ is a run. Superlinear convergence of $x^k \to x^*$ means $x^k \to x^*$ and, for every $\eta > 0$, eventually $\|x^{k+1} - x^*\| \le \eta\|x^k - x^*\|$.

Formalization targets

Goal: Theorem 4.1 (p. 15)

The page reads: "Assume that (H1), (H2) hold and that ψ and f are in L^q(Ω). Then the primal-dual active set strategy or, equivalently, the semismooth Newton method converge superlinearly if ‖y⁰ − y*‖ is sufficiently small and λ⁰ = β(y⁰ − ψ)." The formalized goal is the statement the proof establishes: with $c = \beta$, there is $\rho > 0$ such that every run with

$$\|y^0 - y^*\|_{L^2} < \rho, \qquad \lambda^0 = f - Ay^0$$

converges superlinearly to $(y^*, \lambda^*)$ in $L^2 \times L^2$. The initialization differs from the printed one; see Formalization scope.

Milestones

1. Theorem 1.1 (Chen–Nashed–Qi): slant differentiability near a zero $x^*$ with uniformly bounded $G(x)^{-1}$ gives local superlinear convergence of $x^{k+1} = x^k - G(x^k)^{-1}F(x^k)$.
2. Proposition 4.1(ii): for $1 \le p < q \le \infty$, $\max(0,\cdot) : L^q \to L^p$ is slantly differentiable with slanting function $G_m$.
3. (4.9)–(4.10): for $c = \beta$, (4.2) is equivalent to $\beta y^* - \beta\psi + \max(0, Cy^* - f + \beta\psi) = 0$ and $\lambda^* = f - Cy^* - \beta y^*$.
4. Equivalence of the algorithms: along a run with $c = \beta$ and $\lambda^0 = f - Ay^0$, $\lambda^k + \beta(y^k - \psi) = f - Cy^k - \beta\psi$ for all $k$, so the active sets are those of the reduced algorithm.
5. Slant differentiability of the reduced map $F(y) = \beta y - \beta\psi + \max(0, Cy - f + \beta\psi)$ on $L^2$, with $G_F(y+h) = \beta I + G_m(Cy - f + \beta\psi + Ch)C$, $\delta = 1$.
6. Bounded inverses: $G_F(z)$ is invertible on $L^2$, with $\|G_F(z)^{-1}\|$ bounded uniformly in $z$.

Two companion items accompany the goal: existence of a run from every $y^0$, and Proposition 4.1(i), the paper's counterexamples showing that $G_m$ fails to be a slanting function from $L^p$ to $L^p$.

Significance

Theorem 4.1 is the infinite-dimensional justification of a method used throughout control-constrained optimal control: it shows that the method converges locally superlinearly for the continuous problem itself, not only for each discretization. Example 1 of the paper shows that distributed control of the Poisson equation, and boundary control with Sobolev embeddings, satisfy (H2). Proposition 4.1 isolates the structural reason: the pointwise max is a Newton-differentiable map only between spaces with a norm gap.

None of these results is known to be machine-checked. A complete development would provide slant differentiability in Banach spaces, the Chen–Nashed–Qi local convergence theorem, the norm-gap differentiability of $\max(0,\cdot)$ between Lebesgue spaces, and invertibility of block operators on $L^2$ of a measurable partition. Each of these is reusable for other semismooth Newton analyses in function space.

Difficulty

The obvious argument fails at the max. In finite dimension, $\max(0,\cdot)$ is slantly differentiable with $G_m$ because a small perturbation does not change the sign of any nonzero component. In $L^2$, a perturbation $h$ of small norm can flip the sign of $y$ on a set of positive measure, and on that set the error $\max(0, y+h) - \max(0, y) - G_m(y+h)h$ is as large as $|y|$. Proposition 4.1(i) shows that this error is not $o(\|h\|_{L^p})$ in $L^p$ for any $p$. Superlinear convergence in $L^2$ therefore needs the argument of the max to be controlled in a stronger norm than the error is measured in, which is what (H2) and $f, \psi \in L^q$ provide. A second difficulty is that the two-variable algorithm is not literally a Newton method for a map of $y$ alone; it must be identified with the reduced algorithm, and that identification depends on the initialization.

Formalization scope

• Spaces. $L^p$ is Mathlib's Lp ℝ p μ on an arbitrary finite measure space; $q \in (2, \infty]$ is an extended real with 2 < q. The paper's bounded Lipschitz domain is replaced by a finite measure space: the proofs use only $|\Omega| < \infty$, and Mathlib has no notion of Lipschitz boundary.
• Pointwise statements on $L^p$ classes are almost everywhere statements about representatives. (H2) is stated as $Ay = Cy + \beta y$ a.e. for every $y \in L^2$, which avoids building the inclusion $L^q \subseteq L^2$.
• Hypotheses kept: self-adjointness of $A$, (H1) with explicit $\gamma > 0$, (H2) with $\beta > 0$ and $q > 2$, $f, \psi \in L^q$. The solution $(y^*, \lambda^*)$ of (4.2) is a hypothesis; it exists and is unique under (H1), as the paper states on p. 12.
• The initialization. The printed $\lambda^0 = \beta(y^0 - \psi)$ does not support the proof, which uses "$\lambda^0 + \beta(y^0 - \psi) = f - Cy^0 - \beta\psi$" and $c = \beta$. That identity holds exactly for $\lambda^0 = f - Ay^0$. The goal uses $\lambda^0 = f - Ay^0$ and $c = \beta$. With the printed initialization the first active set is $\{y^0 > \psi\}$, and for $y^0$ slightly below $y^*$ the first iterate solves the unconstrained problem, which can be far from $y^*$.
• Superlinear convergence is stated for the pair $(y^k, \lambda^k)$ in the product norm $\max(\|y\|, \|\lambda\|)$, without dividing by $\|x^k - x^*\|$, so finite termination qualifies. "Sufficiently small" is an $\exists\rho > 0$ chosen before the run, on $\|y^0 - y^*\|$ only.
• No trivialization. The goal mentions neither the reduced algorithm, nor $G_F$, nor Proposition 4.1; the norm gap $q > 2$ is not weakened to $C \in \mathcal{L}(L^2)$, under which Proposition 4.1(i) shows that $G_m$ need not be a slanting function; and the companion run_exists shows that the runs the goal quantifies over exist.
• Definitions (PDASNewton.FunSpace.Setting): slanting functions, superlinear convergence, $G_m$, property (A) for $\max(0,\cdot) : L^q \to L^p$, system (4.2), one step and runs of the algorithm. These duplicate the finite-dimensional definitions of the other missions of the series in a separate namespace.

Proofs of any milestone are welcome, as are reusable lemmas on Lebesgue spaces (Hölder on sets of small measure, multiplication operators, Lax–Milgram on $L^2$ of a measurable subset).

Selected references

• M. Hintermüller, K. Ito, K. Kunisch, The primal-dual active set strategy as a semismooth Newton method, SIAM J. Optim. 13(3) (2002) 865–888. https://doi.org/10.1137/S1052623401383558 ; authors' version https://hal.science/hal-01660511
• X. Chen, Z. Nashed, L. Qi, Smoothing methods and semismooth methods for nondifferentiable operator equations, SIAM J. Numer. Anal. 38 (2000) 1200–1216. https://doi.org/10.1137/S0036142999356719
• M. Ulbrich, Semismooth Newton methods for operator equations in function spaces, SIAM J. Optim. 13 (2003) 805–841. https://doi.org/10.1137/S1052623400371569
• L. Qi, J. Sun, A nonsmooth version of Newton's method, Math. Programming 58 (1993) 353–367. https://doi.org/10.1007/BF01581275