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.

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.

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.

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.

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.

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.

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.

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.

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.

Motivation and actuarial context

A prospective life insurance reserve describes the expected remaining loss on a policy at a valuation date. An alternative way to understand the insurer's total future loss is to allocate it between individual policy years. Each year produces an insurance cashflow and a change in the reserve needed to support future benefits. When properly centred by the reserve balance, the resulting annual gains have expectation zero. Hattendorff's theorem connects this allocation to the striking result that losses for distinct years are uncorrelated and the variance of total discounted loss is the sum of their individual discounted variances.

The classical finite annual result is covered by Gerber, Life Insurance Mathematics, third edition, §6.7, particularly equations (6.7.3) and (6.7.6)–(6.7.10) [1]. A modern actuarial derivation is developed in the European Actuarial Journal article An elementary derivation of Hattendorff's theorem [2]. The connection to martingale increments is emphasised by Norberg [3] and by Gerber, Leung and Shiu [4].

This mission formalises a finite-scenario annual-loss allocation and Hattendorff-style variance identity. It makes the distinction between a proved algebraic decomposition and the deeper stochastic theorem explicit: annual orthogonality is a hypothesis of the capstone, with its derivation from conditional mortality and reserve dynamics reserved for a subsequent extension. Thus the mission does not claim that an arbitrary pair of yearly cashflows is uncorrelated.

Finite mortality scenarios and expected values

Let $\Omega$ be a finite sample space, and let $w_\omega$ denote the probability assigned to scenario $\omega$. A valid scenario probability law has nonnegative weights summing to one. The mission defines the finite weighted expectation

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

Its supporting results establish expected values of constants and linear combinations. For scenario cashflows $X$ and $Y$, weighted variance and covariance are defined by

$$\begin{aligned} \operatorname{Var}_w(X) &=\sum_\omega w_\omega \left(X(\omega)-\mathbb E_w[X]\right)^2,\\ \operatorname{Cov}_w(X,Y) &=\sum_\omega w_\omega \left(X(\omega)-\mathbb E_w[X]\right) \left(Y(\omega)-\mathbb E_w[Y]\right). \end{aligned}$$

The definitions work for arbitrary real arrays of weights, while the actuarial probability interpretation assumes valid scenario probabilities. Finite sums avoid moment-integrability issues without imposing an artificial condition such as independence between years.

Annual insurer gains and reserve changes

Let $C_k(\omega)$ be the net insurer cash outgo during policy year $k$, measured at that year's start, and let $R_k$ be the deterministic opening prospective reserve under a given in-force valuation basis. With per-year discount factor $v$, define the annual gain or loss component

$$G_k(\omega)=C_k(\omega)+vR_{k+1}-R_k.$$

The term $vR_{k+1}$ represents the discounted liability carried into the next year, while $R_k$ is the reserve released from the opening position. The sign convention is insurer loss, so positive values represent net outgo or an adverse change.

If the annual reserve balance is

$$\mathbb E_w[C_k]+vR_{k+1}=R_k,$$

then linearity gives

$$\mathbb E_w[G_k]=0.$$

This is the first actuarial component of Hattendorff's framework: properly reserved annual losses are centred under the valuation basis. The finite scenario weights need to sum to one, and the reserve balance must be assumed or established. Merely defining $G_k$ does not give it zero mean.

Discounted loss allocation and telescoping

The total discounted annual gain through $n$ years is

$$L_n(\omega)=\sum_{0\le k<n}v^kG_k(\omega).$$

Expanding the annual gain definition and telescoping the reserve terms gives the pathwise identity

$$\boxed{ L_n(\omega)= \sum_{0\le k<n}v^k C_k(\omega) +v^n R_n-R_0. }$$

The terminal reserve is retained explicitly. It must not be assumed zero for an arbitrary incomplete policy horizon. This exact finite-period formula corresponds to the annual allocation of loss and reserve changes discussed in [1, §6.7, equation (6.7.3)], with the horizon and terminal liability clearly stated.

