Convex Optimization

Motivation

A robust counterpart draws a hard line. Inside the uncertainty set the constraint must hold; outside it, nothing is promised — and in a real problem the perturbation does sometimes land outside. Chapter 3 answered this for linear problems with the globalized robust counterpart: keep the constraint exactly on the normal range $\mathcal{Z}$, and let it degrade at a controlled rate outside, proportionally to the distance from $\mathcal{Z}$. That mission published Proposition 3.2.1, which says the GRC of an uncertain linear inequality is equivalent to two ordinary robust counterparts.

Chapter 11 of Ben-Tal, El Ghaoui and Nemirovski, Robust Optimization (Princeton, 2009) does the same for conic constraints, and the move is not routine. The left hand side of a conic constraint is a vector, not a scalar, so "the constraint is violated by at most $\alpha \,\mathrm{dist}(\zeta, \mathcal{Z})$" has no direct meaning. What replaces it is the observation that a scalar inequality $a^Ty - b \le 0$ is the inclusion $a^Ty - b \in \mathbf{Q} \equiv \mathcal{R}_-$, and that the violation is the distance from the left hand side to $\mathbf{Q}$. In that form the notion lifts verbatim, and the whole chapter follows.

Setting

Definition 11.1.2. Consider an uncertain convex constraint

$$\Bigl[P^0 + \sum_{\ell=1}^L \zeta_\ell P^\ell\Bigr]y - \Bigl[p^0 + \sum_{\ell=1}^L \zeta_\ell p^\ell\Bigr] \ \in\ \mathbf{Q}, \tag{11.1.4}$$

with $\mathbf{Q} \subseteq \mathcal{R}^k$ nonempty, closed and convex. Let the perturbation space split as $\mathcal{R}^L = \mathcal{R}^{L_1}\times\cdots\times\mathcal{R}^{L_S}$, each factor carrying a normal range $\mathcal{Z}^s$, a closed convex cone $\mathcal{L}^s$ and a norm $\|\cdot\|_s$, and let $\|\cdot\|_{\mathbf{Q}}$ be a norm on $\mathcal{R}^k$. A candidate $y$ is robust feasible with global sensitivities $\alpha_s$ if

$$\mathrm{dist}\bigl(P(y,\zeta), \mathbf{Q}\bigr) \ \le\ \sum_{s=1}^S \alpha_s\, \mathrm{dist}(\zeta^s, \mathcal{Z}^s|\mathcal{L}^s) \qquad \forall\, \zeta \in \mathcal{Z} + \mathcal{L}, \tag{11.1.6}$$

where $\mathrm{dist}(u,\mathbf{Q}) = \min_{v\in\mathbf{Q}}\|u - v\|_{\mathbf{Q}}$ and $\mathrm{dist}(\zeta^s,\mathcal{Z}^s|\mathcal{L}^s) = \min\{\|\zeta^s - v\|_s : v \in \mathcal{Z}^s,\ \zeta^s - v \in \mathcal{L}^s\}$.

The object that makes the analysis work is the recessive cone of $\mathbf{Q}$ (Definition 11.3.1): for any $\bar x \in \mathbf{Q}$,

$$\mathrm{Rec}(\mathbf{Q}) = \{h : \bar x + th \in \mathbf{Q}\ \ \forall t \ge 0\},$$

which does not depend on $\bar x$ and is a nonempty closed convex cone.

Formalization targets

Goal — Proposition 11.3.3, the decomposition of the conic GRC

A candidate $y$ is feasible for the GRC (11.1.6) if and only if it satisfies the system

$$\text{(a)}\quad \Bigl[P^0 + \sum_\ell \zeta_\ell P^\ell\Bigr]y - \Bigl[p^0 + \sum_\ell \zeta_\ell p^\ell\Bigr] \in \mathbf{Q} \qquad \forall \zeta \in \mathcal{Z} = \mathcal{Z}^1\times \cdots\times\mathcal{Z}^S,$$ $$\text{(b}_s)\quad \mathrm{dist}\Bigl(\sum_{\ell} [P^\ell y - p^\ell](E_s\zeta^s)_\ell,\ \mathrm{Rec}(\mathbf{Q})\Bigr) \ \le\ \alpha_s \qquad \forall \zeta^s \in \mathcal{L}^s \text{ with } \|\zeta^s\|_s \le 1, \quad s = 1,\ldots,S .$$

Line (a) is the ordinary robust counterpart over the normal range. Each line (b$_s$) is a bounded semi-infinite constraint — the perturbation ranges over the unit ball of a cone, not over an unbounded set — measuring the distance to the recessive cone rather than to $\mathbf{Q}$ itself.

Supporting targets

$$\text{(Def 11.3.1)}\quad \mathrm{Rec}(\mathbf{Q}) \text{ is independent of the base point and is a nonempty closed convex cone},$$ $$\text{(Ex 11.3.2)}\quad \mathbf{Q} \text{ bounded} \Rightarrow \mathrm{Rec}(\mathbf{Q}) = \{0\}; \quad \mathbf{Q} \text{ a cone} \Rightarrow \mathrm{Rec}(\mathbf{Q}) = \mathbf{Q}; \quad \mathrm{Rec}\{u : Au - b \in \mathbf{K}\} = \{h : Ah \in \mathbf{K}\},$$ $$\text{(Prop 11.4.1)}\quad \Psi_\Xi(\mathcal{M}) = \Psi_{\Xi_*}(\mathcal{M}^*), \qquad \Psi(\mathcal{M}) = \max\{\mathrm{dist}_{\|\cdot\|_F}(\mathcal{M}e, \mathbf{K}^F) : e \in \mathbf{K}^E,\ \|e\|_E \le 1\} .$$

Significance

The goal is the chapter's structural result and it does exactly what Proposition 3.2.1 did one level down: it converts a single semi-infinite constraint over an unbounded perturbation set into a robust counterpart over the bounded normal range plus finitely many constraints over unit balls. That matters because every tractability result of Chapters 6 to 9 is about bounded uncertainty sets; without the decomposition none of them applies to a GRC.

The two halves of the decomposition are genuinely different objects. Line (a) is familiar. Lines (b$_s$) are not: they measure the distance from a linear image of a ball to the recessive cone, and that is the function

$$\Psi(\mathcal{M}) = \max\bigl\{\mathrm{dist}(\mathcal{M}e, \mathbf{K}^F) : e \in \mathbf{K}^E,\ \|e\|_E \le 1\bigr\}$$

of §11.4, which is almost a norm on linear maps — nonnegative, positively homogeneous, subadditive, but neither symmetric nor strictly positive. Proposition 11.4.1 says this function is self-dual in the precise sense that $\Psi$ of a map with respect to a setup equals $\Psi$ of the adjoint map with respect to the dual setup: dual norms, dual cones, source and destination exchanged. That single identity is what lets every bound on $\Psi$ be computed on whichever side of the duality is tractable, and it is the engine of §11.4's tractability results.

The recessive cone results are the vocabulary. The one that earns its place is $\mathrm{Rec}\{u : Au - b \in \mathbf{K}\} = \{h : Ah \in \mathbf{K}\}$: the conic sets of this book are all of that form, so it says the recessive cone of every constraint in sight is computed by deleting the constant term.

Difficulty

The goal is an equivalence and the two directions are asymmetric.

Forward — GRC implies the system — is where the recessive cone is discovered rather than used. Fix $\bar\zeta \in \mathcal{Z}$ and $\zeta^s$ in the unit ball of $\mathcal{L}^s$, and run $\zeta_i = \bar\zeta + i\,\zeta^s$ out along the cone. The GRC bounds the distance to $\mathbf{Q}$ by $\alpha_s i$, so there are $q_i \in \mathbf{Q}$ with $\|P(y,\bar\zeta) + i\Phi(y)E_s\zeta^s - q_i\|_{\mathbf{Q}} \le \alpha_s i$; the rescaled points $q_i/i$ stay bounded, and a limit point of them lies in $\mathrm{Rec}(\mathbf{Q})$ by the limit characterization of the recessive cone. This is a genuine compactness argument, and it is why the recessive cone — not $\mathbf{Q}$ — is what appears in lines (b$_s$).

Backward is a decomposition-and-assemble: split each $\zeta^s = \bar\zeta^s + \delta^s$ with $\bar\zeta^s \in \mathcal{Z}^s$, $\delta^s \in \mathcal{L}^s$ realizing the distance, get a point of $\mathbf{Q}$ from line (a) and a recession direction from each line (b$_s$), and add them — using that $\mathbf{Q} + \mathrm{Rec}(\mathbf{Q}) \subseteq \mathbf{Q}$.

