The Lee–Yang circle theorem

33 fully proved

A. Asano contraction

TheoremAsano's lemma in one variable#✓fully proved

Asano's lemma in one variable: if A + E t + D t² has no zero in the open unit disk, then neither has A + D t.

theorem asano_quadratic_contraction
    (A E D z : ℂ)
    (hstable : ∀ t : ℂ, ‖t‖ < 1 → A + E * t + D * t ^ 2 ≠ 0)
    (hz : ‖z‖ < 1) : A + D * z ≠ 0

Used by 1

Used byAsano's contraction lemma

DefinitionMulti-affine function of several complex variables#✓fully proved

A function of finitely many complex variables is multi-affine if it is affine in each variable separately.

def IsMultiAffine {I : Type*} [DecidableEq I] (p : (I → ℂ) → ℂ) : Prop :=
  ∀ (i : I) (z : I → ℂ) (t : ℂ),
    p (Function.update z i t) =
      p (Function.update z i 0) +
        t * (p (Function.update z i 1) - p (Function.update z i 0))

Used by 2

Used byAsano's contraction lemma · Ferromagnetic Lee–Yang polynomial has no zero in the open unit disk

DefinitionPolydisc stability of a function of complex variables#✓fully proved

A function of complex variables is polydisc stable if it has no zero when every variable lies in the open unit disk.

def PolydiscStable {I : Type*} (p : (I → ℂ) → ℂ) : Prop :=
  ∀ z : I → ℂ, (∀ i, ‖z i‖ < 1) → p z ≠ 0

Used by 2

Used byAsano's contraction lemma · Ferromagnetic Lee–Yang polynomial has no zero in the open unit disk

DefinitionAsano contraction of two variables#✓fully proved

The Asano contraction of the variables i and j: for p = A + B z_i + C z_j + D z_i z_j it is A + D z_i, computed from the values of p at z_i, z_j ∈ {0, 1}.

def asanoContract {I : Type*} [DecidableEq I]
    (p : (I → ℂ) → ℂ) (i j : I) :
    (I → ℂ) → ℂ := fun z ↦
  let z00 := Function.update (Function.update z i 0) j 0
  let z10 := Function.update (Function.update z i 1) j 0
  let z01 := Function.update (Function.update z i 0) j 1
  let z11 := Function.update (Function.update z i 1) j 1
  p z00 + z i * (p z11 - p z10 - p z01 + p z00)

Used by 3

Used byAsano's contraction lemma · Ferromagnetic Lee–Yang polynomial has no zero in the open unit disk · Successive Asano contraction along a list of incidences

TheoremAsano's contraction lemma#✓fully proved

Asano's contraction lemma: the Asano contraction of a multi-affine polydisc-stable polynomial is polydisc stable (Asano, Phys. Rev. Lett. 24 (1970)).

theorem asanoContract_stable {I : Type*} [DecidableEq I]
    (p : (I → ℂ) → ℂ) (hpAff : IsMultiAffine p)
    (hpStable : PolydiscStable p) {i j : I} (hij : i ≠ j) :
    PolydiscStable (asanoContract p i j)

Uses 4 · Used by 1

Statement usesMulti-affine function of several complex variables · Polydisc stability of a function of complex variables · Asano contraction of two variables

Proof usesAsano's lemma in one variable

Used byFerromagnetic Lee–Yang polynomial has no zero in the open unit disk

LemmaEdge factor has no zero in the open unit bidisk for 0 ≤ r ≤ 1#✓fully proved

The two-variable edge factor 1 + ab + r (a + b) with 0 ≤ r ≤ 1 has no zero in the open unit bidisk.

lemma leeYang_edgeFactor_ne_zero {r : ℝ} (hr0 : 0 ≤ r) (hr1 : r ≤ 1)
    {a b : ℂ} (ha : ‖a‖ < 1) (hb : ‖b‖ < 1) :
    1 + a * b + (r : ℂ) * (a + b) ≠ 0

