Probability

Motivation and actuarial setting

Prospective policy reserves measure the expected present value of an insurer's remaining benefits less remaining premiums, per policy still in force at a valuation date. When premiums and benefits occur at annual dates, consecutive reserve values satisfy a one-year cashflow balance. That recursion is central to valuation systems, reserve roll-forwards and the decomposition of a life insurance premium into risk and savings components.

This mission develops the annual net premium reserve recursion for a finite-term life assurance. It builds on the conceptual framework of prospective policy values without importing unconfirmed declarations from earlier Prove2Me missions. The principal actuarial sources are Gerber, Life Insurance Mathematics, third edition, Chapter 6 §6.3, notably equation (6.3.4) [1], and Dickson, Hardy and Waters, Actuarial Mathematics for Life Contingent Risks, first edition, Chapter 7 §7.3.3 [2]. Both develop the balance between an opening reserve, the premium due and the expected benefit plus closing reserve.

A key objective is correct treatment of impossible conditional events: the aggregate expected-loss recursion does not require next-year survival to have positive probability, while the familiar conditional-reserve formula needs the next year's reserve to be defined for an in-force life.

Time axis and cashflows

Let $K:\Omega\to\mathbb N$ be measurable curtate lifetime under a probability measure $P$. Fix the contract term $n\in\mathbb N$, integer valuation date $t$, deterministic annual discount factor $v$, death benefit $b$ and level premium $\pi$. The insurer receives a premium at the start of each policy year $j<n$ for which $K\ge j$. If $K<n$, it pays the death benefit at the end of policy year $K$, at calendar time $K+1$.

The realised present value of the remaining net insurer loss, evaluated immediately before the time-$t$ premium, is

$$L_{n,t}(\omega) =bv^{K(\omega)+1-t} \mathbf1_{\{t\le K(\omega)<n\}} -\pi\sum_{t\le j<n}v^{j-t}\mathbf1_{\{K(\omega)\ge j\}}.$$

The date-$t$ premium appears in this expression and is worth one unit before multiplying by $\pi$. Premiums earned before $t$ are excluded. The cashflow has finite calendar horizon even if the lifetime distribution is unbounded.

One-year death and survival partition

Define the probabilities of being in force, dying during the following year and surviving one further year by

$$S_t=P(K\ge t),\qquad D_t=P(K=t),\qquad S_{t+1}=P(K\ge t+1).$$

The event $\{K\ge t\}$ partitions into two disjoint events, $\{K=t\}$ and $\{K\ge t+1\}$, so

$$S_t=D_t+S_{t+1}.$$

When $S_t>0$, conditional annual death and survival probabilities are

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

No annual death-event independence assumption is made. The result follows directly from the disjoint partition of a natural-valued lifetime.

Pathwise and aggregate cashflow recursions

For $t<n$, the future loss satisfies the pointwise identity

$$L_{n,t}(\omega)+\pi\,\mathbf1_{\{K(\omega)\ge t\}} =vb\,\mathbf1_{\{K(\omega)=t\}} +vL_{n,t+1}(\omega).$$

If the person dies in year $t$, the current premium is collected and the discounted death benefit becomes due. If the person survives, the one-step-discounted continuation accounts for all remaining premiums and the eventual death benefit. Before the start of the contract's surviving period, all relevant terms vanish.

Taking expectations and using integrability of the finite-term cashflow gives the unnormalised recurrence

$$\mathbb E_P[L_{n,t}]+\pi S_t =v\left(bD_t+\mathbb E_P[L_{n,t+1}]\right).$$

This identity remains meaningful when $S_{t+1}=0$, because the future loss at $t+1$ is zero almost surely in that case. It is the safest formulation to prove before dividing by survival probabilities.

The conditional annual reserve

For $S_t>0$, define the prospective reserve per policy in force at time $t$ as

$$V_t=\frac{\mathbb E_P[L_{n,t}]}{S_t}.$$

The Lean definition uses ordinary real division, which is totalised at zero, but the actuarial interpretation above is asserted only under a positive survival-probability assumption. If both $S_t>0$ and $S_{t+1}>0$, substitute $\mathbb E[L_{n,t}]=S_tV_t$ and $\mathbb E[L_{n,t+1}]=S_{t+1}V_{t+1}$ into the aggregate identity. Division by $S_t$ yields

$$\boxed{V_t+\pi=v\bigl(q_tb+p_tV_{t+1}\bigr).}$$

The equation is the classical annual reserve balance: opening reserve plus premium equals the expected discounted claim and next-year reserve. Gerber [1, §6.3] also develops its decomposition into risk and savings premiums. This mission targets the core recursion and its probability and integrability prerequisites, rather than treating that later decomposition as already formalised.

The death-certain boundary $S_{t+1}=0$ is not hidden under a fictitious conditional reserve at $t+1$. The aggregate identity above applies directly. A later extension can derive the explicit terminal conditional formula from it while preserving the zero-probability interpretation.

Formal graph and boundary cases

The draft introduces four definitions: the realised remaining loss, the in-force survival mass, death-year mass and prospective reserve quotient. Its twelve supporting theorems establish maturity and inception boundaries, the survival-event partition, conditional death/survival probabilities, loss integrability, the pointwise and integrated one-year recursions, reserve normalisation and the conditional reserve identity. A capstone combines the probability identity with the annual reserve recursion.

For $t\ge n$, no covered future cashflow remains. At $t=0$, $S_0=1$, so the reserve is the unconditional expected loss at issue. The principal recursions allow any fixed real $v$; the usual insurance interpretation adopts a nonnegative discount factor. The proof obligations are finite-horizon and do not require a maximum possible lifetime.

The items are proposed Lean statements rather than accepted proofs. Their modules are dependency-ordered, with imports only at the beginning of each file. Until the supporting definitions have been individually published, downstream proof targets which import their modules must not be represented as ready for successful standalone compilation.

References

[1] Gerber, Hans U. (1997), Life Insurance Mathematics, third edition, Springer, Chapter 6, §6.3, Recursions, especially equations (6.3.4)–(6.3.10) and the premium risk/savings interpretation. Springer book DOI.

[2] Dickson, David C. M., Hardy, Mary R. and Waters, Howard R. (2009), Actuarial Mathematics for Life Contingent Risks, first edition, Chapter 7, Policy Values, §7.3.3, Recursive formulae for policy values. This chapter explicitly develops one-year annual policy-value recursions and related annual profit calculations.

[3] Open Actuarial Textbooks Project, Life Contingencies: Basic Life Contingent Benefits, Chapter 3, for the curtate-lifetime timing conventions used in the finite death-benefit and premium cashflows.

Motivation and actuarial context

Life-contingent benefits may depend on more than whether an insured life is alive or dead. Disability, recovery, critical illness and multiple causes of exit can all be represented by finite sets of states with possible transitions between them. Multiple-state models make it possible to value benefits on a transition, annuities paid while occupying a state, and different amounts payable according to the insured's health or other status. Dickson, Hardy and Waters develop the actuarial multiple-state setting in Actuarial Mathematics for Life Contingent Risks (2009), Chapter 8 [1]. Promislow presents a discrete-time, potentially non-stationary Markov model and its insurance and annuity applications in Fundamentals of Actuarial Mathematics (2015), §§19.2.1–19.2.3 [2].

This mission establishes the finite-state, discrete-time algebra needed before tackling more difficult continuous-time transition intensities, differential equations or multistate reserves. The capstone connects composition of transition matrices with discounted state-dependent cashflows. The mathematical emphasis is on correct probabilities, annual timing and finite sums.

Discrete-time transition kernel

Let $S$ be a nonempty finite set of possible policyholder states. For one policy year, define $P_{ab}$ as the probability of ending the year in state $b$, conditional on starting in state $a$. To represent a genuine transition kernel it must satisfy

$$P_{ab}\ge0,\qquad \sum_{b\in S}P_{ab}=1 \quad(a,b\in S).$$

The model allows a different transition matrix in each year. It does not assume a constant transition law or that every state can reach every other state. For two successive policy years, with transition kernels $P$ and $Q$, the two-step transition probability is

$$(PQ)_{ac}=\sum_{b\in S}P_{ab}Q_{bc}.$$

The intermediate state $b$ is summed out. This is the finite Chapman–Kolmogorov composition used in the non-stationary discrete Markov chain of [2, §19.2.1]. The proof must show that composing two nonnegative row-stochastic kernels produces another nonnegative row-stochastic kernel. Associativity,

$$(PQ)R=P(QR),$$

then permits an arbitrary finite sequence of yearly transition matrices to be grouped without changing the resulting transition probabilities.

The matrix calculations alone are not a theorem asserting that an arbitrary stochastic process has the Markov property. They formalise the transition-probability algebra assuming the yearly probabilities are the kernels of a Markov model. Proving a full path-space conditional-probability construction is outside this mission.

Discounted state-dependent cashflows

Suppose an annual payment depends on the state occupied after the next transition. Write $r_b$ for the amount paid at the next year end when the new state is $b$, and $N_b$ for the continuation value at that date. Let $v$ be the deterministic one-period discount factor. The one-step prospective value in current state $a$ is

$$V(a)=v\sum_{b\in S}P_{ab}(r_b+N_b).$$

Both $r$ and $N$ are measured at the next year end, so this formula applies precisely one period of discounting to both. A constant amount $c$ paid at the next year end has value $vc$, by the row-sum property. The valuation operator is linear in reward and continuation cashflows, and it is nonnegative when the discount factor, transition probabilities and cashflows are nonnegative.

