Optimal Couplings

This file provides the topological foundation to show that the space of couplings between two distributions with finite support is compact, and that continuous functions (like expected value) attain their supremum on this space.

The space of SPMFs as a bounded closed subset of Option (α × β) → ℝ

theorem map_fst_eval {α β : Type u} [Finite α] [Finite β] (c : SPMF (α × β)) (a : α) : (Prod.fst <$> c) a = ∑ b : β, c (a, b)

theorem map_snd_eval {α β : Type u} [Finite α] [Finite β] (c : SPMF (α × β)) (b : β) : (Prod.snd <$> c) b = ∑ a : α, c (a, b)

def couplings_set {α β : Type u} [Finite α] [Finite β] (p : SPMF α) (q : SPMF β) : Set (Option (α × β) → ℝ)

theorem isClosed_couplings_set {α β : Type u} [Finite α] [Finite β] (p : SPMF α) (q : SPMF β) : IsClosed (couplings_set p q)

theorem isBounded_couplings_set {α β : Type u} [Finite α] [Finite β] (p : SPMF α) (q : SPMF β) : Bornology.IsBounded (couplings_set p q)

theorem isCompact_couplings_set {α β : Type u} [Finite α] [Finite β] (p : SPMF α) (q : SPMF β) : IsCompact (couplings_set p q)

theorem mem_couplings_set_of_isCoupling {α β : Type u} [Finite α] [Finite β] {p : SPMF α} {q : SPMF β} (c : SPMF (α × β)) (hc : c.IsCoupling p q) : (fun (z : Option (α × β)) => (c.toPMF z).toReal) ∈ couplings_set p q

theorem SPMF.exists_max_coupling {α β : Type u} [Finite α] [Finite β] {p : SPMF α} {q : SPMF β} (f : Option (α × β) → ENNReal) (hf : ∀ (z : Option (α × β)), f z ≠ ⊤) (h_nonempty : Nonempty (p.Coupling q)) (h_comp : IsCompact (couplings_set p q)) : ∃ (c : p.Coupling q), ⨆ (c' : p.Coupling q), ∑' (z : Option (α × β)), ↑↑c' z * f z = ∑' (z : Option (α × β)), ↑↑c z * f z