Actuarial Mathematics XXIII: Countable-Lifetime Hattendorff Limit

Mathematical source and original extension

Elias S. W. Shiu and Xiaoyi Xiong (2021), An elementary derivation of Hattendorff's theorem, European Actuarial Journal 11, 319–323, https://doi.org/10.1007/s13385-020-00256-9. In that paper equation (1) defines the fully discrete insurer's complete-life loss; equation (2) gives the Hattendorff variance formula, and equations (3)–(5) connect annual reserve recursion to the net amount at risk by summation by parts.

The present mission proposes an original countable-outcome and L²-convergence formalisation of that discrete formula. It is not asserted that the authors stated this exact Lean theorem, and it does not inherit proofs from the earlier finite-scenario missions.

Unbounded lifetime and conditional mortality

Let $K\in\mathbb N$ be the realised curtate lifetime, the number of full years remaining until the year of death. Its possible values are not uniformly bounded. Set $w_k=\Pr(K=k)$, where $w_k\ge0$ and $\sum_{k=0}^{\infty}w_k=1$. Assume the survival tail is positive in every year:

$$S_t=\sum_{k\ge t}w_k>0,\qquad q_t=\frac{w_t}{S_t},\qquad p_t=\frac{S_{t+1}}{S_t}=1-q_t.$$

These are unconditional death masses $w_t$ and conditional mortality and survival rates $q_t,p_t$. Some individual $w_t$ may be zero. The outcome space is genuinely countable; a finite Fintype of realised death years would force a bounded support and undermine the claimed infinite-horizon extension.

Mortality surprises and reserve losses

The annual mortality martingale difference is defined pathwise by

$$I_t(k)=\mathbf1_{\{k=t\}}-q_t\mathbf1_{\{k\ge t\}}.$$

For $t<k$, $I_t(k)=-q_t$; at death $t=k$, $I_t(k)=1-q_t$; and after death $t>k$, it is zero. Let the discounted net amount at risk for the payment at year-end $t+1$ be $\rho_t=v^{t+1}(b_{t+1}-V_{t+1})$. This matches Shiu–Xiong's year-end death-benefit timing. The truncated centred reserve loss and the pathwise complete-life centred loss are

$$Z_n(k)=\sum_{t=0}^{n-1}\rho_tI_t(k),\qquad Z_\infty(k)=Z_{k+1}(k).$$

The complete-life variable is well-defined on each realised finite $k$ and $Z_n(k)=Z_\infty(k)$ whenever $n>k$. These definitions only model the centred innovation component. A separate cashflow reserve-recursion bridge, as in earlier missions, is needed to identify a given insurer contract loss $L$ with $V_0+Z_\infty$; this mission does not silently assert that for arbitrary premium sequences.

Supporting results and convergence condition

The discrete expectations are weighted countable sums. Show, under summability and positive in-force mass,

$$\mathbb E[I_t]=0,\quad \mathbb E[I_i I_j]=0\;(i\ne j),\quad \mathbb E[I_t^2]=w_tp_t.$$

Using finite sums and cross-year orthogonality first gives

$$\mathbb E[Z_n^2]=\sum_{t=0}^{n-1}\rho_t^2w_tp_t.$$

The capstone introduces the mathematically substantive L² risk condition

$$\sum_{t=0}^{\infty}\rho_t^2w_tp_t<\infty.$$

This implies that the sequence of truncated centred losses is Cauchy in the probability-weighted L² space; its limit equals the pathwise stabilised $Z_\infty$. Hence

$$\boxed{\mathbb E[Z_\infty]=0,\qquad \operatorname{Var}(Z_\infty)=\mathbb E[Z_\infty^2] =\sum_{t=0}^{\infty}\rho_t^2w_tp_t.}$$

The capstone explicitly assumes nonnegative weights, unit total mass, positive survival tails, countable weight summability and risk-variance summability. The formal statement must not be weakened to merely a pointwise convergence or an unjustified interchange of infinite sums.

Exact-rational validation and boundaries

A geometric law with $q=\frac14$, $p=\frac34$, $w_k=qp^k$ and $\rho_t=2$ gives

$$Z_\infty(k)=2(p-qk),\qquad \mathbb E[Z_\infty]=0,\quad\operatorname{Var}(Z_\infty)=3.$$

Its finite-year variance is $3(1-p^n)$. The repository includes exact-rational tests for 13 horizons. The model allows an individually zero death mass but requires positive tails. Every scenario terminates in some finite year; adding a $K=\infty$ outcome with positive weight would require a separate transversality condition and is not part of this mission.

Prove2Me proof structure

The mission supplies four mathematical definitions, eleven supporting milestone theorems and one combined capstone theorem. Prove the indicator identities, the countable weighted first and second moments, finite orthogonality and finite allocation, and finally the L² passage to the unbounded lifetime. The target Lean namespace is `ActuarialValuation` in the pinned Mathlib environment. Finite-year results from earlier actuarial missions are background, not automatic countable-measure proof imports. None of the present open theorem statements is an accepted proof.

Motivation: from actuarial reserves to Hattendorff's theorem

