Increasing events and the FKG lattice condition

DefinitionIncreasing event#✓fully proved

An event A ⊆ ConfigSpace E is increasing if it is an upper set for the coordinatewise order: ω ∈ A and ω ≤ ω' imply ω' ∈ A. This is IsUpperSet A.

def IsIncreasing (A : Set (ConfigSpace E)) : Prop := IsUpperSet A

Uses 1 · Used by 199

Statement usesConfiguration space of a statistical-mechanics model

Used bySharp-threshold bound assuming the KKL inequality on \((1/2, q)\) · Sharp-threshold window bound assuming the KKL inequality on \((1/2, q)\) · Sharp-threshold bound under the \(p\)-biased KKL hypothesis · Sharp-threshold window under the \(p\)-biased KKL hypothesis · Sharp-threshold bound from the conditional KKL statement · FKG inequality for increasing events · Holley inequality for increasing events · Holley's inequality · Harris inequality · Harris inequality for finitely dependent increasing events · Section of an increasing event is increasing · Complement of an increasing event is decreasing · Complement of a decreasing event is increasing · Indicator of an increasing event is monotone · Intersection of two increasing events is increasing · Arbitrary intersections of increasing events are increasing · An event is increasing iff its indicator is monotone · Union of two increasing events is increasing · Russo's formula · Russo's formula · Pivotal coordinates of an increasing event · Contribution of one coordinate to Russo's formula · Russo's formula on a single fiber · BK 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 of increasing events is increasing · Union bound from the three-event BK inequality · BK inequality on countable configuration spaces · Increasing-event probabilities are monotone in the parameter · 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 · Occurrence of an increasing event is monotone in the configuration · False slice of an increasing event lies in the true slice · Slices of an increasing event are increasing · Reimer's inequality for two upper families · 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 · Harris–FKG inequality for an increasing and a decreasing event · Harris–FKG inequality for increasing events · BK inequality for decreasing events under product weights · Slice inequalities in the one-coordinate BK induction step · Strassen's theorem, easy direction · Stochastic domination compares real-valued masses · Stochastic domination is reflexive · Stochastic domination of measures on configurations · Stochastic domination is transitive · Strassen's theorem · Positively associated measure · Positive association for probability measures is the Harris–FKG inequality · Harris–FKG inequality for a positively associated probability measure · Square-root trick · RSW gluing from side separation · Wired \(q = 2\) origin-to-boundary probability at most Bernoulli · Sharp threshold from a KKL-type influence inequality · Russo's formula · Sharp threshold from influences · Aizenman–Barsky inequality on a finite graph · Aizenman–Barsky inequality on infinite vertex-transitive graphs · Duminil-Copin–Tassion differential inequality · Mean-field differential inequality for inhomogeneous percolation · Russo's formula · Russo's formula · Russo's formula for the Bernoulli product measure · Russo's formula · Russo's formula · Russo's formula · Finite projections of increasing events are increasing · Increasing-event probabilities along a decreasing chain are antitone · Stochastic domination from below passes to weak limits · Weak limit of a decreasing chain is dominated by its terms · Weak limit of an increasing chain dominates its terms · Lower bounds on clopen-event probabilities pass to weak limits · Increasing-event probabilities along an increasing chain are monotone · Convergence of increasing-event probabilities along an increasing chain · Stochastic domination from above passes to weak limits · Uniqueness of the Gibbs state · FK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sup-based \(\beta_c\) equals \(-\tfrac{1}{2}\log(1 - p_c)\) for \(d \ge 2\) · Existence of the Ising phase transition · Ergodicity of the plus state · Translation invariance of the plus state · Extremality of the plus state · Set where coupled measures differ is countable under a convex pressure · Coupled measures agree off a countable set, given a convex pressure · Monotonicity in \(p\) of free \(q = 2\) edge marginals on a finite graph · Left-continuity of the free \(q = 2\) edge density in \(t\) · Free \(q = 2\) edge density is monotone in \(p\) on \((0, 1)\) · Wired \(q = 2\) edge density is monotone in \(t\) · Right-continuity of the wired \(q = 2\) edge density in \(t\) · The percolation event is increasing · Wired box-boundary connection probability is monotone in \(p\) at \(q = 2\) · Event of some open self-avoiding walk is increasing · Event that a given walk is open is increasing · Wired box bound \((2dp)^m\) on the open-walk event for \(q \ge 1\) · Wired law at most the \(q = 1\) law on increasing events, \(q \ge 1\) · Free–wired sandwich for boundary graphs inside the boundary clique · Sandwich between the free and all-wired boundary conditions · Random-cluster comparison of boundary conditions for \(q \ge 1\) · Boundary-graph FK measure increases in \(p\) for \(q \ge 1\) · Conditional measures increase with the wiring for \(q \ge 1\) · Monotone couplings with equal edge marginals agree on up-sets · Boundary wirings lie between free and wired when \(q \ge 1\) · Free–wired domination on a finite graph for \(q \ge 1\) · FKG inequality for increasing random-cluster events · Monotonicity of the random-cluster measure in p · Free box measure dominated by the wired one for \(q \ge 1\) · Wirings with the boundary clique dominate the wired measure, \(q \ge 1\) · Wired measure conditionally dominated by larger wirings, \(q \ge 1\) · Wired box measure dominates the induced-wiring measure for \(q \ge 1\) · Conditional outer wired probability at most the inner wired one, \(q \ge 1\) · Domination by the inner wired measure under a coarser induced wiring · Free inner measure is dominated by the conditional outer measure · Free inner measure is dominated by every induced-wiring measure · Inner wired domination for vertex sets of \(\mathbb{Z}^d\) · Outer wired all-open probability at most the inner wired one · Inner wired domination of the restricted outer wired measure · FKG inequality for free \(q = 2\) box measures on smaller-box events · FKG inequality for the free \(q = 2\) infinite-volume measure · FKG inequality for the wired \(q = 2\) infinite-volume measure · Wired \(q = 2\) measure dominates the free one on increasing cylinders · FKG inequality for wired \(q = 2\) box measures on smaller-box events · FKG inequality for the wired measure when \(q \ge 1\) · Convergence and ordering of free and wired limits at \(q = 2\) · Convergence and ordering at \(q = 2\) in subsequence form · Wired all-open probabilities converge to the infinite-volume value · Free all-open probabilities converge to the infinite-volume value · Free translation invariance from free placements of every shift · Wired translation invariance from wired placements of every shift · Closed-annulus wired bound on origin-to-\(\partial\Lambda_n\), \(q = 2\) · Ordered free and wired subsequential limits exist for \(q \ge 1\) · Free limit at most wired limit along a common subsequence, \(q \ge 1\) · Free \(q=2\) box masses of increasing cylinders tend to infinite volume · Free \(q = 2\) box measures of increasing cylinders converge · Free \(q = 2\) infinite-volume mass of increasing cylinders as a box limit · One-step growth of free \(q = 2\) measures of increasing cylinders · Free \(q = 2\) box measures of increasing cylinders are monotone · Conditional free measure dominates the smaller free box for \(q \ge 1\) · Free measure is dominated by induced-wiring measures for \(q \ge 1\) · Increasing box events gain free \(q = 2\) probability in the next box · One-step box monotonicity of free measures for \(q \ge 1\) · Secant bound gives free–wired density agreement off a countable set · Free density is at most each translated wired marginal · Translated wired marginals converge to the wired density · Equal wired densities from equal translated marginals · Wired infinite-volume measure as limit on increasing cylinder events · Wired box probabilities of increasing cylinder events converge · Wired \(q = 2\) increasing-event probabilities do not grow with the box · Wired infinite-volume probability equals the infimum over boxes · Convergence to the free two-point function under stochastic increase · Box restriction pulls increasing events back to increasing events · Masses of clopen increasing events converge along decreasing measures · Convergence to the wired two-point function under stochastic decrease · Conditional wired decrease on inner increasing events for \(q \ge 1\) · Origin-to-boundary connection is an increasing event · Boundary-connection event of \(\Lambda_n\) on \(\Lambda_m\) is increasing · Wired \(q = 2\) probability of \(0 \leftrightarrow \partial\Lambda_n\) in \(\Lambda_{n+1}\) at most in \(\Lambda_n\) · Wired box measures decrease on increasing cylinder events at \(q = 2\) · Wired box measures decrease on inner increasing events for \(q \ge 1\) · Countably many parameters admit a separating increasing event · Per-box \(q = 2\) uniqueness off a countable set of tilts · Monotone-coupled laws with equal edge marginals agree on up-sets · Secant bound gives \(q = 2\) edge-event uniqueness off a countable set · Per-box uniqueness of the random-cluster measures off a countable set · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Free-energy data give \(q = 2\) box uniqueness off countably many \(t\) · Free off-centre lower bound by the recentred small-box marginal · Free unit-edge marginals converge to the free density · Wired unit-edge marginals converge to the wired density · Parametric agreement on increasing events off a countable set · Free \(q = 2\) edge density lies in \((0, 1)\) · Wired \(q = 2\) edge density lies in \((0, 1)\) · Box symmetries preserve the free \(q = 2\) density of box edges · Box symmetries preserve the wired \(q = 2\) density of box edges · FKG inequality for connection events for \(q \ge 1\) · Translation invariance of the free \(q = 2\) infinite-volume measure · Free \(q = 2\) box edge marginals are at most the free density · Wired \(q = 2\) box edge marginals are at least the wired density · Ergodicity of the wired random-cluster measure · Conditional product cap for multi-open events in boxes · Constant free density gives an upper bound on expected open edges · Equal free densities from merging free marginals · Constant wired density gives a lower bound on expected open edges · Equal wired densities from merging wired marginals · Wired box products approximate infinite-volume products · Upper decorrelation of the wired measure from factorization · Domain monotonicity of wired \(q = 2\) box measures · Wired \(q = 2\) measure is ergodic under the factorization bound · Domain monotonicity of wired multi-open probabilities · Decay of the edge-indicator functional from equal wired densities · Free translation invariance from the placement hypothesis · Wired translation invariance from the placement hypothesis · Mean-field lower bound for the spontaneous magnetization · 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\)

