Multi-edge events and translation invariance of q = 2 FK measures

15 fully proved

A. Multi-edge events

DefinitionEvent that all edges of a finite set are open#✓fully proved

The event A_t that every edge of the finite set t is open. On box configurations it is cdc_boxMultiOpenEvent (med_boxMultiOpenEvent_eq).

def med_genericMultiOpenEvent {V : Type*} (t : Finset (Sym2 V)) :
    Set (ConfigSpace (Sym2 V)) :=
  {ω | ∀ e ∈ t, ω e = true}

Uses 1 · Used by 10

Statement usesConfiguration space of a statistical-mechanics model

Used byRestriction pulls back all-open events to their images · Outer wired all-open probability at most the inner wired one · Translation covariance of free box masses · Translation covariance of wired box masses · Mass of the all-open event under a weight function · Per-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

B. Finite-volume masses

DefinitionMass of the all-open event under a weight function#✓fully proved

The mass ∑_ω 1_{A_t}(ω) μ(ω) of the event that every edge of t is open, for a weight function μ on a finite configuration space; it is eventMassProb μ A_t (med_multiMassProb_eq_eventMassProb).

noncomputable def med_multiMassProb (μ : ConfigSpace (Sym2 V) → ℝ) (t : Finset (Sym2 V)) : ℝ :=
  ∑ ω : ConfigSpace (Sym2 V),
    (med_genericMultiOpenEvent t).indicator (fun _ => (1 : ℝ)) ω * μ ω

Uses 2 · Used by 22

Statement usesConfiguration space of a statistical-mechanics model · Event that all edges of a finite set are open

Used byOuter wired all-open probability at most the inner wired one · Translation covariance of free box masses · Translation covariance of wired box masses · Wired box measure of an all-open event equals its box mass · Free box measure of an all-open event equals its box mass · Free translation invariance from free placements of every shift · Equal free probabilities from eventually equal translated masses · Free placement for a shift via eventually equal box masses · Difference of wired all-open masses of an edge set and its translate · Wired translation invariance from wired placements of every shift · Equal wired probabilities from eventually equal translated masses · Wired placement for a shift via eventually equal box masses · Per-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 · Wired all-open probability on a translated box · Translated wired box mass equals the centered box mass · Translated free box mass of an edge set · Translated free box mass equals the centred box probability

LemmaWired box measure of an all-open event equals its box mass#✓fully proved

The wired box measure on Λ_m, pushed to ℤ^d, gives A_t the box mass of t.

lemma med_centred_mass_eq (m : ℕ) (t : Finset (Sym2 (boxVerts d m))) {p : ℝ}
    (hp : 0 < p) (hp1 : p < 1) :
    (wiredFiniteMeasure d m hp hp1 (by norm_num : (0 : ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d)))).real
          (cdc_multiOpenEvent (t.image (edgeIncl d m)))
      = med_multiMassProb (wiredFkProb (boxGraph d m) (boxBoundary d m) p 2) t

Uses 14 · Used by 4

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\) · Event that every edge of a finite set is open · Inclusion of box edges into \(\mathbb{Z}^d\) · Mass of the all-open event under a weight function · 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 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 · Wired \(\Lambda_m\) measure of a \(\Lambda_m\) cylinder event as a sum

Used byEqual wired probabilities from eventually equal translated masses · Ergodicity 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

LemmaFree box measure of an all-open event equals its box mass#✓fully proved

The free box measure on Λ_m, pushed to ℤ^d, gives A_t the box mass of t.

lemma med_free_centred_mass_eq (m : ℕ) (t : Finset (Sym2 (boxVerts d m))) {p : ℝ}
    (hp : 0 < p) (hp1 : p < 1) :
    (freeFiniteMeasure d m hp hp1 (by norm_num : (0 : ℝ) < 2)
        : Measure (ConfigSpace (Sym2 (Site d)))).real
          (cdc_multiOpenEvent (t.image (edgeIncl d m)))
      = med_multiMassProb (fkProb (boxGraph d m) p 2) t