A prospective insurance reserve is the conditional expected amount needed to fund the remaining liabilities of an in-force policy. Annual realised claims differ from their conditional expectations, and the variation in total discounted insurer loss can be allocated to these unexpected annual outcomes. Hattendorff's theorem expresses that allocation as a sum of year-specific variance contributions. The fully discrete case contains an important factor: the conditional probability of surviving the policy year.

Shiu and Xiong's article An elementary derivation of Hattendorff's theorem [1] gives a direct discrete derivation. With curtate lifetime $K$, annual death benefits $b_{j+1}$ paid at time $j+1$, premiums $\pi_j$ paid at time $j$, discount factor $v$ and prospective reserve $V_{j+1}$, their formulas include

$$L=v^{K+1}b_{K+1}-\sum_{j=0}^{K}v^j\pi_j \qquad\text{and}\qquad \rho_j=v^{j+1}(b_{j+1}-V_{j+1}).$$

In particular, the variance identity they derive has a mortality-year survival factor,

$$\operatorname{Var}(L)=\mathbb E\!\left[\rho_K^2p_{x+K}\right].$$

This mission establishes the finite-scenario mortality-innovation component of that result. It derives the orthogonality of annual death surprises rather than assuming it. It does not yet identify their weighted sum with the full insurance loss $L-V_0$; that requires the separate time-dependent reserve recursion and summation-by-parts identities in [1, equation (3)]. Those insurance cashflow bridge obligations are explicitly reserved for the next mathematical stage.

Finite lifetime model

Let $\Omega$ be a finite scenario space, $w_\omega\ge0$ its weights and $K:\Omega\to\mathbb N$ a curtate future lifetime, where $K=j$ means death during year $j$, at the end of which the death benefit is payable.

For policy duration $t$, define the in-force probability mass and the death-year mass:

$$S_t=\sum_{\omega\in\Omega}w_\omega\mathbf1_{\{K(\omega)\ge t\}}, \qquad D_t=\sum_{\omega\in\Omega}w_\omega\mathbf1_{\{K(\omega)=t\}}.$$

For probabilistic interpretation assume in addition $\sum_\omega w_\omega=1$. The exact algebraic statements do not generally require weight normalisation, though they explicitly require nonnegative weights for probability inequalities.

The disjoint identity

$$\{K\ge t\}=\{K=t\}\mathbin{\dot\cup}\{K\ge t+1\}$$

gives $S_t=D_t+S_{t+1}$. If $S_t>0$, the conditional one-year 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.$$

Division by $S_t=0$ is totalised as a Lean real expression but is not interpreted as conditioning on an impossible event. All substantive annual-innovation results impose positive in-force mass for the years used.

A centred innovation for every policy year

For each outcome and policy year define the mortality innovation

$$I_t(\omega)= \mathbf1_{\{K(\omega)=t\}} -q_t\mathbf1_{\{K(\omega)\ge t\}}.$$

It equals $1-q_t$ for death in year $t$, equals $-q_t$ for an individual surviving that year, and equals zero after death. Under $S_t>0$,

$$\mathbb E_w[I_t]=D_t-q_tS_t=0.$$

The orthogonality is more than a generic assumption. For $i<j$, if $I_j\ne0$ then the policy is still in force at $j$, so the preceding year $i$ must have been survived and $I_i=-q_i$. If $I_j=0$, the product is also zero. Thus, pointwise,

$$I_iI_j=-q_iI_j,\qquad i<j.$$

Taking the weighted expectation and using the centring of $I_j$ gives

$$\mathbb E_w[I_iI_j]=0,\qquad i<j,\quad S_j>0.$$

These innovations can be uncorrelated despite being highly dependent events generated by the same curtate lifetime. They must not be claimed independent.

The one-year discrete second moment

By conditioning on the death-year and survival outcomes, the squared mortality surprise has expected value

$$\begin{aligned} \mathbb E_w[I_t^2] &=D_t(1-q_t)^2+S_{t+1}q_t^2\\ &=D_t\,p_t,\qquad S_t>0. \end{aligned}$$

The final conditional survival factor $p_t$ is characteristic of the fully discrete actuarial Hattendorff identity. It is not an arbitrary variance weight, and it cannot be dropped by borrowing a continuous-time formula.

For a finite horizon $n$, let $\rho_t\in\mathbb R$ be any deterministic year-specific net-amount-at-risk coefficient. Define the discounted innovation portfolio

$$Z_n(\omega)=\sum_{0\le t<n}\rho_t I_t(\omega).$$

When $S_t>0$ for each $t<n$, the annual zero-mean and cross-year orthogonality identities yield

$$\boxed{ \mathbb E_w[Z_n]=0,\qquad \operatorname{Var}_w(Z_n)= \sum_{0\le t<n}\rho_t^2D_tp_t. }$$

For nonnegative unit-sum weights this is the usual finite-scenario variance. The capstone couples the derived pairwise cross-year zero moments with the resulting finite-horizon variance formula. No reserve balance, actuarial premium equation or conditional L² filtration theorem is silently assumed.

Formal proof structure and scope

