Strassen's theorem for configurations on a finite set

5 fully proved

Transport

DefinitionDown-set of a partial order#✓fully proved

D is a down-set of P: x ≤ y and y ∈ D imply x ∈ D.

def IsDown (D : Finset P) : Prop := ∀ x y, x ≤ y → y ∈ D → x ∈ D

Used by 2

Used byStrassen's theorem · Strassen's theorem

AbbreviationOrdered pairs of a partial order#✓fully proved

The ordered pairs (x, y) with x ≤ y; couplings supported on the order are vectors indexed by OrderPairs P.

abbrev OrderPairs (P : Type*) [PartialOrder P] := {p : P × P // p.1 ≤ p.2}

Used by 2

Used byStrassen's theorem · Strassen's theorem

TheoremStrassen's theorem#✓fully proved

Strassen's theorem on a finite poset P, for nonnegative vectors: if μ and ν have equal total mass and ν(D) ≤ μ(D) for every down-set D, there is a nonnegative c on the ordered pairs x ≤ y with first marginal μ and second marginal ν. This is the ordered-pair vector form of MathlibExt.Probability.StrassenCouplingWanted.forall_isUpperSet_sum_le_iff_exists_coupling.

theorem exists_coupling_vec (μ ν : P → ℝ)
    (hμpos : ∀ x, 0 ≤ μ x) (hνpos : ∀ x, 0 ≤ ν x)
    (hTOT : ∑ x, μ x = ∑ x, ν x)
    (hDOM : ∀ D : Finset P, IsDown D → ∑ x ∈ D, ν x ≤ ∑ x ∈ D, μ x) :
    ∃ c : OrderPairs P → ℝ, (∀ q, 0 ≤ c q) ∧
      (∀ x, (∑ q : OrderPairs P, if (q : P × P).1 = x then c q else 0) = μ x) ∧
      (∀ y, (∑ q : OrderPairs P, if (q : P × P).2 = y then c q else 0) = ν y)

Uses 4 · Used by 1

Statement usesDown-set of a partial order · Ordered pairs of a partial order

Proof usesFinite upper sets · Strassen's theorem on a finite poset, equal-mass form

Used byStrassen's theorem

Stat Mech

DefinitionMeasure on ordered pairs from a mass vector#✓fully proved

The measure on pairs of configurations that puts mass c q on each ordered pair q.

noncomputable def kappaOfVec
    (c : {p : ConfigSpace E × ConfigSpace E // p.1 ≤ p.2} → ℝ) :
    Measure (ConfigSpace E × ConfigSpace E) :=
  ∑ q : {p : ConfigSpace E × ConfigSpace E // p.1 ≤ p.2},
    (ENNReal.ofReal (c q)) • Measure.dirac (q : ConfigSpace E × ConfigSpace E)

Uses 1 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model

Used byStrassen's theorem

TheoremStrassen's theorem#✓fully proved

Strassen's theorem for configurations on a finite set: if μ ≼ ν are probability measures on ConfigSpace E, there is a finite monotone coupling of μ and ν (V. Strassen, The existence of probability measures with given marginals, 1965). The converse is StatMech.MonotoneCoupling.stochasticallyDominated.

theorem exists_monotoneCoupling_of_stochasticallyDominated
    [Finite E] (μ ν : Measure (ConfigSpace E)) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
    (hdom : μ ≼ ν) :
    ∃ κ : Measure (ConfigSpace E × ConfigSpace E),
      IsFiniteMeasure κ ∧ MonotoneCoupling μ ν κ

Uses 10 · Used by 4

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

Proof usesIncreasing event · Stochastic domination compares real-valued masses · Down-set of a partial order · Ordered pairs of a partial order · Strassen's theorem · Measure on ordered pairs from a mass vector · Set of coordinatewise ordered configuration pairs

Used byHolley's coupling 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\)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.