DefinitionDecreasing event#✓fully proved

An event A ⊆ ConfigSpace E is decreasing if it is a lower set for the coordinatewise order. This is IsLowerSet A.

def IsDecreasing (A : Set (ConfigSpace E)) : Prop := IsLowerSet A

Uses 1 · Used by 10

Statement usesConfiguration space of a statistical-mechanics model

Used byComplement of an increasing event is decreasing · Complement of a decreasing event is increasing · Reimer's inequality for two lower families · 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 · Harris–FKG inequality for an increasing and a decreasing event · BK inequality for decreasing events · BK inequality for decreasing events under product weights · Square-root trick

LemmaComplement of an increasing event is decreasing#✓fully proved

The complement of an increasing event is decreasing (IsUpperSet.compl).

lemma IsIncreasing.compl {A : Set (ConfigSpace E)} (hA : IsIncreasing A) :
    IsDecreasing Aᶜ

Uses 3 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Decreasing event · Increasing event

Used bySquare-root trick

LemmaComplement of a decreasing event is increasing#✓fully proved

The complement of a decreasing event is increasing (IsLowerSet.compl).

lemma IsDecreasing.compl {A : Set (ConfigSpace E)} (hA : IsDecreasing A) :
    IsIncreasing Aᶜ

Uses 3 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Decreasing event · Increasing event

