Translation invariance and ergodicity of random fields

DefinitionShift of a configuration by a group element#✓fully proved

The shift of a configuration by g : G: (shift g ω) e = ω (g⁻¹ • e). This is the action arrowAction of Mathlib on functions out of E.

def shift (g : G) (ω : ConfigSpace E) : ConfigSpace E := fun e => ω (g⁻¹ • e)

Uses 1 · Used by 61

Statement usesConfiguration space of a statistical-mechanics model

Used byShift-invariant countably valued functions are a.s. constant under ergodicity · Number of infinite clusters is almost surely constant · Translation of the open subgraph as a graph homomorphism · Inverse translation of the open subgraph · Translation invariance of the Bernoulli product measure · Exponential decay below p̃_c · Bernoulli zero-one law for infinite groups acting finite-to-one · Ergodicity of Bernoulli measures under free infinite-group actions · Ergodic measure on configuration space · Translation-invariant measure on configuration space · Configuration shift is the action on functions · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Nonvacuity of the a.s.-tail theorem via the all-plus Dirac mass · All-plus Dirac mass gives the all-plus event probability one · Ergodicity of the plus state · Translation invariance of the plus state · Extremality of the plus state · Continuous functions with decaying shifted integrals · Decay of shifted integrals for minus box measures · Shifted minus-boundary box measure · Decay of shifted integrals for plus box measures · Shifted plus-boundary box measure · Difference between an integral and its shifted version · Free translation invariance from free placements of every shift · Wired translation invariance from wired placements of every shift · Every lattice edge has the free \(q = 2\) density of \(\{0, e_0\}\) · Every lattice edge has the wired \(q = 2\) density of \(\{0, e_0\}\) · Almost-invariant events are trivial under an ergodic measure · Ergodicity of the wired random-cluster measure · Submodule of functions with vanishing free shift decay · Submodule of functions with vanishing wired shift decay · Translated free box measure · Translated wired box measure · Conditional product cap for multi-open events in boxes · Extreme invariant measures are ergodic · Translation-invariant self-mixing measures are ergodic · Self-mixing on cylinder events · Mixing for finite families of cylinder events · 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 · 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 · Wired \(q = 2\) measure is ergodic under the factorization bound · Decay of the edge-indicator functional from equal wired densities · Shift-decay functional of a sequence of measures · Shift decay extends from a dense set of test functions · Free integral shift decay along a box sequence · Identity shift satisfies the free decay hypothesis · Free translation invariance from integral shift decay · Wired integral shift decay along a box sequence · Identity shift satisfies the wired decay hypothesis · Wired translation invariance from integral shift decay · Free translation invariance from the placement hypothesis · Wired translation invariance from the placement hypothesis · 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\)

LemmaConfiguration shift is the action on functions#✓fully proved

shift is Mathlib's arrowAction of G on functions E → Bool.

lemma shift_eq_arrowAction_smul (g : G) (ω : ConfigSpace E) :
    letI := arrowAction (G := G) (A := E) (B := Bool)
    shift g ω = g • ω

Uses 2

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

DefinitionTranslation-invariant measure on configuration space#✓fully proved

A measure on ConfigSpace E is translation invariant if every shift shift g, g : G, preserves it.

def IsTranslationInvariant (μ : Measure (ConfigSpace E)) : Prop :=
  ∀ g : G, MeasureTheory.MeasurePreserving (shift g : ConfigSpace E → ConfigSpace E) μ μ

Uses 2 · Used by 32

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

Used byShift-invariant countably valued functions are a.s. constant under ergodicity · Translation invariance of the Bernoulli product measure · Bernoulli zero-one law for infinite groups acting finite-to-one · Ergodicity of Bernoulli measures under free infinite-group actions · Ergodic measure on configuration space · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Nonvacuity of the a.s.-tail theorem via the all-plus Dirac mass · All-plus Dirac mass gives the all-plus event probability one · Ergodicity of the plus state · Translation invariance of the plus state · Extremality of the plus state · Free translation invariance from free placements of every shift · Wired translation invariance from wired placements of every shift · Every lattice edge has the free \(q = 2\) density of \(\{0, e_0\}\) · Every lattice edge has the wired \(q = 2\) density of \(\{0, e_0\}\) · Almost-invariant events are trivial under an ergodic measure · Translation invariance of the free \(q = 2\) infinite-volume measure · Extreme invariant measures are ergodic · Translation invariance of the wired \(q = 2\) infinite-volume measure · Translation-invariant self-mixing measures are ergodic · Wired \(q = 2\) measure is ergodic under the factorization bound · Translation invariance of the free FK measure from cylinder decay · Translation invariance of the wired FK measure from cylinder decay · Extreme point of the invariant probability measures · Free translation invariance from decay on a dense set · Wired translation invariance from decay on a dense set · Free translation invariance from integral shift decay · Wired translation invariance from integral shift decay · Free translation invariance from the placement hypothesis · Wired translation invariance from the placement hypothesis · 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\)

