On this page

GaussianApplicationsapplicationsSKGapSpectral

The spectral gap of the heat-bath dynamics from a bound on its square

GaussianApplications.SKGap.Spectralapplications/SKGap/Spectral.v124 lines8 lemmas and theoremssource

Imports 3 library modules and 9 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.reals.reals, mathcomp.algebra.ring_tactic, mathcomp.algebra.field_tactic

Imported by 1

GaussianApplications.SKGap.Poincare

Part of target T4 of phase 12 (AGENTS.md, section Phase 12), the spectral gap of the heat-bath dynamics of the Sherrington-Kirkpatrick model for beta < 1/2: the spectral step of item T4a. A Rocq formalization of the credited argument of the end of the proof of the proposition 'Gap and covariance under scaled interactions and fields' (rcut:prop:uniform-gap) of 'Cutoff throughout the high-temperature Sherrington-Kirkpatrick phase' (family 227 of the OpenAI math collection, revision 1581d4cbd, file appendices/entropy.tex). It follows the TeX, not a Lean module of the collection.

Take any matrix A and field theta, the Ising law nu of SKGapDefinitions.v, the projections D_i = I - E_i of SKGap/Ising.v and L = ising_gen A theta = sum_i D_i, the heat-bath generator with rate one at every site, up to sign. In L^2(nu), L is linear (ising_gen_lin) and self-adjoint (ising_gen_sym, from ising_dproj_adj), <f, L f>_nu is the Dirichlet form (ising_gen_form), hence nonnegative, and the kernel of L is the constants (ising_gen_ker, from ising_dirichlet_eq0). So wpoincare_from_square of probability/finite_gap.v applies: if k E(g) <= nu[(L g)^2] for every g, then k Var_nu(f) <= E(f) for every f (ising_gap_from_square). The manuscript applies the bound to a nonconstant eigenfunction of L; the library uses the spectral theorem for the matrix of L.

Main results

Results	Statement
ising_gap_from_squareising_gen_formising_gen_symising_gen_ker	The spectral step of T4 (item T4a). For any matrix `A`, field `theta` and real `k`: if `k E(g) <= nu[(L g)^2]` for every `g`, where `nu` is the Ising law, `E = ising_dirichlet A theta` and `L = ising_gen A theta = sum_i D_i`, then `k Var_nu(f) <= E(f)` for every `f`. In `L^2(nu)`, `L` is linear and self-adjoint, `<f, L f>_nu = E(f)`, and the kernel of `L` is the constants, so `wpoincare_from_square` of `probability/finite_gap.v` applies. `R`, `n`, `A`, `theta` and `k` are implicit.

Declarations8 exported

sectionising_gap

