GaussianApplications

This directory, with logical root GaussianApplications, formalizes seven theorems, T1 to T7, from five manuscripts of the OpenAI math collection (openai/math at revision 1581d4cbd, families 126, 154, 222, 227 and 235): Gaussian matrix series, tensor packing, the GOE edge, the spectral gap of the SK model, orthogonal splitting of positive semidefinite matrices, the Ising perceptron and random k-SAT. Each header cites its manuscript and, after the marker Lean:, any Lean module it follows.

Everything is over an arbitrary R : realType and requires only MathComp and library/, which holds the general mathematics; this directory holds the statements and the parts specific to a model.

Each target has frozen statement files, XStatement.v and, where needed, XDefinitions.v, and a theorem file XTheorem.v. T1, T2, T3 and T5 follow from library theorems; T4, T6 and T7 have proof folders.

Reading order

1. MatrixSeriesStatement.v: matrix_series_statement, the statement of T1.
2. MatrixSeriesTheorem.v: proves T1 from random_matrix/matrix_series.v.
3. TensorPackingStatement.v: tensor_packing_statement, the statement of T2.
4. TensorPackingTheorem.v: proves T2 from matrix/tensor_packing.v.
5. GoeEdgeStatement.v: goe_edge_statement, the statement of T3.
6. GoeEdgeTheorem.v: proves T3 from random_matrix/goe_edge.v.
7. PsdSplittingStatement.v: psd_splitting_statement, the statement of T5.
8. PsdSplittingTheorem.v: proves T5 from matrix/psd_splitting.v.
9. SKGapDefinitions.v: the Ising law, its Dirichlet form and covariance, and the SK coupling.
10. SKGapStatement.v: sk_gap_statement, the statement of T4.
11. SKGap/Ising.v: conditional expectations given the other spins, and the weights of two spins.
12. SKGap/Disorder.v: the good-disorder event and its probability.
13. SKGap/Spectral.v: the gap from a bound on the square of the generator.
14. SKGap/TwoSpin.v: the uniform two-spin inequality.
15. SKGap/Poincare.v: the gap and the covariance bound under good disorder.
16. SKGapTheorem.v: proves T4.
17. PerceptronSignDefinitions.v: the pressure, its Gaussian and sign means, and the potentials.
18. PerceptronSignStatement.v: perceptron_sign_statement, the statement of T6.
19. Perceptron/Pressure.v: derivatives of the pressure and the comparison with an explicit constant.
20. PerceptronSignTheorem.v: proves T6.
21. SatVarianceDefinitions.v: clauses, the capped satisfiable prefix length and its variance.
22. SatVarianceStatement.v: sat_variance_statement, the statement of T7.
23. RandomSAT/Model.v: solution sets, the lifetime of a clause sequence, and the first variable of a clause.
24. RandomSAT/Pivotal.v: the variance of the lifetime by a recursion over the clauses.
25. RandomSAT/Replacement.v: forced variables, the killing probability, and replacing a shorter clause.
26. RandomSAT/Forcing.v: integrated forcing of the first variable.
27. RandomSAT/Variance.v: the explicit variance bound.
28. SatVarianceTheorem.v: proves T7.

Core definitions

