GaussianAnalysisRocq library documentation
Main resultsGlossary
On this page
GaussianApplicationsapplicationsSKGapIsing

The Ising law on the cube and its conditional expectations

GaussianApplications.SKGap.Isingapplications/SKGap/Ising.v595 lines66 lemmas and theorems, 6 definitionssource
Imports 3 library modules and 20 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.classical.classical_sets, mathcomp.classical.functions, mathcomp.algebra.interval, mathcomp.reals.reals, mathcomp.analysis.topology_theory.topology, mathcomp.analysis.normedtype_theory.normedtype, mathcomp.analysis.sequences, mathcomp.analysis.derive, mathcomp.analysis.realfun, mathcomp.analysis.exp, mathcomp.algebra.ring_tactic, mathcomp.algebra.field_tactic, mathcomp.algebra.arithmetic_tactic

Imported by 3

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. 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, appendices/entropy.tex, subsection 'A two-spin estimate and a uniform gap'). The objects are those of the frozen applications/SKGapDefinitions.v. The file follows the manuscript. In the Lean modules of the collection, the pair law is the product of the two names of the first line below, and v_i is the name of the second line:

Lean: pairBaseMass, pairDensity (SKRatio/Calculus/TwoSpin.lean)

Lean: conditionalVariance (SKRatio/Calculus/PlusSpin.lean)

  • Spin flips: spin_set and its algebra, the involution spin_flip, sum_pair2 (a sum over the cube is half the sum over the pairs x^(i,+), x^(i,-)), and cube_const (a function invariant under every spin_set is constant).
  • sk_tanh and sk_cosh, with expR_spin: exp (b u) = cosh u (1 + b tanh u) for a spin b, and, by monotonicity (MathComp-Analysis ger0_derive1_ndecry), |tanh u| <= |u| and |tanh u - u| <= |u|^3 (sk_tanh_norm_le, sk_tanh_sub_le).
  • For a matrix A and a field theta: the weights are positive and the masses sum to one; ising_mean is linear and monotone; the conditional expectation ising_cexp i given the spins outside i and the projection ising_dproj i = I - E_i satisfy D_i f = (x_i - m_i) d_i f (ising_dproj_eq), nu[(D_i f)^2] = nu[v_i (d_i f)^2] (ising_energy) and nu[g D_i f] = nu[D_i g D_i f] (ising_dproj_adj). The Dirichlet form is the sum of the energies, and it vanishes only on constants (ising_dirichlet_eq0). ising_gen f = sum_i D_i f is minus the generator of the heat-bath dynamics with rate one at every site.
  • ising_weight_block: for A symmetric with zero diagonal and i != j, the weights of the four configurations of the spins i and j with the other spins fixed are K (1 + a x)(1 + b y)(1 + t x y), with K > 0, |a|, |b| < 1 and t = tanh A_ij: the pair law of the manuscript.

Main results

ResultsStatement
ising_dproj_eqising_energyising_dproj_adjising_dirichlet_eq0ising_weight_blocksk_tanh_sub_le
For the Ising law nu of a matrix A and a field theta on {-1, 1}^n (the definitions of T4), the conditional expectation E_i given the spins outside i and D_i = I - E_i satisfy D_i f = (x_i - m_i) d_i f, nu[(D_i f)^2] = nu[v_i (d_i f)^2] and nu[g D_i f] = nu[D_i g D_i f]; the Dirichlet form vanishes only on the constants; ising_gen f = sum_i D_i f. For A symmetric with zero diagonal and i != j, the weights of the four configurations of the spins i and j, the other spins fixed, are K (1 + a x)(1 + b y)(1 + t x y) with K > 0, |a|, |b| < 1 and t = tanh A_ij. |tanh u| <= |u| and |tanh u - u| <= |u|^3.

Declarations72 exported

