Ising model on a finite graph

• The finite-volume Ising Gibbs measure
• Bridges between the StatMech Ising model and Physlib

DefinitionConfiguration equivalence induced by a vertex relabeling#✓fully proved

The equivalence of configuration spaces induced by a vertex equivalence σ : V ≃ W: ω ↦ ω ∘ σ.

def isingCfgEquiv (σ : V ≃ W) : ConfigSpace W ≃ ConfigSpace V where
  toFun ω := fun x => ω (σ x)
  invFun ω := fun y => ω (σ.symm y)
  left_inv ω := by funext y; simp
  right_inv ω := by funext x; simp

Uses 1 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model

Used byFinite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization · Simon–Lieb inequality in the infinite-volume plus state

DefinitionConfigurations on a disjoint union as pairs of configurations#✓fully proved

The equivalence between configurations on V ⊕ W and pairs of configurations on V and W.

def isingSumConfigEquiv : ConfigSpace (V ⊕ W) ≃ ConfigSpace V × ConfigSpace W :=
  Equiv.sumPiEquivProdPi (fun _ : V ⊕ W => Bool)

Uses 1 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model

Used byFinite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization · Simon–Lieb inequality in the infinite-volume plus state

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.