Probability

Motivation

The classical Chernoff bound controls the probability that a sum of independent, nonnegative, uniformly bounded random variables deviates from its mean, with exponentially small tails governed by the Kullback–Leibler divergence between two Bernoulli laws. Many problems in numerical linear algebra, graph sparsification, compressed sensing and randomized algorithms instead require control of a sum of independent random matrices: the smallest singular value of a random matrix with independent columns, the spectrum of a sampled Laplacian, or the conditioning of a random submatrix. For these, what matters is not a scalar sum but the extreme eigenvalues of a random positive-semidefinite matrix.

Ahlswede and Winter (2002) introduced a matrix version of the Laplace transform method and proved a matrix Chernoff bound for identically distributed summands. Tropp's paper (arXiv:1004.4389, Found. Comput. Math. 2012) replaced the Golden–Thompson step of their argument with Lieb's concavity theorem, obtaining a master tail bound for independent sums, and derived from it matrix Chernoff, Bernstein and Azuma inequalities that require no identical distribution and lose only a dimensional factor. This mission formalizes the matrix Chernoff inequalities of §5 of that paper.

Timeline:

• 2002, Ahlswede–Winter: matrix Laplace transform method; matrix Chernoff bound for i.i.d. summands via Golden–Thompson.
• 2010, Oliveira: a variant of the Laplace transform method used in Proposition 3.1 of the paper.
• 2010–2012, Tropp: master tail bound via Lieb's theorem (Theorem 3.6), and Theorem 5.1 / Corollary 5.2 for independent, non-identical psd summands.

Setting

All matrices are $d\times d$ complex matrices with $d\ge1$. For a self-adjoint (Hermitian) matrix $A$, $\lambda_{\max}(A)$ and $\lambda_{\min}(A)$ are its algebraically largest and smallest eigenvalues. The semidefinite order $A\preccurlyeq B$ means that $B-A$ is positive semidefinite (psd). Functions of a self-adjoint matrix are defined spectrally: if $A = Q\Lambda Q^*$ then $f(A) = Qf(\Lambda)Q^*$; this gives the matrix exponential $e^A$ and, on positive-definite matrices, the matrix logarithm $\log A$.

A random matrix is a measurable map $X:\Omega\to\mathbb C^{d\times d}$ on a probability space $(\Omega,\mathcal F,\mathbb P)$, and its expectation $\mathbb E X$ is taken entrywise. The matrix moment generating function of $X$ is $\theta\mapsto\mathbb E\,e^{\theta X}$.

The objects of the mission are independent random Hermitian matrices $X_1,\dots,X_n$ that are almost surely psd contractions: $X_k\succcurlyeq0$ and $\lambda_{\max}(X_k)\le1$. Their average expectation has extreme eigenvalues

$$\bar\mu_{\min} = \lambda_{\min}\Big(\frac1n\sum_{k=1}^n\mathbb E X_k\Big),\qquad \bar\mu_{\max}=\lambda_{\max}\Big(\frac1n\sum_{k=1}^n\mathbb E X_k\Big),$$

and the binary information divergence is

$$\mathrm D(a\,\|\,u) = a(\log a-\log u)+(1-a)(\log(1-a)-\log(1-u)),\qquad a,u\in[0,1].$$

In Lean these are lambdaMax, lambdaMin, mexp, mlog, mean and binDiv in the namespace MatrixTail.Chernoff.

Formalization targets

Goal: Theorem 5.1 (Matrix Chernoff I)

$$\mathbb P\Big\{\lambda_{\min}\Big(\tfrac1n\textstyle\sum_k X_k\Big)\le\alpha\Big\}\le d\,e^{-n\,\mathrm D(\alpha\|\bar\mu_{\min})}\quad(0\le\alpha\le\bar\mu_{\min}),$$ $$\mathbb P\Big\{\lambda_{\max}\Big(\tfrac1n\textstyle\sum_k X_k\Big)\ge\alpha\Big\}\le d\,e^{-n\,\mathrm D(\alpha\|\bar\mu_{\max})}\quad(\bar\mu_{\max}\le\alpha\le1).$$

Milestones

1. Theorem 3.6 (master tail bound): for every $\theta>0$ at which the mgfs exist, $\mathbb P\{\lambda_{\max}(\sum_kX_k)\ge t\}\le e^{-\theta t}\operatorname{tr}\exp(\sum_k\log\mathbb E\,e^{\theta X_k})$.
2. Corollary 3.9: the same with the mgfs under one logarithm, $d\cdot\exp(-\theta t+n\log\lambda_{\max}(\frac1n\sum_k\mathbb E\,e^{\theta X_k}))$.
3. Lemma 5.8 (Chernoff mgf): $\mathbb E\,e^{\theta X}\preccurlyeq\mathbf I+(e^\theta-1)\mathbb E X$ for a random psd contraction $X$.
4. Display (5.1): $\mathbb P\{\lambda_{\max}(\sum_kX_k)\ge t\}\le d\exp(-\theta t+n\log(1+(e^\theta-1)\bar\mu_{\max}))$.
5. Display (5.2): $\mathbb P\{\lambda_{\min}(\sum_kX_k)\le t\}\le d\exp(\theta t+n\log(1-(1-e^{-\theta})\bar\mu_{\min}))$.

Further statement

Corollary 5.2 (Matrix Chernoff II), the form usually quoted: with $\lambda_{\max}(X_k)\le R$, $\mu_{\min},\mu_{\max}$ the extreme eigenvalues of $\sum_k\mathbb E X_k$,

$$\mathbb P\{\lambda_{\min}(\textstyle\sum_kX_k)\le(1-\delta)\mu_{\min}\}\le d\Big[\tfrac{e^{-\delta}}{(1-\delta)^{1-\delta}}\Big]^{\mu_{\min}/R},\quad \mathbb P\{\lambda_{\max}(\textstyle\sum_kX_k)\ge(1+\delta)\mu_{\max}\}\le d\Big[\tfrac{e^{\delta}}{(1+\delta)^{1+\delta}}\Big]^{\mu_{\max}/R}.$$

Significance

Theorem 5.1 matches the strongest scalar Chernoff bound for independent, non-identical Bernoulli trials, up to the factor $d$, which cannot be removed (coupon collector, Remark 5.6). Corollary 5.2 is the version used in applications: lower bounds on the smallest singular value of matrices with independent columns (Remark 5.4), spectral sparsification, column subset selection and random sampling of matrices. Remark 5.5 derives from it the expectation bound $\mathbb E\lambda_{\max}(\sum_kX_k)\le C\max\{\mu_{\max},R\log d\}$.

The results are proved in the paper, from Lieb's concavity theorem. As far as is known, no machine-checked proof of a matrix Chernoff inequality exists in Lean or Mathlib. A formalization yields a reusable statement for the random-matrix and randomized-numerical-linear-algebra literature, and the milestones (the master bound, the single-logarithm corollary and the semidefinite mgf bound) are reusable beyond this mission.

Difficulty

The scalar Chernoff argument uses $\mathbb E\,e^{\theta(X+Y)}=\mathbb E\,e^{\theta X}\,\mathbb E\,e^{\theta Y}$ for independent $X,Y$. For matrices $e^{A+B}\neq e^Ae^B$ unless $A$ and $B$ commute, so the trace of the mgf of a sum does not factor. The Golden–Thompson inequality handles two summands but does not extend to three, which is why the Ahlswede–Winter bound needed identical distributions. The master bound (Theorem 3.6) requires Lieb's concavity theorem, which has no counterpart in Mathlib. Corollary 3.9 in addition needs operator concavity of the matrix logarithm, and Lemma 5.8 needs the transfer of a scalar inequality to the semidefinite order through the spectral calculus.

Formalization scope