Uses 13 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · 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\) · Probability of an ambient FK configuration · Free random-cluster measure on a box · Mass of the all-open event under a weight function · Site of the hypercubic lattice · Box \((-n, n)^d\) in 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 · Free box measure of a cylinder event as a finite sum

Used byEqual free probabilities from eventually equal translated masses · Translation invariance of the free \(q = 2\) infinite-volume measure · Translated free box mass equals the centred box probability

C. Translation covariance

LemmaTranslation covariance of wired box masses#✓fully proved

The wired mass of t in Λ_m equals the wired mass of t + v in v + Λ_m.

lemma med_centred_eq_translated_wired (m : ℕ) (v : Site d) (t : Finset (Sym2 (boxVerts d m)))
    {p : ℝ} :
    med_multiMassProb (wiredFkProb (boxGraph d m) (boxBoundary d m) p 2) t
      = med_multiMassProb
          (wiredFkProb (fvs_transBoxGraph d m v) (fvs_transBoxBoundary d m v) p 2)
          (t.image (Sym2.map (fvs_transEquiv d m v)))

Uses 19 · Used by 2

Statement usesVertex boundary of a box · Nearest-neighbour graph on a box · Vertices 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 · 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

Proof usesConfiguration space of a statistical-mechanics model · Boundary-matching isomorphisms preserve wired FK probabilities · Event that all edges of a finite set are open · Pull-back of an edge configuration along a vertex bijection · Pull-back of configurations as an equivalence · Hypercubic lattice \(\mathbb{Z}^d\) · Inner vertex boundary of a box

Used byEqual wired probabilities from eventually equal translated masses · Translated wired box mass equals the centered box mass

LemmaTranslation covariance of free box masses#✓fully proved

The free mass of t in Λ_m equals the free mass of t + v in v + Λ_m.

lemma med_centred_eq_translated_free (m : ℕ) (v : Site d) (t : Finset (Sym2 (boxVerts d m)))
    {p : ℝ} :
    med_multiMassProb (fkProb (boxGraph d m) p 2) t
      = med_multiMassProb
          (fkProb (fvs_transBoxGraph d m v) p 2)
          (t.image (Sym2.map (fvs_transEquiv d m v)))

Uses 16 · Used by 2

Statement usesNearest-neighbour graph on a box · Vertices 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 · Mass of the all-open event under a weight function · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesConfiguration space of a statistical-mechanics model · Isomorphic graphs have equal free FK probabilities after relabelling · Event that all edges of a finite set are open · Pull-back of an edge configuration along a vertex bijection · Pull-back of configurations as an equivalence · Hypercubic lattice \(\mathbb{Z}^d\)

Used byEqual free probabilities from eventually equal translated masses · Translated free box mass equals the centred box probability

D. Limits along boxes

LemmaWired all-open probabilities converge to the infinite-volume value#✓fully proved

Restatement of cdc_wired_multiOpenEvent_tendsto: the wired box probabilities of A_t converge to the wired infinite-volume probability.

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

Uses 11 · 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 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 · Event that every edge of a set of box edges is open, on a box · Wired infinite-volume measure as limit on increasing cylinder events · Increasing event

Used byEqual wired probabilities from eventually equal translated masses · Translation invariance of the wired \(q = 2\) infinite-volume measure · Translated wired box masses converge to the infinite-volume mass · Wired shift invariance of an all-open event from decaying differences

LemmaFree all-open probabilities converge to the infinite-volume value#✓fully proved

Restatement of cdc_free_multiOpenEvent_tendsto: the free box probabilities of A_t converge to the free infinite-volume probability.

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

Uses 11 · 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\) · Free random-cluster measure on a box · Free infinite-volume random-cluster measure · 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 · Free \(q=2\) box masses of increasing cylinders tend to infinite volume · Increasing event

