GaussianAnalysisRocq library documentation
Main resultsGlossary
On this page
GaussianApplicationsapplicationsSKGapPoincare

The spectral gap and the covariance under good disorder

GaussianApplications.SKGap.Poincareapplications/SKGap/Poincare.v422 lines21 lemmas and theorems, 3 definitionssource
Imports 9 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.algebra.sesquilinear, mathcomp.classical.boolp, mathcomp.reals.reals, mathcomp.analysis.sequences, mathcomp.analysis.exp, mathcomp.algebra.ring_tactic, mathcomp.algebra.field_tactic, mathcomp.algebra.arithmetic_tactic

Imported by 1

Part of target T4 of phase 12 (AGENTS.md, section Phase 12). A Rocq formalization 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 Lean counterpart:

Lean: exists_uniform_gap_tolerance (SKRatio/Variational/UniformGap.lean)

  • ising_gen_sq_ge, the sum of the two-spin inequality (ising_two_spin of TwoSpin.v) over the ordered pairs: with T = (tanh A_ij), T2 = (tanh^2 A_ij), opnorm T <= M, 2 opnorm T2 <= M and sum_j |tanh A_ij|^3 <= rho for every i, and |tanh A_ij| <= 1/1000: nu[(sum_i D_i f)^2] >= (1 - M - 140000 rho) E(f). The two quadratic forms are bounded by operator norms, with v_i^2 (1 + m_i^2) <= v_i, as in the manuscript.
  • ising_cov_from_gap: from k Var_nu(f) <= E(f) for every f, opnorm Cov_nu(x) <= 1 / k, by the linear functions f(x) = <c, x>, for which d_i f = c_i (half_diff_form).
  • sk_gap_deterministic: for 0 <= beta < 1/2, 0 < delta <= sk_gap_tol beta = min (1/2000) ((1 - 2 beta) / 400000), J symmetric with zero diagonal, opnorm J <= 2 beta + delta, sum_j J_ij^2 <= beta^2 + delta for every row, |J_ij| <= delta, and 0 <= s <= 1: kappa Var_nu(f) <= E(f) for every f and opnorm Cov_nu(x) <= 1 / kappa, with kappa = (1 - 2 beta) / 2 and nu the Ising law of s J with any field. It combines ising_gen_sq_ge, the bounds |tanh u| <= |u| and |tanh u - u| <= |u|^3 with the Schur test (opnorm_row_sum of library/matrix/spectral_gap.v), and the spectral step ising_gap_from_square of Spectral.v. The manuscript states the gap for all large n on its good-disorder event; here the tolerance is explicit and works for every n.
  • sk_coupling_sym, sk_coupling_diag: the SK coupling is symmetric with zero diagonal.

Main results

ResultsStatement
ising_gen_sq_geising_cov_from_gapsk_gap_deterministic
For A symmetric with zero diagonal, |tanh A_ij| <= 1/1000, opnorm (tanh A_ij) <= M, 2 opnorm (tanh^2 A_ij) <= M and sum_j |tanh A_ij|^3 <= rho for every row: nu[(sum_i D_i f)^2] >= (1 - M - 140000 rho) E(f). For k > 0, from k Var_nu(f) <= E(f) for all f: opnorm Cov_nu(x) <= 1 / k. The deterministic gap: for 0 <= beta < 1/2, 0 < delta <= sk_gap_tol beta = min (1/2000) ((1 - 2 beta)/400000), J symmetric with zero diagonal, opnorm J <= 2 beta + delta, sum_j J_ij^2 <= beta^2 + delta and |J_ij| <= delta, and 0 <= s <= 1: kappa Var_nu(f) <= E(f) for every f and opnorm Cov_nu(x) <= 1 / kappa, kappa = (1 - 2 beta)/2, for the Ising law of s J and any field.

Declarations24 exported

