On this page
Two bounds for real symmetric matrices
Imports 3 library modules and 10 external
- GaussianAnalysis.matrix.euclidean
- GaussianAnalysis.matrix.real_spectral
- GaussianAnalysis.matrix.opnorm
External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, mathcomp.algebra.matrix, mathcomp.algebra.sesquilinear, mathcomp.reals.reals, mathcomp.algebra.ring_tactic, mathcomp.algebra.field_tactic, mathcomp.algebra.arithmetic_tactic
- psd_square_gap, a gap from the square: if B is symmetric and positive semidefinite and k x^T B x <= |B x|^2 for every column x, then k |x|^2 <= x^T B x for every x orthogonal to the kernel of B. In an eigenbasis of B (symmetric_spectral) the hypothesis says that every eigenvalue is 0 or at least k.
- opnorm_row_sum, the Schur test for symmetric matrices: if B is symmetric, rho >= 0 and sum_j |B_ij| <= rho for every row i, then opnorm B <= rho.
- mulmx_col_mxdot and mxdot_mulmx_sum write (P x)_i and x^T B x as sums.
This file is a Rocq formalization, in general form, of two steps of the credited argument of the proposition 'Gap and covariance under scaled interactions and fields' of 'Cutoff throughout the high-temperature Sherrington-Kirkpatrick phase' (family 227 of the OpenAI math collection, revision 1581d4cbd, appendices/entropy.tex): the row-sum bound for the operator norm of a symmetric matrix, and the gap read from the inequality |A f|^2 >= kappa <f, A f>. Target T4 of phase 12 (AGENTS.md, section Phase 12) uses both. The file follows no Lean module.
Main results
| Results | Statement |
|---|---|
A gap from the square: for B symmetric and positive semidefinite with k x^T B x <= |B x|^2 for every column x, k |x|^2 <= x^T B x for every x orthogonal to the kernel of B; in an eigenbasis, every eigenvalue is 0 or at least k. Used by target T4 of phase 12 for the spectral gap of the heat-bath dynamics. | |
The Schur test for symmetric matrices: for B symmetric, rho >= 0 and sum_j |B_ij| <= rho for every row i, opnorm B <= rho. |
Declarations4 exported
Variable R : realType.
forall [R : realType] [n : nat] (P : 'M_n) (x : 'cV_n) (i : 'I_n), (P *m x) i 0 = mxdot (row i P)^T x
Statement as written in the source
Lemma mulmx_col_mxdot n (P : 'M[R]_n) (x : 'cV[R]_n) i : (P *m x) i 0 = mxdot (row i P)^T x.
Used by 1 declaration in 1 file
- this file: psd_square_gap
forall [R : realType] [n : nat] [B : 'M_n] [k : R] [x : 'cV_n], B \is symmetricmx -> (forall y : 'cV_n, 0 <= mxdot y (B *m y)) -> (forall y : 'cV_n, k * mxdot y (B *m y) <= mxdot (B *m y) (B *m y)) -> (forall y : 'cV_n, B *m y = 0 -> mxdot y x = 0) -> k * mxdot x x <= mxdot x (B *m x)
A gap from the square: for B symmetric and positive semidefinite with k x^T B x <= |B x|^2 for every column x, k |x|^2 <= x^T B x for every x orthogonal to the kernel of B; in an eigenbasis, every eigenvalue is 0 or at least k. Used by target T4 of phase 12 for the spectral gap of the heat-bath dynamics.
Statement as written in the source
Used by 1 declaration in 1 file
- GaussianAnalysis.probability.finite_gap: wgap_from_square
forall [R : realType] [n : nat] (B : 'M_n) (x : 'cV_n), mxdot x (B *m x) = \sum_i \sum_j x i 0 * B i j * x j 0
Statement as written in the source
Lemma mxdot_mulmx_sum n (B : 'M[R]_n) (x : 'cV[R]_n) : mxdot x (B *m x) = \sum_i \sum_j x i 0 * B i j * x j 0.
Used by 3 declarations in 2 files
- this file: opnorm_row_sum
- GaussianApplications.SKGap.Poincare: pair_quad_le, ising_cov_form
forall [R : realType] [n : nat] [B : 'M_n] [rho : R], B \is symmetricmx -> 0 <= rho -> (forall i : 'I_n, \sum_j `|B i j| <= rho) -> opnorm B <= rho
The Schur test for symmetric matrices: for B symmetric, rho >= 0 and sum_j |B_ij| <= rho for every row i, opnorm B <= rho.
Statement as written in the source
Lemma opnorm_row_sum n (B : 'M[R]_n) (rho : R) : B \is symmetricmx -> 0 <= rho -> (forall i, \sum_j `|B i j| <= rho) -> opnorm B <= rho.
Used by 1 declaration in 1 file
- GaussianApplications.SKGap.Poincare: gap_from_bounds