The empty-term case has $L_0=0$. Increasing the horizon from $n$ to $n+1$ adds precisely $v^nG_n$. These boundary and recursion lemmas form a useful independent verification layer for the finite sum.

Orthogonality and the variance decomposition

When distinct annual gains have zero covariance,

$$\operatorname{Cov}_w(G_i,G_j)=0 \qquad (i\ne j,\;i,j<n),$$

their discounted aggregate variance has no cross-year terms:

$$\boxed{ \operatorname{Var}_w(L_n) =\sum_{0\le k<n}v^{2k}\operatorname{Var}_w(G_k). }$$

Importantly, uncorrelated does not mean independent. Annual losses are linked by the same insured life, survival history and reserve process. Hattendorff's theorem establishes the required uncorrelatedness from the correct conditional insurance model; the zero-covariance condition is an explicit hypothesis in this mission's finite-scenario algebraic capstone. This distinction is important for the formalisation and is consistent with [1, equations (6.7.6)–(6.7.8)] and the martingale explanation in [3–4].

The supporting theorem on variance of a sum, variance scaling and covariance symmetry makes the algebra behind the annual allocation explicit. Zero-mean gain and zero-covariance assumptions must be separately justified when moving from this finite abstract setting to a particular mortality model.

Capstone and subsequent formal development

The capstone assumes a finite scenario law whose weights sum to one, a sequence of yearly cashflows $C_k$, deterministic reserves $R_k$, a reserve balance for each year $k<n$, and pairwise zero covariance of the resulting annual gains. It then proves three statements together: each year's gain is centred, the discounted variance splits additively by year, and the discounted sum telescopes to net cashflows plus the terminal reserve less opening reserve.

Five definitions establish weighted expectation, annual reserve gain, discounted aggregate gain, variance and covariance. Thirteen supporting theorem targets handle elementary expectation algebra, finite-year telescoping, zero-mean reserve gains, covariance symmetry and orthogonal variance decomposition. A capstone combines these results.

This is explicitly the finite algebraic and reserve-accounting stage, not a complete proof of Hattendorff's theorem for arbitrary life insurance contracts. A later mission should construct the curtate-lifetime annual innovations using the published reserve recursions of Mission XI, establish the conditional mean-zero property from survival information and derive cross-year orthogonality without assuming it. Only that later bridge will discharge the substantive stochastic obligation. No independence claim is made.

Every item is a proposed Lean statement. The isolated-module imports appear before other Lean commands, and no unpublished definition is treated as already available to the live compiler.

References

[1] Gerber, Hans U. (1997), Life Insurance Mathematics, third edition, Springer, Chapter 6, §6.7, Allocation of the Overall Loss to Policy Years, equations (6.7.3)–(6.7.10). Publisher book record.

[2] An elementary derivation of Hattendorff's theorem, European Actuarial Journal (2021), DOI: 10.1007/s13385-020-00256-9. Develops the annual insurer-loss formula using the prospective reserve recurrence.

[3] Norberg, Ragnar (1992), “Hattendorff's theorem and Thiele's differential equation generalized”, Scandinavian Actuarial Journal, pp. 2–14. Places the annual uncorrelated-loss principle in a broader stochastic and martingale setting.

[4] 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. Relates the actuarial theorem to uncorrelated martingale increments.

Motivation and actuarial context

A traditional life-insurance model may have one way of exiting the insured state, namely death. Many actuarial contracts instead allow multiple mutually exclusive decrements. A policyholder might exit through death, disability, withdrawal or retirement, and different causes may trigger different benefits. A net premium reserve must therefore allow one-year payments that vary by the cause of exit, as well as the liability continuing for policies that do not exit.

Gerber, Life Insurance Mathematics, third edition, Chapter 7 §7.5 [1], derives the multiple-decrement reserve and its one-year recursion, followed by a decomposition of premium into reserve accumulation and the expected cost of the net amounts at risk. The same models are related to the broader multiple-state framework developed in Dickson, Hardy and Waters (2009), Chapter 8, including §8.8 on multiple decrements [2].