For a payment $r_c$ arising only at the end of the second year, the two-stage recursion simplifies to

$$\begin{aligned} V_0(a) &=v\sum_b P_{ab} \left(v\sum_cQ_{bc}r_c\right)\\ &=v^2\sum_c(PQ)_{ac}r_c. \end{aligned}$$

This identity reconciles backward valuation with forward transition-probability composition. It is the discrete precursor to larger actuarial valuation and reserve recursions. Promislow's §§19.2.2–19.2.3 discuss state- and transition-dependent insurance and annuity cashflows [2].

Boundary conditions and limitations

When the discount factor is zero, a payment made only at the next year end has zero present value. When all future rewards and continuation values are zero, the valuation is zero. Neither algebraic identity requires a particular health-state interpretation.

The theorem graph uses a finite state type and sums over all states. A true actuarial example must supply valid transition probabilities, distinguish payments made on entering a state from those made for occupying the state, and preserve the timing of an insurance payment at the end of the year. No independence between annual state indicators is assumed. Multistate variance calculations need joint transition probabilities rather than naively treating indicators as independent [2, §19.2.2].

The mission creates three definitions, twelve supporting theorems and one capstone. The proof path begins with row normalisation and nonnegativity, proves composition and associativity, and then develops constant, zero, linear and two-step discounted reward identities. The capstone combines the preservation of a stochastic kernel, associative composition and the two-step reward valuation.

These are proposed Lean theorem statements, not claims of completed proofs. This draft uses Mathlib's finite-sum and elementary order algebra, with no reliance on unpublished actuarial mission definitions.

References

[1] Dickson, David C. M., Hardy, Mary R. and Waters, Howard R. (2009), Actuarial Mathematics for Life Contingent Risks, first edition, Cambridge University Press, Chapter 8, Multiple State Models, especially §§8.2–8.4. This provides the actuarial interpretation of state transitions and the Markov modelling assumptions.

[2] Promislow, S. David (2015), Fundamentals of Actuarial Mathematics, third edition, Wiley, ISBN 9781118782460, Chapter 19, Multi-state Models, §§19.2.1–19.2.3. The discrete non-stationary transition model and subsequent state-dependent life insurance and annuity examples are the direct cashflow motivation.

[3] Norris, J. R. (1997), Markov Chains, Cambridge University Press, §1.1, Definition and Basic Properties. The book defines a stochastic matrix by its probability-distribution rows and states Theorems 1.1.1–1.1.3 on the Markov property and powers of the transition matrix. Its basic homogeneous-chain construction is a supporting special case, not an assertion that the time-varying matrices in this mission are all equal.

Motivation and actuarial context

A net premium is usually set at policy inception. As an insured life survives and the remaining insurance term shortens, the expected future claim outgo and future premium income change. A prospective policy value measures the expected present value of the insurer's future loss on a policy that is still in force at the valuation date. This is the natural next stage after the equivalence principle of Actuarial Mathematics VIII. Dickson, Hardy and Waters provide the insurer's future-loss definition and the annual-cashflow policy-value framework in Actuarial Mathematics for Life Contingent Risks (2009), Chapter 7, §§7.3.1–7.3.3 [1]. Promislow covers both deterministic reserve recursions and the stochastic approach to reserves [2].

This mission formalises a finite-term life-assurance reserve at an integer valuation duration. Its central feature is survival conditioning: the reserve is a liability per surviving in-force policy, rather than the unconditional present value of the original contract. Separating these quantities avoids a common modelling error in stochastic policy values.

Model, contract timing and in-force event

Let $K:\Omega\to\mathbb N$ be measurable curtate future lifetime under a probability measure $P$. Let $n\in\mathbb N$ denote the term, $t\in\mathbb N$ the valuation duration, $v\in\mathbb R$ a fixed per-period discount factor, $b\in\mathbb R$ the death benefit and $\pi\in\mathbb R$ the annual level premium.

Premiums are payable in advance at integer times $j<n$ while the life is alive. The benefit, if payable, occurs at the end of the year of death, at date $K+1$. Only cashflows on or after duration $t$ enter the reserve, with discount exponents measured from $t$.

The in-force survival event is

$$S_t=\{\omega\in\Omega:K(\omega)\ge t\}.$$

When $P(S_t)>0$, conditioning on this event gives the valuation basis for policies in force at $t$. A statement about reserves conditional on survival must not silently assume that $P(S_t)>0$.

Future benefit, premium and loss values

The remaining unit term-assurance benefit present value is

$$B_{n,t}(\omega)= \mathbf1_{\{t\le K(\omega)<n\}}\,v^{K(\omega)+1-t}.$$

The remaining premium-annuity present value is

$$Y_{n,t}(\omega)= \sum_{t\le j<n} v^{j-t} \mathbf1_{\{K(\omega)\ge j\}}.$$

The realised future net loss is therefore

$$L_{n,t}(\omega;b,\pi)= bB_{n,t}(\omega)-\pi Y_{n,t}(\omega).$$

These finite expressions make it explicit whether a premium due at the valuation instant is included. Here $t$ is immediately before the premium at time $t$, consistent with an annual premium payable in advance. The choice is essential when comparing reserve formulas across valuation conventions.

At $t=0$ the in-force event is certain. At or after $t=n$, both remaining cashflow components vanish because the contract's coverage and premium period have ended.

Prospective reserve and normalisation

For positive survival probability, the prospective term-policy reserve per in-force policy is

$$V_{n,t} =\mathbb E_P[L_{n,t}\mid S_t] =\frac{\mathbb E_P[L_{n,t}]}{P(S_t)}.$$

The second equality holds because the model defines the realised future loss as zero outside $S_t$. It is a conditional-event expectation, rather than an unrestricted claim about conditional expectation with respect to an arbitrary sigma-algebra. The formal quotient definition makes the denominator explicit, and the principal reserve interpretation and capstone theorem retain $P(S_t)>0$ as a hypothesis.

Linearity separates the reserve into benefit and premium components:

$$V_{n,t}= b\,\mathbb E_P[B_{n,t}\mid S_t] -\pi\,\mathbb E_P[Y_{n,t}\mid S_t].$$

In particular, multiplying both cashflow amounts by $c\in\mathbb R$ gives

$$V_{n,t}(cb,c\pi)=cV_{n,t}(b,\pi).$$

The finite payment period ensures integrability for any fixed real discount factor. When studying economic reserve properties, a nonnegative or positive discount factor can be imposed separately. No assumption of independence between survival indicators, benefits and premiums is made.

Boundary cases and formalisation strategy

The principal boundary checks are survival at inception, $t=0$; exhaustion of cover at $t\ge n$; finite sums with $n=0$; and zero in-force probability. The total real-valued quotient happens to evaluate to zero when both its numerator and denominator are zero in Lean, but this does not create an actuarially meaningful conditional reserve for an impossible in-force event. The descriptive and main conditional theorems are explicitly scoped to positive probability.

Five definitions provide the in-force event, future benefit PV, future premium PV, future loss PV and the prospective reserve. Supporting theorems develop survival-event measurability, cashflow boundaries, nonnegativity where applicable, integrability, inception valuation, benefit–premium decomposition and scaling. The capstone combines the survival-normalised expected-loss identity, valuation decomposition and scaling.

The formalisation is deliberately self-contained at the level of future cashflow definitions so the owner Draft does not depend on the unconfirmed publication of any Mission VIII declarations. The intended later bridge is an exact identity between the duration-zero future loss and the loss-at-issue formula from Mission VIII, once those definitions are published. All theorems are proposed proof targets, not assertions of accepted proofs.

Gerber [4, §§6.3 and 6.5] provides an independent treatment of net premium reserves and annual reserve recursions. Its equation (6.5.6) expresses a whole-life net reserve through the premium difference, illustrating the same prospective viewpoint but not asserting the more general term-reserve theorem of this mission.

References

[1] Dickson, David C. M., Hardy, Mary R. and Waters, Howard R. (2009), Actuarial Mathematics for Life Contingent Risks, first edition, Chapter 7, Policy Values, Cambridge University Press. Relevant sections: §7.3.1 (future loss), §7.3.2 (policy values for annual cashflows) and §7.3.3 (recursive policy values), printed pages 176–195.

[2] Promislow, S. David (2015), Fundamentals of Actuarial Mathematics, third edition, Wiley, ISBN 9781118782460. In particular §6.3 (reserve recursion) and §15.5 (stochastic reserves).

[3] Dickson, Hardy and Waters (2009), Chapter 6, §6.5.1, equation (6.1), on the equivalence principle at policy inception, publisher book record.

[4] Gerber, Hans U. (1997), Life Insurance Mathematics, third edition, Springer, Chapter 6, Net Premium Reserves, §6.3 and §6.5, including the premium-difference reserve formula (6.5.6).

Motivation and actuarial context

The equivalence principle is one of the foundational methods of setting premiums for life-contingent contracts. It requires that the insurer's expected present value of future benefits equal the expected present value of future net premium income at policy inception. As a result, the expected present value of the net future-loss random variable is zero. Dickson, Hardy and Waters define the net future-loss random variable in Actuarial Mathematics for Life Contingent Risks (2009), §6.4, and state the equivalence principle in §6.5.1, equation (6.1) [1]. Promislow develops the corresponding stochastic premium principle in Fundamentals of Actuarial Mathematics (2015), §15.6.1 [2].