The formal graph contains seven definitions: survival and death masses, conditional death and survival rates, the mortality innovation, its finite discounted portfolio and a finite weighted variance. Supporting theorems establish event partitions, nonnegativity, $q_t+p_t=1$, behaviour after death, innovation centring, a pointwise earlier/later product identity, orthogonality, the discrete second-moment formula, zero horizon and portfolio moments. The capstone packages zero covariance and the mortality-weighted variance allocation.

The variance theorem is valid for arbitrary deterministic coefficient sequence $\rho$ and any finite number of years with positive survival mass; it does not presume every life dies before that horizon. $n=0$ is covered by the empty sum. For standard actuarial application choose $\rho_t=v^{t+1}(b_{t+1}-V_{t+1})$, as in [1]. A future bridge must show that this particular innovation portfolio equals the centred insurer loss under the correct reserve recursion and endpoint conventions.

The root theorem is therefore a genuine probabilistic predecessor, not an assertion that the entire traditional Hattendorff theorem has already been proved. The mission is proposed for formal proof: private remote statement elaboration and finite rational tests, if accepted, do not constitute public Prove2Me proof acceptance.

References

[1] Shiu, Elias S. W. and Xiong, Xiaoyi (2021), “An elementary derivation of Hattendorff's theorem”, European Actuarial Journal, 11, pp. 319–323, equations (1)–(3). This is the direct source for the fully discrete variance factor, net amount at risk and finite summation-by-parts strategy.

[2] Gerber, Hans U. (1997), Life Insurance Mathematics, third edition, Springer, Chapter 6, §6.7, Allocation of the Overall Loss to Policy Years. The reserve-change and annual-loss decomposition provides broader actuarial context.

[3] Gerber, Hans U., Leung, Bartholomew P. K. and Shiu, Elias S. W. (2003), “Indicator Function and Hattendorff Theorem”, North American Actuarial Journal, 7(1), pp. 38–47. Explains the central role of indicator functions and the relationship to uncorrelated martingale increments.

Motivation: from one-step reinsurance decisions to an optimal policy

An insurer may adjust its reinsurance retention or other risk-management decision repeatedly, rather than optimising a single future year's payments. Current action choices affect both the immediate net reward and the state of the business next year, which changes the value of all later decisions. A finite-horizon Markov decision process makes this multi-year optimisation precise.

Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Chapter 4 [1], develops the finite-horizon Bellman equations and existence of optimal deterministic Markov policies for finite decision problems. Mission XV introduces a finite-action Bellman operator and excess-of-loss claim splitting, but is still under moderator review. This mission formalises the full finite-horizon backward recursion and optimal deterministic policy existence, without importing an unreviewed declaration.

The reinsurance motivation comes from Brachetta and Ceci's optimal excess-of-loss study [2]. Their original problem is a continuous-time stochastic-factor and HJB verification problem. The present mission is strictly a finite-state, finite-action, discrete-time precursor. Neither the stochastic-factor diffusion nor the jump-process verification theorem is asserted here.

Finite states, actions and one-year valuation

Let $S$ be a finite state type, and let $A$ be a finite nonempty set of admissible control actions. A state can encode a simplified surplus, rating, claims regime or any finite risk-class abstraction. At the beginning of a policy year the insurer is in state $s$ and selects an action $a$.

Let $P(s,a,t)$ be the transition weight for next state $t$, and $r(s,a)$ the immediate reward. The usual Markov model requires $P(s,a,t)\ge0$ and $\sum_tP(s,a,t)=1$ for every $s,a$. The general algebraic definitions accept real matrices, while the economic probabilistic interpretation requires valid row-stochasticity.

If $U(t)$ is the continuation value in state $t$, the return from action $a$ is

$$Q(s,a;U)=r(s,a)+v\sum_{t\in S}P(s,a,t)U(t),$$

where $v$ is a deterministic annual discount factor. The discount is applied to following-year continuation, not to the current reward. For policy interpretation $0\le v\le1$ is conventional, but finite-horizon algebra makes sense at other fixed real $v$ as well.

The one-year Bellman optimisation is

$$(TU)(s)=\max_{a\in A}Q(s,a;U).$$

The maximum is attained because $A$ is finite and nonempty. Both this attainment and the inequality $Q(s,a;U)\le(TU)(s)$ are explicit supporting theorem obligations.

Finite-horizon policy evaluation

Let $h(s)$ denote a terminal benefit or terminal value. A deterministic nonstationary Markov policy is a mapping

$$\pi:\mathbb N\times S\longrightarrow A.$$

Here $\pi_n(s)$ is the action chosen when $n+1$ decisions remain, so the index counts backwards towards the terminal time. This makes the recursion valid for a homogeneous one-step transition model without reversing calendar-time transitions.

For a fixed policy, recursively define

$$\begin{aligned} V^\pi_0(s)&=h(s),\\ V^\pi_{n+1}(s) &=r(s,\pi_n(s)) +v\sum_{t\in S}P(s,\pi_n(s),t)V^\pi_n(t). \end{aligned}$$