Matrices are Matrix (Fin d) (Fin d) ℂ with [NeZero d]; the semidefinite order is Mathlib's MatrixOrder (A ≤ B ↔ (B − A).PosSemidef). exp and log of a matrix are the continuous functional calculus cfc. $\lambda_{\max}$, $\lambda_{\min}$ are sSup/sInf of the real spectrum. Expectation is entrywise. Random matrices are measurable with respect to the Borel σ-algebra on matrices, independence is iIndepFun, and the probability measure is a probability measure. The summands are Hermitian for every outcome; "psd" and "$\lambda_{\max}\le1$" hold almost surely. The sequence has $n\ge1$ terms wherever an average $1/n$ appears. An infimum over $\theta>0$ is stated as a bound for every admissible $\theta>0$; integrability of $e^{\theta X_k}$ is a hypothesis only in Theorem 3.6 and Corollary 3.9, where the summands are unbounded. In Lean $\log 0=0$, so at the boundary values $\bar\mu\in\{0,1\}$ the divergence is finite where the paper's is $+\infty$; this only weakens the stated bound.

A formalization in which $d=0$ (empty spectrum, $\lambda_{\max}=0$) or $n=0$ (the average $1/0=0$) were allowed, or in which the range of $\alpha$ were dropped, would state a different, partly false theorem; these cases are excluded.

A complete development needs Lieb's theorem or another route to the master bound, operator concavity of the logarithm, the spectral mapping theorem and the transfer rule for the functional calculus on Hermitian matrices, monotonicity of the trace exponential, and the scalar optimization in $\theta$. Contributions of any of these as stand-alone lemmas are welcome.

Selected references

• J. A. Tropp, User-Friendly Tail Bounds for Sums of Random Matrices, arXiv:1004.4389v7 (2011); Found. Comput. Math. 12 (2012) 389–434. https://arxiv.org/abs/1004.4389, https://doi.org/10.1007/s10208-011-9099-z
• R. Ahlswede, A. Winter, Strong converse for identification via quantum channels, IEEE Trans. Inform. Theory 48 (2002) 569–579. https://doi.org/10.1109/18.985947
• E. H. Lieb, Convex trace functions and the Wigner–Yanase–Dyson conjecture, Adv. Math. 11 (1973) 267–288. https://doi.org/10.1016/0001-8708(73)90011-X
• R. I. Oliveira, Sums of random Hermitian matrices and an inequality by Rudelson, Electron. Commun. Probab. 15 (2010) 203–212. https://arxiv.org/abs/1004.3821

Motivation

A matrix Gaussian series $\sum_k \gamma_k A_k$, a sum of fixed self-adjoint matrices each multiplied by an independent standard normal variable, is the simplest sum of independent random matrices. It already appears in the analysis of random designs, in compressed sensing, in randomized numerical linear algebra and in quantum information, wherever one needs to know how large the spectrum of a random linear combination of matrices can be. Its Rademacher analogue $\sum_k \varepsilon_k A_k$, with random signs, plays the same role in symmetrization arguments.

For real coefficients $a_k$ the answer is classical: $\sum_k \gamma_k a_k$ is normal with variance $\sum_k a_k^2$, so its upper tail is at most $e^{-t^2/2\sigma^2}$. Tropp's paper (arXiv:1004.4389v7) shows that the same bound holds for the largest eigenvalue of a matrix series, with an explicit dimensional factor and with the variance parameter $\|\sum_k A_k^2\|$.

Timeline. Noncommutative Khintchine inequalities (Lust-Piquard 1986; Lust-Piquard and Pisier 1991) control the moments of matrix Rademacher and Gaussian series and imply tail bounds of this type. Ahlswede and Winter (2002, arXiv:quant-ph/0012127) introduced the matrix Laplace transform method, whose bounds depend on the sum of the norms $\sum_k\|A_k^2\|$. Oliveira (2010, arXiv:1004.3821) obtained bounds of the same form as Theorem 4.1. Tropp (2012) derived the result from a master inequality built on Lieb's concavity theorem (1973), which produces the norm of the sum, $\|\sum_k A_k^2\|$, as variance parameter. The paper itself notes that Theorem 4.1 and Corollary 4.2 are not new results; the contribution is the route through the master bound.

Setting

Fix a dimension $d\ge1$. Matrices are $d\times d$ complex arrays; a matrix is self-adjoint if it equals its conjugate transpose. For a self-adjoint $A$, $\lambda_{\max}(A)$ is its largest eigenvalue, and $\|A\|$ is the spectral norm, the operator norm on $\mathbb C^d$ with the Euclidean norm. Functions of a self-adjoint matrix are defined through its eigen-decomposition: $e^A$, $\log A$ (for positive-definite $A$), $\cosh A$. The semidefinite order $A\preccurlyeq H$ means that $H-A$ is positive semidefinite.

A random matrix is a measurable map from a probability space $(\Omega,\mathcal F,\mathbb P)$ into the $d\times d$ complex matrices; its expectation $\mathbb E X$ is taken entry by entry. A Rademacher variable takes the values $\pm1$ with probability $1/2$ each; a standard normal variable has law $N(0,1)$.

The data of the mission are fixed self-adjoint matrices $A_1,\dots,A_n$ and independent scalar variables $\xi_1,\dots,\xi_n$, all standard normal or all Rademacher. The variance parameter is

$$\sigma^2 := \Big\|\sum_k A_k^2\Big\|.$$

Formalization targets

Goal: Theorem 4.1 (p. 14)

For all $t\ge0$,

$$\mathbb P\Big\{\lambda_{\max}\Big(\sum_k\xi_kA_k\Big)\ge t\Big\}\le d\,e^{-t^2/2\sigma^2},\qquad \mathbb P\Big\{\Big\|\sum_k\xi_kA_k\Big\|\ge t\Big\}\le 2d\,e^{-t^2/2\sigma^2}.$$

Milestones

1. Theorem 3.6 (master tail bound, p. 12): for independent random self-adjoint $X_k$ and every $t$,

$$\mathbb P\Big\{\lambda_{\max}\Big(\sum_kX_k\Big)\ge t\Big\}\le\inf_{\theta>0}e^{-\theta t}\operatorname{tr}\exp\Big(\sum_k\log\mathbb Ee^{\theta X_k}\Big).$$

2. Corollary 3.7 (p. 12): if $\mathbb Ee^{\theta X_k}\preccurlyeq e^{g(\theta)A_k}$ with $g\ge0$, then the tail is at most $d\inf_{\theta>0}e^{-\theta t+g(\theta)\rho}$ with $\rho=\lambda_{\max}(\sum_kA_k)$.
3. Display (2.4) (p. 8): $\cosh(A)\preccurlyeq e^{A^2/2}$ for every self-adjoint $A$.
4. Lemma 4.3 (p. 15): $\mathbb Ee^{\varepsilon\theta A}\preccurlyeq e^{\theta^2A^2/2}$ for Rademacher $\varepsilon$ and $\mathbb Ee^{\gamma\theta A}=e^{\theta^2A^2/2}$ for standard normal $\gamma$.

Further item: Corollary 4.2 (p. 15)

For fixed $d_1\times d_2$ matrices $B_k$ and $\sigma^2=\max\{\|\sum_kB_kB_k^*\|,\|\sum_kB_k^*B_k\|\}$,

$$\mathbb P\Big\{\Big\|\sum_k\xi_kB_k\Big\|\ge t\Big\}\le(d_1+d_2)\,e^{-t^2/2\sigma^2}.$$

Significance

The result. Theorem 4.1 is the template for every inequality in the paper: a scalar tail bound carried over to matrices at the cost of a factor $d$, with a variance parameter that is the norm of a sum rather than a sum of norms. The difference matters: $\sum_k\|A_k^2\|$ can exceed $\|\sum_kA_k^2\|$ by a factor of $d$, and §4 of the paper shows that both the variance parameter and the dimensional factor in (4.3) are needed in general. Corollary 4.2 transfers the bound to the largest singular value of a rectangular series, which covers Gaussian matrices with nonuniform variances (§4.3).