This mission makes that principle a rigorous theorem for a finite-term life assurance financed by level premiums payable annually in advance. It proves that a unique net premium exists when at least one premium is due and nonnegative discount factors are used, and it separately addresses the zero-term case where uniqueness fails. The formal treatment distinguishes realised loss from expected loss, keeps mortality and discounting assumptions explicit, and avoids treating survival-contingent benefits and premiums as independent.

Insurance contract, premium dates and realised loss

Let $(\Omega,P)$ represent the probability space, with a measurable natural-valued curtate future lifetime $K$. Let $n\in\mathbb N$ denote the policy term, $v\in\mathbb R$ the annual discount factor, $b\in\mathbb R$ a deterministic death benefit and $\pi\in\mathbb R$ a level premium.

A unit $n$-year term assurance pays once, at the end of the year of death, if death occurs within the covered term. Its realised benefit present value is $A_n$, reusing the published definition from Actuarial Mathematics II. In conventional cashflow notation,

$$A_n(\omega)= \sum_{0\le k<n}v^{k+1}\mathbf 1_{\{K(\omega)=k\}}.$$

This is the discrete term-assurance structure from [3, §3.2.2, equation (3.8)]. Premiums are due at the start of each covered year while the insured remains alive. The realised present value of unit premium income is

$$Y_n(\omega)= \sum_{0\le k<n}v^k\mathbf 1_{\{K(\omega)\ge k\}}.$$

The insurer's discounted net future loss at inception is then

$$L_n(\omega;\pi,b) =bA_n(\omega)-\pi Y_n(\omega).$$

The same curtate lifetime determines both premium income and death benefit outgo. No independence assumption is made between these two random variables.

The equivalence-principle premium

Because the sums are finite, their measurability and integrability can be established from measurability of $K$ for any finite real $v$. Linearity of expectation gives

$$\mathbb E_P[L_n(\pi,b)] =b\mathbb E_P[A_n]-\pi\mathbb E_P[Y_n].$$

For a positive term $n\ge1$ and $v\ge0$, the first premium at time zero is certain: $v^0=1$. All subsequent premium present values are nonnegative. Consequently,

$$Y_n(\omega)\ge1, \qquad \mathbb E_P[Y_n]\ge1>0.$$

The denominator in the premium formula is therefore strictly positive. Solving the linear expected-loss equation leads to the net level premium

$$\pi^*(b)= \frac{b\mathbb E_P[A_n]}{\mathbb E_P[Y_n]}, \qquad \mathbb E_P[L_n(\pi^*(b),b)]=0.$$

The theorem also proves uniqueness: any real premium $\pi$ satisfying $\mathbb E_P[L_n(\pi,b)]=0$ must equal $\pi^*(b)$. This is the formal analogue of the equivalence premium calculation in [1, equation (6.1)]. As a related worked example, [1, equation (6.2)] gives a net premium for an endowment contract using the ratio of benefit and premium-annuity values. The mission specialises the general principle to an $n$-year term assurance.

Scaling, boundaries and assumptions

Linearity yields the scaling identity

$$\pi^*(cb)=c\pi^*(b)$$

for any constant $c$. In particular, a zero benefit produces a zero premium under the ratio definition. A nonnegative benefit gives a nonnegative premium when $0\le v$, although the core algebraic scaling theorem does not require positive $b$.

The boundary $n=0$ is deliberately distinct. Neither a term-assurance benefit nor a premium can occur, so $A_0=Y_0=L_0=0$. Every quoted level premium has zero expected loss in this empty contract, and uniqueness does not follow. The ratio definition is therefore paired with explicit theorem hypotheses rather than falsely suggesting a unique zero-term premium.

At $v=0$ and $n\ge1$, the certain initial premium remains payable at inception, while all covered death benefits are paid at strictly positive times and have zero discounted value. The net premium is zero. At $v=1$, all payment sums remain finite and integrable for fixed $n$, so no artificial upper bound $v<1$ is needed for these finite-term results.

Formalisation and dependency structure

The mission introduces three definitions: the realised finite premium annuity-due present value, the realised term-policy loss, and the equivalence net premium. Supporting theorems establish the initial premium lower bound, measurability and integrability, positivity of the expected premium annuity, linearity of expected loss, existence and uniqueness of the equivalence premium, benefit scaling, and the zero-term and zero-discount boundaries. The capstone combines positivity, zero expected loss, uniqueness and benefit scaling.

The only previously published actuarial definition imported is the $n$-year term-assurance present value from Mission II. The mathematical arguments use finite sums and integration under a probability measure, rather than relying on unproved statements from other draft missions. All declarations in this owner Draft are mathematical proof targets. Their presence in a proposal does not mean that their proofs have been accepted.

Gerber [4, §5.3.1] independently develops annual-premium term insurance, including its realised loss and the net premium equations (5.3.9)–(5.3.11). Those results corroborate the payment timing and the equivalence-premium construction adopted here.

References

[1] Dickson, David C. M., Hardy, Mary R. and Waters, Howard R. (2009), Actuarial Mathematics for Life Contingent Risks, first edition, Cambridge University Press, book DOI 10.1017/CBO9780511800146. See §6.4, The present value of future loss random variable, and §6.5.1, Net premiums, particularly equations (6.1)–(6.2).

[2] Promislow, S. David (2015), Fundamentals of Actuarial Mathematics, third edition, Wiley, ISBN 9781118782460. See §15.6.1, The equivalence principle, and §15.6, The stochastic approach to premiums.

[3] Open Actuarial Textbooks Project, Life Contingencies, Chapter 3, Basic Life Contingent Benefits, §3.2.2, equation (3.8), finite term assurance.

[4] Gerber, Hans U. (1997), Life Insurance Mathematics, third edition, Springer, Chapter 5, Net Premiums, particularly §5.3.1, equations (5.3.9)–(5.3.11), on finite term insurance and net annual premiums.

Motivation and actuarial context

Whole-life assurance and a whole-life annuity-due are two fundamental life-contingent contracts. The assurance provides one unit of benefit at the end of the year of death, whereas the annuity-due provides one unit at the start of each year that the life is still eligible for payment, including time zero. Under a constant positive effective annual interest rate, their realised present values satisfy an exact finite-geometric-series identity. This provides an unusually direct connection between insurance benefits, annuity values and the distribution of curtate future lifetime. The relationship and its expected-value and variance consequences are stated in Life Contingencies, Chapter 3, equations (3.13)–(3.14) [1].

This mission formally develops that equivalence in Lean, starting from the individual cashflows and ending with a capstone theorem that combines the pointwise, expectation and variance results. It also isolates the assumptions needed for these results, supplies reusable bounds and integrability lemmas, and treats the zero-interest boundary separately. Related treatments of whole-life insurance and life annuities are available in the actuarial textbooks of Promislow [2] and Dickson, Hardy and Waters [3]. The mission's declarations are proposed proof obligations, not claims that every theorem has already been proved.

Contracts and notation

Let $K:\Omega\to\mathbb N$ be the natural-valued curtate future lifetime of the insured life. In outcome $\omega$, death occurs during policy year $K(\omega)+1$. Let $i>0$ be a flat, deterministic annual effective interest rate and define

$$v=\frac{1}{1+i},\qquad 0<v<1.$$

The unit whole-life assurance, payable at the end of the year of death, has realised present value

$$Z_A(\omega)=v^{K(\omega)+1}.$$

This is the assurance contract defined in [1, §3.2.1, equation (3.7)]. The unit whole-life annuity-due makes payments at dates $0,1,\ldots,K(\omega)$ and therefore has realised present value

$$Z_D(\omega)=\sum_{k=0}^{K(\omega)}v^k.$$

The annuity cashflow and the flat-interest specialisation are discussed in [1, §3.3.1, equations (3.11) and (3.13)]. The difference in timing is essential: the assurance payment occurs at $K+1$, one year after the last annuity-due payment at $K$.

Pointwise assurance–annuity equivalence

For $i>0$, the finite geometric sum gives

$$\begin{aligned} Z_D(\omega) &=\frac{1-v^{K(\omega)+1}}{1-v}\\ &=\frac{1+i}{i}\bigl(1-Z_A(\omega)\bigr). \end{aligned}$$

Equivalently, writing $d=i/(1+i)=1-v$ for the annual effective rate of discount,

$$Z_A(\omega)+dZ_D(\omega)=1.$$

These are pathwise statements. They hold for every realised natural-valued lifetime and require no assumptions about a mortality law or independence between annual survival events. They formalise the finite-series relationship in [1, equation (3.13)], rather than relying on an approximation or a selected life table.

Expected present values and variance

Now let $P$ be a probability measure on $\Omega$ and suppose that $K$ is measurable. The assumption $i>0$ implies $0<v<1$, and the realised values obey

$$0<Z_A(\omega)\le 1, \qquad 0\le Z_D(\omega)\le\frac{1+i}{i}.$$

These deterministic bounds establish integrability, including the required second moments, even where $K$ has unbounded support across outcomes. Taking expectations of the pointwise identity yields

$$\mathbb E_P[Z_D] =\frac{1+i}{i}\left(1-\mathbb E_P[Z_A]\right).$$

If $A_x=\mathbb E_P[Z_A]$ and $\ddot a_x=\mathbb E_P[Z_D]$ denote the corresponding actuarial values for a life aged $x$, then

$$\ddot a_x=\frac{1+i}{i}(1-A_x).$$

Translation by a constant leaves variance unchanged, and scaling multiplies variance by the square of the factor. Thus

$$\operatorname{Var}_P(Z_D) =\left(\frac{1+i}{i}\right)^2 \operatorname{Var}_P(Z_A).$$