Used by 1

Used byFerromagnetic Lee–Yang polynomial has no zero in the open unit disk

B. The half-edge polynomial

AbbreviationVariables of the half-edge polynomial#✓fully proved

The variables of the half-edge polynomial: one anchor variable per vertex and one half-edge variable per incidence (v, e).

abbrev LeeYangVar : Type _ := V ⊕ (V × ↑G.edgeFinset)

Used by 18

Used byAnchor variable of a vertex · Term of a vertex factor selected by a Boolean choice · Vertex part of the half-edge polynomial · Anchor variables of the vertices with plus spin · Selection indicator of a choice on the variables · Set of variables selected by a choice · Term of the expanded half-edge polynomial for a choice · Ferromagnetic Lee–Yang polynomial has no zero in the open unit disk · Consistency of a variable set with a list of incidences · Successive Asano contraction along a list of incidences · Half-edge polynomial with every incidence contracted · Diagonal point with anchors at q and half-edge variables at zero · Term of an edge factor selected by two Boolean choices · Edge part of the half-edge polynomial · Removal of listed half-edge variables from a variable set · Half-edge variable of an incidence · Half-edge polynomial of a graph · Edge factor in half-edge variables

DefinitionAnchor variable of a vertex#✓fully proved

The anchor variable of a vertex.

def leeYangAnchor (v : V) : LeeYangVar G := Sum.inl v

Uses 1 · Used by 6

Statement usesVariables of the half-edge polynomial

Used byTerm of a vertex factor selected by a Boolean choice · Vertex part of the half-edge polynomial · Ferromagnetic Lee–Yang polynomial has no zero in the open unit disk · Consistency of a variable set with a list of incidences · Successive Asano contraction along a list of incidences · Half-edge polynomial of a graph

DefinitionHalf-edge variable of an incidence#✓fully proved

The half-edge variable of the incidence (v, e).

def leeYangHalf (v : V) (e : ↑G.edgeFinset) : LeeYangVar G := Sum.inr (v, e)

Uses 1 · Used by 6

Statement usesVariables of the half-edge polynomial

Used byFerromagnetic Lee–Yang polynomial has no zero in the open unit disk · Consistency of a variable set with a list of incidences · Successive Asano contraction along a list of incidences · Term of an edge factor selected by two Boolean choices · Removal of listed half-edge variables from a variable set · Edge factor in half-edge variables

DefinitionEdge factor in half-edge variables#✓fully proved

The edge factor 1 + w_u w_v + e^{-2β} (w_u + w_v) of the edge e = {u, v}, in its half-edge variables.

noncomputable def leeYangNormalizedEdgeFactor (beta : ℝ)
    (e : ↑G.edgeFinset) (z : LeeYangVar G → ℂ) : ℂ :=
  Sym2.lift ⟨fun u v ↦
    1 + z (leeYangHalf G u e) * z (leeYangHalf G v e) +
      (Real.exp (-2 * beta) : ℂ) *
        (z (leeYangHalf G u e) + z (leeYangHalf G v e)), by
          intro u v
          ring⟩ e.1

Uses 2 · Used by 3

Statement usesVariables of the half-edge polynomial · Half-edge variable of an incidence

Used byFerromagnetic Lee–Yang polynomial has no zero in the open unit disk · Edge part of the half-edge polynomial · Half-edge polynomial of a graph

DefinitionHalf-edge polynomial of a graph#✓fully proved

The half-edge polynomial: the product of 1 + z_v over the vertices and of the edge factors over the edges.

noncomputable def leeYangHalfEdgeProduct (beta : ℝ)
    (z : LeeYangVar G → ℂ) : ℂ :=
  (∏ v : V, (1 + z (leeYangAnchor G v))) *
    ∏ e : ↑G.edgeFinset, leeYangNormalizedEdgeFactor G beta e z

Uses 3 · Used by 2