Formalizing it. The theorem is proved in the paper; the work here is to formalize that proof. The milestones are reusable beyond this mission: Theorem 3.6 and Corollary 3.7 are the common entry point of the Chernoff, Bernstein and Azuma missions of this series, and the Rademacher half of Lemma 4.3 is used again in the matrix Azuma mission. No machine-checked proof of these matrix inequalities was found in Mathlib or on the platform when this mission was drafted.

Difficulty

The scalar argument bounds $\mathbb E e^{\theta\sum_k X_k}$ by the product of the individual mgfs, using $e^{a+b}=e^ae^b$. For matrices this identity fails when the summands do not commute, and the trace inequality that replaces it for two matrices (Golden–Thompson) has no analogue for three or more. Controlling the trace mgf of a sum of many noncommuting independent matrices therefore requires a genuinely matrix-analytic input with no scalar counterpart; the naive product bound is not available. A second difficulty is infrastructural: matrix functions, the semidefinite order and expectations of random matrices must be combined in a single setting.

Formalization scope

Matrices are Matrix (Fin d) (Fin d) ℂ with [NeZero d]; self-adjointness is IsHermitian; $e^A$, $\log A$, $\cosh A$ are Mathlib's continuous functional calculus cfc; $\preccurlyeq$ is Mathlib's Loewner order under MatrixOrder; $\lambda_{\max}$ is the supremum of the real spectrum; $\|\cdot\|$ is the operator norm on $\ell_2$. Expectation is entrywise, and the paper's standing regularity assumption is made explicit as entrywise integrability of every matrix whose expectation is taken. The infimum over $\theta>0$ is stated pointwise: the bound is asserted for every $\theta>0$ at which the mgfs exist, which is equivalent to the infimum form. Independence is iIndepFun of the scalar variables, and "Gaussian or Rademacher" is the disjunction of two hypotheses, never a mixture of laws.

The variance parameter is the norm of the sum $\|\sum_kA_k^2\|$; a formalization with $\sum_k\|A_k^2\|$, with a constant different from $1/2$, or with the dimensional factor omitted is a different theorem. At $\sigma^2=0$, Lean's division by zero makes the bound the trivial $d$; this is the only degenerate case and it is valid.

The development needs: the spectral calculus for Hermitian matrices, monotonicity of the trace exponential, operator monotonicity of the matrix logarithm, Lieb's theorem, and moments of the Gaussian. These are reusable well beyond this paper; proofs of the milestones, of supporting matrix-analysis lemmas, and alternative routes (for instance through noncommutative Khintchine inequalities) are all welcome.

Selected references

• J. A. Tropp, User-Friendly Tail Bounds for Sums of Random Matrices, Found. Comput. Math. 12 (2012) 389–434; cited from arXiv:1004.4389v7. https://arxiv.org/abs/1004.4389, https://doi.org/10.1007/s10208-011-9099-z
• R. Ahlswede and A. Winter, Strong converse for identification via quantum channels, IEEE Trans. Inform. Theory 48 (2002) 569–579. https://arxiv.org/abs/quant-ph/0012127
• R. I. Oliveira, Sums of random Hermitian matrices and an inequality by Rudelson, Electron. Commun. Probab. 15 (2010) 203–212. https://arxiv.org/abs/1004.3821
• E. H. Lieb, Convex trace functions and the Wigner–Yanase–Dyson conjecture, Adv. Math. 11 (1973) 267–288. https://doi.org/10.1016/0001-8708(73)90011-X
• F. Lust-Piquard and G. Pisier, Non commutative Khintchine and Paley inequalities, Ark. Mat. 29 (1991) 241–260. https://doi.org/10.1007/BF02384340

Motivation

A data curator holds a database of $n$ individual records and wants to publish something from which many statistics can be computed, while guaranteeing differential privacy: no single record should noticeably change what is published (Dwork, McSherry, Nissim, Smith 2006). Interactive mechanisms answer queries one at a time and add noise to each answer, so their accuracy degrades as more queries are asked; Dinur and Nissim showed that answering too many arbitrary queries accurately reveals the database (Dinur, Nissim 2003).

Blum, Ligett and Roth asked a different question: can a curator release, once and non-interactively, a synthetic database that is accurate simultaneously for every query of a large, structured class, while remaining differentially private? Their answer (arXiv:1109.2229; JACM 60(2), 2013; conference version STOC 2008) is yes for every class of counting queries over a discretized universe, with accuracy governed by the class's VC-dimension rather than its cardinality. The mechanism it introduces, the Net mechanism, became the starting point of the literature on private query release (SmallDB, private multiplicative weights, and the lower bounds that followed).

Setting

Fix a finite data universe $X$ (for instance $X=\{0,1\}^k$). The curator's input is an $n$-tuple $z=(z_1,\dots,z_n)\in X^n$, read as a multiset of records. Two inputs are neighbouring if they differ in exactly one entry.

A database of arbitrary size $D\in X^*$ is a finite nonempty multiset of elements of $X$. For a predicate $\varphi:X\to\{0,1\}$ the counting query is

$$Q_\varphi(D)=\frac{1}{|D|}\sum_{x\in D}\varphi(x),$$

the fraction of records satisfying $\varphi$. A class $C$ of predicates is identified with its class of counting queries, and its VC-dimension $\mathrm{VCDIM}(C)$ is the size of the largest set of points that $C$ shatters.