DefinitionErgodic measure on configuration space#✓fully proved

A measure on ConfigSpace E is ergodic for the shift action of G if it is translation invariant and every measurable set with shift g ⁻¹' s = s for all g has measure 0 or μ univ. See also Mathlib's ErgodicSMul, which asks the same for a.e.-invariant sets.

def IsErgodic (μ : Measure (ConfigSpace E)) : Prop :=
  IsTranslationInvariant (G := G) μ ∧
    ∀ s : Set (ConfigSpace E), MeasurableSet s →
      (∀ g : G, (shift g : ConfigSpace E → ConfigSpace E) ⁻¹' s = s) →
        μ s = 0 ∨ μ s = μ Set.univ

Uses 3 · Used by 12

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

Used byShift-invariant countably valued functions are a.s. constant under ergodicity · Number of infinite clusters is almost surely constant · Zero or one infinite cluster, given ergodicity and \(\mu(N \ge 2) = 0\) · Ergodicity of Bernoulli measures under free infinite-group actions · All-plus Dirac mass gives the all-plus event probability one · Ergodicity of the plus state · Extremality of the plus state · Almost-invariant events are trivial under an ergodic measure · Ergodicity of the wired random-cluster measure · Extreme invariant measures are ergodic · Translation-invariant self-mixing measures are ergodic · Wired \(q = 2\) measure is ergodic under the factorization bound

LemmaIndependence of coordinates under the Bernoulli product measure#✓fully proved

Coordinates are independent under the Bernoulli product measure. See also Mathlib's ProbabilityTheory.iIndepFun_infinitePi, of which this is a special case.

lemma bernoulli_iIndepFun (p : ℝ≥0) (hp : p ≤ 1) :
    iIndepFun (fun (e : E) (ω : ConfigSpace E) => ω e)
      (bernoulliProductMeasure (E := E) p hp)

Uses 3 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli product measure on configuration space

Proof usesBernoulli distribution on the Booleans

Used byBernoulli product pulled back along an injection is Bernoulli · Bernoulli zero-one law for infinite groups acting finite-to-one

LemmaBernoulli zero-one law for infinite groups acting finite-to-one#✓fully proved

Invariant events of the Bernoulli product measure have probability 0 or 1.

lemma bernoulli_ergodic [Countable E] [Infinite G]
    (hfin : ∀ a b : E, {g : G | g • a = b}.Finite)
    (p : ℝ≥0) (hp : p ≤ 1) {s : Set (ConfigSpace E)} (hs : MeasurableSet s)
    (hinv : ∀ g : G, (shift g : ConfigSpace E → ConfigSpace E) ⁻¹' s = s) :
    bernoulliProductMeasure (E := E) p hp s = 0 ∨
      bernoulliProductMeasure (E := E) p hp s
        = bernoulliProductMeasure (E := E) p hp Set.univ

Uses 7 · Used by 1

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

Proof usesTranslation-invariant measure on configuration space · Independence of coordinates under the Bernoulli product measure · Translation invariance of the Bernoulli product measure · Bernoulli distribution on the Booleans

Used byErgodicity of Bernoulli measures under free infinite-group actions

LemmaErgodicity of Bernoulli measures under free infinite-group actions#✓fully proved

The Bernoulli product measure is ergodic under every action of an infinite group with injective orbit maps.

lemma bernoulli_isErgodic [Countable E] [Infinite G]
    (hinj : ∀ a : E, Function.Injective (fun g : G => g • a))
    (p : ℝ≥0) (hp : p ≤ 1) :
    ConfigSpace.IsErgodic (G := G) (bernoulliProductMeasure (E := E) p hp)

Uses 7

Statement usesErgodic measure on configuration space · Bernoulli product measure on configuration space

Proof usesConfiguration space of a statistical-mechanics model · Translation-invariant measure on configuration space · Shift of a configuration by a group element · Bernoulli zero-one law for infinite groups acting finite-to-one · Translation invariance of the Bernoulli product measure

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.