The upper edge of the Gaussian orthogonal ensemble

Let a have law gauss (d * d) with d >= 1, and let W = goe_mx a be the GOE matrix of random_matrix/goe.v: its entries W_ij, i <= j, are independent and centered, of variance 1 / d off the diagonal and 2 / d on it. Its largest eigenvalue lambda_max W (matrix/lambda_max.v) has mean at most 2 (goe_lambda_max_mean), the right edge of the semicircle law (wigner.v). For every t >= 0, P(lambda_max W >= 2 + t) <= exp (- d t^2 / 4) (goe_lambda_max_tail), and the same holds for - W (goe_lambda_maxN_tail), so P(opnorm W >= 2 + t) <= 2 exp (- d t^2 / 4) (goe_opnorm_edge_tail). The file does not bound E opnorm W by 2: goe.v bounds it by 2 sqrt 2.

The proof compares Gaussian processes. For a unit column x, x^T W x = sqrt (2 / d) <a, mxvec (x x^T)> (goe_mx_form), a linear function of a. For a finite family x_0, ..., x_k of unit columns, the process x_j^T W x_j is the row a *m goe_form_mx xs. Its increments have variance (4 / d) (1 - <x_j, x_l>^2) <= (8 / d) (1 - <x_j, x_l>) (goe_form_incr_var), the increment variance of (2 / sqrt d) <g, x_j> for g of law gauss d, diagonal entries included. The Sudakov-Fernique inequality (sudakov_fernique) and E |g| <= sqrt d (gauss_frobenius_mean) give E max_j x_j^T W x_j <= 2 (goe_form_max_mean). On an eps-net of the unit sphere, lambda_max A <= max_j x_j^T A x_j + 2 eps opnorm A (lambda_max_net_le), and E opnorm W <= 2 sqrt 2 (goe_opnorm_mean), so letting eps tend to 0 bounds the mean. The map a |-> lambda_max W is sqrt (2 / d)-Lipschitz (goe_lambda_max_lipschitz, from frobenius_goe_mx), hence measurable and integrable, and Gaussian concentration with the sharp constant (gauss_concentration_upper_tail) gives the tails. The matrix - W is goe_mx (- a) (goe_mxN), and gauss (d * d) is invariant under a |-> - a (integral_gauss_opp).

This file is a Rocq formalization of the credited argument of 'Cutoff throughout the high-temperature Sherrington-Kirkpatrick phase' (family 227 of the OpenAI math collection, revision 1581d4cbd): the lemma 'Gaussian concentration and comparison' and the first paragraph of the proof of the proposition 'Good disorder', in the appendix 'Uniform spectral and entropy estimates' (appendices/entropy.tex). The Lean modules that follow the same argument, in lean/OAI/Probability/SKRatio of the collection:

Lean: goe_expected_top (Matrices/DiagonalTMemLp.lean, line 93)

Lean: goe_norm_tail (Matrices/GoeMatrixQuadCoeff.lean, line 115)

The manuscript, the Lean modules and this file differ in three ways. The manuscript takes beta W with beta < 1/2; here beta = 1. It compares the suprema over the unit sphere as continuous processes on a compact set; here the comparison is on finite families, and a net passes to the sphere. Its concentration inequality, from the argument of Maurey and Pisier, bounds the moment generating function of F - E F by exp (pi^2 D^2 s^2 / 8) for F D-Lipschitz, which gives exp (- d t^2 / pi^2) for the upper tail of lambda_max W; the Lean modules use the same inequality and bound P(opnorm W > 2 + t) by 2 exp (- d t^2 / pi^2). Here the sharp constant of gauss_concentration gives exp (- d t^2 / 4) and 2 exp (- d t^2 / 4), for the non-strict inequalities.