This mission formalises the one-year multiple-decrement reserve balance and premium decomposition for a finite set of causes. It is a deliberately local actuarial model: it handles one policy year and deterministic opening and closing reserves, without assuming that the complete lifetime-dependent reserve functions from Missions XI or XII have already been published.

One-year decrement law

Let $J$ be a finite set of mutually exclusive causes of exit. Fix a policy in force at the start of the year. Let $p$ denote the conditional probability of surviving in force to the following year, and $q_j$ the conditional probability of decrement cause $j\in J$ during the year.

The one-year decrement law is valid when

$$p\ge0,\qquad q_j\ge0,\qquad p+\sum_{j\in J}q_j=1.$$

The possible decrement causes are alternative outcomes of the same year. Their probabilities are added because the causes are mutually exclusive; they are not independent risks. The survival probability refers to remaining in force, rather than necessarily being alive in every possible post-decrement state.

The formal model treats $J$ as any finite type. No nonempty-type hypothesis is required: if $J$ is empty, the unit-probability law forces $p=1$ and reduces to certain survival, without exit benefits.

Benefit payments and the annual reserve balance

Let $b_j$ be the benefit payable at the end of the year following exit for cause $j$. The conditional expected exit benefit before discounting is

$$B=\sum_{j\in J}q_jb_j.$$

Let $R$ be the reserve immediately before the current premium, let $R_+$ denote the reserve required at the next annual valuation for surviving policies, and let $v$ be the annual discount factor. Assume the year-end reserve for policies which exit is zero after payment of the cause-specific benefit. Under this timing, the expected present value of the following-year liability is

$$v\left(pR_+ +\sum_{j\in J}q_jb_j\right).$$

The required premium $\Pi$ is defined by the annual reserve balance

$$\boxed{R+\Pi=v\left(pR_+ +\sum_{j\in J}q_jb_j\right).}$$

Equivalently, the formula defines

$$\Pi=v\left(pR_++B\right)-R.$$

This is the discrete conditional one-year multiple-decrement generalisation of the annual life-reserve recursion in [1, equation (7.5.2)]. It does not assert that the reserves $R$ and $R_+$ were derived from a complete prospective valuation, nor that an arbitrary premium chosen externally automatically satisfies the balance. Those tasks require a separate multi-year model.

Savings and risk premium components

The one-year required premium can be separated into two economically interpretable parts. The savings premium grows the opening reserve towards the next reserve:

$$\Pi^{\mathrm{sav}}=vR_+-R.$$

The risk premium finances benefits above or below the amount of reserve that would otherwise remain at the next annual valuation:

$$\Pi^{\mathrm{risk}}= v\sum_{j\in J}q_j(b_j-R_+).$$

Since the decrement law satisfies $\sum_jq_j=1-p$,

$$\begin{aligned} \Pi^{\mathrm{sav}}+\Pi^{\mathrm{risk}} &=vR_+-R+ v\sum_jq_j(b_j-R_+)\\ &=v\left(pR_++\sum_jq_jb_j\right)-R\\ &=\Pi. \end{aligned}$$

Thus the principal premium decomposition is

$$\boxed{\Pi=\Pi^{\mathrm{sav}}+\Pi^{\mathrm{risk}}.}$$

This follows the savings and risk-premium interpretation of [1, equations (7.5.3)–(7.5.5)]. A negative risk premium is possible algebraically when cause benefits are lower than the continuing reserve. The formal theorem does not assume all monetary amounts are nonnegative.

Boundary cases and formal theorem graph

If $p=0$, every in-force policy exits during the year, and the continuing reserve term vanishes:

$$\Pi=vB-R.$$

If no decrement can occur, $p=1$ and $q_j=0$ for every cause, the required premium reduces to the savings component alone,

$$\Pi=\Pi^{\mathrm{sav}}=vR_+-R.$$

If every cause of exit pays exactly the same amount as the following-year reserve, $b_j=R_+$, the risk component is zero. Scaling all monetary benefits and reserve amounts by a common factor scales the premium by that factor.

