The Lee–Yang polynomial of a finite Ising model

DefinitionNumber of minus spins of a configuration#✓fully proved

The number of minus spins (sites with value false) of a configuration.

def minusSpinCount (s : ConfigSpace V) : ℕ :=
  (Finset.univ.filter fun x => s x = false).card

Uses 1 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model

Used byLee–Yang circle theorem · Ferromagnetic Lee–Yang polynomial has no zero in the open unit disk · Lee–Yang polynomial of a finite Ising model

DefinitionZero-field Boltzmann weight of a configuration#✓fully proved

The zero-field Boltzmann weight exp (β ∑_{e ∈ E(G)} σ_x σ_y) of a configuration.

noncomputable def zeroFieldInteractionWeight (β : ℝ) (s : ConfigSpace V) : ℝ :=
  Real.exp (β * ∑ e ∈ G.edgeFinset, bond s e)

Uses 2 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Bond variable of an unordered pair

Used byLee–Yang circle theorem · Ferromagnetic Lee–Yang polynomial has no zero in the open unit disk · Lee–Yang polynomial of a finite Ising model

DefinitionLee–Yang polynomial of a finite Ising model#✓fully proved

The Lee–Yang polynomial ∑_σ exp (β ∑_e σ_x σ_y) X^k(σ) of the Ising model on G, where k(σ) is the number of minus spins; its variable is the fugacity exp (-2βh).

noncomputable def leeYangPolynomial (β : ℝ) : ℝ[X] :=
  ∑ s : ConfigSpace V,
    Polynomial.C (zeroFieldInteractionWeight G β s) *
      Polynomial.X ^ minusSpinCount s

Uses 3 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Number of minus spins of a configuration · Zero-field Boltzmann weight of a configuration

Used byLee–Yang circle theorem · Lee–Yang polynomial with complex coefficients

DefinitionLee–Yang polynomial with complex coefficients#✓fully proved

The Lee–Yang polynomial with complex coefficients, whose zeros the Lee–Yang circle theorem locates.

noncomputable def leeYangComplexPolynomial (β : ℝ) : ℂ[X] :=
  (leeYangPolynomial G β).map (algebraMap ℝ ℂ)

Uses 1 · Used by 3

Statement usesLee–Yang polynomial of a finite Ising model

Used byLee–Yang circle property of a graph · Lee–Yang circle theorem · Ferromagnetic Lee–Yang polynomial has no zero in the open unit disk

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.