Statement usesVariables of the half-edge polynomial · Anchor variable of a vertex · Edge factor in half-edge variables

Used byFerromagnetic Lee–Yang polynomial has no zero in the open unit disk · Half-edge polynomial with every incidence contracted

DefinitionVertex part of the half-edge polynomial#✓fully proved

The vertex part ∏_v (1 + z_v) of the half-edge polynomial.

noncomputable def leeYangAnchorProduct (z : LeeYangVar G → ℂ) : ℂ :=
  ∏ v : V, (1 + z (leeYangAnchor G v))

Uses 2 · Used by 1

Statement usesVariables of the half-edge polynomial · Anchor variable of a vertex

Used byFerromagnetic Lee–Yang polynomial has no zero in the open unit disk

DefinitionEdge part of the half-edge polynomial#✓fully proved

The edge part of the half-edge polynomial: the product of the edge factors.

noncomputable def leeYangEdgeProduct (beta : ℝ) (z : LeeYangVar G → ℂ) : ℂ :=
  ∏ e : ↑G.edgeFinset, leeYangNormalizedEdgeFactor G beta e z

Uses 2 · Used by 1

Statement usesVariables of the half-edge polynomial · Edge factor in half-edge variables

Used byFerromagnetic Lee–Yang polynomial has no zero in the open unit disk

C. Contracting all incidences

DefinitionSuccessive Asano contraction along a list of incidences#✓fully proved

Successive Asano contraction of the half-edge variable of each incidence in the list into the anchor variable of its vertex.

def leeYangContractList (L : List (V × ↑G.edgeFinset))
    (p : (LeeYangVar G → ℂ) → ℂ) : (LeeYangVar G → ℂ) → ℂ :=
  L.foldl (fun q x ↦ asanoContract q (leeYangAnchor G x.1)
    (leeYangHalf G x.1 x.2)) p

Uses 4 · Used by 2

Statement usesVariables of the half-edge polynomial · Asano contraction of two variables · Anchor variable of a vertex · Half-edge variable of an incidence

Used byFerromagnetic Lee–Yang polynomial has no zero in the open unit disk · Half-edge polynomial with every incidence contracted

DefinitionVertex–edge incidences of a graph#✓fully proved

The incidences (v, e) of G, with v an endpoint of e.

noncomputable def leeYangIncidenceFinset : Finset (V × ↑G.edgeFinset) :=
  Finset.univ.filter fun x ↦ x.1 ∈ x.2.1

Used by 2

Used byFerromagnetic Lee–Yang polynomial has no zero in the open unit disk · Half-edge polynomial with every incidence contracted

DefinitionHalf-edge polynomial with every incidence contracted#✓fully proved

The half-edge polynomial after contracting every incidence.

noncomputable def leeYangContractedProduct (beta : ℝ) :
    (LeeYangVar G → ℂ) → ℂ :=
  leeYangContractList G (leeYangIncidenceFinset G).toList
    (leeYangHalfEdgeProduct G beta)

Uses 4 · Used by 1

Statement usesVariables of the half-edge polynomial · Successive Asano contraction along a list of incidences · Half-edge polynomial of a graph · Vertex–edge incidences of a graph

Used byFerromagnetic Lee–Yang polynomial has no zero in the open unit disk

D. Expansion of the contracted polynomial

DefinitionMonomial of a set of variables#✓fully proved

The monomial ∏_{i ∈ S} z_i.

def leeYangMonomial {I : Type*} (S : Finset I) (z : I → ℂ) : ℂ :=
  ∏ i ∈ S, z i

Used by 1

Used byFerromagnetic Lee–Yang polynomial has no zero in the open unit disk

DefinitionChosen first endpoint of an edge#✓fully proved

A chosen first endpoint of an edge.

noncomputable def leeYangEndpoint0 (e : ↑G.edgeFinset) : V := e.1.out.1

Used by 5

