Finite Strassen stochastic domination

DefinitionFinite upper sets#✓fully proved

A finite subset \(U\) of a preordered set \(\alpha\) is an upper set (is upward closed) if for all \(x, y \in \alpha\) with \(x \in U\) and \(x \le y\), also \(y \in U\).

def IsUpperSet {α : Type*} [Preorder α] (U : Finset α) : Prop :=
  ∀ ⦃x y : α⦄, x ∈ U → x ≤ y → y ∈ U

Used by 3

Used byStrassen's theorem on a finite poset, equal-mass form · Strassen's theorem on a finite poset · Strassen's theorem

TheoremStrassen's theorem on a finite poset, equal-mass form#✓fully proved

Let \(\alpha\) be a finite partially ordered set and let \(p, q : \alpha \to \mathbb{R}\) be nonnegative functions with \(\sum_{x \in \alpha} p(x) = \sum_{x \in \alpha} q(x)\). Then \(\sum_{x \in U} p(x) \le \sum_{x \in U} q(x)\) for every upper set \(U \subseteq \alpha\) if and only if there is a function \(\pi : \alpha \times \alpha \to \mathbb{R}\) such that \(\pi(x, y) \ge 0\) for all \(x, y \in \alpha\), \(\sum_{y \in \alpha} \pi(x, y) = p(x)\) for every \(x \in \alpha\), \(\sum_{x \in \alpha} \pi(x, y) = q(y)\) for every \(y \in \alpha\), and \(\pi(x, y) = 0\) whenever \(x \not\le y\).

theorem forall_isUpperSet_sum_le_iff_exists_coupling
    {α : Type*} [Fintype α] [PartialOrder α]
    (p q : α → ℝ)
    (hp_nonneg : ∀ x, 0 ≤ p x)
    (hq_nonneg : ∀ x, 0 ≤ q x)
    (hsum : ∑ x : α, p x = ∑ x : α, q x) :
    (∀ U : Finset α, IsUpperSet U → ∑ x ∈ U, p x ≤ ∑ x ∈ U, q x) ↔
    ∃ π : α → α → ℝ,
      (∀ x y, 0 ≤ π x y) ∧
      (∀ x, ∑ y : α, π x y = p x) ∧
      (∀ y, ∑ x : α, π x y = q y) ∧
      (∀ x y, ¬ x ≤ y → π x y = 0)

Uses 1 · Used by 2

Statement usesFinite upper sets

Used byStrassen's theorem on a finite poset · Strassen's theorem

TheoremStrassen's theorem on a finite poset#✓fully proved

Let \(\alpha\) be a finite partially ordered set and let \(p, q : \alpha \to \mathbb{R}\) be probability mass functions, that is, nonnegative functions with \(\sum_{x \in \alpha} p(x) = 1\) and \(\sum_{x \in \alpha} q(x) = 1\). Then \(\sum_{x \in U} p(x) \le \sum_{x \in U} q(x)\) for every upper set \(U \subseteq \alpha\) if and only if there is a function \(\pi : \alpha \times \alpha \to \mathbb{R}\) such that \(\pi(x, y) \ge 0\) for all \(x, y \in \alpha\), \(\sum_{y \in \alpha} \pi(x, y) = p(x)\) for every \(x \in \alpha\), \(\sum_{x \in \alpha} \pi(x, y) = q(y)\) for every \(y \in \alpha\), and \(\pi(x, y) = 0\) whenever \(x \not\le y\).

theorem strassen_coupling_finite_poset
    {α : Type*} [Fintype α] [PartialOrder α] [DecidableEq α]
    [DecidableLE α]
    (p q : α → ℝ)
    (hp_nonneg : ∀ x, 0 ≤ p x)
    (hq_nonneg : ∀ x, 0 ≤ q x)
    (hp_sum : ∑ x : α, p x = 1)
    (hq_sum : ∑ x : α, q x = 1) :
    (∀ U : Finset α, IsUpperSet U → ∑ x ∈ U, p x ≤ ∑ x ∈ U, q x) ↔
    ∃ π : α → α → ℝ,
      (∀ x y, 0 ≤ π x y) ∧
      (∀ x, ∑ y : α, π x y = p x) ∧
      (∀ y, ∑ x : α, π x y = q y) ∧
      (∀ x y, ¬ x ≤ y → π x y = 0)

Sources

• V. Strassen, "The Existence of Probability Measures with Given Marginals", Ann. Math. Statist. 36 (1965), 423-439, DOI 10.1214/aoms/1177700153.

Uses 2

Statement usesFinite upper sets

Proof usesStrassen's theorem on a finite poset, equal-mass form

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.