On this page

GaussianAnalysisRocq · MathComp · MathComp-Analysis

A Rocq library on Gaussian measures, Gaussian comparison and concentration inequalities, and the linear algebra and probability tools they need. It is written over an arbitrary R : realType, in the style of MathComp-Analysis, so that parts of it can later be proposed to MathComp-Analysis. It does not depend on the ellipsoid fitting papers. The proofs of the two theorems in theories/ and extension/ use it at Stdlib's R.

94library files

58,531lines of Rocq

2,342lemmas and theorems

301definitions

28application files, 5,905 lines

Status. No human has reviewed the statements of the library yet, as library/README.md says; the table of main results is the place to start. Every theorem is proved: no file contains Admitted, Axiom or Parameter, and make check rejects them. MathComp's classical axioms may be used.

The seven directories

gaussian/The measurable structure and the norm of real matrices, Lebesgue measure and the standard Gaussian measure on 'rV[R]_n, marginals and Fubini, moments, Gaussian integration by parts (Stein's identity) in one and several dimensions, differentiability from continuous partial derivatives, continuity of parameter integrals, Gaussian interpolation between two covariances9 files · 3,637 lines · 156 lemmas · 10 definitions comparison/Linear images and rotation invariance, shifts, tails, moment generating functions and chi-square laws, concentration of Lipschitz functions and the Poincare inequality, Slepian, Sudakov-Fernique and Gordon comparison inequalities, Sudakov's minoration, escape through a mesh, norms of Gaussian matrices, the convex Gaussian min-max theorem, the Ornstein-Uhlenbeck semigroup and the Brascamp-Lieb inequality19 files · 12,644 lines · 439 lemmas · 47 definitions matrix/The spectral theorem for real symmetric matrices, the positive part of a symmetric matrix and whitening, operator, Frobenius and nuclear norms, nets on spheres and coverings of nuclear-norm balls, von Neumann's trace inequality and the Hoffman-Wielandt inequality, the cone of matrices of bounded condition number, its distance and support function, the maximizer of a trace-penalized quadratic on a closed convex set of matrices, effective ranks, the operator norm of sums of independent random matrices, the largest eigenvalue as the supremum of the quadratic form on the unit sphere, the orthogonal splitting of positive semidefinite matrices17 files · 7,498 lines · 410 lemmas · 47 definitions probability/Paley-Zygmund and other moment inequalities, the Lindeberg replacement method, subgaussian and subexponential variables (Hoeffding, Bernstein, Hanson-Wright), the norms of random vectors and matrices with subgaussian coordinates, the Efron-Stein inequality, product laws by rows and conditioning on coordinates, measurable choices of minimizers, symmetrization and the small-ball method, the semicircle law and the scalar variational problem of the Gaussian model, and its version over clipped profiles with its dual form, the omission form of the Efron-Stein inequality24 files · 14,080 lines · 557 lemmas · 76 definitions fourier/Characteristic functions of laws on the line and on row vectors, written without complex numbers; Levy concentration functions, Esseen's inequality and the Kolmogorov-Rogozin inequality under a second moment condition; Gaussian regularization and the bound of probabilities by the integral of the characteristic function; the vector small-ball estimate of Koehler and Sohn; the Fourier inversion theorem6 files · 5,771 lines · 196 lemmas · 21 definitions convex/Self-concordant barriers and the log-determinant barrier, minimizers of least squares objectives with a barrier, the Lindeberg replacement for barrier-regularized least squares with regular features and the removal of the barrier and of the ridge, projections onto closed convex sets and Moreau's decomposition for closed convex cones12 files · 7,573 lines · 269 lemmas · 44 definitions random_matrix/The Gaussian orthogonal ensemble: the Schwinger-Dyson equation for its moments, the operator norm, Wigner's semicircle law, and the invariance of its law under orthogonal conjugation, with the diagonal of equivariant matrix functions; the restricted isometry of matrices with independent subexponential columns (Adamczak, Litvak, Pajor and Tomczak-Jaegermann) and the norms of sparse combinations of subgaussian vectors; the trace moments and the operator norm of Gaussian matrix series, and the sharp upper edge of the GOE (its largest eigenvalue has mean at most 2 and Gaussian tails above it)7 files · 7,328 lines · 315 lemmas · 56 definitions

Classical results

Results and constructions known by a name, as library/README.md names them, with the declarations that state or define them. The table of main results lists all the others.

`gaussian/`