The EPV and variance identities are stated in [1, equation (3.14)]. In particular, the variance factor is squared. No independence assumption is imposed: the assurance and annuity values are functions of the same lifetime, and the variance identity follows from their exact affine relationship.

Interest-rate boundary and scope

At zero interest, $v=1$, the whole-life annuity-due has realised value

$$Z_D(\omega)=\sum_{k=0}^{K(\omega)}1=K(\omega)+1.$$

This is a separate pointwise theorem. The expression $(1+i)/i$ is undefined at $i=0$, and an arbitrary distribution of $K$ need not give a finite undiscounted expected payment count or a finite variance. An expectation theorem at zero interest would require a suitable first-moment assumption on $K$, while a finite variance requires a second moment.

The simple assurance–annuity equivalence also relies on a flat deterministic interest basis. Under a non-flat yield curve the discounted cashflow series has varying discount factors and the same fixed geometric multiplier does not generally exist. The source expressly makes this limitation in [1, §3.3.1].

Formalisation and proof structure

The mission adds one definition, the whole-life assurance realised present value, together with eleven supporting theorems and one capstone. The supporting graph establishes discount-factor positivity, the finite geometric sum, assurance positivity, the pointwise and unit identities, a boundedness lemma, integrability of both contracts, and their expected-value and variance relationships. A separate theorem handles zero interest. The capstone combines the key pathwise identity, expected-value relation, variance scaling and unit identity.

The only imported published actuarial definition is the existing whole-life annuity-due present-value definition from the earlier mission. The assurance definition is introduced here. The proposed proofs should use the appropriate finite-sum and probability-measure results from the pinned Mathlib, and no unproved theorem from another actuarial mission should be treated as an available proof dependency. These formal dependencies are distinct from the published textbook references below.

References

[1] Open Actuarial Textbooks Project, Life Contingencies: The Mathematics, Statistics, and Economics of Life Insurance, Chapter 3, Basic Life Contingent Benefits. Principal results: §3.3.1, equations (3.13)–(3.14), on the flat-interest annuity identity, EPV and variance. Assurance definition: §3.2.1, equation (3.7). Whole-life annuities: §3.3.1, equations (3.11)–(3.12).

[2] Promislow, S. David (2010), Fundamentals of Actuarial Mathematics, Wiley. Publisher book record, particularly Chapters 4, Life Annuities, and 5, Life Insurance. This provides wider actuarial background rather than an attribution of equations (3.13)–(3.14) to Promislow.

[3] Dickson, David C. M., Hardy, Mary R. and Waters, Howard R. (2019), Actuarial Mathematics for Life Contingent Risks, third edition, Cambridge University Press, particularly Chapters 4, Insurance Benefits, 5, Annuities, and 12, Yield Curves and Non-Diversifiable Risk. These chapters provide context for contract valuation and the distinction between flat and varying interest rates.

Motivation and actuarial context

A whole-life annuity provides payments contingent on the annuitant remaining alive. A guaranteed life annuity adds a minimum number of payments, irrespective of early death. This alters the insurer's cashflows, since payments during the guarantee period are certain and subsequent payments depend on survival. It is an important contract structure for retirement income and provides a natural bridge between annuities certain, whole-life annuities and deferred life annuities. The payment definitions and expected present values are given in the Open Actuarial Textbooks Project's Life Contingencies, Chapter 3, §3.3.4, equations (3.19) and (3.20) [1]. Guaranteed payments are also covered within the broader treatments of life annuities in [2] and [3].

The objective of this mission is to formalise both annuities payable in advance (due) and annuities payable in arrears (immediate), including their exact cashflow decompositions, expected values and variances. It develops the mathematical justification for infinite survival-weighted sums when the distribution of lifetime is not bounded above. These are formal theorem targets to be proved, rather than results already established merely by publishing the statements.

Contract definition and payment timing

Let $K:\Omega\to\mathbb N$ be curtate future lifetime, where $K(\omega)$ is the number of complete future years lived in outcome $\omega$. Let $n\in\mathbb N$ be the number of guaranteed annual payments and let $v\in\mathbb R$ be a constant per-period discount factor. Each payment has unit amount, and an empty sum has value zero.

For an annuity-due, payments occur at times $0,1,\ldots$. The first $n$ payments at times $0,\ldots,n-1$ are certain. Additional payments occur at times $n,\ldots,K(\omega)$, if any.

For an annuity-immediate, payments occur at times $1,2,\ldots$. The first $n$ payments at times $1,\ldots,n$ are certain. Additional payments occur at times $n+1,\ldots,K(\omega)$, if any. The separate timing conventions are essential to the guaranteed-period boundary cases.

Realised present-value identities

The guaranteed annuity-due has realised present value

$$\begin{aligned} Z_{G,\mathrm{due}}(\omega) &=\sum_{0\le k<\max\{K(\omega)+1,n\}}v^k\\ &=\underbrace{\sum_{0\le k<n}v^k}_{C_{\mathrm{due}}} +\underbrace{\sum_{n\le k\le K(\omega)}v^k}_{D_{\mathrm{due}}(\omega)}. \end{aligned}$$

For an annuity-immediate, the corresponding identity is

$$\begin{aligned} Z_{G,\mathrm{imm}}(\omega) &=\sum_{0\le k<\max\{K(\omega),n\}}v^{k+1}\\ &=\underbrace{\sum_{0\le k<n}v^{k+1}}_{C_{\mathrm{imm}}} +\underbrace{\sum_{n\le k<K(\omega)}v^{k+1}}_{D_{\mathrm{imm}}(\omega)}. \end{aligned}$$

Here $C$ is the deterministic annuity-certain prefix and $D$ is the survival-dependent deferred continuation. The equations reproduce the underlying payment timing of [1, equations (3.19)–(3.20)]. They also connect to the deferred-annuity formulas in [1, equations (3.17)–(3.18)]. Additional pointwise theorems express each guaranteed value as its corresponding whole-life value plus the extra payments required when death occurs during the guarantee.

Expected values and variance

Let $P$ be a probability measure and assume that $K$ is measurable. For the analytical theorems, impose $0\le v<1$. Write $\Pr(K\ge k)=P(\{\omega:K(\omega)\ge k\})$. The expected present values are

$$\mathbb E_P[Z_{G,\mathrm{due}}] =\sum_{0\le k<n}v^k +\sum_{k=n}^{\infty}v^k\Pr(K\ge k)$$

and

$$\mathbb E_P[Z_{G,\mathrm{imm}}] =\sum_{0\le k<n}v^{k+1} +\sum_{k=n}^{\infty}v^{k+1}\Pr(K\ge k+1).$$

The fixed prefix and survival-weighted tail are those in the guaranteed-annuity textbook formulas [1]. A formal proof must establish measurability and integrability and justify taking expectation through the infinite sum. The geometric bound supplied by $0\le v<1$ makes these conclusions possible for a natural-valued lifetime distribution with unbounded support. No maximum attainable lifetime is assumed.

Since $C_{\mathrm{due}}$ and $C_{\mathrm{imm}}$ are deterministic, adding them changes the expected values but does not change the variances:

$$\begin{aligned} \operatorname{Var}_P(Z_{G,\mathrm{due}}) &=\operatorname{Var}_P(D_{\mathrm{due}}),\\ \operatorname{Var}_P(Z_{G,\mathrm{imm}}) &=\operatorname{Var}_P(D_{\mathrm{imm}}). \end{aligned}$$

These variance equalities are derived theorems, based on translation invariance of variance, rather than separate numbered statements in §3.3.4. The general survival-cashflow moment framework in [1, §3.1.1, equations (3.3), (3.5)–(3.6)] supplies background. No independence assumption between annual survival events is introduced.

Boundary cases and formal proof structure

When $n=0$, both guaranteed annuities reduce to their corresponding whole-life annuities. When $K(\omega)=n$, the due annuity can still pay at time $n$, while the immediate deferred continuation is empty and the $n$ guaranteed immediate payments remain. When $K(\omega)=0$, the due contract has its time-zero payment, and an immediate contract with $n>0$ still pays the $n$ certain instalments.

The finite realised-value identities hold algebraically for every real $v$, including zero, one and negative values. The stated integrability, infinite expected-value and variance theorems deliberately use $0\le v<1$. In particular, an arbitrary undiscounted lifetime distribution need not have a finite expected payment count.

The mission introduces four definitions, fourteen supporting theorems and one capstone. The intended proof path establishes cashflow decompositions and zero-guarantee identities, develops geometric bounds and measurable survival events, proves the expected-value and variance relations, and then assembles the capstone from the supporting results.

The formal dependency graph reuses six published Prove2Me declarations: the curtate-survival event and its measurability theorem, together with whole-life and deferred present-value definitions for due and immediate annuities. These are technical dependencies, distinct from the bibliographic sources below. An unproved theorem from an earlier mission is not treated as an available proof dependency.

References

[1] Open Actuarial Textbooks Project, Life Contingencies: The Mathematics, Statistics, and Economics of Life Insurance, Chapter 3, Basic Life Contingent Benefits. Principal source: §3.3.4, equations (3.19)–(3.20). Related foundations: §3.3.1 (3.11)–(3.12), §3.3.3 (3.17)–(3.18), and §3.1.1 (3.3), (3.5)–(3.6). The explanatory sentence after (3.20) calls the contract deferred, although the section heading and displayed expressions describe a guaranteed annuity.

[2] Promislow, S. David (2010), “Life Annuities”, Chapter 4 of Fundamentals of Actuarial Mathematics, Wiley, DOI: 10.1002/9781119971528.ch4. The chapter's published summary includes guaranteed payments.

