Van den Berg–Kesten inequality

DefinitionAgreement of configurations on a set#✓fully proved

agreeOn K ω ω': the configurations ω and ω' take the same value at every coordinate of K. This is Set.EqOn ω' ω K (see StatMech.agreeOn_iff_eqOn).

def agreeOn (K : Set E) (ω ω' : ConfigSpace E) : Prop := ∀ e ∈ K, ω' e = ω e

Uses 1 · Used by 35

Statement usesConfiguration space of a statistical-mechanics model

Used byEvents depending on a coordinate set are closed under unions · Events depending on a coordinate set are closed under intersection · An event depends on the coordinates its indicator depends on · Agreement on a set under configuration relabeling · Agreement on a set as pointwise equality · Agreement on a set restricts to subsets · Reflexivity of agreement on a set · Symmetry of agreement on a set · Transitivity of agreement on a set · Disjoint occurrence preserves finite dependence · Occurrence of a finitely dependent event within its window · Section of a disjoint occurrence · Occurrence is monotone in the coordinate set · Occurrence of an increasing event is monotone in the configuration · Occurrence is monotone in the event · Occurrence of an event on a coordinate set · Occurrence is invariant under relabeling coordinates · Occurrence avoiding the first coordinate passes to the false slice · Occurrence with first coordinate false passes to the false slice · Occurrence with first coordinate true passes to the true slice · Occurrence on a one-point configuration space · Reimer equality for a left event and a right event · Event depending only on a set of coordinates · Disjoint occurrence equals intersection for disjoint dependence sets · Reimer's inequality for events on disjoint coordinate sets · Reimer's inequality on one coordinate · Independence of events on complementary coordinate sets · Event determined by a set of coordinates · Independence of events determined by disjoint coordinate sets · Disjoint occurrence of an increasing and a decreasing event · BK inequality for decreasing events under product weights · Monotonicity in \(p\) of the Bernoulli percolation probability · Aizenman–Barsky inequality on a finite graph · Aizenman–Barsky inequality on infinite vertex-transitive graphs · Mean-field differential inequality for inhomogeneous percolation

LemmaAgreement on a set as pointwise equality#✓fully proved

agreeOn is the pointwise form of Set.EqOn.

lemma agreeOn_iff_eqOn {K : Set E} {ω ω' : ConfigSpace E} : agreeOn K ω ω' ↔ Set.EqOn ω' ω K

Uses 2

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

LemmaReflexivity of agreement on a set#✓fully proved

Every configuration agrees with itself (Set.eqOn_refl).

@[refl] lemma agreeOn_refl (K : Set E) (ω : ConfigSpace E) : agreeOn K ω ω

Uses 2 · Used by 1

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

Used byAn event occurring on a set contains the configuration

LemmaSymmetry of agreement on a set#✓fully proved

agreeOn is symmetric (Set.EqOn.symm).

lemma agreeOn_symm {K : Set E} {ω ω' : ConfigSpace E} (h : agreeOn K ω ω') :
    agreeOn K ω' ω

Uses 2 · Used by 1

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

Used byDisjoint occurrence preserves finite dependence

LemmaTransitivity of agreement on a set#✓fully proved

agreeOn is transitive (Set.EqOn.trans).

lemma agreeOn_trans {K : Set E} {ω ω' ω'' : ConfigSpace E}
    (h : agreeOn K ω ω') (h' : agreeOn K ω' ω'') : agreeOn K ω ω''

Uses 2 · Used by 3

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

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

LemmaAgreement on a set restricts to subsets#✓fully proved

Agreement on a set implies agreement on any subset (Set.EqOn.mono).

lemma agreeOn_mono {K K' : Set E} (hKK' : K ⊆ K') {ω ω' : ConfigSpace E}
    (h : agreeOn K' ω ω') : agreeOn K ω ω'

Uses 2 · Used by 6

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

Used byOccurrence is monotone in the coordinate set · Reimer's inequality for events on disjoint coordinate sets · 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

DefinitionOccurrence of an event on a coordinate set#✓fully proved

OccursOn A K ω: the event A occurs on the coordinate set K at ω, meaning that every configuration agreeing with ω on K lies in A.

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

Uses 2 · Used by 29

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

Used byDisjoint occurrence of events · Disjoint occurrence is symmetric · Disjoint occurrence of increasing events is increasing · Disjoint occurrence is monotone in both events · Disjoint occurrence lies in the intersection · Disjoint occurrence on a one-point space is the intersection · Disjoint occurrence preserves finite dependence · Occurrence of a finitely dependent event within its window · Section of a disjoint occurrence · Membership in a disjoint occurrence · An event occurring on a set contains the configuration · Occurrence is monotone in the coordinate set · Occurrence of an increasing event is monotone in the configuration · Occurrence is monotone in the event · Occurrence is invariant under relabeling coordinates · Occurrence avoiding the first coordinate passes to the false slice · Occurrence with first coordinate false passes to the false slice · Occurrence with first coordinate true passes to the true slice · Occurrence on a one-point configuration space · Disjoint occurrence commutes with relabeling coordinates · False slice of a disjoint occurrence · True slice of a disjoint occurrence · Disjoint occurrence equals intersection for disjoint dependence sets · Reimer's inequality on one coordinate · Disjoint occurrence of an increasing and a decreasing event · BK inequality for decreasing events under product weights · Aizenman–Barsky inequality on a finite graph · Aizenman–Barsky inequality on infinite vertex-transitive graphs · Mean-field differential inequality for inhomogeneous percolation

LemmaAn event occurring on a set contains the configuration#✓fully proved

If A occurs on some K at ω, then ω ∈ A.

lemma OccursOn.mem_self {A : Set (ConfigSpace E)} {K : Set E} {ω : ConfigSpace E}
    (h : OccursOn A K ω) : ω ∈ A

Uses 3 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Occurrence of an event on a coordinate set

Proof usesReflexivity of agreement on a set

Used byDisjoint occurrence lies in the intersection · Occurrence on a one-point configuration space · Disjoint occurrence equals intersection for disjoint dependence sets · Reimer's inequality on one coordinate

LemmaOccurrence is monotone in the coordinate set#✓fully proved

Occurrence on K implies occurrence on any larger coordinate set.

lemma OccursOn.mono {A : Set (ConfigSpace E)} {K K' : Set E} {ω : ConfigSpace E}
    (h : OccursOn A K ω) (hKK' : K ⊆ K') : OccursOn A K' ω

Uses 4

Statement usesConfiguration space of a statistical-mechanics model · Occurrence of an event on a coordinate set

Proof usesAgreement of configurations on a set · Agreement on a set restricts to subsets

LemmaOccurrence is monotone in the event#✓fully proved

Occurrence of A on K implies occurrence of any larger event B ⊇ A on K.

lemma OccursOn.mono_event {A B : Set (ConfigSpace E)} {K : Set E}
    {ω : ConfigSpace E} (h : OccursOn A K ω) (hAB : A ⊆ B) : OccursOn B K ω

Uses 3 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Occurrence of an event on a coordinate set

Proof usesAgreement of configurations on a set

Used byDisjoint occurrence is monotone in both events

DefinitionDisjoint occurrence of events#✓fully proved

The disjoint occurrence A □ B: the configurations ω for which there are disjoint coordinate sets K and L such that A occurs on K at ω and B occurs on L at ω.

def disjointOccurrence (A B : Set (ConfigSpace E)) : Set (ConfigSpace E) :=
  {ω | ∃ K L : Set E, Disjoint K L ∧ OccursOn A K ω ∧ OccursOn B L ω}

Uses 2 · Used by 45

Statement usesConfiguration space of a statistical-mechanics model · Occurrence of an event on a coordinate set

Used byBK criterion for Bernoulli product measures · Van den Berg–Kesten inequality · BK inequality for product weights on \(n\) ordered coordinates · BK inequality for product weights on a finite set · Disjoint occurrence is symmetric · Disjoint occurrence of increasing events is increasing · Disjoint occurrence is monotone in both events · Notation for disjoint occurrence · Disjoint occurrence lies in the intersection · Disjoint occurrence on a one-point space is the intersection · Union bound from the three-event BK inequality · Disjoint occurrence preserves finite dependence · BK inequality on countable configuration spaces · Section of a disjoint occurrence · BK inequality for three increasing events · BK inequality for inhomogeneous Bernoulli measures on a finite set · BK inequality for inhomogeneous measures on a countable set · Membership in a disjoint occurrence · Disjoint occurrence commutes with relabeling coordinates · False slice of a disjoint occurrence · True slice of a disjoint occurrence · Reimer equality for a left event and a right event · Disjoint occurrence equals intersection for disjoint dependence sets · Reimer's inequality for events on disjoint coordinate sets · Reimer's inequality on one coordinate · Reimer equality for events determined by disjoint coordinates · Reimer's inequality for two lower families · Reimer's inequality for two upper families · Reimer's inequality · Disjoint occurrence of an increasing and a decreasing event · Reimer's inequality for mixed monotone events, Bernoulli measure · Reimer's inequality for mixed monotone events, product weights · BK inequality for decreasing events · BK inequality for decreasing events under product weights · Reimer's inequality for Bernoulli measures, assuming the core case · Reimer's inequality · Reimer's inequality for product weights, assuming the core case · Reimer's inequality on the one-point configuration space · Reimer's inequality for disjoint events · Reimer's inequality for negatively correlated events · Reimer's inequality for the XOR and XNOR events · Slice inequalities in the one-coordinate BK induction step · Aizenman–Barsky inequality on a finite graph · Aizenman–Barsky inequality on infinite vertex-transitive graphs · Mean-field differential inequality for inhomogeneous percolation

LemmaMembership in a disjoint occurrence#✓fully proved

Membership in A □ B unfolded.

lemma mem_disjointOccurrence {A B : Set (ConfigSpace E)} {ω : ConfigSpace E} :
    ω ∈ disjointOccurrence A B ↔
      ∃ K L : Set E, Disjoint K L ∧ OccursOn A K ω ∧ OccursOn B L ω

Uses 3 · Used by 6

Statement usesConfiguration space of a statistical-mechanics model · Occurrence of an event on a coordinate set · Disjoint occurrence of events

Used byDisjoint occurrence on a one-point space is the intersection · Disjoint occurrence commutes with relabeling coordinates · False slice of a disjoint occurrence · True slice of a disjoint occurrence · Reimer's inequality on one coordinate · BK inequality for decreasing events under product weights

LemmaNotation for disjoint occurrence#✓fully proved

The notation A □ B unfolds to disjointOccurrence A B.

lemma disjointOccurrence_notation (A B : Set (ConfigSpace E)) :
    (A □ B : Set (ConfigSpace E)) = disjointOccurrence A B

Uses 2

Statement usesConfiguration space of a statistical-mechanics model · Disjoint occurrence of events

TheoremDisjoint occurrence lies in the intersection#✓fully proved

Disjoint occurrence implies occurrence of both events: A □ B ⊆ A ∩ B.

theorem disjointOccurrence_subset_inter (A B : Set (ConfigSpace E)) :
    disjointOccurrence A B ⊆ A ∩ B

Uses 4 · Used by 6

Statement usesConfiguration space of a statistical-mechanics model · Disjoint occurrence of events

Proof usesOccurrence of an event on a coordinate set · An event occurring on a set contains the configuration

Used byDisjoint occurrence equals intersection for disjoint dependence sets · Disjoint occurrence of an increasing and a decreasing event · Reimer's inequality for negatively correlated events · Aizenman–Barsky inequality on a finite graph · Aizenman–Barsky inequality on infinite vertex-transitive graphs · Mean-field differential inequality for inhomogeneous percolation

TheoremDisjoint occurrence is symmetric#✓fully proved

Disjoint occurrence is symmetric: A □ B = B □ A.

theorem disjointOccurrence_comm (A B : Set (ConfigSpace E)) :
    disjointOccurrence A B = disjointOccurrence B A

Uses 3

Statement usesConfiguration space of a statistical-mechanics model · Disjoint occurrence of events

Proof usesOccurrence of an event on a coordinate set

TheoremDisjoint occurrence is monotone in both events#✓fully proved

Disjoint occurrence is monotone in both events.

theorem disjointOccurrence_mono {A A' B B' : Set (ConfigSpace E)}
    (hA : A ⊆ A') (hB : B ⊆ B') :
    disjointOccurrence A B ⊆ disjointOccurrence A' B'

Uses 4 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Disjoint occurrence of events

Proof usesOccurrence of an event on a coordinate set · Occurrence is monotone in the event

Used byBK inequality for product weights on \(n\) ordered coordinates · Slice inequalities in the one-coordinate BK induction step

TheoremOccurrence of an increasing event is monotone in the configuration#✓fully proved

If an increasing event A occurs on K at ω and ω ≤ ω', then A occurs on K at ω'.

theorem OccursOn.mono_config {A : Set (ConfigSpace E)} (hA : IsIncreasing A)
    {K : Set E} {omega omega' : ConfigSpace E} (homega : omega ≤ omega')
    (hocc : OccursOn A K omega) : OccursOn A K omega'

Uses 4 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Increasing event · Occurrence of an event on a coordinate set

Proof usesAgreement of configurations on a set

Used byDisjoint occurrence of increasing events is increasing

TheoremDisjoint occurrence of increasing events is increasing#✓fully proved

The disjoint occurrence of two increasing events is increasing.

theorem disjointOccurrence_isIncreasing {A B : Set (ConfigSpace E)}
    (hA : IsIncreasing A) (hB : IsIncreasing B) :
    IsIncreasing (disjointOccurrence A B)

Uses 5 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Increasing event · Disjoint occurrence of events

Proof usesOccurrence of an event on a coordinate set · Occurrence of an increasing event is monotone in the configuration

Used byBK criterion for Bernoulli product measures · BK inequality for three increasing events

DefinitionProduct weight of a configuration#✓fully proved

The product weight ∏ x, φ x (ω x) of a configuration ω, where φ x b is the weight of value b at coordinate x.

def pweight [Fintype E] (φ : E → Bool → ℝ) (ω : ConfigSpace E) : ℝ := ∏ x, φ x (ω x)

Uses 1 · Used by 24

Statement usesConfiguration space of a statistical-mechanics model

Used byConfiguration weight as a product weight · Bernoulli product measure as a weighted probability · BK inequality for product weights on \(n\) ordered coordinates · BK inequality for inhomogeneous Bernoulli measures on a finite set · Product weight factors over the first coordinate · Nonnegativity of the product weight · Product weight is invariant under relabeling coordinates · Product probability weight has total mass one · Weighted probability of an event · Monotonicity of the weighted probability · Weighted probability by conditioning on the first coordinate · Weighted probability is invariant under relabeling coordinates · Inclusion–exclusion for the weighted probability · Weighted disjoint pairs as a doubled-weight probability · Reimer's inequality on one coordinate · Independence of events on complementary coordinate sets · Harris–FKG inequality for an increasing and a decreasing event · Harris–FKG inequality for increasing events · BK inequality for decreasing events under product weights · Reimer's inequality on the one-point configuration space · Reimer's inequality for disjoint events · Aizenman–Barsky inequality on a finite graph · Aizenman–Barsky inequality on infinite vertex-transitive graphs · Mean-field differential inequality for inhomogeneous percolation

LemmaNonnegativity of the product weight#✓fully proved

A product of nonnegative coordinate weights is nonnegative.

lemma pweight_nonneg [Fintype E] {φ : E → Bool → ℝ} (hφ : ∀ x b, 0 ≤ φ x b)
    (ω : ConfigSpace E) : 0 ≤ pweight φ ω

Uses 2 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Product weight of a configuration

Used byMonotonicity of the weighted probability · Harris–FKG inequality for increasing events · Reimer's inequality for disjoint events · Mean-field differential inequality for inhomogeneous percolation

DefinitionWeighted probability of an event#✓fully proved

The pweight φ-mass ∑ ω ∈ S, pweight φ ω of an event S. When φ ≥ 0 and φ x false + φ x true = 1 for all x, this is the probability of S under the product measure whose coordinate x has law φ x.

noncomputable def wprob [Fintype E] [DecidableEq E] (φ : E → Bool → ℝ)
    (S : Set (ConfigSpace E)) : ℝ :=
  ∑ ω, S.indicator (fun _ => (1 : ℝ)) ω * pweight φ ω

Uses 2 · Used by 38

Statement usesConfiguration space of a statistical-mechanics model · Product weight of a configuration

Used byEvent weight as a product-weight probability · Bernoulli product measure as a weighted probability · Van den Berg–Kesten inequality · BK inequality for product weights on \(n\) ordered coordinates · BK inequality for product weights on a finite set · BK inequality for inhomogeneous Bernoulli measures on a finite set · Monotonicity of the weighted probability · Weighted probability by conditioning on the first coordinate · Weighted probability is invariant under relabeling coordinates · Inclusion–exclusion for the weighted probability · Reimer equality for a left event and a right event · Weighted disjoint pairs as a doubled-weight probability · Reimer's inequality for events on disjoint coordinate sets · Reimer's inequality on one coordinate · Independence of events on complementary coordinate sets · Reimer equality for events determined by disjoint coordinates · Independence of events determined by disjoint coordinate sets · Reimer's inequality for two lower families · Reimer's inequality for two upper families · Reimer's inequality · Reimer's inequality for mixed monotone events, Bernoulli measure · Reimer's inequality for mixed monotone events, product weights · Harris–FKG inequality for an increasing and a decreasing event · Harris–FKG inequality for increasing events · BK inequality for decreasing events · BK inequality for decreasing events under product weights · Reimer's inequality for Bernoulli measures, assuming the core case · Reimer's inequality · Reimer's inequality for product weights, assuming the core case · Reimer's inequality on the one-point configuration space · Negatively correlated events · Reimer's inequality for disjoint events · Reimer's inequality for negatively correlated events · Slice inequalities in the one-coordinate BK induction step · Aizenman–Barsky inequality on a finite graph · Aizenman–Barsky inequality on infinite vertex-transitive graphs · Mean-field differential inequality for inhomogeneous percolation · Inhomogeneous Duminil-Copin–Tassion quantity \(\varphi(S)\)

LemmaMonotonicity of the weighted probability#✓fully proved

wprob φ is monotone for nonnegative weights.

lemma wprob_mono [Fintype E] [DecidableEq E] {φ : E → Bool → ℝ} (hφ : ∀ x b, 0 ≤ φ x b)
    {S T : Set (ConfigSpace E)} (h : S ⊆ T) : wprob φ S ≤ wprob φ T

Uses 4 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Weighted probability of an event

Proof usesProduct weight of a configuration · Nonnegativity of the product weight

Used byBK inequality for product weights on \(n\) ordered coordinates · Reimer's inequality for negatively correlated events · Slice inequalities in the one-coordinate BK induction step · Mean-field differential inequality for inhomogeneous percolation

LemmaProduct probability weight has total mass one#✓fully proved

A product probability weight has total mass 1.

lemma sum_pweight_eq_one [Fintype E] [DecidableEq E] {w : E → Bool → ℝ}
    (hw1 : ∀ x, w x false + w x true = 1) :
    (∑ b : ConfigSpace E, pweight w b) = 1

Uses 2 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Product weight of a configuration

Used byIndependence of events on complementary coordinate sets · Harris–FKG inequality for an increasing and a decreasing event · Harris–FKG inequality for increasing events · Mean-field differential inequality for inhomogeneous percolation

LemmaInclusion–exclusion for the weighted probability#✓fully proved

Inclusion–exclusion for wprob.

lemma wprob_union_inter [Fintype E] [DecidableEq E] (φ : E → Bool → ℝ)
    (U V : Set (ConfigSpace E)) :
    wprob φ (U ∪ V) + wprob φ (U ∩ V) = wprob φ U + wprob φ V

Uses 3 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Weighted probability of an event

Proof usesProduct weight of a configuration

Used byBK inequality for product weights on \(n\) ordered coordinates

LemmaScalar inequality behind the BK induction step#✓fully proved

The scalar inequality behind the induction step of the BK inequality: with q = 1 - p, p, q ≥ 0, if c0 ≤ m ≤ a0 b0, c1 ≤ a0 b1 + a1 b0 - m and c1 ≤ a1 b1, then q c0 + p c1 ≤ (q a0 + p a1) (q b0 + p b1).

lemma bk_algebra (a0 a1 b0 b1 p q c0 c1 m : ℝ)
    (hq : q = 1 - p) (hp0 : 0 ≤ p) (hq0 : 0 ≤ q)
    (hmab : m ≤ a0 * b0) (hc0m : c0 ≤ m)
    (hc1u : c1 ≤ a0 * b1 + a1 * b0 - m) (hc1v : c1 ≤ a1 * b1) :
    q * c0 + p * c1 ≤ (q * a0 + p * a1) * (q * b0 + p * b1)

Used by 1

Used byBK inequality for product weights on \(n\) ordered coordinates

DefinitionSlice of an event at the first coordinate#✓fully proved

The section of an event C on Fin (n + 1) at first coordinate x: the configurations ω' on Fin n with Fin.cons x ω' ∈ C.

def slice {n : ℕ} (C : Set (ConfigSpace (Fin (n + 1)))) (x : Bool) :
    Set (ConfigSpace (Fin n)) := {ω' | Fin.cons x ω' ∈ C}

Uses 1 · Used by 11

Statement usesConfiguration space of a statistical-mechanics model

Used byBK inequality for product weights on \(n\) ordered coordinates · Indicator of an event at a prepended configuration · Occurrence avoiding the first coordinate passes to the false slice · Occurrence with first coordinate false passes to the false slice · Occurrence with first coordinate true passes to the true slice · False slice of a disjoint occurrence · True slice of a disjoint occurrence · False slice of an increasing event lies in the true slice · Slices of an increasing event are increasing · Weighted probability by conditioning on the first coordinate · Slice inequalities in the one-coordinate BK induction step

DefinitionCoordinate set with the first coordinate removed#✓fully proved

The coordinate set {j | j.succ ∈ K}: K with the first coordinate removed, shifted down.

def sliceSet {n : ℕ} (K : Set (Fin (n + 1))) : Set (Fin n) := {j | j.succ ∈ K}

Used by 6

Used byOccurrence avoiding the first coordinate passes to the false slice · Occurrence with first coordinate false passes to the false slice · Occurrence with first coordinate true passes to the true slice · False slice of a disjoint occurrence · True slice of a disjoint occurrence · Removing the first coordinate preserves disjointness

LemmaIndicator of an event at a prepended configuration#✓fully proved

The indicator of S at Fin.cons x ω' is the indicator of the slice at ω'.

lemma indicator_slice {n : ℕ} (S : Set (ConfigSpace (Fin (n + 1)))) (x : Bool)
    (ω' : ConfigSpace (Fin n)) :
    S.indicator (fun _ => (1 : ℝ)) (Fin.cons x ω')
      = (slice S x).indicator (fun _ => (1 : ℝ)) ω'

Uses 2

Statement usesConfiguration space of a statistical-mechanics model · Slice of an event at the first coordinate

LemmaProduct weight factors over the first coordinate#✓fully proved

The product weight factors over the first coordinate.

lemma pweight_cons {n : ℕ} (φ : Fin (n + 1) → Bool → ℝ) (x : Bool) (ω' : ConfigSpace (Fin n)) :
    pweight φ (Fin.cons x ω') = φ 0 x * pweight (fun j => φ j.succ) ω'

Uses 2 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Product weight of a configuration

Used byWeighted probability by conditioning on the first coordinate

TheoremWeighted probability by conditioning on the first coordinate#✓fully proved

Conditioning on the first coordinate: wprob φ S = φ 0 false * wprob ψ (slice S false) + φ 0 true * wprob ψ (slice S true), where ψ is φ on the remaining coordinates.

theorem wprob_slice {n : ℕ} (φ : Fin (n + 1) → Bool → ℝ) (S : Set (ConfigSpace (Fin (n + 1)))) :
    wprob φ S = φ 0 false * wprob (fun j => φ j.succ) (slice S false)
             + φ 0 true * wprob (fun j => φ j.succ) (slice S true)

Uses 5 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Slice of an event at the first coordinate · Weighted probability of an event

Proof usesProduct weight of a configuration · Product weight factors over the first coordinate

Used byBK inequality for product weights on \(n\) ordered coordinates

LemmaSlices of an increasing event are increasing#✓fully proved

Slices of an increasing event are increasing.

lemma slice_isIncreasing {n : ℕ} {C : Set (ConfigSpace (Fin (n + 1)))} (hC : IsIncreasing C)
    (x : Bool) : IsIncreasing (slice C x)

Uses 3 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Increasing event · Slice of an event at the first coordinate

Used byBK inequality for product weights on \(n\) ordered coordinates · Slice inequalities in the one-coordinate BK induction step

LemmaFalse slice of an increasing event lies in the true slice#✓fully proved

For an increasing event, the false slice is contained in the true slice.

lemma slice_false_subset_true {n : ℕ} {C : Set (ConfigSpace (Fin (n + 1)))}
    (hC : IsIncreasing C) : slice C false ⊆ slice C true

Uses 3 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Increasing event · Slice of an event at the first coordinate

Used byBK inequality for product weights on \(n\) ordered coordinates · Slice inequalities in the one-coordinate BK induction step

LemmaOccurrence with first coordinate false passes to the false slice#✓fully proved

Occurrence on K at Fin.cons false ω' passes to the false slice.

lemma occursOn_slice_of_false {n : ℕ} {C : Set (ConfigSpace (Fin (n + 1)))}
    {K : Set (Fin (n + 1))} {ω' : ConfigSpace (Fin n)}
    (h : OccursOn C K (Fin.cons false ω')) :
    OccursOn (slice C false) (sliceSet K) ω'

Uses 5 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Occurrence of an event on a coordinate set · Slice of an event at the first coordinate · Coordinate set with the first coordinate removed

Proof usesAgreement of configurations on a set

Used byFalse slice of a disjoint occurrence

LemmaOccurrence with first coordinate true passes to the true slice#✓fully proved

Occurrence on K at Fin.cons true ω' passes to the true slice.

lemma occursOn_slice_true {n : ℕ} {C : Set (ConfigSpace (Fin (n + 1)))}
    {K : Set (Fin (n + 1))} {ω' : ConfigSpace (Fin n)}
    (h : OccursOn C K (Fin.cons true ω')) :
    OccursOn (slice C true) (sliceSet K) ω'

Uses 5 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Occurrence of an event on a coordinate set · Slice of an event at the first coordinate · Coordinate set with the first coordinate removed

Proof usesAgreement of configurations on a set

Used byTrue slice of a disjoint occurrence

LemmaOccurrence avoiding the first coordinate passes to the false slice#✓fully proved

If the witness set K avoids the first coordinate, occurrence on K passes to the false slice whatever the value of the first coordinate.

lemma occursOn_slice_false_notmem {n : ℕ} {C : Set (ConfigSpace (Fin (n + 1)))}
    {K : Set (Fin (n + 1))} {x : Bool} {ω' : ConfigSpace (Fin n)}
    (h0 : (0 : Fin (n + 1)) ∉ K) (h : OccursOn C K (Fin.cons x ω')) :
    OccursOn (slice C false) (sliceSet K) ω'

Uses 5 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Occurrence of an event on a coordinate set · Slice of an event at the first coordinate · Coordinate set with the first coordinate removed

Proof usesAgreement of configurations on a set

Used byTrue slice of a disjoint occurrence

LemmaRemoving the first coordinate preserves disjointness#✓fully proved

sliceSet preserves disjointness.

lemma sliceSet_disjoint {n : ℕ} {K L : Set (Fin (n + 1))} (h : Disjoint K L) :
    Disjoint (sliceSet K) (sliceSet L)

Uses 1 · Used by 2

Statement usesCoordinate set with the first coordinate removed

Used byFalse slice of a disjoint occurrence · True slice of a disjoint occurrence

TheoremFalse slice of a disjoint occurrence#✓fully proved

The false slice of A □ B is contained in the disjoint occurrence of the false slices.

theorem slice_disjointOccurrence_false {n : ℕ} {A B : Set (ConfigSpace (Fin (n + 1)))} :
    slice (disjointOccurrence A B) false ⊆
      disjointOccurrence (slice A false) (slice B false)

Uses 8 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Disjoint occurrence of events · Slice of an event at the first coordinate

Proof usesOccurrence of an event on a coordinate set · Membership in a disjoint occurrence · Occurrence with first coordinate false passes to the false slice · Coordinate set with the first coordinate removed · Removing the first coordinate preserves disjointness

Used byBK inequality for product weights on \(n\) ordered coordinates

TheoremTrue slice of a disjoint occurrence#✓fully proved

The true slice of A □ B is contained in (A₀ □ B₁) ∪ (A₁ □ B₀), where A₀, A₁ are the slices of A (similarly for B): the first coordinate is used by at most one witness.

theorem slice_disjointOccurrence_true {n : ℕ} {A B : Set (ConfigSpace (Fin (n + 1)))} :
    slice (disjointOccurrence A B) true ⊆
      disjointOccurrence (slice A false) (slice B true) ∪
      disjointOccurrence (slice A true) (slice B false)

Uses 9 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Disjoint occurrence of events · Slice of an event at the first coordinate

Proof usesOccurrence of an event on a coordinate set · Membership in a disjoint occurrence · Occurrence avoiding the first coordinate passes to the false slice · Occurrence with first coordinate true passes to the true slice · Coordinate set with the first coordinate removed · Removing the first coordinate preserves disjointness

Used byBK inequality for product weights on \(n\) ordered coordinates

LemmaOccurrence on a one-point configuration space#✓fully proved

On a one-point configuration space, OccursOn A K ω reduces to ω ∈ A.

lemma occursOn_subsingleton {n : ℕ} [Subsingleton (ConfigSpace (Fin n))]
    {A : Set (ConfigSpace (Fin n))} {K : Set (Fin n)} {ω : ConfigSpace (Fin n)} :
    OccursOn A K ω ↔ ω ∈ A

Uses 4 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Occurrence of an event on a coordinate set

Proof usesAn event occurring on a set contains the configuration · Agreement of configurations on a set

Used byDisjoint occurrence on a one-point space is the intersection

LemmaDisjoint occurrence on a one-point space is the intersection#✓fully proved

On a one-point configuration space, A □ B = A ∩ B.

lemma disjointOccurrence_subsingleton {n : ℕ} [Subsingleton (ConfigSpace (Fin n))]
    (A B : Set (ConfigSpace (Fin n))) :
    disjointOccurrence A B = A ∩ B

Uses 5 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Disjoint occurrence of events

Proof usesOccurrence of an event on a coordinate set · Membership in a disjoint occurrence · Occurrence on a one-point configuration space

Used byBK inequality for product weights on \(n\) ordered coordinates · Reimer's inequality on the one-point configuration space

TheoremBK inequality for product weights on \(n\) ordered coordinates#✓fully proved

The BK inequality on Fin n for a product probability weight φ: wprob φ (A □ B) ≤ wprob φ A * wprob φ B for increasing A, B.

theorem bk_wprob : ∀ (n : ℕ) (φ : Fin n → Bool → ℝ),
    (∀ i b, 0 ≤ φ i b) → (∀ i, φ i false + φ i true = 1) →
    ∀ (A B : Set (ConfigSpace (Fin n))), IsIncreasing A → IsIncreasing B →
    wprob φ (disjointOccurrence A B) ≤ wprob φ A * wprob φ B

Uses 16 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Increasing event · Disjoint occurrence of events · Weighted probability of an event

Proof usesScalar inequality behind the BK induction step · Disjoint occurrence is monotone in both events · Disjoint occurrence on a one-point space is the intersection · Product weight of a configuration · Slice of an event at the first coordinate · False slice of a disjoint occurrence · True slice of a disjoint occurrence · False slice of an increasing event lies in the true slice · Slices of an increasing event are increasing · Monotonicity of the weighted probability · Weighted probability by conditioning on the first coordinate · Inclusion–exclusion for the weighted probability

Used byBK inequality for product weights on a finite set · Slice inequalities in the one-coordinate BK induction step

DefinitionRelabeling configurations along a bijection#✓fully proved

The bijection ω ↦ ω ∘ e from configurations on F to configurations on E induced by e : E ≃ F. This is e.symm.arrowCongr (Equiv.refl Bool) (StatMech.cfgEquiv_eq_arrowCongr).

def cfgEquiv (e : E ≃ F) : ConfigSpace F ≃ ConfigSpace E where
  toFun ω := fun x => ω (e x)
  invFun ω := fun y => ω (e.symm y)
  left_inv ω := by funext y; simp
  right_inv ω := by funext x; simp

Uses 1 · Used by 10

Statement usesConfiguration space of a statistical-mechanics model

Used byAgreement on a set under configuration relabeling · BK inequality for product weights on a finite set · Configuration relabeling agrees with the library arrow equivalence · Monotonicity of configuration relabeling · Occurrence is invariant under relabeling coordinates · Disjoint occurrence commutes with relabeling coordinates · Product weight is invariant under relabeling coordinates · Weighted probability is invariant under relabeling coordinates · Reimer's inequality for product weights, assuming the core case · Aizenman–Barsky inequality on infinite vertex-transitive graphs

LemmaConfiguration relabeling agrees with the library arrow equivalence#✓fully proved

cfgEquiv e agrees with Mathlib's Equiv.arrowCongr.

lemma cfgEquiv_eq_arrowCongr (e : E ≃ F) :
    cfgEquiv e = e.symm.arrowCongr (Equiv.refl Bool)

Uses 2

Statement usesConfiguration space of a statistical-mechanics model · Relabeling configurations along a bijection

LemmaMonotonicity of configuration relabeling#✓fully proved

cfgEquiv e is monotone.

lemma cfgEquiv_mono (e : E ≃ F) {ω ω' : ConfigSpace F} (h : ω ≤ ω') :
    cfgEquiv e ω ≤ cfgEquiv e ω'

Uses 2 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Relabeling configurations along a bijection

Used byBK inequality for product weights on a finite set

LemmaAgreement on a set under configuration relabeling#✓fully proved

Agreement on e '' K corresponds to agreement on K after transport by cfgEquiv e.

lemma agreeOn_cfgEquiv (e : E ≃ F) (K : Set E) (ωf ωf' : ConfigSpace F) :
    agreeOn (e '' K) ωf ωf' ↔ agreeOn K (cfgEquiv e ωf) (cfgEquiv e ωf')

Uses 3 · Used by 1

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

Used byOccurrence is invariant under relabeling coordinates

LemmaOccurrence is invariant under relabeling coordinates#✓fully proved

Occurrence is preserved by relabeling the coordinates.

lemma occursOn_cfgEquiv (e : E ≃ F) (A : Set (ConfigSpace E)) (K : Set E) (ωf : ConfigSpace F) :
    OccursOn ((cfgEquiv e) ⁻¹' A) (e '' K) ωf ↔ OccursOn A K (cfgEquiv e ωf)

Uses 5 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Occurrence of an event on a coordinate set · Relabeling configurations along a bijection

Proof usesAgreement of configurations on a set · Agreement on a set under configuration relabeling

Used byDisjoint occurrence commutes with relabeling coordinates

TheoremDisjoint occurrence commutes with relabeling coordinates#✓fully proved

Disjoint occurrence commutes with relabeling the coordinates.

theorem preimage_disjointOccurrence (e : E ≃ F) (A B : Set (ConfigSpace E)) :
    (cfgEquiv e) ⁻¹' (disjointOccurrence A B)
      = disjointOccurrence ((cfgEquiv e) ⁻¹' A) ((cfgEquiv e) ⁻¹' B)

Uses 6 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Relabeling configurations along a bijection · Disjoint occurrence of events

Proof usesOccurrence of an event on a coordinate set · Membership in a disjoint occurrence · Occurrence is invariant under relabeling coordinates

Used byBK inequality for product weights on a finite set · Reimer's inequality for product weights, assuming the core case

LemmaProduct weight is invariant under relabeling coordinates#✓fully proved

The product weight is invariant under relabeling the coordinates.

lemma pweight_transfer [Fintype E] [Fintype F] (e : E ≃ F) (φ : E → Bool → ℝ)
    (ωf : ConfigSpace F) :
    pweight φ (cfgEquiv e ωf) = pweight (fun y => φ (e.symm y)) ωf

Uses 3 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Relabeling configurations along a bijection · Product weight of a configuration

Used byWeighted probability is invariant under relabeling coordinates

LemmaWeighted probability is invariant under relabeling coordinates#✓fully proved

wprob is invariant under relabeling the coordinates.

lemma wprob_transfer [Fintype E] [DecidableEq E] [Fintype F] [DecidableEq F]
    (e : E ≃ F) (φ : E → Bool → ℝ) (S : Set (ConfigSpace E)) :
    wprob φ S = wprob (fun y => φ (e.symm y)) ((cfgEquiv e) ⁻¹' S)

Uses 5 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Relabeling configurations along a bijection · Weighted probability of an event

Proof usesProduct weight of a configuration · Product weight is invariant under relabeling coordinates

Used byBK inequality for product weights on a finite set · Reimer's inequality for product weights, assuming the core case · Aizenman–Barsky inequality on infinite vertex-transitive graphs

TheoremBK inequality for product weights on a finite set#✓fully proved

The BK inequality for a product probability weight on a finite set E: if φ ≥ 0 and φ x false + φ x true = 1 for all x, then wprob φ (A □ B) ≤ wprob φ A * wprob φ B for all increasing events A, B.

theorem bk_wprob_general [Fintype E] [DecidableEq E] (φ : E → Bool → ℝ)
    (hφ0 : ∀ x b, 0 ≤ φ x b) (hφ1 : ∀ x, φ x false + φ x true = 1)
    {A B : Set (ConfigSpace E)} (hA : IsIncreasing A) (hB : IsIncreasing B) :
    wprob φ (disjointOccurrence A B) ≤ wprob φ A * wprob φ B

Uses 9 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Increasing event · Disjoint occurrence of events · Weighted probability of an event

Proof usesBK inequality for product weights on \(n\) ordered coordinates · Relabeling configurations along a bijection · Monotonicity of configuration relabeling · Disjoint occurrence commutes with relabeling coordinates · Weighted probability is invariant under relabeling coordinates

Used byVan den Berg–Kesten inequality · BK inequality for inhomogeneous Bernoulli measures on a finite set · Reimer's inequality for two upper families · BK inequality for decreasing events under product weights

LemmaBernoulli point masses sum to one#✓fully proved

The two point masses of the Bernoulli(p) measure add up to 1.

lemma bernoulliMeasure_real_false_add_true {p : ℝ≥0} (hp : p ≤ 1) :
    (bernoulliMeasure p hp).real {false} + (bernoulliMeasure p hp).real {true} = 1

Uses 1 · Used by 6

Statement usesBernoulli distribution on the Booleans

Used byVan den Berg–Kesten inequality · BK inequality for inhomogeneous Bernoulli measures on a finite set · Reimer equality for events determined by disjoint coordinates · Reimer's inequality for mixed monotone events, Bernoulli measure · BK inequality for decreasing events · Reimer's inequality for Bernoulli measures, assuming the core case

TheoremBernoulli product measure as a weighted probability#✓fully proved

The product Bernoulli measure of an event is its wprob for the Bernoulli marginals.

theorem bernoulli_real_eq_wprob [Fintype E] [DecidableEq E] {p : ℝ≥0} (hp : p ≤ 1)
    (S : Set (ConfigSpace E)) :
    (bernoulliProductMeasure (E := E) p hp).real S
      = wprob (fun (_ : E) (b : Bool) => (bernoulliMeasure p hp).real {b}) S

Uses 7 · Used by 6

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli distribution on the Booleans · Bernoulli product measure on configuration space · Weighted probability of an event

Proof usesProbability of an event as a sum of configuration masses · Mass of a configuration under a finite Bernoulli product measure, real form · Product weight of a configuration

Used byVan den Berg–Kesten inequality · Reimer equality for events determined by disjoint coordinates · Reimer's inequality for mixed monotone events, Bernoulli measure · BK inequality for decreasing events · Reimer's inequality for Bernoulli measures, assuming the core case · Reimer's inequality for disjoint events

TheoremVan den Berg–Kesten inequality#✓fully proved

The van den Berg–Kesten (BK) inequality (van den Berg and Kesten 1985): under the product Bernoulli(p) measure on a finite configuration space, for increasing events A and B, P_p(A □ B) ≤ P_p(A) * P_p(B).

theorem bk_inequality [Fintype E] [DecidableEq E] {p : ℝ≥0} (hp : p ≤ 1)
    {A B : Set (ConfigSpace E)} (hA : IsIncreasing A) (hB : IsIncreasing B) :
    (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 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Increasing event · 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 · BK inequality for product weights on a finite set · Weighted probability of an event

Used byBK criterion for Bernoulli product measures · BK inequality on countable configuration spaces

TheoremOccurrence of a finitely dependent event within its window#✓fully proved

If A depends only on F and occurs on K at ω, then it occurs on K ∩ F at every configuration agreeing with ω on F.

theorem ibk_occursOn_inter_finite {A : Set (ConfigSpace E)} {F : Finset E}
    {K : Set E} {omega omega' : ConfigSpace E}
    (hA : DependsOn A (F : Set E)) (hocc : OccursOn A K omega)
    (hagree : agreeOn (F : Set E) omega omega') :
    OccursOn A (K ∩ (F : Set E)) omega'

Uses 4 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Event depending only on a set of coordinates · Occurrence of an event on a coordinate set · Agreement of configurations on a set

Used byDisjoint occurrence preserves finite dependence

TheoremDisjoint occurrence preserves finite dependence#✓fully proved

If A and B depend only on the coordinates in F, so does A □ B.

theorem ibk_disjointOccurrence_dependsOn {A B : Set (ConfigSpace E)} {F : Finset E}
    (hA : DependsOn A (F : Set E)) (hB : DependsOn B (F : Set E)) :
    DependsOn (disjointOccurrence A B) (F : Set E)

Uses 7 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Event depending only on a set of coordinates · Disjoint occurrence of events

Proof usesOccurrence of an event on a coordinate set · Agreement of configurations on a set · Symmetry of agreement on a set · Occurrence of a finitely dependent event within its window

Used byBK inequality on countable configuration spaces · BK inequality for three increasing events · BK inequality for inhomogeneous measures on a countable set

TheoremSection of a disjoint occurrence#✓fully proved

The section on F of A □ B is contained in the disjoint occurrence of the sections.

theorem ibk_section_disjointOccurrence_subset (A B : Set (ConfigSpace E))
    (F : Finset E) :
    ih_section (disjointOccurrence A B) F ⊆
      disjointOccurrence (ih_section A F) (ih_section B F)

Uses 6 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Disjoint occurrence of events · Section of an event on a finite coordinate set

Proof usesOccurrence of an event on a coordinate set · Agreement of configurations on a set · Filling a finite configuration with closed coordinates

Used byBK inequality on countable configuration spaces · BK inequality for inhomogeneous measures on a countable set

TheoremBK inequality on countable configuration spaces#✓fully proved

The BK inequality on a countable configuration space: for increasing events A, B depending only on the coordinates in a finite set F, P_p(A □ B) ≤ P_p(A) * P_p(B).

theorem ibk_inequality_of_finite_dependsOn {p : ℝ≥0} (hp : p ≤ 1)
    {A B : Set (ConfigSpace E)} (F : Finset E)
    (hAdep : DependsOn A (F : Set E)) (hBdep : DependsOn B (F : Set E))
    (hAinc : IsIncreasing A) (hBinc : IsIncreasing B) :
    (bernoulliProductMeasure (E := E) p hp).real (disjointOccurrence A B) ≤
      (bernoulliProductMeasure (E := E) p hp).real A *
        (bernoulliProductMeasure (E := E) p hp).real B

Uses 13 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Event depending only on a set of coordinates · Increasing event · Bernoulli product measure on configuration space · Disjoint occurrence of events

Proof usesBernoulli distribution on the Booleans · Van den Berg–Kesten inequality · Disjoint occurrence preserves finite dependence · Section of a disjoint occurrence · Finitely dependent event is a cylinder over its section · Section of an event on a finite coordinate set · Section of an increasing event is increasing · Bernoulli product measure of a cylinder event, real-valued form

Used byBK inequality for three increasing events

TheoremBK inequality for three increasing events#✓fully proved

The BK inequality for three increasing events depending on finitely many coordinates: P_p(P □ (Q □ R)) ≤ P_p(P) * P_p(Q) * P_p(R).

theorem ibk_triple_of_finite_dependsOn {p : ℝ≥0} (hp : p ≤ 1)
    {P Q R : Set (ConfigSpace E)} (F : Finset E)
    (hPdep : DependsOn P (F : Set E)) (hQdep : DependsOn Q (F : Set E))
    (hRdep : DependsOn R (F : Set E))
    (hP : IsIncreasing P) (hQ : IsIncreasing Q) (hR : IsIncreasing R) :
    (bernoulliProductMeasure (E := E) p hp).real
        (disjointOccurrence P (disjointOccurrence Q R)) ≤
      (bernoulliProductMeasure (E := E) p hp).real P *
        (bernoulliProductMeasure (E := E) p hp).real Q *
        (bernoulliProductMeasure (E := E) p hp).real R

Uses 8 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Event depending only on a set of coordinates · Increasing event · Bernoulli product measure on configuration space · Disjoint occurrence of events

Proof usesDisjoint occurrence of increasing events is increasing · Disjoint occurrence preserves finite dependence · BK inequality on countable configuration spaces

Used byUnion bound from the three-event BK inequality

TheoremUnion bound from the three-event BK inequality#✓fully proved

Union bound from the three-event BK inequality: if C ⊆ ⋃ i ∈ s, P i □ (Q i □ R i) with all events increasing and depending on a common finite window, then P_p(C) ≤ ∑ i ∈ s, P_p(P i) * P_p(Q i) * P_p(R i).

theorem ibk_criterion_of_finite_dependsOn {I : Type*} {p : ℝ≥0} (hp : p ≤ 1)
    (s : Finset I) (P Q R : I → Set (ConfigSpace E)) (F : Finset E)
    (hPdep : ∀ i ∈ s, DependsOn (P i) (F : Set E))
    (hQdep : ∀ i ∈ s, DependsOn (Q i) (F : Set E))
    (hRdep : ∀ i ∈ s, DependsOn (R i) (F : Set E))
    (hP : ∀ i ∈ s, IsIncreasing (P i))
    (hQ : ∀ i ∈ s, IsIncreasing (Q i))
    (hR : ∀ i ∈ s, IsIncreasing (R i))
    {C : Set (ConfigSpace E)}
    (hC : C ⊆ ⋃ i ∈ s, disjointOccurrence (P i) (disjointOccurrence (Q i) (R i))) :
    (bernoulliProductMeasure (E := E) p hp).real C ≤
      ∑ i ∈ s, (bernoulliProductMeasure (E := E) p hp).real (P i) *
        (bernoulliProductMeasure (E := E) p hp).real (Q i) *
        (bernoulliProductMeasure (E := E) p hp).real (R i)

Uses 7

Statement usesConfiguration space of a statistical-mechanics model · Event depending only on a set of coordinates · Increasing event · Bernoulli product measure on configuration space · Disjoint occurrence of events

Proof usesBernoulli distribution on the Booleans · BK inequality for three increasing events

TheoremIncreasing-event probabilities are monotone in the parameter#✓fully proved

Monotonicity in the parameter: for an increasing event A depending only on a finite set of coordinates and p ≤ q, P_p(A) ≤ P_q(A). The proof uses Russo's formula.

theorem ibk_measure_mono_parameter {p q : ℝ≥0} (hp : p ≤ 1) (hq : q ≤ 1)
    (hpq : p ≤ q) {A : Set (ConfigSpace E)} (F : Finset E)
    (hAdep : DependsOn A (F : Set E)) (hAinc : IsIncreasing A) :
    (bernoulliProductMeasure (E := E) p hp).real A ≤
      (bernoulliProductMeasure (E := E) q hq).real A

Uses 12 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Event depending only on a set of coordinates · Increasing event · Bernoulli product measure on configuration space

Proof usesRusso's formula · Differentiability in \(p\) of the probability of a cylinder event · Indicator of an event depends on the coordinates the event depends on · Finite projections of increasing events are increasing · Weight of the event that a coordinate is pivotal · Nonnegativity of the pivotal weight · Bernoulli weight of an event · Probability of a finitely dependent event as a finite weight

Used byMonotonicity in \(p\) of the Bernoulli percolation probability

DefinitionInhomogeneous Bernoulli product measure#✓fully proved

The product measure on ConfigSpace E under which coordinate e is open (true) with probability p e, independently.

noncomputable def inhomBernoulliProductMeasure (p : E → ℝ≥0)
    (hp : ∀ e, p e ≤ 1) : Measure (ConfigSpace E) :=
  Measure.infinitePi (fun e => bernoulliMeasure (p e) (hp e))

Uses 2 · Used by 5

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli distribution on the Booleans

Used byInhomogeneous Bernoulli product with constant parameter · BK inequality for inhomogeneous Bernoulli measures on a finite set · BK inequality for inhomogeneous measures on a countable set · Aizenman–Barsky inequality on infinite vertex-transitive graphs · Bond percolation measure on the ghost graph

TheoremInhomogeneous Bernoulli product with constant parameter#✓fully proved

For a constant parameter, the inhomogeneous product is bernoulliProductMeasure.

theorem inhomBernoulliProductMeasure_const (p : ℝ≥0) (hp : p ≤ 1) :
    inhomBernoulliProductMeasure (E := E) (fun _ => p) (fun _ => hp)
      = bernoulliProductMeasure p hp

Uses 3

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

TheoremBK inequality for inhomogeneous Bernoulli measures on a finite set#✓fully proved

The BK inequality for an inhomogeneous Bernoulli product measure on a finite set.

theorem inhom_bk_inequality [Fintype E] [DecidableEq E]
    (p : E → ℝ≥0) (hp : ∀ e, p e ≤ 1)
    {A B : Set (ConfigSpace E)} (hA : IsIncreasing A) (hB : IsIncreasing B) :
    (inhomBernoulliProductMeasure p hp).real (disjointOccurrence A B) ≤
      (inhomBernoulliProductMeasure p hp).real A *
        (inhomBernoulliProductMeasure p hp).real B

Uses 9 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Increasing event · Disjoint occurrence of events · Inhomogeneous Bernoulli product measure

Proof usesBernoulli distribution on the Booleans · Bernoulli point masses sum to one · BK inequality for product weights on a finite set · Product weight of a configuration · Weighted probability of an event

Used byBK inequality for inhomogeneous measures on a countable set

TheoremBK inequality for inhomogeneous measures on a countable set#✓fully proved

The BK inequality for an inhomogeneous Bernoulli product measure on a countable set, for increasing events depending on finitely many coordinates.

theorem inhom_bk_of_finite_dependsOn (p : E → ℝ≥0) (hp : ∀ e, p e ≤ 1)
    {A B : Set (ConfigSpace E)} (F : Finset E)
    (hAdep : DependsOn A (F : Set E)) (hBdep : DependsOn B (F : Set E))
    (hAinc : IsIncreasing A) (hBinc : IsIncreasing B) :
    (inhomBernoulliProductMeasure p hp).real (disjointOccurrence A B) ≤
      (inhomBernoulliProductMeasure p hp).real A *
        (inhomBernoulliProductMeasure p hp).real B

Uses 12

Statement usesConfiguration space of a statistical-mechanics model · Event depending only on a set of coordinates · Increasing event · Disjoint occurrence of events · Inhomogeneous Bernoulli product measure

Proof usesBernoulli distribution on the Booleans · Disjoint occurrence preserves finite dependence · Section of a disjoint occurrence · Finitely dependent event is a cylinder over its section · Section of an event on a finite coordinate set · Section of an increasing event is increasing · BK inequality for inhomogeneous Bernoulli measures on a finite set

TheoremBK criterion for Bernoulli product measures#✓fully proved

The BK criterion: if C ⊆ ⋃_i P_i ∘ Q_i ∘ R_i with increasing events, then P_p(C) ≤ ∑_i P_p(P_i) P_p(Q_i) P_p(R_i) for the Bernoulli product measure. Reference: J. van den Berg, H. Kesten, "Inequalities with applications to percolation and reliability", J. Appl. Probab. 22 (1985) 556–569.

theorem bk_criterion {ι : Type*} [Fintype E] [DecidableEq E] {p : ℝ≥0} (hp : p ≤ 1)
    (s : Finset ι) (P Q R : ι → Set (ConfigSpace E))
    (hP : ∀ i ∈ s, IsIncreasing (P i)) (hQ : ∀ i ∈ s, IsIncreasing (Q i))
    (hR : ∀ i ∈ s, IsIncreasing (R i))
    {C : Set (ConfigSpace E)}
    (hC : C ⊆ ⋃ i ∈ s, disjointOccurrence (P i) (disjointOccurrence (Q i) (R i))) :
    (bernoulliProductMeasure (E := E) p hp).real C
      ≤ ∑ i ∈ s, (bernoulliProductMeasure (E := E) p hp).real (P i)
          * (bernoulliProductMeasure (E := E) p hp).real (Q i)
          * (bernoulliProductMeasure (E := E) p hp).real (R i)

Uses 7

Statement usesConfiguration space of a statistical-mechanics model · Increasing event · Bernoulli product measure on configuration space · Disjoint occurrence of events

Proof usesBernoulli distribution on the Booleans · Van den Berg–Kesten inequality · Disjoint occurrence of increasing events is increasing

DefinitionOpen subgraph of a configuration#✓fully proved

The subgraph of G of edges open in the configuration ω.

def openSub (G : SimpleGraph V) (ω : ConfigSpace (Sym2 V)) : SimpleGraph V where
  Adj x y := G.Adj x y ∧ ω s(x, y) = true
  symm := by
    constructor
    intro x y ⟨hadj, hopen⟩
    exact ⟨hadj.symm, by rwa [Sym2.eq_swap]⟩
  loopless := ⟨fun x ⟨hadj, _⟩ => G.loopless.1 x hadj⟩

Uses 1 · Used by 7

Statement usesConfiguration space of a statistical-mechanics model

Used byOpen connection between two vertices inside a set · Aizenman–Barsky inequality on a finite graph · Aizenman–Barsky inequality on infinite vertex-transitive graphs · Edges used by an open walk in an induced subgraph · Transfer of an open walk between agreeing configurations · Transfer of an open walk avoiding a fixed edge · Mean-field differential inequality for inhomogeneous percolation

DefinitionOpen connection between two vertices inside a set#✓fully proved

x and y are joined by an open path staying in A.

def ConnWithin (G : SimpleGraph V) (ω : ConfigSpace (Sym2 V)) (A : Set V) (x y : A) : Prop :=
  ((openSub G ω).induce A).Reachable x y

Uses 2 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Open subgraph of a configuration

Used byOpen connection inside a set to a target set · Aizenman–Barsky inequality on a finite graph · Aizenman–Barsky inequality on infinite vertex-transitive graphs · Mean-field differential inequality for inhomogeneous percolation

DefinitionOpen connection inside a set to a target set#✓fully proved

u ∈ A is joined by an open path in A to some vertex of A ∩ B.

def ConnToSet (G : SimpleGraph V) (ω : ConfigSpace (Sym2 V)) (A : Set V)
    (u : V) (B : Set V) : Prop :=
  ∃ (hu : u ∈ A) (b : V) (hb : b ∈ A), b ∈ B ∧ ConnWithin G ω A ⟨u, hu⟩ ⟨b, hb⟩

Uses 2 · Used by 5

Statement usesConfiguration space of a statistical-mechanics model · Open connection between two vertices inside a set

Used byConnection event inside a set · Aizenman–Barsky inequality on a finite graph · Aizenman–Barsky inequality on infinite vertex-transitive graphs · Vertices not connected to a target set · Mean-field differential inequality for inhomogeneous percolation

DefinitionConnection event inside a set#✓fully proved

The event that u is connected to B by an open path inside A.

def connEvent (G : SimpleGraph V) (A : Set V) (u : V) (B : Set V) :
    Set (ConfigSpace (Sym2 V)) := {ω | ConnToSet G ω A u B}

Uses 2 · Used by 8

Statement usesConfiguration space of a statistical-mechanics model · Open connection inside a set to a target set

Used byAizenman–Barsky inequality on a finite graph · Finite-volume percolation magnetization · Sites connected to \(o\) with ghost edges closed · Aizenman–Barsky inequality on infinite vertex-transitive graphs · Infinite-volume percolation magnetization · Event that a vertex is connected to a target set · Mean-field differential inequality for inhomogeneous percolation · Inhomogeneous Duminil-Copin–Tassion quantity \(\varphi(S)\)

DefinitionEvent that an edge is open#✓fully proved

The event that the edge {x, y} is open.

def edgeOpenEvent (x y : V) : Set (ConfigSpace (Sym2 V)) := {ω | ω s(x, y) = true}

Uses 1 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model

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

DefinitionOrdered boundary pairs of a set#✓fully proved

The ordered pairs (x, y) with x ∈ S, y ∉ S adjacent in G.

def shk_boundaryPairs [Fintype V] [DecidableEq V] (G : SimpleGraph V) (S : Finset V)
    [DecidableRel G.Adj] : Finset (V × V) :=
  Finset.univ.filter (fun q => q.1 ∈ S ∧ q.2 ∉ S ∧ G.Adj q.1 q.2)

Used by 2

Used byMean-field differential inequality for inhomogeneous percolation · Inhomogeneous Duminil-Copin–Tassion quantity \(\varphi(S)\)

DefinitionEdge law of inhomogeneous bond percolation#✓fully proved

The edge law of inhomogeneous bond percolation: open with probability 1 - exp(-βJ_e), closed with probability exp(-βJ_e).

noncomputable def shk_edgeLaw (beta : ℝ) (J : E → ℝ) (e : E) (b : Bool) : ℝ :=
  if b then 1 - Real.exp (-beta * J e) else Real.exp (-beta * J e)

Used by 3

Used byMean-field differential inequality for inhomogeneous percolation · Inhomogeneous Duminil-Copin–Tassion quantity \(\varphi(S)\) · Product of the edge laws over all other edges

DefinitionSupport of the first-exit decomposition events#✓fully proved

The edges inside S, the boundary edges of S, and the edges inside the window Λ: the support of the events in the first-exit decomposition.

noncomputable def shk_firstExitSupport (S Lam : Finset (Site d)) :
    Finset (Sym2 (Site d)) :=
  (edgesWithinFinset S ∪
      (boundaryEdges d S).image (fun q => s(q.1, q.2))) ∪
    edgesWithinFinset Lam

Uses 3

Statement usesSite of the hypercubic lattice · Oriented edge boundary of a finite lattice set · Pairs of sites of a finite set

73 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.