Bandit Algorithms Machine Learning Probability+1·Captain: mikedeng1

Bypassing the Monster: A Faster and Simpler Optimal Algorithm for Contextual Bandits Under Realizability: FALCON+ Has Regret ≤ 14.3·Σₘ√(K𝓔(τₘ₋₁−τₘ₋₂))(τₘ−τₘ₋₁) + τ₁ + √(8T log(2/δ)) w.p. 1−δResearch Paper

Contextual bandits and the reduction to regression

A contextual bandit is a sequential decision problem: in each round a learner sees a context (a user's features, a patient's covariates), picks one of $K$ actions, and observes the reward of that action only. Applications include recommendation, dynamic pricing and adaptive clinical decisions. The difficulty is statistical and computational at once: the learner must explore to learn which action is best for which context, and the class of models it learns over is typically huge.

A long-standing question was whether contextual bandits can be solved optimally with nothing more than an offline regression oracle, a black-box supervised learning routine that fits a predictor of rewards to i.i.d. data. Earlier optimal algorithms either required a cost-sensitive classification oracle called many times per round (the "monster" of Agarwal et al., 2014) or an online regression oracle that must handle adversarially generated data (Foster and Rakhlin, 2020). Simchi-Levi and Xu (2022) answered the question with FALCON+, which calls an arbitrary offline regression oracle once per epoch, $O(\log T)$ or $O(\log\log T)$ times in total, and whose regret is governed by the oracle's estimation error.

Timeline:

2014: Agarwal, Hsu, Kale, Langford, Li and Schapire, Taming the Monster: optimal regret with $\tilde O(\sqrt{KT})$ calls to a classification oracle.
2020: Foster and Rakhlin, Beyond UCB: SquareCB, optimal regret with an online regression oracle, via inverse gap weighting.
2020 (arXiv) / 2022 (journal): Simchi-Levi and Xu, FALCON and FALCON+: optimal regret with an offline regression oracle.

Setting

There is a finite set $\mathcal A$ of $K$ actions and a set $\mathcal X$ of contexts. In round $t$ nature draws a context $x_t$ and a reward vector $r_t\in[0,1]^{\mathcal A}$ from a fixed unknown distribution $\mathcal D$ ; the learner sees $x_t$ , picks $a_t$ and observes $r_t(a_t)$ . The conditional mean reward is $f^*(x,a)=\mathbb E[r_t(a)\mid x_t=x]$ , and $\pi_{f^*}(x)$ is an action maximizing $f^*(x,\cdot)$ . The regret after $T$ rounds is

\sum_{t=1}^T\big(r_t(\pi_{f^*}(x_t))-r_t(a_t)\big).

An action selection kernel $p(a\mid x)$ gives a probability distribution over actions for each context. The offline regression oracle $\mathrm{OffReg}_{\mathcal F}$ takes $n$ samples $(x_i,a_i,r_i(a_i))$ and returns a predictor $\hat f:\mathcal X\times\mathcal A\to\mathbb R$ . It satisfies Assumption 2 with error function $\mathcal E_{\mathcal F,\delta}(n)$ if, for every kernel $p$ , when the samples are i.i.d. with $(x_i,r_i)\sim\mathcal D$ and $a_i\sim p(\cdot\mid x_i)$ , then with probability at least $1-\delta$ ,

\mathbb E_{x\sim\mathcal D_{\mathcal X},\,a\sim p(\cdot\mid x)}\big[(\hat f(x,a)-f^*(x,a))^2\big]\le\mathcal E_{\mathcal F,\delta}(n).

FALCON+ runs in epochs given by a schedule $0=\tau_0<\tau_1<\tau_2<\cdots$ . In epoch $m$ it sets $\gamma_1=1$ and $\gamma_m=\tfrac12\sqrt{K/\mathcal E_{\mathcal F,\delta/(2m^2)}(\tau_{m-1}-\tau_{m-2})}$ for $m\ge2$ ; it obtains $\hat f_m$ by feeding only the data of epoch $m-1$ to the oracle ( $\hat f_1\equiv0$ ); and in every round $t$ of the epoch it plays

p_t(a)=\frac{1}{K+\gamma_m\big(\hat f_m(x_t,\hat a_t)-\hat f_m(x_t,a)\big)}\ \ (a\ne\hat a_t),\qquad p_t(\hat a_t)=1-\sum_{a\ne\hat a_t}p_t(a),

where $\hat a_t$ maximizes $\hat f_m(x_t,\cdot)$ . The epoch of round $t$ is $m(t)=\min\{m\ge1:t\le\tau_m\}$ .

Formalization targets

Goal: Theorem 2 in explicit form

If $\tau_m\ge2^m$ and $\gamma_1\le\cdots\le\gamma_{m(T)}$ for $m\le m(T)$ , then for every $T\ge1$ and $\delta>0$ , with probability at least $1-\delta$ ,

\sum_{t=1}^T\big(r_t(\pi_{f^*}(x_t))-r_t(a_t)\big)\le 14.3\sum_{m=2}^{m(T)}\sqrt{K\,\mathcal E_{\mathcal F,\delta/(2m^2)}(\tau_{m-1}-\tau_{m-2})}\,(\tau_m-\tau_{m-1})+\tau_1+\sqrt{8T\log(2/\delta)}.

The paper states Theorem 2 as an $O(\cdot)$ bound; this is the explicit inequality its proof establishes, with the additive terms kept. It holds for every oracle, error function and schedule satisfying the hypotheses, so it is the shape of the result rather than a rate for a particular class.

Milestones

In attack order: Lemma A.2 (each oracle call is accurate with probability $1-\delta/(2m^2)$ ; the good event $\Gamma_2$ has probability $1-\delta/2$ ); Lemma A.3 (the kernel $p_m$ is induced by a randomized policy $Q_m$ on $\Psi=\mathcal A^{\mathcal X}$ ); Lemma A.4 (the conditional expected regret of a round is the implicit regret of $Q_{m(t)}$ ); Lemmas A.5 and A.6 (low predicted regret and bounded divergence $V(p_m,\pi)\le K+\gamma_m\widehat{\mathrm{Reg}}(\pi)$ ); Lemma A.7 (prediction error of implicit rewards on $\Gamma_2$ ); Lemma A.8 (true and predicted implicit regret agree up to factor 2 and $5.15K/\gamma_m$ ); Lemma A.9 ( $\sum_\pi Q_m(\pi)\mathrm{Reg}(\pi)\le7.15K/\gamma_m$ ); Lemma A.10 in expectation; the Azuma display (A.10); and Lemma A.10 with high probability.

Significance

Theorem 2 makes contextual bandits reducible to offline regression with no loss in rate: for any function class with an estimation-error bound, plugging that bound into the theorem gives the regret. With empirical entropy $O(\varepsilon^{-p})$ this yields $O(T^{(1+p)/(2+p)}\log T)$ , matching the known lower bound, and for linear classes it improves the best known bound when $K\ll T$ (Examples 1–2 of the paper). The oracle is called once per epoch on i.i.d. data, so any off-the-shelf supervised learner can be used, with a guarantee transferred automatically.

Formalizing the result produces a machine-checked offline-to-online reduction, independent of the function class. The paper's result is proved, but it has no machine-checked proof; the platform has formal statements for the online-oracle algorithm SquareCB and for the classification-oracle algorithm of Agarwal et al., not for this reduction. The milestones isolate reusable facts about inverse-gap-weighted kernels (Lemmas A.3, A.5, A.6) and an epoch-wise induction pattern (Lemma A.8) that recur in later work on bandits and reinforcement learning with regression oracles.

Difficulty

The obvious argument fails at the regression step. A natural approach feeds all past data to the oracle, but those data are adaptively collected and not i.i.d., so an offline guarantee does not apply to them; FALCON+ uses only the previous epoch's data, which are i.i.d. given the past, and the analysis must make this conditional application of Assumption 2 rigorous on a product space (Lemma A.2). The second obstacle is that the oracle's error is measured under the kernel of the previous epoch, while regret is incurred under the current one. Transferring the error across epochs requires the divergence $V(p,\pi)$ and the two-sided comparison of true and predicted implicit regret in Lemma A.8, proved by induction on epochs with exact constants; a one-sided bound does not close the induction.

Formalization scope

Lean representation and conventions:

Finite contexts. $\mathcal X$ is a Fintype with the discrete σ-algebra. The paper claims Theorem 2 for arbitrary $\mathcal X$ , but its detailed proof (App. A.1–A.6) is "under the condition that $|\mathcal X|<\infty$ "; the uncountable case (App. A.7) is not formalized. No bound depends on $|\mathcal X|$ .
Rewards in $[0,1]$ , the model of §1.2 and the assumption of the proof of Theorem 2. Setup 2's heavy-tailed generality (Condition (5)) is not formalized.
Nature's law is a context marginal $\mathcal D_{\mathcal X}$ with a Markov reward kernel; $f^*(x,a)$ is the kernel mean.
The run lives on the canonical space $\mathbb N\to(\mathcal X\times\mathbb R^{\mathcal A})\times[0,1]$ with the i.i.d. product law of $\mathcal D\otimes\mathrm{Uniform}[0,1]$ ; actions are drawn by the inverse CDF from the uniform coordinate.
Probabilities in failure form: "with probability at least $1-\delta$ " is "the failure set has outer measure at most $\delta$ ".
Added hypotheses (disclosed in every statement): $\mathcal E_{\mathcal F,\delta}(n)>0$ (Algorithm 2 divides by it); measurability of the oracle and of the tie-breaking rule for $\hat a_t$ (App. A.7, p. 1929, assumes such conditions directly); $\delta>0$ ; $T\ge1$ .
The tie-breaking rule for $\hat a_t$ and the maximizer $\pi_{f^*}$ are universally quantified.
Quantities the paper indexes by a round $t$ are indexed by its epoch; $\Upsilon_{t-1}$ is replaced by the coordinate filtration, which contains it.

A trivializing formalization is ruled out: the goal is a bound on the realized regret of the run of Algorithm 2, whose oracle sees only $(x,a,r(a))$ samples of the previous epoch; it is not a bound for an algorithm that is handed $f^*$ or its population error, or that observes the full reward vector.

Infrastructure needed: conditional application of an i.i.d. guarantee inside a product measure (Fubini over Measure.infinitePi), Azuma–Hoeffding for bounded martingale differences (proved on the platform as bounded_diff_martingale_two_sided), and finite-sum algebra for inverse gap weighting. The kernel lemmas A.3, A.5 and A.6 are reusable beyond this mission. Proofs of any milestone are welcome, as are proofs of the goal from the milestones.

Selected references

D. Simchi-Levi and Y. Xu, Bypassing the Monster: A Faster and Simpler Optimal Algorithm for Contextual Bandits Under Realizability, Mathematics of Operations Research 47(3):1904–1931, 2022. https://doi.org/10.1287/moor.2021.1193
D. J. Foster and A. Rakhlin, Beyond UCB: Optimal and Efficient Contextual Bandits with Regression Oracles, ICML 2020. https://arxiv.org/abs/2002.04926
A. Agarwal, D. Hsu, S. Kale, J. Langford, L. Li and R. E. Schapire, Taming the Monster: A Fast and Simple Algorithm for Contextual Bandits, ICML 2014. https://arxiv.org/abs/1402.0555

14 thms2 active usersReviewed

Completed

Convex Optimization Dynamical Systems Optimization·Captain: mikedeng1

Understanding the Acceleration Phenomenon via High-Resolution Differential Equations V: Along the High-Resolution ODE of NAG-C, inf ‖∇f(X(u))‖² ≤ (12 + 9sL)‖x₀ − x⋆‖²/(2√s(t³ − t₀³))Research Paper

Motivation

Nesterov's accelerated gradient method for smooth convex functions, called NAG-C in the source paper, minimizes an $L$ -smooth convex function $f$ with function values decreasing at the rate $O(L/k^2)$ . That rate is optimal among first-order methods (Nesterov, 1983). A line of work starting with Su, Boyd & Candès (2016) studies such methods through ordinary differential equations obtained in the limit of vanishing step size. Their low-resolution ODE $\ddot X+\frac3t\dot X+\nabla f(X)=0$ reproduces the $O(1/t^2)$ function-value rate. The same ODE also models the heavy-ball method, so it cannot explain why Nesterov's method behaves differently from heavy-ball.

Shi, Du, Jordan & Su (arXiv:1810.08907v3) keep the $O(\sqrt s)$ terms of the limit, where $s$ is the step size. The resulting high-resolution ODEs contain a gradient-correction term $\sqrt s\,\nabla^2 f(X)\dot X$ , which is absent from the heavy-ball ODE. This mission formalizes the paper's analysis of the high-resolution ODE of NAG-C (Section 4.1, pp. 21–24). Along this ODE the smallest squared gradient norm up to time $t$ decays like $1/t^3$ , while the low-resolution ODE gives only $1/t^2$ . Small gradients are the natural stopping criterion in practice and the natural target in nonconvex and dual problems, which is why the squared gradient norm is studied separately from function values (Nesterov, 2012).

Setting

Let $f:\mathbb R^n\to\mathbb R$ have gradient $\nabla f$ and Hessian $\nabla^2 f$ . For $L>0$ , the class $\mathcal F^1_L(\mathbb R^n)$ consists of the differentiable $f$ with

f(y)\ge f(x)+\langle\nabla f(x),y-x\rangle,\qquad \|\nabla f(x)-\nabla f(y)\|\le L\|x-y\|\qquad(x,y\in\mathbb R^n).

The class $\mathcal F^2_L(\mathbb R^n)$ is its subclass of twice continuously differentiable functions whose Hessian is Lipschitz continuous. A minimizer $x^\star$ of $f$ is fixed.

Given a step size $s>0$ , put $t_0=1.5\sqrt s$ . The high-resolution ODE of NAG-C (1.12) is

\ddot X(t)+\frac3t\dot X(t)+\sqrt s\,\nabla^2 f(X(t))\dot X(t)+\Big(1+\frac{3\sqrt s}{2t}\Big)\nabla f(X(t))=0\qquad(t\ge t_0),

with $X(t_0)=x_0$ and $\dot X(t_0)=-\sqrt s\,\nabla f(x_0)$ . The analysis uses the Lyapunov function (4.1)

\mathcal E(t)=t\Big(t+\frac{\sqrt s}{2}\Big)\big(f(X)-f(x^\star)\big)+\frac12\big\|t\dot X+2(X-x^\star)+t\sqrt s\,\nabla f(X)\big\|^2 .

With $s=0$ it reduces to the Lyapunov function of Su, Boyd and Candès.

Formalization targets

Goal: Theorem 5 (p. 21)

For every $f\in\mathcal F^2_L(\mathbb R^n)$ , every step size $s>0$ , and every solution $X$ of (1.12),

\inf_{t_0\le u\le t}\|\nabla f(X(u))\|^2\le\frac{(12+9sL)\,\|x_0-x^\star\|^2}{2\sqrt s\,(t^3-t_0^3)}\qquad\text{for all }t>t_0 .

With $s=1/L$ this is $O(\sqrt L/t^3)$ . The infimum cannot be dropped, because the gradient norm need not decrease along the trajectory.

Milestones (pp. 22–23)

The exact derivative of $\mathcal E$ along (1.12) (first display of the proof of Lemma 4.1, p. 23).
Lemma 4.1, (4.2): $\frac{d\mathcal E}{dt}\le-\big[\sqrt s\,t^2+(\frac1L+\frac s2)t+\frac{\sqrt s}{2L}\big]\|\nabla f(X)\|^2$ for $t\ge t_0$ .
The integrated form: $\int_{t_0}^t\big[\sqrt s\,u^2+(\frac1L+\frac s2)u+\frac{\sqrt s}{2L}\big]\|\nabla f(X(u))\|^2\,du\le\mathcal E(t_0)-\mathcal E(t)\le\mathcal E(t_0)$ .
(4.3): the infimum is at most $\mathcal E(t_0)$ divided by $\sqrt s(t^3-t_0^3)/3+(\frac1L+\frac s2)(t^2-t_0^2)/2+\frac{\sqrt s}{2L}(t-t_0)$ .
$\mathcal E(t_0)\le 3s\cdot\frac L2\|x_0-x^\star\|^2+2\|x_0-x^\star\|^2$ , from the initial conditions.
(4.4): the same bound as (4.3) with numerator $(2+1.5sL)\|x_0-x^\star\|^2$ . Keeping only the cubic term of the denominator gives Theorem 5.

A companion item states Corollary 4.2 (p. 24): $f(X(t))-f(x^\star)\le\frac{(4+3sL)\|x_0-x^\star\|^2}{t(2t+\sqrt s)}$ for $t>t_0$ .

Significance

Theorem 5 is the continuous-time model of the paper's Theorem 6, which shows that NAG-C itself, without modification, drives $\min_{i\le k}\|\nabla f(x_i)\|^2$ to zero at the rate $O(L^2/k^3)$ . Combining the $O(1/t^2)$ function-value rate with $\|\nabla f\|^2\le 2L(f-f^\star)$ gives only $O(L/t^2)$ . Previously known $O(L^2/k^3)$ rates required modified methods (Ghadimi & Lan, 2016). The proof attributes the improvement to the gradient-correction term: the factor $\|\nabla f(X)\|^2$ in Lemma 4.1 comes from the term $t\sqrt s\,\nabla f(X)$ in (4.1), which exists only because of the Hessian term in (1.12). The authors conjecture that the low-resolution ODE does not achieve the $1/t^3$ rate (p. 23).

The results of Section 4.1 are proved in the paper; no machine-checked version of them is known. Formalizing them produces a checked Lyapunov analysis of a second-order ODE with Hessian damping and explicit constants. It also gives a template that the discrete analysis of NAG-C (a separate mission in this series) mirrors step by step. Related Hessian-damped systems are analysed in Attouch, Chbani, Fadili & Riahi (2020), with qualitative integrability conclusions instead of an explicit bound on the infimum.

Difficulty