Variables (R : realType) (n : nat) (A : 'M[R]_n) (theta : 'cV[R]_n).
Local Notation cube := {ffun 'I_n -> bool}.
Local Notation nu := (ising_mass A theta).
Local Notation E := (ising_mean A theta).
Local Notation D := (ising_dproj A theta).
Local Notation L := (ising_gen A theta).
Implicit Types (f g : cube -> R).

lemma wdot_ising source, line 52

forall [R : realType] [n : nat] (A : 'M_n) (theta : 'cV_n) (f g : {ffun 'I_n -> bool} -> R),
wdot (ising_mass A theta) f g =
ising_mean A theta (fun x : {ffun 'I_n -> bool} => f x * g x)

The inner product of L^2(nu).

Statement as written in the source

Lemma wdot_ising f g : wdot nu f g = E (fun x => f x * g x).

Used by 2 declarations in 1 file

this file: ising_gen_dot, ising_gap_from_square

lemma ising_gen_lin source, line 59

forall [R : realType] [n : nat] (A : 'M_n) (theta : 'cV_n) (a : R)
  (f g : {ffun 'I_n -> bool} -> R) (x : {ffun 'I_n -> bool}),
ising_gen A theta (fun y : {ffun 'I_n -> bool} => a * f y + g y) x =
a * ising_gen A theta f x + ising_gen A theta g x

The generator is linear and self-adjoint, its form is the Dirichlet form and its kernel is the constants.

Statement as written in the source

Lemma ising_gen_lin (a : R) f g x :
  L (fun y => a * f y + g y) x = a * L f x + L g x.

Used by 1 declaration in 1 file

this file: ising_gap_from_square

lemma ising_gen_dot source, line 68

forall [R : realType] [n : nat] (A : 'M_n) (theta : 'cV_n) (f g : {ffun 'I_n -> bool} -> R),
wdot (ising_mass A theta) f (ising_gen A theta g) =
\sum_i
   ising_mean A theta
     (fun x : {ffun 'I_n -> bool} => ising_dproj A theta i f x * ising_dproj A theta i g x)

Statement as written in the source

Lemma ising_gen_dot f g :
  wdot nu f (L g) = \sum_i E (fun x => D i f x * D i g x).

Used by 2 declarations in 1 file

this file: ising_gen_form, ising_gen_sym

lemma ising_gen_form main result source, line 78

forall [R : realType] [n : nat] (A : 'M_n) (theta : 'cV_n) (f : {ffun 'I_n -> bool} -> R),
wdot (ising_mass A theta) f (ising_gen A theta f) = ising_dirichlet A theta f

Main result

Stated in the README together with ising_gap_from_square.

Statement as written in the source

Lemma ising_gen_form f : wdot nu f (L f) = ising_dirichlet A theta f.

Used by 3 declarations in 1 file

this file: ising_gen_ge0, ising_gen_ker, ising_gap_from_square

lemma ising_gen_sym main result source, line 84

forall [R : realType] [n : nat] (A : 'M_n) (theta : 'cV_n) (f g : {ffun 'I_n -> bool} -> R),
wdot (ising_mass A theta) f (ising_gen A theta g) =
wdot (ising_mass A theta) (ising_gen A theta f) g

Main result

Stated in the README together with ising_gap_from_square.

Statement as written in the source

Lemma ising_gen_sym f g : wdot nu f (L g) = wdot nu (L f) g.

Used by 1 declaration in 1 file

this file: ising_gap_from_square

lemma ising_gen_ge0 source, line 90

forall [R : realType] [n : nat] (A : 'M_n) (theta : 'cV_n) (f : {ffun 'I_n -> bool} -> R),
0 <= wdot (ising_mass A theta) f (ising_gen A theta f)

Statement as written in the source

Lemma ising_gen_ge0 f : 0 <= wdot nu f (L f).

Used by 1 declaration in 1 file

this file: ising_gap_from_square

lemma ising_gen_ker main result source, line 93

forall [R : realType] [n : nat] (A : 'M_n) (theta : 'cV_n) (g : {ffun 'I_n -> bool} -> R),
(forall x : {ffun 'I_n -> bool}, ising_gen A theta g x = 0) <->
(forall x y : {ffun 'I_n -> bool}, g x = g y)

Main result

Stated in the README together with ising_gap_from_square.

Statement as written in the source

Lemma ising_gen_ker g : (forall x, L g x = 0) <-> (forall x y, g x = g y).

Used by 1 declaration in 1 file

this file: ising_gap_from_square

theorem ising_gap_from_square main result source, line 107

forall [R : realType] [n : nat] [A : 'M_n] [theta : 'cV_n] [k : R],
(forall g : {ffun 'I_n -> bool} -> R,
 k * ising_dirichlet A theta g <=
 ising_mean A theta (fun x : {ffun 'I_n -> bool} => ising_gen A theta g x ^+ 2)) ->
forall f : {ffun 'I_n -> bool} -> R, k * ising_var A theta f <= ising_dirichlet A theta f

The interface of the assembly of T4: a bound of the Dirichlet form by the squared norm of the generator gives the spectral gap.

Main result, as the README states it

The spectral step of T4 (item T4a). For any matrix A, field theta and real k: if k E(g) <= nu[(L g)^2] for every g, where nu is the Ising law, E = ising_dirichlet A theta and L = ising_gen A theta = sum_i D_i, then k Var_nu(f) <= E(f) for every f. In L^2(nu), L is linear and self-adjoint, <f, L f>_nu = E(f), and the kernel of L is the constants, so wpoincare_from_square of probability/finite_gap.v applies. R, n, A, theta and k are implicit.

Statement as written in the source

Theorem ising_gap_from_square (k : R) :
  (forall g, k * ising_dirichlet A theta g <=
     E (fun x => ising_gen A theta g x ^+ 2)) ->
  forall f, k * ising_var A theta f <= ising_dirichlet A theta f.

Used by 1 declaration in 1 file

GaussianApplications.SKGap.Poincare: gap_from_bounds

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.