The policy is nonstationary because its choice at the same state may differ according to remaining time $n$. It is Markov because the action depends only on current state and remaining horizon, not on the entire historical path. The mission does not introduce a path-space filtration or general history-dependent randomised policy, so the precise capstone compares deterministic nonstationary Markov policies.

Optimal backward induction

Define $V_n(s)$ by the finite Bellman recursion

$$\begin{aligned} V_0(s)&=h(s),\\ V_{n+1}(s)&= \max_{a\in A}\left[ r(s,a)+v\sum_{t\in S}P(s,a,t)V_n(t) \right]. \end{aligned}$$

Under $P(s,a,t)\ge0$ and $v\ge0$, a larger continuation function cannot reduce the value of any action; taking a finite maximum preserves this monotonicity. That simple inequality allows induction on the remaining horizon to show

$$V^\pi_n(s)\le V_n(s) \qquad\text{for every deterministic Markov policy }\pi.$$

The second substantive step is existence of an attaining policy. Since $A$ is finite and nonempty, at each remaining horizon and each state there is at least one maximising action. Choosing such actions and combining them recursively gives a single nonstationary deterministic Markov policy $\pi^\star$ satisfying

$$V^{\pi^\star}_n(s)=V_n(s) \qquad\text{for all states }s.$$

The capstone combines the universal upper bound and existence of an attaining policy. This is genuinely more than a one-step maximum: it is an optimality result over an arbitrary finite number of sequential decisions.

A complete optimality result against all history-dependent randomised policies would need an additional equivalence argument showing no improvement from extra history or randomisation. Such an extension is well-known for suitable finite Markov models but is not silently claimed by this narrower Lean target.

Formal graph and limiting cases

Four proposed definitions encode the one-step action return, the finite Bellman maximum, policy evaluation and recursively optimal horizon value. Eleven supporting theorem targets establish zero-discount behaviour, action domination and attainment, monotonicity of action and Bellman values, zero-horizon and successor recursions, policy domination and existence of an attaining policy. The capstone packages the latter two results.

At $n=0$ there are no decisions and both values are precisely $h$. At $v=0$, any continuation is irrelevant to the one-step value. Nonnegative weights and discount are explicit hypotheses for monotonicity and policy domination, rather than false claims for signed matrix weights. The existence of an attaining maximiser in each finite action set does not itself require stochastic row-sum assumptions.

To obtain a reinsurance model from this graph, one must specify how each action corresponds to an admissible retention, how the retention changes reinsurance premiums and retained claim distributions, and how those assumptions determine the transition matrix $P$ and rewards $r$. That specialised bridge is separate from the finite-horizon mathematical result.

All theorems are proposed Lean proof targets. Preliminary remote elaboration establishes statement well-formedness only if verified by the authoritative compiler. It does not constitute a completed proof or approval of the mission's mathematical design.

References

[1] Puterman, Martin L. (1994), Markov Decision Processes: Discrete Stochastic Dynamic Programming, Chapter 4, Finite-Horizon Markov Decision Processes, Wiley. This is the direct mathematical reference for finite-horizon Bellman recursions, backward induction and existence of optimal deterministic policies under finite-state/action assumptions.

[2] Brachetta, Matteo and Ceci, Claudia (2019), “Optimal Excess-of-Loss Reinsurance for Stochastic Factor Risk Models”, Risks 7(2), article 48. This motivates insurance retention as a controlled decision but uses a continuous-time stochastic-factor/HJB model not established by this mission.

[3] Schäffeler, Maximilian and Abdulaziz, Mohammad (2022), “Formally Verified Solution Methods for Markov Decision Processes”, computer-assisted formalisation of Bellman equations, value iteration and optimal policy existence in Isabelle/HOL. This is methodology context only; no proof code is imported into Lean from that project.

Motivation

A tall $N\times n$ matrix with independent standard normal entries is, with high probability, a near-isometry: all its singular values lie in $[\sqrt N-\sqrt n,\ \sqrt N+\sqrt n]$ up to Gaussian fluctuations. This is Gordon's theorem together with Gaussian concentration (Vershynin 2012, Theorem 5.32 and Corollary 5.35), the non-asymptotic counterpart of the Bai–Yin law and the model result for the whole theory of non-asymptotic random matrices. In randomized numerical linear algebra the same two ingredients give the expected spectral norm of $S\Gamma T$ (Halko–Martinsson–Tropp 2011, Proposition 10.1 (10.2)), its second moment (Tropp–Webber 2023, Lemma B.1), and the lower tail of $\sigma_{\min}$ of a Gaussian sketch, which controls the inverse moments $\mathbb E\,\sigma_{\min}^{-2p}$ that appear in the analysis of sketching algorithms with rank truncation. None of these results is available in Mathlib; this mission proves them.

Setting

A standard Gaussian matrix $A\in\mathbb R^{N\times n}$ has independent $\mathcal N(0,1)$ entries; its law is $\gamma_{N,n}$. Its extreme singular values are

$$s_{\min}(A)=\inf_{\|x\|_2=1}\|Ax\|_2,\qquad s_{\max}(A)=\sup_{\|x\|_2=1}\|Ax\|_2=\|A\|,$$