The obvious route goes through the function-value rate and the inequality $\|\nabla f\|^2\le2L(f-f^\star)$ . It loses a factor of $t$ and yields only $1/t^2$ . The cubic rate needs a Lyapunov function whose derivative contains a term proportional to $t^2\|\nabla f(X)\|^2$ . Proving the derivative identity requires differentiating $t\mapsto\nabla f(X(t))$ through the chain rule with the Hessian, and then cancelling that derivative against the gradient-correction term of the ODE. The derivative bound also uses the co-coercivity inequality $f(x^\star)\ge f(X)+\langle\nabla f(X),x^\star-X\rangle+\frac1{2L}\|\nabla f(X)\|^2$ of $L$ -smooth convex functions. The remaining steps are measure-theoretic: integrate a one-sided derivative bound on $[t_0,t]$ , and compare an infimum with a weighted average.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n), $\nabla f$ is Mathlib's gradient, and $\nabla^2 f(x)v$ is the Fréchet derivative of the gradient map applied to $v$ .
The classes $\mathcal F^1_L$ and $\mathcal F^2_L$ are stated in the first-order form printed on p. 8. The Hessian's Lipschitz constant is existential, since the paper fixes none.
The minimizer $x^\star$ is a hypothesis $f(x^\star)\le f(z)$ for all $z$ . The paper presupposes it exists.
The step size is any $s>0$ ; there is no condition $s\le1/L$ .
A solution of (1.12) is a pair $(X,V)$ with $X(t_0)=x_0$ and $V(t_0)=-\sqrt s\,\nabla f(x_0)$ . For every $t\ge t_0$ , $X$ has derivative $V(t)$ and $V$ has the derivative prescribed by (1.12), both relative to $[t_0,\infty)$ .
Every statement quantifies over all solutions. Existence and uniqueness (the paper's Proposition 2.2) are not assumed.
The infimum $\inf_{t_0\le u\le t}$ ranges over the points of the interval $[t_0,t]$ . Statements involving it hold for $t>t_0$ , as on the page.
Derivative bounds assert that the derivative exists.
The integral bound asserts integrability of its integrand.

Ruled out. A formalization would hold for junk reasons in any of these cases: the infimum is written as a bounded infimum over all reals (in Lean this is $\le 0$ ); the velocity is not tied to $\dot X$ ; the goal is stated at $t=t_0$ (where Lean divides by $0$ ); or derivatives are written with deriv, which is $0$ where a function is not differentiable. The statements here avoid all of these.

Infrastructure. A complete development needs:

the chain rule for $\nabla f\circ X$ along a path;
the co-coercivity inequality for $L$ -smooth convex functions;
the fundamental theorem of calculus for one-sided derivatives on $[t_0,t]$ ;
the mean-value comparison of an infimum with a weighted average.

The co-coercivity inequality and the interval-integral comparison are reusable beyond this mission. Proofs of the milestones in any order are welcome, as are independent proofs of the goal.

Selected references

B. Shi, S. S. Du, M. I. Jordan, W. J. Su, Understanding the Acceleration Phenomenon via High-Resolution Differential Equations, arXiv:1810.08907v3, 2018; Math. Program. (2021), DOI 10.1007/s10107-021-01681-8. https://arxiv.org/abs/1810.08907
W. Su, S. Boyd, E. J. Candès, A Differential Equation for Modeling Nesterov's Accelerated Gradient Method: Theory and Insights, J. Mach. Learn. Res. 17(153), 2016. https://arxiv.org/abs/1503.01243
Y. Nesterov, A method of solving a convex programming problem with convergence rate O(1/k²), Soviet Math. Dokl. 27, 1983. https://www.mathnet.ru/eng/dan46009
Y. Nesterov, How to make the gradients small, Optima 88, 2012. http://www.mathopt.org/Optima-Issues/optima88.pdf
S. Ghadimi, G. Lan, Accelerated gradient methods for nonconvex nonlinear and stochastic programming, Math. Program. 156, 2016. https://arxiv.org/abs/1310.3787
H. Attouch, Z. Chbani, J. Fadili, H. Riahi, First-order optimization algorithms via inertial systems with Hessian driven damping, Math. Program., 2020. https://arxiv.org/abs/1907.10536

9 thms2 active usersReviewed

Combinatorics Linear Optimization Optimization·Captain: mikedeng1

The Running Intersection Relaxation of the Multilinear Polytope 2: If a Hypergraph Is Not β-Acyclic, Its Multilinear Polytope Is Strictly Contained in the Running Intersection RelaxationResearch Paper

Motivation

Many nonconvex optimization problems in binary variables have a polynomial objective or polynomial constraints. The standard way to bring them into the reach of linear and mixed-integer programming solvers is to introduce one new variable per monomial and to study the convex hull of the resulting set of feasible 0/1 vectors, the multilinear polytope. Strong linear descriptions of this polytope translate directly into tighter relaxations in global solvers such as BARON, which is where the inequalities of this mission were tested (Del Pia and Khajavirad 2021, §2.5).

The multilinear polytope of a general hypergraph has no compact description, so the question is for which hypergraphs a given family of inequalities is enough. The quadratic case is classical: the Boolean quadric polytope of a graph (Padberg 1989) is described by its standard linearization exactly when the graph is a forest, and the odd-cycle inequalities are the first facets that appear on a cycle. For higher-degree monomials, Del Pia and Khajavirad showed in 2018 that their flower relaxation is exact if and only if the hypergraph is γ-acyclic. The 2021 paper introduces the stronger running intersection relaxation and asks the same question for it. This mission formalizes the necessary condition the paper proves: the relaxation cannot be exact unless the hypergraph is β-acyclic.

Setting

A hypergraph $G=(V,E)$ is a finite node set $V$ with a set $E$ of subsets of $V$ of size at least two (no loops, no parallel edges). Its multilinear set is

\mathcal S_G=\Big\{z\in\{0,1\}^{V+E}: z_e=\prod_{v\in e}z_v\ \ \forall e\in E\Big\},

and the multilinear polytope is $\mathrm{MP}_G=\operatorname{conv}\mathcal S_G$ . The standard linearization is

\mathrm{MP}^{\mathrm{LP}}_G=\Big\{z: z_v\le 1\ \forall v;\ z_e\ge 0,\ z_e\ge\sum_{v\in e}z_v-|e|+1\ \forall e;\ z_e\le z_v\ \forall e,\ v\in e\Big\}.

An ordering $p_1,\dots,p_m$ of a multiset of sets is a running intersection ordering if each $p_k$ , $k\ge2$ , meets the union of its predecessors inside a single predecessor $p_j$ ; it induces $N(p_1)=\emptyset$ and $N(p_k)=p_k\cap\bigcup_{i<k}p_i$ . A running intersection inequality has a center $e_0\in E$ , neighbors $e_k$ ( $k\in K$ ) meeting $e_0$ such that $\tilde E=\{e_0\cap e_k\}$ admits a running intersection ordering, and nodes $u_k\in N(e_0\cap e_k)$ when these sets are nonempty:

-\sum_{k:\,N(e_0\cap e_k)\ne\emptyset}z_{u_k}+\sum_{v\in e_0\setminus\bigcup_k e_k}z_v+\sum_{k\in K}z_{e_k}-z_{e_0}\le\omega-1,

with $\omega$ the number of connected components of $(e_0,\tilde E)$ . The running intersection relaxation $\mathrm{MP}^{\mathrm{RI}}_G$ is $\mathrm{MP}^{\mathrm{LP}}_G$ together with all these inequalities.

A β-cycle of length $t\ge3$ is a sequence $v_1,e_1,\dots,v_t,e_t,v_1$ of distinct nodes and distinct edges in which each $v_i$ lies in $e_{i-1}$ and $e_i$ and in no other $e_j$ ; $G$ is β-acyclic if it has none. For $W\subseteq V$ the subhypergraph $G_W$ has node set $W$ and edges $\{e\cap W: |e\cap W|\ge2\}$ .

Formalization targets

Goal: Proposition 5

G\ \text{not β-acyclic}\ \Longrightarrow\ \mathrm{MP}_G\subsetneq\mathrm{MP}^{\mathrm{RI}}_G .

The milestones follow the paper's proof, in order:

$\mathrm{MP}_G\subseteq\mathrm{MP}^{\mathrm{LP}}_G$ (p. 1014) and validity of every running intersection inequality (Proposition 1), giving $\mathrm{MP}_G\subseteq\mathrm{MP}^{\mathrm{RI}}_G$ .
Lemma 3: β-cycles of $G_{V'}$ lift to β-cycles of $G$ of the same length.
Lemma 5: $\mathrm{MP}_{G_{\bar V}}=\mathrm{proj}_{G_{\bar V}}(\mathrm{MP}_G\cap L_{\bar V})$ , with $L_{\bar V}=\{z: z_v=1\ \forall v\notin\bar V\}$ .
Lemma 6: $\mathrm{MP}^{\mathrm{RI}}_{G_{\bar V}}\subseteq\mathrm{proj}_{G_{\bar V}}(\mathrm{MP}^{\mathrm{RI}}_G\cap L_{\bar V})$ .
The reduction: strictness for $G_W$ implies strictness for $G$ .
For a shortest β-cycle $C$ , $G_{V(C)}$ is a chordless cycle, possibly enclosed by the edge $V(C)$ .
Strictness for a chordless cycle.
Strictness for a chordless cycle enclosed by the edge $V(C)$ .

Significance

The result is one half of the paper's picture of when the running intersection relaxation is exact. Proposition 5 shows β-acyclicity is necessary; Theorem 3 of the paper shows that kite-free β-acyclicity is sufficient; Example 2 shows β-acyclicity alone is not. Combined with the 2018 characterization of the flower relaxation by γ-acyclicity, it places the running intersection relaxation strictly between two acyclicity notions and tells a solver designer that on hypergraphs with β-cycles some other family of cuts (for instance odd-cycle-type inequalities lifted from Padberg's) is unavoidable.

The intermediate results are reusable on their own. Lemma 5 is a general statement that multilinear polytopes of induced subhypergraphs are projections of faces, and Lemma 3 with the shortest-cycle structure step is pure hypergraph combinatorics.

The result is proved in the paper. No part of it, nor the multilinear polytope, nor the Boolean quadric polytope, is formalized in Lean or Mathlib as far as a search of the platform showed. Lemma 6 is stated in the paper without proof, and the two strictness cases are justified there by "it can be checked" and by a citation of Padberg; a formal proof closes these gaps.

Difficulty

The obvious argument exhibits a point of $\mathrm{MP}^{\mathrm{RI}}_G\setminus\mathrm{MP}_G$ directly from a β-cycle of $G$ . This fails because a β-cycle of $G$ is surrounded by arbitrary other edges, which contribute running intersection inequalities that can cut off any candidate point. The paper's route is to pass to the subhypergraph induced by the cycle's nodes, and that step requires two facts with real content: the projection lemmas (Lemma 6 is an inclusion between relaxations defined by different families of inequalities), and the structure of $G_{V(C)}$ , which holds only for a shortest β-cycle. A long β-cycle can have chords in $G_{V(C)}$ .

Strictness on the two small families requires a point, or an inequality, separating $\mathrm{MP}$ from $\mathrm{MP}^{\mathrm{RI}}$ . That means controlling every running intersection inequality of the cycle, over all centers, neighbor sets, orderings and choices of $u_k$ , and also checking that the separating inequality is valid for $\mathrm{MP}$ .

Formalization scope

Lean conventions:

Nodes are elements of a finite type α with decidable equality. Hypergraphs carry their node set and their edge set as Finsets, with every edge of size at least two.
Points of $\mathbb R^{V+E}$ are functions α ⊕ Finset α → ℝ, and every polytope of $G$ is pinned to zero off $G$ 's own coordinates, so polytopes of different hypergraphs, and the projection $\mathrm{proj}_{G_{\bar V}}$ , live in one space.
$\mathrm{MP}^{\mathrm{LP}}_G$ is exactly (8), with no row $z_v\ge0$ .
$\mathrm{MP}^{\mathrm{RI}}_G$ quantifies over all centers, all sets of distinct neighbors other than $e_0$ , all running intersection orderings and all choices of $u_k$ .
$\omega$ is the number of connected components of the 2-section graph on $e_0$ .
Orderings and cycles are 0-indexed.
The projection takes the choice $e'(f)$ of an edge of $G$ with trace $f$ as an argument, and Lemmas 5 and 6 hold for every choice.
The strict inclusion $\subset$ of the paper is Lean's ⊂ ( $\subseteq$ and $\ne$ ).

There is one disclosed addition. Lemma 6 and the reduction step assume that $G_{\bar V}$ has no isolated node. Without it both statements are false: since (8) has no lower bound on $z_v$ , a node isolated in $G_{\bar V}$ is unbounded below in $\mathrm{MP}^{\mathrm{RI}}_{G_{\bar V}}$ . The paper uses them only for $\bar V=V(C)$ , where the hypothesis holds. The goal itself carries no added hypothesis.

A trivializing formalization is ruled out. A relaxation missing some running intersection inequalities (a fixed ordering, a fixed $u_k$ , a fixed neighbor set) would make strictness easier, and an empty or mis-pinned relaxation would make the inclusion false. The definitions here take the full family.

A complete development needs:

convex hulls of finite point sets and separation of a point from them;
connected components of the 2-section graph;
running intersection orderings;
the combinatorics of β-cycles.

The β-cycle and subhypergraph material and Lemma 5 are reusable beyond this mission. Contributions are welcome on any milestone, on alternative proofs of the two strictness cases (for instance by an explicit fractional point), and on a proof of Lemma 6.

Selected references

A. Del Pia and A. Khajavirad, The running intersection relaxation of the multilinear polytope, Mathematics of Operations Research 46(3):1008–1037, 2021. https://doi.org/10.1287/moor.2021.1121
A. Del Pia and A. Khajavirad, A polyhedral study of binary polynomial programs, Mathematics of Operations Research 42(2):389–410, 2017. https://doi.org/10.1287/moor.2016.0804
A. Del Pia and A. Khajavirad, The multilinear polytope for acyclic hypergraphs, SIAM Journal on Optimization 28(2):1049–1076, 2018. https://doi.org/10.1137/16M1095998
M. Padberg, The Boolean quadric polytope: some characteristics, facets and relatives, Mathematical Programming 45:139–172, 1989. https://doi.org/10.1007/BF01589101
C. Beeri, R. Fagin, D. Maier and M. Yannakakis, On the desirability of acyclic database schemes, Journal of the ACM 30(3):479–513, 1983. https://doi.org/10.1145/2402.322389

11 thms2 active usersReviewed

Combinatorics Linear Optimization Optimization·Captain: mikedeng1

The Running Intersection Relaxation of the Multilinear Polytope 1: For Kite-Free β-Acyclic Hypergraphs the Running Intersection Relaxation Equals the Multilinear PolytopeResearch Paper

Motivation

Binary polynomial optimization asks to minimize a polynomial over $\{0,1\}^n$ . The standard way to attack it with linear programming is to introduce one variable $z_e$ for every monomial $\prod_{v\in e} z_v$ and to work with the convex hull of the resulting set of binary points. This convex hull, the multilinear polytope, is the object behind the cutting planes that global solvers such as BARON add at every node of a branch-and-bound tree, and in general its facets are as hard to describe as the original problem is to solve. The useful theory is therefore structural: which hypergraphs of monomials give multilinear polytopes with an explicit, combinatorial description.

A line of work by Del Pia and Khajavirad answers this for increasingly general classes of acyclic hypergraphs: Berge-acyclic and γ-acyclic hypergraphs via flower inequalities (SIAM J. Optim. 2018), sufficient conditions for decomposing multilinear sets (Math. Program. 2018), and, in the paper this mission formalizes (Math. Oper. Res. 2021), the running intersection inequalities, a generalization of flower inequalities that does not need γ-acyclicity. The paper reports that adding these cuts reduces BARON's root-node relaxation gap by more than 95% on most of 35 computer-vision instances.

Setting

A hypergraph $G=(V,E)$ has a finite node set $V$ and a set $E$ of subsets of $V$ , each with at least two nodes. Points live in $\mathbb R^{V+E}$ , one coordinate per node and per edge. The multilinear set and multilinear polytope are

\mathcal S_G=\Big\{z\in\{0,1\}^{V+E}: z_e=\prod_{v\in e}z_v\ \forall e\in E\Big\},\qquad \mathrm{MP}_G=\operatorname{conv}\mathcal S_G .

The standard linearization $\mathrm{MP}^{\mathrm{LP}}_G$ replaces each equation $z_e=\prod_{v\in e}z_v$ by its convex hull over the unit cube: $z_v\le 1$ , $z_e\ge 0$ , $z_e\ge\sum_{v\in e}z_v-|e|+1$ and $z_e\le z_v$ for $v\in e$ .

An ordering $p_1,\dots,p_m$ of a family of sets is a running intersection ordering if each $p_k$ meets the union of its predecessors inside a single predecessor $p_j$ ; write $N(p_k)=p_k\cap\bigcup_{i<k}p_i$ and $N(p_1)=\emptyset$ . Given a center edge $e_0$ and neighbor edges $e_k$ , $k\in K$ , meeting $e_0$ such that the sets $e_0\cap e_k$ admit a running intersection ordering, and nodes $u_k\in N(e_0\cap e_k)$ wherever this set is nonempty, the running intersection inequality is

-\sum_{k:\,N(e_0\cap e_k)\neq\emptyset}z_{u_k}+\sum_{v\in e_0\setminus\bigcup_k e_k}z_v+\sum_{k\in K}z_{e_k}-z_{e_0}\le\omega-1,

with $\omega$ the number of connected components of the hypergraph on $e_0$ with edges $e_0\cap e_k$ . The running intersection relaxation $\mathrm{MP}^{\mathrm{RI}}_G$ is $\mathrm{MP}^{\mathrm{LP}}_G$ together with all these inequalities.

A β-cycle is a cyclic sequence of $t\ge 3$ distinct nodes and distinct edges $v_1,e_1,\dots,v_t,e_t$ in which $v_i$ lies in $e_{i-1}$ and $e_i$ and in no other edge of the cycle; $G$ is β-acyclic if it has none. A kite is three edges $e_0,e_1,e_2$ with $|e_0\cap e_1\cap e_2|\ge 2$ , $(e_0\cap e_1)\setminus e_2\ne\emptyset$ and $(e_0\cap e_2)\setminus e_1\ne\emptyset$ ; $G$ is kite-free if it has none. $G$ is two-laminar if any two distinct edges sharing at least two nodes are strictly nested.

Formalization targets

Goal: Theorem 3 (p. 1023)

For every kite-free β-acyclic hypergraph $G$ without isolated nodes,

\mathrm{MP}_G=\mathrm{MP}^{\mathrm{RI}}_G .

Milestones

In attack order: validity of the inequalities (Proposition 1); heredity of β-acyclicity (Lemma 3); kite-free implies edge-induced subhypergraphs are two-laminar (Lemma 7); β-acyclicity as the running intersection property of every edge subset (Lemma 4); the explicit facet description of $\mathrm{MP}_G$ for two-laminar β-acyclic $G$ by system (20) (Proposition 6) and its consequence $\mathrm{MP}_G=\mathrm{MP}^{\mathrm{RI}}_G$ there (Corollary 3); the decomposition theorem for multilinear sets (Theorem 1); and five steps of the inductive proof of Theorem 3 in §5.3: $G_\omega$ is kite-free β-acyclic with one maximal edge fewer, the inductive step $\mathrm{MP}_{G^+}=\mathrm{MP}^{\mathrm{RI}}_{G^+}$ , Claim 14 on partial hypergraphs, the projection $\mathrm{MP}_G=\mathrm{proj}\,\mathrm{MP}_{G^+}$ , and the Fourier–Motzkin step $\mathrm{MP}^{\mathrm{RI}}_G\subseteq\mathrm{proj}\,\mathrm{MP}^{\mathrm{RI}}_{G^+}$ .

Companions

Theorem 2 (p. 1022), the polynomial-size extended formulation $\mathrm{MP}_{G^+}=\bigcap_{i}\mathrm{MP}_{G^+_i}$ over the maximal edges, and the form (19) taken by running intersection inequalities in kite-free β-acyclic hypergraphs.

Significance

Theorem 3 gives a description of the multilinear polytope in the original space, by inequalities defined combinatorially from the hypergraph, for a class that strictly contains the γ-acyclic hypergraphs covered by flower inequalities. With Theorem 2 it implies that linear optimization and separation over $\mathrm{MP}_G$ are polynomial for kite-free β-acyclic hypergraphs, and that separation can be done without the ellipsoid method. The paper also shows (Proposition 5, a separate mission of this series) that β-acyclicity is necessary for $\mathrm{MP}_G=\mathrm{MP}^{\mathrm{RI}}_G$ , so the characterization sits close to the boundary of what such relaxations can achieve.

All results of this mission are proved in the paper; none is machine-checked. A complete development would be the first formal treatment of hypergraph acyclicity degrees and of multilinear polytopes, and would include a formal Fourier–Motzkin elimination argument on a structured polytope.

Difficulty

The inclusion $\mathrm{MP}_G\subseteq\mathrm{MP}^{\mathrm{RI}}_G$ is a validity check. The reverse inclusion is the content. A direct argument through integrality fails: for two-laminar β-acyclic hypergraphs, facets have general integer coefficients, so total unimodularity and balancedness arguments used for laminar hypergraphs do not apply. The decomposition step is also harder than in earlier work: the shared part of the two pieces may be an edge whose nodes are only partly covered by edges of one side, so a point cannot be written by pairing one vertex of each side. Finally, the induction lifts to $G^+$ , which has an extra variable, and the projection back must be shown to produce only running intersection inequalities, which requires recognizing every Fourier–Motzkin combination as one.

Formalization scope

Nodes form a type α with Fintype and DecidableEq; a point is a function z : α ⊕ Finset α → ℝ, and every polytope of a hypergraph vanishes off that hypergraph's coordinates, so that polytopes of different hypergraphs, lifts and projections are literal sets in one space. Hypergraphs have no loops or parallel edges, as the paper assumes. Orderings are lists, 0-based. The relaxation quantifies over every center, every neighbor set, every running intersection ordering and every choice of the nodes $u_k$ ; the number of components counts isolated nodes and ignores loops. The standard linearization has no row $z_v\ge 0$ , exactly as printed.

One hypothesis is added to the paper: no isolated nodes, on Theorem 3, Corollary 3, Theorem 2 and the inductive step. It is necessary: for $V=\{a,b,c\}$ , $E=\{\{a,b\}\}$ the point with $z_c=-1$ and all other coordinates $0$ lies in $\mathrm{MP}^{\mathrm{RI}}_G$ but not in $\mathrm{MP}_G$ . No other result carries it.

A trivializing formalization is ruled out by construction: restricting the relaxation to one fixed ordering or choice of $u_k$ would make the goal false rather than easy, and the goal is an equality of sets, not an inclusion.

A complete development needs: convex hulls of finite sets of 0/1 points, hypergraph connectivity, β-acyclicity and the running intersection property (Lemma 4 is a classical database-theory theorem of Beeri, Fagin, Maier and Yannakakis), and Fourier–Motzkin elimination. The hypergraph acyclicity layer is reusable beyond this mission, including by the two other missions of this series. Proofs of any milestone, and of reusable lemmas on hypergraph acyclicity, are welcome.

Selected references

A. Del Pia, A. Khajavirad, The running intersection relaxation of the multilinear polytope, Math. Oper. Res. 46(3):1008–1037, 2021. https://doi.org/10.1287/moor.2021.1121
A. Del Pia, A. Khajavirad, The multilinear polytope for acyclic hypergraphs, SIAM J. Optim. 28(2):1049–1076, 2018. https://doi.org/10.1137/16M1095998
A. Del Pia, A. Khajavirad, On decomposability of multilinear sets, Math. Program. 170(2):387–415, 2018. https://doi.org/10.1007/s10107-017-1158-y
C. Beeri, R. Fagin, D. Maier, M. Yannakakis, On the desirability of acyclic database schemes, J. ACM 30(3):479–513, 1983. https://doi.org/10.1145/2402.322389
R. Fagin, Degrees of acyclicity for hypergraphs and relational database schemes, J. ACM 30(3):514–550, 1983. https://doi.org/10.1145/2402.322390

14 thms2 active usersReviewed

Completed

Numerical Analysis Optimization·Captain: mikedeng1

Douglas-Rachford Splitting and ADMM for Nonconvex Optimization: Tight Convergence Results I: Under the Tight Stepsize Bound, the Nonconvex DRS Residual Vanishes and Cluster Points Are StationaryResearch Paper

Why nonconvex Douglas–Rachford splitting

Douglas–Rachford splitting (DRS) minimizes a sum $\varphi=\varphi_1+\varphi_2$ by alternating the proximal mappings of the two terms. It goes back to the alternating-direction schemes for heat conduction of Douglas and Rachford (1956), was cast as a splitting method for monotone operators by Lions and Mercier (1979), and through its dual form, the alternating direction method of multipliers (ADMM), it is a workhorse of signal processing, statistics and distributed optimization. For convex problems its convergence theory is complete. In applications, however, DRS and ADMM are routinely run on nonconvex problems (sparse regression with nonconvex penalties, phase retrieval, feasibility problems with nonconvex sets), and there the classical theory says nothing.

Timeline. Li and Pong (2016) proved subsequential convergence of DRS with $\lambda=1$ for a smooth $\varphi_1$ with Lipschitz gradient, for a sufficiently small stepsize, using the augmented Lagrangian as a merit function, and showed that cluster points are stationary. Li, Liu and Pong (Comput. Optim. Appl. 68(2), 2017) treated the Peaceman–Rachford case $\lambda=2$ with a modified merit function and proved boundedness of the iterates for level-bounded $\varphi$ . Themelis and Patrinos (arXiv:1709.05747, SIAM J. Optim. 2020) obtained convergence for every relaxation $\lambda\in(0,2)$ , and beyond $2$ for strongly convex $\varphi_1$ , under stepsize bounds that they show to be tight. This mission formalizes that convergence result.

Setting

Let $\mathbb R^p$ carry the Euclidean inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$ , and let $\overline{\mathbb R}=\mathbb R\cup\{\infty\}$ . A function $h:\mathbb R^p\to\overline{\mathbb R}$ is proper if it is finite somewhere, and level bounded if every sublevel set $\{x\mid h(x)\le\alpha\}$ , $\alpha\in\mathbb R$ , is bounded. A differentiable $h:\mathbb R^p\to\mathbb R$ is $L$ -smooth if $\|\nabla h(x)-\nabla h(y)\|\le L\|x-y\|$ , and $\sigma$ -hypoconvex if $h-\frac\sigma2\|\cdot\|^2$ is convex; $\sigma$ may be negative.

Assumption I. $\varphi_1:\mathbb R^p\to\mathbb R$ is $L$ -smooth and $\sigma$ -hypoconvex with $\sigma\in[-L,L]$ ; $\varphi_2:\mathbb R^p\to\overline{\mathbb R}$ is proper and lower semicontinuous; and $\varphi=\varphi_1+\varphi_2$ has a minimizer.

The proximal mapping of $h$ with stepsize $\gamma>0$ is the set

\operatorname{prox}_{\gamma h}(x)=\operatorname*{arg\,min}_{w}\Big\{h(w)+\tfrac1{2\gamma}\|w-x\|^2\Big\}.

A DRS run with stepsize $\gamma$ and relaxation $\lambda$ is a sequence $(s^k,u^k,v^k)_{k\in\mathbb N}$ with

u^k\in\operatorname{prox}_{\gamma\varphi_1}(s^k),\qquad v^k\in\operatorname{prox}_{\gamma\varphi_2}(2u^k-s^k),\qquad s^{k+1}=s^k+\lambda(v^k-u^k).

The Douglas–Rachford envelope (DRE) is

\varphi^{\mathrm{DR}}_\gamma(s)=\min_{w}\Big\{\varphi_2(w)+\varphi_1(u)+\langle\nabla\varphi_1(u),w-u\rangle+\tfrac1{2\gamma}\|w-u\|^2\Big\},\qquad u=\operatorname{prox}_{\gamma\varphi_1}(s).

With $p=\sigma/L$ , $[r]_-=\max\{0,-r\}$ and $\delta=\sqrt{(p\lambda)^2-8p(\lambda-2)}$ , the admissible parameters are: $\lambda\in(0,2)$ with $\gamma<\min\{\frac{2-\lambda}{2[\sigma]_-},\frac1L\}$ ; or, when $\sigma>0$ , $2\le\lambda<\frac4{1+\sqrt{1-p}}$ with $\frac{p\lambda-\delta}{4\sigma}<\gamma<\frac{p\lambda+\delta}{4\sigma}$ .

Formalization targets

Goal: Theorem 4.3 (subsequential convergence)

Under Assumption I and admissible $(\gamma,\lambda)$ , every DRS run from any $s^0$ satisfies

$\displaystyle\min_{i\le k}\|u^i-v^i\|=o(1/\sqrt k)$ ;
$(u^k)$ and $(v^k)$ have the same cluster points, each cluster point $u'$ satisfies $0\in\hat\partial\varphi(u')$ , and $\varphi(u')=\lim_k\varphi^{\mathrm{DR}}_\gamma(s^k)$ , a finite limit;
if $\varphi$ is level bounded, $(s^k,u^k,v^k)$ is bounded.

Milestones

In attack order: the lower bounds for smooth hypoconvex functions (Theorem 2.2); single-valuedness and Lipschitz properties of $\operatorname{prox}_{\gamma\varphi_1}$ (Proposition 2.3(i), (ii)); real-valuedness and strict continuity of the DRE (Proposition 3.2); the sandwich $\varphi(v)+\frac{1-\gamma L}{2\gamma}\|u-v\|^2\le\varphi^{\mathrm{DR}}_\gamma(s)\le\varphi(u)$ (Proposition 3.3); $\inf\varphi=\inf\varphi^{\mathrm{DR}}_\gamma$ and the equivalence of level boundedness (Theorem 3.4(i), (iii)); and the sufficient decrease

\varphi^{\mathrm{DR}}_\gamma(s)-\varphi^{\mathrm{DR}}_\gamma(s^+)\ge\frac{c}{(1+\gamma L)^2}\|s-s^+\|^2,\qquad c>0

(Theorem 4.1). Two companion items: Remark 3.1 ( $\varphi_1$ , $\varphi_2$ prox-bounded with threshold at least $1/L$ , and DRS runs exist from every $s^0$ when $\gamma L<1$ ) and the stationarity measure of Theorem 4.3(ii), $\operatorname{dist}(0,\hat\partial\varphi(v^k))\le\frac{1-\gamma\sigma}{\gamma}\|u^k-v^k\|$ .

Significance

The result gives convergence guarantees for DRS with any relaxation parameter $\lambda\in(0,2)$ on nonconvex problems where only $\varphi_1$ is required to be smooth, with stepsizes up to $1/L$ when $\varphi_1$ is convex. The companion mission on tightness (Theorem 4.7 of the paper) shows that DRS can fail to converge for $\gamma>1/L$ , so these ranges cannot be enlarged under Assumption I. Through the equivalence of DRS and ADMM (§5 of the paper, a later mission of this series), the same conclusions transfer to nonconvex ADMM with a tight penalty bound.

The paper's proofs are complete, so the remaining work is formalization. As far as the platform's records show, no machine-checked proof of convergence of nonconvex DRS exists: the published DRS items cover the convex, monotone-operator setting only. The development also produces reusable pieces: the lower bounds for hypoconvex smooth functions, the proximal calculus of smooth functions, and the Douglas–Rachford envelope as a Lyapunov function.

Difficulty

In the convex case DRS is a fixed-point iteration of an averaged operator, and convergence follows from Fejér monotonicity. For nonconvex $\varphi_2$ the reflected proximal maps are not nonexpansive, so this argument has no starting point. Convergence must instead come from a merit function that decreases along the iterates, and the difficulty is to find one whose decrease survives every relaxation $\lambda\in(0,2)$ with stepsizes all the way up to $1/L$ . Small-stepsize decrease estimates for $\lambda=1$ do not extend to the full range. Cluster points must then be shown stationary for a lower semicontinuous, possibly nonconvex $\varphi_2$ , which needs the outer semicontinuity of its proximal mapping rather than any continuity.

Formalization scope

Points are EuclideanSpace ℝ (Fin p); every dimension $p$ , including $0$ , is allowed. $\varphi_1$ is real-valued and $\varphi_2$ , $\varphi$ and $\varphi^{\mathrm{DR}}_\gamma$ are EReal-valued and never $-\infty$ . The proximal mapping is a set, and runs are selections from it; no proximal function is chosen. The DRE is the EReal infimum of the expression above over $u\in\operatorname{prox}_{\gamma\varphi_1}(s)$ , which is the page's value because that set is a singleton for $\gamma L<1$ . Stationarity is $0\in\hat\partial\varphi(u')$ in the regular (Fréchet) subdifferential, the published platform definition NonconvexSplitting.Shared.IsRegularSubgrad; this is what the proof gives and is stronger than limiting stationarity. Cluster points are MapClusterPt points, and the rate $o(1/\sqrt k)$ is $\sqrt k\min_{i\le k}\|u^i-v^i\|\to0$ . All reciprocal bounds are multiplied out ( $\gamma L<1$ , $2\gamma[\sigma]_-<2-\lambda$ ), respecting the paper's convention $1/0=\infty$ .

Standing assumptions are Assumption I plus $L>0$ , which is added because the ranges use $p=\sigma/L$ ; for $L=0$ , $\varphi_1$ is affine. Three printed statements are corrected:

the closing "In fact" bound of Theorem 4.3(ii) is printed with $\frac{1-\gamma\sigma}{2\gamma}$ , which fails for $\varphi_1\equiv0$ , $\varphi_2=\frac a2x^2$ (the distance is $\|u-v\|/\gamma$ ); it is a separate item with $\frac{1-\gamma\sigma}{\gamma}$ and is not part of the goal;
in (4.3) the second entry of the max is printed $\frac12-\frac{\gamma L}{\lambda}$ ; the proof ((4.8), p. 11) gives $\frac{\gamma L}{\lambda}-\frac12$ , and the printed constant fails for $\varphi_1=\frac L2x^2$ , $\varphi_2\equiv0$ , $\lambda=1$ , $\gamma L=0.9$ ;
(4.5) is printed with $\frac{\sigma}{\lambda}$ where the proof ((4.10), p. 12) gives $\sigma$ ; the printed constant is negative at $\sigma=L$ , $\lambda=3$ , $\gamma L=0.75$ , inside the range (4.4).

