Multi-marginal couplings

This file defines a multi-marginal coupling as a probability measure on a dependent product with prescribed one-coordinate marginals. It provides coordinate and pair projections, coordinatewise maps, reindexing, and, over a finite index type, the independent product coupling.

These constructions form the finite multi-marginal part of Layer 0 of the optimal-transport roadmap. The definitions allow heterogeneous coordinate spaces; repeated-coordinate projections are also allowed, which is useful for forming diagonal marginals. Finiteness of the index type is assumed only where the independent product measure is involved, since the marginal, projection, reindexing and coordinatewise-map API needs nothing beyond measurable pushforwards.

structure TauCeti.Measure.IsMultiCoupling {ι : Type u} {X : ι → Type v} [(i : ι) → MeasurableSpace (X i)] (π : MeasureTheory.Measure ((i : ι) → X i)) (μ : (i : ι) → MeasureTheory.Measure (X i)) : Prop

A measure on a dependent product is a multi-marginal coupling of μ when its pushforward by every coordinate evaluation is the corresponding measure μ i.

• marginal_eq (i : ι) : MeasureTheory.Measure.map (Function.eval i) π = μ i

theorem TauCeti.Measure.IsMultiCoupling.project {ι : Type u} {X : ι → Type v} [(i : ι) → MeasurableSpace (X i)] {π : MeasureTheory.Measure ((i : ι) → X i)} {μ : (i : ι) → MeasureTheory.Measure (X i)} {κ : Type w} (hπ : IsMultiCoupling π μ) (e : κ → ι) : IsMultiCoupling (MeasureTheory.Measure.map (fun (x : (i : ι) → X i) (j : κ) => x (e j)) π) fun (j : κ) => μ (e j)

Projecting a multi-marginal coupling along a family of coordinates gives another multi-marginal coupling. The coordinate family need not be injective.

theorem TauCeti.Measure.IsMultiCoupling.map {ι : Type u} {X : ι → Type v} [(i : ι) → MeasurableSpace (X i)] {π : MeasureTheory.Measure ((i : ι) → X i)} {μ : (i : ι) → MeasureTheory.Measure (X i)} {Y : ι → Type w} [(i : ι) → MeasurableSpace (Y i)] (hπ : IsMultiCoupling π μ) (f : (i : ι) → X i → Y i) (hf : ∀ (i : ι), Measurable (f i)) : IsMultiCoupling (MeasureTheory.Measure.map (fun (x : (i : ι) → X i) (i : ι) => f i (x i)) π) fun (i : ι) => MeasureTheory.Measure.map (f i) (μ i)

Applying measurable maps coordinatewise to a multi-marginal coupling pushes each marginal forward by the corresponding map.

theorem TauCeti.Measure.IsMultiCoupling.fst_map_pair {ι : Type u} {X : ι → Type v} [(i : ι) → MeasurableSpace (X i)] {π : MeasureTheory.Measure ((i : ι) → X i)} {μ : (i : ι) → MeasureTheory.Measure (X i)} (hπ : IsMultiCoupling π μ) (i j : ι) : (MeasureTheory.Measure.map (fun (x : (i : ι) → X i) => (x i, x j)) π).fst = μ i

The pair projection of a multi-marginal coupling has the prescribed first marginal.

theorem TauCeti.Measure.IsMultiCoupling.snd_map_pair {ι : Type u} {X : ι → Type v} [(i : ι) → MeasurableSpace (X i)] {π : MeasureTheory.Measure ((i : ι) → X i)} {μ : (i : ι) → MeasureTheory.Measure (X i)} (hπ : IsMultiCoupling π μ) (i j : ι) : (MeasureTheory.Measure.map (fun (x : (i : ι) → X i) => (x i, x j)) π).snd = μ j

The pair projection of a multi-marginal coupling has the prescribed second marginal.

@[simp]

theorem TauCeti.Measure.isMultiCoupling_pi {ι : Type u} {X : ι → Type v} [(i : ι) → MeasurableSpace (X i)] [Fintype ι] (μ : (i : ι) → MeasureTheory.Measure (X i)) [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] : IsMultiCoupling (MeasureTheory.Measure.pi μ) μ

The finite product of probability measures is a multi-marginal coupling of its factors.

@[reducible, inline]

