Correlation inequalities for spin systems

Inequalities for the correlations of ferromagnetic Ising models: the Griffiths (GKS) and FKG inequalities, monotonicity in the couplings and the temperature, and the Griffiths–Hurst–Sherman inequality with its consequences for the magnetization.

TheoremFKG inequality#✓fully proved

FKG inequality for the Ising model. For β ≥ 0 and any field, increasing functions are positively correlated under the Ising Gibbs distribution on a finite graph.

C. M. Fortuin, P. W. Kasteleyn and J. Ginibre, Correlation inequalities on some partially ordered sets, Comm. Math. Phys. 22 (1971). See also MathlibExt.Probability.CorrelationInequalities.FKG.

theorem ifk_isingProb_positively_associated {β : ℝ} (hβ : 0 ≤ β) (h : ℝ)
    {f g : ConfigSpace V → ℝ} (hf : Monotone f) (hg : Monotone g) :
    (∑ s, isingProb G β h s * f s) * (∑ s, isingProb G β h s * g s)
      ≤ ∑ s, isingProb G β h s * (f s * g s)

abbrev ConfigSpace (E : Type*) : Type _ := E → Bool

MathlibExt/Probability/Configuration/ConfigSpace.lean:40

noncomputable def isingProb (β h : ℝ) (s : ConfigSpace V) : ℝ :=
  isingWeight G β h s / isingZ G β h

PhyslibExt/CondensedMatter/IsingModel/Gibbs.lean:141

Uses 11

Statement usesConfiguration space of a statistical-mechanics model · Gibbs probability of an Ising configuration

Proof usesFKG lattice condition · Bond variable of an unordered pair · Ising Hamiltonian on a finite graph · Ising Gibbs probabilities sum to one · Boltzmann weight of an Ising configuration · Ising partition function · Positivity of the Ising partition function · Spin of a configuration at a site · FKG inequality

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.