the infimum and supremum over the unit sphere of $\mathbb R^n$ ($n\ge1$); $\|A\|$ is the spectral norm. For a wide matrix $G\in\mathbb R^{k\times t}$, $k\le t$, the usual $\sigma_{\min}(G)$ is $s_{\min}(G^{\mathsf T})$. The Frobenius norm is $\|A\|_F=(\sum_{i,j}A_{ij}^2)^{1/2}$; a function $h$ on matrices is $L$-Lipschitz if $|h(X)-h(Y)|\le L\|X-Y\|_F$. A chi-square variable with $d$ degrees of freedom is $\chi_d^2=\sum_{i=1}^d g_i^2$ for independent standard normals $g_i$. The letter $e$ denotes Euler's number.

Formalization targets

Goal — deviation of the extreme singular values (Vershynin, Corollary 5.35)

For every $t\ge0$, with probability at least $1-2e^{-t^2/2}$,

$$\sqrt N-\sqrt n-t\ \le\ s_{\min}(A)\qquad\text{and}\qquad s_{\max}(A)\ \le\ \sqrt N+\sqrt n+t .$$

This is the goal because it is the statement users of Gaussian matrices quote: a quantitative near-isometry with explicit sub-Gaussian deviations. It follows from the expectation bounds (Gordon) and concentration, both of which are milestones.

Milestones

• Gaussian concentration for Lipschitz functions of a Gaussian matrix: $\mathbb P\{h(G)\ge\mathbb E h(G)+Lt\}\le e^{-t^2/2}$ (HMT Proposition 10.3; Vershynin Proposition 5.34).
• Gordon–Chevet bound. $\mathbb E\|S\Gamma T\|\le\|S\|\|T\|_F+\|S\|_F\|T\|$ (HMT Proposition 10.1 (10.2), A.2) and its second-moment form $(\mathbb E\|S\Gamma T\|^2)^{1/2}\le\|S\|\|T\|_F+\|S\|_F\|T\|$ (Tropp–Webber Lemma B.1).
• Gordon's theorem. $\sqrt N-\sqrt n\le\mathbb E s_{\min}(A)\le\mathbb E s_{\max}(A)\le\sqrt N+\sqrt n$ (Vershynin Theorem 5.32).
• One-sided tail of $s_{\min}$. $\mathbb P\{s_{\min}(A)\le\sqrt N-\sqrt n-u\}\le e^{-u^2/2}$ for $u\ge0$ (Davidson–Szarek Theorem II.13; one-sided form of Vershynin Corollary 5.35).
• Chi-square lower tail. $\mathbb P\{\chi_d^2\le u\}\le(eu/d)^{d/2}$ for $0\le u\le d$ (Dasgupta–Gupta Lemma 2.2).
• Small-ball bound for $s_{\min}$. $\mathbb P\{s_{\min}(A)\le s\}\le n\bigl(\frac{e\,ns^2}{N-n+1}\bigr)^{(N-n+1)/2}$ for $s\ge0$, $ns^2\le N-n+1$, from the invertibility-via-distance lemma of Rudelson–Vershynin (Lemma 3.5), rotational invariance and the chi-square lower tail.

Significance

The results. Gordon's theorem is sharp: $\mathbb E s_{\min}$ and $\mathbb E s_{\max}$ are pinned to within $O(1)$ of the Bai–Yin limits for every $N,n$. Gaussian concentration upgrades it to tail bounds with the optimal sub-Gaussian rate, and the Chevet-type bound is the same mechanism for $S\Gamma T$, where it yields the expected spectral error of the randomized SVD. The small-ball bound covers the other regime, $s\to0$, with polynomial decay of the exact order $N-n+1$; together the two tails make every negative moment $\mathbb E s_{\min}(A)^{-2p}$, $2p<N-n+1$, finite and explicitly bounded, which is what the early-truncated analysis needs.

Formalizing them. Mathlib has the standard Gaussian measure on finite-dimensional inner product spaces but neither Gaussian concentration for Lipschitz functions, nor Slepian's or Gordon's comparison inequalities, nor any result on singular values of random matrices. These are foundational pieces of high-dimensional probability whose formalization would be reused far beyond this series.

Difficulty

The upper bound in Gordon's theorem is proved by Slepian's comparison lemma for the Gaussian process $(u,v)\mapsto\langle Au,v\rangle$ on $S^{n-1}\times S^{N-1}$, and the lower bound by Gordon's minimax comparison inequality for $\max_v\min_u\langle Au,v\rangle$; both require a theory of Gaussian processes indexed by continuous parameter sets, or at least a discretization argument with careful limits. Gaussian concentration (Tsirelson–Ibragimov–Sudakov) is usually proved through the Gaussian logarithmic Sobolev inequality or the Ornstein–Uhlenbeck semigroup, with a smoothing step to pass from smooth to Lipschitz functions. Both are long developments with no Mathlib support. The elementary alternatives do not reach the stated constants: an $\varepsilon$-net argument bounds $\mathbb E\|A\|$ by $C(\sqrt N+\sqrt n)$ with $C>1$, and a union bound over rows for the small-ball estimate is exactly how the stated bound is obtained, but it needs the fact that the distance from a Gaussian vector to a fixed $(n-1)$-dimensional subspace is a $\chi_{N-n+1}$ variable, which again rests on rotational invariance.