[3] Dickson, David C. M., Hardy, Mary R. and Waters, Howard R. (2019), Actuarial Mathematics for Life Contingent Risks, third edition, Cambridge University Press, Chapter 5, Annuities. General context for life-annuity valuation.

Motivation

Whole-life and deferred life annuities extend survival-contingent payments beyond a fixed policy term. A whole-life annuity may pay on each eligible anniversary until death, while a deferred annuity begins after a specified waiting period. Both are standard components of pension and life-contingency valuation.

Actuarial Mathematics I established how to value finite cashflows. Missions III and IV provide curtate survival events and temporary annuity schedules. This mission develops the infinite-horizon valuation step: it justifies the lifetime payment series and its expected present value, including the conditions under which expectation can be exchanged with the discounted survival series.

The mortality and discount model

Let $(\Omega,\mathcal F,P)$ be a probability space and let $K:\Omega\to\mathbb N$ be a measurable curtate future lifetime. Define the survival event at time $k$ by

$$S_k=\{\omega:K(\omega)\ge k\}.$$

For expected present value statements, assume a deterministic annual discount factor $v$ satisfying

$$0\le v<1.$$

This condition provides a geometric bound on the payments and justifies exchanging expectation with the discounted survival series. No particular life table or independence between survival dates is assumed, and $K$ need not have a finite upper bound.

Whole-life annuities

With unit payments in advance, a life with realised curtate lifetime $K(\omega)$ receives a payment at time zero and at each subsequent beginning-of-year date through time $K(\omega)$. Its present value can be written

$$Z_{\mathrm{WL,due}}(\omega)=\sum_{k=0}^{K(\omega)}v^k =\sum_{k=0}^{\infty}v^k\mathbf1_{\{K(\omega)\ge k\}}.$$

Its expected present value, given by equation (3.11), is

$$\mathbb E_P[Z_{\mathrm{WL,due}}] =\sum_{k=0}^{\infty}v^kP(S_k).$$

A whole-life annuity in arrears pays at times $1,\ldots,K(\omega)$, with no payment at time zero:

$$Z_{\mathrm{WL,immediate}}(\omega) =\sum_{k=0}^{\infty}v^{k+1}\mathbf1_{\{K(\omega)\ge k+1\}}.$$

Equation (3.12) gives its expected present value:

$$\mathbb E_P[Z_{\mathrm{WL,immediate}}] =\sum_{k=0}^{\infty}v^{k+1}P(S_{k+1}).$$

The payment in advance at time zero is certain, and the remaining payments match the arrears stream. Thus their pointwise and expected values satisfy

$$Z_{\mathrm{WL,immediate}}=Z_{\mathrm{WL,due}}-1.$$

Deferred life annuities

For a deferral period $n\in\mathbb N$, a deferred annuity in advance has its first possible payment at time $n$, with no payments before then. Equation (3.17) gives its indicator representation:

$$Z_{\mathrm{deferred,due}} =\sum_{k=n}^{\infty}v^k\mathbf1_{\{K\ge k\}},$$

and its expected present value is

$$\mathbb E_P[Z_{\mathrm{deferred,due}}] =\sum_{k=n}^{\infty}v^kP(S_k).$$

A deferred annuity in arrears starts at time $n+1$ and requires survival to that date. Equation (3.18) gives

$$Z_{\mathrm{deferred,immediate}} =\sum_{k=n}^{\infty}v^{k+1}\mathbf1_{\{K\ge k+1\}},$$

with expected present value

$$\mathbb E_P[Z_{\mathrm{deferred,immediate}}] =\sum_{k=n}^{\infty}v^{k+1}P(S_{k+1}).$$

The timing conditions matter. If $K=n$, there is a due payment at time $n$, but no immediate payment at time $n+1$. When $n=0$, each deferred annuity is its corresponding whole-life annuity.

Whole-life values minus temporary annuities

The discounted cashflows in equations (3.17) and (3.18) are the corresponding whole-life streams with the first $n$ potential payment dates removed. Pointwise, this gives

$$Z_{\mathrm{deferred,due}} =Z_{\mathrm{WL,due}} -\sum_{k=0}^{n-1}v^k\mathbf1_{S_k},$$

and

$$Z_{\mathrm{deferred,immediate}} =Z_{\mathrm{WL,immediate}} -\sum_{k=0}^{n-1}v^{k+1}\mathbf1_{S_{k+1}}.$$

Taking expectations gives the source's deferred-annuity valuation differences: each deferred annuity's expected present value is the corresponding whole-life expected present value less that of the temporary annuity.

The finite prefix sums reproduce the temporary-annuity schedules from Mission IV without importing its unpublished declarations. Mission IV remains a Draft, so its new theorems are not available as published imports. The two published curtate survival results from Mission III can be used.

Formalisation and analytical scope

The four new definitions use a finite payment sum for each realised natural-valued lifetime. Each realised cashflow therefore has finite support, even when the possible lifetimes are unbounded. The milestones connect these finite realised sums with infinite survival-indicator series, prove the deferred and initial-payment decompositions, establish integrability under the geometric discount condition, and derive four infinite expected-value formulas.

The capstone combines these formulas and decompositions for the same probability measure, curtate lifetime, discount factor and deferral period. The measure need not arise from a particular mortality model.

The condition $0\le v<1$ applies to the expected present value claims. Pointwise present value identities hold for any real $v$, since each realised natural-valued lifetime is finite and so produces only finitely many payments. At $v=1$, an arbitrary lifetime distribution can have infinite expectation, so finite expected values cannot be assumed. The condition used here is sufficient; it is not claimed to be the sharpest possible condition under the source's financial discount assumptions.

Source and dependencies

The primary source is Life Contingencies: The Mathematics, Statistics, and Economics of Life Insurance, Chapter 3 §3.3.1 equations (3.11)–(3.12) and §3.3.3 equations (3.17)–(3.18). The temporary prefixes are the payment schedules from §3.3.2 equations (3.15)–(3.16), and the general expectation-of-cashflows step is equation (3.3).

• https://openacttextdev.github.io/LifeCon/C-SimpleBenefit.html
• https://openacttextdev.github.io/LifeCon/C-ModelingLifeTimes.html

This mission covers whole-life and deferred annuities. Guaranteed-period benefits, flat-interest assurance–annuity equivalence and continuous-time intensity-based valuations are separate later projects.

Motivation

A life annuity pays a series of amounts while its recipient survives. A term assurance pays at most once during the policy term, whereas a temporary life annuity may pay several times. The indicators for its payments can therefore overlap, so a correct second-moment calculation must retain the dependence between them.

This mission formalises temporary life annuities payable in advance and in arrears, using the finite contingent-cashflow framework established in Actuarial Mathematics I. It reuses the curtate survival-event definition from Actuarial Mathematics III.

Survival events and dependence

Let $(\Omega,\mathcal F,P)$ be a probability space, and let $K:\Omega\to\mathbb N$ be the measurable curtate future lifetime, counting completed years. The event that the life survives to time $k$ is

$$S_k=\{\omega:K(\omega)\ge k\}.$$

These events are nested. For all $i,j\in\mathbb N$,

$$S_i\cap S_j=S_{\max(i,j)}.$$

Consequently their indicators satisfy

$$\mathbf1_{S_i}(\omega)\mathbf1_{S_j}(\omega)=\mathbf1_{S_{\max(i,j)}}(\omega).$$

This matters for second moments: survival to one payment date and survival to another are not mutually exclusive. Their intersection is survival to the later date. No independence assumption is made.

Temporary life annuity payable in advance

A unit temporary life annuity payable in advance makes up to $n$ payments, at times $k=0,\dots,n-1$. The payment at time $k$ is made if $K\ge k$. With deterministic annual discount factor $v$, its random present value is

$$Z_{\mathrm{due}}=\sum_{k=0}^{n-1}v^k\mathbf1_{S_k}.$$

The expected present value is

$$\mathbb E_P[Z_{\mathrm{due}}]=\sum_{k=0}^{n-1}v^kP(S_k).$$

These are the temporary-annuity-in-advance identities in Chapter 3, equation (3.15). The first payment, at time zero, is certain whenever $n\ge1$.

Temporary life annuity payable in arrears

A unit temporary life annuity payable in arrears has potential payments at times $k+1$, for $k=0,\dots,n-1$. A payment is made only if $K\ge k+1$:

$$Z_{\mathrm{immediate}}=\sum_{k=0}^{n-1}v^{k+1}\mathbf1_{S_{k+1}}.$$

Its expected present value is

$$\mathbb E_P[Z_{\mathrm{immediate}}]=\sum_{k=0}^{n-1}v^{k+1}P(S_{k+1}).$$

These are the corresponding payment-in-arrears identities in equation (3.16). In particular, a life with $K=0$ can receive the first payment of the annuity in advance, but no payment from the annuity in arrears.

Second moments and variance

The general moment calculations in Section 3.1.1 apply to the payment schedules in equations (3.15) and (3.16). Intersections of survival events reduce to the requirement to survive to the later date.

For payments in advance, the finite double-sum second moment is

$$\mathbb E_P[Z_{\mathrm{due}}^2]= \sum_{i=0}^{n-1}\sum_{j=0}^{n-1}v^{i+j}P(S_{\max(i,j)}).$$

For payments in arrears, it is

$$\mathbb E_P[Z_{\mathrm{immediate}}^2]= \sum_{i=0}^{n-1}\sum_{j=0}^{n-1} v^{i+j+2}P(S_{\max(i+1,j+1)}).$$