Gaussian integration by parts (Stein's identity), in one and several dimensionsnormal_ibp gauss_ibp gauss_ibp2
Gaussian interpolation between two covariances, and Kahane's comparison inequalitygauss_interpolation gauss_comparison
Lebesgue measure on row vectors, and the density of the standard Gaussian measurelebesgue_rV gauss_lebesgue_rV

`comparison/`

Slepian's inequalityslepian
Sudakov-Fernique inequalitysudakov_fernique
Gordon's min-max inequalitygordon
Gordon's escape through a meshgordon_escape
Sudakov's minoration and the dual Sudakov inequalitysudakov_minoration dual_sudakov
Gaussian concentration of Lipschitz functions (Tsirelson, Ibragimov, Sudakov)gauss_concentration
Gaussian Poincare inequality for Lipschitz functionsgauss_poincare_lipschitz
Cameron-Martin formulaintegral_gauss_shift
Convex Gaussian min-max theoremcgmt_lower cgmt_upper
Ornstein-Uhlenbeck semigroup and Mehler transformou mehler
Brascamp-Lieb inequality, Gaussian and Lebesgue formsgauss_brascamp_lieb brascamp_lieb

`matrix/`

Spectral theorem for real symmetric matricessymmetric_spectral
Von Neumann's trace inequality and the Hoffman-Wielandt inequalityvon_neumann_trace hoffman_wielandt
Nets of the unit ball and the unit spherenet_exists unit_sphere_net
Range duality for the nuclear normrange_duality
Orthogonal splitting of positive semidefinite matricespsd_splitting

`probability/`

Paley-Zygmund inequalitypaley_zygmund
Lindeberg's replacement principlelindeberg_replacement
Hoeffding's inequalitysubgaussian_sum
Bernstein's inequalitybernstein bernstein_sum
Hanson-Wright inequalityhanson_wright
Efron-Stein inequality, and Steele's omission formefron_stein efron_stein_omission
Gine-Zinn symmetrization and Ledoux-Talagrand contractionsymmetrization contraction
Mendelson's small-ball methodsmall_ball_method

`fourier/`

Esseen's inequalityesseen
Concentration of sums under a second moment condition (Kolmogorov-Rogozin type)conc_fun_sum
Vector small-ball estimate of Koehler and Sohnvector_small_ball
Fourier inversion on row vectorscf_rV_inversion

`convex/`

Moreau's decomposition for closed convex conesmoreau
Dikin ellipsoid of a self-concordant function (Nesterov-Nemirovskii)sc_dikin
Lindeberg replacement for barrier-regularized least squares (Theorem 2.9 of Koehler and Sohn)barrier_lindeberg_mean barrier_lindeberg_variance

`random_matrix/`

Schwinger-Dyson equation for the GOEgoe_schwinger_dyson
Wigner's semicircle law for the GOEwigner
Sharp upper edge of the GOEgoe_lambda_max_mean goe_lambda_max_tail
Restricted isometry of matrices with independent subexponential columns (Adamczak, Litvak, Pajor and Tomczak-Jaegermann)restricted_isometry
Moments of Gaussian matrix seriesgauss_mx_series_moment
Weierstrass approximation of Lipschitz functionsweierstrass_lipschitz

The vocabulary

The definitions of the library that the library and the applications use most, counted by the declarations whose statement or proof mentions them.

596 usesmxdot matrix/euclidean.vthe Frobenius inner product of A, B : 'M[R]_(m, n), \sum_i \sum_j A i j * B i j
369 usesfrobenius matrix/euclidean.vthe Frobenius norm Num.sqrt (mxdot A A) of A; the Euclidean norm when A is a row or a column vector
300 usesgauss gaussian/gauss.vthe standard Gaussian measure on 'rV[R]_n
156 usesopnorm matrix/opnorm.vthe operator norm of A, the supremum of frobenius (A *m x) over the columns x with frobenius x <= 1
121 usestuple_prod probability/lindeberg.vthe product of the probability measures mu 0, ..., mu n.-1 on n.-tuple T: the law of n independent random elements with laws mu 0, ..., mu n.-1
80 usesgoe_mx random_matrix/goe.vthe GOE matrix (A + A^T) / sqrt (2 d) of a row vector a of size d * d, A = vec_mx a
66 useslebesgue_rV gaussian/lebesgue_rV.vthe function of lebesgue_rV_rec n, with the same structure; the lemmas are stated for it
59 usesorthogonalmx matrix/euclidean.vthe square matrix M is orthogonal: M *m M^T = 1
55 usesupper_moment probability/variational.v\int[mu]_x ((x - w)_+)^k, the upper partial moment of order k at w: m(w) for k = 1, s(w) for k = 2
46 usesunif_mean probability/finite_mean.v#|T|^-1 * \sum_(x : T) f x, the mean of f : T -> R under the uniform law of the finite type T
45 usestuple_set probability/lindeberg.vthe tuple x with its coordinate i replaced by t
43 usesrmax comparison/slepian.vthe largest coordinate of the row vector z
41 usesrV_cons gaussian/gauss.vthe row vector of size n.+1 with first coordinate p.1, and then the coordinates of p.2 : 'rV_n
37 usesspec matrix/von_neumann.vthe eigenvalues of the symmetric matrix A, in decreasing order
35 usessemicircle_prob probability/semicircle_law.vthe measure with density semicircle_pdf r with respect to Lebesgue measure
31 usescf_norm fourier/charfun.vthe modulus of the characteristic function of mu at t
30 usesescape_inf comparison/escape.vinf_(x in T) |G *m x|
27 usescf_rV_norm fourier/charfun_rV.vits modulus cmod (cf_rV nu theta)
27 usesconc_fun fourier/esseen.vsup_a mu [a, a + L], the Levy concentration function
27 usesunit_ball matrix/nets.vthe closed unit ball [set x | frobenius x <= 1] of 'cV[R]_n

How the directories depend on each other

	gaussian	comparison	matrix	probability	fourier	convex	random_matrix	applications
gaussian	18	1	1
comparison	74	45	20	4		2
matrix	7	9	46	7	1	3	1
probability	8	8	11	36		4
fourier	21	11	5	6	11
convex	9	1	26	13		25
random_matrix	19	18	23	5	1		6
applications	18	1	24	9			9	43

Each cell counts the Require edges from the files of the row directory to the files of the column directory; the diagonal counts the edges inside a directory. The directories are organized by topic, not in layers: several pairs require each other in both directions, through different files.

Applications

Rocq formalizations of theorems of manuscripts of the OpenAI math collection (openai/math at revision 1581d4cbd, under the Apache License 2.0) whose proofs reuse the library GaussianAnalysis of library/. The logical root is GaussianApplications. See the overview of the applications.

Target	Manuscript (family)	Statement files	Library files	Proof folder
T1. Gaussian matrix series	Pointwise convergence of fourfold ergodic averages for mixing transformations (154), Lemma 4.2	`MatrixSeriesStatement.v`	`random_matrix/matrix_series.v`
T2. Tensor packing in finite dimensions	the same (154), Theorem 4.1	`TensorPackingStatement.v`	`matrix/tensor_packing.v`
T3. Sharp upper edge of the GOE	Cutoff throughout the high-temperature Sherrington-Kirkpatrick phase (227), appendix "Uniform spectral and entropy estimates"	`GoeEdgeStatement.v`	`matrix/lambda_max.v`, `random_matrix/goe_edge.v`
T4. Spectral gap of the SK heat-bath dynamics for beta < 1/2	the same (227)	`SKGapDefinitions.v`, `SKGapStatement.v`	`matrix/spectral_gap.v`, `probability/finite_gap.v`, `random_matrix/goe_entries.v`	`SKGap/`
T5. Orthogonal splitting of positive semidefinite matrices	Exponential PSD rank of positively shifted matching matrices (126), lemma "Orthogonal splitting"	`PsdSplittingStatement.v`	`matrix/psd_splitting.v`
T6. Sign/Gaussian comparison for the Ising perceptron pressure	The free energy of the Ising random perceptron (222), Theorem ext:sign	`PerceptronSignDefinitions.v`, `PerceptronSignStatement.v`	`probability/rademacher_lindeberg.v`, `probability/log_partition.v`	`Perceptron/`
T7. Capped variance for random k-SAT	A limiting satisfiability threshold for every fixed clause size (235), Proposition "Polynomial concentration"	`SatVarianceDefinitions.v`, `SatVarianceStatement.v`	`probability/finite_mean.v`; `probability/efron_stein_omission.v`, the general form of the manuscript's lemma 'Deletion variance bound', is not used by the proof	`RandomSAT/`

Conventions

Reals. Every result is stated for an arbitrary R : realType, or a weaker structure such as realFieldType when that is enough. No file requires Stdlib's Reals, Lra, Psatz or MathComp's Rstruct: make check rejects them in library/.
Vocabulary. MathComp's: row and column vectors 'rV[R]_n and 'cV[R]_n, matrices 'M[R]_(m, n), `|x|, Num.sqrt, expR, ln, n%:R, \sum, and the measures, integrals and probability of MathComp-Analysis (measure, lebesgue_integral, probability, normal_distribution). No lists of coordinates.
Tactics. From mathcomp Require Import arithmetic_tactic provides lra, nra and psatz on any real field; ring_tactic and field_tactic provide ring and field.
Names and style. MathComp's naming conventions for lemmas, ssreflect proof style, lowercase file names, and a documentation header at the top of each file in MathComp's format: each definition and notation with a one-line reading.
Axioms. No Admitted, Axiom or Parameter. MathComp's classical axioms (boolp) may be used.

Reading the signatures

The notations of MathComp and MathComp-Analysis that fill the statements.

Notation	Meaning
`'rV[R]_n`, `'cV[R]_n`, `'M[R]_(m, n)`	row vectors, column vectors and m × n matrices with entries in R; `x 0 i` and `A i j` are entries
`'I_n`	the natural numbers below n (MathComp's ordinals), used as indices
`n.+1`	n + 1, for natural numbers
`A m B`, `A^T`, `a : A`	matrix product, transpose, product by a scalar
`\sum_(i < n) F i`, `\prod_(i < n) F i`	finite sums and products over the indices below n
`\|x\|	the absolute value of a real; on matrices, MathComp's norm, the largest absolute value of an entry (the Euclidean norm is `frobenius`)
`\bar R`, `x%:E`	the extended reals over R, and the real x seen as an extended real
`(e)%E`, `(e)%R`, `(n)%N`	e read with the operations of the extended reals, of rings, or of natural numbers
`[set: T]`, `[set x \| P x]`, f @^-1` A	the full set of T, the set of the x with P x, and the preimage of A under f
`\int[mu]_x f x`	the integral of f against the measure mu, with values in the extended reals
`measurable_fun D f`, `mu.-integrable D f`	f is measurable on D; f is integrable against mu on D
`forall {R : realType} [n : nat], ...`	in a printed signature, the arguments in braces and brackets are implicit: Rocq infers them from the others

How to read this documentation

Pages. Each file of the library has a page: its documentation header, the rows of the table of main results that concern it, then its declarations in source order, inside their sections. A section shows the Context, Variable and Hypothesis lines that its declarations may use.
Signatures. The code block of a lemma is its type as Rocq prints it with About, after the sections are closed: it lists every argument, implicit ones in braces (maximal) or brackets (non-maximal), and the hypotheses. The statement as written in the source, inside its section, is one click away. A definition shows its type and its body.
Links. In the source statements, every name links to its declaration through the .glob files that Rocq writes when it compiles, so the links are exact. In the printed signatures, the names that the source statement uses are linked the same way; other names are linked when they are unique in the library. Names of MathComp and MathComp-Analysis show their full path on hover.
Local declarations. Let definitions live only inside their section, and Local lemmas are not imported with their file. They are hidden by default; a checkbox on each page shows them.
Used by. Under each declaration, the list of the declarations of both packages whose statement or proof refers to it.
Written for this documentation. The guide at the top of each directory page was written from the sources and the README, then checked against the Rocq statements by an independent reading. The classical results on this page are named as in the README rows. Everything else is extracted from the sources mechanically.

Building

Tested with:

Package	Version
OCaml	5.3.0
Rocq (`rocq-core`)	9.1.1
Rocq Stdlib (`rocq-stdlib`)	9.0.0
Hierarchy Builder	1.10.3
MathComp	2.6.0
MathComp finmap	2.2.4
MathComp-Analysis, with `reals-stdlib` and `analysis-stdlib`	1.16.0

To install them in a new opam switch:

opam switch create ellipsoid-fitting ocaml-base-compiler.5.3.0
opam repo add rocq-released https://rocq-prover.org/opam/released
opam repo add coq-released https://coq.inria.fr/opam/released
opam install --deps-only ./rocq-ellipsoid-fitting.opam

Then, from the repository root:

make check ROCQ_SWITCH=ellipsoid-fitting JOBS=8   # the switch created above
make check ROCQ_SWITCH= JOBS=8                    # the rocq on your PATH

Generated from commit 9046883 (tag phase12) of the ellipsoid fitting repository. Signatures are printed by Rocq 9.1.1; links in the source statements come from the compiled .glob files. The source links open the files on GitHub at this commit, in the now-public repository.