Probability

Motivation

Many decision problems in operations research ask for the best element of a finite set of alternatives when each alternative's cost is random: which projects to fund when resource use is uncertain, which crew pairings to fly when delays are random, which items to pack into a knapsack whose overflow is penalized. The expected cost is rarely available in closed form, because it is a high-dimensional integral over the distribution of the random data. The sample average approximation (SAA) method replaces the expectation by an average over a random sample and solves the resulting deterministic problem with a standard discrete optimization routine. The method is widely used in stochastic programming (see Shapiro, Dentcheva and Ruszczyński, Lectures on Stochastic Programming, SIAM 2009, Ch. 5, https://doi.org/10.1137/1.9780898718751).

Kleywegt and Shapiro (preprint; published with Homem-de-Mello as SIAM J. Optim. 12(2):479–502, 2002, https://doi.org/10.1137/S1052623499363220) ask why the method works so well for discrete problems. Their answer is a large-deviations statement: when the feasible set is finite, the probability that the SAA problem returns a wrong answer decays exponentially in the sample size. This mission formalizes that result, Proposition 2.2 of the two-author preprint, together with its consistency companion, Proposition 2.1.

Setting

Let $\mathcal S$ be a nonempty finite set, $W$ a random element of a measurable space $\mathcal W$, and $G : \mathcal S \times \mathcal W \to \mathbb R$ such that $G(x,\cdot)$ is measurable and $\mathbb E|G(x,W)| < \infty$ for every $x \in \mathcal S$. The true problem (1.1) is

$$v^* = \min_{x \in \mathcal S} g(x), \qquad g(x) = \mathbb E\, G(x, W).$$

Let $W^1, W^2, \dots$ be an independent, identically distributed sample with the law of $W$. The sample average function and the SAA problem (2.1) are

$$\hat g_N(x) = \frac1N \sum_{n=1}^N G(x, W^n), \qquad \hat v_N = \min_{x \in \mathcal S} \hat g_N(x).$$

For $\varepsilon \ge 0$, the $\varepsilon$-optimal sets are $\mathcal S^\varepsilon = \{x \in \mathcal S : g(x) \le v^* + \varepsilon\}$ and $\hat{\mathcal S}^\varepsilon_N = \{x \in \mathcal S : \hat g_N(x) \le \hat v_N + \varepsilon\}$; at $\varepsilon = 0$ they are the optimal sets $\mathcal S^*$ and $\hat{\mathcal S}_N$. Two numbers drive the analysis: the maximal deviation $\delta_N = \max_{x \in \mathcal S}|\hat g_N(x) - g(x)|$ of (2.2), and the well-conditioning number

$$\alpha(\varepsilon) = \min_{x \in \mathcal S \setminus \mathcal S^\varepsilon} g(x) - v^* - \varepsilon$$

of (2.3), the gap between the $\varepsilon$-optimal solutions and the rest.

For a real random variable $X$ with moment generating function $M(t) = \mathbb E\, e^{tX}$ and logarithmic moment generating function $\Lambda(t) = \log M(t) \in (-\infty, +\infty]$, the rate function is $I(z) = \sup_{t \ge 0}\{tz - \Lambda(t)\}$. Assumption A requires that for every $x \in \mathcal S$ the moment generating function of $G(x, W)$ be finite in a neighbourhood of $t = 0$.

Formalization targets

Goal: Proposition 2.2

Under Assumption A, for every $\varepsilon \ge 0$ there is $\gamma > 0$ with

$$\limsup_{N \to \infty} \frac1N \log\Big[1 - P\big(\hat{\mathcal S}^\varepsilon_N \subset \mathcal S^\varepsilon\big)\Big] \le -\gamma. \tag{2.5}$$

The constant $\gamma$ is not specified: it depends on $\alpha(\varepsilon)$ through rate functions and cannot be computed before the problem is solved. The goal asserts only its existence, which is the paper's claim.

Milestones

1. $\alpha(\varepsilon) > 0$ whenever $\mathcal S \setminus \mathcal S^\varepsilon \ne \emptyset$ (2.3).
2. $\delta_N < \alpha(\varepsilon)/2$ implies $\hat{\mathcal S}^\varepsilon_N \subset \mathcal S^\varepsilon$.
3. The union bound $1 - P(\hat{\mathcal S}^\varepsilon_N \subset \mathcal S^\varepsilon) \le \sum_{x \in \mathcal S} P\{|\hat g_N(x) - g(x)| \ge \alpha(\varepsilon)/2\}$.
4. The large-deviations upper bound (2.4): $\frac1N \log P(Z_N \ge a) \le -I(a)$ for i.i.d. averages $Z_N$.
5. $I(a) > 0$ for $a$ above the mean, when $M$ is finite near $0$.
6. Under Assumption A, $P\{|\hat g_N(x) - g(x)| \ge r\} \le e^{-N\gamma_x} + e^{-N\gamma'_x}$ with $\gamma_x, \gamma'_x > 0$.

Companions

Proposition 2.1 ($\hat v_N \to v^*$ w.p.1, and $\hat{\mathcal S}^\varepsilon_N \subset \mathcal S^\varepsilon$ w.p.1 for $N$ large enough), the almost-sure convergence $\delta_N \to 0$ of (2.2), the singleton consequence ($\mathcal S^\varepsilon = \{x^*\}$ implies $\hat{\mathcal S}^\varepsilon_N = \{x^*\}$ eventually), the facts $I(\mu) = 0 = \min I$, the Example of §3.2 showing that a sample size $N > k/2$ can be required, and the computation $\alpha(0) = \min_i c_i$ on the hypercube with best value $1/k^{1/p}$ (§4).

Significance

Proposition 2.2 explains the practical behaviour of the SAA method on discrete problems: an exact optimal solution of the true problem is obtained with probability approaching one exponentially fast, so a moderate sample often suffices even when the number of feasible solutions is astronomically large. It is the basis of the paper's replication argument (§3.2: the probability of success $p(N)$ of one SAA replication tends to one exponentially fast) and identifies $\alpha(\varepsilon)$ as the quantity that governs the difficulty of a stochastic discrete problem, which the numerical study of §4 then examines. Later sample-size estimates for SAA (Shapiro, Dentcheva and Ruszczyński 2009, §5.3) refine the same argument into explicit, non-asymptotic bounds.

The result is proved in the paper. The mission produces a machine-checked proof of it and of its ingredients, including a Lean statement of the Cramér–Chernoff upper bound with the rate function $I$ in the extended reals and the positivity of $I$ above the mean under a local moment condition. To our knowledge none of these is formalized on the platform or in Mathlib in this form.

Difficulty

The argument is short on paper; the formal difficulty is in the large-deviations step. Mathlib has the Chernoff inequality $P(X \ge a) \le e^{-ta}\,\mathbb E e^{tX}$ and the factorization of moment generating functions of independent sums, but the step from there to $\frac1N \log P(Z_N \ge a) \le -I(a)$ requires passing to a supremum over $t$ in the extended reals, handling $t$ where $M(t) = \infty$, and the case $P(Z_N \ge a) = 0$. The positivity $I(a) > 0$ requires $\Lambda'(0) = \mu$, i.e. differentiating the moment generating function at an interior point of its domain. A naive attempt that works with real logarithms fails at probability zero, where $\log 0$ is not $-\infty$, and an attempt that bounds $\delta_N$ by Chebyshev's inequality gives only a polynomial rate.

Formalization scope

The feasible set is a Finset of an arbitrary type X, assumed nonempty; minima and maxima over it are Finset.inf' and Finset.sup', so they are attained. The sample is a sequence W : ℕ → Ω → 𝒲 of measurable maps on a probability space, mutually independent (iIndepFun) and identically distributed with W 0; the paper's $W^n$ is W (n - 1), and $g(x)$ is the expectation of $G(x, W^1)$. Measurability of $G(x,\cdot)$ is Borel measurability. Logarithms of probabilities are ENNReal.log, with $\log 0 = -\infty$, and the limit superior in (2.5) is taken in the extended reals; this is the paper's convention and it makes the goal correct when $\mathcal S^\varepsilon = \mathcal S$, where the event is sure. Assumption A is stated as integrability of $e^{tG(x,W)}$ for $t$ near $0$, not through the value of Mathlib's mgf, which is $0$ where the expectation is infinite. The logarithmic moment generating function is the published definition BellWilliams2001.ThresholdPolicy.logMGF (extended-real valued, $+\infty$ off the domain of $M$), and $I$ is the supremum over $t \ge 0$ only, as on p. 3. Wherever $\alpha(\varepsilon)$ appears, the nonemptiness of $\mathcal S \setminus \mathcal S^\varepsilon$ is a hypothesis; the goal does not mention $\alpha$ and needs none.

A trivializing formalization is ruled out: with Real.log the event "$\hat{\mathcal S}^\varepsilon_N \subset \mathcal S^\varepsilon$ is sure" would give $\log 0 = 0$ and make the goal false, and a rate function built from mgf would count infinite moment generating functions as $\Lambda = \log 0 = 0$; neither encoding is used.

A complete development needs the Cramér–Chernoff bound for i.i.d. sums with an extended-real rate function, differentiability of the moment generating function at interior points, and the strong law of large numbers applied to finitely many functions. The large-deviations items (milestones 4 and 5, and $I(\mu) = 0$) are stated for an arbitrary i.i.d. real sequence and are reusable beyond this mission. Proofs of any item, including the optional examples, are welcome.

Selected references

• A. J. Kleywegt and A. Shapiro, The sample average approximation method for stochastic discrete optimization, preprint (two-author version), https://edoc.hu-berlin.de/server/api/core/bitstreams/2dcf2d5b-5fb9-44d1-b36a-5e378c803717/content. Published with T. Homem-de-Mello in SIAM J. Optim. 12(2):479–502, 2002. https://doi.org/10.1137/S1052623499363220
• A. Dembo and O. Zeitouni, Large Deviations Techniques and Applications, 2nd ed., Springer, 1998. https://doi.org/10.1007/978-1-4612-5320-4
• A. Shapiro, D. Dentcheva and A. Ruszczyński, Lectures on Stochastic Programming: Modeling and Theory, SIAM, 2009. https://doi.org/10.1137/1.9780898718751

Motivation

A correlated equilibrium (Aumann, 1974) is a probability distribution over the strategy profiles of a game such that no player gains by deviating from the strategy it recommends. It is the natural solution concept for repeated play by adaptive agents, because the set of correlated equilibria is a polytope described by linear inequalities and, as Hart and Mas-Colell showed, it can be reached by simple learning rules that use only a player's own past payoffs and regrets.

Hart and Mas-Colell's paper (Econometrica 68 (2000) 1127–1150) has two procedures. Its Main Theorem concerns regret matching (2.2), in which a player switches away from its last strategy with probabilities proportional to its regrets; it is the subject of a companion mission. Section 3 studies a variant in which, at every period, the player plays an invariant vector of the regret matrix, and proves with Blackwell's approachability theorem (Blackwell, 1956) that the player's regrets vanish almost surely, whatever the other players do. This result, Theorem A, is the target of this mission. It is the conditional ("internal") counterpart of Hannan's no-regret property (Hannan, 1957) and the template for later internal-regret algorithms in online learning (Cesa-Bianchi and Lugosi, 2006).

Timeline. Hannan (1957) gave a procedure with vanishing unconditional regret; Blackwell (1956) proved the approachability theorem and derived a universally consistent procedure from it; Foster and Vohra (1997) obtained convergence to correlated equilibria through calibrated forecasts; Fudenberg and Levine (1995, 1999) introduced universal consistency and calibrated smooth fictitious play; Hart and Mas-Colell (2000) gave Theorem A and regret matching.

Setting

A finite game $\Gamma=(N,(S^i)_{i\in N},(u^i)_{i\in N})$ has a finite set $N$ of players, a finite nonempty strategy set $S^i$ for each player, and payoffs $u^i:S\to\mathbb R$ on $S=\prod_i S^i$. For $s\in S$ and $k\in S^i$, $u^i(k,s^{-i})$ is $i$'s payoff when $i$'s coordinate of $s$ is replaced by $k$.

The game is played at $t=1,2,\dots$. After the history $h_t=(s_1,\dots,s_t)$ each player chooses a mixed action, and given $h_t$ the players randomize independently. For $j\ne k$ in $S^i$ the regret of player $i$ for not having played $k$ whenever it played $j$ is

$$D^i_t(j,k)=\frac1t\sum_{\tau\le t:\,s^i_\tau=j}\big[u^i(k,s^{-i}_\tau)-u^i(s_\tau)\big],\qquad R^i_t(j,k)=\max\{D^i_t(j,k),0\}.$$

With $R^i_t(j,j):=0$, a probability vector $q^i_t\in\Delta(S^i)$ satisfies (3.1) if

$$\sum_{k\in S^i}q^i_t(k)R^i_t(k,j)=q^i_t(j)\sum_{k\in S^i}R^i_t(j,k)\qquad\text{for every }j\in S^i,$$

i.e. $q^i_t$ is an invariant distribution of the transition matrix of regret matching. The empirical distribution of play is $z_t(s)=\frac1t|\{\tau\le t: s_\tau=s\}|$.

Formalization targets

Goal: Theorem A (p. 1133)

If at every period $t+1$ player $i$ plays a probability vector satisfying (3.1), then, whatever the other players do,

$$R^i_t(j,k)\xrightarrow[t\to\infty]{}0\quad\text{almost surely, for all }j\ne k\text{ in }S^i.$$

Milestones (the proof of Theorem A, pp. 1135–1138)

1. (3.5): the nonnegative matrix with entries $\lambda(j,k)$ off the diagonal and $0$ on it has an invariant vector $q_\lambda\in\Delta(S^i)$.
2. (3.4a)–(3.4b): for the vector payoff $v(s^i,s^{-i})\in\mathbb R^L$, $L=\{(j,k):j\ne k\}$, the quantity $\lambda\cdot v(q,s^{-i})$ equals $\sum_j\alpha(j)u^i(j,s^{-i})$.
3. Blackwell's condition for $\mathbb R^L_-$: for $\lambda\ge0$ and $q_\lambda$ solving (3.5), $\lambda\cdot v(q_\lambda,s^{-i})=0$ for every $s^{-i}$.
4. Support function: $w_{\mathbb R^L_-}(\lambda)=0$ on $\mathbb R^L_+$ and $+\infty$ elsewhere.
5. Closest point: $D_t$ has coordinates $D^i_t(j,k)$, the projection onto $\mathbb R^L_-$ is $[D_t]^-$, and $\lambda(D_t)=[D_t]^+$ is the regret vector.
6. Blackwell's approachability theorem, "Moreover" part: the Blackwell procedure drives $\operatorname{dist}(D_t,\mathcal C)$ to $0$ almost surely against any opponent.

Companions

The Corollary (p. 1134): if every player follows (3.1), $z_t$ converges almost surely to the set of correlated equilibria. The equivalence of (3.1) with invariance for the (2.2) matrix (p. 1133). Theorem B (p. 1139): the procedure proportional to unconditional regrets $[D^i_t(k)]^+$ satisfies Hannan's universal consistency (4.1).

Significance

Theorem A shows that conditional regrets can be driven to zero by a stationary rule of fixed size $m^i\times m^i$, with no assumption on the other players beyond conditional independence. Combined with the Proposition of §3 it gives the Corollary: if all players follow such a rule, play converges to the set of correlated equilibria. The same argument with a different vector payoff yields Theorem B, a short proof of Hannan consistency. The approachability reduction used here is the standard route from vector-valued games to no-regret learning.

Theorem A and Blackwell's theorem are proved results. What this mission adds is a machine-checked development: a formal statement of Theorem A for arbitrary opponents, a formal statement of Blackwell's procedure in Hart and Mas-Colell's form (condition (3.2) via the support function, opponents that see the whole history), and the algebra connecting the two. Prove2Me already has Blackwell's original THEOREM 1 (strategies depending only on past payoff vectors, geometric separation condition); it is a different statement, and deriving this one from it, or proving it directly, is part of the work.

Difficulty

The algebra (milestones 1–5) is finite-dimensional and elementary, apart from the existence of an invariant vector, which needs a fixed-point or Perron–Frobenius type argument for a matrix that is not stochastic. The probabilistic core is milestone 6. The geometric picture of the paper (Figure 1) shows that the expected next average payoff moves closer to $\mathcal C$, but that controls only $\operatorname{dist}(E[D_{t+1}\mid h_t],\mathcal C)$, not the realized averages (footnote 15 of the paper); the opponent adapts to the whole history, so the increments are neither independent nor identically distributed, and the almost-sure statement has to be obtained on a measure known only through its conditional laws given each history.

Formalization scope

• The game is finite with nonempty strategy sets; payoffs are real. $\Delta(Q)$ is Mathlib's stdSimplex. $\mathbb R^L$ is EuclideanSpace ℝ L with its inner product and Euclidean distance.
• Time is 0-based in Lean (play τ is $s_{\tau+1}$); every regret quantity is a function of a finite history Fin t → S, and every statement uses histories of length $t+1\ge1$.
• A behaviour profile assigns a probability vector to every player, period and history. A play is any sequence of random variables on any probability space such that, given each history of positive probability, the next profile has the product law of the players' mixed actions. Theorem A constrains only player $i$, and only from period 2 on; the other players are arbitrary.
• The zero diagonal of (3.1) is explicit. The support function's value $+\infty$ is never computed in the reals: (3.2) is encoded as "$\lambda\cdot v(q_\lambda,b)\le M$ for every real upper bound $M$ of $\lambda\cdot\mathcal C$", and milestone 4 uses IsLUB/¬ BddAbove.
• In Blackwell's theorem, nonemptiness of $\mathcal C$ is stated explicitly (it is implicit in the existence of the closest point), and the choices $\lambda\mapsto q_\lambda$ and the projection $F$ are given as functions with the stated properties.
• Requiring $q^i_t$ to be a probability vector rules out the trivial solution $q=0$ of (3.1); the goal mentions neither $v$, $\mathbb R^L_-$ nor Blackwell, so it cannot be discharged by its own milestones' definitions.

Useful infrastructure, reusable beyond this mission: the existence of invariant vectors of nonnegative matrices, projections onto orthants, and a general Blackwell approachability theorem for history-dependent opponents. Proofs of any milestone, of the companions, and alternative proofs of Theorem A are welcome.

Selected references

• S. Hart and A. Mas-Colell, A simple adaptive procedure leading to correlated equilibrium, Econometrica 68(5) (2000), 1127–1150. https://doi.org/10.1111/1468-0262.00153
• D. Blackwell, An analog of the minimax theorem for vector payoffs, Pacific Journal of Mathematics 6 (1956), 1–8. https://doi.org/10.2140/pjm.1956.6.1
• R. J. Aumann, Subjectivity and correlation in randomized strategies, Journal of Mathematical Economics 1 (1974), 67–96. https://doi.org/10.1016/0304-4068(74)90037-8
• J. Hannan, Approximation to Bayes risk in repeated play, Contributions to the Theory of Games III (1957), 97–139. https://doi.org/10.1515/9781400882151-006
• D. P. Foster and R. V. Vohra, Calibrated learning and correlated equilibrium, Games and Economic Behavior 21 (1997), 40–55. https://doi.org/10.1006/game.1997.0595
• N. Cesa-Bianchi and G. Lugosi, Prediction, Learning, and Games, Cambridge University Press, 2006. https://doi.org/10.1017/CBO9780511546921

Motivation

The learning with errors (LWE) problem underlies most of post-quantum public-key cryptography. Its hardness rests on Regev's reduction from worst-case lattice problems to LWE (Regev, J. ACM 2009). The reduction is iterative: it repeatedly turns samples of a discrete Gaussian on a lattice into samples of a narrower one. Its classical step, Lemma 3.11, needs the following fact. Adding continuous Gaussian noise to a discrete Gaussian sample gives, up to a small statistical distance, a continuous Gaussian. That fact is Claim 3.9 of the paper. Through Corollary 3.10 it turns a lattice point plus noise into an LWE-type sample with a periodic Gaussian error.

The tool behind it is the smoothing parameter of Micciancio and Regev (SIAM J. Comput. 2007). Above this width a discrete Gaussian on a lattice behaves like a continuous one. Claims of this type have since become standard in lattice-based cryptography: discrete Gaussian sampling, trapdoors, and the convolution theorems of Peikert (CRYPTO 2010).

This mission formalizes Claim 3.9 from the published J. ACM article (Article 34, 2009). The paper's main theorem, Theorem 3.1, is a quantum reduction about efficient algorithms. It is outside this series of missions.

Setting

Work in $\mathbb{R}^n$ with the Euclidean norm and Lebesgue measure. For $s > 0$ the Gaussian function is $\rho_s(x) = \exp(-\pi\|x/s\|^2)$, its shift is $\rho_{s,c}(x) = \rho_s(x - c)$, and $\nu_s = \rho_s/s^n$ is a probability density (Eqs. (4)–(5)). For a countable set $A$, $\rho_s(A) = \sum_{x \in A}\rho_s(x)$.

A lattice $L \subset \mathbb{R}^n$ is the set of integer combinations of $n$ linearly independent vectors. Its dual is $L^* = \{y : \langle x, y\rangle \in \mathbb{Z}\ \forall x \in L\}$, and $\det(L^*) = 1/\det(L)$, where $\det(L)$ is the volume of a fundamental parallelepiped. For $u \in \mathbb{R}^n$ and $r > 0$, the discrete Gaussian $D_{L+u,r}$ is the distribution on the coset $L + u$ with mass $\rho_r(y)/\rho_r(L+u)$ at $y$ (Eq. (6)).

For $\epsilon > 0$ the smoothing parameter $\eta_\epsilon(L)$ is the smallest $s$ with $\rho_{1/s}(L^*\setminus\{0\}) \le \epsilon$ (Definition 2.10).

The statistical distance of two densities is $\Delta(\varphi_1,\varphi_2) = \int_{\mathbb{R}^n}|\varphi_1 - \varphi_2|$, with no factor $\tfrac12$, so it ranges in $[0,2]$.

Let $r, s > 0$ and $t = \sqrt{r^2+s^2}$. The distribution $Y$ is obtained by sampling $y \sim D_{L+u,r}$ and adding independent noise with density $\nu_s$. Its density is

$$Y(x) = \sum_{y \in L+u} D_{L+u,r}(y)\,\nu_s(x - y).$$

Formalization targets

Goal: Claim 3.9 (p. 34:25)

If $rs/t \ge \eta_\epsilon(L)$ for some $0 < \epsilon < \tfrac12$, then

$$\Delta(Y, \nu_t) \le 4\epsilon .$$

Milestones, in attack order

1. Lemma 2.14 (Poisson summation), already proved on the platform and used here as a reference: $f(L) = \det(L^*)\hat f(L^*)$.
2. The remark after Definition 2.10 (p. 34:19). The map $s \mapsto \rho_{1/s}(L^*\setminus\{0\})$ is continuous and strictly decreasing on $(0,\infty)$, with limits $\infty$ at $0$ and $0$ at $\infty$, and $\eta_\epsilon(L)$ is its inverse.
3. The Fourier transform of a shifted Gaussian (p. 34:25), $\widehat{\rho_{\sigma,c}}(w) = e^{-2\pi i\langle c,w\rangle}\sigma^n\rho_{1/\sigma}(w)$.
4. Claim 3.8 (p. 34:24). If $r \ge \eta_\epsilon(L)$, then $\rho_r(L+c) \in r^n\det(L^*)(1\pm\epsilon)$.
5. Eq. (11) (p. 34:25), $Y(x) = s^{-n}\rho_t(x)\,\rho_{rs/t,(r/t)^2x-u}(L)/\rho_{r,-u}(L)$.
6. The pointwise bound (p. 34:26), $|Y(x) - \rho_t(x)/t^n| \le \rho_t(x)/t^n\cdot 4\epsilon$.

A supporting item states the bridge used in both proofs: if $s \ge \eta_\epsilon(L)$, then $\rho_{1/s}(L^*\setminus\{0\}) \le \epsilon$.

Significance

Claim 3.9 is what makes Regev's iterative step classical. A discrete Gaussian sample, blurred by continuous noise, cannot be told apart from a continuous Gaussian of the combined width, except with probability $2\epsilon$. Corollary 3.10 projects this onto a direction $z$ and reduces it modulo 1 to obtain LWE samples with periodic Gaussian error $\Psi_\beta$. Without it, the reduction from lattice problems to LWE has no way to produce its error distribution. Claim 3.8, a milestone here, says that above the smoothing parameter the discrete Gaussian measure is almost invariant under shifts. It is the basic estimate of the theory.

The results are proved in the paper; none of them is formalized. Lean's Mathlib has lattices, their covolume, dual submodules and the Gaussian Fourier transform. The platform has the Poisson summation formula for lattices. This mission adds the smoothing parameter, discrete Gaussians on cosets, and the first machine-checked convolution theorem for discrete and continuous Gaussians. Later work, such as Corollary 3.10 or Peikert's general convolution theorem, can build on it.

Difficulty

Neither density is a finite object. $Y$ is an infinite sum over a coset of a lattice, normalized by another infinite sum. A direct term-by-term comparison of $Y(x)$ with $\nu_t(x)$ fails: the sum defining $Y(x)$ is a Gaussian sum over a shifted lattice, and its value genuinely varies with the position of $(r/t)^2x - u$ relative to $L$; for narrow Gaussians the variation is of order one. The claim is that this oscillation is uniformly small, with a relative error that depends only on $\epsilon$, not on $n$, $x$ or $u$. Two ratios of lattice sums must be bounded at once, uniformly in $x$. The constant $4\epsilon$ uses $\epsilon < \tfrac12$ in an essential way, because $(1+\epsilon)/(1-\epsilon)$ must stay below $1+4\epsilon$.

The smoothing parameter is defined as a least element. That the least element exists, i.e. that the infimum is attained, is itself a statement about continuity and strict monotonicity of an infinite sum in its width.

Formalization scope

• $\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n).
• A lattice is a Submodule ℤ with [DiscreteTopology L] [IsZLattice ℝ L].
• $L^*$ is LinearMap.BilinForm.dualSubmodule (innerₗ _) L.
• $\det(L^*)$ is written $\det(L)^{-1}$ with $\det(L)$ = ZLattice.covolume L.
• Lattice sums are real tsums. They are genuinely summable, so no summability hypothesis is added.
• $\eta_\epsilon(L)$ is the real infimum of $\{s > 0 : \rho_{1/s}(L^*\setminus\{0\}) \le \epsilon\}$. Its attainment is milestone 2, not part of the definition.
• $Y$ is defined by its density, the formula on the first line of the proof.
• $\Delta$ is a lower Lebesgue integral with values in $[0,\infty]$ and no $\tfrac12$. A Bochner integral of a non-integrable difference would be $0$ and make the bound free; this form rules that trivialization out.

Added hypotheses, each disclosed in the item.

• $\epsilon > 0$ in Claim 3.9 and the pointwise bound (Claim 3.8 prints it). Definition 2.10 defines $\eta_\epsilon$ only for $\epsilon > 0$, and for $\epsilon \le 0$ the defining set is empty, so the hypothesis $\eta_\epsilon(L) \le rs/t$ would be vacuous.
• $r > 0$ in Claim 3.8, where $\rho_r$ requires it, and likewise $s > 0$ in the supporting item "$s \ge \eta_\epsilon(L) \Rightarrow \rho_{1/s}(L^*\setminus\{0\}) \le \epsilon$".
• $n \ge 1$ in the smoothing remark, which fails for $n = 0$, where $L^*\setminus\{0\}$ is empty.

Other conventions.

• Lemma 2.14 is printed "for any function", with technical conditions omitted (p. 34:20). The referenced platform theorem is the version for Schwartz functions in translated form; every Gaussian used here is Schwartz.
• Eq. (11) is formalized as the equality of its first and fifth lines, the real-valued completing-the-square identity. The Fourier-side lines are not stated.
• The Fourier transform is Mathlib's 𝓕, $\int h(x)e^{-2\pi i\langle x,w\rangle}dx$, as on p. 34:20.

Reusable beyond this mission: the Gaussian, coset-sum and smoothing-parameter definitions, Claim 3.8, and the shifted Fourier transform. Proofs of any milestone are welcome, and so are proofs of the summability and Schwartz facts for Gaussians on lattices that every milestone needs.

Selected references

• O. Regev, On Lattices, Learning with Errors, Random Linear Codes, and Cryptography, Journal of the ACM 56(6), Article 34, 2009. https://doi.org/10.1145/1568318.1568324
• D. Micciancio and O. Regev, Worst-Case to Average-Case Reductions Based on Gaussian Measures, SIAM Journal on Computing 37(1), 2007. https://doi.org/10.1137/S0097539705447360
• C. Peikert, An Efficient and Parallel Gaussian Sampler for Lattices, CRYPTO 2010, LNCS 6223. https://doi.org/10.1007/978-3-642-14623-7_5

Motivation

The Learning with Errors (LWE) problem, introduced by Regev in On Lattices, Learning with Errors, Random Linear Codes, and Cryptography (J. ACM 56(6), 2009, Article 34; doi:10.1145/1568318.1568324), asks to recover a secret vector $s \in \mathbb{Z}_p^n$ from noisy inner products $\langle a, s\rangle/p + e \bmod 1$. The noise $e$ is drawn from a periodic normal distribution $\Psi_\beta$ on the circle $\mathbb{T} = \mathbb{R}/\mathbb{Z}$: a centred normal variable reduced modulo $1$. LWE has since become the main hardness assumption of lattice-based cryptography, including the post-quantum standards built on it.

Regev's reductions repeatedly need to compare $\Psi_\alpha$ and $\Psi_\beta$ for nearby parameters, for instance when the noise parameter is known only up to a small relative error. Claim 2.2 of the paper (p. 34:16) quantifies this: the two periodic normal distributions are close in statistical distance, linearly in the relative change $\beta/\alpha - 1$. This mission formalizes Claim 2.2 and the steps of its proof. The source is the published J. ACM article; the paper's main theorem, a quantum reduction from worst-case lattice problems to LWE, is outside this series.

Setting

Identify $\mathbb{T} = \mathbb{R}/\mathbb{Z}$ with the segment $[0,1)$ with addition modulo $1$. For $\beta > 0$ the normal density with mean $0$ and standard deviation $\beta/\sqrt{2\pi}$ is

$$\nu_\beta(x) = \frac{1}{\beta}\exp\Bigl(-\pi\Bigl(\frac{x}{\beta}\Bigr)^2\Bigr), \qquad x \in \mathbb{R},$$

(Eq. (5) in dimension one), and the periodic normal density (Eq. (7)) is its periodization

$$\Psi_\beta(r) = \sum_{k=-\infty}^{\infty} \frac{1}{\beta}\exp\Bigl(-\pi\Bigl(\frac{r-k}{\beta}\Bigr)^2\Bigr), \qquad r \in [0,1),$$

the density of a $\nu_\beta$-distributed variable reduced modulo $1$.

The statistical distance of two densities $\varphi_1, \varphi_2$ (p. 34:14) is

$$\Delta(\varphi_1, \varphi_2) = \int |\varphi_1 - \varphi_2|,$$

the integral taken over $\mathbb{R}$ for densities on the line and over $[0,1)$ for densities on $\mathbb{T}$. The paper uses this normalization without a factor $\tfrac12$, so that $\Delta$ ranges in $[0,2]$ on probability densities. In Lean these objects are RegevLWE.PeriodicGauss.nu, Psi, statDist and statDistT.

Formalization targets

Goal: Claim 2.2

For any $0 < \alpha < \beta \le 2\alpha$,

$$\Delta(\Psi_\alpha, \Psi_\beta) \le 9\Bigl(\frac{\beta}{\alpha} - 1\Bigr).$$

The hypotheses and the constant $9$ are exactly as printed.

Milestones

1. The bound on the line (proof of Claim 2.2, first sentence). For $0 < \alpha < \beta \le 2\alpha$,

$$\Delta(\nu_\alpha, \nu_\beta) \le 9\Bigl(\frac{\beta}{\alpha} - 1\Bigr).$$

2. Reduction modulo 1 does not increase $\Delta$ (p. 34:15, used on p. 34:16): for integrable $\varphi_1, \varphi_2$ on $\mathbb{R}$, the periodizations $\tilde\varphi_i(r) = \sum_k \varphi_i(r-k)$ satisfy $\Delta(\tilde\varphi_1, \tilde\varphi_2) \le \Delta(\varphi_1, \varphi_2)$.
3. The three displayed steps of the proof after normalizing to $\alpha = 1$, $\beta = 1 + \epsilon$, $0 < \epsilon \le 1$: the first display (a triangle-inequality split and an exact evaluation), the pointwise bound

$$\bigl|e^{-\pi(1-1/(1+\epsilon)^2)x^2} - 1\bigr| \le \pi\bigl(1 - 1/(1+\epsilon)^2\bigr)x^2 \le 2\pi\epsilon x^2,$$

and the final evaluation

$$\epsilon + 2\pi\epsilon\int_{\mathbb{R}} x^2 e^{-\pi x^2/(1+\epsilon)^2}\,dx = \epsilon + \epsilon(1+\epsilon)^3 \le 9\epsilon.$$

Significance

Claim 2.2 is a stability statement for the LWE error distribution. It lets an algorithm that works for one noise parameter be applied to a nearby one at a controlled cost in statistical distance, which is how Regev's reductions tolerate an approximately known parameter. It also states a quantitative fact about wrapped normal distributions, which appear outside cryptography, for example in directional statistics.

The result is proved in the paper; no machine-checked proof is known to this mission. Formalizing it produces a reusable one-dimensional toolkit: the $L^1$ distance between two centred normal densities, the second moment of a Gaussian in Regev's normalization, and the contraction of $L^1$ distance under periodization. Each of these is a building block for formalizing the rest of the paper's analysis of Gaussian noise.

Difficulty

The arithmetic is elementary; the work is in the analysis. The statement on $\mathbb{T}$ involves infinite series inside an integral, and the passage from the line to the circle requires exchanging a sum over $\mathbb{Z}$ with an integral and controlling the series almost everywhere. A direct attack on $\Psi_\alpha - \Psi_\beta$ termwise on $[0,1)$ does not by itself produce a bound in terms of $\beta/\alpha - 1$; the comparison has to be made on the line first. On the line, the scaling to $\alpha = 1$ is a change of variables in a Lebesgue integral, and the evaluation of $\int x^2 e^{-\pi x^2/\sigma^2}dx = \sigma^3/(2\pi)$ requires Gaussian moment identities in the paper's normalization rather than Mathlib's.

Formalization scope

• Reals and densities. Everything is one-dimensional over $\mathbb{R}$; distributions are represented by their densities, not by measures. $\mathbb{T}$ is the interval Set.Ico 0 1 with Lebesgue measure; $\Psi_\beta$ is a real tsum over $k \in \mathbb{Z}$, which converges absolutely for $\beta \ne 0$.
• Statistical distance. $\Delta$ is a lower Lebesgue integral ∫⁻ ENNReal.ofReal |φ₁ - φ₂| valued in $[0,\infty]$, with no factor $\tfrac12$, as on p. 34:14. Bounds are compared through ENNReal.ofReal. A Bochner integral would be $0$ on a non-integrable difference and would make any upper bound trivially true; the extended-valued integral rules this out.
• Added hypotheses. None on the goal or on the line bound. The modulo-1 milestone assumes $\varphi_1, \varphi_2$ integrable (the paper states the data-processing fact for random variables, whose densities are integrable); only the "modulo 1" instance used in the proof is stated, not the general inequality for arbitrary randomized functions. The pointwise bound is stated for every $\epsilon \ge 0$, a harmless generalization of the proof's range $0 < \epsilon \le 1$. The first display is stated as its three component facts (inequality, evaluation $= \epsilon$, and the rewriting of the integrand), which together give the printed chain.
• No trivialization. The goal is Claim 2.2 on $\mathbb{T}$, not the bound on the line, and neither side can collapse to a junk value: the left side is an extended nonnegative integral and the right side is positive under the hypotheses.
• Welcome contributions. Gaussian moment lemmas in the normalization $e^{-\pi x^2/s^2}$, the periodization contraction for general integrable functions, and a measure-level statement identifying $\Psi_\beta$ with the pushforward of $\nu_\beta$ under reduction modulo $1$.

Selected references

• O. Regev, On Lattices, Learning with Errors, Random Linear Codes, and Cryptography, Journal of the ACM 56(6), Article 34, 2009. https://doi.org/10.1145/1568318.1568324
• D. Micciancio and S. Goldwasser, Complexity of Lattice Problems: A Cryptographic Perspective, Kluwer, 2002 (cited on p. 34:15 for the data-processing property of statistical distance). https://doi.org/10.1007/978-1-4615-0897-7

Motivation

Learning with errors (LWE) asks to recover a secret vector $s \in \mathbb Z_p^n$ from noisy inner products $(a_i, \langle a_i, s\rangle + e_i)$, where the $a_i$ are uniform and the errors $e_i$ are drawn from a narrow distribution $\chi$ on $\mathbb Z_p$. Regev introduced the problem and showed that solving it is at least as hard as solving worst-case lattice problems by a quantum algorithm (Regev 2009). The same paper uses LWE to build a public-key cryptosystem, the ancestor of most lattice-based encryption schemes in use today, including the schemes standardized by NIST in 2024 (ML-KEM, derived from Kyber).

A cryptosystem has two halves: security (an eavesdropper learns nothing about the plaintext) and correctness (the legitimate receiver recovers the plaintext). This mission is the correctness half of Regev's scheme: Lemma 5.1 of the paper, which converts a tail bound on the noise into a bound on the probability that decryption fails. The source is the published article, Journal of the ACM 56(6), Article 34 (2009). The paper's main theorem, a quantum reduction from lattice problems to LWE, is outside this series.

Setting

Fix an integer $p \ge 2$ and let $\mathbb Z_p = \{0, 1, \dots, p-1\}$ with addition modulo $p$. Fix integers $n, m \ge 0$ and a probability distribution $\chi$ on $\mathbb Z_p$. All additions are in $\mathbb Z_p$, and $\langle a, s\rangle = \sum_j a_j s_j$ for $a, s \in \mathbb Z_p^n$.

• Distance from zero. For $a \in \mathbb Z_p$, $|a|$ (absZ) is the integer $a$ if $a \in \{0, \dots, \lfloor p/2\rfloor\}$ and $p - a$ otherwise.
• Convolution powers. $\chi^{\star k}$ (convPow χ k) is the law of the sum of $k$ independent samples from $\chi$; $\chi^{\star 0}$ is the point mass at $0$.
• Private key. $s \in \mathbb Z_p^n$, chosen uniformly.
• Public key. $a_1, \dots, a_m \in \mathbb Z_p^n$ independent and uniform, $e_1, \dots, e_m \in \mathbb Z_p$ independent with law $\chi$, and $(a_i, b_i)_{i=1}^m$ with $b_i = \langle a_i, s\rangle + e_i$ (publicKey).
• Encryption. A subset $S \subseteq [m]$ is chosen uniformly among all $2^m$ subsets. The bit $0$ is encrypted as $\bigl(\sum_{i\in S} a_i, \sum_{i\in S} b_i\bigr)$ and the bit $1$ as $\bigl(\sum_{i\in S} a_i, \lfloor p/2\rfloor + \sum_{i\in S} b_i\bigr)$ (encrypt).
• Decryption. A pair $(a, b)$ decrypts to $0$ if $b - \langle a, s\rangle$ is closer to $0$ than to $\lfloor p/2\rfloor$ modulo $p$, i.e. $|b - \langle a, s\rangle| < |b - \langle a, s\rangle - \lfloor p/2\rfloor|$, and to $1$ otherwise (decrypt, decodeResidue).

The outcome distribution outcome n m χ c of a bit $c$ is the law of the decrypted bit when all of $s$, $a_1,\dots,a_m$, $e_1,\dots,e_m$ and $S$ are drawn as above.

Formalization targets

Goal: Lemma 5.1 (Correctness), p. 34:35

Let $\delta > 0$ and assume that for every $k \in \{0, 1, \dots, m\}$,

$$\Pr_{e \sim \chi^{\star k}}\Bigl[\,|e| < \Bigl\lfloor \frac p2\Bigr\rfloor\Big/2\,\Bigr] > 1 - \delta .$$

Then for each bit $c \in \{0,1\}$,

$$\Pr[\text{decryption of an encryption of } c \text{ equals } c] \ge 1 - \delta ,$$

the probability being over all the randomness of the protocol. The lemma has no hard-coded parameters: $p$, $m$, $n$, $\chi$ and $\delta$ are arbitrary, and the paper's concrete choice ($p$ prime in $[n^2, 2n^2]$, $\chi = \bar\Psi_{\alpha(n)}$) is supplied separately by Claim 5.2.

Milestones (proof of Lemma 5.1, p. 34:36)

1. Residue identity. For an encryption $(a, b)$ of $0$, $b - \langle a, s\rangle = \sum_{i\in S} e_i$; for an encryption of $1$, $b - \langle a, s\rangle = \lfloor p/2\rfloor + \sum_{i\in S} e_i$.
2. Residue law. For a fixed $S$, $\sum_{i\in S} e_i \sim \chi^{\star |S|}$.
3. Rounding. If $|x| < \lfloor p/2\rfloor/2$ then $x$ is closer to $0$ than to $\lfloor p/2\rfloor$, so the residue $x$ decrypts to $0$ and the residue $\lfloor p/2\rfloor + x$ decrypts to $1$.

Significance

The result. Lemma 5.1 is the interface between the noise distribution and the scheme: any bound on the tails of the convolution powers $\chi^{\star k}$, $k \le m$, gives a bound on the decryption error, independently of the security analysis. With Claim 5.2 it shows that the paper's parameters decrypt correctly except with negligible probability. The same template (residue equals accumulated noise; small noise rounds correctly) underlies the correctness proofs of essentially every later LWE-based encryption scheme.

Formalizing it. The result is proved in the paper and is elementary; it is not open. As far as is known, no machine-checked statement of Regev's scheme as a probability experiment exists on Prove2Me; related platform items concern a different scheme (a dual-Regev variant with deterministic noise bounds over an even modulus). The mission's contribution is a faithful, reusable definition of the cryptosystem as a probability experiment over all of its randomness, together with a proof of its correctness lemma. The definitions (the distance $|\cdot|$ on $\mathbb Z_p$, convolution powers of a distribution on $\mathbb Z_p$, i.i.d. product distributions) are reusable by later missions on the security proof (Claim 5.3, Lemma 5.4) or on other LWE schemes.

Difficulty

The arithmetic is short; the work lies in the probability bookkeeping. The hypothesis controls the law of the noise for each fixed subset size, while the conclusion is about a single experiment in which $S$ is random and independent of the errors, and the keys $s$ and $a_i$ are random too. The step that needs care is identifying the law of $\sum_{i\in S} e_i$ for a fixed $S$ with $\chi^{\star|S|}$ from a product distribution, and then averaging over $S$; the uniform choices of $s$ and $a_i$ must be shown not to affect the residue. A second point is the rounding step: $|\cdot|$ is a cyclic distance on $\mathbb Z_p$, and the strict inequality $|x| < \lfloor p/2\rfloor/2$ is sharp (at $|x| = \lfloor p/2\rfloor/2$ the residue is equidistant and decrypts to $1$), so odd and even $p$ and ties must be handled exactly as printed.

Formalization scope

• $p : \mathbb N$ with [NeZero p] and the hypothesis $2 \le p$ (the paper defines $\mathbb Z_p$ for $p \ge 2$, p. 34:14). Primality, part of the paper's parameter choice, is not assumed: Lemma 5.1 does not use it.
• $\mathbb Z_p$ is ZMod p, vectors are Fin n → ZMod p, $\langle a, s\rangle$ is a ⬝ᵥ s, bits are Fin 2, and subsets of $[m]$ are Finset (Fin m).
• Distributions are PMFs. $\chi^{\star k}$ is defined recursively by binds; the i.i.d. errors use the product PMF with mass $\prod_i \chi(e_i)$; uniform choices are PMF.uniformOfFintype. The experiment outcome n m χ c draws $s$, then $a$, then $e$, then $S$, all independently.
• $|a|$ is computed from the representative a.val; $\lfloor p/2\rfloor$ is natural-number division p / 2; $\lfloor p/2\rfloor/2$ is compared in $\mathbb R$, since it can be a half-integer.
• Decryption ties ($|x| = |x - \lfloor p/2\rfloor|$) decrypt to $1$, as printed ("Otherwise, the decryption is 1").
• Probabilities in the goal are real numbers (toReal of PMF masses, exact because they are at most $1$). The form ENNReal.ofReal (1 − δ) < Pr was rejected: for $\delta \ge 1$ it would add the hypothesis $\Pr > 0$, which the page does not make.
• The goal is not a statement about a fixed key, a fixed subset $S$ or a fixed error vector: the probability is over all of $s$, $a_i$, $e_i$ and $S$, and the hypothesis quantifies over every $k \in \{0, \dots, m\}$. A formalization conditioning on any of these would be a different (weaker) theorem. For $k = 0$ the hypothesis reads $1 > 1 - \delta$, true for $\delta > 0$, so it imposes no hidden restriction.
• No printed slip was found in Lemma 5.1 or its proof.

Contributions welcome: proofs of the three milestones and the goal; general lemmas on convolution powers and product distributions of PMFs on finite groups.

Selected references

• O. Regev, On Lattices, Learning with Errors, Random Linear Codes, and Cryptography, Journal of the ACM 56(6), Article 34, 2009. https://doi.org/10.1145/1568318.1568324
• O. Regev, The Learning with Errors Problem, IEEE Conference on Computational Complexity (invited survey), 2010. https://doi.org/10.1109/CCC.2010.26
• NIST, Module-Lattice-Based Key-Encapsulation Mechanism Standard, FIPS 203, 2024. https://doi.org/10.6028/NIST.FIPS.203

Motivation

Stable distributions were proposed as models of asset returns by Mandelbrot and Fama in the 1960s, because empirical returns show heavier tails than the normal law allows; Rachev and Mittnik's monograph Stable Paretian Models in Finance (2000) collects the later development. When the vector $\varrho$ of per-share returns of $s$ assets follows a multivariate $\alpha$-stable law with $\alpha\in(1,2)$, its distribution is determined by the stability index $\alpha$, a shift $m_0\in\mathbb R^s$, and a finite Borel measure $\Gamma$ on the unit sphere, the spectral measure. The risk of a portfolio is then measured by the scale parameter of the return, and choosing an efficient portfolio becomes a deterministic optimization problem in $(\alpha,\Gamma)$.

In practice neither $\alpha$ nor $\Gamma$ is known: both are estimated from data. Whether the optimal portfolio is robust to estimation error is therefore a practical question. Section 5 of Rachev and Römisch, Quantitative stability in stochastic programming: The method of probability metrics (Math. Oper. Res. 27(4), 2002; this mission follows the authors' preprint), answers it with an explicit modulus, as an application of the paper's general stability theory for stochastic programs under perturbations of the underlying probability measure.

Setting

Fix $s\in\mathbb N$ and equip $\mathbb R^s$ with the Euclidean scalar product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$.

• $\Sigma^s=\{\xi\in\mathbb R^s:\langle\xi,\xi\rangle=1\}$ is the unit sphere, and $\mathcal P(\Sigma^s)$ is the set of Borel probability measures on it (normalized spectral measures).
• $X=\{x\in\mathbb R^s_+:\sum_{i=1}^s x_i=1\}$ is the set of portfolios: $x_i$ is the proportion of shares held in asset $i$.
• For $\alpha\in(1,2)$ and $\Gamma\in\mathcal P(\Sigma^s)$, the risk of $x$ is

$$r_{\alpha,\Gamma}(x)=\int_{\Sigma^s}|\langle x,\xi\rangle|^\alpha\,\Gamma(d\xi).$$

• Problem (22) is $\min\{r_{\alpha,\Gamma}(x):x\in X\}$, with optimal value $v(\alpha,\Gamma)$ and solution set $S(\alpha,\Gamma)$.
• The dual Lipschitz metric $\zeta_1$ (the Fortet–Mourier metric of order $1$) on $\mathcal P(\Sigma^s)$ is

$$\zeta_1(\Gamma,\tilde\Gamma)=\sup\Big\{\Big|\int_{\Sigma^s}f\,d\Gamma-\int_{\Sigma^s}f\,d\tilde\Gamma\Big|: f:\Sigma^s\to\mathbb R,\ |f(\xi)-f(\tilde\xi)|\le\|\xi-\tilde\xi\|\Big\}.$$

• The growth function of (22) is $\psi(\tau)=\min\{r_{\alpha,\Gamma}(x)-v(\alpha,\Gamma): d(x,S(\alpha,\Gamma))\ge\tau,\ x\in X\}$ for $\tau\ge0$, its generalized inverse is $\psi^{-1}(t)=\sup\{\tau\ge0:\psi(\tau)\le t\}$, and the stability modulus is $\Psi(\eta)=\eta+\psi^{-1}(2\eta)$.
• $\Gamma$ is nonsingular if $\int_{\Sigma^s}|\langle x,\xi\rangle|^2\Gamma(d\xi)=0$ implies $x=0$.

Formalization targets

Goal: Theorem 5.2, first assertion (p. 25)

For each $(\alpha,\Gamma)\in(1,2)\times\mathcal P(\Sigma^s)$ there is $\delta>0$ such that

$$\sup_{x\in S(\tilde\alpha,\tilde\Gamma)}d\big(x,S(\alpha,\Gamma)\big)\le\Psi\big(\alpha\,\zeta_1(\Gamma,\tilde\Gamma)+e^{-1}|\alpha-\tilde\alpha|\big)$$

whenever $(\tilde\alpha,\tilde\Gamma)\in(1,2)\times\mathcal P(\Sigma^s)$ and $\zeta_1(\Gamma,\tilde\Gamma)+|\alpha-\tilde\alpha|<\delta$. The modulus $\Psi$ is not fixed: it is whatever the growth of the unperturbed problem gives.

Companion: Theorem 5.2, "Moreover" (p. 25)

If $\Gamma$ is nonsingular, then (22) has a unique solution and $\Psi(\eta)\le C\eta^{1/2}$ for some $C>0$ and all sufficiently small $\eta\ge0$.

Milestones

1. Lemma 5.1, first assertion (p. 24): $f_0(\xi,x)=|\langle x,\xi\rangle|^\alpha$ is convex in $x$, and $|f_0(\xi,x)-f_0(\tilde\xi,\tilde x)|\le\alpha(\|\xi-\tilde\xi\|+\|x-\tilde x\|)$ on $\Sigma^s\times X$.
2. Lemma 5.1, second assertion (p. 24): $S(\alpha,\Gamma)\ne\emptyset$, and $\frac14\alpha(\alpha-1)\int_{\Sigma^s}|\langle x-x_*,z\rangle|^2\Gamma(dz)\le r_{\alpha,\Gamma}(x)-v(\alpha,\Gamma)$ for all $x\in X$ and some $x_*\in S(\alpha,\Gamma)$.
3. Proof of Theorem 5.2 (p. 25): $\sup_{t\in[-1,1]}\big||t|^\alpha-|t|^{\tilde\alpha}\big|\le e^{-1}|\alpha-\tilde\alpha|$.
4. Proof of Theorem 5.2 (p. 25): $|r_{\alpha,\Gamma}(x)-r_{\tilde\alpha,\tilde\Gamma}(x)|\le\alpha\zeta_1(\Gamma,\tilde\Gamma)+e^{-1}|\alpha-\tilde\alpha|$ for $x\in X$.
5. Proof of Theorem 5.2 (p. 25): for nonsingular $\Gamma$, $c\|x\|^2\le\int_{\Sigma^s}|\langle x,\xi\rangle|^2\Gamma(d\xi)$ for some $c=c(s,\Gamma)>0$.
6. Proof of Theorem 5.2 (p. 25): for nonsingular $\Gamma$, (22) has a unique solution $x_*$ and $\frac14c\alpha(\alpha-1)\|x-x_*\|^2\le r_{\alpha,\Gamma}(x)-v(\alpha,\Gamma)$ on $X$.

Significance

The theorem bounds how far the optimal portfolios can move when the stability index and the spectral measure are both perturbed, with a modulus computed from the unperturbed problem alone. Combined with the companion, the efficient portfolio of a nonsingular spectral measure is unique and moves by at most $O\big((\zeta_1(\Gamma,\tilde\Gamma)+|\alpha-\tilde\alpha|)^{1/2}\big)$. Since $\zeta_1$ metrizes weak convergence on the compact sphere, any consistent estimator of $\Gamma$ in the weak topology, together with a consistent estimator of $\alpha$, yields consistent estimates of the optimal portfolio, and convergence rates for $\zeta_1$ translate into rates for the portfolio. The paper notes (Example 5.3) that spectral measures of linear transformations of independent stable variables with a full-rank matrix are nonsingular, so the Hölder case covers the discrete spectral measures used in practice.

The result is proved in the paper; nothing here is open. To our knowledge none of it is machine-checked: Mathlib has strong convexity and the real power function but no stability theory of stochastic programs and no Fortet–Mourier metrics. The mission produces a checked proof of the result and a reusable formal treatment of the growth-function modulus $\Psi$ in a concrete, fully explicit instance.

Difficulty

The obvious argument compares the optimal values of the two problems and concludes that a perturbed minimizer is nearly optimal for the unperturbed problem. Turning near-optimality into a distance bound requires the growth function $\psi$ and its generalized inverse; $\psi$ is defined by an infimum over a set that may be empty, and $\psi^{-1}$ by a supremum that may be infinite, so this step has to be handled in extended arithmetic with care. A second difficulty is the $\zeta_1$ term: the map $\xi\mapsto|\langle x,\xi\rangle|^\alpha$ must be shown to be $\alpha$-Lipschitz on the sphere uniformly over $x\in X$, which uses $\|x\|\le1$ on the simplex. The change of exponent from $\alpha$ to $\tilde\alpha$ is controlled by a sharp calculus inequality whose constant $e^{-1}$ needs $\alpha,\tilde\alpha\ge1$. In the nonsingular case, the quadratic form $\int|\langle x,\xi\rangle|^2\Gamma(d\xi)$ must be shown to dominate $c\|x\|^2$, a compactness argument on the unit sphere of $\mathbb R^s$.

Formalization scope

• $\mathbb R^s$ is EuclideanSpace ℝ (Fin s) with coordinates indexed $0,\dots,s-1$. The paper says "the (Euclidean) scalar product", so Euclidean norms are the paper's own.
• $\Sigma^s$ is Metric.sphere 0 1. A spectral measure is a probability measure on $\mathbb R^s$ with $\Gamma((\Sigma^s)^c)=0$, and every integral is a set integral over $\Sigma^s$. For $s=0$ the sphere is empty, no spectral measure exists, and every statement is vacuous, as in the paper.
• The standing assumption $\alpha\in(1,2)$ of Section 5 is a hypothesis of every statement. The $\alpha$-stable law itself is not formalized: the characteristic function on p. 23 only motivates (22), and the mission captures problem (22) exactly.
• $\zeta_1$ is a supremum in $[0,\infty]$ over functions on $\mathbb R^s$ that are $1$-Lipschitz on $\Sigma^s$, integrated over $\Sigma^s$ only. Such functions are continuous on the compact sphere, so no integral can collapse to a default value. For probability measures, $\zeta_1\le2$.
• $v$ is the real infimum of $r_{\alpha,\Gamma}$ over $X$. $S$ is the set of minimizers. The paper's "min" in $\psi$ is read as an infimum in the extended reals, equal to $+\infty$ when no feasible point is at distance at least $\tau$. Distances to sets are extended distances (Metric.infEDist, $+\infty$ to the empty set), and $\psi^{-1}$ and $\Psi$ take values in $[0,\infty]$.
• Ruled out: a real-valued supremum for $\psi^{-1}$ (which would be $0$ on unbounded sets), a real distance (which is $0$ to the empty set), and test functions integrated over all of $\mathbb R^s$ (whose off-sphere values could make an integral undefined). Any of these would make the goal trivially true.
• "Sufficiently small $\eta$" is read as "all $\eta\in[0,\eta_0]$ for some $\eta_0>0$". Milestone 6 holds for every constant $c>0$ of the norm bound of milestone 5, fixed before $\alpha$, as $c=c(s,\Gamma)$ on the page.

Welcome contributions: the inequality $\big||t|^\alpha-|t|^{\tilde\alpha}\big|\le e^{-1}|\alpha-\tilde\alpha|$ on $[-1,1]$, strong convexity of $|t|^\alpha$ on $[-1,1]$, and a general lemma converting a growth function and a uniform objective perturbation into a distance bound; the last is reusable for every stability result of the paper.

Selected references

• S. T. Rachev, W. Römisch, Quantitative stability in stochastic programming: The method of probability metrics, Mathematics of Operations Research 27(4) (2002) 792–818. https://doi.org/10.1287/moor.27.4.792.304 (preprint at edoc.hu-berlin.de, followed here).
• S. T. Rachev, S. Mittnik, Stable Paretian Models in Finance, Wiley, Chichester, 2000 (reference [33] of the paper).
• G. Samorodnitsky, M. S. Taqqu, Stable Non-Gaussian Random Processes, Chapman & Hall, 1994. https://doi.org/10.1201/9780203738818
• B. Mandelbrot, The variation of certain speculative prices, Journal of Business 36(4) (1963) 394–419. https://doi.org/10.1086/294632
• R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3