These are ordered double sums. Every ordered pair of payment dates contributes, including the diagonal terms and both orders of each off-diagonal pair. The corresponding variances are

$$\operatorname{Var}_P(Z_{\mathrm{due}})= \mathbb E_P[Z_{\mathrm{due}}^2]-\bigl(\mathbb E_P[Z_{\mathrm{due}}]\bigr)^2,$$ $$\operatorname{Var}_P(Z_{\mathrm{immediate}})= \mathbb E_P[Z_{\mathrm{immediate}}^2]-\bigl(\mathbb E_P[Z_{\mathrm{immediate}}]\bigr)^2.$$

The double-sum second-moment results are formal specialisations of the general moment equations (3.5)–(3.6). They are not additional numbered results in Section 3.3.2, which gives the expectation and present-value identities in equations (3.15) and (3.16).

Formalisation goal

The main theorem packages the expected values, second moments and variances of both annuities under the same $P$, $K$, $v$ and $n$. Its supporting milestones establish the nesting of survival events and the products of their indicators, the finite payment schedules, and the successive valuation identities.

Both definitions are instances of the generic finite present-value construction from Actuarial Mathematics I. The curtate survival event is imported from Actuarial Mathematics III. Together, these provide reusable foundations for later missions on deferred and guaranteed life annuities.

The finite sums cover $n=0$, when both annuities have zero present value, and $n=1$, when the advance annuity includes the certain payment at time zero and the arrears annuity pays only if the life has completed at least one year. Algebraically, the identities allow any real $v$. In actuarial applications, $v$ is normally positive. This mission asserts neither convergence of an infinite whole-life annuity nor statistical independence of survival payments.

Source references

The primary source is Life Contingencies: The Mathematics, Statistics, and Economics of Life Insurance, Open Actuarial Textbooks Project, Chapter 3 §3.1.1 equations (3.5)–(3.6) and §3.3.2 equations (3.15)–(3.16).

• https://openacttextdev.github.io/LifeCon/C-SimpleBenefit.html
• https://openacttextdev.github.io/LifeCon/C-ModelingLifeTimes.html
• https://prove2.me/missions/Actuarial_Mathematics_I%3A_Present_Values_of_Contingent_Cashflows

This is a draft mission and has not yet been published. It formalises finite-term annual payments. Continuous payment timing, deferred whole-life payments, guaranteed-period annuities and infinite valuation are planned separately.

Motivation

An endowment assurance pays a fixed benefit either when the policyholder dies during the policy term or when the policy reaches its maturity date. It therefore brings death-contingent and survival-contingent payments together in one valuation framework.

Actuarial Mathematics I established general identities for valuing finite contingent cashflows. Mission II formalised unit term assurance and the mutually exclusive events of death in different policy years. This mission extends those foundations to pure endowments and endowment assurances, covering payment dates, expected present values, second moments and variances.

Exact lifetime and curtate lifetime

Let $(\Omega,\mathcal F,P)$ be a probability space. The exact future lifetime $T$ takes nonnegative real values, while the curtate future lifetime $K$ records completed years. Their relationship is

$$K(\omega)\le T(\omega)<K(\omega)+1.$$

For a term $n\in\mathbb N$, the textbook's pure-endowment payment in equation (3.9) depends on strict survival:

$$E_n^{>}=\{\omega:T(\omega)>n\}.$$

The endowment-assurance formula in equation (3.10), by contrast, uses a maturity payment when $K+1>n$, equivalently when $K\ge n$. Define

$$E_n^{\ge}=\{\omega:K(\omega)\ge n\}.$$

These events differ if death occurs exactly at time $n$. Given the relationship between exact and curtate lifetime,

$$E_n^{\ge}=E_n^{>}\cup\{\omega:T(\omega)=n\}.$$

Thus equation (3.9) uses exact lifetime and excludes death at $T=n$, whereas equation (3.10) uses curtate lifetime and includes it, since then $K=\lfloor T\rfloor=n$. This endpoint identity clarifies the textbook's conventions; it is not itself a numbered textbook result. No assumption is made that death at a policy anniversary has probability zero.

Pure-endowment benefit

Under the strict exact-lifetime convention, a unit pure endowment payable at time $n$ has random present value

$$Z_{\mathrm{pure}}=v^n\mathbf1_{\{T>n\}}.$$

Equation (3.9) gives its expected value and variance:

$$\mathbb E_P[Z_{\mathrm{pure}}]=v^nP(T>n),$$ $$\operatorname{Var}_P(Z_{\mathrm{pure}}) =v^{2n}P(T>n)\bigl(1-P(T>n)\bigr).$$

Here $v$ is a deterministic annual discount factor. The Lean algebra permits any real $v$, including the conventional case of a positive discount factor.

Endowment-assurance benefit

The endowment assurance pays a unit benefit at the end of the policy year of death if death occurs within the first $n$ years. Otherwise, it pays at time $n$. As in equation (3.10), its present value is defined by

$$Z_{\mathrm{endow}}(\omega)=v^{\min(K(\omega)+1,n)}.$$

The theorem expresses this value as the sum of the unit term assurance from Mission II and the curtate maturity payment:

$$Z_{\mathrm{endow}} =\sum_{k=0}^{n-1}v^{k+1}\mathbf1_{\{K=k\}} +v^n\mathbf1_{\{K\ge n\}}.$$

The death benefit and maturity benefit are mutually exclusive. This gives the expected value and second moment:

$$\mathbb E_P[Z_{\mathrm{endow}}] =\sum_{k=0}^{n-1}v^{k+1}P(K=k)+v^nP(K\ge n),$$ $$\mathbb E_P[Z_{\mathrm{endow}}^2] =\sum_{k=0}^{n-1}v^{2(k+1)}P(K=k)+v^{2n}P(K\ge n).$$

The variance is then

$$\operatorname{Var}_P(Z_{\mathrm{endow}}) =\mathbb E_P[Z_{\mathrm{endow}}^2] -\bigl(\mathbb E_P[Z_{\mathrm{endow}}]\bigr)^2.$$

Formalisation goals and milestones

The formalisation proves measurability of the strict and curtate survival events, the exact boundary-event bridge, disjointness of death during the term from survival to maturity, and the pure-endowment expectation and variance. It also proves the endowment decomposition, expectation, second moment and variance. The formal capstone brings these results together under one probability measure, using the same exact and curtate lifetimes, term and discount factor. It states the boundary bridge explicitly and includes the pure-endowment mean and variance, along with the endowment present value, mean, second moment and variance.

The formalisation reuses Mission II's definition of term-assurance present value rather than reconstructing it. The main namespace remains ActuarialValuation, so later life-annuity missions can use the survival-event lemmas.

The edge cases require care. When $n=0$, the endowment assurance pays immediately. The strict pure endowment, however, still depends on whether $T>0$. Death at exactly $T=n$ is represented separately and is never excluded by an unstated continuity assumption. The finite real-valued Lean identities permit negative or zero discount factors as a mathematical generalisation, although ordinary actuarial applications use positive discount factors.

Source and scope

The primary source is the Open Actuarial Textbooks Project, Life Contingencies: The Mathematics, Statistics, and Economics of Life Insurance, Chapter 2 §2.4.3, Chapter 3 §3.2.3 equation (3.9) and §3.2.4 equation (3.10).

• https://openacttextdev.github.io/LifeCon/C-ModelingLifeTimes.html
• https://openacttextdev.github.io/LifeCon/C-SimpleBenefit.html
• https://prove2.me/missions/Actuarial_Mathematics_I%3A_Present_Values_of_Contingent_Cashflows

Mission II, Actuarial Mathematics II: Term Assurance Present Values and Moments, is under moderator review at drafting time. Its relevant published definitions and theorem IDs are referenced directly.

This mission formalises unit benefits over a finite term with deterministic annual discounting. It establishes a finite-horizon result, not an infinite-horizon theorem. It does not cover immediate death benefits, arbitrary benefit scales, lifetime-dependent interest, infinite whole-life present values or the full continuous-time theory of mortality.

Motivation

An $n$-year term assurance pays a benefit if the insured person dies in one of the first $n$ policy years. It can pay only once. This matters when calculating the second moment: claims in different years cannot both occur, so the cross-products between them are zero.

Actuarial Mathematics I established finite expected present values, second moments and variances for general collections of contingent payments. This mission applies those results to one life and a fixed-term death benefit. It proves the familiar term-assurance formulas from reusable death-year events, rather than treating them as isolated actuarial notation.

Mathematical setting

Let $(\Omega,\mathcal F,P)$ be a probability space and let $K:\Omega\to\mathbb N$ be a measurable curtate future lifetime: the number of complete future years lived before death. For $k\in\mathbb N$, define the event of death during policy year $k+1$ by

$$D_k=\{\omega\in\Omega:K(\omega)=k\}.$$

Each event $D_k$ is measurable. The events are pairwise disjoint: if $i\ne j$, then $D_i\cap D_j=\varnothing$.

Fix a policy term $n\in\mathbb N$ and a constant annual discount factor $v$. A unit benefit is payable at time $k+1$ if death occurs during year $k+1$, for $0\leq k<n$. Its random present value is

$$Z_n(\omega)=\sum_{k=0}^{n-1}v^{k+1}\mathbf1_{D_k}(\omega).$$

When $n=0$, the sum is zero. The implementation uses the previously published `ActuarialValuation.presentValue` definition with the schedule of death-year events, reusing the general valuation machinery. The theorem statements allow any real $v$, so the finite algebra also holds beyond the economic setting $0<v\leq1$. The positive discount factors customary in the source are a special case.