The goal does not mention these constants. Its hypotheses are exactly Assumption I with $L>0$ , $\gamma>0$ , the admissible ranges, and a DRS run. The goal assumes no decrease of the envelope, no square-summability, no boundedness of the iterates, and no residual $u^k\ne v^k$ . The companion Remark 3.1 shows that runs exist, so the goal is not vacuous.

A complete development needs the regular subdifferential calculus for a smooth plus lower semicontinuous sum, the proximal optimality condition $\frac1\gamma(x-\bar x)\in\hat\partial h(\bar x)$ , existence of proximal points for prox-bounded lsc functions, and the outer semicontinuity of the proximal mapping. All of these are reusable beyond this mission. Contributions to any milestone, or to these general lemmas as separate theorems, are welcome.

Selected references

A. Themelis, P. Patrinos, Douglas–Rachford splitting and ADMM for nonconvex optimization: tight convergence results, SIAM J. Optim. 30(1):149–181, 2020; arXiv:1709.05747v4. https://arxiv.org/abs/1709.05747 , https://doi.org/10.1137/18M1163993
G. Li, T. K. Pong, Douglas–Rachford splitting for nonconvex optimization with application to nonconvex feasibility problems, Math. Program. 159:371–401, 2016. https://doi.org/10.1007/s10107-015-0963-5
G. Li, T. Liu, T. K. Pong, Peaceman–Rachford splitting for a class of nonconvex optimization problems, Comput. Optim. Appl. 68(2):407–436, 2017 (reference [24] of the paper).
P.-L. Lions, B. Mercier, Splitting algorithms for the sum of two nonlinear operators, SIAM J. Numer. Anal. 16(6):964–979, 1979. https://doi.org/10.1137/0716071
R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3

11 thms2 active usersReviewed

Completed

Dynamical Systems Probability Stochastic Systems·Captain: mikedeng1

Propagation of Chaos for Stochastic Spatially Structured Neuronal Networks with Delay driven by Jump Diffusions 2: The Neuronal Network Converges in L² to Its McKean–Vlasov LimitResearch Paper

Motivation

Large networks of neurons are often modelled as systems of coupled stochastic differential equations: each neuron carries a low-dimensional state (a membrane potential and recovery variables, as in the FitzHugh–Nagumo model), receives synaptic input from the other neurons with a transmission delay, and is perturbed by noise. Because the number of neurons is large, one studies the mean-field limit: as the population grows, each neuron should evolve independently of every other fixed neuron, driven by its own noise and by an averaged population input. This asymptotic independence is called propagation of chaos, and the limiting single-neuron equation is a McKean–Vlasov equation.

Mehri, Scheutzow, Stannat and Zangeneh (arXiv:1805.01654v3, Ann. Appl. Probab. 2020, DOI 10.1214/19-AAP1499) prove propagation of chaos for a model combining features that earlier work treated separately: monotone (one-sided Lipschitz) local dynamics, general path-dependent delays, Lévy-type jump noise, spatial structure with several subpopulations, and a random environment (disorder). Earlier mean-field results for neuronal networks were obtained under global Lipschitz assumptions (Quiñinao and Touboul 2015; Touboul 2014, two papers), for locally Lipschitz coefficients (Baladron, Fasoli, Faugeras and Touboul 2012, with the clarification note of Bossy, Faugeras and Talay 2015) and for one-sided Lipschitz coefficients (Luçon and Stannat 2014; Touboul 2012); with jump noise, only under global Lipschitz or gradient-type local dynamics (Andreis, Dai Pra and Fischer 2018). This mission formalizes the paper's second main result, Theorem 1.8. The first mission of the series formalizes the well-posedness of the McKean–Vlasov equation (Theorem 1.5).

Setting

Neurons sit at positions $r$ in a bounded set $\Gamma\subset\mathbb R^k$ , partitioned into $P$ measurable subpopulation regions $\Gamma_\alpha$ . The $N$ -th network consists of a finite set $\mathcal A_N\subset\Gamma$ of $N$ positions, and neurons of subpopulation $\alpha$ carry the weight $1/\mathcal S_{\mathcal A_N,\alpha}$ . The state $X^{r,\mathcal A_N}_t\in\mathbb R^d$ of the neuron at $r$ solves the network equation (1)

dX^{r,\mathcal A_N}_t=f\,dt+g\,dW^r_t+\int_U h\,\tilde N^r(dt,d\xi)+\sum_{\alpha=1}^P\frac{1}{\mathcal S_{\mathcal A_N,\alpha}}\sum_{\tilde r\in\mathcal A_N\cap\Gamma_\alpha}\Big[\theta\,dt+\beta\,dB^{r,\alpha}_t+\int_U\eta\,\tilde N^{r,\alpha}(dt,d\xi)\Big],

where $f,g,h$ are evaluated at $(t,r,X^{r,\mathcal A_N}_{t-},\omega')$ and $\theta,\beta,\eta$ at $(t,r,\tilde r,X^{r,\mathcal A_N}_{t-},X^{\tilde r,\mathcal A_N}_{(t-\tau)^-:t^-},\omega')$ , the last argument being the path of the presynaptic neuron over the delay window $[t-\tau,t]$ . The noises $W^r$ , $B^{r,\alpha}$ are independent Brownian motions, $\tilde N^r$ , $\tilde N^{r,\alpha}$ independent compensated Poisson random measures with intensity $dt\otimes\nu$ , and $\omega'$ is a random disorder with expectation $\mathcal E$ . Each neuron starts from a path $z^r$ on $[-\tau,0]$ .

Given a finite measure $\mathcal R$ on $\Gamma$ with $\mathcal R(\Gamma_\alpha)=1$ , the McKean–Vlasov equation (6) describes a continuum of neurons $X^r$ , $r\in\Gamma$ , whose interaction is $\sum_\alpha\int_{\Gamma_\alpha}\tilde{\mathbb E}[\theta(t,r,r',X^r_{t-},\tilde X^{r'}_{(t-\tau)^-:t^-},\omega')]\mathcal R(dr')$ , with $\tilde X$ an independent copy of $X$ (and likewise for $\beta$ , $\eta$ ). The mean-field equation (5) for a neuron $r$ of the network has the same form, with $X^r$ replaced by a process $\bar X^r$ that starts from the same $z^r$ and is driven by the same noises $W^r, B^{r,\alpha}, \tilde N^r,\tilde N^{r,\alpha}$ as neuron $r$ of the network, while the interaction is computed from the law of the solution of (6).

Formalization targets

Goal: Theorem 1.8

Under Hypothesis 1.6 and the chaotic initial condition (the $z^r$ are independent, with $z^r$ distributed as $\hat z^\alpha$ for $r\in\Gamma_\alpha$ ),

\lim_{N\to\infty}\mathcal E\sup_{t\in[-\tau,T],\,r\in\mathcal A_N}\mathbb E\big|X^{r,\mathcal A_N}_t-\bar X^r_t\big|^2=0 .

The theorem asserts convergence without a rate, which is the stable form of the result.

Milestones

Proposition 1.2: the network equation (1) is well posed.
Lemma 1.7: positions in one cell $\Gamma^{m,\varepsilon}_\alpha$ of the partition of Hypothesis 1.6 have solutions of (6) within $C_2(t,\omega')\varepsilon$ in mean square.
Display (18): the first moment estimate for $X^{r,\mathcal A_N}-\bar X^r$ , in terms of the fluctuation terms $I^\theta_\alpha$ , $I^\beta_\alpha$ , $I^\eta_\alpha$ .
The bound (p. 20) of each $I$ -term by $6(\cdots)C_2(t,\omega')$ .
The Gronwall bound (p. 21) with constant $36$ , at a fixed disorder.
The bound (p. 21) after integration over the disorder, with a constant $C(T)$ independent of $\varepsilon$ and $N$ .

The proof also uses Lemma 1.4 (the moment bound $C_1$ for solutions of (6)), which is a milestone of the first mission of this series and is not restated here.

Significance

Theorem 1.8 justifies replacing a large, spatially structured network of delayed, jump-driven neurons by a single McKean–Vlasov equation indexed by position. The limit is the object on which neural field models and their bifurcation analysis are built; the theorem identifies the hypotheses on the spatial distribution of neurons (condition (10): the neuron counts per cell, normalized by the weights, converge to $\mathcal R$ ) under which that replacement is valid in a random environment.

The result is proved in the paper; no machine-checked proof exists. Formalizing it requires a coherent Lean layer for strong solutions of delay SDEs with jumps, mean-field interaction terms, Poisson random measures with product marks, and independence of countable families of drivers. The intermediate bounds of §3 are explicit and quantitative, and each is a self-contained target.

Difficulty

The interaction of the network is an empirical average over finitely many neurons, while the limit uses an expectation over a continuum of positions. The difference splits into three errors of different nature: a fluctuation term, whose control requires that the limit processes $\bar X^{\tilde r}$ of distinct neurons be independent (which holds only because each is driven by its own noise and starts from an independent initial condition); a spatial discretization error within each cell, which requires a quantitative regularity of the solution of (6) in the position variable; and a counting error between the neuron counts and the measure $\mathcal R$ . A naive comparison of the network with (6) directly, without the coupled processes $\bar X^r$ of (5), gives no pathwise relation and does not work. The coefficients are only one-sided Lipschitz in the local variable, so moment bounds must come from monotonicity rather than from global Lipschitz estimates, and the disorder enters the constants through exponentials whose integrability is exactly assumption (H6).

Formalization scope

Positions are EuclideanSpace ℝ (Fin k), states EthierKurtz.SDEState d, and subpopulations Fin P (0-based). Neurons carry labels in ℕ with an injective position map, so $\mathcal A_N$ is a finite set of labels and $\bigcup_N\mathcal A_N$ is countable. Brownian integrals are the published EthierKurtz.HasBrownianItoIntegral per coordinate, compensated jump integrals the published JacodTodorov10.LLN.HasCompInt, and all Poisson measures of the network form one (𝓕_t)-Poisson random measure on a product mark space. Integrands are cut off after the horizon $T$ . All expectations, suprema and the disorder expectation $\mathcal E$ are taken in $[0,\infty]$ , so no statement can be satisfied by a junk value of a real integral or supremum; (H6) states the boundedness of its supremum explicitly. The copy $\hat X$ enters only through its law: the solution of (6) lives on its own probability space and the mean-field terms are expectations over it.

Conventions and corrections, all disclosed in the items: the theorem is stated for every family of solutions of (1), (5) and (6) (hypotheses), not for "the" solutions; (H1′) is printed with $x-y$ and is read as $x-\tilde x$ ; $I^\eta_\alpha$ carries the expectation of (17), which the display on p. 20 omits; the second Gronwall inequality on p. 21 (constant $144$ ) drops a factor of $C_1$ and is not posed; the coefficients' path argument carries the product σ-algebra; the filtration satisfies the usual conditions (Appendix A); the solution class of (6) is a bound for every time. The solution notions are not trivializing: every stochastic integral is tied to the given noise by a published predicate, the mean-field terms are computed from the solution of (6) itself, the limit processes share the network's noise and initial conditions, and the finite constant of the integrated bound is quantified before $\varepsilon$ and $N$ .

Reusable beyond this mission: the strong-solution predicate for jump SDEs with delay, the noise predicates for countable families of drivers, and the network and mean-field interaction terms. Contributions toward a stochastic calculus for these predicates (Itô's formula for $|X|^2$ with jumps, Gronwall arguments with left limits) are welcome.

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, Ann. Appl. Probab. 30 (2020); arXiv:1805.01654v3. https://arxiv.org/abs/1805.01654
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). https://doi.org/10.1186/2190-8567-2-10
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). https://doi.org/10.1186/s13408-015-0031-8
J. Touboul, Propagation of chaos in neural fields, Ann. Appl. Probab. 24(3):1298–1328 (2014); arXiv:1108.2414. https://arxiv.org/abs/1108.2414
J. Touboul, Spatially extended networks with singular multi-scale connectivity patterns, J. Stat. Phys. 156(3):546–573 (2014).
C. Quiñinao, J. Touboul, Limits and dynamics of randomly connected neuronal networks, Acta Appl. Math. 136(1):167–192 (2015).
E. Luçon, W. Stannat, Mean field limit for disordered diffusions with singular interactions, Ann. Appl. Probab. 24(5):1946–1993 (2014).
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).

15 thms2 active usersReviewed

Control Theory Dynamical Systems Graph Theory+1·Captain: mikedeng1

Sub/Super-Stochastic Matrix with Applications to Bipartite Tracking Control over Signed Networks 3: ψ < 1/(τd_M), Structural Balance and Leader Reachability Give Asynchronous Bipartite TrackingResearch Paper

Motivation

Networks of agents that interact both cooperatively and competitively are modelled by signed graphs: a positive edge weight means that one agent moves towards another, a negative weight means that it moves towards the other's opposite. Since Altafini's work on consensus over antagonistic networks (IEEE TAC 2013), the standard target on such networks has been bipartite consensus or bipartite tracking: the agents split into two camps that converge to values of equal size and opposite sign. With a leader, the camp containing the leader tracks the leader's state and the other camp tracks its negative.

Most analyses assume that all agents update at the same instants. In practice agents sample and communicate on their own clocks. Shi, Zheng, Shao and Cheng (arXiv:2004.01867v2, SIAM J. Control Optim. 2021) handle this asynchronous setting with a matrix tool: products of sub-stochastic matrices (nonnegative, row sums at most one) whose row-sum deficits propagate along the communication graph. This mission formalizes their first application, bipartite tracking of first-order agents with a static leader (§3).

Setting

There is one leader $v_0$ and $n$ followers $v_1,\dots,v_n$ . Follower weights form a matrix $\mathcal A=[a_{ij}]\in\mathbb R^{n\times n}$ : the edge $(v_j,v_i)$ exists iff $a_{ij}\neq 0$ , cooperative if $a_{ij}>0$ , competitive if $a_{ij}<0$ . The number $a_{i0}$ is the weight of the leader edge $(v_0,v_i)$ , which exists iff $a_{i0}\ne 0$ . The digraph $\tilde{\mathcal G}$ consists of the followers' digraph, the leader and the leader edges.

C1 (structural balance). The agents split as $\mathcal V_1\cup\mathcal V_2$ with $v_0\in\mathcal V_1$ , every weight inside a set is $\ge 0$ and every weight between the sets is $\le 0$ .
C2 (leader reachability). Every follower is reached from $v_0$ by a directed path in $\tilde{\mathcal G}$ .

Time is discrete with step size $\tau>0$ . Follower $v_i$ communicates only at its own instants $s^i_0\tau<s^i_1\tau<\cdots$ with $s^i_0=0$ and

s^i_{k+1}-s^i_k\le h\qquad(2.10)

for a constant $h\in\mathbb Z_+$ . Positions $x_i(k)\in\mathbb R^p$ evolve by $x_0(k+1)=x_0(k)$ and $x_i(k+1)=x_i(k)+\tau u_i(k)$ , with the asynchronous protocol

u_i(k)=\psi\sum_{v_j\in\mathcal N_i}|a_{ij}|\big[\operatorname{sgn}(a_{ij})x_j(k)-x_i(k)\big]+\psi|a_{i0}|\big[\operatorname{sgn}(a_{i0})x_0(k)-x_i(k)\big]

at the instants of $v_i$ , and $u_i(k)=0$ otherwise. Here $\psi>0$ is a gain. Bipartite tracking (Definition 3.1) means $\|x_i(k)-x_0(k)\|\to 0$ for $v_i\in\mathcal V_1$ and $\|x_i(k)+x_0(k)\|\to 0$ for $v_i\in\mathcal V_2$ . With $d_M=\max_i\big(\sum_{v_j\in\mathcal N_i}|a_{ij}|+|a_{i0}|\big)$ , the gain condition is

\psi<\frac{1}{\tau d_M}.\qquad(3.7)

In the error coordinates $e_i=x_i-x_0$ on $\mathcal V_1$ and $e_i=-x_i-x_0$ on $\mathcal V_2$ , the closed loop is $e(k+1)=(M(k)\otimes I_p)e(k)$ with $M(k)=I_n-\tau\psi\mathcal D(k)-\tau\psi\mathcal B(k)+\tau\psi|\mathcal A(k)|$ , where only the rows of followers active at time $k\tau$ differ from the identity.

Formalization targets

Goal: Theorem 3.3, sufficiency

\psi<\frac1{\tau d_M},\ \ \mathrm{C1},\ \ \mathrm{C2}\ \Longrightarrow\ \lim_{k\to\infty}\|x_i(k)-x_0(k)\|=0\ (v_i\in\mathcal V_1),\quad \lim_{k\to\infty}\|x_i(k)+x_0(k)\|=0\ (v_i\in\mathcal V_2),

for every choice of instants satisfying (2.10) and every initial state.

Milestones

Theorem 2.4 1): a product $F_q\cdots F_1$ of sub-stochastic matrices is sub-stochastic.
Theorem 2.4 2): with positive diagonals, if every row $i_2$ is fed through $[F_{s_2}]_{i_2i_1}>0$ by a row $i_1$ with $\Lambda_{i_1}[F_{s_1}]<1$ , $s_1<s_2$ , then $\|\prod_{s=1}^qF_s\|_\infty<1$ and $\rho(\prod_{s=1}^qF_s)<1$ .
The matrices $M(k)$ (p. 15): under (3.7) they are sub-stochastic with positive diagonals, and $\Lambda_i[M(k)]<1$ exactly when $v_i$ hears the leader at $k\tau$ .
Error system (3.6): under C1, $e_i(k+1)=\sum_j[M(k)]_{ij}e_j(k)$ .
Lemma 3.2: under (3.7), C1 and C2, $\big\|\prod_{s=k}^{k+Ph-1}M(s)\big\|_\infty<1$ for every $k$ , where $P=\max_i d(v_0,v_i)$ is the largest directed distance from the leader.

Significance

The theorem says that asynchrony costs nothing qualitatively: as long as every follower communicates at least once every $h$ steps and the gain respects (3.7), the network reaches bipartite tracking under the same topological conditions C1 and C2 as in the synchronous case. No common clock, dwell-time condition or joint connectivity of the switching graphs is required. The same product argument is reused in the rest of the paper for second-order and general linear agents, delays and switching topologies, so the milestones here are the base case of that series.

The result is proved in the paper; it has not been formalized. Formalizing it produces a checked theory of products of sub-stochastic matrices with row-sum deficits (Theorem 2.4), which applies to positive switched systems in general, and a reusable encoding of signed digraphs with a leader, structural balance and asynchronous protocols.

Difficulty

Each single matrix $M(k)$ is only marginally stable: its rows of followers that do not hear the leader at time $k\tau$ sum to exactly one, so no single step contracts, and the spectral radius of an individual $M(k)$ may equal one. Contraction appears only in products, and only once a deficit created at a leader edge has had time to travel along the paths of C2, one edge per window of $h$ steps; this requires that deficits never disappear again, which is where positive diagonals (from (3.7)) enter. The passage from "every window product has $\|\cdot\|_\infty<1$ " to convergence also needs a uniform bound below one over all windows; the paper's (3.14) uses it without comment. The bound holds because $M(k)$ depends on $k$ only through the set of active followers, so the window products range over a finite set.

Formalization scope

Followers are Fin n (0-based) and the leader is not an index; $a_{ij}$ is a i j and $a_{i0}$ is b i. Positions lie in EuclideanSpace ℝ (Fin p); the paper's norm is unspecified and all norms on $\mathbb R^p$ give the same limits. Eigenvalues are complex: $\rho(F)<1$ means every element of spectrum ℂ of the complexified matrix has modulus $<1$ . $\|F\|_\infty$ is the largest absolute row sum. Products multiply later factors on the left. $\operatorname{sgn}$ is Real.sign. The maxima $d_M$ and $P$ are given as values with IsGreatest hypotheses over exactly the printed sets, and (3.7) is kept as printed. C1 is stated for the partition $\mathcal V_1=\{v_0\}\cup V_1$ , $\mathcal V_2=$ the remaining followers; fixing the leader in $\mathcal V_1$ is the paper's "with no loss of generality" convention. Definition 3.1 is stated for that same partition.

Only the "if" half of Theorem 3.3 is a target. Definition 3.1 presupposes the partition of C1, so necessity of C1 has no formal meaning, and the printed necessity argument is an informal case discussion. Theorem 2.4 2) is stated with one $(i_1,s_1,s_2)$ per row $i_2$ , as its proof and the example on p. 8 use it; this is implied by the literal reading.

Three formalizations would trivialize the goal and are ruled out: a protocol in which every follower updates at every step (the synchronous special case, which drops the asynchronous instants); dropping the sign conditions of C1, or leaving the leader's side free, under which the followers of $\mathcal V_2$ need not approach $-x_0$ ; and a goal stated about the error system (3.6) instead of the agents' positions $x_i$ .

The development needs finite matrix products, the ∞-norm bound on eigenvalues (Gershgorin), and elementary walk reachability in digraphs. All of these exist in Mathlib in some form. Contributions are welcome on every milestone. The product theorem 2.4 does not depend on the network model and is reusable for positive switched systems.

Selected references

L. Shi, W. X. Zheng, J. Shao, Y. Cheng, Sub/super-stochastic matrix with applications to bipartite tracking control over signed networks, arXiv:2004.01867v2, 2020; SIAM J. Control Optim. 59 (2021). https://arxiv.org/abs/2004.01867, https://doi.org/10.1137/19M1239982
C. Altafini, Consensus problems on networks with antagonistic interactions, IEEE Trans. Automat. Control 58(4), 2013. https://doi.org/10.1109/TAC.2012.2224251

9 thms2 active usersReviewed

Probability Stochastic Systems·Captain: mikedeng1

Liouville Quantum Gravity and the Brownian Map II: Geodesics and Continuity of the Embedding: A Quantitative Kolmogorov–Čentsov Criterion, P[M ≥ t] ≤ c₁t^(−α) for the Hölder Norm MResearch Paper

Motivation

The Kolmogorov–Čentsov continuity criterion is the standard way to prove that a random field has a continuous version: a moment bound on increments, $\mathbf E|X_u - X_v|^\alpha \le c_0|u - v|^{d+\beta}$ , yields a modification whose paths are Hölder continuous of every order $\gamma < \beta/\alpha$ (Karatzas–Shreve 1991, §2.2; Revuz–Yor 1999, Ch. I). It is used for Brownian motion, Brownian sheets, solutions of stochastic PDEs, Gaussian free field approximations and many other random fields.

The classical statement says only that the Hölder constant $M$ is finite almost surely. Many applications need more: a bound on the tail $\mathbf P[M \ge t]$ whose constant depends only on the parameters $\alpha, \beta, c_0$ and not on the particular field, so that the bound holds uniformly over a family of fields.

This mission formalizes such a quantitative version, Proposition 2.3 in §2.3 of J. Miller and S. Sheffield, Liouville quantum gravity and the Brownian map II: geodesics and continuity of the embedding (Ann. Probab. 2021). The authors state it, note that it follows "by carefully following the proof" of the classical criterion, and write the proof out (pp. 30–31). They apply it to the circle-average process of the Gaussian free field (Proposition 2.4, p. 33) and again in Lemma 5.12 (p. 63).

The paper's main theorems (the $\sqrt{8/3}$ -Liouville quantum gravity sphere equipped with the QLE(8/3, 0) metric has the law of the Brownian map; continuity of the embedding) are not part of this mission. Their objects, among them the Gaussian free field, SLE $_6$ , quantum surfaces, the QLE metric of Miller–Sheffield 2020 and the Brownian map, have no formal substrate in Mathlib or on the platform. Proposition 2.3 is a self-contained probabilistic tool that the paper proves in full, and it is statable today.

Setting

Fix a dimension $d \in \mathbb N$ . The index set is the cube $[0,1]^d$ with the Euclidean distance $|u - v|$ . A random field is a family $(X_u)_{u \in [0,1]^d}$ of real random variables on a probability space $(\Omega, \mathcal F, \mathbf P)$ . The field satisfies the Kolmogorov condition with constants $\alpha, \beta, c_0 > 0$ if

\mathbf E\big[|X_u - X_v|^\alpha\big] \le c_0 |u - v|^{d+\beta} \qquad \text{for all } u, v \in [0,1]^d. \tag{2.6}

A modification of $X$ is a field $Y$ on the same space with $\mathbf P[Y_u = X_u] = 1$ for every $u$ . For $\gamma > 0$ , the $\gamma$ -Hölder norm of a function $f$ on the cube is

M_\gamma(f) = \sup_{u \ne v} \frac{|f(u) - f(v)|}{|u - v|^\gamma} \in [0, \infty].

The proof works on the dyadic grid $\mathcal D_k$ , the points of the cube whose coordinates are integer multiples of $2^{-k}$ , and on the set $\widetilde{\mathcal D}_k$ of adjacent pairs $\{u, v\} \subseteq \mathcal D_k$ , which differ in exactly one coordinate, by $2^{-k}$ . In Lean the cube is Cube d, and the grid and the pairs are dyadicGrid d k and IsAdjacentPair d k u v.

Formalization targets

Goal: Proposition 2.3 (p. 30)

For every $\gamma \in (0, \beta/\alpha)$ there is a constant $c_1(\gamma) > 0$ , depending only on $d, \alpha, \beta, \gamma, c_0$ , such that every field satisfying (2.6) has one modification $Y$ with, for every $\gamma \in (0, \beta/\alpha)$ ,

\forall \omega\ \exists M > 0:\ |Y_u(\omega) - Y_v(\omega)| \le M|u - v|^\gamma \ \ \forall u, v, \tag{2.7}

\mathbf P\big[M_\gamma(Y(\omega)) \ge t\big] \le c_1(\gamma)\, t^{-\alpha} \qquad \text{for all } t \ge 1. \tag{2.8}

Milestones (attack order)

