Feasible Frontiers for Sub-Gamma Envelopes: the Variance–Pole Trade-off for Infinitely Divisible Laws
Yichuan Chen, Xin Wang
math.PR
Sep 19, 2026 · v1
TL;DR
The AI-use declaration reports a partial Lean 4 formalization, carried out with Claude, of the canonical factorization and exact-frontier results in Sections 2–3.
Abstract
A right sub-gamma bound is described by a quadratic proxy $v$ and a pole $c$, and the pair is not unique: enlarging either preserves it. Fixing $v$ at the variance $V$ removes the ambiguity at quadratic order but is a convention, not a consequence. For centered infinitely divisible laws with finite nonzero variance we determine the entire boundary of the feasible set, the map $v\mapsto c_*(v)$. A Beta$(1,2)$ multiplier applied to the normalised Kolmogorov canonical measure turns feasibility into a one-dimensional comparison and yields an exact variational formula: the frontier is convex, nonincreasing, and its feasible set is convex. The abscissa of convergence of the moment generating function imposes a $v$-insensitive floor on $c_*$, so a law whose variance-exact pole sits on it has a flat frontier, whereas the third-cumulant obstruction exists only at $v=V$. Whenever that pole lies strictly above both floors the frontier drops strictly as soon as $v>V$; if the control is also purely local with $κ_3^2/(9V^2)>κ_4/(12V)$, the drop has a square-root profile, and in the remaining boundary case a cube-root profile, with derivative $-\infty$ at $V$ either way. We then characterise when the optimised frontier reproduces the exact Chernoff deviation: equality holds at a level exactly when some pair on the frontier is tangent to the cumulant generating function at a Legendre maximiser for that level. At the levels tabulated in a worked example $v=V$ costs four to thirty percent; for a centered exponential a gap persists at every level, reaching thirteen percent.
Problem
Right sub-gamma bounds are described by a variance factor v and a pole c, and the pair is not unique. Fixing v at the variance V is a convention. The goal is to determine the full feasible frontier v ↦ c_*(v) for centered infinitely divisible laws with finite nonzero variance.
Approach
A Beta(1,2) multiplier is applied to the normalised Kolmogorov canonical measure, giving a factorization K_X(t)=(Vt²/2)M_R(t). This reduces feasibility to a one-dimensional comparison with a scaled exponential transform and yields an exact variational formula for the frontier. Local, boundary and interior control mechanisms are analysed, and the frontier is optimised to compare against the exact Chernoff deviation. The declaration states that the results of Sections 2–3 were partially formalized in Lean 4.
Results
The frontier is convex and nonincreasing, and the feasible set is convex. Boundary-controlled laws have flat frontiers, while locally controlled laws show square-root or cube-root drops just above V. The optimised frontier matches the Chernoff deviation exactly when some frontier pair is tangent to the cumulant generating function at a Legendre maximiser; in the worked examples, fixing v=V costs 4–30%.