Main theorem

The capstone proves these three identities together.

Expected present value:

$$\mathbb E_P[Z_n]=\sum_{k=0}^{n-1}v^{k+1}P(D_k).$$

Second moment:

$$\mathbb E_P[Z_n^2]=\sum_{k=0}^{n-1}v^{2(k+1)}P(D_k).$$

Variance:

$$\operatorname{Var}_P(Z_n)= \sum_{k=0}^{n-1}v^{2(k+1)}P(D_k) -\left(\sum_{k=0}^{n-1}v^{k+1}P(D_k)\right)^2.$$

The second-moment simplification comes from the mutual exclusivity of distinct death-year events, not from independence. In the general double sum from Actuarial Mathematics I, every off-diagonal intersection of death-year events is empty, leaving a single sum.

Formalisation milestones

The milestones proceed from measurability of each death-year event to disjointness across years, vanishing products of distinct death-year indicators, the finite present-value representation, the expected value, the second moment and the variance. The proposal gives each mathematical statement and Lean target type separately. The capstone combines the three moment identities for the same $K$, $v$, $n$ and $P$.

The project uses the existing `ActuarialValuation` namespace and imports published Mission I results where they apply. All dates are annual, and benefits are payable at the end of the year of death. Multiple lives, benefits payable immediately on death, stochastic discounts, select-life models and whole-of-life infinite sums are outside the scope of this capstone.

Why these results matter

A complete proof provides a reusable one-life mortality event model and a verified finite-term insurance valuation formula. The model can support a later mission on pure endowments and endowment assurances, where survival-to-term events complement death-in-term events, and another on temporary annuities, where survival events are nested rather than disjoint.

The results also make it straightforward to compare the traditional actuarial single-sum variance formula with the general dependent-cashflow theorem proved in Mission I.

Source and scope

The main mathematical source is Life Contingencies: The Mathematics, Statistics, and Economics of Life Insurance, Chapter 2 §2.4.3 for curtate future lifetime, Chapter 3 §3.1.1 equation (3.4) for disjoint-event moments, and §3.2.2 equation (3.8) for term-assurance present value, mean and variance.

• https://openacttextdev.github.io/LifeCon/C-ModelingLifeTimes.html
• https://openacttextdev.github.io/LifeCon/C-SimpleBenefit.html
• https://actuaries.org.uk/media/yfnkmkbq/cm1_syllabus-2026-_final-proof.pdf (CM1 2026, life-contingency valuation objectives)
• Actuarial Mathematics I: Present Values of Contingent Cashflows

These established actuarial formulas are not new mathematical conjectures. The contribution is a precise formal link in Lean from a curtate-lifetime model to the general contingent-payment valuation layer.

Formalisation challenges

The death-year set must be shown measurable from the measurability of $K$. The disjointness arguments must also cover degenerate cases such as $n=0$. The generic second-moment theorem uses an ordered double sum. The proof must remove only terms justified by $D_i\cap D_j=\varnothing$, retain the diagonal terms and use the correct end-of-year exponent $k+1$.

All formal declarations are written for Prove2Me's pinned Mathlib revision `0df444a360eaa60ab8c11dca51a86af692955474`. No local Lean compiler is used. Any private preflight compilation, if needed, is performed through Prove2Me's remote system.

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.

Motivation

An inventory policy specifies how much stock to hold before demand arrives. Its financial value is the expected sum of holding and shortage costs. Learning a useful policy and estimating its value are different statistical tasks. This proposal starts the formalization of the principal bounds in Qin, Simchi-Levi and Zhu, Information Limits of Multistage Inventory Control, using the September 29, 2026 arXiv version as a fixed source.

Setting

There are $T$ periods, independent bounded demands, positive holding and shortage costs, zero ordering costs, zero lead time, and zero terminal salvage. An action $y$ must satisfy $y\ge\max(x,0)$. The one-period cost is $h(y-d)^++p(d-y)^+$. Backlog has next state $y-d$; lost sales has next state $(y-d)^+$ and observes only $\min(d,y)$. An error tolerance always refers to total expected cost, not average cost per period. A scalar observation is counted once even if an algorithm reuses it in several periods.

The first fully specified statistical target is the stationary valuation lower bound. Holding and shortage costs are both one, the initial inventory is one, and IID demands equal zero with probability $\rho$ and one otherwise. The optimal value is defined by the actual finite-horizon Bellman infimum over feasible real actions. It is not defined to equal the formula being proved. An arbitrary randomized estimator is a Markov kernel from the finite binary archive to the real line; the same kernel is used under both laws. This includes deterministic estimators as point-mass kernels.

Formalization targets

The first target is Theorem 3.7, including its confidence dependence. Put $\rho_\pm=1-1/(2T)\pm128\epsilon/T^2$. For $T\ge8$, $0<\epsilon\le T/1024$, and $0<\eta<1/2$, simultaneous $\epsilon$-accuracy on the two instances with probability at least $1-\eta$ requires

$$M\ge\frac{T^3}{360448\epsilon^2}(1-2\eta)\log\frac{1-\eta}{\eta}.$$

Its milestones establish zero-base-stock optimality, the exact value polynomial, its derivative and quadratic sensitivity, value separation, the KL bound, and the testing reduction. The derivative has a complete local Lean proof; the other statistical proof obligations remain open. The numerical constant is retained to match the source exactly.

The complete requested program also retains the adaptive full-observation policy lower bound (Theorem 3.1), the censored lower bound and integer-count correction (Theorem 3.3 and Proposition 3.5), the stationary policy upper bound (Proposition 4.5 and Corollary 4.7), the Product ERM benchmark, and the censored upper and matching minimax rate (Section 5.4). Their full statistical encodings have not yet been added to this initial draft. They must not be inferred from the first target or from the elementary supporting lemmas. The local source map records their assumptions and dependencies.

Significance

The valuation family has a common known optimal policy, yet estimating its cost requires a cubic number of scalar observations in the horizon at fixed accuracy and confidence. This gives a concrete distinction between identifying an action and measuring its consequences. The first target preserves both the inherited-stock condition and the full confidence factor; replacing inherited stock by an empty start would change the claim.

Five additional supporting statements isolate qualified recensoring, one-period truncation, cap closure, ERM regret transfer, and optimal-value stability. They are shared by later bounds. These five results and the value-polynomial derivative have passed local Lean checking in the pinned environment; their axiom audits show only propext, Classical.choice, and Quot.sound, with no sorryAx. This is local evidence, not server verification. A correct proof of the one-period truncation identity alone does not establish dynamic optimality, statistical coverage, or a minimax rate. Likewise a deterministic ERM inequality does not prove uniform convergence.

Difficulty

The information lower bounds quantify over data-dependent randomized procedures. Encoding only a fixed allocation or a deterministic output would lose part of the intended theorem. The full policy lower bound additionally permits adaptive sampling and randomized deployment, so it needs a different transcript model from the IID stationary valuation module. Censored upper bounds require conditional independence given the entire boundary array; ordinary predictability is insufficient. The $1/r$ factor counts all prescribed logs, including discarded observations.

Upper bounds depend on the horizon-normalized convergence result from Xie, Ma and Xin, now included in the companion draft VC Theory for Inventory Policies: Xie–Ma–Xin Bounds. The source cited here as Corollary 4 is Corollary 4.10 in that paper's v3; Theorem 4.9 is its inventory fat-shattering ingredient. The companion also retains stationary and (s,S) upper and lower bound families and Product ERM. Its Lemma 4.12 cyclic partition has a complete local Lean proof. Statistical convergence, two-sided and periodwise-cost extensions, high-probability product transfer, and the censoring reductions remain open proof obligations. Neither this draft nor its companion assumes those results have already been formally proved.

Formalization scope

The environment is Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Draft theorem statements contain sorry because they are proof targets. Definition files contain no unproved assertions. Locally checked solution files must be distinguished from platform-verified proofs; a draft upload performs no server verification. Independent read-backs accompany the items so their quantifiers, domains, and total-function conventions can be reviewed directly.

The Bellman definition uses real infima. Proving nonemptiness and lower boundedness of the feasible objective set belongs to its optimality proof. Probability interpretations of finite sample weights apply only when $\rho\in[0,1]$; the hard-instance parameter bounds enforce an interior interval. The zero-sample case remains available to the testing theorem. No hypothesis assumes the desired lower bound, optimal-value formula, or derivative bound.

This is an editable initial draft, with the stationary valuation module and common algebraic foundations. It is not a certificate that all bounds in the paper have been formally proved, nor a launch-ready encoding of the complete bounds program.

Selected references

• Hanzhang Qin, David Simchi-Levi and Ruihao Zhu, Information Limits of Multistage Inventory Control: Learning, Valuation, and Censoring, arXiv:2609.37380v1, 2026. https://arxiv.org/abs/2609.37380v1
• Yaqi Xie, Will Ma and Linwei Xin, VC Theory for Inventory Policies, arXiv:2404.11509v3, 2026. https://arxiv.org/abs/2404.11509v3

Prove Lieb’s concavity theorem (Theorem 8.1.1, also stated as Theorem 3.4.1): for fixed Hermitian H, the function A ↦ tr exp(H + log A) is concave on positive-definite matrices. This is the deterministic foundation of Chapter 3’s probabilistic argument.