• lambda_max, goe_mx (library/matrix/lambda_max.v, library/random_matrix/goe.v): the supremum of x^T A x over unit columns x, and the GOE matrix (A + A^T) / sqrt (2 d) with A = vec_mx a.
• ising_weight, ising_mass, ising_mean, ising_var (SKGapDefinitions.v): for a matrix A and a field theta, the weight exp (x^T A x / 2 + <theta, x>) of a spin configuration x, the normalized law nu, its mean and variance.
• half_diff, ising_cond_mean, ising_cond_var, ising_dirichlet (SKGapDefinitions.v): the half-difference d_i f, the conditional mean m_i of the spin i given the others, v_i = 1 - m_i^2, and the Dirichlet form E(f) = sum_i nu[v_i (d_i f)^2].
• ising_cov, sk_coupling (SKGapDefinitions.v): the covariance matrix of the spins, and J = beta (W - Diag W) with W = goe_mx a.
• ising_dproj, ising_gen (SKGap/Ising.v): D_i = I - E_i, with E_i the conditional expectation given the spins outside i, and L = sum_i D_i.
• sk_good_disorder (SKGap/Disorder.v): the a such that J = sk_coupling beta a has opnorm J <= 2 beta + delta, sum_j J_ij^2 <= beta^2 + delta for every i, and |J_ij| <= delta.
• perceptron_pressure, gauss_pressure, sign_pressure, bounded_C3 (PerceptronSignDefinitions.v): p_N(G, f) = (1/N) ln (2^(-N) sum_x exp (sum_mu f ((G x)_mu / sqrt N))) for patterns G in 'M[R]_(M, N), its means under Gaussian and uniform sign patterns, and the potentials f with three derivatives, f''' continuous, |f| <= B0, |f'| <= B1, |f''| <= B2 and |f'''| <= B3.
• sat_prefix_len, sat_capped_var (SatVarianceDefinitions.v): the largest m <= M such that the first m clauses of a tuple of M proper signed k-clauses are satisfiable together, and its variance for M = 2^(k+1) n independent uniform clauses on n variables.

Main results

T1, Gaussian matrix series. matrix_series_theorem: for symmetric H_1, ..., H_r in 'M[R]_n, S = sum_j H_j H_j, g of law gauss r and q >= 1, E tr (sum_j g_j H_j)^(2q) <= (2q - 1)!! opnorm S^(q-1) tr S (gauss_mx_series_moment). For B_1, ..., B_r in 'M[R]_(m, p) and q >= 1, E opnorm (sum_j g_j B_j) <= ((2q - 1)!! sigma^(2(q-1)) tau)^(1/(2q)), with sigma^2 = max (opnorm (sum_j B_j B_j^T), opnorm (sum_j B_j^T B_j)) and tau = 2 tr (sum_j B_j B_j^T) (gauss_mx_series_opnorm); and E opnorm (sum_j g_j B_j) <= 5 d^(1/4) sqrt (ln (2 + d)) for every real d >= 1 with sigma^2 <= sqrt d and tau <= 2 d (gauss_mx_series_opnorm_log; the statement asks only for some C > 0 in place of 5).

T2, tensor packing. tensor_packing_theorem: for x_a and y_a, a < m, in the unit balls of 'rV[R]_n1 and 'rV[R]_n2, relations Gx and Gy on 'I_m with at most L successors at each vertex containing every pair a != b with |<x_a, x_b>| > eta, respectively |<y_a, y_b>| > eta, Frobenius-orthonormal A_1, ..., A_r in 'M[R]_(n1, n2) with r <= d for an integer d >= 1, 0 < eps <= 1 and 0 <= eta <= eps^2 / 10^4, at most 30000 (1 + L) / eps^2 exp (30000 eps^(-2) sqrt d ln (2 + d)) indices a have sum_k (x_a A_k y_a^T)^2 >= eps^2.

T3, GOE edge. goe_edge_theorem: for d >= 1, a of law gauss (d * d) and W = goe_mx a, a |-> lambda_max W is measurable and integrable, E lambda_max W <= 2, and for every t >= 0, P(lambda_max W >= 2 + t) and P(lambda_max (- W) >= 2 + t) are at most exp (- d t^2 / 4) and P(opnorm W >= 2 + t) <= 2 exp (- d t^2 / 4).