A randomized mechanism $A$, whose output on input $z$ is a random database $\hat D\in X^*$, is $\varepsilon$-differentially private if $\Pr[A(z)\in S]\le e^{\varepsilon}\Pr[A(z')\in S]$ for all neighbouring $z,z'$ and all sets $S$ of outputs. It is $(\alpha,\delta)$-useful for $C$ if for every input $z$, with probability at least $1-\delta$, $|Q_\varphi(\hat D)-Q_\varphi(z)|\le\alpha$ for every $\varphi\in C$.

The global sensitivity of $f:X^n\to\mathbb R$ is $GS_f=\max|f(z)-f(z')|$ over neighbouring pairs. An $\alpha$-net for $C$ is a finite set $N\subseteq X^*$ such that every $D\in X^*$ has some $D'\in N$ with $|Q_\varphi(D)-Q_\varphi(D')|\le\alpha$ for all $\varphi\in C$; $N_\alpha(C)$ denotes a net of minimum size.

The exponential mechanism with quality score $q:X^n\times R\to\mathbb R$ over a finite range $R$ outputs $r$ with probability proportional to $\exp(\varepsilon q(z,r)/(2GS_q))$. The Net mechanism is the exponential mechanism over $R=N_\alpha(C)$ with score $q(z,D')=-\max_{\varphi\in C}|Q_\varphi(z)-Q_\varphi(D')|$.

Formalization targets

Goal: Theorem 3.10

There is an absolute constant $c>0$ such that, for every finite $X$, $d=\mathrm{VCDIM}(C)\ge1$, $n\ge1$, $\varepsilon>0$, $0<\delta\le1$, $0<\alpha\le\tfrac12$, whenever

$$\alpha\ \ge\ \frac{c}{\varepsilon\alpha^2 n}\Big(d\log|X|\log\frac1\alpha+\log\frac1\delta\Big),$$

a minimum $\tfrac\alpha2$-net exists and the Net mechanism run on any minimum $\tfrac\alpha2$-net is $(\alpha,\delta)$-useful for $C$. The constant is left unspecified, as in the paper; the goal asserts the shape of the bound, not a value of $c$.

Milestones

1. Observation 2.4: $GS_{Q_\varphi}\le 1/n$.
2. Theorem 3.2 and Property 3.3: the exponential mechanism, hence the Net mechanism, is $\varepsilon$-differentially private.
3. Property 3.4: for any query class with sensitivities at most $\Delta$, the Net mechanism is $(2\alpha,\delta)$-useful once $\alpha\ge\frac{2\Delta}{\varepsilon}\log\frac{|N_\alpha(C)|}{\delta}$.
4. Corollary 3.5: for counting queries, $(2\alpha,\delta)$-useful once $\alpha\ge\frac{2}{\varepsilon n}\log\frac{|N_\alpha(C)|}{\delta}$.
5. Lemma 3.7 and Theorem 3.6 (finite classes): $|N_\alpha(C)|\le|X|^{\lceil\log|C|/\alpha^2\rceil}$.
6. Lemma 3.8 and Theorem 3.9 (finite VC-dimension): $|N_\alpha(C)|\le|X|^{c_0\,d\log(1/\alpha)/\alpha^2}$.

Significance

The result. Theorem 3.10 shows that a database of size roughly $\tilde O(\mathrm{VCDIM}(C)\log|X|/(\alpha^3\varepsilon))$ suffices to release, privately, a synthetic database answering every query of $C$ to within $\alpha$. This is only a polynomial factor above what sampling needs without privacy, and it covers classes with exponentially many queries in $n$, which interactive noise addition cannot. Together with Property 3.3 it is the first general feasibility result for non-interactive private release, and it identified VC-dimension as the governing parameter.

Formalizing it. The result is proved in the paper, modulo the cited uniform-convergence lemma (Lemma 3.8). No part of it is machine-checked on the platform. A complete development would give a formal exponential mechanism with a general score and its privacy proof, a formal utility analysis of a mechanism with a finite range, and a formal ε-approximation theorem for VC classes, which is the deepest dependency and reusable across learning theory.

Difficulty

The privacy and utility of the exponential mechanism (Theorem 3.2, Property 3.4) are short ratio arguments. The difficulty is concentrated in bounding the size of the net. For finite classes a random-sampling and union-bound argument suffices (Lemma 3.7). For infinite classes the union bound over $C$ is unavailable, and Lemma 3.8 needs uniform convergence over a class of finite VC-dimension, uniformly over every finite multiset $D$: a symmetrization or chaining argument together with the Sauer–Shelah lemma, none of which is in Mathlib in this form. The obvious route of applying the finite-class bound to the restriction of $C$ to the support of $D$ gives a size depending on $|D|$ and fails.

Formalization scope

• Inputs are Fin n → X with X : Type finite; neighbouring means "replace one entry", the platform's PrivLearn.Generic.Neighbors. The paper's "$|D\Delta D'|\le1$" read literally for equal-size multisets forces $D=D'$ and would make every mechanism private.
• Databases of arbitrary size are nonempty multisets (Database X), with every set measurable. Queries are real functions on multisets, so the same query reads inputs and outputs. Predicates are X → Bool; VC-dimension is the platform's HighDimProb.Chaining.vcDim (valued in ℕ∞; the theorems take it finite, equal to $d\ge1$).
• Usefulness and α-nets use "for all $Q\in C$", not a real supremum. $N_\alpha(C)$ is never an infimum of cardinalities: statements quantify over minimum nets and assert that one exists.
• The exponential mechanism is a finite mixture of point masses. Where the paper divides by $GS_q$, Theorem 3.2 and Properties 3.3–3.4 assume $GS_q>0$; Corollary 3.5 and Theorem 3.10 need no such hypothesis, because for counting queries $GS_q=0$ forces a regime in which every output is accurate.
• $O(\cdot)$ instantiations. Lemma 3.8: $|D'|\le c_0\,d\log(1/\alpha)/\alpha^2$. Theorem 3.9: $|N_\alpha(C)|\le|X|^{c_0 d\log(1/\alpha)/\alpha^2}$ (real power). Theorem 3.10: the condition $\alpha\ge\frac{c}{\varepsilon\alpha^2n}(d\log|X|\log\frac1\alpha+\log\frac1\delta)$. Each constant is absolute and quantified before the universe and the class. Theorem 3.10's $(\alpha,\delta)$ is Corollary 3.5's $(2\alpha',\delta)$ at $\alpha'=\alpha/2$, so the mechanism runs on a minimum $\alpha/2$-net. Lemma 3.7 and Theorem 3.6 round $\log|C|/\alpha^2$ up and assume $|C|\ge3$, as the paper's proof does.
• Excluded corners, disclosed in each statement: $d=0$, $\alpha>\tfrac12$. Logarithms are natural. The "solving for α" display $\tilde O(\cdot)^{1/3}$ of Theorem 3.10 is out of scope.
• A trivializing formalization is ruled out: usefulness is required of the Net mechanism as defined, whose output law is a genuine probability distribution over a nonempty net of nonempty databases (Property 3.3 records this), not of a zero measure, an empty net, or a net containing the empty database.

Welcome contributions: a general ε-approximation theorem for VC classes (Lemma 3.8), reusable well beyond this mission; a reusable exponential-mechanism privacy proof; the finite-range utility analysis of Property 3.4.

Selected references

• A. Blum, K. Ligett, A. Roth, A Learning Theory Approach to Non-Interactive Database Privacy, arXiv:1109.2229v1, 2011; J. ACM 60(2), 2013. https://arxiv.org/abs/1109.2229
• F. McSherry, K. Talwar, Mechanism Design via Differential Privacy, FOCS 2007. https://doi.org/10.1109/FOCS.2007.66
• C. Dwork, F. McSherry, K. Nissim, A. Smith, Calibrating Noise to Sensitivity in Private Data Analysis, TCC 2006. https://doi.org/10.1007/11681878_14
• I. Dinur, K. Nissim, Revealing Information while Preserving Privacy, PODS 2003. https://doi.org/10.1145/773153.773173
• M. Anthony, P. L. Bartlett, Neural Network Learning: Theoretical Foundations, Cambridge University Press, 1999. https://doi.org/10.1017/CBO9780511624216
• V. N. Vapnik, Statistical Learning Theory, Wiley, 1998.
• Y. Li, P. M. Long, A. Srinivasan, Improved Bounds on the Sample Complexity of Learning, J. Comput. Syst. Sci. 62(3), 2001. https://doi.org/10.1006/jcss.2000.1741

Motivation

Differential privacy (Dwork, McSherry, Nissim, Smith 2006) asks that a randomized algorithm run on a database behave almost identically whether or not any single record is changed. A central question for data curators is non-interactive release: publish, once, a sanitized object (ideally a synthetic database) from which analysts can answer many statistical queries accurately. Blum, Ligett and Roth (arXiv:1109.2229, JACM 2013) showed that over a discrete data universe this is possible for every class of counting queries of bounded VC-dimension, with accuracy governed by the VC-dimension and the logarithm of the universe size.

That dependence on the universe size raises an obvious question: can the discretization be removed? For real-valued data the class of interval queries ("what fraction of the records lies in $[a,b]$?") has VC-dimension 2, so a learning-theoretic intuition suggests that releasing a database accurate for all intervals should be easy. Section 5 of the paper shows that it is impossible under differential privacy. This mission formalizes that impossibility.

The phenomenon was later quantified: Bun, Nissim, Stemmer and Vadhan (FOCS 2015) showed that for approximate differential privacy, releasing threshold queries over a finite ordered domain of size $N$ requires sample size growing with $\log^* N$, so that the infinite case is impossible for approximate privacy as well. The present result is the pure-privacy statement for the real line.

Setting

A real-valued database of size $n \ge 1$ is a tuple $z = (z_1,\dots,z_n) \in \mathbb R^n$. Two databases are neighbours if they differ in exactly one coordinate. A mechanism maps each database $z$ to a probability distribution $A(z)$ on a measurable output space $O$. It is $\varepsilon$-differentially private if for all neighbours $z, z'$ and all measurable $S \subseteq O$,

$$\Pr[A(z) \in S] \le e^{\varepsilon}\,\Pr[A(z') \in S].$$

For real $a \le b$ the interval query is $Q_{[a,b]}(z) = \#\{i : a \le z_i \le b\}/n$. A mechanism with a readout $\mathrm{ans}(o,a,b)$ (the answer that output $o$ gives to $Q_{[a,b]}$; for synthetic data $\hat D$, $\mathrm{ans}(\hat D,a,b) = Q_{[a,b]}(\hat D)$) is $(\alpha,\delta)$-useful for interval queries if for every database $z$,

$$\Pr_{o\sim A(z)}\big[\forall a \le b:\ |\mathrm{ans}(o,a,b) - Q_{[a,b]}(z)| \le \alpha\big] \ge 1-\delta .$$

A real number $r$ is a $\theta$-percentile point of $z$ (the paper's "$50-\delta, 50+\delta$ percentile" with $\theta = \delta/100$) if at least $(1/2-\theta)n$ entries satisfy $z_i \le r$ and at least $(1/2-\theta)n$ entries satisfy $z_i \ge r$. A mechanism with real outputs answers median queries usefully with positive probability if on every database its output is a $\theta$-percentile point with positive probability.

In Lean, databases are Fin n → ℝ; neighbours and differential privacy are the published PrivLearn.Generic.Neighbors and PrivLearn.Generic.IsDP; the new objects are intervalQuery, IsPercentile, AnswersMedianUsefully and UsefulIntervals in PrivateRelease.Continuous.

Formalization targets

Goal: Corollary 5.2 (p. 15)

For every $n \ge 1$, $\varepsilon \ge 0$ and $\alpha, \delta < 1/2$, no $\varepsilon$-differentially private mechanism with a measurable readout is $(\alpha,\delta)$-useful for interval queries on $\mathbb R^n$:

$$\mathrm{IsDP}(A,\varepsilon) \;\Longrightarrow\; \neg\,\mathrm{UsefulIntervals}(A,\mathrm{ans},\alpha,\delta).$$

No constant is hard-coded; the thresholds $1/2$ are the paper's.

Milestone: Theorem 5.1 (p. 14)

For every $n \ge 1$, $0 \le \theta < 1/2$ and real $\varepsilon$, no $\varepsilon$-differentially private mechanism $A : \mathbb R^n \to \mathcal P(\mathbb R)$ answers median queries usefully with positive probability on every database:

$$\mathrm{IsDP}(A,\varepsilon) \;\Longrightarrow\; \exists z,\ \Pr_{r\sim A(z)}[r \text{ is a } \theta\text{-percentile point of } z] = 0 .$$

Significance

The result. Corollary 5.2 is the reason the paper's general release mechanism needs a discretized data universe and why its halfspace mechanism (§6) relaxes usefulness to large-margin queries. More broadly it separates private release from non-private learning: the class of intervals is learnable from $O(1/\alpha^2)$ samples without privacy, yet no pure-private mechanism can release it at all over $\mathbb R$. It anticipates the line of work on private learning of thresholds and the role of the domain size in private query release.

Formalizing it. Both statements are proved in the paper; neither is, to our knowledge, machine-checked. A formal proof needs the countability of the atoms of a finite measure on $\mathbb R$, the stability of differential privacy under measurable post-processing, and a measurable selection of a percentile point from approximate interval answers. These pieces (especially post-processing for general measurable outputs) are reusable across formalized differential privacy.

Difficulty

The obvious argument for Theorem 5.1, a direct comparison of two neighbouring databases, gives nothing: changing one record moves the percentile set only slightly, and differential privacy allows each probability to change by a factor $e^{\varepsilon}$, so no single pair of neighbours yields a contradiction. A naive appeal to "the median reveals a record" also fails, since the statement must exclude even mechanisms that are correct with tiny positive probability.

For Corollary 5.2 the difficulty is measure-theoretic: the usefulness event intersects uncountably many conditions, the release must be converted into a single real output measurably, and the converted output must be a percentile point on the useful event for every real database, not only those in $[0,1]$.

Formalization scope

Conventions committed to in Lean:

• Databases are ordered tuples Fin n → ℝ with $n \ge 1$; the paper's neighbour relation "$|D\Delta D'| \le 1$" is read as replace-one-entry.
• Mechanisms are families of probability measures (IsProbabilityMeasure (A z) is a hypothesis). Theorem 5.1's outputs live in $\mathbb R$ with its Borel σ-algebra.
• Interval queries use closed intervals $[a,b]$ with $a \le b$, as in the paper's indicator $I_{a_1,a_2}$ (p. 12).
• Usefulness is required on every database in $\mathbb R^n$ (Definition 2.10 with $X = \mathbb R$). The usefulness event need not be measurable; its probability is the outer measure.
• The goal is stated for an arbitrary measurable output space with a readout $\mathrm{ans}$ measurable in the output for each fixed query. Synthetic data is a special case, so the formal goal is at least as strong as the paper's. The readout's measurability is necessary for the statement to be true with outer measures.
• The percentile set counts entries equal to $r$ on both sides. A one-sided reading ($\#\{z_i \le r\}/n \in [1/2-\theta, 1/2+\theta]$) makes the set empty for constant databases, so that Theorem 5.1 would hold vacuously; the chosen definition always contains a sample median and equals $\{c\}$ on a constant database $(c,\dots,c)$ (both facts were checked locally in Lean).
• Trivializing readings are ruled out: the percentile set is never empty, the mechanism is a probability measure (the zero measure is differentially private), and $n = 0$ (no neighbours, $Q = 0/0 = 0$ in Lean) is excluded.
• There is no O(·)/Ω(·) in this section, so no constant was instantiated.
• Not formalized: the clause of Corollary 5.2 "nor for any class $C$ that generalizes interval queries to higher dimensions (for example, halfspaces, axis-aligned rectangles, or spheres)", because the paper does not define "generalizes".

Contributions welcome: a proof of Theorem 5.1; a general post-processing lemma for IsDP; the reduction from interval usefulness to median answers.

Selected references

• A. Blum, K. Ligett, A. Roth, A Learning Theory Approach to Non-Interactive Database Privacy, arXiv:1109.2229v1, 2011; J. ACM 60(2), 2013. https://arxiv.org/abs/1109.2229, https://doi.org/10.1145/2450142.2450148
• C. Dwork, F. McSherry, K. Nissim, A. Smith, Calibrating Noise to Sensitivity in Private Data Analysis, TCC 2006. https://doi.org/10.1007/11681878_14
• M. Bun, K. Nissim, U. Stemmer, S. Vadhan, Differentially Private Release and Learning of Threshold Functions, FOCS 2015. https://arxiv.org/abs/1504.07553

Motivation

Differential privacy (Dwork, McSherry, Nissim and Smith 2006) is the standard guarantee for releasing statistics about a sensitive database: replacing one record changes the probability of any outcome by at most a factor $e^{\varepsilon}$. In their paper on non-interactive database privacy, Blum, Ligett and Roth propose an alternative motivated by learning theory, distributional privacy. When a database is a sample from a population, a release should reveal no more about the sample than is inherent in the population itself. Their example is a group of hospitals, each treating a random sample of the patients with a disease in a region: a hospital can publish information that describes the regional population without revealing which hospital's patients produced it.

The two notions look incomparable at first. Differential privacy protects only databases that differ in one record, but protects every such pair; distributional privacy can protect databases that differ in all their records, but only for typical pairs, and it tolerates a small failure probability $\beta$. §7 of the paper (p. 19) shows that distributional privacy is the stronger notion once $\beta$ is small compared with $1/n^2$. This mission formalizes that implication, Theorem 7.3.

Setting

Fix a data universe $X$ and a measurable space $R$ of outputs. In §7 a database of size $n$ is a set $D\subseteq X$ with $|D|=n$; databases are drawn without replacement, so they have no repeated elements. A mechanism $A$ assigns to each database $D$ of size $n$ the probability law $A(D)$ of its random output, a measure on $R$, and $\Pr[A(D)\in E]$ denotes $A(D)(E)$.

• Two databases $D,D'$ of size $n$ are neighbours if $D'$ is obtained from $D$ by replacing one element: $|D\setminus D'|=1$.
• $A$ is $\varepsilon$-differentially private (Definition 2.1, p. 5) if $\Pr[A(D)\in E]\le e^{\varepsilon}\Pr[A(D')\in E]$ for all neighbours $D,D'$ and all measurable events $E\subseteq R$.
• For a finite population $S\subseteq X$ with $|S|\ge n$, two $S$-neighbours $D_1,D_2$ (Definition 7.1) are drawn independently, each uniformly among the $n$-element subsets of $S$.
• A pair $(D_1,D_2)$ is good if $\Pr[A(D_1)\in E]\le e^{\varepsilon}\Pr[A(D_2)\in E]$ for all measurable $E$ simultaneously.
• $A$ is $(\varepsilon,\beta)$-distributionally private (Definition 7.2) if, for every such $S$, the $S$-neighbours form a good pair with probability at least $1-\beta$; equivalently, at most $\beta\binom{|S|}{n}^2$ ordered pairs of $n$-subsets of $S$ are bad.

The Lean development uses the same names: SetNeighbors, IsDPSet, GoodPair, badPairCount and IsDistPrivate in the namespace PrivateRelease.Distributional.

Formalization targets

Goal: Theorem 7.3

For a family of mechanisms $(A_n)_n$, one per database size, and failure probabilities $\beta_n=o(1/n^2)$:

$$n^2\beta_n\to0\ \text{ and }\ A_n\text{ is }(\varepsilon,\beta_n)\text{-distributionally private for all }n\ \Longrightarrow\ A_n\text{ is }\varepsilon\text{-differentially private for all sufficiently large }n.$$

The goal keeps the paper's asymptotic hypothesis and leaves the rate of $\beta_n$ unfixed beyond $o(1/n^2)$.

Milestone: the fixed-size statement

For a single size $n$, the threshold the paper's argument actually uses:

$$\beta<\frac{1}{(n+1)^2}\ \text{ and }\ A\text{ is }(\varepsilon,\beta)\text{-distributionally private}\ \Longrightarrow\ A\text{ is }\varepsilon\text{-differentially private on databases of size }n.$$

The goal follows from it, since $n^2\beta_n\to0$ forces $\beta_n<1/(n+1)^2$ eventually.

Significance

The result. Theorem 7.3 places distributional privacy above differential privacy: a mechanism designed for the distributional guarantee automatically inherits every consequence of differential privacy, including its composition properties and its robustness to auxiliary information about individuals. The paper complements it with a separation (Theorem 7.5), so the inclusion is strict. A footnote extends the conclusion to $t\varepsilon$-privacy for databases that differ in $t$ elements.

Formalizing it. The theorem is proved in the paper; to our knowledge it has no machine-checked proof. The value of the formalization lies in fixing the definitions. Definition 7.2 is informal about the sampling model ("drawn at random without replacement"), about whether the guarantee holds for all events at once or event by event, and about what $\beta=o(1/n^2)$ means for a mechanism defined on one database size. The proof's count "with probability $2/n^2$" is also loose: the exact probability of a given unordered pair is $2/(n+1)^2$. The mission records one precise reading of each and the theorem under it, and the definitions are reusable for further work on distributional privacy and on the paper's separation result.

Difficulty

The mathematics is short; the difficulty is in the encoding. The step that fails under a careless reading is the passage from "with probability $1-\beta$" to "with certainty": it requires the population $S$ to be finite and small (the proof takes $|S|=n+1$), so that a single pair has probability bounded below. If the guarantee is read event by event (for each $E$, most pairs satisfy the inequality for that $E$), the counting argument still applies to each event separately, but the definition is weaker than the paper's. If databases are allowed to repeat elements, the theorem is false, because distributional privacy never examines a database with repetitions while differential privacy does.

Formalization scope

• Databases are Finset X of cardinality $n$; a mechanism is A : Finset X → Measure R, and only its values on $n$-element sets matter. [DecidableEq X] is assumed for set difference.
• Neighbours replace one element ((D \ D').card = 1). The paper's literal "$|D\Delta D'|\le1$" holds for equal-size sets only when $D=D'$; the replace-one reading is the intended one.
• Events are measurable subsets of $R$; with the σ-algebra $\top$ on $R$ these are all sets.
• Only finite populations $S$ are quantified. This weakens the hypothesis of Theorem 7.3 and so makes the theorem stronger. The two draws are independent, and pairs are counted as ordered pairs.
• The asymptotic hypothesis is Tendsto (fun n => n^2 * β n) atTop (𝓝 0) and the conclusion is ∀ᶠ n in atTop; the claim for every $n$ would be false at small $n$.
• No probability-measure hypothesis is imposed: the theorem is an implication between two families of inequalities. The hypotheses are satisfiable, for instance by any constant mechanism.
• A trivializing formalization is ruled out: $\beta$ is constrained by $n^2\beta_n\to0$, since for $\beta\ge1$ distributional privacy holds for every mechanism and the implication would be false; and the bad event is "some measurable $E$ violates the inequality", not a per-event condition.
• Explicit thresholds: the paper's "$\beta=o(1/n^2)$" with its count "$2/n^2$" becomes $\beta<1/(n+1)^2$ in the fixed-size milestone; no other $O(\cdot)$ appears.
• Out of scope: Theorem 7.5 (the separation) with Definition 7.4, because its query $Q_{2/\varepsilon}$ needs $2/\varepsilon\in\mathbb N$, its databases are bit-vectors rather than sets, and "with constant probability" is never quantified.

Contributions welcome: proofs of the milestone and the goal, and the footnote's $t\varepsilon$ extension for databases differing in $t$ elements, stated as a new theorem.

Selected references

• A. Blum, K. Ligett, A. Roth, A Learning Theory Approach to Non-Interactive Database Privacy, arXiv:1109.2229v1, 2011; J. ACM 60(2), 2013. https://arxiv.org/abs/1109.2229 , https://doi.org/10.1145/2450142.2450148
• C. Dwork, F. McSherry, K. Nissim, A. Smith, Calibrating Noise to Sensitivity in Private Data Analysis, TCC 2006. https://doi.org/10.1007/11681878_14

Motivation

A data curator holds a database of $n$ records and wants to publish answers to a large family of statistical questions about it without revealing any individual record. Differential privacy (Dwork, McSherry, Nissim, Smith 2006) makes the requirement precise, and the most basic questions are counting queries: what fraction of the records satisfy a given predicate? Blum, Ligett and Roth (arXiv:1109.2229, JACM 2013) showed that a single private release can answer every query of a class $C$ to error $\alpha$ once the database has size roughly $\log|X| \cdot \mathrm{VCDIM}(C)/(\alpha^3\epsilon)$, so that the sample size depends on the class only through its VC-dimension, a quantity from learning theory.

This mission formalizes the converse in §3.1 of that paper: the dependence on the VC-dimension cannot be removed. On databases of fewer than $\mathrm{VCDIM}(C)/2$ records, every differentially private mechanism has constant error on some query of $C$. The argument is an early instance of the reconstruction attack idea of Dinur and Nissim (2003): accurate answers to many counting queries determine the database, and a mechanism that determines its input cannot be private.

Setting

Let $X$ be a set (the data universe). An input database of size $n$ is a tuple $z = (z_1,\dots,z_n) \in X^n$. A predicate is a map $\varphi : X \to \{0,1\}$, and its counting query is

$$Q_\varphi(z) = \frac{1}{n}\,\#\{i : \varphi(z_i) = 1\}.$$

A class $C$ of predicates is identified with its class of counting queries. A finite set $S \subseteq X$ is shattered by $C$ if every function $S \to \{0,1\}$ is the restriction of some $\varphi \in C$; the VC-dimension $\mathrm{VCDIM}(C) \in \mathbb N \cup \{\infty\}$ is the supremum of the sizes of shattered sets.

A mechanism $M$ maps each input $z \in X^n$ to a probability distribution $M(z)$ on an output space $O$; an output $o$ is read through an answer map $\mathrm{ans}(o, \varphi) \in \mathbb R$. Two inputs are neighbours if they differ in exactly one entry. The mechanism is $\epsilon$-differentially private if $M(z)(E) \le e^{\epsilon} M(z')(E)$ for all neighbours $z, z'$ and all measurable events $E$. It is $(\alpha,\delta)$-useful for $C$ if for every input $z$, with probability at least $1-\delta$ over $o \sim M(z)$, every query is answered to within $\alpha$:

$$\forall \varphi \in C:\quad |\mathrm{ans}(o,\varphi) - Q_\varphi(z)| \le \alpha .$$

In the paper the output is a synthetic database $\hat D$ and $\mathrm{ans}(\hat D,\varphi) = Q_\varphi(\hat D)$.

Formalization targets

Goal: Theorem 3.11 (p. 11)

There is an absolute constant $c > 0$ such that for every universe $X$, class $C$, size $n \ge 1$ with $n \le \mathrm{VCDIM}(C)/2$, $0 \le \epsilon \le 1$ and $0 < \delta \le 1/4$: every $\epsilon$-differentially private mechanism that is $(\alpha,\delta)$-useful for $C$ on databases of size $n$ satisfies

$$\alpha \ \ge\ \frac{c}{4 + 16\epsilon}.$$

Milestones

1. Lemma 3.12. For a set $S$ of size $d$ and the family $\mathcal D_S$ of its subsets of size $d/2$, and $Q_T$ the counting query of a predicate equal to the indicator of $T$ on $S$: $Q_T(T) - Q_T(T') = |T\Delta T'|/d$ for $T, T' \in \mathcal D_S$.
2. Lemma 3.13. For an $(\alpha,\delta)$-useful mechanism, a fixed procedure recovers from $M(T)$ a set $T' \in \mathcal D_S$ with $|T'\Delta T| \le 2d\alpha$, with probability at least $1-\delta$.
3. The final inequality of the proof (p. 12), with $\delta$ kept. Under the goal's hypotheses with $0 < \delta < 1$ and any $\epsilon$:

$$(1-\delta)(1-2\alpha) \ \le\ e^{\epsilon}(\delta + 2\alpha).$$

Significance

Theorem 3.11 shows that the VC-dimension term in the paper's upper bound is necessary: for a class of VC-dimension $d$, no private mechanism is accurate on databases of size below $d/2$, whatever its running time. It thereby locates the sample complexity of private query release between $\mathrm{VCDIM}(C)$ and $\mathrm{VCDIM}(C)\cdot\log|X|$ up to accuracy and privacy factors, a gap that later work on private learning and on fingerprinting codes studied in detail (Bun, Ullman, Vadhan 2014).

The theorem is proved in the paper; to the best of current knowledge it has no machine-checked proof. Formalizing it produces a checked reconstruction-attack lower bound for differential privacy, together with the corrected statement disclosed below: the printed proof drops the failure probability $\delta$ of the two reconstructions, and keeping it shows that the conclusion requires $\delta$ below $1/(1+e^{\epsilon})$, not merely "bounded away from 1". Milestone 3 records the inequality the argument actually yields.

Difficulty

The combinatorial core (Lemmas 3.12 and 3.13) is elementary. The difficulty lies in the last step, which compares the output distributions on two different inputs. The paper argues about a uniformly random $T \in \mathcal D_S$, a random element $x \in T$ and a random $y \notin T$, and the swapped set $\hat T = (T\setminus\{x\})\cup\{y\}$. Privacy applies to one fixed pair of neighbouring inputs and one fixed event, while the reconstruction guarantee only controls $|T'\Delta T|$, not whether a particular element is recovered. The "probabilities" $\Pr[x \in T']$ of the printed proof mix the mechanism's randomness with the random choice of $T$, $x$, $y$, and they are not the probability of any single event under any single $M(z)$, so the privacy inequality cannot be applied to them as written. The reconstruction event must also be measurable, which depends on the readout, and the failure probability $\delta$ must be carried through both reconstructions. A proof that sets $\delta = 0$, as the printed one does, does not prove the stated theorem.

Formalization scope

• Databases. Inputs are Fin n → X with $n \ge 1$; the empty database is excluded because every mechanism is private on it and $Q_\varphi = 0/0$ there. In the proof, a set $T \in \mathcal D_S$ is given to the mechanism as any injective listing of its elements.
• Neighbours. The paper's "$|D\Delta D'| \le 1$" for databases of equal size is read as replacing one entry (PrivLearn.Generic.Neighbors); read literally, it would make every mechanism private and the theorem false. Under this reading $T$ and $\hat T$ are neighbours, so the paper's factor $e^{2\epsilon}$ becomes $e^{\epsilon}$.
• Mechanisms. The output space is an arbitrary measurable space and answers are read through ans. Synthetic-data mechanisms are the special case $O =$ databases, so the lower bound covers a larger class of mechanisms. The hypotheses require IsProbabilityMeasure (M z) and the measurability of o ↦ ans o φ for $\varphi \in C$. Without the first, the zero measure is private; without the second, a mechanism into a trivial $\sigma$-algebra would be private and "useful".
• Ω and the range of δ. The paper writes $\alpha \ge \Omega(1/(4+16\epsilon))$ for "$0<\delta<1$ bounded away from 1 by a constant". The Lean goal quantifies one absolute constant $c > 0$ before every other binder and assumes $0 < \delta \le 1/4$. The proof gives $\alpha \ge ((1-\delta) - e^{\epsilon}\delta)/(2(1-\delta+e^{\epsilon}))$, which is positive only for $\delta < 1/(1+e^{\epsilon})$ (about $0.27$ at $\epsilon=1$). The hypotheses $\epsilon \le 1$ and $n \le \mathrm{VCDIM}(C)/2$ are the paper's, the latter written $2n \le \mathrm{VCDIM}(C)$ in $\mathbb N\cup\{\infty\}$.
• Ruled out. The statement quantifies over every mechanism satisfying the hypotheses, randomized or not, so no restriction to deterministic or constant-output mechanisms makes the bound easy. The usefulness event is weighed by a probability measure, so the zero measure cannot be "useful". The constant cannot depend on $n$, $d$, $X$ or $C$.
• Infrastructure. The development reuses the published PrivLearn.Generic.Privacy (neighbours, IsDP) and Vershynin's HighDimProb.Chaining.Shatters and vcDim. Contributions needed: subsets of shattered sets are shattered, and $2n \le \mathrm{VCDIM}(C)$ yields a shattered set of size exactly $2n$; measurability of the argmin reconstruction; the averaging/bijection argument. The first two are reusable beyond this mission.

Selected references

• A. Blum, K. Ligett, A. Roth, A Learning Theory Approach to Non-Interactive Database Privacy, arXiv:1109.2229v1 (2011); J. ACM 60(2), 2013. https://arxiv.org/abs/1109.2229 , https://doi.org/10.1145/2450142.2450148
• C. Dwork, F. McSherry, K. Nissim, A. Smith, Calibrating Noise to Sensitivity in Private Data Analysis, TCC 2006. https://doi.org/10.1007/11681878_14
• I. Dinur, K. Nissim, Revealing Information while Preserving Privacy, PODS 2003. https://doi.org/10.1145/773153.773173
• M. Bun, J. Ullman, S. Vadhan, Fingerprinting Codes and the Price of Approximate Differential Privacy, STOC 2014. https://arxiv.org/abs/1311.3158
• R. Vershynin, High-Dimensional Probability, Cambridge University Press, 2018, §8.3 (VC dimension). https://doi.org/10.1017/9781108231596

Motivation

Sums of independent random matrices appear wherever a large matrix is built from random pieces: sample covariance matrices in statistics, random sparsification and sampling in numerical linear algebra, random graphs and their Laplacians, and compressed sensing. The basic question is how far the largest eigenvalue of such a sum can stray above its typical value. For sums of independent real random variables the answer is given by the classical inequalities of Chernoff, Hoeffding and Bernstein, all derived by the Laplace transform method: bound the tail by the moment generating function, and use independence to factor the moment generating function of the sum.

Ahlswede and Winter (2002) showed that a matrix analogue of the Laplace transform method exists, and Oliveira (2010) refined the starting inequality. Tropp's paper (arXiv:1004.4389) replaced the Ahlswede–Winter decoupling step by a consequence of Lieb's concavity theorem (Lieb 1973) and obtained a single master tail bound from which matrix versions of the Gaussian-series, Chernoff, Bernstein and Azuma inequalities follow with sharp variance parameters. This mission formalizes that master bound, the first of five missions covering the paper.

Timeline:

• 1973: Lieb proves concavity of $A\mapsto \operatorname{tr}\exp(H+\log A)$ on positive-definite matrices; Epstein gives a second proof (Epstein 1973).
• 2002: Ahlswede and Winter introduce the matrix Laplace transform method, decoupling summands with the Golden–Thompson inequality.
• 2010: Oliveira's variant of the matrix Laplace transform bound.
• 2010–2012: Tropp derives the master bound for independent sums from Lieb's theorem (journal version: Found. Comput. Math. 12 (2012)); in 2011 he also derives Lieb's theorem from the joint convexity of quantum relative entropy (arXiv:1101.1070).

Setting

All matrices are $d\times d$ arrays of complex numbers with $d\ge1$. A matrix $A$ is self-adjoint (Hermitian) when $A=A^*$; it then has real eigenvalues, and $\lambda_{\max}(A)$ denotes the largest one. For a function $f:\mathbb R\to\mathbb R$ and a self-adjoint $A=Q\Lambda Q^*$ with $Q$ unitary and $\Lambda$ diagonal, $f(A):=Qf(\Lambda)Q^*$. This defines the matrix exponential $e^{A}$ of every self-adjoint matrix and the matrix logarithm $\log A$ of every positive-definite matrix, with $\log(e^A)=A$. The trace exponential is $A\mapsto\operatorname{tr}e^{A}$.

A random self-adjoint matrix is a measurable map $X$ from a probability space $(\Omega,\mathcal F,\mathbb P)$ to the self-adjoint matrices. Its expectation $\mathbb E X$ is the matrix of the expectations of its entries. A finite sequence $X_1,\dots,X_n$ is independent when the maps are jointly independent. The matrix moment generating function and matrix cumulant generating function of $X$ are

$$M_X(\theta):=\mathbb E\,e^{\theta X},\qquad \Xi_X(\theta):=\log\mathbb E\,e^{\theta X},\qquad\theta\in\mathbb R,$$

which may fail to exist for some $\theta$. In the Lean development these objects are lambdaMax, mexp, mlog, trExp and mean in the namespace MatrixTail.Master.

Formalization targets

Goal: the master tail bound (Theorem 3.6)

For independent random self-adjoint matrices $X_1,\dots,X_n$ and every $t\in\mathbb R$,

$$\mathbb P\Bigl\{\lambda_{\max}\Bigl(\sum_k X_k\Bigr)\ge t\Bigr\}\le\inf_{\theta>0}\Bigl\{e^{-\theta t}\cdot\operatorname{tr}\exp\Bigl(\sum_k\log\mathbb E\,e^{\theta X_k}\Bigr)\Bigr\}.$$

It contains no constants and no assumption beyond independence: every later inequality of the paper specializes it.

Milestones

1. Proposition 3.1 (Laplace transform method): $\mathbb P\{\lambda_{\max}(Y)\ge t\}\le\inf_{\theta>0}\{e^{-\theta t}\,\mathbb E\operatorname{tr}e^{\theta Y}\}$.
2. Theorem 3.2 (Lieb): for fixed self-adjoint $H$, $A\mapsto\operatorname{tr}\exp(H+\log A)$ is concave on the positive-definite cone.
3. Corollary 3.3: $\mathbb E\operatorname{tr}\exp(H+X)\le\operatorname{tr}\exp(H+\log\mathbb E\,e^{X})$.
4. Lemma 3.4 (subadditivity of matrix cgfs): $\mathbb E\operatorname{tr}\exp(\sum_k\theta X_k)\le\operatorname{tr}\exp(\sum_k\log\mathbb E\,e^{\theta X_k})$ for $\theta\in\mathbb R$.

Significance

The master bound reduces every tail estimate for $\lambda_{\max}$ of an independent sum to semidefinite bounds on the individual cumulant generating functions. The paper's matrix Gaussian and Rademacher series bound, matrix Chernoff inequality and matrix Bernstein inequality are each one such bound away from it, and the matrix Bernstein inequality in particular is a standard tool in randomized numerical linear algebra, matrix completion and covariance estimation. Missions II–IV of this series take the master bound as their first milestone.

All results here are proved in the literature. What remains is formalization: none of Lieb's concavity theorem, the matrix Laplace transform bound or the subadditivity of matrix cumulant generating functions is in Mathlib, and a machine-checked Lieb theorem would be reusable throughout quantum information theory (strong subadditivity of entropy, joint convexity of relative entropy).

Difficulty

The scalar argument factors $\mathbb E\exp(\sum_k\theta X_k)=\prod_k\mathbb E\,e^{\theta X_k}$, which needs $e^{a+b}=e^ae^b$. For non-commuting matrices $e^{A+B}\ne e^Ae^B$, so this step fails. The Golden–Thompson inequality $\operatorname{tr}e^{A+H}\le\operatorname{tr}(e^Ae^H)$ handles two summands but its three-matrix analogue is false, so it does not iterate. Lieb's concavity theorem is the deep input; it does not follow from elementary properties of the exponential, which is neither operator monotone nor operator convex. On the formal side, the matrix functional calculus of Mathlib carries little of the trace-function theory the statements rely on.

Formalization scope

Matrices are Matrix (Fin d) (Fin d) ℂ with [NeZero d] wherever $\lambda_{\max}$ appears; for $d=0$ the largest eigenvalue would be $0$ and the bound would fail at $t\le0$. Exponential and logarithm are Mathlib's continuous functional calculus cfc. Random matrices are measurable maps for the Borel σ-algebra on the entries, independence is iIndepFun, and P is a probability measure. Expectation is entrywise.

The paper's standing assumption that expectations exist is made explicit and only where an expectation is taken: every entry of $e^{\theta X_k}$ is integrable for the $\theta$ in question. The infimum over $\theta>0$ is stated as the bound for every $\theta>0$ at which the moment generating functions exist; since an inequality $p\le\inf_\theta F(\theta)$ is equivalent to $p\le F(\theta)$ for every $\theta$, and the paper treats a non-existent moment generating function as $+\infty$, this is exact. A real-valued infimum over $\theta$, or dropping the integrability hypotheses, would make the statements trivially true through Lean's default values ($\inf$ of an unbounded set and the integral of a non-integrable function are $0$); the formalization rules both out.

Useful infrastructure beyond this mission: trace inequalities for cfc on Hermitian matrices, monotonicity of the trace exponential in the semidefinite order, and Lieb's concavity theorem itself. Contributions of any of these as standalone lemmas are welcome.

Selected references

• J. A. Tropp, User-Friendly Tail Bounds for Sums of Random Matrices, arXiv:1004.4389v7 (2011); Found. Comput. Math. 12 (2012) 389–434. https://arxiv.org/abs/1004.4389, https://doi.org/10.1007/s10208-011-9099-z
• R. Ahlswede and A. Winter, Strong converse for identification via quantum channels, IEEE Trans. Inform. Theory 48(3) (2002) 569–579. https://arxiv.org/abs/quant-ph/0012127
• R. I. Oliveira, Sums of random Hermitian matrices and an inequality by Rudelson, Electron. Commun. Probab. 15 (2010) 203–212. https://arxiv.org/abs/1004.3821
• E. H. Lieb, Convex trace functions and the Wigner–Yanase–Dyson conjecture, Adv. Math. 11 (1973) 267–288. https://doi.org/10.1016/0001-8708(73)90011-X
• H. Epstein, Remarks on two theorems of E. Lieb, Comm. Math. Phys. 31 (1973) 317–325. https://doi.org/10.1007/BF01646492
• J. A. Tropp, From joint convexity of quantum relative entropy to a concavity theorem of Lieb, Proc. Amer. Math. Soc. 140 (2012) 1757–1760. https://arxiv.org/abs/1101.1070