On this page
Sharp upper edge of the GOE: the theorem
Imports 2 library modules and 13 external
External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, mathcomp.algebra.matrix, mathcomp.classical.boolp, mathcomp.classical.classical_sets, mathcomp.reals.reals, mathcomp.analysis.ereal, mathcomp.analysis.measure_theory.measure, mathcomp.analysis.lebesgue_measure, mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral, mathcomp.analysis.probability_theory.probability
Target T3 of phase 12. goe_edge_theorem proves goe_edge_statement of GoeEdgeStatement.v: for d >= 1, a of law gauss (d * d) and W = goe_mx a, the map a |-> lambda_max W is measurable and integrable, E lambda_max W <= 2, 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), for every t >= 0. Each conjunct is a result of library/random_matrix/goe_edge.v (goe_lambda_max_mean, goe_lambda_max_tail, goe_lambda_maxN_tail, goe_opnorm_edge_tail), whose header describes the proof.
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' (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 statement is at beta = 1 and has the sharp tail constant d / 4, where the TeX and the Lean modules have a constant with pi^2.
Main results
| Results | Statement |
|---|---|
Proves goe_edge_statement (T3): for every R : realType, d >= 1, a of law gauss (d * d) and W = goe_mx a, the map a |-> lambda_max W is measurable and integrable, E lambda_max W <= 2, 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), for every t >= 0. From library/. |
Declarations1 exported
Proves goe_edge_statement (T3): for every R : realType, d >= 1, a of law gauss (d * d) and W = goe_mx a, the map a |-> lambda_max W is measurable and integrable, E lambda_max W <= 2, 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), for every t >= 0. From library/.
Statement as written in the source
Theorem goe_edge_theorem : goe_edge_statement.