The draft introduces five definitions: a valid annual decrement law, expected cause benefit, required annual premium, savings premium and risk premium. Eleven supporting theorems establish probability conditions, zero and scaled benefits, reserve balance, zero-survival and no-decrement limits, risk-free exits and the premium decomposition. The capstone combines the one-year reserve balance with the savings/risk identity.

The definitions and theorem types are independent of unconfirmed Prove2Me actuarial declarations from earlier missions. Imports of local definitions are explicitly placed at the beginning of each Lean file, and the proposed statements do not treat a Draft declaration as a published theorem. The proofs of the individual statements remain to be supplied after captain and moderator review.

References

[1] Gerber, Hans U. (1997), Life Insurance Mathematics, third edition, Springer, Chapter 7, Multiple Decrements, §7.5, The Net Premium Reserve, equations (7.5.1)–(7.5.5). In particular (7.5.2) is the annual multiple-decrement recursion and (7.5.3)–(7.5.5) separate the savings and risk portions.

[2] Dickson, David C. M., Hardy, Mary R. and Waters, Howard R. (2009), Actuarial Mathematics for Life Contingent Risks, first edition, Chapter 8, Cambridge University Press, §8.8, Multiple Decrement Models.

[3] Dickson, Hardy and Waters (2009), Chapter 7, Policy Values, annual policy-value recursions. The one-cause formula provides the earlier special case from which the multiple-cause generalisation develops.

Motivation

A chance-constrained program minimizes a cost $f(x)$ over a closed set $X\subseteq\mathbb R^n$ subject to a constraint that must hold with high probability rather than surely:

$$\min_{x\in X} f(x)\quad\text{s.t.}\quad \mathbb P\bigl(C(x,\xi)\le 0\bigr)\ge 1-\alpha,$$

where $\xi$ is a random vector, $C(x,\xi)=\max_j c_j(x,\xi)$ collects the uncertain constraints, and $\alpha\in(0,1)$ is the tolerated risk. Such models are used in power-system dispatch, portfolio selection, and supply-chain and process design, wherever a constraint may be violated in rare scenarios at a controlled rate.

The probability is rarely computable, so in practice it is replaced by an estimate from an i.i.d. sample $\xi_1,\dots,\xi_N$. The empirical frequency is a step function of $x$ and yields a mixed-integer program. Peña-Ordieres, Luedtke and Wächter (arXiv:1905.07377v2; SIAM J. Optim. 30(3), 2020) replace the indicator by a smooth approximation, which turns the sample problem into a smooth nonlinear program that standard solvers can handle. The question this mission addresses is whether a point accepted by the smoothed sample problem is actually feasible for the true chance constraint, and with what probability.

Timeline. Luedtke and Ahmed (SIAM J. Optim. 19 (2008)) proved finite-sample feasibility guarantees for the empirical (non-smooth) sample approximation, first for finite $X$ and then, under a Lipschitz condition on $C$, for bounded $X$ (their Theorem 10). Peña-Ordieres, Luedtke and Wächter (2020) extended these guarantees to the smoothed approximation (Theorems 3.8, 3.11 and 3.13 of the preprint).

Setting

Let $\varepsilon>0$ and let $\gamma_\varepsilon:[-\varepsilon,\varepsilon]\to[0,1]$ be admissible: strictly decreasing, symmetric in the sense $\gamma_\varepsilon(-y)=1-\gamma_\varepsilon(y)$, and such that the smoothed indicator

$$\Gamma_\varepsilon(y)=\begin{cases}1& y\le-\varepsilon\\ \gamma_\varepsilon(y)&-\varepsilon<y<\varepsilon\\ 0& y\ge\varepsilon\end{cases}$$

is differentiable on $\mathbb R$. The paper's concrete choice is a quartic-kernel polynomial (its (2.6)).

For a decision $x$ and a level $t$, define