Used byHarris–FKG inequality for an increasing and a decreasing event · Square-root trick

LemmaIntersection of two increasing events is increasing#✓fully proved

The intersection of two increasing events is increasing (IsUpperSet.inter).

lemma IsIncreasing.inter {A B : Set (ConfigSpace E)}
    (hA : IsIncreasing A) (hB : IsIncreasing B) : IsIncreasing (A ∩ B)

Uses 2 · Used by 3

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

Used byRSW gluing from side separation · FKG inequality for the free \(q = 2\) infinite-volume measure · FKG inequality for the wired \(q = 2\) infinite-volume measure

LemmaUnion of two increasing events is increasing#✓fully proved

The union of two increasing events is increasing (IsUpperSet.union).

lemma IsIncreasing.union {A B : Set (ConfigSpace E)}
    (hA : IsIncreasing A) (hB : IsIncreasing B) : IsIncreasing (A ∪ B)

Uses 2

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

LemmaArbitrary intersections of increasing events are increasing#✓fully proved

An intersection of increasing events is increasing (isUpperSet_iInter).

lemma isIncreasing_iInter {ι : Sort*} {A : ι → Set (ConfigSpace E)}
    (hA : ∀ i, IsIncreasing (A i)) : IsIncreasing (⋂ i, A i)