Proposition 11.4.1 is a chain of polarity identities: the polar of $X + K$ is $X^o \cap (-K_*)$ for compact convex $X$ containing the origin, the polar of a norm ball of radius $\alpha$ is the dual-norm ball of radius $1/\alpha$, and bipolarity. Each step is standard and the composition is not.

Formalization scope

Built on the module published by the third mission of this series, which carries the linear-case globalized robust counterpart and the dual cone. New here: norms as functions with their defining properties, dual norms, the two distances, the recessive cone, the conic GRC, and the function $\Psi$.

Conventions committed to:

• Norms are functions carrying an explicit predicate, not typeclass instances. Chapter 11 quantifies over arbitrary norms $\|\cdot\|_{\mathbf{Q}}$ and $\|\cdot\|_s$ on fixed coordinate spaces, and a statement must be able to range over them; a typeclass instance would fix one norm per type. IsNormOn bundles definiteness, absolute homogeneity and the triangle inequality, and nonnegativity follows from them.
• The dual norm is a predicate, not a construction. $\|f\|^* = \sup\{f^Te : \|e\| \le 1\}$ is asserted as a least upper bound of the set of values, so no supremum is taken on faith.
• Distances are infima, not minima. The source writes $\min$, which is correct because the sets are closed; writing $\inf$ avoids carrying an attainment proof into every statement, and agrees with the minimum whenever the source's own hypotheses hold.
• The recessive cone is indexed by a base point. Definition 11.3.1 defines it at an arbitrary $\bar x \in \mathbf{Q}$ and then asserts independence of the choice; that assertion is one of the published items, so the definition cannot presuppose it.
• The perturbation is carried as a family of blocks, $\zeta = (\zeta^1,\ldots,\zeta^S)$ with $\zeta^s \in \mathcal{R}^{L_s}$, rather than as a single vector in $\mathcal{R}^L$ together with the embeddings $E_s$. This is the same data and removes the index bookkeeping of $E_s$ from every statement.
• $\Psi$ is a predicate on a real number, as for the dual norm and for the same reason.
• §11.2 and §11.5 are out of scope: the definition of a tight safe approximation of a GRC and the worked analysis of nonexpansive dynamical systems. The first is a definition the chapter uses only to phrase §11.4's programme, the second an application.

Selected references

• A. Ben-Tal, L. El Ghaoui and A. Nemirovski, Robust Optimization, Princeton University Press, 2009. Chapter 11, §§11.1, 11.3-11.4, pp. 281-294; Chapter 3 for the linear case. https://doi.org/10.1515/9781400831050
• A. Ben-Tal, S. Boyd and A. Nemirovski, Extending scope of robust optimization: comprehensive robust counterparts of uncertain problems, Mathematical Programming 107 (2006), 63-89. https://doi.org/10.1007/s10107-005-0679-z
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

Motivation

Estimating a large matrix that is approximately low rank from a few noisy linear measurements is a basic problem of high-dimensional statistics. It covers matrix completion (recovering a ratings table from a small sample of entries), multi-task regression and quantum state tomography. The standard estimator penalizes the nuclear norm, the sum of the singular values, which is the convex surrogate of the rank. Koltchinskii, Lounici and Tsybakov (arXiv:1011.6256v4; Ann. Statist. 39(5), 2011) study a variant of this estimator that uses the known distribution of the design. Their Theorem 1 proves sharp oracle inequalities, with leading constant 1, under a global isometry condition on the design (Assumption 1).

Global isometry is a strong requirement. For sparse vectors, the analogous requirement was relaxed to the restricted eigenvalue condition of Bickel, Ritov and Tsybakov (Ann. Statist. 37, 2009), which only asks for curvature on a cone of approximately sparse directions. The random-design version is due to Koltchinskii (Bernoulli 15, 2009), and a matrix version of the cone appears in Negahban, Ravikumar, Wainwright and Yu (arXiv:1010.2731). Theorem 2 of the paper is the matrix counterpart of the restricted eigenvalue analysis for this estimator. It keeps the leading constant 1, and the price is a stronger tuning condition, λ ≥ 3‖M‖∞ instead of 2‖M‖∞. Section 5.4 of the same paper derives from it a sharp sparsity oracle inequality for the ordinary vector Lasso.

Setting

Observe n pairs (Xᵢ, Yᵢ), i = 1, …, n, where Xᵢ is a random m₁ × m₂ real matrix and Yᵢ a real random variable, satisfying the trace regression model

$$\mathbb E(Y_i \mid X_i) = \operatorname{tr}(X_i^\top A_0),$$

for an unknown matrix A₀. Write ⟨A, B⟩ = tr(AᵀB), and let ‖A‖₁, ‖A‖₂ and ‖A‖∞ be the nuclear, Frobenius and operator norms, the last being the largest singular value. The design enters through the bilinear form

$$\langle A, B\rangle_{L_2(\Pi)} = \frac1n\sum_{i=1}^n \mathbb E\big(\langle A, X_i\rangle\langle B, X_i\rangle\big),$$

with semi-norm ‖A‖_{L₂(Π)}. Two random objects are built from the sample: the noise matrix M = (1/n) Σᵢ (YᵢXᵢ − 𝔼(YᵢXᵢ)), and, for λ > 0 and a set 𝔸 of matrices, the estimator Â^λ, any minimizer over 𝔸 of

$$L_n(A) = \|A\|_{L_2(\Pi)}^2 - \Big\langle \frac2n\sum_{i=1}^n Y_iX_i, A\Big\rangle + \lambda\|A\|_1 .$$

Let A = Σ_{j≤r} σⱼ uⱼvⱼᵀ be a singular value decomposition, with support (S₁, S₂), the spans of the uⱼ and of the vⱼ. Write 𝒫_A⊥(B) = P_{S₁⊥} B P_{S₂⊥} for the part of B orthogonal to both singular spaces, and 𝒫_A(B) = B − 𝒫_A⊥(B). When 𝔸 is a linear subspace and c₀ ≥ 0, the cone ℂ_{A,c₀} consists of the B ∈ 𝔸 with ‖𝒫_A⊥(B)‖₁ ≤ c₀‖𝒫_A(B)‖₁. The restricted constant μ_{c₀}(A) is the infimum of the μ′ > 0 such that ‖𝒫_A(B)‖₂ ≤ μ′‖B‖{L₂(Π)} for every B ∈ ℂ{A,c₀}. The paper uses μ(A) := μ₅(A).

Formalization targets

Goal: Theorem 2, (2.19)

Let 𝔸 be a linear subspace. If λ ≥ 3‖M‖∞, then

$$\|\hat A^\lambda - A_0\|_{L_2(\Pi)}^2 \le \inf_{A \in \mathbb A}\Big[\|A - A_0\|_{L_2(\Pi)}^2 + \lambda^2\mu^2(A)\operatorname{rank}(A)\Big].$$

The bound is deterministic: it holds for every realization of the sample on which λ ≥ 3‖M‖∞. A₀ need not lie in 𝔸, and nothing is assumed about the design beyond what makes the objects finite.

Milestones

The milestones are the displays of the proof, in the order the proof uses them:

1. (2.8), the inequality obtained from the first-order optimality condition of the estimator, which the proof of Theorem 1 already uses;
2. (2.20), in the case ⟨Â^λ − A₀, Â^λ − A⟩_{L₂(Π)} > 0;
3. (2.21), the splitting of ⟨M, Â^λ − A⟩ along 𝒫_A and 𝒫_A⊥;
4. (2.22), the inequality (λ − 2Δ)‖𝒫_A⊥(Â^λ − A)‖₁ ≤ (λ + 2Δ)‖𝒫_A(Â^λ − A)‖₁ with Δ = ‖M‖∞;
5. the membership Â^λ − A ∈ ℂ_{A,5} and the resulting bound by μ(A);
6. the final two-step display with the constant 1 + 2√2/3.

Significance