• the true cdf $F(t;x)=\mathbb P(C(x,\xi)\le t)$;
• the smoothed cdf $F_\varepsilon(t;x)=\int\Gamma_\varepsilon(C(x,\xi)-t)\,d\mathbb P_\xi$;
• the smoothed sample cdf $F^N_\varepsilon(t;x)=\frac1N\sum_{i=1}^N\Gamma_\varepsilon(C(x,\xi_i)-t)$.

The true feasible set is $X_\alpha=\{x\in X\mid F(0;x)\ge1-\alpha\}$, and the shifted sample feasible set with shift $t$ and sample risk level $\delta$ is

$$X^{N,t}_{\varepsilon,\delta}=\{x\in X\mid F^N_\varepsilon(-t;x)\ge 1-\delta\}.$$

Throughout, $C(x,\xi)$ has a continuous distribution for each $x\in X$ (Assumption 3.1). The margin of a point is $M_x=F(0;x)-F_\varepsilon(-t;x)+(\alpha-\delta)$; Assumption 3.7 asks that $\delta\in[0,\alpha]$ and $M:=\inf_{x\in X}M_x>0$.

Formalization targets

Goal: Theorem 3.13

Suppose $X$ is bounded with sup-norm diameter $D$, that $|C(x,\xi)-C(y,\xi)|\le L\|x-y\|_\infty$ for all $x,y\in X$ with probability one (Assumption 3.12), and that Assumption 3.7 holds with $t>0$ and $\delta>0$. Then for every $\beta\in(0,\delta]$,

$$\mathbb P\bigl(X^{N,2t}_{\varepsilon,(\delta-\beta)}\subseteq X_\alpha\bigr)\ge 1-\lceil1/\beta\rceil\,\lceil 2LD/t\rceil^n\exp\{-2NM^2\}.$$

Milestones

1. Theorem 3.8. For $x\in X\setminus X_\alpha$, $\ \mathbb P(F^N_\varepsilon(-t;x)\ge1-\delta)\le\exp\{-2NM_x^2\}$.
2. Theorem 3.11. For finite $X$, $\ \mathbb P(X^{N,t}_{\varepsilon,\delta}\subseteq X_\alpha)\ge 1-|X\setminus X_\alpha|\exp\{-2NM^2\}$.
3. The net claim (proof of Theorem 3.13). Each slice $X_j$ of $X$ by the value of $F(0;\cdot)$ at resolution $1/\lceil1/\beta\rceil$ has a finite subset $Z_j$ with $|Z_j|\le\lceil2LD/t\rceil^n$ that is a $t/L$-net of $X_j$ in $\|\cdot\|_\infty$.
4. (3.5). Theorem 3.11 applied to the net $Z$ with levels $\alpha-\beta$ and $\delta-\beta$.
5. The transfer step. $x\in X^{N,2t}_{\varepsilon,(\delta-\beta)}$ and $\|x-z\|_\infty\le t/L$ imply $F^N_\varepsilon(-t;z)\ge1-\delta+\beta$.
6. Corollary 3.9 (companion). If $C(x,\xi)$ has a density strictly decreasing on $(-\varepsilon,\varepsilon)$ and $F(0;x)<1-\alpha$, then $\beta_x=F(0;x)-F_\varepsilon(0;x)>0$ and $\mathbb P(F^N_\varepsilon(0;x)\ge1-\alpha)\le\exp\{-2N\beta_x^2\}$.

Significance

The result. Theorem 3.13 gives an explicit, non-asymptotic sample size $N$ under which every point accepted by the smoothed sample problem (with a small shift $2t$ and a slightly tightened risk level $\delta-\beta$) is feasible for the original chance constraint, uniformly over an infinite decision set. Solving the smooth approximation therefore yields certifiably feasible solutions with a quantified failure probability, the bound depending on the dimension $n$ only through the covering number $\lceil 2LD/t\rceil^n$. Corollary 3.9 adds that, under a monotone density near zero, the unshifted smoothed approximation is conservative.