lemma, theoremdefinitioninstancelocal
Arguments spin {R} b.
Arguments spin_vec {R n} x.
sectionspin_flip
Variable n : nat.
Implicit Types (x : {ffun 'I_n -> bool}) (i j : 'I_n) (b c : bool).
lemma spin_setE source, line 64 
forall [n : nat] (x : {ffun 'I_n -> bool}) (i : 'I_n) (b : bool) (j : 'I_n),
spin_set x i b j = (if j == i then b else x j)
Statement as written in the source
Lemma spin_setE x i b j : spin_set x i b j = if j == i then b else x j.
lemma spin_set_id source, line 67 
forall [n : nat] (x : {ffun 'I_n -> bool}) (i : 'I_n), spin_set x i (x i) = x
Statement as written in the source
Lemma spin_set_id x i : spin_set x i (x i) = x.
Used by 3 declarations in 1 file
lemma spin_set_val source, line 70 
forall [n : nat] [x : {ffun 'I_n -> bool}] [i : 'I_n] [b : bool],
x i = b -> spin_set x i b = x
Statement as written in the source
Lemma spin_set_val x i b : x i = b -> spin_set x i b = x.
Used by 1 declaration in 1 file
lemma spin_setK source, line 73 
forall [n : nat] (x : {ffun 'I_n -> bool}) (i : 'I_n) (b c : bool),
spin_set (spin_set x i b) i c = spin_set x i c
Statement as written in the source
Lemma spin_setK x i b c : spin_set (spin_set x i b) i c = spin_set x i c.
Used by 8 declarations in 2 files
lemma spin_set_same source, line 76 
forall [n : nat] (x : {ffun 'I_n -> bool}) (i : 'I_n) (b : bool), spin_set x i b i = b
Statement as written in the source
Lemma spin_set_same x i b : spin_set x i b i = b.
Used by 5 declarations in 3 files
lemma spin_set_other source, line 79 
forall [n : nat] (x : {ffun 'I_n -> bool}) [i j : 'I_n] (b : bool),
j != i -> spin_set x i b j = x j
Statement as written in the source
Lemma spin_set_other x i j b : j != i -> spin_set x i b j = x j.
Used by 2 declarations in 2 files
lemma spin_setC source, line 82 
forall [n : nat] (x : {ffun 'I_n -> bool}) [i j : 'I_n] (b c : bool),
i != j -> spin_set (spin_set x i b) j c = spin_set (spin_set x j c) i b
Statement as written in the source
Lemma spin_setC x i j b c : i != j ->
  spin_set (spin_set x i b) j c = spin_set (spin_set x j c) i b.
Used by 2 declarations in 1 file
definition spin_flip source, line 90
Type
forall [n : nat], {ffun 'I_n -> bool} -> 'I_n -> {ffun 'I_n -> bool}
Definition
Definition spin_flip x i := spin_set x i (~~ x i).
Used by 3 declarations in 1 file
lemma spin_flipK source, line 92 
forall [n : nat] (x : {ffun 'I_n -> bool}) (i : 'I_n), spin_flip (spin_flip x i) i = x
Statement as written in the source
Lemma spin_flipK x i : spin_flip (spin_flip x i) i = x.
Used by 1 declaration in 1 file
lemma sum_flip source, line 95 
forall [n : nat] [V : GRing.Nmodule.Exports.nmodType] (i : 'I_n)
  (G : {ffun 'I_n -> bool} -> V),
\sum_x G x = \sum_x G (spin_flip x i)
Statement as written in the source
Lemma sum_flip (V : nmodType) i (G : {ffun 'I_n -> bool} -> V) :
  \sum_x G x = \sum_x G (spin_flip x i).
Used by 1 declaration in 1 file
lemma sum_pair2 source, line 99 
forall [n : nat] [R : nzRingType] (i : 'I_n) (G : {ffun 'I_n -> bool} -> R),
\sum_x (G (spin_set x i true) + G (spin_set x i false)) = 2 * \sum_x G x
Statement as written in the source
Lemma sum_pair2 (R : ringType) i (G : {ffun 'I_n -> bool} -> R) :
  \sum_x (G (spin_set x i true) + G (spin_set x i false)) = 2 * \sum_x G x.
Used by 2 declarations in 2 files
lemma cube_const source, line 107 
forall [n : nat] [T : Type] [f : {ffun 'I_n -> bool} -> T],
(forall (x : {ffun 'I_n -> bool}) (i : 'I_n) (b : bool), f (spin_set x i b) = f x) ->
forall x y : {ffun 'I_n -> bool}, f x = f y
Statement as written in the source
Lemma cube_const (T : Type) (f : {ffun 'I_n -> bool} -> T) :
  (forall x i b, f (spin_set x i b) = f x) -> forall x y, f x = f y.
Used by 1 declaration in 1 file
sectionspin_values
Variable R : realType.
lemma spin_sqr source, line 131 
forall (R : realType) (b : bool), spin b ^+ 2 = 1
Statement as written in the source
Lemma spin_sqr b : spin b ^+ 2 = 1 :> R.
lemma spin_norm source, line 134 
forall (R : realType) (b : bool), `|spin b| = 1
Statement as written in the source
Lemma spin_norm b : `|spin b| = 1 :> R.
Used by 4 declarations in 1 file
lemma spin_mul source, line 137 
forall (R : realType) (b c : bool), spin b * spin c = spin (b == c)
Statement as written in the source
Lemma spin_mul b c : spin b * spin c = spin (b == c) :> R.
Used by 1 declaration in 1 file
sectionsk_tanh
Local Open Scope classical_set_scope.
Variable R : realType.
Implicit Types u : R.
definition sk_cosh source, line 147
Type
forall [R : realType], R -> R
Definition
Definition sk_cosh u : R := (expR u + expR (- u)) / 2.
Used by 3 declarations in 1 file
definition sk_tanh source, line 149
Type
forall [R : realType], R -> R
Definition
Definition sk_tanh u : R := (expR u - expR (- u)) / (expR u + expR (- u)).
Used by 18 declarations in 3 files
lemma sk_cosh_den source, line 151 
forall [R : realType] (u : R), 0 < expR u + expR (- u)
Statement as written in the source
Lemma sk_cosh_den u : 0 < expR u + expR (- u).
Used by 8 declarations in 1 file
lemma sk_cosh_gt0 source, line 154 
forall [R : realType] (u : R), 0 < sk_cosh u
Statement as written in the source
Lemma sk_cosh_gt0 u : 0 < sk_cosh u.
Used by 1 declaration in 1 file
lemma sk_tanh_lt1 source, line 157 
forall [R : realType] (u : R), `|sk_tanh u| < 1
Statement as written in the source
Lemma sk_tanh_lt1 u : `|sk_tanh u| < 1.
Used by 1 declaration in 1 file
lemma sk_tanh0 source, line 164 
forall R : realType, sk_tanh 0 = 0
Statement as written in the source
Lemma sk_tanh0 : sk_tanh 0 = 0.
Used by 1 declaration in 1 file
lemma sk_tanhN source, line 167 
forall [R : realType] (u : R), sk_tanh (- u) = - sk_tanh u
Statement as written in the source
Lemma sk_tanhN u : sk_tanh (- u) = - sk_tanh u.
Used by 2 declarations in 1 file
lemma expR_spin source, line 174 
forall [R : realType] (u : R) (b : bool),
expR (spin b * u) = sk_cosh u * (1 + spin b * sk_tanh u)
Statement as written in the source
Lemma expR_spin u b : expR (spin b * u) = sk_cosh u * (1 + spin b * sk_tanh u).
Used by 1 declaration in 1 file
lemma is_derive_expRN' source, line 180 
forall [R : realType] (z : R), is_derive z 1 (fun z0 : R => expR (- z0)) (- expR (- z))
Statement as written in the source
Lemma is_derive_expRN' (z : R) :
  is_derive z 1 (fun z : R => expR (- z)) (- expR (- z)).
Used by 2 declarations in 1 file
lemma sinh_le_mul_cosh source, line 190 
forall [R : realType] [u : R], 0 <= u -> expR u - expR (- u) <= u * (expR u + expR (- u))

sinh z <= z cosh z for z >= 0, by monotonicity.

Statement as written in the source
Lemma sinh_le_mul_cosh u : 0 <= u ->
  expR u - expR (- u) <= u * (expR u + expR (- u)).
Used by 2 declarations in 1 file
lemma sk_tanh_ge0 source, line 215 
forall [R : realType] [u : R], 0 <= u -> 0 <= sk_tanh u
Statement as written in the source
Lemma sk_tanh_ge0 u : 0 <= u -> 0 <= sk_tanh u.
Used by 1 declaration in 1 file
lemma sk_tanh_le source, line 221 
forall [R : realType] [u : R], 0 <= u -> sk_tanh u <= u
Statement as written in the source
Lemma sk_tanh_le u : 0 <= u -> sk_tanh u <= u.
Used by 2 declarations in 1 file
lemma cubic_le_sinh source, line 229 
forall [R : realType] [u : R],
0 <= u -> (u - u ^+ 3) * (expR u + expR (- u)) <= expR u - expR (- u)

(u - u^3) cosh u <= sinh u for u >= 0, by monotonicity.

Statement as written in the source
Lemma cubic_le_sinh u : 0 <= u ->
  (u - u ^+ 3) * (expR u + expR (- u)) <= expR u - expR (- u).
Used by 1 declaration in 1 file
lemma sk_tanh_cubic source, line 274 
forall [R : realType] [u : R], 0 <= u -> u - u ^+ 3 <= sk_tanh u
Statement as written in the source
Lemma sk_tanh_cubic u : 0 <= u -> u - u ^+ 3 <= sk_tanh u.
Used by 1 declaration in 1 file
lemma sk_tanh_norm_le source, line 281 
forall [R : realType] (u : R), `|sk_tanh u| <= `|u|
Statement as written in the source
Lemma sk_tanh_norm_le u : `|sk_tanh u| <= `|u|.
Used by 1 declaration in 1 file
lemma sk_tanh_sub_le main result source, line 291 
forall [R : realType] (u : R), `|sk_tanh u - u| <= `|u| ^+ 3
Main result

Stated in the README together with ising_dproj_eq.

Statement as written in the source
Lemma sk_tanh_sub_le u : `|sk_tanh u - u| <= `|u| ^+ 3.
Used by 1 declaration in 1 file
sectionising
Variables (R : realType) (n : nat) (A : 'M[R]_n) (theta : 'cV[R]_n).
Local Notation cube := {ffun 'I_n -> bool}.
Local Notation w := (ising_weight A theta).
Local Notation nu := (ising_mass A theta).
Local Notation E := (ising_mean A theta).
Implicit Types (x : cube) (i j : 'I_n) (f g : cube -> R).
lemma ising_weight_gt0 source, line 313 
forall [R : realType] [n : nat] (A : 'M_n) (theta : 'cV_n) (x : {ffun 'I_n -> bool}),
0 < ising_weight A theta x
Statement as written in the source
Lemma ising_weight_gt0 x : 0 < w x.
Used by 4 declarations in 1 file
lemma ising_Z_gt0 source, line 316 
forall [R : realType] [n : nat] (A : 'M_n) (theta : 'cV_n),
0 < \sum_x ising_weight A theta x
Statement as written in the source
Lemma ising_Z_gt0 : 0 < \sum_x w x.
Used by 5 declarations in 2 files
lemma ising_mass_gt0 source, line 324 
forall [R : realType] [n : nat] (A : 'M_n) (theta : 'cV_n) (x : {ffun 'I_n -> bool}),
0 < ising_mass A theta x
Statement as written in the source
Lemma ising_mass_gt0 x : 0 < nu x.
Used by 3 declarations in 2 files
lemma ising_mass_sum source, line 327 
forall [R : realType] [n : nat] (A : 'M_n) (theta : 'cV_n), \sum_x ising_mass A theta x = 1
Statement as written in the source
Lemma ising_mass_sum : \sum_x nu x = 1.
Used by 2 declarations in 2 files
lemma ising_meanE source, line 330 
forall [R : realType] [n : nat] (A : 'M_n) (theta : 'cV_n) (f : {ffun 'I_n -> bool} -> R),
ising_mean A theta f =
(\sum_x ising_weight A theta x * f x) / \sum_x ising_weight A theta x
Statement as written in the source
Lemma ising_meanE f : E f = (\sum_x w x * f x) / \sum_x w x.
Used by 2 declarations in 2 files
lemma ising_mean_ext source, line 336 
forall [R : realType] [n : nat] (A : 'M_n) (theta : 'cV_n) [f g : {ffun 'I_n -> bool} -> R],
f =1 g -> ising_mean A theta f = ising_mean A theta g
Statement as written in the source
Lemma ising_mean_ext f g : f =1 g -> E f = E g.
Used by 8 declarations in 2 files
lemma ising_meanD source, line 339 
forall [R : realType] [n : nat] (A : 'M_n) (theta : 'cV_n) (f g : {ffun 'I_n -> bool} -> R),
ising_mean A theta (fun x : {ffun 'I_n -> bool} => f x + g x) =
ising_mean A theta f + ising_mean A theta g
Statement as written in the source
Lemma ising_meanD f g : E (fun x => f x + g x) = E f + E g.
Used by 2 declarations in 2 files
lemma ising_meanZ source, line 342 
forall [R : realType] [n : nat] (A : 'M_n) (theta : 'cV_n) (c : R)
  (f : {ffun 'I_n -> bool} -> R),
ising_mean A theta (fun x : {ffun 'I_n -> bool} => c * f x) = c * ising_mean A theta f
Statement as written in the source
Lemma ising_meanZ c f : E (fun x => c * f x) = c * E f.
Used by 4 declarations in 2 files
lemma ising_meanN source, line 345 
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} => - f x) = - ising_mean A theta f
Statement as written in the source
Lemma ising_meanN f : E (fun x => - f x) = - E f.
Used by 1 declaration in 1 file
lemma ising_meanB source, line 351 
forall [R : realType] [n : nat] (A : 'M_n) (theta : 'cV_n) (f g : {ffun 'I_n -> bool} -> R),
ising_mean A theta (fun x : {ffun 'I_n -> bool} => f x - g x) =
ising_mean A theta f - ising_mean A theta g
Statement as written in the source
Lemma ising_meanB f g : E (fun x => f x - g x) = E f - E g.
lemma ising_mean_cst source, line 354 
forall [R : realType] [n : nat] (A : 'M_n) (theta : 'cV_n) (c : R),
ising_mean A theta (fun=> c) = c
Statement as written in the source
Lemma ising_mean_cst c : E (fun _ => c) = c.
Used by 4 declarations in 2 files
lemma ising_mean_le source, line 357 
forall [R : realType] [n : nat] (A : 'M_n) (theta : 'cV_n) [f g : {ffun 'I_n -> bool} -> R],
(forall x : {ffun 'I_n -> bool}, f x <= g x) ->
ising_mean A theta f <= ising_mean A theta g
Statement as written in the source
Lemma ising_mean_le f g : (forall x, f x <= g x) -> E f <= E g.
Used by 3 declarations in 2 files
lemma ising_mean_ge0 source, line 363 
forall [R : realType] [n : nat] (A : 'M_n) (theta : 'cV_n) [f : {ffun 'I_n -> bool} -> R],
(forall x : {ffun 'I_n -> bool}, 0 <= f x) -> 0 <= ising_mean A theta f
Statement as written in the source
Lemma ising_mean_ge0 f : (forall x, 0 <= f x) -> 0 <= E f.
Used by 4 declarations in 2 files
lemma ising_mean_sum source, line 368 
forall [R : realType] [n : nat] (A : 'M_n) (theta : 'cV_n) [I : finType]
  (F : I -> {ffun 'I_n -> bool} -> R),
ising_mean A theta (fun x : {ffun 'I_n -> bool} => \sum_k F k x) =
\sum_k ising_mean A theta (F k)
Statement as written in the source
Lemma ising_mean_sum (I : finType) (F : I -> cube -> R) :
  E (fun x => \sum_k F k x) = \sum_k E (F k).
Used by 4 declarations in 2 files
lemma ising_mean_eq0 source, line 375 
forall [R : realType] [n : nat] [A : 'M_n] [theta : 'cV_n] [f : {ffun 'I_n -> bool} -> R],
(forall x : {ffun 'I_n -> bool}, 0 <= f x) ->
ising_mean A theta f = 0 -> forall x : {ffun 'I_n -> bool}, f x = 0
Statement as written in the source
Lemma ising_mean_eq0 f : (forall x, 0 <= f x) -> E f = 0 -> forall x, f x = 0.
Used by 1 declaration in 1 file
lemma ising_mean_pair source, line 384 
forall [R : realType] [n : nat] (A : 'M_n) (theta : 'cV_n) (i : 'I_n)
  (f : {ffun 'I_n -> bool} -> R),
ising_mean A theta f =
(\sum_x
    (ising_weight A theta (spin_set x i true) * f (spin_set x i true) +
     ising_weight A theta (spin_set x i false) * f (spin_set x i false))) /
2 / \sum_x ising_weight A theta x
Statement as written in the source
Lemma ising_mean_pair i f :
  E f = (\sum_x (w (spin_set x i true) * f (spin_set x i true) +
                 w (spin_set x i false) * f (spin_set x i false))) /
        2 / \sum_x w x.
Used by 1 declaration in 1 file
lemma ising_mean_pair_eq source, line 394 
forall [R : realType] [n : nat] [A : 'M_n] [theta : 'cV_n] [i : 'I_n]
  [f g : {ffun 'I_n -> bool} -> R],
(forall x : {ffun 'I_n -> bool},
 ising_weight A theta (spin_set x i true) * f (spin_set x i true) +
 ising_weight A theta (spin_set x i false) * f (spin_set x i false) =
 ising_weight A theta (spin_set x i true) * g (spin_set x i true) +
 ising_weight A theta (spin_set x i false) * g (spin_set x i false)) ->
ising_mean A theta f = ising_mean A theta g
Statement as written in the source
Lemma ising_mean_pair_eq i f g :
  (forall x, w (spin_set x i true) * f (spin_set x i true) +
               w (spin_set x i false) * f (spin_set x i false) =
             w (spin_set x i true) * g (spin_set x i true) +
               w (spin_set x i false) * g (spin_set x i false)) ->
  E f = E g.
Used by 2 declarations in 1 file
definition ising_cexp source, line 407
Type
forall [R : realType] [n : nat],
'M_n -> 'cV_n -> 'I_n -> ({ffun 'I_n -> bool} -> R) -> {ffun 'I_n -> bool} -> R
Definition
Definition ising_cexp i f x : R :=
  (w (spin_set x i true) * f (spin_set x i true) +
   w (spin_set x i false) * f (spin_set x i false)) /
  (w (spin_set x i true) + w (spin_set x i false)).

The conditional expectation given the spins outside i, and the projection D_i = I - E_i.

Used by 7 declarations in 2 files
definition ising_dproj source, line 412
Type
forall [R : realType] [n : nat],
'M_n -> 'cV_n -> 'I_n -> ({ffun 'I_n -> bool} -> R) -> {ffun 'I_n -> bool} -> R
Definition
Definition ising_dproj i f x : R := f x - ising_cexp i f x.
Used by 14 declarations in 4 files
definition ising_gen source, line 414
Type
forall [R : realType] [n : nat],
'M_n -> 'cV_n -> ({ffun 'I_n -> bool} -> R) -> {ffun 'I_n -> bool} -> R
Definition
Definition ising_gen f x : R := \sum_i ising_dproj i f x.
Used by 10 declarations in 2 files
lemma ising_pair_den source, line 416 
forall [R : realType] [n : nat] (A : 'M_n) (theta : 'cV_n) (i : 'I_n)
  (x : {ffun 'I_n -> bool}),
0 < ising_weight A theta (spin_set x i true) + ising_weight A theta (spin_set x i false)
Statement as written in the source
Lemma ising_pair_den i x : 0 < w (spin_set x i true) + w (spin_set x i false).
Used by 6 declarations in 2 files
lemma ising_cexp_set source, line 419 
forall [R : realType] [n : nat] (A : 'M_n) (theta : 'cV_n) (i : 'I_n)
  (f : {ffun 'I_n -> bool} -> R) (x : {ffun 'I_n -> bool}) (b : bool),
ising_cexp A theta i f (spin_set x i b) = ising_cexp A theta i f x
Statement as written in the source
Lemma ising_cexp_set i f x b : ising_cexp i f (spin_set x i b) = ising_cexp i f x.
Used by 2 declarations in 1 file
lemma ising_cond_mean_set source, line 422 
forall [R : realType] [n : nat] (A : 'M_n) (theta : 'cV_n) (i : 'I_n)
  (x : {ffun 'I_n -> bool}) (b : bool),
ising_cond_mean A theta i (spin_set x i b) = ising_cond_mean A theta i x
Statement as written in the source
Lemma ising_cond_mean_set i x b :
  ising_cond_mean A theta i (spin_set x i b) = ising_cond_mean A theta i x.
Used by 2 declarations in 1 file
lemma ising_cond_var_set source, line 426 
forall [R : realType] [n : nat] (A : 'M_n) (theta : 'cV_n) (i : 'I_n)
  (x : {ffun 'I_n -> bool}) (b : bool),
ising_cond_var A theta i (spin_set x i b) = ising_cond_var A theta i x
Statement as written in the source
Lemma ising_cond_var_set i x b :
  ising_cond_var A theta i (spin_set x i b) = ising_cond_var A theta i x.
Used by 1 declaration in 1 file
lemma half_diff_set source, line 430 
forall [R : realType] [n : nat] (i : 'I_n) (f : {ffun 'I_n -> bool} -> R)
  (x : {ffun 'I_n -> bool}) (b : bool),
half_diff i f (spin_set x i b) = half_diff i f x
Statement as written in the source
Lemma half_diff_set i f x b : half_diff i f (spin_set x i b) = half_diff i f x.
Used by 2 declarations in 1 file
lemma ising_cond_mean_lt1 source, line 433 
forall [R : realType] [n : nat] (A : 'M_n) (theta : 'cV_n) (i : 'I_n)
  (x : {ffun 'I_n -> bool}),
`|ising_cond_mean A theta i x| < 1
Statement as written in the source
Lemma ising_cond_mean_lt1 i x : `|ising_cond_mean A theta i x| < 1.
Used by 2 declarations in 1 file
lemma ising_cond_var_ge0 source, line 442 
forall [R : realType] [n : nat] (A : 'M_n) (theta : 'cV_n) (i : 'I_n)
  (x : {ffun 'I_n -> bool}),
0 <= ising_cond_var A theta i x
Statement as written in the source
Lemma ising_cond_var_ge0 i x : 0 <= ising_cond_var A theta i x.
Used by 2 declarations in 1 file
lemma ising_cond_var_le1 source, line 449 
forall [R : realType] [n : nat] (A : 'M_n) (theta : 'cV_n) (i : 'I_n)
  (x : {ffun 'I_n -> bool}),
ising_cond_var A theta i x <= 1
Statement as written in the source
Lemma ising_cond_var_le1 i x : ising_cond_var A theta i x <= 1.
Used by 1 declaration in 1 file
lemma ising_pair_val source, line 452 
forall [R : realType] [n : nat] (i : 'I_n) (F : {ffun 'I_n -> bool} -> R)
  (x : {ffun 'I_n -> bool}),
F x = F (spin_set x i (x i))
Statement as written in the source
Lemma ising_pair_val i (F : cube -> R) x : F x = F (spin_set x i (x i)).
Used by 2 declarations in 1 file
lemma ising_dproj_eq main result source, line 455 
forall [R : realType] [n : nat] (A : 'M_n) (theta : 'cV_n) (i : 'I_n)
  (f : {ffun 'I_n -> bool} -> R) (x : {ffun 'I_n -> bool}),
ising_dproj A theta i f x = (spin (x i) - ising_cond_mean A theta i x) * half_diff i f x
Main result, as the README states it

For the Ising law nu of a matrix A and a field theta on {-1, 1}^n (the definitions of T4), the conditional expectation E_i given the spins outside i and D_i = I - E_i satisfy D_i f = (x_i - m_i) d_i f, nu[(D_i f)^2] = nu[v_i (d_i f)^2] and nu[g D_i f] = nu[D_i g D_i f]; the Dirichlet form vanishes only on the constants; ising_gen f = sum_i D_i f. For A symmetric with zero diagonal and i != j, the weights of the four configurations of the spins i and j, the other spins fixed, are K (1 + a x)(1 + b y)(1 + t x y) with K > 0, |a|, |b| < 1 and t = tanh A_ij. |tanh u| <= |u| and |tanh u - u| <= |u|^3.

Statement as written in the source
Lemma ising_dproj_eq i f x :
  ising_dproj i f x = (spin (x i) - ising_cond_mean A theta i x) * half_diff i f x.
Used by 2 declarations in 2 files
lemma ising_energy main result source, line 464 
forall [R : realType] [n : nat] (A : 'M_n) (theta : 'cV_n) (i : 'I_n)
  (f : {ffun 'I_n -> bool} -> R),
ising_mean A theta (fun x : {ffun 'I_n -> bool} => ising_dproj A theta i f x ^+ 2) =
ising_mean A theta
  (fun x : {ffun 'I_n -> bool} => ising_cond_var A theta i x * half_diff i f x ^+ 2)
Main result

Stated in the README together with ising_dproj_eq.

Statement as written in the source
Lemma ising_energy i f :
  E (fun x => ising_dproj i f x ^+ 2) =
  E (fun x => ising_cond_var A theta i x * half_diff i f x ^+ 2).
Used by 2 declarations in 2 files
lemma ising_dproj_adj main result source, line 475 
forall [R : realType] [n : nat] (A : 'M_n) (theta : 'cV_n) (i : 'I_n)
  (f g : {ffun 'I_n -> bool} -> R),
ising_mean A theta (fun x : {ffun 'I_n -> bool} => g x * ising_dproj A theta i f x) =
ising_mean A theta
  (fun x : {ffun 'I_n -> bool} => ising_dproj A theta i g x * ising_dproj A theta i f x)
Main result

Stated in the README together with ising_dproj_eq.

Statement as written in the source
Lemma ising_dproj_adj i f g :
  E (fun x => g x * ising_dproj i f x) =
  E (fun x => ising_dproj i g x * ising_dproj i f x).
Used by 1 declaration in 1 file
lemma ising_dirichletE source, line 485 
forall [R : realType] [n : nat] (A : 'M_n) (theta : 'cV_n) (f : {ffun 'I_n -> bool} -> R),
ising_dirichlet A theta f =
\sum_i ising_mean A theta (fun x : {ffun 'I_n -> bool} => ising_dproj A theta i f x ^+ 2)
Statement as written in the source
Lemma ising_dirichletE f :
  ising_dirichlet A theta f = \sum_i E (fun x => ising_dproj i f x ^+ 2).
Used by 3 declarations in 2 files
lemma ising_dirichlet_ge0 source, line 489 
forall [R : realType] [n : nat] (A : 'M_n) (theta : 'cV_n) (f : {ffun 'I_n -> bool} -> R),
0 <= ising_dirichlet A theta f
Statement as written in the source
Lemma ising_dirichlet_ge0 f : 0 <= ising_dirichlet A theta f.
Used by 2 declarations in 2 files
lemma ising_dproj_eq0 source, line 495 
forall [R : realType] [n : nat] [A : 'M_n] [theta : 'cV_n] [i : 'I_n]
  [f : {ffun 'I_n -> bool} -> R],
(forall x : {ffun 'I_n -> bool}, ising_dproj A theta i f x = 0) ->
forall (x : {ffun 'I_n -> bool}) (b : bool), f (spin_set x i b) = f x
Statement as written in the source
Lemma ising_dproj_eq0 i f :
  (forall x, ising_dproj i f x = 0) -> forall x b, f (spin_set x i b) = f x.
Used by 1 declaration in 1 file
lemma ising_dirichlet_eq0 main result source, line 509 
forall [R : realType] [n : nat] [A : 'M_n] [theta : 'cV_n] [f : {ffun 'I_n -> bool} -> R],
ising_dirichlet A theta f = 0 -> forall x y : {ffun 'I_n -> bool}, f x = f y
Main result

Stated in the README together with ising_dproj_eq.

Statement as written in the source
Lemma ising_dirichlet_eq0 f : ising_dirichlet A theta f = 0 -> forall x y, f x = f y.
Used by 1 declaration in 1 file
sectionising_block
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 w := (ising_weight A theta).
Implicit Types (x : cube) (i j : 'I_n).
lemma mxdot_deltal source, line 530 
forall [R : realType] [n : nat] (M : 'cV_n)
  (k : 'I_n),
mxdot (delta_mx k 0) M = M k 0
Statement as written in the source
Lemma mxdot_deltal (M : 'cV[R]_n) k : mxdot (delta_mx k 0) M = M k 0.
Used by 1 declaration in 1 file
lemma spin_vec_set2 source, line 533 
forall (R : realType) [n : nat] (x : {ffun 'I_n -> bool}) [i j : 'I_n] (c d : bool),
i != j ->
spin_vec (spin_set (spin_set x i c) j d) =
spin_vec x - spin (x i) *: delta_mx i 0 - spin (x j) *: delta_mx j 0 +
spin c *: delta_mx i 0 + spin d *: delta_mx j 0
Statement as written in the source
Lemma spin_vec_set2 x i j c d : i != j ->
  spin_vec (spin_set (spin_set x i c) j d) =
  (spin_vec x - spin (x i) *: delta_mx i 0 - spin (x j) *: delta_mx j 0) +
  spin c *: delta_mx i 0 + spin d *: delta_mx j 0 :> 'cV[R]_n.
Used by 1 declaration in 1 file
lemma quad_expand source, line 546 
forall [R : realType] [n : nat] [A : 'M_n],
A \is symmetricmx ->
(forall k : 'I_n, A k k = 0) ->
forall (i j : 'I_n) (u : 'cV_n) (al be : R),
mxdot (u + al *: delta_mx i 0 + be *: delta_mx j 0)
  (A *m (u + al *: delta_mx i 0 + be *: delta_mx j 0)) =
mxdot u (A *m u) + 2 * al * (A *m u) i 0 + 2 * be * (A *m u) j 0 + 2 * al * be * A i j
Statement as written in the source
Lemma quad_expand i j (u : 'cV[R]_n) (al be : R) :
  mxdot (u + al *: delta_mx i 0 + be *: delta_mx j 0)
    (A *m (u + al *: delta_mx i 0 + be *: delta_mx j 0)) =
  mxdot u (A *m u) + 2 * al * (A *m u) i 0 + 2 * be * (A *m u) j 0 +
  2 * al * be * A i j.
Used by 1 declaration in 1 file
lemma lin_expand source, line 562 
forall [R : realType] [n : nat] (theta : 'cV_n) (i j : 'I_n) (u : 'cV_n) (al be : R),
mxdot theta (u + al *: delta_mx i 0 + be *: delta_mx j 0) =
mxdot theta u + al * theta i 0 + be * theta j 0
Statement as written in the source
Lemma lin_expand i j (u : 'cV[R]_n) (al be : R) :
  mxdot theta (u + al *: delta_mx i 0 + be *: delta_mx j 0) =
  mxdot theta u + al * theta i 0 + be * theta j 0.
Used by 1 declaration in 1 file
lemma ising_weight_block main result source, line 567 
forall [R : realType] [n : nat] [A : 'M_n] (theta : 'cV_n),
A \is symmetricmx ->
(forall k : 'I_n, A k k = 0) ->
forall (x : {ffun 'I_n -> bool}) [i j : 'I_n],
i != j ->
exists
  (K : join_Num_POrderNmodule_between_Algebra_BaseAddUMagma_and_Order_Preorder R) 
(a b : join_Num_NumDomain_between_GRing_PzSemiRing_and_Num_SemiNormedZmodule R),
  [/\ 0 < K, `|a| < 1, `|b| < 1
    & forall c d : bool,
      ising_weight A theta (spin_set (spin_set x i c) j d) =
      K * ((1 + a * spin c) * (1 + b * spin d) * (1 + sk_tanh (A i j) * spin c * spin d))]
Main result

Stated in the README together with ising_dproj_eq.

Statement as written in the source
Lemma ising_weight_block x i j : i != j ->
  exists K a b, [/\ 0 < K, `|a| < 1, `|b| < 1 &
    forall c d, w (spin_set (spin_set x i c) j d) =
      K * ((1 + a * spin c) * (1 + b * spin d) *
           (1 + sk_tanh (A i j) * spin c * spin d))].
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.