Used byEqual free probabilities from eventually equal translated masses · Translation invariance of the free \(q = 2\) infinite-volume measure · Translated free box masses converge to the free infinite-volume value

E. The off-centre multi-edge carrier

DefinitionDifference of wired all-open masses of an edge set and its translate#✓fully proved

The difference between the wired mass of t in Λ_m and the wired mass of t + v in v + Λ_m; it vanishes by translation covariance.

noncomputable def med_offCentreMultiCarrier (v : Site d) (N : ℕ) (t : Finset (Sym2 (boxVerts d N)))
    (p : ℝ) (m : ℕ) (hNm : N ≤ m) : ℝ :=
  med_multiMassProb (wiredFkProb (boxGraph d m) (boxBoundary d m) p 2)
      (t.image (innerEdgeLE d hNm))
    - 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 13

Statement usesVertex boundary of a box · Nearest-neighbour graph on a box · Vertices 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

F. Homogeneity from translated masses

LemmaEqual wired probabilities from eventually equal translated masses#✓fully proved

If the wired mass of t + v in v + Λ_m eventually equals the wired mass of t' in Λ_m, the wired infinite-volume measure gives A_t and A_{t'} the same probability.

lemma med_wiredMultiHomogeneous_of_cofinal (v : Site d) (N : ℕ)
    (t t' : Finset (Sym2 (boxVerts d N))) {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (htrans : ∀ᶠ m in atTop, ∀ (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)))
          = med_multiMassProb (wiredFkProb (boxGraph d m) (boxBoundary d m) p 2)
              (t'.image (innerEdgeLE d hNm))) :
    (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)))

Uses 22 · 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\) · Event that every edge of a finite set is open · Inclusion of box edges into \(\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\) · Mass of the all-open event under a weight function · Wired random-cluster probability of a configuration · Wired infinite-volume random-cluster measure · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Proof usesEdge inclusion into \(\mathbb{Z}^d\) factors through \(\Lambda_m\) · Translation covariance of wired box masses · Wired box measure of an all-open event equals its box mass · Wired all-open probabilities converge to the infinite-volume value · Wired random-cluster measure on a box

Used byWired translation invariance from wired placements of every shift

LemmaEqual free probabilities from eventually equal translated masses#✓fully proved

If the free mass of t + v in v + Λ_m eventually equals the free mass of t' in Λ_m, the free infinite-volume measure gives A_t and A_{t'} the same probability.

lemma med_freeMultiHomogeneous_of_cofinal (v : Site d) (N : ℕ)
    (t t' : Finset (Sym2 (boxVerts d N))) {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (htrans : ∀ᶠ m in atTop, ∀ (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)))
          = med_multiMassProb (fkProb (boxGraph d m) p 2) (t'.image (innerEdgeLE d hNm))) :
    (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)))

Uses 20 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · 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\) · Probability of an ambient FK configuration · Free infinite-volume random-cluster measure · 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

Proof usesEdge inclusion into \(\mathbb{Z}^d\) factors through \(\Lambda_m\) · Free random-cluster measure on a box · Translation covariance of free box masses · Free box measure of an all-open event equals its box mass · Free all-open probabilities converge to the infinite-volume value

Used byFree translation invariance from free placements of every shift

G. Placements and translation invariance

DefinitionWired placement for a shift via eventually equal box masses#✓fully proved

A wired placement for the shift g: every finite edge set s and its shift g⁻¹ s are images of box edge sets t, t' of a common box Λ_N such that the wired mass of t + g in g + Λ_m eventually equals the wired mass of t' in Λ_m. See also lmc_wiredPlacement.