abbrev TauCeti.MultiCoupling {ι : Type u} {X : ι → Type v} [(i : ι) → MeasurableSpace (X i)] (μ : (i : ι) → MeasureTheory.ProbabilityMeasure (X i)) : Type (max u v)

Probability measures on a dependent product with prescribed coordinate marginals. The index type carries no finiteness assumption: it is MultiCoupling.pi and MultiCoupling.instNonempty, not the bundle itself, that need ι to be finite.

Equations

• TauCeti.MultiCoupling μ = { π : MeasureTheory.ProbabilityMeasure ((i : ι) → X i) // TauCeti.Measure.IsMultiCoupling ↑π fun (i : ι) => ↑(μ i) }

noncomputable def TauCeti.MultiCoupling.pi {ι : Type u} {X : ι → Type v} [(i : ι) → MeasurableSpace (X i)] [Fintype ι] (μ : (i : ι) → MeasureTheory.ProbabilityMeasure (X i)) : MultiCoupling μ

The independent product probability measure, regarded as a multi-marginal coupling.

Equations

• TauCeti.MultiCoupling.pi μ = ⟨MeasureTheory.ProbabilityMeasure.pi μ, ⋯⟩

instance TauCeti.MultiCoupling.instNonempty {ι : Type u} {X : ι → Type v} [(i : ι) → MeasurableSpace (X i)] {μ : (i : ι) → MeasureTheory.ProbabilityMeasure (X i)} [Finite ι] : Nonempty (MultiCoupling μ)

Every family of probability measures indexed by a finite type has a multi-marginal coupling.

@[simp]

theorem TauCeti.MultiCoupling.coe_pi {ι : Type u} {X : ι → Type v} [(i : ι) → MeasurableSpace (X i)] [Fintype ι] (μ : (i : ι) → MeasureTheory.ProbabilityMeasure (X i)) : ↑(pi μ) = MeasureTheory.ProbabilityMeasure.pi μ

The underlying probability measure of the independent multi-coupling is the product probability measure.

noncomputable def TauCeti.MultiCoupling.marginal {ι : Type u} {X : ι → Type v} [(i : ι) → MeasurableSpace (X i)] {μ : (i : ι) → MeasureTheory.ProbabilityMeasure (X i)} (π : MultiCoupling μ) (i : ι) : MeasureTheory.ProbabilityMeasure (X i)

The ith marginal of a bundled multi-marginal coupling.

Equations

• π.marginal i = (↑π).map fun (x : (i : ι) → X i) => x i

theorem TauCeti.MultiCoupling.coe_marginal {ι : Type u} {X : ι → Type v} [(i : ι) → MeasurableSpace (X i)] {μ : (i : ι) → MeasureTheory.ProbabilityMeasure (X i)} (π : MultiCoupling μ) (i : ι) : ↑(π.marginal i) = MeasureTheory.Measure.map (Function.eval i) ↑↑π

The underlying measure of a coordinate marginal is the corresponding pushforward. This is not a simp lemma: simp rewrites π.marginal i to μ i via marginal_eq instead.

@[simp]

theorem TauCeti.MultiCoupling.marginal_eq {ι : Type u} {X : ι → Type v} [(i : ι) → MeasurableSpace (X i)] {μ : (i : ι) → MeasureTheory.ProbabilityMeasure (X i)} (π : MultiCoupling μ) (i : ι) : π.marginal i = μ i

Every coordinate marginal of a bundled multi-marginal coupling is its prescribed endpoint.

theorem TauCeti.MultiCoupling.ext {ι : Type u} {X : ι → Type v} [(i : ι) → MeasurableSpace (X i)] {μ : (i : ι) → MeasureTheory.ProbabilityMeasure (X i)} {π κ : MultiCoupling μ} (h : ↑↑π = ↑↑κ) : π = κ

Two bundled multi-marginal couplings are equal when their underlying measures are equal.

theorem TauCeti.MultiCoupling.ext_iff {ι : Type u} {X : ι → Type v} [(i : ι) → MeasurableSpace (X i)] {μ : (i : ι) → MeasureTheory.ProbabilityMeasure (X i)} {π κ : MultiCoupling μ} : π = κ ↔ ↑↑π = ↑↑κ

noncomputable def TauCeti.MultiCoupling.project {ι : Type u} {X : ι → Type v} [(i : ι) → MeasurableSpace (X i)] {μ : (i : ι) → MeasureTheory.ProbabilityMeasure (X i)} {κ : Type w} (π : MultiCoupling μ) (e : κ → ι) : MultiCoupling fun (j : κ) => μ (e j)

Project a coupling to a family of coordinates. The coordinate family need not be injective.

Equations

• π.project e = ⟨(↑π).map fun (x : (i : ι) → X i) (j : κ) => x (e j), ⋯⟩

@[simp]

theorem TauCeti.MultiCoupling.coe_project {ι : Type u} {X : ι → Type v} [(i : ι) → MeasurableSpace (X i)] {μ : (i : ι) → MeasureTheory.ProbabilityMeasure (X i)} {κ : Type w} (π : MultiCoupling μ) (e : κ → ι) : ↑(π.project e) = (↑π).map fun (x : (i : ι) → X i) (j : κ) => x (e j)

The underlying probability measure of a coordinate projection is the corresponding pushforward.

@[simp]

theorem TauCeti.MultiCoupling.project_id {ι : Type u} {X : ι → Type v} [(i : ι) → MeasurableSpace (X i)] {μ : (i : ι) → MeasureTheory.ProbabilityMeasure (X i)} (π : MultiCoupling μ) : π.project id = π

Projecting along the identity coordinate family leaves a multi-marginal coupling unchanged.

@[simp]

theorem TauCeti.MultiCoupling.project_comp {ι : Type u} {X : ι → Type v} [(i : ι) → MeasurableSpace (X i)] {μ : (i : ι) → MeasureTheory.ProbabilityMeasure (X i)} {κ : Type w} {τ : Type u_1} (π : MultiCoupling μ) (e : κ → ι) (d : τ → κ) : (π.project e).project d = π.project (e ∘ d)

Projecting successively agrees with projecting along the composite coordinate family.

noncomputable def TauCeti.MultiCoupling.reindex {ι : Type u} {X : ι → Type v} [(i : ι) → MeasurableSpace (X i)] {μ : (i : ι) → MeasureTheory.ProbabilityMeasure (X i)} {κ : Type w} (π : MultiCoupling μ) (e : κ ≃ ι) : MultiCoupling fun (j : κ) => μ (e j)

Reindex a multi-marginal coupling along an equivalence of index types.

Equations

• π.reindex e = π.project ⇑e

@[simp]

theorem TauCeti.MultiCoupling.coe_reindex {ι : Type u} {X : ι → Type v} [(i : ι) → MeasurableSpace (X i)] {μ : (i : ι) → MeasureTheory.ProbabilityMeasure (X i)} {κ : Type w} (π : MultiCoupling μ) (e : κ ≃ ι) : ↑(π.reindex e) = (↑π).map fun (x : (i : ι) → X i) (j : κ) => x (e j)

Reindexing is the pushforward by precomposition with the index equivalence.

@[simp]

theorem TauCeti.MultiCoupling.reindex_refl {ι : Type u} {X : ι → Type v} [(i : ι) → MeasurableSpace (X i)] {μ : (i : ι) → MeasureTheory.ProbabilityMeasure (X i)} (π : MultiCoupling μ) : π.reindex (Equiv.refl ι) = π

Reindexing by the identity equivalence leaves a multi-marginal coupling unchanged.

@[simp]

theorem TauCeti.MultiCoupling.reindex_trans {ι : Type u} {X : ι → Type v} [(i : ι) → MeasurableSpace (X i)] {μ : (i : ι) → MeasureTheory.ProbabilityMeasure (X i)} {κ : Type w} {τ : Type u_1} (π : MultiCoupling μ) (e : κ ≃ ι) (d : τ ≃ κ) : (π.reindex e).reindex d = π.reindex (d.trans e)

Reindexing successively agrees with reindexing by the composite equivalence.

noncomputable def TauCeti.MultiCoupling.map {ι : Type u} {X : ι → Type v} [(i : ι) → MeasurableSpace (X i)] {μ : (i : ι) → MeasureTheory.ProbabilityMeasure (X i)} {Y : ι → Type w} [(i : ι) → MeasurableSpace (Y i)] (π : MultiCoupling μ) (f : (i : ι) → X i → Y i) (hf : ∀ (i : ι), Measurable (f i)) : MultiCoupling fun (i : ι) => (μ i).map (f i)

Applying measurable maps coordinatewise to a multi-marginal coupling.

Equations

• π.map f hf = ⟨(↑π).map fun (x : (i : ι) → X i) (i : ι) => f i (x i), ⋯⟩

@[simp]

theorem TauCeti.MultiCoupling.coe_map {ι : Type u} {X : ι → Type v} [(i : ι) → MeasurableSpace (X i)] {μ : (i : ι) → MeasureTheory.ProbabilityMeasure (X i)} {Y : ι → Type w} [(i : ι) → MeasurableSpace (Y i)] (π : MultiCoupling μ) (f : (i : ι) → X i → Y i) (hf : ∀ (i : ι), Measurable (f i)) : ↑(π.map f hf) = (↑π).map fun (x : (i : ι) → X i) (i : ι) => f i (x i)

The underlying probability measure of a coordinatewise map is the corresponding pushforward.

theorem TauCeti.MultiCoupling.coe_map_id {ι : Type u} {X : ι → Type v} [(i : ι) → MeasurableSpace (X i)] {μ : (i : ι) → MeasureTheory.ProbabilityMeasure (X i)} (π : MultiCoupling μ) : ↑(π.map (fun (x : ι) => id) ⋯) = ↑π

Mapping every coordinate by the identity leaves the underlying probability measure unchanged. This is not a simp lemma: simp unfolds the left-hand side through coe_map.

@[simp]

theorem TauCeti.MultiCoupling.map_pi {ι : Type u} {X : ι → Type v} [(i : ι) → MeasurableSpace (X i)] [Fintype ι] {Y : ι → Type w} [(i : ι) → MeasurableSpace (Y i)] (μ : (i : ι) → MeasureTheory.ProbabilityMeasure (X i)) (f : (i : ι) → X i → Y i) (hf : ∀ (i : ι), Measurable (f i)) : (pi μ).map f hf = pi fun (i : ι) => (μ i).map (f i)

Coordinatewise mapping preserves the independent product coupling.

noncomputable def TauCeti.MultiCoupling.projectPair {ι : Type u} {X : ι → Type v} [(i : ι) → MeasurableSpace (X i)] {μ : (i : ι) → MeasureTheory.ProbabilityMeasure (X i)} (π : MultiCoupling μ) (i j : ι) : MeasureTheory.ProbabilityMeasure (X i × X j)

The joint law of coordinates i and j of a multi-marginal coupling.

Equations

• π.projectPair i j = (↑π).map fun (x : (i : ι) → X i) => (x i, x j)

theorem TauCeti.MultiCoupling.coe_projectPair {ι : Type u} {X : ι → Type v} [(i : ι) → MeasurableSpace (X i)] {μ : (i : ι) → MeasureTheory.ProbabilityMeasure (X i)} (π : MultiCoupling μ) (i j : ι) : ↑(π.projectPair i j) = MeasureTheory.Measure.map (fun (x : (i : ι) → X i) => (x i, x j)) ↑↑π

The underlying measure of a pair projection is the corresponding pushforward. This is not a simp lemma: simp rewrites the marginals of a pair projection through fst_projectPair and snd_projectPair instead.

@[simp]

theorem TauCeti.MultiCoupling.fst_projectPair {ι : Type u} {X : ι → Type v} [(i : ι) → MeasurableSpace (X i)] {μ : (i : ι) → MeasureTheory.ProbabilityMeasure (X i)} (π : MultiCoupling μ) (i j : ι) : (↑(π.projectPair i j)).fst = ↑(μ i)

The first marginal of a pair projection is its first selected coordinate.

@[simp]

theorem TauCeti.MultiCoupling.snd_projectPair {ι : Type u} {X : ι → Type v} [(i : ι) → MeasurableSpace (X i)] {μ : (i : ι) → MeasureTheory.ProbabilityMeasure (X i)} (π : MultiCoupling μ) (i j : ι) : (↑(π.projectPair i j)).snd = ↑(μ j)

The second marginal of a pair projection is its second selected coordinate.

@[simp]

theorem TauCeti.MultiCoupling.projectPair_self {ι : Type u} {X : ι → Type v} [(i : ι) → MeasurableSpace (X i)] {μ : (i : ι) → MeasureTheory.ProbabilityMeasure (X i)} (π : MultiCoupling μ) (i : ι) : π.projectPair i i = (μ i).map fun (x : X i) => (x, x)

Selecting the same coordinate twice gives its diagonal law.