(2.9), p. 30: $\mathbf P[|X_u - X_v| \ge \delta] \le c_0 \delta^{-\alpha}|u - v|^{d+\beta}$ .
(2.10), p. 31: for $\{u, v\} \in \widetilde{\mathcal D}_k$ , $\mathbf P[|X_u - X_v| \ge t2^{-\gamma k}] \le c_0 t^{-\alpha} 2^{-k(d+\beta-\alpha\gamma)}$ .
(2.11), p. 31: $\mathbf P[\max_{\widetilde{\mathcal D}_k} |X_u - X_v| \ge t2^{-\gamma k}] \le c_1 t^{-\alpha}2^{-k(\beta-\alpha\gamma)}$ , with $c_1$ uniform in $k$ , $t$ and the field (this $c_1$ is not the one of (2.8)).
(2.12), p. 31: $\mathbf P[\sup_k \max_{\widetilde{\mathcal D}_k} 2^{\gamma k}|X_u - X_v| \ge t] \le c_2 t^{-\alpha}$ .
Closing claim of the proof, p. 31: a deterministic statement. If $2^{\gamma k}|f(u) - f(v)| \le t$ for all adjacent pairs at all levels, then $|f(u) - f(v)| \le c_3 t|u - v|^\gamma$ for all dyadic $u, v$ , with $c_3$ depending on $d, \gamma$ only.
(2.7), p. 30: the classical criterion alone, a modification that is $\gamma$ -Hölder for every $\gamma \in (0, \beta/\alpha)$ .

Significance

The tail bound (2.8) is what makes the criterion usable for families of fields. In the paper, it bounds the modulus of continuity of the Gaussian free field circle averages at every scale with a single constant, which feeds the estimates on the Liouville quantum gravity metric. More generally, polynomial tails for Hölder norms with field-independent constants are the input to tightness arguments for sequences of random fields, to union bounds over many scales or many fields, and to moment bounds for Hölder norms.

The result itself is known: the authors derive it from the textbook proof, which they write out. What is missing is a machine-checked version. At the pinned Mathlib revision, ProbabilityTheory.IsKolmogorovProcess defines the hypothesis (2.6), but no continuity theorem is proved from it, qualitative or quantitative. The platform has an Open goal for the qualitative one-parameter theorem on $[0, \infty)$ , KolmogorovChentsov.exists_modification_holderOnWith_Icc, a different statement that the mission does not duplicate. A proof of this mission's goal would give the classical $d$ -parameter criterion on the cube (milestone 6) and its quantitative form together.

Difficulty

The probabilistic steps (2.9)–(2.12) are Markov's inequality and two union bounds. They become concrete once the adjacent pairs are counted: $|\widetilde{\mathcal D}_k|$ is of order $d\,2^{dk}$ , and summing over scales needs $\gamma < \beta/\alpha$ . Formalizing them requires care with suprema in $[0,\infty]$ and with outer measures of events that are not obviously measurable.

The central difficulty is the deterministic chaining claim and the passage from dyadic points to the whole cube. The paper calls the claim "not difficult to see", but its constant must be uniform over pairs of dyadic points of arbitrarily fine and unequal levels, and the obvious attempt, comparing values along the straight segment between two points, fails because the points of the segment are not dyadic, so the hypothesis says nothing about them. The second difficulty is the modification itself: one field $Y$ must serve every $\gamma < \beta/\alpha$ at once, must agree with $X$ almost surely at every point, and the tail bound for the dyadic supremum must transfer to the Hölder norm over the whole cube, an uncountable supremum whose event is not obviously measurable.

Formalization scope

Index set: Cube d, the subtype of EuclideanSpace ℝ (Fin d) with coordinates in $[0,1]$ , so $|u - v|$ is Euclidean. Because all constants are existential, the statements do not depend on the norm, but Euclidean is the default reading.
Hypothesis (2.6): Mathlib's IsKolmogorovProcess X P α (d + β) c₀ with c₀ : ℝ≥0, plus 0 < α, 0 < β, 0 < c₀. It reads (2.6) with the lower Lebesgue integral in $[0,\infty]$ , so it cannot hold through a junk value of a non-integrable expectation. It also requires each pair $(X_u, X_v)$ to be Borel measurable, which is the measurability included in "random field". The probability space is [IsProbabilityMeasure P].
Hölder norm: $M_\gamma$ is eHolderNorm γ, valued in $[0,\infty]$ . A real supremum, which is 0 on unbounded families and would make (2.8) trivially true, is ruled out. The supremum of (2.12) is likewise an ℝ≥0∞-valued ⨆, and its event is $\{t \le \sup\}$ , not the weaker "some term is $\ge t$ ".
Uniformity: the constants $c_1$ of (2.8) (a function of $\gamma$ ), $c_1$ of (2.11), $c_2$ and $c_3$ are quantified before the probability space and the field. A version in which the constant may depend on the field, or one with a different modification for each $\gamma$ , is a weaker theorem and is ruled out. The probability space ranges over Type (universe 0).
Conventions: (2.7) holds for every $\omega$ (the paper states it for the modification itself). Probabilities of events not shown measurable are outer measures. The dyadic level $k$ ranges over $\mathbb N$ including $0$ . Adjacent pairs are ordered, which doubles a count that the constants absorb. The milestones add $t > 0$ and $\delta > 0$ , which the paper leaves implicit, and carry $\gamma \in (0, \beta/\alpha)$ from (2.10) on. The constants may depend on $d$ , which the paper's list " $\alpha, \beta, \gamma, c_0$ " leaves implicit.

