Finite multi-marginal couplings

For finitely many finite spaces, a multi-marginal transport plan can be represented by a probability mass function on the dependent product whose coordinate pushforwards are prescribed. This file packages that finite model, its independent product coupling, its real-valued cost, and the bridge to the measure-theoretic TauCeti.MultiCoupling API.

These definitions supply the finite coupling infrastructure used by the multi-marginal duality development in Layer 2, item 6 of the optimal-transport roadmap.

@[reducible, inline]

abbrev TauCeti.FiniteMultiCoupling {ι : Type u} {X : ι → Type v} (μ : (i : ι) → PMF (X i)) : Type (max 0 u v)

A finite multi-marginal coupling is a probability mass function on the dependent product whose pushforward by each coordinate evaluation is the prescribed marginal.

theorem TauCeti.FiniteMultiCoupling.ext {ι : Type u} {X : ι → Type v} {μ : (i : ι) → PMF (X i)} {π σ : FiniteMultiCoupling μ} (h : ∀ (x : (i : ι) → X i), ↑π x = ↑σ x) : π = σ

Two finite multi-marginal couplings are equal when their point masses agree.

theorem TauCeti.FiniteMultiCoupling.ext_iff {ι : Type u} {X : ι → Type v} {μ : (i : ι) → PMF (X i)} {π σ : FiniteMultiCoupling μ} : π = σ ↔ ∀ (x : (i : ι) → X i), ↑π x = ↑σ x

@[simp]

theorem TauCeti.FiniteMultiCoupling.map_eval {ι : Type u} {X : ι → Type v} {μ : (i : ι) → PMF (X i)} (π : FiniteMultiCoupling μ) (i : ι) : PMF.map (Function.eval i) ↑π = μ i

The marginal condition, in its canonical pushforward form.

theorem TauCeti.FiniteMultiCoupling.isMultiCoupling_toMeasure {ι : Type u} {X : ι → Type v} {μ : (i : ι) → PMF (X i)} [(i : ι) → MeasurableSpace (X i)] (π : FiniteMultiCoupling μ) : Measure.IsMultiCoupling (↑π).toMeasure fun (i : ι) => (μ i).toMeasure

The measure of a finite multi-marginal coupling is a measure-theoretic multi-coupling of the measures associated to its marginals.

noncomputable def TauCeti.FiniteMultiCoupling.toMultiCoupling {ι : Type u} {X : ι → Type v} {μ : (i : ι) → PMF (X i)} [(i : ι) → MeasurableSpace (X i)] (π : FiniteMultiCoupling μ) : MultiCoupling fun (i : ι) => ⟨(μ i).toMeasure, ⋯⟩

A finite multi-marginal coupling, regarded as the bundled measure-theoretic coupling of the probability measures associated to its marginals.

@[simp]

theorem TauCeti.FiniteMultiCoupling.coe_toMultiCoupling {ι : Type u} {X : ι → Type v} {μ : (i : ι) → PMF (X i)} [(i : ι) → MeasurableSpace (X i)] (π : FiniteMultiCoupling μ) : ↑↑π.toMultiCoupling = (↑π).toMeasure

The measure underlying the bundled coupling associated to a finite coupling is the measure of its probability mass function.

noncomputable def TauCeti.FiniteMultiCoupling.independent {ι : Type u} {X : ι → Type v} [Fintype ι] [(i : ι) → Fintype (X i)] (μ : (i : ι) → PMF (X i)) : FiniteMultiCoupling μ

The independent finite multi-marginal coupling.

@[simp]

theorem TauCeti.FiniteMultiCoupling.independent_apply {ι : Type u} {X : ι → Type v} [Fintype ι] [(i : ι) → Fintype (X i)] (μ : (i : ι) → PMF (X i)) (x : (i : ι) → X i) : ↑(independent μ) x = ∏ i : ι, (μ i) (x i)

The point mass of the independent coupling is the product of its marginal point masses.

instance TauCeti.FiniteMultiCoupling.instNonempty {ι : Type u} {X : ι → Type v} {μ : (i : ι) → PMF (X i)} [Finite ι] [∀ (i : ι), Finite (X i)] : Nonempty (FiniteMultiCoupling μ)

Every finite family of probability mass functions has a finite multi-marginal coupling.

def TauCeti.FiniteMultiCoupling.cost {ι : Type u} {X : ι → Type v} {μ : (i : ι) → PMF (X i)} [Fintype ((i : ι) → X i)] (c : ((i : ι) → X i) → ℝ) (π : FiniteMultiCoupling μ) : ℝ

The real cost of a finite multi-marginal coupling.

theorem TauCeti.FiniteMultiCoupling.cost_def {ι : Type u} {X : ι → Type v} {μ : (i : ι) → PMF (X i)} [Fintype ((i : ι) → X i)] (c : ((i : ι) → X i) → ℝ) (π : FiniteMultiCoupling μ) : cost c π = ∑ x : (i : ι) → X i, c x * (↑π x).toReal

The defining finite-sum formula for the cost of a multi-marginal coupling.

@[simp]

theorem TauCeti.FiniteMultiCoupling.cost_add_const {ι : Type u} {X : ι → Type v} {μ : (i : ι) → PMF (X i)} [Fintype ((i : ι) → X i)] (c : ((i : ι) → X i) → ℝ) (π : FiniteMultiCoupling μ) (a : ℝ) : cost (fun (x : (i : ι) → X i) => c x + a) π = cost c π + a

Adding a constant to the cost adds that constant to every plan's cost.

theorem TauCeti.FiniteMultiCoupling.cost_eq_integral {ι : Type u} {X : ι → Type v} {μ : (i : ι) → PMF (X i)} [Fintype ((i : ι) → X i)] [(i : ι) → MeasurableSpace (X i)] [MeasurableSingletonClass ((i : ι) → X i)] (π : FiniteMultiCoupling μ) (c : ((i : ι) → X i) → ℝ) : cost c π = ∫ (x : (i : ι) → X i), c x ∂(↑π).toMeasure

The finite-sum cost is the integral of the cost against the measure associated to the coupling.