lemma, theoremdefinitioninstancelocal
sectionpair_sum
Variables (R : realType) (n : nat) (A : 'M[R]_n) (theta : 'cV[R]_n).
Hypothesis Asym : A \is symmetricmx.
Hypothesis Adiag : forall k, A k k = 0.
Local Notation cube := {ffun 'I_n -> bool}.
Local Notation E := (ising_mean A theta).
Local Notation m := (ising_cond_mean A theta).
Local Notation v := (ising_cond_var A theta).
Local Notation D := (ising_dproj A theta).
Implicit Types (x : cube) (i j : 'I_n) (f : cube -> R).
definition sk_tanh_mx source, line 63
Type
forall [R : realType] [n : nat], 'M_n -> 'M_n
Definition
Definition sk_tanh_mx : 'M[R]_n := \matrix_(i, j) sk_tanh (A i j).
Used by 3 declarations in 1 file
definition sk_tanh2_mx source, line 64
Type
forall [R : realType] [n : nat], 'M_n -> 'M_n
Definition
Definition sk_tanh2_mx : 'M[R]_n := \matrix_(i, j) sk_tanh (A i j) ^+ 2.
Used by 3 declarations in 1 file
lemma sk_tanh_diag source, line 66 
forall [R : realType] [n : nat] [A : 'M_n],
(forall k : 'I_n, A k k = 0) -> forall i : 'I_n, sk_tanh (A i i) = 0
Statement as written in the source
Lemma sk_tanh_diag i : sk_tanh (A i i) = 0.
Used by 1 declaration in 1 file
lemma A_sym source, line 69 
forall [R : realType] [n : nat] [A : 'M_n],
A \is symmetricmx -> forall i j : 'I_n, A j i = A i j
Statement as written in the source
Lemma A_sym i j : A j i = A i j.
Used by 2 declarations in 1 file
lemma ising_gen_sq_expand source, line 72 
forall [R : realType] [n : nat] (A : 'M_n) (theta : 'cV_n) (f : {ffun 'I_n -> bool} -> R),
ising_mean A theta (fun x : {ffun 'I_n -> bool} => ising_gen A theta f x ^+ 2) =
\sum_i
   (ising_mean A theta
      (fun x : {ffun 'I_n -> bool} => ising_cond_var A theta i x * half_diff i f x ^+ 2) +
    \sum_(j | j != i)
       ising_mean A theta
         (fun x : {ffun 'I_n -> bool} =>
          ising_dproj A theta i f x * ising_dproj A theta j f x))
Statement as written in the source
Lemma ising_gen_sq_expand f :
  E (fun x => ising_gen A theta f x ^+ 2) =
  \sum_i (E (fun x => v i x * half_diff i f x ^+ 2) +
          \sum_(j | j != i) E (fun x => D i f x * D j f x)).
Used by 1 declaration in 1 file
lemma pair_quad_le source, line 89 
forall [R : realType] [n : nat] [A : 'M_n] (theta : 'cV_n) (f : {ffun 'I_n -> bool} -> R)
  (x : {ffun 'I_n -> bool}) [M : R],
opnorm (sk_tanh_mx A) <= M ->
2 * opnorm (sk_tanh2_mx A) <= M ->
\sum_i
   \sum_j
      (sk_tanh (A i j) +
       2 * sk_tanh (A i j) ^+ 2 * ising_cond_mean A theta i x * ising_cond_mean A theta j x) *
      ising_cond_var A theta i x * ising_cond_var A theta j x * 
      half_diff i f x * half_diff j f x <=
M * \sum_i ising_cond_var A theta i x * half_diff i f x ^+ 2

The quadratic forms of the two-spin inequality, summed over the pairs.

Statement as written in the source
Lemma pair_quad_le f x (M : R) :
  opnorm sk_tanh_mx <= M -> 2 * opnorm sk_tanh2_mx <= M ->
  \sum_i \sum_j (sk_tanh (A i j) + 2 * sk_tanh (A i j) ^+ 2 * m i x * m j x) *
     v i x * v j x * half_diff i f x * half_diff j f x <=
  M * \sum_i v i x * half_diff i f x ^+ 2.
Used by 1 declaration in 1 file
lemma ising_gen_sq_ge main result source, line 131 
forall [R : realType] [n : nat] [A : 'M_n] (theta : 'cV_n),
A \is symmetricmx ->
(forall k : 'I_n, A k k = 0) ->
forall (f : {ffun 'I_n -> bool} -> R) [M rho : R],
(forall i j : 'I_n, `|sk_tanh (A i j)| <= 1 / 10 ^+ 3) ->
opnorm (sk_tanh_mx A) <= M ->
2 * opnorm (sk_tanh2_mx A) <= M ->
(forall i : 'I_n, \sum_j `|sk_tanh (A i j)| ^+ 3 <= rho) ->
(1 - M - 14 * 10 ^+ 4 * rho) * ising_dirichlet A theta f <=
ising_mean A theta (fun x : {ffun 'I_n -> bool} => ising_gen A theta f x ^+ 2)
Main result, as the README states it

For A symmetric with zero diagonal, |tanh A_ij| <= 1/1000, opnorm (tanh A_ij) <= M, 2 opnorm (tanh^2 A_ij) <= M and sum_j |tanh A_ij|^3 <= rho for every row: nu[(sum_i D_i f)^2] >= (1 - M - 140000 rho) E(f). For k > 0, from k Var_nu(f) <= E(f) for all f: opnorm Cov_nu(x) <= 1 / k. The deterministic gap: for 0 <= beta < 1/2, 0 < delta <= sk_gap_tol beta = min (1/2000) ((1 - 2 beta)/400000), J symmetric with zero diagonal, opnorm J <= 2 beta + delta, sum_j J_ij^2 <= beta^2 + delta and |J_ij| <= delta, and 0 <= s <= 1: kappa Var_nu(f) <= E(f) for every f and opnorm Cov_nu(x) <= 1 / kappa, kappa = (1 - 2 beta)/2, for the Ising law of s J and any field.

Statement as written in the source
Lemma ising_gen_sq_ge f (M rho : R) :
  (forall i j, `|sk_tanh (A i j)| <= 1 / 10 ^+ 3) ->
  opnorm sk_tanh_mx <= M -> 2 * opnorm sk_tanh2_mx <= M ->
  (forall i, \sum_j `|sk_tanh (A i j)| ^+ 3 <= rho) ->
  (1 - M - 14 * 10 ^+ 4 * rho) * ising_dirichlet A theta f <=
  E (fun x => ising_gen A theta f x ^+ 2).
Used by 1 declaration in 1 file
sectioncovariance
Variables (R : realType) (n : nat) (A : 'M[R]_n) (theta : 'cV[R]_n).
Local Notation cube := {ffun 'I_n -> bool}.
Local Notation E := (ising_mean A theta).
Implicit Types (x : cube) (c : 'cV[R]_n).
lemma ising_var_alt source, line 204 
forall [R : realType] [n : nat] (A : 'M_n) (theta : 'cV_n) (f : {ffun 'I_n -> bool} -> R),
ising_var A theta f =
ising_mean A theta (fun x : {ffun 'I_n -> bool} => f x ^+ 2) - ising_mean A theta f ^+ 2
Statement as written in the source
Lemma ising_var_alt (f : cube -> R) :
  ising_var A theta f = E (fun x => f x ^+ 2) - E f ^+ 2.
Used by 1 declaration in 1 file
lemma spin_form_sum source, line 214 
forall [R : realType] [n : nat] (c : 'cV_n) (x : {ffun 'I_n -> bool}),
mxdot c (spin_vec x) = \sum_k c k 0 * spin (x k)
Statement as written in the source
Lemma spin_form_sum c x : mxdot c (spin_vec x) = \sum_k c k 0 * spin (x k).
Used by 2 declarations in 1 file
lemma half_diff_form source, line 217 
forall [R : realType] [n : nat] (c : 'cV_n) (i : 'I_n) (x : {ffun 'I_n -> bool}),
half_diff i (fun y : {ffun 'I_n -> bool} => mxdot c (spin_vec y)) x = c i 0
Statement as written in the source
Lemma half_diff_form c i x :
  half_diff i (fun y => mxdot c (spin_vec y)) x = c i 0.
Used by 1 declaration in 1 file
lemma ising_dirichlet_form source, line 228 
forall [R : realType] [n : nat] (A : 'M_n) (theta c : 'cV_n),
ising_dirichlet A theta (fun y : {ffun 'I_n -> bool} => mxdot c (spin_vec y)) <= mxdot c c
Statement as written in the source
Lemma ising_dirichlet_form c :
  ising_dirichlet A theta (fun y => mxdot c (spin_vec y)) <= mxdot c c.
Used by 1 declaration in 1 file
lemma ising_cov_form source, line 238 
forall [R : realType] [n : nat] (A : 'M_n) (theta c : 'cV_n),
mxdot c (ising_cov A theta *m c) =
ising_var A theta (fun y : {ffun 'I_n -> bool} => mxdot c (spin_vec y))
Statement as written in the source
Lemma ising_cov_form c :
  mxdot c (ising_cov A theta *m c) = ising_var A theta (fun y => mxdot c (spin_vec y)).
Used by 1 declaration in 1 file
lemma ising_cov_sym source, line 262 
forall [R : realType] [n : nat] (A : 'M_n) (theta : 'cV_n),
ising_cov A theta \is symmetricmx
Statement as written in the source
Lemma ising_cov_sym : ising_cov A theta \is symmetricmx.
Used by 1 declaration in 1 file
lemma ising_var_ge0 source, line 270 
forall [R : realType] [n : nat] (A : 'M_n) (theta : 'cV_n) (f : {ffun 'I_n -> bool} -> R),
0 <= ising_var A theta f
Statement as written in the source
Lemma ising_var_ge0 f : 0 <= ising_var A theta f.
Used by 1 declaration in 1 file
lemma ising_cov_from_gap main result source, line 273 
forall [R : realType] [n : nat] [A : 'M_n] [theta : 'cV_n] [k : R],
0 < k ->
(forall f : {ffun 'I_n -> bool} -> R, k * ising_var A theta f <= ising_dirichlet A theta f) ->
opnorm (ising_cov A theta) <= k^-1
Main result

Stated in the README together with ising_gen_sq_ge.

Statement as written in the source
Lemma ising_cov_from_gap (k : R) : 0 < k ->
  (forall f, k * ising_var A theta f <= ising_dirichlet A theta f) ->
  opnorm (ising_cov A theta) <= k^-1.
Used by 1 declaration in 1 file
sectiondeterministic_gap
Variables (R : realType) (n : nat).
Implicit Types (beta delta s : R) (J A : 'M[R]_n).
lemma pow_le_norm source, line 293 
forall [R : realType] (k : nat) [x y : R], `|x| <= `|y| -> `|x| ^+ k <= `|y| ^+ k
Statement as written in the source
Lemma pow_le_norm (k : nat) (x y : R) : `|x| <= `|y| -> `|x| ^+ k <= `|y| ^+ k.
Used by 2 declarations in 1 file
lemma sqr_le_abs source, line 296 
forall [R : realType] [x y : R], `|x| <= `|y| -> x ^+ 2 <= y ^+ 2
Statement as written in the source
Lemma sqr_le_abs (x y : R) : `|x| <= `|y| -> x ^+ 2 <= y ^+ 2.
Used by 2 declarations in 1 file
definition sk_gap_tol source, line 302
Type
forall [R : realType], R -> R
Definition
Definition sk_gap_tol beta : R := Num.min (1 / (2 * 10 ^+ 3)) ((1 - 2 * beta) / (4 * 10 ^+ 5)).
Used by 4 declarations in 2 files
lemma sk_gap_tol_gt0 source, line 304 
forall [R : realType] [beta : R], beta < 1 / 2 -> 0 < sk_gap_tol beta
Statement as written in the source
Lemma sk_gap_tol_gt0 beta : beta < 1 / 2 -> 0 < sk_gap_tol beta.
Used by 1 declaration in 1 file
lemma gap_from_bounds source, line 307 
forall [R : realType] [n : nat] [beta delta : R] [A : 'M_n] (theta : 'cV_n),
0 <= beta ->
beta < 1 / 2 ->
0 < delta ->
delta <= sk_gap_tol beta ->
A \is symmetricmx ->
(forall i : 'I_n, A i i = 0) ->
opnorm A <= 2 * beta + delta ->
(forall i : 'I_n, \sum_j A i j ^+ 2 <= beta ^+ 2 + delta) ->
(forall i j : 'I_n, `|A i j| <= delta) ->
forall f : {ffun 'I_n -> bool} -> R,
(1 - 2 * beta) / 2 * ising_var A theta f <= ising_dirichlet A theta f
Statement as written in the source
Lemma gap_from_bounds beta delta A (theta : 'cV[R]_n) :
  0 <= beta -> beta < 1 / 2 -> 0 < delta -> delta <= sk_gap_tol beta ->
  A \is symmetricmx -> (forall i, A i i = 0) ->
  opnorm A <= 2 * beta + delta ->
  (forall i, \sum_j A i j ^+ 2 <= beta ^+ 2 + delta) ->
  (forall i j, `|A i j| <= delta) ->
  forall f, (1 - 2 * beta) / 2 * ising_var A theta f <= ising_dirichlet A theta f.
Used by 1 declaration in 1 file
lemma scaled_bounds source, line 363 
forall [R : realType] [n : nat] [beta delta : R] [J : 'M_n] [s : R],
J \is symmetricmx ->
(forall i : 'I_n, J i i = 0) ->
opnorm J <= 2 * beta + delta ->
(forall i : 'I_n, \sum_j J i j ^+ 2 <= beta ^+ 2 + delta) ->
(forall i j : 'I_n, `|J i j| <= delta) ->
0 <= s ->
s <= 1 ->
[/\ s *: J \is symmetricmx, forall i : 'I_n, (s *: J) i i = 0,
    opnorm (s *: J) <= 2 * beta + delta,
    forall i : 'I_n, \sum_j (s *: J) i j ^+ 2 <= beta ^+ 2 + delta
  & forall i j : 'I_n, `|(s *: J) i j| <= delta]
Statement as written in the source
Lemma scaled_bounds beta delta J s :
  J \is symmetricmx -> (forall i, J i i = 0) ->
  opnorm J <= 2 * beta + delta ->
  (forall i, \sum_j J i j ^+ 2 <= beta ^+ 2 + delta) ->
  (forall i j, `|J i j| <= delta) ->
  0 <= s -> s <= 1 ->
  [/\ s *: J \is symmetricmx, (forall i, (s *: J) i i = 0),
      opnorm (s *: J) <= 2 * beta + delta,
      (forall i, \sum_j (s *: J) i j ^+ 2 <= beta ^+ 2 + delta) &
      (forall i j, `|(s *: J) i j| <= delta)].
Used by 1 declaration in 1 file
theorem sk_gap_deterministic main result source, line 388 
forall [R : realType] [n : nat] [beta delta : R] [J : 'M_n] [s : R] (theta : 'cV_n),
0 <= beta ->
beta < 1 / 2 ->
0 < delta ->
delta <= sk_gap_tol beta ->
J \is symmetricmx ->
(forall i : 'I_n, J i i = 0) ->
opnorm J <= 2 * beta + delta ->
(forall i : 'I_n, \sum_j J i j ^+ 2 <= beta ^+ 2 + delta) ->
(forall i j : 'I_n, `|J i j| <= delta) ->
0 <= s ->
s <= 1 ->
(forall f : {ffun 'I_n -> bool} -> R,
 (1 - 2 * beta) / 2 * ising_var (s *: J) theta f <= ising_dirichlet (s *: J) theta f) /\
opnorm (ising_cov (s *: J) theta) <= ((1 - 2 * beta) / 2)^-1
Main result

Stated in the README together with ising_gen_sq_ge.

Statement as written in the source
Theorem sk_gap_deterministic beta delta J s (theta : 'cV[R]_n) :
  0 <= beta -> beta < 1 / 2 -> 0 < delta -> delta <= sk_gap_tol beta ->
  J \is symmetricmx -> (forall i, J i i = 0) ->
  opnorm J <= 2 * beta + delta ->
  (forall i, \sum_j J i j ^+ 2 <= beta ^+ 2 + delta) ->
  (forall i j, `|J i j| <= delta) ->
  0 <= s -> s <= 1 ->
  (forall f, (1 - 2 * beta) / 2 * ising_var (s *: J) theta f <=
             ising_dirichlet (s *: J) theta f) /\
  opnorm (ising_cov (s *: J) theta) <= ((1 - 2 * beta) / 2)^-1.
Used by 1 declaration in 1 file
sectionsk_coupling_facts
Variable R : realType.
lemma sk_coupling_sym source, line 411 
forall [R : realType] [n : nat] (beta : R) (a : 'rV_(n * n)),
sk_coupling beta a \is symmetricmx
Statement as written in the source
Lemma sk_coupling_sym n (beta : R) (a : 'rV[R]_(n * n)) :
  sk_coupling beta a \is symmetricmx.
Used by 1 declaration in 1 file
lemma sk_coupling_diag source, line 418 
forall [R : realType] [n : nat] (beta : R) (a : 'rV_(n * n)) (i : 'I_n),
sk_coupling beta a i i = 0
Statement as written in the source
Lemma sk_coupling_diag n (beta : R) (a : 'rV[R]_(n * n)) i :
  sk_coupling beta a i i = 0.
Used by 1 declaration in 1 file
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.