A complete development needs counting lemmas for the dyadic grid, a chaining lemma on dyadic points, and the extension of a uniformly Hölder function from a dense subset (Mathlib's HolderOnWith and uniform-continuity extension tools apply). The chaining lemma and the quantitative criterion are reusable for any Hölder-regularity argument on cubes. Contributions are welcome for each milestone independently and for an alternative proof of the goal through Mathlib's PairReduction chaining machinery.

Selected references

J. Miller, S. Sheffield, Liouville quantum gravity and the Brownian map II: geodesics and continuity of the embedding, Ann. Probab., 2021 (accepted manuscript, Apollo repository, University of Cambridge). https://doi.org/10.1214/21-AOP1506
J. Miller, S. Sheffield, Liouville quantum gravity and the Brownian map I: the QLE(8/3, 0) metric, Invent. Math. 219(1), 75–152, 2020. https://arxiv.org/abs/1507.00719
I. Karatzas, S. E. Shreve, Brownian Motion and Stochastic Calculus, 2nd ed., Graduate Texts in Mathematics 113, Springer, 1991. https://doi.org/10.1007/978-1-4612-0949-2
D. Revuz, M. Yor, Continuous Martingales and Brownian Motion, 3rd ed., Grundlehren der Mathematischen Wissenschaften 293, Springer, 1999. https://doi.org/10.1007/978-3-662-06400-9
Mathlib, Mathlib/Probability/Process/Kolmogorov.lean (the predicate IsKolmogorovProcess). https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Probability/Process/Kolmogorov.lean

8 thms2 active usersReviewed

Completed

Operations Research Optimal Transport Optimization+1·Captain: mikedeng1

Sinkhorn Distributionally Robust Optimization 1: Strong Duality — the Worst-Case Expectation over a Sinkhorn Ball Equals inf over λ ≥ 0 of λρ̄ + λε·E log E_Q[e^{f/(λε)}]Research Paper

Motivation

Distributionally robust optimization (DRO) hedges a decision against uncertainty in the data distribution. It minimizes the worst-case expected loss over an ambiguity set of distributions around a nominal one, typically the empirical distribution of the data. Ambiguity sets built from the Wasserstein (optimal-transport) distance are standard in operations research and machine learning, because they contain distributions with supports different from the nominal one. A known drawback is that the worst case is attained at discrete distributions, which is unrealistic when the true distribution is continuous.

Wang, Gao and Xie (arXiv:2109.11926v5) replace the Wasserstein distance by the Sinkhorn distance, the entropically regularized optimal-transport cost of Cuturi (NeurIPS 2013). Their main theorem is a strong duality result: the infinite-dimensional worst-case problem over a Sinkhorn ball equals a one-dimensional convex minimization. This mission formalizes that theorem.

Timeline:

2013: Cuturi introduces the Sinkhorn distance as a fast surrogate for optimal transport.
2016–2023: strong duality for Wasserstein DRO, by Gao and Kleywegt (arXiv:1604.02199), Blanchet and Murthy (arXiv:1604.01446), and Zhang, Yang and Gao (arXiv:2205.00362).
2021–2025: Wang, Gao and Xie prove strong duality for Sinkhorn DRO for a general measurable sample space, a measurable loss and an arbitrary nominal distribution.

Setting

Let $\mathcal Z$ be a measurable space. The data are:

a nominal probability distribution $\widehat{\mathbb P}$ ;
a σ-finite reference measure $\nu\neq0$ ;
a transport cost $c:\mathcal Z\times\mathcal Z\to[0,\infty]$ ;
a regularization parameter $\epsilon>0$ and a radius $\rho\in\mathbb R$ ;
a loss $f:\mathcal Z\to\mathbb R\cup\{\infty\}$ .

For a probability distribution $\mathbb P$ , the Sinkhorn distance (Definition 1, with reference measures $\widehat{\mathbb P}$ and $\nu$ ) is

\mathcal W_\epsilon(\widehat{\mathbb P},\mathbb P)=\inf_{\gamma\in\Gamma(\widehat{\mathbb P},\mathbb P)}\mathbb E_{(x,y)\sim\gamma}\Big[c(x,y)+\epsilon\log\frac{d\gamma(x,y)}{d\widehat{\mathbb P}(x)\,d\nu(y)}\Big],

where $\Gamma(\widehat{\mathbb P},\mathbb P)$ is the set of couplings with these marginals. The primal value is the worst-case expected loss over the Sinkhorn ball,

V=\sup\big\{\mathbb E_{\mathbb P}[f]:\ \mathcal W_\epsilon(\widehat{\mathbb P},\mathbb P)\le\rho\big\}.

The dual problem uses three more objects. The kernel distribution is $d\mathbb Q_{x,\epsilon}(z)\propto e^{-c(x,z)/\epsilon}\,d\nu(z)$ . The adjusted radius is $\bar\rho=\rho+\epsilon\,\mathbb E_{x\sim\widehat{\mathbb P}}[\log\mathbb E_{z\sim\nu}e^{-c(x,z)/\epsilon}]$ . The dual value is

V_D=\inf_{\lambda\ge0}\Big\{\lambda\bar\rho+\lambda\epsilon\,\mathbb E_{x\sim\widehat{\mathbb P}}\Big[\log\mathbb E_{z\sim\mathbb Q_{x,\epsilon}}\big[e^{f(z)/(\lambda\epsilon)}\big]\Big]\Big\},

where the objective at $\lambda=0$ is $\operatorname{ess\,sup}_\nu f$ .

Assumption 1 requires:

$c$ is measurable and, for $\widehat{\mathbb P}$ -a.e. $x$ , finite $\nu$ -a.e.;
$\mathbb E_\nu e^{-c(x,\cdot)/\epsilon}<\infty$ for $\widehat{\mathbb P}$ -a.e. $x$ ;
$f$ is measurable;
every coupling with first marginal $\widehat{\mathbb P}$ disintegrates along $\widehat{\mathbb P}$ .

Condition 1 asks for some $\lambda>0$ with $\mathbb E_{\mathbb Q_{x,\epsilon}}[e^{f/(\lambda\epsilon)}]<\infty$ for $\widehat{\mathbb P}$ -a.e. $x$ .

Formalization targets

Goal: Theorem 1 (strong duality)

Under Assumption 1:

\text{(I) }\ \exists\,\mathbb P:\ \mathcal W_\epsilon(\widehat{\mathbb P},\mathbb P)\le\rho\iff\bar\rho\ge0;\qquad \text{(II) }\ \bar\rho\ge0\implies V=V_D.

(III) If $\bar\rho>0$ , then $V=V_D<\infty$ when the dual objective is finite at some $\lambda>0$ , and $V=V_D=\infty$ otherwise.

(IV) If $\bar\rho>0$ and Condition 1 holds, then $0$ is the unique dual minimizer if and only if

\operatorname{ess\,sup}_\nu f<\infty\quad\text{and}\quad\bar\rho\ge\epsilon\,\mathbb E_{x\sim\widehat{\mathbb P}}\big[\log\big(1/\mathbb Q_{x,\epsilon}(A)\big)\big],\qquad A=\{f=\operatorname{ess\,sup}_\nu f\}.

Milestones

The milestones are the numbered lemmas of the paper's proof, in the order the proof uses them:

Lemma EC.2: the Gibbs variational principle, $\sup_{\mathbb P\ll\nu}\mathbb E_{\mathbb P}[f-\tau\log\frac{d\mathbb P}{d\nu}]=\tau\log\mathbb E_\nu e^{f/\tau}$ .
Lemma EC.3: measurability of the inner value $x\mapsto v_x(\lambda)$ .
Lemma 1: weak duality $V\le V_D$ .
Lemma 2: a KL-constrained reformulation of the primal problem.
Lemma EC.4: existence of a dual minimizer.
Lemma 3: the first-order condition (9) and uniqueness when $\lambda^*>0$ .
Lemma EC.5: the criterion for $\lambda^*=0$ .

Significance

The result. Theorem 1 turns a supremum over an infinite-dimensional set of distributions into a scalar convex program. That program can be solved by first-order methods using only samples from $\widehat{\mathbb P}$ and from the kernels $\mathbb Q_{x,\epsilon}$ , which is the basis of the paper's algorithm (Section 4). The proof also constructs the worst-case distribution: it is absolutely continuous with respect to $\nu$ , not discrete. Theorem 1(IV) says exactly when the ambiguity constraint is binding. The finite-support conic reformulation (Corollary 1) and the closed form for linear losses (Example 1) both follow from the theorem.

Formalizing it. The theorem is proved in the paper; no machine-checked proof exists. Formalization adds two things. First, it pins down the extended-valued conventions: $V$ , $V_D$ and $f$ all take values in $[-\infty,\infty]$ , and the paper does not specify how undefined expectations and the $\lambda=0$ objective are treated. Second, it checks every case of the proof, including the degenerate ones. Doing so has already corrected two statements; see Formalization scope.

Difficulty

Weak duality (Lemma 1) is Lagrangian relaxation plus the Gibbs principle. The difficulty is the reverse inequality $V\ge V_D$ . Interchanging the supremum over distributions with the infimum over $\lambda$ requires a minimax theorem. The usual minimax theorems need compactness or semicontinuity in the distribution variable. The paper's setting has neither: $\mathcal Z$ is an arbitrary measurable space, $f$ is only measurable and may be $+\infty$ , and $\widehat{\mathbb P}$ is arbitrary. So a minimax theorem cannot be applied directly.

The proof instead constructs near-optimal primal distributions from the dual minimizer. This needs three separate cases:

$\lambda^*>0$ , with a first-order condition;
$\lambda^*=0$ , with a distribution concentrated on the essential maximizers of $f$ ;
Condition 1 fails, with a truncation argument.

Each case needs integrability facts about $\mathbb E_{\mathbb Q_{x,\epsilon}}[e^{f/(\lambda\epsilon)}]$ in which $x$ and $\lambda$ interact. Disintegrating couplings (Assumption 1(IV)) and making the extended-valued expectations meaningful are a further source of work in Lean.

Formalization scope

All values (primal value, Sinkhorn distance, dual objective) are EReal. Expectations are the published DupacovaWets.Consistency.expect: $\int g^+-\int g^-$ , with lower Lebesgue integrals in $[0,\infty]$ and the convention $\infty-\infty=+\infty$ . The Bochner integral appears only in $\bar\rho$ , which every theorem assumes finite.

Further conventions:

Sinkhorn distance. The cost and the entropy form a single integrand. A coupling not absolutely continuous with respect to $\widehat{\mathbb P}\otimes\nu$ contributes $+\infty$ . An infeasible primal has $V=-\infty$ .
Dual objective. The value at $\lambda=0$ is defined as Mathlib's essSup f ν, not as a limit. Logarithms are ENNReal.log, so $\log\infty=\infty$ and $\log 0=-\infty$ ; $e^{+\infty}=+\infty$ .
Kernels. $\mathbb Q_{x,\epsilon}$ is a normalized withDensity measure. Families $\{\gamma_x\}_{x\in\operatorname{supp}\widehat{\mathbb P}}$ are Markov kernels on all of $\mathcal Z$ .

Hypotheses added to the page:

$\nu$ is σ-finite and nonzero;
$\epsilon>0$ ;
$x\mapsto\log\mathbb E_\nu e^{-c(x,\cdot)/\epsilon}$ is $\widehat{\mathbb P}$ -integrable, so that $\bar\rho\in\mathbb R$ .

" $\nu\{0\le c<\infty\}=1$ " is read as " $\nu$ -a.e.". " $\lambda^*=0$ " is read as " $0$ is the unique dual minimizer".

Corrections to the paper:

Theorem 1(III). The paper's version with Condition 1 is false: a.e.-finite inner expectations do not make the dual objective finite. A counterexample on $\mathbb N$ is in the goal's note. The goal is stated with the integrated condition "the dual objective is finite at some $\lambda>0$ ".
Lemma 3. The lemma is stated under the added hypothesis that the dual objective is finite at some $\lambda_1<\lambda^*$ (and is not $-\infty$ at $\lambda^*$ ). Without it, $\lambda^*$ can sit at the edge of the domain where the objective is finite, and (9) fails.

No statement involves an $O(\cdot)$ constant.

A formalization that lets an undefined Sinkhorn integrand evaluate to $-\infty$ (Mathlib's $\top+\bot=\bot$ ) is ruled out: it would put every distribution into the ball and make the theorem trivial. The combined integrand and the $+\infty$ convention exclude this.

A complete development needs:

a Gibbs/Donsker–Varadhan variational principle for σ-finite reference measures and extended-valued functions;
disintegration of couplings;
convexity and differentiation of $\lambda\mapsto\lambda\log\mathbb E e^{f/\lambda}$ .

The first two are reusable well beyond this mission. Contributions toward any milestone, and toward these general lemmas, are welcome.

Selected references

J. Wang, R. Gao, Y. Xie, Sinkhorn Distributionally Robust Optimization, arXiv:2109.11926v5, 2025. https://arxiv.org/abs/2109.11926
M. Cuturi, Sinkhorn Distances: Lightspeed Computation of Optimal Transport, NeurIPS, 2013. https://arxiv.org/abs/1306.0895
R. Gao, A. Kleywegt, Distributionally Robust Stochastic Optimization with Wasserstein Distance, Mathematics of Operations Research, 2023. https://arxiv.org/abs/1604.02199
J. Blanchet, K. Murthy, Quantifying Distributional Model Risk via Optimal Transport, Mathematics of Operations Research, 2019. https://arxiv.org/abs/1604.01446
L. Zhang, J. Yang, R. Gao, A Short and General Duality Proof for Wasserstein Distributionally Robust Optimization, Operations Research, 2024. https://arxiv.org/abs/2205.00362

12 thms2 active usersReviewed

Convex Optimization Operations Research Probability·Captain: mikedeng1

Arbitrage and Duality in Nondominated Discrete-Time Models I: Under NA(𝒫) the Superhedging Price Equals the Supremum of Expectations over Martingale Measures and Is AttainedResearch Paper

Motivation

Classical arbitrage pricing fixes one probability measure $P$ describing the market and asks for the cheapest way to dominate a payoff $P$ -almost surely. When the model itself is uncertain, this choice is not available: a trader who only trusts a family $\mathcal P$ of possible models wants a hedge that works under every one of them. Two literatures meet here. Robust (model-independent) finance studies hedging that must hold for all paths, as in the martingale-optimal-transport approach to option bounds (Beiglböck, Henry-Labordère, Penkner, 2013). Nondominated model uncertainty studies families $\mathcal P$ with no single reference measure, as in the quasi-sure analysis of Denis–Martini (2006) and the volatility-uncertainty literature. Bouchard and Nutz (2015) give a discrete-time framework that contains both extremes (all measures on a path space; a single measure) and prove the fundamental theorems and superhedging duality for it.

Timeline of the dominated and robust predecessors:

1990. Dalang, Morton and Willinger prove the discrete-time fundamental theorem of asset pricing (FTAP) for one measure.
2001. Kabanov and Stricker give a short proof of the closedness of the superhedgeable cone behind the DMW theorem. The proof of Theorem 2.2 follows their argument.
2013. Acciaio, Beiglböck, Penkner, Schachermayer prove a model-independent FTAP for a pathwise no-arbitrage notion, with options.
2015. Bouchard and Nutz prove the FTAP, the superhedging theorem and the second FTAP under a nondominated family $\mathcal P$ , with dynamic trading in stocks and static trading in finitely many options.

Setting

Fix a horizon $T\in\mathbb N$ and a Polish space $\Omega_1$ . Paths are $\omega=(\omega_1,\dots,\omega_T)\in\Omega=\Omega_1^T$ , and $\Omega_t=\Omega_1^t$ holds the first $t$ coordinates. Information at time $t$ is the universal completion $\mathcal F_t$ of the Borel $\sigma$ -field of $\Omega_t$ .

For each $t<T$ and history $\omega\in\Omega_t$ , a nonempty convex set $\mathcal P_t(\omega)$ of probability measures on $\Omega_1$ describes the possible laws of the next coordinate. Its graph must be an analytic set. The set of models $\mathcal P$ consists of all products $P=P_0\otimes P_1\otimes\cdots\otimes P_{T-1}$ whose kernels choose $P_t(\omega)\in\mathcal P_t(\omega)$ . A property holds $\mathcal P$ -quasi surely (q.s.) if it holds $P$ -a.s. for every $P\in\mathcal P$ .

There are $d$ stocks with Borel prices $S_t:\Omega_t\to\mathbb R^d$ and $e$ options $g=(g^1,\dots,g^e)$ , Borel on $\Omega$ , bought or sold at time $0$ at price $0$ . A semistatic strategy $(H,h)$ consists of a predictable $H$ and a vector $h\in\mathbb R^e$ ; its terminal gain is

H\bullet S_T+hg=\sum_{u=1}^T H_u\,(S_u-S_{u-1})+\sum_{i=1}^e h^ig^i .

No-arbitrage NA( $\mathcal P$ ) says that a gain which is q.s. nonnegative is q.s. zero. The superhedging price of a claim $f$ is

\pi(f)=\inf\{x\in\mathbb R:\ \exists (H,h),\ x+H\bullet S_T+hg\ge f\ \ \mathcal P\text{-q.s.}\}.

The dual objects are the martingale measures $Q\lll\mathcal P$ , meaning $Q\ll P$ for some $P\in\mathcal P$ . Under $Q$ the stock $S$ is a martingale and $E_Q[g^i]=0$ for all $i$ ; they form the set $\mathcal Q$ . Given a weight $\varphi\ge1$ , set $\mathcal Q_\varphi=\{Q\in\mathcal Q: E_Q[\varphi]<\infty\}$ . Expectations of arbitrary measurable functions use the convention $E[f]=E[f^+]-E[f^-]$ with $\infty-\infty=-\infty$ .

Formalization targets

Goal: Theorem 5.1(b)

Let $\varphi\ge1$ be a random variable with $|g^i|\le\varphi$ , let NA( $\mathcal P$ ) hold, and let $f$ be upper semianalytic with $|f|\le\varphi$ . Then

\pi(f)=\sup_{Q\in\mathcal Q_\varphi}E_Q[f]\in(-\infty,\infty],

and some $(H,h)$ satisfies $\pi(f)+H\bullet S_T+hg\ge f$ $\mathcal P$ -q.s.

Milestones

The milestones follow the paper's proof:

General setting (§2). Closedness of the superhedgeable cone under q.s. convergence (Theorem 2.2), and existence of optimal strategies (Theorem 2.3).
One-period market (§3). The fundamental lemma (Lemma 3.3), the one-period FTAP (Theorem 3.1), approximation lemmas (Lemmas 3.5, 3.6) and one-period duality (Theorem 3.4).
Expectation bound (Lemma A.2). The elementary bound $E_Q[f]\le x$ for a superhedge under a consistent local martingale measure.
Multi-period market without options (§4). Local characterization of NA (Lemma 4.6, Theorem 4.5), measurable one-step duality (Lemma 4.10), dynamic superhedging (Lemma 4.13) and duality (Theorem 4.9).
With options (§5). The first and second fundamental theorems (Theorem 5.1(a), (c)).

Significance

The superhedging theorem identifies the robust price of a claim as a supremum of linear prices. This turns a hedging problem into an optimization over measures, which is how robust option bounds are computed in practice. Remark 1.4 of the paper gives another consequence: every martingale inequality $E[f(M_1,\dots,M_T)]\le a$ follows from a pathwise inequality $f\le a+H\bullet S_T$ . The first and second fundamental theorems make the nondominated framework a complete analogue of the classical theory. NA( $\mathcal P$ ) is equivalent to $\mathcal P$ and $\mathcal Q$ sharing their polar sets, and replicable claims are those whose price is the same under every martingale measure.

All results are proved in the paper. None of them, nor the classical dominated discrete-time FTAP, is formalized in Lean or Mathlib as far as is known. A formalization produces machine-checked statements of the model (analytic random sets, products of universally measurable kernels, quasi-sure analysis) and proofs of the fundamental theorems on top of it. Alternative arguments and extensions (portfolio constraints, infinitely many options) are also welcome.

Difficulty

There is no reference measure. Two dominated tools therefore fail. Closedness in $L^0(P)$ cannot be applied, because convergence must hold quasi surely. A Hahn–Banach separation in a single $L^p(P)$ space cannot produce martingale measures either. The paper argues one period at a time instead and glues the periods together measurably. That gluing is where the work lies. The one-period dual value $\mathcal E_t(f)(\omega)$ and the one-period hedge $y(\omega)$ must depend measurably on the history $\omega$ , but the value function of a Borel claim need not be Borel. The argument therefore runs in the class of upper semianalytic functions and needs measurable selection theorems for analytic sets. A recursion that tries to keep everything Borel breaks down at the first step.

Formalization scope

Spaces. $\Omega_t$ is Fin t → Ω₁ with [PolishSpace Ω₁] [BorelSpace Ω₁]. Measures are Borel measures, and $\mathcal F_t$ -measurability is universal measurability. The published definition BertsekasShreve.AnalyticSelection.Measurability is reused for this.
Models. $\mathfrak P(\Omega_1)$ is Mathlib's ProbabilityMeasure with the weak topology. $\mathcal P$ is generated by Borel Markov kernels lying in $\mathcal P_t(\cdot)$ almost surely; this is the paper's equivalent formulation on p. 4.
Strategies. Lean's H u is the paper's $H_{u+1}$ , a universally measurable function of the first $u$ coordinates.
Values in EReal. Expectations of non-integrable functions are the extended expectation $E[f^+]-E[f^-]$ . Prices are EReal infima with $\inf\emptyset=+\infty$ , and suprema over $\mathcal Q_\varphi$ are EReal suprema.
Settings. The §2 and §3 milestones are stated in the paper's more general settings: a general filtered space, and a one-period market on an arbitrary measurable space.
Citations. Page numbers are those of the arXiv v3 reprint (arXiv:1305.6008v3), not the journal's pp. 823–859.

Two encodings would trivialize the mission and are excluded. Replacing $\mathcal P$ by an arbitrary set of measures drops the product structure that the theorems need. Bochner integrals for $E_Q[f]$ would return $0$ on non-integrable claims and make the duality meaningless. Neither encoding is used.

A complete development needs:

analytic and universally measurable sets and the Jankov–von Neumann selection theorem;
products of universally measurable kernels;
quasi-sure analysis;
relative interiors and separation in $\mathbb R^d$ ;
discrete-time local and generalized martingales.

The selection and kernel infrastructure is reusable well beyond this paper, for instance in dynamic programming on Borel spaces. Contributions of these foundations are welcome.

Selected references

B. Bouchard, M. Nutz, Arbitrage and duality in nondominated discrete-time models, Ann. Appl. Probab. 25(2) (2015) 823–859. https://arxiv.org/abs/1305.6008 , https://doi.org/10.1214/14-AAP1011
R. C. Dalang, A. Morton, W. Willinger, Equivalent martingale measures and no-arbitrage in stochastic securities market models, Stochastics Stochastics Rep. 29 (1990) 185–201. https://mathscinet.ams.org/mathscinet-getitem?mr=1041035
B. Acciaio, M. Beiglböck, F. Penkner, W. Schachermayer, A model-free version of the fundamental theorem of asset pricing and the super-replication theorem, Math. Finance 26(2) (2016) 233–251. https://arxiv.org/abs/1301.5568
M. Beiglböck, P. Henry-Labordère, F. Penkner, Model-independent bounds for option prices — a mass transport approach, Finance Stoch. 17(3) (2013) 477–501. https://arxiv.org/abs/1106.5929
L. Denis, C. Martini, A theoretical framework for the pricing of contingent claims in the presence of model uncertainty, Ann. Appl. Probab. 16 (2006) 827–852. https://mathscinet.ams.org/mathscinet-getitem?mr=2244434
Y. Kabanov, C. Stricker, A teachers' note on no-arbitrage criteria, Séminaire de Probabilités XXXV, Lecture Notes in Math. 1755 (2001) 149–152. https://mathscinet.ams.org/mathscinet-getitem?mr=1837282
D. P. Bertsekas, S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978 (Chapter 7, analytic sets and measurable selection).

21 thms2 active usersReviewed

Completed

Algebraic Topology Geometry & Topology Symplectic Geometry·Captain: Mazecto

Conley–Zehnder Index I: Axiomatic Characterization on Paths of Symplectic MatricesResearch Paper

Motivation

The Conley–Zehnder index assigns an integer to a path of symplectic matrices that starts at the identity and ends at a matrix without eigenvalue $1$ . It is how periodic orbits of Hamiltonian and Reeb flows get graded. In Floer homology it gives the grading of the chain complex, generated by the $1$ -periodic orbits of a nondegenerate Hamiltonian (Salamon–Zehnder 1992; Salamon 1999). In contact homology and symplectic field theory it grades Reeb orbits. In the analysis of pseudoholomorphic curves it enters the Fredholm index formula for the linearized Cauchy–Riemann operator through the asymptotic orbits. In three-dimensional Reeb dynamics it defines dynamical convexity (every periodic orbit has index at least $3$ ), the hypothesis of the Hofer–Wysocki–Zehnder theorem on disk-like global surfaces of section (HWZ 1998).

Timeline. Conley and Zehnder introduced the index in their Morse-type index theory for periodic solutions of Hamiltonian equations (Conley–Zehnder 1984). Salamon and Zehnder gave the definition through a rotation function $\rho : \mathrm{Sp}(2n) \to S^1$ and related it to the Maslov index (SZ92). Robbin and Salamon extended it to arbitrary paths as a half-integer Maslov-type index (Robbin–Salamon 1993). Gutt attributes the properties naturality, homotopy, zero, product, loop, signature, determinant and inverse, and the characterization of the index by homotopy, loop and signature alone, to Salamon's lecture notes (Sal99) and to Audin–Damian (AD14); the statements used here are those of Gutt, Propositions 8–9. Gutt gives a self-contained account with several equivalent formulas, including the normalized complex determinant of the complex-linear part used below (Gutt 2014, §2).

Setting

Write $\mathbb{R}^{2n}$ with coordinates $(q,p)$ and let

J_0 = \begin{pmatrix} 0 & -\mathrm{Id} \\ \mathrm{Id} & 0 \end{pmatrix}.

The symplectic group $\mathrm{Sp}(2n)$ is the set of real $2n\times 2n$ matrices $A$ with $A J_0 A^{\mathsf T} = J_0$ . Let $\mathrm{Sp}^*(2n)$ be the set of $A \in \mathrm{Sp}(2n)$ with $\det(\mathrm{Id} - A) \neq 0$ .

$\mathrm{SP}(n)$ is the set of continuous paths $\psi : [0,1] \to \mathrm{Sp}(2n)$ with $\psi(0) = \mathrm{Id}$ and $\psi(1) \in \mathrm{Sp}^*(2n)$ . It carries the compact-open topology.

For $A \in \mathrm{Sp}(2n)$ , the complex-linear part is $C_A = \tfrac12 (A - J_0 A J_0)$ . It commutes with $J_0$ , so it has the block form $\begin{pmatrix} X & -Y \\ Y & X\end{pmatrix}$ , which is the complex matrix $X + iY$ once $\mathbb{R}^{2n}$ is identified with $\mathbb{C}^n$ by $(x,y) \mapsto x + iy$ . Set

\hat\rho(A) = \frac{\det_{\mathbb C}(X+iY)}{|\det_{\mathbb C}(X+iY)|} \in S^1.

Let $W^+ = -\mathrm{Id}$ and $W^- = \mathrm{diag}(2,-1,\dots,-1,\tfrac12,-1,\dots,-1)$ . Each $\psi \in \mathrm{SP}(n)$ extends to a path $\tilde\psi : [0,2] \to \mathrm{Sp}(2n)$ with $\tilde\psi = \psi$ on $[0,1]$ , $\tilde\psi(t) \in \mathrm{Sp}^*(2n)$ for $t \geq 1$ , and $\tilde\psi(2) \in \{W^+, W^-\}$ . The map $\hat\rho^2 \circ \tilde\psi$ is then a loop in $S^1$ , and

\mu_{CZ}(\psi) = \deg\big(\hat\rho^2 \circ \tilde\psi\big).

For a loop $\varphi : [0,1] \to \mathrm{Sp}(2n)$ with $\varphi(0) = \varphi(1) = \mathrm{Id}$ , the Maslov index is $\mu(\varphi) = \deg(\hat\rho\circ\varphi)$ . For a symmetric matrix $S$ , $\mathrm{Sign}(S)$ is the number of positive eigenvalues minus the number of negative eigenvalues.

Formalization targets

Goal: existence and uniqueness

The map $\mu_{CZ} : \mathrm{SP}(n) \to \mathbb{Z}$ has the following three properties, and every map $\mu : \mathrm{SP}(n) \to \mathbb{Z}$ with these properties equals $\mu_{CZ}$ :

Homotopy. $\mu$ is constant on the connected components of $\mathrm{SP}(n)$ .
Loop. $\mu(\varphi\psi) = \mu(\psi) + 2\mu(\varphi)$ for every loop $\varphi$ at $\mathrm{Id}$ and every $\psi \in \mathrm{SP}(n)$ .
Signature. If $S = S^{\mathsf T}$ is nondegenerate and all of its eigenvalues have absolute value $< 2\pi$ , then $\mu\big(t \mapsto \exp(tJ_0S)\big) = \tfrac12 \mathrm{Sign}(S)$ .

Milestones

$\det_{\mathbb C} C_A \neq 0$ for every $A \in \mathrm{Sp}(2n)$ .
$\deg(\hat\rho^2\circ\tilde\psi)$ exists and does not depend on the extension $\tilde\psi$ .
$\deg(\hat\rho\circ\varphi)$ is well defined for loops.
Naturality. $\mu_{CZ}(\varphi\psi\varphi^{-1}) = \mu_{CZ}(\psi)$ for every path $\varphi$ in $\mathrm{Sp}(2n)$ .
Homotopy, for $\mu_{CZ}$ .
Zero. If $\psi(s)$ has no eigenvalue on the unit circle for $s > 0$ , then $\mu_{CZ}(\psi) = 0$ .
Product. $\mu_{CZ}(\psi'\diamond\psi'') = \mu_{CZ}(\psi') + \mu_{CZ}(\psi'')$ under the symplectic block embedding $\mathrm{Sp}(2n')\times\mathrm{Sp}(2n'') \hookrightarrow \mathrm{Sp}(2(n'+n''))$ .
Loop, for $\mu_{CZ}$ .
Signature, for $\mu_{CZ}$ .
Determinant. $(-1)^{n-\mu_{CZ}(\psi)} = \operatorname{sign}\det(\mathrm{Id} - \psi(1))$ .
Inverse. $\mu_{CZ}(\psi^{-1}) = \mu_{CZ}(\psi^{\mathsf T}) = -\mu_{CZ}(\psi)$ .
Uniqueness. Homotopy, loop and signature determine $\mu_{CZ}$ on $\mathrm{SP}(n)$ .

Significance

The result. The characterization makes the index a canonical invariant: any construction of an integer invariant of nondegenerate symplectic paths that is homotopy invariant and has the correct loop and signature behaviour is the Conley–Zehnder index. In practice this is how different definitions in the literature are identified with one another (rotation function, polar decomposition, complex-linear part, crossing forms, spectral flow of asymptotic operators). The listed properties are used directly to compute indices of concrete orbits, for instance the iterates of orbits of ellipsoids and the orbits of convex energy surfaces.

Formalizing it. All results here are classical and proved. No formalization of the Conley–Zehnder index exists in Mathlib. This mission produces a reusable library for symplectic linear algebra in Lean: the index and the Maslov index of loops as functions on path spaces, together with their computational properties. It is the first stage of a formalization of the Fredholm theory of linearized Cauchy–Riemann operators, whose index formula is stated in terms of Conley–Zehnder indices. It also gives a general-dimension definition against which the two-dimensional winding-interval definitions used in existing dynamical-convexity statements can be compared.

Difficulty

The index is defined through a choice: an extension of the path to $W^\pm$ inside $\mathrm{Sp}^*(2n)$ and a continuous argument of a circle-valued map. Before any property can be stated as a property of a function, the result must be shown independent of these choices. That is not a local computation: it depends on the global topology of the symplectic group and on how the set of matrices with eigenvalue $1$ sits inside it.

The properties themselves are statements about the degree of maps into $S^1$ built from determinants, and $\hat\rho$ is not a homomorphism. So none of the properties follows from a calculation on a single matrix, and loop and product require control of degrees under pointwise products and block sums. The uniqueness statement quantifies over all integer-valued functions on a path space. The argument for it has to use only the three listed properties and the topology of $\mathrm{SP}(n)$ .

Formalization scope

Namespace ConleyZehnder; all definitions are in ConleyZehnder_Setting.
Matrices are Matrix (Fin n ⊕ Fin n) (Fin n ⊕ Fin n) ℝ. $J_0$ is Mathlib's Matrix.J, and $\mathrm{Sp}(2n)$ is Matrix.symplecticGroup. Paths are C(unitInterval, Mat n) with the compact-open topology. $\mathrm{SP}(n)$ is a Set of such paths, and "connected component" means connectedComponentIn (SP n).
Index maps are functions $\mu$ on all of C(unitInterval, Mat n). Every property constrains $\mu$ only on $\mathrm{SP}(n)$ , and the paths $\varphi\psi\varphi^{-1}$ , $\psi^{-1}$ , $\psi^{\mathsf T}$ , $\psi'\diamond\psi''$ and $\exp(tJ_0S)$ are passed as continuous maps with the stated pointwise values.
Degree is expressed by continuous real lifts: IsArgLift f θ means $f(t) = e^{i\theta(t)}$ . IsCZValue ψ k says that some extension and some lifts give $2\big(\Delta\theta_\psi + \Delta\theta_\chi\big) = 2\pi k$ , where $\chi$ is the part of the extension after $t = 1$ . czIndex and maslovIndex are defined by choice from these predicates, with fallback value $0$ . Milestones 2 and 3 are what make the fallback unreachable. Without them, any property proved for czIndex would say nothing about the actual index.
The circle-valued map is $\hat\rho$ of Gutt, Corollary 12, formula (9). The rotation function $\rho$ of Salamon–Zehnder (built from eigenvalue multiplicities and Krein signs) is not formalized. Gutt, Proposition 10 and Corollaries 11–12, shows that the degrees agree. The Maslov index of loops is also taken with $\hat\rho$ .
The signature uses Matrix.IsHermitian.eigenvalues; for real matrices, Hermitian means symmetric. The norm bound is stated as $|\lambda| < 2\pi$ for every eigenvalue $\lambda$ . The signature property is stated as $2\mu = \mathrm{Sign}(S)$ .
$n = 0$ is allowed: $\mathrm{SP}(0)$ is a single path and every property holds for it.

Contributions welcome: general lemmas on degrees of maps $[0,1]\to S^1$ (existence and uniqueness of lifts, additivity under products and concatenation, homotopy invariance), and the topology of $\mathrm{Sp}(2n)$ and $\mathrm{Sp}^*(2n)$ . These are reusable well beyond this mission.

Selected references

C. Conley, E. Zehnder, Morse-type index theory for flows and periodic solutions for Hamiltonian equations, Comm. Pure Appl. Math. 37 (1984), 207–253. https://doi.org/10.1002/cpa.3160370204
D. Salamon, E. Zehnder, Morse theory for periodic solutions of Hamiltonian systems and the Maslov index, Comm. Pure Appl. Math. 45 (1992), 1303–1360. https://doi.org/10.1002/cpa.3160451004
J. Robbin, D. Salamon, The Maslov index for paths, Topology 32 (1993), 827–844. https://doi.org/10.1016/0040-9383(93)90052-W
H. Hofer, K. Wysocki, E. Zehnder, The dynamics on three-dimensional strictly convex energy surfaces, Ann. of Math. 148 (1998), 197–289. https://doi.org/10.2307/120994
D. Salamon, Lectures on Floer homology, in: Symplectic Geometry and Topology, IAS/Park City Math. Ser. 7, AMS (1999), 143–229. https://doi.org/10.1090/pcms/007/05
M. Audin, M. Damian, Morse Theory and Floer Homology, Universitext, Springer (2014); French original 2010. https://doi.org/10.1007/978-1-4471-5496-9
J. Gutt, Generalized Conley–Zehnder index, Ann. Fac. Sci. Toulouse Math. (6) 23 (2014), 907–932. https://doi.org/10.5802/afst.1430 (arXiv:1307.7239)

32 thms2 active usersReviewed

Completed

Actuarial Science Probability·Captain: WillR

Actuarial Mathematics XXX: Discrete Tail Value-at-Risk with Quantile AtomsTextbook

Actuarial Mathematics XXX: Discrete Tail Value-at-Risk with Quantile Atoms

Primary source in the user's PDF Library

S. David Promislow, Fundamentals of Actuarial Mathematics (third edition, 2015), Chapter 22, Section 22.5.3, Definition 22.5 and equation (22.9), PDF pages 439–442, defines tail value-at-risk using the value-at-risk quantile plus the stop-loss expected excess divided by one minus confidence. The textbook demonstrates the error in conditioning only on losses strictly greater than, or greater than or equal to, a discrete VaR when the quantile contains an atom. Its two-coin example has losses 0, 1, 1, 2 with equal joint probabilities: $\mathrm{VaR}_{0.5}=1$ and $\mathrm{TVaR}_{0.5}=1.5$ . The present mission provides an exact finite integer-lattice formalisation of that convention.

Discrete loss distribution and quantile conditions

Let aggregate loss $S$ be integer valued on $\{0,1,\dots,B\}$ with nonnegative masses $w_s$ , usually summing to one. Choose confidence $0\le\alpha<1$ and an integer quantile $q$ . The strict tail above the quantile is

T_B(q)=\sum_{s=q+1}^{B}w_s.

The worst $1-\alpha$ fraction of outcomes includes every loss strictly larger than q, then only enough outcomes at q to complete the required probability. Write that selected quantile-point mass as

a_q=(1-\alpha)-T_B(q).

For this selection to be feasible, q must be an appropriate upper quantile, captured by

T_B(q)\le1-\alpha\le T_B(q)+w_q, \qquad\text{equivalently}\qquad 0\le a_q\le w_q.

The inequalities are explicit formal hypotheses. An arbitrary q need not be a valid VaR for the given confidence, even though the algebraic TVaR expression remains defined by the source.

Fractional atom selection and stop-loss representation

The expected monetary loss across the worst $1-\alpha$ probability mass is

A_B(q,\alpha)=\sum_{s=q+1}^{B}s\,w_s+q\,a_q.

Consequently, the correct tie-adjusted tail average is

\operatorname{TVaR}_{\alpha} =\frac{A_B(q,\alpha)}{1-\alpha}.

The related net stop-loss transform is

\Pi_B(q)=\sum_{s=0}^{B}(s-q)_+w_s.

A finite reorganisation yields the fundamental actuarial formula

\boxed{\operatorname{TVaR}_{\alpha} =q+\frac{\Pi_B(q)}{1-\alpha}.}

The term at the VaR atom contributes q times just the required fraction, not q times every atom observation. For the two-coin loss distribution $w=(1/4,1/2,1/4)$ , q=1 and $\alpha=1/2$ , the strict tail is 1/4 and the selected mass at the quantile is 1/4. The numerator is $2(1/4)+1(1/4)=3/4$ , so TVaR equals 3/2. The alternatives $E[S\mid S>1]=2$ and $E[S\mid S\ge1]=4/3$ are not the correct tie-adjusted TVaR at this confidence.

Under nonnegative probability coefficients and positive tail probability, the stop-loss premium is nonnegative and therefore $\operatorname{TVaR}_{\alpha}\ge q$ . When $q=B$ , the stop-loss transform is zero and TVaR equals B, provided the quantile is selected consistently.

Theorem graph and validation

Five definitions represent strict tail probability, net stop-loss excess expectation, selected quantile atom, selected tail monetary numerator and its normalised TVaR. Twelve supporting theorem targets establish strict-tail and excess nonnegativity, terminal bounds, atom feasibility, exact tail coverage, tail numerator algebra, the stop-loss TVaR identity, the quantile lower bound and an explicit discrete two-coin counterexample to naive conditional-tail averaging. The thirteenth target combines feasible atom allocation, TVaR/stop-loss equality and $\operatorname{TVaR}\ge q$ .

An independent exact-rational suite checked 84 finite claim-grid/confidence combinations, including confidence zero and near one, integer quantile boundaries, strict loss tail and selected quantile-atom fractions.

This is a finite-support discrete loss theorem and does not silently assert continuous-tail integration, arbitrary infinite-support convergence or a general proof of coherent-risk-measure subadditivity. Its connection to the bounded stop-loss mission XXVIII is mathematical only; imports of that unpublished Draft are not permitted.

18 thms2 active usersReviewed

Completed

Actuarial Science Probability·Captain: WillR

Actuarial Mathematics XXXI: Buehlmann and Buehlmann-Straub Credibility OptimisationTextbook

Actuarial Mathematics XXXI: Bühlmann and Bühlmann–Straub Credibility Optimisation

Research from the user's actuarial PDF Library

S. David Promislow, Fundamentals of Actuarial Mathematics (third edition, 2015), Chapter 24, Sections 24.5.2 and 24.5.3, PDF pages 489–491, derives Bühlmann least-squares credibility and extends it to unequal period exposure using the Bühlmann–Straub model. Relevant equations are (24.13)–(24.16), and the weighted generalisation on printed page 464. A complementary openly accessible reference is Loss Data Analytics, Chapter 12, Experience Rating Using Credibility Theory, https://openacttexts.github.io/LDAVer2/ChapCredibility.html.

The book's narrative contains an apparent transposition in one terminology sentence about v and w, but its mathematical definitions and formulas consistently identify $v=E[\operatorname{Var}(X\mid\Theta)]$ as the expected process variance and $w=\operatorname{Var}(E[X\mid\Theta])$ as variance of hypothetical means. This mission uses those mathematical definitions, not the reversed labels.

Process noise, persistent heterogeneity and exposure weighting

Let $\Theta$ denote the underlying class of a policyholder. The collective mean risk is $\mu=E[E(X\mid\Theta)]$ . Let

\mathrm{EPV}=E[\operatorname{Var}(X\mid\Theta)],\qquad \mathrm{VHM}=\operatorname{Var}(E[X\mid\Theta]).

EPV describes claim variability within a risk, whereas VHM describes the persistent difference in expected claims between risks. If observations across periods are conditionally independent given $\Theta$ , and period $i$ has exposure volume $p_i$ , a Bühlmann–Straub period mean has conditional process variance proportional to $1/p_i$ .

For n periods of observed per-unit claims $x_i$ , define positive total exposure and the weighted experience mean by

P=\sum_{i=0}^{n-1}p_i>0,\qquad \bar x_P=\frac{\sum_{i=0}^{n-1}p_ix_i}{P}.

The least-squares credibility factor is

\boxed{Z=\frac{P\,\mathrm{VHM}}{P\,\mathrm{VHM}+\mathrm{EPV}}.}

This is equivalent to $P/(P+K)$ if $\mathrm{VHM}>0$ and $K=\mathrm{EPV}/\mathrm{VHM}$ , but the displayed formula also covers $\mathrm{VHM}=0$ with positive EPV. The denominator must be strictly positive; if both variance components vanish then every credibility weight produces the same prediction-error objective, so a unique ratio must not be asserted.

The resulting credibility premium per unit exposure is

\hat\mu=Z\bar x_P+(1-Z)\mu.

Why this weight is least-squares optimal

The usual risk-type prediction objective is a mean-squared error of estimating the hypothetical risk mean. Under the conditional variance and independence assumptions its quadratic part is

\mathrm{MSE}(z)=\mathrm{VHM}(1-z)^2+ \frac{\mathrm{EPV}}{P}z^2.

For positive exposure, multiplication by P does not change its minimiser. To avoid introducing division by zero into the Lean source, define the algebraically equivalent scaled risk

R_P(z)=P\,\mathrm{VHM}(1-z)^2+\mathrm{EPV}z^2.

With nonnegative P, EPV and VHM and strictly positive sum $D=P\,\mathrm{VHM}+\mathrm{EPV}$ , completing the square gives

\boxed{R_P(z)=\frac{P\,\mathrm{VHM}\,\mathrm{EPV}}{D} +D(z-Z)^2.}

Thus $0\le Z\le1$ , $R_P(Z)\le R_P(z)$ for any real z, and the optimiser is unique since D is strictly positive. When VHM=0 and EPV>0, Z=0 and the premium is fully collective. When EPV=0 with P·VHM>0, Z=1 and the premium uses individual experience.

Worked benchmark from the user's book

Promislow's printed Example 24.8 uses group exposure volumes 40, 25 and 35 and aggregate period claim totals 4,000, 2,000 and 2,500. The weighted per-person experience is $8500/100=85$ . With collective mean 100, EPV 125 and VHM 5, the experience credibility is

Z=\frac{100(5)}{100(5)+125}=0.8,\qquad \hat\mu=0.8(85)+0.2(100)=88.

The original example then multiplies 88 by a forecast next-period exposure of 45 to obtain expected aggregate claims 3,960. The Lean mission targets the per-unit credibility estimator, not a blanket rule that every future exposure must equal 45.

Graph, numerical checks and limits

Five source definitions represent finite total exposure, weighted observations, optimal weight, credibility premium and exposure-scaled MSE. Fourteen supporting theorem targets establish exposure summation, weighted constant observations, factor bounds and boundaries, premium identities, square completion, minimum and uniqueness. The fifteenth target combines admissibility and global least-squares optimality.

An independent exact-rational check verified 609 combinations of exposure, EPV, VHM and proposed credibility factors. It checked the completed-square equality, bounded optimal factor, global minimality and uniqueness for nonzero denominators, and reproduced Example 24.8.

A general Bayesian posterior mean is not always linear in observed experience. This mission proves optimality among affine credibility estimators under the stated covariance model, rather than asserting universal posterior-mean exactness. The formal risk quadratic encodes the variance decomposition and does not itself formalise an arbitrary latent stochastic probability space.

20 thms2 active usersReviewed

Completed

Actuarial Science Probability·Captain: WillR

Actuarial Mathematics XXIX: Poisson Thinning and Claim-Type SuperpositionTextbook

Actuarial Mathematics XXIX: Poisson Thinning and Claim-Type Superposition

Source research and exact formalisation

Library primary source: S. David Promislow, Fundamentals of Actuarial Mathematics (third edition, 2015), Chapter 21, sections 21.8.1–21.9, PDF pages 411–413, particularly formula (21.9), Poisson thinning discussion on page 412 and claim-type joint mass factorisation and superposition on page 413. Further open teaching source: SCMA469 Actuarial Statistics, Chapter 5.6, Poisson process superposition and thinning, https://pairote-sat.github.io/SCMA469/poisson-processes.html. These sources distinguish single-stream thinning, independence of split streams and combination of already independent processes. The new Lean targets give explicit finite count-probability identities rather than claiming a general measure-theoretic process theorem.

Model and meaning of the variables

For a Poisson claim frequency $\lambda\ge0$ , define the mass at integer claim count $n\ge0$ by

p_\lambda(n)=e^{-\lambda}\frac{\lambda^n}{n!}.

A frequency class selected with probability $p\in[0,1]$ , independently for every original claim, receives intensity $\lambda p$ ; the other class receives intensity $\lambda(1-p)$ . Their intensities must sum to $\lambda$ . A total of $a+b$ claims has count probability $p_\lambda(a+b)$ . Given that count, exactly $a$ marked claims and $b$ unmarked claims occur with conditional binomial probability $\binom{a+b}{a}p^a(1-p)^b$ . Thus the joint count mass is

J_{\lambda,p}(a,b) =p_\lambda(a+b)\binom{a+b}{a}p^a(1-p)^b.

The splitting identity is the exact factorisation

\boxed{J_{\lambda,p}(a,b) =p_{\lambda p}(a)\,p_{\lambda(1-p)}(b).}

This product shows independence of the two count variables, rather than deriving independence merely from matching their marginal Poisson distributions. Cases $p=0$ , $p=1$ , $\lambda=0$ and count zero are included.

For independent Poisson claim-frequency streams with rates $\lambda_1,\lambda_2$ , superposition gives

\boxed{\sum_{k=0}^{n}p_{\lambda_1}(k)p_{\lambda_2}(n-k) =p_{\lambda_1+\lambda_2}(n).}

The identity uses a finite convolution coefficient for each total claim count. The total-rate parameter is additive. Algebraic theorems can allow signed real parameters, while the actuarial probability interpretation requires nonnegative rates and valid marking probabilities.

Proof programme and boundaries

Five definitions introduce Poisson count mass, count convolution, selected intensity, split count joint mass and superposed intensity. Twelve supporting theorems include the factorial count recursion, zero-count probabilities, rate partition, nonnegativity, convolution at zero, the binomial superposition identity, marked mass factorisation and zero-rate boundary. The thirteenth theorem combines exact superposition and splitting.

The substantial algebraic steps use the factorial ratio $(n+1)p_\lambda(n+1)=\lambda p_\lambda(n)$ , the binomial theorem and $e^{x+y}=e^xe^y$ , with all denominators equal to positive natural factorials. Count variables are nonnegative integers and finite coefficient identities do not themselves assert a construction of continuous-time Poisson processes. That stronger stochastic process claim is outside this mission.

An independent 80-digit decimal evaluation verified 1,968 count-convolution and split-joint identities, including $\lambda=0$ , $p=0$ , $p=1$ , mixed rates and both zero and positive counts.

This Draft is formally self-contained. It does not import the unpublished aggregate-claims theorems from XXVII and never claims that a proof is accepted simply because an open Lean proposition elaborates in a private authoring check.

18 thms2 active usersReviewed

Completed

Actuarial Science Probability·Captain: WillR

Actuarial Mathematics XXVIII: Discrete Stop-Loss Premium and Tail-Sum ValuationTextbook

Actuarial Mathematics XXVIII: Discrete Stop-Loss Premium and Tail-Sum Valuation

Actuarial sources and the derived finite-grid theorem

Harry H. Panjer (1980), The Aggregate Claims Distribution and Stop-Loss Reinsurance, Transactions of the Society of Actuaries 32, 523–535, examines aggregate distributions and stop-loss reinsurance. Panjer and Willmot (1982), Recursions for Compound Distributions, ASTIN Bulletin, connects efficient compound-claim recursion to net stop-loss premium calculations. Gordon E. Willmot, Steve Drekic and Jun Cai (2005), Equilibrium compound distributions and stop-loss moments, Scandinavian Actuarial Journal, DOI https://doi.org/10.1080/03461230510009691, studies tail/integrated-tail representations relevant to stop-loss valuation.

The mission gives a deliberately finite, integer-lattice and exact version of stop-loss valuation. It works on probability mass coefficients $w_s\ge0$ for integer aggregate losses $0\le s\le B$ . Some algebraic identities are true even for unnormalised real coefficients; this distinction is retained in the formal theorem types rather than assuming a distribution without stating it.

Insurance payment timing and strict attachment convention

The attachment $d\in\mathbb N$ is the insurer's retained limit, with reinsurer payment at the claim settlement date of

R_d(s)=(s-d)_+=\max(s-d,0),\qquad \min(s,d)+R_d(s)=s.

A claim exactly equal to d pays zero excess. The expected net stop-loss premium does not contain expense or variance loading:

\Pi_B(d)=\sum_{s=0}^{B}(s-d)_+w_s.

The insurer's retained limited expected loss is

L_B(d)=\sum_{s=0}^{B}\min(s,d)w_s, \qquad \mu_B=\sum_{s=0}^{B}sw_s.

The pointwise cashflow partition gives the actuarial bridge $L_B(d)+\Pi_B(d)=\mu_B$ . It is valid for any real mass coefficients by linearity of the finite sum.

Tail recursion and stop-loss transform

Let the strict loss tail be

T_B(d)=\sum_{s=d+1}^{B}w_s =\Pr(S>d)

when the coefficients form a normalised probability law. Raising the attachment from d to d+1 changes the payout by one unit on exactly the event $S>d$ . Consequently

\Pi_B(d)-\Pi_B(d+1)=T_B(d),\qquad T_B(d)-T_B(d+1)=w_{d+1}

for $d+1\le B$ , and the last difference is zero outside the grid.

Because $\Pi_B(d)=0$ at $d\ge B$ , the adjacent recurrence telescopes into the finite discrete tail-sum identity

\boxed{\Pi_B(d)=\sum_{j=d}^{B}T_B(j).}

With nonnegative probability coefficients, tails are nonnegative and decrease with attachment. It follows that $\Pi_B$ is nonnegative, nonincreasing and discretely convex:

\Pi_B(d)+\Pi_B(d+2)-2\Pi_B(d+1)\ge0.

The term at attachment B in the tail sum is zero. Deductibles above B also produce zero premium. The zero-attachment premium equals the full gross expected aggregate claim $\mu_B$ .

Proposed proof structure

Five local definitions cover the nonnegative excess payment, bounded expected excess premium, strict aggregate tail, retained limited mean and gross aggregate expected claim. Fourteen supporting milestone theorems establish individual claim boundaries, payment partition, zero/full attachments, nonnegativity, one-step premium and tail differences, monotonicity, discrete convexity, the limited-mean bridge and exact tail-sum valuation.

The capstone combines in one target theorem:

the gross claim expectation equals retained expected loss plus ceded net premium;
net stop-loss premium equals the sum of strict aggregate-loss tails;
the premium as a function of integer attachment has nonnegative second differences.

An independent exact-rational verification checked 72 bounded grid/attachment cases, including deductibles above the maximum loss and unnormalised nonnegative coefficient arrays. The cashflow, increment, tail-sum and convexity identities all passed.

Limitations and relationship to the sequence

The bounded-grid model can be populated by Actuarial XXVI's finite individual-risk aggregate PMF. Actuarial XXVII's compound Poisson model is generally unbounded, so its full stop-loss premium requires infinite-sum convergence and cannot be treated as if it shared this finite maximum B. Such a limit and numerical truncation-error guarantee would be a separate mission.

The formal source is self-contained until earlier definitions are actually published, and never imports a theorem merely because a prior mission was drafted. All supporting and capstone theorems are open Lean proof obligations.

20 thms2 active usersReviewed

Completed

Actuarial Science Probability·Captain: WillR

Actuarial Mathematics XXVI: Individual-Risk Aggregate Claims by ConvolutionTextbook

Actuarial Mathematics XXVI: Individual-Risk Aggregate Claims by Convolution

Research provenance and new formalisation

R. J. Verrall (1989), The individual risk model: a compound distribution, Journal of the Institute of Actuaries, volume 116(1), pages 101–107, DOI https://doi.org/10.1017/S0020268100036465, develops the connection between individual and collective aggregate-risk modelling. Nelson De Pril (1989), The Aggregate Claims Distribution in the Individual Model with Arbitrary Positive Claims, ASTIN Bulletin, volume 19(1), pages 9–24, DOI https://doi.org/10.2143/AST.19.1.2014913, develops exact aggregate-distribution recursion for the individual-risk model.

The present mission is a finite, integer-lattice, independent Bernoulli-policy formalisation. It derives probability-mass support, nonnegativity and normalisation from convolution, rather than claiming that either author already supplied these exact Lean theorem types.

Individual policies, integer benefits and dependence assumptions

Policy $i$ pays a fixed nonnegative integer benefit $b_i$ with probability $p_i$ , where $0\le p_i\le1$ . It pays nothing otherwise. The Bernoulli policy's payment distribution, as opposed to its event distribution, is

h_i(s)=(1-p_i)\mathbf1_{\{s=0\}}+p_i\mathbf1_{\{s=b_i\}}, \qquad s\in\mathbb N.

A zero-benefit policy has both events paying zero. Therefore its single payment coefficient at $s=0$ is $1$ , not $1-p_i$ . This corner case is explicitly retained, rather than assuming every $b_i$ is strictly positive.

The total loss over n independent policies is $S_n=\sum_{i<n}b_iB_i$ , with independent Bernoulli indicators $B_i$ . Its maximum possible loss is $B_n=\sum_{i<n}b_i$ .

Exact convolution and portfolio recursion

For coefficient arrays $f,g:\mathbb N\to\mathbb R$ , define their discrete convolution by

(f*g)(s)=\sum_{k=0}^{s}f(k)g(s-k).

With no policies the payment mass is $\delta_0(s)=\mathbf1_{\{s=0\}}$ . Each additional policy is introduced by

g_0(s)=\delta_0(s),\qquad g_{n+1}(s)=\bigl(g_n*h_{n}\bigr)(s).

A bound-aware mass operator is $M_B(f)=\sum_{s=0}^{B}f(s)$ . If the first distribution vanishes above B and the second above C, convolution satisfies $M_{B+C}(f*g)=M_B(f)M_C(g)$ , even for unnormalised intermediate coefficient arrays.

The companion algebraic lemmas establish convolution identity, commutativity and associativity. A distributional lemma establishes that nonnegative component masses imply nonnegative convolution coefficients.

Fundamental theorem

Under $0\le p_i\le1$ for every included policy, the portfolio aggregate is a valid bounded probability mass function:

\boxed{ g_n(s)\ge0\quad(\forall s\ge0),\qquad \sum_{s=0}^{B_n}g_n(s)=1,\qquad g_n(s)=0\quad(s>B_n). }

These are three distinct requirements: nonnegativity, normalisation on the exact finite benefit bound and zero support above that bound. All must be proved, including empty portfolios and policies whose benefit is zero. Independence is encoded by the convolution construction, not inferred from unrelated marginal Bernoulli probabilities.

Proof structure and validation

Five new definitions introduce convolution, one-policy Bernoulli mass, bounded total mass, maximum possible claim and recursive portfolio probability mass. Fourteen supporting milestones prove convolution identities and support/mass preservation, the policy recursion, and bounded portfolio mass and nonnegativity; the fifteenth theorem is the capstone.

An independent exact-rational benchmark enumerated all binary claim/no-claim events across 1,365 distinct heterogeneous policy configurations, with zero and repeated benefits and probabilities at 0, 1/4, 1/2 and 1. Direct event enumeration agreed exactly with recursive convolution, giving nonnegative coefficients and unit total mass.

The source uses natural-valued grid claims, not continuous severities, and finite portfolios only. It does not assume any unpublished other mission's definitions exist in the Lean environment. Imported Lean definitions are local within this mission, with all imports before namespaces. Every theorem remains an open proof obligation until proved on the authoritative Prove2Me remote compiler.

20 thms2 active usersReviewed

Completed

Actuarial Science Probability·Captain: WillR

Actuarial Mathematics XXVII: Compound Poisson Panjer RecursionTextbook

Actuarial Mathematics XXVII: Compound Poisson Panjer Recursion

Original actuarial research and the exact specialisation

Harry H. Panjer (1981), Recursive Evaluation of a Family of Compound Distributions, ASTIN Bulletin 12(1), 22–26, DOI https://doi.org/10.1017/S0515036100006796, proves a recursion for aggregate-claim distributions with suitable claim-frequency laws. The original paper treats a wider class than Poisson claim counts. Sundt and Jewell (1981), Further Results on Recursive Evaluation of Compound Distributions, ASTIN Bulletin 12(1), 27–39, DOI https://doi.org/10.1017/S0515036100006802, develops its extensions.

This mission formalises the positive-integer-severity compound Poisson case. The restriction on zero-sized claims is essential to the exact finite-count mixture used by the Lean definitions. It does not claim that a finite truncated Poisson mixture is automatically a probability distribution if zero severity has positive mass.

Count frequency and conditional aggregate severity

Let $N\sim\operatorname{Poisson}(\lambda)$ with $\lambda\ge0$ . Its count probabilities are

p_m=e^{-\lambda}\frac{\lambda^m}{m!},\qquad m=0,1,\ldots.

Each claim has a positive integer severity with mass $f_j$ . The key support condition is $f_0=0$ . The usual stochastic interpretation additionally requires $f_j\ge0$ and total severity mass one, although the algebraic Panjer theorem itself works for arbitrary real $f_j$ satisfying $f_0=0$ .

For exactly m independent claims, $f^{*m}$ is the m-fold discrete convolution, with $f^{*0}=\delta_0$ and $f^{*(m+1)}=f*f^{*m}$ . Each positive claim contributes at least one unit, hence

s<m\Longrightarrow f^{*m}(s)=0.

It follows that the compound Poisson coefficient at aggregate loss s can be written as an exact finite sum, despite the count distribution being unbounded:

g_s=\sum_{m=0}^{s}e^{-\lambda}\frac{\lambda^m}{m!}f^{*m}(s).

At $\lambda=0$ , the distribution is $\delta_0$ . When $f_0=0$ , the zero-loss aggregate mass equals $g_0=e^{-\lambda}$ .

Panjer recurrence and uniqueness

Panjer's recursion for this model is

\boxed{ g_0=e^{-\lambda},\qquad g_s=\frac{\lambda}{s}\sum_{j=1}^{s}j\,f_j\,g_{s-j} \quad(s\ge1). }

It can be derived by combining the Poisson count ratio $(m+1)p_{m+1}=\lambda p_m$ with the convolution-power coefficients. The zero-severity term has a factor j=0 and vanishes. Consequently the right-hand side at s depends only on the earlier aggregate coefficients $g_0,\ldots,g_{s-1}$ . A separate theorem asserts that the initial mass and this recurrence uniquely determine the aggregate mass sequence.

The main Lean theorem is a conjunction of the no-claim initial value, the one-step recursion for every $s+1$ , and uniqueness for any real sequence satisfying those identities. It is an exact theorem about coefficients, not a numerical approximation or an unsupported claim of convergence of a severity generating function.

Validation and important boundaries

Five local definitions represent severity convolution, m-claim convolution powers, Poisson frequency mass, the aggregate mixture and the Panjer coefficient update. Thirteen supporting theorems include power recursion, support, count ratio, zero rate, nonnegative coefficients, the Panjer identity and uniqueness. The fourteenth is the capstone.

The independent high-precision benchmark compared two implementations: (i) direct Poisson-weighted convolution powers and (ii) the Panjer recurrence. They agreed to better than $10^{-60}$ across 264 rate, severity and aggregate-size combinations using 70-digit decimal arithmetic, including zero frequency, fixed unit severity, two-point severity and a three-point severity with a gap.

The positive integer severity condition $f_0=0$ cannot simply be dropped: when zero-valued claims occur, $m>s$ can still contribute to aggregate loss s, and the true Poisson initial value becomes $\exp[-\lambda(1-f_0)]$ . That more general form, and arbitrary Panjer (a,b,0) counting laws, are explicitly out of scope.

No unpublished definitions are imported from Actuarial XXVI. The problem is mathematically linked but formally self-contained while XXVI is still a Draft. The theorem targets remain unproved until valid Lean submissions are accepted by Prove2Me.

23 thms2 active usersReviewed

Completed

Actuarial Science Probability·Captain: WillR

Actuarial Mathematics XXV: Mean-Variance Reinsurance and Optimal Quota ShareTextbook

Actuarial Mathematics XXV: Mean-Variance Reinsurance and Optimal Quota Share

Primary research and scope

Marek Kaluszka (2001), Optimal reinsurance under mean-variance premium principles, Insurance: Mathematics and Economics 28(1), 61–67, https://doi.org/10.1016/S0167-6687(00)00066-4, examines optimal retention when the reinsurance premium depends on claim mean and variance. Manuel Guerra and Maria de Lourdes Centeno (2010), Optimal Reinsurance for Variance Related Premium Calculation Principles, ASTIN Bulletin 40(1), 97–121, https://doi.org/10.2143/AST.40.1.2049220, studies the effect of variance-based loading on reinsurance decisions.

This mission isolates a clean Bernoulli claim and continuous quota-share specialisation, with a closed-form optimum and a finite-menu alternative. It does not assert the general optimal-retention functional results or the VaR/CVaR optimisations in the cited papers.

Insurer and reinsurer cashflow model

Let $X=b\,B$ , where $B$ is a Bernoulli indicator with $\Pr(B=1)=q$ . Its claim amount is $b\ge0$ and the claim probability satisfies $0\le q\le1$ . A quota share $r\in[0,1]$ is the insurer's retained proportion of each realised claim:

R_r(X)=rX,\qquad C_r(X)=(1-r)X,\qquad R_r(X)+C_r(X)=X.

The reinsurer receives a fixed premium at policy inception that is an expected-value premium plus a loading on ceded variance. Using parameters $\lambda\ge0$ and $\alpha\ge0$ , where each variance coefficient has reciprocal currency units, define

\Pi_r=\mathbb E[C_r(X)]+\lambda\operatorname{Var}(C_r(X)) =q(1-r)b+\lambda q(1-q)(1-r)^2b^2.

The insurer's objective adds expected retained claims, the reinsurance premium and a variance-based risk-capital charge on retained loss:

J(r)=\mathbb E[R_r(X)]+\Pi_r+\alpha\operatorname{Var}(R_r(X)).

For any real $r$ , the relevant expectation and variance formulas yield

J(r)=qb+q(1-q)b^2\bigl[\lambda(1-r)^2+\alpha r^2\bigr].

The premium $\Pi_r$ is deterministic once the contract and model are fixed, so it does not contribute additional random loss variance. A quota-share arrangement may change both the expected ceded premium and the variance of retained claims; both effects are included.

Continuous optimal quota-share retention

Assume $\lambda+\alpha>0$ in addition to nonnegative coefficients. Completing the square gives

\lambda(1-r)^2+\alpha r^2 =\frac{\lambda\alpha}{\lambda+\alpha} +(\lambda+\alpha)\left(r-\frac{\lambda}{\lambda+\alpha}\right)^2.

It follows that the optimal insurer retention, not the ceded proportion, is

\boxed{r^*=\frac{\lambda}{\lambda+\alpha}\in[0,1],\qquad J(r^*)\le J(r)\;\text{for all }r\in\mathbb R.}

The solution can be at a boundary. If $\lambda=0<\alpha$ the insurer fully cedes the claim, $r^*=0$ . If $\alpha=0<\lambda$ , it retains everything, $r^*=1$ . If both coefficients vanish, all retentions have the same objective and the displayed ratio is undefined: this case is explicitly excluded. With $0<q<1$ , nonzero claim amount and positive total coefficient, $r^*$ is unique. For zero variance, for example $q=0$ or $q=1$ , every retention has the same variance component, so uniqueness does not follow and is not asserted.

A real insurer may instead face a finite menu $A$ of quoted retentions $r_a$ . Since $A$ is nonempty and finite, a cost-minimising member $a^*$ always exists, but there is no promise that $r_{a^*}=r^*$ .

Structure and intended Lean proof

The five definitions represent retained claim, ceded claim, variance premium, insurer capital objective and closed-form continuous retention. Twelve intermediate theorem obligations establish cashflow conservation, claim nonnegativity, full retention and full cession boundaries, objective expansion, admissibility of the candidate, quadratic square completion, global optimality, strict uniqueness when appropriate and finite-menu attainment. The capstone combines $0\le r^*\le1$ with $J(r^*)\le J(r)$ for every real alternative.

The proof uses elementary real algebra and finite-set minimum selection. It requires neither local stochastic simulation nor a limit-of-policy-years theorem. The Bernoulli setup is deliberate, making the mean/variance premium principle analytically exact and testable before attempting general loss distributions.

Model boundaries

Annual claim occurrence is a single Bernoulli event. Multiple correlated claims, expense loadings, default, credit risk, taxes, multi-period dynamic adjustment and Solvency II regulatory capital are not modelled. The capital coefficient is a chosen deterministic variance penalty rather than a regulatory capital formula. An optimal $r^*$ in this model should not be confused with an optimal excess-of-loss attachment point or with the entropic risk-sensitive optimum in Missions XXI–XXII.

All displayed theorem targets are unproved obligations until the authoritative Prove2Me compiler accepts a valid Lean proof. The owner Draft is for captain confirmation and moderator review, not an accepted theorem library.

18 thms2 active usersReviewed

Completed

Actuarial Science Probability·Captain: WillR

Actuarial Mathematics XXIV: Multiple-Decrement Mortality Innovation VarianceTextbook

Actuarial Mathematics XXIV: Multiple-Decrement Mortality Innovation Variance

Research and distinction from the single-decrement formula

Shiu and Xiong (2021), An elementary derivation of Hattendorff's theorem, European Actuarial Journal 11, 319–323, https://doi.org/10.1007/s13385-020-00256-9, derives the fully discrete mortality variance formula using reserve differences and summation by parts. The present mission develops the multiple-decrement extension on a countable lifetime space, keeping the covariance of different termination causes in the same policy year. This is a new derived formalisation rather than a claim that Shiu and Xiong printed these exact competing-risk theorems.

The earlier Actuarial XIV mission considers multiple-decrement valuation and premium recursion, while XVI investigates yearly mortality innovation orthogonality. Neither automatically supplies the countable competing-cause variance theorem, particularly when the net amount at risk is different for each decrement cause.

Model, parameters and timing

The termination year is a natural number $K\in\mathbb N$ . Its cause $D$ belongs to a finite type $C$ . For every policy year $t$ and cause $c$ , write $w_{t,c}=\Pr(K=t,D=c)$ . Causes are mutually exclusive: exactly one cause is realised on termination.

Require $w_{t,c}\ge0$ , $\sum_{t=0}^\infty\sum_{c\in C}w_{t,c}=1$ and a strictly positive in-force mass at every policy year:

D_t=\sum_{c\in C}w_{t,c},\qquad S_t=\sum_{k\ge t}D_k>0,\qquad q_{t,c}=\frac{w_{t,c}}{S_t}.

The cause probabilities do not have to be equal. Their sum is at most one because survival through the year remains possible. The realised cause has no independent probability after termination: this is one joint time-and-cause categorical distribution, not a collection of independent single-decrement lives.

Cause-specific year surprises

For a realised scenario $(k,d)$ , define the year $t$ , cause $c$ surprise:

I_{t,c}(k,d)=\mathbf1_{\{k=t,\ d=c\}}- q_{t,c}\mathbf1_{\{k\ge t\}}.

All these innovations vanish when $k<t$ . At termination $(t,c)$ , the cause-c innovation is $1-q_{t,c}$ . The innovation of any other cause $d\ne c$ in the same year equals $-q_{t,d}$ . Therefore treating the cause indicators as independent would be wrong.

Let $\rho_{t,c}$ be the discounted cause-specific net amount at risk payable at the end of year $t+1$ . With cause-dependent death benefits $b_{t+1,c}$ and an appropriate prospective reserve $V_{t+1}$ , a typical amount is $\rho_{t,c}=v^{t+1}(b_{t+1,c}-V_{t+1})$ . The finite-horizon centred reserve surprise is

Z_n(k,d)=\sum_{t<n}\sum_{c\in C}\rho_{t,c}I_{t,c}(k,d).

The mission defines this random variable directly. A cashflow-specific reserve recursion would be a further theorem, not a hidden hypothesis.

Correct annual variance including cause covariance

Cause-specific innovations from different years are orthogonal. At the same year, however, distinct causes have negative weighted cross moments:

\mathbb E[I_{t,c}I_{t,d}] =-\frac{w_{t,c}w_{t,d}}{S_t}\qquad(c\ne d).

The full annual Hattendorff contribution is therefore

A_t=\sum_{c\in C}w_{t,c}\rho_{t,c}^2- \frac{\bigl(\sum_{c\in C}w_{t,c}\rho_{t,c}\bigr)^2}{S_t}.

This subtracts the square of the aggregate weighted amount at risk, rather than subtracting separate squares for individual causes. It is the unconditional variance contribution from one year's categorical decrement shock. The assumptions $w_{t,c}\ge0$ , $S_t>0$ and $D_t\le S_t$ imply $A_t\ge0$ by weighted Cauchy–Schwarz.

The capstone asserts

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

It works with an arbitrary finite cause set and a countably infinite possible termination-year set. It does not yet claim an infinite-horizon limit, which can be developed by applying XXIII-style summability to these $A_t$ .

Proof programme and boundaries

There are five new definitions, ten supporting milestone theorems and one capstone. The supporting obligations establish nonnegative year masses, exact observed/other-cause innovation values, zero horizon, the successor-year identity, nonnegative annual variance, scaling of risk exposure, and the negative cross-cause moment before proving the full year-by-year allocation.

The proof must distinguish the finite inner cause sum from the infinite outer lifetime sum; nonnegative mass and summability are explicitly required for countable expectation manipulations. The formal model allows zero annual incidence for a particular cause, but demands positive aggregate survival tails so the conditional fractions are defined. All proof obligations use the pinned Mathlib version and require authoritative Prove2Me remote compilation and accepted Lean proofs.

16 thms2 active usersReviewed

Completed

Quantum Error Correction Quantum Gravity Quantum Information·Captain: Alien60

Almheiri–Dong–Harlow 2015: Bulk Locality and Quantum Error Correction in AdS/CFTResearch Paper

Motivation

The AdS/CFT correspondence relates a theory of quantum gravity in anti-de Sitter space (the bulk) to a quantum field theory without gravity on its boundary (the CFT). A central question is how a local field operator $\phi(x)$ deep in the bulk is represented by boundary operators. Almheiri, Dong and Harlow (JHEP 04 (2015) 163) pointed out a puzzle.

The bulk operator can be reconstructed on several different boundary regions. For example, it can be reconstructed on $A\cup B$ , on $B\cup C$ or on $A\cup C$ , but not on any single one of them.
These reconstructions cannot all be the same CFT operator: an operator commuting with all local operators on a time slice must be trivial.

Their resolution is that the bulk effective theory is a quantum error-correcting code. Bulk operators are logical operators acting on a code subspace of the CFT Hilbert space. Different boundary representations agree only on that subspace, as one logical operator of an erasure-correcting code can be implemented on different subsets of qubits.

The mathematical backbone of that resolution is a finite-dimensional criterion for when a logical operator can be implemented on a given subsystem. This mission formalizes it (Appendix B of the paper), with the examples and corollaries of Section 3.

Timeline.

1996–1997: Schumacher and Nielsen characterize correctability by vanishing correlations with a reference system, condition (3.14) (arXiv:quant-ph/9604022). Grassl, Beth and Pellizzari give the matrix-element form (3.19) (arXiv:quant-ph/9610042).
1999: Cleve, Gottesman and Lo introduce the three-qutrit code as a quantum secret-sharing scheme (arXiv:quant-ph/9901025).
2006: Ryu and Takayanagi propose the holographic entanglement-entropy formula (arXiv:hep-th/0603001).
2007: Bény, Kempf and Kribs develop operator-algebra quantum error correction (arXiv:quant-ph/0608071, arXiv:0705.1574), of which the theorem here is a special case.
2014–2015: Almheiri, Dong and Harlow recast bulk reconstruction as quantum error correction; Pastawski, Yoshida, Harlow and Preskill build holographic tensor-network codes (arXiv:1503.06237).
2016: Dong, Harlow and Wall establish reconstruction in the entanglement wedge (arXiv:1601.05416). Harlow derives the Ryu–Takayanagi formula from operator-algebra error correction (arXiv:1607.03901).

Setting

The physical Hilbert space is a tensor product $\mathcal H = \mathcal H_E\otimes\mathcal H_{\bar E}$ of finite-dimensional spaces. $E$ is the part that may be erased (lost), and $\bar E$ is the part that remains. A code subspace is a subspace $\mathcal H_{\mathcal C}\subseteq\mathcal H$ .

An operator $O$ acts within the code subspace if both $O$ and $O^\dagger$ map $\mathcal H_{\mathcal C}$ into itself. Such an operator has a representation on $\bar E$ if there is an operator $O_{\bar E}$ acting only on $\bar E$ , that is of the form $\mathbb 1_E\otimes Y$ , with

O_{\bar E}|\tilde\psi\rangle = O|\tilde\psi\rangle,\qquad O_{\bar E}^\dagger|\tilde\psi\rangle = O^\dagger|\tilde\psi\rangle\qquad\text{for all }|\tilde\psi\rangle\in\mathcal H_{\mathcal C}.

Representations on $E$ are defined in the same way, with operators $X\otimes\mathbb 1_{\bar E}$ .

The three-qutrit code (Section 3.1) encodes one qutrit into three via

|\tilde\imath\rangle = \tfrac{1}{\sqrt3}\textstyle\sum_{a\in\mathbb Z_3}|a,\ a+i,\ a+2i\rangle,

that is, $|\tilde 0\rangle = (|000\rangle+|111\rangle+|222\rangle)/\sqrt3$ and so on (Eq. (3.3)).

Formalization targets

Goal: the basic theorem of operator-algebra quantum error correction (Section 3.5, proof in Appendix B)

For an operator $O$ acting within $\mathcal H_{\mathcal C}$ ,

O\ \text{has a representation on }\bar E\iff \langle\tilde\psi'|\,[O,\,X_E\otimes\mathbb 1_{\bar E}]\,|\tilde\psi\rangle = 0\ \ \text{for all } X_E \text{ on } E \text{ and all } |\tilde\psi\rangle,|\tilde\psi'\rangle\in\mathcal H_{\mathcal C}.

Milestones (in source order)

Section 3.1 (after Eq. (3.3)): for every encoded three-qutrit state, the reduced density matrix of each single qutrit is $\tfrac13\mathbb 1$ .
Eqs. (3.4)–(3.6): the permutation $U_{12}$ of Eq. (3.6) is unitary, and $(U_{12}\otimes I_3)|\tilde\imath\rangle = |i\rangle\otimes\tfrac1{\sqrt3}(|00\rangle+|11\rangle+|22\rangle)$ .
Eqs. (3.9)–(3.10): for every single-qutrit operator $O$ , the operator $O_{12} = U_{12}^\dagger (O\otimes\mathbb 1) U_{12}$ , with $O$ acting on the first qutrit, satisfies $O_{12}|\tilde\imath\rangle = \sum_j O_{ji}|\tilde\jmath\rangle$ .
Section 3.2, Eqs. (3.19) ⟺ (3.21): the projection of every $X_E$ onto the code subspace is proportional to the identity iff every operator acting within the code subspace has a representation on $\bar E$ . The source states, citing the literature, that (3.19) is equivalent to correctability of the erasure of $E$ ; that equivalence is not formalized.
Section 3.5, two-qubit example: on the code spanned by $(|00\rangle+|11\rangle)/\sqrt2$ and $(|01\rangle+|10\rangle)/\sqrt2$ , the logical $X$ is realized by the bit flip of either qubit. No operator on the first qubit alone reproduces the logical $Z$ on the code, and every logical operator realizable on the first qubit acts on the code as $a\mathbb 1 + b\bar X$ : the code corrects only the subalgebra generated by $\mathbb 1$ and $\bar X$ .
Section 3.5, algebraic no-cloning: if $O_1$ has a representation on $\bar E$ and $O_2$ has a representation on $E$ , then $O_1$ and $O_2$ commute on the code subspace. Consequently, the elements of any family of logical operators that is represented both on $E$ and on $\bar E$ commute pairwise on the code subspace, so a non-abelian algebra cannot be represented on both.

Significance

The result. The goal theorem characterizes, by a checkable commutation condition, which logical operators survive the loss of $E$ ; milestone 4 is its specialization to full erasure correction. Milestone 6 explains why a non-commuting algebra of bulk operators cannot be represented on two complementary boundary regions at once, so reconstructions of $\phi(x)$ on different regions are distinct operators that agree only on the code subspace. The three-qutrit code models this: every logical operator is realized on any two qutrits, and no single qutrit carries information.

Formalizing it. All statements are proved in the source, or cited there from standard references, and are finite-dimensional. This mission produces machine-checked versions and a reusable vocabulary of code subspaces, logical operators and subsystem representations. That vocabulary is the starting point for formalizing the later results it underlies, in particular the subsystem and operator-algebra theorems of Harlow's derivation of the Ryu–Takayanagi formula (arXiv:1607.03901).

Status honesty. The mathematics is unconditional finite-dimensional linear algebra. The application to AdS/CFT rests on the conjectured duality and on bulk effective field theory, and is context only; none of it enters the hypotheses. The appendix proof is the authors' own, and the theorem is a special case of the results of Bény, Kempf and Kribs. The equivalence of (3.19) with correctability of the erasure (the existence of a recovery unitary, Eqs. (3.14)–(3.18)) is cited in the source from Schumacher–Nielsen and Grassl–Beth–Pellizzari, and is not part of this mission. No machine-checked proof of any of these statements is known. Neither Mathlib nor Physlib (including its quantum-information library) formalizes code subspaces, erasure correction or operator-algebra quantum error correction.

Difficulty

The forward direction of the goal is a direct computation. The converse is an existence statement: an operator $O_{\bar E}=\mathbb 1_E\otimes Y$ has to be produced from a hypothesis that constrains only the matrix elements of $O$ between code states. That hypothesis says nothing about how $O$ acts off the code subspace, and $O$ generally acts nontrivially on $E$ . So no candidate for $Y$ can be read off from $O$ itself.

Milestone 4 has the same character in both directions. One direction must produce a representation on $\bar E$ for every operator acting within the code subspace, starting from the scalar condition (3.19), which concerns operators on $E$ alone. The other direction is a non-existence claim about operators on $E$ , to be derived from a property quantified over all logical operators.

The explicit-code milestones are finite but involve the irrational normalization $1/\sqrt3$ and a $27$ -dimensional space.

Formalization scope

Representation. Vectors on $\mathcal H_E\otimes\mathcal H_{\bar E}$ are functions on $e\times\bar e$ for finite types $e,\bar e$ , with $E$ first. Operators are complex matrices, tensor products are Mathlib's Kronecker product ⊗ₖ, $O^\dagger$ is the conjugate transpose, and $\langle w|u\rangle$ is star w ⬝ᵥ u.
Code subspace. The code subspace is an arbitrary complex subspace (Submodule ℂ). It is described without a basis: " $\langle\tilde\imath|\cdots|\tilde\jmath\rangle = 0$ for all $i,j$ " is stated for all pairs of code vectors, which is equivalent by sesquilinearity.
Proportionality. Eq. (3.19), $\langle\tilde\imath|X_E|\tilde\jmath\rangle = \delta_{ij}C(X)$ , is stated basis-free as $\langle w|X_E v\rangle = c\,\langle w|v\rangle$ for one constant $c$ and all code vectors $v,w$ .
Three-qutrit vectors. These are indexed by $((q_1,q_2),q_3)$ . $U_{12}$ is the permutation matrix of the table in Eq. (3.6), and the single-qutrit reduced states are partial traces over the other two qutrits.
Not trivial. The goal quantifies over every code subspace and every operator acting within it. The zero subspace makes both sides true and is harmless. The examples are fixed concrete codes.
Not formalized. Cited but not proved in the source: (3.14) with the recovery unitary (3.16)–(3.18), and the bound (3.25). Heuristic: the count (3.22) and the Page-theorem argument after it. Definitions only: quantum secret sharing (Section 3.3), (3.23) and (3.24). Immediate or by symmetry: (3.20), recovery from qutrits 2,3 or 1,3, and the $*$ -subalgebra remark after the theorem. Out of scope: Sections 4–5 (the AdS/CFT model, backreaction).
Infrastructure. A complete development needs lemmas on Kronecker products acting on vectors ((A ⊗ₖ B) *ᵥ v), conjugate transposes of Kronecker products, orthogonal projection onto a Submodule, and partial traces. These are reusable; stand-alone contributions are welcome.

Selected references

A. Almheiri, X. Dong, D. Harlow, Bulk locality and quantum error correction in AdS/CFT, JHEP 04 (2015) 163. arXiv:1411.7041
C. Bény, A. Kempf, D. W. Kribs, Generalization of quantum error correction via the Heisenberg picture, Phys. Rev. Lett. 98, 100502 (2007). arXiv:quant-ph/0608071
C. Bény, A. Kempf, D. W. Kribs, Quantum error correction of observables, Phys. Rev. A 76, 042303 (2007). arXiv:0705.1574
B. Schumacher, M. A. Nielsen, Quantum data processing and error correction, Phys. Rev. A 54, 2629 (1996). arXiv:quant-ph/9604022
M. Grassl, T. Beth, T. Pellizzari, Codes for the quantum erasure channel, Phys. Rev. A 56, 33 (1997). arXiv:quant-ph/9610042
R. Cleve, D. Gottesman, H.-K. Lo, How to share a quantum secret, Phys. Rev. Lett. 83, 648 (1999). arXiv:quant-ph/9901025
S. Ryu, T. Takayanagi, Holographic derivation of entanglement entropy from AdS/CFT, Phys. Rev. Lett. 96, 181602 (2006). arXiv:hep-th/0603001
F. Pastawski, B. Yoshida, D. Harlow, J. Preskill, Holographic quantum error-correcting codes: toy models for the bulk/boundary correspondence, JHEP 06 (2015) 149. arXiv:1503.06237
X. Dong, D. Harlow, A. C. Wall, Reconstruction of bulk operators within the entanglement wedge in gauge-gravity duality, Phys. Rev. Lett. 117, 021601 (2016). arXiv:1601.05416
D. Harlow, The Ryu–Takayanagi formula from quantum error correction, Commun. Math. Phys. 354, 865 (2017). arXiv:1607.03901

10 thms2 active usersReviewed

Completed

Actuarial Science Probability·Captain: WillR

Actuarial Mathematics XXII: Finite-State Entropic Bellman ControlTextbook

Fully Discrete Entropic Bellman Control with Finite Insurance States and Retention Actions

Insurance motivation and valuation horizon

An insurer choosing a retention or other reinsurance action in one year may affect both the immediate net claim cost and the distribution of liabilities in the following year. When the insurer values uncertainty using an exponential risk measure, the relevant policy objective applies the same conditional risk valuation recursively across policy years. A finite-horizon state-and-action model makes the timing, transition probabilities and policy optimality statement mathematically explicit.

This mission studies a finite-state, finite-action, discrete-time cost minimisation problem. Actions may represent a menu of excess-of-loss retention levels, but the formal statements allow any finite action menu and any state-dependent insurer cost schedule. It extends the cost-control ideas in prior actuarial missions into an explicitly risk-sensitive dynamic model. The result is a specialisation of finite-horizon recursive risk-sensitive Markov decision theory, with its own finite real-valued hypotheses and theorem proof obligations.

Timing, transition probabilities and discounting

Let $S$ be the finite collection of financial, underwriting or liability states and $A$ a finite nonempty set of insurance actions. At the beginning of a policy year the insurer observes the current state $s\in S$ and selects an action $a\in A$ . At the end of that year, the state becomes $t\in S$ with conditional transition probability $P(s,a,t)$ .

We require, for each current state and action,

P(s,a,t)\ge0\quad\text{for all }t, \qquad \sum_{t\in S}P(s,a,t)=1.

An individual destination is allowed to have probability zero. The annual real-valued cost $c(s,a,t)$ includes the insurer's net premium, claim and treaty cashflows for the covered year, with its sign convention chosen so that larger positive values mean higher losses. A deterministic terminal amount $h(s)$ values residual liabilities when the chosen finite horizon ends. With consistent payment-date conventions, let $\beta\ge0$ be the factor applied to the next year's continuation cost and $\gamma>0$ the entropic risk-aversion parameter for costs.

The real-valued stage costs are finite by construction. Hence, because the transition row is a genuine probability law, the exponential moment defined below is strictly positive.

Conditional entropic valuation of one year

For any future state-value function $F:S\to\mathbb R$ , define

M_{\gamma,\beta}(s,a;F) =\sum_{t\in S}P(s,a,t) \exp\!\left(\gamma\bigl[c(s,a,t)+\beta F(t)\bigr]\right)

and the one-year risk-sensitive insurer cost

\boxed{ Q_{\gamma,\beta}(s,a;F) =\frac{1}{\gamma}\log M_{\gamma,\beta}(s,a;F). }

The cost and continuation value are included in one conditional exponential moment. The former is paid or valued within the current period, and the latter carries the next-year discount factor. The same chosen action changes both the costs and the transition row.

If every destination has the identical current-period cost $c$ and continuation $u$ , then probability normalisation implies $Q_{\gamma,\beta}=c+\beta u$ . If every annual cost is increased by a fixed $k$ , the stage value increases by $k$ under the unit-mass probability row. With nonnegative transition probabilities, $\gamma>0$ and $\beta\ge0$ , increasing either annual costs or future costs cannot decrease the entropic stage value.

The discount factor must remain inside the exponential

For an annual cost $c(s,a,t)=d(s,a)$ independent of the next state, the expression simplifies to

Q_{\gamma,\beta}(s,a;F) =d(s,a)+\frac1\gamma \log\left(\sum_{t\in S}P(s,a,t) e^{\gamma\beta F(t)}\right).

Writing $\rho_\eta(F)=\eta^{-1}\log\sum_tP(s,a,t)e^{\eta F(t)}$ , the continuation term for $\beta>0$ is $\beta\rho_{\gamma\beta}(F)$ . In general it differs from $\beta\rho_\gamma(F)$ . Entropic risk valuation is cash-additive and monotone under the stated conditions, but it is not generally homogeneous in the random cost. For $\beta=0$ , continuation costs make no contribution and no division by $\gamma\beta$ is performed.

This matters in actuarial applications: transplanting an expectation-based Bellman formula and simply replacing each conditional expectation with a fixed-parameter entropic premium would alter the intended discounted model.

Remaining-horizon policy and Bellman recursions

Let $n\in\mathbb N$ denote the number of policy years remaining. A deterministic nonstationary Markov policy $\pi:\mathbb N\times S\to A$ selects action $\pi(k,s)$ when $k+1$ years remain and the current state is $s$ .

Its recursively valued insurer cost is

J^\pi_0(s)=h(s), \qquad J^\pi_{k+1}(s) =Q_{\gamma,\beta}\!\left(s,\pi(k,s);J^\pi_k\right).

Define the finite-action entropic Bellman minimum by $TF(s)=\min_{a\in A}Q_{\gamma,\beta}(s,a;F)$ . Its finite-horizon optimum satisfies

V_0(s)=h(s), \qquad V_{k+1}(s) =\boxed{\min_{a\in A}Q_{\gamma,\beta}(s,a;V_k)}.

At horizon zero the terminal amount is the entire valuation. At each successor horizon, the minimum is attained because the action set is finite and nonempty. Positive risk aversion, nonnegative discounting and a stochastic transition row make the entropic stage map monotone in its continuation argument. Those properties support induction from the terminal year backwards.

Proposed fundamental theorem

For the finite model above, the capstone combines domination of every deterministic nonstationary Markov policy with existence of an attaining Markov policy:

\boxed{ \begin{aligned} &V_n(s)\le J^\pi_n(s) &&\text{for every policy }\pi\text{ and state }s,\\ &\exists\,\pi^*\quad J^{\pi^*}_n(s)=V_n(s) &&\text{for every state }s. \end{aligned} }

The second line asserts a single policy that works simultaneously for all starting states. Its state- and remaining-horizon-dependent actions may be obtained by selecting a minimiser at each finite Bellman step.

The formal graph contains definitions for the transition exponential moment, entropic stage valuation, finite-action minimum, fixed-policy value and Bellman value. The supporting theorem targets establish strict positivity, deterministic-value reduction, monotonicity, cash additivity, minimum comparison and attainment, the base and successor horizon identities, policy cost domination and an attaining policy. The capstone joins the latter optimality statements.

Mathematical scope and boundary cases

All probability distributions here have finite support in a finite state space, and the horizon is finite. Stochastic rows are required only where a conditional cost interpretation or positivity is used. Zero transition probabilities for particular destinations cause no division-by-zero problem. A zero-horizon value is exactly its terminal cost; $\beta=0$ removes future exposure from each one-step valuation. The type-level definition permits an empty state type, for which assertions at each starting state are vacuous, while the action type remains nonempty.

The positive-risk-aversion assumption excludes $\gamma=0$ . Any analytical expected-value limit as $\gamma\to0$ would require a separate result. Negative gamma is outside the proposed monotone insurer-cost interpretation.

The capstone is stated for deterministic nonstationary Markov policies only. It does not formally establish comparison with all randomised or history-dependent strategies, optimality for infinite horizons or an HJB verification theorem for continuous-time stochastic factors. A finite treaty price from other actuarial missions may later be substituted into $c$ , after its own publication and consistency checks. No additional imported theorem dependencies are assumed here.

Evidence and source attribution

The source declarations have been checked by Prove2Me's private remote Lean compiler at the pinned Mathlib revision. The remote compiler's overall failure is deliberately caused by the incomplete proof bodies and a terminal type-mismatch sentinel; there were no unexpected declaration elaboration errors. This validates the proposed types and definitions, not any Lean proof. Independent high-precision finite model evaluation supports the mathematical direction, subject to the limitations of numerical evidence. The listed mathematical results remain proof obligations until accepted proof submissions exist.

[1] Bäuerle, Nicole and Glauner, Alexander (2022), Markov decision processes with recursive risk measures, European Journal of Operational Research, 296(3), 953–966. In the author preprint, Definition 4.6 states the one-step recursive risk operators, Theorem 4.7 establishes the finite-horizon Bellman value and existence of Markov optimal policies under Assumptions 3.1 and 4.2, and equation (4.2) is the one-step minimisation in the backward-induction proof. This mission explicitly specialises the framework to finite insurance costs and entropic valuation.

[2] Bäuerle, Nicole and Jaśkiewicz, Anna (2024), Markov decision processes with risk-sensitive criteria: an overview, Mathematical Methods of Operations Research, 99, 141–178. Example 1(a), equation (2) gives an entropic certainty equivalent in reward convention. The sign has been translated to an insurer cost/loss convention here.

[3] Actuarial Mathematics XVII: Finite-Horizon Markov Decision and Optimal Policy Valuation, previously published finite-state/action Markov recursion declarations. The present mission uses a distinct cost-minimising entropic stage operator, so it does not import XVII's reward-maximising Bellman definitions.

[4] Actuarial Mathematics XXI: Finite Exponential Premiums and Risk-Sensitive Retention, an earlier owner Draft concerning one-period entropic reinsurance premiums. Its unpublished declarations are not imported as available source modules.

18 thms2 active usersReviewed

Completed

Actuarial Science Probability·Captain: WillR

Actuarial Mathematics XVIII: Expected-Value Reinsurance Premiums and Optimal Finite RetentionTextbook

Motivation: a priced excess-of-loss treaty and a finite retention decision

An excess-of-loss reinsurance treaty divides each insurance claim between the insurer and a reinsurer at an agreed retention. The cedant retains the first portion of the claim while the reinsurer pays the excess. The decision to purchase reinsurance trades off the reinsurer's premium against the insurer's retained claims and risk-capital requirement.

Bäuerle and Glauner [1, §6] discuss the classic expected-value premium principle for reinsurance,

\pi_R(C)=(1+\theta)\,\mathbb E[C],

where $C$ is the ceded claim amount and $\theta$ is the reinsurer's safety loading. Their paper develops a broader discrete-time dynamic reinsurance application under risk measures. Glauner [2] develops a risk-sensitive Markov decision formulation for dynamic reinsurance with general premium principles. Brachetta and Ceci [3] provide the related continuous-time stochastic-factor excess-of-loss problem, which includes a more complicated HJB verification theorem.

This mission establishes a finite-scenario, single-period insurance cost and finite-retention optimisation layer. It makes the expected-value premium algebra precise, shows how the safety loading changes expected insurer cost, and introduces an illustrative, transparently specified variance-based capital add-on. The finite optimum is then attained by one of a nonempty set of allowable retentions. This mathematical bridge can later be incorporated into Mission XVII's finite-horizon optimal policy recursion.

Split each claim at the retention

Let $z\in\mathbb R$ be a realised gross insurance claim and $a\in\mathbb R$ the retention limit. The actuarial interpretation concerns $z\ge0$ , $a\ge0$ ; the Lean definitions extend the formulas to all reals for algebraic convenience.

The retained and ceded claims are respectively

r(z,a)=\min(z,a),\qquad c(z,a)=z-\min(z,a).

Consequently

r(z,a)+c(z,a)=z.

The insurer cannot retain more than either the original claim or its chosen retention. The ceded amount is nonnegative and decreases, or stays constant, as the retention is increased. These results follow directly from the minimum function without needing a particular claim distribution.

Finite-scenario expected-value reinsurance cost

Let $\Omega$ be a finite set of claim scenarios, with weights $w_\omega\ge0$ summing to one, and gross claim function $Z(\omega)$ . Define

\mathbb E_w[X]=\sum_{\omega\in\Omega}w_\omega X(\omega).

The expected retained loss is $\mathbb E_w[r(Z,a)]$ , while the reinsurer's premium for the ceded part, under the expected-value premium principle with loading $\theta$ , is

\pi_R(a)=(1+\theta)\,\mathbb E_w[c(Z,a)].

The insurer's expected cost, comprising retained claims plus reinsurance premium, is

C_\theta(a)=\mathbb E_w[r(Z,a)] +(1+\theta)\mathbb E_w[c(Z,a)].

Because retained and ceded claims add to gross claims, linearity gives the useful exact identity

\boxed{ C_\theta(a)=\mathbb E_w[Z] +\theta\,\mathbb E_w[c(Z,a)]. }

If $\theta=0$ , total expected cost equals gross expected claims and is independent of retention. If $\theta\ge0$ and scenario weights are nonnegative, increasing retention reduces the expected ceded amount and therefore cannot increase this pure expected cost:

a\le b\implies C_\theta(b)\le C_\theta(a).

This is not a general claim that greater retention is better for an insurer. It shows precisely why a risk criterion is needed when retention involves a trade-off: expected-value pricing with a nonnegative loading alone rewards retaining more risk.

An explicit retained-risk capital charge

To introduce a simple finite model of capital cost, define the retained-claim variance

\operatorname{Var}_w[r(Z,a)] =\sum_{\omega\in\Omega}w_\omega \left(r(Z(\omega),a)-\mathbb E_w[r(Z,a)]\right)^2.

For nonnegative weights this variance is nonnegative. Let $\lambda\ge0$ be an illustrative cost per unit of retained variance and define

\boxed{ J_{\theta,\lambda}(a)= C_\theta(a)+ \lambda\,\operatorname{Var}_w[r(Z,a)]. }

The functional $J$ is an explicit modelling choice for this mission, not a formula attributed directly to Bäuerle and Glauner. Their paper uses more general risk measures and cost-of-capital principles, which motivate the need for a risk-sensitive criterion. A variance charge is a mathematically simple finite-scenario proxy rather than the complete dynamic capital methodology of [1–2].

Under $\lambda\ge0$ and nonnegative scenario weights,

J_{\theta,\lambda}(a)\ge C_\theta(a).

At $\lambda=0$ , the added capital cost disappears. Unlike pure expected cost, the variance-adjusted objective need not be monotone in retention. The optimum can depend on the distribution, reinsurer loading and variance charge.

Selecting an optimal retention from a finite menu

Let $A$ be a finite nonempty set of permissible treaty choices, and let $\alpha:A\to\mathbb R$ give the retention level associated with each choice. For an actuarial contract assume $\alpha_a\ge0$ , though the Lean maximum/minimum existence theorems need only finiteness and nonemptiness.

Define the best achievable risk-adjusted cost

J^\star=\min_{a\in A}J_{\theta,\lambda}(\alpha_a).

The supporting theorems establish that every candidate has cost at least $J^\star$ , and some admissible choice $a^\star$ achieves equality:

J^\star\le J_{\theta,\lambda}(\alpha_a) \quad\text{for every }a\in A, \qquad J^\star=J_{\theta,\lambda}(\alpha_{a^\star}).

This result is finite-action existence, not a claimed optimal continuous stochastic control. If the chosen retention menu and claim process become state dependent, this one-step reward or cost can be fed into the finite-horizon dynamic programming model of Mission XVII, subject to an appropriate specification of state transitions.

Formal theorem graph, boundaries and limitations

The draft has seven definitions: retained claim, ceded claim, finite weighted expectation, loaded expected premium cost, retained variance, risk-adjusted objective and finite optimal retention cost. Fourteen supporting theorem targets prove split and bounds, the monotone ceded claim, premium decomposition, zero loading, monotonic pure expected cost, nonnegative retained variance, zero variance-charge limit and finite argmin existence. The capstone combines universal optimal-cost lower bounds and an attaining retention choice.

The algebraic identities hold for arbitrary real weights and monetary amounts, with nonnegative weights required for probability inequalities and variance nonnegativity. A unit-sum condition is necessary for interpreting weights as a probability law, although the core finite-sum identities remain true without it. The actuarial discussion assumes nonnegative claims and retention, and nonnegative loading and capital coefficient where specified.

No Monte Carlo approximation, continuous-time wealth process, ruin probability, stochastic premium model or HJB partial differential equation is asserted. The mission is a finite expected-cost and finite risk-penalty formalisation, designed as a controlled predecessor to more complex dynamic reinsurance.

All Lean statements are proposed proof obligations. A private declaration-compilation check, even if all statements elaborate, is not an accepted proof, and unpublished local definitions cannot be treated as already importable in individual theorem files.

References

[1] Bäuerle, Nicole and Glauner, Alexander (2021), “Minimizing spectral risk measures applied to Markov decision processes”, Mathematical Methods of Operations Research, Section 6, Dynamic optimal reinsurance, particularly equation (6.1), the premium-principle discussion and the discrete-time risk-sensitive optimisation context.

[2] Glauner, Alexander (2022), “Dynamic reinsurance in discrete time minimizing the insurer's cost of capital”, Scandinavian Actuarial Journal, pp. 279–306. Establishes a broader discrete-time reinsurance/Markov decision framework with general risk measures and premium principles; it does not specifically prescribe the variance-only charge chosen here.

[3] Brachetta, Matteo and Ceci, Claudia (2019), “Optimal Excess-of-Loss Reinsurance for Stochastic Factor Risk Models”, Risks 7(2), article 48, and open preprint. Motivates the retained claim function and later continuous-time control research, not a direct derivation of this finite-stage capital add-on.

22 thms2 active usersReviewed

Completed

Actuarial Science Probability·Captain: WillR

Actuarial Mathematics XXI: Finite Exponential Premiums and Risk-Sensitive RetentionTextbook

Motivation and actuarial context

Insurance premiums are commonly calculated from an expected claim with a safety loading, but this approach does not by itself distinguish risks having the same mean and different tail behaviour. A classical alternative is the exponential premium principle, also known as the entropic certainty equivalent. It charges for the full distribution of a loss through the expectation of an exponential transformation. Tsanakas and Desli [1] explain how the exponential premium principle arises from expected utility theory, and compare its properties with other premium and risk-measure principles.

Bäuerle and Glauner [2–3] study risk-sensitive Markov decision processes, including recursively applied risk measures and the entropic functional. This motivates a later dynamic reinsurance programme. The present mission deliberately formalises the finite-scenario, one-step algebra: positivity of the exponential moment, cash additivity and monotonicity of the premium, and attainment of a risk-sensitive choice from a finite menu of reinsurance retentions. It is not a theorem about general stochastic processes, asymptotic ruin probabilities or continuous-time optimal control.

Finite weighted exponential valuation

Let $\Omega$ be a finite set of insurance-claim scenarios, $X:\Omega\to\mathbb R$ a loss amount, and $w_\omega$ the weight of each scenario. For a probability law assume

w_\omega\ge0,\qquad\sum_{\omega\in\Omega}w_\omega=1.

The positive risk-sensitivity parameter is $\gamma>0$ . Define the exponential moment

M_\gamma(X)=\sum_{\omega\in\Omega}w_\omega e^{\gamma X(\omega)}.

For a nonnegative unit-sum weight law, $M_\gamma(X)>0$ for every real $\gamma$ , since at least one scenario has positive weight and every exponential factor is positive. This guarantees that the real logarithm is applied to a strictly positive number.

The entropic insurance premium is

\boxed{ \rho_\gamma(X)=\frac{1}{\gamma}\log M_\gamma(X). }

For any $\gamma\ne0$ with positive exponential moment this is a well-defined finite certainty equivalent. The formal Lean definition uses real division for every $\gamma$ , which is totalised at zero, but the actuarial interpretation and monotonicity theorem use strictly positive sensitivity. The formalisation does not assert that the $\gamma=0$ formula is the limiting expected-value premium: proving that limit requires a separate analytic theorem.

Premium principles and deterministic cash shifts

If $X(\omega)=c$ in every scenario, then

M_\gamma(X)=e^{\gamma c}, \qquad \rho_\gamma(X)=c,\quad\gamma\ne0.

In particular, zero claims have zero premium. The key cash-additivity or translation-invariance identity is

M_\gamma(X+c)=e^{\gamma c}M_\gamma(X),

and consequently, whenever $M_\gamma(X)>0$ and $\gamma\ne0$ ,

\boxed{\rho_\gamma(X+c)=\rho_\gamma(X)+c.}

Thus a known extra expense of $c$ is added directly to the premium, rather than changing how stochastic variability is priced. This monetary risk-measure property is one of the central axioms discussed by Tsanakas and Desli [1].

For two scenario claim amounts satisfying $X(\omega)\le Y(\omega)$ for every $\omega$ , positive sensitivity $\gamma>0$ , and nonnegative probability weights, exponential and logarithmic monotonicity give

\rho_\gamma(X)\le\rho_\gamma(Y).

The supporting theorems prove the exponential-moment ordering first, then transfer it through the increasing logarithm and division by $\gamma>0$ . The formal source does not assume the two risks are independent or that a moment-generating function exists outside the finite scenario model.

A finite excess-of-loss reinsurance decision

Suppose the cedant chooses an excess-of-loss retention $a$ . For a realised gross claim $z$ , the amount retained by the insurer is

r(z,a)=\min(z,a).

Conventional insurance interpretation requires nonnegative claims and retention. The underlying Lean function is real-valued on all arguments so algebraic order properties can be stated without additional domain restrictions.

Let $q(a)$ be a deterministic reinsurance premium quoted for retention $a$ . The combined risk-sensitive cost of the retention choice is

\boxed{ J_\gamma(a)=q(a)+\rho_\gamma(r(Z,a)). }

This is a model choice: the insurer adds the quoted cost of its treaty to the entropic valuation of the stochastic losses it still retains. The quoted premium is an arbitrary input function. The mission does not assume it decreases with higher retention, or that it has been calculated by the reinsurer using the same exponential premium principle.

Let $A$ be a finite, nonempty set of allowed treaty choices, with $\alpha:A\to\mathbb R$ mapping each choice to a retention level. The optimal cost is

J_\gamma^\star=\min_{a\in A}J_\gamma(\alpha_a).

Since the action set is finite and nonempty, the minimum is attained. The capstone establishes that every menu action has cost at least $J_\gamma^\star$ , and there is an action $a^\star$ satisfying

\boxed{ J_\gamma^\star\le J_\gamma(\alpha_a)\quad\forall a\in A, \qquad J_\gamma^\star=J_\gamma(\alpha_{a^\star}). }

This is finite-menu optimisation. It does not by itself establish a finite-horizon optimal policy, solve a risk-sensitive Bellman equation, or prove optimality over a continuous retention interval. Those extensions require explicit state transitions and additional regularity or compactness assumptions.

Formal proof graph and important boundaries

Five definitions establish the finite exponential moment, entropic premium, retained claim, risk-sensitive one-period reinsurance cost, and finite-menu optimal cost. Thirteen supporting theorems establish nonnegative and positive exponential moments, constant-claim cases, factorisation and cash additivity, exponential and premium monotonicity, monotonic retained claim, and finite argmin bounds and attainment. The capstone combines finite-menu domination and an attaining retention.

The definitions and theorem statements apply to arbitrary finite types and real weights where algebraically meaningful; the probabilistic interpretation needs nonnegative weights of total one. Finite moments are automatically finite for real-valued scenarios, but the logarithm requires a positive moment for the usual risk valuation. The proof of cash additivity uses $\gamma\ne0$ . The monotonicity theorem uses $\gamma>0$ and nonnegative scenario weights.

This draft is a finite actuarial risk-valuation precursor. The literature includes further results, such as comparisons with expected value, convexity and recursion of risk measures. They are not declared proved by this mission. Neither a successfully elaborated Lean statement nor an independent arithmetic test constitutes an accepted Lean proof.

References

[1] Tsanakas, Andreas and Desli, Evangelia (2003), “Risk measures and theories of choice”, British Actuarial Journal, 9(4), pp. 959–991. Discusses exponential premium calculation, expected utility and the monetary properties and limitations of different risk measures. Open academic record.

[2] Bäuerle, Nicole and Glauner, Alexander (2021), “Minimizing spectral risk measures applied to Markov decision processes”, Mathematical Methods of Operations Research. Introduces the entropic certainty equivalent as $\gamma^{-1}\log\mathbb E[e^{\gamma X}]$ when discussing risk-sensitive decision processes.

[3] Bäuerle, Nicole and Glauner, Alexander (2022), “Markov decision processes with recursive risk measures”, European Journal of Operational Research, 296(3), pp. 953–966. Develops recursive risk-sensitive Bellman equations and optimal Markov policies under suitable assumptions; the present mission only proves the simpler one-period finite-scenario predecessor.

19 thms2 active usersReviewed

Completed

Actuarial Science Probability·Captain: WillR

Actuarial Mathematics XIX: Finite-Horizon Reserve Loss and Hattendorff Innovation BridgeTextbook

Motivation and connection to discrete Hattendorff's theorem

A prospective insurance reserve is an actuarial estimate of future net obligations conditional on the policy being in force. A realised claim can differ from this estimate because death may occur earlier or later than expected. For a fully discrete life insurance contract, Hattendorff's theorem allocates the variance of the insurer's loss to individual policy years. A decisive preliminary identity is that the realised insurer loss at issue, after subtracting the opening reserve, equals a sum of discounted net amounts at risk multiplied by centred mortality innovations.

Shiu and Xiong [1] express loss at issue in their equation (1), derive a one-year reserve finite-difference identity in equation (3), and sum the resulting reserve changes in equations (4)–(5). This mission makes the corresponding finite-horizon, pathwise reserve-loss identity precise, including a terminal prospective reserve for policies still in force when the chosen horizon ends. It is the cashflow side of the finite-scenario innovation analysis proposed in Mission XVI.

The central distinction is important: the mission proves a deterministic identity for each possible curtate death year, provided the annual conditional rates and reserve recurrence are consistent. It does not itself construct the mortality probability distribution, derive conditional rates from a measure, prove annual orthogonality, or establish the final variance formula. Those tasks belong to the probabilistic components in XVI and their eventual integration.

Contract timing and cashflow variables

Let $K\in\mathbb N$ denote curtate future lifetime. The event $K=t$ means the insured dies during policy year $t$ , with the associated benefit paid at time $t+1$ . Define the real-valued indicators

S_t(K)=\mathbf1_{\{K\ge t\}}, \qquad D_t(K)=\mathbf1_{\{K=t\}}.

These satisfy the disjoint partition

S_t(K)=D_t(K)+S_{t+1}(K).

Let $n\in\mathbb N$ be the finite valuation horizon, $v\in\mathbb R$ a per-year discount factor, $\pi_t$ the premium at the start of policy year $t$ , $b_{t+1}$ the death benefit at its end, and $V_t$ the prospective reserve at time $t$ on the in-force basis.

The finite-horizon net insurer loss, including the reserve required at the horizon for a policy still in force, is

\boxed{ L_n(K)= \sum_{0\le t<n}\! \left[v^{t+1}b_{t+1}D_t(K) -v^t\pi_t S_t(K)\right] +v^nV_nS_n(K). }

The first term values year-end death benefits, the second subtracts premiums paid at the beginning of each covered year only while the policy remains in force, and the third carries forward the continuing liability.

For $n=0$ no premium or death benefit is included and $L_0(K)=V_0$ . If $K\ge n$ , the insurer has not paid a death benefit during the chosen horizon, and the value includes $v^nV_n$ . Therefore the mission does not assume that everyone dies before the selected horizon, nor does it discard an outstanding terminal liability.

One-year reserve recurrence

Let $q_t$ denote the conditional probability of death during policy year $t$ , given the policy is still in force at its start, and let $p_t$ denote conditional survival through that year. Their one-year normalisation is

p_t+q_t=1.

Let the annual prospective reserve balance be

\boxed{ V_t+\pi_t =v\left(p_tV_{t+1}+q_tb_{t+1}\right). }

This is the discrete one-year recurrence appearing in [1, equation (3)] before multiplication by $v^t$ and rearrangement. The source has an annual premium paid at the beginning and a death benefit at the end. The rates $p_t,q_t$ , benefit $b_{t+1}$ , premium $\pi_t$ and reserve sequence $V_t$ are inputs to the formal statement. Their actuarial origin is not silently assumed.

The formalisation deliberately permits arbitrary real quantities for the algebra. The usual probability interpretation additionally requires $0\le p_t,q_t\le1$ , and the conventional financial interpretation requires a valid positive discount factor. These stronger conditions are not needed for the pathwise identity itself once the two recurrence equalities are assumed.

Net amount at risk and annual mortality surprise

The year- $t$ realised mortality surprise is

I_t(K)=D_t(K)-q_tS_t(K).

This equals $1-q_t$ on death in year $t$ , $-q_t$ when the insured survives through year $t$ , and zero after the policy has ended. It is a pointwise cashflow expression here; statistical centring requires a later assumption that the supplied $q_t$ is the correct conditional death probability.

Define the discounted net amount at risk and its annual contribution:

\rho_t=v^{t+1}(b_{t+1}-V_{t+1}), \qquad \rho_tI_t(K).

The finite innovation value is

Z_n(K)=\sum_{0\le t<n}\rho_tI_t(K).

Unlike the more general mortality innovation mission, this draft explicitly connects the coefficient $\rho_t$ to the death benefit and prospective reserve rather than treating it as an arbitrary monetary sequence.

One-year cancellation and the finite-horizon theorem

To see the mechanism, consider the change in the reserve-adjusted insurer loss when the horizon increases from $t$ to $t+1$ :

\begin{aligned} L_{t+1}(K)-L_t(K) ={}&v^{t+1}b_{t+1}D_t(K) -v^t\pi_tS_t(K)\\ &+v^{t+1}V_{t+1}S_{t+1}(K) -v^tV_tS_t(K). \end{aligned}

Substituting $S_{t+1}=S_t-D_t$ , the one-year reserve balance, and $p_t+q_t=1$ reduces that entire expression to

\boxed{ L_{t+1}(K)-L_t(K) =v^{t+1}(b_{t+1}-V_{t+1}) \left(D_t(K)-q_tS_t(K)\right). }

Sum this identity from $t=0$ to $n-1$ . All intermediate reserve balances cancel, leaving the capstone:

\boxed{ L_n(K)-V_0 =\sum_{0\le t<n} v^{t+1}(b_{t+1}-V_{t+1})I_t(K) =Z_n(K). }

This equality holds for every $K$ and finite $n$ provided the year-by-year normalisation and reserve balance hold on the relevant years. It includes $n=0$ without a special artificial convention and it retains the terminal liability already included in $L_n$ . Neither $V_0=0$ nor $V_n=0$ is required.

When later coupled to a genuine mortality distribution and the statistical identities in Mission XVI, the representation provides the missing bridge for a finite-horizon discrete Hattendorff variance theorem. Such a coupling must explicitly reconcile the probability model, its conditional rates, and the definition of weighted variance. No published theorem is treated as a proved dependency merely because it has appeared as an Open Prove2Me target.

Formal proof graph and publication safeguards

Six definitions introduce the in-force and death-year indicators, the realised finite loss with terminal reserve, an annual reserve balance predicate, a centred mortality surprise and the discounted net-at-risk innovation sum. Twelve supporting theorems establish time-zero and after-death indicators, the disjoint event partition, the zero-horizon loss and innovation, realised death/survival shock cases, finite-sum successor identities and the pivotal one-year reserve-adjusted loss identity. The capstone proves the finite pathwise equality for every curtate death year under annual assumptions for all years $t<n$ .

All source declarations use correct leading Lean imports. Every local definition import is required by the declaration it uses; the dependency graph must remain acyclic. Preliminary private remote elaboration checks only statement syntax and types. It is not an accepted Lean proof, nor does it show that not-yet-published definition modules are individually importable.

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), (4) and (5). In particular, their one-year reserve recurrence and summation-by-parts argument motivate the loss-to-innovation representation.