Formalization scope

Matrices are sampled from the product measure $\gamma_{N,n}$ on arrays. $s_{\min}$ is sMin, the real infimum over the unit sphere of $\mathbb R^n$; $n\ge1$ is assumed so the sphere is nonempty, and $N\ge n$ is not assumed for Gordon's theorem (for $N<n$ one has $s_{\min}=0$ and the lower bound is trivial, as in the source). $s_{\max}$ is Mathlib's $\ell_2$ operator norm. Expectation bounds are stated together with integrability of their integrands, so the Lean convention that non-integrable functions integrate to $0$ cannot trivialize them. Probabilities are measures in $[0,\infty]$ compared with $\operatorname{ofReal}$ of the real bound; the goal's lower bound $1-2e^{-t^2/2}$ uses truncated subtraction and is vacuous for $t\le\sqrt{2\log2}$, exactly as in the source. Gaussian concentration is stated with $L>0$ and $t\ge0$, which the sources leave implicit (for $L=0$ or $t<0$ the event has probability one). Results that the sketching literature states for wide $k\times t$ matrices are stated here for tall $N\times n$ matrices via $\sigma_{\min}(G)=s_{\min}(G^{\mathsf T})$, with $(N,n)=(t,k)$.

Welcome contributions: Gaussian concentration for Lipschitz functions on $\mathbb R^d$ (any proof), Slepian's and Gordon's inequalities, the $1$-Lipschitz property of $s_{\min}$ and $s_{\max}$, the chi-square Chernoff bounds, and the law of the distance from a Gaussian vector to a subspace.

Selected references

• N. Halko, P.-G. Martinsson, J. A. Tropp, Finding structure with randomness: probabilistic algorithms for constructing approximate matrix decompositions, SIAM Review 53(2), 217–288, 2011. https://arxiv.org/abs/0909.4061
• J. A. Tropp, R. J. Webber, Randomized algorithms for low-rank matrix approximation: design, analysis, and applications, 2023. https://arxiv.org/abs/2306.12418
• R. Vershynin, Introduction to the non-asymptotic analysis of random matrices, in Compressed Sensing: Theory and Applications, Cambridge University Press, 2012. https://arxiv.org/abs/1011.3027
• L. Isserlis, On a formula for the product-moment coefficient of any order of a normal frequency distribution in any number of variables, Biometrika 12, 134–139, 1918. https://doi.org/10.1093/biomet/12.1-2.134
• S. Dasgupta, A. Gupta, An elementary proof of a theorem of Johnson and Lindenstrauss, Random Structures & Algorithms 22, 60–65, 2003. https://doi.org/10.1002/rsa.10073
• M. Rudelson, R. Vershynin, The Littlewood–Offord problem and invertibility of random matrices, Advances in Mathematics 218, 600–633, 2008. https://arxiv.org/abs/math/0703503
• Y. Chen, J. Dongarra, Condition numbers of Gaussian random matrices, SIAM J. Matrix Anal. Appl. 27(3), 603–620, 2005. https://doi.org/10.1137/040616413
• A. Edelman, Eigenvalues and condition numbers of random matrices, SIAM J. Matrix Anal. Appl. 9(4), 543–560, 1988. https://doi.org/10.1137/0609045
• Y. Gordon, Some inequalities for Gaussian processes and applications, Israel J. Math. 50, 265–289, 1985. https://doi.org/10.1007/BF02759761
• K. R. Davidson, S. J. Szarek, Local operator theory, random matrices and Banach spaces, Handbook of the Geometry of Banach Spaces, Vol. 1, 317–366, 2001. https://doi.org/10.1016/S1874-5849(01)80010-3
• M. Ledoux, The Concentration of Measure Phenomenon, AMS Mathematical Surveys and Monographs 89, 2001. https://doi.org/10.1090/surv/089

Shared definitions: the items of this mission import Definitions.Def_GaussianMatrix_basic, a draft of Mission I; submit that proposal first so the import resolves at compile time.

Series: I. Rotation Invariance and Moment Identities · II. Inverse Moments of the Pseudoinverse · III. Extreme Singular Values and Concentration. All three missions share the definition bundle GaussianMatrix_basic, published with Mission I, and the namespace GaussianMatrix.

Motivation

Randomized algorithms for low-rank approximation — the randomized SVD of Halko, Martinsson and Tropp (HMT 2011), generalized Nyström, randomized subspace iteration, one-pass sketching (Tropp–Webber 2023) — multiply the input matrix by a random test matrix $\Omega$ with independent standard normal entries. Every error bound for these methods rests on a small number of facts about such standard Gaussian matrices: they are invariant under rotations, disjoint blocks of a rotated copy are independent, and the second and fourth moments of a linearly transformed Gaussian matrix are given by explicit formulas. These facts are classical, but none of them is available in Mathlib, so a Lean development of randomized numerical linear algebra currently has to carry every one of them as an explicit hypothesis of its main theorems. This mission removes those hypotheses.

