Motivation

Value-at-Risk (VaR) is the regulatory risk measure for banking and insurance capital: it is the quantile of a loss distribution at a fixed tail probability. Two questions arise when several agents use it. First, risk sharing: if an aggregate loss $X$ is split among agents $i=1,\dots,n$, each measuring its share with its own risk measure, what is the smallest total risk the group can achieve and which split achieves it? Second, model uncertainty: an agent rarely knows the distribution of a loss exactly, and a common response is to evaluate the worst case over all distributions close to an estimate, here in the sense of the Wasserstein distance used in distributionally robust optimization (Esfahani and Kuhn, 2018).

F. Liu, T. Mao, R. Wang and L. Wei, Inf-Convolution, Optimal Allocations, and Model Uncertainty for Tail Risk Measures (Mathematics of Operations Research, 2022; the version used here is the authors' SSRN copy 3490348 of January 16, 2022, ssrn.com/abstract=3490348), combine the two questions. When each agent uses a Wasserstein-robust VaR and the split must be comonotonic (every share increases with the total, the usual requirement in insurance), their Theorem 6 gives the optimal total risk in closed form and shows that one agent should carry the entire loss.

Setting

Fix an atomless probability space $(\Omega,\mathcal F,\mathbb P)$: every event of positive probability contains an event of strictly smaller positive probability. A random variable $X$ is a loss, with distribution function $F_X(x)=\mathbb P(X\le x)$. The domain is $\mathcal X=L^\infty$, the essentially bounded measurable random variables.

For $\alpha\in(0,1)$ the left and right Value-at-Risk are

$$\mathrm{VaR}^L_\alpha(X)=\inf\{x: F_X(x)\ge1-\alpha\},\qquad \mathrm{VaR}^R_\alpha(X)=\inf\{x: F_X(x)>1-\alpha\},$$

so a small $\alpha$ looks far into the tail of the loss. $\Lambda\in\{L,R\}$ selects one of the two.

The Wasserstein metric of order $k\ge1$ between $X$ and $Y$ with quantile functions $F^{-1}$ and $G^{-1}$ is

$$W_k(X,Y)=\Big(\int_0^1|F^{-1}(x)-G^{-1}(x)|^k\,\mathrm dx\Big)^{1/k},$$

and the robust version of a risk measure $\rho$ at radius $\delta>0$ is

$$[\rho]^k_\delta(X)=\sup\{\rho(Y): Y\in L^\infty,\ W_k(Y,X)\le\delta\}.$$

Two random variables $X,Y$ are comonotonic if $(X(\omega)-X(\omega'))(Y(\omega)-Y(\omega'))\ge0$ for all $\omega,\omega'$ in an event of probability one. The comonotonic allocations of $X$ among $n$ agents are

$$\mathbb A^+_n(X)=\{(X_1,\dots,X_n)\in(L^\infty)^n: X_1+\dots+X_n=X,\ X_i \text{ comonotonic with } X\},$$

and the constrained inf-convolution of $\rho_1,\dots,\rho_n$ is $\boxplus_{i=1}^n\rho_i(X)=\inf\{\sum_i\rho_i(X_i):(X_1,\dots,X_n)\in\mathbb A^+_n(X)\}$. An allocation attaining the infimum is optimal.

Formalization targets

Goal: Theorem 6 (p. 31)

Let $X\in L^\infty$ and $\Lambda\in\{L,R\}$.

(i) If $0<\delta_1\le\dots\le\delta_n$ and $\alpha\in(0,1)$, then

$$\mathop{\boxplus}_{i=1}^n[\mathrm{VaR}^\Lambda_\alpha]^1_{\delta_i}(X)=[\mathrm{VaR}^\Lambda_\alpha]^1_{\delta_1}(X)+\sum_{i=2}^n\frac{\delta_i}{\alpha}.$$

(ii) If $1>\alpha_1\ge\dots\ge\alpha_n>0$ and $\delta>0$, then

$$\mathop{\boxplus}_{i=1}^n[\mathrm{VaR}^\Lambda_{\alpha_i}]^1_{\delta}(X)=[\mathrm{VaR}^\Lambda_{\alpha_1}]^1_{\delta}(X)+\sum_{i=2}^n\frac{\delta}{\alpha_i}.$$

In either case $(X,0,\dots,0)$ is an optimal comonotonic allocation.

Milestones

1. Proposition 4(iii), (34)–(35), p. 30. For $k\ge1$, $\delta>0$, $\alpha\in(0,1)$: $[\mathrm{VaR}^L_\alpha]^k_\delta(X)=[\mathrm{VaR}^R_\alpha]^k_\delta(X)=x$, where $x$ is the unique solution of $\int_0^\alpha(x-\mathrm{VaR}^R_u(X))_+^k\,\mathrm du=\delta^k$, and $[\mathrm{VaR}^R_\alpha]^k_\delta(X)\ge\mathrm{VaR}^R_\alpha(X)+\delta/\alpha^{1/k}$.
2. (40), p. 31. With $V_\delta=[\mathrm{VaR}^L_\alpha]^1_\delta$: $V_\delta(Y)\le0$ if and only if $\int_0^\alpha(-\mathrm{VaR}^L_u(Y))_+\,\mathrm du\ge\delta$.
3. (39), p. 31. For $\delta_1\le\delta_2$: $V_{\delta_1}\boxplus V_{\delta_2}(X)\le V_{\delta_1}(X)+\delta_2/\alpha$, through the allocation $(X+\delta_2/\alpha,\,-\delta_2/\alpha)$.
4. (38), p. 31. For $\delta_1\le\delta_2$: $V_{\delta_1}\boxplus V_{\delta_2}(X)=V_{\delta_1}(X)+\delta_2/\alpha$.
5. (41), p. 33. For $\lambda\ge1$ with $\lambda\alpha<1$: $[\mathrm{VaR}^\Lambda_\alpha]^1_\delta\ge[\mathrm{VaR}^\Lambda_{\lambda\alpha}]^1_{\lambda\delta}$ on $L^\infty$.

Significance

The theorem is one of the few explicit solutions of a risk-sharing problem with model uncertainty and non-convex agents. Without uncertainty, the inf-convolution of VaRs is a VaR at the summed level (Theorem 1 of the same paper), and its optimal allocations split the tail of the loss across agents. Under Wasserstein uncertainty and a comonotonicity constraint the structure changes: the optimum concentrates the whole loss on the agent least sensitive to uncertainty when the levels agree, or least sensitive to risk when the radii agree, and the remaining agents hold only cash. In particular the equal split $(X/n,\dots,X/n)$, optimal for identical convex risk measures, is in general not optimal here. Proposition 4(iii) is independently useful: it computes the worst-case VaR over a one-dimensional Wasserstein ball of any order and shows that left and right VaR coincide after robustification.

The results are proved in the paper. As far as is known, none of them has a machine-checked proof; this mission produces the first formal statements and, eventually, proofs. The quantile-based Wasserstein metric, the robust risk measure and the comonotonic inf-convolution are reusable objects for further work on robust risk measures.

Difficulty

The upper bound is a direct computation with one explicit allocation. The lower bound is the hard part. VaR is not convex, so the duality arguments that solve the inf-convolution of convex risk measures do not apply, and the robust VaR is not a distortion risk measure to which the Expected Shortfall formula of Proposition 4(ii) applies. The paper itself notes (p. 30) that the inf-convolution of robust VaRs over all allocations is hard to compute because VaR lacks convexity, and obtains only two-sided bounds there, which are generally not sharp. The explicit formula of Theorem 6 depends on the comonotonicity constraint, on the order $k=1$, and on the agents sharing either the level or the radius; the paper states it only under these assumptions, and the ordering of the radii or levels is necessary for the identity as written, since it singles out the agent who carries the loss. For Proposition 4(iii), the supremum over the ball is a supremum over distributions, and identifying it with a real number requires realising worst-case distributions as random variables on the given space, which is where atomlessness is used.

Formalization scope

Random variables are functions $\Omega\to\mathbb R$; $L^\infty$ is the set of measurable, almost surely bounded functions, with no quotient. The probability measure is atomless in the splitting sense. The quantile function is $F^{-1}_X(x)=\mathrm{VaR}^L_{1-x}(X)$, and the Wasserstein integral is the interval integral over $[0,1]$; for $X,Y\in L^\infty$ its integrand is bounded and monotone on $(0,1)$, so the integral is the paper's. The supremum in the robust measure ranges over $Y\in L^\infty$ only, as in the paper. It is a real supremum: the set is nonempty since it contains $\rho(X)$, and for VaR its boundedness from above is part of the statement of Proposition 4(iii), so no junk value enters. Allocation constraints $\sum_iX_i=X$ hold pointwise. The constrained inf-convolution is valued in the extended reals. The $n=m+1$ agents are indexed by Fin (m+1), so $n\ge1$; the orderings of the radii and of the levels are hypotheses, since without them the identities fail. Theorem 6 is stated for order $k=1$; Proposition 4(iii) for every real $k\ge1$. The single implicit hypothesis made explicit is $\lambda\alpha<1$ in (41), which keeps the VaR level in $(0,1)$.

A formalization in which the robust supremum ranges over all measurable functions, or over an unbounded set where the real supremum is $0$, would make the identities trivial or false; both are excluded by the definitions above.

The development needs: quantile functions of bounded random variables and their monotonicity; the existence on an atomless space of a random variable with a prescribed quantile function; comonotonic additivity of VaR; and the interval-integral calculus for monotone integrands. Contributions of general lemmas on quantile functions and on one-dimensional Wasserstein distances are welcome and reusable beyond this mission.

Selected references

• F. Liu, T. Mao, R. Wang, L. Wei, Inf-Convolution, Optimal Allocations, and Model Uncertainty for Tail Risk Measures, Mathematics of Operations Research, 2022; SSRN version of January 16, 2022. https://ssrn.com/abstract=3490348 , https://doi.org/10.1287/moor.2021.1217
• P. Embrechts, H. Liu, R. Wang, Quantile-based risk sharing, Operations Research 66(4), 2018. https://doi.org/10.1287/opre.2017.1716
• P. Mohajerin Esfahani, D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric, Mathematical Programming 171, 2018. https://doi.org/10.1007/s10107-017-1172-1
• J. Dhaene, S. Vanduffel, M. Goovaerts, R. Kaas, Q. Tang, D. Vyncke, Risk measures and comonotonicity: a review, Stochastic Models 22(4), 2006. https://doi.org/10.1080/15326340600878016

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.

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.

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.

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.

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.