Motivation

Panjer recursions allow compound claim distributions to be computed without enumerating many severity convolutions. The original Panjer paper and the Sundt–Jewell family extension establish the actuarial context. The previous LXXVII mission covers finite-support frequency distributions with zero claim amounts. Here the claim count ranges over all nonnegative integers, so correct series convergence and coefficient interchange become new formal obligations.

Setting

Let N be Poisson with claim count intensity λ≥0 or geometric with parameter q in [0,1). Independently distributed claim severities are nonnegative integer valued, with pmf f_j and possibly f_0>0. For each claim count n, the distribution f^{*n} is formed using genuine convolution; the empty portfolio assigns mass one to zero. The compound mass g_k is defined as the infinite sum of p_n times the n-fold convolution coefficient, independently of any Panjer formula.

Formalization targets

The formalisation develops a connected set of actuarial identities, beginning with precise model definitions and ending with the prospective valuation result.

Countably infinite count laws and convolution powers

True infinite aggregate mass is nonnegative.

$$p_n^{\mathrm{Poi}}=e^{-\lambda}\frac{\lambda^n}{n!}$$

Probability generating functions, mass normalisation and zero atoms

Compound Poisson zero mass comes from thinning.

$$g_k=\sum_{n=0}^{\infty}p_n(f^{*n})_k,\quad g_0=G_N(f_0)$$

Full Poisson and geometric infinite Panjer recurrence

The genuinely infinite Poisson and geometric aggregates obey their independently derived corrected Panjer laws.

$$(1-qf_0)g_k=q\sum_{j=1}^kf_jg_{k-j}$$

Capstone theorem

The genuinely infinite Poisson and geometric aggregates obey their independently derived corrected Panjer laws.

$$(1-qf_0)g_k=q\sum_{j=1}^kf_jg_{k-j}$$

Significance

The capstone derives both infinite frequency families' entire positive-aggregate recurrence. For Poisson frequency the kernel includes a severity-size factor λj/k; for geometric frequency it contains an essential zero-claim correction 1−qf_0. The zero aggregate mass itself is the count PGF evaluated at severity f_0, not merely the probability of having no claims. The 1981 ASTIN literature underpins these equations, while a countably supported Lean formalisation makes their analytic conditions explicit.

Difficulty

Unlike the finite claim count in LXXVII, an infinite frequency model requires genuine convergence before double series may be rearranged. Proving the Poisson and geometric frequency normalisations is distinct from proving convergence of the actual aggregate pmf. At a fixed amount k a finite inner convolution remains, but summation over the count n is infinite. The nontrivial step is justifying probability-generating function composition and extracting the correct severity coefficients without assuming the desired recurrence or silently truncating Poisson claims. Special cases with all claim sizes zero are included.

Formalization scope

Existing actuarial theory establishes the analytical principle, whereas the formal work here must prove the stated identities in Lean using the true distribution and event definitions. Some prior mission targets describe finite distributions or a candidate valuation, but they do not establish these stronger infinite-support or measured first-passage results. The boundary assumptions are part of each mathematical statement and cannot be replaced by a tautological definition. A complete proof requires independent source lemmas, explicit handling of the limiting case and verification of every transformation before concluding the capstone.

The generating-function series is defined from the probability mass of each count; the count law is genuinely infinite, not a finite upper cutoff with a hidden tail. In particular, the positive Panjer recursion cannot be used to define its own aggregate coefficients: the aggregate mass must first be constructed from convolution powers and the count weights. At claim size zero, the event of positive frequency with all zero-valued claims contributes to the true aggregate zero probability. Geometric count and Poisson count require distinct coefficient functions, even though they share the same actuarial notation for the severity distribution.

This mission addresses actual infinite Poisson and geometric count laws, with arbitrary properly normalised discrete severities. It does not cover noninteger-shape negative-binomial frequency, complex-domain analytic continuation or continuous claim sizes. The formal target makes probability nonnegativity and summed severity mass explicit, and all Lean proofs remain open. The resulting count/compound transforms can be reused in later collective-risk, stop-loss and capital modelling applications. It deliberately excludes vacuous proof strategies that define the aggregate distribution as the recurrence answer.

These are original derived finite/analytic Actuarial formalisation targets rather than reproductions of a numbered textbook theorem. Exact Lean binder declarations are authoritative. The complete source uses targeted Mathlib imports and no local Lean compilation. All proof bodies remain genuinely open and do not constitute accepted results. Assumptions about negative rates, survival, policyholder independence, discounting and benefit timing must be preserved exactly.

Selected references

• Harry H. Panjer (1981), Recursive Evaluation of a Family of Compound Distributions, ASTIN Bulletin 12(1), pp. 22–26. https://doi.org/10.1017/S0515036100006796
• Bjørn Sundt and William S. Jewell (1981), Further Results on Recursive Evaluation of Compound Distributions, ASTIN Bulletin 12(1), pp. 27–39. https://doi.org/10.1017/S0515036100006802
• S. David Promislow (2015), Fundamentals of Actuarial Mathematics, Chapter 21. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/ftoc.xhtml