Motivation

Life insurers and pension schemes promise cashflows whose payment depends on future events. A term assurance pays if the insured dies within a stated period. A pension pays when a member survives to an instalment date. A contingent survivor pension may continue after the member dies. These liabilities differ in the events triggering payment, but share one mathematical operation: discount the amounts payable and aggregate them to obtain a random present value. Expected present value is used in premium setting and liability valuation, while the second moment and variance quantify how much the discounted liability can vary.

The open textbook Life Contingencies: The Mathematics, Statistics, and Economics of Life Insurance, Chapter 3, §3.1, introduces uncertain discounted cashflows using indicators, and derives their expected values in equation (3.3). Its treatment also distinguishes independent indicators from indicators connected through death or survival. This mission establishes a finite-horizon generalisation of those identities that handles arbitrary dependencies among payment-triggering events.

Setting

Fix a measurable sample space $(\Omega,\mathcal F)$ with a probability measure $P$. A finite set $I$ indexes distinct payment obligations. Each obligation $i\in I$ has a non-negative integer payment date $t_i\in\mathbb N$, a deterministic cashflow amount $c_i\in\mathbb R$, and a measurable event $A_i\in\mathcal F$ that triggers payment. The deterministic discount function $d:\mathbb N\to\mathbb R$ assigns a multiplier to each date. Write $\mathbf 1_{A_i}(\omega)$ for the real-valued event indicator, equal to one on $A_i$ and zero otherwise.

The random present value is

$$Z(\omega)=\sum_{i\in I}d(t_i)c_i\mathbf 1_{A_i}(\omega).$$

The same date can support multiple obligations with distinct contingencies, such as member and survivor payments, pension tranches and expenses. The index distinguishes obligations even when their payment times coincide. Amounts may be positive, zero or negative and triggering events can be mutually exclusive, nested, independent or arbitrarily dependent. Finite schedules also allow no obligations. Each present value is bounded and has finite first and second moments because the schedule is finite, amounts are deterministic real numbers, and indicators are bounded.

Formalisation targets

The capstone theorem proves the expected present value, second moment and variance identities for the same random variable $Z$. The expected present value is

$$\mathbb E_P[Z]=\sum_{i\in I}d(t_i)c_iP(A_i).$$

The second moment retains all dependence terms, including pairs of different obligations payable on the same date:

$$\mathbb E_P[Z^2]=\sum_{i\in I}\sum_{j\in I} d(t_i)c_i\,d(t_j)c_j\,P(A_i\cap A_j).$$

Consequently,

$$\operatorname{Var}_P(Z)=\sum_{i\in I}\sum_{j\in I} d(t_i)c_i\,d(t_j)c_j\, \left(P(A_i\cap A_j)-P(A_i)P(A_j)\right).$$

The finite identity for expected present value specialises the textbook's equation (3.3). The general joint-event second-moment identity extends its §3.1.1 discussion to arbitrary dependence. The goal combines all three formulas in a single result, with supporting milestone theorems for integrability, square-integrability, one-event expectation, the finite-schedule expectation formula, pairwise event interactions, the second moment and the variance.

Significance

A single reusable statement should allow a future mission to specify the trigger events and payment schedule of a policy and immediately obtain its discounted mean and variance. A life assurance can use disjoint death-year events, and an annuity can use nested survival-to-payment events. A guaranteed pension, deferred benefit, survivor pension or multiple-decrement model can use more general indicators. Later missions can also specialise the variance expression when events are known to be independent or mutually exclusive.

Examples of why the dependence assumptions matter. Write $w_i=d(t_i)c_i$ for each discounted obligation amount:

• Mutually exclusive death-year benefits: If $A_i\cap A_j=\varnothing$ for every distinct pair $i\ne j$, the general second moment simplifies to $\mathbb E_P[Z^2]=\sum_{i\in I}w_i^2P(A_i)$. This is the event structure behind term-assurance death-year payments.
• Nested survival payments: For an annuity whose $A_i$ denotes survival to time $t_i$, whenever $t_i\leq t_j$ we have $A_j\subseteq A_i$, and hence $P(A_i\cap A_j)=P(A_j)$. The later-survival probability therefore appears in the cross-term.
• Different benefits at the same date: Two obligations indexed $1$ and $2$ may both have payment time $5$, while depending on different events. Their second moment includes the cross-term $2w_1w_2P(A_1\cap A_2)$, even though $t_1=t_2$.

These specialisations use the same capstone rather than different definitions of actuarial present value.

The mathematical identities are established results of elementary probability and financial mathematics. The formalisation contribution is a stable actuarial cashflow interface connecting the relevant Lean measure-theoretic and probability results. It does not assert that the classical equations are newly discovered, or that general insurance reserving, stochastic interest rates or continuous-time survival models have already been formalised.

Difficulty

The event indicator is a bounded random variable, but its mathematical expectation is represented in Lean by integration against a measure. The development must reconcile the real-valued integrals with event probabilities represented as extended non-negative reals. Moreover, expanding the square of a finite random cashflow sum requires pairwise intersections without adding an independence assumption. The usual simplification that removes cross-terms is invalid for nested survival events or arbitrary dependent payment events.

The target also uses the real-valued variance from Mathlib. Its general API permits variables outside $L^2$, so a faithful proof must establish square-integrability for the finite event-based present value rather than use any default value for an undefined or infinite variance.

Formalisation scope

The initial development is discrete-time and finite-horizon, with distinct payment obligations indexed by a finite set. Each obligation has a nonnegative integer payment time. Different obligations may have the same payment time. Discount multipliers and payments are deterministic real values; no positivity assumption is needed for the algebraic identities. Each trigger is a measurable event and the underlying measure is a probability measure. Empty index sets and zero or negative payments are included. The joint-event formula remains valid when the same outcome triggers more than one payment.

Use Mathlib's existing MeasureTheory.Measure, MeasurableSet, integration and ProbabilityTheory.variance rather than redefining them. A lightweight namespace ActuarialValuation should define the random present value and retain clear time and cashflow parameter names. Supporting results should be small and import only genuine mathematical dependencies. The formalisation uses a generic obligation index type and a payment-time function into the natural numbers. The event family and amounts are indexed by obligations rather than by time.

There is no finite-to-infinite inference in the target; infinite sums require separate convergence results. There are no mortality rates, hazard functions, Markov transition kernels or stochastic discount factors in this mission. Those are targets for later missions, building on the valuation layer.

Selected references

• Life Contingencies: The Mathematics, Statistics, and Economics of Life Insurance, Chapter 3, §3.1, equations (3.1)–(3.3) and §3.1.1, https://openacttextdev.github.io/LifeCon/C-SimpleBenefit.html.
• Lean community, Mathlib 4: ProbabilityTheory.variance, https://leanprover-community.github.io/mathlib4_docs/Mathlib/Probability/Moments/Variance.html.
• Prove2Me, Captain tour, https://prove2.me/tour/mission-captain.