Events determined by disjoint coordinate sets

DefinitionEvent determined by a set of coordinates#✓fully proved

DeterminedBy A K: whether a configuration lies in A depends only on its values on K. This is definitionally StatMech.DependsOn A K.

def DeterminedBy (A : Set (ConfigSpace E)) (K : Set E) : Prop :=
  ∀ ω ω' : ConfigSpace E, agreeOn K ω ω' → (ω ∈ A ↔ ω' ∈ A)

Uses 2 · Used by 6

Statement usesConfiguration space of a statistical-mechanics model · Agreement of configurations on a set

Used byDetermined-by and depends-on are the same predicate · Reimer equality for events determined by disjoint coordinates · Independence of events determined by disjoint coordinate sets · Aizenman–Barsky inequality on a finite graph · Aizenman–Barsky inequality on infinite vertex-transitive graphs · Mean-field differential inequality for inhomogeneous percolation

LemmaDetermined-by and depends-on are the same predicate#✓fully proved

DeterminedBy and DependsOn are the same predicate.

lemma determinedBy_iff_dependsOn {A : Set (ConfigSpace E)} {K : Set E} :
    DeterminedBy A K ↔ DependsOn A K

Uses 3

Statement usesConfiguration space of a statistical-mechanics model · Event depending only on a set of coordinates · Event determined by a set of coordinates

TheoremIndependence of events determined by disjoint coordinate sets#✓fully proved

Events determined by disjoint coordinate sets are independent under a product probability weight: wprob φ (A ∩ B) = wprob φ A * wprob φ B.

theorem wprob_inter_eq_mul_of_determined [Fintype E] [DecidableEq E]
    (A B : Set (ConfigSpace E)) {K L : Set E}
    (hKL : Disjoint K L) (φ : E → Bool → ℝ) (h1 : ∀ x, φ x false + φ x true = 1)
    (hA : DeterminedBy A K) (hB : DeterminedBy B L) :
    wprob φ (A ∩ B) = wprob φ A * wprob φ B

Uses 7 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Event determined by a set of coordinates · Weighted probability of an event

Proof usesEvent depending only on a set of coordinates · Agreement of configurations on a set · Agreement on a set restricts to subsets · Independence of events on complementary coordinate sets

Used byAizenman–Barsky inequality on a finite graph · Aizenman–Barsky inequality on infinite vertex-transitive graphs · Mean-field differential inequality for inhomogeneous percolation

TheoremReimer equality for events determined by disjoint coordinates#✓fully proved

Reimer's inequality with equality for events determined by disjoint coordinate sets: under the product Bernoulli(p) measure, P_p(A □ B) = P_p(A) * P_p(B).

theorem reimer_bernoulli_eq_of_determinedDisjoint [Fintype E] [DecidableEq E] {p : ℝ≥0}
    (hp : p ≤ 1) {A B : Set (ConfigSpace E)} {K L : Set E} (hKL : Disjoint K L)
    (hA : DeterminedBy A K) (hB : DeterminedBy B L) :
    (bernoulliProductMeasure (E := E) p hp).real (disjointOccurrence A B)
      = (bernoulliProductMeasure (E := E) p hp).real A
        * (bernoulliProductMeasure (E := E) p hp).real B

Uses 9

Statement usesConfiguration space of a statistical-mechanics model · Event determined by a set of coordinates · Bernoulli product measure on configuration space · Disjoint occurrence of events

Proof usesBernoulli distribution on the Booleans · Bernoulli point masses sum to one · Bernoulli product measure as a weighted probability · Reimer's inequality for events on disjoint coordinate sets · Weighted probability of an event

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.