Translation invariance and ergodicity of the q = 2 random-cluster measures

LemmaAlmost-invariant events are trivial under an ergodic measure#✓fully proved

Under an ergodic measure, a measurable set invariant up to null sets has measure 0 or 1. See also Mathlib's aeconst_of_forall_preimage_smul_ae_eq for ErgodicSMul.

lemma aeconst_of_ae_invariant
    {μ : Measure (ConfigSpace E)} [IsProbabilityMeasure μ] [Countable G]
    (hμ : IsErgodic (G := G) μ)
    {s : Set (ConfigSpace E)} (hs : MeasurableSet s)
    (hinv : ∀ g : G, (shift g : ConfigSpace E → ConfigSpace E) ⁻¹' s =ᵐ[μ] s) :
    μ s = 0 ∨ μ s = 1

Uses 4 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Ergodic measure on configuration space · Shift of a configuration by a group element

Proof usesTranslation-invariant measure on configuration space

Used byExtremality of the plus state

DefinitionSelf-mixing on cylinder events#✓fully proved

For every cylinder event A and ε > 0 there is a translation g with |μ(A ∩ g⁻¹A) - μ(A)²| < ε.

def fmc_SelfMixing [Countable E] (μ : Measure (ConfigSpace E)) : Prop :=
  ∀ A ∈ measurableCylinders (fun _ : E => Bool), ∀ ε : ℝ, 0 < ε →
    ∃ g : G, |μ.real (A ∩ (shift g : ConfigSpace E → ConfigSpace E) ⁻¹' A)
      - (μ.real A) ^ 2| < ε

Uses 2 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Shift of a configuration by a group element

Used byErgodicity of the plus state · Extremality of the plus state · Translation-invariant self-mixing measures are ergodic · Wired \(q = 2\) measure is ergodic under the factorization bound

LemmaCylinder approximation of events under a finite measure#✓fully proved

Every measurable event is approximated by a cylinder event in symmetric difference; the general form of exists_cylinder_symmDiff_lt (Ergodicity).

lemma fmc_exists_cylinder_symmDiff_lt [Countable E] (μ : Measure (ConfigSpace E))
    [IsFiniteMeasure μ] {A : Set (ConfigSpace E)} (hA : MeasurableSet A) {ε : ℝ≥0∞} (hε : 0 < ε) :
    ∃ C ∈ measurableCylinders (fun _ : E => Bool), μ (C ∆ A) < ε

Uses 1 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model

Used byTranslation-invariant self-mixing measures are ergodic

LemmaTranslation-invariant self-mixing measures are ergodic#✓fully proved

A translation-invariant self-mixing probability measure is ergodic.

lemma fmc_isErgodic_of_selfMixing [Countable E] {μ : Measure (ConfigSpace E)}
    [IsProbabilityMeasure μ] (hμ : IsTranslationInvariant (G := G) μ)
    (hmix : fmc_SelfMixing (G := G) μ) :
    IsErgodic (G := G) μ

Uses 6 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Ergodic measure on configuration space · Translation-invariant measure on configuration space · Self-mixing on cylinder events

Proof usesShift of a configuration by a group element · Cylinder approximation of events under a finite measure

Used byErgodicity of the plus state · Extremality of the plus state · Wired \(q = 2\) measure is ergodic under the factorization bound

DefinitionEvent that every coordinate of a finite set is open#✓fully proved

The event O_T that every coordinate in T is open. See also cdc_multiOpenEvent and med_genericMultiOpenEvent.

def fmu_multiOpen (T : Finset E) : Set (ConfigSpace E) := {ω | ∀ e ∈ T, ω e = true}

Uses 1 · Used by 25

Statement usesConfiguration space of a statistical-mechanics model

Used byInf-based and sup-based Ising critical points agree for \(d \ge 2\) · Ergodicity of the plus state · Translation invariance of the plus state · Extremality of the plus state · Off-centre domination of all-plus events · Asymptotic shift homogeneity of all-plus events in plus boxes · Shift homogeneity of all-plus events in the plus state · Ergodicity of the wired random-cluster measure · Disjoint-box cap hypothesis for multi-open events · Conditional product cap for multi-open events in boxes · Pair mixing of multi-open events · Upper decay of correlations of multi-open events · Far-box product domination of multi-open events · Finite-box disjoint product domination of multi-open events · Wired box products approximate infinite-volume products · Finite-box product domination from the factorization bound · Upper decorrelation of the wired measure from factorization · Domain monotonicity for translated pairs of multi-open events · Disjoint-box factorization bound for box measures · All-open Dirac mass satisfies the factorization bound · Domain monotonicity for edge sets realized in a box · Wired \(q = 2\) measure is ergodic under the factorization bound · Domain monotonicity of wired multi-open probabilities · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\)

DefinitionCoordinate state as a real number#✓fully proved

The state of coordinate e as a real number in {0, 1}.

noncomputable def fmu_xR (ω : ConfigSpace E) (e : E) : ℝ := if ω e then 1 else 0

Uses 1 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model

Used byErgodicity of the plus state · Extremality of the plus state · Product indicator of a multi-open event · Wired \(q = 2\) measure is ergodic under the factorization bound

DefinitionProduct indicator of a multi-open event#✓fully proved

The indicator of O_T as the product ∏_{e ∈ T} ω(e).

noncomputable def fmu_moInd (T : Finset E) (ω : ConfigSpace E) : ℝ := ∏ e ∈ T, fmu_xR ω e

Uses 2 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Coordinate state as a real number

Used byErgodicity of the plus state · Extremality of the plus state · Wired \(q = 2\) measure is ergodic under the factorization bound

DefinitionIndicator of agreeing with a pattern on a finite set#✓fully proved

The indicator that ω agrees with τ on F.

noncomputable def fmu_traceInd (F : Finset E) (τ : E → Bool) (ω : ConfigSpace E) : ℝ :=
  if (∀ e ∈ F, ω e = τ e) then 1 else 0

Uses 1 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model

Used byErgodicity of the plus state · Extremality of the plus state · Wired \(q = 2\) measure is ergodic under the factorization bound

DefinitionInclusion–exclusion coefficient of a multi-open event#✓fully proved

The inclusion–exclusion coefficient of O_T in the expansion of the trace indicator of τ on F.

noncomputable def fmu_traceCoef [DecidableEq E] (F : Finset E) (τ : E → Bool) (T : Finset E) : ℝ :=
  (∏ e ∈ T, (if τ e then (1 : ℝ) else -1)) * (∏ e ∈ F \ T, (if τ e then (0 : ℝ) else 1))

Used by 3

Used byErgodicity of the plus state · Extremality of the plus state · Wired \(q = 2\) measure is ergodic under the factorization bound

DefinitionPair mixing of multi-open events#✓fully proved

For every finite family of finite sets T and δ > 0 there is one translation g with |μ(O_T ∩ g⁻¹O_{T'}) - μ(O_T) μ(O_{T'})| < δ for all T, T' in the family.

def fmu_PairMixing (μ : Measure (ConfigSpace E)) : Prop :=
  ∀ (P : Finset (Finset E)) (δ : ℝ), 0 < δ →
    ∃ g : G, ∀ T ∈ P, ∀ T' ∈ P,
      |μ.real (fmu_multiOpen T ∩
          (shift g : ConfigSpace E → ConfigSpace E) ⁻¹' fmu_multiOpen T')
        - μ.real (fmu_multiOpen T) * μ.real (fmu_multiOpen T')| < δ

Uses 3 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Shift of a configuration by a group element · Event that every coordinate of a finite set is open

Used byErgodicity of the plus state · Extremality of the plus state · Wired \(q = 2\) measure is ergodic under the factorization bound

DefinitionMixing for finite families of cylinder events#✓fully proved

The analogue of fmu_PairMixing for finite families of cylinder events.

def fmu_GenMixing (μ : Measure (ConfigSpace E)) : Prop :=
  ∀ (𝒜 : Finset (Set (ConfigSpace E))),
    (∀ A ∈ 𝒜, A ∈ measurableCylinders (fun _ : E => Bool)) →
    ∀ δ : ℝ, 0 < δ →
    ∃ g : G, ∀ A ∈ 𝒜, ∀ B ∈ 𝒜,
      |μ.real (A ∩ (shift g : ConfigSpace E → ConfigSpace E) ⁻¹' B)
        - μ.real A * μ.real B| < δ

Uses 2

Statement usesConfiguration space of a statistical-mechanics model · Shift of a configuration by a group element

DefinitionUpper decay of correlations of multi-open events#✓fully proved

The one-sided form of fmu_PairMixing: μ(O_T ∩ g⁻¹O_{T'}) ≤ μ(O_T) μ(O_{T'}) + δ.

def fmu_UpperDecay (μ : Measure (ConfigSpace E)) : Prop :=
  ∀ (P : Finset (Finset E)) (δ : ℝ), 0 < δ →
    ∃ g : G, ∀ T ∈ P, ∀ T' ∈ P,
      μ.real (fmu_multiOpen T ∩
          (shift g : ConfigSpace E → ConfigSpace E) ⁻¹' fmu_multiOpen T')
        ≤ μ.real (fmu_multiOpen T) * μ.real (fmu_multiOpen T') + δ

Uses 3 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Shift of a configuration by a group element · Event that every coordinate of a finite set is open

Used byErgodicity of the plus state · Extremality of the plus state · Upper decorrelation of the wired measure from factorization · Wired \(q = 2\) measure is ergodic under the factorization bound

DefinitionExtreme point of the invariant probability measures#✓fully proved

μ is a translation-invariant probability measure that is not a nontrivial convex combination of two distinct translation-invariant probability measures.

def IsInvariantExtremePoint (μ : Measure (ConfigSpace E)) : Prop :=
  IsTranslationInvariant (G := G) μ ∧ IsProbabilityMeasure μ ∧
    ∀ (ν₁ ν₂ : Measure (ConfigSpace E)) (a b : ℝ≥0∞),
      IsTranslationInvariant (G := G) ν₁ → IsTranslationInvariant (G := G) ν₂ →
        IsProbabilityMeasure ν₁ → IsProbabilityMeasure ν₂ →
          0 < a → 0 < b → a + b = 1 → μ = a • ν₁ + b • ν₂ → ν₁ = ν₂

Uses 2 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Translation-invariant measure on configuration space

Used byExtremality of the plus state · Extreme invariant measures are ergodic

LemmaExtreme invariant measures are ergodic#✓fully proved

An extreme point of the translation-invariant probability measures is ergodic.

lemma fec_isErgodic_of_invariantExtremePoint {μ : Measure (ConfigSpace E)}
    (hμ : IsInvariantExtremePoint (G := G) μ) :
    IsErgodic (G := G) μ

Uses 5

Statement usesConfiguration space of a statistical-mechanics model · Ergodic measure on configuration space · Extreme point of the invariant probability measures

Proof usesTranslation-invariant measure on configuration space · Shift of a configuration by a group element

DefinitionConditional product cap for multi-open events in boxes#✓fully proved

For every finite family of finite edge sets and box index N, some translation g satisfies, for all large m: each O_T ∩ g⁻¹O_{T'} is A ∩ B on Λ_m with A increasing and B depending only on edges outside some F, the conditional masses of A on the fibres of F (with a boundary graph containing the wired one) are at most μ_N(O_T), and the mass of B is at most μ_N(O_{T'}).

StatMech.FK.fdb_BoxConditionalProductCap · 24 lines

def fdb_BoxConditionalProductCap {p : ℝ} (hp : 0 < p) (hp1 : p < 1) : Prop :=
  ∀ (P : Finset (Finset (Sym2 (Site d)))) (N : ℕ),
    ∃ g : Multiplicative (Site d), ∀ᶠ m in atTop, ∀ T ∈ P, ∀ T' ∈ P,
      ∃ (F : Finset (Sym2 (boxVerts d m)))
        (S_A S_B : Set (ConfigSpace (Sym2 (boxVerts d m))))
        (C' : SimpleGraph (boxVerts d m)) (_ : DecidableRel C'.Adj),
        (fmu_multiOpen T ∩
          (shift g : ConfigSpace (Sym2 (Site d)) → ConfigSpace (Sym2 (Site d)))
            ⁻¹' fmu_multiOpen T') = boxRestrict d m ⁻¹' (S_A ∩ S_B) ∧
        MeasurableSet (boxRestrict d m ⁻¹' (S_A ∩ S_B)) ∧
        MeasurableSet (boxRestrict d m ⁻¹' S_B) ∧
        IsIncreasing S_A ∧
        DependsOnOutside F S_B ∧
        boundaryCliqueGraph (boxBoundary d m) ≤ C' ∧
        (0 ≤ (wiredFiniteMeasure d N hp hp1 (by norm_num : (0 : ℝ) < 2)
            : Measure (ConfigSpace (Sym2 (Site d)))).real (fmu_multiOpen T)) ∧
        (∀ ψ ∈ fibreReps F,
          (∑ ρ, S_A.indicator (fun _ => (1 : ℝ)) ρ * condBcProb (boxGraph d m) C' p 2 F ψ ρ)
            ≤ (wiredFiniteMeasure d N hp hp1 (by norm_num : (0 : ℝ) < 2)
                : Measure (ConfigSpace (Sym2 (Site d)))).real (fmu_multiOpen T)) ∧
        ((wiredFiniteMeasure d m hp hp1 (by norm_num : (0 : ℝ) < 2)
            : Measure (ConfigSpace (Sym2 (Site d)))).real (boxRestrict d m ⁻¹' S_B)
          ≤ (wiredFiniteMeasure d N hp hp1 (by norm_num : (0 : ℝ) < 2)
              : Measure (ConfigSpace (Sym2 (Site d)))).real (fmu_multiOpen T'))

Uses 15

Statement usesConfiguration space of a statistical-mechanics model · Shift of a configuration by a group element · Event depending only on edges outside a set · Vertex boundary of a box · Nearest-neighbour graph on a box · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Vertices of the box \((-n, n)^d\) · Conditional random-cluster measure with a boundary wiring · Fibre representatives with every edge of a set closed · Event that every coordinate of a finite set is open · Wired random-cluster measure on a box · Increasing event · Site of the hypercubic lattice · Complete graph on the boundary vertices · Box \((-n, n)^d\) in the hypercubic lattice

DefinitionFar-box product domination of multi-open events#✓fully proved

For every finite family of finite edge sets, box index m, and δ > 0, some translation g satisfies μ(O_T ∩ g⁻¹O_{T'}) ≤ μ_m(O_T) μ_m(O_{T'}) + δ for all T, T' in the family.

def ftb_FarBoxProductDom {p : ℝ} (_hp : 0 < p) (_hp1 : p < 1)
    (μbox : ℕ → Measure (ConfigSpace (Sym2 (Site d))))
    (μ : Measure (ConfigSpace (Sym2 (Site d)))) : Prop :=
  ∀ (P : Finset (Finset (Sym2 (Site d)))) (m : ℕ) (δ : ℝ), 0 < δ →
    ∃ g : Multiplicative (Site d), ∀ T ∈ P, ∀ T' ∈ P,
      μ.real (fmu_multiOpen T ∩
          (shift g : ConfigSpace (Sym2 (Site d)) → ConfigSpace (Sym2 (Site d)))
            ⁻¹' fmu_multiOpen T')
        ≤ (μbox m).real (fmu_multiOpen T) * (μbox m).real (fmu_multiOpen T') + δ

Uses 4

Statement usesConfiguration space of a statistical-mechanics model · Shift of a configuration by a group element · Event that every coordinate of a finite set is open · Site of the hypercubic lattice

DefinitionFinite-box disjoint product domination of multi-open events#✓fully proved

For every finite family of finite edge sets and box index N, some translation g satisfies, for all large m, μ_m(O_T ∩ g⁻¹O_{T'}) ≤ μ_N(O_T) μ_N(O_{T'}) for all T, T' in the family.

def ftb_FiniteBoxDisjointProductDom {p : ℝ} (_hp : 0 < p) (_hp1 : p < 1)
    (μbox : ℕ → Measure (ConfigSpace (Sym2 (Site d)))) : Prop :=
  ∀ (P : Finset (Finset (Sym2 (Site d)))) (N : ℕ),
    ∃ g : Multiplicative (Site d), ∀ᶠ m in atTop, ∀ T ∈ P, ∀ T' ∈ P,
      (μbox m).real (fmu_multiOpen T ∩
          (shift g : ConfigSpace (Sym2 (Site d)) → ConfigSpace (Sym2 (Site d)))
            ⁻¹' fmu_multiOpen T')
        ≤ (μbox N).real (fmu_multiOpen T) * (μbox N).real (fmu_multiOpen T')

Uses 4

Statement usesConfiguration space of a statistical-mechanics model · Shift of a configuration by a group element · Event that every coordinate of a finite set is open · Site of the hypercubic lattice

DefinitionTranslated wired box measure#✓fully proved

The wired finite-volume random-cluster measure on Λ_n translated by g.

noncomputable def erg_wiredShiftedFinite {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q)
    (g : Multiplicative (Site d)) (n : ℕ) :
    ProbabilityMeasure (ConfigSpace (Sym2 (Site d))) :=
  (wiredFiniteMeasure d n hp hp1 hq).map (shift g)

Uses 4 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Shift of a configuration by a group element · Wired random-cluster measure on a box · Site of the hypercubic lattice

Used byWired translation invariance from integral shift decay

DefinitionTranslated free box measure#✓fully proved

The free finite-volume random-cluster measure on Λ_n translated by g.

noncomputable def erg_freeShiftedFinite {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q)
    (g : Multiplicative (Site d)) (n : ℕ) :
    ProbabilityMeasure (ConfigSpace (Sym2 (Site d))) :=
  (freeFiniteMeasure d n hp hp1 hq).map (shift g)

Uses 4 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Shift of a configuration by a group element · Free random-cluster measure on a box · Site of the hypercubic lattice

Used byFree translation invariance from integral shift decay

DefinitionWired integral shift decay along a box sequence#✓fully proved

Along the box sequence φ, the wired box integrals of f and of f ∘ θ_g differ by a quantity tending to zero, for every bounded continuous f.

def ivt_wiredIntegralShiftDecay {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q)
    (g : Multiplicative (Site d)) (φ : ℕ → ℕ) : Prop :=
  ∀ f : (ConfigSpace (Sym2 (Site d))) →ᵇ ℝ,
    Tendsto (fun n =>
        (∫ x, f x ∂((wiredFiniteMeasure d (φ n) hp hp1 hq : ProbabilityMeasure _) : Measure _))
          - (∫ x, f (shift g x)
              ∂((wiredFiniteMeasure d (φ n) hp hp1 hq : ProbabilityMeasure _) : Measure _)))
      atTop (𝓝 0)

Uses 4 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Shift of a configuration by a group element · Wired random-cluster measure on a box · Site of the hypercubic lattice

Used byWired translation invariance from decay on a dense set · Identity shift satisfies the wired decay hypothesis · Wired translation invariance from integral shift decay

DefinitionFree integral shift decay along a box sequence#✓fully proved

Along the box sequence φ, the free box integrals of f and of f ∘ θ_g differ by a quantity tending to zero, for every bounded continuous f.

def ivt_freeIntegralShiftDecay {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q)
    (g : Multiplicative (Site d)) (φ : ℕ → ℕ) : Prop :=
  ∀ f : (ConfigSpace (Sym2 (Site d))) →ᵇ ℝ,
    Tendsto (fun n =>
        (∫ x, f x ∂((freeFiniteMeasure d (φ n) hp hp1 hq : ProbabilityMeasure _) : Measure _))
          - (∫ x, f (shift g x)
              ∂((freeFiniteMeasure d (φ n) hp hp1 hq : ProbabilityMeasure _) : Measure _)))
      atTop (𝓝 0)

Uses 4 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Shift of a configuration by a group element · Free random-cluster measure on a box · Site of the hypercubic lattice

Used byFree translation invariance from decay on a dense set · Identity shift satisfies the free decay hypothesis · Free translation invariance from integral shift decay

LemmaWired translation invariance from integral shift decay#✓fully proved

The wired infinite-volume FK measure is translation invariant if the integral decay hypothesis holds for every shift and every convergent box subsequence. See also flc_wiredIV_isTranslationInvariant, which proves invariance for q = 2 without hypotheses.

lemma ivt_wiredIV_isTranslationInvariant_of_decay {p q : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (hq : 0 < q)
    (hdecay : ∀ (g : Multiplicative (Site d)) (φ : ℕ → ℕ), StrictMono φ →
        WeakConvergesTo (fun n => wiredFiniteMeasure d (φ n) hp hp1 hq)
          (wiredInfiniteVolume d hp hp1 hq) →
        ivt_wiredIntegralShiftDecay hp hp1 hq g φ) :
    ConfigSpace.IsTranslationInvariant (G := Multiplicative (Site d))
      (wiredInfiniteVolume d hp hp1 hq : Measure (ConfigSpace (Sym2 (Site d))))

Uses 12 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Translation-invariant measure on configuration space · Wired integral shift decay along a box sequence · Wired random-cluster measure on a box · Wired infinite-volume random-cluster measure · Site of the hypercubic lattice · Weak convergence of probability measures on configuration space

Proof usesShift of a configuration by a group element · Translated wired box measure · Wired infinite-volume measure is a subsequential weak limit · Weak convergence implies convergence of integrals · Convergence of integrals implies weak convergence

Used byWired translation invariance from decay on a dense set

LemmaFree translation invariance from integral shift decay#✓fully proved

The free infinite-volume FK measure is translation invariant if the integral decay hypothesis holds for every shift and every convergent box subsequence. See also bdp_freeIV_isTranslationInvariant, which proves invariance for q = 2 without hypotheses.

lemma ivt_freeIV_isTranslationInvariant_of_decay {p q : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (hq : 0 < q)
    (hdecay : ∀ (g : Multiplicative (Site d)) (φ : ℕ → ℕ), StrictMono φ →
        WeakConvergesTo (fun n => freeFiniteMeasure d (φ n) hp hp1 hq)
          (freeInfiniteVolume d hp hp1 hq) →
        ivt_freeIntegralShiftDecay hp hp1 hq g φ) :
    ConfigSpace.IsTranslationInvariant (G := Multiplicative (Site d))
      (freeInfiniteVolume d hp hp1 hq : Measure (ConfigSpace (Sym2 (Site d))))

Uses 12 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Translation-invariant measure on configuration space · Free random-cluster measure on a box · Free infinite-volume random-cluster measure · Free integral shift decay along a box sequence · Site of the hypercubic lattice · Weak convergence of probability measures on configuration space

Proof usesShift of a configuration by a group element · Translated free box measure · Free infinite-volume measure is a subsequential weak limit · Weak convergence implies convergence of integrals · Convergence of integrals implies weak convergence

Used byFree translation invariance from decay on a dense set

LemmaIdentity shift satisfies the wired decay hypothesis#✓fully proved

The identity shift satisfies the wired decay hypothesis, so it is not vacuous.

lemma ivt_wiredIntegralShiftDecay_one {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q)
    (φ : ℕ → ℕ) : ivt_wiredIntegralShiftDecay hp hp1 hq (1 : Multiplicative (Site d)) φ

Uses 5

Statement usesWired integral shift decay along a box sequence · Site of the hypercubic lattice

Proof usesConfiguration space of a statistical-mechanics model · Shift of a configuration by a group element · Wired random-cluster measure on a box

LemmaIdentity shift satisfies the free decay hypothesis#✓fully proved

The identity shift satisfies the free decay hypothesis, so it is not vacuous.

lemma ivt_freeIntegralShiftDecay_one {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q)
    (φ : ℕ → ℕ) : ivt_freeIntegralShiftDecay hp hp1 hq (1 : Multiplicative (Site d)) φ

Uses 5

Statement usesFree integral shift decay along a box sequence · Site of the hypercubic lattice

Proof usesConfiguration space of a statistical-mechanics model · Shift of a configuration by a group element · Free random-cluster measure on a box

DefinitionShift-decay functional of a sequence of measures#✓fully proved

The difference ∫ f dμ_n - ∫ f ∘ θ_g dμ_n between the integrals of f and of its shift by g against the n-th measure.

noncomputable def isd_decayFun (μ : ℕ → ProbabilityMeasure (ConfigSpace (Sym2 (Site d))))
    (g : Multiplicative (Site d)) (f : (ConfigSpace (Sym2 (Site d))) →ᵇ ℝ) (n : ℕ) : ℝ :=
  (∫ x, f x ∂(μ n : Measure _)) - (∫ x, f (shift g x) ∂(μ n : Measure _))

Uses 3 · Used by 16

Statement usesConfiguration space of a statistical-mechanics model · Shift of a configuration by a group element · Site of the hypercubic lattice

Used byFree translation invariance from free placements of every shift · Wired translation invariance from wired placements of every shift · Submodule of functions with vanishing free shift decay · Submodule of functions with vanishing wired shift decay · Cylinder decay along the free box measures · Translation invariance of the free FK measure from cylinder decay · Decay of the edge-indicator functional from equal wired densities · Cylinder decay along the wired box measures · Translation invariance of the wired FK measure from cylinder decay · Free shift decay on a dense set of test functions · Free translation invariance from decay on a dense set · Shift decay extends from a dense set of test functions · Wired shift decay on a dense set of test functions · Wired translation invariance from decay on a dense set · Free translation invariance from the placement hypothesis · Wired translation invariance from the placement hypothesis

LemmaShift decay extends from a dense set of test functions#✓fully proved

If D_n(f') → 0 for all f' in a dense set of bounded continuous functions, then D_n(f) → 0 for every bounded continuous f. This is the equicontinuity argument of EquicontinuousAt.tendsto_of_mem_closure, specialized to the uniformly Lipschitz family f ↦ D_n(f).

lemma isd_tendsto_decay_of_dense (μ : ℕ → ProbabilityMeasure (ConfigSpace (Sym2 (Site d))))
    (g : Multiplicative (Site d)) {D : Set ((ConfigSpace (Sym2 (Site d))) →ᵇ ℝ)}
    (hD : Dense D)
    (hdecay : ∀ f' ∈ D, Tendsto (isd_decayFun μ g f') atTop (𝓝 0))
    (f : (ConfigSpace (Sym2 (Site d))) →ᵇ ℝ) :
    Tendsto (isd_decayFun μ g f) atTop (𝓝 0)

Uses 4 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Shift-decay functional of a sequence of measures · Site of the hypercubic lattice

Proof usesShift of a configuration by a group element

Used byFree translation invariance from decay on a dense set · Wired translation invariance from decay on a dense set

DefinitionWired shift decay on a dense set of test functions#✓fully proved

Decay of D_n along the wired box measures φ^1_{Λ_{φ(n)}} on some dense set of bounded continuous functions.

def isd_wiredDenseDecay {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q)
    (g : Multiplicative (Site d)) (φ : ℕ → ℕ) : Prop :=
  ∃ D : Set ((ConfigSpace (Sym2 (Site d))) →ᵇ ℝ), Dense D ∧
    ∀ f' ∈ D,
      Tendsto (isd_decayFun (fun n => wiredFiniteMeasure d (φ n) hp hp1 hq) g f')
        atTop (𝓝 0)

Uses 4 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Shift-decay functional of a sequence of measures · Wired random-cluster measure on a box · Site of the hypercubic lattice

Used byTranslation invariance of the wired FK measure from cylinder decay · Wired translation invariance from decay on a dense set

DefinitionFree shift decay on a dense set of test functions#✓fully proved

Decay of D_n along the free box measures φ^0_{Λ_{φ(n)}} on some dense set of bounded continuous functions.

def isd_freeDenseDecay {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q)
    (g : Multiplicative (Site d)) (φ : ℕ → ℕ) : Prop :=
  ∃ D : Set ((ConfigSpace (Sym2 (Site d))) →ᵇ ℝ), Dense D ∧
    ∀ f' ∈ D,
      Tendsto (isd_decayFun (fun n => freeFiniteMeasure d (φ n) hp hp1 hq) g f')
        atTop (𝓝 0)

Uses 4 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Free random-cluster measure on a box · Shift-decay functional of a sequence of measures · Site of the hypercubic lattice

Used byTranslation invariance of the free FK measure from cylinder decay · Free translation invariance from decay on a dense set

LemmaWired translation invariance from decay on a dense set#✓fully proved

The wired infinite-volume FK measure is translation invariant if, for every shift and every convergent box subsequence, D_n decays on a dense set. See also flc_wiredIV_isTranslationInvariant (unconditional for q = 2).

lemma isd_wiredIV_isTranslationInvariant_of_denseDecay {p q : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (hq : 0 < q)
    (hdense : ∀ (g : Multiplicative (Site d)) (φ : ℕ → ℕ), StrictMono φ →
        WeakConvergesTo (fun n => wiredFiniteMeasure d (φ n) hp hp1 hq)
          (wiredInfiniteVolume d hp hp1 hq) →
        isd_wiredDenseDecay hp hp1 hq g φ) :
    ConfigSpace.IsTranslationInvariant (G := Multiplicative (Site d))
      (wiredInfiniteVolume d hp hp1 hq : Measure (ConfigSpace (Sym2 (Site d))))

Uses 11 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Translation-invariant measure on configuration space · Wired shift decay on a dense set of test functions · Wired random-cluster measure on a box · Wired infinite-volume random-cluster measure · Site of the hypercubic lattice · Weak convergence of probability measures on configuration space

Proof usesShift-decay functional of a sequence of measures · Shift decay extends from a dense set of test functions · Wired translation invariance from integral shift decay · Wired integral shift decay along a box sequence

Used byTranslation invariance of the wired FK measure from cylinder decay

LemmaFree translation invariance from decay on a dense set#✓fully proved

The free infinite-volume FK measure is translation invariant if, for every shift and every convergent box subsequence, D_n decays on a dense set. See also bdp_freeIV_isTranslationInvariant (unconditional for q = 2).

lemma isd_freeIV_isTranslationInvariant_of_denseDecay {p q : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (hq : 0 < q)
    (hdense : ∀ (g : Multiplicative (Site d)) (φ : ℕ → ℕ), StrictMono φ →
        WeakConvergesTo (fun n => freeFiniteMeasure d (φ n) hp hp1 hq)
          (freeInfiniteVolume d hp hp1 hq) →
        isd_freeDenseDecay hp hp1 hq g φ) :
    ConfigSpace.IsTranslationInvariant (G := Multiplicative (Site d))
      (freeInfiniteVolume d hp hp1 hq : Measure (ConfigSpace (Sym2 (Site d))))

Uses 11 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Translation-invariant measure on configuration space · Free random-cluster measure on a box · Free infinite-volume random-cluster measure · Free shift decay on a dense set of test functions · Site of the hypercubic lattice · Weak convergence of probability measures on configuration space

Proof usesShift-decay functional of a sequence of measures · Shift decay extends from a dense set of test functions · Free translation invariance from integral shift decay · Free integral shift decay along a box sequence

Used byTranslation invariance of the free FK measure from cylinder decay

DefinitionEdge-open indicator as a continuous function#✓fully proved

The indicator ω ↦ 1{ω_e = 1} of the edge e being open, as a continuous function.

noncomputable def idc_coordCM (e : Sym2 (Site d)) : C(ConfigSpace (Sym2 (Site d)), ℝ) :=
  ⟨fun ω => if ω e then (1 : ℝ) else 0,
    (continuous_of_discreteTopology (f := fun b : Bool => if b then (1 : ℝ) else 0)).comp
      (continuous_apply e)⟩

Uses 2 · Used by 8

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice

Used byFree translation invariance from free placements of every shift · Wired translation invariance from wired placements of every shift · Continuous monomial indicator that every edge of a set is open · Edge-open indicator as a bounded continuous function · Cylinder algebra generated by edge indicators · Density of cylinder functions among bounded continuous functions · Free translation invariance from the placement hypothesis · Wired translation invariance from the placement hypothesis

DefinitionEdge-open indicator as a bounded continuous function#✓fully proved

The edge indicator ω ↦ 1{ω_e = 1} as a bounded continuous function.

noncomputable def idc_coordBcf (e : Sym2 (Site d)) : ConfigSpace (Sym2 (Site d)) →ᵇ ℝ :=
  BoundedContinuousFunction.mkOfCompact (idc_coordCM e)

Uses 3 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Edge-open indicator as a continuous function · Site of the hypercubic lattice

Used byFree box integral of an edge indicator is the free edge marginal · Wired box integral of an edge indicator is the wired edge marginal · Decay of the edge-indicator functional from equal wired densities

LemmaWired box integral of an edge indicator is the wired edge marginal#✓fully proved

The integral of the indicator of a box edge against the wired box measure on Λ_m is the wired edge marginal.

lemma idc_integral_coordBcf_wired (N m : ℕ) (hNm : N ≤ m) (eb : Sym2 (boxVerts d N))
    {p : ℝ} (hp : 0 < p) (hp1 : p < 1) :
    (∫ ω, idc_coordBcf (edgeIncl d N eb) ω
        ∂((wiredFiniteMeasure d m hp hp1 (by norm_num : (0 : ℝ) < 2)
          : ProbabilityMeasure _) : Measure _))
      = edgeMargProb (wiredFkProb (boxGraph d m) (boxBoundary d m) p 2) (innerEdgeLE d hNm eb)

Uses 17

Statement usesConfiguration space of a statistical-mechanics model · Vertex boundary of a box · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Edge marginal of a mass function · Edge-open indicator as a bounded continuous function · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Wired random-cluster measure on a box · Wired random-cluster probability of a configuration · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesEvent that a box edge is open · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Restriction of a configuration from \(\Lambda_m\) to \(\Lambda_n\) · Restriction to \(\Lambda_n\) factors through \(\Lambda_m\) · Wired \(\Lambda_m\) measure of a \(\Lambda_m\) cylinder event as a sum

LemmaFree box integral of an edge indicator is the free edge marginal#✓fully proved

The integral of the indicator of a box edge against the free box measure on Λ_m is the free edge marginal.

lemma idc_integral_coordBcf_free (N m : ℕ) (hNm : N ≤ m) (eb : Sym2 (boxVerts d N))
    {p : ℝ} (hp : 0 < p) (hp1 : p < 1) :
    (∫ ω, idc_coordBcf (edgeIncl d N eb) ω
        ∂((freeFiniteMeasure d m hp hp1 (by norm_num : (0 : ℝ) < 2)
          : ProbabilityMeasure _) : Measure _))
      = edgeMargProb (fkProb (boxGraph d m) p 2) (innerEdgeLE d hNm eb)

Uses 16

Statement usesConfiguration space of a statistical-mechanics model · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Edge marginal of a mass function · Probability of an ambient FK configuration · Free random-cluster measure on a box · Edge-open indicator as a bounded continuous function · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesEvent that a box edge is open · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Restriction of a configuration from \(\Lambda_m\) to \(\Lambda_n\) · Restriction to \(\Lambda_n\) factors through \(\Lambda_m\) · Free box measure of a cylinder event as a finite sum

LemmaDecay of the edge-indicator functional from equal wired densities#✓fully proved

If the box edge e and its shift g⁻¹ e have the same wired q = 2 density, the decay functional of the indicator of e along the wired box measures tends to zero.

lemma idc_wired_coord_decay_of_density_eq (N : ℕ) (eb eb' : Sym2 (boxVerts d N))
    (g : Multiplicative (Site d)) {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (hshift : g⁻¹ • (edgeIncl d N eb) = edgeIncl d N eb')
    (hdens : wiredEdgeDensity d 2 (edgeIncl d N eb) p
      = wiredEdgeDensity d 2 (edgeIncl d N eb') p) :
    Tendsto (isd_decayFun (fun m => wiredFiniteMeasure d m hp hp1 (by norm_num : (0 : ℝ) < 2))
        g (idc_coordBcf (edgeIncl d N eb))) atTop (𝓝 0)

Uses 15

Statement usesVertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Edge-open indicator as a bounded continuous function · Shift-decay functional of a sequence of measures · Wired infinite-volume edge density · Wired random-cluster measure on a box · Site of the hypercubic lattice

Proof usesConfiguration space of a statistical-mechanics model · Shift of a configuration by a group element · Event that a box edge is open · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Event that an edge is open · Wired infinite-volume measure as limit on increasing cylinder events · Wired infinite-volume random-cluster measure · Increasing event

DefinitionCylinder algebra generated by edge indicators#✓fully proved

The subalgebra of continuous functions generated by the edge indicators.

noncomputable def idc_cylinderAlg (d : ℕ) : Subalgebra ℝ C(ConfigSpace (Sym2 (Site d)), ℝ) :=
  Algebra.adjoin ℝ (Set.range (idc_coordCM (d := d)))

Uses 3 · Used by 6

Statement usesConfiguration space of a statistical-mechanics model · Edge-open indicator as a continuous function · Site of the hypercubic lattice

Used byFree translation invariance from free placements of every shift · Wired translation invariance from wired placements of every shift · Cylinder algebra as bounded continuous functions · Density of cylinder functions among bounded continuous functions · Free translation invariance from the placement hypothesis · Wired translation invariance from the placement hypothesis

DefinitionCylinder algebra as bounded continuous functions#✓fully proved

The cylinder algebra viewed as a set of bounded continuous functions.

noncomputable def idc_cylinderBcfSet (d : ℕ) : Set (ConfigSpace (Sym2 (Site d)) →ᵇ ℝ) :=
  BoundedContinuousFunction.mkOfCompact ''
    (idc_cylinderAlg d : Set C(ConfigSpace (Sym2 (Site d)), ℝ))

Uses 3 · Used by 9

Statement usesConfiguration space of a statistical-mechanics model · Cylinder algebra generated by edge indicators · Site of the hypercubic lattice

Used byFree translation invariance from free placements of every shift · Wired translation invariance from wired placements of every shift · Density of cylinder functions among bounded continuous functions · Cylinder decay along the free box measures · Translation invariance of the free FK measure from cylinder decay · Cylinder decay along the wired box measures · Translation invariance of the wired FK measure from cylinder decay · Free translation invariance from the placement hypothesis · Wired translation invariance from the placement hypothesis

LemmaDensity of cylinder functions among bounded continuous functions#✓fully proved

The cylinder functions are dense in the bounded continuous functions, by Stone–Weierstrass on the compact configuration space.

lemma idc_cylinderBcfSet_dense (d : ℕ) : Dense (idc_cylinderBcfSet d)

Uses 5 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Cylinder algebra as bounded continuous functions · Site of the hypercubic lattice

Proof usesEdge-open indicator as a continuous function · Cylinder algebra generated by edge indicators

Used byTranslation invariance of the free FK measure from cylinder decay · Translation invariance of the wired FK measure from cylinder decay

DefinitionCylinder decay along the wired box measures#✓fully proved

The decay functional tends to zero along the wired box measures for every cylinder function.

def idc_wiredCylinderDecay {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q)
    (g : Multiplicative (Site d)) (φ : ℕ → ℕ) : Prop :=
  ∀ f ∈ idc_cylinderBcfSet d,
    Tendsto (isd_decayFun (fun n => wiredFiniteMeasure d (φ n) hp hp1 hq) g f) atTop (𝓝 0)

Uses 5 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Cylinder algebra as bounded continuous functions · Shift-decay functional of a sequence of measures · Wired random-cluster measure on a box · Site of the hypercubic lattice

Used byWired translation invariance from wired placements of every shift · Translation invariance of the wired FK measure from cylinder decay · Wired translation invariance from the placement hypothesis

DefinitionCylinder decay along the free box measures#✓fully proved

The decay functional tends to zero along the free box measures for every cylinder function.

def idc_freeCylinderDecay {p q : ℝ} (hp : 0 < p) (hp1 : p < 1) (hq : 0 < q)
    (g : Multiplicative (Site d)) (φ : ℕ → ℕ) : Prop :=
  ∀ f ∈ idc_cylinderBcfSet d,
    Tendsto (isd_decayFun (fun n => freeFiniteMeasure d (φ n) hp hp1 hq) g f) atTop (𝓝 0)

Uses 5 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Free random-cluster measure on a box · Cylinder algebra as bounded continuous functions · Shift-decay functional of a sequence of measures · Site of the hypercubic lattice

Used byFree translation invariance from free placements of every shift · Translation invariance of the free FK measure from cylinder decay · Free translation invariance from the placement hypothesis

LemmaTranslation invariance of the wired FK measure from cylinder decay#✓fully proved

The wired infinite-volume FK measure is translation invariant if cylinder decay holds for every shift and every convergent box subsequence. See also flc_wiredIV_isTranslationInvariant (unconditional for q = 2).

lemma idc_wiredIV_isTranslationInvariant_of_cylinderDecay {p q : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (hq : 0 < q)
    (hcyl : ∀ (g : Multiplicative (Site d)) (φ : ℕ → ℕ), StrictMono φ →
        WeakConvergesTo (fun n => wiredFiniteMeasure d (φ n) hp hp1 hq)
          (wiredInfiniteVolume d hp hp1 hq) →
        idc_wiredCylinderDecay hp hp1 hq g φ) :
    ConfigSpace.IsTranslationInvariant (G := Multiplicative (Site d))
      (wiredInfiniteVolume d hp hp1 hq : Measure (ConfigSpace (Sym2 (Site d))))

Uses 12 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Translation-invariant measure on configuration space · Cylinder decay along the wired box measures · Wired random-cluster measure on a box · Wired infinite-volume random-cluster measure · Site of the hypercubic lattice · Weak convergence of probability measures on configuration space

Proof usesCylinder algebra as bounded continuous functions · Density of cylinder functions among bounded continuous functions · Shift-decay functional of a sequence of measures · Wired shift decay on a dense set of test functions · Wired translation invariance from decay on a dense set

Used byWired translation invariance from wired placements of every shift · Wired translation invariance from the placement hypothesis

LemmaTranslation invariance of the free FK measure from cylinder decay#✓fully proved

The free infinite-volume FK measure is translation invariant if cylinder decay holds for every shift and every convergent box subsequence. See also bdp_freeIV_isTranslationInvariant (unconditional for q = 2).

lemma idc_freeIV_isTranslationInvariant_of_cylinderDecay {p q : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (hq : 0 < q)
    (hcyl : ∀ (g : Multiplicative (Site d)) (φ : ℕ → ℕ), StrictMono φ →
        WeakConvergesTo (fun n => freeFiniteMeasure d (φ n) hp hp1 hq)
          (freeInfiniteVolume d hp hp1 hq) →
        idc_freeCylinderDecay hp hp1 hq g φ) :
    ConfigSpace.IsTranslationInvariant (G := Multiplicative (Site d))
      (freeInfiniteVolume d hp hp1 hq : Measure (ConfigSpace (Sym2 (Site d))))

Uses 12 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Translation-invariant measure on configuration space · Free random-cluster measure on a box · Free infinite-volume random-cluster measure · Cylinder decay along the free box measures · Site of the hypercubic lattice · Weak convergence of probability measures on configuration space

Proof usesCylinder algebra as bounded continuous functions · Density of cylinder functions among bounded continuous functions · Shift-decay functional of a sequence of measures · Free shift decay on a dense set of test functions · Free translation invariance from decay on a dense set

Used byFree translation invariance from free placements of every shift · Free translation invariance from the placement hypothesis

DefinitionTranslation of \(\mathbb{Z}^d\) by a vector#✓fully proved

Translation x ↦ x + v as a permutation of ℤ^d.

def fktc_translate (v : Site d) : Site d ≃ Site d where
  toFun := fun x => x + v
  invFun := fun x => x - v
  left_inv := by intro x; funext i; simp
  right_inv := by intro x; funext i; simp

Uses 1 · Used by 8

Statement usesSite of the hypercubic lattice

Used byAizenman–Barsky inequality on \(\mathbb{Z}^d\) · Aizenman–Barsky inequality on \(\mathbb{Z}^d\) with neighbour row sum · Translation invariance of free and wired densities if marginals merge · An edge and its translate lie in a common centered box · Translation invariance of the free density given merging marginals · A site and its translate lie in a common centered box · Unit translations are not box symmetries · Translation invariance of the wired density given merging marginals

LemmaUnit translations are not box symmetries#✓fully proved

Translation by a unit vector does not preserve the centered boxes, so it is not a BoxSym.

lemma fktc_translate_not_box_mem (j : Fin d) :
    ¬ (∀ n x, fktc_translate (fun i => if i = j then (1:ℤ) else 0) x ∈ box d n
        ↔ x ∈ box d n)

Uses 3

Statement usesTranslation of \(\mathbb{Z}^d\) by a vector · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

LemmaA site and its translate lie in a common centered box#✓fully proved

A site and its translate lie in a common centered box.

lemma fktc_point_and_translate_in_box (v x : Site d) :
    ∃ N, x ∈ box d N ∧ fktc_translate v x ∈ box d N

Uses 3

Statement usesTranslation of \(\mathbb{Z}^d\) by a vector · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

LemmaAn edge and its translate lie in a common centered box#✓fully proved

The endpoints of an edge and of its translate lie in a common centered box.

lemma fktc_edge_and_translate_in_box (v x y : Site d) :
    ∃ N, x ∈ box d N ∧ y ∈ box d N ∧
      fktc_translate v x ∈ box d N ∧ fktc_translate v y ∈ box d N

Uses 3

Statement usesTranslation of \(\mathbb{Z}^d\) by a vector · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

DefinitionUnordered pair of two sites of a box \(\Lambda_N\)#✓fully proved

The pair {x, y} as an element of Sym2 Λ_N, for sites x, y ∈ Λ_N.

def fktc_boxEdge {N : ℕ} {x y : Site d} (hx : x ∈ box d N) (hy : y ∈ box d N) :
    Sym2 (boxVerts d N) :=
  s(⟨x, hx⟩, ⟨y, hy⟩)

Uses 3 · Used by 3

Statement usesVertices of the box \((-n, n)^d\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byTranslation invariance of free and wired densities if marginals merge · Translation invariance of the free density given merging marginals · Translation invariance of the wired density given merging marginals

LemmaWired edge density is constant on orbits of a box symmetry#✓fully proved

The wired edge density is constant on each orbit of a box symmetry.

lemma fktc_wired_box_density_const_of_orbit (S : BoxSym d) (N : ℕ)
    (EB : Finset (Sym2 (boxVerts d N))) (eb₀ : Sym2 (boxVerts d N)) {p : ℝ}
    (hp : 0 < p) (hp1 : p < 1)
    (horb : ∀ eb ∈ EB, ∃ k : ℕ, eb = (Sym2.map (S.lift N))^[k] eb₀) :
    ∀ eb ∈ EB, wiredEdgeDensity d 2 (edgeIncl d N eb) p
      = wiredEdgeDensity d 2 (edgeIncl d N eb₀) p

Uses 6 · Used by 1

Statement usesBox symmetry of \(\mathbb{Z}^d\) · Restriction of a box symmetry to a box · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Wired infinite-volume edge density

Proof usesBox symmetries preserve the wired \(q = 2\) density of box edges

Used byWired lower bound on expected open edges along a box-symmetry orbit

LemmaFree edge density is constant on orbits of a box symmetry#✓fully proved

The free edge density is constant on each orbit of a box symmetry.

lemma fktc_free_box_density_const_of_orbit (S : BoxSym d) (N : ℕ)
    (EB : Finset (Sym2 (boxVerts d N))) (eb₀ : Sym2 (boxVerts d N)) {p : ℝ}
    (hp : 0 < p) (hp1 : p < 1)
    (horb : ∀ eb ∈ EB, ∃ k : ℕ, eb = (Sym2.map (S.lift N))^[k] eb₀) :
    ∀ eb ∈ EB, freeEdgeDensity d 2 (edgeIncl d N eb) p
      = freeEdgeDensity d 2 (edgeIncl d N eb₀) p

Uses 6 · Used by 1

Statement usesBox symmetry of \(\mathbb{Z}^d\) · Restriction of a box symmetry to a box · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Free infinite-volume edge density

Proof usesBox symmetries preserve the free \(q = 2\) density of box edges

Used byFree upper bound on expected open edges along a box-symmetry orbit

LemmaEqual wired densities from merging wired marginals#✓fully proved

If the wired marginals of two box edges on Λ_{N+k} differ by a quantity tending to zero, the two edges have the same wired density.

lemma fktc_wired_density_eq_of_marg_decay (N : ℕ) (eb eb' : Sym2 (boxVerts d N))
    {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (hdecay : Tendsto (fun k =>
        edgeMargProb (wiredFkProb (boxGraph d (N + k)) (boxBoundary d (N + k)) p 2)
            (innerEdgeLE d (Nat.le_add_right N k) eb)
          - edgeMargProb (wiredFkProb (boxGraph d (N + k)) (boxBoundary d (N + k)) p 2)
            (innerEdgeLE d (Nat.le_add_right N k) eb')) atTop (𝓝 0)) :
    wiredEdgeDensity d 2 (edgeIncl d N eb) p
      = wiredEdgeDensity d 2 (edgeIncl d N eb') p

Uses 21 · Used by 1

Statement usesVertex boundary of a box · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Edge marginal of a mass function · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Wired infinite-volume edge density · Wired random-cluster probability of a configuration · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesConfiguration space of a statistical-mechanics model · Event that a box edge is open · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Restriction of a configuration from \(\Lambda_m\) to \(\Lambda_n\) · Restriction to \(\Lambda_n\) factors through \(\Lambda_m\) · Event that an edge is open · Wired infinite-volume measure as limit on increasing cylinder events · Wired random-cluster measure on a box · Wired \(\Lambda_m\) measure of a \(\Lambda_m\) cylinder event as a sum · Wired infinite-volume random-cluster measure · Increasing event

Used byTranslation invariance of the wired density given merging marginals

LemmaEqual free densities from merging free marginals#✓fully proved

If the free marginals of two box edges on Λ_{N+k} differ by a quantity tending to zero, the two edges have the same free density.

lemma fktc_free_density_eq_of_marg_decay (N : ℕ) (eb eb' : Sym2 (boxVerts d N))
    {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (hdecay : Tendsto (fun k =>
        edgeMargProb (fkProb (boxGraph d (N + k)) p 2)
            (innerEdgeLE d (Nat.le_add_right N k) eb)
          - edgeMargProb (fkProb (boxGraph d (N + k)) p 2)
            (innerEdgeLE d (Nat.le_add_right N k) eb')) atTop (𝓝 0)) :
    freeEdgeDensity d 2 (edgeIncl d N eb) p
      = freeEdgeDensity d 2 (edgeIncl d N eb') p

Uses 20 · Used by 1

Statement usesNearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Edge marginal of a mass function · Probability of an ambient FK configuration · Free infinite-volume edge density · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesConfiguration space of a statistical-mechanics model · Event that a box edge is open · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Restriction of a configuration from \(\Lambda_m\) to \(\Lambda_n\) · Restriction to \(\Lambda_n\) factors through \(\Lambda_m\) · Event that an edge is open · Free \(q=2\) box masses of increasing cylinders tend to infinite volume · Free random-cluster measure on a box · Free box measure of a cylinder event as a finite sum · Free infinite-volume random-cluster measure · Increasing event

Used byTranslation invariance of the free density given merging marginals

LemmaTranslation invariance of the wired density given merging marginals#✓fully proved

An edge and its translate have the same wired density if their wired marginals merge along the boxes. See also bdp_wiredEdgeDensity_translation_inv, which proves the conclusion without the merging hypothesis.

lemma fktc_wired_density_translation_inv (v x y : Site d) {p : ℝ}
    (hp : 0 < p) (hp1 : p < 1)
    (hcof : ∃ N, ∃ hx : x ∈ box d N, ∃ hy : y ∈ box d N,
        ∃ hx' : fktc_translate v x ∈ box d N, ∃ hy' : fktc_translate v y ∈ box d N,
      Tendsto (fun k =>
        edgeMargProb (wiredFkProb (boxGraph d (N + k)) (boxBoundary d (N + k)) p 2)
            (innerEdgeLE d (Nat.le_add_right N k) (fktc_boxEdge hx hy))
          - edgeMargProb (wiredFkProb (boxGraph d (N + k)) (boxBoundary d (N + k)) p 2)
            (innerEdgeLE d (Nat.le_add_right N k) (fktc_boxEdge hx' hy'))) atTop (𝓝 0)) :
    wiredEdgeDensity d 2 s(x, y) p
      = wiredEdgeDensity d 2 s(fktc_translate v x, fktc_translate v y) p

Uses 13 · Used by 1

Statement usesVertex boundary of a box · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Edge marginal of a mass function · Unordered pair of two sites of a box \(\Lambda_N\) · Translation of \(\mathbb{Z}^d\) by a vector · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Wired infinite-volume edge density · Wired random-cluster probability of a configuration · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesInclusion of box edges into \(\mathbb{Z}^d\) · Equal wired densities from merging wired marginals

Used byTranslation invariance of free and wired densities if marginals merge

LemmaTranslation invariance of the free density given merging marginals#✓fully proved

An edge and its translate have the same free density if their free marginals merge along the boxes. See also bdp_freeEdgeDensity_translation_inv, which proves the conclusion without the merging hypothesis.

lemma fktc_free_density_translation_inv (v x y : Site d) {p : ℝ}
    (hp : 0 < p) (hp1 : p < 1)
    (hcof : ∃ N, ∃ hx : x ∈ box d N, ∃ hy : y ∈ box d N,
        ∃ hx' : fktc_translate v x ∈ box d N, ∃ hy' : fktc_translate v y ∈ box d N,
      Tendsto (fun k =>
        edgeMargProb (fkProb (boxGraph d (N + k)) p 2)
            (innerEdgeLE d (Nat.le_add_right N k) (fktc_boxEdge hx hy))
          - edgeMargProb (fkProb (boxGraph d (N + k)) p 2)
            (innerEdgeLE d (Nat.le_add_right N k) (fktc_boxEdge hx' hy'))) atTop (𝓝 0)) :
    freeEdgeDensity d 2 s(x, y) p
      = freeEdgeDensity d 2 s(fktc_translate v x, fktc_translate v y) p

Uses 12 · Used by 1

Statement usesNearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Edge marginal of a mass function · Probability of an ambient FK configuration · Unordered pair of two sites of a box \(\Lambda_N\) · Translation of \(\mathbb{Z}^d\) by a vector · Free infinite-volume edge density · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesInclusion of box edges into \(\mathbb{Z}^d\) · Equal free densities from merging free marginals

Used byTranslation invariance of free and wired densities if marginals merge

LemmaTranslation invariance of free and wired densities if marginals merge#✓fully proved

Translation invariance of the free and wired densities of an edge under the merging hypotheses of fktc_wired_density_translation_inv and fktc_free_density_translation_inv.

StatMech.FK.fktc_density_translation_inv · 19 lines

lemma fktc_density_translation_inv (v x y : Site d) {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (hcofW : ∃ N, ∃ hx : x ∈ box d N, ∃ hy : y ∈ box d N,
        ∃ hx' : fktc_translate v x ∈ box d N, ∃ hy' : fktc_translate v y ∈ box d N,
      Tendsto (fun k =>
        edgeMargProb (wiredFkProb (boxGraph d (N + k)) (boxBoundary d (N + k)) p 2)
            (innerEdgeLE d (Nat.le_add_right N k) (fktc_boxEdge hx hy))
          - edgeMargProb (wiredFkProb (boxGraph d (N + k)) (boxBoundary d (N + k)) p 2)
            (innerEdgeLE d (Nat.le_add_right N k) (fktc_boxEdge hx' hy'))) atTop (𝓝 0))
    (hcofF : ∃ N, ∃ hx : x ∈ box d N, ∃ hy : y ∈ box d N,
        ∃ hx' : fktc_translate v x ∈ box d N, ∃ hy' : fktc_translate v y ∈ box d N,
      Tendsto (fun k =>
        edgeMargProb (fkProb (boxGraph d (N + k)) p 2)
            (innerEdgeLE d (Nat.le_add_right N k) (fktc_boxEdge hx hy))
          - edgeMargProb (fkProb (boxGraph d (N + k)) p 2)
            (innerEdgeLE d (Nat.le_add_right N k) (fktc_boxEdge hx' hy'))) atTop (𝓝 0)) :
    wiredEdgeDensity d 2 s(x, y) p
        = wiredEdgeDensity d 2 s(fktc_translate v x, fktc_translate v y) p
      ∧ freeEdgeDensity d 2 s(x, y) p
        = freeEdgeDensity d 2 s(fktc_translate v x, fktc_translate v y) p

Uses 15

Statement usesVertex boundary of a box · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Edge marginal of a mass function · Probability of an ambient FK configuration · Unordered pair of two sites of a box \(\Lambda_N\) · Translation of \(\mathbb{Z}^d\) by a vector · Free infinite-volume edge density · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Wired infinite-volume edge density · Wired random-cluster probability of a configuration · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesTranslation invariance of the free density given merging marginals · Translation invariance of the wired density given merging marginals

LemmaConstant wired density gives a lower bound on expected open edges#✓fully proved

If the wired density is constant on a set EB of box edges, |EB| times that density is at most the expected number of open edges of EB under the wired measure on any larger box.

lemma fktc_wired_density_eq_const (N n : ℕ) (hNn : N ≤ n)
    (EB : Finset (Sym2 (boxVerts d N))) (eb₀ : Sym2 (boxVerts d N)) {p : ℝ}
    (hconst : ∀ eb ∈ EB, wiredEdgeDensity d 2 (edgeIncl d N eb) p
      = wiredEdgeDensity d 2 (edgeIncl d N eb₀) p)
    (hp : 0 < p) (hp1 : p < 1) :
    (EB.card : ℝ) * wiredEdgeDensity d 2 (edgeIncl d N eb₀) p
      ≤ ∑ ω : ConfigSpace (Sym2 (boxVerts d n)),
          dfi_openEdgeCount (EB.image (innerEdgeLE d hNn)) ω
            * wiredFkProb (boxGraph d n) (boxBoundary d n) p 2 ω

Uses 24 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Vertex boundary of a box · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Number of open edges in a finite edge set · Inclusion of box edges into \(\mathbb{Z}^d\) · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Wired infinite-volume edge density · Wired random-cluster probability of a configuration · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesEvent that a box edge is open · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Restriction of a configuration from \(\Lambda_m\) to \(\Lambda_n\) · Restriction to \(\Lambda_n\) factors through \(\Lambda_m\) · Inclusion of \(\Lambda_n\) into \(\Lambda_m\) for \(n \le m\) · Edge marginal of a mass function · Event that an edge is open · Infimum of wired box probabilities of a box event · Wired infinite-volume probability equals the infimum over boxes · Wired random-cluster measure on a box · Wired \(\Lambda_m\) measure of a \(\Lambda_m\) cylinder event as a sum · Wired infinite-volume random-cluster measure · Increasing event

Used byWired lower bound on expected open edges along a box-symmetry orbit

LemmaConstant free density gives an upper bound on expected open edges#✓fully proved

If the free density is constant on a set EB of box edges, the expected number of open edges of EB under the free measure on any larger box is at most |EB| times that density.

lemma fktc_free_density_eq_const (N n : ℕ) (hNn : N ≤ n)
    (EB : Finset (Sym2 (boxVerts d N))) (eb₀ : Sym2 (boxVerts d N)) {p : ℝ}
    (hconst : ∀ eb ∈ EB, freeEdgeDensity d 2 (edgeIncl d N eb) p
      = freeEdgeDensity d 2 (edgeIncl d N eb₀) p)
    (hp : 0 < p) (hp1 : p < 1) :
    (∑ ω : ConfigSpace (Sym2 (boxVerts d n)),
          dfi_openEdgeCount (EB.image (innerEdgeLE d hNn)) ω
            * fkProb (boxGraph d n) p 2 ω)
      ≤ (EB.card : ℝ) * freeEdgeDensity d 2 (edgeIncl d N eb₀) p

Uses 24 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Number of open edges in a finite edge set · Inclusion of box edges into \(\mathbb{Z}^d\) · Probability of an ambient FK configuration · Free infinite-volume edge density · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesEvent that a box edge is open · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Restriction of a configuration from \(\Lambda_m\) to \(\Lambda_n\) · Restriction to \(\Lambda_n\) factors through \(\Lambda_m\) · Inclusion of \(\Lambda_n\) into \(\Lambda_m\) for \(n \le m\) · Edge marginal of a mass function · Event that an edge is open · Limit of free \(q = 2\) box measures of a cylinder event · Free \(q = 2\) infinite-volume mass of increasing cylinders as a box limit · Free \(q = 2\) box measures are bounded by the limit value · Free random-cluster measure on a box · Free box measure of a cylinder event as a finite sum · Free infinite-volume random-cluster measure · Increasing event

Used byFree upper bound on expected open edges along a box-symmetry orbit

LemmaWired lower bound on expected open edges along a box-symmetry orbit#✓fully proved

fktc_wired_density_eq_const for a set of edges contained in one orbit of a box symmetry.

lemma fktc_wired_density_eq_const_orbit (S : BoxSym d) (N n : ℕ) (hNn : N ≤ n)
    (EB : Finset (Sym2 (boxVerts d N))) (eb₀ : Sym2 (boxVerts d N)) {p : ℝ}
    (hp : 0 < p) (hp1 : p < 1)
    (horb : ∀ eb ∈ EB, ∃ k : ℕ, eb = (Sym2.map (S.lift N))^[k] eb₀) :
    (EB.card : ℝ) * wiredEdgeDensity d 2 (edgeIncl d N eb₀) p
      ≤ ∑ ω : ConfigSpace (Sym2 (boxVerts d n)),
          dfi_openEdgeCount (EB.image (innerEdgeLE d hNn)) ω
            * wiredFkProb (boxGraph d n) (boxBoundary d n) p 2 ω

Uses 15

Statement usesConfiguration space of a statistical-mechanics model · Box symmetry of \(\mathbb{Z}^d\) · Restriction of a box symmetry to a box · Vertex boundary of a box · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Number of open edges in a finite edge set · Inclusion of box edges into \(\mathbb{Z}^d\) · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Wired infinite-volume edge density · Wired random-cluster probability of a configuration · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesWired edge density is constant on orbits of a box symmetry · Constant wired density gives a lower bound on expected open edges

LemmaFree upper bound on expected open edges along a box-symmetry orbit#✓fully proved

fktc_free_density_eq_const for a set of edges contained in one orbit of a box symmetry.

lemma fktc_free_density_eq_const_orbit (S : BoxSym d) (N n : ℕ) (hNn : N ≤ n)
    (EB : Finset (Sym2 (boxVerts d N))) (eb₀ : Sym2 (boxVerts d N)) {p : ℝ}
    (hp : 0 < p) (hp1 : p < 1)
    (horb : ∀ eb ∈ EB, ∃ k : ℕ, eb = (Sym2.map (S.lift N))^[k] eb₀) :
    (∑ ω : ConfigSpace (Sym2 (boxVerts d n)),
          dfi_openEdgeCount (EB.image (innerEdgeLE d hNn)) ω
            * fkProb (boxGraph d n) p 2 ω)
      ≤ (EB.card : ℝ) * freeEdgeDensity d 2 (edgeIncl d N eb₀) p

Uses 14

Statement usesConfiguration space of a statistical-mechanics model · Box symmetry of \(\mathbb{Z}^d\) · Restriction of a box symmetry to a box · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Number of open edges in a finite edge set · Inclusion of box edges into \(\mathbb{Z}^d\) · Probability of an ambient FK configuration · Free infinite-volume edge density · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesFree edge density is constant on orbits of a box symmetry · Constant free density gives an upper bound on expected open edges

DefinitionEvent that every edge of a finite set is open#✓fully proved

The event that every edge of s is open. Equal to fmu_multiOpen (see ftb_fmu_eq_cdc_multiOpen).

def cdc_multiOpenEvent (s : Finset (Sym2 (Site d))) :
    Set (ConfigSpace (Sym2 (Site d))) :=
  {ω | ∀ e ∈ s, ω e = true}

Uses 2 · Used by 32

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice

Used byWired box measure of an all-open event equals its box mass · Wired all-open probabilities converge to the infinite-volume value · Free box measure of an all-open event equals its box mass · Free all-open probabilities converge to the infinite-volume value · Free translation invariance from free placements of every shift · Equal free probabilities from eventually equal translated masses · Wired translation invariance from wired placements of every shift · Equal wired probabilities from eventually equal translated masses · Translation invariance of the free \(q = 2\) infinite-volume measure · Ergodicity of the wired random-cluster measure · Free \(q = 2\) multi-edge homogeneity under a translation · Wired \(q = 2\) multi-edge homogeneity under a translation · Translation invariance of the wired \(q = 2\) infinite-volume measure · Wired box products approximate infinite-volume products · Upper decorrelation of the wired measure from factorization · Wired \(q = 2\) measure is ergodic under the factorization bound · Domain monotonicity of wired multi-open probabilities · Free translation invariance from the placement hypothesis · Free placement gives shift homogeneity on all-open events · Equal free probabilities for \(t\) and \(v + t\) from matching box limits · Free placement hypothesis for a shift via box-mass limits · Identity shift satisfies the free placement hypothesis · Translated wired box mass equals the centered box mass · Translated free box mass equals the centred box probability · Translated free box masses converge to the free infinite-volume value · Translated wired box masses converge to the infinite-volume mass · Wired translation invariance from the placement hypothesis · Wired placement gives shift homogeneity on all-open events · Wired shift invariance of an all-open event from matching limits · Wired shift invariance of an all-open event from decaying differences · Wired placement hypothesis for a shift · Identity shift satisfies the wired placement hypothesis

DefinitionContinuous monomial indicator that every edge of a set is open#✓fully proved

The continuous function ω ↦ ∏_{e ∈ s} ω(e), the indicator of cdc_multiOpenEvent s.

noncomputable def cdc_monomialCM (s : Finset (Sym2 (Site d))) :
    C(ConfigSpace (Sym2 (Site d)), ℝ) :=
  ∏ e ∈ s, idc_coordCM e

Uses 3 · Used by 5

Statement usesConfiguration space of a statistical-mechanics model · Edge-open indicator as a continuous function · Site of the hypercubic lattice

Used byFree translation invariance from free placements of every shift · Wired translation invariance from wired placements of every shift · Monomial indicator as a bounded continuous function · Free translation invariance from the placement hypothesis · Wired translation invariance from the placement hypothesis

DefinitionMonomial indicator as a bounded continuous function#✓fully proved

cdc_monomialCM s as a bounded continuous function.

noncomputable def cdc_monomialBcf (s : Finset (Sym2 (Site d))) :
    ConfigSpace (Sym2 (Site d)) →ᵇ ℝ :=
  BoundedContinuousFunction.mkOfCompact (cdc_monomialCM s)

Uses 3 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Continuous monomial indicator that every edge of a set is open · Site of the hypercubic lattice

Used byFree translation invariance from free placements of every shift · Wired translation invariance from wired placements of every shift · Free translation invariance from the placement hypothesis · Wired translation invariance from the placement hypothesis

DefinitionEvent that every edge of a set of box edges is open, on a box#✓fully proved

The event that every edge of t ⊆ E(Λ_N) is open, on configurations of Λ_N.

def cdc_boxMultiOpenEvent (N : ℕ) (t : Finset (Sym2 (boxVerts d N))) :
    Set (ConfigSpace (Sym2 (boxVerts d N))) :=
  {σ | ∀ eb ∈ t, σ eb = true}

Uses 2 · Used by 14

Statement usesConfiguration space of a statistical-mechanics model · Vertices of the box \((-n, n)^d\)

Used byWired box measure of an all-open event equals its box mass · Wired all-open probabilities converge to the infinite-volume value · Free box measure of an all-open event equals its box mass · Free all-open probabilities converge to the infinite-volume value · Free translation invariance from free placements of every shift · Wired translation invariance from wired placements of every shift · Ergodicity of the wired random-cluster measure · Disjoint-box cap hypothesis for multi-open events · Wired box products approximate infinite-volume products · Upper decorrelation of the wired measure from factorization · Wired \(q = 2\) measure is ergodic under the factorization bound · Domain monotonicity of wired multi-open probabilities · Free translation invariance from the placement hypothesis · Wired translation invariance from the placement hypothesis

DefinitionWired \(q = 2\) multi-edge homogeneity under a translation#✓fully proved

The wired q = 2 infinite-volume measure gives every multi-open event the same mass as its translate by g⁻¹.

def cdc_wiredMultiHomogeneous {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (g : Multiplicative (Site d)) : Prop :=
  ∀ s : Finset (Sym2 (Site d)),
    (wiredInfiniteVolume d hp hp1 (by norm_num : (0 : ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d)))).real (cdc_multiOpenEvent s)
      = (wiredInfiniteVolume d hp hp1 (by norm_num : (0 : ℝ) < 2)
          : Measure (ConfigSpace (Sym2 (Site d)))).real
            (cdc_multiOpenEvent (s.image (fun e => g⁻¹ • e)))

Uses 4 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Event that every edge of a finite set is open · Wired infinite-volume random-cluster measure · Site of the hypercubic lattice

Used byWired translation invariance from wired placements of every shift · Wired translation invariance from the placement hypothesis · Wired placement gives shift homogeneity on all-open events · Wired infinite-volume measure is homogeneous under the identity shift

DefinitionFree \(q = 2\) multi-edge homogeneity under a translation#✓fully proved

The free q = 2 infinite-volume measure gives every multi-open event the same mass as its translate by g⁻¹.

def cdc_freeMultiHomogeneous {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (g : Multiplicative (Site d)) : Prop :=
  ∀ s : Finset (Sym2 (Site d)),
    (freeInfiniteVolume d hp hp1 (by norm_num : (0 : ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d)))).real (cdc_multiOpenEvent s)
      = (freeInfiniteVolume d hp hp1 (by norm_num : (0 : ℝ) < 2)
          : Measure (ConfigSpace (Sym2 (Site d)))).real
            (cdc_multiOpenEvent (s.image (fun e => g⁻¹ • e)))

Uses 4 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Event that every edge of a finite set is open · Free infinite-volume random-cluster measure · Site of the hypercubic lattice

Used byFree translation invariance from free placements of every shift · Free translation invariance from the placement hypothesis · Free placement gives shift homogeneity on all-open events · Free infinite-volume measure is homogeneous under the identity shift

DefinitionSubmodule of functions with vanishing wired shift decay#✓fully proved

The continuous functions whose shift-decay functional along the wired box measures (on the subsequence φ) tends to 0, as a submodule.

StatMech.FK.cdc_wiredDecaySet · 29 lines

noncomputable def cdc_wiredDecaySet {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (g : Multiplicative (Site d)) (φ : ℕ → ℕ) :
    Submodule ℝ C(ConfigSpace (Sym2 (Site d)), ℝ) where
  carrier := {h | Tendsto (isd_decayFun
      (fun n => wiredFiniteMeasure d (φ n) hp hp1 (by norm_num : (0 : ℝ) < 2)) g
      (BoundedContinuousFunction.mkOfCompact h)) atTop (𝓝 0)}
  add_mem' {h h'} hh hh' := by
    simp only [Set.mem_ofPred_eq] at hh hh' ⊢
    have hsum := hh.add hh'
    rw [add_zero] at hsum
    refine hsum.congr (fun n => ?_)
    rw [BoundedContinuousFunction.mkOfCompact_add, cdc_decayFun_add]
  zero_mem' := by
    simp only [Set.mem_ofPred_eq]
    have hz : isd_decayFun
        (fun n => wiredFiniteMeasure d (φ n) hp hp1 (by norm_num : (0 : ℝ) < 2)) g
        (BoundedContinuousFunction.mkOfCompact (0 : C(ConfigSpace (Sym2 (Site d)), ℝ)))
      = fun _ => (0 : ℝ) := by
      funext n
      rw [BoundedContinuousFunction.mkOfCompact_zero, cdc_decayFun_zero]
    rw [hz]; exact tendsto_const_nhds
  smul_mem' c h hh := by
    simp only [Set.mem_ofPred_eq] at hh ⊢
    have hsmul := hh.const_mul c
    rw [mul_zero] at hsmul
    refine hsmul.congr (fun n => ?_)
    have hms : BoundedContinuousFunction.mkOfCompact (c • h)
        = c • BoundedContinuousFunction.mkOfCompact h := rfl
    rw [hms, cdc_decayFun_smul]

Uses 5 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Shift of a configuration by a group element · Shift-decay functional of a sequence of measures · Wired random-cluster measure on a box · Site of the hypercubic lattice

Used byWired translation invariance from wired placements of every shift · Wired translation invariance from the placement hypothesis

DefinitionSubmodule of functions with vanishing free shift decay#✓fully proved

The continuous functions whose shift-decay functional along the free box measures (on the subsequence φ) tends to 0, as a submodule.

StatMech.FK.cdc_freeDecaySet · 29 lines

noncomputable def cdc_freeDecaySet {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (g : Multiplicative (Site d)) (φ : ℕ → ℕ) :
    Submodule ℝ C(ConfigSpace (Sym2 (Site d)), ℝ) where
  carrier := {h | Tendsto (isd_decayFun
      (fun n => freeFiniteMeasure d (φ n) hp hp1 (by norm_num : (0 : ℝ) < 2)) g
      (BoundedContinuousFunction.mkOfCompact h)) atTop (𝓝 0)}
  add_mem' {h h'} hh hh' := by
    simp only [Set.mem_ofPred_eq] at hh hh' ⊢
    have hsum := hh.add hh'
    rw [add_zero] at hsum
    refine hsum.congr (fun n => ?_)
    rw [BoundedContinuousFunction.mkOfCompact_add, cdc_decayFun_add]
  zero_mem' := by
    simp only [Set.mem_ofPred_eq]
    have hz : isd_decayFun
        (fun n => freeFiniteMeasure d (φ n) hp hp1 (by norm_num : (0 : ℝ) < 2)) g
        (BoundedContinuousFunction.mkOfCompact (0 : C(ConfigSpace (Sym2 (Site d)), ℝ)))
      = fun _ => (0 : ℝ) := by
      funext n
      rw [BoundedContinuousFunction.mkOfCompact_zero, cdc_decayFun_zero]
    rw [hz]; exact tendsto_const_nhds
  smul_mem' c h hh := by
    simp only [Set.mem_ofPred_eq] at hh ⊢
    have hsmul := hh.const_mul c
    rw [mul_zero] at hsmul
    refine hsmul.congr (fun n => ?_)
    have hms : BoundedContinuousFunction.mkOfCompact (c • h)
        = c • BoundedContinuousFunction.mkOfCompact h := rfl
    rw [hms, cdc_decayFun_smul]

Uses 5 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Shift of a configuration by a group element · Free random-cluster measure on a box · Shift-decay functional of a sequence of measures · Site of the hypercubic lattice

Used byFree translation invariance from free placements of every shift · Free translation invariance from the placement hypothesis

DefinitionDisjoint-box cap hypothesis for multi-open events#✓fully proved

For every finite family of finite edge sets and scale N, some translation g and margin r realize each pair T, g⁻¹T' in Λ_{N+r} with g⁻¹T' outside a set F, such that the conditional masses of O_T on fibres of F (with a boundary graph containing the wired one) are at most μ_N(O_T) and the box mass of g⁻¹O_{T'} is at most μ_N(O_{T'}).

StatMech.FK.dgf_DisjointBoxAnalyticCap · 19 lines

def dgf_DisjointBoxAnalyticCap {p : ℝ} (hp : 0 < p) (hp1 : p < 1) : Prop :=
  ∀ (P : Finset (Finset (Sym2 (Site d)))) (N : ℕ),
    ∃ (g : Multiplicative (Site d)) (r : ℕ), ∀ T ∈ P, ∀ T' ∈ P,
      ∃ (F tT tT' : Finset (Sym2 (boxVerts d (N + r))))
        (C' : SimpleGraph (boxVerts d (N + r))) (_ : DecidableRel C'.Adj),
        T = tT.image (edgeIncl d (N + r)) ∧
        T'.image (fun e => g⁻¹ • e) = tT'.image (edgeIncl d (N + r)) ∧
        (∀ e ∈ tT', e ∉ F) ∧
        boundaryCliqueGraph (boxBoundary d (N + r)) ≤ C' ∧
        (∀ ψ ∈ fibreReps F,
          (∑ ρ, (cdc_boxMultiOpenEvent (N + r) tT).indicator (fun _ => (1 : ℝ)) ρ
              * condBcProb (boxGraph d (N + r)) C' p 2 F ψ ρ)
            ≤ (wiredFiniteMeasure d N hp hp1 (by norm_num : (0 : ℝ) < 2)
                : Measure (ConfigSpace (Sym2 (Site d)))).real (fmu_multiOpen T)) ∧
        ((wiredFiniteMeasure d (N + r) hp hp1 (by norm_num : (0 : ℝ) < 2)
            : Measure (ConfigSpace (Sym2 (Site d)))).real
              (boxRestrict d (N + r) ⁻¹' (cdc_boxMultiOpenEvent (N + r) tT'))
          ≤ (wiredFiniteMeasure d N hp hp1 (by norm_num : (0 : ℝ) < 2)
              : Measure (ConfigSpace (Sym2 (Site d)))).real (fmu_multiOpen T'))

Uses 14

Statement usesConfiguration space of a statistical-mechanics model · Vertex boundary of a box · Nearest-neighbour graph on a box · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Vertices of the box \((-n, n)^d\) · Event that every edge of a set of box edges is open, on a box · Conditional random-cluster measure with a boundary wiring · Inclusion of box edges into \(\mathbb{Z}^d\) · Fibre representatives with every edge of a set closed · Event that every coordinate of a finite set is open · Wired random-cluster measure on a box · Site of the hypercubic lattice · Complete graph on the boundary vertices · Box \((-n, n)^d\) in the hypercubic lattice

DefinitionEdge inclusion of a translated box into \(\mathbb{Z}^d\)#✓fully proved

The inclusion of edges of the translated box v + Λ_m into the edges of ℤ^d.

noncomputable def lmc_transEdgeIncl (d m : ℕ) (v : Site d) :
    Sym2 (fvs_transBoxVerts d m v) → Sym2 (Site d) :=
  Sym2.map (Subtype.val : fvs_transBoxVerts d m v → Site d)

Uses 3 · Used by 5

Statement usesTranslated box in \(\mathbb{Z}^d\) · Vertex type of a translated box · Site of the hypercubic lattice

Used byTranslation invariance of the free \(q = 2\) infinite-volume measure · Ergodicity of the wired random-cluster measure · Translation invariance of the wired \(q = 2\) infinite-volume measure · Translated box edges are shifted centered box edges · Images of translated edge sets are shifted images

LemmaTranslated box edges are shifted centered box edges#✓fully proved

Including a translated box edge equals shifting the included centered box edge by v.

lemma lmc_transEdgeIncl_sigma_eq_smul (d m : ℕ) (v : Site d) (eb : Sym2 (boxVerts d m)) :
    lmc_transEdgeIncl d m v (Sym2.map (fvs_transEquiv d m v) eb)
      = (Multiplicative.ofAdd v) • (edgeIncl d m eb)

Uses 8 · Used by 1

Statement usesVertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Vertex type of a translated box · Translation from the centered box onto a translated box · Edge inclusion of a translated box into \(\mathbb{Z}^d\) · Site of the hypercubic lattice

Proof usesTranslated box in \(\mathbb{Z}^d\) · Box \((-n, n)^d\) in the hypercubic lattice

Used byImages of translated edge sets are shifted images

LemmaImages of translated edge sets are shifted images#✓fully proved

The image of a translated edge set in ℤ^d is the shift by v of the image of the centered set.

lemma lmc_transImage_eq_smulImage (d m : ℕ) (v : Site d) (t : Finset (Sym2 (boxVerts d m))) :
    (t.image (Sym2.map (fvs_transEquiv d m v))).image (lmc_transEdgeIncl d m v)
      = (t.image (edgeIncl d m)).image (fun e => (Multiplicative.ofAdd v) • e)

Uses 8 · Used by 3

Statement usesVertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Translated box in \(\mathbb{Z}^d\) · Vertex type of a translated box · Translation from the centered box onto a translated box · Edge inclusion of a translated box into \(\mathbb{Z}^d\) · Site of the hypercubic lattice

Proof usesTranslated box edges are shifted centered box edges

Used byTranslation invariance of the free \(q = 2\) infinite-volume measure · Ergodicity of the wired random-cluster measure · Translation invariance of the wired \(q = 2\) infinite-volume measure

DefinitionWired all-open probability on a translated box#✓fully proved

The probability, under the wired q = 2 FK measure on the translated box v + Λ_m, that all edges of the translated copy of t ⊆ E(Λ_N) are open.

noncomputable def lmc_transBoxMass (v : Site d) (N : ℕ) (t : Finset (Sym2 (boxVerts d N)))
    (p : ℝ) (m : ℕ) (hNm : N ≤ m) : ℝ :=
  med_multiMassProb
    (wiredFkProb (fvs_transBoxGraph d m v) (fvs_transBoxBoundary d m v) p 2)
    ((t.image (innerEdgeLE d hNm)).image (Sym2.map (fvs_transEquiv d m v)))

Uses 11 · Used by 9

Statement usesVertices of the box \((-n, n)^d\) · Translated box in \(\mathbb{Z}^d\) · Vertex boundary of a translated box · Nearest-neighbour graph on a translated box · Vertex type of a translated box · Translation from the centered box onto a translated box · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Mass of the all-open event under a weight function · Wired random-cluster probability of a configuration · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byErgodicity of the wired random-cluster measure · Translation invariance of the wired \(q = 2\) infinite-volume measure · Translated wired box mass equals the centered box mass · Translated wired box masses converge to the infinite-volume mass · Wired placement gives shift homogeneity on all-open events · Wired shift invariance of an all-open event from matching limits · Wired shift invariance of an all-open event from decaying differences · Wired placement hypothesis for a shift · Identity shift satisfies the wired placement hypothesis

LemmaTranslated wired box mass equals the centered box mass#✓fully proved

The translated wired box mass equals the probability of the unshifted event under the wired finite-volume measure on the centered box Λ_m.

lemma lmc_transBoxMass_eq_centred (v : Site d) (N : ℕ) (t : Finset (Sym2 (boxVerts d N)))
    {p : ℝ} (hp : 0 < p) (hp1 : p < 1) (m : ℕ) (hNm : N ≤ m) :
    lmc_transBoxMass v N t p m hNm
      = (wiredFiniteMeasure d m hp hp1 (by norm_num : (0:ℝ) < 2)
          : Measure (ConfigSpace (Sym2 (Site d)))).real
            (cdc_multiOpenEvent (t.image (edgeIncl d N)))

Uses 21 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Vertices of the box \((-n, n)^d\) · Event that every edge of a finite set is open · Inclusion of box edges into \(\mathbb{Z}^d\) · Wired all-open probability on a translated box · Wired random-cluster measure on a box · Site of the hypercubic lattice

Proof usesVertex boundary of a box · Nearest-neighbour graph on a box · Edge inclusion into \(\mathbb{Z}^d\) factors through \(\Lambda_m\) · Translated box in \(\mathbb{Z}^d\) · Vertex boundary of a translated box · Nearest-neighbour graph on a translated box · Vertex type of a translated box · Translation from the centered box onto a translated box · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Translation covariance of wired box masses · Wired box measure of an all-open event equals its box mass · Mass of the all-open event under a weight function · Wired random-cluster probability of a configuration · Box \((-n, n)^d\) in the hypercubic lattice

Used byErgodicity of the wired random-cluster measure · Translated wired box masses converge to the infinite-volume mass

LemmaTranslated wired box masses converge to the infinite-volume mass#✓fully proved

The translated wired box masses converge to the wired infinite-volume probability that all edges of t are open.

lemma lmc_transBoxMass_tendsto_centred_iv (v : Site d) (N : ℕ)
    (t : Finset (Sym2 (boxVerts d N))) {p : ℝ} (hp : 0 < p) (hp1 : p < 1) :
    Tendsto (fun m : ℕ => lmc_transBoxMass v N t p (N + m) (Nat.le_add_right N m)) atTop
      (𝓝 ((wiredInfiniteVolume d hp hp1 (by norm_num : (0:ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d)))).real
          (cdc_multiOpenEvent (t.image (edgeIncl d N)))))

Uses 10 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Vertices of the box \((-n, n)^d\) · Event that every edge of a finite set is open · Inclusion of box edges into \(\mathbb{Z}^d\) · Wired all-open probability on a translated box · Wired infinite-volume random-cluster measure · Site of the hypercubic lattice

Proof usesTranslated wired box mass equals the centered box mass · Wired all-open probabilities converge to the infinite-volume value · Wired random-cluster measure on a box

Used byWired shift invariance of an all-open event from matching limits · Wired shift invariance of an all-open event from decaying differences · Identity shift satisfies the wired placement hypothesis

LemmaWired shift invariance of an all-open event from matching limits#✓fully proved

If the translated wired box masses also converge to the wired infinite-volume probability of the shifted set v + t, the wired infinite-volume measure gives t and v + t the same probability.

StatMech.FK.lmc_wiredMultiHomogeneous_of_cofinal · 15 lines

lemma lmc_wiredMultiHomogeneous_of_cofinal (v : Site d) (N : ℕ)
    (t : Finset (Sym2 (boxVerts d N))) {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (hcofinal : Tendsto (fun m : ℕ => lmc_transBoxMass v N t p (N + m) (Nat.le_add_right N m))
        atTop
        (𝓝 ((wiredInfiniteVolume d hp hp1 (by norm_num : (0:ℝ) < 2)
            : Measure (ConfigSpace (Sym2 (Site d)))).real
              (cdc_multiOpenEvent
                ((t.image (edgeIncl d N)).image (fun e => (Multiplicative.ofAdd v) • e)))))) :
    (wiredInfiniteVolume d hp hp1 (by norm_num : (0:ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d)))).real
          (cdc_multiOpenEvent (t.image (edgeIncl d N)))
      = (wiredInfiniteVolume d hp hp1 (by norm_num : (0:ℝ) < 2)
          : Measure (ConfigSpace (Sym2 (Site d)))).real
            (cdc_multiOpenEvent
              ((t.image (edgeIncl d N)).image (fun e => (Multiplicative.ofAdd v) • e)))

Uses 8 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Vertices of the box \((-n, n)^d\) · Event that every edge of a finite set is open · Inclusion of box edges into \(\mathbb{Z}^d\) · Wired all-open probability on a translated box · Wired infinite-volume random-cluster measure · Site of the hypercubic lattice

Proof usesTranslated wired box masses converge to the infinite-volume mass

Used byWired placement gives shift homogeneity on all-open events

LemmaWired shift invariance of an all-open event from decaying differences#✓fully proved

If the translated wired box masses differ from the centered box masses of a set t' with v + t = t' by a sequence tending to zero, the wired infinite-volume measure gives t and v + t the same probability.

StatMech.FK.lmc_wiredMultiHomogeneous_of_decay · 17 lines

lemma lmc_wiredMultiHomogeneous_of_decay (v : Site d) (N N' : ℕ)
    (t : Finset (Sym2 (boxVerts d N))) (t' : Finset (Sym2 (boxVerts d N')))
    {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (hst' : (t.image (edgeIncl d N)).image (fun e => (Multiplicative.ofAdd v) • e)
        = t'.image (edgeIncl d N'))
    (hdecay : Tendsto
        (fun m : ℕ => lmc_transBoxMass v N t p (N + m) (Nat.le_add_right N m)
          - (wiredFiniteMeasure d (N' + m) hp hp1 (by norm_num : (0:ℝ) < 2)
              : Measure (ConfigSpace (Sym2 (Site d)))).real
                (cdc_multiOpenEvent (t'.image (edgeIncl d N')))) atTop (𝓝 0)) :
    (wiredInfiniteVolume d hp hp1 (by norm_num : (0:ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d)))).real
          (cdc_multiOpenEvent (t.image (edgeIncl d N)))
      = (wiredInfiniteVolume d hp hp1 (by norm_num : (0:ℝ) < 2)
          : Measure (ConfigSpace (Sym2 (Site d)))).real
            (cdc_multiOpenEvent
              ((t.image (edgeIncl d N)).image (fun e => (Multiplicative.ofAdd v) • e)))

Uses 10

Statement usesConfiguration space of a statistical-mechanics model · Vertices of the box \((-n, n)^d\) · Event that every edge of a finite set is open · Inclusion of box edges into \(\mathbb{Z}^d\) · Wired all-open probability on a translated box · Wired random-cluster measure on a box · Wired infinite-volume random-cluster measure · Site of the hypercubic lattice

Proof usesTranslated wired box masses converge to the infinite-volume mass · Wired all-open probabilities converge to the infinite-volume value

DefinitionWired placement hypothesis for a shift#✓fully proved

The placement hypothesis for the shift g: every finite edge set lies in a box whose translated wired box masses converge to the wired infinite-volume probability of the set shifted by g⁻¹.

def lmc_wiredPlacement {p : ℝ} (hp : 0 < p) (hp1 : p < 1) (g : Multiplicative (Site d)) : Prop :=
  ∀ s : Finset (Sym2 (Site d)),
    ∃ (N : ℕ) (t : Finset (Sym2 (boxVerts d N))),
      s = t.image (edgeIncl d N)
        ∧ Tendsto
            (fun m : ℕ => lmc_transBoxMass (Multiplicative.toAdd g⁻¹) N t p (N + m)
              (Nat.le_add_right N m)) atTop
            (𝓝 ((wiredInfiniteVolume d hp hp1 (by norm_num : (0:ℝ) < 2)
                : Measure (ConfigSpace (Sym2 (Site d)))).real
                  (cdc_multiOpenEvent (s.image (fun e => g⁻¹ • e)))))

Uses 7 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Vertices of the box \((-n, n)^d\) · Event that every edge of a finite set is open · Inclusion of box edges into \(\mathbb{Z}^d\) · Wired all-open probability on a translated box · Wired infinite-volume random-cluster measure · Site of the hypercubic lattice

Used byTranslation invariance of the wired \(q = 2\) infinite-volume measure · Wired translation invariance from the placement hypothesis · Wired placement gives shift homogeneity on all-open events · Identity shift satisfies the wired placement hypothesis

LemmaWired placement gives shift homogeneity on all-open events#✓fully proved

The placement hypothesis for g gives g-homogeneity of the wired infinite-volume measure on all events "every edge of s is open".

lemma lmc_wiredMultiHomogeneous {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (g : Multiplicative (Site d)) (hplace : lmc_wiredPlacement hp hp1 g) :
    cdc_wiredMultiHomogeneous hp hp1 g

Uses 10 · Used by 2

Statement usesWired \(q = 2\) multi-edge homogeneity under a translation · Wired placement hypothesis for a shift · Site of the hypercubic lattice

Proof usesConfiguration space of a statistical-mechanics model · Vertices of the box \((-n, n)^d\) · Event that every edge of a finite set is open · Inclusion of box edges into \(\mathbb{Z}^d\) · Wired all-open probability on a translated box · Wired shift invariance of an all-open event from matching limits · Wired infinite-volume random-cluster measure

Used byWired translation invariance from the placement hypothesis · Wired infinite-volume measure is homogeneous under the identity shift

LemmaIdentity shift satisfies the wired placement hypothesis#✓fully proved

The identity shift satisfies the wired placement hypothesis.

lemma lmc_wiredPlacement_one {p : ℝ} (hp : 0 < p) (hp1 : p < 1) :
    lmc_wiredPlacement hp hp1 (1 : Multiplicative (Site d))

Uses 10 · Used by 1

Statement usesWired placement hypothesis for a shift · Site of the hypercubic lattice

Proof usesConfiguration space of a statistical-mechanics model · Vertices of the box \((-n, n)^d\) · Event that every edge of a finite set is open · Inclusion of box edges into \(\mathbb{Z}^d\) · Wired all-open probability on a translated box · Translated wired box masses converge to the infinite-volume mass · Wired infinite-volume random-cluster measure · Box \((-n, n)^d\) in the hypercubic lattice

Used byWired infinite-volume measure is homogeneous under the identity shift

LemmaWired infinite-volume measure is homogeneous under the identity shift#✓fully proved

The wired infinite-volume measure is homogeneous under the identity shift.

lemma lmc_wiredMultiHomogeneous_one {p : ℝ} (hp : 0 < p) (hp1 : p < 1) :
    cdc_wiredMultiHomogeneous hp hp1 (1 : Multiplicative (Site d))

Uses 4

Statement usesWired \(q = 2\) multi-edge homogeneity under a translation · Site of the hypercubic lattice

Proof usesWired placement gives shift homogeneity on all-open events · Identity shift satisfies the wired placement hypothesis

LemmaWired translation invariance from the placement hypothesis#✓fully proved

The wired q = 2 infinite-volume FK measure on ℤ^d is translation invariant if every shift satisfies the wired placement hypothesis.

lemma lmc_wiredIV_isTranslationInvariant_of_placement {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (hplace : ∀ g : Multiplicative (Site d), lmc_wiredPlacement hp hp1 g) :
    ConfigSpace.IsTranslationInvariant (G := Multiplicative (Site d))
      (wiredInfiniteVolume d hp hp1 (by norm_num : (0:ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d))))

Uses 27 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Translation-invariant measure on configuration space · Wired placement hypothesis for a shift · Wired infinite-volume random-cluster measure · Site of the hypercubic lattice

Proof usesShift of a configuration by a group element · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Vertices of the box \((-n, n)^d\) · Event that every edge of a set of box edges is open, on a box · Monomial indicator as a bounded continuous function · Continuous monomial indicator that every edge of a set is open · Event that every edge of a finite set is open · Submodule of functions with vanishing wired shift decay · Wired \(q = 2\) multi-edge homogeneity under a translation · Inclusion of box edges into \(\mathbb{Z}^d\) · Wired infinite-volume measure as limit on increasing cylinder events · Edge-open indicator as a continuous function · Cylinder algebra generated by edge indicators · Cylinder algebra as bounded continuous functions · Cylinder decay along the wired box measures · Translation invariance of the wired FK measure from cylinder decay · Shift-decay functional of a sequence of measures · Wired placement gives shift homogeneity on all-open events · Wired random-cluster measure on a box · Increasing event · Box \((-n, n)^d\) in the hypercubic lattice · Weak convergence of probability measures on configuration space

Used byTranslation invariance of the wired \(q = 2\) infinite-volume measure

DefinitionTranslated free box mass of an edge set#✓fully proved

The probability, under the free q = 2 FK measure on the translated box v + Λ_m, that all edges of the translated copy of t ⊆ E(Λ_N) are open.

noncomputable def lmc_transBoxMassFree (v : Site d) (N : ℕ) (t : Finset (Sym2 (boxVerts d N)))
    (p : ℝ) (m : ℕ) (hNm : N ≤ m) : ℝ :=
  med_multiMassProb (fkProb (fvs_transBoxGraph d m v) p 2)
    ((t.image (innerEdgeLE d hNm)).image (Sym2.map (fvs_transEquiv d m v)))

Uses 10 · Used by 7

Statement usesVertices of the box \((-n, n)^d\) · Probability of an ambient FK configuration · Translated box in \(\mathbb{Z}^d\) · Nearest-neighbour graph on a translated box · Vertex type of a translated box · Translation from the centered box onto a translated box · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Mass of the all-open event under a weight function · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byTranslation invariance of the free \(q = 2\) infinite-volume measure · Free placement gives shift homogeneity on all-open events · Equal free probabilities for \(t\) and \(v + t\) from matching box limits · Free placement hypothesis for a shift via box-mass limits · Identity shift satisfies the free placement hypothesis · Translated free box mass equals the centred box probability · Translated free box masses converge to the free infinite-volume value

LemmaTranslated free box mass equals the centred box probability#✓fully proved

The translated free box mass equals the probability of the unshifted event under the free finite-volume measure on the centered box Λ_m.

lemma lmc_transBoxMassFree_eq_centred (v : Site d) (N : ℕ) (t : Finset (Sym2 (boxVerts d N)))
    {p : ℝ} (hp : 0 < p) (hp1 : p < 1) (m : ℕ) (hNm : N ≤ m) :
    lmc_transBoxMassFree v N t p m hNm
      = (freeFiniteMeasure d m hp hp1 (by norm_num : (0:ℝ) < 2)
          : Measure (ConfigSpace (Sym2 (Site d)))).real
            (cdc_multiOpenEvent (t.image (edgeIncl d N)))

Uses 19 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Vertices of the box \((-n, n)^d\) · Event that every edge of a finite set is open · Inclusion of box edges into \(\mathbb{Z}^d\) · Free random-cluster measure on a box · Translated free box mass of an edge set · Site of the hypercubic lattice

Proof usesNearest-neighbour graph on a box · Edge inclusion into \(\mathbb{Z}^d\) factors through \(\Lambda_m\) · Probability of an ambient FK configuration · Translated box in \(\mathbb{Z}^d\) · Nearest-neighbour graph on a translated box · Vertex type of a translated box · Translation from the centered box onto a translated box · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Translation covariance of free box masses · Free box measure of an all-open event equals its box mass · Mass of the all-open event under a weight function · Box \((-n, n)^d\) in the hypercubic lattice

Used byTranslated free box masses converge to the free infinite-volume value

LemmaTranslated free box masses converge to the free infinite-volume value#✓fully proved

The translated free box masses converge to the free infinite-volume probability that all edges of t are open.

lemma lmc_transBoxMassFree_tendsto_centred_iv (v : Site d) (N : ℕ)
    (t : Finset (Sym2 (boxVerts d N))) {p : ℝ} (hp : 0 < p) (hp1 : p < 1) :
    Tendsto (fun m : ℕ => lmc_transBoxMassFree v N t p (N + m) (Nat.le_add_right N m)) atTop
      (𝓝 ((freeInfiniteVolume d hp hp1 (by norm_num : (0:ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d)))).real
          (cdc_multiOpenEvent (t.image (edgeIncl d N)))))

Uses 10 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Vertices of the box \((-n, n)^d\) · Event that every edge of a finite set is open · Inclusion of box edges into \(\mathbb{Z}^d\) · Free infinite-volume random-cluster measure · Translated free box mass of an edge set · Site of the hypercubic lattice

Proof usesFree random-cluster measure on a box · Translated free box mass equals the centred box probability · Free all-open probabilities converge to the infinite-volume value

Used byEqual free probabilities for \(t\) and \(v + t\) from matching box limits · Identity shift satisfies the free placement hypothesis

LemmaEqual free probabilities for \(t\) and \(v + t\) from matching box limits#✓fully proved

If the translated free box masses also converge to the free infinite-volume probability of the shifted set v + t, the free infinite-volume measure gives t and v + t the same probability.

StatMech.FK.lmc_freeMultiHomogeneous_of_cofinal · 15 lines

lemma lmc_freeMultiHomogeneous_of_cofinal (v : Site d) (N : ℕ)
    (t : Finset (Sym2 (boxVerts d N))) {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (hcofinal : Tendsto (fun m : ℕ => lmc_transBoxMassFree v N t p (N + m) (Nat.le_add_right N m))
        atTop
        (𝓝 ((freeInfiniteVolume d hp hp1 (by norm_num : (0:ℝ) < 2)
            : Measure (ConfigSpace (Sym2 (Site d)))).real
              (cdc_multiOpenEvent
                ((t.image (edgeIncl d N)).image (fun e => (Multiplicative.ofAdd v) • e)))))) :
    (freeInfiniteVolume d hp hp1 (by norm_num : (0:ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d)))).real
          (cdc_multiOpenEvent (t.image (edgeIncl d N)))
      = (freeInfiniteVolume d hp hp1 (by norm_num : (0:ℝ) < 2)
          : Measure (ConfigSpace (Sym2 (Site d)))).real
            (cdc_multiOpenEvent
              ((t.image (edgeIncl d N)).image (fun e => (Multiplicative.ofAdd v) • e)))

Uses 8 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Vertices of the box \((-n, n)^d\) · Event that every edge of a finite set is open · Inclusion of box edges into \(\mathbb{Z}^d\) · Free infinite-volume random-cluster measure · Translated free box mass of an edge set · Site of the hypercubic lattice

Proof usesTranslated free box masses converge to the free infinite-volume value

Used byFree placement gives shift homogeneity on all-open events

DefinitionFree placement hypothesis for a shift via box-mass limits#✓fully proved

The placement hypothesis for the shift g and the free measure: every finite edge set lies in a box whose translated free box masses converge to the free infinite-volume probability of the set shifted by g⁻¹.

def lmc_freePlacement {p : ℝ} (hp : 0 < p) (hp1 : p < 1) (g : Multiplicative (Site d)) : Prop :=
  ∀ s : Finset (Sym2 (Site d)),
    ∃ (N : ℕ) (t : Finset (Sym2 (boxVerts d N))),
      s = t.image (edgeIncl d N)
        ∧ Tendsto
            (fun m : ℕ => lmc_transBoxMassFree (Multiplicative.toAdd g⁻¹) N t p (N + m)
              (Nat.le_add_right N m)) atTop
            (𝓝 ((freeInfiniteVolume d hp hp1 (by norm_num : (0:ℝ) < 2)
                : Measure (ConfigSpace (Sym2 (Site d)))).real
                  (cdc_multiOpenEvent (s.image (fun e => g⁻¹ • e)))))

Uses 7 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Vertices of the box \((-n, n)^d\) · Event that every edge of a finite set is open · Inclusion of box edges into \(\mathbb{Z}^d\) · Free infinite-volume random-cluster measure · Translated free box mass of an edge set · Site of the hypercubic lattice

Used byTranslation invariance of the free \(q = 2\) infinite-volume measure · Free translation invariance from the placement hypothesis · Free placement gives shift homogeneity on all-open events · Identity shift satisfies the free placement hypothesis

LemmaFree placement gives shift homogeneity on all-open events#✓fully proved

The free placement hypothesis for g gives g-homogeneity of the free infinite-volume measure on all events "every edge of s is open".

lemma lmc_freeMultiHomogeneous {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (g : Multiplicative (Site d)) (hplace : lmc_freePlacement hp hp1 g) :
    cdc_freeMultiHomogeneous hp hp1 g

Uses 10 · Used by 2

Statement usesFree \(q = 2\) multi-edge homogeneity under a translation · Free placement hypothesis for a shift via box-mass limits · Site of the hypercubic lattice

Proof usesConfiguration space of a statistical-mechanics model · Vertices of the box \((-n, n)^d\) · Event that every edge of a finite set is open · Inclusion of box edges into \(\mathbb{Z}^d\) · Free infinite-volume random-cluster measure · Equal free probabilities for \(t\) and \(v + t\) from matching box limits · Translated free box mass of an edge set

Used byFree translation invariance from the placement hypothesis · Free infinite-volume measure is homogeneous under the identity shift

LemmaIdentity shift satisfies the free placement hypothesis#✓fully proved

The identity shift satisfies the free placement hypothesis.

lemma lmc_freePlacement_one {p : ℝ} (hp : 0 < p) (hp1 : p < 1) :
    lmc_freePlacement hp hp1 (1 : Multiplicative (Site d))

Uses 10 · Used by 1

Statement usesFree placement hypothesis for a shift via box-mass limits · Site of the hypercubic lattice

Proof usesConfiguration space of a statistical-mechanics model · Vertices of the box \((-n, n)^d\) · Event that every edge of a finite set is open · Inclusion of box edges into \(\mathbb{Z}^d\) · Free infinite-volume random-cluster measure · Translated free box mass of an edge set · Translated free box masses converge to the free infinite-volume value · Box \((-n, n)^d\) in the hypercubic lattice

Used byFree infinite-volume measure is homogeneous under the identity shift

LemmaFree infinite-volume measure is homogeneous under the identity shift#✓fully proved

The free infinite-volume measure is homogeneous under the identity shift.

lemma lmc_freeMultiHomogeneous_one {p : ℝ} (hp : 0 < p) (hp1 : p < 1) :
    cdc_freeMultiHomogeneous hp hp1 (1 : Multiplicative (Site d))

Uses 4

Statement usesFree \(q = 2\) multi-edge homogeneity under a translation · Site of the hypercubic lattice

Proof usesFree placement gives shift homogeneity on all-open events · Identity shift satisfies the free placement hypothesis

LemmaFree translation invariance from the placement hypothesis#✓fully proved

The free q = 2 infinite-volume FK measure on ℤ^d is translation invariant if every shift satisfies the free placement hypothesis.

lemma lmc_freeIV_isTranslationInvariant_of_placement {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (hplace : ∀ g : Multiplicative (Site d), lmc_freePlacement hp hp1 g) :
    ConfigSpace.IsTranslationInvariant (G := Multiplicative (Site d))
      (freeInfiniteVolume d hp hp1 (by norm_num : (0:ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d))))

Uses 27 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Translation-invariant measure on configuration space · Free infinite-volume random-cluster measure · Free placement hypothesis for a shift via box-mass limits · Site of the hypercubic lattice

Proof usesShift of a configuration by a group element · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Vertices of the box \((-n, n)^d\) · Event that every edge of a set of box edges is open, on a box · Submodule of functions with vanishing free shift decay · Free \(q = 2\) multi-edge homogeneity under a translation · Monomial indicator as a bounded continuous function · Continuous monomial indicator that every edge of a set is open · Event that every edge of a finite set is open · Inclusion of box edges into \(\mathbb{Z}^d\) · Free \(q=2\) box masses of increasing cylinders tend to infinite volume · Free random-cluster measure on a box · Edge-open indicator as a continuous function · Cylinder algebra generated by edge indicators · Cylinder algebra as bounded continuous functions · Cylinder decay along the free box measures · Translation invariance of the free FK measure from cylinder decay · Shift-decay functional of a sequence of measures · Free placement gives shift homogeneity on all-open events · Increasing event · Box \((-n, n)^d\) in the hypercubic lattice · Weak convergence of probability measures on configuration space

Used byTranslation invariance of the free \(q = 2\) infinite-volume measure

DefinitionSup norm of a site of \(\mathbb{Z}^d\)#✓fully proved

The sup-norm max_i |v_i| of a site v.

def flc_vrad (v : Site d) : ℕ := Finset.univ.sup (fun i => (v i).natAbs)

Uses 1 · Used by 6

Statement usesSite of the hypercubic lattice

Used byTranslation invariance of the plus state · Translation invariance of the free \(q = 2\) infinite-volume measure · Translate of a vertex of \(\Lambda_N\) as a vertex of \(\Lambda_{N+r}\) · Translate of an edge of \(\Lambda_N\) as an edge of \(\Lambda_{N+r}\) · Ergodicity of the wired random-cluster measure · Translation invariance of the wired \(q = 2\) infinite-volume measure

DefinitionInclusion of a subset of sites into a larger one#✓fully proved

The inclusion of a subset of sites into a larger one, as a map of subtypes.

def flc_incl {Sin Sout : Set (Site d)} (hsub : Sin ⊆ Sout) (x : {y : Site d // y ∈ Sin}) :
    {y : Site d // y ∈ Sout} :=
  ⟨(x : Site d), hsub x.2⟩

Uses 1 · Used by 6

Statement usesSite of the hypercubic lattice

Used byPer-box uniqueness of the random-cluster measures off a countable set · Free off-centre lower bound by the recentred small-box marginal · Wired off-centre upper bound by the recentred small-box marginal · Translation invariance of the free \(q = 2\) infinite-volume measure · Ergodicity of the wired random-cluster measure · Translation invariance of the wired \(q = 2\) infinite-volume measure

DefinitionBox edge set included into \(\Lambda_m\) and translated by \(v\)#✓fully proved

The edge set t of Λ_N, included into Λ_m and translated by v.

noncomputable def flc_transEdges (v : Site d) (N : ℕ) (t : Finset (Sym2 (boxVerts d N)))
    (m : ℕ) (hNm : N ≤ m) : Finset (Sym2 (fvs_transBoxVerts d m v)) :=
  (t.image (innerEdgeLE d hNm)).image (Sym2.map (fvs_transEquiv d m v))

Uses 7 · Used by 3

Statement usesVertices of the box \((-n, n)^d\) · Translated box in \(\mathbb{Z}^d\) · Vertex type of a translated box · Translation from the centered box onto a translated box · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byTranslation invariance of the free \(q = 2\) infinite-volume measure · Ergodicity of the wired random-cluster measure · Translation invariance of the wired \(q = 2\) infinite-volume measure

TheoremTranslation invariance of the wired \(q = 2\) infinite-volume measure#✓fully proved

The wired q = 2 infinite-volume random-cluster measure on ℤ^d is translation invariant.

theorem flc_wiredIV_isTranslationInvariant {p : ℝ} (hp : 0 < p) (hp1 : p < 1) :
    ConfigSpace.IsTranslationInvariant (G := Multiplicative (Site d))
      (wiredInfiniteVolume d hp hp1 (by norm_num : (0 : ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d))))

Uses 34 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Translation-invariant measure on configuration space · Wired infinite-volume random-cluster measure · Site of the hypercubic lattice

Proof usesVertex boundary of a box · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Event that every edge of a finite set is open · Inclusion of box edges into \(\mathbb{Z}^d\) · Edge inclusion into \(\mathbb{Z}^d\) factors through \(\Lambda_m\) · Inclusion of a subset of sites into a larger one · Box edge set included into \(\Lambda_m\) and translated by \(v\) · Sup norm of a site of \(\mathbb{Z}^d\) · Translated box in \(\mathbb{Z}^d\) · Vertex boundary of a translated box · Nearest-neighbour graph on a translated box · Vertex type of a translated box · Translation from the centered box onto a translated box · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Wired all-open probability on a translated box · Edge inclusion of a translated box into \(\mathbb{Z}^d\) · Images of translated edge sets are shifted images · Wired translation invariance from the placement hypothesis · Wired placement hypothesis for a shift · Wired box measure of an all-open event equals its box mass · Wired all-open probabilities converge to the infinite-volume value · Mass of the all-open event under a weight function · Image of an inner-graph edge in the outer graph · Outer wired all-open probability at most the inner wired one · Wired random-cluster measure on a box · Wired random-cluster probability of a configuration · Nearest neighbours in \(\mathbb{Z}^d\) · Box \((-n, n)^d\) in the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\)

Used byEvery lattice edge has the wired \(q = 2\) density of \(\{0, e_0\}\) · Wired \(q = 2\) measure is ergodic under the factorization bound

LemmaDomain monotonicity of wired \(q = 2\) box measures#✓fully proved

For q = 2 and N ≤ m, the wired Λ_m measure of an increasing Λ_N cylinder event is at most its wired Λ_N measure.

lemma fwm_wired_box_domain_monotone (N m : ℕ) (hNm : N ≤ m) {p : ℝ}
    (hp : 0 < p) (hp1 : p < 1)
    {S : Set (ConfigSpace (Sym2 (boxVerts d N)))} (hS : IsIncreasing S) :
    (wiredFiniteMeasure d m hp hp1 (by norm_num : (0 : ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d)))).real (boxRestrict d N ⁻¹' S)
      ≤ (wiredFiniteMeasure d N hp hp1 (by norm_num : (0 : ℝ) < 2)
          : Measure (ConfigSpace (Sym2 (Site d)))).real (boxRestrict d N ⁻¹' S)

Uses 7 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Vertices of the box \((-n, n)^d\) · Wired random-cluster measure on a box · Increasing event · Site of the hypercubic lattice

Proof usesWired \(q = 2\) increasing-event probabilities do not grow with the box

Used byDomain monotonicity of wired multi-open probabilities

LemmaDomain monotonicity of wired multi-open probabilities#✓fully proved

For q = 2 and N ≤ m, the wired Λ_m probability that a set of Λ_N edges is open is at most its wired Λ_N probability.

lemma fwm_wired_multiOpen_domain_monotone (N m : ℕ) (hNm : N ≤ m)
    (t : Finset (Sym2 (boxVerts d N))) {p : ℝ} (hp : 0 < p) (hp1 : p < 1) :
    (wiredFiniteMeasure d m hp hp1 (by norm_num : (0 : ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d)))).real
          (fmu_multiOpen (t.image (edgeIncl d N)))
      ≤ (wiredFiniteMeasure d N hp hp1 (by norm_num : (0 : ℝ) < 2)
          : Measure (ConfigSpace (Sym2 (Site d)))).real
            (fmu_multiOpen (t.image (edgeIncl d N)))

Uses 11 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Event that every coordinate of a finite set is open · Wired random-cluster measure on a box · Site of the hypercubic lattice

Proof usesRestriction of a configuration of \(\mathbb{Z}^d\) to a box · Event that every edge of a set of box edges is open, on a box · Event that every edge of a finite set is open · Domain monotonicity of wired \(q = 2\) box measures · Increasing event

Used byDomain monotonicity for edge sets realized in a box

LemmaDomain monotonicity for edge sets realized in a box#✓fully proved

The same for an edge set of ℤ^d given as the image of Λ_N edges.

lemma fwm_wired_domain_monotone_of_realised {N m : ℕ} (hNm : N ≤ m)
    {s : Finset (Sym2 (Site d))} (t : Finset (Sym2 (boxVerts d N)))
    (hst : s = t.image (edgeIncl d N)) {p : ℝ} (hp : 0 < p) (hp1 : p < 1) :
    (wiredFiniteMeasure d m hp hp1 (by norm_num : (0 : ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d)))).real (fmu_multiOpen s)
      ≤ (wiredFiniteMeasure d N hp hp1 (by norm_num : (0 : ℝ) < 2)
          : Measure (ConfigSpace (Sym2 (Site d)))).real (fmu_multiOpen s)

Uses 7 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Event that every coordinate of a finite set is open · Wired random-cluster measure on a box · Site of the hypercubic lattice

Proof usesDomain monotonicity of wired multi-open probabilities

Used byErgodicity of the wired random-cluster measure · Domain monotonicity for translated pairs of multi-open events

LemmaDomain monotonicity for translated pairs of multi-open events#✓fully proved

The same for the event "T open and g·T' open", when T ∪ g⁻¹·T' lies in Λ_N.

StatMech.FK.fwm_wired_cross_le_box_domain · 15 lines

lemma fwm_wired_cross_le_box_domain {N m : ℕ} (hNm : N ≤ m)
    (g : Multiplicative (Site d)) (T T' : Finset (Sym2 (Site d)))
    {t : Finset (Sym2 (boxVerts d N))}
    (hreal : T ∪ T'.image (fun e => g⁻¹ • e) = t.image (edgeIncl d N))
    {p : ℝ} (hp : 0 < p) (hp1 : p < 1) :
    (wiredFiniteMeasure d m hp hp1 (by norm_num : (0 : ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d)))).real
          (fmu_multiOpen T ∩
            (shift g : ConfigSpace (Sym2 (Site d)) → ConfigSpace (Sym2 (Site d)))
              ⁻¹' fmu_multiOpen T')
      ≤ (wiredFiniteMeasure d N hp hp1 (by norm_num : (0 : ℝ) < 2)
          : Measure (ConfigSpace (Sym2 (Site d)))).real
            (fmu_multiOpen T ∩
              (shift g : ConfigSpace (Sym2 (Site d)) → ConfigSpace (Sym2 (Site d)))
                ⁻¹' fmu_multiOpen T')

Uses 8 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Shift of a configuration by a group element · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Event that every coordinate of a finite set is open · Wired random-cluster measure on a box · Site of the hypercubic lattice

Proof usesDomain monotonicity for edge sets realized in a box

Used byFinite-box product domination from the factorization bound

DefinitionDisjoint-box factorization bound for box measures#✓fully proved

The disjoint-box factorization bound for a family of box measures μbox: for every finite family P of edge sets realized in Λ_N there are a translation g and r such that each T ∪ g⁻¹·T' lies in Λ_(N+r) and μbox (N+r) (T open, g·T' open) ≤ μbox N (T open) · μbox N (T' open). The parameters p only index the family.

def fwm_WiredDisjointBoxFactorise {p : ℝ} (_hp : 0 < p) (_hp1 : p < 1)
    (μbox : ℕ → Measure (ConfigSpace (Sym2 (Site d)))) : Prop :=
  ∀ (P : Finset (Finset (Sym2 (Site d)))) (N : ℕ),
    (∀ T ∈ P, ∃ t : Finset (Sym2 (boxVerts d N)), T = t.image (edgeIncl d N)) →
    ∃ (g : Multiplicative (Site d)) (r : ℕ), ∀ T ∈ P, ∀ T' ∈ P,
      (∃ t : Finset (Sym2 (boxVerts d (N + r))),
          T ∪ T'.image (fun e => g⁻¹ • e) = t.image (edgeIncl d (N + r)))
      ∧ (μbox (N + r)).real (fmu_multiOpen T ∩
            (shift g : ConfigSpace (Sym2 (Site d)) → ConfigSpace (Sym2 (Site d)))
              ⁻¹' fmu_multiOpen T')
          ≤ (μbox N).real (fmu_multiOpen T) * (μbox N).real (fmu_multiOpen T')

Uses 6 · Used by 5

Statement usesConfiguration space of a statistical-mechanics model · Shift of a configuration by a group element · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Event that every coordinate of a finite set is open · Site of the hypercubic lattice

Used byErgodicity of the wired random-cluster measure · Finite-box product domination from the factorization bound · Upper decorrelation of the wired measure from factorization · All-open Dirac mass satisfies the factorization bound · Wired \(q = 2\) measure is ergodic under the factorization bound

LemmaFinite-box product domination from the factorization bound#✓fully proved

Under the factorization bound for the wired measures, for some translation g and all large m, φ¹_{Λ_m}(T open, g·T' open) ≤ φ¹_{Λ_N}(T open) φ¹_{Λ_N}(T' open) for all T, T' ∈ P.

StatMech.FK.fwm_finiteBoxDisjointProductDom_conclusion_of_factorise · 16 lines

lemma fwm_finiteBoxDisjointProductDom_conclusion_of_factorise {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (hfac : fwm_WiredDisjointBoxFactorise hp hp1
      (fun m => (wiredFiniteMeasure d m hp hp1 (by norm_num : (0 : ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d))))))
    (P : Finset (Finset (Sym2 (Site d)))) (N : ℕ)
    (hreal : ∀ T ∈ P, ∃ t : Finset (Sym2 (boxVerts d N)), T = t.image (edgeIncl d N)) :
    ∃ g : Multiplicative (Site d), ∀ᶠ m in atTop, ∀ T ∈ P, ∀ T' ∈ P,
      (wiredFiniteMeasure d m hp hp1 (by norm_num : (0 : ℝ) < 2)
          : Measure (ConfigSpace (Sym2 (Site d)))).real
            (fmu_multiOpen T ∩
              (shift g : ConfigSpace (Sym2 (Site d)) → ConfigSpace (Sym2 (Site d)))
                ⁻¹' fmu_multiOpen T')
        ≤ (wiredFiniteMeasure d N hp hp1 (by norm_num : (0 : ℝ) < 2)
              : Measure (ConfigSpace (Sym2 (Site d)))).real (fmu_multiOpen T)
          * (wiredFiniteMeasure d N hp hp1 (by norm_num : (0 : ℝ) < 2)
              : Measure (ConfigSpace (Sym2 (Site d)))).real (fmu_multiOpen T')

Uses 9 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Shift of a configuration by a group element · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Event that every coordinate of a finite set is open · Disjoint-box factorization bound for box measures · Wired random-cluster measure on a box · Site of the hypercubic lattice

Proof usesDomain monotonicity for translated pairs of multi-open events

Used byUpper decorrelation of the wired measure from factorization

LemmaRealized edge sets stay realized in larger boxes#✓fully proved

An edge set realized in Λ_(N₀) is realized in every larger box.

lemma fwm_realised_box_mono {N₀ N : ℕ} (h : N₀ ≤ N) {s : Finset (Sym2 (Site d))}
    {t : Finset (Sym2 (boxVerts d N₀))} (hst : s = t.image (edgeIncl d N₀)) :
    s = (t.image (innerEdgeLE d h)).image (edgeIncl d N)

Uses 6 · Used by 2

Statement usesVertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesEdge inclusion into \(\mathbb{Z}^d\) factors through \(\Lambda_m\)

Used byErgodicity of the wired random-cluster measure · Upper decorrelation of the wired measure from factorization

LemmaEvery finite family of edge sets is realized in some box#✓fully proved

Every finite family of finite edge sets is realized in some box.

lemma fwm_exists_realising_box (P : Finset (Finset (Sym2 (Site d)))) :
    ∃ N : ℕ, ∀ T ∈ P, ∃ t : Finset (Sym2 (boxVerts d N)), T = t.image (edgeIncl d N)

Uses 4 · Used by 1

Statement usesVertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Site of the hypercubic lattice

Proof usesBox \((-n, n)^d\) in the hypercubic lattice

Used byUpper decorrelation of the wired measure from factorization

LemmaWired box products approximate infinite-volume products#✓fully proved

For q = 2, products of wired box probabilities of open-edge events approximate the wired infinite-volume products within δ, for some box Λ_m with m ≥ N₀.

lemma fwm_exists_common_box_ge_wired (P : Finset (Finset (Sym2 (Site d)))) (N₀ : ℕ)
    {p : ℝ} (hp : 0 < p) (hp1 : p < 1) {δ : ℝ} (hδ : 0 < δ) :
    ∃ m : ℕ, N₀ ≤ m ∧ ∀ T ∈ P, ∀ T' ∈ P,
      |(wiredFiniteMeasure d m hp hp1 (by norm_num : (0 : ℝ) < 2)
            : Measure (ConfigSpace (Sym2 (Site d)))).real (fmu_multiOpen T)
        * (wiredFiniteMeasure d m hp hp1 (by norm_num : (0 : ℝ) < 2)
            : Measure (ConfigSpace (Sym2 (Site d)))).real (fmu_multiOpen T')
        - (wiredInfiniteVolume d hp hp1 (by norm_num : (0 : ℝ) < 2)
              : Measure (ConfigSpace (Sym2 (Site d)))).real (fmu_multiOpen T)
          * (wiredInfiniteVolume d hp hp1 (by norm_num : (0 : ℝ) < 2)
              : Measure (ConfigSpace (Sym2 (Site d)))).real (fmu_multiOpen T')| < δ

Uses 13 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Event that every coordinate of a finite set is open · Wired random-cluster measure on a box · Wired infinite-volume random-cluster measure · Site of the hypercubic lattice

Proof usesRestriction of a configuration of \(\mathbb{Z}^d\) to a box · Vertices of the box \((-n, n)^d\) · Event that every edge of a set of box edges is open, on a box · Event that every edge of a finite set is open · Inclusion of box edges into \(\mathbb{Z}^d\) · Wired infinite-volume measure as limit on increasing cylinder events · Increasing event · Box \((-n, n)^d\) in the hypercubic lattice

Used byUpper decorrelation of the wired measure from factorization

LemmaUpper decorrelation of the wired measure from factorization#✓fully proved

The factorization bound for the wired q = 2 box measures gives upper decorrelation of the wired infinite-volume measure.

lemma fwm_upperDecay_of_factorise {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (hfac : fwm_WiredDisjointBoxFactorise hp hp1
      (fun m => (wiredFiniteMeasure d m hp hp1 (by norm_num : (0 : ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d)))))) :
    fmu_UpperDecay (G := Multiplicative (Site d))
      (wiredInfiniteVolume d hp hp1 (by norm_num : (0 : ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d))))

Uses 22 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Upper decay of correlations of multi-open events · Disjoint-box factorization bound for box measures · Wired random-cluster measure on a box · Wired infinite-volume random-cluster measure · Site of the hypercubic lattice

Proof usesShift of a configuration by a group element · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Vertices of the box \((-n, n)^d\) · Event that every edge of a set of box edges is open, on a box · Event that every edge of a finite set is open · Inclusion of box edges into \(\mathbb{Z}^d\) · Infimum of wired box probabilities of a box event · Wired infinite-volume probability equals the infimum over boxes · Event that every coordinate of a finite set is open · Wired box products approximate infinite-volume products · Every finite family of edge sets is realized in some box · Finite-box product domination from the factorization bound · Realized edge sets stay realized in larger boxes · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Increasing event · Box \((-n, n)^d\) in the hypercubic lattice

Used byWired \(q = 2\) measure is ergodic under the factorization bound

LemmaWired \(q = 2\) measure is ergodic under the factorization bound#✓fully proved

If the wired q = 2 box measures satisfy the factorization bound, the wired infinite-volume measure is ergodic under translations of ℤ^d.

lemma fwm_wiredIV_isErgodic_of_factorise {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (hfac : fwm_WiredDisjointBoxFactorise hp hp1
      (fun m => (wiredFiniteMeasure d m hp hp1 (by norm_num : (0 : ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d)))))) :
    IsErgodic (G := Multiplicative (Site d))
      (wiredInfiniteVolume d hp hp1 (by norm_num : (0 : ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d))))

Uses 27 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Ergodic measure on configuration space · Disjoint-box factorization bound for box measures · Wired random-cluster measure on a box · Wired infinite-volume random-cluster measure · Site of the hypercubic lattice

Proof usesTranslation-invariant measure on configuration space · Shift of a configuration by a group element · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Vertices of the box \((-n, n)^d\) · Event that every edge of a set of box edges is open, on a box · Event that every edge of a finite set is open · Inclusion of box edges into \(\mathbb{Z}^d\) · Translation invariance of the wired \(q = 2\) infinite-volume measure · Self-mixing on cylinder events · Translation-invariant self-mixing measures are ergodic · Pair mixing of multi-open events · Upper decay of correlations of multi-open events · Product indicator of a multi-open event · Event that every coordinate of a finite set is open · Inclusion–exclusion coefficient of a multi-open event · Indicator of agreeing with a pattern on a finite set · Coordinate state as a real number · Upper decorrelation of the wired measure from factorization · FKG inequality for the wired \(q = 2\) infinite-volume measure · Increasing event · Box \((-n, n)^d\) in the hypercubic lattice

Used byErgodicity of the wired random-cluster measure

LemmaAll-open Dirac mass satisfies the factorization bound#✓fully proved

The factorization bound is satisfiable: the Dirac mass on the all-open configuration satisfies it.

lemma fwm_wiredDisjointBoxFactorise_dirac {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    [MeasurableSingletonClass (ConfigSpace (Sym2 (Site d)))] :
    fwm_WiredDisjointBoxFactorise hp hp1
      (fun _ => (Measure.dirac (fun _ : Sym2 (Site d) => true)))

Uses 10

Statement usesConfiguration space of a statistical-mechanics model · Disjoint-box factorization bound for box measures · Site of the hypercubic lattice

Proof usesShift of a configuration by a group element · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Edge inclusion into \(\mathbb{Z}^d\) factors through \(\Lambda_m\) · Event that every coordinate of a finite set is open · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Box \((-n, n)^d\) in the hypercubic lattice

DefinitionEmpty boundary predicate#✓fully proved

The empty boundary predicate.

def bdp_noBdry (_v : Vout) : Prop := False

Used by 3

Used byPer-box uniqueness of the random-cluster measures off a countable set · Free off-centre lower bound by the recentred small-box marginal · Translation invariance of the free \(q = 2\) infinite-volume measure

TheoremTranslation invariance of the free \(q = 2\) infinite-volume measure#✓fully proved

The free q = 2 infinite-volume random-cluster measure on ℤ^d is translation invariant.

theorem bdp_freeIV_isTranslationInvariant {p : ℝ} (hp : 0 < p) (hp1 : p < 1) :
    ConfigSpace.IsTranslationInvariant (G := Multiplicative (Site d))
      (freeInfiniteVolume d hp hp1 (by norm_num : (0 : ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d))))

Uses 59 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Translation-invariant measure on configuration space · Free infinite-volume random-cluster measure · Site of the hypercubic lattice

Proof usesRandom-cluster probability with a boundary wiring · Empty wiring gives the free random-cluster measure · Random-cluster comparison of boundary conditions for \(q \ge 1\) · Random-cluster weight with a boundary wiring · Partition function with a boundary wiring · Empty boundary predicate · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Event that every edge of a finite set is open · Conditional random-cluster measure with a boundary wiring · Fibre of configurations agreeing off an edge set · Inclusion of box edges into \(\mathbb{Z}^d\) · Edge inclusion into \(\mathbb{Z}^d\) factors through \(\Lambda_m\) · Bernoulli edge product · Probability of an ambient FK configuration · Unnormalized random-cluster weight · Ambient FK normalizer · Inclusion of a subset of sites into a larger one · Box edge set included into \(\Lambda_m\) and translated by \(v\) · Sup norm of a site of \(\mathbb{Z}^d\) · Free random-cluster measure on a box · Translated box in \(\mathbb{Z}^d\) · Vertex type of a translated box · Translation from the centered box onto a translated box · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Free translation invariance from the placement hypothesis · Free placement hypothesis for a shift via box-mass limits · Translated free box mass of an edge set · Edge inclusion of a translated box into \(\mathbb{Z}^d\) · Images of translated edge sets are shifted images · Free box measure of an all-open event equals its box mass · Free all-open probabilities converge to the infinite-volume value · Event that all edges of a finite set are open · Mass of the all-open event under a weight function · Number of open clusters · Number of clusters under a boundary wiring · Adjacency matching of the inner embedding · Law of total probability over outside configurations · Conditional outer probability as an induced-wiring probability · Wiring induced on the inner graph · Image of an inner-graph edge in the outer graph · Finite set of inner edges · Restriction of an outer configuration to inner edges · Restriction pulls back all-open events to their images · Restricting a glued configuration recovers the inner one · Lattice inclusion matches induced adjacency · Projection closing every inner edge · Gluing of inner and outer configurations · Outer wired fibre masses sum to one · Open subgraph of an edge configuration · Increasing event · Complete graph on the boundary vertices · Box \((-n, n)^d\) in the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Boundary wiring relation

Used byEvery lattice edge has the free \(q = 2\) density of \(\{0, e_0\}\)

LemmaFree \(q = 2\) box edge marginals are at most the free density#✓fully proved

Edge marginals of the free box measure are at most the free infinite-volume density (the case N = n of dfi_free_per_edge_le).

lemma bdp_free_per_edge_upper (n : ℕ) (e : Sym2 (boxVerts d n)) {p : ℝ}
    (hp : 0 < p) (hp1 : p < 1) :
    edgeMargProb (fkProb (boxGraph d n) p 2) e
      ≤ freeEdgeDensity d 2 (edgeIncl d n e) p

Uses 23 · Used by 1

Statement usesNearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Edge marginal of a mass function · Probability of an ambient FK configuration · Free infinite-volume edge density · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesConfiguration space of a statistical-mechanics model · Event that a box edge is open · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Restriction of a configuration from \(\Lambda_m\) to \(\Lambda_n\) · Restriction to \(\Lambda_n\) factors through \(\Lambda_m\) · Inclusion of \(\Lambda_n\) into \(\Lambda_m\) for \(n \le m\) · Event that an edge is open · Limit of free \(q = 2\) box measures of a cylinder event · Free \(q = 2\) infinite-volume mass of increasing cylinders as a box limit · Free \(q = 2\) box measures are bounded by the limit value · Free random-cluster measure on a box · Free box measure of a cylinder event as a finite sum · Free infinite-volume random-cluster measure · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Increasing event

Used byTwo-sided free \(q = 2\) bulk bounds from the free sandwich

LemmaWired \(q = 2\) box edge marginals are at least the wired density#✓fully proved

Edge marginals of the wired box measure are at least the wired infinite-volume density (the case N = n of dfi_wired_per_edge_ge).

lemma bdp_wired_per_edge_lower (n : ℕ) (e : Sym2 (boxVerts d n)) {p : ℝ}
    (hp : 0 < p) (hp1 : p < 1) :
    wiredEdgeDensity d 2 (edgeIncl d n e) p
      ≤ edgeMargProb (wiredFkProb (boxGraph d n) (boxBoundary d n) p 2) e

Uses 23 · Used by 1

Statement usesVertex boundary of a box · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Edge marginal of a mass function · Wired infinite-volume edge density · Wired random-cluster probability of a configuration · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesConfiguration space of a statistical-mechanics model · Event that a box edge is open · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Restriction of a configuration from \(\Lambda_m\) to \(\Lambda_n\) · Restriction to \(\Lambda_n\) factors through \(\Lambda_m\) · Inclusion of \(\Lambda_n\) into \(\Lambda_m\) for \(n \le m\) · Event that an edge is open · Infimum of wired box probabilities of a box event · Wired infinite-volume probability equals the infimum over boxes · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Wired random-cluster measure on a box · Wired \(\Lambda_m\) measure of a \(\Lambda_m\) cylinder event as a sum · Wired infinite-volume random-cluster measure · Increasing event

Used byTwo-sided wired \(q = 2\) bulk bounds from the wired sandwich

DefinitionFree off-centre sandwich hypothesis#✓fully proved

For every edge e' of Λ_N and every t, there are interior edge sets I_n of Λ_n carrying asymptotically all edges on which the free density equals that of e' and the free box marginals are at least that density minus δ_n → 0.

def bdp_FreeOffCentreSandwich (N : ℕ) : Prop :=
  ∀ (e' : Sym2 (boxVerts d N)) (t : ℝ),
    ∃ (In : (n : ℕ) → Finset (Sym2 (boxVerts d n))) (δ : ℕ → ℝ),
      (∀ n, In n ⊆ (boxGraph d n).edgeFinset) ∧
      (∀ n, 0 ≤ δ n) ∧ Tendsto δ atTop (𝓝 0) ∧
      (∀ n, ∀ e ∈ In n,
        freeEdgeDensity d 2 (edgeIncl d n e) (fsc_logistic t)
          = freeEdgeDensity d 2 (edgeIncl d N e') (fsc_logistic t)) ∧
      (∀ n, ∀ e ∈ In n,
        freeEdgeDensity d 2 (edgeIncl d N e') (fsc_logistic t) - δ n
          ≤ edgeMargProb (fkProb (boxGraph d n) (fsc_logistic t) 2) e) ∧
      Tendsto (fun n =>
        (((boxGraph d n).edgeFinset.card - (In n).card : ℝ)) / (boxGraph d n).edgeFinset.card)
        atTop (𝓝 0)

Uses 9 · Used by 1

Statement usesNearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Edge marginal of a mass function · Probability of an ambient FK configuration · Free infinite-volume edge density · Logistic function \(e^t/(1+e^t)\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byFree off-centre sandwich from free rotation residues

DefinitionWired off-centre sandwich hypothesis#✓fully proved

For every edge e' of Λ_N and every t, there are interior edge sets I_n of Λ_n carrying asymptotically all edges on which the wired density equals that of e' and the wired box marginals are at most that density plus δ_n → 0.

def bdp_WiredOffCentreSandwich (N : ℕ) : Prop :=
  ∀ (e' : Sym2 (boxVerts d N)) (t : ℝ),
    ∃ (In : (n : ℕ) → Finset (Sym2 (boxVerts d n))) (δ : ℕ → ℝ),
      (∀ n, In n ⊆ (boxGraph d n).edgeFinset) ∧
      (∀ n, 0 ≤ δ n) ∧ Tendsto δ atTop (𝓝 0) ∧
      (∀ n, ∀ e ∈ In n,
        wiredEdgeDensity d 2 (edgeIncl d n e) (fsc_logistic t)
          = wiredEdgeDensity d 2 (edgeIncl d N e') (fsc_logistic t)) ∧
      (∀ n, ∀ e ∈ In n,
        edgeMargProb (wiredFkProb (boxGraph d n) (boxBoundary d n) (fsc_logistic t) 2) e
          ≤ wiredEdgeDensity d 2 (edgeIncl d N e') (fsc_logistic t) + δ n) ∧
      Tendsto (fun n =>
        (((boxGraph d n).edgeFinset.card - (In n).card : ℝ)) / (boxGraph d n).edgeFinset.card)
        atTop (𝓝 0)

Uses 10 · Used by 1

Statement usesVertex boundary of a box · Nearest-neighbour graph on a box · Vertices of the box \((-n, n)^d\) · Inclusion of box edges into \(\mathbb{Z}^d\) · Edge marginal of a mass function · Logistic function \(e^t/(1+e^t)\) · Wired infinite-volume edge density · Wired random-cluster probability of a configuration · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byWired off-centre sandwich from wired rotation residues

DefinitionShift vector moving \(\Lambda_N\) to a disjoint box#✓fully proved

The vector (2N + 1) e_{i₀}, which translates Λ_N to a disjoint box.

noncomputable def cbk_shiftVec {d : ℕ} (i₀ : Fin d) (N : ℕ) : Site d :=
  fun i => if i = i₀ then (2 * N + 1 : ℤ) else 0

Uses 1 · Used by 1

Statement usesSite of the hypercubic lattice

Used byErgodicity of the wired random-cluster measure

DefinitionTranslate of a vertex of \(\Lambda_N\) as a vertex of \(\Lambda_{N+r}\)#✓fully proved

The vertex of Λ_{N+r} obtained by translating a vertex of Λ_N by v with ‖v‖_∞ ≤ r.

noncomputable def cbk_shiftBoxVert {N r : ℕ} (v : Site d) (hv : flc_vrad v ≤ r)
    (a : boxVerts d N) : boxVerts d (N + r) :=
  ⟨v + (a : Site d), by
    intro i
    have ha : ((a : Site d) i).natAbs ≤ N := a.2 i
    have hvi : (v i).natAbs ≤ flc_vrad v := flc_vrad_le v i
    have : ((v + (a : Site d)) i) = v i + (a : Site d) i := by simp [Pi.add_apply]
    rw [this]
    calc (v i + (a : Site d) i).natAbs ≤ (v i).natAbs + ((a : Site d) i).natAbs :=
          Int.natAbs_add_le _ _
      _ ≤ flc_vrad v + N := Nat.add_le_add hvi ha
      _ ≤ N + r := by omega⟩

Uses 4 · Used by 2

Statement usesVertices of the box \((-n, n)^d\) · Sup norm of a site of \(\mathbb{Z}^d\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byTranslate of an edge of \(\Lambda_N\) as an edge of \(\Lambda_{N+r}\) · Ergodicity of the wired random-cluster measure

DefinitionTranslate of an edge of \(\Lambda_N\) as an edge of \(\Lambda_{N+r}\)#✓fully proved

The edge of Λ_{N+r} obtained by translating an edge of Λ_N by v with ‖v‖_∞ ≤ r.

noncomputable def cbk_shiftEdge {N r : ℕ} (v : Site d) (hv : flc_vrad v ≤ r) :
    Sym2 (boxVerts d N) → Sym2 (boxVerts d (N + r)) :=
  Sym2.map (cbk_shiftBoxVert v hv)

Uses 4 · Used by 1

Statement usesVertices of the box \((-n, n)^d\) · Translate of a vertex of \(\Lambda_N\) as a vertex of \(\Lambda_{N+r}\) · Sup norm of a site of \(\mathbb{Z}^d\) · Site of the hypercubic lattice

Used byErgodicity of the wired random-cluster measure

TheoremErgodicity of the wired random-cluster measure#✓fully proved

For d ≥ 1 and p ∈ (0, 1), the wired q = 2 infinite-volume random-cluster measure on ℤ^d is ergodic under translations (Grimmett, The Random-Cluster Model, 2006, Theorem 4.19).

theorem cbk_wiredIV_isErgodic {d : ℕ} (hd : 1 ≤ d) {p : ℝ} (hp : 0 < p) (hp1 : p < 1) :
    IsErgodic (G := Multiplicative (Site d))
      (wiredInfiniteVolume d hp hp1 (by norm_num : (0 : ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d))))

Uses 74

Statement usesConfiguration space of a statistical-mechanics model · Ergodic measure on configuration space · Wired infinite-volume random-cluster measure · Site of the hypercubic lattice

Proof usesShift of a configuration by a group element · Agreement of configurations off an edge set · Event depending only on edges outside a set · Random-cluster probability with a boundary wiring · Boundary clique gives the wired random-cluster measure · Disintegration of a boundary-wired measure over conditioning fibres · Random-cluster weight with a boundary wiring · Partition function with a boundary wiring · Vertex boundary of a box · Nearest-neighbour graph on a box · Restriction of a configuration of \(\mathbb{Z}^d\) to a box · Inclusion of \(\Lambda_n\) into \(\Lambda_m\) for \(n \le m\) · Vertices of the box \((-n, n)^d\) · Translate of a vertex of \(\Lambda_N\) as a vertex of \(\Lambda_{N+r}\) · Translate of an edge of \(\Lambda_N\) as an edge of \(\Lambda_{N+r}\) · Shift vector moving \(\Lambda_N\) to a disjoint box · Event that every edge of a set of box edges is open, on a box · Event that every edge of a finite set is open · Conditional random-cluster measure with a boundary wiring · Conditional measures increase with the wiring for \(q \ge 1\) · Fibre of configurations agreeing off an edge set · Inclusion of box edges into \(\mathbb{Z}^d\) · Edge inclusion into \(\mathbb{Z}^d\) factors through \(\Lambda_m\) · Bernoulli edge product · Fibre representatives with every edge of a set closed · Inclusion of a subset of sites into a larger one · Box edge set included into \(\Lambda_m\) and translated by \(v\) · Sup norm of a site of \(\mathbb{Z}^d\) · Event that every coordinate of a finite set is open · Translated box in \(\mathbb{Z}^d\) · Vertex boundary of a translated box · Nearest-neighbour graph on a translated box · Vertex type of a translated box · Translation from the centered box onto a translated box · Disjoint-box factorization bound for box measures · Realized edge sets stay realized in larger boxes · Wired \(q = 2\) measure is ergodic under the factorization bound · Domain monotonicity for edge sets realized in a box · Partition function of a conditioning fibre · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Wired all-open probability on a translated box · Translated wired box mass equals the centered box mass · Edge inclusion of a translated box into \(\mathbb{Z}^d\) · Images of translated edge sets are shifted images · Wired box measure of an all-open event equals its box mass · Event that all edges of a finite set are open · Mass of the all-open event under a weight function · Number of clusters under a boundary wiring · Adjacency matching of the inner embedding · Conditional outer wired probability at most the inner wired one, \(q \ge 1\) · Wiring induced on the inner graph · Image of an inner-graph edge in the outer graph · Finite set of inner edges · Restriction of an outer configuration to inner edges · Restriction pulls back all-open events to their images · Lattice inclusion matches induced adjacency · Lattice induced wirings are coarser than the inner boundary clique · Outer wired all-open probability at most the inner wired one · Inner edge set is the range of the edge map · Closing the edges of a set in a configuration · Wired random-cluster measure on a box · Wired \(\Lambda_m\) measure of a \(\Lambda_m\) cylinder event as a sum · Wired random-cluster probability of a configuration · Increasing event · Nearest neighbours in \(\mathbb{Z}^d\) · Complete graph on the boundary vertices · Box \((-n, n)^d\) in the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Inner vertex boundary of a box · Boundary wiring relation

116 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.