T5, orthogonal splitting. psd_splitting_theorem: for L >= 1 and positive semidefinite A_1, ..., A_L in 'M[R]_n, there are orthogonal projections P_1, ..., P_L, possibly zero, with P_s P_t = 0 for s != t, sum_s P_s = 1 and sum_z sum_(s != z) |P_s A_z P_s|_F^2 <= 2^(L-1) sum_z sum_(z' != z) tr (A_z A_z').

T4, SK spectral gap. sk_gap_theorem: for 0 <= beta < 1/2 and kappa = (1 - 2 beta) / 2, there are measurable sets E_n of 'rV[R]_(n * n) such that, for every eps > 0, gauss (n * n) (E_n) >= 1 - eps for all large n, and for a in E_n, s in [0, 1] and every field theta, the Ising law nu of s (sk_coupling beta a) and theta satisfies kappa Var_nu(f) <= E(f) for every f and opnorm (ising_cov) <= 1 / kappa. The events are sk_good_disorder n beta (sk_gap_tol beta) (sk_good_disorder_prob, sk_gap_deterministic). The key inequality is ising_two_spin: for A symmetric with zero diagonal, i != j and t = tanh A_ij with |t| <= 1/1000, nu[D_i f D_j f] >= - nu[(t + 2 t^2 m_i m_j) v_i v_j d_i f d_j f] - 70000 |t|^3 (nu[v_i (d_i f)^2] + nu[v_j (d_j f)^2]).

T6, perceptron pressure. perceptron_sign_theorem: for bounds B0, ..., B3 and C = 1 + (|B3| + 6 |B1| |B2| + 6 |B1|^3) / 2, for every f with bounded_C3 f B0 B1 B2 B3, every M and N >= 1, g |-> p_N(vec_mx g, f) is integrable against gauss (M * N) and |sign_pressure M N f - gauss_pressure M N f| <= C M N^(-3/2).

T7, random k-SAT. sat_variance_theorem: for k >= 3 there is C > 0 with sat_capped_var R n k <= C n^(1 + 2/k) for every n >= k + 1; sat_variance_bound_explicit gives C = 8 4^(k+1) k (3 k + 2^(k+2)). On the way, sat_prefix_lenE identifies the capped prefix length with the lifetime (life) of the set of all assignments, and by killE_forced one uniform k-clause empties a nonempty set with b forced variables (forced) with probability C(b, k) / (C(n, k) 2^k).

How the proofs go

• T1: Gaussian integration by parts and a trace inequality give E tr X^(2q+2) <= (2q + 1) opnorm S E tr X^(2q) for symmetric H_j; rectangular matrices go through the symmetric dilation.
• T2: spectral cuts at sqrt d, coverings, Sudakov's minoration and the last bound of T1.
• T3: the Sudakov-Fernique inequality on finite families of unit vectors and a net give E lambda_max W <= 2; lambda_max W is sqrt (2 / d)-Lipschitz in a, and Gaussian concentration gives the tails, with a sharper constant than the pi^2 of the TeX and the Lean modules.
• T5: the spectral projection of A - B onto its nonnegative eigenspaces splits two matrices, then an induction on L relative to an orthogonal projection.
• T4: SKGap/Disorder.v bounds four failure events with goe_opnorm_edge_tail and Gaussian and chi-square tails. SKGap/TwoSpin.v bounds the remainder in t by a real polynomial certificate (ts_certificate, ts_coef_bound) instead of the manuscript's complex Cauchy estimate. Summing the two-spin inequality over pairs bounds nu[(L f)^2] below by a multiple of E(f) (ising_gen_sq_ge), and the Schur test (opnorm_row_sum) controls the multiple under good disorder; since L is self-adjoint with the constants as kernel, wpoincare_from_square gives the gap.
• T6: each entry of G enters one coordinate of G x, so log_partition_derive3 bounds the third derivative in each entry by (B3 + 6 B1 B2 + 6 B1^3) / (N^2 sqrt N), and rademacher_gauss_lindeberg replaces the M N entries one at a time (perceptron_sign_compare); the continuity of f''' is not used.
• T7 follows the route of the Lean development. The law of total variance for the first clause bounds the variance of the lifetime by 2 m times a sum of mean truncated killing probabilities min(M q, 1) (life_var_le_occ), where the manuscript omits one clause. Each is at most a multiple of the fraction of forced variables (trunc_le_forced), whose mean is the probability that the first variable is forced (forced_frac_head); integrated_head_forcing bounds the sum of these probabilities, through kill_replacement.

Connections

The directory requires modules of gaussian/, matrix/, random_matrix/ and probability/, and comparison/gauss_smoothing.v; nothing of convex/ or fourier/. No module of library/, extension/ or theories/ requires it. Only the seven axiom checks of check/, such as check/SKGapAssumptions.v, require its statement and theorem files.