Used bySelection indicator of a choice on the variables · Ferromagnetic Lee–Yang polynomial has no zero in the open unit disk · Term of an edge factor selected by two Boolean choices · Real disagreement weight of a spin configuration · Edge choices induced by a spin configuration

DefinitionOther endpoint of an edge#✓fully proved

The other endpoint of an edge.

noncomputable def leeYangEndpoint1 (e : ↑G.edgeFinset) : V := e.1.out.2

Used by 5

Used bySelection indicator of a choice on the variables · Ferromagnetic Lee–Yang polynomial has no zero in the open unit disk · Term of an edge factor selected by two Boolean choices · Real disagreement weight of a spin configuration · Edge choices induced by a spin configuration

DefinitionTerm of a vertex factor selected by a Boolean choice#✓fully proved

The term of 1 + z_v selected by a Boolean choice.

def leeYangAnchorChoiceFactor (z : LeeYangVar G → ℂ) (v : V) (b : Bool) : ℂ :=
  if b then z (leeYangAnchor G v) else 1

Uses 2 · Used by 2

Statement usesVariables of the half-edge polynomial · Anchor variable of a vertex

Used byTerm of the expanded half-edge polynomial for a choice · Ferromagnetic Lee–Yang polynomial has no zero in the open unit disk

DefinitionTerm of an edge factor selected by two Boolean choices#✓fully proved

The term of the edge factor selected by a pair of Boolean choices, one per endpoint.

noncomputable def leeYangEdgeChoiceFactor (beta : ℝ) (z : LeeYangVar G → ℂ)
    (e : ↑G.edgeFinset) (b : Bool × Bool) : ℂ :=
  (if b.1 = b.2 then 1 else (Real.exp (-2 * beta) : ℂ)) *
    (if b.1 then z (leeYangHalf G (leeYangEndpoint0 G e) e) else 1) *
    (if b.2 then z (leeYangHalf G (leeYangEndpoint1 G e) e) else 1)

Uses 4 · Used by 2

Statement usesVariables of the half-edge polynomial · Chosen first endpoint of an edge · Other endpoint of an edge · Half-edge variable of an incidence

Used byTerm of the expanded half-edge polynomial for a choice · Ferromagnetic Lee–Yang polynomial has no zero in the open unit disk

DefinitionTerm of the expanded half-edge polynomial for a choice#✓fully proved

The term of the expanded half-edge polynomial selected by a choice at every vertex and every edge.

noncomputable def leeYangChoiceTerm (beta : ℝ)
    (x : (V → Bool) × (↑G.edgeFinset → Bool × Bool))
    (z : LeeYangVar G → ℂ) : ℂ :=
  (∏ v : V, leeYangAnchorChoiceFactor G z v (x.1 v)) *
    ∏ e : ↑G.edgeFinset, leeYangEdgeChoiceFactor G beta z e (x.2 e)

Uses 3 · Used by 1

Statement usesVariables of the half-edge polynomial · Term of a vertex factor selected by a Boolean choice · Term of an edge factor selected by two Boolean choices

Used byFerromagnetic Lee–Yang polynomial has no zero in the open unit disk

DefinitionCoefficient of a term of the expanded half-edge polynomial#✓fully proved

The coefficient of a term of the expanded half-edge polynomial: e^{-2β} for every edge whose two choices differ.

noncomputable def leeYangChoiceWeight (beta : ℝ)
    (x : (V → Bool) × (↑G.edgeFinset → Bool × Bool)) : ℂ :=
  ∏ e : ↑G.edgeFinset,
    if (x.2 e).1 = (x.2 e).2 then 1 else (Real.exp (-2 * beta) : ℂ)

Used by 1

Used byFerromagnetic Lee–Yang polynomial has no zero in the open unit disk

DefinitionSelection indicator of a choice on the variables#✓fully proved

Whether a choice selects each variable.

