Convex Optimization Operations Research Probability·Captain: mikedeng1

Arbitrage and Duality in Nondominated Discrete-Time Models II: Nondominated Optional Decomposition — a Supermartingale Under Every Martingale Measure Is V₀ + H•S − KResearch Paper

Motivation

In a financial market with a single probability model, the Optional Decomposition Theorem describes the processes that can be dominated by trading. If a process $V$ is a supermartingale under every equivalent martingale measure, then it can be written as an initial value plus a stochastic integral against the stock price, minus an increasing process that represents consumption. El Karoui and Quenez proved it for diffusion models (SIAM J. Control Optim. 33 (1995)) and Kramkov for locally bounded semimartingales (Probab. Theory Related Fields 105 (1996)). It is the step that turns the superhedging price, a supremum of expectations over martingale measures, into an actual dynamic hedging strategy.

Model uncertainty replaces the single model by a set $\mathcal P$ of probability measures that may be mutually singular. This happens, for example, when volatility is only known to lie in an interval. There is then no reference measure, "almost surely" becomes "quasi surely" (outside a set that is null under every model), and the classical proofs, which rely on one dominating measure, do not apply. Bouchard and Nutz (Ann. Appl. Probab. 2015, arXiv:1305.6008) built the discrete-time theory of this setting: no-arbitrage, the fundamental theorem of asset pricing, superhedging duality and, in §6, a nondominated optional decomposition. This mission formalizes that last result.

Timeline:

1995: El Karoui and Quenez, optional decomposition in diffusion models.
1996: Kramkov, for locally bounded semimartingales.
2014: Nutz, superreplication duality under model uncertainty in discrete time (Finance Stoch. 18 (2014)).
2015: Bouchard and Nutz, the fundamental theorem, superhedging duality and the optional decomposition in nondominated discrete time (Theorem 6.1).

Setting

Fix a Polish space $\Omega_1$ , a horizon $T \in \mathbb N$ and $d \in \mathbb N$ . Let $\Omega_t := \Omega_1^t$ for $t = 0, \dots, T$ . Then $\Omega_0$ is a single point and $\Omega := \Omega_T$ , and a point of $\Omega_t$ is read as the first $t$ coordinates of a path. The $\sigma$ -field $\mathcal F_t$ is the universal completion of $\mathcal B(\Omega_t)$ .

For each $t < T$ and each node $\omega \in \Omega_t$ a nonempty convex set $\mathcal P_t(\omega)$ of probability measures on $\Omega_1$ is given, and its graph is an analytic set. The set of possible models $\mathcal P$ consists of all products $P_0 \otimes P_1 \otimes \cdots \otimes P_{T-1}$ whose kernels take values in $\mathcal P_t(\cdot)$ . A set is $\mathcal P$ -polar if it is null under every $P \in \mathcal P$ . A property holds $\mathcal P$ -quasi surely (q.s.) if it holds outside a polar set.

Stock prices $S_t : \Omega_t \to \mathbb R^d$ are Borel. A strategy $H \in \mathcal H$ is predictable: $H_u$ is a function of the first $u-1$ coordinates. The wealth at time $t$ is

H \bullet S_t = \sum_{u=1}^t H_u \Delta S_u, \qquad \Delta S_u = S_u - S_{u-1}.

NA( $\mathcal P$ ) holds if $H \bullet S_T \ge 0$ q.s. implies $H \bullet S_T = 0$ q.s. A martingale measure is a probability $Q$ under which $S$ is a martingale. The set

\mathcal Q = \{Q \lll \mathcal P : Q \text{ is a martingale measure}\}

contains those $Q$ that are absolutely continuous with respect to some $P \in \mathcal P$ (written $Q \lll \mathcal P$ ). A function $f$ with values in $[-\infty, \infty]$ is upper semianalytic if every set $\{f > c\}$ is analytic.

At one node $\omega \in \Omega_t$ , the increment $\Delta S_{t+1}(\omega, \cdot)$ defines a one-period market under $\mathcal P_t(\omega)$ , with its own no-arbitrage condition NA( $\mathcal P_t(\omega)$ ) and one-period martingale measures $\mathcal Q_t(\omega)$ . The conditional sublinear expectation is

\mathcal E_t(f)(\omega) = \sup_{Q \in \mathcal Q_t(\omega)} E_Q[f(\omega, \cdot)].

Formalization targets

Goal: Theorem 6.1 (nondominated optional decomposition)

Let NA( $\mathcal P$ ) hold and let $V$ be an adapted process such that $V_t$ is upper semianalytic and in $L^1(Q)$ for all $Q \in \mathcal Q$ and $t \in \{1, \dots, T\}$ . Then the following are equivalent:

$V$ is a supermartingale under each $Q \in \mathcal Q$ ;
there exist $H \in \mathcal H$ and an adapted increasing process $K$ with $K_0 = 0$ such that

V_t = V_0 + H \bullet S_t - K_t \quad \mathcal P\text{-q.s.}, \qquad t = 0, 1, \dots, T.

Milestones

Lemma 4.6: the set $N_t$ of nodes where NA( $\mathcal P_t(\omega)$ ) fails is universally measurable, and it is polar under NA( $\mathcal P$ ).
Theorem 4.5: NA( $\mathcal P$ ) holds if and only if every $N_t$ is polar, if and only if every $P \in \mathcal P$ is absolutely continuous with respect to some $Q \in \mathcal Q$ .
Lemma 4.10: $\mathcal E_t(f)$ is upper semianalytic, and there is a universally measurable $y$ with

\mathcal E_t(f)(\omega) + y(\omega)\,\Delta S_{t+1}(\omega, \cdot) \ge f(\omega, \cdot) \quad \mathcal P_t(\omega)\text{-q.s.}

at every arbitrage-free node where $f(\omega,\cdot) > -\infty$ q.s.

(6.1): under condition 1 of the goal, $\mathcal E_t(V_{t+1}) \le V_t$ $\mathcal P$ -q.s. for every $t < T$ .

Significance

The decomposition is the dynamic counterpart of superhedging duality. Duality identifies the price $\sup_{Q} E_Q[f]$ . The optional decomposition, applied to the process of conditional superhedging prices, produces one strategy that superhedges under all models at once and a nonnegative increasing process recording the surplus. The proof works in a nondominated model with one strategy $H$ that is measurable in the universal completion, and this is what makes the theorem usable under volatility or model uncertainty, where no single model can be singled out. The equivalence also characterizes the processes that are supermartingales under every $Q \in \mathcal Q$ : up to a polar set they are exactly the wealth processes of strategies that consume.

The result is proved in the paper; no part of it has a machine-checked proof, on the platform or in Mathlib. Mathlib has martingales, conditional expectation and analytic sets. It has no quasi-sure analysis, no product of measurable selectors of a random set of measures, no conditional sublinear expectation and no superhedging. The mission produces a machine-checked development of the one-period-to-multi-period machinery of the paper (Theorem 4.5, Lemmas 4.6 and 4.10) and of the decomposition itself.

Difficulty

With one dominating measure, the classical proof works under a fixed equivalent martingale measure and uses conditional expectations and a single null-set structure. Here the measures in $\mathcal P$ may be mutually singular, so conditional expectations under different $Q$ disagree off their supports, and no countable family of measures controls all null sets. The proof has to work node by node, $\omega \mapsto \mathcal P_t(\omega)$ . Every object built at a node (the worst-case conditional expectation, a near-optimal measure, a hedging ratio) must then be glued back together measurably in $\omega$ . Borel measurability is not preserved by taking suprema over the random set $\mathcal Q_t(\omega)$ . Upper semianalyticity is, but only together with measurable selection theorems for analytic sets (Jankov–von Neumann) and the universal completion. The first idea, which is to apply the classical theorem under each $P \in \mathcal P$ separately, fails. It gives one strategy per model, and in general uncountably many models cannot be aggregated into one strategy.

Formalization scope

The Lean development uses the following conventions.

Paths and measures. $\Omega_t$ is Fin t → Ω₁, and measures are Borel. $\mathcal F_t$ -measurability is universal measurability, which is the published platform definition BertsekasShreve.AnalyticSelection.IsUniversallyMeasurable.
Polar sets. A polar set is null in outer measure under every model. The exceptional sets in the statements are universally measurable, and for such sets this agrees with the paper's definition.
The model set. $\mathcal P$ consists of the laws of Borel Markov kernels that lie in $\mathcal P_t$ almost surely, which is the paper's equivalent formulation on p. 4.
Processes. A process is a family V t : (Fin t → Ω₁) → ℝ, so adaptedness is built into the type.
Strategies. The Lean strategy H u is the paper's $H_{u+1}$ .
Expectations. Expectations of functions with values in $[-\infty, \infty]$ follow (1.1) in EReal, with $\infty - \infty = -\infty$ . Suprema over $\mathcal Q_t(\omega)$ are taken in EReal.
Options. The setting has no options ( $e = 0$ ).
Page numbers. Pages and indices are those of the arXiv v3 reprint (arXiv:1305.6008v3), not the journal pagination 823–859.

The increasing process $K$ must be adapted and nondecreasing on every path. Dropping monotonicity would make condition 2 trivially true, with $K := V_0 + H \bullet S - V$ for any $H$ . Integrability and supermartingale properties are always stated with explicit $Q$ -integrability, so Bochner integrals of non-integrable functions cannot make a statement vacuous.

The development needs the following infrastructure:

analytic sets and measurable selection (some of it exists for Bertsekas–Shreve on the platform);
measurability of $(\omega, Q) \mapsto E_Q[f(\omega,\cdot)]$ ;
products of kernels;
the one-period fundamental theorem and superhedging duality.

These pieces are shared with the companion mission Arbitrage and Duality in Nondominated Discrete-Time Models I, which formalizes the superhedging theorem. Contributions to either side are welcome. The paper derives (ii) ⇒ (i) from Lemma A.1, a classical fact about local and generalized martingales under one measure, which is not posed as a milestone here.

Selected references

B. Bouchard, M. Nutz, Arbitrage and duality in nondominated discrete-time models, Ann. Appl. Probab. 25(2), 823–859, 2015. https://doi.org/10.1214/14-AAP1011, arXiv:1305.6008v3 https://arxiv.org/abs/1305.6008
N. El Karoui, M.-C. Quenez, Dynamic programming and pricing of contingent claims in an incomplete market, SIAM J. Control Optim. 33, 29–66, 1995. MR1311659, https://mathscinet.ams.org/mathscinet-getitem?mr=1311659
D. O. Kramkov, Optional decomposition of supermartingales and hedging contingent claims in incomplete security markets, Probab. Theory Related Fields 105, 459–479, 1996. MR1402653, https://mathscinet.ams.org/mathscinet-getitem?mr=1402653
M. Nutz, Superreplication under model uncertainty in discrete time, Finance Stoch. 18, 791–803, 2014. MR3255751, https://mathscinet.ams.org/mathscinet-getitem?mr=3255751
D. P. Bertsekas, S. E. Shreve, Stochastic Optimal Control: The Discrete Time Case, Mathematics in Science and Engineering 139, Academic Press, 1978. MR0511544, https://mathscinet.ams.org/mathscinet-getitem?mr=0511544

10 thms1 active userReviewed

Control Theory Partial Differential Equations Probability·Captain: mikedeng1

Viscosity Solutions to Parabolic Master Equations and McKean–Vlasov SDEs with Closed-Loop Controls 2: Comparison Principle and Uniqueness for Viscosity Solutions of Parabolic Master EquationsResearch Paper

Motivation

Master equations are partial differential equations whose state variable is a probability measure. They arise as the dynamic programming equations of mean-field control problems, as the limits of large particle systems, and as the pricing equations of options on a whole population. Their coefficients and solutions are functions on a Wasserstein space, which is infinite dimensional, and classical (smooth) solutions are known only under strong regularity assumptions (Cardaliaguet–Delarue–Lasry–Lions 2019). A notion of weak solution for which existence, comparison and uniqueness can all be proved is therefore the basic missing tool.

C. Wu and J. Zhang (Ann. Appl. Probab. 2020) propose such a notion for parabolic master equations on the space of laws of continuous paths, in the spirit of the viscosity theory for path-dependent PDEs of Ekren, Keller, Touzi and Zhang (Ann. Probab. 2014). This mission formalizes its §4: the definition of viscosity solutions and the comparison principle that makes them unique.

Setting

Fix a horizon $T$ and a dimension $d$ . The canonical space is $\Omega=C([0,T];\mathbb R^d)$ with the uniform norm $\|\omega\|$ , the canonical process is $X_t(\omega)=\omega_t$ , and $\mathcal F_t=\sigma(X_s:s\le t)$ . $\mathcal P_2$ is the set of probability measures $\mu$ on $\Omega$ with $\mathbb E^\mu\|X\|^2<\infty$ ; $\mu_{[0,t]}$ is the law of the stopped path $X_{t\wedge\cdot}$ . The state space is $\Theta=[0,T]\times\mathcal P_2$ with the pseudometric

