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.
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?
A risk measure assigns a number, typically a capital requirement, to a random financial loss. When a total loss is shared among agents, each judging its share by its own risk measure , the smallest achievable aggregate risk is the inf-convolution
It describes optimal risk sharing in insurance, reinsurance and among the desks of a financial institution, and it is the basic object of the risk-sharing literature (Delbaen 2012; Rüschendorf 2013).
Regulatory risk measures such as Value-at-Risk (VaR) and Expected Shortfall depend only on the upper tail of the loss distribution. Liu and Wang (2021) formalized this as tail risk measures. Embrechts, Liu and Wang (2018) showed that the inf-convolution of VaRs and Range-VaRs is again of the same type with summed levels, and Liu, Wang and Wei (2020) showed that inf-convolutions of law-invariant risk measures are law-invariant under weak conditions. Theorem 3 of Liu, Mao, Wang and Wei (2022) unifies these observations for arbitrary tail risk measures. This mission is drawn from the authors' SSRN version of January 16, 2022.
Fix an atomless probability space : every event of positive probability contains an event of strictly smaller positive probability. Positive values of a random variable are losses. Write . For the left and right VaR are
The domain is , the essentially bounded random variables.
For the tail of beyond its -quantile is the random variable with distribution function (display (6) of the paper). A functional is a -tail risk measure if whenever and have the same law. For this is law-invariance. The functional is monotone if a.s. implies , and (sup-norm) continuous from above if whenever a.s. and .
The allocations of are , and is the infimum above over . It takes values in .
Let be an -tail risk measure with , , and suppose one of is monotone and continuous from above. Then
The theorem says that tail-dependence survives optimal risk sharing, and it quantifies how much: the aggregate looks at a tail of probability at most the sum of the individual ones. The parameter is sharp, since and has smallest tail parameter . Consequently, results proved for tail risk measures (representations through law-invariant functionals of the tail, existence of optimal allocations) apply to the outcome of a risk-sharing market, not only to its participants. The hypotheses are weak: no convexity, no translation invariance, and only one agent needs monotonicity and a mild continuity.
The result is proved in the paper; its proof relies on two results it cites but does not state, Lemma 1 and Theorem 2 of Liu, Wang and Wei (2020), and on Corollary 1 of Embrechts, Liu and Wang (2018). None of the three, and no part of the theory of tail risk measures or inf-convolutions on probability spaces, is formalized on the platform or in Mathlib as far as a search found. A formalization therefore has to build the cited results as well; milestones 2, 3 and 5 isolate them in the form used.
Tail-invariance of each concerns one share at a time, while the inf-convolution is a constraint on the sum of the shares: modifying a share below its quantile breaks the budget . The obvious argument, applying the tail property of each to its share of and of , fails because an allocation of does not induce an allocation of when but . Even when an allocation of cannot in general be transported to an allocation of exactly. This is why the theorem needs an atomless space and a continuity hypothesis on one agent, and why the cited law-invariance result is the hardest part to formalize.
All objects live in the namespace TailRiskSharing.TailConv, in one definitions file. Conventions:
NoAtoms).EReal, so it can be , and monotonicity and the tail property are stated for that EReal-valued functional without assuming finiteness.The goal cannot be satisfied trivially: the tail parameter is and never a number above 1, the inf-convolution is not truncated to a real value, and none of the hypotheses is vacuous (constant functionals satisfy all of them). Contributions are welcome for each cited result as reusable lemmas: the quantile subadditivity of Embrechts et al., monotonicity of an inf-convolution, and law-invariance of inf-convolutions on atomless spaces.
Online stochastic matching models display advertising and similar allocation problems in which requests arrive one at a time and must be served immediately. A bipartite graph links a set of advertisers to a set of impression types; requests arrive, each of a type drawn independently with , and each request must be assigned at once and irrevocably to an unmatched interested advertiser, or dropped. Performance is measured by the competitive ratio , where OPT is the maximum matching of the realized graph.
Without distributional knowledge the best possible ratio is (Karp, Vazirani and Vazirani, 1990). Knowing the type distribution allows more:
This mission concerns the analytic core of Theorem 3, the general-rates bound.
For an advertiser , let be the LP flow into . Its neighbours , which include a dummy advertiser with , are indexed by . For each neighbour, is the expected number of random lists , and is the neighbour's flow, so that . Write and .
Claim 2 of the paper introduces the functions
where is the probability that is matched through a list headed by . The per-advertiser bracket is
and the reduced function of three variables is
In Lean these are h, g, bracket f x y and R f β s in RandomListsMatching.GeneralRates.
For , any and reals with , and ,
The paper bounds below by (p. 15), so this inequality is the whole of what Theorem 3's numerical constant rests on.
The result. Theorem 3 gives for online stochastic matching with general (non-integral) arrival rates, improving the of Manshadi et al. The probabilistic half of its proof reduces matching probabilities to the closed forms and ; the paper then states that "in the remaining part of the section, we only use algebraic manipulations and the following properties of functions and ". That remaining part, posed here, is an exact real inequality, and it is where the constant is decided.
Formalizing it. The paper proves Claim 3 in one line ("can be easily verified by taking first and second order partial derivatives") and Claim 4 by a grid computation over cubes of side , with no recorded error analysis. A machine-checked proof replaces both. It also settles the regime of the constant: Claim 4 as printed, with the constraint "for ", is false, and the bound holds in the limit form stated here. None of these statements has a formal proof anywhere, to the extent of the search made for this mission.
The margin is small. The minimum of over the feasible region is about , attained near on the boundary ; the margin over is under . Any argument that loses a constant factor in the estimates of , or replaces by a rational bound that is not tight to five digits, fails. The bound is a three-variable statement with the minimum on a boundary face, so a one-variable monotonicity argument does not settle it.
The second difficulty is the function itself. Its two-case definition is continuous but the quotient form has a removable singularity at , which is exactly the end of the interval on which Claim 3 asserts convexity and concavity. Derivative computations that are routine away from the diagonal need care there.
The natural first idea for the goal, to apply Claim 4 directly to the bracket, does not type-check: the bracket depends on the whole family , and the reduction to three variables through the chord and cross-sum bounds is a separate step.
Real.exp 1, is Real.log 2, and is the exact rational (0.706 : ℝ).Fin k, and is allowed.MonotoneOn, AntitoneOn); convexity is ConvexOn ℝ (Set.Icc 0 y). The derivative in (5) is deriv (fun t => h y t) 0, the derivative in the second argument; the page's is a slip.A complete development needs the derivative calculus of on , including the diagonal, and certified interval bounds for and . The latter is reusable well beyond this mission. Proofs of Claim 3 or Claim 4 alone are welcome contributions.
In distributed optimization, agents connected by a communication network jointly minimize the average of their private losses, exchanging vectors only with their neighbours. This is the computational model of decentralized machine learning (data held by many machines, no central server), of sensor networks and of multi-agent control. A central family of methods is gradient tracking: each agent keeps, besides its copy of the decision variable, an estimate of the network-wide average gradient, refreshed by mixing with neighbours. Gradient tracking removes the steady-state bias of plain decentralized gradient descent and, for smooth strongly convex problems, converges linearly (Nedić, Olshevsky & Shi 2017; Qu & Li 2018).
Sun, Daneshmand and Scutari (arXiv:1905.02637v2, SIAM J. Optim. 2022) study SONATA, a gradient-tracking scheme in which each agent replaces its loss by a strongly convex surrogate and solves a small local problem per round. The setting is broader than earlier linear-rate results in three ways: the problem may be composite (a convex, possibly nonsmooth regularizer ), constrained (a closed convex set ), and only the average loss needs to be strongly convex, not each local loss. Linearizing surrogates recover proximal gradient tracking; surrogates that keep the full local loss recover DANE- and CEASE-type methods, whose rates improve when the local losses are similar.
Agents hold functions . With , Problem (P) is
Assumption A: is nonempty, closed and convex; each is twice differentiable on an open set and convex; on with ; is convex on . Then on for some constants (display (1)), and .
The network is a connected undirected graph on the agents (Assumption B) and a doubly stochastic weight matrix with , on edges and off edges (Assumption D). Its mixing rate is , the largest singular value of (tensored with ).
Each agent has a surrogate , on , whose gradient in matches at , is -Lipschitz, and which is -strongly convex in (Assumption C). Display (15) supplies constants with on ; , , , .
SONATA (Algorithm 1) with step size starts from , and repeats
With the optimal solution, the analysis tracks the optimality gap , the consensus errors , (deviations from the network averages), the tracking error and the step .
If , there is such that for every , every SONATA run and every agent ,
The goal fixes no rate: it asserts R-linear convergence for all small step sizes, which is the shape the paper proves. The explicit rate of Theorem 3.10 and the iteration counts of Corollaries 3.11–3.14 are not posed.
In the order of the proof: the tracking invariant (19); Lemma 3.1 (per-agent descent); Lemma 3.2 (a lower bound on ); Lemma 3.3 (); Proposition 3.4 (); Proposition 3.5 (consensus errors contract at rate up to ); Proposition 3.6 ( bounded by and ); Proposition 3.8 (the four inequalities (50a)–(50d) for the transformed sequences ); and (54), .
Theorem 3.9 gives a linear rate for distributed composite, constrained optimization with gradient tracking, under strong convexity of the average loss only. It covers, through the choice of surrogate, proximal gradient tracking and the distributed versions of DANE and CEASE, and the constants quantify how much a surrogate gains when local losses are similar. The chain of Propositions 3.4–3.8 is a reusable template: an optimality-gap recursion, consensus recursions and a step bound, closed by a small-gain argument.
The result is proved in the paper; to our knowledge no part of it has been formalized. The mission produces a machine-checked statement of the model and of the full chain. Useful contributions include proofs of the individual milestones, a proof of the goal from the milestones, and the general facts they rest on.
The obvious argument fails in two places. First, the local step does not descend on by itself: the tracker is not , and the surrogate's curvature differs from 's, so Lemma 3.1 must compare Hessians of and along a segment through (15), and the descent holds only up to the tracking error. Second, no single quantity contracts: contracts up to consensus errors, consensus errors contract up to , and is bounded back by . No Lyapunov function is given, and the loop gain of (55) involves every constant of the problem, so showing it can be pushed below 1 for some is where the step-size threshold comes from. Also, is not an assumption: it must be derived from connectivity and Assumption D.
Agents' vectors live in EuclideanSpace ℝ (Fin d), stacked vectors are Fin m → EuclideanSpace ℝ (Fin d), and their norm is always the Euclidean norm written out (), never Lean's sup norm. Hessians are derivatives of gradients; Loewner bounds are quadratic-form inequalities. The surrogate's gradient and Hessian are in its first argument. is the operator norm of on Euclidean . Time is 0-based.
A SONATA run is a relation: is any minimizer of the local problem, and any minimizer of on . Assumption A gives no lower semicontinuity of , so minimizers need not exist in general; the paper assumes they do, and so does the formalization, without adding a hypothesis on . A sanity file exhibits instances of all assumptions and of runs (including a nonconstant one), so the run predicate is not empty. " convex" is read as convexity on plus a positive semidefinite Hessian on ; is convex on only. The constants of (1) and (15) are parameters: each statement holds for every valid choice. All of Assumptions A–D are hypotheses of every statement (the paper's standing assumption of §3.3).
Trivializing formalizations are ruled out: is not assumed in place of Assumptions B and D; is chosen before the step size, the starting point and the run; is required; norms of stacked vectors are Euclidean. Two printed slips are handled openly: in Proposition 3.4 is stated with positivity only when or (at , (41) gives ), and is kept as printed in (52d) although (47) has 3. In Lemma 3.2, Lean's makes the bound trivial when .
A full development needs: the mean-value and Taylor estimates for functions with bounded Hessian on a convex set, first-order optimality for constrained convex minimization, the spectral bound for graph-compliant doubly stochastic matrices (posed elsewhere on the platform as StochGradTrack.Const.lemma_1 for a closely related model), and elementary estimates on finite maxima. These are reusable beyond this mission.
A quadratically constrained quadratic program (QCQP) minimizes a quadratic function subject to quadratic inequality and equality constraints. QCQPs contain max-cut, binary programming, the trust-region subproblem and many problems from signal processing and control, and are NP-hard in general. The standard convex approach is the Shor semidefinite relaxation, which lifts to the matrix and relaxes to an arbitrary positive semidefinite completion. Two questions decide how useful the relaxation is for a given QCQP: is its optimal value equal to the QCQP's (SDP exactness), and does its projected epigraph equal the convex hull of the QCQP's epigraph (convex hull exactness)?
A. L. Wang and F. Kılınç-Karzan (arXiv:1911.09195v3, Math. Program. 2021) give sufficient conditions for both, in terms of the faces of a dual set and a symmetry parameter , the quadratic eigenvalue multiplicity. Their Theorems 1 and 2 require to be polyhedral and on every semidefinite face . This mission formalizes §4.3 of the paper, which shows that neither hypothesis can be weakened on its own.
Timeline. Fujie and Kojima (1997) recorded the dual description of the SDP value used here. Ye and Zhang (2003) and Beck and Eldar (2006) gave sufficient conditions under which the trust-region subproblem with one additional quadratic inequality has a tight SDP relaxation; Locatelli (2016) gave an exactness condition for a variant of the trust-region subproblem, and Burer and Ye (2019) for diagonal QCQPs. Wang and Kılınç-Karzan (2020) unified these conditions through the facial structure of , and showed in their Propositions 2 and 3 that their own hypotheses are sharp.
A QCQP in variables with constraints, of them inequalities, is
with , . Its epigraph is . With and , the SDP relaxation minimizes subject to or and ; its value is , and is the set of for which some feasible has .
For write , and . The dual set is
Assumption 1: the QCQP is feasible and for some with on the inequalities. Assumption 2: is attained whenever it is finite. Assumption 3: is polyhedral. A face of is definite if some has , and semidefinite otherwise. The quadratic eigenvalue multiplicity is the largest such that every equals for some , .
The Lean development uses the same names: QCQP N m, Opt, OptSDP, D, DSDP, Gamma, bγ, qγ, Assumption1–Assumption3, IsSemidefiniteFace, IsQuadEigMult, affdim.
The milestones pin the paper's witness, the QCQP (13): .
There is a QCQP in variables with constraints satisfying Assumptions 1 and 2, with multiplicity and on every semidefinite face, but with . The companion items about its witness (14) state , , and .
The result. Theorems 1 and 2 of the paper are the general sufficient conditions behind many earlier exactness results for SDP relaxations. Propositions 2 and 3 show that the two hypotheses are each necessary in the sense that relaxing either one by the smallest possible amount produces a counterexample: lowering the multiplicity bound by one, or replacing polyhedrality by mere attainment of the dual supremum. Anyone trying to extend the theorems therefore has to change the form of the conditions, not just their constants.
Formalizing it. Both propositions are proved in the paper; none of this has been machine-checked. A formal proof requires Lemma 1, a strong-duality statement for a parametric SDP that is reusable across the whole paper, and explicit computations of faces, affine dimensions and multiplicities for two concrete families. The multiplicity claim in particular ("the largest ") is asserted but not argued on the page, and a formal proof must supply it.
The concrete computations for (13) and (14) are elementary in isolation; the work lies in three places. First, Lemma 1 is a conic duality statement, including attainment of the outer minimum, that depends on Assumption 1; it is the bridge from the SDP to the dual set, and Mathlib has no semidefinite duality theory to build on. Second, the face structure: one must show that the hyperplane is the only semidefinite face of the halfspace of (13), and that every face of the disk of (14) gives a single point . Third, "the multiplicity is " requires ruling out every larger block structure , not only exhibiting one of size . A naive witness with only shown would establish a lower bound on the multiplicity, which is not the statement.
Points of are Fin N → ℝ; the paper's constraint is index of Fin m, and constraint is an inequality exactly when its index is below mI. and are infima in EReal, so infeasible and unbounded programs take the values rather than a junk real. A supremum bound is written as for every . Faces are nonempty convex extreme subsets of . The quadratic eigenvalue multiplicity is the greatest admitting a block form, under the identification of block , entry with coordinate . Proposition 3 says " variables"; the construction lives in , so the formal statement uses .
The goal is existential, as on the page, and a solver may exhibit any witness; it cannot be met trivially, because the multiplicity must equal exactly, the dimensions , are fixed by the type, and both and are required.
The QCQP (13) is given in full: the page states only the matrices , and the linear terms encode the constraints as . Lemma 1 is the reusable piece, and proofs of it are welcome independently of this mission; so are general lemmas on faces of halfspaces and balls and on Kronecker block structure.
A quadratically constrained quadratic program (QCQP) minimizes a quadratic function subject to quadratic inequality and equality constraints. QCQPs model trust-region subproblems, max-cut and other binary programs, phase retrieval, and many problems in signal processing and control; in general they are NP-hard. The standard tool for bounding and solving them is the Shor semidefinite relaxation (Shor 1990), which lifts the variable to a matrix and replaces every quadratic term by a linear function of . The relaxation is a convex program, so it can be solved efficiently, but it is only useful when one knows that it is tight: that its optimal value equals that of the QCQP, or, more strongly, that it describes the convex hull of the QCQP's epigraph.
Wang and Kılınç-Karzan (arXiv:1911.09195v3, Math. Program. 2021) give sufficient conditions for tightness. Section 6 of the paper concerns QCQPs with symmetry: when every quadratic form is identical copies of one smaller form, . Such problems arise as quadratic matrix programs in the sense of Beck 2007, where the variable is a matrix and the objective and constraints are traces of quadratic matrix expressions. Beck showed (Corollary 4.4) that gives value exactness under a regularity assumption; Theorem 7 of the paper gives the convex-hull result for ; this mission's Theorem 8 covers .
Fix variables and constraints. For let with symmetric, , . The QCQP is
and its epigraph is .
With , the SDP relaxation has value
and its projected epigraph is the set of for which some satisfies the constraints with . Always and .
For write and , and let . Assumption 1 requires that the QCQP be feasible and that some with on the inequalities have .
The quadratic eigenvalue multiplicity (Definition 3) is the largest integer such that and every , , equals for some . Finally,
is the hyperplane on which the SDP relaxation attains its value.
Under Assumption 1, if , then
Theorem 8 says that one copy of symmetry fewer than Theorem 7 requires still makes the SDP relaxation exact in value, and identifies the relaxation's optimal set: every optimal point of the relaxation, projected to , is a convex combination of optimal epigraph points of the QCQP. In particular the relaxation's optimal points can be decomposed into QCQP optima, which is what makes the relaxation a solution method and not only a bound. Remark 14 of the paper places the result between Beck's (only ) and Theorem 7's (the full convex hull), and records the conjecture that all three thresholds are sharp.
The theorem is proved in the paper (Appendix B). No machine-checked proof of it, or of the multiplicity results of Section 6, is known to exist. A formal proof needs a Lean development of the Shor relaxation, its Lagrangian dual, conic strong duality with dual attainment for an SDP with sign-constrained multipliers, and the Kronecker structure of the data.
The inclusion is routine. The converse needs, for an SDP-optimal point, a decomposition into feasible QCQP points that are themselves optimal. A rank-one decomposition of the SDP matrix does not suffice in general: its terms leave the feasible set unless the perturbation directions are orthogonal to all the linear parts , including the objective's. With multiplicity there is room for all orthogonality conditions; with only the constraint conditions can be imposed, and the objective condition has to come from elsewhere. The difficulty sits in that last condition and in the conic duality step, whose dual must attain its value under Assumption 1 alone (no polyhedrality of , no attainment assumption).
The Lean development lives in the namespace QCQPTightness.MultTight. The data are a structure QCQP N m with symmetric , constraints indexed by Fin m, and constraint i an inequality exactly when (i : ℕ) < mI (the paper's inequalities come first). Vectors are Fin N → ℝ; points of are pairs (x, t). and are infima in EReal, and is defined from that EReal value; this is why the goal states as a separate conjunct: if were , would be empty and the first conjunct trivial. is (Q * Y).trace; is PosSemidef; is y ⬝ᵥ y = 1. The identification sends block , entry to coordinate s + n * j.
Standing assumptions: the goal carries (p. 1) and Assumption 1. The multiplicity is the largest (IsGreatest), as on the page. The milestones take an explicit representation instead, which makes them apply to every representation, and drop and Assumption 1 where the step does not use them. The rank-induction milestone carries , which the page's sentence omits but its proof uses ("by minimality of "); without it the claim is false.
A trivializing formalization would assume system (19), or the vanishing of , in the goal; the goal assumes neither, and both are milestones to be proved.
Reusable infrastructure: the QCQP and Shor-relaxation definitions are shared with the other missions of this series, and a general SDP strong-duality statement exists on the platform (ConvexOptimization.sdp_strong_duality) in a different form (a minimization without sign-constrained variables). Contributions welcome: proofs of the milestones, a conic duality lemma with sign-constrained multipliers, and Kronecker-product lemmas such as .
Value-at-Risk (VaR) is the quantile-based capital requirement written into banking and insurance regulation (Basel, Solvency II). When several institutions, desks or subsidiaries each hold capital according to their own VaR, a natural question is how a total loss should be split among them so that the aggregate capital is as small as possible. This is the risk sharing problem, and its value is the inf-convolution of the agents' risk measures.
For VaR the problem is non-convex, so the convex-analytic toolbox of risk sharing does not apply. Embrechts, Liu and Wang (2018) solved it when every agent uses the left quantile: the inf-convolution of left VaRs at levels is the left VaR at level . The case of right quantiles, and of agents mixing the two versions, remained open. Liu, Mao, Wang and Wei close it in Theorem 1 of Inf-convolution, Optimal Allocations, and Model Uncertainty for Tail Risk Measures (Mathematics of Operations Research, 2022). This mission formalizes that theorem from the authors' SSRN version of 16 January 2022 (SSRN 3490348); all page and display numbers refer to that version.
Fix an atomless probability space : every event of positive probability contains an event of strictly smaller positive probability. A random variable is a measurable ; the set of all of them is , and a positive value of is a loss. Write . For a level ,
are the left and right VaR. They coincide unless is flat at height , in which case . For write .
Given agents with risk measures , the allocations of are (display (4)), and the inf-convolution is
An allocation attaining the infimum is optimal. A partition of is a family of measurable, pairwise disjoint events covering .
Let with and ; put if all and otherwise. Then
is optimal; 3. for every partition independent of with , the allocation (9) is optimal.
The result. Theorem 1 gives a closed form for quantile-based risk sharing among any number of agents with any mix of left and right quantiles. The answer is asymmetric: one right-quantile agent turns the whole convolution into a right quantile. Part 2 shows that the minimum is attained, and the optimal allocation has a simple shape: every agent holds an equal share of the capital, and the excess loss over the aggregate quantile goes to one agent at a time, chosen by the partition. Part 3 gives that partition explicitly when an independent randomization is available. The formulas are the base case for the paper's later results on tail risk measures (Theorems 2–4), where a VaR agent shares risk with an agent using a general tail risk measure.
Formalizing it. The theorem is proved in the paper; no machine-checked proof of it, or of (7), is known. The mission produces a checked theory of left and right quantiles on a general probability space, of inf-convolution with values in , and of the explicit optimal allocation. The milestone (7) is itself a published theorem of another paper, cited and not reproved here, so formalizing it is part of the work.
The known left-quantile result does not transfer to right quantiles. A right VaR is characterized by a family of strict tail bounds, for every (display (10)), while a left VaR needs one non-strict bound (display (11)). The events have probability strictly below but may approach as , so the split of the left-quantile case, chosen once for a fixed event, does not keep each agent's share strictly below its level. This is why the right and mixed cases were open, and why the existence part (ii) depends on the atomlessness of the space. Passing from two agents to agents requires associativity of when intermediate values may be .
All objects are defined in one file, TailRiskSharing.VaRConv.Setting:
MeasureTheory.Measure with IsProbabilityMeasure and the classical atomless property, which is the paper's standing assumption (§2.1, p. 5). It is kept on every inf-convolution statement and on the goal, including part 3, where the paper notes (Remark 3) that it is not needed.EReal, never a real sInf. Statements of the form assert equality with a coerced real number.ProbabilityTheory.Indep between the σ-algebra generated by the partition and the σ-algebra generated by .A trivializing formalization is excluded: the inf-convolution cannot collapse to a junk value of a real infimum, the levels cannot degenerate to , and the agent count cannot be .
A complete development needs the basic quantile calculus (monotonicity and left-continuity of , translation and scaling rules), a splitting lemma for atomless spaces, and the associativity of inf-convolution. These are reusable for the rest of this paper's series and for any quantile-based risk sharing result. Proofs of milestones and of the general lemmas are welcome as separate contributions.
The Frank-Wolfe algorithm (also called the conditional gradient method) minimizes a smooth convex function over a compact convex set using only a linear minimization oracle in place of a projection. Each step solves a linearized problem over the feasible set and moves toward its solution. This makes it the method of choice when projections are expensive but linear subproblems are cheap or have closed-form solutions: nuclear-norm balls, polytopes, and the semidefinite feasible sets that come up in distributionally robust estimation.
Nguyen, Shafieezadeh-Abadeh, Kuhn and Mohajerin Esfahani (arXiv:1911.03539v2, Math. Oper. Res. 48(1), 2023) need such a method for a nonlinear semidefinite program that computes Wasserstein minimax mean square error estimators. Its feasible set is not strongly convex in the traditional sense, and the linear subproblems can only be solved approximately. Section 6.1 of the paper analyses a fully adaptive Frank-Wolfe algorithm under these conditions: it uses an inexact oracle, a backtracking estimate of the smoothness constant, and a weakened, gradient-dependent notion of strong convexity of the feasible set. The section proves a linear convergence rate. This mission formalizes that rate and the lemmas of its proof.
Timeline. Frank and Wolfe (1956) introduced the method for quadratic programs. Levitin and Polyak (1966) proved linear convergence over strongly convex sets when the gradient is bounded away from zero, with the adaptive stepsize (6.4); Garber and Hazan (2015) revisited this regime. Pedregosa, Négiar, Askari and Jaggi (2020) introduced the backtracking line search with adaptive smoothness parameters β_t used here, and proved its sublinear rate. Section 6.1 combines that line search with inexact oracles and blockwise strong convexity with respect to .
The decision variable is with blocks , and carries the Euclidean norm . The problem is
where is a product of convex compact sets and is convex and differentiable on . The partial gradient with respect to block is .
An inexact oracle with precision is a map with
For it returns an exact solution of the linearized problem. At a point the search direction is and the surrogate duality gap is .
Assumption 6.1 consists of three conditions:
Algorithm 1 starts from with parameters , and . At iteration it sets and . It then picks as the smallest element of that passes the sufficient-decrease test
and moves to with that stepsize .
With , every run of Algorithm 1 satisfies
In the order the proof uses them:
The result. Theorem 6.2 gives a linear rate for a Frank-Wolfe method that never needs the global smoothness constant , that tolerates approximate linear subproblems, and that works on feasible sets which are strongly convex only in the weak, gradient-dependent sense of Assumption 6.1 (ii). In the paper it justifies the algorithm used to compute Nash equilibria of Wasserstein minimax MMSE estimation problems at dimensions where interior-point SDP solvers run out of memory. The analysis is generic and applies to any problem meeting Assumption 6.1.
Formalizing it. The result is proved in the paper, but the printed constant is wrong. In Lemma 6.3 (ii) the factor is maximized at , where it equals ; the page drops the square. Lemma 6.3 (ii), (6.12) and Theorem 6.2 are therefore false as printed for . A two-dimensional instance (unit disk, linear objective, ) violates the printed rate after one step. The printed and corrected rates agree for an exact oracle (). The mission states the corrected constant throughout and quotes the printed text in the milestones. No machine-checked proof of a linear rate for Frank-Wolfe with adaptive line search is known to us.
The obvious argument, "β-smoothness plus a contraction per step", does not go through directly. The line search may pick far below , so the contraction factor in case (ii) is controlled by and needs the separate fact that never exceeds . That fact depends on being the smallest accepted trial value, and it fails for an arbitrary accepted one. The lower bound of Lemma 6.3 (ii) comes from testing the oracle inequality against a point built from Assumption 6.1 (ii). That point is assembled block by block, and the step back to uses the Euclidean (not the sup) norm on the product space. The constant then comes from an explicit one-variable optimization, which is where the printed proof errs.
The space is PiLp 2 (fun k : Fin K => EuclideanSpace ℝ (Fin (d k))), so ‖·‖ is Euclidean and is the block gradient f s k. Conventions:
Disclosed changes relative to the page:
Trivializing readings are excluded. A sorry-free companion file exhibits, for every , an instance (interval , linear objective, exact oracle) satisfying every hypothesis of the goal, together with an explicit infinite run whose initial suboptimality is positive. The run predicate forces the smallest accepted , and the norm is Euclidean.
Everything needed is in Mathlib: gradients in Hilbert spaces, convexity, PiLp. The descent lemma along a segment for a function with Lipschitz gradient on a convex set, used for (6.9), is reusable beyond this mission. Contributions welcome: proofs of the milestones, and a Lean proof that the printed constant fails on the disk instance.
The alternating direction method of multipliers (ADMM) solves problems of the form subject to . Themelis and Patrinos (arXiv:1709.05747v4, SIAM J. Optim. 30(1):149–181, 2020) show that, for nonconvex and , ADMM is the Douglas–Rachford splitting method applied to a reformulated problem whose second term is the image function , . Their convergence theory for DRS requires the nonsmooth term to be proper and lower semicontinuous (Assumption IIa4), so whether inherits lower semicontinuity from decides whether the theory applies to a given ADMM instance.
Image functions, also called epi-compositions or infimal post-compositions, are classical objects of variational analysis (Rockafellar and Wets, Variational Analysis; Bauschke and Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces; Auslender and Teboulle, Asymptotic Cones and Functions). For convex the question of when is closed has a long history through recession functions; Section 5.4.1 of the paper gives a characterization that needs no convexity.
Let . For the domain is ; is lower semicontinuous (lsc) if its epigraph is closed, and level bounded if every set , , is bounded.
Fix a matrix . The image function of under (Definition 5.1) is
with values in . Its domain is : outside that set the infimum is over values only.
Condition (5.5) at a point compares the best value of on the affine fibre with the values of far away along directions that nearly annihilates:
The right side equals .
For every lsc and every ,
Theorem 5.11 turns Assumption IIa4, a property of a derived function, into a checkable condition on and . Its level-bounded corollary covers every lsc with bounded sublevel sets, and the characterization explains why the pathological example (5.4) of the paper, in which is even , fails: a minimizing sequence on the fibre escapes to infinity while applied to it converges. Combined with the convergence theorem for ADMM in the same paper (Theorem 5.6), this identifies the ADMM instances to which the tight DRS stepsize theory applies.
The theorem is proved in the paper. As far as is known, no machine-checked proof of it, or of any closedness criterion for image functions, exists in Lean or in Mathlib. A formalization fixes the exact range of the equivalence, which the printed statement gets wrong (see Formalization scope), and supplies reusable infrastructure: the image function in EReal, and liminfs along the filter ", ".
Lower semicontinuity of at asks that values of on fibres , , not drop below . The natural argument picks near-minimizers on these fibres and passes to a limit; this works only when the stay bounded, and nothing in lsc of alone prevents them from escaping to infinity. The difficulty is to account exactly for the unbounded case, which must be compared with the fibre through by a translation , and that requires a point with . The converse requires turning a failure of (5.5), stated as a filter liminf, into a sequence witnessing the failure of lower semicontinuity.
EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin p); is a continuous linear map between them. Every dimension, including , is allowed.EReal, and is assumed never to take the value . The image function is the EReal infimum , which may be and is off . Properness of is not assumed in the goal: if both sides hold.LowerSemicontinuousAt, the neighbourhood form of the page's sequential level-set criterion.A contextual bandit is a sequential decision problem: in each round a learner sees a context (a user's features, a patient's covariates), picks one of actions, and observes the reward of that action only. Applications include recommendation, dynamic pricing and adaptive clinical decisions. The difficulty is statistical and computational at once: the learner must explore to learn which action is best for which context, and the class of models it learns over is typically huge.
A long-standing question was whether contextual bandits can be solved optimally with nothing more than an offline regression oracle, a black-box supervised learning routine that fits a predictor of rewards to i.i.d. data. Earlier optimal algorithms either required a cost-sensitive classification oracle called many times per round (the "monster" of Agarwal et al., 2014) or an online regression oracle that must handle adversarially generated data (Foster and Rakhlin, 2020). Simchi-Levi and Xu (2022) answered the question with FALCON+, which calls an arbitrary offline regression oracle once per epoch, or times in total, and whose regret is governed by the oracle's estimation error.
Timeline:
There is a finite set of actions and a set of contexts. In round nature draws a context and a reward vector from a fixed unknown distribution ; the learner sees , picks and observes . The conditional mean reward is , and is an action maximizing . The regret after rounds is
An action selection kernel gives a probability distribution over actions for each context. The offline regression oracle takes samples and returns a predictor . It satisfies Assumption 2 with error function if, for every kernel , when the samples are i.i.d. with and , then with probability at least ,
FALCON+ runs in epochs given by a schedule . In epoch it sets and for ; it obtains by feeding only the data of epoch to the oracle (); and in every round of the epoch it plays
where maximizes . The epoch of round is .
If and for , then for every and , with probability at least ,
The paper states Theorem 2 as an bound; this is the explicit inequality its proof establishes, with the additive terms kept. It holds for every oracle, error function and schedule satisfying the hypotheses, so it is the shape of the result rather than a rate for a particular class.
In attack order: Lemma A.2 (each oracle call is accurate with probability ; the good event has probability ); Lemma A.3 (the kernel is induced by a randomized policy on ); Lemma A.4 (the conditional expected regret of a round is the implicit regret of ); Lemmas A.5 and A.6 (low predicted regret and bounded divergence ); Lemma A.7 (prediction error of implicit rewards on ); Lemma A.8 (true and predicted implicit regret agree up to factor 2 and ); Lemma A.9 (); Lemma A.10 in expectation; the Azuma display (A.10); and Lemma A.10 with high probability.
Theorem 2 makes contextual bandits reducible to offline regression with no loss in rate: for any function class with an estimation-error bound, plugging that bound into the theorem gives the regret. With empirical entropy this yields , matching the known lower bound, and for linear classes it improves the best known bound when (Examples 1–2 of the paper). The oracle is called once per epoch on i.i.d. data, so any off-the-shelf supervised learner can be used, with a guarantee transferred automatically.
Formalizing the result produces a machine-checked offline-to-online reduction, independent of the function class. The paper's result is proved, but it has no machine-checked proof; the platform has formal statements for the online-oracle algorithm SquareCB and for the classification-oracle algorithm of Agarwal et al., not for this reduction. The milestones isolate reusable facts about inverse-gap-weighted kernels (Lemmas A.3, A.5, A.6) and an epoch-wise induction pattern (Lemma A.8) that recur in later work on bandits and reinforcement learning with regression oracles.
The obvious argument fails at the regression step. A natural approach feeds all past data to the oracle, but those data are adaptively collected and not i.i.d., so an offline guarantee does not apply to them; FALCON+ uses only the previous epoch's data, which are i.i.d. given the past, and the analysis must make this conditional application of Assumption 2 rigorous on a product space (Lemma A.2). The second obstacle is that the oracle's error is measured under the kernel of the previous epoch, while regret is incurred under the current one. Transferring the error across epochs requires the divergence and the two-sided comparison of true and predicted implicit regret in Lemma A.8, proved by induction on epochs with exact constants; a one-sided bound does not close the induction.
Lean representation and conventions:
Fintype with the discrete σ-algebra. The paper claims Theorem 2 for arbitrary , but its detailed proof (App. A.1–A.6) is "under the condition that "; the uncountable case (App. A.7) is not formalized. No bound depends on .A trivializing formalization is ruled out: the goal is a bound on the realized regret of the run of Algorithm 2, whose oracle sees only samples of the previous epoch; it is not a bound for an algorithm that is handed or its population error, or that observes the full reward vector.
Infrastructure needed: conditional application of an i.i.d. guarantee inside a product measure (Fubini over Measure.infinitePi), Azuma–Hoeffding for bounded martingale differences (proved on the platform as bounded_diff_martingale_two_sided), and finite-sum algebra for inverse gap weighting. The kernel lemmas A.3, A.5 and A.6 are reusable beyond this mission. Proofs of any milestone are welcome, as are proofs of the goal from the milestones.
Nesterov's accelerated gradient method for smooth convex functions, called NAG-C in the source paper, minimizes an -smooth convex function with function values decreasing at the rate . That rate is optimal among first-order methods (Nesterov, 1983). A line of work starting with Su, Boyd & Candès (2016) studies such methods through ordinary differential equations obtained in the limit of vanishing step size. Their low-resolution ODE reproduces the function-value rate. The same ODE also models the heavy-ball method, so it cannot explain why Nesterov's method behaves differently from heavy-ball.
Shi, Du, Jordan & Su (arXiv:1810.08907v3) keep the terms of the limit, where is the step size. The resulting high-resolution ODEs contain a gradient-correction term , which is absent from the heavy-ball ODE. This mission formalizes the paper's analysis of the high-resolution ODE of NAG-C (Section 4.1, pp. 21–24). Along this ODE the smallest squared gradient norm up to time decays like , while the low-resolution ODE gives only . Small gradients are the natural stopping criterion in practice and the natural target in nonconvex and dual problems, which is why the squared gradient norm is studied separately from function values (Nesterov, 2012).
Let have gradient and Hessian . For , the class consists of the differentiable with
The class is its subclass of twice continuously differentiable functions whose Hessian is Lipschitz continuous. A minimizer of is fixed.
Given a step size , put . The high-resolution ODE of NAG-C (1.12) is
with and . The analysis uses the Lyapunov function (4.1)
With it reduces to the Lyapunov function of Su, Boyd and Candès.
For every , every step size , and every solution of (1.12),
With this is . The infimum cannot be dropped, because the gradient norm need not decrease along the trajectory.
A companion item states Corollary 4.2 (p. 24): for .
Theorem 5 is the continuous-time model of the paper's Theorem 6, which shows that NAG-C itself, without modification, drives to zero at the rate . Combining the function-value rate with gives only . Previously known rates required modified methods (Ghadimi & Lan, 2016). The proof attributes the improvement to the gradient-correction term: the factor in Lemma 4.1 comes from the term in (4.1), which exists only because of the Hessian term in (1.12). The authors conjecture that the low-resolution ODE does not achieve the rate (p. 23).
The results of Section 4.1 are proved in the paper; no machine-checked version of them is known. Formalizing them produces a checked Lyapunov analysis of a second-order ODE with Hessian damping and explicit constants. It also gives a template that the discrete analysis of NAG-C (a separate mission in this series) mirrors step by step. Related Hessian-damped systems are analysed in Attouch, Chbani, Fadili & Riahi (2020), with qualitative integrability conclusions instead of an explicit bound on the infimum.
The obvious route goes through the function-value rate and the inequality . It loses a factor of and yields only . The cubic rate needs a Lyapunov function whose derivative contains a term proportional to . Proving the derivative identity requires differentiating through the chain rule with the Hessian, and then cancelling that derivative against the gradient-correction term of the ODE. The derivative bound also uses the co-coercivity inequality of -smooth convex functions. The remaining steps are measure-theoretic: integrate a one-sided derivative bound on , and compare an infimum with a weighted average.
EuclideanSpace ℝ (Fin n), is Mathlib's gradient, and is the Fréchet derivative of the gradient map applied to .Ruled out. A formalization would hold for junk reasons in any of these cases: the infimum is written as a bounded infimum over all reals (in Lean this is ); the velocity is not tied to ; the goal is stated at (where Lean divides by ); or derivatives are written with deriv, which is where a function is not differentiable. The statements here avoid all of these.
Infrastructure. A complete development needs:
The co-coercivity inequality and the interval-integral comparison are reusable beyond this mission. Proofs of the milestones in any order are welcome, as are independent proofs of the goal.
Many nonconvex optimization problems in binary variables have a polynomial objective or polynomial constraints. The standard way to bring them into the reach of linear and mixed-integer programming solvers is to introduce one new variable per monomial and to study the convex hull of the resulting set of feasible 0/1 vectors, the multilinear polytope. Strong linear descriptions of this polytope translate directly into tighter relaxations in global solvers such as BARON, which is where the inequalities of this mission were tested (Del Pia and Khajavirad 2021, §2.5).
The multilinear polytope of a general hypergraph has no compact description, so the question is for which hypergraphs a given family of inequalities is enough. The quadratic case is classical: the Boolean quadric polytope of a graph (Padberg 1989) is described by its standard linearization exactly when the graph is a forest, and the odd-cycle inequalities are the first facets that appear on a cycle. For higher-degree monomials, Del Pia and Khajavirad showed in 2018 that their flower relaxation is exact if and only if the hypergraph is γ-acyclic. The 2021 paper introduces the stronger running intersection relaxation and asks the same question for it. This mission formalizes the necessary condition the paper proves: the relaxation cannot be exact unless the hypergraph is β-acyclic.
A hypergraph is a finite node set with a set of subsets of of size at least two (no loops, no parallel edges). Its multilinear set is
and the multilinear polytope is . The standard linearization is
An ordering of a multiset of sets is a running intersection ordering if each , , meets the union of its predecessors inside a single predecessor ; it induces and . A running intersection inequality has a center , neighbors () meeting such that admits a running intersection ordering, and nodes when these sets are nonempty:
with the number of connected components of . The running intersection relaxation is together with all these inequalities.
A β-cycle of length is a sequence of distinct nodes and distinct edges in which each lies in and and in no other ; is β-acyclic if it has none. For the subhypergraph has node set and edges .
The milestones follow the paper's proof, in order:
The result is one half of the paper's picture of when the running intersection relaxation is exact. Proposition 5 shows β-acyclicity is necessary; Theorem 3 of the paper shows that kite-free β-acyclicity is sufficient; Example 2 shows β-acyclicity alone is not. Combined with the 2018 characterization of the flower relaxation by γ-acyclicity, it places the running intersection relaxation strictly between two acyclicity notions and tells a solver designer that on hypergraphs with β-cycles some other family of cuts (for instance odd-cycle-type inequalities lifted from Padberg's) is unavoidable.
The intermediate results are reusable on their own. Lemma 5 is a general statement that multilinear polytopes of induced subhypergraphs are projections of faces, and Lemma 3 with the shortest-cycle structure step is pure hypergraph combinatorics.
The result is proved in the paper. No part of it, nor the multilinear polytope, nor the Boolean quadric polytope, is formalized in Lean or Mathlib as far as a search of the platform showed. Lemma 6 is stated in the paper without proof, and the two strictness cases are justified there by "it can be checked" and by a citation of Padberg; a formal proof closes these gaps.
The obvious argument exhibits a point of directly from a β-cycle of . This fails because a β-cycle of is surrounded by arbitrary other edges, which contribute running intersection inequalities that can cut off any candidate point. The paper's route is to pass to the subhypergraph induced by the cycle's nodes, and that step requires two facts with real content: the projection lemmas (Lemma 6 is an inclusion between relaxations defined by different families of inequalities), and the structure of , which holds only for a shortest β-cycle. A long β-cycle can have chords in .
Strictness on the two small families requires a point, or an inequality, separating from . That means controlling every running intersection inequality of the cycle, over all centers, neighbor sets, orderings and choices of , and also checking that the separating inequality is valid for .
Lean conventions:
α with decidable equality. Hypergraphs carry their node set and their edge set as Finsets, with every edge of size at least two.α ⊕ Finset α → ℝ, and every polytope of is pinned to zero off 's own coordinates, so polytopes of different hypergraphs, and the projection , live in one space.⊂ ( and ).There is one disclosed addition. Lemma 6 and the reduction step assume that has no isolated node. Without it both statements are false: since (8) has no lower bound on , a node isolated in is unbounded below in . The paper uses them only for , where the hypothesis holds. The goal itself carries no added hypothesis.
A trivializing formalization is ruled out. A relaxation missing some running intersection inequalities (a fixed ordering, a fixed , a fixed neighbor set) would make strictness easier, and an empty or mis-pinned relaxation would make the inclusion false. The definitions here take the full family.
A complete development needs:
The β-cycle and subhypergraph material and Lemma 5 are reusable beyond this mission. Contributions are welcome on any milestone, on alternative proofs of the two strictness cases (for instance by an explicit fractional point), and on a proof of Lemma 6.
Binary polynomial optimization asks to minimize a polynomial over . The standard way to attack it with linear programming is to introduce one variable for every monomial and to work with the convex hull of the resulting set of binary points. This convex hull, the multilinear polytope, is the object behind the cutting planes that global solvers such as BARON add at every node of a branch-and-bound tree, and in general its facets are as hard to describe as the original problem is to solve. The useful theory is therefore structural: which hypergraphs of monomials give multilinear polytopes with an explicit, combinatorial description.
A line of work by Del Pia and Khajavirad answers this for increasingly general classes of acyclic hypergraphs: Berge-acyclic and γ-acyclic hypergraphs via flower inequalities (SIAM J. Optim. 2018), sufficient conditions for decomposing multilinear sets (Math. Program. 2018), and, in the paper this mission formalizes (Math. Oper. Res. 2021), the running intersection inequalities, a generalization of flower inequalities that does not need γ-acyclicity. The paper reports that adding these cuts reduces BARON's root-node relaxation gap by more than 95% on most of 35 computer-vision instances.
A hypergraph has a finite node set and a set of subsets of , each with at least two nodes. Points live in , one coordinate per node and per edge. The multilinear set and multilinear polytope are
The standard linearization replaces each equation by its convex hull over the unit cube: , , and for .
An ordering of a family of sets is a running intersection ordering if each meets the union of its predecessors inside a single predecessor ; write and . Given a center edge and neighbor edges , , meeting such that the sets admit a running intersection ordering, and nodes wherever this set is nonempty, the running intersection inequality is
with the number of connected components of the hypergraph on with edges . The running intersection relaxation is together with all these inequalities.
A β-cycle is a cyclic sequence of distinct nodes and distinct edges in which lies in and and in no other edge of the cycle; is β-acyclic if it has none. A kite is three edges with , and ; is kite-free if it has none. is two-laminar if any two distinct edges sharing at least two nodes are strictly nested.
For every kite-free β-acyclic hypergraph without isolated nodes,
In attack order: validity of the inequalities (Proposition 1); heredity of β-acyclicity (Lemma 3); kite-free implies edge-induced subhypergraphs are two-laminar (Lemma 7); β-acyclicity as the running intersection property of every edge subset (Lemma 4); the explicit facet description of for two-laminar β-acyclic by system (20) (Proposition 6) and its consequence there (Corollary 3); the decomposition theorem for multilinear sets (Theorem 1); and five steps of the inductive proof of Theorem 3 in §5.3: is kite-free β-acyclic with one maximal edge fewer, the inductive step , Claim 14 on partial hypergraphs, the projection , and the Fourier–Motzkin step .
Theorem 2 (p. 1022), the polynomial-size extended formulation over the maximal edges, and the form (19) taken by running intersection inequalities in kite-free β-acyclic hypergraphs.
Theorem 3 gives a description of the multilinear polytope in the original space, by inequalities defined combinatorially from the hypergraph, for a class that strictly contains the γ-acyclic hypergraphs covered by flower inequalities. With Theorem 2 it implies that linear optimization and separation over are polynomial for kite-free β-acyclic hypergraphs, and that separation can be done without the ellipsoid method. The paper also shows (Proposition 5, a separate mission of this series) that β-acyclicity is necessary for , so the characterization sits close to the boundary of what such relaxations can achieve.
All results of this mission are proved in the paper; none is machine-checked. A complete development would be the first formal treatment of hypergraph acyclicity degrees and of multilinear polytopes, and would include a formal Fourier–Motzkin elimination argument on a structured polytope.
The inclusion is a validity check. The reverse inclusion is the content. A direct argument through integrality fails: for two-laminar β-acyclic hypergraphs, facets have general integer coefficients, so total unimodularity and balancedness arguments used for laminar hypergraphs do not apply. The decomposition step is also harder than in earlier work: the shared part of the two pieces may be an edge whose nodes are only partly covered by edges of one side, so a point cannot be written by pairing one vertex of each side. Finally, the induction lifts to , which has an extra variable, and the projection back must be shown to produce only running intersection inequalities, which requires recognizing every Fourier–Motzkin combination as one.
Nodes form a type α with Fintype and DecidableEq; a point is a function z : α ⊕ Finset α → ℝ, and every polytope of a hypergraph vanishes off that hypergraph's coordinates, so that polytopes of different hypergraphs, lifts and projections are literal sets in one space. Hypergraphs have no loops or parallel edges, as the paper assumes. Orderings are lists, 0-based. The relaxation quantifies over every center, every neighbor set, every running intersection ordering and every choice of the nodes ; the number of components counts isolated nodes and ignores loops. The standard linearization has no row , exactly as printed.
One hypothesis is added to the paper: no isolated nodes, on Theorem 3, Corollary 3, Theorem 2 and the inductive step. It is necessary: for , the point with and all other coordinates lies in but not in . No other result carries it.
A trivializing formalization is ruled out by construction: restricting the relaxation to one fixed ordering or choice of would make the goal false rather than easy, and the goal is an equality of sets, not an inclusion.
A complete development needs: convex hulls of finite sets of 0/1 points, hypergraph connectivity, β-acyclicity and the running intersection property (Lemma 4 is a classical database-theory theorem of Beeri, Fagin, Maier and Yannakakis), and Fourier–Motzkin elimination. The hypergraph acyclicity layer is reusable beyond this mission, including by the two other missions of this series. Proofs of any milestone, and of reusable lemmas on hypergraph acyclicity, are welcome.
In online allocation, requests arrive one at a time and each must be accepted or rejected on arrival, using a limited budget of resources. Revenue management, ad allocation and hiring all fit this pattern. A natural benchmark for an online policy is the prophet, or Offline: the decision maker who sees the whole arrival sequence in advance and acts optimally on it. The regret of a policy is the expected gap between Offline's value and the policy's value. Policies that track a fixed solution of a fluid relaxation lose on the order of (Proposition 1 of the paper), so the question is whether a simple adaptive policy can achieve regret bounded independently of and of the budget.
The simplest such problem is the multi-secretary problem: hire at most of sequentially arriving candidates, each drawn i.i.d. from finitely many ability classes. Arlotto and Gurvich (Stochastic Systems 2019) showed that a budget-ratio policy has regret bounded uniformly in and , using a martingale argument. Vera and Banerjee (SSRN 3158062; Management Science 2021) introduced the compensated coupling, a sample-path identity that expresses the regret of any online policy as the compensation Offline must be paid to follow it. They used it to prove constant regret for a simple re-solve-and-threshold rule, the Fluid Bayes Selector, with the explicit constant . This mission formalizes that result together with the compensated coupling it rests on.
A finite-horizon online decision problem has states , arrival types , actions , a transition function , a reward function , and a set of feasible actions in each state. Time is counted as time to go: decisions are made at , and is the type arriving at time-to-go . A standing assumption requires the best feasible reward in every state to be attained and to lie in a fixed bounded interval.
Given the whole arrival sequence, Offline's value obeys the Bellman equation
An online policy chooses a feasible action at each time from the arrivals observed so far. Starting from it produces a state process and a value , and its regret on a path is . An action is satisfying for Offline at when it attains the Bellman maximum. The disagreement set is the set of paths on which it does not, and the marginal compensation is the amount by which it falls short.
In the multi-secretary problem there are classes with rewards and arrival probabilities , i.i.d. over time (multinomial arrivals). The state is the remaining budget . Accepting needs , earns and lowers the budget by one; rejecting earns nothing. With , the Fluid Bayes Selector (Algorithm 2, in the rounded form of Appendix B.3) behaves as follows at time-to-go with budget . If it rejects. Otherwise it always accepts class , and it accepts a class iff .
For every horizon and every initial budget ,
where and . The goal keeps the paper's explicit constant: neither nor appears in it.
The result. Theorem 2 gives the best known regret bound for the multi-secretary problem with an explicit, simple constant. The compensated coupling (Lemma 1) holds for any finite-horizon problem with exogenous arrivals. It turns a regret bound into a bound on disagreement probabilities, and the paper reuses it for online packing, online matching and general online allocation, and for Bayes Selectors whose disagreement probabilities are only estimated.
Formalizing it. The theorem is proved in the paper; no machine-checked proof of it, or of the compensated coupling, is known to us. The mission produces a reusable formal model of finite-horizon online decision problems with an Offline benchmark. It also produces a formal compensated-coupling identity that applies to any policy, and a binomial Chernoff–Hoeffding bound in elementary finite-sum form. Each of these supports other missions on prophet benchmarks, resolving heuristics and network revenue management.
Comparing the online policy with one fixed offline solution does not work: Offline's optimal decisions change with every future arrival, and tracking a single offline plan only gives regret of order . The compensated coupling avoids this by re-coupling Offline to Online at every step. That shifts the difficulty to two places. The first is an exact description of when Offline's Bellman equation disagrees with the policy, which involves ties between equal rewards and the boundary budget . The second is a bound on the conditional probability of disagreement that is uniform over all budgets. That conditional probability is a binomial tail evaluated at a budget that is itself random but independent of the remaining arrivals.
Lean conventions:
Fin n with [NeZero n], and Lean index 0 is the paper's class .Antitone r, so ties are allowed.θ t is the arrival at time-to-go t, and the counts include the current arrival.The policy is the rounded rule of Appendix B.3, which always accepts class when the budget is positive. Algorithm 2 read literally would reject class when , and the bound , which excludes class , is proved for the Appendix B.3 rule. The policy is defined by its explicit thresholds and not through an arbitrary optimal solution of the fluid LP, because with tied rewards that LP has several solutions.
A formalization that replaced the expectation by a Bochner integral of a non-measurable function, or Offline by a fluid relaxation, would make the bound trivial or a different theorem. Both are excluded by construction.
Contributions are welcome at every level: proofs of the milestones, a proof of Eq. (18) from Mathlib's sub-Gaussian machinery, and lemmas computing Offline's value in the multi-secretary problem (the top- rewards among the remaining arrivals), which are reusable beyond this mission.
Douglas–Rachford splitting (DRS) minimizes a sum by alternating the proximal mappings of the two terms. It goes back to the alternating-direction schemes for heat conduction of Douglas and Rachford (1956), was cast as a splitting method for monotone operators by Lions and Mercier (1979), and through its dual form, the alternating direction method of multipliers (ADMM), it is a workhorse of signal processing, statistics and distributed optimization. For convex problems its convergence theory is complete. In applications, however, DRS and ADMM are routinely run on nonconvex problems (sparse regression with nonconvex penalties, phase retrieval, feasibility problems with nonconvex sets), and there the classical theory says nothing.
Timeline. Li and Pong (2016) proved subsequential convergence of DRS with for a smooth with Lipschitz gradient, for a sufficiently small stepsize, using the augmented Lagrangian as a merit function, and showed that cluster points are stationary. Li, Liu and Pong (Comput. Optim. Appl. 68(2), 2017) treated the Peaceman–Rachford case with a modified merit function and proved boundedness of the iterates for level-bounded . Themelis and Patrinos (arXiv:1709.05747, SIAM J. Optim. 2020) obtained convergence for every relaxation , and beyond for strongly convex , under stepsize bounds that they show to be tight. This mission formalizes that convergence result.
Let carry the Euclidean inner product and norm , and let . A function is proper if it is finite somewhere, and level bounded if every sublevel set , , is bounded. A differentiable is -smooth if , and -hypoconvex if is convex; may be negative.
Assumption I. is -smooth and -hypoconvex with ; is proper and lower semicontinuous; and has a minimizer.
The proximal mapping of with stepsize is the set
A DRS run with stepsize and relaxation is a sequence with
The Douglas–Rachford envelope (DRE) is
With , and , the admissible parameters are: with ; or, when , with .
Under Assumption I and admissible , every DRS run from any satisfies
In attack order: the lower bounds for smooth hypoconvex functions (Theorem 2.2); single-valuedness and Lipschitz properties of (Proposition 2.3(i), (ii)); real-valuedness and strict continuity of the DRE (Proposition 3.2); the sandwich (Proposition 3.3); and the equivalence of level boundedness (Theorem 3.4(i), (iii)); and the sufficient decrease
(Theorem 4.1). Two companion items: Remark 3.1 (, prox-bounded with threshold at least , and DRS runs exist from every when ) and the stationarity measure of Theorem 4.3(ii), .
The result gives convergence guarantees for DRS with any relaxation parameter on nonconvex problems where only is required to be smooth, with stepsizes up to when is convex. The companion mission on tightness (Theorem 4.7 of the paper) shows that DRS can fail to converge for , so these ranges cannot be enlarged under Assumption I. Through the equivalence of DRS and ADMM (§5 of the paper, a later mission of this series), the same conclusions transfer to nonconvex ADMM with a tight penalty bound.
The paper's proofs are complete, so the remaining work is formalization. As far as the platform's records show, no machine-checked proof of convergence of nonconvex DRS exists: the published DRS items cover the convex, monotone-operator setting only. The development also produces reusable pieces: the lower bounds for hypoconvex smooth functions, the proximal calculus of smooth functions, and the Douglas–Rachford envelope as a Lyapunov function.
In the convex case DRS is a fixed-point iteration of an averaged operator, and convergence follows from Fejér monotonicity. For nonconvex the reflected proximal maps are not nonexpansive, so this argument has no starting point. Convergence must instead come from a merit function that decreases along the iterates, and the difficulty is to find one whose decrease survives every relaxation with stepsizes all the way up to . Small-stepsize decrease estimates for do not extend to the full range. Cluster points must then be shown stationary for a lower semicontinuous, possibly nonconvex , which needs the outer semicontinuity of its proximal mapping rather than any continuity.
Points are EuclideanSpace ℝ (Fin p); every dimension , including , is allowed. is real-valued and , and are EReal-valued and never . The proximal mapping is a set, and runs are selections from it; no proximal function is chosen. The DRE is the EReal infimum of the expression above over , which is the page's value because that set is a singleton for . Stationarity is in the regular (Fréchet) subdifferential, the published platform definition NonconvexSplitting.Shared.IsRegularSubgrad; this is what the proof gives and is stronger than limiting stationarity. Cluster points are MapClusterPt points, and the rate is . All reciprocal bounds are multiplied out (, ), respecting the paper's convention .
Standing assumptions are Assumption I plus , which is added because the ranges use ; for , is affine. Three printed statements are corrected:
The goal does not mention these constants. Its hypotheses are exactly Assumption I with , , the admissible ranges, and a DRS run. The goal assumes no decrease of the envelope, no square-summability, no boundedness of the iterates, and no residual . The companion Remark 3.1 shows that runs exist, so the goal is not vacuous.
A complete development needs the regular subdifferential calculus for a smooth plus lower semicontinuous sum, the proximal optimality condition , existence of proximal points for prox-bounded lsc functions, and the outer semicontinuity of the proximal mapping. All of these are reusable beyond this mission. Contributions to any milestone, or to these general lemmas as separate theorems, are welcome.
Networks of agents that interact both cooperatively and competitively are modelled by signed graphs: a positive edge weight means that one agent moves towards another, a negative weight means that it moves towards the other's opposite. Since Altafini's work on consensus over antagonistic networks (IEEE TAC 2013), the standard target on such networks has been bipartite consensus or bipartite tracking: the agents split into two camps that converge to values of equal size and opposite sign. With a leader, the camp containing the leader tracks the leader's state and the other camp tracks its negative.
Most analyses assume that all agents update at the same instants. In practice agents sample and communicate on their own clocks. Shi, Zheng, Shao and Cheng (arXiv:2004.01867v2, SIAM J. Control Optim. 2021) handle this asynchronous setting with a matrix tool: products of sub-stochastic matrices (nonnegative, row sums at most one) whose row-sum deficits propagate along the communication graph. This mission formalizes their first application, bipartite tracking of first-order agents with a static leader (§3).
There is one leader and followers . Follower weights form a matrix : the edge exists iff , cooperative if , competitive if . The number is the weight of the leader edge , which exists iff . The digraph consists of the followers' digraph, the leader and the leader edges.
Time is discrete with step size . Follower communicates only at its own instants with and
for a constant . Positions evolve by and , with the asynchronous protocol
at the instants of , and otherwise. Here is a gain. Bipartite tracking (Definition 3.1) means for and for . With , the gain condition is
In the error coordinates on and on , the closed loop is with , where only the rows of followers active at time differ from the identity.
for every choice of instants satisfying (2.10) and every initial state.
The theorem says that asynchrony costs nothing qualitatively: as long as every follower communicates at least once every steps and the gain respects (3.7), the network reaches bipartite tracking under the same topological conditions C1 and C2 as in the synchronous case. No common clock, dwell-time condition or joint connectivity of the switching graphs is required. The same product argument is reused in the rest of the paper for second-order and general linear agents, delays and switching topologies, so the milestones here are the base case of that series.
The result is proved in the paper; it has not been formalized. Formalizing it produces a checked theory of products of sub-stochastic matrices with row-sum deficits (Theorem 2.4), which applies to positive switched systems in general, and a reusable encoding of signed digraphs with a leader, structural balance and asynchronous protocols.
Each single matrix is only marginally stable: its rows of followers that do not hear the leader at time sum to exactly one, so no single step contracts, and the spectral radius of an individual may equal one. Contraction appears only in products, and only once a deficit created at a leader edge has had time to travel along the paths of C2, one edge per window of steps; this requires that deficits never disappear again, which is where positive diagonals (from (3.7)) enter. The passage from "every window product has " to convergence also needs a uniform bound below one over all windows; the paper's (3.14) uses it without comment. The bound holds because depends on only through the set of active followers, so the window products range over a finite set.
Followers are Fin n (0-based) and the leader is not an index; is a i j and is b i. Positions lie in EuclideanSpace ℝ (Fin p); the paper's norm is unspecified and all norms on give the same limits. Eigenvalues are complex: means every element of spectrum ℂ of the complexified matrix has modulus . is the largest absolute row sum. Products multiply later factors on the left. is Real.sign. The maxima and are given as values with IsGreatest hypotheses over exactly the printed sets, and (3.7) is kept as printed. C1 is stated for the partition , the remaining followers; fixing the leader in is the paper's "with no loss of generality" convention. Definition 3.1 is stated for that same partition.
Only the "if" half of Theorem 3.3 is a target. Definition 3.1 presupposes the partition of C1, so necessity of C1 has no formal meaning, and the printed necessity argument is an informal case discussion. Theorem 2.4 2) is stated with one per row , as its proof and the example on p. 8 use it; this is implied by the literal reading.
Three formalizations would trivialize the goal and are ruled out: a protocol in which every follower updates at every step (the synchronous special case, which drops the asynchronous instants); dropping the sign conditions of C1, or leaving the leader's side free, under which the followers of need not approach ; and a goal stated about the error system (3.6) instead of the agents' positions .
The development needs finite matrix products, the ∞-norm bound on eigenvalues (Gershgorin), and elementary walk reachability in digraphs. All of these exist in Mathlib in some form. Contributions are welcome on every milestone. The product theorem 2.4 does not depend on the network model and is reusable for positive switched systems.
The Kolmogorov–Čentsov continuity criterion is the standard way to prove that a random field has a continuous version: a moment bound on increments, , yields a modification whose paths are Hölder continuous of every order (Karatzas–Shreve 1991, §2.2; Revuz–Yor 1999, Ch. I). It is used for Brownian motion, Brownian sheets, solutions of stochastic PDEs, Gaussian free field approximations and many other random fields.
The classical statement says only that the Hölder constant is finite almost surely. Many applications need more: a bound on the tail whose constant depends only on the parameters and not on the particular field, so that the bound holds uniformly over a family of fields.
This mission formalizes such a quantitative version, Proposition 2.3 in §2.3 of J. Miller and S. Sheffield, Liouville quantum gravity and the Brownian map II: geodesics and continuity of the embedding (Ann. Probab. 2021). The authors state it, note that it follows "by carefully following the proof" of the classical criterion, and write the proof out (pp. 30–31). They apply it to the circle-average process of the Gaussian free field (Proposition 2.4, p. 33) and again in Lemma 5.12 (p. 63).
The paper's main theorems (the -Liouville quantum gravity sphere equipped with the QLE(8/3, 0) metric has the law of the Brownian map; continuity of the embedding) are not part of this mission. Their objects, among them the Gaussian free field, SLE, quantum surfaces, the QLE metric of Miller–Sheffield 2020 and the Brownian map, have no formal substrate in Mathlib or on the platform. Proposition 2.3 is a self-contained probabilistic tool that the paper proves in full, and it is statable today.
Fix a dimension . The index set is the cube with the Euclidean distance . A random field is a family of real random variables on a probability space . The field satisfies the Kolmogorov condition with constants if
A modification of is a field on the same space with for every . For , the -Hölder norm of a function on the cube is
The proof works on the dyadic grid , the points of the cube whose coordinates are integer multiples of , and on the set of adjacent pairs , which differ in exactly one coordinate, by . In Lean the cube is Cube d, and the grid and the pairs are dyadicGrid d k and IsAdjacentPair d k u v.
For every there is a constant , depending only on , such that every field satisfying (2.6) has one modification with, for every ,
The tail bound (2.8) is what makes the criterion usable for families of fields. In the paper, it bounds the modulus of continuity of the Gaussian free field circle averages at every scale with a single constant, which feeds the estimates on the Liouville quantum gravity metric. More generally, polynomial tails for Hölder norms with field-independent constants are the input to tightness arguments for sequences of random fields, to union bounds over many scales or many fields, and to moment bounds for Hölder norms.
The result itself is known: the authors derive it from the textbook proof, which they write out. What is missing is a machine-checked version. At the pinned Mathlib revision, ProbabilityTheory.IsKolmogorovProcess defines the hypothesis (2.6), but no continuity theorem is proved from it, qualitative or quantitative. The platform has an Open goal for the qualitative one-parameter theorem on , KolmogorovChentsov.exists_modification_holderOnWith_Icc, a different statement that the mission does not duplicate. A proof of this mission's goal would give the classical -parameter criterion on the cube (milestone 6) and its quantitative form together.
The probabilistic steps (2.9)–(2.12) are Markov's inequality and two union bounds. They become concrete once the adjacent pairs are counted: is of order , and summing over scales needs . Formalizing them requires care with suprema in and with outer measures of events that are not obviously measurable.
The central difficulty is the deterministic chaining claim and the passage from dyadic points to the whole cube. The paper calls the claim "not difficult to see", but its constant must be uniform over pairs of dyadic points of arbitrarily fine and unequal levels, and the obvious attempt, comparing values along the straight segment between two points, fails because the points of the segment are not dyadic, so the hypothesis says nothing about them. The second difficulty is the modification itself: one field must serve every at once, must agree with almost surely at every point, and the tail bound for the dyadic supremum must transfer to the Hölder norm over the whole cube, an uncountable supremum whose event is not obviously measurable.
Cube d, the subtype of EuclideanSpace ℝ (Fin d) with coordinates in , so is Euclidean. Because all constants are existential, the statements do not depend on the norm, but Euclidean is the default reading.IsKolmogorovProcess X P α (d + β) c₀ with c₀ : ℝ≥0, plus 0 < α, 0 < β, 0 < c₀. It reads (2.6) with the lower Lebesgue integral in , so it cannot hold through a junk value of a non-integrable expectation. It also requires each pair to be Borel measurable, which is the measurability included in "random field". The probability space is [IsProbabilityMeasure P].eHolderNorm γ, valued in . A real supremum, which is 0 on unbounded families and would make (2.8) trivially true, is ruled out. The supremum of (2.12) is likewise an ℝ≥0∞-valued ⨆, and its event is , not the weaker "some term is ".Type (universe 0).A complete development needs counting lemmas for the dyadic grid, a chaining lemma on dyadic points, and the extension of a uniformly Hölder function from a dense subset (Mathlib's HolderOnWith and uniform-continuity extension tools apply). The chaining lemma and the quantitative criterion are reusable for any Hölder-regularity argument on cubes. Contributions are welcome for each milestone independently and for an alternative proof of the goal through Mathlib's PairReduction chaining machinery.
Mathlib/Probability/Process/Kolmogorov.lean (the predicate IsKolmogorovProcess). https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Probability/Process/Kolmogorov.leanSinkhorn distributionally robust optimization (Wang, Gao and Xie, arXiv:2109.11926) hedges a learning or decision problem against distribution shift. It minimizes the worst-case expected loss over all distributions within an entropically regularized optimal-transport distance (the Sinkhorn distance) of a nominal distribution . Strong duality, the subject of the first mission of this series, reduces the problem at a fixed Lagrange multiplier to minimizing an objective of nested-expectation form,
A logarithm sits between the two expectations, so a mini-batch of samples gives a biased estimate of and of its subgradients, and stochastic gradient methods do not apply directly. Problems of this shape are known as conditional stochastic optimization (Hu, Chen and He 2020, 2021; references [54], [55] of arXiv:2109.11926v5). The paper's algorithmic contribution is a biased stochastic mirror descent (BSMD) for this objective, with two subgradient estimators and explicit complexity guarantees. This mission formalizes that guarantee, Theorem 2 of the paper.
The decision lives in a closed convex set . A norm on satisfies with (Assumption EC.1), and has dual norm . A distance generating function is continuously differentiable on and -strongly convex with respect to . It induces the Bregman divergence and the prox-mapping .
The data are a probability measure and a Markov kernel on a measurable space , fixed , and a loss . Assumption 2 requires three things: (I) is convex in ; (II) it is -Lipschitz in for the Euclidean norm; (III) for . Write .
The level- approximation replaces the inner expectation by an average of i.i.d. draws:
Its sample subgradient is . The SG estimator is . The RT-MLMC estimator draws a level with probability and returns , where is the antithetic difference between the level- subgradient and the average of its two half-sample versions. BSMD iterates , , with a fresh sample at every step.
For let , , and . With the SG estimator and
or with the RT-MLMC estimator, and
the average of the iterates is δ-optimal:
Theorem 2 converts into sample complexities: draws from with either estimator. From , SG needs draws and RT-MLMC . The -rate matches the lower bound for general convex stochastic programming. This is what makes Sinkhorn DRO computationally competitive with empirical risk minimization, and it is the inner oracle of the paper's bisection search over (Theorem 3, not part of this mission). Lemma EC.7 is a reusable statement in its own right: mirror descent with uniformly biased stochastic subgradients loses only an additive .
The result is proved in the paper, partly by citation: the bias and variance bounds are attributed to Hu et al. and the BSMD bound to Nemirovski et al. To our knowledge none of it is machine-checked. The mission produces a self-contained Lean proof and, along the way, a formal mirror-descent analysis with biased oracles and an MLMC variance bound for log-sum-exp functionals.
The obvious route is to treat as an unbiased stochastic subgradient of and cite standard stochastic mirror descent. That fails because is a subgradient of , not of . Closing the gap requires the uniform bias bound of Lemma EC.6 (I), a second-order Taylor bound for on against the variance of a sample mean. The RT-MLMC bound requires the antithetic cancellation in to be exhibited explicitly. The naive bound gives no decay in , and the estimator's second moment then grows like instead of . Finally, the expectation over a run of dependent iterates needs a careful product-measure argument: the iterate is a function of , and is independent of it.
Representation. is EuclideanSpace ℝ (Fin d). The mirror norm is a function with the norm axioms and Assumption EC.1, and its dual norm is a real supremum over its unit ball. is a gradient within .
Prox-mapping. It is a map characterized by its argmin property on .
The kernel. is an arbitrary Markov kernel. This contains the paper's Gibbs kernel , which the BSMD analysis never uses.
Subgradients. "" always means a selected subgradient; no differentiability of the loss is assumed. and are given in explicit chain-rule form, the same selected subgradients in every block.
Randomness. A run of length is driven by i.i.d. samples under Measure.pi. The RT-MLMC sample is , with level reading the first draws.
Measurability and integrability. The prox-mapping and the subgradient selector are measurable. Every expectation in a conclusion comes with its integrability, which rules out a vacuous reading in which a non-integrable quantity has expectation .
Explicit forms of the paper's . The paper writes and ; its proof (p. ec20) yields the hyper-parameters stated above. They are fixed in the goal, not quantified existentially:
The max 1 guards enforce the paper's and . The sample counts are not stated as Lean claims, since they follow by construction: per iteration, one draw from , plus draws from for SG or in expectation for RT-MLMC. Remark EC.1 prints the latter as .
Two corrections to the printed text.
Contributions welcome. Proofs of the milestones. A reusable Lean development of stochastic mirror descent with biased oracles. The MLMC bias and variance lemmas for of a sample mean. A follow-up mission on the bisection search (Theorem 3).
The Conley–Zehnder index assigns an integer to a path of symplectic matrices that starts at the identity and ends at a matrix without eigenvalue . It is how periodic orbits of Hamiltonian and Reeb flows get graded. In Floer homology it gives the grading of the chain complex, generated by the -periodic orbits of a nondegenerate Hamiltonian (Salamon–Zehnder 1992; Salamon 1999). In contact homology and symplectic field theory it grades Reeb orbits. In the analysis of pseudoholomorphic curves it enters the Fredholm index formula for the linearized Cauchy–Riemann operator through the asymptotic orbits. In three-dimensional Reeb dynamics it defines dynamical convexity (every periodic orbit has index at least ), the hypothesis of the Hofer–Wysocki–Zehnder theorem on disk-like global surfaces of section (HWZ 1998).
Timeline. Conley and Zehnder introduced the index in their Morse-type index theory for periodic solutions of Hamiltonian equations (Conley–Zehnder 1984). Salamon and Zehnder gave the definition through a rotation function and related it to the Maslov index (SZ92). Robbin and Salamon extended it to arbitrary paths as a half-integer Maslov-type index (Robbin–Salamon 1993). Gutt attributes the properties naturality, homotopy, zero, product, loop, signature, determinant and inverse, and the characterization of the index by homotopy, loop and signature alone, to Salamon's lecture notes (Sal99) and to Audin–Damian (AD14); the statements used here are those of Gutt, Propositions 8–9. Gutt gives a self-contained account with several equivalent formulas, including the normalized complex determinant of the complex-linear part used below (Gutt 2014, §2).
Write with coordinates and let
The symplectic group is the set of real matrices with . Let be the set of with .
is the set of continuous paths with and . It carries the compact-open topology.
For , the complex-linear part is . It commutes with , so it has the block form , which is the complex matrix once is identified with by . Set
Let and . Each extends to a path with on , for , and . The map is then a loop in , and
For a loop with , the Maslov index is . For a symmetric matrix , is the number of positive eigenvalues minus the number of negative eigenvalues.
The map has the following three properties, and every map with these properties equals :
The result. The characterization makes the index a canonical invariant: any construction of an integer invariant of nondegenerate symplectic paths that is homotopy invariant and has the correct loop and signature behaviour is the Conley–Zehnder index. In practice this is how different definitions in the literature are identified with one another (rotation function, polar decomposition, complex-linear part, crossing forms, spectral flow of asymptotic operators). The listed properties are used directly to compute indices of concrete orbits, for instance the iterates of orbits of ellipsoids and the orbits of convex energy surfaces.
Formalizing it. All results here are classical and proved. No formalization of the Conley–Zehnder index exists in Mathlib. This mission produces a reusable library for symplectic linear algebra in Lean: the index and the Maslov index of loops as functions on path spaces, together with their computational properties. It is the first stage of a formalization of the Fredholm theory of linearized Cauchy–Riemann operators, whose index formula is stated in terms of Conley–Zehnder indices. It also gives a general-dimension definition against which the two-dimensional winding-interval definitions used in existing dynamical-convexity statements can be compared.
The index is defined through a choice: an extension of the path to inside and a continuous argument of a circle-valued map. Before any property can be stated as a property of a function, the result must be shown independent of these choices. That is not a local computation: it depends on the global topology of the symplectic group and on how the set of matrices with eigenvalue sits inside it.
The properties themselves are statements about the degree of maps into built from determinants, and is not a homomorphism. So none of the properties follows from a calculation on a single matrix, and loop and product require control of degrees under pointwise products and block sums. The uniqueness statement quantifies over all integer-valued functions on a path space. The argument for it has to use only the three listed properties and the topology of .
ConleyZehnder; all definitions are in ConleyZehnder_Setting.Matrix (Fin n ⊕ Fin n) (Fin n ⊕ Fin n) ℝ. is Mathlib's Matrix.J, and is Matrix.symplecticGroup. Paths are C(unitInterval, Mat n) with the compact-open topology. is a Set of such paths, and "connected component" means connectedComponentIn (SP n).C(unitInterval, Mat n). Every property constrains only on , and the paths , , , and are passed as continuous maps with the stated pointwise values.IsArgLift f θ means . IsCZValue ψ k says that some extension and some lifts give , where is the part of the extension after . czIndex and maslovIndex are defined by choice from these predicates, with fallback value . Milestones 2 and 3 are what make the fallback unreachable. Without them, any property proved for czIndex would say nothing about the actual index.Matrix.IsHermitian.eigenvalues; for real matrices, Hermitian means symmetric. The norm bound is stated as for every eigenvalue . The signature property is stated as .Contributions welcome: general lemmas on degrees of maps (existence and uniqueness of lifts, additivity under products and concatenation, homotopy invariance), and the topology of and . These are reusable well beyond this mission.
S. David Promislow, Fundamentals of Actuarial Mathematics (third edition, 2015), Chapter 22, Section 22.5.3, Definition 22.5 and equation (22.9), PDF pages 439–442, defines tail value-at-risk using the value-at-risk quantile plus the stop-loss expected excess divided by one minus confidence. The textbook demonstrates the error in conditioning only on losses strictly greater than, or greater than or equal to, a discrete VaR when the quantile contains an atom. Its two-coin example has losses 0, 1, 1, 2 with equal joint probabilities: and . The present mission provides an exact finite integer-lattice formalisation of that convention.
Let aggregate loss be integer valued on with nonnegative masses , usually summing to one. Choose confidence and an integer quantile . The strict tail above the quantile is
The worst fraction of outcomes includes every loss strictly larger than q, then only enough outcomes at q to complete the required probability. Write that selected quantile-point mass as
For this selection to be feasible, q must be an appropriate upper quantile, captured by
The inequalities are explicit formal hypotheses. An arbitrary q need not be a valid VaR for the given confidence, even though the algebraic TVaR expression remains defined by the source.
The expected monetary loss across the worst probability mass is
Consequently, the correct tie-adjusted tail average is
The related net stop-loss transform is
A finite reorganisation yields the fundamental actuarial formula
The term at the VaR atom contributes q times just the required fraction, not q times every atom observation. For the two-coin loss distribution , q=1 and , the strict tail is 1/4 and the selected mass at the quantile is 1/4. The numerator is , so TVaR equals 3/2. The alternatives and are not the correct tie-adjusted TVaR at this confidence.
Under nonnegative probability coefficients and positive tail probability, the stop-loss premium is nonnegative and therefore . When , the stop-loss transform is zero and TVaR equals B, provided the quantile is selected consistently.
Five definitions represent strict tail probability, net stop-loss excess expectation, selected quantile atom, selected tail monetary numerator and its normalised TVaR. Twelve supporting theorem targets establish strict-tail and excess nonnegativity, terminal bounds, atom feasibility, exact tail coverage, tail numerator algebra, the stop-loss TVaR identity, the quantile lower bound and an explicit discrete two-coin counterexample to naive conditional-tail averaging. The thirteenth target combines feasible atom allocation, TVaR/stop-loss equality and .
An independent exact-rational suite checked 84 finite claim-grid/confidence combinations, including confidence zero and near one, integer quantile boundaries, strict loss tail and selected quantile-atom fractions.
This is a finite-support discrete loss theorem and does not silently assert continuous-tail integration, arbitrary infinite-support convergence or a general proof of coherent-risk-measure subadditivity. Its connection to the bounded stop-loss mission XXVIII is mathematical only; imports of that unpublished Draft are not permitted.
S. David Promislow, Fundamentals of Actuarial Mathematics (third edition, 2015), Chapter 24, Sections 24.5.2 and 24.5.3, PDF pages 489–491, derives Bühlmann least-squares credibility and extends it to unequal period exposure using the Bühlmann–Straub model. Relevant equations are (24.13)–(24.16), and the weighted generalisation on printed page 464. A complementary openly accessible reference is Loss Data Analytics, Chapter 12, Experience Rating Using Credibility Theory, https://openacttexts.github.io/LDAVer2/ChapCredibility.html.
The book's narrative contains an apparent transposition in one terminology sentence about v and w, but its mathematical definitions and formulas consistently identify as the expected process variance and as variance of hypothetical means. This mission uses those mathematical definitions, not the reversed labels.
Let denote the underlying class of a policyholder. The collective mean risk is . Let
EPV describes claim variability within a risk, whereas VHM describes the persistent difference in expected claims between risks. If observations across periods are conditionally independent given , and period has exposure volume , a Bühlmann–Straub period mean has conditional process variance proportional to .
For n periods of observed per-unit claims , define positive total exposure and the weighted experience mean by
The least-squares credibility factor is
This is equivalent to if and , but the displayed formula also covers with positive EPV. The denominator must be strictly positive; if both variance components vanish then every credibility weight produces the same prediction-error objective, so a unique ratio must not be asserted.
The resulting credibility premium per unit exposure is
The usual risk-type prediction objective is a mean-squared error of estimating the hypothetical risk mean. Under the conditional variance and independence assumptions its quadratic part is
For positive exposure, multiplication by P does not change its minimiser. To avoid introducing division by zero into the Lean source, define the algebraically equivalent scaled risk
With nonnegative P, EPV and VHM and strictly positive sum , completing the square gives
Thus , for any real z, and the optimiser is unique since D is strictly positive. When VHM=0 and EPV>0, Z=0 and the premium is fully collective. When EPV=0 with P·VHM>0, Z=1 and the premium uses individual experience.
Promislow's printed Example 24.8 uses group exposure volumes 40, 25 and 35 and aggregate period claim totals 4,000, 2,000 and 2,500. The weighted per-person experience is . With collective mean 100, EPV 125 and VHM 5, the experience credibility is
The original example then multiplies 88 by a forecast next-period exposure of 45 to obtain expected aggregate claims 3,960. The Lean mission targets the per-unit credibility estimator, not a blanket rule that every future exposure must equal 45.
Five source definitions represent finite total exposure, weighted observations, optimal weight, credibility premium and exposure-scaled MSE. Fourteen supporting theorem targets establish exposure summation, weighted constant observations, factor bounds and boundaries, premium identities, square completion, minimum and uniqueness. The fifteenth target combines admissibility and global least-squares optimality.
An independent exact-rational check verified 609 combinations of exposure, EPV, VHM and proposed credibility factors. It checked the completed-square equality, bounded optimal factor, global minimality and uniqueness for nonzero denominators, and reproduced Example 24.8.
A general Bayesian posterior mean is not always linear in observed experience. This mission proves optimality among affine credibility estimators under the stated covariance model, rather than asserting universal posterior-mean exactness. The formal risk quadratic encodes the variance decomposition and does not itself formalise an arbitrary latent stochastic probability space.
Library primary source: S. David Promislow, Fundamentals of Actuarial Mathematics (third edition, 2015), Chapter 21, sections 21.8.1–21.9, PDF pages 411–413, particularly formula (21.9), Poisson thinning discussion on page 412 and claim-type joint mass factorisation and superposition on page 413. Further open teaching source: SCMA469 Actuarial Statistics, Chapter 5.6, Poisson process superposition and thinning, https://pairote-sat.github.io/SCMA469/poisson-processes.html. These sources distinguish single-stream thinning, independence of split streams and combination of already independent processes. The new Lean targets give explicit finite count-probability identities rather than claiming a general measure-theoretic process theorem.
For a Poisson claim frequency , define the mass at integer claim count by
A frequency class selected with probability , independently for every original claim, receives intensity ; the other class receives intensity . Their intensities must sum to . A total of claims has count probability . Given that count, exactly marked claims and unmarked claims occur with conditional binomial probability . Thus the joint count mass is
The splitting identity is the exact factorisation
This product shows independence of the two count variables, rather than deriving independence merely from matching their marginal Poisson distributions. Cases , , and count zero are included.
For independent Poisson claim-frequency streams with rates , superposition gives
The identity uses a finite convolution coefficient for each total claim count. The total-rate parameter is additive. Algebraic theorems can allow signed real parameters, while the actuarial probability interpretation requires nonnegative rates and valid marking probabilities.
Five definitions introduce Poisson count mass, count convolution, selected intensity, split count joint mass and superposed intensity. Twelve supporting theorems include the factorial count recursion, zero-count probabilities, rate partition, nonnegativity, convolution at zero, the binomial superposition identity, marked mass factorisation and zero-rate boundary. The thirteenth theorem combines exact superposition and splitting.
The substantial algebraic steps use the factorial ratio , the binomial theorem and , with all denominators equal to positive natural factorials. Count variables are nonnegative integers and finite coefficient identities do not themselves assert a construction of continuous-time Poisson processes. That stronger stochastic process claim is outside this mission.
An independent 80-digit decimal evaluation verified 1,968 count-convolution and split-joint identities, including , , , mixed rates and both zero and positive counts.
This Draft is formally self-contained. It does not import the unpublished aggregate-claims theorems from XXVII and never claims that a proof is accepted simply because an open Lean proposition elaborates in a private authoring check.
Harry H. Panjer (1980), The Aggregate Claims Distribution and Stop-Loss Reinsurance, Transactions of the Society of Actuaries 32, 523–535, examines aggregate distributions and stop-loss reinsurance. Panjer and Willmot (1982), Recursions for Compound Distributions, ASTIN Bulletin, connects efficient compound-claim recursion to net stop-loss premium calculations. Gordon E. Willmot, Steve Drekic and Jun Cai (2005), Equilibrium compound distributions and stop-loss moments, Scandinavian Actuarial Journal, DOI https://doi.org/10.1080/03461230510009691, studies tail/integrated-tail representations relevant to stop-loss valuation.
The mission gives a deliberately finite, integer-lattice and exact version of stop-loss valuation. It works on probability mass coefficients for integer aggregate losses . Some algebraic identities are true even for unnormalised real coefficients; this distinction is retained in the formal theorem types rather than assuming a distribution without stating it.
The attachment is the insurer's retained limit, with reinsurer payment at the claim settlement date of
A claim exactly equal to d pays zero excess. The expected net stop-loss premium does not contain expense or variance loading:
The insurer's retained limited expected loss is
The pointwise cashflow partition gives the actuarial bridge . It is valid for any real mass coefficients by linearity of the finite sum.
Let the strict loss tail be
when the coefficients form a normalised probability law. Raising the attachment from d to d+1 changes the payout by one unit on exactly the event . Consequently
for , and the last difference is zero outside the grid.
Because at , the adjacent recurrence telescopes into the finite discrete tail-sum identity
With nonnegative probability coefficients, tails are nonnegative and decrease with attachment. It follows that is nonnegative, nonincreasing and discretely convex:
The term at attachment B in the tail sum is zero. Deductibles above B also produce zero premium. The zero-attachment premium equals the full gross expected aggregate claim .
Five local definitions cover the nonnegative excess payment, bounded expected excess premium, strict aggregate tail, retained limited mean and gross aggregate expected claim. Fourteen supporting milestone theorems establish individual claim boundaries, payment partition, zero/full attachments, nonnegativity, one-step premium and tail differences, monotonicity, discrete convexity, the limited-mean bridge and exact tail-sum valuation.
The capstone combines in one target theorem:
An independent exact-rational verification checked 72 bounded grid/attachment cases, including deductibles above the maximum loss and unnormalised nonnegative coefficient arrays. The cashflow, increment, tail-sum and convexity identities all passed.
The bounded-grid model can be populated by Actuarial XXVI's finite individual-risk aggregate PMF. Actuarial XXVII's compound Poisson model is generally unbounded, so its full stop-loss premium requires infinite-sum convergence and cannot be treated as if it shared this finite maximum B. Such a limit and numerical truncation-error guarantee would be a separate mission.
The formal source is self-contained until earlier definitions are actually published, and never imports a theorem merely because a prior mission was drafted. All supporting and capstone theorems are open Lean proof obligations.
R. J. Verrall (1989), The individual risk model: a compound distribution, Journal of the Institute of Actuaries, volume 116(1), pages 101–107, DOI https://doi.org/10.1017/S0020268100036465, develops the connection between individual and collective aggregate-risk modelling. Nelson De Pril (1989), The Aggregate Claims Distribution in the Individual Model with Arbitrary Positive Claims, ASTIN Bulletin, volume 19(1), pages 9–24, DOI https://doi.org/10.2143/AST.19.1.2014913, develops exact aggregate-distribution recursion for the individual-risk model.
The present mission is a finite, integer-lattice, independent Bernoulli-policy formalisation. It derives probability-mass support, nonnegativity and normalisation from convolution, rather than claiming that either author already supplied these exact Lean theorem types.
Policy pays a fixed nonnegative integer benefit with probability , where . It pays nothing otherwise. The Bernoulli policy's payment distribution, as opposed to its event distribution, is
A zero-benefit policy has both events paying zero. Therefore its single payment coefficient at is , not . This corner case is explicitly retained, rather than assuming every is strictly positive.
The total loss over n independent policies is , with independent Bernoulli indicators . Its maximum possible loss is .
For coefficient arrays , define their discrete convolution by
With no policies the payment mass is . Each additional policy is introduced by
A bound-aware mass operator is . If the first distribution vanishes above B and the second above C, convolution satisfies , even for unnormalised intermediate coefficient arrays.
The companion algebraic lemmas establish convolution identity, commutativity and associativity. A distributional lemma establishes that nonnegative component masses imply nonnegative convolution coefficients.
Under for every included policy, the portfolio aggregate is a valid bounded probability mass function:
These are three distinct requirements: nonnegativity, normalisation on the exact finite benefit bound and zero support above that bound. All must be proved, including empty portfolios and policies whose benefit is zero. Independence is encoded by the convolution construction, not inferred from unrelated marginal Bernoulli probabilities.
Five new definitions introduce convolution, one-policy Bernoulli mass, bounded total mass, maximum possible claim and recursive portfolio probability mass. Fourteen supporting milestones prove convolution identities and support/mass preservation, the policy recursion, and bounded portfolio mass and nonnegativity; the fifteenth theorem is the capstone.
An independent exact-rational benchmark enumerated all binary claim/no-claim events across 1,365 distinct heterogeneous policy configurations, with zero and repeated benefits and probabilities at 0, 1/4, 1/2 and 1. Direct event enumeration agreed exactly with recursive convolution, giving nonnegative coefficients and unit total mass.
The source uses natural-valued grid claims, not continuous severities, and finite portfolios only. It does not assume any unpublished other mission's definitions exist in the Lean environment. Imported Lean definitions are local within this mission, with all imports before namespaces. Every theorem remains an open proof obligation until proved on the authoritative Prove2Me remote compiler.
Harry H. Panjer (1981), Recursive Evaluation of a Family of Compound Distributions, ASTIN Bulletin 12(1), 22–26, DOI https://doi.org/10.1017/S0515036100006796, proves a recursion for aggregate-claim distributions with suitable claim-frequency laws. The original paper treats a wider class than Poisson claim counts. Sundt and Jewell (1981), Further Results on Recursive Evaluation of Compound Distributions, ASTIN Bulletin 12(1), 27–39, DOI https://doi.org/10.1017/S0515036100006802, develops its extensions.
This mission formalises the positive-integer-severity compound Poisson case. The restriction on zero-sized claims is essential to the exact finite-count mixture used by the Lean definitions. It does not claim that a finite truncated Poisson mixture is automatically a probability distribution if zero severity has positive mass.
Let with . Its count probabilities are
Each claim has a positive integer severity with mass . The key support condition is . The usual stochastic interpretation additionally requires and total severity mass one, although the algebraic Panjer theorem itself works for arbitrary real satisfying .
For exactly m independent claims, is the m-fold discrete convolution, with and . Each positive claim contributes at least one unit, hence
It follows that the compound Poisson coefficient at aggregate loss s can be written as an exact finite sum, despite the count distribution being unbounded:
At , the distribution is . When , the zero-loss aggregate mass equals .
Panjer's recursion for this model is
It can be derived by combining the Poisson count ratio with the convolution-power coefficients. The zero-severity term has a factor j=0 and vanishes. Consequently the right-hand side at s depends only on the earlier aggregate coefficients . A separate theorem asserts that the initial mass and this recurrence uniquely determine the aggregate mass sequence.
The main Lean theorem is a conjunction of the no-claim initial value, the one-step recursion for every , and uniqueness for any real sequence satisfying those identities. It is an exact theorem about coefficients, not a numerical approximation or an unsupported claim of convergence of a severity generating function.
Five local definitions represent severity convolution, m-claim convolution powers, Poisson frequency mass, the aggregate mixture and the Panjer coefficient update. Thirteen supporting theorems include power recursion, support, count ratio, zero rate, nonnegative coefficients, the Panjer identity and uniqueness. The fourteenth is the capstone.
The independent high-precision benchmark compared two implementations: (i) direct Poisson-weighted convolution powers and (ii) the Panjer recurrence. They agreed to better than across 264 rate, severity and aggregate-size combinations using 70-digit decimal arithmetic, including zero frequency, fixed unit severity, two-point severity and a three-point severity with a gap.
The positive integer severity condition cannot simply be dropped: when zero-valued claims occur, can still contribute to aggregate loss s, and the true Poisson initial value becomes . That more general form, and arbitrary Panjer (a,b,0) counting laws, are explicitly out of scope.
No unpublished definitions are imported from Actuarial XXVI. The problem is mathematically linked but formally self-contained while XXVI is still a Draft. The theorem targets remain unproved until valid Lean submissions are accepted by Prove2Me.
Marek Kaluszka (2001), Optimal reinsurance under mean-variance premium principles, Insurance: Mathematics and Economics 28(1), 61–67, https://doi.org/10.1016/S0167-6687(00)00066-4, examines optimal retention when the reinsurance premium depends on claim mean and variance. Manuel Guerra and Maria de Lourdes Centeno (2010), Optimal Reinsurance for Variance Related Premium Calculation Principles, ASTIN Bulletin 40(1), 97–121, https://doi.org/10.2143/AST.40.1.2049220, studies the effect of variance-based loading on reinsurance decisions.
This mission isolates a clean Bernoulli claim and continuous quota-share specialisation, with a closed-form optimum and a finite-menu alternative. It does not assert the general optimal-retention functional results or the VaR/CVaR optimisations in the cited papers.
Let , where is a Bernoulli indicator with . Its claim amount is and the claim probability satisfies . A quota share is the insurer's retained proportion of each realised claim:
The reinsurer receives a fixed premium at policy inception that is an expected-value premium plus a loading on ceded variance. Using parameters and , where each variance coefficient has reciprocal currency units, define
The insurer's objective adds expected retained claims, the reinsurance premium and a variance-based risk-capital charge on retained loss:
For any real , the relevant expectation and variance formulas yield
The premium is deterministic once the contract and model are fixed, so it does not contribute additional random loss variance. A quota-share arrangement may change both the expected ceded premium and the variance of retained claims; both effects are included.
Assume in addition to nonnegative coefficients. Completing the square gives
It follows that the optimal insurer retention, not the ceded proportion, is
The solution can be at a boundary. If the insurer fully cedes the claim, . If , it retains everything, . If both coefficients vanish, all retentions have the same objective and the displayed ratio is undefined: this case is explicitly excluded. With , nonzero claim amount and positive total coefficient, is unique. For zero variance, for example or , every retention has the same variance component, so uniqueness does not follow and is not asserted.
A real insurer may instead face a finite menu of quoted retentions . Since is nonempty and finite, a cost-minimising member always exists, but there is no promise that .
The five definitions represent retained claim, ceded claim, variance premium, insurer capital objective and closed-form continuous retention. Twelve intermediate theorem obligations establish cashflow conservation, claim nonnegativity, full retention and full cession boundaries, objective expansion, admissibility of the candidate, quadratic square completion, global optimality, strict uniqueness when appropriate and finite-menu attainment. The capstone combines with for every real alternative.
The proof uses elementary real algebra and finite-set minimum selection. It requires neither local stochastic simulation nor a limit-of-policy-years theorem. The Bernoulli setup is deliberate, making the mean/variance premium principle analytically exact and testable before attempting general loss distributions.
Annual claim occurrence is a single Bernoulli event. Multiple correlated claims, expense loadings, default, credit risk, taxes, multi-period dynamic adjustment and Solvency II regulatory capital are not modelled. The capital coefficient is a chosen deterministic variance penalty rather than a regulatory capital formula. An optimal in this model should not be confused with an optimal excess-of-loss attachment point or with the entropic risk-sensitive optimum in Missions XXI–XXII.
All displayed theorem targets are unproved obligations until the authoritative Prove2Me compiler accepts a valid Lean proof. The owner Draft is for captain confirmation and moderator review, not an accepted theorem library.