Uses 2

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

LemmaIndicator of an increasing event is monotone#✓fully proved

The real indicator function of an increasing event is monotone.

lemma IsIncreasing.indicator_monotone {A : Set (ConfigSpace E)} (hA : IsIncreasing A) :
    Monotone (A.indicator (fun _ => (1 : ℝ)))

Uses 2 · Used by 4

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

Used byFKG inequality for increasing events · Holley inequality for increasing events · An event is increasing iff its indicator is monotone · Monotone couplings with equal edge marginals agree on up-sets

TheoremAn event is increasing iff its indicator is monotone#✓fully proved

An event is increasing iff its real indicator function is monotone. See also Set.monotone_mem, the analogous statement for the Prop-valued membership predicate.

theorem isIncreasing_iff_indicator_monotone {A : Set (ConfigSpace E)} :
    IsIncreasing A ↔ Monotone (A.indicator (fun _ => (1 : ℝ)))

Uses 3

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

Proof usesIndicator of an increasing event is monotone

DefinitionFKG lattice condition#✓fully proved

The FKG lattice condition on a weight π : ConfigSpace E → ℝ: π ω * π ω' ≤ π (ω ⊔ ω') * π (ω ⊓ ω') for all configurations ω ω'. For a positive weight this is log-supermodularity. Mathlib's fkg and holley state it in the form π a * π b ≤ π (a ⊓ b) * π (a ⊔ b).

def FKGLatticeCondition (π : ConfigSpace E → ℝ) : Prop :=
  ∀ ω ω', π ω * π ω' ≤ π (ω ⊔ ω') * π (ω ⊓ ω')

Uses 1 · Used by 18

Statement usesConfiguration space of a statistical-mechanics model

Used byFKG inequality · FKG inequality for increasing events · Harris inequality · Log-modular weights satisfy the FKG lattice condition · Harris–FKG inequality for increasing events · Griffiths–Hurst–Sherman inequality · FKG lattice condition for the agreement law when \(\beta, h \ge 0\) · Griffiths–Hurst–Sherman inequality · Griffiths–Hurst–Sherman inequality · FKG inequality · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Ergodicity of the plus state · Extremality of the plus state · FKG inequality for the random-cluster measure, \(q \ge 1\) · FKG lattice condition for the random-cluster measure · FKG lattice condition for the wired measure when \(q \ge 1\) · 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\)

LemmaLog-modular weights satisfy the FKG lattice condition#✓fully proved

A log-modular weight, π ω * π ω' = π (ω ⊔ ω') * π (ω ⊓ ω'), satisfies the FKG lattice condition.

lemma FKGLatticeCondition.of_logModular {π : ConfigSpace E → ℝ}
    (h : ∀ ω ω', π ω * π ω' = π (ω ⊔ ω') * π (ω ⊓ ω')) : FKGLatticeCondition π

Uses 2 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · FKG lattice condition

Used byHarris inequality · Harris–FKG inequality for increasing events

11 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.