\mathcal W_2\big((t,\mu),(t',\mu')\big)=\big(|t-t'|+\mathcal W_2^2(\mu_{[0,t]},\mu'_{[0,t']})\big)^{1/2},

where $\mathcal W_2$ on laws is the 2-Wasserstein distance. A function $V:\Theta\to\mathbb R$ has a time derivative $\partial_tV$ , a path derivative $\partial_\mu V(t,\mu,\omega)\in\mathbb R^d$ and a second derivative $\partial_\omega\partial_\mu V(t,\mu,\omega)\in\mathbb R^{d\times d}$ , defined through a functional Itô formula along semimartingale laws.

The master equation (3.1) is

\mathbb LV(t,\mu):=\partial_tV(t,\mu)+G\big(t,\mu,V(t,\mu),\partial_\mu V(t,\mu,\cdot),\partial_\omega\partial_\mu V(t,\mu,\cdot)\big)=0,

with a generator $G$ that is continuous in $(t,\mu)$ , Lipschitz in $y$ , and Lipschitz in $(Z,\Gamma)$ in the averaged sense (3.2) of Assumption 3.1.

For $L>0$ , $\mathcal P_L(t,\mu)$ is the set of laws $\mathbb P\in\mathcal P_2$ that agree with $\mu$ up to time $t$ and under which $X$ is a semimartingale on $[t,T]$ with drift bounded by $L$ and half squared diffusion bounded by $L$ . Test functions at $(t,\mu)$ are $C^{1,1,1}$ functions on $[t,t+\delta]\times\mathcal P_L(t,\mu)$ touching $V$ from above or below there, (4.2). $V\in C^0(\Theta)$ is an $L$ -viscosity subsolution (supersolution) if $\mathbb L\varphi(t,\mu)\ge0$ ( $\le0$ ) for every such test function, and a viscosity solution if it is both for one $L>0$ (Definition 4.4). The Perron envelopes $\overline V$ , $\underline V$ of (4.17) are the infimum of piecewise classical supersolutions above $g$ and the supremum of piecewise classical subsolutions below $g$ .

Formalization targets

Goal: comparison and uniqueness (Theorem 4.13)

Under Assumption 3.1 and $g\in C^0(\mathcal P_2)$ , if $V_1$ is a viscosity subsolution, $V_2$ a viscosity supersolution, $V_1(T,\cdot)\le g\le V_2(T,\cdot)$ , the classes $\underline{\mathcal U}_g,\overline{\mathcal U}_g$ are nonempty, and

\overline V=\underline V=:V,\qquad(4.19)

then $V_1\le V\le V_2$ on $\Theta$ , and $V$ is the unique viscosity solution with terminal condition $g$ .

Milestones

the moment estimate (4.1) over $\mathcal P_L(t,\mu)$ ;
Lemma 4.1: $[t,T]\times\mathcal P_L(t,\mu)$ is compact under $\mathcal W_2$ ;
Theorem 4.7: viscosity solutions are characterized by semi-jets of paraboloids;
Theorem 4.9: the change of variable $\tilde V=e^{\lambda t}V$ ;
Theorem 4.6: consistency with classical solutions;
Theorem 4.11: partial comparison when one side is smooth;
Proposition 4.12: a continuous lower envelope $\underline V$ is a viscosity subsolution.

Significance

The comparison principle is what turns a definition into a theory: it gives uniqueness, it identifies value functions of mean-field control problems with the solution of their master equation, and it is the input of stability and convergence arguments for numerical schemes. Theorem 4.13 reduces well-posedness to condition (4.19), and the authors verify (4.19) in examples (§4.6) via Theorem 4.14. The compactness of $\mathcal P_L(t,\mu)$ (Lemma 4.1) is the device that replaces local compactness, which the Wasserstein space lacks; it is reusable for any viscosity theory over semimartingale laws.

These results are proved on paper. No machine-checked development of viscosity solutions on Wasserstein spaces, or of the path-dependent functional Itô calculus on laws, is known to exist. A formalization would produce a checked notion of viscosity solution for master equations, the compactness of bounded-characteristic semimartingale laws, and the comparison machinery, and would expose the points where the printed proofs are sketched (see below).

Difficulty

The obvious route, copying the finite-dimensional theory, fails at two places. First, the doubling-of-variables argument for comparison needs a penalization on the state space that is smooth and coercive; on $\mathcal P_2$ under $\mathcal W_2$ neither is available, which is why comparison is reached through partial comparison and Perron envelopes. Second, maxima of $\varphi-V$ need not be attained on Wasserstein balls, which are not compact; the theory therefore tests only on $[t,T]\times\mathcal P_L(t,\mu)$ , and Lemma 4.1 (via Zheng's tightness criterion for semimartingale laws and uniform integrability of $\|X\|^2$ ) is what makes the extrema exist. The printed proof of Theorem 4.13 opens with " $\overline V$ is lower semicontinuous and $\underline V$ is upper semicontinuous"; as printed the directions are swapped (an infimum of functions continuous in $\mu$ is upper semicontinuous in $\mu$ ), and the members of $\mathcal U$ are only càdlàg in $t$ , so the continuity of $V$ needed for the conclusion requires an argument of its own.

Formalization scope

Time is $\mathbb R_{\ge0}$ , and every condition is imposed only at $t\le T$ , $\mu\in\mathcal P_2$ . $\mathbb R^d$ is the Euclidean space, matrices are $d\times d$ real matrices with the Frobenius norm, and $A:B=\sum_{ij}A_{ij}B_{ij}$ . $\mathcal W_2$ is the published WassersteinDRO.Duality.wassersteinDistance on laws of paths; Brownian motion and the Itô integral are the published EthierKurtz definitions. Membership in $\mathcal P_L(t,\mu)$ is the existence of a representation of $\mathbb P$ as the law of an Itô process from time $t$ with $|b|\le L$ , $\tfrac12|\sigma|^2\le L$ (§2.4). A $C^{1,1,1}$ object is a record of a function and three derivative functions, and the functional Itô formula (2.25) is required in drift form for every representation, which equals (2.25) because the stochastic integral has mean zero. Test sets encode " $\inf(\varphi-V)=0$ " literally, and the data of a test function at $(t,\mu)$ are its values at $(t,\mathbb P)$ , $\mathbb P\in\mathcal P_L(t,\mu)$ . The Perron envelopes are extended-real infima and suprema over the classes (4.18); (4.19) is stated with a real-valued $V$ .

Two readings are fixed. Assumption 3.1(i) is continuity of $(t,\mu)\mapsto G(t,\mu,y,Z(X_{t\wedge\cdot}),\Gamma(X_{t\wedge\cdot}))$ for fixed continuous $Z,\Gamma$ of linear growth. " $V\in C_b^{1,1,1}(\Theta)$ " in Theorems 4.6 and 4.11 is replaced by the larger class it is used through (Remark 4.3(i)): data continuous on $\Theta$ lying in $C_b^{1,1,1}([t_1,t_2]\times\mathcal P_L(t_1,\mu))$ for all $t_1<t_2$ , $L$ , $\mu$ , so those statements are at least as strong as printed.

The definitions cannot be satisfied vacuously: every test set requires a witness law in $\mathcal P_L(t,\mu)$ , the class $C_b^{1,1,1}$ contains the constants (checked in Lean), and a viscosity solution uses one $L$ for both halves. The semi-jets range only over $\mathcal F_t$ -measurable continuous arguments of linear growth, as printed.

Contributions are welcome at every level: the moment bound (4.1) and Lemma 4.1 need tightness and uniform-integrability results for semimartingale laws on path space that Mathlib does not have; Theorems 4.7 and 4.9 are self-contained manipulations of the definitions; Theorems 4.6 and 4.11 and Proposition 4.12 need the compactness lemma and the Itô identity of test functions.

Selected references

C. Wu, J. Zhang, Viscosity solutions to parabolic master equations and McKean–Vlasov SDEs with closed-loop controls, Ann. Appl. Probab. 30(2) (2020) 936–986. https://doi.org/10.1214/19-AAP1521
I. Ekren, C. Keller, N. Touzi, J. Zhang, On viscosity solutions of path dependent PDEs, Ann. Probab. 42(1) (2014) 204–236. https://doi.org/10.1214/12-AOP788
P. Cardaliaguet, F. Delarue, J.-M. Lasry, P.-L. Lions, The Master Equation and the Convergence Problem in Mean Field Games, Annals of Mathematics Studies 201, Princeton University Press, 2019. https://doi.org/10.2307/j.ctvckq7qf
R. Carmona, F. Delarue, Probabilistic Theory of Mean Field Games with Applications I, Springer, 2018. https://doi.org/10.1007/978-3-319-58920-6
W. A. Zheng, Tightness results for laws of diffusion processes application to stochastic mechanics, Ann. Inst. H. Poincaré Probab. Statist. 21(2) (1985) 103–124. http://www.numdam.org/item/AIHPB_1985__21_2_103_0/

15 thms1 active userReviewed

Algorithmic Game Theory Dynamic Programming Probability+1·Captain: mikedeng1

Approximate Markov-Nash Equilibria for Discrete-Time Risk-Sensitive Mean-Field Games 2: The Mean-Field Equilibrium Policy Is an ε-Markov-Nash Equilibrium of Every Large Enough N-Agent GameResearch Paper

Motivation

Games with many interacting agents, such as traffic participants, users of a shared communication channel or firms in a market, are rarely solvable exactly: a Nash equilibrium of an $N$ -player stochastic game requires each agent to track the whole population, and its computation grows with $N$ . Mean-field game theory replaces the population by its limiting distribution. A single representative agent faces a deterministic flow of state distributions, and consistency requires that this flow is the one the agent's own optimal policy generates. The equilibrium of this limit problem is then used as an approximate equilibrium of the finite game, with each agent acting only on its own state.

Most of this theory concerns risk-neutral agents, who minimize an expected cost. Saldi, Başar and Raginsky (arXiv:1808.03929; Math. Oper. Res. 2020) treat discrete-time agents with an exponential utility of the discounted cost, the classical risk-sensitive criterion that penalizes the variance of the cost as well as its mean. The paper proves two results: a mean-field equilibrium exists (Theorem 1, the first mission of this series), and the equilibrium policy is an approximate Nash equilibrium of every large enough finite game (Theorem 3, this mission). The risk-neutral counterpart is Saldi, Başar and Raginsky, SIAM J. Control Optim. 2018 (arXiv:1612.07878).

Setting

States lie in a Polish metric space $\mathsf X$ , actions in a compact Polish space $\mathsf A$ , and $\mathcal P(\mathsf X)$ is the set of Borel probability measures with the weak topology. The model consists of a transition kernel $p(\cdot\mid x,a,\mu)$ , a one-stage cost $c(x,a,\mu)\ge0$ , an initial law $\mu_0$ , a discount factor $\beta\in(0,1)$ and a risk factor $\lambda>0$ .

In the $N$ -agent game, the states $x^N_i(0)$ are i.i.d. $\mu_0$ . At each time $t$ , agent $i$ draws $a^N_i(t)\sim\pi^i_t(\cdot\mid x^N_i(t))$ from its Markov policy $\pi^i$ , and the next states are drawn independently from $p(\cdot\mid x^N_i(t),a^N_i(t),e^{(N)}_t)$ , where $e^{(N)}_t=\frac1N\sum_{j}\delta_{x^N_j(t)}$ is the empirical distribution of the states. Agent $i$ 's cost is

J^{(N)}_i(\boldsymbol\pi^{(N)})=E^{\boldsymbol\pi^{(N)}}\Big[e^{\lambda\sum_{t=0}^\infty\beta^tc(x^N_i(t),a^N_i(t),e^{(N)}_t)}\Big].

A profile is an $\varepsilon$ -Markov-Nash equilibrium if no agent can lower its $J^{(N)}_i$ by more than $\varepsilon$ by switching to another Markov policy.

In the mean-field game, one agent faces a flow $\boldsymbol\mu=(\mu_t)$ : $x(t+1)\sim p(\cdot\mid x(t),a(t),\mu_t)$ , with cost $J_{\boldsymbol\mu}(\pi)=E^\pi[e^{\lambda\sum_t\beta^tc(x(t),a(t),\mu_t)}]$ . A mean-field equilibrium is a pair $(\pi,\boldsymbol\mu)$ in which $\pi$ minimizes $J_{\boldsymbol\mu}$ and $\boldsymbol\mu=\Lambda(\pi)$ is the flow of state laws that $\pi$ generates.

The hypotheses are Assumption 1 (bounded continuous $c$ with $|c|\le K$ , weakly continuous $p$ , compact $\mathsf A$ , and a moment function $w$ with $\int w\,dp\le\alpha w$ and $\int w\,d\mu_0<\infty$ ) and Assumption 2. Part (a) of Assumption 2 asks that the moduli

\omega_p(r)=\sup_{x,a}\sup_{d_{BL}(\mu,\nu)\le r}\|p(\cdot\mid x,a,\mu)-p(\cdot\mid x,a,\nu)\|_{TV},\qquad\omega_c(r)=\sup_{x,a}\sup_{d_{BL}(\mu,\nu)\le r}|c(x,a,\mu)-c(x,a,\nu)|

tend to $0$ , where $d_{BL}$ is the bounded-Lipschitz metric. Part (b) asks that the equilibrium policy $\pi$ be weakly continuous in the state.

Formalization targets

Goal: Theorem 3 (p. 23)

For every $\varepsilon>0$ there is $N(\varepsilon)$ such that, for every $N\ge N(\varepsilon)$ , the profile $(\pi,\dots,\pi)$ is an $\varepsilon$ -Markov-Nash equilibrium:

J^{(N)}_i(\pi,\dots,\pi)\le\inf_{\sigma\in\mathsf M}J^{(N)}_i(\pi,\dots,\sigma,\dots,\pi)+\varepsilon\qquad\text{for all }i .

The statement fixes no rate. It is the paper's main approximation result.

Milestones

The milestones follow the paper's proof. The first seven work in an augmented model, whose state $s=(x,c)$ carries the accumulated discounted cost, so that the exponential criterion becomes a terminal cost $e^{\lambda c(n+1)}$ . They are: Proposition 6 (the augmented model has the same finite-horizon costs); Lemma 5 (the augmented flow $\Delta_{t+1}=\Delta_tP^\pi_{t,\Delta_t}$ ); Proposition 7 (propagation of chaos, $\mathcal L(\Delta^{(N)}_t)\to\delta_{\Delta_t}$ ); Proposition 8 (convergence of the augmented cost); Proposition 9 (propagation of chaos with one deviating agent); Proposition 10 (the deviating agent's state law); Proposition 11 (the deviating agent's augmented cost). The last three are stated in the original model: Theorem 4 (the finite-horizon limits (14)–(15)), Corollary 1 (the infinite-horizon comparison), and the first display of the proof of Theorem 3 (deviations may be restricted to weakly continuous policies).

Significance

Theorem 3 justifies the use of a mean-field equilibrium as a decentralized policy in risk-sensitive games with many players. The equilibrium is computed once, from a single-agent problem, and each agent uses only its own state, yet no agent of a large enough population gains more than $\varepsilon$ by deviating. The result extends the risk-neutral approximation theorem to the multiplicative criterion. Because the exponential cost does not decompose over time, the risk-neutral argument cannot be applied directly: the proof first passes through the augmented model and a finite-horizon truncation.

The result is proved in the paper; none of it is formalized. The mission formalizes the statement and the proof's intermediate results. That requires the $N$ -agent law, a product of $N$ kernels driven by the empirical measure, built from Mathlib's Ionescu-Tulcea construction, and propagation of chaos for an interacting Markov chain on a Polish space. Alternative proofs of any milestone are welcome, as are quantitative versions of the limits.

Difficulty

The cost is the expectation of a product of one-stage factors, not a sum, so the convergence of the empirical measure gives no direct control of it. The paper therefore enlarges the state with the accumulated cost, and the finite-horizon limits must then be transferred back to the infinite horizon through a uniform tail bound. The coupling between agents runs through the empirical measure, which enters both the transition and the cost. Propagation of chaos (Proposition 7) is an induction over time that needs continuity of $p$ and $c$ in the measure argument uniformly in $(x,a)$ (Assumption 2-(a)) and a conditional variance bound. The deviating agent is not exchangeable with the others: its state law must be compared with that of a mean-field chain under its own policy (Proposition 10), uniformly over arbitrary sequences of deviations. Finally, a best response may be only measurable. The reduction to weakly continuous deviations, which the paper takes from its risk-neutral predecessor, is needed before any weak-convergence argument applies.

Formalization scope

Lean namespace RiskSensMFG.Nash. The definitions are in four files: the model, policies, the single-agent law and the flow (Model); the mean-field equilibrium, $d_{BL}$ , total variation and Assumption 2-(a) (Equilibrium); the $N$ -agent game (Game); and the augmented model (Augmented). Conventions:

$\mathsf X$ is a complete separable metric space with its Borel $\sigma$ -field, and $\mathsf A$ is a compact Polish space. $\mathcal P(\mathsf X)$ is Mathlib's ProbabilityMeasure with the weak topology and its Borel $\sigma$ -field (not the Giry one), and $p$ is a Markov Kernel. The standing assumptions $\beta\in(0,1)$ , $\lambda>0$ and $c\ge0$ measurable are a predicate Model.Standing. Assumption 1 is stated in full, including the moment function, although the proof of Theorem 3 does not use parts (d)–(e).
Time is 0-based. Agents are indexed by Fin N, and the paper's Agent 1 is index 0; limits in $N$ are taken along $N+1$ so that Agent 1 exists. The empirical measure of the empty configuration is set to $\mu_0$ and enters no statement.
The equilibrium's optimality is required against Markov policies only, which is a weaker hypothesis than Definition 3's optimality over all policies, so the goal is at least as strong as printed. The $\varepsilon$ of Definition 2 is on the scale of $J=E[e^{\lambda\sum\beta^tc}]$ . Equilibrium and optimality are stated in "for every deviation" form, with no infimum over a type.
Assumption 2-(a) and the modulus $\omega_g$ of Proposition 10 are written as $\varepsilon$ – $\delta$ statements, which is equivalent to " $\omega(r)\to0$ " because the moduli are nondecreasing. Total variation is $\sup_{|g|\le1}|\int g\,d\mu-\int g\,d\nu|$ .
The augmented cost coordinate is the discounted sum $\sum_{k<t}\beta^kc(\cdot)$ ; the page prints it without $\beta^k$ , which contradicts $P_t$ . The coordinate lies in $\mathbb R$ rather than $[0,L]$ , because $\mathsf X\times[0,L]$ is not invariant under $P_t$ , and the terminal cost is $e^{\lambda\max(0,\min(c,L))}$ , which equals $e^{\lambda c}$ on reachable states. Corollary 1's printed " $\lim\ge$ " (the limit is not shown to exist) is stated as three limit and eventual-inequality claims.

No hypothesis is vacuous: a sorry-free check exhibits a model satisfying the standing assumptions, Assumptions 1 and 2 and the equilibrium condition simultaneously, with $J^{(N)}_i\ge1$ . This rules out the trivial reading in which a non-integrable integrand makes every cost $0$ and every profile an $\varepsilon$ -equilibrium. Theorem 1 (existence of the equilibrium) is the other mission of the series; here the equilibrium is a hypothesis.

Selected references

N. Saldi, T. Başar, M. Raginsky, Discrete-time Risk-sensitive Mean-field Games, arXiv:1808.03929v2, 2018; published as Approximate Markov-Nash Equilibria for Discrete-Time Risk-Sensitive Mean-Field Games, Math. Oper. Res. 45(4), 2020. https://arxiv.org/abs/1808.03929, https://doi.org/10.1287/moor.2019.1044
N. Saldi, T. Başar, M. Raginsky, Markov–Nash Equilibria in Mean-Field Games with Discounted Cost, SIAM J. Control Optim. 56(6), 2018. https://arxiv.org/abs/1612.07878
N. Bäuerle, U. Rieder, More Risk-Sensitive Markov Decision Processes, Math. Oper. Res. 39(1), 2014. https://doi.org/10.1287/moor.2013.0601
O. Hernández-Lerma, J. B. Lasserre, Discrete-Time Markov Control Processes: Basic Optimality Criteria, Springer, 1996. https://doi.org/10.1007/978-1-4612-0729-0
R. M. Dudley, Real Analysis and Probability, Cambridge University Press, 2002 (§11.3, the bounded-Lipschitz metric). https://doi.org/10.1017/CBO9780511755347

16 thms1 active userReviewed

Completed

Actuarial Science Probability·Captain: WillR

Actuarial Mathematics XXIII: Countable-Lifetime Hattendorff LimitTextbook

Actuarial Mathematics XXIII: Countable-Lifetime Hattendorff Limit

Mathematical source and original extension

Elias S. W. Shiu and Xiaoyi Xiong (2021), An elementary derivation of Hattendorff's theorem, European Actuarial Journal 11, 319–323, https://doi.org/10.1007/s13385-020-00256-9. In that paper equation (1) defines the fully discrete insurer's complete-life loss; equation (2) gives the Hattendorff variance formula, and equations (3)–(5) connect annual reserve recursion to the net amount at risk by summation by parts.

The present mission proposes an original countable-outcome and L²-convergence formalisation of that discrete formula. It is not asserted that the authors stated this exact Lean theorem, and it does not inherit proofs from the earlier finite-scenario missions.

Unbounded lifetime and conditional mortality

Let $K\in\mathbb N$ be the realised curtate lifetime, the number of full years remaining until the year of death. Its possible values are not uniformly bounded. Set $w_k=\Pr(K=k)$ , where $w_k\ge0$ and $\sum_{k=0}^{\infty}w_k=1$ . Assume the survival tail is positive in every year:

S_t=\sum_{k\ge t}w_k>0,\qquad q_t=\frac{w_t}{S_t},\qquad p_t=\frac{S_{t+1}}{S_t}=1-q_t.

These are unconditional death masses $w_t$ and conditional mortality and survival rates $q_t,p_t$ . Some individual $w_t$ may be zero. The outcome space is genuinely countable; a finite Fintype of realised death years would force a bounded support and undermine the claimed infinite-horizon extension.

Mortality surprises and reserve losses

The annual mortality martingale difference is defined pathwise by

I_t(k)=\mathbf1_{\{k=t\}}-q_t\mathbf1_{\{k\ge t\}}.

For $t<k$ , $I_t(k)=-q_t$ ; at death $t=k$ , $I_t(k)=1-q_t$ ; and after death $t>k$ , it is zero. Let the discounted net amount at risk for the payment at year-end $t+1$ be $\rho_t=v^{t+1}(b_{t+1}-V_{t+1})$ . This matches Shiu–Xiong's year-end death-benefit timing. The truncated centred reserve loss and the pathwise complete-life centred loss are

Z_n(k)=\sum_{t=0}^{n-1}\rho_tI_t(k),\qquad Z_\infty(k)=Z_{k+1}(k).

The complete-life variable is well-defined on each realised finite $k$ and $Z_n(k)=Z_\infty(k)$ whenever $n>k$ . These definitions only model the centred innovation component. A separate cashflow reserve-recursion bridge, as in earlier missions, is needed to identify a given insurer contract loss $L$ with $V_0+Z_\infty$ ; this mission does not silently assert that for arbitrary premium sequences.

Supporting results and convergence condition

The discrete expectations are weighted countable sums. Show, under summability and positive in-force mass,

\mathbb E[I_t]=0,\quad \mathbb E[I_i I_j]=0\;(i\ne j),\quad \mathbb E[I_t^2]=w_tp_t.

Using finite sums and cross-year orthogonality first gives

\mathbb E[Z_n^2]=\sum_{t=0}^{n-1}\rho_t^2w_tp_t.

The capstone introduces the mathematically substantive L² risk condition

\sum_{t=0}^{\infty}\rho_t^2w_tp_t<\infty.

This implies that the sequence of truncated centred losses is Cauchy in the probability-weighted L² space; its limit equals the pathwise stabilised $Z_\infty$ . Hence

\boxed{\mathbb E[Z_\infty]=0,\qquad \operatorname{Var}(Z_\infty)=\mathbb E[Z_\infty^2] =\sum_{t=0}^{\infty}\rho_t^2w_tp_t.}

The capstone explicitly assumes nonnegative weights, unit total mass, positive survival tails, countable weight summability and risk-variance summability. The formal statement must not be weakened to merely a pointwise convergence or an unjustified interchange of infinite sums.

Exact-rational validation and boundaries

A geometric law with $q=\frac14$ , $p=\frac34$ , $w_k=qp^k$ and $\rho_t=2$ gives

Z_\infty(k)=2(p-qk),\qquad \mathbb E[Z_\infty]=0,\quad\operatorname{Var}(Z_\infty)=3.

Its finite-year variance is $3(1-p^n)$ . The repository includes exact-rational tests for 13 horizons. The model allows an individually zero death mass but requires positive tails. Every scenario terminates in some finite year; adding a $K=\infty$ outcome with positive weight would require a separate transversality condition and is not part of this mission.

Prove2Me proof structure

The mission supplies four mathematical definitions, eleven supporting milestone theorems and one combined capstone theorem. Prove the indicator identities, the countable weighted first and second moments, finite orthogonality and finite allocation, and finally the L² passage to the unbounded lifetime. The target Lean namespace is `ActuarialValuation` in the pinned Mathlib environment. Finite-year results from earlier actuarial missions are background, not automatic countable-measure proof imports. None of the present open theorem statements is an accepted proof.

21 thms1 active userReviewed

Completed

Actuarial Science Probability·Captain: WillR

Actuarial Mathematics XVI: Discrete Mortality Innovations and Hattendorff OrthogonalityTextbook

Motivation: from actuarial reserves to Hattendorff's theorem

A prospective insurance reserve is the conditional expected amount needed to fund the remaining liabilities of an in-force policy. Annual realised claims differ from their conditional expectations, and the variation in total discounted insurer loss can be allocated to these unexpected annual outcomes. Hattendorff's theorem expresses that allocation as a sum of year-specific variance contributions. The fully discrete case contains an important factor: the conditional probability of surviving the policy year.

Shiu and Xiong's article An elementary derivation of Hattendorff's theorem [1] gives a direct discrete derivation. With curtate lifetime $K$ , annual death benefits $b_{j+1}$ paid at time $j+1$ , premiums $\pi_j$ paid at time $j$ , discount factor $v$ and prospective reserve $V_{j+1}$ , their formulas include

L=v^{K+1}b_{K+1}-\sum_{j=0}^{K}v^j\pi_j \qquad\text{and}\qquad \rho_j=v^{j+1}(b_{j+1}-V_{j+1}).

In particular, the variance identity they derive has a mortality-year survival factor,

\operatorname{Var}(L)=\mathbb E\!\left[\rho_K^2p_{x+K}\right].

This mission establishes the finite-scenario mortality-innovation component of that result. It derives the orthogonality of annual death surprises rather than assuming it. It does not yet identify their weighted sum with the full insurance loss $L-V_0$ ; that requires the separate time-dependent reserve recursion and summation-by-parts identities in [1, equation (3)]. Those insurance cashflow bridge obligations are explicitly reserved for the next mathematical stage.

Finite lifetime model

Let $\Omega$ be a finite scenario space, $w_\omega\ge0$ its weights and $K:\Omega\to\mathbb N$ a curtate future lifetime, where $K=j$ means death during year $j$ , at the end of which the death benefit is payable.

For policy duration $t$ , define the in-force probability mass and the death-year mass:

S_t=\sum_{\omega\in\Omega}w_\omega\mathbf1_{\{K(\omega)\ge t\}}, \qquad D_t=\sum_{\omega\in\Omega}w_\omega\mathbf1_{\{K(\omega)=t\}}.

For probabilistic interpretation assume in addition $\sum_\omega w_\omega=1$ . The exact algebraic statements do not generally require weight normalisation, though they explicitly require nonnegative weights for probability inequalities.

The disjoint identity

\{K\ge t\}=\{K=t\}\mathbin{\dot\cup}\{K\ge t+1\}

gives $S_t=D_t+S_{t+1}$ . If $S_t>0$ , the conditional one-year death and survival probabilities are

q_t=\frac{D_t}{S_t},\qquad p_t=\frac{S_{t+1}}{S_t},\qquad q_t+p_t=1.

Division by $S_t=0$ is totalised as a Lean real expression but is not interpreted as conditioning on an impossible event. All substantive annual-innovation results impose positive in-force mass for the years used.

A centred innovation for every policy year

For each outcome and policy year define the mortality innovation

I_t(\omega)= \mathbf1_{\{K(\omega)=t\}} -q_t\mathbf1_{\{K(\omega)\ge t\}}.

It equals $1-q_t$ for death in year $t$ , equals $-q_t$ for an individual surviving that year, and equals zero after death. Under $S_t>0$ ,

\mathbb E_w[I_t]=D_t-q_tS_t=0.

The orthogonality is more than a generic assumption. For $i<j$ , if $I_j\ne0$ then the policy is still in force at $j$ , so the preceding year $i$ must have been survived and $I_i=-q_i$ . If $I_j=0$ , the product is also zero. Thus, pointwise,

I_iI_j=-q_iI_j,\qquad i<j.

Taking the weighted expectation and using the centring of $I_j$ gives

\mathbb E_w[I_iI_j]=0,\qquad i<j,\quad S_j>0.

These innovations can be uncorrelated despite being highly dependent events generated by the same curtate lifetime. They must not be claimed independent.

The one-year discrete second moment

By conditioning on the death-year and survival outcomes, the squared mortality surprise has expected value

\begin{aligned} \mathbb E_w[I_t^2] &=D_t(1-q_t)^2+S_{t+1}q_t^2\\ &=D_t\,p_t,\qquad S_t>0. \end{aligned}

The final conditional survival factor $p_t$ is characteristic of the fully discrete actuarial Hattendorff identity. It is not an arbitrary variance weight, and it cannot be dropped by borrowing a continuous-time formula.

For a finite horizon $n$ , let $\rho_t\in\mathbb R$ be any deterministic year-specific net-amount-at-risk coefficient. Define the discounted innovation portfolio

Z_n(\omega)=\sum_{0\le t<n}\rho_t I_t(\omega).

When $S_t>0$ for each $t<n$ , the annual zero-mean and cross-year orthogonality identities yield

\boxed{ \mathbb E_w[Z_n]=0,\qquad \operatorname{Var}_w(Z_n)= \sum_{0\le t<n}\rho_t^2D_tp_t. }

For nonnegative unit-sum weights this is the usual finite-scenario variance. The capstone couples the derived pairwise cross-year zero moments with the resulting finite-horizon variance formula. No reserve balance, actuarial premium equation or conditional L² filtration theorem is silently assumed.

Formal proof structure and scope

The formal graph contains seven definitions: survival and death masses, conditional death and survival rates, the mortality innovation, its finite discounted portfolio and a finite weighted variance. Supporting theorems establish event partitions, nonnegativity, $q_t+p_t=1$ , behaviour after death, innovation centring, a pointwise earlier/later product identity, orthogonality, the discrete second-moment formula, zero horizon and portfolio moments. The capstone packages zero covariance and the mortality-weighted variance allocation.

The variance theorem is valid for arbitrary deterministic coefficient sequence $\rho$ and any finite number of years with positive survival mass; it does not presume every life dies before that horizon. $n=0$ is covered by the empty sum. For standard actuarial application choose $\rho_t=v^{t+1}(b_{t+1}-V_{t+1})$ , as in [1]. A future bridge must show that this particular innovation portfolio equals the centred insurer loss under the correct reserve recursion and endpoint conventions.

The root theorem is therefore a genuine probabilistic predecessor, not an assertion that the entire traditional Hattendorff theorem has already been proved. The mission is proposed for formal proof: private remote statement elaboration and finite rational tests, if accepted, do not constitute public Prove2Me proof acceptance.

References

[1] Shiu, Elias S. W. and Xiong, Xiaoyi (2021), “An elementary derivation of Hattendorff's theorem”, European Actuarial Journal, 11, pp. 319–323, equations (1)–(3). This is the direct source for the fully discrete variance factor, net amount at risk and finite summation-by-parts strategy.

[2] Gerber, Hans U. (1997), Life Insurance Mathematics, third edition, Springer, Chapter 6, §6.7, Allocation of the Overall Loss to Policy Years. The reserve-change and annual-loss decomposition provides broader actuarial context.

[3] Gerber, Hans U., Leung, Bartholomew P. K. and Shiu, Elias S. W. (2003), “Indicator Function and Hattendorff Theorem”, North American Actuarial Journal, 7(1), pp. 38–47. Explains the central role of indicator functions and the relationship to uncorrelated martingale increments.

21 thms1 active userReviewed

Completed

Actuarial Science Probability·Captain: WillR

Actuarial Mathematics XVII: Finite-Horizon Markov Decision and Optimal Policy ValuationTextbook

Motivation: from one-step reinsurance decisions to an optimal policy

An insurer may adjust its reinsurance retention or other risk-management decision repeatedly, rather than optimising a single future year's payments. Current action choices affect both the immediate net reward and the state of the business next year, which changes the value of all later decisions. A finite-horizon Markov decision process makes this multi-year optimisation precise.

Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Chapter 4 [1], develops the finite-horizon Bellman equations and existence of optimal deterministic Markov policies for finite decision problems. Mission XV introduces a finite-action Bellman operator and excess-of-loss claim splitting, but is still under moderator review. This mission formalises the full finite-horizon backward recursion and optimal deterministic policy existence, without importing an unreviewed declaration.

The reinsurance motivation comes from Brachetta and Ceci's optimal excess-of-loss study [2]. Their original problem is a continuous-time stochastic-factor and HJB verification problem. The present mission is strictly a finite-state, finite-action, discrete-time precursor. Neither the stochastic-factor diffusion nor the jump-process verification theorem is asserted here.

Finite states, actions and one-year valuation

Let $S$ be a finite state type, and let $A$ be a finite nonempty set of admissible control actions. A state can encode a simplified surplus, rating, claims regime or any finite risk-class abstraction. At the beginning of a policy year the insurer is in state $s$ and selects an action $a$ .

Let $P(s,a,t)$ be the transition weight for next state $t$ , and $r(s,a)$ the immediate reward. The usual Markov model requires $P(s,a,t)\ge0$ and $\sum_tP(s,a,t)=1$ for every $s,a$ . The general algebraic definitions accept real matrices, while the economic probabilistic interpretation requires valid row-stochasticity.

If $U(t)$ is the continuation value in state $t$ , the return from action $a$ is

Q(s,a;U)=r(s,a)+v\sum_{t\in S}P(s,a,t)U(t),

where $v$ is a deterministic annual discount factor. The discount is applied to following-year continuation, not to the current reward. For policy interpretation $0\le v\le1$ is conventional, but finite-horizon algebra makes sense at other fixed real $v$ as well.

The one-year Bellman optimisation is

(TU)(s)=\max_{a\in A}Q(s,a;U).

The maximum is attained because $A$ is finite and nonempty. Both this attainment and the inequality $Q(s,a;U)\le(TU)(s)$ are explicit supporting theorem obligations.

Finite-horizon policy evaluation

Let $h(s)$ denote a terminal benefit or terminal value. A deterministic nonstationary Markov policy is a mapping

\pi:\mathbb N\times S\longrightarrow A.

Here $\pi_n(s)$ is the action chosen when $n+1$ decisions remain, so the index counts backwards towards the terminal time. This makes the recursion valid for a homogeneous one-step transition model without reversing calendar-time transitions.

For a fixed policy, recursively define

\begin{aligned} V^\pi_0(s)&=h(s),\\ V^\pi_{n+1}(s) &=r(s,\pi_n(s)) +v\sum_{t\in S}P(s,\pi_n(s),t)V^\pi_n(t). \end{aligned}

The policy is nonstationary because its choice at the same state may differ according to remaining time $n$ . It is Markov because the action depends only on current state and remaining horizon, not on the entire historical path. The mission does not introduce a path-space filtration or general history-dependent randomised policy, so the precise capstone compares deterministic nonstationary Markov policies.

Optimal backward induction

Define $V_n(s)$ by the finite Bellman recursion

\begin{aligned} V_0(s)&=h(s),\\ V_{n+1}(s)&= \max_{a\in A}\left[ r(s,a)+v\sum_{t\in S}P(s,a,t)V_n(t) \right]. \end{aligned}

Under $P(s,a,t)\ge0$ and $v\ge0$ , a larger continuation function cannot reduce the value of any action; taking a finite maximum preserves this monotonicity. That simple inequality allows induction on the remaining horizon to show

V^\pi_n(s)\le V_n(s) \qquad\text{for every deterministic Markov policy }\pi.

The second substantive step is existence of an attaining policy. Since $A$ is finite and nonempty, at each remaining horizon and each state there is at least one maximising action. Choosing such actions and combining them recursively gives a single nonstationary deterministic Markov policy $\pi^\star$ satisfying

V^{\pi^\star}_n(s)=V_n(s) \qquad\text{for all states }s.

The capstone combines the universal upper bound and existence of an attaining policy. This is genuinely more than a one-step maximum: it is an optimality result over an arbitrary finite number of sequential decisions.

A complete optimality result against all history-dependent randomised policies would need an additional equivalence argument showing no improvement from extra history or randomisation. Such an extension is well-known for suitable finite Markov models but is not silently claimed by this narrower Lean target.

Formal graph and limiting cases

Four proposed definitions encode the one-step action return, the finite Bellman maximum, policy evaluation and recursively optimal horizon value. Eleven supporting theorem targets establish zero-discount behaviour, action domination and attainment, monotonicity of action and Bellman values, zero-horizon and successor recursions, policy domination and existence of an attaining policy. The capstone packages the latter two results.

At $n=0$ there are no decisions and both values are precisely $h$ . At $v=0$ , any continuation is irrelevant to the one-step value. Nonnegative weights and discount are explicit hypotheses for monotonicity and policy domination, rather than false claims for signed matrix weights. The existence of an attaining maximiser in each finite action set does not itself require stochastic row-sum assumptions.

To obtain a reinsurance model from this graph, one must specify how each action corresponds to an admissible retention, how the retention changes reinsurance premiums and retained claim distributions, and how those assumptions determine the transition matrix $P$ and rewards $r$ . That specialised bridge is separate from the finite-horizon mathematical result.

All theorems are proposed Lean proof targets. Preliminary remote elaboration establishes statement well-formedness only if verified by the authoritative compiler. It does not constitute a completed proof or approval of the mission's mathematical design.

References

[1] Puterman, Martin L. (1994), Markov Decision Processes: Discrete Stochastic Dynamic Programming, Chapter 4, Finite-Horizon Markov Decision Processes, Wiley. This is the direct mathematical reference for finite-horizon Bellman recursions, backward induction and existence of optimal deterministic policies under finite-state/action assumptions.

[2] Brachetta, Matteo and Ceci, Claudia (2019), “Optimal Excess-of-Loss Reinsurance for Stochastic Factor Risk Models”, Risks 7(2), article 48. This motivates insurance retention as a controlled decision but uses a continuous-time stochastic-factor/HJB model not established by this mission.

[3] Schäffeler, Maximilian and Abdulaziz, Mohammad (2022), “Formally Verified Solution Methods for Markov Decision Processes”, computer-assisted formalisation of Bellman equations, value iteration and optimal policy existence in Isabelle/HOL. This is methodology context only; no proof code is imported into Lean from that project.

16 thms1 active userReviewed

Completed

Numerical Analysis Probability Random Matrix Theory·Captain: tc

Gaussian Random Matrices III: Extreme Singular Values and ConcentrationTextbook

Motivation

A tall $N\times n$ matrix with independent standard normal entries is, with high probability, a near-isometry: all its singular values lie in $[\sqrt N-\sqrt n,\ \sqrt N+\sqrt n]$ up to Gaussian fluctuations. This is Gordon's theorem together with Gaussian concentration (Vershynin 2012, Theorem 5.32 and Corollary 5.35), the non-asymptotic counterpart of the Bai–Yin law and the model result for the whole theory of non-asymptotic random matrices. In randomized numerical linear algebra the same two ingredients give the expected spectral norm of $S\Gamma T$ (Halko–Martinsson–Tropp 2011, Proposition 10.1 (10.2)), its second moment (Tropp–Webber 2023, Lemma B.1), and the lower tail of $\sigma_{\min}$ of a Gaussian sketch, which controls the inverse moments $\mathbb E\,\sigma_{\min}^{-2p}$ that appear in the analysis of sketching algorithms with rank truncation. None of these results is available in Mathlib; this mission proves them.

Setting

A standard Gaussian matrix $A\in\mathbb R^{N\times n}$ has independent $\mathcal N(0,1)$ entries; its law is $\gamma_{N,n}$ . Its extreme singular values are

s_{\min}(A)=\inf_{\|x\|_2=1}\|Ax\|_2,\qquad s_{\max}(A)=\sup_{\|x\|_2=1}\|Ax\|_2=\|A\|,

the infimum and supremum over the unit sphere of $\mathbb R^n$ ( $n\ge1$ ); $\|A\|$ is the spectral norm. For a wide matrix $G\in\mathbb R^{k\times t}$ , $k\le t$ , the usual $\sigma_{\min}(G)$ is $s_{\min}(G^{\mathsf T})$ . The Frobenius norm is $\|A\|_F=(\sum_{i,j}A_{ij}^2)^{1/2}$ ; a function $h$ on matrices is $L$ -Lipschitz if $|h(X)-h(Y)|\le L\|X-Y\|_F$ . A chi-square variable with $d$ degrees of freedom is $\chi_d^2=\sum_{i=1}^d g_i^2$ for independent standard normals $g_i$ . The letter $e$ denotes Euler's number.

Formalization targets

Goal — deviation of the extreme singular values (Vershynin, Corollary 5.35)

For every $t\ge0$ , with probability at least $1-2e^{-t^2/2}$ ,

\sqrt N-\sqrt n-t\ \le\ s_{\min}(A)\qquad\text{and}\qquad s_{\max}(A)\ \le\ \sqrt N+\sqrt n+t .

This is the goal because it is the statement users of Gaussian matrices quote: a quantitative near-isometry with explicit sub-Gaussian deviations. It follows from the expectation bounds (Gordon) and concentration, both of which are milestones.

Milestones

Gaussian concentration for Lipschitz functions of a Gaussian matrix: $\mathbb P\{h(G)\ge\mathbb E h(G)+Lt\}\le e^{-t^2/2}$ (HMT Proposition 10.3; Vershynin Proposition 5.34).
Gordon–Chevet bound. $\mathbb E\|S\Gamma T\|\le\|S\|\|T\|_F+\|S\|_F\|T\|$ (HMT Proposition 10.1 (10.2), A.2) and its second-moment form $(\mathbb E\|S\Gamma T\|^2)^{1/2}\le\|S\|\|T\|_F+\|S\|_F\|T\|$ (Tropp–Webber Lemma B.1).
Gordon's theorem. $\sqrt N-\sqrt n\le\mathbb E s_{\min}(A)\le\mathbb E s_{\max}(A)\le\sqrt N+\sqrt n$ (Vershynin Theorem 5.32).
One-sided tail of $s_{\min}$ . $\mathbb P\{s_{\min}(A)\le\sqrt N-\sqrt n-u\}\le e^{-u^2/2}$ for $u\ge0$ (Davidson–Szarek Theorem II.13; one-sided form of Vershynin Corollary 5.35).
Chi-square lower tail. $\mathbb P\{\chi_d^2\le u\}\le(eu/d)^{d/2}$ for $0\le u\le d$ (Dasgupta–Gupta Lemma 2.2).
Small-ball bound for $s_{\min}$ . $\mathbb P\{s_{\min}(A)\le s\}\le n\bigl(\frac{e\,ns^2}{N-n+1}\bigr)^{(N-n+1)/2}$ for $s\ge0$ , $ns^2\le N-n+1$ , from the invertibility-via-distance lemma of Rudelson–Vershynin (Lemma 3.5), rotational invariance and the chi-square lower tail.

Significance

The results. Gordon's theorem is sharp: $\mathbb E s_{\min}$ and $\mathbb E s_{\max}$ are pinned to within $O(1)$ of the Bai–Yin limits for every $N,n$ . Gaussian concentration upgrades it to tail bounds with the optimal sub-Gaussian rate, and the Chevet-type bound is the same mechanism for $S\Gamma T$ , where it yields the expected spectral error of the randomized SVD. The small-ball bound covers the other regime, $s\to0$ , with polynomial decay of the exact order $N-n+1$ ; together the two tails make every negative moment $\mathbb E s_{\min}(A)^{-2p}$ , $2p<N-n+1$ , finite and explicitly bounded, which is what the early-truncated analysis needs.

Formalizing them. Mathlib has the standard Gaussian measure on finite-dimensional inner product spaces but neither Gaussian concentration for Lipschitz functions, nor Slepian's or Gordon's comparison inequalities, nor any result on singular values of random matrices. These are foundational pieces of high-dimensional probability whose formalization would be reused far beyond this series.

Difficulty

The upper bound in Gordon's theorem is proved by Slepian's comparison lemma for the Gaussian process $(u,v)\mapsto\langle Au,v\rangle$ on $S^{n-1}\times S^{N-1}$ , and the lower bound by Gordon's minimax comparison inequality for $\max_v\min_u\langle Au,v\rangle$ ; both require a theory of Gaussian processes indexed by continuous parameter sets, or at least a discretization argument with careful limits. Gaussian concentration (Tsirelson–Ibragimov–Sudakov) is usually proved through the Gaussian logarithmic Sobolev inequality or the Ornstein–Uhlenbeck semigroup, with a smoothing step to pass from smooth to Lipschitz functions. Both are long developments with no Mathlib support. The elementary alternatives do not reach the stated constants: an $\varepsilon$ -net argument bounds $\mathbb E\|A\|$ by $C(\sqrt N+\sqrt n)$ with $C>1$ , and a union bound over rows for the small-ball estimate is exactly how the stated bound is obtained, but it needs the fact that the distance from a Gaussian vector to a fixed $(n-1)$ -dimensional subspace is a $\chi_{N-n+1}$ variable, which again rests on rotational invariance.

Formalization scope

Matrices are sampled from the product measure $\gamma_{N,n}$ on arrays. $s_{\min}$ is sMin, the real infimum over the unit sphere of $\mathbb R^n$ ; $n\ge1$ is assumed so the sphere is nonempty, and $N\ge n$ is not assumed for Gordon's theorem (for $N<n$ one has $s_{\min}=0$ and the lower bound is trivial, as in the source). $s_{\max}$ is Mathlib's $\ell_2$ operator norm. Expectation bounds are stated together with integrability of their integrands, so the Lean convention that non-integrable functions integrate to $0$ cannot trivialize them. Probabilities are measures in $[0,\infty]$ compared with $\operatorname{ofReal}$ of the real bound; the goal's lower bound $1-2e^{-t^2/2}$ uses truncated subtraction and is vacuous for $t\le\sqrt{2\log2}$ , exactly as in the source. Gaussian concentration is stated with $L>0$ and $t\ge0$ , which the sources leave implicit (for $L=0$ or $t<0$ the event has probability one). Results that the sketching literature states for wide $k\times t$ matrices are stated here for tall $N\times n$ matrices via $\sigma_{\min}(G)=s_{\min}(G^{\mathsf T})$ , with $(N,n)=(t,k)$ .

Welcome contributions: Gaussian concentration for Lipschitz functions on $\mathbb R^d$ (any proof), Slepian's and Gordon's inequalities, the $1$ -Lipschitz property of $s_{\min}$ and $s_{\max}$ , the chi-square Chernoff bounds, and the law of the distance from a Gaussian vector to a subspace.

Selected references

N. Halko, P.-G. Martinsson, J. A. Tropp, Finding structure with randomness: probabilistic algorithms for constructing approximate matrix decompositions, SIAM Review 53(2), 217–288, 2011. https://arxiv.org/abs/0909.4061
J. A. Tropp, R. J. Webber, Randomized algorithms for low-rank matrix approximation: design, analysis, and applications, 2023. https://arxiv.org/abs/2306.12418
R. Vershynin, Introduction to the non-asymptotic analysis of random matrices, in Compressed Sensing: Theory and Applications, Cambridge University Press, 2012. https://arxiv.org/abs/1011.3027
L. Isserlis, On a formula for the product-moment coefficient of any order of a normal frequency distribution in any number of variables, Biometrika 12, 134–139, 1918. https://doi.org/10.1093/biomet/12.1-2.134
S. Dasgupta, A. Gupta, An elementary proof of a theorem of Johnson and Lindenstrauss, Random Structures & Algorithms 22, 60–65, 2003. https://doi.org/10.1002/rsa.10073
M. Rudelson, R. Vershynin, The Littlewood–Offord problem and invertibility of random matrices, Advances in Mathematics 218, 600–633, 2008. https://arxiv.org/abs/math/0703503
Y. Chen, J. Dongarra, Condition numbers of Gaussian random matrices, SIAM J. Matrix Anal. Appl. 27(3), 603–620, 2005. https://doi.org/10.1137/040616413
A. Edelman, Eigenvalues and condition numbers of random matrices, SIAM J. Matrix Anal. Appl. 9(4), 543–560, 1988. https://doi.org/10.1137/0609045
Y. Gordon, Some inequalities for Gaussian processes and applications, Israel J. Math. 50, 265–289, 1985. https://doi.org/10.1007/BF02759761
K. R. Davidson, S. J. Szarek, Local operator theory, random matrices and Banach spaces, Handbook of the Geometry of Banach Spaces, Vol. 1, 317–366, 2001. https://doi.org/10.1016/S1874-5849(01)80010-3
M. Ledoux, The Concentration of Measure Phenomenon, AMS Mathematical Surveys and Monographs 89, 2001. https://doi.org/10.1090/surv/089

Shared definitions: the items of this mission import Definitions.Def_GaussianMatrix_basic, a draft of Mission I; submit that proposal first so the import resolves at compile time.

Series: I. Rotation Invariance and Moment Identities · II. Inverse Moments of the Pseudoinverse · III. Extreme Singular Values and Concentration. All three missions share the definition bundle GaussianMatrix_basic, published with Mission I, and the namespace GaussianMatrix.

8 thms1 active userReviewed

Completed

Numerical Analysis Probability Random Matrix Theory·Captain: tc

Gaussian Random Matrices I: Rotation Invariance and Moment IdentitiesTextbook

Motivation

Randomized algorithms for low-rank approximation — the randomized SVD of Halko, Martinsson and Tropp (HMT 2011), generalized Nyström, randomized subspace iteration, one-pass sketching (Tropp–Webber 2023) — multiply the input matrix by a random test matrix $\Omega$ with independent standard normal entries. Every error bound for these methods rests on a small number of facts about such standard Gaussian matrices: they are invariant under rotations, disjoint blocks of a rotated copy are independent, and the second and fourth moments of a linearly transformed Gaussian matrix are given by explicit formulas. These facts are classical, but none of them is available in Mathlib, so a Lean development of randomized numerical linear algebra currently has to carry every one of them as an explicit hypothesis of its main theorems. This mission removes those hypotheses.

Setting

For $p,m\in\mathbb N$ , a standard Gaussian matrix of size $p\times m$ is a random matrix $\Gamma\in\mathbb R^{p\times m}$ whose $pm$ entries are independent $\mathcal N(0,1)$ random variables. Its law, written $\gamma_{p,m}$ , is the product measure $\bigotimes_{i<p}\bigotimes_{j<m}\mathcal N(0,1)$ on real $p\times m$ arrays.

For a real matrix $A$ , $\|A\|_F^2=\sum_{i,j}A_{ij}^2$ is the squared Frobenius norm; $\operatorname{rank}A$ is the dimension of its column space. A matrix $V_1\in\mathbb R^{n\times k}$ has orthonormal columns when $V_1^{\mathsf T}V_1=I_k$ ; a square such matrix is orthogonal. For $t\ge1$ , a matrix $S\in\mathbb R^{n\times t}$ with independent $\mathcal N(0,1/t)$ entries is written $S=t^{-1/2}\Omega$ with $\Omega\sim\gamma_{n,t}$ , so that $SS^{\mathsf T}=\tfrac1t\Omega\Omega^{\mathsf T}$ is an unbiased sketch of the identity.

Formalization targets

Goal — Gaussian approximate matrix multiplication

For fixed $M\in\mathbb R^{a\times n}$ , $N\in\mathbb R^{b\times n}$ and $S\in\mathbb R^{n\times t}$ with independent $\mathcal N(0,1/t)$ entries,

\mathbb E\,\bigl\|MSS^{\mathsf T}N^{\mathsf T}-MN^{\mathsf T}\bigr\|_F^2=\frac{\|M\|_F^2\|N\|_F^2+\|MN^{\mathsf T}\|_F^2}{t}\le\frac2t\|M\|_F^2\|N\|_F^2 .

This is the exact mean-squared error of the sketched product $MSS^{\mathsf T}N^{\mathsf T}$ as an estimator of $MN^{\mathsf T}$ , a direct consequence of Isserlis' pairing formula for Gaussian fourth moments. It is the goal because it is the one fourth-moment computation the series needs and because every other identity in the mission is a step towards it.

Milestones

Rotational invariance. $U\Gamma V\sim\gamma_{p,m}$ for orthogonal $U\in\mathbb R^{p\times p}$ , $V\in\mathbb R^{m\times m}$ (HMT §10.1).
Blocks of a rotated Gaussian matrix. For $V_1\in\mathbb R^{n\times k}$ with orthonormal columns, $V_1^{\mathsf T}\Omega\sim\gamma_{k,t}$ ; for orthonormal $V_1,V_2$ with $V_1^{\mathsf T}V_2=0$ , the blocks $V_1^{\mathsf T}\Omega$ and $V_2^{\mathsf T}\Omega$ are independent (HMT, proof of Theorem 10.5).
Second moment. $\mathbb E\|S\Gamma T\|_F^2=\|S\|_F^2\|T\|_F^2$ (HMT Proposition 10.1 (10.1); Tropp–Webber Lemma B.1).
Fourth moment. $\mathbb E\|S\Gamma T\|_F^4=(\|S\|_F^2\|T\|_F^2)^2+2\|S^{\mathsf T}S\|_F^2\|TT^{\mathsf T}\|_F^2$ , the Isserlis formula for the Gaussian quadratic form $\operatorname{tr}(\Gamma^{\mathsf T}S^{\mathsf T}S\,\Gamma\,TT^{\mathsf T})$ ; its special case $\mathbb E\|\Omega\|_F^4=(kt)^2+2kt$ is the chi-square second moment (HMT Proposition A.8).
Full rank. $\operatorname{rank}\Gamma=\min\{p,m\}$ almost surely (HMT, proof of Theorem 10.5 and Proposition A.5).

Significance

The results. Rotational invariance and block independence are the mechanism behind every conditioning argument in randomized linear algebra: writing the right singular vectors of the input as $[V_1\ V_2]$ , the sketch splits into independent standard Gaussian blocks $\Omega_1=V_1^{\mathsf T}\Omega$ and $\Omega_2=V_2^{\mathsf T}\Omega$ , and one may condition on $\Omega_1$ while treating $\Omega_2$ as fresh. The second-moment identity then turns the deterministic range-finder bound $\|\Sigma_2\Omega_2\Omega_1^{\dagger}\|_F$ into $\|\Sigma_2\|_F^2\,\mathbb E\|\Omega_1^{\dagger}\|_F^2$ , and the approximate-multiplication identity gives the one-pass error terms. Almost-sure full rank is what makes $\Omega_1^{\dagger}$ a genuine pseudoinverse.

Formalizing them. Mathlib has the one-dimensional Gaussian measure, product measures, independence of coordinate projections, and (recently) the standard Gaussian measure on a finite-dimensional inner product space together with its invariance under linear isometries. None of the matrix-level statements above is in Mathlib. Once proved here they are reusable by every later mission in the series and by any formalization of randomized low-rank approximation, whose expectation-level inputs (e.g. $\mathbb E\|\Sigma_2\Omega_2\Omega_1^{\dagger}\|_F^2=\frac{k}{t-k-1}\|\Sigma_2\|_F^2$ ) follow from these milestones together with the inverse moments of Mission II.

Difficulty

Rotational invariance is not a computation with densities on $\mathbb R^{pm}$ that Mathlib supports out of the box: the clean route is through characteristic functions or through the basis-independence of the standard Gaussian on an inner product space, transported along the linear isometry $\Gamma\mapsto U\Gamma V$ of $\mathbb R^{p\times m}$ with the Frobenius inner product. Independence of the blocks requires identifying $[V_1\ V_2]^{\mathsf T}\Omega$ with a product measure and then projecting onto disjoint coordinate sets, with a completion of $[V_1\ V_2]$ to an orthogonal matrix when $k+r<n$ . The moment identities are finite computations, but the fourth-moment identity needs the Gaussian moments $\mathbb E g^4=3$ , $\mathbb E g^2=1$ organized through Isserlis' pairing formula over a four-fold sum of indices; the obvious entrywise expansion produces $O((pm)^4)$ terms that must be collapsed symbolically. Almost-sure full rank is the statement that the zero set of a nonzero polynomial ( $\det$ of a maximal square submatrix) is Lebesgue-null, which must be established for the product Gaussian measure.

Formalization scope

The sample space is the function type $\mathbb R^{p}\to\mathbb R^{m}\to\mathbb R$ with the product $\sigma$ -algebra; a sample is viewed as a matrix through the identity map $\mathrm{of}$ . Expectations are real Bochner integrals: for an identity with a nonzero right-hand side this forces integrability, and the integrands here are polynomials in Gaussian entries. Laws are stated as equalities of pushforward measures; independence is Mathlib's IndepFun. Dimensions may be $0$ ; all statements remain true in that case. The hypothesis $V_1^{\mathsf T}V_1=I_k$ silently forces $k\le n$ (vacuous otherwise), which matches the source.

The definition bundle GaussianMatrix_basic supplies the law $\gamma_{p,m}$ , $\|\cdot\|_F^2$ , $\|\cdot\|_F$ , the spectral norm (Mathlib's $\ell_2$ operator norm), the smallest singular value and the pseudoinverse $G^{\dagger}=G^{\mathsf T}(GG^{\mathsf T})^{-1}$ ; it is shared by the whole series. Welcome contributions: the Gaussian integration-by-parts and Isserlis lemmas for finite index sets, the identification of $\gamma_{p,m}$ with Mathlib's stdGaussian on the Frobenius inner product space, and the "polynomial zero sets are null" lemma for product measures.

Selected references

N. Halko, P.-G. Martinsson, J. A. Tropp, Finding structure with randomness: probabilistic algorithms for constructing approximate matrix decompositions, SIAM Review 53(2), 217–288, 2011. https://arxiv.org/abs/0909.4061
J. A. Tropp, R. J. Webber, Randomized algorithms for low-rank matrix approximation: design, analysis, and applications, 2023. https://arxiv.org/abs/2306.12418
R. Vershynin, Introduction to the non-asymptotic analysis of random matrices, in Compressed Sensing: Theory and Applications, Cambridge University Press, 2012. https://arxiv.org/abs/1011.3027
L. Isserlis, On a formula for the product-moment coefficient of any order of a normal frequency distribution in any number of variables, Biometrika 12, 134–139, 1918. https://doi.org/10.1093/biomet/12.1-2.134
S. Dasgupta, A. Gupta, An elementary proof of a theorem of Johnson and Lindenstrauss, Random Structures & Algorithms 22, 60–65, 2003. https://doi.org/10.1002/rsa.10073
M. Rudelson, R. Vershynin, The Littlewood–Offord problem and invertibility of random matrices, Advances in Mathematics 218, 600–633, 2008. https://arxiv.org/abs/math/0703503
Y. Chen, J. Dongarra, Condition numbers of Gaussian random matrices, SIAM J. Matrix Anal. Appl. 27(3), 603–620, 2005. https://doi.org/10.1137/040616413
A. Edelman, Eigenvalues and condition numbers of random matrices, SIAM J. Matrix Anal. Appl. 9(4), 543–560, 1988. https://doi.org/10.1137/0609045
Y. Gordon, Some inequalities for Gaussian processes and applications, Israel J. Math. 50, 265–289, 1985. https://doi.org/10.1007/BF02759761
K. R. Davidson, S. J. Szarek, Local operator theory, random matrices and Banach spaces, Handbook of the Geometry of Banach Spaces, Vol. 1, 317–366, 2001. https://doi.org/10.1016/S1874-5849(01)80010-3
M. Ledoux, The Concentration of Measure Phenomenon, AMS Mathematical Surveys and Monographs 89, 2001. https://doi.org/10.1090/surv/089

Series: I. Rotation Invariance and Moment Identities · II. Inverse Moments of the Pseudoinverse · III. Extreme Singular Values and Concentration. All three missions share the definition bundle GaussianMatrix_basic, published with Mission I, and the namespace GaussianMatrix.

8 thms1 active userReviewed

Dynamical Systems Probability Stochastic Systems·Captain: mikedeng1

Propagation of Chaos for Stochastic Spatially Structured Neuronal Networks with Delay driven by Jump Diffusions 1: The Spatially Structured McKean–Vlasov Delay Equation with Jumps Is Well-PosedResearch Paper

Motivation

Networks of conductance-based neurons, such as FitzHugh–Nagumo networks, are modelled by systems of stochastic differential equations in which each neuron interacts with the others through synapses, and the signal from one neuron reaches another only after a transmission delay. Biological neurons sit at positions in space, belong to a few distinct subpopulations, are driven by Brownian and Poisson (jump) noise, and vary from one to another; the last feature is modelled by a random disorder parameter. When the number of neurons tends to infinity, the state of a typical neuron is expected to follow a McKean–Vlasov equation: an SDE whose coefficients depend on the law of its own solution. S. Mehri, M. Scheutzow, W. Stannat and B. Z. Zangeneh (arXiv:1805.01654; Ann. Appl. Probab. 30 (2020), DOI 10.1214/19-AAP1499) prove that this limit equation is well-posed, with coefficients that are only monotone (one-sided Lipschitz), a general delay, jump noise, spatial structure and disorder all at once, and then prove propagation of chaos towards it.

Earlier work, as surveyed on p. 3 of the paper, covered parts of this setting: global Lipschitz coefficients (Quiñinao and Touboul 2015, and the paper's references [10, 11]), locally Lipschitz coefficients (Baladron, Fasoli, Faugeras and Touboul 2012, with the clarification of Bossy, Faugeras and Talay 2015 on the localization by hitting times; the same issue affects Touboul 2012), one-sided Lipschitz coefficients with diffusive noise (Luçon and Stannat 2014), and Lévy noise under global Lipschitz assumptions or gradient-type local dynamics (Andreis, Dai Pra and Fischer 2018). The paper constructs the solution by an Euler approximation, which, by the authors' account, had not been applied to McKean–Vlasov equations before.

Setting

Fix dimensions $d$ (state), $m$ , $n$ (noise), $k$ (space), a delay $\tau > 0$ and $P \ge 1$ subpopulations, located at pairwise disjoint measurable regions $\Gamma_1,\dots,\Gamma_P \subset \mathbb R^k$ whose union $\Gamma$ is bounded. A finite Borel measure $\mathcal R$ on $\Gamma$ with $\mathcal R(\Gamma_\alpha) = 1$ describes the spatial distribution of neurons. A disorder probability space $(\Omega',\mathcal F',\mathbb P')$ is fixed. On a filtered probability space $(\Omega,\mathcal F,(\mathcal F_t),\mathbb P)$ there are an $m$ -dimensional Brownian motion $W$ , $n$ -dimensional Brownian motions $B^1,\dots,B^P$ , Poisson random measures $N, N^1, \dots, N^P$ on $[0,\infty)\times U$ with intensity $dt\otimes\nu$ ( $\nu$ σ-finite; $\tilde N = N - dt\otimes\nu$ ), all independent, and initial paths $\hat z^\zeta \in L^2(\Omega;\text{Càdlàg}([-\tau,0];\mathbb R^d))$ .

For a path $y$ , write $y_{(t-\tau)^-:t^-}$ for the segment $u\mapsto y_{(t+u)^-}$ , $u\in[-\tau,0]$ . The equation is

dX^r_t = f(t,r,X^r_{t-},\omega')dt + g(\cdot)dW_t + \int_U h(\cdot,\xi)\tilde N(dt,d\xi) + \sum_{\alpha=1}^P\int_{\Gamma_\alpha}\tilde{\mathbb E}\big[\theta(t,r,r',X^r_{t-},\tilde X^{r'}_{(t-\tau)^-:t^-},\omega')\big]\mathcal R(dr')dt

+ \sum_{\alpha=1}^P\int_{\Gamma_\alpha}\tilde{\mathbb E}[\beta(\cdots)]\mathcal R(dr')dB^\alpha_t + \sum_{\alpha=1}^P\int_{\Gamma_\alpha}\int_U\tilde{\mathbb E}[\eta(\cdots,\xi)]\mathcal R(dr')\tilde N^\alpha(dt,d\xi),\qquad X^r_t = \hat z^\zeta_t\ (r\in\Gamma_\zeta,\ t\in[-\tau,0]), \tag{6}

where $\tilde X$ is an independent copy of the solution $X$ and $\tilde{\mathbb E}$ its expectation. The local dynamics $f, g, h$ satisfy the monotonicity and growth conditions (H1)–(H3) of Hypothesis 1.1 with locally integrable random rates $L_t(\omega')$ , $K_t(\omega')$ , $\tilde K_t(R,\omega')$ ; the synaptic coefficients $\theta, \beta, \eta$ are Lipschitz (H4) and of linear growth (H5) in $(x, y)$ , with rates $\bar L_t(\omega')$ , $\bar K_t(\omega')$ , the path variable measured through a probability measure $\lambda$ on $[-\tau,0]$ . In Lean, the model is the definition module NeuroMV.WellPosed.Setting: Space, Coeffs, Hyp1_1, Noise/IsNoise, IsStrongSol6, InClass and the constant C1 of (7).

Formalization targets

Goal: Theorem 1.5 (p. 7)

For every $T>0$ there is a process $X^r_t(\omega;\omega')$ , measurable in $(r,\omega',\omega)$ , such that for $\mathbb P'$ -almost every $\omega'$ , $X(\omega')$ is a strong solution of (6) on $[-\tau,T]$ ,

X(\omega') \in L^\infty\big([-\tau,T],dt;L^2(\Omega\times\Gamma,\mathbb P\otimes\mathcal R;\mathbb R^d)\big),

and every other strong solution $Y$ in that class satisfies $\int_\Gamma\mathbb E|X^r_t - Y^r_t|^2\mathcal R(dr) = 0$ for all $t\in[-\tau,T]$ .

Milestones

Theorem A.2 (p. 23): well-posedness of the general path-dependent delay SDE (20) with jumps under the monotonicity Hypothesis A.1, joint measurability in $(t,\omega,\omega')$ , the moment bound (22), and convergence of the Euler approximation (21).
The scheme (11) exists and is measurable (p. 9), and satisfies the uniform bound (12): $\sup_{t\in[-\tau,T]}\mathbb E|X^{n,r}_t|^2 \le C_1(T,\omega')$ .
Claims (iv) and (v) (p. 10): the schemes are Cauchy in probability uniformly on $[0,T]$ , and their limit solves (6).
Lemma 1.4 (p. 6): every solution in the class satisfies $\sup_{s\in[-\tau,t]}\mathbb E|X^r_s|^2 \le C_1(t,\omega')$ .
Uniqueness (pp. 16–17): two solutions in the class agree in $L^2(\Omega\times\Gamma)$ at every time.

Significance

Theorem 1.5 makes the infinite-population limit of the network well defined; the second main result of the paper, Theorem 1.8, proves that the network converges to it in $L^2$ . The theorem applies to coefficients that are only monotone in the state, which covers the cubic nonlinearity of FitzHugh–Nagumo neurons (Example 1.3), and to synaptic weights of conductance type driven by jump noise. Theorem A.2, proved in the appendix, is a well-posedness and Euler-convergence result for monotone stochastic delay equations with jumps and random coefficients, stated by the authors as new in this generality; it is reusable beyond this paper.

The results are proved in the paper; none of them has a machine-checked proof. The mission produces a Lean statement of the limit equation with the published Brownian and compensated Poisson integral relations, and invites formal proofs of the scheme estimates, the Cauchy property, the identification of the limit, the moment bound and uniqueness.

Difficulty

Under monotone coefficients there is no global contraction, so the Picard iteration that proves McKean–Vlasov well-posedness under Lipschitz assumptions does not apply. Localization by stopping times, the standard replacement for SDEs with monotone coefficients, does not localize the mean-field terms, which depend on the law of the solution at all positions; mishandling this step is the gap that Bossy, Faugeras and Talay pointed out in earlier work, and the acknowledgements (p. 30) record that the first version of this paper contained an unjustified application of the moment estimate of Lemma 1.4. A priori bounds must therefore be uniform in the approximation, and the limit of the mean-field stochastic integrals must be identified, with jumps and delay present. A second difficulty is measurability: the mean-field integrals require the solution to be measurable in the position $r'$ , and the theorem asserts measurability in $(r,\omega')$ .

Formalization scope

Representation. Positions are EuclideanSpace ℝ (Fin k), states EthierKurtz.SDEState d, matrices Matrix (Fin d) (Fin m) ℝ with the Hilbert–Schmidt norm; subpopulations are Fin P, 0-based. Processes are indexed by ℝ on $[-\tau,T]$ ; drivers by ℝ≥0. Path segments are functions ℝ → ℝ^d read on $[-\tau,0]$ with the product (cylinder) σ-algebra; the paper's sup-norm Borel σ-algebra is larger, so joint measurability of the coefficients for the cylinder σ-algebra is a mild added requirement.
Noise and integrals. Brownian integrals are the published EthierKurtz.HasBrownianItoIntegral, compensated jump integrals the published JacodTodorov10.LLN.HasCompInt, coordinatewise, with integrands cut off after $T$ . All Poisson measures are one JacodTodorov10.LLN.IsFPoisson measure on a product mark space, equivalent to independent measures $N, N^\alpha$ . Independence of the initial data from the drivers is encoded by $\mathcal F_0$ -measurability.
Mean field. The copy $\tilde X$ enters only through its law, so $\tilde{\mathbb E}$ is an expectation over $X$ itself; the mean-field integrands are required to be integrable on $\Gamma_\alpha\times\Omega$ . Expectations and suprema are in $[0,\infty]$ ; Bochner integrals carry integrability clauses.
Hypotheses. Hypothesis 1.1 (H1)–(H5) and the regularity of p. 2; (H6) is omitted from every item, because it involves the network data of (1) only and the proof never uses it. The class $L^\infty$ – $L^2$ is a bound for every $t$ rather than a.e. $t$ .
Every position. The goal requires the integral identity at every $r\in\Gamma$ , as (6) is posed; §2 proves it for $\mathcal R\times\mathbb P'$ -a.e. $(r,\omega')$ (p. 16), and on the remaining null set of positions (6) is an ordinary delay SDE solved by Theorem A.2 — a step the paper leaves implicit. Claim (v) keeps the $\mathcal R$ -a.e. reading.
No trivialization. The stochastic integrals are the published relations tied to $W$ , $B^\alpha$ , $N$ , $N^\alpha$ , not free processes; the mean-field terms are computed from the solution's own segments; the solution class is non-empty for zero coefficients (a sorry-free check accompanies the mission); and the scheme and limit are the paper's, not new processes with their own noise.
Not stated. Claims (i)–(iii) of §2 (the remainder estimate and the a priori bounds before the stopping time) are not separate items.
Welcome contributions. Itô's formula for jump diffusions in this encoding, Gronwall-type lemmas in $[0,\infty]$ , stability of the published integral relations under convergence in probability, and the monotone delay SDE theory of Appendix A are all reusable beyond this mission.

Selected references

S. Mehri, M. Scheutzow, W. Stannat, B. Z. Zangeneh, Propagation of Chaos for Stochastic Spatially Structured Neuronal Networks with Delay driven by Jump Diffusions, arXiv:1805.01654v3, 2019; Ann. Appl. Probab. 30, 2020. https://arxiv.org/abs/1805.01654, https://doi.org/10.1214/19-AAP1499
J. Baladron, D. Fasoli, O. Faugeras, J. Touboul, Mean-field description and propagation of chaos in networks of Hodgkin–Huxley and FitzHugh–Nagumo neurons, J. Math. Neurosci. 2:10, 2012.
M. Bossy, O. Faugeras, D. Talay, Clarification and complement to "Mean-field description and propagation of chaos in networks of Hodgkin–Huxley and FitzHugh–Nagumo neurons", J. Math. Neurosci. 5:19, 2015.
E. Luçon, W. Stannat, Mean field limit for disordered diffusions with singular interactions, Ann. Appl. Probab. 24(5):1946–1993, 2014.
C. Quiñinao, J. Touboul, Limits and dynamics of randomly connected neuronal networks, Acta Appl. Math. 136(1):167–192, 2015.
J. Touboul, Limits and dynamics of stochastic neuronal networks with random heterogeneous delays, J. Stat. Phys. 149(4):569–597, 2012.
L. Andreis, P. Dai Pra, M. Fischer, McKean–Vlasov limit for interacting systems with simultaneous jumps, Stoch. Anal. Appl., 2018.
W. Liu, M. Röckner, Stochastic Partial Differential Equations: An Introduction, Universitext, Springer, 2015.

The bibliographic data of the last seven entries are taken from the reference list of the paper (pp. 30–31).

17 thms1 active userReviewed

Algorithmic Game Theory Dynamic Programming Probability+1·Captain: mikedeng1

Approximate Markov-Nash Equilibria for Discrete-Time Risk-Sensitive Mean-Field Games 1: A Risk-Sensitive Mean-Field Game with Compact Actions and Weakly Continuous Kernel Has a Mean-Field EquilibriumResearch Paper

Motivation

Mean-field games describe large populations of identical agents who interact only through the distribution of their states. Each agent solves a stochastic control problem in which the population appears through a deterministic flow of distributions, and an equilibrium requires that this flow coincide with the distribution the agents generate themselves. The theory goes back to Huang, Malhamé and Caines (2006) and Lasry and Lions (2007) in continuous time. In discrete time, Saldi, Başar and Raginsky (SIAM J. Control Optim. 2018) proved existence of equilibria for risk-neutral agents with discounted costs on Polish state spaces.

Risk-neutral agents care only about expected cost. Many applications in engineering and finance call for agents that also penalize the variability of their cost. A standard way to model this is the exponential (risk-sensitive) criterion $E[\exp(\lambda\cdot\text{cost})]$ with risk factor $\lambda>0$ . Its theory for single-agent Markov decision processes goes back to Howard and Matheson (1972) and Jacobson (1973), and Bäuerle and Rieder (Math. Oper. Res. 2014) treat general utilities. Saldi, Başar and Raginsky (arXiv:1808.03929, Math. Oper. Res. 2020) carry the discrete-time mean-field program over to this criterion. This mission covers its first main result: existence of a mean-field equilibrium (Theorem 1).

Setting

The state space $\mathsf X$ and the action space $\mathsf A$ are Polish, and $\mathsf A$ is compact. $\mathcal P(E)$ denotes the probability measures on $E$ , with the topology of weak convergence and its Borel σ-field. The model consists of:

a stochastic kernel $p(\cdot\,|\,x,a,\mu)$ on $\mathsf X$ given $\mathsf X\times\mathsf A\times\mathcal P(\mathsf X)$ ;
a one-stage cost $c(x,a,\mu)\in[0,K]$ ;
an initial law $\mu_0$ , a discount factor $\beta\in(0,1)$ and a risk factor $\lambda>0$ .

A Markov policy is a sequence $\pi=(\pi_t)_{t\ge0}$ of kernels $\pi_t(da\,|\,x)$ . A policy in general is allowed to depend on the whole history $(x(0),a(0),\dots,x(t))$ . Given a measure flow $\mu=(\mu_t)_{t\ge0}\subset\mathcal P(\mathsf X)$ , a generic agent evolves as

x(0)\sim\mu_0,\qquad a(t)\sim\pi_t(\cdot\,|\,\text{history}),\qquad x(t+1)\sim p(\cdot\,|\,x(t),a(t),\mu_t),

and pays the risk-sensitive cost

J_\mu(\pi)=E^\pi\Big[\exp\Big(\lambda\sum_{t=0}^\infty\beta^tc(x(t),a(t),\mu_t)\Big)\Big].

For a Markov policy, $\Lambda(\pi)$ is the flow of state laws it generates: it starts at $\mu_0$ and satisfies $\mu_{t+1}(\cdot)=\int p(\cdot\,|\,x,a,\mu_t)\,\pi_t(da|x)\,\mu_t(dx)$ . A pair $(\pi,\mu)$ is a mean-field equilibrium if $\mu=\Lambda(\pi)$ and $\pi$ minimizes $J_\mu$ over all policies.

Assumption 1 asks for the following:

(a) $c$ is continuous with $\|c\|\le K$ ;
(b) $p$ is weakly continuous in $(x,a,\mu)$ ;
(c) $\mathsf A$ is compact;
(d) there are $\alpha\ge0$ and a continuous moment function $w\ge1$ (compact sets $K_n\uparrow\mathsf X$ with $\inf_{x\notin K_n}w(x)\to\infty$ ) with $\int w(y)\,p(dy|x,a,\mu)\le\alpha w(x)$ ;
(e) $\int w\,d\mu_0<\infty$ .

Formalization targets

Goal: Theorem 1 (p. 10)

Under Assumption 1 there are a Markov policy $\pi$ and a flow $\mu$ with

\mu=\Lambda(\pi)\qquad\text{and}\qquad J_\mu(\pi)=\inf_{\sigma\in\Pi}J_\mu(\sigma).

Milestones

In the paper's order of proof:

Proposition 1: Markov policies achieve the optimal value.
Lemmas 1–3: the finite- and infinite-horizon optimal value functions $J^n_k(\cdot,\lambda\beta^k)$ and $J_k(\cdot,\lambda\beta^k)$ of the nonhomogeneous MDP of a fixed flow are bounded and continuous. They satisfy the dynamic programming equation $T_kJ_{k+1}(\cdot,\lambda\beta^{k+1})=J_k(\cdot,\lambda\beta^k)$ , and

\big\|J^n_k(\cdot,\lambda\beta^k)-J_k(\cdot,\lambda\beta^k)\big\|\le\frac{\lambda K}{1-\beta}e^{\frac{\lambda\beta^kK}{1-\beta}}\beta^{n+1}.

Theorem 2: a Markov policy is optimal if and only if it almost surely selects minimizers in the dynamic programming equation.
Propositions 2–5 and Lemma 4: equilibria are fixed points of a set-valued map $\Gamma$ on state–action flows in $\Xi=\prod_t\{\nu:\nu_1(w)\le\alpha^tM\}$ ; the optimal value functions depend continuously on the flow; and the graph of $\Gamma$ is closed in $\Xi\times\Xi$ .

Significance

The result. Theorem 1 is what makes the second main result of the paper meaningful. That result, Theorem 3 and the second mission of this series, states that the equilibrium policy is an $\varepsilon$ -Markov–Nash equilibrium of every $N$ -agent game with $N$ large enough. Equilibria of finite risk-sensitive games with many agents are rarely computable, so a mean-field equilibrium gives an approximately optimal decentralized policy that ignores the other agents' states. Along the way, the paper proves results on nonhomogeneous risk-sensitive MDPs that it describes as "mostly absent and dispersed in the literature": uniform finite-to-infinite horizon bounds and a characterization of optimal Markov policies. These results are useful outside game theory.

Formalizing it. The result is proved on paper. No part of it, nor of the risk-neutral precursor, has a machine-checked proof. Formalization produces a verified theory of nonhomogeneous risk-sensitive MDPs on Polish spaces, a verified closed-graph argument for the mean-field map, and an exact record of the hypotheses. The paper omits or cites several steps: Proposition 1, Proposition 2, Lemma 2, the conditional optimality (8) and the nonemptiness and convexity of $\Gamma(\nu)$ . A formalization has to supply them.

Difficulty

The obvious route is Banach's fixed point theorem for the dynamic programming operator, as in risk-neutral discounted MDPs. It fails here: the cost is multiplicative, and the operator $T_k$ is not a contraction. Uniform convergence of value iteration has to come from the explicit tail bound of Lemma 3 instead.

The second obstacle is the fixed point itself. The natural map, from a flow to the flows of its optimal policies, is set-valued and lives on an infinite product of spaces of measures. Kakutani–Fan–Glicksberg applies only after three steps:

re-encoding the problem on state–action flows (the map $\Gamma=C\cap B$ );
proving compactness of $\Xi$ through the moment function (tightness);
proving that the graph of $\Gamma$ is closed (Proposition 4).

The last step requires the optimal value functions to vary continuously with the flow (Proposition 5) and a portmanteau argument for sets defined by optimality conditions. None of this machinery (the Kakutani–Fan–Glicksberg theorem in locally convex spaces, Prokhorov compactness via moment functions, continuous convergence) is in Mathlib in the required form.

Formalization scope

$\mathcal P(E)$ is a type synonym of Mathlib's ProbabilityMeasure E with the weak topology and its Borel σ-field. The kernel $p$ is a Mathlib Kernel on $\mathsf X\times\mathsf A\times\mathcal P(\mathsf X)$ . Policies are sequences of Markov kernels, and history-dependent policies take $(\mathsf X\times\mathsf A)^t\times\mathsf X$ as input. The law $P^\pi$ is built with the Ionescu–Tulcea kernel Kernel.trajMeasure, one coordinate $(x(t),a(t))$ per time step. Time is $0$ -based.

Standing hypotheses on every statement:

$\mathsf X$ and $\mathsf A$ are Polish and Borel;
$\mathsf A$ is compact and nonempty (used tacitly by the paper);
$\beta\in(0,1)$ , $\lambda>0$ , and $c\ge0$ is measurable;
Assumption 1.

For §4.2 the pair $(\alpha,w)$ defining $\Xi$ is an explicit argument. In §4.1, "policy" means Markov policy, as the paper states on p. 11. The conditional expectations "given $x(k)=x$ " are expectations for the chain started at time $k$ in $x$ . Lemma 1 is stated with $\zeta_{k,n}=\sum_{t=k}^n\beta^t$ , the quantity its proof uses; the page prints $\sum_{t=k}^n\beta^k$ .

The goal asks for a Markov equilibrium policy that is optimal against all history-dependent policies, at least as strong as Definition 3. Optimality is " $\le$ the cost of every policy", not an infimum, so it has no junk case. The cost is a genuine integral: with $c\ge0$ bounded, the integrand lies in $[1,e^{\lambda K/(1-\beta)}]$ , so no policy is trivially optimal. The moment-function predicate has no infimum, so compact $\mathsf X$ is admitted.

Contributions are welcome at every level:

risk-sensitive dynamic programming on Borel spaces (reusable for any MDP);
the Kakutani–Fan–Glicksberg theorem in locally convex spaces;
Prokhorov compactness from moment functions;
measurable selection and disintegration of state–action measures.

Selected references

N. Saldi, T. Başar, M. Raginsky, Discrete-time Risk-sensitive Mean-field Games, arXiv:1808.03929v2, 2018; published as Approximate Markov-Nash Equilibria for Discrete-Time Risk-Sensitive Mean-Field Games, Math. Oper. Res. 45(4), 2020. https://arxiv.org/abs/1808.03929
N. Saldi, T. Başar, M. Raginsky, Markov–Nash Equilibria in Mean-Field Games with Discounted Cost, SIAM J. Control Optim. 56(6), 2018. https://doi.org/10.1137/17M1112583
N. Bäuerle, U. Rieder, More Risk-Sensitive Markov Decision Processes, Math. Oper. Res. 39(1), 2014. https://doi.org/10.1287/moor.2013.0601
O. Hernández-Lerma, J. B. Lasserre, Discrete-Time Markov Control Processes: Basic Optimality Criteria, Springer, 1996. https://doi.org/10.1007/978-1-4612-0729-0
C. D. Aliprantis, K. C. Border, Infinite Dimensional Analysis, 3rd ed., Springer, 2006. https://doi.org/10.1007/3-540-29587-9

15 thms1 active userReviewed

Algorithmic Game Theory Graph Theory Probability+1·Captain: mikedeng1

A Case Study on Stochastic Games on Large Graphs in Mean Field and Sparse Regimes II: Large-Graph Limits of the Equilibrium Through the Laplacian Eigenvalue DistributionResearch Paper

Motivation

Mean field games describe large populations of agents who interact symmetrically: every agent sees the same average of all the others. Many populations interact instead along a network, where each agent responds only to its neighbours. Lacker and Soret (arXiv:2005.14102v2, 2021; Math. Oper. Res. 2022) study a linear-quadratic stochastic differential game on a finite graph that is simple enough to solve explicitly on every vertex-transitive graph, and then ask what happens to the equilibrium as the graph grows. The question is the network analogue of the classical convergence problem for mean field games: does the $n$ -player equilibrium have a limit, and does that limit depend on the graph only through a small amount of information?

The answer of the paper is that the limit is governed by the empirical eigenvalue distribution of the graph Laplacian. Dense graph sequences (degrees tending to infinity) all have the same limit, the mean field game; sparse ones (bounded degrees) have limits that depend on the graph, through its spectrum. This mission formalizes that large-graph limit theorem, Theorem 2.6 of the paper. Mission I of the series formalizes the explicit equilibrium on a fixed transitive graph (Theorem 2.5), on which this mission builds.

Setting

Let $G$ be a finite simple graph on vertex set $\{1,\dots,n\}$ with adjacency matrix $A_G$ and degree matrix $D_G$ . Its Laplacian is $L_G = D_G^{-1}A_G - I$ . $G$ is transitive if every vertex can be mapped to every other one by a graph automorphism; such a graph is regular, of degree $\delta(G)$ , and $L_G$ is then symmetric with eigenvalues $\lambda^G_1,\dots,\lambda^G_n\in[-2,0]$ . The empirical eigenvalue distribution is $\mu_G = \frac1n\sum_i\delta_{\lambda^G_i}$ .

Fix a horizon $T>0$ , a volatility $\sigma>0$ and a weight $c>0$ . Player $v$ controls the state

dX_v(t) = \alpha_v(t,\boldsymbol X(t))\,dt + \sigma\,dW_v(t),\qquad t\in[0,T],

driven by independent Brownian motions, with Markovian feedback controls $\alpha_v$ , and pays

J_v = \tfrac12\,\mathbb E\Big[\int_0^T|\alpha_v(t,\boldsymbol X(t))|^2dt + c\,\Big|X_v(T) - \tfrac1{\deg(v)}\sum_{u\sim v}X_u(T)\Big|^2\Big].

On a transitive graph without isolated vertices, Theorem 2.5 gives an explicit Nash equilibrium: with $Q_G(x) = \det(I - xL_G)^{1/n}$ and $f_G$ the solution of $f_G' = c\,Q_G'(f_G)$ , $f_G(0) = 0$ on $[0,T]$ , the feedback is $\alpha^G_i(t,\boldsymbol x) = -e_i^\top P_G(t)\boldsymbol x$ with $P_G(t) = -f_G'(T-t)L_G(I - f_G(T-t)L_G)^{-1}$ . The resulting equilibrium state process $\boldsymbol X^G$ is Gaussian, and the value is $\mathrm{Val}(G) = \frac1n\sum_v J_v$ .

For a probability measure $\mu$ define $Q_\mu(x) = \exp\int_{[-2,0]}\log(1-x\lambda)\,\mu(d\lambda)$ , so that $Q_{\mu_G} = Q_G$ .

Formalization targets

Goal: Theorem 2.6

Let $(G_n)$ be finite transitive graphs without isolated vertices, $|G_n|\to\infty$ , with $\boldsymbol X^{G_n}(0) = 0$ , and suppose $\mu_{G_n}\to\mu$ weakly for a probability measure $\mu$ . Then (1) the ODE $f_\mu' = c\,Q_\mu'(f_\mu)$ , $f_\mu(0) = 0$ has a unique solution on $[0,T]$ ; (2) for every vertex sequence $k_n$ and $t\in[0,T]$ ,

\mathrm{Law}\big(X^{G_n}_{k_n}(t)\big)\to\mathcal N\big(0,V_\mu(t)\big),\qquad V_\mu(t) = \sigma^2\int_0^t\int_{[-2,0]}\Big(\frac{1-\lambda f_\mu(T-t)}{1-\lambda f_\mu(T-s)}\Big)^2\mu(d\lambda)\,ds;

(3) the empirical measure $\frac1{|G_n|}\sum_i\delta_{X^{G_n}_i(t)}$ converges weakly in probability to $\mathcal N(0,V_\mu(t))$ ; (4)

\lim_{n\to\infty}\mathrm{Val}(G_n) = -\frac{\sigma^2}2\log\int_{[-2,0]}\frac{-\lambda}{1-\lambda f_\mu(T)}\,\mu(d\lambda).

Milestones

The milestones are the statements the paper's proof (§3, §6, §7.1) relies on: the stability of $f_\mu$ in $\mu$ (Proposition 3.2, last sentence); the finite-graph variance formula (2.7); monotonicity and concavity of $f_\mu$ (Proposition 3.3, first sentence); correlation decay (Proposition 2.12) for distinct vertices; the relation between degrees and the spectral limit (Lemma 7.1); the Gaussian Poincaré bound (7.3) and the concentration (7.1) of the empirical measure; and the spectral form (2.9) of the value.

Significance

Theorem 2.6 reduces the large-population behaviour of a network game to one spectral object. For complete graphs $\mu = \delta_{-1}$ and the limit is the mean field game; for sparse sequences such as cycles, tori, or random regular graphs, $\mu$ is a non-degenerate measure and the limiting variance and value differ from the mean field ones. The theorem thereby gives a quantitative criterion for when a mean field approximation of a network game is accurate, and it shows propagation of chaos in both regimes: in the dense case because interactions are weak, in the sparse case because typical players are far apart in the graph.

The result is proved in the paper; none of it has been machine-checked. A complete formalization requires a Lean account of Gaussian laws of linear SDEs with additive noise, of weak convergence of spectral measures of graph Laplacians, and of a Gaussian Poincaré inequality, none of which is currently in Mathlib in the needed form. Each of these is reusable well beyond this mission.

Difficulty

Parts (2) and (4) follow from the finite-graph formulas once $f_{G_n}\to f_\mu$ uniformly, but that convergence requires stability of a nonlinear ODE whose vector field is defined through the spectral measure, uniformly over a class of measures. The harder step is (3). Convergence of one player's law does not imply convergence of the empirical measure: the players are correlated, and on sparse graphs every player has a bounded number of strong neighbours, so the correlations do not vanish uniformly. Bounding them requires an estimate that decays in the graph distance and in the degree, and combining it with the growth of graph balls, which is controlled differently in the dense and in the sparse regime. The usual mean field route is closed: unless the graph is complete, the state vector is not exchangeable, so propagation-of-chaos arguments based on exchangeability do not apply.

Formalization scope

The Lean development lives in namespace GraphLQGame.Asymptotics.

Vertices $\{1,\dots,n\}$ are Fin n; a graph sequence is G : ∀ k, SimpleGraph (Fin (N k)) with $N_k\to\infty$ .
$L_G$ is the random-walk Laplacian above, not Mathlib's lapMatrix. $\mu_G$ is built from the real roots of the characteristic polynomial of $L_G$ , with multiplicity.
Weak convergence of measures on $\mathbb R$ is convergence of $\int h\,d\mu_k$ for every bounded continuous $h$ . Weak convergence in probability of the empirical measure is convergence in probability of $\int h\,dm^{G_n}(t)$ for every bounded continuous $h$ .
A state process is a pathwise strong solution of (2.1) on its own probability space, driven by a standard Brownian motion and adapted to its completed filtration. Statements about several graphs are statements about laws.
Costs are $[0,\infty]$ -valued lower integrals; the value is computed after asserting finiteness.
In $P_G$ , $f_G'(T-t)$ is written as its ODE value $c\,Q_G'(f_G(T-t))$ . ODE solutions are constrained on $[0,T]$ (or on $\mathbb R_+$ for Propositions 3.2 and 3.3), with uniqueness stated on that domain.
The Gaussian law $\mathcal N(0,V)$ is gaussianReal 0 V.toNNReal; $V_\mu(t)\ge0$ .

The goal quantifies over every solution $f_{G_n}$ , $f_\mu$ and every equilibrium state process, and also asserts that the graph ODE solutions and the state processes exist, so it cannot be discharged vacuously. Proposition 2.12 is stated for distinct vertices: as printed, (2.17) is also claimed for $u = v$ , where it fails on complete graphs of large degree; the off-diagonal case is the one the proof of Theorem 2.6 uses. Theorem 2.5 (mission I) is not restated here; a solver proves what is needed of it.

Contributions are welcome at every level: Gaussian laws of linear SDEs, spectral measures of graph matrices, ODE stability, a Gaussian Poincaré inequality, and the milestones themselves.

Selected references

D. Lacker, A. Soret, A case study on stochastic games on large graphs in mean field and sparse regimes, arXiv:2005.14102v2, 2021; published in Math. Oper. Res., 2022, https://doi.org/10.1287/moor.2021.1179. https://arxiv.org/abs/2005.14102
F. Chung, Spectral Graph Theory, CBMS Regional Conference Series in Mathematics 92, AMS, 1997. https://doi.org/10.1090/cbms/092
S. Boucheron, G. Lugosi, P. Massart, Concentration Inequalities: A Nonasymptotic Theory of Independence, Oxford University Press, 2013 (Theorem 3.20, Gaussian Poincaré inequality). https://doi.org/10.1093/acprof:oso/9780199535255.001.0001
R. Carmona, F. Delarue, Probabilistic Theory of Mean Field Games with Applications I, Springer, 2018. https://doi.org/10.1007/978-3-319-58920-6

17 thms1 active userReviewed

Algorithmic Game Theory Graph Theory Probability+1·Captain: mikedeng1

A Case Study on Stochastic Games on Large Graphs in Mean Field and Sparse Regimes III: The Mean Field Game Control Is an ε-Nash Equilibrium on Any Finite Graph, With ε_v ∝ deg(v)^(-1/2)Research Paper

Why mean field approximations on graphs need a threshold

Mean field games (MFGs) describe the limit of symmetric stochastic differential games as the number of players tends to infinity, when every player interacts with the empirical distribution of all the others. Their main practical use is the converse direction: an equilibrium of the limiting game supplies a simple, decentralized control that is an approximate Nash equilibrium of the game with finitely many players. For the complete graph, where everybody interacts with everybody, this is classical, with the standard rate $O(1/\sqrt n)$ (Carmona and Delarue, Probabilistic Theory of Mean Field Games, Vol. II, §6.1; Huang, Malhamé and Caines 2006, Theorem 12), as recalled on p. 10 of the paper.

Many interacting systems are not complete graphs: players see only their neighbours in a network. The question is then how dense the network must be for the mean field approximation to remain valid. Lacker and Soret (arXiv:2005.14102v2) answer it exactly for a linear-quadratic "flocking" game, where explicit computations are possible. This mission formalizes their Theorem 2.11, which applies to every finite graph, with no transitivity or regularity assumed.

Setting

Let $G$ be a finite simple graph on the vertex set $V=\{1,\dots,n\}$ ; $u\sim v$ means $u$ and $v$ are adjacent and $\deg_G(v)$ is the number of neighbours of $v$ . Fix a horizon $T>0$ , a volatility $\sigma>0$ and a cost weight $c>0$ . Each player $v\in V$ controls a real state $X_v$ through

dX_v(t)=\alpha_v(t,\boldsymbol X(t))\,dt+\sigma\,dW_v(t),\qquad t\in[0,T],

where $W_1,\dots,W_n$ are independent standard Brownian motions and $\boldsymbol X=(X_u)_{u\in V}$ . A Markovian control $\alpha_v\in\mathcal A_G$ is a Borel function of time and the full state $\boldsymbol X(t)\in\mathbb R^V$ , of linear growth. The cost of player $v$ under a profile $\boldsymbol\alpha=(\alpha_u)_{u\in V}$ is

J_v(\boldsymbol\alpha)=\frac12\,\mathbb E\Big[\int_0^T|\alpha_v(t,\boldsymbol X(t))|^2\,dt+c\,\Big|X_v(T)-\frac1{\deg_G(v)}\sum_{u\sim v}X_u(T)\Big|^2\Big],

and $\frac12\mathbb E[\int_0^T|\alpha_v|^2dt+c|X_v(T)|^2]$ for an isolated vertex: each player wants to end near the average of its neighbours at minimal quadratic effort. For a vector $\boldsymbol\varepsilon\in\mathbb R^V_+$ , a profile is a Markovian $\boldsymbol\varepsilon$ -Nash equilibrium if no player $v$ can lower its cost by more than $\varepsilon_v$ by switching unilaterally to another control $\beta\in\mathcal A_G$ , written $(\beta,\boldsymbol\alpha^{-v})$ .

The mean-field control is

\alpha^{\mathrm{MF}}(t,y)=\frac{-cy}{1+c(T-t)},\qquad \alpha^{\mathrm{MF}}_v(t,\boldsymbol x)=\alpha^{\mathrm{MF}}(t,x_v):

each player looks only at its own state, as if its neighbours' average were frozen at its mean.

Formalization targets

Goal: Theorem 2.11

Define $\epsilon^G_v=\sigma^2\frac{cT}{1+cT}\sqrt{\frac{cT(2+cT)}{\deg_G(v)}}$ if $\deg_G(v)\ge1$ and $\epsilon^G_v=0$ if $\deg_G(v)=0$ , and with the minimal degree $\delta(G)=\min_v\deg_G(v)$ ,

\epsilon_G=\sigma^2\frac{cT}{1+cT}\sqrt{\frac{cT(2+cT)}{1\vee\delta(G)}}.

Then, with zero initial states, the state equation for $(\alpha^{\mathrm{MF}}_v)_{v\in V}$ has a solution, and

(\alpha^{\mathrm{MF}}_v)_{v\in V}\ \text{is an } \epsilon^G\text{-Nash equilibrium and an } \epsilon_G\text{-Nash equilibrium on } G.

Milestones

Lemma 7.2: $\alpha^{\mathrm{MF}}$ is optimal for the one-player problem $\min\frac12\mathbb E[\int_0^T\beta^2dt+c|Y(T)|^2]$ , $dY=\beta\,dt+\sigma dW$ , over all progressively measurable $\beta$ .
Isolated vertices (p. 40): $J_v(\boldsymbol\alpha)=\inf_\beta J_v(\beta,\boldsymbol\alpha^{-v})$ when $\deg_G(v)=0$ .
(7.7): under $\alpha^{\mathrm{MF}}$ , $(X_u(T))_u$ are i.i.d. $N(0,\sigma^2T/(1+cT))$ , so the neighbour average has second moment $\sigma^2T/(\deg_G(v)(1+cT))$ .
Steps (1), (2), (3) (p. 41): a lower bound on $J_v(\beta,\boldsymbol\alpha^{-v})$ , an energy bound for deviations no worse than the zero control, and the comparison with $J_v(\boldsymbol\alpha^{\mathrm{MF}})$ .
(7.5): for $\deg_G(v)\ge1$ and every admissible $\beta$ , $J_v(\beta,\boldsymbol\alpha^{-v})\ge J_v(\boldsymbol\alpha)-\epsilon^G_v$ .

Significance

The result. Theorem 2.11 gives an explicit threshold for the mean field approximation on networks: along any sequence of graphs whose minimal degree diverges, the decentralized control $\alpha^{\mathrm{MF}}$ is an $\epsilon_{G_n}$ -Nash equilibrium with $\epsilon_{G_n}\to0$ , and the vector form says more: if the average of $(1\vee\deg_{G_n}(v))^{-1/2}$ over vertices tends to zero, the per-player errors vanish on average (the paper's (2.16)). The rate $\deg_G(v)^{-1/2}$ quantifies how the accuracy of the approximation depends on denseness. In the same paper, transitive graphs whose degrees stay bounded lead to equilibria that do not agree with the mean field one, so a denseness condition cannot be dropped.

Formalizing it. The theorem is proved in the paper; to our knowledge no part of it is machine-checked. A formal development needs, beyond the statement, a verification argument for a one-dimensional linear-quadratic control problem with additive noise, Gaussian computations for linear SDEs driven by Brownian motion, and the comparison of costs between the equilibrium system and a system with one deviating player. The one-player result (Lemma 7.2) and the Gaussian facts of (7.7) are reusable well beyond this mission.

Difficulty

The obvious argument compares a deviating player with an isolated player and treats the neighbour average as noise independent of the deviation. Two things stand in the way. The cost of player $v$ couples its terminal state with the neighbours' average through a cross term $\mathbb E[\frac1{\deg_G(v)}\sum_{u\sim v}X_u(T)\,Y_v(T)]$ , and the deviation $\beta(t,\boldsymbol Y(t))$ may look at the neighbours' states, so the cross term does not vanish; it has to be bounded through the size of the deviation's energy. And an arbitrary deviation has no a priori energy bound: one is available only for deviations that do at least as well as the zero control, which is why the argument passes through a (near-)optimal deviation. Lemma 7.2 itself requires a verification theorem over all progressively measurable controls, not only feedback ones.

Formalization scope

The Lean development lives in the namespace GraphLQGame.DenseApprox and uses the shared encoding of this series:

vertices are Fin n (the paper's $\{1,\dots,n\}$ become $\{0,\dots,n-1\}$ ), the state space is EthierKurtz.SDEState n, and $G$ is any SimpleGraph (Fin n); isolated vertices are allowed;
controls are Borel with linear growth on $[0,T]$ only; their values at other times are never used, and the formula for $\alpha^{\mathrm{MF}}$ outside $[0,T]$ is evaluated with Lean's total division;
a solution of the state equation is a pathwise strong solution carrying its own probability space and an $n$ -dimensional standard Brownian motion; costs are $[0,\infty]$ -valued lower Lebesgue integrals, and the Nash inequality is required for every solution of the profile and of each deviation (faithful by strong uniqueness);
$T,\sigma,c>0$ are the standing assumptions of §2.1;
initial states are zero. The printed theorem does not mention $X(0)$ ; the paper fixes non-random initial states that are "in many cases" zero, and the whole proof is for $X(0)=0$ . With non-zero initial states the claim fails in general, so this is a disclosed hypothesis;
the goal also asserts that the state equation for $\alpha^{\mathrm{MF}}$ has a solution, so the Nash property cannot hold vacuously; Lemma 7.2 is stated over every continuous adapted solution of its SDE, and Step (2) carries, as an explicit hypothesis, the comparison with the zero control that its proof uses.

A formalization in which $\alpha^{\mathrm{MF}}$ is compared only with deviations depending on the player's own state, or in which the costs are Bochner integrals that vanish when not integrable, would be trivially or wrongly satisfied; both are ruled out by the encoding above.

Welcome contributions: the verification argument for Lemma 7.2, the Gaussian law of linear SDEs with additive noise, and proofs of the three steps. Related missions in this series: I (an explicit Nash equilibrium on transitive graphs) and II (large-graph limits).

Selected references

D. Lacker, A. Soret, A case study on stochastic games on large graphs in mean field and sparse regimes, arXiv:2005.14102v2, 2021; Math. Oper. Res. 47 (2022). https://arxiv.org/abs/2005.14102
R. Carmona, F. Delarue, Probabilistic Theory of Mean Field Games with Applications II, Springer, 2018. https://doi.org/10.1007/978-3-319-56436-4
M. Huang, R. P. Malhamé, P. E. Caines, Large population stochastic dynamic games: closed-loop McKean–Vlasov systems and the Nash certainty equivalence principle, Commun. Inf. Syst. 6 (2006), 221–252. https://doi.org/10.4310/CIS.2006.v6.n3.a5
H. Pham, Continuous-time Stochastic Control and Optimization with Financial Applications, Springer, 2009 (verification theorem, Theorem 3.5.2). https://doi.org/10.1007/978-3-540-89500-8

14 thms1 active userReviewed

Combinatorics Graph Theory·Captain: mikedeng1

Stability Results on the Circumference of a Graph 1: A 2-Connected Graph with More Than (⌊c/2⌋−1)(n−c) Edges Off a Longest Cycle of Length c ≥ 10 Lies in W_{n,⌊c/2⌋,c} or (c Odd) in X_{n,c} ∪ Y_{n,c}Research Paper

Motivation

The circumference $c(G)$ of a graph $G$ is the length of a longest cycle. Extremal graph theory asks how many edges force a long cycle. The Erdős–Gallai theorem (1959) states that every $n$ -vertex graph has at most $c(G)(n-1)/2$ edges. Bondy (1971) strengthened it by counting only the edges near a longest cycle: if $C$ is a longest cycle of length $c$ , the number of edges with at most one endpoint in $C$ is at most $\tfrac c2(n-c)$ , and at most $\lfloor c/2\rfloor (n-c)$ when $G$ is 2-connected. Since $V(C)$ spans at most $\binom c2$ edges, this implies the Erdős–Gallai bound.

A stability result complements an extremal one: a graph close to the extremal bound must be close in structure to the extremal graphs. Jie Ma and Bo Ning (Combinatorica, 2020; arXiv:1708.00704) proved stability versions of Kopylov's edge theorem for 2-connected graphs of given circumference and of Bondy's theorem above. This mission formalizes their stability version of Bondy's theorem, Theorem 1.12. In the paper it is also one of the two halves of the proof of the main stability theorem; the other half is a separate mission in this series.

Timeline (as recorded in §1 of the paper). Dirac (1952): every 2-connected graph has $c(G)\ge\min\{2\delta(G),|V(G)|\}$ . Erdős and Gallai (1959): $e(G)\le c(G)(n-1)/2$ . Bondy (1971): the bound on edges with at most one endpoint on a longest cycle, and the degree theorem stated here as Theorem 2.1. Woodall (1976): $e(G)\le f(n,\lfloor c/2\rfloor,c)$ for 2-connected $G$ with circumference $c\le(2n+2)/3$ . Kopylov (1977): $e(G)\le\max\{f(n,2,c),f(n,\lfloor c/2\rfloor,c)\}$ for 2-connected $G$ with circumference $c\le n-1$ ; another proof by Fan, Lv and Wang (2004). Fan (1990): an improved version of Bondy's bound for 2-connected graphs, and average-degree bounds on long paths. Füredi, Kostochka and Verstraëte (2016): stability for Kopylov's theorem when $n\ge 3\lfloor c/2\rfloor$ ; Füredi, Kostochka, Luo and Verstraëte (2018): the complete stability version, with the families $\mathcal X_{n,c}$ , $\mathcal Y_{n,c}$ . Ma and Ning (2017 preprint, 2020): the results of this mission.

Setting

All graphs are finite and simple, on the vertex set $\{0,\dots,n-1\}$ . A path or cycle of length $k$ has $k$ edges. A graph is 2-connected if it has at least three vertices, is connected, and remains connected after deleting any one vertex. A cycle $C$ is a longest cycle if no cycle of $G$ has more edges; $V(C)$ is its vertex set and $c$ its length.

For a longest cycle $C$ , write $e(G-C)+e(G-C,C)$ for the number of edges with at most one endpoint in $C$ . A vertex $u$ is an isolated vertex of $G-C$ if $u\notin V(C)$ and every neighbour of $u$ lies on $C$ ; $d_C(u)$ is its number of neighbours on $C$ .

The extremal graphs are:

$W_{n,k,c}$ : a clique $K_{c-k+1}$ together with $n-(c-k+1)$ further vertices, each adjacent to the same $k$ vertices of the clique and to nothing else.
$\mathcal X_{n,c}$ : graphs on $A\cup B\cup X$ with $A$ a clique of size $\lfloor c/2\rfloor$ , $B$ and $X$ stable, $A$ completely joined to $B$ , and two vertices $a\in A$ , $b\in B$ such that $N(x)=\{a,b\}$ for all $x\in X$ .
$\mathcal Y_{n,c}$ : graphs on $A\cup B\cup Y$ with $A$ a clique of size $\lfloor c/2\rfloor$ , $B$ stable, $A$ completely joined to $B$ , $G[Y]$ a star forest with at least two stars each having an edge, and two distinct $a,b\in A$ such that each star $S$ has exactly $\{a,b\}$ as outside neighbourhood and, if $|V(S)|\ge 3$ , its leaves have degree $2$ and a common neighbour in $\{a,b\}$ .

$G\subseteq W$ means that $G$ is isomorphic to a subgraph of $W$ .

Formalization targets

Goal: Theorem 1.12

Let $G$ be 2-connected on $n$ vertices and $C$ a longest cycle of length $c$ with $10\le c\le n-1$ . If

e(G-C)+e(G-C,C) > \left(\left\lfloor \tfrac c2\right\rfloor-1\right)(n-c),

then $G\subseteq W_{n,\lfloor c/2\rfloor,c}$ , or $c$ is odd and $G$ is a subgraph of a member of $\mathcal X_{n,c}\cup\mathcal Y_{n,c}$ .

Milestones

Theorem 2.1 (Bondy): all but one vertex of degree $\ge k$ in a 2-connected graph give $c(G)\ge\min\{n,2k\}$ .
Theorem 2.2 (Fan), first assertion: a longest $(x,y)$ -path is at least as long as the average degree of the other vertices.
Lemma 2.3: a 2-connected component $H$ of $G-C$ with average degree $r$ satisfies $c\ge 2r$ , with equality only for a clique attached to two common vertices of $C$ .
Theorem 3.2: without connectivity and for $4\le c\le n-1$ , the same edge condition gives $c\in\{6,7,9\}$ , or a vertex off $C$ with $\lfloor c/2\rfloor$ neighbours on $C$ , or a cycle $C'$ meeting $C$ in at most one vertex with $|C'|\ge 2\lfloor c/2\rfloor-3$ (disjoint) or $\ge 2\lfloor c/2\rfloor-1$ (one common vertex).
Theorem 3.1: for 2-connected $G$ and $10\le c\le n-1$ , an isolated vertex $u$ of $G-C$ with $d_C(u)=\lfloor c/2\rfloor$ .
Lemma 3.3: such a vertex forces $G\subseteq W_{n,\lfloor c/2\rfloor,c}$ when $c$ is even, and $G\subseteq W_{n,\lfloor c/2\rfloor,c}$ or $G$ in a member of $\mathcal X_{n,c}\cup\mathcal Y_{n,c}$ when $c\ge 9$ is odd.

Significance

In $W_{n,\lfloor c/2\rfloor,c}$ every one of the $n-c$ vertices off a longest cycle sends $\lfloor c/2\rfloor$ edges to the cycle, so Bondy's bound $\lfloor c/2\rfloor(n-c)$ is attained. Theorem 1.12 says that exceeding $(\lfloor c/2\rfloor-1)(n-c)$ already leaves only three structures: a subgraph of $W_{n,\lfloor c/2\rfloor,c}$ , or for odd $c$ a subgraph of a member of $\mathcal X_{n,c}$ or $\mathcal Y_{n,c}$ . In the paper it is one of the two cases of the proof of the main stability theorem (Theorem 1.9): a graph with many edges and a longest cycle $C$ has either many edges with at most one endpoint on $C$ , handled here, or many edges inside $V(C)$ , handled by the closure argument of the companion mission.

The result is proved in the paper; none of it, nor Bondy's or Fan's theorems, is formalized on the platform or in Mathlib. The mission produces machine-checked statements of the goal, of the cited tools (Bondy's Theorem 2.1, Fan's Theorem 2.2, Lemma 2.3), and of the steps Theorems 3.1, 3.2 and Lemma 3.3, together with reusable definitions of 2-connectivity, longest cycles and the extremal families.

Difficulty

The obvious approach counts edges at the vertices off $C$ : each such vertex has at most $\lfloor c/2\rfloor$ neighbours on $C$ , since otherwise two consecutive cycle vertices would let the cycle be extended. This bound is far from enough. The edge count also includes edges between vertices off $C$ , and components of $G-C$ can be large, 2-connected, and attached to $C$ in complicated ways. The bound $(\lfloor c/2\rfloor-1)(n-c)$ has to be beaten by every such configuration at once, and Theorem 3.2 states exceptional small cycle lengths $c\in\{6,7,9\}$ for which the analysis does not close. A second difficulty is the passage from one vertex of degree $\lfloor c/2\rfloor$ to a global description of $G$ : in the odd case, the structure of every component of $G-C$ has to be determined, which is where the families $\mathcal X_{n,c}$ and $\mathcal Y_{n,c}$ appear.

Formalization scope

Graphs are SimpleGraph (Fin n) with decidable adjacency. A cycle is a closed walk C : G.Walk u u with C.IsCycle; its length is C.length and its vertex set C.support.toFinset. "Longest cycle" is the predicate that every cycle of $G$ is at most as long as $C$ ; no supremum of cycle lengths is used. 2-connectivity is: at least three vertices, connected, and connected after deleting any one vertex. It is stated for an arbitrary finite vertex type so that it applies to the induced subgraph $G[H]$ in Lemma 2.3. The edge count off $C$ is the number of edges with an endpoint outside $V(C)$ , and $\lfloor c/2\rfloor$ is natural-number division; under the stated bounds every natural-number subtraction is exact.

$W_{n,k,c}$ is defined on fixed labels (clique $\{0,\dots,c-k\}$ , hubs $\{0,\dots,k-1\}$ ), and " $G\subseteq W$ " is a graph embedding G ⊑ W. Membership in $\mathcal X_{n,c}$ and $\mathcal Y_{n,c}$ are predicates on labelled graphs, closed under relabelling, and " $G$ is a subgraph of a member" is G ≤ H for some member $H$ . No hypothesis is added to any statement. Fan's Theorem 2.2 is stated without its equality characterization.

Trivializing formalizations are ruled out explicitly: the alternative " $c$ is odd and …" is a conjunction, never an implication; the circumference is never a junk supremum; containment in $W$ is up to isomorphism, never ≤ on fixed labels; and 2-connectivity excludes $K_2$ and disconnected graphs.

The definitions are reusable for any work on circumference, longest cycles and Bondy–Erdős–Gallai-type problems. Contributions of proofs of the cited tools (Bondy's and Fan's theorems) are especially welcome, as is a proof of Erdős–Gallai's edge theorem, which the proof of Theorem 3.2 uses and which is posed elsewhere on the platform.

Selected references

J. Ma and B. Ning, Stability results on the circumference of a graph, Combinatorica 40 (2020); arXiv:1708.00704v2. https://arxiv.org/abs/1708.00704 , https://doi.org/10.1007/s00493-019-3843-4
J. A. Bondy, Large cycles in graphs, Discrete Mathematics 1 (1971/72), no. 2, 121–132.
G. Fan, Long cycles and the codiameter of a graph, I, Journal of Combinatorial Theory, Series B 49 (1990) 151–180.
P. Erdős and T. Gallai, On maximal paths and circuits of graphs, Acta Mathematica Academiae Scientiarum Hungaricae 10 (1959) 337–356.
G. Fan, X. Lv, P. Wang, Cycles in 2-connected graphs, Journal of Combinatorial Theory, Series B 92 (2004) 379–394.
Z. Füredi, A. Kostochka, J. Verstraëte, Stability in the Erdős–Gallai theorems on cycles and paths, Journal of Combinatorial Theory, Series B 121 (2016) 197–228.
Z. Füredi, A. Kostochka, R. Luo, J. Verstraëte, Stability in the Erdős–Gallai theorem on cycles and paths, II, Discrete Mathematics 341 (2018) 1253–1263.
G. N. Kopylov, Maximal paths and cycles in a graph, Soviet Mathematics Doklady 18 (1977) 593–596.
D. R. Woodall, Maximal circuits of graphs I, Acta Mathematica Academiae Scientiarum Hungaricae 28 (1976) 77–80.

8 thms1 active userReviewed

Convex Optimization Optimization·Captain: mikedeng1

DC Programming and DCA: Thirty Years of Developments: For f = g − h with g, h ∈ Γ₀(ℝⁿ), at x ∈ ri(dom g) ∩ ri(dom h) d-Stationarity of f Is Equivalent to Strong Criticality ∅ ≠ ∂h(x) ⊂ ∂g(x)Research Paper

Motivation

DC programming is the minimization of a function $f = g - h$ that is a difference of two convex functions. The class contains every $C^2$ function on a compact convex set and most nonconvex models of sparse learning, clustering, combinatorial relaxations and robust optimization, and its standard method, the DC Algorithm (DCA), replaces $h$ by its affine minorant at the current iterate and solves a convex program at each step. DCA was introduced by Pham Dinh Tao in 1985 and developed jointly with Le Thi Hoai An from 1994 on (Pham Dinh & Le Thi 1998); the survey of Le Thi & Pham Dinh 2018 collects thirty years of that work.

DCA is guaranteed to reach critical or strongly critical points, notions that depend on the chosen decomposition $g - h$ , while a decomposition-free notion, directional (d-)stationarity of $f$ itself, is what a user of a nonconvex model usually wants. Ahn, Pang & Xin 2017 warned that DC criticality can be much weaker than d-stationarity. Theorem 1 of the 2018 survey (p. 9) states when the two coincide. Its proof is omitted in the paper ("can be easily deduced … It is omitted here").

Setting

Let $X = \mathbb R^n$ with the canonical inner product $\langle\cdot,\cdot\rangle$ . Functions take values in $\mathbb R\cup\{\pm\infty\}$ . The effective domain of $\varphi$ is $\operatorname{dom}\varphi = \{x : \varphi(x) < +\infty\}$ , and $\Gamma_0(X)$ is the set of proper, lower semicontinuous, convex functions $X \to \mathbb R\cup\{+\infty\}$ .

The standard DC program is

(P_{dc})\qquad \alpha = \inf\{f(x) := g(x) - h(x) : x\in X\},\qquad g, h\in\Gamma_0(X),

with the convention $+\infty - (+\infty) = +\infty$ , and $\alpha$ is assumed finite. Finiteness of $\alpha$ forces $\operatorname{dom} g\subset\operatorname{dom} h$ , so $\operatorname{dom} f = \operatorname{dom} g$ .

The subdifferential of $\varphi$ at $x$ is

\partial\varphi(x) = \{y\in X : \varphi(x) < +\infty,\ \varphi(v) \ge \varphi(x) + \langle y, v - x\rangle\ \ \forall v\in X\}.

A point $x$ is strongly critical for $f = g - h$ if $\emptyset \ne \partial h(x)\subset\partial g(x)$ .

The directional derivative of $\varphi$ at $x\in\operatorname{dom}\varphi$ in direction $u$ is $\varphi'(x;u) = \lim_{t\downarrow 0}(\varphi(x+tu) - \varphi(x))/t$ . For convex $\varphi$ it equals $\inf_{t>0}(\varphi(x+tu)-\varphi(x))/t$ . A point $x\in\operatorname{dom} f$ is d-stationary for $f$ if $f'(x;u)\ge 0$ for every $u\in X$ . The support function of $C\subset X$ is $\chi^*_C(u) = \sup_{y\in C}\langle u, y\rangle$ , with $\chi^*_\emptyset \equiv -\infty$ . Finally, $\operatorname{ri} C$ is the relative interior of $C$ , its interior inside the affine hull $\operatorname{aff} C$ .

Formalization targets

Goal: Theorem 1(iii)

For $x\in\operatorname{ri}(\operatorname{dom} g)\cap\operatorname{ri}(\operatorname{dom} h)$ ,

x \text{ is d-stationary for } f \iff \emptyset\ne\partial h(x)\subset\partial g(x).

Milestones

Theorem 1(i): for $x\in\operatorname{dom} g$ with $\partial h(x)\ne\emptyset$ ,

f'(x;u) = g'(x;u) - h'(x;u)\qquad \forall u\in X.

Theorem 1(ii), first sentence: under the same hypotheses, $x$ is d-stationary iff $g'(x;u)\ge h'(x;u)$ for all $u$ .
Theorem 1(iv): for $x\in\operatorname{ri}(\operatorname{dom} g)$ with $\partial h(x)\ne\emptyset$ , d-stationarity implies strong criticality.
Theorem 1(v): for $x\in\operatorname{ri}(\operatorname{dom} h)$ , strong criticality implies d-stationarity.

Companion statements

Theorem 1(ii), second sentence: for $x\in\operatorname{dom} g$ , if $g'(x;\cdot) = \chi^*_{\partial g(x)}$ and $h'(x;\cdot) = \chi^*_{\partial h(x)}$ , then d-stationarity and strong criticality coincide.
Theorem 1(vi): if $\operatorname{aff}(\operatorname{dom} g) = \operatorname{aff}(\operatorname{dom} h)$ , then $\operatorname{ri}(\operatorname{dom} g)\subset\operatorname{ri}(\operatorname{dom} h)$ and the equivalence holds on $\operatorname{ri}(\operatorname{dom} g)$ .

Part (iii) is the goal because it is the equivalence the paper uses to justify DCA, stated under a hypothesis symmetric in $g$ and $h$ ; (vi) is the more general companion.

Significance

The theorem connects the output of DCA with a stationarity notion intrinsic to $f$ . Without it, the strong criticality certified by DCA would be a property of a decomposition rather than of the problem, and different decompositions of the same $f$ could certify different points. With it, at points in the relative interiors of the domains, every strongly critical point is d-stationary, and conversely no d-stationary point is missed by the criticality test.

Parts (i) and (ii) are stated in the paper without proof, and so is the rest of Theorem 1; none of it has a machine-checked proof. The mission produces a formal statement of all six parts with the extended-real conventions made explicit. Three of the printed parts are false as stated without the nonemptiness of $\partial h(x)$ ; the formal versions add that hypothesis and record a counterexample for each, so the formalization also corrects the printed statement.

Difficulty

The obvious argument writes $f'(x;u) = g'(x;u) - h'(x;u)$ and reads off both directions from $g'\ge h'$ . Two steps of it fail. First, the difference can be $-\infty - (-\infty)$ or $+\infty - (+\infty)$ , and the limit defining $f'$ need not be the difference of the limits; the nonemptiness of $\partial h(x)$ is exactly what rules out the first case. Second, passing from " $g'(x;\cdot)\ge h'(x;\cdot)$ " to " $\partial h(x)\subset\partial g(x)$ " needs $h'(x;\cdot)$ to equal the support function of $\partial h(x)$ , which holds in the relative interior of $\operatorname{dom} h$ but fails on its relative boundary, where $h'(x;\cdot)$ need not be lower semicontinuous. The relative interior, not the interior, is essential: the domains may be lower-dimensional.

Formalization scope

$X$ is EuclideanSpace ℝ (Fin n), and every function maps into EReal. The published definitions TaoAnDCA.GlobalOpt.Setting supply $\operatorname{dom}$ (effDom), the DC objective with $+\infty - (+\infty) = +\infty$ (dcSub), the subdifferential (subdiff) and $\alpha$ (primalValue); $\Gamma_0(X)$ is the published IsProperClosedConvex. Every statement carries the standing assumptions of Theorem 1 as binders: $g, h\in\Gamma_0(X)$ , $\alpha\ne-\infty$ and $\alpha\ne+\infty$ . The mission's definitions are:

convDirDeriv: the convex directional derivative by the paper's infimum formula, in EReal;
HasDirDerivE: the predicate that the one-sided limit along $t\downarrow 0$ exists in EReal and equals a given value;
IsDStationary: $x\in\operatorname{dom}\varphi$ and, for every direction, the limit exists and is $\ge 0$ ;
IsStronglyCritical: both $\partial h(x)\ne\emptyset$ and $\partial h(x)\subset\partial g(x)$ ;
supportFn: the extended-real support function, $-\infty$ on $\emptyset$ .

The relative interior is Mathlib's intrinsicInterior ℝ, the affine hull is affineSpan ℝ. The subgradient inequality has the standard sign; display (1) of the paper prints the opposite sign, a slip. The only hypothesis added to the page is $\partial h(x)\ne\emptyset$ , in parts (i), (ii) first sentence and (iv), each of which is false without it; parts (ii) second sentence, (iii), (v) and (vi) are stated as printed.

The statement admits trivializing formalizations, which this one rules out. Strong criticality without the nonemptiness of $\partial h(x)$ is vacuous wherever $\partial h(x) = \emptyset$ . A d-stationarity defined through limUnder, a real-valued derivative, or "every limit is nonnegative" holds vacuously where the limit does not exist. And $g - h$ written in raw EReal would give $+\infty - (+\infty) = -\infty$ .

A complete development needs the monotonicity of convex difference quotients in EReal, limit arithmetic for extended reals, and the formula $\varphi'(x;\cdot) = \chi^*_{\partial\varphi(x)}$ for $\varphi\in\Gamma_0(\mathbb R^n)$ at points of $\operatorname{ri}(\operatorname{dom}\varphi)$ (Rockafellar 1970, Theorem 23.4), together with the nonemptiness of $\partial\varphi$ there. These results on extended-real convex functions are reusable well beyond DC programming, and contributions of them as separate theorems are welcome.

Selected references

H. A. Le Thi, T. Pham Dinh, DC programming and DCA: thirty years of developments, Mathematical Programming Ser. B 169 (2018), 5–68. https://doi.org/10.1007/s10107-018-1235-y
T. Pham Dinh, H. A. Le Thi, A d.c. optimization algorithm for solving the trust-region subproblem, SIAM Journal on Optimization 8 (1998), 476–505. https://doi.org/10.1137/S1052623494274313
M. Ahn, J.-S. Pang, J. Xin, Difference-of-convex learning: directional stationarity, optimality, and sparsity, SIAM Journal on Optimization 27 (2017), 1637–1665. https://doi.org/10.1137/16M1084754
R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

10 thms1 active userReviewed

Control Theory Optimization Probability+1·Captain: mikedeng1

Open-Loop and Closed-Loop Solvabilities for Stochastic Linear Quadratic Optimal Control Problems 1: The Cost Is Uniformly Convex iff the Riccati Equation Has a Strongly Regular SolutionResearch Paper

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

Lemma 2.2: the cost of a feedback control $\Theta X+u$ , written through the solution of a Lyapunov equation.
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$ .
Proposition 4.1: uniform convexity gives unique open-loop solvability and $V^0(t,x)\ge\alpha|x|^2$ .
Proposition 4.4: every Lyapunov solution satisfies $R+D^\top PD\ge\lambda I$ and $P\ge\alpha I$ , with the same $\lambda,\alpha$ .
(4.20) and the monotonicity $P_1\ge P_i\ge P_{i+1}\ge\alpha I$ of the iteration (4.18)–(4.19).
Uniform convergence of the iteration to a strongly regular solution.
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

14 thms1 active userReviewed

Analysis Mathematical Physics Probability·Captain: mikedeng1

Conformal Weldings of Random Surfaces: SLE and the Quantum Gravity Zipper 1: Reverse SLE_κ/GFF Coupling — Zipping Up a Free Boundary GFF by a Reverse Loewner Flow Preserves Its LawResearch Paper

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)

The reverse-flow table on p. 44: $\frac{d}{dt}f_t'(z)=2f_t'(z)/f_t(z)^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)}$ .
$\operatorname{Im}f_t(z)$ is strictly increasing in $t$ .
$|\partial_tC_t(z)|$ is bounded uniformly for $z$ in a compact subset of $\mathbb H$ and all $t$ .
For fixed $z$ , $\mathfrak h_t(z)$ is a martingale.
For mean-zero $\rho$ , $(\mathfrak h_t,\rho)$ is a martingale.
For fixed $x\neq y$ , $\mathfrak h_t(x)\mathfrak h_t(y)+G_t(x,y)$ is a martingale.
(4.2): $(\mathfrak h_t,\rho_1)(\mathfrak h_t,\rho_2)+E_t(\rho_1,\rho_2)$ is a martingale.
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))$ .
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

14 thms1 active userReviewed

Analysis Probability Stochastic Systems·Captain: mikedeng1

On Well-Posedness of Forward–Backward SDEs—A Unified Approach 1: Under Cases I–III the FBSDE Has a Decoupling Field with Bounded Difference Quotients and a Unique L² Solution on [0, T]Research Paper

Motivation

A forward–backward stochastic differential equation (FBSDE) couples a forward SDE, solved from an initial state, with a backward SDE, solved from a terminal condition that depends on the forward state. Such systems arise from the stochastic maximum principle, from quasilinear parabolic PDEs through Feynman–Kac formulas, and in mathematical finance. Whenever a control problem or a market model is solved through its first-order conditions, a fully coupled FBSDE appears, and the question is whether it has a unique solution.

The history has a recurring gap: each method covers a different regime, and none handles coefficients that are random, fully coupled, and have a forward diffusion depending on the martingale integrand $Z$ , over an arbitrary horizon.

1993: F. Antonelli proved well-posedness over a small time interval by contraction, under a smallness condition on the coupling.
1994: J. Ma, P. Protter and J. Yong introduced the four-step scheme, solving Markovian FBSDEs with deterministic coefficients over arbitrary horizons through a quasilinear PDE; the forward diffusion may not depend on $z$ in a degenerate way.
1995–1999: Y. Hu, S. Peng and Z. Wu developed the method of continuation, which allows random coefficients over arbitrary horizons under a monotonicity condition on the coefficients.
1999–2002: E. Pardoux and S. Tang, and F. Delarue, extended the PDE and fixed-point approaches under weak-coupling or strong-monotonicity conditions, in the Markovian setting.
2015: J. Ma, Z. Wu, D. Zhang and J. Zhang (the source of this mission) gave a unified approach through the decoupling field and a scalar ordinary differential equation that dominates its spatial derivative.

Setting

Fix a horizon $T>0$ and a probability space carrying a one-dimensional Brownian motion $B$ , with $\mathbb F$ its natural filtration augmented by the null sets. All processes are real valued. The FBSDE (1.1) is

X_t=x+\int_0^t b(s,\Theta_s)\,ds+\int_0^t\sigma(s,\Theta_s)\,dB_s,\qquad Y_t=g(X_T)+\int_t^T f(s,\Theta_s)\,ds-\int_t^T Z_s\,dB_s ,

for $t\in[0,T]$ , with $\Theta=(X,Y,Z)$ . The coefficients $b,\sigma,f$ depend on $(t,\omega,x,y,z)$ and $g$ on $(x,\omega)$ . Assumption 2.1 asks that they be progressively measurable for fixed $(x,y,z)$ , that $I_0^2=\mathbb E\{(\int_0^T[|b|+|f|](t,0,0,0)dt)^2+\int_0^T|\sigma|^2(t,0,0,0)dt+|g(0)|^2\}$ be finite, and that they be Lipschitz in $(x,y,z)$ with a common constant $K_0$ , uniformly in $\omega$ . Solutions are sought in the space $\mathbb L^2$ of progressively measurable $\Theta$ with $\|\Theta\|^2_{\mathbb L^2}=\mathbb E\{\sup_t(|X_t|^2+|Y_t|^2)+\int_0^T|Z_t|^2dt\}<\infty$ .

A decoupling field (Definition 2.2) is a random field $u(t,x)$ with $u(T,\cdot)=g$ such that, on every short interval $[t_1,t_2]$ and from every square-integrable initial state, the FBSDE with terminal map $u(t_2,\cdot)$ is uniquely solvable and its solution satisfies $Y_t=u(t,X_t)$ .

The difference quotients (3.1) of the coefficients — $\tilde b_i,\tilde\sigma_i,\tilde f_i$ in the variables $x,y,z$ ( $i=1,2,3$ ) and $\tilde h$ for $g$ — enter the scalar function

F=f_1+f_2y+y(b_1+b_2y)+\frac{(f_3+b_3y)\,y\,(\sigma_1+\sigma_2y)}{1-\sigma_3y},

and its essential supremum $\overline F(t,y)$ and infimum $\underline F(t,y)$ over all quotients give the dominating ODEs (3.13): $\overline y_t=\overline h+\int_t^T\overline F(s,\overline y_s)ds$ and $\underline y_t=\underline h+\int_t^T\underline F(s,\underline y_s)ds$ , with $\overline h,\underline h$ the bounds of $\tilde h$ .

Formalization targets

Goal: Theorem 7.4

Fix $c_1,c_2,c_3$ with $c_1>0$ , $0<c_2<c_3$ , $c_1c_3<1$ (5.13). There are $\varepsilon>0$ and $C>0$ , depending only on $T$ , $K_0$ and $c_1,c_2,c_3$ , such that whenever Assumption 2.1 holds and the quotients satisfy one of the nine conditions of Cases I–III ((5.14); (5.15)–(5.18); (5.19)–(5.22)), uniformly in the quotient arguments, then (i) the FBSDE has a decoupling field $u$ whose quotient $(u(t,x_1)-u(t,x_2))/(x_1-x_2)$ obeys the bound assumed of $\tilde h$ with $c_2$ replaced by $c_3$ , and (ii) for every $x$ there is a unique solution in $\mathbb L^2$ , with

\|\Theta\|^2_{\mathbb L^2}\le C\,\big[\,|x|^2+I_0^2\,\big].

Milestones

Lemma 5.1: comparison for scalar backward ODEs between a sub- and a super-solution.
Theorems 5.9, 5.10, 5.11: under each case, the dominating ODEs have bounded solutions with the bound of $h$ transported to $c_3$ , and $1-\sigma_3y$ stays away from $0$ .
Theorems 6.1, 6.2, 6.3: over a short horizon $T\le\delta$ , unique solvability, solutions of (3.13) in a band, and a random field $u$ whose quotients lie between $\underline y$ and $\overline y$ .
Theorem 2.3: a decoupling field gives a unique global solution with $Y_t=u(t,X_t)$ .

A companion statement, Corollary 7.5, gives well-posedness over $[0,T]$ under the sign conditions (7.5) or (7.6), with no smallness constant.

Significance

The theorem replaces structural assumptions (small horizon, monotonicity, deterministic coefficients, $\sigma$ independent of $z$ ) by conditions that can be read off the coefficients through a scalar ODE. It covers random coefficients and a forward diffusion that depends on $z$ , the case in which the classical Riccati-type obstruction $\sigma_3h=1$ appears, and it recovers the earlier sufficient conditions as special cases (§7.4 of the paper). The decoupling field produced in (i) is uniformly Lipschitz, which is the input to the comparison and stability results of §8 and to numerical schemes based on $Y_t=u(t,X_t)$ .

The result is proved in the paper; nothing here is open mathematically. None of it is formalized: there is no machine-checked existence theory for coupled FBSDEs in any proof assistant this mission is aware of. A complete development would be the first formal well-posedness theorem for a fully coupled FBSDE, and the milestones — the ODE comparison lemma, the small-time theory, and the patching argument of Theorem 2.3 — are each self-contained.

Difficulty

The obvious approach is a contraction argument on $[0,T]$ . It works only when $T$ is small, because the Lipschitz constant of the solution map grows with the coupling; iterating it over a partition requires a terminal condition $u(t_i,\cdot)$ whose Lipschitz constant does not deteriorate from one subinterval to the next. Controlling that constant is the whole problem. Its spatial derivative satisfies a backward stochastic Riccati equation with quadratic growth in both $y$ and $z$ and a singularity where $1-\sigma_3y=0$ ; such equations need not have bounded solutions, and the standard comparison theory for quadratic BSDEs does not apply off the region where the generator is Lipschitz. A second difficulty is the small-time theory itself: when $\sigma$ depends on $z$ , even a linear FBSDE with constant coefficients is well posed on short intervals only if $\sigma_3h\ne1$ (Theorem 7.1 of the paper), so in Cases II and III, where $\sigma_3$ and $h$ are large, the contraction argument does not apply even for small $T$ .

Formalization scope

The development reuses the platform's Peng1990.SMP.Stochastic (standard Brownian motion, $L^2_{\mathcal F}$ , the $L^2$ Itô integral IsItoIntegral) and the augmented Brownian filtration of ReflectedBSDE.Existence.Setting. Time is $\mathbb R_{\ge0}$ , time integrals are over real intervals, and the stochastic integral $\int_{t_1}^t\sigma\,dB$ is $J_t-J_{t_1}$ for an Itô integral process $J$ of $\mathbf 1_{(t_1,t_2]}\sigma(s,\Theta_s)$ .

Committed conventions:

Lipschitz bounds use the $\ell^1$ norm on $\mathbb R^3$ and hold for every $\omega$ ; $I_0^2$ and $\|\Theta\|^2_{\mathbb L^2}$ are lower Lebesgue integrals in $[0,\infty]$ .
Uniqueness is uniqueness in $\mathbb L^2$ : $X,Y$ agree a.s. at each time and $Z$ agrees $dt\otimes d\mathbb P$ -a.e.
Solutions are unique only up to modification, so (7.2) is asserted for one solution in $\mathbb L^2$ .
Definition 2.2's " $0=t_1<t_2\le T$ " is read as $0\le t_1$ , as the proof of Theorem 2.3 uses it.
Every condition on the quotients holds for every $t\in[0,T]$ , almost surely, for all arguments with distinct coordinates. $\overline F(t,c)\le\varepsilon$ is stated in exactly that form. $\overline F,\underline F,\overline h,\underline h$ as functions are $\mathrm{EReal}$ -valued, and solutions of (3.13) keep them finite.
" $(1-\sigma_3y)^{-1}$ is bounded" is $|1-\tilde\sigma_3y_t|\ge\kappa>0$ . Every use of $\alpha_3=b_2-b_3\sigma_2/\sigma_3$ carries $\tilde\sigma_3\ne0$ , and (5.19), (5.21) carry the heading $\sigma_3\ne0$ of Table 3 in the goal.
The quotient bounds on $u$ hold for each $t$ and each pair $x_1\ne x_2$ almost surely.
Lemma 5.1 additionally assumes $y^1\le y^2$ and $L\ge0$ , both implicit on the page.

The constants $\varepsilon$ , $\delta$ and $C$ are chosen before the probability space and the coefficients. A formalization that places them after the coefficients, integrates without integrability, divides at the pole $1-\sigma_3y=0$ , uses a real-valued essential supremum of an unbounded family, or states uniqueness without a solution class would make the statements vacuous or false; none of these is used.

Contributions are welcome on every milestone. The ODE layer (Lemma 5.1 and the a priori bounds of Theorems 5.9–5.11) needs only real analysis and is a natural first target. The stochastic layer needs Itô-integral facts (linearity, restriction to subintervals, the Burkholder–Davis–Gundy and Doob inequalities in $L^2$ ) and the Lipschitz BSDE theory; these are reusable well beyond this mission.

Selected references

J. Ma, Z. Wu, D. Zhang, J. Zhang, On well-posedness of forward–backward SDEs—a unified approach, Ann. Appl. Probab. 25(4):2168–2214, 2015. https://arxiv.org/abs/1110.4658
F. Antonelli, Backward–forward stochastic differential equations, Ann. Appl. Probab. 3(3):777–793, 1993. https://doi.org/10.1214/aoap/1177005363
J. Ma, P. Protter, J. Yong, Solving forward–backward stochastic differential equations explicitly — a four step scheme, Probab. Theory Related Fields 98:339–359, 1994. https://doi.org/10.1007/BF01192258
Y. Hu, S. Peng, Solution of forward–backward stochastic differential equations, Probab. Theory Related Fields 103:273–283, 1995. https://doi.org/10.1007/BF01204218
S. Peng, Z. Wu, Fully coupled forward–backward stochastic differential equations and applications to optimal control, SIAM J. Control Optim. 37(3):825–843, 1999. https://doi.org/10.1137/S0363012996313549
F. Delarue, On the existence and uniqueness of solutions to FBSDEs in a non-degenerate case, Stochastic Process. Appl. 99:209–286, 2002. https://doi.org/10.1016/S0304-4149(02)00085-6
J. Ma, J. Yong, Forward–Backward Stochastic Differential Equations and their Applications, Lecture Notes in Math. 1702, Springer, 1999. https://doi.org/10.1007/978-3-540-48831-6

14 thms1 active userReviewed

Algebraic Geometry Optimization·Captain: mikedeng1

Exploiting Symmetries in SDP-Relaxations for Polynomial Optimization 2: A Symmetric Quartic Is Nonnegative iff Each Restriction f^ω to a 2-Partition ω Is a Sum of SquaresResearch Paper

Motivation

Deciding whether a real polynomial is non-negative on $\mathbb R^n$ is NP-hard already for quartics, and the standard computational substitute is to ask whether it is a sum of squares (SOS) of polynomials, which is a semidefinite feasibility problem. The two notions agree only in three cases, determined by Hilbert in 1888: univariate polynomials, quadratic forms, and ternary quartic forms (equivalently, polynomials of degree at most 4 in two variables). Outside those cases there are non-negative polynomials that are not SOS, among them symmetric ones: Choi and Lam exhibited a symmetric quartic form in four variables that is non-negative but not SOS.

Many polynomial optimization problems are symmetric, invariant under permutations of the variables. Riener, Theobald, Jansson Andrén and Lasserre (arXiv:1103.0486, Math. Oper. Res. 2013) study how symmetry reduces the size of SDP relaxations. Their §5 uses the degree principle, introduced by Timofte (2003) and refined by Riener (2012), to replace one symmetric problem in $n$ variables by finitely many problems in few variables. For symmetric quartics this yields an exact SOS certificate of non-negativity in every dimension: Theorem 5.5, the goal of this mission.

Timeline:

1888: Hilbert shows that non-negative ternary quartic forms are sums of squares (of quadratic forms).
1977: Choi and Lam give a non-negative symmetric quartic form in four variables that is not SOS.
2003: Timofte proves the half-degree principle for symmetric polynomials (J. Math. Anal. Appl.).
2012: Riener refines it to semialgebraic constraints, with $r = \max\{2, \lfloor \deg f/2\rfloor, \deg g_j\}$ (J. Pure Appl. Algebra).
2012–2013: Riener, Theobald, Jansson Andrén and Lasserre derive Theorem 5.5.

Setting

Let $\mathbb R[X] = \mathbb R[X_1, \dots, X_n]$ . A polynomial $f$ is symmetric if $f(X_{\sigma(1)}, \dots, X_{\sigma(n)}) = f$ for every permutation $\sigma$ ; its degree $\deg f$ is the total degree. A polynomial $p$ is a sum of squares if $p = \sum_{i=1}^k h_i^2$ for some polynomials $h_i$ in the same variables.

For symmetric $f, g_1, \dots, g_m \in \mathbb R[X]$ put

K = \{x \in \mathbb R^n : g_1(x) \ge 0, \dots, g_m(x) \ge 0\}, \qquad r := \max\{2, \lfloor (\deg f)/2 \rfloor, \deg g_1, \dots, \deg g_m\},

and let $A_r \subseteq \mathbb R^n$ be the set of points with at most $r$ distinct components.

An $r$ -partition of $n$ is a vector $\omega = (\omega_1, \dots, \omega_r)$ of positive, non-increasing integers with $\omega_1 + \dots + \omega_r = n$ ; $\Omega$ denotes the set of all of them. For $\omega \in \Omega$ ,

f^\omega := f(\underbrace{T_1, \dots, T_1}_{\omega_1}, \dots, \underbrace{T_r, \dots, T_r}_{\omega_r}) \in \mathbb R[T_1, \dots, T_r],

and $K^\omega := \{t \in \mathbb R^r : g_1^\omega(t) \ge 0, \dots, g_m^\omega(t) \ge 0\}$ . For $r = 2$ the partitions are $(\omega_1, \omega_2)$ with $\omega_1 \ge \omega_2 \ge 1$ , $\omega_1 + \omega_2 = n$ ; there are $\lfloor n/2 \rfloor$ of them.

Formalization targets

Goal: Theorem 5.5 (p. 23)

For $n \ge 2$ and a symmetric $f \in \mathbb R[X_1, \dots, X_n]$ of degree $4$ ,

\big(\forall x \in \mathbb R^n:\ f(x) \ge 0\big) \iff \big(\forall \omega \in \Omega:\ f^\omega \text{ is a sum of squares in } \mathbb R[T_1, T_2]\big),

with $\Omega$ the set of 2-partitions of $n$ .

Milestones

Proposition 5.1 (p. 21, quoted from Riener [33, Theorem 4.5]), the degree principle:

\inf_{x \in K} f(x) = \inf_{x \in K \cap A_r} f(x).

Display (5.1) (p. 22), for $r \le n$ :

\inf_{x \in K} f(x) = \min_{\omega \in \Omega}\ \inf_{t \in K^\omega} f^\omega(t).

Hilbert's theorem (p. 23): every non-negative ternary quartic form is a sum of squares.
The step of the proof of Theorem 5.5 (p. 23): a polynomial in two variables of degree at most 4 is non-negative if and only if it is a sum of squares.

Significance

Theorem 5.5 turns non-negativity of a symmetric quartic in any number of variables into $\lfloor n/2 \rfloor$ semidefinite feasibility problems of fixed size, one per 2-partition, each in two variables. This is a certificate scheme that is exact, in contrast with the SOS relaxation in $n$ variables, which fails for the Choi–Lam quartic. Proposition 5.1 and (5.1) are the general mechanism behind it, and they apply to any symmetric problem whose degrees are small relative to $n$ : they underlie the reduced relaxation hierarchy of Theorem 5.2 of the same paper.

All four milestones and the goal are proved results in the literature; the work is formalization. As far as a search of the platform shows, neither the degree principle nor Hilbert's ternary quartic theorem has a machine-checked statement on Prove2Me, and Mathlib has the vocabulary (MvPolynomial.IsSymmetric, IsSumSq) but neither theorem. Hilbert's theorem is a classical result of real algebraic geometry that is reusable far beyond this mission, for example in any SOS-exactness argument in low dimension.

Difficulty

The obvious route to the goal is to apply Hilbert's theorem to each $f^\omega$ , and that is the whole printed proof; it gives only the direction "non-negative implies every $f^\omega$ is SOS". The converse, "every $f^\omega$ SOS implies $f$ non-negative", is not a consequence of Hilbert's theorem: it says that a symmetric quartic attains its infimum, if anywhere, on points with at most two distinct coordinate values, which is the degree principle with $r = \max\{2, \lfloor 4/2 \rfloor\} = 2$ . The paper quotes the degree principle from Riener's earlier work without proof, and it is not available in Mathlib.

Hilbert's theorem itself is the hardest item. It is a statement about all non-negative quartic forms in three variables, with no symmetry to exploit, and every known proof needs substantial real algebraic geometry beyond what Mathlib provides; it is not a computation on a Gram matrix.

Formalization scope

Polynomials are MvPolynomial (Fin n) ℝ; evaluation is MvPolynomial.eval; degree is totalDegree; symmetric is MvPolynomial.IsSymmetric; sum of squares is Mathlib's IsSumSq in the relevant polynomial ring (the empty sum $0$ is allowed, as on the page). An $r$ -partition is encoded by its block map $b : \mathrm{Fin}\ n \to \mathrm{Fin}\ r$ , required to be monotone, surjective and with non-increasing fibre sizes; this is in bijection with the page's $\Omega$ , and $f^\omega$ is the substitution $X_i \mapsto T_{b(i)}$ . Infima in Proposition 5.1 and (5.1) are taken in EReal, so empty feasible sets give $+\infty$ and unbounded problems give $-\infty$ ; no extended-real arithmetic is used.

Disclosed additions and readings, each forced by the page:

$n \ge 2$ in Theorem 5.5. For $n = 1$ there is no 2-partition and $f = X_1^4 - 1$ is a counterexample.
$r \le n$ in (5.1). For $r > n$ there is no $r$ -partition and the right-hand side is $+\infty$ .
"Ternary quartic polynomial" is a ternary quartic form in Hilbert's theorem; the inhomogeneous reading is false.
"Of degree 4" is "degree at most 4" in the step of the proof (milestone 4), since substitution can lower the degree; the goal keeps "degree exactly 4" as printed.

Ruled out: replacing "sum of squares" by non-negativity of $f^\omega$ (which would make the goal Proposition 5.1 alone), real-valued infima (which are $0$ on empty or unbounded sets), or arbitrary maps $\mathrm{Fin}\ n \to \mathrm{Fin}\ 2$ in place of 2-partitions.

Welcome contributions: Hilbert's theorem on ternary quartics in any standard form; homogenization and dehomogenization lemmas for MvPolynomial and IsSumSq; the degree principle, first for $K = \mathbb R^n$ (the case the goal needs) and then with constraints.

Selected references

C. Riener, T. Theobald, L. Jansson Andrén, J. B. Lasserre, Exploiting symmetries in SDP-relaxations for polynomial optimization, Math. Oper. Res. 38(1):122–141, 2013; arXiv:1103.0486v3. https://arxiv.org/abs/1103.0486, https://doi.org/10.1287/moor.1120.0558
C. Riener, On the degree and half-degree principle for symmetric polynomials, J. Pure Appl. Algebra 216(4):850–856, 2012. https://doi.org/10.1016/j.jpaa.2011.08.012
V. Timofte, On the positivity of symmetric polynomial functions. Part I: General results, J. Math. Anal. Appl. 284(1):174–190, 2003. https://doi.org/10.1016/S0022-247X(03)00301-9
D. Hilbert, Über die Darstellung definiter Formen als Summe von Formenquadraten, Math. Ann. 32:342–350, 1888. https://doi.org/10.1007/BF01443605
M. D. Choi, T. Y. Lam, Extremal positive semidefinite forms, Math. Ann. 231:1–18, 1977. https://doi.org/10.1007/BF01360024

7 thms1 active userReviewed

Harmonic Analysis Numerical Analysis Probability·Captain: mikedeng1

Isotropic Gaussian Random Fields on the Sphere: Regularity, Fast Simulation and Stochastic Partial Differential Equations III: Karhunen–Loève Truncation Error ≤ κ^{−β} a.s. for β < (α−2)/2Research Paper

Why approximate a random field on the sphere?

An isotropic Gaussian random field is a spatial random quantity whose probability law is unchanged when the sphere is rotated. Such fields model spatially distributed uncertainty when no direction is preferred. The question in this mission is concrete: if a field is simulated by retaining only finitely many spherical harmonic frequencies, how rapidly does the simulation approach the full field? Lang and Schwab study this question while developing regularity, simulation, and stochastic partial differential equation results for isotropic fields on spheres (Lang and Schwab, 2015). Their §5 separates the error in expected spatial energy from the error seen along an individual sample. The latter is the target here.

The field and its finite approximation

Let $S^2$ be the unit sphere in $\mathbb R^3$ and let $\sigma$ be surface area measure, with $\sigma(S^2)=4\pi$ . A point $y$ has angular coordinates $(\vartheta,\varphi)$ , where $y=(\sin\vartheta\cos\varphi,\sin\vartheta\sin\varphi,\cos\vartheta)$ . Spherical harmonics $Y_{\ell m}$ are the normalized complex functions indexed by a degree $\ell\ge0$ and an order $-\ell\le m\le\ell$ . They form an orthonormal basis of complex $L^2(S^2)$ with this unnormalized surface measure. The real factor $L_{\ell m}(\vartheta)$ is the normalized associated Legendre function appearing in $Y_{\ell m}(\vartheta,\varphi)=L_{\ell m}(\vartheta)e^{im\varphi}$ for $m\ge0$ (§2, pp. 4–5).

The angular power spectrum is a nonnegative sequence $(A_\ell)_{\ell\ge0}$ recording the variance at each harmonic degree. Let $X^1_{\ell m}$ and $X^2_{\ell m}$ be independent standard normal random variables for the indices that occur below. The centered real field used in §5 is the ordered series

T(y)=\sum_{\ell=0}^{\infty}\left(\sqrt{A_\ell}X^1_{\ell0}L_{\ell0}(\vartheta)+\sqrt{2A_\ell}\sum_{m=1}^{\ell}L_{\ell m}(\vartheta)\bigl(X^1_{\ell m}\cos(m\varphi)+X^2_{\ell m}\sin(m\varphi)\bigr)\right).

Its Karhunen–Loève truncation $T^\kappa$ retains the outer sum through degree $\kappa$ . These are the approximations analyzed and simulated in the paper (§5, p. 25). The norm $\|f\|_{L^2(S^2)}$ measures the spatial size of a sample $f$ , while $\|Z\|_{L^p(\Omega;L^2(S^2))}$ takes the $p$ th moment of that spatial norm over randomness. Lemma 5.1 relates this explicit series, in law, to an arbitrary centered isotropic Gaussian field with the same angular power spectrum (pp. 23–24).

Formalization targets

The goal, Corollary 5.4, assumes $C>0$ , $\alpha>2$ , an integer $\ell_0\ge1$ , and the tail condition $A_\ell\le C\ell^{-\alpha}$ for $\ell>\ell_0$ . It asserts almost-sure convergence in spatial $L^2$ and, for each $\beta<(\alpha-2)/2$ , an eventual samplewise bound (p. 28):

\|T-T^\kappa\|_{L^2(S^2)}\le\kappa^{-\beta}\qquad\text{for all sufficiently large }\kappa,\quad\mathbb P\text{-almost surely}.

The attack path retains three intermediate statements from §5. The squared mean-square error equals the exact spectral tail $\sum_{\ell>\kappa}(2\ell+1)A_\ell$ (the proof of Proposition 5.2, p. 26). Proposition 5.2 establishes convergence in $L^2(\Omega;L^2(S^2))$ and the bound

\|T-T^\kappa\|_{L^2(\Omega;L^2(S^2))}\le\widehat C\,\kappa^{-(\alpha-2)/2},\qquad \widehat C^2=C\left(\frac2{\alpha-2}+\frac1{\alpha-1}\right)

for $\kappa\ge\ell_0$ (p. 25). Theorem 5.3 gives the same exponent for every finite $p\ge1$ , with a constant depending only on $p,C,\alpha$ (p. 27). The goal's exponent may approach, but does not include, $(\alpha-2)/2$ .

What the result supplies

The mean-square estimate controls average approximation error, but it does not itself say whether one sequence of simulated fields converges along almost every outcome. Corollary 5.4 supplies that pathwise assertion and a quantitative rate for each exponent below the spectral threshold. It identifies the resolution needed to make the spatial error small for almost every sample, rather than only on average. The threshold directly links harmonic spectral decay to numerical truncation quality.

The cited results are already proved in the paper; the remaining task is to formalize their statements and proofs for the explicit KL model. The definition layer provides a reusable real representation of normalized spherical harmonics and mixed norms on $S^2$ . A completed proof would also make the transition from Gaussian moment estimates to samplewise convergence available as a machine-checked argument in this setting. No claim is made that these results already have machine-checked proofs.

Main difficulty

The spherical harmonics are orthonormal, but an error bound for the full field needs more than termwise estimates. It must control the infinite tail while keeping the harmonic normalization, Gaussian variances, and the surface measure consistent. The passage from an expected error to one bound that eventually holds along almost every sample also requires estimates for arbitrarily high finite moments. A fixed second-moment bound does not yield the full range of exponents in Corollary 5.4. The paper's constant in Proposition 5.2 and the parameter dependence of the constant in Theorem 5.3 therefore matter to the final statement.

Formalization scope

Lean uses EuclideanSpace ℝ (Fin 3) for the sphere. Coordinates $0,1,2$ represent the paper's $y_1,y_2,y_3$ . volume.toSphere supplies surface measure of mass $4\pi$ . Legendre polynomials use Rodrigues' formula; the associated harmonics use Cartesian coordinates through $(y_1+i y_2)^m=\sin^m\vartheta e^{im\varphi}$ , so they are defined at the poles without choosing an angle there. The field is the limit of the ordered partial sums $T^\kappa$ . A nonconvergent sequence receives Lean's arbitrary limit value, but the theorems concern almost-everywhere convergence and norms, where such exceptional values must be shown irrelevant.

Spatial squared norms and mixed $L^p$ norms are extended nonnegative integrals. This keeps nonintegrable functions from taking a false zero norm. Lean's natural numbers include zero; $\ell_0\in\mathbb N$ in the paper is recorded as $\ell_0\ge1$ . Decay is required only above $\ell_0$ , exactly where the paper requires it. Coefficients that enter the series are measurable, jointly independent, and standard normal. The unused coordinates $X^2_{\ell0}$ are zero, as specified in Lemma 5.1; coefficients at invalid indices are unconstrained. The field is the explicit series of p. 25, with Lemma 5.1 supplying the paper's identification in law with any centered isotropic field. In Theorem 5.3 the constant is chosen before the field and probability space, preventing it from depending on a particular spectrum or cutoff. The almost-sure conclusion is a spatial $L^2$ claim, never a pointwise assertion at each sphere point.

The displayed identity on p. 26 omits a square on its left-hand norm, although the neighboring formulas use squared norms. The formal error identity restores the square and the milestone preserves the printed wording. Contributions to the harmonic normalization, exact spectral identity, uniform finite-moment estimates, and the final almost-sure result all fit this mission. The normalizations, the positive cutoff, and the explicit independent Gaussian coefficients rule out vacuous or zero-field encodings.

Selected references

A. Lang and Ch. Schwab, Isotropic Gaussian random fields on the sphere: regularity, fast simulation and stochastic partial differential equations, Annals of Applied Probability 25(6), 2015. arXiv:1305.1170v3

7 thms1 active userReviewed

Combinatorics Graph Theory Mathematical Physics·Captain: mikedeng1

Algorithms for #BIS-Hard Problems on Expander Graphs 2: On Bipartite α-Expanders, the High-Fugacity Hard-Core Partition Function Reduces to Two Kotecký–Preiss Polymer ModelsResearch Paper

Motivation

The hard-core model on a finite graph $G$ at fugacity $\lambda > 0$ weights each independent set $I$ of $G$ by $\lambda^{|I|}$ . Its normalizing constant, the independence polynomial $Z_G(\lambda)$ , is a basic object of statistical physics (a lattice gas with hard-core exclusion) and of combinatorics ( $Z_G(1)$ counts independent sets).

The complexity of approximating $Z_G(\lambda)$ on graphs of maximum degree $\Delta$ is settled for general graphs: below the uniqueness threshold $\lambda_c(\Delta) = (\Delta-1)^{\Delta-1}/(\Delta-2)^{\Delta}$ there is a deterministic approximation scheme (Weitz, STOC 2006, doi:10.1145/1132516.1132538), and above it the problem is NP-hard to approximate. On bipartite graphs the picture is different. Approximately counting independent sets of a bipartite graph defines the class #BIS, whose complexity is a major open problem of approximate counting, and Cai, Galanis, Goldberg, Guo, Jerrum, Štefankovič and Vigoda showed that for $\Delta \ge 3$ and $\lambda > \lambda_c(\Delta)$ the hard-core model on bipartite graphs of maximum degree $\Delta$ is #BIS-hard (arXiv:1311.4839).

One route to partial progress is to find natural classes of bipartite graphs on which these #BIS-hard problems become tractable. Helmuth, Perkins and Regts did this for the hard-core model at high fugacity on the torus $(\mathbb Z/n\mathbb Z)^d$ , using Pirogov–Sinai contour models and the cluster expansion (arXiv:1806.11548). Jenssen, Keevash and Perkins extended the method to abstract polymer models and to all bounded-degree bipartite expanders (arXiv:1807.04804; SIAM J. Comput. 49(4), 2020). This mission formalizes the mathematical core of their Theorem 1.

Setting

Let $G$ be a finite bipartite graph with vertex classes $\mathcal O$ (odd vertices) and $\mathcal E$ (even vertices), $n = |\mathcal O| + |\mathcal E|$ , and maximum degree at most $\Delta$ . For a vertex set $S$ , the vertex boundary $\partial S$ is the set of vertices outside $S$ with a neighbour in $S$ . For $\alpha > 0$ , $G$ is a bipartite $\alpha$ -expander if

|\partial S| \ge (1+\alpha)|S| \quad\text{for all } S \subseteq \mathcal O,\ |S| \le |\mathcal O|/2, \text{ and all } S \subseteq \mathcal E,\ |S| \le |\mathcal E|/2.

A subset of one class is small if it has at most half as many vertices as that class. The hard-core partition function is

Z_G(\lambda) = \sum_{I \in \mathcal I(G)} \lambda^{|I|},

with $\mathcal I(G)$ the independent sets of $G$ . A number $\hat Z$ is an $\varepsilon$ -relative approximation to $Z$ if $e^{-\varepsilon}\hat Z \le Z \le e^{\varepsilon}\hat Z$ .

$G^2$ is the graph on the same vertices in which two distinct vertices are adjacent when their distance in $G$ is at most $2$ ; a set is $G^2$ -connected when it induces a connected subgraph of $G^2$ . An even polymer is a nonempty, small, $G^2$ -connected set $\gamma \subseteq \mathcal E$ ; odd polymers are defined in $\mathcal O$ . Two polymers are compatible if their distance in $G$ exceeds $2$ . Each polymer has the weight

w_\gamma = \frac{\lambda^{|\gamma|}}{(1+\lambda)^{|\partial\gamma|}},

and the polymer partition functions are $\Xi^{\mathcal E}(G) = \sum_\Gamma \prod_{\gamma\in\Gamma} w_\gamma$ , summed over the families $\Gamma$ of pairwise compatible even polymers (the empty family included), and $\Xi^{\mathcal O}(G)$ likewise. Even polymers describe deviations from the ground state "all odd vertices occupied", and odd polymers from the other ground state.

Formalization targets

Goal: the deterministic core of Theorem 1

For $\alpha > 0$ , $\Delta \ge 3$ , every bipartite $\alpha$ -expander $G$ of maximum degree at most $\Delta$ on $n \ge 3$ vertices, and every

\lambda > \max\left\{(2e^3\Delta^4)^{1/\alpha},\ e^{11/\alpha}\right\},

$\tilde Z_G(\lambda) = (1+\lambda)^{|\mathcal O|}\,\Xi^{\mathcal E}(G) + (1+\lambda)^{|\mathcal E|}\,\Xi^{\mathcal O}(G)$ is an $e^{-n}$ -relative approximation to $Z_G(\lambda)$ ;
both polymer models satisfy the Kotecký–Preiss condition with $g(\gamma) = |\gamma|$ : for every polymer $\gamma$ ,

\sum_{\gamma' \text{ incompatible with } \gamma} w_{\gamma'}\, e^{2|\gamma'|} \le |\gamma|.

Milestones

In the order of the paper's proof: Lemma 18 (every independent set has a small side); the identity $\tilde Z_G(\lambda) = Z_G(\lambda) + \sum_{I \text{ sparse}} \lambda^{|I|}$ ; the size bound $(2+\alpha)|I| \le n$ for sparse independent sets; Lemma 20 (part 1 of the goal); the weight bound $w_\gamma \le (1+\lambda)^{-\alpha|\gamma|}$ ; the count of at most $(e\Delta^2)^t$ $G^2$ -connected $t$ -sets through a vertex; and inequality (8), $\sum_{\gamma' \ni v} (1+\lambda)^{-\alpha|\gamma'|} e^{2|\gamma'|} \le 1/\Delta^2$ .

Significance

The two parts of the goal are exactly what Theorem 8 of the paper (adapted from Helmuth, Perkins and Regts) consumes: given a polymer model satisfying the Kotecký–Preiss condition, the truncated cluster expansion of $\log \Xi$ yields an FPTAS and, through self-reducibility, a polynomial-time sampler. Together they give a deterministic approximate counting algorithm for a #BIS-hard problem on a natural graph class, at fugacities far above $\lambda_c(\Delta)$ , the regime in which the problem is hard on general bipartite graphs. The same template (reduction to polymer models around ground states, then Kotecký–Preiss) underlies the paper's results for the Potts model, for random regular bipartite graphs and for proper colourings, and a large later literature on algorithms at low temperature.

The result is proved in the paper; to our knowledge none of it has been machine-checked. A formalization adds a precise treatment of the degenerate cases (see below), a reusable formal definition of abstract polymer models over vertex sets, and the elementary but intricate bijection between compatible polymer families and sparse sets.

Difficulty

Each step is elementary, and the difficulty lies in the bookkeeping. The reduction needs an exact correspondence between families of pairwise compatible polymers and sparse subsets of a class, and an exact double count over independent sets. The quantitative step of Lemma 20 compares the total weight of sparse independent sets, which have at most $n/(2+\alpha)$ vertices, with $Z_G(\lambda) \ge \lambda^{n/2}$ ; the printed last inequality, $2^n\lambda^{-\alpha n/(4+2\alpha)} \le e^{-n}$ , follows from $\lambda > e^{11/\alpha}$ only for $\alpha$ up to about $1.25$ , and larger $\alpha$ forces both classes to have at most nine vertices, a finite range that needs its own argument. The Kotecký–Preiss half needs the count of connected sets in a bounded-degree graph (Lemma 14 of the paper, from Galvin and Kahn), applied to $G^2$ , and a geometric series.

Formalization scope

The algorithmic conclusion of Theorem 1 (an FPTAS and a polynomial-time sampling algorithm, with running time $(n/\varepsilon)^{O(\log\Delta)}$ ) is not formalized: Mathlib has no machine model and the running times carry unspecified constants. The goal is the mathematics the algorithm rests on: the reduction to two polymer models and the Kotecký–Preiss condition for both. The cluster expansion and Theorem 8 are not part of the mission.

Conventions. The graph is a SimpleGraph V on a finite type, with $\mathcal O$ a Finset V and $\mathcal E$ its complement; bipartiteness is a hypothesis. The fugacity is lam. " $|S| \le |\mathcal O|/2$ " is 2 * #S ≤ #O in $\mathbb N$ . Distances use the extended distance SimpleGraph.edist, so vertices in different components are never close. The Kotecký–Preiss sum ranges over the polymers of the same class incompatible with $\gamma$ , including $\gamma$ itself. Polymers are capped at half of their own class, not at $n/2$ ; the condition without this cap, or with compatibility in place of incompatibility, would be a different statement.

Two hypotheses differ from the page. Theorem 1 states the threshold as $\lambda > C\Delta^{4/\alpha}$ for an absolute constant $C$ ; the goal uses the threshold its proof uses (§4.3). The hypothesis $n \ge 3$ is added: on the edgeless graph with one vertex in each class the expansion condition is vacuous, no side of the independent set $V$ is small, and Lemma 18 and Lemma 20 fail.

A complete development needs: the bijection between compatible families and sparse sets, Lemma 14 for $G^2$ , and real-power estimates. The polymer-model and graph-power definitions are reusable for the sibling missions of this series. Proofs of individual milestones are welcome independently.

Selected references

M. Jenssen, P. Keevash, W. Perkins, Algorithms for #BIS-hard problems on expander graphs, SIAM J. Comput. 49(4) (2020) 681–710. doi:10.1137/19M1286669, arXiv:1807.04804
T. Helmuth, W. Perkins, G. Regts, Algorithmic Pirogov–Sinai theory, Probab. Theory Related Fields 176 (2020) 851–895. arXiv:1806.11548
R. Kotecký, D. Preiss, Cluster expansion for abstract polymer models, Comm. Math. Phys. 103 (1986) 491–498. doi:10.1007/BF01211762
J.-Y. Cai, A. Galanis, L. A. Goldberg, H. Guo, M. Jerrum, D. Štefankovič, E. Vigoda, #BIS-hardness for 2-spin systems on bipartite bounded degree graphs in the tree non-uniqueness region, J. Comput. System Sci. 82 (2016) 690–711. arXiv:1311.4839
D. Weitz, Counting independent sets up to the tree threshold, STOC 2006, 140–149. doi:10.1145/1132516.1132538
D. Galvin, J. Kahn, On phase transition in the hard-core model on $\mathbb Z^d$ , Combin. Probab. Comput. 13 (2004) 137–164. doi:10.1017/S0963548303005947

10 thms1 active userReviewed

Linear Optimization Machine Learning Statistics·Captain: mikedeng1

Fast Rates for Contextual Linear Optimization 1: Under the Margin Condition, ERM over a Policy Class of Natarajan Dimension η Has Regret O(B(η log(|Z∠|+1) log(n+1)/n)^((1+α)/(2+α)))Research Paper

Motivation

Many operational decisions are linear programs whose cost vector is uncertain but partly predictable: shortest-path routing with uncertain travel times, portfolio choice with uncertain returns, shipment planning with uncertain costs. Before deciding, one observes features $X$ (traffic, market signals) correlated with the costs $Y$ . Contextual linear optimization asks for a policy mapping features to decisions that minimizes the conditional expected cost, learned from past data $(X_1, Y_1), \dots, (X_n, Y_n)$ .

Two families of methods compete. Estimate-then-optimize fits a regression of $Y$ on $X$ and plugs it into the optimizer. Empirical risk minimization (ERM) and its "integrated" variants choose a policy directly to minimize the empirical decision cost. A widespread view holds that the integrated approach should win because it targets the decision cost. Hu, Kallus and Mao (arXiv:2011.03030, Management Science 2022) compare the two through their regret rates. Slow, noise-independent rates of order $n^{-1/2}$ do not separate them. The separation appears under a margin (noise) condition controlling how often the problem is nearly dual-degenerate. This mission formalizes the paper's fast rate for ERM, Theorem 6.

Timeline. Margin conditions for classification go back to Mammen–Tsybakov (1999) and Tsybakov (2004); Massart–Nédélec (2006) obtained the corresponding fast rates for ERM over VC classes. El Balghiti, Elmachtoub, Grigas and Tewari (2019) gave slow generalization bounds for decision-focused losses in terms of the Natarajan dimension. Hu, Kallus and Mao (2020, revised 2021) proved the fast rate for ERM over policy classes of finite Natarajan dimension, a matching lower bound, and a faster rate for estimate-then-optimize.

Setting

The decision set is a polytope $\mathcal Z = \{z \in \mathbb R^d : Az \le b\}$ , nonempty, with $\|z\| \le B$ on $\mathcal Z$ for some $B > 0$ ; $\mathcal Z^\angle$ is its finite set of extreme points. The pair $(X, Y) \in \mathbb R^p \times \mathbb R^d$ has $\|Y\| \le 1$ , and $f^*(x) = \mathbb E[Y \mid X = x]$ . The optimal set at $x$ is $\mathcal Z^*(x) = \arg\min_{z \in \mathcal Z} f^*(x)^\top z$ .

A policy is a map $\pi : \mathbb R^p \to \mathcal Z^\angle$ . A data-driven policy $\hat\pi$ maps a sample $\mathcal D$ of $n$ i.i.d. draws to a policy, and its regret is

\mathrm{Regret}(\hat\pi) = \mathbb E_{\mathcal D}\mathbb E_X\bigl[f^*(X)^\top\hat\pi(X) - \min_{z \in \mathcal Z} f^*(X)^\top z\bigr].

Given a class $\Pi$ of policies, $\hat\pi^{\mathrm{ERM}}_\Pi$ returns a member of $\Pi$ minimizing $\frac1n\sum_i Y_i^\top\pi(X_i)$ .

The gap $\Delta(x)$ is the difference between the best value over suboptimal extreme points and the optimal value, set to $0$ when every point of $\mathcal Z$ is optimal. Assumption 2 (noise condition) with parameters $\alpha, \gamma \ge 0$ requires

\mathbb P_X\bigl(0 < \Delta(X) \le \delta\bigr) \le (\gamma\delta/B)^\alpha \qquad \text{for all } \delta > 0.

The Natarajan dimension of $\Pi$ is the largest $k$ for which there are points $x_1, \dots, x_k$ and labels $s_i \ne s'_i$ such that every pattern of choices between $s_i$ and $s'_i$ is realized by some $\pi \in \Pi$ .

Formalization targets

Goal: Theorem 6

If Assumption 2 holds, $\mathbb P(|\mathcal Z^*(X)| > 1) = 0$ , $\Pi$ has Natarajan dimension at most $\eta$ , and $\Pi$ contains an optimal policy $\pi^*$ , then for a constant $C(\alpha, \gamma)$ depending only on $\alpha, \gamma$ ,

\mathrm{Regret}(\hat\pi^{\mathrm{ERM}}_\Pi) \le C(\alpha, \gamma)\,B\left(\frac{\eta\log(|\mathcal Z^\angle| + 1)\log(n + 1)}{n}\right)^{\frac{1+\alpha}{2+\alpha}}.

The constant is existential and uniform over all dimensions, polytopes, distributions, classes, $\eta$ and $n$ ; the goal fixes no numerical value.

Milestones

With $d(\pi, \pi') = \frac1B\mathbb E_X[f^*(X)^\top(\pi'(X) - \pi(X))]$ and $d_\Delta(\pi, \pi') = \mathbb P_X(\pi(X) \ne \pi'(X))$ :

Lemma 1: $d(\pi^*, \pi) \le 2d_\Delta(\pi^*, \pi)$ and $d_\Delta(\pi^*, \pi) \le c_1 d(\pi^*, \pi)^{\alpha/(\alpha+1)}$ with $c_1 = (\alpha\gamma^\alpha)^{-\alpha/(\alpha+1)}(\alpha+1)\gamma^\alpha$ .
Lemma 2 (Bousquet's inequality): for a countable class bounded by $\bar H$ with second moments at most $\delta^2$ , $S - \mathbb E S$ exceeds $\sqrt{2(\delta^2 + 4\bar H\mathbb E S)t/n} + 2\bar Ht/(3n)$ with probability at most $e^{-t}$ .
Lemma 3: the localized excess-loss process satisfies $\mathbb E_{\mathcal D}[\sup_{h \in \mathcal H_\delta}(\mathbb E_n h - \mathbb E_P h)] \le (1+\sqrt2)C_0\sqrt{5\eta\log(|\mathcal Z^\angle|^2+1)\log(n+1)/n}\,\delta$ for $n$ above a threshold.
Tail bound (proof of Theorem 6, p. 27): for $t \ge 1$ , $\mathbb P(d(\pi^*, \hat\pi^{\mathrm{ERM}}_\Pi) \ge K t(\bar V\log(n+1)/n)^{(1+\alpha)/(2+\alpha)}) \le e^{-t}$ with $\bar V = 5\eta\log(|\mathcal Z^\angle|^2+1)$ and $n \ge c\bar V\log(n+1)$ .

Significance

Theorem 6 shows that the regret of ERM improves from $n^{-1/2}$ to $n^{-(1+\alpha)/(2+\alpha)}$ when the instance is rarely near dual degeneracy. With $\alpha = 1$ , the generic case when $X$ has a bounded density and $f^*$ is linear, the rate is $n^{-2/3}$ . Theorem 7 of the same paper (mission 2 of this series) shows that the exponent is optimal for any method that uses only the policy class. Theorem 8 (mission 3) shows that estimate-then-optimize can reach $n^{-(1+\alpha)/2}$ , which is the paper's case against the conventional preference for integrated methods.

The result is proved in the paper; no machine-checked proof is known. Formalizing it adds a checked fast-rate theorem for a decision-focused learning method, a Lean statement of Bousquet's inequality in the form used throughout statistical learning theory, and a localized empirical-process bound for classes of finite Natarajan dimension.

Difficulty

The slow rate follows from uniform convergence of the empirical cost over $\Pi$ . This argument cannot give more than $n^{-1/2}$ : it bounds the deviation of every policy by the same worst-case amount, ignoring that near-optimal policies have small variance. The fast rate needs a variance–mean relation (Lemma 1, which is where the noise condition and the uniqueness assumption $\mathbb P(|\mathcal Z^*(X)| > 1) = 0$ enter), a concentration inequality that exploits small variance (Lemma 2), and a localized complexity bound (Lemma 3), combined over shells of the class. Lemma 2 is itself a deep result whose known proofs go through the entropy method. Lemma 3 rests on chaining and on bounding the pseudo-dimension of the excess-loss class by the Natarajan dimension, neither of which is in Mathlib.

Formalization scope

All declarations live in the namespace FastCLO.ERM. Conventions:

Spaces are EuclideanSpace ℝ (Fin k). The polytope is a structure carrying $A$ , $b$ , $B > 0$ , nonemptiness and the bound $\|z\| \le B$ ; $|\mathcal Z^\angle|$ is the cardinality of Set.extremePoints, whose finiteness is a proof obligation, not a hypothesis.
The distribution is given by the law $\mu$ of $X$ and a Markov kernel $\kappa$ for $Y$ given $X$ , with $\|Y\| \le 1$ $\kappa(x)$ -almost surely for every $x$ ; $f^*$ is the kernel mean; data are Measure.pi of $\mu \otimes \kappa$ .
Regret is measured against the optimal value; this equals the paper's $f^*(X)^\top(\hat\pi(X) - \pi^*(X))$ .
ERM is any selection from the empirical argmin over the whole class; the paper's tie-breaking order is not encoded. The ERM rule is assumed jointly measurable in the data and the feature (an added hypothesis, so that the regret is a genuine integral).
" $\pi^* \in \Pi$ " means some member of $\Pi$ is optimal at almost every $x$ ; "Natarajan dimension at most $\eta$ " means $\Pi$ does not shatter $\eta + 1$ points.
Added hypotheses: $n \ge 1$ wherever the paper divides by $n$ ; $\bar H > 0$ in Lemma 2; measurability of the supremum in Lemma 3; $\eta \ge 1$ in the tail bound (the paper's $\epsilon_n > 0$ ). Constants ( $C$ , $C_0$ , $K$ , $c$ ) are quantified before everything they are uniform over.

A statement in which the regret integrated the empirical cost instead of $f^*$ , or in which ERM minimized over a subset of the class, or in which the constant could depend on the instance, would be a different theorem; the Lean statements rule these out by construction.

Needed infrastructure: Bousquet's (or Talagrand's) inequality, symmetrization and Dudley chaining for empirical processes, packing bounds for classes of finite pseudo-dimension, and the Natarajan-to-pseudo-dimension reduction. These are reusable far beyond this mission; contributions of any of them are welcome.

Selected references

Y. Hu, N. Kallus, X. Mao, Fast Rates for Contextual Linear Optimization, Management Science, 2022; arXiv:2011.03030v3, 2021. https://arxiv.org/abs/2011.03030
O. Bousquet, A Bennett concentration inequality and its application to suprema of empirical processes, Comptes Rendus Mathématique 334(6), 2002. https://doi.org/10.1016/S1631-073X(02)02292-6
P. Massart, É. Nédélec, Risk bounds for statistical learning, Annals of Statistics 34(5), 2006. https://doi.org/10.1214/009053606000000786
A. B. Tsybakov, Optimal aggregation of classifiers in statistical learning, Annals of Statistics 32(1), 2004. https://doi.org/10.1214/aos/1079120131
O. El Balghiti, A. N. Elmachtoub, P. Grigas, A. Tewari, Generalization Bounds in the Predict-then-Optimize Framework, NeurIPS 2019; arXiv:1905.11488. https://arxiv.org/abs/1905.11488
B. K. Natarajan, On learning sets and functions, Machine Learning 4, 1989. https://doi.org/10.1007/BF00114804

10 thms1 active userReviewed

Combinatorics Graph Theory Mathematical Physics·Captain: mikedeng1

Algorithms for #BIS-Hard Problems on Expander Graphs 1: On α-Expanders of Maximum Degree Δ, the Low-Temperature Potts Partition Function Reduces to a Kotecký–Preiss Polymer ModelResearch Paper

Motivation

The ferromagnetic Potts model assigns a larger weight to a coloring when more adjacent vertices have the same color. Computing its partition function is an approximate counting problem with connections to statistical physics and counting complexity. For three or more colors, Goldberg and Jerrum established #BIS-hardness of approximation on general graphs, and Galanis, Štefankovič, Vigoda, and Yang refined the hardness result for bounded-degree bipartite graphs Goldberg–Jerrum, Galanis et al.. These results make it useful to identify graph classes where the partition sum can still be approximated efficiently.

Jenssen, Keevash, and Perkins proved that edge expansion supplies such a class at sufficiently large inverse temperature. Their Theorem 3 gives an FPTAS and a polynomial-time sampling algorithm for the $q$ -color ferromagnetic Potts model on finite $\alpha$ -expanders of maximum degree $\Delta$ , when $\alpha>0$ , $\Delta\ge3$ , $q\ge2$ , and $\beta\ge(4+2\log(q\Delta))/\alpha$ Jenssen–Keevash–Perkins. This mission records the mathematical reduction and the polymer convergence condition on which their algorithmic conclusion rests.

Setting

Let $G=(V,E)$ be a finite simple graph, let $n=|V|$ , and let $e(G)=|E|$ . A coloring $\omega:V\to[q]$ gives each vertex one of $q$ colors. Write $m(G,\omega)$ for the number of edges whose endpoints receive the same color. The Potts partition function at inverse temperature $\beta$ is

Z_{G,q}(\beta)=\sum_{\omega:V\to[q]}\exp\bigl(\beta m(G,\omega)\bigr).

For $S\subseteq V$ , its edge boundary $\partial_e S$ consists of the edges with exactly one endpoint in $S$ . The graph is an $\alpha$ -expander if $|\partial_e S|\ge\alpha|S|$ whenever $2|S|\le n$ . The maximum-degree assumption means that each vertex has at most $\Delta$ neighbors. All logarithms here are natural logarithms.

A color $j$ is a strict majority in $\omega$ when $2|\omega^{-1}(j)|>n$ . Let $Z_G^j(\beta)$ be the Potts sum over colorings with that majority, and let $Z_G^*(\beta)=\sum_{j\in[q]}Z_G^j(\beta)$ . Because two colors cannot each occupy more than half the vertices, these sectors do not overlap. The monochromatic colorings are the model's ground states at positive $\beta$ .

A polymer $\gamma$ is a nonempty vertex set for which the induced graph $G[\gamma]$ is connected and $2|\gamma|\le n$ . Let $\nabla(\gamma)$ be all edges with at least one endpoint in $\gamma$ . Two polymers are compatible when the distance between every vertex of one and every vertex of the other exceeds one. In particular, overlapping or adjacent polymers are incompatible. With $Z_{G[\gamma],q-1}(\beta)$ the Potts sum on the induced graph using the other $q-1$ colors, define

w_\gamma=\exp\bigl(-\beta|\nabla(\gamma)|\bigr)Z_{G[\gamma],q-1}(\beta),\qquad \Xi(G)=\sum_{\Gamma\text{ pairwise compatible}}\prod_{\gamma\in\Gamma}w_\gamma.

The sum includes the empty family. An $\varepsilon$ -relative approximation $\widehat Z$ to $Z$ means $e^{-\varepsilon}\widehat Z\le Z\le e^\varepsilon\widehat Z$ Jenssen–Keevash–Perkins, Definitions 10–11.

Formalization targets

The goal is the deterministic core of Theorem 3. For a nonempty $\alpha$ -expander with the degree, color, and temperature bounds above, the explicit polymer expression approximates the Potts partition sum:

\widehat Z=q\exp\bigl(\beta e(G)\bigr)\Xi(G),\qquad e^{-2e^{-n}}\widehat Z\le Z_{G,q}(\beta)\le e^{2e^{-n}}\widehat Z.

The error $2e^{-n}$ is the composition of the two $e^{-n}$ -relative approximations in Lemmas 12 and 13; the paper does not print it as a separate constant. The same goal also asserts the Kotecký–Preiss condition, with the paper's decay function $g(\gamma)=|\gamma|$ , for every polymer $\gamma$ :

\sum_{\gamma':\,d(\gamma',\gamma)\le1}w_{\gamma'}e^{2|\gamma'|}\le|\gamma|.

The milestone list follows the source's stated claims: Lemma 12 bounds the contribution outside the strict-majority sectors; Lemma 13 compares one sector with $e^{\beta e(G)}\Xi(G)$ ; the weight bound controls individual polymers; Lemma 14 counts connected induced subgraphs containing a specified vertex; and displayed inequality (5) bounds the resulting per-vertex sum Jenssen–Keevash–Perkins, pp. 13–16.

Significance

The reduction makes a Potts partition sum on an expanding graph accessible through a finite polymer model whose weights have controlled decay. The Kotecký–Preiss condition is a quantitative convergence criterion for abstract polymer expansions Kotecký–Preiss. In this setting the two statements provide the mathematical hypotheses used with the algorithmic framework cited by the paper Helmuth–Perkins–Regts. Without the approximation, computing the polymer sum would not give a controlled Potts estimate; without the convergence condition, the cited framework would not apply at the stated temperature threshold.

The paper proves the mathematical and algorithmic results. This mission supplies Lean definitions and compile-checked statements, with proofs still to be formalized. A completed development would give reusable formal accounts of finite Potts sums, strict-majority sectors, graph edge expansion, polymer compatibility and weights, and the connected-set counting bound that the paper cites from Galvin and Kahn Galvin–Kahn.

Difficulty

The tempting approximation is to count only monochromatic colorings. That discards all nearby colorings, whose total weight matters even at low temperature. The polymer model retains connected deviations from a monochromatic coloring, but it also admits collections whose union is larger than half the graph. Controlling the weight of these extra configurations is part of the approximation statement. Separately, the convergence criterion sums over every polymer within distance one of a given polymer. A bound on one weight does not control that sum unless the number of connected vertex sets of each size is also bounded. These are the distinct estimates captured by Lemmas 12–14 and inequality (5) Jenssen–Keevash–Perkins, §3.

Formalization scope

The Lean representation uses SimpleGraph V on a finite vertex type. Vertex sets are finite sets, the edge boundary counts each crossing edge once through its orientation from inside to outside, and polymer distance is extended graph distance, so disconnected components are infinitely far apart. Strict-majority colorings use $2|\omega^{-1}(j)|>n$ ; expansion and polymers use the non-strict bound $2|S|\le n$ . The polymer weight uses the full incident-edge set $\nabla(\gamma)$ and the induced Potts sum on $q-1$ colors. The empty compatible family contributes one to $\Xi(G)$ .

The vertex set is required to be nonempty in the goal and approximation lemmas: for $n=0$ , the strict-majority sum is zero while the Potts partition sum is one. Lemma 14 states $\Delta\ge1$ because its printed bound is false for an isolated vertex with $\Delta=0$ . The weight bound states $\beta\ge0$ , which is implied by the goal's threshold. These are the only additional domain pins. The stated goal uses the paper's exact $\Delta\ge3$ , $q\ge2$ , and $\beta\ge(4+2\log(q\Delta))/\alpha$ ; no free approximation value or freely chosen polymer family can trivialize it.

The algorithm and its running time are out of scope because this Mathlib environment has no machine model for the FPTAS and the paper uses unquantified big-O running times. The goal is the mathematical reduction and Kotecký–Preiss hypothesis consumed by Theorem 8. Contributions that establish the five milestone statements, the color-symmetry identity, or the combination of their bounds are useful; the finite graph and partition-sum definitions are reusable beyond this mission.

Selected references

M. Jenssen, P. Keevash, and W. Perkins, Algorithms for #BIS-Hard Problems on Expander Graphs, SIAM Journal on Computing 49(4), 2020. DOI.
R. Kotecký and D. Preiss, Cluster Expansion for Abstract Polymer Models, Communications in Mathematical Physics 103, 1986. DOI.
D. Galvin and J. Kahn, On Phase Transition in the Hard-Core Model on $\mathbb Z^d$ , Combinatorics, Probability and Computing 13(2), 2004. DOI.
L. A. Goldberg and M. Jerrum, Approximating the Partition Function of the Ferromagnetic Potts Model, Journal of the ACM 59(5), 2012. arXiv.
A. Galanis, D. Štefankovič, E. Vigoda, and L. Yang, Ferromagnetic Potts Model: Refined #BIS-Hardness and Related Results, SIAM Journal on Computing 45(6), 2016. DOI.
T. Helmuth, W. Perkins, and G. Regts, Algorithmic Pirogov–Sinai Theory, Probability Theory and Related Fields, 2020. DOI.

7 thms1 active userReviewed

Harmonic Analysis Probability·Captain: mikedeng1

Isotropic Gaussian Random Fields on the Sphere: Regularity, Fast Simulation and Stochastic Partial Differential Equations II: Σ A_ℓ ℓ^{1+β} < ∞ Gives a Continuous Modification, γ-Hölder for γ < β/2Research Paper

Motivation

A random field on a sphere assigns a random value to every direction. Such fields appear when the underlying data are directional, including spherical models in spatial statistics and geophysics. The covariance of an isotropic field can be recorded by an angular power spectrum: one nonnegative number for each spherical harmonic degree. This changes the sample regularity question into a concrete spectral question. How fast must these numbers decay so that a realization is continuous, and how regular can that realization be? Lang and Schwab, 2015 give a sufficient summability condition and an exact range of Hölder exponents in their Theorem 4.5.

The question matters when a field is evaluated on a mesh or represented by finitely many spherical harmonics. A covariance function can be regular even when the original version of a random field has badly chosen values on null sets. The useful result is therefore the existence of one regular modification: at each fixed sphere point it agrees with the given field almost surely, while its sample paths are regular across the entire sphere. The paper treats this sample path result in §4, separately from its spectral characterization of covariance regularity in §3 and its later simulation and stochastic heat equation results.

Setting

Write $S^2=\{x\in\mathbb R^3:\|x\|=1\}$ for the unit sphere. Its geodesic distance is $d(x,y)=\arccos\langle x,y\rangle$ , the length of the shorter great circle arc between $x$ and $y$ . A random field $T$ is a jointly measurable map from a probability space times $S^2$ to the real numbers. A field is Gaussian when every finite collection of its values has a joint Gaussian distribution. Isotropy says that rotating all observation points together does not change that joint distribution. These are the conventions of Definition 2.1 in the paper.

For each degree $\ell\ge0$ , let $P_\ell$ be the Legendre polynomial normalized by $P_\ell(1)=1$ , and let $A_\ell\ge0$ be its angular power. The field has a constant mean and covariance determined by $(A_\ell)$ :

\operatorname{Cov}(T(x),T(y)) =\sum_{\ell=0}^{\infty}A_\ell\frac{2\ell+1}{4\pi}P_\ell(\langle x,y\rangle).

Because $\langle x,y\rangle=\cos d(x,y)$ , the same covariance is expressed by the distance kernel $k(r)=\sum_{\ell\ge0}A_\ell(2\ell+1)P_\ell(\cos r)/(4\pi)$ for $0\le r\le\pi$ . A modification $T'$ of $T$ means $T'(x)=T(x)$ almost surely for each fixed $x$ ; it need not agree on one common full measure set at every $x$ . The paper's Assumption 4.1, specialized to $S^2$ , asks for finiteness of $\sum_{\ell\ge0}A_\ell\ell^{1+\beta}$ .

Formalization targets

Goal: sample regularity

For $0<\beta\le2$ , the target is Theorem 4.5 of Lang and Schwab:

\sum_{\ell=0}^{\infty}A_\ell\ell^{1+\beta}<\infty \quad\Longrightarrow\quad \exists\,T'\text{ modifying }T\text{ with paths Hölder of every order }0<\gamma<\beta/2.

The same modification serves every eligible exponent. The result leaves the Hölder constant free to depend on the sample and the exponent, as it must.

Supporting targets

The four milestones follow the source's statements and its proof order. The Legendre polynomial bounds on p. 16 lead to Lemma 4.2, $|k(0)-k(r)|\le C_\beta r^\beta$ for $r\in[0,\pi]$ and $\beta\in[0,2]$ . Lemma 4.3 transfers this to $\mathbb E|T(x)-T(y)|^{2p}\le C_{\beta,p}d(x,y)^{\beta p}$ for every positive integer $p$ . Theorem 4.4 is a Kolmogorov–Chentsov theorem for any random field on $S^2$ : a moment exponent $2+\varepsilon p$ produces a continuous modification with every Hölder exponent below $\varepsilon$ . The Gaussian and isotropic hypotheses belong to Lemma 4.3 and the goal; they are absent from Theorem 4.4.

Significance

The theorem provides a checkable bridge from a harmonic description of a field to sample path behavior. A practitioner can estimate or impose decay of the angular power spectrum, then know that a version of the field admits interpolation on the sphere with any exponent below $\beta/2$ . The endpoint $\beta/2$ is not asserted. The moment estimate and the spherical modification theorem can also be reused when studying fields produced by other models; in particular, Theorem 4.4 needs no Gaussian assumption.

The result was proved in the 2015 paper; this mission concerns its machine checked formalization. Mathlib supplies Gaussian process and measure theory interfaces, but the paper's sphere distance, Legendre normalization, angular kernel and spherical version of Kolmogorov–Chentsov must be connected. A platform goal for a Kolmogorov–Chentsov theorem on $[0,\infty)$ uses a different index space and hypotheses, so it does not cover the present milestone. The finished development will provide a reusable sphere indexed modification theorem as well as the paper's specific spectral criterion.

Difficulty

A bound on the covariance kernel controls the second moment of field increments, but it does not by itself supply one continuous version with a common pathwise regularity statement. The desired exponent concerns values at uncountably many points, whereas the definition of modification gives an almost sure equality separately at each point. The gap is visible even for simple processes: changing a field at one random location can preserve each fixed point's law while destroying continuity of individual paths. The sphere also carries a two dimensional geodesic metric, so a one dimensional modification theorem indexed by time cannot be substituted without a new argument.

Formalization scope

Lean represents $S^2$ as the unit metric sphere in three dimensional Euclidean space. Coordinates have indices $0,1,2$ for the paper's $1,2,3$ . All regularity statements use $d(x,y)=\arccos\langle x,y\rangle$ , not the subtype's chord distance. Rodrigues' formula defines $P_\ell$ , and the kernel is a real infinite sum with its factor $(2\ell+1)/(4\pi)$ . The spectrum is nonnegative and has $\sum(2\ell+1)A_\ell<\infty$ as part of the field model, matching the finite variance convention used in §2. The covariance formulation allows a nonzero constant mean: Theorem 4.5 does not require centering.

The moment inequalities use extended nonnegative integrals, avoiding a default zero for nonintegrable real integrals. The paper's positive integers are expressed with an explicit $1\le p$ because Lean's naturals include zero. Real powers follow the usual convention: the degree zero term of $\ell^{1+\beta}$ is zero when $\beta\ge0$ . On compact $S^2$ , local Hölder continuity gives a global constant for each path and exponent. Exceptional sample paths may be redefined, so the formal conclusion states continuity and Hölder regularity for every sample of the chosen modification. The modification retains pointwise almost sure agreement and measurable evaluations; omitting agreement would make the goal trivial.

Contributions can address Legendre inequalities, covariance and Gaussian moment calculations, and a general Kolmogorov–Chentsov theorem for compact manifolds. The latter is reusable beyond this paper. The auxiliary Legendre and kernel definitions are also available to later spherical field missions.

Selected references

A. Lang and Ch. Schwab, Isotropic Gaussian random fields on the sphere: regularity, fast simulation and stochastic partial differential equations, Annals of Applied Probability 25(6), 2015, arXiv:1305.1170v3, DOI:10.1214/14-AAP1067.

7 thms1 active userReviewed

Numerical Analysis Partial Differential Equations Probability·Captain: mikedeng1

Isotropic Gaussian Random Fields on the Sphere: Regularity, Fast Simulation and Stochastic Partial Differential Equations IV: Heat-Equation Spectral Truncation Error ≤ κ^{−β} a.s. for β < α/2Research Paper

Motivation

Stochastic partial differential equations on the sphere model quantities that live on the surface of the Earth or of the sky and are perturbed by spatially correlated noise: temperature anomalies, geophysical fields, fluctuations of the cosmic microwave background. The simplest such model is the stochastic heat equation on the unit sphere $\mathbb S^2$ with additive isotropic noise. Because the noise is isotropic and the Laplace–Beltrami operator is diagonal in the spherical harmonics, the equation decouples into one scalar Ornstein–Uhlenbeck equation per harmonic, and the solution can be simulated exactly in law by truncating its spherical-harmonic expansion at a degree $\kappa$ . The practical question is how fast this spectral truncation converges, in mean square and along a single simulated path.

A. Lang and Ch. Schwab answer this in §7 of Isotropic Gaussian random fields on the sphere: regularity, fast simulation and stochastic partial differential equations (arXiv:1305.1170v3, Ann. Appl. Probab. 25(6), 2015). Their rates are expressed through the decay of the angular power spectrum of the noise, the same quantity that governs the sample regularity and the Karhunen–Loève truncation of isotropic Gaussian random fields in the earlier sections of the paper.

Setting

Let $\mathbb S^2\subset\mathbb R^3$ be the unit sphere with surface measure $\sigma$ (total mass $4\pi$ ) and $L^2(\mathbb S^2)$ the real square-integrable functions with norm $\|f\|^2_{L^2(\mathbb S^2)}=\int|f|^2d\sigma$ . The spherical harmonics $Y_{\ell m}$ , $\ell\ge0$ , $|m|\le\ell$ , are built from the Legendre polynomials $P_\ell(\mu)=2^{-\ell}(\ell!)^{-1}\frac{d^\ell}{d\mu^\ell}(\mu^2-1)^\ell$ ; the functions $Y_{\ell0}$ , $\sqrt2\operatorname{Re}Y_{\ell m}$ , $\sqrt2\operatorname{Im}Y_{\ell m}$ ( $1\le m\le\ell$ ) form a real orthonormal basis of the degree- $\ell$ harmonics, on which the Laplace–Beltrami operator acts as multiplication by $-\lambda_\ell$ , $\lambda_\ell=\ell(\ell+1)$ .

On a probability space $(\Omega,\mathcal A,\mathbb P)$ let $\beta^i_{\ell m}$ ( $\ell\ge0$ , $0\le m\le\ell$ , $i=1,2$ ) be independent real Brownian motions, and let $(A_\ell)_{\ell\ge0}$ , $A_\ell\ge0$ , be an angular power spectrum. The isotropic $Q$ -Wiener process is

W(t)=\sum_{\ell\ge0}\sqrt{A_\ell}\Big(\beta^1_{\ell0}(t)Y_{\ell0}+\sqrt2\sum_{m=1}^{\ell}\big(\beta^1_{\ell m}(t)\operatorname{Re}Y_{\ell m}+\beta^2_{\ell m}(t)\operatorname{Im}Y_{\ell m}\big)\Big).

The stochastic heat equation is

dX(t)=\Delta_{\mathbb S^2}X(t)\,dt+dW(t),\qquad X(0)=X_0\in L^2(\Omega;L^2(\mathbb S^2)).

Its solution is $X(t)=\sum_{\ell\ge0}X_\ell(t)$ with

X_\ell(t)=e^{-\lambda_\ell t}\sum_{m=-\ell}^{\ell}(X_0,Y_{\ell m})Y_{\ell m}+\sqrt{A_\ell}\Big(\int_0^te^{-\lambda_\ell(t-s)}d\beta^1_{\ell0}(s)\,Y_{\ell0}+\sqrt2\sum_{m=1}^{\ell}\Big(\int_0^te^{-\lambda_\ell(t-s)}d\beta^1_{\ell m}(s)\operatorname{Re}Y_{\ell m}+\int_0^te^{-\lambda_\ell(t-s)}d\beta^2_{\ell m}(s)\operatorname{Im}Y_{\ell m}\Big)\Big),

and the spectral approximation is $X^\kappa(t)=\sum_{\ell=0}^{\kappa}X_\ell(t)$ . The norm $\|Z\|_{L^p(\Omega;L^2(\mathbb S^2))}=(\mathbb E\|Z\|^p_{L^2(\mathbb S^2)})^{1/p}$ measures random fields. The standing assumption of §7 is the decay condition

A_\ell\le C\,\ell^{-\alpha}\quad\text{for all }\ell>\ell_0,\qquad \ell_0\in\{1,2,\dots\},\ \alpha>0 .

Formalization targets

Goal: Corollary 7.3 (p. 43)

For every $t>0$ and every $\beta<\alpha/2$ , almost surely

\|X(t)-X^\kappa(t)\|_{L^2(\mathbb S^2)}\le\kappa^{-\beta}\quad\text{for all sufficiently large }\kappa .

The goal fixes no constant; only the exponent $\alpha/2$ enters, so it survives any improvement of the constants below.

Milestones

Display (3), p. 36. For $\ell\ge1$ , $\int_0^te^{-\ell(\ell+1)(t-s)}d\beta(s)\sim\mathcal N\big(0,(2\ell(\ell+1))^{-1}(1-e^{-2\ell(\ell+1)t})\big)$ .
Lemma 7.1, pp. 39–40, as proved. If the coefficients of $X_0$ are independent of the noise, then for $t>0$ and $\kappa\ge\ell_0$

\|X(t)-X^\kappa(t)\|^2_{L^2(\Omega;L^2(\mathbb S^2))}\le C\Big(\frac2\alpha+\frac1{\alpha+1}\Big)\kappa^{-\alpha}+e^{-2(\kappa+1)(\kappa+2)t}\|X_0\|^2_{L^2(\Omega;L^2(\mathbb S^2))}.

Lemma 7.2, pp. 41–43, as proved. For each $p>0$ there is $\hat C_p=\hat C_p(p,C,\alpha)$ with, for $t>0$ and $\kappa\ge\ell_0$ ,

\|X(t)-X^\kappa(t)\|_{L^p(\Omega;L^2(\mathbb S^2))}\le\hat C_p\kappa^{-\alpha/2}+e^{-(\kappa+1)(\kappa+2)t}\|X_0\|_{L^{\max(p,2)}(\Omega;L^2(\mathbb S^2))}.

Significance

Corollary 7.3 is the pathwise convergence rate of the spectral method for the stochastic heat equation on the sphere: a single simulated path of the truncated series is within $\kappa^{-\beta}$ of the true path in $L^2(\mathbb S^2)$ for all large $\kappa$ , for any $\beta<\alpha/2$ . Combined with the exact-in-law recursion on a time grid (pp. 36–38), it says that the only source of error in simulating this SPDE is the spectral truncation, and that the rate is governed by the decay exponent of the noise spectrum alone, with $\alpha>0$ sufficing (no trace-class condition $\alpha>2$ is needed, thanks to the smoothing of the heat semigroup). The mean-square and $L^p$ estimates of Lemmas 7.1 and 7.2 are the quantitative inputs; the $L^p$ bound for all $p$ is what makes a Borel–Cantelli argument possible.

The results are proved in the paper; none of them, nor the stochastic heat equation on the sphere, nor spherical harmonics, has a machine-checked formalization on the platform or in Mathlib. The work here is to formalize the known proof. Two printed statements need correction (see Formalization scope); the milestones state the bounds that the paper's proofs establish.

Difficulty

The obvious argument writes $X(t)-X^\kappa(t)$ as the tail of the series, splits it into the damped initial condition and the noise, and bounds each. The noise part is a Gaussian random field whose angular power spectrum $A_\ell(1-e^{-2\lambda_\ell t})/(2\lambda_\ell)$ decays like $\ell^{-(\alpha+2)}$ , so its truncation error is controlled by the corresponding estimates for isotropic Gaussian random fields (Proposition 5.2 and Theorem 5.3 of the paper), which must be re-derived here. Several steps have no current library support: the Wiener integral of a deterministic integrand and its Gaussian law, orthonormality and completeness of the spherical harmonics in $L^2(\mathbb S^2,\sigma)$ , moment equivalence for Gaussian vectors in a Hilbert space (to pass from $p=2$ to all $p$ ), and the passage between the pointwise series and its $L^2$ limit. The initial-condition tail decays like $e^{-(\kappa+1)(\kappa+2)t}$ but not uniformly as $t\downarrow0$ , which is exactly why the printed "uniformly in time" bounds fail and why every statement takes $t>0$ fixed.

Formalization scope

$\mathbb S^2$ is Metric.sphere (0 : EuclideanSpace ℝ (Fin 3)) 1 with coordinates indexed $0,1,2$ (the paper's $y_1,y_2,y_3$ ); $\sigma$ is the measure toSphere of Lebesgue measure, of mass $4\pi$ . Spherical harmonics are written in Cartesian form, $P_{\ell m}(\cos\vartheta)e^{im\varphi}=(-1)^mP_\ell^{(m)}(y_3)(y_1+iy_2)^m$ , which is the paper's function also at the poles. For real $X_0$ the projection $\sum_m(X_0,Y_{\ell m})Y_{\ell m}$ is written in the real orthonormal basis.
Brownian motions are Mathlib's IsBrownianReal processes on $\mathbb R_{\ge0}$ , independent as a family of path-valued random variables. The stochastic convolution $\int_0^te^{-r(t-s)}db(s)$ is defined pathwise as $b(t)-r\int_0^te^{-r(t-s)}b(s)\,ds$ , which equals the Wiener integral almost surely (integration by parts; $b(0)=0$ a.s.). This is the one place where a stochastic integral is replaced by a pathwise expression.
The Laplace–Beltrami operator is not defined: the paper's spectral solution formula of p. 36 is taken as the definition of $X(t)$ , as a pointwise limit of partial sums in $(\omega,y)$ ; where they diverge (a $\mathbb P\otimes\sigma$ -null set for $t>0$ ) the value is irrelevant to every norm. All statements take $t>0$ ; the paper's time partition with $n\in\mathbb N$ forces this, and since $X^\kappa(t)$ is defined from the solution itself the independence of the time discretization is automatic and the partition is not an argument.
Norms are lower Lebesgue integrals in $[0,\infty]$ , so no integrability side condition hides in a default value; $X_0$ is jointly measurable with $\mathbb E\|X_0\|^2_{L^2(\mathbb S^2)}<\infty$ ; $A_\ell\ge0$ ; $\ell_0\ge1$ .
Corrections. Lemmas 7.1 and 7.2 claim bounds uniform in time with constants depending only on $\|X_0\|$ , $C$ , $\alpha$ (and $p$ ). Their proofs bound the initial-condition tail by $e^{-2(\kappa+1)(\kappa+2)t}\|X_0\|^2$ (resp. $e^{-(\kappa+1)(\kappa+2)t}\|X_0\|_{L^p}$ ) and absorb it into $C\kappa^{-\alpha}$ with a $t$ -dependent constant; for nonzero $X_0$ the printed uniform bounds are false (as $t\downarrow0$ the error tends to the $L^2$ tail of $X_0$ ). The milestones state the proofs' bounds with the explicit exponential term; for $X_0=0$ Lemma 7.1 is the printed statement, uniformly in $t$ . Lemma 7.1 additionally assumes that the coefficients of $X_0$ are independent of the noise, which its proof uses to drop a cross term. In Lemma 7.2 the constant $\hat C_p$ depends on $p,C,\alpha$ only and is quantified before everything else. Corollary 7.3 is stated for each fixed $t$ : "uniformly in time" is not formalized. The constant on p. 42, $(2/(\alpha-2)+1/(\alpha-1))$ , should read $(2/\alpha+1/(\alpha+1))$ ; it is existential in Lemma 7.2 and has no effect.
A trivializing reading is ruled out: the error is measured against the solution defined by the explicit series, not against an arbitrary process satisfying a hypothesis, and no hypothesis pins the conclusion.
Reusable infrastructure: real spherical harmonics and their orthonormality on $(\mathbb S^2,\sigma)$ , the Wiener integral of deterministic functions and the Ornstein–Uhlenbeck law, and $L^p$ moment equivalence for Gaussian fields. Contributions of any of these, or of the truncation estimates of §5 for the shifted spectrum, are welcome.

Selected references

A. Lang, Ch. Schwab, Isotropic Gaussian random fields on the sphere: regularity, fast simulation and stochastic partial differential equations, Ann. Appl. Probab. 25(6), 2015. arXiv:1305.1170
A. Jentzen, P. E. Kloeden, Overcoming the order barrier in the numerical approximation of stochastic partial differential equations with additive space–time noise, Proc. R. Soc. A 465, 2009. doi:10.1098/rspa.2008.0325
G. Da Prato, J. Zabczyk, Stochastic Equations in Infinite Dimensions, Cambridge University Press, 1992. doi:10.1017/CBO9780511666223
D. Marinucci, G. Peccati, Random Fields on the Sphere, Cambridge University Press, 2011. doi:10.1017/CBO9780511751677

6 thms1 active userReviewed

Completed

Actuarial Science Probability·Captain: WillR

Actuarial Mathematics XII: Multiple-State Insurance and Annuity CashflowsTextbook

Motivation and actuarial setting

Many insurance benefits depend on a policyholder's health or membership state rather than simply on being alive or dead. A disability annuity pays while a life occupies a disabled state; a critical illness or death benefit may be triggered by moving from one state to another. A rigorous multiple-state valuation therefore distinguishes payments for occupying a state from payments for a transition between states, and must also specify the timing of the payments.

The discrete-time models in Promislow, Fundamentals of Actuarial Mathematics, third edition, Chapter 19 §§19.2.1–19.2.3 [1], provide these two actuarial payment categories. Dickson, Hardy and Waters, Actuarial Mathematics for Life Contingent Risks, first edition, Chapter 8 [2], develop related multiple-state assumptions, transition probabilities, premium values and policy values. Norris, Markov Chains, §1.1 [3], supplies the finite-state stochastic-matrix foundation.

This mission develops the corresponding finite-horizon present-value formulas. It is the cashflow extension of the finite-state transition algebra in Mission X, but is designed as a self-contained draft while Mission X's definitions remain unpublished. The key mathematical obligations are correctly weighted transition benefits, state occupation annuities, finite-state distribution propagation, homogeneity and a capstone valuation decomposition.

Finite-state model and probability distributions

Let $S$ be a finite set of insurance states. At the start of policy year $k$ , let $\mu_{k,i}$ represent the probability of state $i$ , and let $P_{k,ij}$ be the conditional probability of occupying state $j$ at the end of the year, conditional on state $i$ at its start.

A state distribution must satisfy

\mu_{k,i}\ge0,\qquad \sum_{i\in S}\mu_{k,i}=1.

A valid one-year transition kernel has nonnegative entries and rows summing to one:

P_{k,ij}\ge0,\qquad \sum_{j\in S}P_{k,ij}=1.

The next year's marginal state distribution is obtained by propagating the current distribution through that kernel:

\mu_{k+1,j}=\sum_{i\in S}\mu_{k,i}P_{k,ij}.

The supporting theorems show that nonnegativity and total probability are preserved by this operation. The transition kernels are allowed to change from one year to the next. A separate path-space process need not be constructed to establish these finite-sum valuation identities, but $\mu$ and $P$ must obey the propagation relationship to represent one coherent Markov insurance model.

State-occupation payments

Let $c_{k,i}$ be the payment made at the beginning of policy year $k$ to a contract then occupying state $i$ . For example, it could represent a disability annuity paid only while the person is disabled. The expected amount at that payment time is

R^{\mathrm{occ}}_k=\sum_{i\in S}\mu_{k,i}c_{k,i}.

The expected present value of the state-occupation cashflows over $n$ policy years is

V_n^{\mathrm{occ}}= \sum_{0\le k<n}v^k\sum_{i\in S}\mu_{k,i}c_{k,i}.

A payment due at time zero is not discounted. A constant amount paid irrespective of state has its own expected value unchanged because the marginal state probabilities add to one. This is consistent with the state-occupation cashflow structure in [1, §19.2.3, equation (19.6)].

State-transition benefits

Let $b_{k,ij}$ be the benefit payable at the end of policy year $k$ when the contract transitions from state $i$ to state $j$ over that year. The expected one-year amount is

R^{\mathrm{tr}}_k= \sum_{i\in S}\sum_{j\in S} \mu_{k,i}P_{k,ij}b_{k,ij}.

The contract's expected present value of those transitions is

V_n^{\mathrm{tr}}= \sum_{0\le k<n}v^{k+1} \sum_{i\in S}\sum_{j\in S} \mu_{k,i}P_{k,ij}b_{k,ij}.

Unlike a reward depending only on the destination state, a transition-specific benefit may distinguish, for example, $i=\text{healthy}\to j=\text{disabled}$ from $i=\text{disabled}\to j=\text{disabled}$ . Keeping the pair $(i,j)$ explicit is necessary to represent such insurance benefits. This is the payment timing and transition structure considered in [1, §19.2.2, equations (19.2)–(19.4)].

Combined cashflows and capstone identity

The mission defines the complete finite-horizon value by adding the two types of cashflow:

\begin{aligned} V_n &=V_n^{\mathrm{occ}}+V_n^{\mathrm{tr}}\\ &=\sum_{0\le k<n}\left[ v^k\sum_i\mu_{k,i}c_{k,i} +v^{k+1}\sum_{i,j}\mu_{k,i}P_{k,ij}b_{k,ij} \right]. \end{aligned}

Because finite sums are linear, scaling both monetary benefit schedules by a constant $a\in\mathbb R$ scales the entire expected present value by $a$ :

V_n(ab,ac)=a\,V_n(b,c).

The capstone combines decomposition of the occupation and transition components with this scaling principle. Related milestones establish the zero-year, zero-benefit and one-year limits. For a one-year contract the exact timing reduces to

V_1=\sum_i\mu_{0,i}c_{0,i} +v\sum_{i,j}\mu_{0,i}P_{0,ij}b_{0,ij}.

The displayed formula is deterministic expected-value algebra for finite state probabilities, rather than a claim about a pathwise cashflow random variable. The later development of a stochastic path-space model, conditional benefits and second moments remains a separate task.

Formal proof structure and limitations

The proposed Lean draft contains five definitions: a finite-state probability distribution, one-step distribution propagation, expected transition-stage reward, expected occupation-stage reward and the combined finite-term PV. Thirteen supporting theorems prove probability propagation, zero and constant payments, scaling, valuation decomposition and the one-year boundary. The final capstone packages the overall value decomposition and benefit scaling.

The formal theorem statements do not require the cashflow amounts to be nonnegative because their linearity is algebraic. Probability interpretation additionally requires legitimate state probabilities and transition kernels. The source explicitly avoids interpreting arbitrary arrays $\mu_k$ and $P_k$ as the marginals of one Markov chain unless they satisfy the propagation identity.

These declarations are proposed mathematical obligations, not accepted proofs. Individual Lean modules import only the definitions their statements actually use, with all imports before Lean commands. Because the local definitions are not yet published as importable Prove2Me modules, downstream theorem previews must be revisited after their definitions are confirmed and published.

References

[1] Promislow, S. David (2015), Fundamentals of Actuarial Mathematics, third edition, Wiley, Chapter 19, Multi-state Models, §§19.2.1–19.2.3. Equations (19.2)–(19.4) address transition-based insurance benefits and equation (19.6) addresses occupation-based annuity benefits.

[2] Dickson, David C. M., Hardy, Mary R. and Waters, Howard R. (2009), Actuarial Mathematics for Life Contingent Risks, first edition, Chapter 8, Multiple State Models, especially §§8.3–8.7 on states, transition probabilities, premiums and policy values.

[3] Norris, J. R. (1997), Markov Chains, Cambridge University Press, Chapter 1, §1.1 on stochastic matrices and discrete-time transition probabilities. The matrix-multiplication setting here permits different kernels at successive durations, in line with Promislow's non-stationary treatment.

19 thms1 active userReviewed

All missions

Arbitrage and Duality in Nondominated Discrete-Time Models II: Nondominated Optional Decomposition — a Supermartingale Under Every Martingale Measure Is V₀ + H•S − KResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 6.1 (nondominated optional decomposition)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Viscosity Solutions to Parabolic Master Equations and McKean–Vlasov SDEs with Closed-Loop Controls 2: Comparison Principle and Uniqueness for Viscosity Solutions of Parabolic Master EquationsResearch Paper

Motivation

Setting

Formalization targets

Goal: comparison and uniqueness (Theorem 4.13)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Approximate Markov-Nash Equilibria for Discrete-Time Risk-Sensitive Mean-Field Games 2: The Mean-Field Equilibrium Policy Is an ε-Markov-Nash Equilibrium of Every Large Enough N-Agent GameResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3 (p. 23)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Actuarial Mathematics XXIII: Countable-Lifetime Hattendorff LimitTextbook

Actuarial Mathematics XXIII: Countable-Lifetime Hattendorff Limit

Mathematical source and original extension

Unbounded lifetime and conditional mortality

Mortality surprises and reserve losses

Supporting results and convergence condition

Exact-rational validation and boundaries

Prove2Me proof structure

Actuarial Mathematics XVI: Discrete Mortality Innovations and Hattendorff OrthogonalityTextbook

Motivation: from actuarial reserves to Hattendorff's theorem

Finite lifetime model

A centred innovation for every policy year

The one-year discrete second moment

Formal proof structure and scope

References

Actuarial Mathematics XVII: Finite-Horizon Markov Decision and Optimal Policy ValuationTextbook

Motivation: from one-step reinsurance decisions to an optimal policy

Finite states, actions and one-year valuation

Finite-horizon policy evaluation

Optimal backward induction

Formal graph and limiting cases

References

Gaussian Random Matrices III: Extreme Singular Values and ConcentrationTextbook

Motivation

Setting

Formalization targets

Goal — deviation of the extreme singular values (Vershynin, Corollary 5.35)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Gaussian Random Matrices I: Rotation Invariance and Moment IdentitiesTextbook

Motivation

Setting

Formalization targets

Goal — Gaussian approximate matrix multiplication

Milestones

Significance

Difficulty

Formalization scope

Selected references

Propagation of Chaos for Stochastic Spatially Structured Neuronal Networks with Delay driven by Jump Diffusions 1: The Spatially Structured McKean–Vlasov Delay Equation with Jumps Is Well-PosedResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1.5 (p. 7)

Milestones

Significance