Formalizing it. The results are proved in the paper; none is formalized anywhere to our knowledge. A formal development would produce a machine-checked one-sided Hoeffding bound for averages of bounded functions of an i.i.d. sample, a union bound over a finite candidate set, and a sup-norm covering lemma, assembled into a uniform feasibility guarantee. These ingredients are reused across the sample-average-approximation literature.

Difficulty

The obvious argument is a union bound over $X$, which fails for infinite $X$: the event $X^{N,2t}_{\varepsilon,(\delta-\beta)}\subseteq X_\alpha$ involves uncountably many points, and is not even obviously measurable. Discretizing $X$ by a sup-norm grid is not enough on its own either: a grid point may be infeasible while nearby points are feasible, and the true cdf $F(0;\cdot)$ need not be continuous in $x$. The paper's device is to discretize simultaneously in $x$ and in the value of $F(0;x)$, which requires covering each level slice separately and then transferring sample feasibility from a point to its representative, at the price of the shift $2t\to t$ and the level change $\delta\to\delta-\beta$. Keeping the constants exactly as printed, with $\lceil1/\beta\rceil$ slices and $\lceil 2LD/t\rceil^n$ points per slice, is part of the task.

Formalization scope

• Decisions are Fin n → ℝ, whose Mathlib norm is the sup norm $\|\cdot\|_\infty$ used in Assumption 3.12 and Theorem 3.13. $X$ is closed (the paper's standing hypothesis).
• $\xi$ takes values in a measurable space $\Xi$ with probability law $\mathbb P_\xi$. The sample is $N\ge1$ measurable maps $\xi_i:\Omega\to\Xi$ on a probability space, mutually independent, each with law $\mathbb P_\xi$. $C(x,\cdot)$ is assumed measurable for $x\in X$ (a disclosed addition: it makes $C(x,\xi)$ a random variable). Assumption 3.1 is encoded as $\mathbb P_\xi(C(x,\xi)=y)=0$ for all $y$.
• Statements of the form "$\mathbb P(A)\ge1-b$" are stated as $\mathbb P(\text{not }A)\le b$ with $\mathbb P$ evaluated as an outer measure; this implies the printed form and assumes no measurability of the event.
• Assumption 3.7's infimum $M$ is a parameter with $M>0$ and $M\le M_x$ on $X$, equivalent to the infimum because the bounds decrease in $M$.
• "Bounded with diameter $D$" is $\|x-y\|_\infty\le D$ on $X$ with $D>0$. Positivity is necessary: for a single infeasible point and $n\ge1$ the printed bound with $D=0$ would read $\mathbb P\ge1$.
• A formalization in which these hypotheses are unsatisfiable, the event is assumed measurable, or $M$ is a junk infimum is ruled out: a sorry-free sanity file exhibits the quartic kernel (2.6) as admissible and a one-point instance meeting the goal's diameter and margin hypotheses.
• Not posed: Hoeffding's inequality (Theorem 3.6), whose one-sided form is in Mathlib (ProbabilityTheory.measure_sum_ge_le_of_iIndepFun with hasSubgaussianMGF_of_mem_Icc_of_integral_eq_zero); and Corollary 3.10, whose printed exponent does not follow from its proof.

Contributions welcome: proofs of any milestone, in particular the sup-norm covering lemma and the Hoeffding step, which are reusable beyond this mission.

Selected references

• A. Peña-Ordieres, J. R. Luedtke, A. Wächter, Solving chance-constrained problems via a smooth sample-based nonlinear approximation, SIAM J. Optim. 30(3), 2020; preprint arXiv:1905.07377v2. https://arxiv.org/abs/1905.07377 , https://doi.org/10.1137/19M1261985
• J. Luedtke, S. Ahmed, A sample approximation approach for optimization with probabilistic constraints, SIAM J. Optim. 19(2), 2008. https://doi.org/10.1137/070702928
• W. Hoeffding, Probability inequalities for sums of bounded random variables, J. Amer. Statist. Assoc. 58, 1963. https://doi.org/10.1080/01621459.1963.10500830