noncomputable def leeYangChoiceSelected
    (x : (V → Bool) × (↑G.edgeFinset → Bool × Bool)) :
    LeeYangVar G → Bool
  | Sum.inl v => x.1 v
  | Sum.inr (v, e) =>
      if v = leeYangEndpoint0 G e then (x.2 e).1
      else if v = leeYangEndpoint1 G e then (x.2 e).2
      else false

Uses 3 · Used by 2

Statement usesVariables of the half-edge polynomial · Chosen first endpoint of an edge · Other endpoint of an edge

Used bySet of variables selected by a choice · Ferromagnetic Lee–Yang polynomial has no zero in the open unit disk

DefinitionSet of variables selected by a choice#✓fully proved

The set of variables selected by a choice, the support of its monomial.

noncomputable def leeYangChoiceSupport
    (x : (V → Bool) × (↑G.edgeFinset → Bool × Bool)) :
    Finset (LeeYangVar G) :=
  Finset.univ.filter fun k ↦ leeYangChoiceSelected G x k = true

Uses 2 · Used by 1

Statement usesVariables of the half-edge polynomial · Selection indicator of a choice on the variables

Used byFerromagnetic Lee–Yang polynomial has no zero in the open unit disk

DefinitionRemoval of listed half-edge variables from a variable set#✓fully proved

Remove from a set of variables the half-edge variables of the listed incidences.

def leeYangEraseHalves (L : List (V × ↑G.edgeFinset))
    (S : Finset (LeeYangVar G)) : Finset (LeeYangVar G) :=
  L.foldl (fun T x ↦ T.erase (leeYangHalf G x.1 x.2)) S

Uses 2 · Used by 1

Statement usesVariables of the half-edge polynomial · Half-edge variable of an incidence

Used byFerromagnetic Lee–Yang polynomial has no zero in the open unit disk

DefinitionConsistency of a variable set with a list of incidences#✓fully proved

A set of variables is consistent with a list of incidences if each listed half-edge variable is selected exactly when the anchor variable of its vertex is.

def LeeYangConsistent (L : List (V × ↑G.edgeFinset))
    (S : Finset (LeeYangVar G)) : Prop :=
  ∀ x ∈ L, leeYangAnchor G x.1 ∈ S ↔ leeYangHalf G x.1 x.2 ∈ S

Uses 3 · Used by 1

Statement usesVariables of the half-edge polynomial · Anchor variable of a vertex · Half-edge variable of an incidence

Used byFerromagnetic Lee–Yang polynomial has no zero in the open unit disk

DefinitionEdge choices induced by a spin configuration#✓fully proved

The edge choices induced by a spin configuration: each edge copies the spins of its endpoints.

noncomputable def leeYangTauOf (sigma : V → Bool) :
    ↑G.edgeFinset → Bool × Bool := fun e ↦
  (sigma (leeYangEndpoint0 G e), sigma (leeYangEndpoint1 G e))

Uses 2 · Used by 1

Statement usesChosen first endpoint of an edge · Other endpoint of an edge

Used byFerromagnetic Lee–Yang polynomial has no zero in the open unit disk

DefinitionAnchor variables of the vertices with plus spin#✓fully proved

The anchor variables of the vertices with spin true.

noncomputable def leeYangAnchorSupport (sigma : V → Bool) :
    Finset (LeeYangVar G) :=
  Finset.univ.filter fun k ↦ match k with
    | Sum.inl v => sigma v = true
    | Sum.inr _ => False

Uses 1 · Used by 1

Statement usesVariables of the half-edge polynomial

Used byFerromagnetic Lee–Yang polynomial has no zero in the open unit disk

E. Restriction to the diagonal

DefinitionDiagonal point with anchors at q and half-edge variables at zero#✓fully proved

The point with every anchor variable equal to q and every half-edge variable equal to 0.

def leeYangDiagonal (q : ℂ) : LeeYangVar G → ℂ
  | Sum.inl _ => q
  | Sum.inr _ => 0

Uses 1 · Used by 1

Statement usesVariables of the half-edge polynomial

