Monotone couplings and stochastic domination

5 fully proved

Stat Mech

DefinitionSet of coordinatewise ordered configuration pairs#✓fully proved

The set of ordered pairs (ω, ω') of configurations with ω ≤ ω' coordinatewise.

def orderSet (E : Type*) : Set (ConfigSpace E × ConfigSpace E) := {p | p.1 ≤ p.2}

Uses 1 · Used by 6

Statement usesConfiguration space of a statistical-mechanics model

Used byMonotone coupling of two measures · Strassen's theorem, easy direction · Strassen's theorem · 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\)

StructureMonotone coupling of two measures#✓fully proved

κ is a monotone coupling of μ and ν: a measure on pairs of configurations with first marginal μ, second marginal ν, and no mass off the ordered pairs ω ≤ ω'.

structure MonotoneCoupling (μ ν : Measure (ConfigSpace E))
    (κ : Measure (ConfigSpace E × ConfigSpace E)) : Prop where
  /-- The first marginal of `κ` is `μ`. -/
  fst_eq : κ.fst = μ
  /-- The second marginal of `κ` is `ν`. -/
  snd_eq : κ.snd = ν
  /-- `κ` is concentrated on the ordered pairs. -/
  supported : κ (orderSet E)ᶜ = 0

Uses 2 · Used by 8

Statement usesConfiguration space of a statistical-mechanics model · Set of coordinatewise ordered configuration pairs

Used byHolley's coupling theorem · Strassen's theorem, easy direction · Existence of a monotone coupling implies stochastic domination · Marginals of a coupling have equal total mass · Strassen's theorem · 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\)

Monotone Coupling

TheoremMarginals of a coupling have equal total mass#✓fully proved

The two marginals of a coupling have the same total mass.

theorem total_mass_eq (h : MonotoneCoupling μ ν κ) : μ Set.univ = ν Set.univ

Uses 2

Statement usesConfiguration space of a statistical-mechanics model · Monotone coupling of two measures

TheoremStrassen's theorem, easy direction#✓fully proved

A finite monotone coupling of μ and ν shows μ ≼ ν: the easy direction of Strassen's theorem.

theorem stochasticallyDominated (h : MonotoneCoupling μ ν κ)
    [IsFiniteMeasure κ] : μ ≼ ν

Uses 5 · Used by 1

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

Proof usesIncreasing event · Set of coordinatewise ordered configuration pairs

Used byExistence of a monotone coupling implies stochastic domination

Stat Mech

TheoremExistence of a monotone coupling implies stochastic domination#✓fully proved

If a finite monotone coupling of μ and ν exists, then μ ≼ ν.

theorem stochasticallyDominated_of_exists_monotoneCoupling
    {μ ν : Measure (ConfigSpace E)}
    (h : ∃ κ : Measure (ConfigSpace E × ConfigSpace E),
          IsFiniteMeasure κ ∧ MonotoneCoupling μ ν κ) :
    μ ≼ ν

Uses 4

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

Proof usesStrassen's theorem, easy direction

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.