Theorem 2 gives a sharp oracle inequality whose only design-dependent quantity is a restricted constant. That constant is finite in situations where the global isometry of Theorem 1 fails. The result covers every linear subspace 𝔸, for example all matrices, the diagonal matrices or matrices with a prescribed sparsity pattern. In the diagonal case it becomes a sharp sparsity oracle inequality for the vector Lasso under a restricted eigenvalue condition (the paper's Theorem 14). The oracle inequalities of Bickel, Ritov and Tsybakov under the same condition have a leading constant larger than 1.

The result is proved in the paper, in about half a page that leans on the proof of Theorem 1. No machine-checked version exists. A formalization pins down two things the printed proof leaves to the reader: the convex-analytic optimality condition behind (2.8), and the "obvious modification of (2.10)" and "some algebra" behind (2.20) and the final display. It also reuses and extends the platform's matrix vocabulary: nuclear and operator norms, SVD data, and the tangent and normal projections of the matrix completion missions.

Difficulty

The estimator is defined implicitly as a minimizer, so the analysis has to go through first-order conditions. Those require the subdifferential of the nuclear norm and a choice of subgradient that matches the support of the comparison matrix A. Mathlib has neither a characterization of this subdifferential nor the monotonicity argument in matrix form. The obvious route, copying Theorem 1, fails at the step that uses Assumption 1 to pass from Frobenius to L₂(Π) norms: without a global isometry, that comparison is available only on the cone ℂ_{A,5}, and the error is known to lie there only in the case ⟨Â^λ − A₀, Â^λ − A⟩_{L₂(Π)} > 0 and only for λ ≥ 3‖M‖∞. The constant 5 = (λ + 2Δ)/(λ − 2Δ) at λ = 3Δ is not slack. A linear subspace, not just a convex set, is needed so that Â^λ − A lies in 𝔸, where the cone lives.

Formalization scope

Matrices are RealMatrix m₁ m₂ from the published MatrixCompletion definitions. These supply ⟨·,·⟩ (matrixInner), the nuclear, Frobenius and operator norms, SVD data SVD A r, the sign matrix Σuⱼvⱼᵀ, and 𝒫_A, 𝒫_A⊥ (tangentProjection, normalProjection). This mission adds two definition files.

• Model. ⟨·,·⟩{L₂(Π)}, M, L_n and the estimator, all at a fixed outcome ω. The structure TraceRegression holds the standing assumptions: measurable Xᵢ and Yᵢ, square-integrable entries of Xᵢ, integrable Yᵢ and YᵢXᵢ, and 𝔼(Yᵢ | σ(Xᵢ)) = tr(XᵢᵀA₀) almost surely. The page leaves the integrability implicit. Without it a Bochner integral would silently be 0 and ‖·‖{L₂(Π)} would be meaningless. Expectations of matrices are entrywise. Independence of the pairs (p. 1) is not assumed: Theorem 2 does not use it. The estimator is any minimizer of L_n over 𝔸.
• Cone and restricted constant. ℂ_{A,c₀} ⊆ 𝔸 and the predicate "μ′ is a cone constant". μ(A) can be +∞ (no constant exists), and a real infimum of an empty set is 0. So every statement is made for every cone constant μ′ for (A, 5). This is equivalent to the infimum form and makes the bound vacuous exactly when the paper's is. A formalization with a real sInf would make (2.19) false and is ruled out.

The other conventions are these. "inf over A ∈ 𝔸" is a bound for every A ∈ 𝔸. rank(A) is Matrix.rank. n ≥ 1 and λ > 0 are assumed, as on the page. (2.8) is stated for a convex 𝔸, as in the proof of Theorem 1 where it is derived. (2.21) is stated for an arbitrary matrix in place of Â^λ − A. No printed statement needed correction.

A complete development needs the subdifferential of the nuclear norm ((2.1) of the paper), the first-order condition for constrained convex minimization, the identity (2.9) and the facts (2.10), and trace duality, which is on the platform as matrix_trace_duality_inequality. The subdifferential of the nuclear norm and the projection estimates are reusable well beyond this mission. Contributions of those general lemmas are welcome.

Selected references

• V. Koltchinskii, K. Lounici, A. B. Tsybakov, Nuclear-norm penalization and optimal rates for noisy low-rank matrix completion, arXiv:1011.6256v4, 2016 (Ann. Statist. 39(5), 2302–2329, 2011). https://arxiv.org/abs/1011.6256
• P. J. Bickel, Y. Ritov, A. B. Tsybakov, Simultaneous analysis of Lasso and Dantzig selector, Ann. Statist. 37(4), 1705–1732, 2009. https://doi.org/10.1214/08-AOS620
• V. Koltchinskii, The Dantzig selector and sparsity oracle inequalities, Bernoulli 15(3), 799–828, 2009. https://doi.org/10.3150/09-BEJ187
• S. Negahban, P. Ravikumar, M. J. Wainwright, B. Yu, A unified framework for high-dimensional analysis of M-estimators with decomposable regularizers, arXiv:1010.2731, 2010 (Statist. Sci. 27(4), 2012). https://arxiv.org/abs/1010.2731
• G. A. Watson, Characterization of the subdifferential of some matrix norms, Linear Algebra Appl. 170, 33–45, 1992. https://doi.org/10.1016/0024-3795(92)90407-2

Motivation

Many estimation problems in statistics and machine learning ask for an unknown matrix observed only through noisy linear measurements: matrix completion (recover a large matrix from a few noisy entries, as in collaborative filtering), multi-task regression, and quantum state tomography. A common structural prior is that the unknown matrix has low rank, and the standard convex surrogate for rank is the nuclear norm, the sum of the singular values. Penalizing a least-squares criterion by the nuclear norm gives an estimator that can be computed by convex optimization.

Koltchinskii, Lounici and Tsybakov (arXiv:1011.6256v4; Ann. Statist. 39(5), 2011) study a nuclear-norm penalized estimator in the general trace regression model and prove that it satisfies sharp oracle inequalities: the excess prediction error is bounded by the best approximation error over a class of matrices with leading constant exactly $1$, plus a remainder governed by either the nuclear norm ("slow rate") or the rank ("fast rate") of the approximating matrix. A distinctive feature of their estimator is that it uses the known design distribution $\Pi$, which the empirical-risk estimators of the earlier literature (Candès and Plan 2010; Rohde and Tsybakov 2011; Negahban and Wainwright 2011) do not exploit; for noisy matrix completion the previously available bounds were suboptimal. Their Theorem 1 is the deterministic core from which the paper's matrix completion rates (Theorem 4) follow by bounding one random matrix in operator norm.

Setting

Let $(X_i,Y_i)$, $i=1,\dots,n$, be random pairs, $X_i$ a real $m_1\times m_2$ matrix and $Y_i$ a real number, satisfying the trace regression model

$$\mathbb E(Y_i\mid X_i)=\langle A_0,X_i\rangle,\qquad \langle A,B\rangle=\operatorname{tr}(A^\top B),$$

for an unknown matrix $A_0$. Let $\Pi_i$ be the law of $X_i$ and $\Pi=\frac1n\sum_i\Pi_i$. The $L_2(\Pi)$ inner product and semi-norm are

$$\langle A,B\rangle_{L_2(\Pi)}=\frac1n\sum_{i=1}^n\mathbb E\big(\langle A,X_i\rangle\langle B,X_i\rangle\big),\qquad \|A\|^2_{L_2(\Pi)}=\langle A,A\rangle_{L_2(\Pi)}.$$

For a matrix $A$ with singular values $\sigma_j(A)$, $\|A\|_1=\sum_j\sigma_j(A)$ is the nuclear norm, $\|A\|_2$ the Frobenius norm, and $\|A\|_\infty=\sigma_1(A)$ the operator norm. If $A=\sum_{j=1}^r\sigma_ju_jv_j^\top$ is a singular value decomposition, the pair $(S_1,S_2)=(\operatorname{span}\{u_j\},\operatorname{span}\{v_j\})$ is the support of $A$, and $P_S$ is the orthogonal projector onto $S$.

Given a set $\mathbb A$ of matrices and $\lambda>0$, the estimator is

$$\hat A^\lambda\in\operatorname*{argmin}_{A\in\mathbb A}L_n(A),\qquad L_n(A)=\|A\|^2_{L_2(\Pi)}-\Big\langle\frac2n\sum_{i=1}^nY_iX_i,A\Big\rangle+\lambda\|A\|_1 .$$

The random matrix

$$\mathbf M=\frac1n\sum_{i=1}^n\big(Y_iX_i-\mathbb E(Y_iX_i)\big)$$

carries all the noise. Assumption 1 asks for a constant $\mu>0$ with $\|A\|^2_{L_2(\Pi)}\ge\mu^{-2}\|A\|_2^2$ for all $A\in\mathbb A-\mathbb A$.

Formalization targets

Goal: Theorem 1

If $\lambda\ge2\|\mathbf M\|_\infty$, then for any set $\mathbb A$

$$\|\hat A^\lambda-A_0\|^2_{L_2(\Pi)}\le\inf_{A\in\mathbb A}\Big[\|A-A_0\|^2_{L_2(\Pi)}+2\lambda\|A\|_1\Big],\tag{2.3}$$

and if moreover $\mathbb A$ is convex and Assumption 1 holds,

$$\|\hat A^\lambda-A_0\|^2_{L_2(\Pi)}\le\inf_{A\in\mathbb A}\Big[\|A-A_0\|^2_{L_2(\Pi)}+\Big(\tfrac{1+\sqrt2}{2}\Big)^2\mu^2\lambda^2\operatorname{rank}(A)\Big],\tag{2.4}$$

and, for every $A\in\mathbb A$ with support $(S_1,S_2)$,

$$\|\hat A^\lambda-A_0\|^2_{L_2(\Pi)}+(\lambda-2\|\mathbf M\|_\infty)\|P_{S_1^\perp}\hat A^\lambda P_{S_2^\perp}\|_1\le\|A-A_0\|^2_{L_2(\Pi)}+\Big(\tfrac{1+\sqrt2}{2}\Big)^2\mu^2\lambda^2\operatorname{rank}(A).\tag{2.5}$$

The theorem is deterministic: it holds at every realization of the sample at which $\lambda\ge2\|\mathbf M\|_\infty$.

Milestones

The milestones follow the paper's proof: the subdifferential of the nuclear norm (2.1); the basic inequality of p. 7 and the slow-rate bound (2.3); the first-order condition (2.6); the identity (2.9) and the facts (2.10); the inequality (2.11); the decomposition bound (2.12)–(2.14); the bound on $\Lambda$ via (2.15); and the combined inequality (2.17). The rank bound (2.16) is included as a supporting statement (not a milestone).

Significance

Theorem 1 separates the statistical problem into a deterministic oracle inequality and a single probabilistic estimate, $\|\mathbf M\|_\infty\le\lambda/2$. Any concentration bound for $\|\mathbf M\|_\infty$ (matrix Bernstein for uniform sampling, Gaussian bounds for fixed designs) then gives a rate. The paper uses it to obtain matrix completion rates which its minimax lower bounds show to be optimal up to logarithmic factors on the class of matrices of rank at most $r$ with entries bounded by $a$. The leading constant $1$ means the bounds remain informative when $A_0$ is not low rank but only well approximated by low-rank matrices.

The result has been proved on paper since 2011; to our knowledge no machine-checked proof exists. A formal proof requires the subdifferential of the nuclear norm and its interplay with the singular-subspace projections, which are reusable for every nuclear-norm method (singular value thresholding, robust PCA, multi-task learning).

Difficulty

The slow-rate bound (2.3) is a short computation from the definition of a minimizer and trace duality. The fast-rate bounds (2.4)–(2.5) are not: a minimizer comparison alone gives only $\lambda\|\hat A^\lambda-A\|_1$ as remainder, which does not scale with $\operatorname{rank}(A)$. One needs the variational inequality (2.6) over the convex set $\mathbb A$, the exact description (2.1) of the nuclear-norm subdifferential at an arbitrary comparison matrix $A$, and a decomposition of $\langle\mathbf M,\hat A^\lambda-A\rangle$ along the support of $A$ in which the component orthogonal to the support is controlled in operator norm and the rest in Frobenius norm. Formally, (2.1) itself requires identifying the abstract singular values with a given decomposition and characterizing the operator-norm ball as the dual of the nuclear norm.

Formalization scope

Matrices are RealMatrix m₁ m₂ = Matrix (Fin m₁) (Fin m₂) ℝ, with the published MatrixCompletion definitions supplying the Frobenius inner product matrixInner, nuclearNorm (sum of Mathlib's singular values), spectralNorm (operator norm), frobeniusNorm, SVD data SVD A r and the projections twoSidedSingularProjection ($P_{S_1}\cdot P_{S_2}$), tangentProjection ($\mathcal P_A$) and normalProjection ($P_{S_1^\perp}\cdot P_{S_2^\perp}$). The sample lives on a probability space (Ω, P) with 0 < n; expectations of matrices are entrywise. Conventions committed to:

1. Realization-wise statements. $\omega$ is fixed; $\hat A$ is any matrix with $\hat A\in\mathbb A$ and $L_n(\hat A)\le L_n(A)$ for all $A\in\mathbb A$. Existence of a minimizer is not asserted.
2. Infima are stated as the bound for every $A\in\mathbb A$ (equivalent; no real sInf is used).
3. The model (1.1) is the conditional expectation of $Y_i$ given the $\sigma$-algebra generated by the entries of $X_i$.
4. Added regularity, not printed in the paper: every entry of $X_i$ is measurable and square integrable, $Y_i$ is measurable and integrable, and $Y_i(X_i)_{jk}$ is integrable. Without these, Lean's Bochner integral returns $0$ and $\|\cdot\|_{L_2(\Pi)}$ and $\mathbf M$ would be meaningless.
5. Independence of the pairs is not assumed; the proof does not use it.
6. Supports are given by SVD data; bounds use A.rank.
7. Corrected statement. The first fact of (2.10), $\|\sum_ju_jv_j^\top\|_\infty=1$, is false for $A=0$ (empty sum); the milestone assumes $r>0$.
8. Steps the paper states for $\hat A^\lambda$ or $\mathbf M$ but which hold for arbitrary matrices ((2.9), (2.10), (2.12)–(2.16)) are stated for arbitrary matrices.

Ruling out trivializations: the goal states (2.3)–(2.5) with the paper's constants and remainder terms, not the intermediate bound (2.17), and $\hat A$ is pinned down as a minimizer over $\mathbb A$, not an arbitrary matrix.

Welcome contributions: proofs of the nuclear-norm subdifferential (2.1) and of the projection facts, which are reusable well beyond this mission, and the measure-theoretic identity $\frac1n\sum_i\mathbb E(Y_iX_i)=\frac1n\sum_i\mathbb E(\langle A_0,X_i\rangle X_i)$ from the model.

Selected references

• V. Koltchinskii, K. Lounici, A. B. Tsybakov, Nuclear-norm penalization and optimal rates for noisy low-rank matrix completion, arXiv:1011.6256v4, 2016 (the source of this mission); Ann. Statist. 39(5), 2302–2329, 2011. https://arxiv.org/abs/1011.6256, https://doi.org/10.1214/11-AOS894
• G. A. Watson, Characterization of the subdifferential of some matrix norms, Linear Algebra Appl. 170, 33–45, 1992 (reference [28] of the source; the description (2.1) of the nuclear-norm subdifferential). https://doi.org/10.1016/0024-3795(92)90407-2
• E. J. Candès, Y. Plan, Matrix completion with noise, Proc. IEEE 98(6), 925–936, 2010. https://doi.org/10.1109/JPROC.2009.2035722
• A. Rohde, A. B. Tsybakov, Estimation of high-dimensional low-rank matrices, Ann. Statist. 39(2), 887–930, 2011. https://doi.org/10.1214/10-AOS860
• S. Negahban, M. J. Wainwright, Estimation of (near) low-rank matrices with noise and high-dimensional scaling, Ann. Statist. 39(2), 1069–1097, 2011. https://doi.org/10.1214/10-AOS850

Motivation

The support vector machine (SVM) is a linear classifier trained by minimising a regularised hinge loss. For training sets with millions of examples, solving the SVM problem to high accuracy by interior-point or dual decomposition methods is too slow, and what is needed is an algorithm whose cost per iteration does not grow with the number of examples. Pegasos (Primal Estimated sub-GrAdient SOlver for SVM), introduced by Shalev-Shwartz, Singer and Srebro in 2007 and analysed in its final form by Shalev-Shwartz, Singer, Srebro and Cotter in Mathematical Programming (2011, doi:10.1007/s10107-010-0420-4), is a stochastic sub-gradient method on the primal SVM objective with step size $1/(\lambda t)$. Its analysis showed that the number of iterations needed for accuracy $\epsilon$ is $\tilde O(1/(\lambda\epsilon))$, independent of the training-set size, and the method became a standard baseline for large-scale linear SVM training.

The analysis rests on a logarithmic-regret bound for online gradient descent on strongly convex functions, due to Hazan, Agarwal and Kale (Machine Learning 69, 2007), which the paper re-proves for non-smooth functions as its Lemma 1 and then applies to the Pegasos iterates in its Theorem 1.

Setting

A training set consists of $m$ examples $(x_i, y_i)$, $i\in[m]$, with $x_i\in\mathbb R^n$ and labels $y_i\in\{+1,-1\}$. The hinge loss of a weight vector $w$ on $(x,y)$ is $\ell(w;(x,y)) = \max\{0,\,1 - y\langle w, x\rangle\}$. For a regularisation parameter $\lambda>0$, the SVM objective (Eq. (1)) is

$$f(w) = \frac\lambda2\|w\|^2 + \frac1m\sum_{i=1}^m \ell(w;(x_i,y_i)),$$

and $w^\star$ denotes a minimiser of $f$ (Eq. (9)). For a mini-batch $A$ of $k\ge1$ example indices, the instantaneous objective (Eq. (7)) is

$$f(w;A) = \frac\lambda2\|w\|^2 + \frac1k\sum_{i\in A}\ell(w;(x_i,y_i)).$$

Mini-batch Pegasos (Fig. 2 of the paper) starts at $w_1 = 0$. At each round $t = 1, 2, \dots$ it receives a mini-batch $A_t$, forms the sub-gradient

$$\nabla_t = \lambda w_t - \frac1k\sum_{i\in A_t}\mathbb 1\bigl[y_i\langle w_t, x_i\rangle < 1\bigr]\,y_i x_i \qquad (8)$$

of $f(\cdot;A_t)$ at $w_t$, and sets $w_{t+1} = w_t - \eta_t\nabla_t$ with $\eta_t = 1/(\lambda t)$. Optionally it then applies the projection step (6), $w_{t+1}\leftarrow\min\{1,(1/\sqrt\lambda)/\|w_{t+1}\|\}\,w_{t+1}$, which maps $w_{t+1}$ to the closest point of the Euclidean ball of radius $1/\sqrt\lambda$. A function $g$ is $\lambda$-strongly convex if $g(w) - \frac\lambda2\|w\|^2$ is convex, and $v$ is a sub-gradient of a convex $g$ at $w_0$ if $g(w) - g(w_0)\ge\langle v, w - w_0\rangle$ for every $w$.

In the Lean development these objects are svmObj, instObj, subgrad, projBall and run in the namespace Pegasos.Analysis; the hinge loss is UnderstandingML.hingeLoss, sub-gradients are UnderstandingML.IsSubgradient, and "$z$ is the projection of $v$ onto $B$" is LogRegretOCO.OGD.IsProj B v z.

Formalization targets

Goal: Theorem 1

Assume $\|x_i\|\le R$ for every $i$, and set $c = (\sqrt\lambda + R)^2$ when the projection step is performed and $c = 4R^2$ when it is not. Then for every sequence of mini-batches and every $T\ge3$,

$$\frac1T\sum_{t=1}^T f(w_t;A_t) \;\le\; \frac1T\sum_{t=1}^T f(w^\star;A_t) + \frac{c\,(1+\ln T)}{2\lambda T}.$$

The constants are the paper's and are stated exactly; a version with a single constant for both variants, or with an unspecified constant, is a weaker theorem.

Milestones

1. Eq. (10): for $\lambda$-strongly convex $g$ with sub-gradient $v$ at $w$, $\langle w - u, v\rangle\ge g(w) - g(u) + \frac\lambda2\|w-u\|^2$.
2. Eq. (11): one projected step satisfies $\langle w_t - u,\nabla_t\rangle\le\frac{\|w_t-u\|^2 - \|w_{t+1}-u\|^2}{2\eta_t} + \frac{\eta_t}2G^2$ (an already-proved platform theorem, stated with a factor 2).
3. Lemma 1: projected sub-gradient steps $\eta_t = 1/(\lambda t)$ on $\lambda$-strongly convex $f_t$ with $\|\nabla_t\|\le G$ satisfy $\frac1T\sum f_t(w_t)\le\frac1T\sum f_t(u) + \frac{G^2(1+\ln T)}{2\lambda T}$ for all $u\in B$.
4. The vector (8) is a sub-gradient of $f(\cdot;A)$; $f(\cdot;A)$ is $\lambda$-strongly convex; the projection step (6) is the projection onto the ball of radius $1/\sqrt\lambda$.
5. The gradient bounds: $\|\nabla_t\|\le\sqrt\lambda + R$ with projection; Eq. (13), $w_{t+1} = \frac1{\lambda t}\sum_{i\le t}v_i$, and $\|\nabla_t\|\le 2R$ without.
6. $\|w^\star\|\le 1/\sqrt\lambda$.

Significance

Theorem 1 is the deterministic core of every guarantee in the paper. Taking expectations over uniformly random mini-batches turns its left side into the expected objective of the iterates and its right side into $f(w^\star)$ plus the rate, which yields the $\tilde O(1/(\lambda\epsilon))$ iteration bound and, via Markov-type arguments, the high-probability bounds of the later sections. Because the bound holds for every sequence of mini-batches, it is also an online-learning regret bound for the sequence of instantaneous objectives.

The result is proved in the paper and is classical. To our knowledge it has no machine-checked proof. Formalizing it produces a verified logarithmic-regret lemma for non-smooth strongly convex sub-gradient descent with an arbitrary closed convex feasible set (the platform currently has the twice-differentiable version with a bounded feasible set), a verified sub-gradient calculus for the regularised hinge loss, and an exact treatment of the Pegasos iteration including both the projected and unprojected variants.

Difficulty

The obvious argument applies Lemma 1 with $B$ the ball of radius $1/\sqrt\lambda$ in both variants and $G$ the sup of $\|\nabla_t\|$ over that ball. This fails twice. Without the projection step the iterates are not confined to that ball, so a separate argument (the closed form (13)) is needed to bound them, and it gives the different constant $4R^2$. With projection, Lemma 1 requires the comparator $w^\star$ to lie in the ball, and $\|w^\star\|\le1/\sqrt\lambda$ is not implied by the elementary comparison $f(w^\star)\le f(0)\le1$, which only gives $\|w^\star\|\le\sqrt{2/\lambda}$; the paper obtains the sharp radius through duality. In Lemma 1 itself, the telescoping only closes because the step size $1/(\lambda t)$ is matched exactly to the strong-convexity modulus; any off-by-one in the step indexing breaks the cancellation.

Formalization scope

Vectors are EuclideanSpace ℝ (Fin n), examples are indexed by Fin m, labels are real numbers with the hypothesis $y_i\in\{+1,-1\}$, and $\lambda>0$, $k\ge1$ are hypotheses. A mini-batch is a $k$-tuple Fin k → Fin m: an injective tuple is a subset of size $k$ as in Fig. 2, a non-injective one is the multi-set with repetitions the paper also allows. The theorem is stated for every sequence of mini-batches A : ℕ → Fin k → Fin m; no probability space appears, because the proof never uses that the batches are random. Iterations are 1-based: run … 1 = 0, the step producing $w_{t+1}$ uses $\eta_t = 1/(\lambda t)$ and the batch $A_t$ only, and index 0 is unused. The variant is selected by a Boolean flag, and $c$ depends on it. $w^\star$ is any $w$ with $f(w^\star)\le f(w)$ for all $w$, minimising the full objective (1), not the instantaneous ones. Strong convexity is the paper's own definition, convexity of $g - \frac\lambda2\|\cdot\|^2$. At $w = 0$ the projection formula is evaluated with Lean's $a/0 = 0$, which gives the intended value $0$. The paper's display (12) has two printed slips (the sign of the $v_t$ term and $x_t$ for $x_i$); the Lean states the correct update, and Eq. (13) is correct as printed.

A trivializing formalization is ruled out: the goal is stated for the concrete iteration run, not for an abstract sequence assumed to be sub-gradient steps or projections, and those facts are separate milestones.

A complete development needs the sub-differential sum rule for a convex function plus a quadratic, convexity of the hinge loss, the variational characterisation of the projection onto a ball, the harmonic-sum bound $\sum_{t\le T}1/t\le1+\ln T$, and a proof of $\|w^\star\|\le1/\sqrt\lambda$ (through duality or a direct optimality argument). Lemma 1 and the sub-gradient lemmas are reusable for any strongly convex stochastic sub-gradient method. Proofs of any milestone, and alternative proofs of the bound on $\|w^\star\|$ that avoid the dual problem, are welcome.

Selected references

• S. Shalev-Shwartz, Y. Singer, N. Srebro, A. Cotter, Pegasos: primal estimated sub-gradient solver for SVM, Mathematical Programming Ser. B 127 (2011) 3–30. https://doi.org/10.1007/s10107-010-0420-4
• E. Hazan, A. Agarwal, S. Kale, Logarithmic regret algorithms for online convex optimization, Machine Learning 69 (2007) 169–192. https://doi.org/10.1007/s10994-007-5016-8
• S. Shalev-Shwartz, Y. Singer, N. Srebro, Pegasos: primal estimated sub-gradient solver for SVM, ICML 2007. https://doi.org/10.1145/1273496.1273598

Motivation

Periodic-review inventory systems with lost sales and a positive replenishment lead time are a basic model of retail and spare-parts operations: demand that cannot be met from stock is lost, and an order placed today arrives $\tau$ periods later. Even with a known demand distribution the optimal policy depends on the whole vector of outstanding orders and is intractable for long lead times, so practice and theory fall back on base-stock (order-up-to) policies, which are asymptotically optimal as the lost-sales penalty grows relative to the holding cost (Huh, Janakiraman, Muckstadt and Rusmevichientong, Management Science 2009).

Computing the best base-stock level still requires the demand distribution. In many settings the distribution is unknown and, worse, demand is censored: the manager records sales, $\min\{D_t, I_t\}$, and never sees the demand lost to a stockout. The paper behind this mission, Huh, Janakiraman, Muckstadt and Rusmevichientong, An Adaptive Algorithm for Finding the Optimal Base-Stock Policy in Lost Sales Inventory Systems with Censored Demand (working paper of February 8, 2007; published in Mathematics of Operations Research 2009, DOI 10.1287/moor.1080.0367), gives an algorithm that learns the optimal base-stock level from sales data alone and bounds its regret against the best base-stock policy. It extended the zero-lead-time adaptive newsvendor analyses (e.g. Huh and Rusmevichientong, Math. Oper. Res. 2009) to positive lead times, where the inventory process is a Markov chain on $\mathbb R^\tau$.

Setting

Demands $D_1, D_2, \dots$ are i.i.d. copies of a nonnegative, continuous random variable $D$ with $E[D] > 0$ and distribution function $F$. The inventory vector in period $t$ is

$$X_t = (Q_{t-1}, \dots, Q_{t-\tau+1}, I_t) \in \mathbb R^\tau_+,$$

the $\tau - 1$ outstanding orders and the on-hand inventory $I_t$; its inventory position is $X_t \cdot \mathbf 1^\tau$. Under the order-up-to-$S$ policy the manager orders $Q_t = [S - X_t\cdot\mathbf 1^\tau]^+$, demand $D_t$ is realized, and

$$I_{t+1} = [I_t - D_t]^+ + Q_{t-\tau+1}.$$

A period with on-hand inventory $y$ costs, in expectation, $C(y) = h\,E[y - D]^+ + b\,E[D - y]^+$, with holding cost $h$ and lost-sales penalty $b$. The long-run average cost of level $S$ is

$$C(I_\infty(S)) = \lim_{T\to\infty} \frac1T \sum_{t=1}^T E[C(I_t(S))],$$

and $S^*$ denotes a level minimizing it over $S \ge 0$. Write $\gamma(S) = \mathcal P[D \le S/(\tau+1)]$.

The algorithm $\textsc{Adaptive}(\alpha,\beta)$ runs in cycles $k = 1, 2, \dots$ of length $T_k = \lceil k^\beta\rceil$; $N(L) = \sum_{k\le L} T_k$. Cycle $k$ uses a fixed level $S_k$. From sales data it computes a sample-path derivative $I'$ by a recursion over the last $\tau$ periods, forms a gradient estimate $H_k \in \{h, -b, 0\}$ from the last period of the cycle, and sets $S_{k+1} = P_{[\underline M, \overline M]}(S_k - \epsilon_k H_k)$ with $\epsilon_k = (\overline M - \underline M)/(\max\{b,h\}k^\alpha)$. The inventory is carried over between cycles. The regret after $L$ cycles is

$$\Lambda(L) = E\Big[\sum_{k=1}^L\sum_{j=1}^{T_k} C(I_{(k,j)})\Big] - C(I_\infty(S^*))\,N(L).$$

Formalization targets

Goal: Theorem 10, corrected

Under Assumption 1 ($0 \le \underline M \le S^* \le \overline M$ and $\gamma(\underline M) > 0$) and infinite support of $D$, for $\alpha,\beta \in (0,1)$ and $L \ge 1$, with $N = N(L)$ and $\nu = \max\{1 - \gamma(\underline M)^{2\tau}, F(\overline M), 1/e\}$,

$$\frac{\Lambda(L)}{N} \le (b+h)\Big[(\overline M - \underline M)\Big(\frac{4}{N^{\frac{1-\alpha}{1+\beta}}} + \frac{4/(1-\alpha)}{N^{\frac{\alpha}{1+\beta}}} + \frac{C_3}{N^{\frac1{1+\beta}}}\Big) + \overline M\,\frac{24\tau/\ln(1/\nu)}{N^{\frac{\beta}{1+\beta}}}\Big],$$

with $C_3 = 12(4\tau)^{1/\beta}\Gamma(1/\beta)(1/\beta)/(\ln(1/\nu))^{1/\beta}$. At $\alpha = \beta = 1/2$ this is $O(N^{-1/3})$.

Milestones

Lemma 5 (tail of $D_1 + \dots + D_t$), Lemma 6 (the inventory position falls to $S$), Theorem 7 (existence, independence of the start, convexity and differentiability of $C(I_\infty(S))$, and existence of $S^*$ with $\gamma(S^*) > 0$), Theorem 11 (projected stochastic gradient descent with biased gradients), Lemmas 12 and 13 (sums over cycles of length $\lceil k^\beta\rceil$), Lemma 14 (the regret $\Lambda_1$ from $S_k \ne S^*$) and Lemma 15 (the transient regret $\Lambda_2$).

Significance

The theorem gives a nonparametric, sales-only policy whose average cost approaches that of the best base-stock policy at an explicit polynomial rate, uniformly over demand distributions satisfying Assumption 1. Its ingredients are reusable: an explicit geometric ergodicity rate for the lost-sales base-stock chain, convexity of the long-run base-stock cost in $S$, and a regret bound for projected gradient descent whose gradients are biased by Markov dependence.

The result is published; to our knowledge none of it has been machine-checked. The mission formalizes the regret bound, which requires Markov-chain ergodicity on a continuous state space, long-run averages, and stochastic approximation with biased gradients. It also repairs the printed constants: Theorem 10 and Lemma 15 are false as printed (see Formalization scope), and the formal statements make the dependence on $\overline M$ explicit.

Difficulty

The obvious route treats the cycle's last-period derivative as an unbiased gradient of $C(I_\infty(S_k))$ and applies standard online convex optimization. That fails: the estimate is computed from a Markov chain started at whatever state the previous cycle left, so it is biased, and the bias decays only as the chain mixes. Controlling the bias requires an explicit mixing rate for a chain on $\mathbb R^\tau_+ \times \{0,1\}^\tau$ whose state includes the derivative process, uniformly over the levels in $[\underline M, \overline M]$ and over starting positions above $S$. The ergodicity argument uses a coalescing demand pattern, which exists only when $\gamma(S) > 0$; without that condition the chain need not be ergodic. A second obstacle is that the objective $C(I_\infty(S))$ is defined as a long-run average, so its convexity and differentiability in $S$ must be established before any gradient argument applies.

Formalization scope

Everything is stated in Lean 4 with Mathlib. The inventory vector is a pair (pipeline Fin (τ-1) → ℝ, newest order first; on-hand ℝ). Lean periods are $0$-based (Lean period $t$ is the paper's $t+1$); cycles are numbered from $1$. Demand is a sequence on a probability space that is i.i.d., nonnegative, integrable, with $E[D] > 0$ and an atomless law; infinite support is $F(x) < 1$ for all $x$; $\tau \ge 1$, $h, b > 0$. The long-run cost is a limsup of Cesàro averages from the empty start (Theorem 7 shows it is a limit from every start), and $S^*$ is any minimizer over $[0,\infty)$. The algorithm is a deterministic function of the demand path; the sample derivative is the recursion the algorithm computes, not a derivative. Integrability of every expectation follows from boundedness of the inventory and is not assumed.

Corrections, all disclosed in the items: Theorem 10 carries $\overline M$ instead of $\overline M - \underline M$ on the $C_4$ term, because the printed bound fails for $\underline M = \overline M = S^*$, $X_{(1,1)} = 0$, $L = 1$, where the right side is $0$ and $\Lambda(1) = C(0) - C(I_\infty(S^*)) > 0$. Lemma 15 carries $\overline M$ and $12\tau + 1$. Lemma 14 keeps its printed constant; its proof appears to use the ergodicity theorem one period early. Theorem 11 is stated on an interval with the bias taken conditionally on the history. Lemmas 5 and 6 are stated for infinite support only.

A goal that bounds the regret by $\Lambda_1$ alone (costs at the steady state of $S_k$), or that lets the levels be any sequence in $[\underline M, \overline M]$, is not the theorem: the regret here uses the realized inventory of the algorithm. Lean's conventions $x/0 = 0$ and $\ln$ of a nonpositive number cannot trivialize the bound, because infinite support and $\gamma(\underline M) > 0$ give $\nu \in [1/e, 1)$. The source is the authors' working paper of February 8, 2007, whose printed page numbers equal the PDF's.

Not yet stated: Theorem 3 and Lemma 4 (ergodicity rate), Theorem 8 and Lemma 9 (bias bounds), Theorem 1 (sample derivatives). They need the joint chain $(X_t, X'_t)$ and are welcome as contributions, as are the general pieces: geometric ergodicity via coalescence, and the biased projected-gradient bound.

Selected references

• W. T. Huh, G. Janakiraman, J. A. Muckstadt, P. Rusmevichientong, An Adaptive Algorithm for Finding the Optimal Base-Stock Policy in Lost Sales Inventory Systems with Censored Demand, working paper, 2007; Mathematics of Operations Research 2009. https://doi.org/10.1287/moor.1080.0367
• W. T. Huh, G. Janakiraman, J. A. Muckstadt, P. Rusmevichientong, Asymptotic Optimality of Order-up-to Policies in Lost Sales Inventory Systems, Management Science 55(3), 2009. https://doi.org/10.1287/mnsc.1080.0945
• W. T. Huh, P. Rusmevichientong, A Nonparametric Asymptotic Analysis of Inventory Planning with Censored Demand, Mathematics of Operations Research 2009. https://doi.org/10.1287/moor.1080.0355
• G. Janakiraman, R. O. Roundy, Lost-Sales Problems with Stochastic Lead Times: Convexity Results for Base-Stock Policies, Operations Research 2004. https://doi.org/10.1287/opre.1040.0130

Minimum discrimination information under moment constraints

Given a reference probability distribution $R$ and a set $\mathcal E$ of probability distributions, the minimum discrimination information problem asks for the member of $\mathcal E$ closest to $R$ in Kullback–Leibler divergence. It is the basis of Kullback's information-theoretic approach to statistics (Kullback 1959), of the maximum-entropy principle of statistical physics (Jaynes 1957), and of large-deviation theory, where Sanov's theorem identifies the rate function of an empirical distribution with exactly this minimum. The most common constraint sets are defined by prescribed expectations $\int f_i\,dP = a_i$, and the classical answer is that the minimizer is an exponential family member, with density $c\exp\sum_i t_i f_i$ with respect to $R$.

That answer was usually justified by Lagrange multipliers, which presuppose that a minimizer exists. Csiszár's paper (Ann. Probab. 1975) treats the problem geometrically, with I-divergence in the role of squared Euclidean distance, and its last result, Theorem 3.3, proves existence and the exponential form at once for unbounded constraint functions, under a hypothesis on the exponential moments of the $f_i$.

Timeline:

• 1959: Kullback formulates the minimum discrimination information theorem: an element of $\mathcal E$ of exponential form is the minimizer (a sufficient condition).
• 1966: Kullback and Khairat (Ann. Math. Statist. 37, 1966) refine the sufficient condition.
• 1972: Čencov proves existence of exponential-form minimizers under general conditions (Statistical Decision Rules and Optimal Inference, Theorem 23.1).
• 1975: Csiszár proves Theorem 3.3 by the minimizing-sequence method of his Theorem 2.1; a first version of the paper assumed $T_R = E^k$, weakened to "$T_R$ open" after Čencov's work.

Setting

All distributions (PD's) live on one measurable space $(X,\mathcal X)$. The I-divergence of $P$ from $Q$ is

$$I(P\|Q)=\int \log p_Q\,dP\ \text{ if } P\ll Q,\qquad I(P\|Q)=+\infty\ \text{ otherwise},$$

where $p_Q$ is the density of $P$ with respect to $Q$; it takes values in $[0,\infty]$ and vanishes only for $P=Q$. The variation distance is $|P-Q|=\int|p_R-q_R|\,dR$ for any PD $R$ dominating both. If $\mathcal E$ is a convex set of PD's containing some $P$ with $I(P\|R)<\infty$, a $Q\in\mathcal E$ with

$$I(Q\|R)=\min_{P\in\mathcal E} I(P\|R)$$

is the I-projection of $R$ on $\mathcal E$.

Fix real-valued measurable functions $f_1,\dots,f_k$ on $X$. For $a=(a_1,\dots,a_k)\in E^k$ (Euclidean $k$-space) the moment set $\mathcal E(a)$ is the set of PD's $P$ with $\int f_i\,dP=a_i$, $i=1,\dots,k$. Further:

• $A_R$ is the set of $a\in E^k$ for which $\mathcal E(a)$ contains some $P$ with $I(P\|R)<\infty$;
• $T_R=\{t\in E^k:\ \exp\sum_i t_i f_i \text{ is } R\text{-integrable}\}$, (3.16);
• $F(a)=\inf_{P\in\mathcal E(a)} I(P\|R)$, (3.18), the optimal value as a function of the constraint levels.

Formalization targets

Goal: Theorem 3.3

If $T_R$ is open in $E^k$, then for every point $a$ of the interior of $A_R$ the I-projection $Q$ of $R$ on $\mathcal E(a)$ exists and

$$q_R(x)=c\exp\sum_{i=1}^k t_i f_i(x)\qquad R\text{-a.e.},$$

for some constant $c$ and some $t\in E^k$.

Milestones

1. (2.2), the parallelogram identity: $I(P_m\|R)+I(P_n\|R)=2I(\tfrac{P_m+P_n}2\|R)+I(P_m\|\tfrac{P_m+P_n}2)+I(P_n\|\tfrac{P_m+P_n}2)$.
2. (2.4): a minimizing sequence $P_n$ in a convex set converges in variation to a PD $Q\ll R$ (closedness of the set is not used).
3. Lemma 3.1: if $e^{tf}$ is $Q$-integrable for small $|t|$, then $I(P_n\|Q)\to0$ implies $\int f\,dP_n\to\int f\,dQ$.
4. (3.18): $A_R$ is convex and $F$ is finite and convex on $A_R$.
5. (3.19): at an interior point $a$ of $A_R$ there is $t$ with $F(b)\ge F(a)+\sum_i t_i(b_i-a_i)$ for all $b\in A_R$.
6. Remark, p. 158: $F$ is differentiable at interior points of $A_R$, and $\operatorname{grad}F(a)=t$, the parameter vector of the I-projection.

Significance

Theorem 3.3 gives existence of maximum-entropy (minimum discrimination information) distributions under finitely many moment constraints with unbounded constraint functions, which covers the usual exponential families of statistics (normal, gamma, Poisson moment constraints) where boundedness fails. It identifies the minimizer's form without assuming a minimizer exists, and the Remark identifies the natural parameters as the gradient of the optimal value, the sensitivity interpretation of Lagrange multipliers. These facts underlie the duality between moment and natural parameters of exponential families and the rate functions of Cramér and Sanov type.

The result is proved, in this paper and (under a slightly weaker hypothesis) by Čencov. None of it is formalized: Mathlib has the Kullback–Leibler divergence of measures (InformationTheory.klDiv) and tilted measures, but no I-projection, no existence theorem for constrained minimizers of KL divergence and no exponential-form characterization. The mission produces a machine-checked version of the existence and form theorem, together with the general steps it uses (the parallelogram identity, convergence of minimizing sequences in variation, continuity of exponential-moment expectations under KL convergence).

Difficulty

The obvious argument fails at the first step: the moment set $\mathcal E(a)$ is convex but not closed in variation when the $f_i$ are unbounded, since $\int f_i\,dP$ is not continuous in variation. A minimizing sequence therefore converges in variation to some $Q$ (as in Theorem 2.1), but nothing places $Q$ in $\mathcal E(a)$: mass can escape to where $|f_i|$ is large. Ruling this out needs quantitative control of $I(P_n\|Q)$, which in turn requires knowing the form of $Q$ before knowing $Q$ is feasible; the interplay with the convexity of $F$ and the openness of $T_R$ is where the work lies. A Lagrange-multiplier argument is not available: it presupposes a minimizer and differentiability that are part of the conclusion.

Formalization scope

• Probability distributions are Measure X with IsProbabilityMeasure; the I-divergence is Mathlib's klDiv : ℝ≥0∞, which for probability measures equals (1.1) with the conventions $\log 0=-\infty$, $\log\frac a0=+\infty$, $0\cdot(\pm\infty)=0$.
• The variation distance uses $P+Q$ as dominating measure (the page allows any dominating PD; the value is the same).
• The I-projection carries $I(Q\|R)<\infty$ explicitly: the page defines it only when $\mathcal E$ meets $\{P: I(P\|R)<\infty\}$.
• $\mathcal E(a)$ requires $P$-integrability of every $f_i$, so the constraint integrals are genuine. $E^k$ is Fin k → ℝ with its product (Euclidean) topology; "inner point" is the topological interior. $k=0$ is allowed.
• $F$ is an infimum in $[0,\infty]$ (equal to $\infty$ outside $A_R$); statements use its real value only on $A_R$, where it is finite. (3.18) prints $I(P\|Q)$; the reference measure is $R$, as the definition of $A_R$ and the proof show. (3.16) prints $(t_1,\dots,t_n)$ for $(t_1,\dots,t_k)$.
• Densities are Radon–Nikodym derivatives and the form (3.2) is an $R$-almost-everywhere identity with no exceptional set of positive measure.
• Lemma 3.1 asserts that $f$ is $P_n$-integrable for large $n$ as well as the convergence, so that $\int f\,dP_n$ is not a default value.
• Trivializing readings are excluded: the goal asserts existence of the I-projection rather than assuming it, $T_R$ is an integrability set (not a set where a junk integral is finite), and the infimum is never a real sInf over a possibly empty set.

A complete development needs: Radon–Nikodym calculus for klDiv (the identity (2.6) $I(P\|R)-I(P\|Q)=\int\log q_R\,dP$), Pinsker's inequality (available on the platform as a reference item), lower semicontinuity of klDiv under convergence in variation, completeness of the space of PD's in variation, and supporting hyperplanes of finite-dimensional convex functions. The KL parallelogram identity, Lemma 3.1 and the variation-distance facts are reusable well beyond this mission. Contributions on any milestone, and on these infrastructure lemmas, are welcome.

Selected references

• I. Csiszár, I-divergence geometry of probability distributions and minimization problems, Ann. Probab. 3(1), 146–158, 1975. https://doi.org/10.1214/aop/1176996454
• S. Kullback, Information Theory and Statistics, Wiley, 1959.
• S. Kullback and M. A. Khairat, A note on minimum discrimination information, Ann. Math. Statist. 37, 279–280, 1966.
• E. T. Jaynes, Information theory and statistical mechanics, Phys. Rev. 106, 620–630, 1957. https://doi.org/10.1103/PhysRev.106.620
• N. N. Čencov, Statistical Decision Rules and Optimal Inference (Russian), Nauka, 1972; English translation, American Mathematical Society, 1982.
• I. N. Sanov, On the probability of large deviations of random variables (Russian), Mat. Sbornik 42, 11–44, 1957.

Motivation

A loss network carries calls that require capacity on one or more links. A call is accepted only when every required link has enough free circuits; otherwise it is lost. This makes the traffic on different links dependent even when calls on different routes arrive independently. Network operators need to know where capacity constraints bind and how offered traffic is converted into carried traffic. Kelly's 1991 survey develops a continuous optimization problem that identifies a characteristic flow vector and gives a linkwise description of blocking in this setting. Kelly, Loss networks (1991), §§1.2 and 2.1.

The paper begins with the equilibrium distribution of the discrete network and uses a continuous relaxation when analyzing its likely state. The resulting primal problem is useful beyond the original probability calculation because it links route flows, capacity constraints, and a convex dual. Theorem 2.8 collects the existence, uniqueness, and correspondence statements for these descriptions. This mission targets that theorem and the intermediate claims Kelly states in §2.1. Kelly (1991), pp. 327–329.

Setting

There are finitely many links $j$ and finitely many routes $r$. Link $j$ has $C_j$ circuits, and one call on route $r$ uses $A_{jr}$ circuits there, with $A_{jr}$ a nonnegative integer. Calls request route $r$ at positive offered rate $\nu_r$. The matrix $A$ need not be a zero–one incidence matrix: one call may use more than one circuit on a link. Kelly's fixed-routing model and its general integer matrix are described in §1.2. Kelly (1991), p. 321.

A real route-flow vector $x=(x_r)$ is primal feasible if $x_r\ge0$ for every route and $\sum_r A_{jr}x_r\le C_j$ for every link. The objective is

$$F(x)=\sum_r\bigl(x_r\log\nu_r-x_r\log x_r+x_r\bigr),$$

with $x_r\log x_r=0$ at $x_r=0$. The primal optimum maximizes $F$ over precisely this feasible set. This is the continuous problem (2.1), rather than an optimization over the integer-valued network state. Kelly (1991), p. 327, (2.1).

A nonnegative vector $y=(y_j)$ assigns one multiplier to each link. The dual objective is

$$D(y)=\sum_r\nu_r\exp\!\left(-\sum_jy_jA_{jr}\right)+\sum_jy_jC_j, \qquad y_j\ge0.$$

A blocking vector $B=(B_j)$ has $0\le B_j<1$. Its carried route flow is $\nu_r\prod_i(1-B_i)^{A_{ir}}$. The conditions on $B$ say that the total carried flow through link $j$ equals $C_j$ when $B_j>0$, and is at most $C_j$ when $B_j=0$. The multiplier and blocking coordinates are related by $B_j=1-e^{-y_j}$, equivalently $y_j=-\log(1-B_j)$. These are equations (2.3), (2.6), and (2.7). Kelly (1991), p. 328.

Formalization targets

Theorem 2.8: primal optimum, blocking solutions, and dual optima

The goal first asserts that the primal problem has exactly one optimizer. Every blocking solution must describe that same optimizer:

$$x_r=\nu_r\prod_j(1-B_j)^{A_{jr}}\quad\text{for every route }r.$$

It also asserts that a blocking solution exists, and that it is unique if $A$ has rank $J$, the number of links. Finally, the transformations $B_j=1-e^{-y_j}$ and $y_j=-\log(1-B_j)$ give a bijection between all blocking solutions and all dual optima. The formal goal includes both directions and both inverse identities, even when the dual optimizer is not unique. Kelly (1991), p. 329, Theorem 2.8.

Claims leading to the theorem

The milestone list follows Kelly's stated progression: unique primal attainment; the Lagrangian maximum and the dual value in (2.2); feasibility and complementary slackness in (2.4)–(2.5); the substitution (2.6); dual attainment; both directions of the blocking–dual correspondence; and strict convexity plus uniqueness under full row rank. One direction of the correspondence is an existing, proved platform theorem, KellyStochasticNetworks.dual_optimum_conditions; it is referenced directly. The other direction remains a new target. Kelly (1991), pp. 327–329.

Significance

The theorem makes the carried flow uniquely determined even when several blocking vectors or dual optimizers describe it. Under full row rank, it also identifies a unique linkwise blocking vector. Its correspondence lets a statement in the flow language be translated to a statement in the multiplier language without selecting a preferred optimizer. The interpretation following Theorem 2.8 explains the linkwise condition: positive blocking occurs only on a saturated link. Kelly (1991), p. 329, discussion after Theorem 2.8.

The mathematical result was proved in the source paper. The work here is to obtain machine-checked proofs of its exact finite-dimensional statements. The published Kelly–Yudovina definition KellyStochasticNetworks.dualObjective already represents the dual formula, and its proved optimum-conditions theorem supplies one direction of the correspondence. The remaining development would give reusable facts about separable entropy objectives, nonnegative linear capacity constraints, complementary slackness, and exponential coordinate changes. Those facts can support later loss-network formalizations without changing this mission's target.

Difficulty

The boundary $x_r=0$ requires care: the objective has a continuous value there, but its logarithmic derivative does not. Thus a calculation that differentiates the objective throughout the closed nonnegative cone does not justify the printed differentiability sentence on p. 327. Dual existence is another boundary issue. A nonnegative capacity permits $C_j=0$, while the paper's stated growth of the dual objective in every nonnegative coordinate can fail at that input. Any formal argument for the complete theorem must cover these domains accurately. Full row rank controls uniqueness of the dual coordinates; without it, the paper explicitly allows nonunique blocking solutions. Kelly (1991), pp. 327–329.

Formalization scope

Lean represents links by Fin J, routes by Fin R, $A_{jr}$ and $C_j$ by natural numbers, and $x_r$, $y_j$, $B_j$, and $\nu_r$ by real numbers. The primal feasible set includes both coordinatewise nonnegativity and every link-capacity inequality. The dual optimum is minimal over the nonnegative orthant, using the published dual objective. The finite sums and products have their usual empty-index values; no hidden nonemptiness assumption is imposed. Matrix rank is taken over the reals and compared with $J$, so the rank condition is full row rank.

The goal assumes $\nu_r>0$ and $C_j\ge1$ for every route and link. Positive rates give the logarithm in the primal objective its intended meaning. Positive capacities exclude a degeneracy in the dual-attainment and blocking parts of the theorem. The value at $x_r=0$ is the continuous extension $x_r\log x_r=0$; no differentiability assertion at that boundary is part of the formal target. Blocking values belong to $[0,1)$, so the inverse logarithm is evaluated on a positive number. A flow optimum always ranges over the exact primal feasible set, and a blocking solution always ranges over the full conditions (2.7); neither can be replaced by an arbitrary vector with a convenient equation.

A complete proof may require finite-dimensional convex analysis, strict concavity of the entropy term, attainment on a closed feasible set, the dual first-order condition, and facts about exponentials, logarithms, products, and matrix rank. The definitions and theorems are kept separate so work on these pieces can be reused. Contributions proving either a milestone or a reusable supporting lemma are in scope.

Selected references

• F. P. Kelly, Loss networks, The Annals of Applied Probability 1(3), 319–378, 1991. DOI: 10.1214/aoap/1177005872.