Used byFerromagnetic Lee–Yang polynomial has no zero in the open unit disk

DefinitionReal disagreement weight of a spin configuration#✓fully proved

The real weight ∏_e e^{-2β [σ_u ≠ σ_v]} of a spin configuration.

noncomputable def leeYangRealChoiceWeight (beta : ℝ) (sigma : V → Bool) : ℝ :=
  ∏ e : ↑G.edgeFinset,
    if sigma (leeYangEndpoint0 G e) = sigma (leeYangEndpoint1 G e) then 1
    else Real.exp (-2 * beta)

Uses 2 · Used by 1

Statement usesChosen first endpoint of an edge · Other endpoint of an edge

Used byFerromagnetic Lee–Yang polynomial has no zero in the open unit disk

F. The Lee–Yang circle theorem

LemmaFerromagnetic Lee–Yang polynomial has no zero in the open unit disk#✓fully proved

The Lee–Yang polynomial of a ferromagnetic Ising model has no zero in the open unit disk.

lemma leeYangComplexPolynomial_ne_zero_in_openUnitDisk
    {beta : ℝ} (hbeta : 0 ≤ beta) {q : ℂ} (hq : ‖q‖ < 1) :
    (leeYangComplexPolynomial G beta).eval q ≠ 0

Uses 38 · Used by 1

Statement usesLee–Yang polynomial with complex coefficients

Proof usesConfiguration space of a statistical-mechanics model · Bond variable of an unordered pair · Spin of a configuration at a site · Multi-affine function of several complex variables · Consistency of a variable set with a list of incidences · Variables of the half-edge polynomial · Polydisc stability of a function of complex variables · Asano contraction of two variables · Asano's contraction lemma · Anchor variable of a vertex · Term of a vertex factor selected by a Boolean choice · Vertex part of the half-edge polynomial · Anchor variables of the vertices with plus spin · Selection indicator of a choice on the variables · Set of variables selected by a choice · Term of the expanded half-edge polynomial for a choice · Coefficient of a term of the expanded half-edge polynomial · Successive Asano contraction along a list of incidences · Half-edge polynomial with every incidence contracted · Diagonal point with anchors at q and half-edge variables at zero · Term of an edge factor selected by two Boolean choices · Edge part of the half-edge polynomial · Chosen first endpoint of an edge · Other endpoint of an edge · Removal of listed half-edge variables from a variable set · Global spin flip · Global spin flip as an involutive equivalence · Half-edge variable of an incidence · Half-edge polynomial of a graph · Vertex–edge incidences of a graph · Monomial of a set of variables · Edge factor in half-edge variables · Real disagreement weight of a spin configuration · Edge choices induced by a spin configuration · Edge factor has no zero in the open unit bidisk for 0 ≤ r ≤ 1 · Number of minus spins of a configuration · Zero-field Boltzmann weight of a configuration

Used byLee–Yang circle theorem

TheoremLee–Yang circle theorem#✓fully proved

For the Ising model on a finite graph with uniform ferromagnetic coupling and β ≥ 0, every complex zero of the partition function in the fugacity z = e^{-2βh} lies on the unit circle (Lee and Yang, Statistical theory of equations of state and phase transitions. II, Phys. Rev. 87 (1952)).

theorem finiteGraph_hasLeeYangCircle {beta : ℝ} (hbeta : 0 ≤ beta) :
    HasLeeYangCircle G beta

Uses 11

Statement usesLee–Yang circle property of a graph

Proof usesConfiguration space of a statistical-mechanics model · Bond variable of an unordered pair · Spin of a configuration at a site · Lee–Yang polynomial with complex coefficients · Ferromagnetic Lee–Yang polynomial has no zero in the open unit disk · Global spin flip · Global spin flip as an involutive equivalence · Lee–Yang polynomial of a finite Ising model · Number of minus spins of a configuration · Zero-field Boltzmann weight of a configuration

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.