Milestones follow the book’s route through generalized Klein, relative-entropy nonnegativity, variational trace formulas, operator Jensen, matrix perspectives, and joint convexity of relative entropy. Logarithm and trace-exponential monotonicity are included as reusable comparisons. The domain allows noncommuting positive-definite matrices without trace normalization.

Source: Tropp, January 2015 version, Chapter 8. Lean statements compile; proofs remain open.

Shared definitions: Chapter 3; submit that draft first.

Series: Ch. 3 | Ch. 4 | Ch. 5 | Ch. 6 | Ch. 7 | Ch. 8.

Control the spectral norm of a matrix series with independent standard Gaussian or Rademacher coefficients. The goal is Theorem 4.1.1, including its variance identity, expected-norm estimate, and tail bound for rectangular complex matrices.

Milestones are the Gaussian and Rademacher matrix mgf/cgf estimates (Lemmas 4.6.2–3) and the Hermitian series bound (Theorem 4.6.1). The formulation keeps the source’s constants, both coefficient laws, and the zero-variance case. The shared Chapter 3 tools connect these transform estimates to concentration.

Source: Tropp, January 2015 version, Chapter 4. Lean statements compile; proofs remain open.

Shared definitions: Chapter 3; submit that draft first.

Series: Ch. 3 | Ch. 4 | Ch. 5 | Ch. 6 | Ch. 7 | Ch. 8.

Replace ambient matrix dimension by intrinsic dimension, the ratio of trace to spectral norm. The goal is intrinsic Matrix Bernstein (Theorem 7.3.1). Intrinsic Matrix Chernoff (Theorem 7.2.1) is a second major target within the mission.

Supporting milestones include the generalized Laplace bound, intrinsic-dimension trace estimate, block-diagonal identities, Hermitian Bernstein, and the expected-norm corollary. The statements retain the source’s constants, threshold restrictions, and matrix-valued mean or variance bounds. Nonzero proxies keep intrinsic dimension well-defined; the expectation constant is universal.

Source: Tropp, January 2015 version, Chapter 7. Lean statements compile; proofs remain open.

Shared definitions: Chapter 3; submit that draft first.

Series: Ch. 3 | Ch. 4 | Ch. 5 | Ch. 6 | Ch. 7 | Ch. 8.

Control the spectral norm of a sum of independent, centered, bounded rectangular random matrices. The goal is Matrix Bernstein (Theorem 6.1.1), including the variance identity and both expected-norm and tail estimates.

Milestones cover Hermitian dilation, variance additivity, the bounded-summand mgf/cgf estimate (Lemma 6.6.2), and Hermitian Bernstein (Theorem 6.6.1). Chapter 3 supplies the general Laplace-transform machinery. The formulation uses the Euclidean operator norm, preserves the one-sided eigenvalue assumption in the Hermitian result, and includes deterministic zero sums.

Source: Tropp, January 2015 version, Chapter 6. Lean statements compile; proofs remain open.

Shared definitions: Chapter 3; submit that draft first.

Series: Ch. 3 | Ch. 4 | Ch. 5 | Ch. 6 | Ch. 7 | Ch. 8.

Bound the extreme eigenvalues of a sum of independent positive-semidefinite random matrices. The goal is the complete Matrix Chernoff theorem (Theorem 5.1.1): both expectation estimates, both tails, and the identities for the mean’s extreme eigenvalues.

The supporting milestone is the matrix mgf/cgf estimate (Lemma 5.4.1); Chapter 3 supplies the master bounds. The Lean statement retains the different lower- and upper-tail deviation ranges, permits zero mean eigenvalues, and handles a zero summand bound explicitly.

Source: Tropp, January 2015 version, Chapter 5. Lean statements compile; proofs remain open.

Shared definitions: Chapter 3; submit that draft first.

Series: Ch. 3 | Ch. 4 | Ch. 5 | Ch. 6 | Ch. 7 | Ch. 8.

Develop the reusable matrix Laplace-transform method behind Tropp’s concentration inequalities. The goal is Theorem 3.6.1: upper and lower tail and expectation bounds for sums of independent Hermitian random matrices, expressed through their matrix cumulant-generating functions.

Milestones cover the eigenvalue tail and expectation bounds (Propositions 3.2.1–2), probabilistic Lieb inequality (Corollary 3.4.2), and trace-cgf subadditivity (Lemma 3.5.1). This mission also supplies the series’ shared spectral, probability, and dilation definitions. Lieb’s underlying concavity theorem is the Chapter 8 goal.

The Lean statements give bounds for each admissible transform parameter, with explicit integrability hypotheses; optimization recovers the source’s infimum/supremum forms.

Source: Tropp, January 2015 version, Chapter 3. Lean statements compile; proofs remain open.

Series: Ch. 3 | Ch. 4 | Ch. 5 | Ch. 6 | Ch. 7 | Ch. 8.

Motivation

A real number is normal in base $b$ when every block of $k$ base-$b$ digits occurs in its expansion with limiting frequency $b^{-k}$, as it would in a sequence of independent uniformly random digits. Borel introduced the notion in 1909 and proved that almost every real number is normal in every base, by an argument that produces no example. This mission collects the two classical papers that do produce examples: Champernowne's construction of $0.123456789101112\ldots$ and the theorem of Copeland and Erdős, which shows that the concatenation of any sufficiently dense increasing sequence of integers, the primes included, is normal.

Timeline.

• 1909. Borel defines normality and proves that Lebesgue-almost every real number is normal in every base (Borel 1909).
• 1933. Champernowne gives the first explicit normal numbers, among them the concatenation of the positive integers, and conjectures that the concatenation of the primes is normal as well (Champernowne 1933, Theorems I–IV).
• 1946. Copeland and Erdős prove normality in base $b$ of $0.a_1a_2a_3\ldots$ for every increasing sequence of positive integers with more than $N^\theta$ terms up to $N$, for every $\theta<1$ and all large $N$; the primes are a special case (Copeland–Erdős 1946).

Setting

A digit sequence is a function $s:\mathbb N\to\mathbb N$; $s_0$ is the first digit after the point. A word is a finite list $w=(w_0,\dots,w_{k-1})$ of naturals. For $N\in\mathbb N$, the occurrence count $\mathrm{count}(s,w,N)$ is the number of positions $i<N$ with $s_{i+j}=w_j$ for every $j<k$; overlapping occurrences each count.

The sequence $s$ is normal in base $b$ (IsNormalSeq b s) if, for every word $w$ with all entries $<b$,

$$\lim_{N\to\infty}\frac{\mathrm{count}(s,w,N)}{N}=b^{-|w|}.$$

The $n$-th base-$b$ digit of a real $x$ after the point is $\mathrm{digit}_b(x,n)=\lfloor x\,b^{\,n+1}\rfloor \bmod b$, and $x$ is normal in base $b$ (IsNormalReal b x) if $n\mapsto \mathrm{digit}_b(x,n)$ is normal in base $b$. The integer part of $x$ plays no role; for a rational with two expansions the floor selects the one not ending in repeated $(b-1)$'s.

Formalization targets

Goal: the Copeland–Erdős theorem

If $a_1<a_2<\cdots$ is an increasing sequence of positive integers such that, for every $\theta<1$, the number of $a_i\le N$ exceeds $N^\theta$ for all large $N$, then the digit sequence obtained by writing the base-$b$ expansions of $a_1,a_2,\ldots$ one after another is normal in base $b$. A machine-checked proof is on the platform.

Milestones

1. Copeland–Erdős counting lemma (p. 858): few strings of length $n$ contain a fixed word a number of times far from the expected count. Proved.
2. Champernowne's Theorems I, II, IV: the block constructions are normal. Proved.
3. Champernowne's Theorem III: the concatenation of the positive integers is normal in every base. Proved.
4. The primes: the Copeland–Erdős constant $0.235711131719\ldots$ is normal in every base. Proved.
5. Borel's theorem: Lebesgue-almost every real number is normal in every base. Classical, but not yet formalized here; this milestone is open.

Significance

These are the standard examples of explicitly given normal numbers, and the Copeland–Erdős block argument is the model for most later constructions. The mission also fixes a definition of normality for real numbers together with the transfer from digit sequences to reals, which other work on normal numbers can import.

Formalization scope

All declarations live in the namespace Normal and use the definition bundle Normal_Core: count, IsNormalSeq, digit, IsNormalReal; ofDigits b s $=\sum_n s_n b^{-(n+1)}$; the concatenation operators flatten, digitsBE, concatDigits; the Champernowne and Copeland–Erdős constants.

Conventions: digits are read after the point with the floor convention above; frequencies are limits of real quotients; words of every length $k\ge 0$ with entries $<b$ are quantified; results for real numbers are stated for bases $b\ge 2$ by hypothesis.

The proofs are imported from the repository xiangyazi24/normal and verified by the platform. Their auxiliary lemmas are published on the platform as dependencies of the milestones and are not listed as items of this mission.

The open question whether $\pi$ is normal is a separate mission and is not approached by the methods here, which rely on the number being given as an explicit concatenation of blocks.

Selected references

• É. Borel, Les probabilités dénombrables et leurs applications arithmétiques, Rend. Circ. Mat. Palermo 27 (1909), 247–271. https://doi.org/10.1007/BF03019651
• D. G. Champernowne, The construction of decimals normal in the scale of ten, J. London Math. Soc. 8 (1933), 254–260. https://doi.org/10.1112/jlms/s1-8.4.254
• A. H. Copeland and P. Erdős, Note on normal numbers, Bull. Amer. Math. Soc. 52 (1946), 857–860. https://doi.org/10.1090/S0002-9904-1946-08657-7