Stochastic domination of measures on configuration space

DefinitionStochastic domination of measures on configurations#✓fully proved

μ is stochastically dominated by ν if their actual ENNReal masses satisfy μ(A) ≤ ν(A) for every measurable increasing event A ⊆ ConfigSpace E.

def StochasticallyDominated (μ ν : Measure (ConfigSpace E)) : Prop :=
  ∀ A : Set (ConfigSpace E), MeasurableSet A → IsIncreasing A → μ A ≤ ν A

Uses 2 · Used by 35

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

Used byHolley's inequality · Strassen's theorem, easy direction · Existence of a monotone coupling implies stochastic domination · Stochastic domination compares real-valued masses · Stochastic domination is reflexive · Stochastic domination is transitive · Strassen's theorem · 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 · 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 · Stochastic domination implies clopen domination, upper measure finite · 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 · Free percolation from domination and free–wired agreement at \(p'\) · Free percolation above \(p_c\) from monotonicity and countable agreement · Comparison inequalities · Random-cluster measure increases stochastically in \(p\) when \(q \ge 1\) · Free box measure dominated by the wired one for \(q \ge 1\) · Convergence to the free two-point function under stochastic increase · Masses of clopen increasing events converge along decreasing measures · Convergence to the wired two-point function under stochastic decrease · 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\) · Mean-field lower bound for the spontaneous magnetization

TheoremStochastic domination is reflexive#✓fully proved

Stochastic domination is reflexive.

@[refl] theorem StochasticallyDominated.refl (μ : Measure (ConfigSpace E)) : μ ≼ μ

Uses 3

Statement usesConfiguration space of a statistical-mechanics model · Stochastic domination of measures on configurations

Proof usesIncreasing event

TheoremStochastic domination is transitive#✓fully proved

Stochastic domination is transitive.

theorem StochasticallyDominated.trans {μ ν ρ : Measure (ConfigSpace E)}
    (h₁ : μ ≼ ν) (h₂ : ν ≼ ρ) : μ ≼ ρ

Uses 3

Statement usesConfiguration space of a statistical-mechanics model · Stochastic domination of measures on configurations

Proof usesIncreasing event

TheoremStochastic domination compares real-valued masses#✓fully proved

For a finite upper measure, stochastic domination also compares real-valued masses.

theorem StochasticallyDominated.real {μ ν : Measure (ConfigSpace E)} (h : μ ≼ ν)
    [IsFiniteMeasure ν] (A : Set (ConfigSpace E)) (hAm : MeasurableSet A)
    (hA : IsIncreasing A) : μ.real A ≤ ν.real A

Uses 3 · Used by 27

Statement usesConfiguration space of a statistical-mechanics model · Increasing event · Stochastic domination of measures on configurations

Used byStrassen's theorem · Increasing-event probabilities along a decreasing chain are antitone · Stochastic domination from below passes 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 · Stochastic domination implies clopen domination, upper measure finite · 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 · Free percolation from domination and free–wired agreement at \(p'\) · Wired \(q = 2\) measure dominates the free one on increasing cylinders · Free limit at most wired limit along a common subsequence, \(q \ge 1\) · Secant bound gives free–wired density agreement off a countable set · Free density is at most each translated wired marginal · Masses of clopen increasing events converge along decreasing measures · Per-box \(q = 2\) uniqueness off a countable set of tilts · 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\) · Mean-field lower bound for the spontaneous magnetization

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.