Setting

For $p,m\in\mathbb N$, a standard Gaussian matrix of size $p\times m$ is a random matrix $\Gamma\in\mathbb R^{p\times m}$ whose $pm$ entries are independent $\mathcal N(0,1)$ random variables. Its law, written $\gamma_{p,m}$, is the product measure $\bigotimes_{i<p}\bigotimes_{j<m}\mathcal N(0,1)$ on real $p\times m$ arrays.

For a real matrix $A$, $\|A\|_F^2=\sum_{i,j}A_{ij}^2$ is the squared Frobenius norm; $\operatorname{rank}A$ is the dimension of its column space. A matrix $V_1\in\mathbb R^{n\times k}$ has orthonormal columns when $V_1^{\mathsf T}V_1=I_k$; a square such matrix is orthogonal. For $t\ge1$, a matrix $S\in\mathbb R^{n\times t}$ with independent $\mathcal N(0,1/t)$ entries is written $S=t^{-1/2}\Omega$ with $\Omega\sim\gamma_{n,t}$, so that $SS^{\mathsf T}=\tfrac1t\Omega\Omega^{\mathsf T}$ is an unbiased sketch of the identity.

Formalization targets

Goal — Gaussian approximate matrix multiplication

For fixed $M\in\mathbb R^{a\times n}$, $N\in\mathbb R^{b\times n}$ and $S\in\mathbb R^{n\times t}$ with independent $\mathcal N(0,1/t)$ entries,

$$\mathbb E\,\bigl\|MSS^{\mathsf T}N^{\mathsf T}-MN^{\mathsf T}\bigr\|_F^2=\frac{\|M\|_F^2\|N\|_F^2+\|MN^{\mathsf T}\|_F^2}{t}\le\frac2t\|M\|_F^2\|N\|_F^2 .$$

This is the exact mean-squared error of the sketched product $MSS^{\mathsf T}N^{\mathsf T}$ as an estimator of $MN^{\mathsf T}$, a direct consequence of Isserlis' pairing formula for Gaussian fourth moments. It is the goal because it is the one fourth-moment computation the series needs and because every other identity in the mission is a step towards it.

Milestones

• Rotational invariance. $U\Gamma V\sim\gamma_{p,m}$ for orthogonal $U\in\mathbb R^{p\times p}$, $V\in\mathbb R^{m\times m}$ (HMT §10.1).
• Blocks of a rotated Gaussian matrix. For $V_1\in\mathbb R^{n\times k}$ with orthonormal columns, $V_1^{\mathsf T}\Omega\sim\gamma_{k,t}$; for orthonormal $V_1,V_2$ with $V_1^{\mathsf T}V_2=0$, the blocks $V_1^{\mathsf T}\Omega$ and $V_2^{\mathsf T}\Omega$ are independent (HMT, proof of Theorem 10.5).
• Second moment. $\mathbb E\|S\Gamma T\|_F^2=\|S\|_F^2\|T\|_F^2$ (HMT Proposition 10.1 (10.1); Tropp–Webber Lemma B.1).
• Fourth moment. $\mathbb E\|S\Gamma T\|_F^4=(\|S\|_F^2\|T\|_F^2)^2+2\|S^{\mathsf T}S\|_F^2\|TT^{\mathsf T}\|_F^2$, the Isserlis formula for the Gaussian quadratic form $\operatorname{tr}(\Gamma^{\mathsf T}S^{\mathsf T}S\,\Gamma\,TT^{\mathsf T})$; its special case $\mathbb E\|\Omega\|_F^4=(kt)^2+2kt$ is the chi-square second moment (HMT Proposition A.8).
• Full rank. $\operatorname{rank}\Gamma=\min\{p,m\}$ almost surely (HMT, proof of Theorem 10.5 and Proposition A.5).

Significance

The results. Rotational invariance and block independence are the mechanism behind every conditioning argument in randomized linear algebra: writing the right singular vectors of the input as $[V_1\ V_2]$, the sketch splits into independent standard Gaussian blocks $\Omega_1=V_1^{\mathsf T}\Omega$ and $\Omega_2=V_2^{\mathsf T}\Omega$, and one may condition on $\Omega_1$ while treating $\Omega_2$ as fresh. The second-moment identity then turns the deterministic range-finder bound $\|\Sigma_2\Omega_2\Omega_1^{\dagger}\|_F$ into $\|\Sigma_2\|_F^2\,\mathbb E\|\Omega_1^{\dagger}\|_F^2$, and the approximate-multiplication identity gives the one-pass error terms. Almost-sure full rank is what makes $\Omega_1^{\dagger}$ a genuine pseudoinverse.

Formalizing them. Mathlib has the one-dimensional Gaussian measure, product measures, independence of coordinate projections, and (recently) the standard Gaussian measure on a finite-dimensional inner product space together with its invariance under linear isometries. None of the matrix-level statements above is in Mathlib. Once proved here they are reusable by every later mission in the series and by any formalization of randomized low-rank approximation, whose expectation-level inputs (e.g. $\mathbb E\|\Sigma_2\Omega_2\Omega_1^{\dagger}\|_F^2=\frac{k}{t-k-1}\|\Sigma_2\|_F^2$) follow from these milestones together with the inverse moments of Mission II.

