Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
The stop-loss transform is the expected value of the positive excess of a claim above an attachment, an important building block of actuarial risk ordering. Increasing retention should never increase an otherwise unchanged pure reinsurance premium. A second useful criterion is that the decrease in price should not exceed the increase in retention, once scenario probabilities are normalised. Insurance mathematics describes stop-loss premiums as decreasing functions of the deductible (https://www.researchgate.net/publication/4958878_The_Concept_of_Comonotonicity_in_Actuarial_Science_And_Finance_Theory). This mission additionally identifies their convexity in retention and develops finite verification targets for the exact bound.
A real loss X(s), a real attachment d and a real scenario weight w(s) determine a positive excess payment max(X(s)-d,0). The pure stop-loss premium at d is the weighted finite sum across s in the range from zero through bound B. Scenario weights are nonnegative for premium-order and convexity theorems. Their finite total W may be arbitrary, while W=1 expresses a genuine probability distribution and yields a sharp unit Lipschitz constant. Two attachments a and b can be combined by d(theta)=(1-theta)a+theta b, with interpolation weight theta between zero and one.
The formal targets progress from structural boundary identities to financial sensitivity and the full capstone. Supporting theorems remain genuine Open declarations until accepted Lean proofs are submitted; no previously accepted proof is silently assumed.
The exact theorem name is ActuarialValuation.retentionExcessPositive_nonneg. An excess loss payment cannot be negative even for signed real inputs, since the positive part is the maximum against zero.
The exact theorem name is ActuarialValuation.retentionStopLossPremium_zero_weight. With no scenario mass, a finite net premium is zero regardless of loss amounts and attachment.
The exact theorem name is ActuarialValuation.retentionStopLossSensitivity_fundamental. The capstone states the three structural constraints on an actuarially valid premium curve, including convex interpolation, when finite scenario weights are normalized.
The graph also contains separately stated supporting inequalities and exact definitions, with the intended original derived mathematical identity written out in every milestone.
These conditions provide powerful reasonableness checks for treaty pricing functions. An actuary can diagnose a premium that rises with retention, or an implausibly large fall inconsistent with maximum ceded-payment change, before relying on a stochastic model. The classical stop-loss transform is extensively studied in insurance finance (https://www.researchgate.net/publication/4958878_The_Concept_of_Comonotonicity_in_Actuarial_Science_And_Finance_Theory). The reusable finite inequalities connect claim severity, scenario weights and contract terms, and can support downstream optimisation, layered reinsurance sensitivity and refinement of discrete tail distributions.
The positive part is a maximum of two affine functions, which is convex but not differentiable when the claim equals the retention. The finite theorem must not assume every claim is above a or b: a distribution can straddle both attachment points. The premium derivative is not required, since pointwise algebraic inequalities suffice to justify convex interpolation and monotone order. The mass-dependent Lipschitz bound becomes one only when total mass is one, so probability normalisation must be stated. Claim severity need not be nonnegative for the algebraic result, while weights must be nonnegative for order preservation.
The Lean representation uses real numbers for claim severities, deductibles, masses and convex interpolation. Finite scenarios are represented by natural indices and Finset.range. Positive excess is a maximum of two real numbers. All inequalities are original derived finite specialisations of well-known stop-loss facts, with explicit mathematical types and numerical boundary conventions. The formalisation intentionally excludes continuous distributions, derivatives, infinite-dimensional weak convergence and loaded commercial premium assumptions. The main goal is nontrivial because it demands the general weighted convexity and Lipschitz properties for an arbitrary finite loss table.
The pinned Mathlib revision and the precise Lean type of each definition or proposition are authoritative. The imported source must use targeted Mathlib modules; one large aggregate compiler check never substitutes for testing individual definition imports and obsolete namespace openings. The source-specific intermediate statements separate units and hypotheses. The finite index always counts claims, scenarios, or observations according to the declaration, not an implicit probability measure. In an insurance pricing setting the difference between a gross loss, a ceded payment, a net premium and a credibility risk estimate is financially important. A positive coefficient does not by itself imply the coefficients sum to one. Likewise a deterministic algebraic identity does not grant stochastic independence or a forecast model. These restrictions preserve the distinction between a purely algebraic result and a probabilistic interpretation. The formal theorem declarations have to maintain exactly the same quantifiers, arithmetic operations and endpoint conventions as the descriptions, including meaningful boundary cases. Future extensions can introduce richer distributions and dependence without altering the precise finite identities established here.
S. David Promislow, Fundamentals of Actuarial Mathematics, third edition, Wiley, 2015, printed page 409. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/
Denuit and colleagues, The Concept of Comonotonicity in Actuarial Science and Finance: Theory, 2002. https://www.researchgate.net/publication/4958878_The_Concept_of_Comonotonicity_in_Actuarial_Science_And_Finance_Theory
Sampling an entire finite-state execution is a different computational task from recognizing a supplied word. A membership circuit must answer correctly on its given input. A sampler instead chooses the input together with its associated output, while preserving their joint distribution. This distinction is relevant when finite-state models describe allowable executions and when parallel generation should avoid a sequential pass through every transition. The source paper establishes constant-depth sampling results for regular languages and finite Markov chains in Appendix E (Zhang et al., 2026).
The mission concerns that appendix's finite-state sampling results. It formalizes all six numbered results E.1–E.6, together with the seed bounds stated in the surrounding text. Each milestone points to a published theorem with a separately checked proof. The objects to sample are complete words, word–acceptance pairs, and complete state trajectories. Sampling only the final state would lose the joint temporal information required by the targets.
A binary deterministic finite automaton has finitely many states, a designated start state, a transition for each state and bit, and a set of accepting states. Starting from its initial state, a binary word of length determines a run. Let be the set of words whose final state is accepting. Put . An arbitrary such automaton represents an arbitrary binary regular language, with no assumption that membership belongs to .
A finite Markov chain consists of a nonempty finite state set , an initial probability vector , and a row-stochastic transition matrix . Entries are nonnegative real numbers, not restricted to rational numbers. For , its probability is . The distribution of all states is denoted . For , conditioning is allowed when the probability that is positive.
A randomized sampler is a deterministic Boolean circuit supplied with independent, unbiased random bits. AND and OR gates have unbounded fan-in; NOT gates and Boolean constants are permitted. Its size is polynomial and its depth has a constant bound independent of trajectory length. Approximate families are nonuniform in both and their real error tolerance : existence does not require efficiently computing circuit descriptions or numerical tables from a supplied transition matrix.
The main goal is the conjunction of all results E.1–E.6, including the linear seed guarantee for E.5. This organizational theorem is not an additional numbered result attributed to the paper. All six milestones must be proved for the goal to hold. The exact Markov sampling criterion in Theorem E.5 is one component. A nonnegative real number is dyadic if it equals for natural numbers , including zero. A chain is path-dyadic when every finite trajectory, including a trajectory of length zero, has a dyadic probability. The target is
On the left, the family has polynomial size in and depth bounded independently of . A supporting target records the linear fair-bit budget when path-dyadicity holds. Lemma E.4 supplies another target: every path-dyadic chain is the coordinatewise projection of a finite chain whose initial and transition probabilities are all dyadic. Path-dyadicity must not be replaced by the stronger requirement that the original transition matrix itself be dyadic (Appendix E.3).
Theorem E.1 concerns exact sampling of a uniformly random word together with its acceptance indicator:
The sampler uses exactly fair bits, polynomial size, and depth depending only on the fixed automaton. This is a sampling assertion and does not assert that membership can be computed in constant depth on an arbitrary externally supplied word.
Theorem E.2 concerns the uniform law on nonempty . For every , the target is
Every possible output is accepted. Size is polynomial in and , and depth depends only on the fixed language or its automaton. In particular, the leading coefficient of the term in the random-bit bound is one (Appendix E.2).
Theorem E.6 is the corresponding approximate target for trajectories conditioned on . It requires total variation error at most , only positive-probability outputs ending in , fair bits, polynomial size in and , and depth depending only on the chain. There is no lower bound on the conditioning probability beyond strict positivity (Appendix E.4).
Lemma E.3 supplies the exact representation used in the Markov construction. A transition-dyadic chain is represented by one binary DFA and a fixed state projection. On a uniform input of length , with positive constants , the states observed after bits project to exactly the complete trajectory law of the chain. The same DFA and projection work for every length, including zero.
These results separate sampling an input together with its finite-state behavior from computing that behavior on a prescribed input. They also identify a precise obstruction to exact sampling with a finite fair-bit seed: each output probability must be dyadic. Approximate sampling allows arbitrary real transition probabilities while retaining the valid trajectory support. The complete trajectory requirement preserves correlations among all time coordinates.
The formalization makes the circuit model, seed accounting, support guarantees and asymptotic quantifiers explicit and reusable. The theorem statements and their separately submitted proofs have passed the platform verifier. The goal proof imports all six milestones; its E.5 milestone in turn imports both the equivalence and the linear seed theorem. Thus the platform dependency graph covers the entire appendix. Platform verification establishes the formal statements; semantic correspondence is documented in the statement descriptions and source references.
A literal step-by-step implementation of a run makes circuit depth grow with , so it does not meet the constant-depth target. Recognition results alone do not furnish the required joint sampler. For approximate word sampling, an error estimate alone is insufficient: the output must remain in the accepted support, and the coefficient-one seed bound must also hold. For exact Markov sampling, unreachable states and non-dyadic individual transitions prevent identifying the desired criterion with entrywise dyadicity. Conditioning on a rare terminal event must not introduce an unstated dependence on its probability.
States are indexed by finite types . Binary words have type ; trajectories have coordinates. Markov vectors and matrices are real-valued and carry normalization and nonnegativity proofs. Sampling probabilities are defined by counting all seeds that give a particular encoded outcome and dividing by . Total variation is half the finite sum of absolute probability differences.
The circuit representation is an explicit topologically ordered gate list with checked wire references. Size counts input bits, gates, gate-input wires and output wires; this yields the usual polynomial-size class. State trajectories use a fixed one-hot encoding at each time coordinate. The invalid-output predicate is checked over every seed, so neither arbitrary decoders nor unrepresented outcomes can satisfy an exact or support-preserving claim. The encodings used by the targets are injective. The circuit family is existentially quantified after the fixed finite-state model; the depth and polynomial constants precede and .
Zero-length words and zero-transition Markov paths are included. The word target excludes empty accepted slices. The conditioned target excludes zero-probability conditioning events. Definitions of division by zero still exist as total Lean functions, but the hypotheses exclude those cases from approximate claims. Extensions of these results, reusable finite-state probability lemmas, and further circuit constructions are welcome. No sampler-existence axiom, vacuous model or final-state-only replacement is part of the interface.
Per-occurrence excess and aggregate excess have different financial triggers. One aggregate deductible applies once to the sum of claims, while a per-risk retention is charged against each loss. Combining many small claims may exhaust an aggregate deductible without producing a payment under any separate per-claim policy. HMRC explains how non-proportional reinsurance differs across individual risks and catastrophe or aggregate protections (https://www.gov.uk/hmrc-internal-manuals/general-insurance-manual/gim8060). The valuation question is how the ceded amounts and their pure expected costs are ordered when otherwise identical annual experience and deductibles are used.
The individual claims x(i), their finite number n, and the deductible d are natural-number monetary quantities. Gross aggregate loss S(n) is the sum of the first n claims. Aggregate recovery is positive excess of S(n) above d; separate per-claim recovery is the sum of each claim's positive excess over d. Finite scenario weights w(s) are real. A scenario maps to an entire loss sequence, and its total claim portfolio is evaluated consistently under both treaty designs. Weighted claims are aggregated for indices from zero to a finite bound B, allowing the scenario count itself to be zero or the probability weights to lack normalisation.
The formal targets progress from structural boundary identities to financial sensitivity and the full capstone. Supporting theorems remain genuine Open declarations until accepted Lean proofs are submitted; no previously accepted proof is silently assumed.
The exact theorem name is ActuarialValuation.aggregateLossTotal_zero. An empty collection of claims has zero gross claims and therefore defines the base case for deductible comparisons.
The exact theorem name is ActuarialValuation.aggregateDeductibleCeded_zero_attachment. With attachment zero, the aggregate excess treaty covers every unit of gross annual claims.
The exact theorem name is ActuarialValuation.aggregateVsPerClaim_fundamental. The capstone joins the nontrivial pointwise reinsurance coverage inequality to the same ordering of expected pure premiums, without conflating a whole-year treaty with a per-claim deductible.
The graph also contains separately stated supporting inequalities and exact definitions, with the intended original derived mathematical identity written out in every milestone.
The comparison can diagnose material pricing errors, since an aggregate deductible and a per-risk deductible with the same quoted monetary value should not normally have the same technical premium. HMRC's treatment of non-proportional reinsurance (https://www.gov.uk/hmrc-internal-manuals/general-insurance-manual/gim8060) makes this distinction a contractual reality. The formal theorem is useful for ceded reserve reconciliation, claims-data audit, treaty design, and future models including several occurrence covers within a separate annual limit. In each case exact mathematical relationships are more valuable than approximate simulation agreement.
The algebra of positive-part natural subtraction differs from ordinary subtraction over integers or real values. The aggregate deductible is taken once, whereas the per-event premium subtracts the same amount separately from each positive claim. The theorem is a weak inequality and must remain valid even when every event is below the separate retention but the aggregate exceeds the annual attachment. The model explicitly includes zero claims, zero deductible, empty portfolios and nonnegative scenario weights. Signed weights would make the expectation order invalid and are not silently permitted in that result.
Lean treats all claim amounts, event counts, attachment values and scenario bounds as natural numbers. Real numbers occur only in the finite expected ceded amounts. Each individual-claim sum uses Finset.range and the pure premium is a further finite sum over scenarios. This is an exact deterministic relationship between two reinsurance structures rather than an assumption of independence or identical event distributions. No catastrophe frequency model, claims adjustment expenses or risk load is included. The established contractual idea motivates original derived finite relations, and the formal statements remain open until proved.
The pinned Mathlib revision and the precise Lean type of each definition or proposition are authoritative. The imported source must use targeted Mathlib modules; one large aggregate compiler check never substitutes for testing individual definition imports and obsolete namespace openings. The source-specific intermediate statements separate units and hypotheses. The finite index always counts claims, scenarios, or observations according to the declaration, not an implicit probability measure. In an insurance pricing setting the difference between a gross loss, a ceded payment, a net premium and a credibility risk estimate is financially important. A positive coefficient does not by itself imply the coefficients sum to one. Likewise a deterministic algebraic identity does not grant stochastic independence or a forecast model. These restrictions preserve the distinction between a purely algebraic result and a probabilistic interpretation. The formal theorem declarations have to maintain exactly the same quantifiers, arithmetic operations and endpoint conventions as the descriptions, including meaningful boundary cases. Future extensions can introduce richer distributions and dependence without altering the precise finite identities established here.
S. David Promislow, Fundamentals of Actuarial Mathematics, third edition, Wiley, 2015, printed page 389. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/
HM Revenue & Customs, General Insurance Manual: Non-proportional reinsurance, GOV.UK, 2023. https://www.gov.uk/hmrc-internal-manuals/general-insurance-manual/gim8060
Hattendorff's theorem allocates the variance of an insurer's life-contingent loss to policy years. In a fully discrete life insurance model, each policy year's contribution depends on the discounted net amount at risk, the probability of dying in that year, and the conditional probability of surviving the year. Shiu and Xiong (1) derive the classical loss-at-issue formula and the corresponding discrete Hattendorff variance through reserve identities and a summation-by-parts argument. Gerber [2, §6.7] discusses the actuarial allocation of total loss to individual policy years.
The related Missions XVI and XIX address two complementary parts of that argument. XVI specifies death/survival masses for a finite lifetime distribution and proposes proofs of centred annual mortality innovations, cross-year orthogonality and variance. XIX describes a pathwise, year-by-year accounting identity expressing insurer loss, including the terminal reserve, as the opening reserve plus discounted mortality innovations. The present mission is the mathematical bridge combining these structures.
It targets the full finite-horizon reserve-loss expectation and variance theorem under consistent conditional mortality probabilities and the annual prospective reserve recurrence. Unlike a purely algebraic zero-covariance lemma, the mortality model supplies the orthogonality. Unlike a standalone cashflow telescoping lemma, the result calculates the variance of the insurer's actual policy loss.
Fix a finite scenario space , with nonnegative probabilities summing to one, and a curtate future lifetime . An insured with dies during policy year .
Define the in-force and death-year probability masses
The disjoint survival/death partition gives . For each year covered by the policy valuation horizon, assume positive in-force mass, , so that the conditional death and survival rates are well-defined:
These rates are derived from one joint lifetime distribution. The annual death indicators are therefore linked across years and are not independent. The zero-covariance result must be derived from the nested survival-event structure rather than assumed.
Let denote the finite number of years covered, a deterministic annual discount factor, the beginning-of-year premium, the death benefit payable at time , and the prospective reserve at time for a policy still in force.
Assume that, for each year , the prospective reserve satisfies
The realised insurer loss, valued at issue, is
The terminal reserve is explicitly included if the insured survives beyond the chosen horizon. Thus , a life may remain insured after year , and neither nor is assumed zero. The original Shiu–Xiong complete-life issue-loss formula is recovered only under appropriate terminal/residual liability conditions; the present finite-horizon formula is the reserve-inclusive extension needed for a finite theorem.
The year- mortality innovation is
The discounted net amount at risk is
By the annual reserve recurrence and the in-force event partition, the change in the insurer's loss across a policy year equals . Summing over years gives the exact pathwise representation
Mission XIX describes this pointwise reserve-loss identity. The present formalisation must bridge XIX's realised-death-year indicator and reserve-derived innovation to XVI's scenario-based mortality innovation. They represent the same object when the death probabilities are calculated from the same model.
From the finite scenario lifetime law and , the annual innovations satisfy
The final factor is the conditional one-year survival probability and is essential to the fully discrete variance formula. It must not be replaced by an assumed independence condition or omitted by importing a continuous-time formula.
Taking expectations of the pathwise identity, using , yields
The variance of an insurer loss is unaffected by adding a deterministic opening reserve when the probability weights have unit total mass. Consequently,
The capstone combines these two results, with no unproved independence assumption. Its mathematical hypotheses explicitly include nonnegative, normalised scenario weights, positive in-force probability for every year in the range, and the one-year reserve recurrence with conditional rates computed from the given lifetime distribution.
The theorem remains valid at : the insurer's finite-horizon loss is deterministically , and the variance sum is empty and equals zero.
The exact final theorem is ActuarialValuation.finiteHattendorffReserveLoss_fundamental. This result is nontrivial at positive horizons. The formal model does not assert independence, fix the opening reserve to zero, or substitute a deterministic insurer loss.
The annual decomposition separates valuation assumptions from stochastic fluctuations in mortality. Shiu and Xiong's classical fully discrete treatment (https://doi.org/10.1007/s13385-020-00256-9) emphasises that a survival factor remains in each annual variance contribution. Preserving this factor makes the result useful for actuarial risk allocation and for reconciling the valuation reserve with actual finite-period insurer loss.
The finite-scenario definitions are reusable in downstream insurance valuation missions, for example multiple-decrement reserves and explicit conditional mortality shock models. The result also supplies finite boundary tests for nonzero opening reserves, death exactly at the horizon, and survival beyond the final premium year.
Annual death events arise from the same curtate lifetime, so their indicator variables have nested dependence. Their centred innovations have vanishing cross-year covariance only under the correct conditional in-force rates and probability-weighting conventions. Incorrect denominators or an unproved independence assumption would change the result.
The pathwise identity also accounts for different timing of premiums and benefits, and includes a terminal reserve for survivors. At the last covered year a policy death and survival are disjoint, so the last benefit and terminal reserve must not both be counted. The exact Lean imports must retain the definitions and parameter order of the previously published mortality and loss modules.
The Lean 4 model uses a finite scenario type with Fintype, real-valued weights, a natural-number curtate lifetime, and the published definition modules from related actuarial missions. Four new definitions and 13 Open theorem obligations form the formal graph, including 12 supporting targets before the conjunction capstone. The accepted proof status of another theorem is never inferred merely from its publication.
The result is finite horizon, finite probability space and fully discrete. The source's complete-life identity would additionally require justified limiting arguments, the disappearance (or valuation) of terminal reserves, integrability and interchange of expectation, variance and limit. None of those conditions is silently assumed here. There is no continuous-time martingale or Lévy-process result in this mission.
The classical full-life result is known mathematically, while the specific finite-horizon Lean declarations remain open proof targets. A compiler-accepted declaration with a sorry body does not establish a proof.
A bounded linear operator between Banach spaces is Fredholm if its kernel is finite-dimensional and its range is closed and of finite codimension. Its index
is an integer that survives deformation: it does not change under small perturbations or under compact perturbations, and it is additive under composition. These properties make Fredholm operators the setting for index theorems. Elliptic differential operators on compact manifolds, Toeplitz operators, linearized Cauchy–Riemann operators in symplectic topology, and the linearizations of nonlinear Fredholm maps in transversality arguments (Sard–Smale) all rest on them. Atkinson's theorem characterizes Fredholm operators as those invertible modulo compact operators. For endomorphisms this says that the image in the Calkin algebra is invertible.
This mission formalizes the abstract theory on Banach spaces over or , following N. Bourbaki, Théories spectrales, Chapitre III, §§ 3–5 (Springer, 2023). It builds on Mathlib's ContinuousLinearMap.IsFredholm, which already provides the definition and its equivalent descriptions on topological vector spaces. It adds the index and the results listed below.
is or . , , are Banach spaces over , and is the Banach space of bounded linear maps with the operator norm.
IsCompactOperator).is Fredholm if and only if there is such that and are compact (Bourbaki III, §5, Corollaire 1, TS III.74).
The result. Atkinson's theorem identifies the Fredholm operators with the units modulo the compact ideal. Together with the stability of the index under compact and small perturbations, it is the abstract input of every Fredholm index computation. Examples are the Fredholm alternative for integral equations, the index of Toeplitz operators, and the index of elliptic and Cauchy–Riemann operators on compact or punctured surfaces.
Formalizing it. Mathlib defines Fredholm operators on topological vector spaces (ContinuousLinearMap.IsFredholm) and proves that four descriptions agree (isFredholm_tfae). It has no index, no statement about compositions, and no perturbation theory. Its documentation lists the Banach-space criterion (milestone 2) and the restriction statement (milestone 5) as not yet formalized. The library built here is intended for reuse by any later index computation.
The statements combine linear algebra and topology. The index is a difference of dimensions of a subspace and a quotient space, and every statement about it carries a Fredholm hypothesis, since Module.finrank is on infinite-dimensional spaces. Openness and local constancy are statements about the operator-norm topology on , and the perturbation statements involve operators that are compact but not necessarily of finite rank. The completeness hypotheses are part of the statements: over incomplete normed spaces, a range of finite codimension need not be closed.
FredholmBanach. The definition module FredholmBanach_Setting defines only index. Fredholm operators are Mathlib's ContinuousLinearMap.IsFredholm and compact operators are Mathlib's IsCompactOperator.[RCLike 𝕜], [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E], and likewise for F and G. Bourbaki states several results for locally convex or Fréchet spaces; this mission specializes all of them to Banach spaces.index u = finrank 𝕜 u.ker - finrank 𝕜 (F ⧸ u.range) in ℤ. Module.finrank is on infinite-dimensional spaces, so index is meaningful only for Fredholm u. Every statement about it assumes u.IsFredholm.finrank 𝕜 (E ⧸ E₁), and "finite codimension" is FiniteDimensional 𝕜 (E ⧸ E₁). The restriction in milestone 5 is ContinuousLinearMap.restrict.E ≃L[𝕜] F. "Finite rank" is FiniteDimensional 𝕜 (u - e).range.Contributions welcome: reusable general-purpose lemmas about bounded and compact operators between Banach spaces.
Let be a loop of symmetric matrices. The asymptotic operator
acts on loops . It appears wherever a pseudoholomorphic curve approaches a periodic orbit. Near a puncture, a finite-energy curve in a symplectization converges to a Reeb orbit, and in a trivialization along that orbit the linearized Reeb flow is . The operator is the Hessian of the action functional at that orbit. The rate of approach and the winding of the curve around the orbit come from its eigenfunctions (Hofer–Wysocki–Zehnder 1995). In Floer theory the operator is the Hessian of the symplectic action at a -periodic orbit, and the gradient-flow operator is the linearized Floer operator (Robbin–Salamon 1995).
The operator links functional analysis to the linear algebra of stage I. is nondegenerate, i.e. is not an eigenvalue, exactly when the time-one map of the linearized flow has no eigenvalue . Then lies in and has a Conley–Zehnder index. The Fredholm index formula for Cauchy–Riemann operators on punctured surfaces is written in terms of the Conley–Zehnder indices of the asymptotic operators at the punctures (Wendl, Lectures on SFT, Lecture 3).
This is stage II of a series that formalizes the Fredholm theory of linearized Cauchy–Riemann operators. Stage I (Conley–Zehnder Index I: Axiomatic Characterization on Paths of Symplectic Matrices) characterizes the Conley–Zehnder index on . This stage sets up the spectral theory of asymptotic operators: the operator itself, self-adjointness, discrete spectrum, compact resolvent, and the dictionary between the kernel of and the time-one map. Later stages are the Fredholm theory of in Banach spaces, elliptic regularity for , and the index formula.
with its Haar probability measure. has coordinates and the Euclidean inner product, and
is continuous with for every .
For every continuous loop of symmetric matrices:
The result. These are the analytic facts that every use of asymptotic operators relies on. Self-adjointness and the discrete spectrum define the eigenvalue branches and the spectral flow. The compact resolvent makes Fredholm of index for every real , and the weighted Sobolev spaces of the later Fredholm theory are chosen with weights avoiding the spectrum. The kernel dictionary identifies nondegenerate asymptotic operators with the paths of stage I. It is the bridge through which Conley–Zehnder indices enter the index formula.
Formalizing it. All results here are classical. Mathlib has partially defined linear maps and their adjoints, the Fourier basis of on the circle, and compact operators. It has no Sobolev spaces on the circle, no unbounded operator with discrete spectrum beyond trivial cases, and no first-order differential operator treated as an unbounded operator. This stage builds the first such example. The same pattern applies to other first-order elliptic operators on , and the library is reusable for spectral flow and for Floer-type operators.
is unbounded and not defined on all of , so self-adjointness is a statement about the domain of the adjoint, not a symmetry identity. The spectral statements concern the resolvent of a first-order differential operator with non-constant coefficients, as an operator on . The kernel dictionary relates classes, defined through Fourier coefficients, to classical solutions of a linear ODE. The statements about concern linear ODEs whose coefficients are only continuous.
AsymptoticOperator; all definitions are in AsymptoticOperator_Setting, which imports stage I's ConleyZehnder_Setting (for Mat n, J₀, IsSymplectic and SP).UnitAddCircle () with AddCircle.haarAddCircle. is Lp (EuclideanSpace ℝ (Fin n ⊕ Fin n)) 2 haarAddCircle, a real Hilbert space.fourierCoeff, applied to the componentwise complexification . and act on through the real-to-complex coercion.LinearPMap, defined by choice as the map whose graph is the set of pairs satisfying the coefficient identity. The fallback is , and milestone 1 makes it unreachable. Self-adjointness is Mathlib's IsSelfAdjoint for LinearPMap, and symmetry is IsFormalAdjoint.HilbertBasis of eigenvectors whose eigenvalues tend to in absolute value along the cofinite filter. This covers , where .Contributions welcome: reusable lemmas on Sobolev spaces of vector-valued functions on the circle (Fourier characterization, continuity of functions), on unbounded self-adjoint operators with compact resolvent, and on linear ODEs with continuous periodic coefficients.
A small insurance fund or participant with limited resources can gain or lose capital repeatedly and be forced to stop at one of two barriers. This is the familiar gambler's ruin problem, useful as a discrete illustration of capital adequacy, finite-state absorption and the distinction between ruin and eventual success. Promislow's treatment derives fair and biased cases using finite capital and a bounded opponent, and Grinstead and Snell present related random-walk absorption probabilities (https://stats.libretexts.org/Bookshelves/Probability_Theory/Introductory_Probability_%28Grinstead_and_Snell%29/12%3A_Random_Walks/12.02%3A_Gambler%27s_Ruin). The practical distinction is whether a probability refers to absorption at some eventual time or only to absorption within a fixed number of additional bets.
A unit-stake capital process occupies a natural-number capital state i between zero and a positive upper barrier N. With probability p the next bet raises capital by one unit; with complementary probability one minus p it lowers capital by one unit. Capital zero and capital N are absorbing. The fair case has p equal to one-half and a linear harmonic success function. In the biased case, a down-to-up odds ratio r is defined by (1−p)/p. An additional finite-horizon model records separately the chance of hitting the upper barrier and the chance of hitting zero before a given step count, leaving unresolved paths in the interior.
The fair finite-capital eventual upper-absorption harmonic candidate is named actuarial_gamblerFairSuccess in the Lean development. A fair unit-stake random walk on capital states zero through positive target N has eventual upper-barrier success probability i/N when starting from integer capital i in the bounded interval. This source defines the harmonic candidate, not the underlying stochastic stopping-time construction.
The downward-to-upward transition probability ratio is named actuarial_gamblerOddsRatio in the Lean development. The fixed probability of an up step is p; the probability of a down step is 1−p. Their ratio (1−p)/p controls the biased harmonic solution and requires p>0 to be interpreted as transition odds.
The biased finite-capital upper-absorption harmonic candidate is named actuarial_gamblerBiasedSuccess in the Lean development. For a biased unit-stake walk with r=(1−p)/p different from one and a positive upper barrier N, the formula gives the eventual probability of hitting N before zero: (1−r^i)/(1−r^N). The denominator must be nonzero. The fair p=1/2 case requires the separate linear formula.
The probability of hitting upper capital target within finitely many steps is named actuarial_gamblerFiniteSuccess in the Lean development. The bounded random walk makes unit upward jumps with probability p and unit downward jumps with probability 1−p. It is absorbed at capital zero or at or above target N. This finite-horizon recursion records only the probability of reaching the success barrier by time n; ongoing paths at the horizon remain unresolved.
The probability of reaching zero capital within finitely many steps is named actuarial_gamblerFiniteRuin in the Lean development. The second finite-horizon recursion tracks absorption at zero capital, the ruin boundary. Successful absorption at the upper target contributes zero ruin probability. At an interior state it mixes successor ruin probabilities, and paths still active at horizon n contribute to neither finite success nor finite ruin.
The formal targets are ordered from elementary boundary and consistency claims to their combined capstone. The exact Lean identifiers below are the authoritative local targets; none of the listed theorem bodies is already accepted as a machine-checked proof. The mathematical results themselves are established actuarial or probability identities.
The declaration ActuarialValuation.gamblerFairSuccess_zero states the following relation. The fair candidate's numerator is zero at the lower absorbing boundary, so the proposed upper-barrier success probability is zero even if the target denominator is algebraically zero.
The declaration ActuarialValuation.gamblerFiniteRuin_nonneg states the following relation. Ruin starts at the boundary indicators zero or one and evolves through nonnegative weighted averages at every interior capital state. Therefore finite-horizon absorption-at-zero probability cannot be negative under valid win probabilities.
The declaration ActuarialValuation.gamblerBoundedRuin_fundamental states the following relation. The capstone formalises the correct first-step harmonic equations for the fair and biased finite-capital random walk and nonnegative bounded finite-horizon absorption-event probabilities. Unlike an infinite-horizon gambler's ruin theorem, it does not assert that every path has already been absorbed by a finite horizon or identify finite success directly with the harmonic candidate.
The exact harmonic functions identify candidate upper-absorption probabilities for fair and biased walks, while the finite-horizon recursions quantify how much absorption can have occurred after a specified number of steps. The latter distinction matters for capital planning because some solvent paths may still be active when an assessment period ends. Standard treatments show the importance of the bias ratio and the two absorbing barriers (https://stats.libretexts.org/Bookshelves/Probability_Theory/Introductory_Probability_%28Grinstead_and_Snell%29/12%3A_Random_Walks/12.02%3A_Gambler%27s_Ruin). The mathematical identities themselves are known; a Lean representation offers checkable conventions around capital zero, positive target, finite horizon and the singular fair limit. Its state-recursion definitions can be reused in finite Markov reward and insurance capital models.
The fair success expression cannot simply be obtained by substituting p=one-half into the biased quotient: both its numerator and denominator become zero. The separate linear expression needs its own fair-case convention. A second easy mistake is to regard finite-horizon success and ruin as exhaustive complementary events. They are disjoint, but an interior path may reach neither barrier during the available number of steps. At extreme probabilities zero or one, the odds ratio may be undefined or degenerate, and an eventual absorption assertion requires hypotheses not present in a finite first-step equality. These boundary distinctions are central to the stated target.
Lean uses natural numbers for capital, positive upper barrier and finite horizon, with real-valued probabilities and harmonic candidate functions. Both boundary states are absorbing; ruin is capital equal to zero, unlike the strictly negative surplus convention in another insurance reserve model. The biased quotient is used only when its normalising denominator is nonzero, and the fair case is represented separately. The source does not assert almost-sure absorption or equality of finite-horizon success with an eventual harmonic function, and it does not equate unresolved paths with failure. Mathlib finite recursion and rational function arithmetic support the scope. Reusable contributions include independent success/ruin state operators, boundary-state lemmas and nonnegative weighted continuation bounds.
The five local definitions form the available mathematical vocabulary: actuarial_gamblerFairSuccess, actuarial_gamblerOddsRatio, actuarial_gamblerBiasedSuccess, actuarial_gamblerFiniteSuccess, actuarial_gamblerFiniteRuin. Their support conditions, nonzero denominators, and variable types are fixed by the Lean declarations rather than inferred from examples. The nontrivial mathematical content must not be replaced by a vacuous premise or by a special case that bypasses the model boundaries. The existing paper mathematics is known, while these particular theorem declarations remain formalisation targets with no accepted proofs. Contributions that strengthen reusable finite identities or expose missing boundary hypotheses are appropriate, provided they preserve the exact authoritative theorem types.
S. David Promislow, Fundamentals of Actuarial Mathematics, third edition, Wiley, 2015. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/
Charles M. Grinstead and J. Laurie Snell, Introduction to Probability, American Mathematical Society, 1997. https://stats.libretexts.org/Bookshelves/Probability_Theory/Introductory_Probability_%28Grinstead_and_Snell%29/12%3A_Random_Walks/12.02%3A_Gambler%27s_Ruin
Non-proportional reinsurance allows an insurer to retain ordinary claims while transferring part of the cost of larger claims to a reinsurer. Such contracts specify both an attachment point and a maximum amount the reinsurer will pay. Confusing the retention with the limit changes ceded payments, claims reporting and the net expected treaty cost. HMRC describes common non-proportional arrangements and their layers in its general-insurance technical guidance (https://www.gov.uk/hmrc-internal-manuals/general-insurance-manual/gim8080). Pricing systems must distinguish an unlimited excess claim from the finite reimbursement available under one layer, including claims exactly at the attachment or at the upper layer boundary.
A gross claim x, attachment d and layer width L are nonnegative natural-number amounts in the same currency unit. An unlimited excess contract pays only the positive part of x minus d. A capped ceded layer pays the smaller of that gross excess and L. Amounts beyond the top of the layer, d plus L, form a separate higher excess. The expected treaty cost is evaluated under a bounded severity distribution with nonnegative mass w(x) at each integer claim amount from zero through the finite bound B. An unlimited stop-loss expected cost uses the same distribution without a layer cap.
The single-claim positive excess over an attachment is named actuarial_layerExcessLoss in the Lean development. The claim amount remaining above the insurer's retained attachment is natural-number positive-part subtraction. Below attachment it is zero, matching the gross excess payment of an unlimited stop-loss treaty.
The capped single-layer reinsurance payment is named actuarial_layerCededPayment in the Lean development. For a claim amount x, a reinsurance layer of width or limit L attaching at d reimburses the lesser of excess x−d positive part and the layer limit. It pays zero below attachment and cannot pay more than L.
The remaining gross excess above the top of the layer is named actuarial_layerHigherExcess in the Lean development. Any part of the claim above the layer's upper attachment d+L is left for higher reinsurance layers or the ultimate insurer. It is the positive excess loss above the sum of the lower attachment and the stated layer width.
The finite aggregate expected ceded loss cost of a layer is named actuarial_layerExpectedCeded in the Lean development. The finite bounded claim-severity mass model computes the net expected excess-of-loss reinsurance premium by weighting each loss payment of the capped layer by its claim probability. Expected ceded cost excludes risk loading and expenses.
The finite unlimited stop-loss expected payment is named actuarial_layerExpectedExcess in the Lean development. The net stop-loss premium above an attachment d is the finite weighted expected excess claim amount without an upper layer cap. The difference of this value at d and at d+L will equal the capped layer's expected ceded cost.
The formal targets are ordered from elementary boundary and consistency claims to their combined capstone. The exact Lean identifiers below are the authoritative local targets; none of the listed theorem bodies is already accepted as a machine-checked proof. The mathematical results themselves are established actuarial or probability identities.
The declaration ActuarialValuation.layerExcessLoss_below states the following relation. When the claim amount does not exceed the attachment, no monetary loss lies above the retention. Saturating natural-number subtraction gives zero excess exactly.
The declaration ActuarialValuation.layerExpectedCeded_stoploss_difference states the following relation. The expected capped ceded payment equals the expected unlimited excess above attachment d, less the excess above the upper layer attachment d+L. The identity follows termwise from the exact pointwise loss partition and finite linearity, with no distribution-normalisation assumption.
The declaration ActuarialValuation.layerCededValuation_fundamental states the following relation. The capstone unifies a bounded single-claim excess-of-loss treaty's payment decomposition with the exact net layer premium as difference of two unlimited stop-loss premiums, and establishes its nonnegative bound against gross excess. It does not assert an expense-loaded reinsurance price or infinite-support integration.
The difference between net unlimited excess payments at two attachments gives an immediately auditable valuation of a finite reinsurance layer. A treaty administrator can reconcile the covered amount, the higher excess and the original unlimited amount without making assumptions about claim frequencies or total policyholder losses. This separation is useful in exposure rating and in modelling multiple reinsurance towers, including arrangements described in the HMRC guidance at https://www.gov.uk/hmrc-internal-manuals/general-insurance-manual/gim8080. The identity is already a standard insurance-payment relation; formalising its finite version would produce reusable payment functions and expected-cost inequalities rather than announcing a new result about treaty markets. It would also distinguish claim indemnities from premiums loaded for operating costs and capital.
An intuitive subtraction of the reinsurance limit from the gross excess can become negative and cannot describe the remaining claim burden below the top of a layer. Likewise, a formula that gives every loss above attachment an unlimited reimbursement silently overstates the provider's maximum liability. Natural-number subtraction in Lean saturates at zero, so any stated decomposition must respect positive-part semantics at both the lower and upper treaty thresholds. There are also two independent directions of monotonicity: increased layer width raises coverage, while a larger retention generally reduces the covered part. The capstone fixes only the former and the precise difference of stop-loss expected amounts.
The source uses natural numbers for money, including the deductible and treaty limit, and real numbers for bounded claim coefficients and expected ceded payment. There is no independent hidden frequency distribution, and the finite claim grid can include zero severity and zero layer width. Nonnegative weights are explicitly required for order and positivity conclusions, while pointwise payment identities hold without probability normalisation. The formalisation does not collapse a capped layer into a trivial unlimited excess contract, nor assume an expense-loaded market premium is equal to an actuarial expectation. Reusable contributions include positive-part payments, min-limited cover, finite layer aggregation and higher-attachment functions. Later models may combine several layers or add claims-inflation adjustments.
The five local definitions form the available mathematical vocabulary: actuarial_layerExcessLoss, actuarial_layerCededPayment, actuarial_layerHigherExcess, actuarial_layerExpectedCeded, actuarial_layerExpectedExcess. Their support conditions, nonzero denominators, and variable types are fixed by the Lean declarations rather than inferred from examples. The nontrivial mathematical content must not be replaced by a vacuous premise or by a special case that bypasses the model boundaries. The existing paper mathematics is known, while these particular theorem declarations remain formalisation targets with no accepted proofs. Contributions that strengthen reusable finite identities or expose missing boundary hypotheses are appropriate, provided they preserve the exact authoritative theorem types.
S. David Promislow, Fundamentals of Actuarial Mathematics, third edition, Wiley, 2015. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/
HM Revenue & Customs, General Insurance Manual: Non-proportional reinsurance, UK government technical guidance, accessed 2026. https://www.gov.uk/hmrc-internal-manuals/general-insurance-manual/gim8080
An insurer can expect premium income to exceed claims and nevertheless become insolvent because the timing and size of claim payments are uncertain. Ruin theory asks about the chance of crossing an insolvency boundary before a specified date or eventually. The classic actuarial approach uses the distribution of yearly net cashflows and, when it exists, an exponential adjustment condition to bound risk as starting capital increases. Finite-state random walks provide a related illustration of first-passage probability and absorption (https://stats.libretexts.org/Bookshelves/Probability_Theory/Introductory_Probability_%28Grinstead_and_Snell%29/12%3A_Random_Walks/12.02%3A_Gambler%27s_Ruin). The mission isolates the finite-horizon inequality that can be stated without imposing the measure-theoretic hypotheses of an infinite stopping-time theorem.
An annual aggregate claim X is a nonnegative integer taking values zero through a fixed maximum B, with annual probabilities w(k). The insurer starts at signed integer surplus u, receives nonnegative integer premium c each year and pays an independent claim from the same finite distribution. The next signed surplus is current surplus plus c minus that claim. Strict ruin occurs as soon as surplus becomes negative, including at time zero if the initial reserve is negative. A finite-horizon ruin probability assigns one to an already-ruined state, zero to a solvent state at zero horizon, and a probability-weighted continuation at other states.
The one-period integer insurance surplus update is named actuarial_ruinNextSurplus in the Lean development. The insurer begins a period with an integer surplus, receives a fixed nonnegative integer premium, then pays the period's aggregate integer claim. The next surplus can be negative, so it is represented as an integer rather than a natural number with saturating subtraction.
The total annual claim probability on a bounded integer grid is named actuarial_ruinClaimMass in the Lean development. The finite annual aggregate-claim model has possible integer loss amounts 0 through B. Its total probability is the sum of those coefficients, required to equal one in the genuine probability interpretation of the recursion.
The exponential moment of one period's net insurance loss is named actuarial_ruinAdjustmentMoment in the Lean development. The adjustment coefficient R compares the annual aggregate claim X with the premium c via the exponential moment E[exp(R(X−c))]. When this quantity is no greater than one and R≥0, the exponential capital bound becomes a supermartingale-style one-step estimate.
The lundberg exponential benchmark for an integer initial surplus is named actuarial_ruinExponentialBound in the Lean development. The benchmark at current surplus u is exp(−Ru). For R≥0 this is at least one if u is negative, allowing it to bound an already-ruined state whose ruin indicator equals one; for a nonnegative initial reserve it falls exponentially with additional starting capital.
The first-passage ruin probability over a finite number of annual periods is named actuarial_ruinProbabilityFinite in the Lean development. The probability of ruin by horizon n records whether surplus was ever strictly negative. Already-ruined integer states have probability one at any horizon. Otherwise the next-year claim distribution mixes the ruin probabilities of all possible updated signed surpluses, recursively for n further years. The horizon is finite and annual claims are modelled as conditionally independent copies of w.
The formal targets are ordered from elementary boundary and consistency claims to their combined capstone. The exact Lean identifiers below are the authoritative local targets; none of the listed theorem bodies is already accepted as a machine-checked proof. The mathematical results themselves are established actuarial or probability identities.
The declaration ActuarialValuation.ruinNextSurplus_zero_claim states the following relation. If the insurance portfolio generates no claim payment during a period, only the fixed premium c affects the insurer's capital. The signed next-period surplus is therefore the old surplus plus the earned premium.
The declaration ActuarialValuation.ruinProbabilityFinite_le_one states the following relation. With an annual claim mass function summing to one, every solvent state averages predecessor-horizon ruin probabilities with nonnegative weights of total one. Since the base and already-ruined values lie at most one, induction establishes that the finite-horizon ruin probability never exceeds one.
The declaration ActuarialValuation.ruinFiniteHorizon_fundamental states the following relation. The capstone formalises a bounded annual integer-claim surplus recursion with an absorbing strict-negative ruin condition. Proper nonnegative annual claim probabilities keep finite-horizon ruin probability within the unit interval. A nonnegative exponential adjustment parameter satisfying E[exp(R(X−c))]≤1 then bounds it by exp(−Ru) for every finite horizon and signed starting capital.
A valid exponential upper bound gives a transparent relationship between initial capital and probability of failure over every finite number of years. It can be used to compare capital buffers or to test an insurer's response to a changed premium and annual claims distribution. The bounded recursive setting is particularly relevant when annual severity is itself computed by exact portfolio convolution. Classical first-passage models distinguish eventual absorption from a finite-horizon crossing event (https://stats.libretexts.org/Bookshelves/Probability_Theory/Introductory_Probability_%28Grinstead_and_Snell%29/12%3A_Random_Walks/12.02%3A_Gambler%27s_Ruin). The formal target is the known exponential comparison property, not a new adjustment-root existence result. It yields reusable recursion and exponential-moment definitions for subsequent finite insurance reserve analysis.
A tempting representation of surplus as a natural number is incorrect for insolvency, because saturating subtraction hides the negative state that defines ruin. A second mistake is to present the exponential capital function as an unconditional bound. It can fail when the claim-loss exponential moment exceeds one, even in a deterministic one-year example. The argument also needs the negative-surplus boundary, at which ruin probability is already one. These complications are visible at finite horizons and cannot be repaired merely by assuming that premium income has a positive expected margin.
The Lean source uses signed integers for surplus and natural numbers for annual claim amounts, premium, severity bound and horizon. Annual probabilities and adjustment exponent are real. The event is strictly negative first-passage ruin, distinct from reaching exactly zero in a gambler's ruin model. A nonnegative adjustment exponent and an explicit upper bound of one on its net-claim exponential moment are mandatory. The source gives the finite recursive quantity algebraically, not an independently constructed probability space, an infinite-horizon supremum or a theorem that a positive adjustment root exists. Reusable developments include finite weighted expectation operators, signed reserve transitions and nonnegative probability bounds; meaningful contributions may extend these to random premiums or general annual claim distributions.
The five local definitions form the available mathematical vocabulary: actuarial_ruinNextSurplus, actuarial_ruinClaimMass, actuarial_ruinAdjustmentMoment, actuarial_ruinExponentialBound, actuarial_ruinProbabilityFinite. Their support conditions, nonzero denominators, and variable types are fixed by the Lean declarations rather than inferred from examples. The nontrivial mathematical content must not be replaced by a vacuous premise or by a special case that bypasses the model boundaries. The existing paper mathematics is known, while these particular theorem declarations remain formalisation targets with no accepted proofs. Contributions that strengthen reusable finite identities or expose missing boundary hypotheses are appropriate, provided they preserve the exact authoritative theorem types.
S. David Promislow, Fundamentals of Actuarial Mathematics, third edition, Wiley, 2015. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/
Charles M. Grinstead and J. Laurie Snell, Introduction to Probability, American Mathematical Society, 1997. https://stats.libretexts.org/Bookshelves/Probability_Theory/Introductory_Probability_%28Grinstead_and_Snell%29/12%3A_Random_Walks/12.02%3A_Gambler%27s_Ruin
Insurers model annual claim frequency to price collections of policies and assess how often unusually large numbers of claims may arrive together. A Poisson count model has equal mean and variance, but heterogeneity between policyholders can produce materially more dispersion. The negative-binomial family is an established alternative, including as a marginal count law obtained by mixing the Poisson intensity over a Gamma distribution. The mathematical relationship, with explicit Gamma shape and rate parameters, is set out in the Stanford discussion of mixture models (https://web.stanford.edu/class/bios221/MixtureLecture.html). A reliable formal description must specify which negative-binomial probability parameter is being used, since actuarial and statistical literature adopt incompatible success and failure conventions.
A negative-binomial count variable N records a nonnegative integer number of claims. The integer shape parameter r is strictly positive, and a real count probability parameter p lies between zero and one, with the upper endpoint excluded when calculating moments. In this convention p is associated with powers of the claim count n, while 1 minus p is associated with powers of the shape r. The Gamma-mixed Poisson model starts from a Gamma-distributed intensity with positive rate beta and integer shape r; at one future exposure unit its negative-binomial count parameter equals the reciprocal of beta plus one.
The negative-binomial claim count coefficient is named actuarial_negBinCountMass in the Lean development. Defines a negative-binomial frequency coefficient for n claims and positive integer shape r, with p the count probability parameter and 1−p the Bernoulli success probability. The finite choose expression is mathematically the conventional formula only for shape r≥1.
The expected claim count under nb size and count parameter is named actuarial_negBinCountMean in the Lean development. For 0≤p<1 and positive integer shape, the negative-binomial mean count equals r p divided by one minus p. This p denotes count rather than Bernoulli success probability, so the formula differs from sources that reverse the parametrisation.
The negative-binomial count variance is named actuarial_negBinCountVariance in the Lean development. For valid negative-binomial parameters, the variance exceeds the mean because uncertainty in the Poisson event frequency introduces additional dispersion. The exact variance is r p divided by (1−p) squared.
The unit-exposure gamma-poisson predictive count parameter is named actuarial_negBinGammaProbability in the Lean development. A Gamma mixing distribution with positive rate beta and positive integer shape yields a negative-binomial mixed-Poisson count law at one exposure unit with the count parameter p=1/(beta+1). This is the reciprocal rate-plus-one, not beta/(beta+1), which is the complementary success parameter.
The integer-shape gamma-poisson predictive count coefficient is named actuarial_negBinGammaPredictive in the Lean development. The model uses a shape/rate Gamma prior for a Poisson rate at unit exposure. The predictive count mass is the integer-shape negative-binomial coefficient evaluated at the rate-derived count parameter. The declaration encodes the known mixture result algebraically without asserting an integral identity.
The formal targets are ordered from elementary boundary and consistency claims to their combined capstone. The exact Lean identifiers below are the authoritative local targets; none of the listed theorem bodies is already accepted as a machine-checked proof. The mathematical results themselves are established actuarial or probability identities.
The declaration ActuarialValuation.negBinGammaProbability_pos states the following relation. Prior Gamma rate b positive implies denominator b+1 strictly positive, so its reciprocal is a valid strictly positive negative-binomial count parameter.
The declaration ActuarialValuation.negBinGammaMean_unit_exposure states the following relation. The frequency mean for the negative-binomial predictive law derived from a Gamma shape/rate prior at one future exposure is shape divided by rate. This agrees with the prior Gamma mean Poisson intensity, not shape times rate.
The declaration ActuarialValuation.negBinClaimFrequency_fundamental states the following relation. The capstone combines the exact integer-shape negative-binomial count-mass recursion and the unit-exposure Gamma-Poisson mixture parameterisation. It verifies both predictive moments and coefficient nonnegativity, without claiming an infinite PMF normalisation proof or a Gamma mixture integral in Lean.
The ability to compute neighbouring frequency coefficients from one another supports actuarial claim-table construction without repeatedly evaluating large factorial ratios. The difference between count variance and mean provides a direct overdispersion diagnostic when comparing heterogeneous risks with a Poisson benchmark. Under a Gamma prior, the mixed frequency mean and variance recover the Gamma shape/rate moments, linking pricing assumptions to uncertainty in latent risk intensity. Panjer's work on recursive compound distribution evaluation shows why stable frequency recurrences matter for downstream aggregate insurance claims (https://doi.org/10.1017/S0515036100006796). The results are known mathematics; an exact formalisation would make the parameter conventions and real-valued boundary assumptions machine checkable and provide coefficient lemmas reusable by collective-risk computations.
The main hazard is a parameterisation mismatch. Some publications place p on the Bernoulli success count and others put p on the recorded total of failures or claims; the mean and Gamma mapping change accordingly. The integer-binomial coefficient must also be interpreted with positive shape: allowing r=0 while retaining the expression choose(n+r−1,n) introduces natural subtraction at a degenerate boundary. Moment formulas include one-minus-p in a denominator and therefore cannot be stated as ordinary probability facts at p=1. Finally, the algebraic coefficient sequence alone does not supply a probability-space proof that Gamma integration produces the count law.
The Lean representation uses natural numbers for integer shape and count, and real numbers for the probability parameter, Gamma prior rate and moment expressions. The combinatorial coefficient is Nat.choose, and all arithmetic is within Mathlib. The zero-shape index is excluded from the conventional distribution claim, although some sign statements remain algebraically valid there. This mission does not assert an infinite normalisation sum, an unrestricted non-integer shape model or a vacuous Gamma-mixture identity proved by defining the mixture as the desired result. Reusable contributions include count-ratio recurrences, nonnegative binomial coefficient calculations and parameter conversion lemmas. Future work could connect those components to a genuine Gamma integral or a separately formalised Panjer aggregate recursion.
The five local definitions form the available mathematical vocabulary: actuarial_negBinCountMass, actuarial_negBinCountMean, actuarial_negBinCountVariance, actuarial_negBinGammaProbability, actuarial_negBinGammaPredictive. Their support conditions, nonzero denominators, and variable types are fixed by the Lean declarations rather than inferred from examples. The nontrivial mathematical content must not be replaced by a vacuous premise or by a special case that bypasses the model boundaries. The existing paper mathematics is known, while these particular theorem declarations remain formalisation targets with no accepted proofs. Contributions that strengthen reusable finite identities or expose missing boundary hypotheses are appropriate, provided they preserve the exact authoritative theorem types.
S. David Promislow, Fundamentals of Actuarial Mathematics, third edition, Wiley, 2015. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/
Harry H. Panjer, Recursive evaluation of a family of compound distributions, ASTIN Bulletin, 1981. https://doi.org/10.1017/S0515036100006796
A pair of insurance portfolios can have the same expected aggregate claim while requiring different ceded premiums or capital to withstand severe outcomes. Expected loss alone cannot identify the difference: the distribution of loss across small and large events also matters. The stop-loss order compares expected loss above every retention level and provides a concrete way to rank riskiness for excess-of-loss contracts. Müller studied wider relationships among such risk orders and their stop-loss transforms (https://doi.org/10.1016/0167-6687(96)90002-5). The present object is a local, explicit change in an integer loss distribution that preserves its first moment but shifts probability from a middle amount towards two neighbouring outcomes.
A bounded aggregate-loss distribution has nonnegative coefficients w(s) for integer losses s between zero and a finite maximum B, with total coefficient mass usually equal to one. Its gross expected claim is the weighted sum of loss amounts and its stop-loss premium at integer deductible d is the expected positive excess above d. A proposed new coefficient array moves an amount delta out of one interior integer claim centre c, placing equal halves at the adjacent claim sizes c minus one and c plus one. Strictly positive centre and a top neighbour no higher than B keep the change within the declared support.
The bounded discrete expected excess above an integer attachment is named actuarial_orderStopLossPremium in the Lean development. The actuarial stop-loss transform multiplies each aggregate loss's excess over the attachment point by its real coefficient and sums over the finite covered loss grid. A nonnegative probability mass law gives its net excess-of-loss reinsurance premium.
The bounded aggregate loss expectation is named actuarial_orderAggregateMean in the Lean development. The finite aggregate claims mean uses the claim amount at each integer index as its payment and multiplies it by its probability mass. Comparing mean claims is necessary when interpreting stop-loss order as mean-preserving convex order.
The aggregate probability within a finite loss bound is named actuarial_orderAggregateMass in the Lean development. The sum of all coefficients on the finite aggregate-loss support is the bounded probability mass, whose value is one for a normalised distribution. An explicit mass operator makes the mean-preserving spread's total-mass conservation separately checkable.
The mean-preserving symmetric transfer from one claim amount to adjacent values is named actuarial_orderNeighbourSpread in the Lean development. A fixed amount δ of probability mass is moved away from an interior integer claim level centre: half is allocated one unit below, and half one unit above. Under 1≤centre and centre+1≤B these three loss levels lie within the support and the transfer preserves the aggregate mean.
The finite-grid stop-loss ordering of aggregate risks is named actuarial_orderStopLossDominates in the Lean development. The first aggregate loss distribution is no riskier in stop-loss order than the second when its expected excess payment never exceeds the other's for any integer attachment d. Equal means and unit total masses can be imposed separately to obtain a mean-preserving spread interpretation.
The formal targets are ordered from elementary boundary and consistency claims to their combined capstone. The exact Lean identifiers below are the authoritative local targets; none of the listed theorem bodies is already accepted as a machine-checked proof. The mathematical results themselves are established actuarial or probability identities.
The declaration ActuarialValuation.orderStopLossPremium_zero states the following relation. Since every nonnegative integer loss exceeds or equals attachment zero, the stop-loss payment equals the gross loss in each scenario. Thus the expected excess premium at attachment zero coincides exactly with the original aggregate expected claim.
The declaration ActuarialValuation.orderNeighbourSpread_stoploss states the following relation. The payment function (s−d) positive-part is convex in the claim amount s. Transferring nonnegative mass symmetrically from centre to its adjacent lower and higher losses can only increase its expected value, with a difference equal to δ/2 times the nonnegative discrete second difference at c.
The declaration ActuarialValuation.orderNeighbourSpread_fundamental states the following relation. The capstone shows that a feasible symmetric probability transfer to adjacent losses produces a valid nonnegative bounded coefficient distribution, preserves the aggregate total probability and mean, yet weakly raises every stop-loss expected excess premium. This is an explicit constructive mean-preserving spread and a finite-lattice convex-order result.
A mean-preserving spread separates the effect of greater claim variability from a change in the underlying expected loss. By conserving total mass and gross mean, the comparison can be attributed to the redistribution of outcomes rather than an increase in total claim cost. Its downstream consequence is a weak rise in the expected ceded payout for every positive-part reinsurance retention. This connects aggregate frequency/severity valuation to ordered risks and tail measures, consistent with wider stop-loss ordering results studied in https://doi.org/10.1016/0167-6687(96)90002-5. Formalising the finite construction provides a reusable bounded-grid example of stochastic-order consequences without requiring an axiomatic treatment of all convex functions.
The obvious claim that any symmetric redistribution increases expected excess is false if the transfer is allowed to cross the boundary of the support or remove more probability than the central cell contains. At centre zero the intended lower neighbouring loss is negative and no longer exists in a natural-number grid. If delta exceeds the centre's initial coefficient, the resulting array is not a probability distribution. Equality of expected claim amounts by itself also does not imply stop-loss order. The formal statement must account for the actual positive-part payment at each possible deductible, including deductions outside the claim support.
Lean represents loss indices, attachment points and the spread centre as naturals, and probability coefficients and expected claims as reals. The claim grid is finite, and the full probability-normalisation equation is separate from local mass conservation. The capstone explicitly requires nonnegative starting coefficients and a feasible interior transfer. It does not substitute a trivial comparison between identical distributions, nor claim general continuous convex order or a complete converse representation of risk ordering. Mathlib finite sums and arithmetic over nonnegative parts are enough for the declared scope. Reusable infrastructure includes finite aggregate means, bounded mass totals and stop-loss order on arrays, suitable for later reinsurance layers and capital-risk measures.
The five local definitions form the available mathematical vocabulary: actuarial_orderStopLossPremium, actuarial_orderAggregateMean, actuarial_orderAggregateMass, actuarial_orderNeighbourSpread, actuarial_orderStopLossDominates. Their support conditions, nonzero denominators, and variable types are fixed by the Lean declarations rather than inferred from examples. The nontrivial mathematical content must not be replaced by a vacuous premise or by a special case that bypasses the model boundaries. The existing paper mathematics is known, while these particular theorem declarations remain formalisation targets with no accepted proofs. Contributions that strengthen reusable finite identities or expose missing boundary hypotheses are appropriate, provided they preserve the exact authoritative theorem types.
S. David Promislow, Fundamentals of Actuarial Mathematics, third edition, Wiley, 2015. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/
Alfred Müller, Orderings of risks: A comparative study via stop-loss transforms, Insurance: Mathematics and Economics, 1996. https://doi.org/10.1016/0167-6687(96)90002-5
Insurers routinely estimate next-period frequency from policyholders who have accumulated unequal historical exposure. A raw observed rate can swing markedly when the exposure base is small, while a collective rate may ignore evidence of persistent individual risk differences. The Gamma–Poisson model gives a precisely defined compromise: a posterior expected claim intensity that responds to observed counts and earned exposure. The literature on credibility analysis documents the distinction between process variation and variation across risks, including the role of Bayesian conjugacy (https://openacttexts.github.io/LDAVer2/ChapCredibility.html). The relevant question is how the posterior parameters and credibility premium behave under sequential reporting, zero-data boundaries and different exposure amounts.
The latent claim frequency is measured in expected events per insured exposure unit. A Gamma prior has shape alpha greater than zero and rate beta greater than zero, so beta is the reciprocal of the Gamma scale. Conditional on this frequency, the observed number of claims C is Poisson with mean equal to exposure E times the intensity. Distinct observed blocks contribute counts C and D and exposures E and F. The formal declarations use natural numbers for counts and real numbers for rates, exposures and expected frequencies. The posterior shape/rate update and credibility-weight equations are the objects of the stated algebraic model.
The gamma posterior shape after observing claim count is named actuarial_gammaPoissonPosteriorShape in the Lean development. The Gamma prior uses the shape-and-rate parameterisation and starts with prior shape α. Observing a nonnegative integer aggregate count C increases the posterior shape to α+C. This is an algebraic conjugacy update rather than a complete formalisation of the Gamma probability density.
The gamma posterior rate after exposure volume is named actuarial_gammaPoissonPosteriorRate in the Lean development. The Gamma distribution's second parameter is a rate, not a scale. The posterior rate is prior rate β plus observed insured exposure E; this explicit convention prevents the common reciprocal-scale error in Poisson-Gamma credibility.
The posterior expected claim frequency per exposure unit is named actuarial_gammaPoissonPosteriorMean in the Lean development. For a Poisson count model and shape/rate Gamma prior, the posterior expected frequency per unit exposure is updated shape divided by updated rate. Positive prior rate and nonnegative exposure ensure an ordinary positive denominator.
The exposure-dependent exact bayesian credibility coefficient is named actuarial_gammaPoissonExperienceWeight in the Lean development. The exact credibility weight in the Poisson-Gamma conjugate model is E divided by β+E. When β>0 and E≥0 this lies between zero and one, approaching greater reliance on claim experience as accumulated exposure increases.
The weighted experience and collective frequency is named actuarial_gammaPoissonCredibilityBlend in the Lean development. The credibility premium combines observed aggregate claims per unit exposure C/E and the Gamma prior population frequency α/β, with respective weights E/(β+E) and β/(β+E). The usual representation requires E>0 and β>0; at zero exposure the claim rate C/E is not a valid observed experience statistic.
The formal targets are ordered from elementary boundary and consistency claims to their combined capstone. The exact Lean identifiers below are the authoritative local targets; none of the listed theorem bodies is already accepted as a machine-checked proof. The mathematical results themselves are established actuarial or probability identities.
The declaration ActuarialValuation.gammaPoissonPosteriorShape_zero states the following relation. When no claims are observed, the sufficient statistic added to the shape is zero. The updated Gamma posterior shape therefore equals its prior shape, even before imposing positivity required by the probabilistic model.
The declaration ActuarialValuation.gammaPoissonCredibilityBlend_exact states the following relation. With positive prior rate and positive observed exposure, the observed claim frequency and collective mean are both well-defined. Substituting weight E/(β+E) and simplifying proves the exact Bayesian credibility decomposition of posterior mean (α+C)/(β+E).
The declaration ActuarialValuation.gammaPoissonCredibility_fundamental states the following relation. The capstone combines exact Gamma-Poisson experience credibility at positive exposure with associative sequential count/exposure updates and admissibility of the Bayesian experience weight. It formalises the conjugate-model parameter and premium algebra without claiming a full measure-theoretic Gamma likelihood integral.
Exact agreement between the posterior mean and the collective/individual premium blend allows underwriting calculations to be reconciled across reporting intervals. Exposure aggregation must not alter the end-of-period estimate when the underlying sufficient statistics are unchanged. The additional Gamma predictive parameter variance explains why a future claim count can exhibit dispersion beyond that of a Poisson distribution with deterministic intensity. These are established properties of conjugate credibility models, rather than new claims about the existence of a posterior distribution; the mathematical background is described in https://openacttexts.github.io/LDAVer2/ChapCredibility.html. The formal output would certify the numeric parameter identities and boundary assumptions in Lean, allowing subsequent developments to reuse the same frequency and credibility conventions.
The common failure is to confuse a Gamma rate with a Gamma scale: this reverses the update and the ratio used as the experience credibility weight. Another false shortcut is to take the product of a zero exposure weight and an undefined observed count divided by zero as a meaningful zero experience contribution. Those algebraic terms are distinguishable in Lean's totalised division and in actuarial modelling. The exact mixture identity needs positive observed exposure, whereas the no-data statement requires both zero exposure and zero observed claims. Strict positivity is also essential when the total rate appears in a denominator.
The Lean development uses Mathlib real arithmetic and natural claim counts. The source represents the posterior parameter update directly and does not formalise an underlying Gamma density, conditional-expectation kernel or integration proof of conjugacy. In particular, no vacuous statistical assumption is allowed to stand in for a parameter identity, and the nonzero-exposure requirement is retained where observed frequency occurs. Reusable contributions include real-valued exposure-ratio identities, independent positivity facts, sequential sufficient-statistic updates and sharply stated data boundaries. Further work could construct the probability-space interpretation or the negative-binomial predictive count law without changing the current capstone.
The five local definitions form the available mathematical vocabulary: actuarial_gammaPoissonPosteriorShape, actuarial_gammaPoissonPosteriorRate, actuarial_gammaPoissonPosteriorMean, actuarial_gammaPoissonExperienceWeight, actuarial_gammaPoissonCredibilityBlend. Their support conditions, nonzero denominators, and variable types are fixed by the Lean declarations rather than inferred from examples. The nontrivial mathematical content must not be replaced by a vacuous premise or by a special case that bypasses the model boundaries. The existing paper mathematics is known, while these particular theorem declarations remain formalisation targets with no accepted proofs. Contributions that strengthen reusable finite identities or expose missing boundary hypotheses are appropriate, provided they preserve the exact authoritative theorem types.
S. David Promislow, Fundamentals of Actuarial Mathematics, third edition, Wiley, 2015. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/
OpenActTexts contributors, Loss Data Analytics: Experience Rating Using Credibility Theory, online actuarial textbook, accessed 2026. https://openacttexts.github.io/LDAVer2/ChapCredibility.html
Multistage stochastic programs model sequential decisions under uncertainty: hydro-thermal scheduling, portfolio management and capacity planning are standard examples. Their dynamic programming equations involve recourse functions (cost-to-go functions) of the decision history, which cannot be computed exactly. Stochastic Dual Dynamic Programming (SDDP), introduced by Pereira and Pinto in 1991, approximates each recourse function from below by a maximum of affine cuts, built at trial points generated by simulating sampled scenarios. SDDP is the method of choice in the energy industry for long-horizon stochastic planning.
Two extensions motivate this mission. Risk-averse planning replaces the expectation at each stage by a coherent risk measure (for instance the Conditional Value-at-Risk), and many applications have convex but nonlinear stage problems. Guigues (2016) proves that the risk-averse sampling algorithm for convex stage problems converges almost surely.
Timeline.
There are stages with decisions and a given . A history is identified with the vector with its Euclidean norm. The random data are interstage independent (H1). For , takes values with probabilities , and is deterministic. A realization consists of a cost with values in , convex constraints and linear constraints . Together with a compact set , they define the feasible set .
The risk measure of stage is given in dual form,
The recourse functions satisfy and, for ,
The first-stage value is . Assumption (H2) requires convexity, lower semicontinuity and properness of the data, and fixes an such that the costs are finite and the feasible sets nonempty on the -fattening . It also asks for a relative-interior point of the nonlinear constraints.
Algorithm 1 keeps cutting-plane models , starting from . At iteration it computes decisions at every node of the scenario tree, by solving the stage problems with in place of . It then samples one scenario , with indices satisfying the independence assumption (H3), and adds at each sampled node one cut
Here attains the supremum in , and is a subgradient of .
Almost surely, for and every node of stage ,
Almost surely, moreover, , and every accumulation point of the first-stage decisions is an optimal solution of the first-stage problem.
Theorem 4.1 guarantees that the algorithm's lower bound converges to the true risk-averse optimal value, and that its first-stage decisions approach optimal ones. It covers nonlinear convex stages, where finite convergence arguments for polyhedral problems do not apply. It also covers every risk measure with a dual representation, including CV@R and its combinations with expectation. Practitioners rely on this to justify stopping rules based on the lower bound.
The result is proved on paper. To our knowledge neither Theorem 4.1 nor its risk-neutral counterpart (Girardeau–Leclère–Philpott, Theorem 3.1) has been machine-checked; the risk-neutral statements are posed, unproved, on this platform. A formalization would check a proof that combines convex analysis (value functions of convex programs, subgradient bounds, Lipschitz continuity on fattenings), cutting-plane bookkeeping and a probabilistic argument (strong law of large numbers along a predictable subsequence).
The cuts are built only along sampled scenarios, so at a given node the approximation is refined only at the iterations whose scenario passes through it. The obvious induction argument controls the error only along those iterations. Extending it to all iterations is the probabilistic core (4.29). It needs the samples to be independent of everything the algorithm has computed so far, and it needs a strong law of large numbers along the subsequence of iterations at which the error is still large. A second difficulty is passing from the current model to the previous one . This needs uniform Lipschitz bounds on the models (Lemmas 3.2, 3.5), which in turn rest on the fattening in (H2) and on the subgradient bound of Proposition 2.2.
PiLp 2), so fattenings, inner products and Lipschitz constants use the Euclidean norm on . Fattenings are closed thickenings.EReal, infima are on empty feasible sets, and weights are real numbers (with ). Limits of gaps are taken in EReal, so that convergence to forces the gaps to become finite.run_exists shows that under (H2), with closed , rules producing a run exist for every sample path.Multistage stochastic programs model decisions taken over time while uncertain data are revealed: generation scheduling in hydro-thermal power systems, capacity expansion, unit commitment, portfolio management. When the uncertainty is represented by a finite scenario tree, the problem becomes one very large deterministic program, and decomposition algorithms solve it stage by stage. For linear problems the standard methods are nested Benders decomposition and its sampling variant, stochastic dual dynamic programming (SDDP), introduced by Pereira and Pinto (1991). Both rely on the convexity of the value functions, which they approximate from below by linear cuts.
Many applications need integer decisions (on/off status of generators, investment choices), and integer variables destroy convexity. Zou, Ahmed and Sun (Math. Program. 175 (2019) 461–502) observed that when the state variables passed between stages are binary, exact convex polyhedral representations still exist on the binary points. They proposed stochastic nested decomposition (SND) and its stage-wise independent special case SDDiP, and identified three properties of cuts (valid, tight, finite) under which the algorithms converge. This mission formalizes that convergence theorem, Theorem 2 of the paper.
Timeline. Birge (1985) gave nested decomposition for multistage linear programs; Pereira and Pinto (1991) introduced SDDP. Philpott and Guan (2008) proved almost sure finite convergence of SDDP-type methods for linear problems, and Girardeau, Leclère and Philpott (2015) extended convergence to convex problems. Zou, Ahmed and Sun (2019) proved finite convergence with probability one for mixed integer problems with binary states and abstract valid, tight and finite cuts, and showed that their Lagrangian cuts have the first two properties.
Let be a scenario tree with stages , root , parent map and children . The nodes of the last stage are the scenarios. Node probabilities satisfy , , and before the last stage, and . Each node has a linear cost and a nonempty compact mixed integer polyhedral set (assumption (A1)). The state is binary, the local variables are general, and the root's parent state is fixed. The problem in local-copy form (2.1) is
Its value functions satisfy the recursion (2.3): over the nodal feasible set, with the expected cost-to-go function .
The SND algorithm keeps an under-approximation of each : the maximum of a lower bound and the aggregated cuts collected so far (3.2). Each iteration samples scenarios with replacement. In the forward step it solves the nodal problems from the root down, which yields the forward tree solution of (3.6). In the backward step, at every sampled node it generates one cut per child at the state and adds their aggregate to . Cuts are valid if on (3.4). They are tight if they equal the value of the child's updated nodal problem at (3.5). They are finite if only finitely many distinct cuts occur. Assumption (A3) requires the nodal solver to return the same optimal solution whenever it is given the same problem.
With sampling with replacement, valid, tight and finite cuts, and a solver satisfying (A3), the following holds with probability one:
Theorem 2 separates the convergence of nested decomposition from the choice of cuts. Any cut family with the three properties yields an exact algorithm for multistage stochastic integer programs with binary states. The paper verifies the properties for integer optimality cuts and, through its Theorem 3, shows that Lagrangian cuts from the local-copy reformulation are valid and tight. The convergence of SDDiP, the variant used in computations, follows from the same theorem, and binary expansion of general integer states extends the reach to mixed integer state spaces.
The result is proved in the paper; no machine-checked proof exists. A formal development would turn its informal points into checked statements: that the minima are attained, that the DP recursion is equivalent to the extensive form, and that the finiteness of cuts is global. It would also supply a reusable framework (scenario trees with node probabilities, cut-based approximations, sampled runs) for the convergence theory of SDDP-type methods.
No single step is deep; the difficulty is the interaction of the pieces. A tempting argument says the approximations stop changing, so the algorithm stops at an optimum. But a stalled run need not be optimal: if a node at which is inexact is never sampled again, nothing changes and the forward solution stays suboptimal. The proof must therefore combine three things: the deterministic finiteness of changes, an almost sure statement about sampling, and the exactness chain (3.8). That chain depends on tightness with respect to the updated approximation of the child, and it fails if tightness refers to the approximation from before the backward step. The equivalence between optimality for the DP recursion and for the extensive form (2.1), used without proof in Claim 1, also requires a backward induction over the tree.
The tree is the platform definition StochasticProg.Multistage.Tree H, with stage of the paper equal to stage = t − 1. Binary vectors are Fin d → Bool, embedded in . The copy variable is eliminated through . Minima are written as infima over sets that the standing assumptions make nonempty, bounded below and attained. Lean iterations are numbered from , and the run is infinite (stopping criteria and bounds play no role).
Readings of informal words. "Optimal solution of (2.1)" means a feasible tree solution of least cost among all feasible tree solutions. "After a finite number of iterations" means from some iteration on, in every iteration (∀ᶠ i in atTop). "With probability one" refers to a probability space carrying independent draws, per iteration, each with law . "Finite" cuts means one finite set for the whole run, as the proof uses it, not a different finite set per iteration. (A3) means the solver is a function of the node, the parent state and the approximation, and returns an optimal solution.
Added hypotheses, which the paper uses without stating them: ; every nodal problem is feasible for every binary parent state, which replaces (A2) (not used by Theorem 2); and the lower bounds under-estimate, , which is Algorithm 1's "initial under-approximation".
Trivializing formalizations are ruled out: tightness refers to the child's approximation after its own update, optimality is for the true extensive form and not relative to , and the probability statement is over independent sampling, not over a fixed sample sequence assumed to visit every scenario.
Contributions welcome: the attainment lemmas for nodal minima, the DP/extensive-form equivalence on trees, and the second Borel–Cantelli argument for repeated sampling. All of these are reusable for other SDDP-type convergence results.
A data center or cloud platform routes each incoming task to one of parallel servers. Sending each task to a server with the shortest queue, the join-the-shortest-queue (JSQ) policy, minimizes waiting in a strong sense, but the dispatcher must learn all queue lengths for every arrival. The power-of-d schemes cut this communication: the dispatcher samples servers and joins the shortest of them. Mukherjee, Borst, van Leeuwaarden and Whiting ask how large must be for the sampled scheme to perform as well as JSQ as . They answer at two scales. At the fluid scale (mission 1 of this series) suffices. At the diffusion scale of the Halfin–Whitt regime, the subject of this mission, suffices, and does not.
Timeline:
There are servers, each with a buffer of size that counts the task in service. Tasks arrive as a Poisson process of rate , and each needs a unit-mean exponential amount of work, served at unit rate. A task sent to a full server is discarded. Under JSQ(d) the dispatcher samples servers without replacement () and sends the task to a server with the shortest queue among them. For this is JSQ.
The state is the occupancy vector , where is the number of servers with at least tasks. The conventions are and for . With the servers ordered by nondecreasing queue length, the -th ordered server has queue length . An arrival at position raises by one when . A departure at position lowers by one when . JSQ(d) routes to the smallest position in a uniform -subset of .
In the Halfin–Whitt regime , the diffusion-scaled state is
Here is the scaled number of idle servers.
Let , and . Assume for large and . If , then in , where for and
Here is a standard Brownian motion and is the nonnegative nondecreasing regulator with . The goal also asserts that this solution is unique.
The goal follows from 1–3.
The result. Theorem 2.4 shows that queue-length queries per arrival already achieve diffusion-level optimality: over any finite horizon only servers are idle and only hold two or more tasks, exactly as under JSQ. With Theorem 2.5 it identifies as the minimal order of . The diffusion limit is also the input for the steady-state analyses of JSQ in this regime (Braverman; Banerjee and Mukherjee).
Formalizing it. The result is proved on paper; nothing in it is machine-checked. A formalization needs:
The Eschenfeldt–Gamarnik limit (milestone 2) is cited by the paper, not proved in it, so its formalization is a separate, substantial contribution.
JSQ(d(N)) cannot be compared with JSQ path by path. The same arrival is routed to different servers under the two schemes, so their occupancy vectors drift apart and do not stay ordered. The obvious generator-based diffusion argument for JSQ(d(N)) itself does not close either. The routing probabilities depend on the whole ordered queue-length profile through -type terms, and these do not reduce to a function of at scale unless is large enough.
The threshold is sharp: for the limit is different (Theorem 2.5). Any argument therefore has to use the growth rate quantitatively, controlling at scale over a finite horizon how often JSQ(d(N)) fails to make a near-shortest choice. A qualitative fluid-type argument cannot do this. A second difficulty is the limit itself: (2.4) is a reflected equation whose regulator enters two coordinates, so even its well-posedness needs a Skorokhod-type argument with feedback.
Lean conventions:
Q i is for , with Q 0 = N, and positions are . The initial vector Fin k → ℝ lists levels .b : ℕ∞ with 2 ≤ b; ⊤ is an infinite buffer.expMeasure (λ + N) interarrival times through the published renewalCount/partialSum. Its i.i.d. marks are arrivals, with probability and a uniform -subset, or departures at a uniform position. Marks are independent of the clock and of a random initial state. The model is therefore the paper's in law. Sampling is without replacement, so JSQ(N) is JSQ.IsBrownianReal.Trivializing formalizations are ruled out. The goal asserts the existence of the limit (Brownian motion, initial value and solution), not merely that every limit point solves (2.4). The system hypotheses are satisfiable: the mark law has total mass one, which is checked in Lean. The convergence is of the whole path, including the tail above level .
Infrastructure needed and welcome:
Algorithms for smooth nonlinear programming, such as augmented Lagrangian, interior point and sequential quadratic programming methods, do not stop at exact Karush–Kuhn–Tucker (KKT) points. They stop at points where the KKT conditions hold approximately. Sequential optimality conditions make this precise: they are properties of sequences with approximate multipliers, satisfied at every local minimizer without any constraint qualification, and verified by the iterates of practical methods. To conclude that a limit point is a KKT point, one still needs a condition on the constraints. Andreani, Martínez, Ramos and Silva (Optimization Online 5197, 2015; Math. Oper. Res. 43(3), 2018, doi:10.1287/moor.2017.0879) identify, for each of several sequential conditions, the weakest such condition. They call it the weakest strict constraint qualification associated with that condition, and they place each one within the classical hierarchy of constraint qualifications.
This mission concerns the Complementary AKKT condition (CAKKT) of Andreani, Martínez and Svaiter (SIAM J. Optim. 20(6), 2010). CAKKT is strictly stronger than AKKT and is satisfied by the limit points of an augmented Lagrangian method under a weak Łojasiewicz-type hypothesis. The paper's §6.1 compares the associated weakest strict CQ, CAKKT-regularity, with Abadie's constraint qualification, one of the classical conditions of nonlinear programming. The answer is that CAKKT-regularity implies Abadie's CQ, and the converse fails.
Timeline:
Let be continuously differentiable, and let
For feasible , is the set of active inequalities. The polar of a set is .
Abadie's CQ holds at when .
An objective satisfies CAKKT at if there are , and with
For and , let be the set of vectors with and . The point is CAKKT-regular if is outer semicontinuous at :
The inclusion always holds, so the content of the goal is the reverse inclusion. The milestones are the statements the paper's proof uses, in attack order:
with the equivalence of the two formulations (4.12)–(4.13) and (4.14)–(4.15) of CAKKT as a milestone.
Theorem 6.4 places CAKKT-regularity in the classical hierarchy. Every point at which CAKKT forces KKT for all objectives also satisfies Abadie's CQ, and therefore Guignard's. The paper's Example 6.1 shows that Abadie's CQ does not imply CAKKT-regularity. A convergence theorem for an algorithm that produces CAKKT sequences therefore cannot be stated under Abadie's CQ alone. Together with Theorem 4.3, this fixes exactly what a CAKKT-based method needs from the constraints.
The results are proved in the paper. None of them, and none of the variational-analysis facts they rest on, is formalized on Prove2Me, and Mathlib has no regular or limiting normal cones of nonconvex sets. The work is to formalize the paper's proof together with the parts of Rockafellar–Wets it cites: Theorem 6.11 (gradients of smooth functions as normals), Proposition 6.5, and Theorems 6.26 and 6.28(b). The last is Clarke's theorem that the regular tangent cone of a closed set is the polar of its limiting normal cone. These facts are reusable well beyond this mission.
The inclusion is elementary. The reverse inclusion cannot be obtained from CAKKT-regularity at alone, because CAKKT-regularity is a statement about multiplier combinations, which live on the polar side. The argument therefore has to pass through normal cones at points near . At such points the active set may differ from , and the complementarity residual must be controlled uniformly. Returning from polars to cones requires the passage from the limiting normal cone to the tangent cone (milestone 7). That is a deep fact about closed sets in finite dimension; it is not a formal manipulation of cones. Equality of polars would only give Guignard's CQ.
is EuclideanSpace ℝ (Fin n), indices are Fin m and Fin p, and gradients are Mathlib's gradient. The objects are:
Constraints n m p of two index families. Every theorem assumes IsC1 (each and is , the paper's standing hypothesis) and feasibility of .tangentConeAt allows negative scalars and is not used). The regular normal cone is empty off the set. The limiting normal cone and outer semicontinuity use the sequential Painlevé–Kuratowski outer limit, and the outer limit in CAKKT-regularity is taken over pairs with .The following would trivialize the goal and are excluded:
A complete development needs Clarke's tangent–normal polarity for closed sets in , the existence of functions realizing regular normals, and a penalty argument for Lemma 6.2. Proofs of the general variational-analysis milestones (3 and 7) are especially welcome, since they serve any mission on nonconvex constraint sets.
Many service systems must match jobs to servers whose quality is not known in advance: crowdsourcing platforms routing tasks to worker types, wireless schedulers assigning users to channels, and switches in data networks. The scheduler learns server quality only by trying servers, and every poor assignment lets work pile up. The natural performance measure is therefore not the cumulative reward loss of classical bandits but the queue-regret: the expected excess backlog compared with a genie that knows the best assignment.
Krishnasamy, Sen, Johari and Shakkottai, Learning Unknown Service Rates in Queues: A Multiarmed Bandit Approach (Operations Research, 2021; arXiv:1604.06377), show that queue-regret has two regimes. In an early stage it grows like the regret of a bandit. In a late stage, once the queue regularly empties, past mistakes are forgotten at every empty instant and the queue-regret decays. This mission formalizes their upper bound for the late stage: a UCB scheduler with forced exploration, Q-UCB, has queue-regret of order .
A discrete-time switch has queues and servers. In every slot , queue receives an arrival and link offers a potential service , all independent and i.i.d. over slots. The scheduler picks a matching , an injective assignment of a server to every queue, and queue evolves as
The scheduler observes only past schedules and the services offered on scheduled links.
Write , for its maximizer, , and . Assumption 1: each queue has a unique best server and the best servers are distinct, so is the unique optimal matching. Assumption 2: for all . The genie queue always uses . Assumption 3: the system starts from the stationary law of . The queue-regret is
Q-UCB (Algorithm 1) explores in slot with probability , scheduling a uniformly random member of a fixed family of matchings that together cover all links. Otherwise it exploits: for each queue it picks the server with the largest index , with the empirical mean and the number of past assignments of link , and schedules a matching closest in Hamming distance to these choices. Fix and set
For every with , and ,
The constants are the paper's, stated exactly.
The theorem shows that a simple learning scheduler loses only in expected backlog in the late stage. Together with the paper's lower bound for consistent policies (Theorem 3), this places the optimal late-stage queue-regret within a polylogarithmic factor. The analysis method has two parts: a high-probability statement that the learner has locked onto the optimal matching, and a regenerative argument that converts it into a bound on queue length. It applies to other learning-in-queues problems in the same way.
All results are proved in the paper (§8.2). None of them has a machine-checked proof. The mission produces a formal model of the learning switch, including the algorithm with arbitrary tie-breaking, the coupled genie and the stationary start, and checks the explicit constants. These constants rely on numerical facts stated in the proofs, for example a positivity check for in Lemma 10(b) and the absorption of lower-order terms into , which a formal proof must verify.
The obvious argument says that UCB eventually identifies the best server, so the queue behaves like the genie's. This fails for two reasons. First, the regret is an expectation of a queue length, and a queue remembers every early mistake until it next empties. So one must bound the current regenerative cycle, and that bound itself depends on the queue length, which forces the recursion of Lemmas 13, 14, 16 and 17. Second, UCB's standard logarithmic-regret analysis bounds the expected number of sub-optimal pulls. It says nothing about whether a sub-optimal pull happens in a specific late window. Forced exploration at rate is what makes all indices concentrate at once, and Lemma 11 requires a union bound over every link, slot and sample count with explicit exponents.
Fin U and Fin K, and slots are . The genie shares arrivals, services and with the system. This coupling is implicit in the paper's proofs and does not change .The source is the arXiv v4 preprint; the paper's proofs are in its §8 and §9.
Large data centers and cloud platforms route each incoming job to one of parallel servers through a single dispatcher. The join-the-shortest-queue (JSQ) policy, which sends each job to a server with the fewest jobs, has strong optimality properties for identical exponential servers, but it needs the queue length of every server at every arrival, which is costly when is in the thousands. The power-of- scheme JSQ() polls only servers chosen at random and joins the shortest among them. For fixed it improves dramatically over random routing, which is the supermarket model of Mitzenmacher and of Vvedenskaya, Dobrushin and Karpelevich, but it does not match JSQ.
Mukherjee, Borst, van Leeuwaarden and Whiting (arXiv:1612.00723, Stochastic Systems 2018) ask how fast must grow for JSQ() to behave like JSQ in the large- limit. This mission concerns their fluid-scale answer: any growth suffices.
Timeline.
There are identical servers, each with a buffer of size counting the job in service. Jobs arrive as a Poisson process of rate and need independent unit-mean exponential service. A job sent to a full server is discarded. The occupancy vector is , where is the number of servers with at least jobs, with the convention . If the servers are listed in nondecreasing order of queue length, the -th ordered server holds jobs. A dispatch scheme picks an ordered position for each arrival, and the arrival raises by one (or is discarded if ).
The schemes are:
Two systems are S-coupled when they share the arrival clock and the departure clock of the -th ordered server for every .
The fluid-scaled state is . It lives in
which carries the distance. For let . The coefficients of (4.4) send all incoming work to level while the rate can be absorbed there, and the excess to level : if then ; otherwise , , and all other vanish.
Assume , and in . Then every subsequence of has a further subsequence converging weakly (Skorohod ) to a limit satisfying
The statement fixes no rate for , which is what makes it the right goal.
The milestones follow the paper's proof.
The result. Theorem 2.1 shows that on the fluid scale the optimality of JSQ costs nothing beyond queue inquiries per job, far fewer than . In particular the fluid limit is the same as that of JSQ, which is fluid-optimal. The coupling framework of §3 (the class CJSQ(), stack orderings, S-coupling) is not tied to JSQ(). The paper uses the same tools for the diffusion-scale Theorem 2.4, for batch arrivals and for the interchange of limits, Proposition 2.2.
Formalizing it. Proofs of the paper's results exist; no machine-checked version does. The mission produces:
The proof of Theorem 4.1 in the paper is sketched in places (the time-scale separation is argued "analogously" to Hunt and Kurtz), so a formal proof would also settle those steps.
The obvious argument would compare JSQ() directly with JSQ: the two disagree whenever the sampled servers miss every shortest queue. When a constant fraction of servers is idle this is rare, but when few servers share the minimum queue length the disagreement rate does not vanish, and a direct coupling fails. The paper instead passes through CJSQ() with , which is close to JSQ() for a suitable and sandwiched between JSQ and MJSQ().
The second difficulty is the topology. The sandwich controls tail sums , so the fluid limit of JSQ is needed in , not coordinatewise. With the state space is infinite-dimensional, and tightness requires uniform control of tails. Finally, the JSQ fluid limit itself involves a separation of time scales: the drift is discontinuous in and arises as an averaged stationary behaviour of a fast process.
ℕ →₀ ℕ with the paper's level index; coordinate holds . The buffer is with ; both finite and infinite are covered.ℕ → ℝ with . carries the distance, computed in .A formalization that states only "every limit point solves (2.1)", or that measures convergence coordinatewise, would be vacuous or weaker: it is ruled out by requiring the limit's existence and convergence.
Needed infrastructure. The development needs Poisson clocks and thinning, martingale bounds for counting processes, compactness in , tightness and Prokhorov's theorem on Polish spaces, and the Skorohod representation. The compactness and tightness criteria (Lemmas 4.6, 4.7) and the stack ordering (Proposition 3.1) are reusable on their own. Proofs of any milestone are welcome, as are proofs of Theorem 2.1 that bypass Theorem 4.1.
In the prophet inequality a gambler observes independent nonnegative random values with known laws one at a time and must decide irrevocably, after seeing each one, whether to stop and keep it. Her expected reward is compared with that of a prophet who knows all realizations and earns . When the values arrive in a fixed adversarial order the best guarantee is (Krengel, Sucheston and Garling, 1977; Samuel-Cahn, 1984). Prophet inequalities are the stopping-theoretic core of posted-price mechanisms in online auctions, where a guarantee for the gambler translates into a welfare or revenue approximation for sequential pricing.
The prophet secretary problem keeps arbitrary independent laws but lets the values arrive in a uniformly random order, as in the secretary problem.
An instance is a list of laws of independent nonnegative random variables , all continuous. A uniformly random permutation of , independent of the values, is the arrival order: at time the gambler sees .
The time threshold algorithm stops at the first time with . Its stopping time is and the gambler's reward is , written .
A blind strategy is a nonincreasing function . Given an instance, draw independently and uniformly from , let be the -th smallest, and choose thresholds by
The strategy is called blind because fixes the levels of the distribution of the maximum at which the gambler stops, independently of the instance and of . The deterministic blind strategy (Definition 3.1) uses in place of . A piecewise-constant strategy uses at most distinct levels.
There is a nonincreasing such that, for every and every continuous instance,
where is the stopping time of the blind strategy . One serves every instance.
Theorem 1.1 raised the guarantee for the prophet secretary problem from just above to , and it separates random-order arrival from adversarial arrival by more than the classical single-threshold analysis. The strategies are distribution-insensitive in a precise sense: the gambler needs only the distribution of the maximum, not the individual laws, and does not depend on . The milestones are general facts about multi-threshold stopping in random order (Lemmas 3.1, 3.3, 4.1, 4.2) that apply to any nonincreasing thresholds, not only to blind ones.
The result is proved in the paper, with one numerical step: Corollary 4.4 evaluates the bound of Lemma 4.3 at a specific vector found by optimization, which the paper does not print. No part of this argument has a machine-checked proof. The formalization would make the reduction from blind to deterministic strategies, the stopping-time estimates and the final numerical certificate explicit and checked. The paper also shows that no blind strategy guarantees more than (Theorem 1.2, outside this mission); any later improvement of the constant leaves this goal, which asserts only , intact.
The obvious argument fixes a threshold and bounds the probability that some value exceeds it; with one threshold this cannot beat , and with time-varying thresholds the events "the gambler has not stopped by time " and "value arrives at time " are dependent, because the arrival of at time removes from the earlier times. The union bound loses exactly the constant one is trying to gain. The analysis must therefore bound the law of the stopping time uniformly over all instances (Lemma 3.3), sharpen the conditional survival probability (Lemma 4.1) and the union bound (Lemma 4.2), and then pass to the limit of large instances. The final constant depends on a numerical optimization over levels, so the closing step is a certified evaluation of an explicit but long expression involving -th roots and logarithms.
All statements import one definitions file, BlindProphetSec.Blind.Setting.
μ : Fin n → Measure ℝ with IsProbabilityMeasure, NullSingletonClass (continuity, the paper's standing assumption of §1.2 and §3) and μ i (Set.Iio 0) = 0 (nonnegativity). Independence is built in: the values are the coordinates of Measure.pi μ. Indices and times are 0-based; the paper's time is j.val + 1.A trivializing formalization is ruled out: the strategy (and the vector of Corollary 4.4) is quantified before and the instance, the constants and are exact rationals, and expectations cannot collapse to through non-integrability.
A complete development needs order statistics of uniform samples, exchangeability arguments for uniformly random permutations, convergence of the padded deterministic strategies, and a certified numerical evaluation of . The random-order stopping vocabulary is reusable for other prophet secretary results, including the upper bound of the companion mission. Contributions to any milestone, including partial results such as Lemma 3.2 (), are welcome. The PDF used is the arXiv preprint, version 2 (arXiv:1807.07483v2, 12 March 2019); all labels and pages refer to it.
Systems of many particles that interact through a singular pair potential and are subject to independent noise appear in plasma physics (Coulomb interactions), in vortex models of fluids, in models of collective behaviour and in the analysis of training dynamics of wide neural networks. When the number of particles is large, the empirical measure of the system is expected to follow a deterministic nonlinear partial differential equation, the mean-field limit. For singular interactions the classical coupling arguments, which need Lipschitz forces, do not apply. The modulated-energy method of Serfaty (Duke Math. J. 2020) and its extensions by Duerinckx, Nguyen, Rosenzweig and Serfaty (NRS21, arXiv:2107.02592) give quantitative convergence for Riesz-type potentials , but with rates that degrade exponentially in time.
M. Rosenzweig and S. Serfaty (arXiv:2108.09878v1, 2021) show that additive noise improves this: the expected modulated energy grows at most polynomially in time for sub-Coulombic potentials (their Theorem 1.1, the subject of the first mission of this series), and stays bounded uniformly in time when the potential is globally superharmonic (their Theorem 1.2, the subject of this mission). Uniform-in-time propagation of chaos had been known for smooth or convex interactions; this result covers singular, non-gradient interactions on the whole space.
Fix , an exponent , a diffusion strength and a matrix with for all . The particle system is
started from pairwise distinct points and driven by independent standard Brownian motions in . The potential is admissible: it satisfies ten assumptions (i)–(x) on symmetry, blow-up at , superharmonicity near , derivative bounds of order , a doubling property, a Fourier transform comparable to , an extension to when , a Calderón–Zygmund property in the cases , and . The model case is .
The mean-field equation is
for a probability density , solved in the mild (Duhamel) sense in . Closeness of the empirical measure to is measured by the modulated energy
where the diagonal is removed. The potential is globally superharmonic if on all of ("" in assumption (iii)).
For globally superharmonic admissible and every there are (depending on ), (depending on ), and such that for all and ,
The right side does not depend on . The case of the paper's display (1.19) is not part of the goal (see Formalization scope).
The proof combines an inequality for the time derivative of the expected modulated energy (Proposition 6.3), lower bounds for the energy and for the diffusion term (Remarks 5.10, 5.11, Proposition 5.12, Remark 5.13, Corollary 5.14), a commutator estimate for the transport term (Proposition 5.15), and decay of (Remark 3.4, Proposition 3.8), with the potential estimates of Lemma 2.3 and Remark 2.5.
A uniform-in-time bound means that the mean-field description is valid on time scales that do not shrink as the accuracy requirement grows. Combined with the control of negative Sobolev norms by the modulated energy, it yields uniform-in-time convergence in law of the empirical measure and, for chaotic initial data, uniform-in-time propagation of chaos at an explicit rate, for singular interactions such as sub-Coulombic Riesz gases with dissipative or conservative dynamics.
The result is proved in the paper. No part of it, nor of the modulated-energy method, is formalized in any proof assistant. A formalization would produce a reusable library: Riesz potentials and their – interpolation, heat-type decay of nonlinear Fokker–Planck equations, smeared potentials and electric-energy lower bounds, renormalized commutator estimates, and a pathwise treatment of interacting diffusions with additive noise. The milestones are independent statements and can be proved separately.
The obvious Gronwall argument on the modulated energy fails twice. First, is not nonnegative; it is bounded below only up to errors involving , and the lower bounds near the singularity need the smearing of point charges on spheres. Second, the error terms produced when the commutator and diffusion terms are bounded must be integrable on ; with the estimates of the general (local superharmonicity) case they grow linearly in time. Global superharmonicity removes an error term and lets every error carry a power of , which decays like by the Carlen–Loss method; for long-range effects still produce growth, which is why that case is excluded. Itô's formula cannot be applied directly to the singular energy and requires a truncation, whose stochastic integrals are removed in expectation only in the limit.
All objects live in the Lean namespace RieszMF.Global and in one definitions module. Space is EuclideanSpace ℝ (Fin d); derivatives are iteratedFDeriv (operator norm), gradient and the Laplacian of Mathlib. The committed conventions:
Restriction. The goal is Theorem 1.2 for only, where the paper's time factor equals . For the proof yields a factor of order rather than the printed ; the logarithmic case is covered by the first mission of this series.
Excluded trivializations. A statement in which is chosen after , or the configuration, in which a divergent integral is read as , in which the solution classes are empty, or which uses or a division by zero is not a formalization of the theorem; the statements here avoid each of these.
Contributions are welcome on any milestone, on the existence of solutions in the classes used (which shows the hypotheses are satisfiable), and on general infrastructure (Riesz potentials, sphere averages, heat-kernel estimates) that other missions can reuse.
Hotel rooms, rental cars, cloud servers, operating rooms and rental equipment are reusable resources: a customer occupies capacity for a fixed service time, and the capacity returns to the firm afterwards. Many of these settings also allow advance reservation, where a request made today is for a service that starts later. Lei and Jasin study dynamic pricing in this setting. Prices are posted period by period, demand is non-stationary, and the firm wants revenue close to the best achievable while never booking more units than it owns.
Classical network revenue management, where capacity is sold once and never returns, has an extensive asymptotic theory. In that literature, controls that re-solve or adjust a fluid (deterministic) plan are known to lose a vanishing fraction of the optimal revenue as demand and capacity grow (Gallego and van Ryzin 1997; Jasin 2014). Reusable resources break the standard argument, because each sale removes capacity for a window of time and not for the rest of the horizon. Lei and Jasin give the first control for reusable resources with non-stationary arrivals, deterministic service times and advance reservation whose average loss is in the scale parameter (Lei and Jasin, Operations Research 2020).
A firm manages resource types with integer capacities and sells service types over periods . At most one request arrives per period. A type- request made at the beginning of period uses units of resource during periods . Here is the service time and the reservation lead time.
In each period the firm chooses a demand-rate vector , which is equivalent to choosing prices. A type- request then arrives with probability , independently of the past given , and the expected revenue rate is . The deterministic relaxation DET-H maximizes over , subject to
Its optimal value bounds the optimal expected revenue, and the average loss of a control is . Let be an optimal solution of DET-H. The quantity is the smallest number of periods with inside any service cycle of type that carries positive demand.
The control DPC-B splits the horizon, for each type , into adjacent batches , each with positive-rate periods. In period it posts
where is the batch containing . The rate is set to when fewer than units of some resource are free at the service start . The buffer protects capacity, and the batch term corrects for the demand surprises of the previous batch.
There is a constant , depending only on , the curvature constant of Assumption A5 and a bound on , such that for every instance, every valid batch partition with and every in the stated range,
The constant is uniform in , , , , and , which is what makes the bound informative.
A companion item states Lemma 2 in this setting: stretching in time solves DET-H for the -th system of display (7).
Along the scaling (7), Theorem 3 with gives an average loss of . The non-adaptive control DPC of the same paper achieves (its Theorem 1). The result shows that batch-level feedback improves on the square-root barrier for reusable resources, and it does so with heterogeneous service times and advance reservation, which cover car rental and hotel bookings.
Theorem 3 and its lemmas are proved in the paper's e-companion. No machine-checked proof of them, and no formal model of reusable-resource revenue management, is known. The mission produces a Lean model of the setting: capacity windows with lead times, the availability table , an adapted control on finite sample paths, and its exact path law. On top of that model it states the paper's main bound in full. Several printed steps need repair (see the scope section), so a formal proof would also settle the exact constants.
The obvious route bounds each period's loss by a Taylor expansion around and controls the deviations by a martingale inequality. That route needs the control to coincide with the unprojected corrected rate for the whole horizon, that is, no capacity shortfall and no clipping. Capacity is a moving window of overlapping services with different lengths and lead times, so a shortfall at one period depends on requests made up to periods earlier, in other batches and other types. The batch correction makes the rates depend on past errors, so the errors are martingale differences, not independent variables. The concentration bound must hold uniformly over batches whose number grows with , with a variance proxy that is not the batch length. The early periods, before any service of type has completed, need a separate threshold (the two cases of (EC.17)).
All objects are defined in the namespace ReusablePricing.DPCB. The conventions are fixed as follows.
Fin T → Option (Fin K), recording no request or one request of a type in each period. Expectations are finite sums against the exact path law: the product over periods of the one-period law, whose probabilities are the rates posted given the past. The demand law is never left as a hypothesis.The constant is quantified before the instance, after only , and . Choosing it after the instance would make the bound trivial, because the loss never exceeds .
A complete development needs Freedman- or Doob-type inequalities for bounded martingale differences on finite path spaces, second-order Taylor bounds for functions on boxes in , and window-counting lemmas for capacity. The first two are reusable well beyond this mission. Contributions of any of the milestones, of general martingale tools for finite adapted processes, or of a proof of the companion Lemma 2 are welcome.
Hotel rooms, rental cars, cloud servers, hospital beds and event spaces are reusable resources: a customer occupies a unit for a while and then returns it. Pricing them differs from classical revenue management, where a sold unit is gone for good. A sale now blocks capacity only for the length of the service, so the binding constraint is how many services overlap at once. Lei and Jasin (Oper. Res. 2020) study dynamic pricing in this setting with deterministic service times and, in the general model, advance reservations. They measure a pricing control by its average loss against a deterministic (fluid) benchmark.
The paper has two main results. Theorem 1 bounds the loss of a static heuristic, the Deterministic Price Control DPC(). Theorem 3 bounds the loss of an adaptive variant and is treated in the companion mission (II). This mission formalizes Theorem 1, the lemmas its proof rests on (Lemmas EC.1–EC.2 and the displays (EC.14), (EC.15) of the e-companion), and two structural lemmas of the model: the fluid upper bound (Lemma 1) and the scaling of the fluid solution (Lemma 2).
A firm manages resource types with integer capacities and offers service types over periods . At most one request arrives per period. A type- request uses units of resource for consecutive periods (a service cycle), and divides .
The firm posts a demand-rate vector with . A type- request then arrives with probability , independently of earlier periods given the posted rates, and the firm earns the revenue rate . Writing for realized arrivals and , the capacity free at the beginning of period is
The deterministic relaxation is
with optimal solution . The revenue rates are strictly concave, bounded by in absolute value, and have interior maximizers (A4). Near their gradients and Hessians are bounded by (A5, with margins ).
The quantity of display (2) is the smallest number of periods with in any service cycle that carries positive demand for some type .
DPC() posts, in period , the rate , clamped to , for every type with . It turns off every other type (rate ). The average loss of a control is .
For ,
with depending only on , and , and not on , , , or the other data.
Companion statements: Lemma 1 ( for every feasible non-anticipating control) and Lemma 2 (for integer , solves the DET of the -th system , , ).
Along the scaling (1), choosing of order in Theorem 1 gives an average loss of . A control computed entirely before the selling horizon is therefore asymptotically optimal for reusable resources, with an explicit rate. This bound is the baseline against which the paper's adaptive control (Theorem 3, rate ) is measured.
The proof shows a pattern common to fluid-based revenue management: a high-probability event on which the heuristic follows the fluid plan exactly, a martingale maximal inequality bounding the complement, and a Taylor bound for the cost of the buffer. Reusable resources add one ingredient: capacity is checked over sliding windows of length .
The results are proved on paper; none is machine-checked. The formalization would provide a checked version of the model (sliding-window capacity, at most one arrival per period, turn-off), of the high-probability analysis, and of the uniform constant. The printed proof has slips that a checked proof must repair. In particular, the exponent obtained by EC.3's choice of is ; it differs from the printed one by an amount that a larger absorbs.
The obvious argument says that DPC keeps an buffer, so it rarely runs out of capacity. The difficulty is that "rarely" has to hold uniformly over every sliding window of periods. The rates DPC posts are themselves random, because a type is turned off whenever the realized free capacity is short.
Lemma EC.1 breaks this circularity by induction over periods on a fixed event. A capacity window of length straddles two consecutive cycles, which costs a factor in , and only the periods with positive deterministic demand carry a buffer, which is why appears. The demand errors form a martingale-difference sequence with predictable, path-dependent rates, so (EC.15) needs a pathwise bound on the cumulative rate within a cycle. That bound comes from the DET constraint, not from independence.
Finally, the constant must not depend on the instance. A bound in which may depend on or is trivial, since the loss never exceeds .
Everything is stated in demand rates, as the paper does for DET and in all its proofs. Prices, A1–A3 and the price-derivative part of A5 do not appear. A turned-off type has rate .
A sample path is a function from to "no request" or "one request of type ". Its probability is the product of the per-period probabilities under the rates the control posts, so expectations are finite sums. Expected revenue is , the tower-property form of the proofs. Periods are , and window sums whose upper limit falls below the lower limit are empty.
The standing hypotheses, bundled as Standing φL φU Ψ R n̲, are:
The statements "on " are claimed for every path of positive probability in the event. Theorem 1 quantifies after , , and before everything else. This rules out the trivial reading in which is chosen per instance. Step 2 uses where the printed line has , and for . in Lemma 2 is an integer.
Two definition files carry the model: ReusablePricing.DPC.Model holds the instance, DET, A4–A5, and the -th system; ReusablePricing.DPC.Control holds the path law, DPC, loss, events and general controls. A complete proof needs a finite-path martingale toolkit: a Doob-type maximal inequality for exponential submartingales on a finite product space, and the Bernoulli moment-generating-function bound. It also needs a multivariate mean-value or Taylor estimate on a box and an induction over sliding capacity windows. The martingale tools are reusable beyond this mission. Contributions of those general lemmas, of proofs of individual milestones, and of the optional asymptotic corollary (4) are welcome.
Systems of particles that interact through a singular pair potential and are driven by independent noise are used to model vortices in viscous fluids, collective motion of micro-organisms, aggregation phenomena and, more recently, the training dynamics of wide neural networks and stochastic gradient methods. When is large, one expects the empirical measure of the particles to be close to the solution of a deterministic nonlinear PDE, the mean-field limit. Proving this with an explicit rate is difficult when the interaction is singular, because the classical coupling arguments need a Lipschitz force.
The modulated-energy method (Duerinckx 2016, Serfaty 2020, Nguyen–Rosenzweig–Serfaty 2021) measures the distance between the particles and the limit through a renormalized Coulomb/Riesz energy and closes a Gronwall argument on it. Rosenzweig and Serfaty (arXiv:2108.09878) extended it to systems with additive noise in the sub-Coulombic range. This mission formalizes their first main result, Theorem 1.1: the expected modulated energy grows at most linearly in time (polynomially for logarithmic interactions). A companion mission covers their uniform-in-time Theorem 1.2.
Fix and . Positions live in with Lebesgue measure. A real matrix satisfies for all (gradient flows , Hamiltonian flows antisymmetric, and mixtures). The interaction potential is admissible: it satisfies ten assumptions (i)–(x), with model cases () and (). In short: is even, blows up at , is superharmonic on a punctured ball , is smooth off the origin with (plus a logarithm when ), has a Fourier transform comparable to , has a doubling property near , admits a superharmonic extension to when , has a Calderón–Zygmund kernel condition when , and satisfies .
The particle system (1.1) is
with distinct initial points, , and independent standard Brownian motions in . The mean-field equation (1.5) is
for a bounded probability density , solved in the class . The modulated energy (1.6) is
the diagonal being removed to discard the infinite self-interaction of each particle.
There are depending on only and, for every , , admissible and value of , a constant and a threshold such that for all and
The exponent and the constant are left unspecified, as in the paper.
In the order the proof uses them:
The theorem is a quantitative mean-field limit for singular interactions with additive noise on the whole space, covering conservative and dissipative dynamics at once. Since controls a negative-order Sobolev distance between and , it gives convergence of the empirical measure, at a rate in that deteriorates at most linearly in for . Its proof isolates estimates (the decay of the nonlinear equation, the sign of the diffusion term, the commutator bound) that are reused for the uniform-in-time result of the companion mission.
The paper's results are proved; none of them has a machine-checked proof. Formalizing the theorem requires the modulated-energy machinery (smeared charges, Fourier positivity, commutator estimates), a Carlen–Loss decay argument, and an Itô-free treatment of the stochastic system. The milestones of §§2–3 are classical harmonic analysis (Riesz potentials, the Gross–Carlen log-Sobolev inequality) and are of independent use.
A direct Gronwall argument on fails twice. The diffusion term has no sign for a general configuration, because the singularity of at the origin is integrated against a signed measure with atoms; its control needs a second modulated-energy estimate for , which is a potential of order and may be super-Coulombic, hence the extension of assumption (viii). The commutator term requires , and bounding it by alone produces exponential growth in time; the polynomial bound needs the time decay of , which for a nonlinear, non-divergence-free drift is not given by comparison with the heat equation. Finally, the Itô computation for along the singular dynamics needs truncation and stopping times, since is not at collisions.
All objects are defined in one module RieszMF.Linear.Setting. Space is EuclideanSpace ℝ (Fin d) with Lebesgue measure; derivatives are iteratedFDeriv with operator norms, is Mathlib's Laplacian, and the Fourier transform is Mathlib's . Assumption (iv) is read with a constant for each ; (vi) and (1.17) as Fourier transforms paired with Schwartz functions vanishing near the origin; (iii) pointwise on the punctured ball; one radius for (iii), (v), (vii), (viii); in (viii). Assumption (vii) for is printed as for , which together with (ii) is unsatisfiable; it is stated as .
The solution of (1.5) is a mild solution (3.1) in with continuity in the norm, with each a probability density; every integral of (3.1) is required to converge. Because the noise is additive, a solution of (1.1) is a measurable process whose paths almost surely are continuous, never collide, and satisfy the integral equation with the Brownian path; no stochastic integral appears. Brownian motions are Mathlib's IsBrownianReal coordinates, jointly independent over all coordinates. Expectations are lower Lebesgue integrals of nonnegative quantities, and Proposition 6.3 is stated in with positive and negative parts on opposite sides, so no and no default value of a divergent integral enters.
The constants follow the paper's dependency lists: depends on only and is chosen before ; and are chosen after and , before the data, , the configuration, the probability space and . A formalization with constants chosen after , or the configuration, with , with a junk-zero integral in or in (3.1), or with an empty solution class does not count. Corollary 5.6 is posed exactly under its printed assumptions, although its proof for uses the superharmonicity of , which those assumptions do not list.
Contributions welcome: proofs of the milestones, a Lean development of Riesz potentials and of the sharp log-Sobolev inequality on , and the well-posedness of the mean-field equation that the goal takes as a hypothesis (Proposition 3.1 and its global continuation, not posed here).
Banks and insurers hold capital against the risk of their positions, and regulators compute that capital with a risk measure, a functional that maps a random loss to a number. The two standard ones are the Value-at-Risk (VaR), a quantile of the loss, and the Expected Shortfall, an average of the upper quantiles (BCBS 2019). Both look only at the upper tail of the loss distribution. Liu and Wang (2021) called such functionals tail risk measures.
When a total loss is split among several agents, each judging its share with its own risk measure, the smallest total capital achievable is the inf-convolution of the agents' risk measures, and a split attaining it is an optimal allocation. Embrechts, Liu and Wang (2018) computed the inf-convolution for VaR and Expected Shortfall agents. Liu, Mao, Wang and Wei (SSRN 3490348, version of January 16, 2022; published in Mathematics of Operations Research, 2022) extend this to agents with general tail risk measures. This mission formalizes their Theorem 2: one agent uses a VaR, the other an arbitrary monetary tail risk measure.
Let be an atomless probability space: every event of positive probability contains an event of strictly smaller positive probability. A random variable is a measurable map , a positive value being a loss, and is the set of all of them. Its distribution function is . For a level the left and right VaR are
A small is a high quantile. The quantile function is , and denotes a random variable that is uniform on with almost surely.
A risk measure is monotone if a.s. implies . It is translation-invariant if for every constant , and monetary if it is both. For , the -tail of has distribution function (display (6) of the paper). A risk measure is a -tail risk measure if whenever and have the same law.
The allocations of between two agents are the pairs with , and the inf-convolution is
For and the paper introduces the truncation
Let , let be a monetary -tail risk measure, and let . For every and every choice of :
Theorem 2 gives a closed form for the inf-convolution and an explicit optimal allocation. The VaR agent takes the loss above the -quantile, minus a constant, and the other agent keeps the rest, which has the same -tail as the truncated . No convexity, law-invariance or distortion structure is assumed for beyond its being a monetary tail risk measure. The theorem generalizes Theorem 5.3 of Wang and Wei (2020, Insurance: Mathematics and Economics 93), which required a distortion risk measure. Specialized to , it gives . Part 4 says that the tail parameters add: the representative agent of a VaR and an -tail agent is an -tail agent. This is the two-agent instance of the paper's Theorem 3. Parts 1 and 3 together contrast the left and right VaR: an optimal allocation always exists for , while for the value is only a limit.
The result is proved in the paper. As far as a search of the platform shows, it has no machine-checked proof, and the platform has no development of quantile-based risk measures on a general atomless probability space. The mission produces the definitions of left and right VaR, tails, tail risk measures and inf-convolution on , and a checked proof of the theorem.
The upper bound in part 1 is a single allocation. The lower bound must hold against every allocation . It reduces to comparing the distribution function of with that of , but only on the -tail. Turning that comparison into needs both monotonicity and the tail property of . Monotonicity is almost-sure and pointwise, the tail property is distributional, and no coupling between and is given, so the two cannot simply be chained. Part 3 needs an interchange of a limit and an infimum together with the one-sided continuity . Part 4 needs the law of the -tail of to depend only on the -tail of . All of this rests on careful quantile bookkeeping: left versus right inverses, and strict versus weak inequalities at atoms of .
Random variables are functions , and the domain is , the measurable functions. The paper allows any convex cone containing that is closed under equality in law and under taking tails, and fixing is one of the instances it names. The probability space is atomless, as §2.1 assumes throughout. , the VaRs and are encoded as above. is not chosen: parts 1–3 are asserted for every uniform with a.s. The equality in law of tails is encoded through display (6), as equality of and . The risk measure is real-valued; the paper allows the value , but the agents of §2.3 are real-valued. Monotonicity and translation invariance are required on , with monotonicity for almost-sure inequalities.
Allocations sum pointwise. The inf-convolution takes values in the extended reals, so no junk value from a real infimum arises. Part 3 is a one-sided limit in the extended reals, which asserts both that the limit exists and its value. Part 4 uses extended-real versions of "monetary" and "tail risk measure". The level ranges and are hypotheses.
Dropping the tail hypothesis on makes part 1 false: on integrable losses the expectation is monetary but not a tail risk measure. A real-valued infimum in place of the extended one would make the inf-convolution a junk when it is . A choice of by Classical.choose would weaken parts 1–3 to one uniform. None of these is used.
A complete development needs quantile calculus for and (right-continuity of , the Galois connection ), the distribution of , and basic facts on infima in EReal. The quantile lemmas are reusable for every other mission of this series and for any formalization of VaR. Proofs of the milestones, and of the folklore fact that inf-convolutions of monetary risk measures are monetary, are welcome as separate contributions.
Estimating an unknown parameter from a noisy linear measurement is the basic problem behind Kalman filtering, signal recovery and linear inverse problems. A Bayesian statistician picks the estimator that minimizes the mean square error under a prior distribution; a minimax statistician guards against the worst prior in some family. The Bayesian answer depends on a prior that is rarely known, and the minimax answer is often intractable.
Nguyen, Shafieezadeh-Abadeh, Kuhn and Mohajerin Esfahani (Math. Oper. Res. 48(1), 2023) bridge the two by letting nature choose the joint distribution of parameter and noise from a ball of radius around a nominal distribution in the type-2 Wasserstein distance. At the problem is Bayesian; as grows it becomes more conservative. For a normal nominal distribution they show that this distributionally robust problem is solved by an affine estimator, that a normal distribution is least favourable, and that both are computable from a finite convex program. The paper extends the Wasserstein Kalman filter of Shafieezadeh-Abadeh et al. (NeurIPS 2018), which treated a joint normal ball on , to the model with independent parameter and noise.
The parameter is and the observation is , with a known observation matrix and noise independent of . Write for the probability distributions on with finite second moments.
The nominal distribution is a product with radii . Three ambiguity sets of product distributions appear:
Then .
For normal with ,
The left side is the Gelbrich MMSE problem (2.1), the right side the dual problem over normal priors (3.3). The Wasserstein problem (1.7), , and its dual (3.1), , lie between them, so all four values coincide.
Companion statements, not milestones: Theorem 3.5 (problem (3.3) equals the finite program (3.4)), Corollary 4.2 (the optimal affine estimator and the optimal normal prior form a Nash equilibrium on ) and Corollary 4.3 (the minimax estimator from a maximizer of (3.4)).
The sandwich theorem says that robustifying the MMSE problem against Wasserstein uncertainty around a normal distribution costs nothing in tractability: the optimal estimator is affine, the worst-case distribution is normal, and both follow from a convex program in the covariance matrices. The resulting estimator is a Kalman-type update with a least favourable covariance in place of the nominal one, which is what makes the result usable in filtering. The paper also extends it to elliptical nominal distributions (Section 5) and develops a Frank–Wolfe method for (3.4) (Section 6).
The results are proved in the paper; none of them is machine-checked. A formalization adds a checked account of a minimax argument that combines optimal transport (the Gelbrich bound and its equality for normal laws), nonlinear semidefinite programming (Propositions A.3 and A.4) and Bayesian estimation for Gaussian laws. The appendix statements are general facts about the Gelbrich ball of covariance matrices and serve beyond this paper.
The left side of the goal is an infimum over affine estimators of a supremum over an infinite-dimensional set of distributions; the right side reverses the order and restricts nature to normal laws while allowing every estimator. Weak duality gives at once. For the reverse inequality, Sion's minimax theorem cannot be applied to the distributions directly: is not convex, since mixtures of normal laws are not normal, and is not compact in any useful topology. The equality has to pass through the finite matrix problems, where the worst covariance matrices must be shown to stay bounded away from singularity so that the normal noise covariance remains positive definite. That is the role of Lemma A.5 and of the hypothesis .
EuclideanSpace ℝ (Fin d). The risk is a lower Lebesgue integral in , and every optimal value is a - or EReal-valued infimum or supremum restricted by a membership predicate. The finite programs (2.2), (3.4), (A.3), (A.5), (A.6), (A.9) take values in EReal.multivariateGaussian. , means, covariances, the PSD square root and the Gelbrich ball are the published definitions WassersteinDRO.Gelbrich.{wassersteinDistance, meanVector, covarianceMatrix, psdSqrt, meanCovarianceUncertaintySet}.sSup/sInf would make the goal trivial or false. A sanity check exhibits a member of whenever , and an affine estimator.Proofs of any milestone are welcome, and so are reusable lemmas on the Gelbrich ball, the matrix square root and Gaussian conditioning.