[2] Gerber, Hans U. (1997), Life Insurance Mathematics, third edition, Springer, Chapter 6, §6.7, allocation of the overall life-insurance loss to individual policy years.

[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. Supports the indicator-based perspective and the relationship between mortality surprises and annual loss allocation.

19 thms2 active usersReviewed

Completed

Actuarial Science Probability·Captain: WillR

Actuarial Mathematics XV: Finite-Action Excess-of-Loss Reinsurance and Bellman ValuationTextbook

Motivation and research scope

An insurer can transfer part of an unusually large claim to a reinsurer using an excess-of-loss contract. The insurer chooses a retention amount and remains liable for each claim only up to that amount, while the reinsurer covers the excess. A retention strategy trades off the cost of reinsurance protection against the amount of insurance loss retained.

Brachetta and Ceci (2019) investigate optimal excess-of-loss retention under a stochastic environment which affects claim frequency, claim severity and reinsurance premiums [1]. Their actual results use a marked point process, an exogenous diffusion factor, terminal exponential utility, a Hamilton–Jacobi–Bellman equation and a continuous-time verification theorem. This mission is not a purported proof of that stochastic HJB result.

Instead, it creates a rigorous finite-scenario, finite-action precursor: exact excess-of-loss claim sharing, weighted retained-claim valuation and the Bellman optimisation operator for a finite collection of actions. The direct source for discrete finite-horizon optimality is Puterman, Markov Decision Processes, Chapter 4 [2], which develops dynamic programming and the existence of deterministic optimal actions. A genuine stochastic reinsurance-control model can later replace the discrete scenario assumptions, construct the controlled wealth process and address the full HJB theorem of [1].

Excess-of-loss retention and ceded claims

Let $z\in\mathbb R$ be a gross claim amount and $a\in\mathbb R$ be the retention threshold. The insured-life/non-life interpretation requires $z\ge0$ and $a\ge0$ , but the Lean functions themselves are defined algebraically on all real numbers.

The insurer retains

r(z,a)=\min(z,a)

and cedes to the reinsurer

c(z,a)=z-\min(z,a).

Consequently the claim is allocated without double counting:

r(z,a)+c(z,a)=z.

The supporting theorems show that retained loss cannot exceed either the original claim or the retention limit, that ceded loss is nonnegative, and that raising the retention threshold cannot reduce the retained loss. For nonnegative claims, setting $a=0$ leaves no retained loss. If $z\le a$ , no excess is ceded.

The division of claim amounts follows the surplus decomposition in Brachetta and Ceci [1, §2], where the retained claim is expressed by the minimum of the claim size and the control.

Finite-scenario expected retained loss and cost

Let $\Omega$ be a finite set of claim scenarios. For scenario $\omega$ , let $z_\omega$ be the gross claim and $w_\omega$ a probability weight. Probability interpretation requires

w_\omega\ge0,\qquad \sum_{\omega\in\Omega}w_\omega=1.

The expected retained claim amount for retention $a$ is

\mathbb E_w[r(Z,a)] =\sum_{\omega\in\Omega}w_\omega\min(z_\omega,a).

Let $q(a)$ be the reinsurance premium charged for that retention. The one-period expected insurance and reinsurance cost is

C(a)=q(a)+\mathbb E_w[r(Z,a)].

This simple expected-cost criterion captures the basic trade-off: a lower retention reduces claims retained, generally at the cost of a higher reinsurance premium. The theorem definitions impose no monotonicity on the premium function $q$ ; if actuarial monotonicity is required, it must be included as a separate hypothesis.

The finite expected-loss function is nonnegative under nonnegative scenarios, retentions and weights. It is increasing in retention when the weights are nonnegative. These are algebraic checks, not a claim that minimising this expected cost is equivalent to maximising exponential terminal utility in [1]. The source article uses the latter, more sophisticated objective.

Discrete optimal decisions and Bellman operator

To prepare for multi-year optimal reinsurance, let $S$ be a finite state space, $A$ a nonempty finite admissible action set, and $P(s,a,t)$ the one-step transition weight from state $s$ to $t$ when action $a$ is selected. Let $r(s,a)$ be the one-period reward, $v$ a deterministic discount factor and $N(t)$ a next-period value.

The return associated with one action is

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

The finite-action Bellman operator is

(TN)(s)=\max_{a\in A}Q(s,a).

Since $A$ is nonempty and finite, the maximum is attained. The capstone formally targets

\begin{aligned} Q(s,a)&\le(TN)(s)\quad\text{for every }a\in A,\\ (TN)(s)&=Q(s,a^\star) \quad\text{for some }a^\star\in A. \end{aligned}

This is the finite-horizon principle of selecting an optimal discrete action, not continuous-time HJB verification. Puterman [2, Chapter 4] discusses the Bellman recursion and the existence of deterministic Markov policies for finite-horizon decision problems. To model reinsurance with this operator, later theorems must specialise $A$ to admissible retention limits, define state-dependent premium and claim distributions, and prove row-stochasticity and any desired utility assumptions.

The draft intentionally does not claim that arbitrary matrix entries $P$ define a valid probability law. The finite Bellman maximum and the two capstone inequalities are algebraically meaningful for arbitrary real weights; a controlled Markov-process interpretation requires additional conditions.

Formal definitions and proof structure

Five definitions introduce gross claim retention, ceded claim, finite weighted retained loss, one-year reinsurance cost and the finite-action Bellman operator. Twelve supporting theorems cover the claim split, nonnegative and monotone retention results, expected retained-loss monotonicity, stage cost and Bellman lower bounds. The capstone packages upper domination and attainment of the Bellman maximum.

All local imports appear before other Lean commands. Every theorem is currently a proposed proof obligation; the source-elaboration checks are private and do not constitute accepted proofs. Definitions that are not yet published cannot be assumed importable in the production theorem preview.

This is a foundations mission for a later reinsurance-control programme. A credible subsequent research mission will need the full conditional marked-point-process model, wealth dynamics, admissible adapted controls, exponential utility and the analytic regularity assumptions of [1] before attempting its backward-PDE verification result.

References

[1] Brachetta, Matteo and Ceci, Claudia (2019), “Optimal Excess-of-Loss Reinsurance for Stochastic Factor Risk Models”, Risks, 7(2), article 48. The claim process and retention control are in §2, the HJB formulation in §3, optimal strategies in §4 and the verification argument in §5. This article motivates the reinsurance problem but its continuous-time verification theorem is outside the present draft.

[2] Puterman, Martin L. (1994), Markov Decision Processes: Discrete Stochastic Dynamic Programming, Chapter 4, “Finite-Horizon Markov Decision Processes”, Wiley, pp. 74–118. Includes finite-horizon policy evaluation, optimality equations, deterministic Markov policies and backward induction. This is the direct source for the discrete Bellman stage.

[3] Brachetta and Ceci (2019), open preprint, arXiv:1904.05422. Independent accessible source for the original stochastic-factor control problem and its distinct continuous-time assumptions.

18 thms2 active usersReviewed

All missions

Bypassing the Monster: A Faster and Simpler Optimal Algorithm for Contextual Bandits Under Realizability: FALCON+ Has Regret ≤ 14.3·Σₘ√(K𝓔(τₘ₋₁−τₘ₋₂))(τₘ−τₘ₋₁) + τ₁ + √(8T log(2/δ)) w.p. 1−δResearch Paper

Contextual bandits and the reduction to regression

Setting

Formalization targets

Goal: Theorem 2 in explicit form

Milestones

Significance

Difficulty

Formalization scope

Selected references

Understanding the Acceleration Phenomenon via High-Resolution Differential Equations V: Along the High-Resolution ODE of NAG-C, inf ‖∇f(X(u))‖² ≤ (12 + 9sL)‖x₀ − x⋆‖²/(2√s(t³ − t₀³))Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 5 (p. 21)

Milestones (pp. 22–23)

Significance

Difficulty

Formalization scope

Selected references

The Running Intersection Relaxation of the Multilinear Polytope 2: If a Hypergraph Is Not β-Acyclic, Its Multilinear Polytope Is Strictly Contained in the Running Intersection RelaxationResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 5

Significance

Difficulty

Formalization scope

Selected references

The Running Intersection Relaxation of the Multilinear Polytope 1: For Kite-Free β-Acyclic Hypergraphs the Running Intersection Relaxation Equals the Multilinear PolytopeResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3 (p. 1023)

Milestones

Companions

Significance

Difficulty

Formalization scope

Selected references

Douglas-Rachford Splitting and ADMM for Nonconvex Optimization: Tight Convergence Results I: Under the Tight Stepsize Bound, the Nonconvex DRS Residual Vanishes and Cluster Points Are StationaryResearch Paper

Why nonconvex Douglas–Rachford splitting

Setting

Formalization targets

Goal: Theorem 4.3 (subsequential convergence)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Propagation of Chaos for Stochastic Spatially Structured Neuronal Networks with Delay driven by Jump Diffusions 2: The Neuronal Network Converges in L² to Its McKean–Vlasov LimitResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1.8

Milestones

Significance

Difficulty

Formalization scope

Selected references

Sub/Super-Stochastic Matrix with Applications to Bipartite Tracking Control over Signed Networks 3: ψ < 1/(τd_M), Structural Balance and Leader Reachability Give Asynchronous Bipartite TrackingResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.3, sufficiency

Milestones

Significance

Difficulty

Formalization scope

Selected references

Liouville Quantum Gravity and the Brownian Map II: Geodesics and Continuity of the Embedding: A Quantitative Kolmogorov–Čentsov Criterion, P[M ≥ t] ≤ c₁t^(−α) for the Hölder Norm MResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 2.3 (p. 30)

Milestones (attack order)

Significance

Difficulty

Formalization scope