def med_wiredPlacement {p : ℝ} (_hp : 0 < p) (_hp1 : p < 1) (g : Multiplicative (Site d)) : Prop :=
  ∀ s : Finset (Sym2 (Site d)),
    ∃ (N : ℕ) (t t' : Finset (Sym2 (boxVerts d N))),
      s = t.image (edgeIncl d N)
        ∧ s.image (fun e => g⁻¹ • e) = t'.image (edgeIncl d N)
        ∧ (∀ᶠ m in atTop, ∀ (hNm : N ≤ m),
            med_multiMassProb
                (wiredFkProb (fvs_transBoxGraph d m (Multiplicative.toAdd g))
                  (fvs_transBoxBoundary d m (Multiplicative.toAdd g)) p 2)
                ((t.image (innerEdgeLE d hNm)).image
                  (Sym2.map (fvs_transEquiv d m (Multiplicative.toAdd g))))
              = med_multiMassProb (wiredFkProb (boxGraph d m) (boxBoundary d m) p 2)
                  (t'.image (innerEdgeLE d hNm)))

Uses 14 · 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\) · 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 byWired translation invariance from wired placements of every shift

DefinitionFree placement for a shift via eventually equal box masses#✓fully proved

A free placement for the shift g, defined as med_wiredPlacement with free masses.

def med_freePlacement {p : ℝ} (_hp : 0 < p) (_hp1 : p < 1) (g : Multiplicative (Site d)) : Prop :=
  ∀ s : Finset (Sym2 (Site d)),
    ∃ (N : ℕ) (t t' : Finset (Sym2 (boxVerts d N))),
      s = t.image (edgeIncl d N)
        ∧ s.image (fun e => g⁻¹ • e) = t'.image (edgeIncl d N)
        ∧ (∀ᶠ m in atTop, ∀ (hNm : N ≤ m),
            med_multiMassProb (fkProb (fvs_transBoxGraph d m (Multiplicative.toAdd g)) p 2)
                ((t.image (innerEdgeLE d hNm)).image
                  (Sym2.map (fvs_transEquiv d m (Multiplicative.toAdd g))))
              = med_multiMassProb (fkProb (boxGraph d m) p 2) (t'.image (innerEdgeLE d hNm)))

Uses 12 · 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\) · 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 byFree translation invariance from free placements of every shift

LemmaWired translation invariance from wired placements of every shift#✓fully proved

The wired infinite-volume q = 2 measure is translation invariant if every shift has a wired placement. See also flc_wiredIV_isTranslationInvariant, which proves invariance without hypotheses.

lemma med_wiredIV_isTranslationInvariant_of_placement {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (hplace : ∀ g : Multiplicative (Site d), med_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 37

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

Proof usesShift of a configuration by a group element · 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 · 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 · 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 · 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 · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Shift-decay functional of a sequence of measures · Mass of the all-open event under a weight function · Equal wired probabilities from eventually equal translated masses · Wired random-cluster measure on a box · Wired random-cluster probability of a configuration · Increasing event · Box \((-n, n)^d\) in the hypercubic lattice · Weak convergence of probability measures on configuration space

LemmaFree translation invariance from free placements of every shift#✓fully proved

The free infinite-volume q = 2 measure is translation invariant if every shift has a free placement. See also bdp_freeIV_isTranslationInvariant, which proves invariance without hypotheses.

lemma med_freeIV_isTranslationInvariant_of_placement {p : ℝ} (hp : 0 < p) (hp1 : p < 1)
    (hplace : ∀ g : Multiplicative (Site d), med_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 35

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

Proof usesShift of a configuration by a group element · 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 · 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\) · Probability of an ambient FK configuration · Free \(q=2\) box masses of increasing cylinders tend to infinite volume · Free random-cluster measure on a box · 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 · 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 · Inclusion of edges of \(\Lambda_n\) into edges of \(\Lambda_m\) · Shift-decay functional of a sequence of measures · Equal free probabilities from eventually equal translated masses · Mass of the all-open event under a weight function · Increasing event · Box \((-n, n)^d\) in the hypercubic lattice · Weak convergence of probability measures on configuration space

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.