Difficulty

Rotational invariance is not a computation with densities on $\mathbb R^{pm}$ that Mathlib supports out of the box: the clean route is through characteristic functions or through the basis-independence of the standard Gaussian on an inner product space, transported along the linear isometry $\Gamma\mapsto U\Gamma V$ of $\mathbb R^{p\times m}$ with the Frobenius inner product. Independence of the blocks requires identifying $[V_1\ V_2]^{\mathsf T}\Omega$ with a product measure and then projecting onto disjoint coordinate sets, with a completion of $[V_1\ V_2]$ to an orthogonal matrix when $k+r<n$. The moment identities are finite computations, but the fourth-moment identity needs the Gaussian moments $\mathbb E g^4=3$, $\mathbb E g^2=1$ organized through Isserlis' pairing formula over a four-fold sum of indices; the obvious entrywise expansion produces $O((pm)^4)$ terms that must be collapsed symbolically. Almost-sure full rank is the statement that the zero set of a nonzero polynomial ($\det$ of a maximal square submatrix) is Lebesgue-null, which must be established for the product Gaussian measure.

Formalization scope

The sample space is the function type $\mathbb R^{p}\to\mathbb R^{m}\to\mathbb R$ with the product $\sigma$-algebra; a sample is viewed as a matrix through the identity map $\mathrm{of}$. Expectations are real Bochner integrals: for an identity with a nonzero right-hand side this forces integrability, and the integrands here are polynomials in Gaussian entries. Laws are stated as equalities of pushforward measures; independence is Mathlib's IndepFun. Dimensions may be $0$; all statements remain true in that case. The hypothesis $V_1^{\mathsf T}V_1=I_k$ silently forces $k\le n$ (vacuous otherwise), which matches the source.

The definition bundle GaussianMatrix_basic supplies the law $\gamma_{p,m}$, $\|\cdot\|_F^2$, $\|\cdot\|_F$, the spectral norm (Mathlib's $\ell_2$ operator norm), the smallest singular value and the pseudoinverse $G^{\dagger}=G^{\mathsf T}(GG^{\mathsf T})^{-1}$; it is shared by the whole series. Welcome contributions: the Gaussian integration-by-parts and Isserlis lemmas for finite index sets, the identification of $\gamma_{p,m}$ with Mathlib's stdGaussian on the Frobenius inner product space, and the "polynomial zero sets are null" lemma for product measures.

Selected references

• N. Halko, P.-G. Martinsson, J. A. Tropp, Finding structure with randomness: probabilistic algorithms for constructing approximate matrix decompositions, SIAM Review 53(2), 217–288, 2011. https://arxiv.org/abs/0909.4061
• J. A. Tropp, R. J. Webber, Randomized algorithms for low-rank matrix approximation: design, analysis, and applications, 2023. https://arxiv.org/abs/2306.12418
• R. Vershynin, Introduction to the non-asymptotic analysis of random matrices, in Compressed Sensing: Theory and Applications, Cambridge University Press, 2012. https://arxiv.org/abs/1011.3027
• L. Isserlis, On a formula for the product-moment coefficient of any order of a normal frequency distribution in any number of variables, Biometrika 12, 134–139, 1918. https://doi.org/10.1093/biomet/12.1-2.134
• S. Dasgupta, A. Gupta, An elementary proof of a theorem of Johnson and Lindenstrauss, Random Structures & Algorithms 22, 60–65, 2003. https://doi.org/10.1002/rsa.10073
• M. Rudelson, R. Vershynin, The Littlewood–Offord problem and invertibility of random matrices, Advances in Mathematics 218, 600–633, 2008. https://arxiv.org/abs/math/0703503
• Y. Chen, J. Dongarra, Condition numbers of Gaussian random matrices, SIAM J. Matrix Anal. Appl. 27(3), 603–620, 2005. https://doi.org/10.1137/040616413
• A. Edelman, Eigenvalues and condition numbers of random matrices, SIAM J. Matrix Anal. Appl. 9(4), 543–560, 1988. https://doi.org/10.1137/0609045
• Y. Gordon, Some inequalities for Gaussian processes and applications, Israel J. Math. 50, 265–289, 1985. https://doi.org/10.1007/BF02759761
• K. R. Davidson, S. J. Szarek, Local operator theory, random matrices and Banach spaces, Handbook of the Geometry of Banach Spaces, Vol. 1, 317–366, 2001. https://doi.org/10.1016/S1874-5849(01)80010-3
• M. Ledoux, The Concentration of Measure Phenomenon, AMS Mathematical Surveys and Monographs 89, 2001. https://doi.org/10.1090/surv/089

Series: I. Rotation Invariance and Moment Identities · II. Inverse Moments of the Pseudoinverse · III. Extreme Singular Values and Concentration. All three missions share the definition bundle GaussianMatrix_basic, published with Mission I, and the namespace GaussianMatrix.