Disintegrating transport plans #
A coupling can be read in two equivalent ways: as a measure on a product with prescribed marginals, or as a source measure followed by a probability kernel whose averaged law is the target. This file connects the coupling API to Mathlib's composition-product and regular conditional-kernel APIs.
For a Markov kernel κ : Kernel X Y, the composition-product μ ⊗ₘ κ couples μ to the
averaged law κ ∘ₘ μ. Conversely, when the target space is standard Borel, a finite coupling
π reconstructs as μ ⊗ₘ π.condKernel, and its conditional kernel averages to the prescribed
target. Any other finite kernel reconstructing the same plan agrees with π.condKernel
μ-almost everywhere.
When the plan is concentrated on a set that meets almost every vertical line in at most one point, the conditional kernel is almost everywhere a Dirac mass, so the plan is determined by its source marginal and that set; this is the form in which uniqueness of contact partners becomes uniqueness of optimal plans.
Main statements #
TauCeti.isCoupling_compProdconstructs a coupling from a source measure and a Markov kernel;TauCeti.isCoupling_compProd_iffcharacterizes when that coupling has a specified target;TauCeti.IsCoupling.compProd_condKernelreconstructs a finite coupling from its source marginal and Mathlib's conditional kernel;TauCeti.IsCoupling.condKernel_compidentifies the averaged conditional law with the target marginal;TauCeti.IsCoupling.ae_eq_condKernel_iff_compProd_eqgives the coupling-facing uniqueness criterion for conditional kernels;TauCeti.IsCoupling.compProd_condDistribandTauCeti.IsCoupling.condDistrib_ae_eq_condKernelgive the same reconstruction through the conditional distribution of the two coordinate maps and identify the two Mathlib interfaces;TauCeti.IsCoupling.ae_exists_condKernel_eq_diracandTauCeti.IsCoupling.eq_of_ae_mem_of_subsingleton— a coupling concentrated on a set with almost all sections subsingletons has Dirac conditional laws, and is determined by its source marginal and that set;- the corresponding declarations in
TauCeti.Couplingspecialize these results to the bundled probability-coupling type.
This is Layer 0, item 3 of the optimal-transport roadmap. The construction and uniqueness theorem
consume Mathlib's MeasureTheory.Measure.disintegrate and
ProbabilityTheory.eq_condKernel_of_measure_eq_compProd; no disintegration is rebuilt here.
References #
- C. Villani, Optimal Transport: Old and New, Grundlehren 338, 2009, Chapter 5, especially Theorem 5.3 (disintegration of measures). The presentation here uses Mathlib's regular conditional kernels on a standard Borel target.
The composition-product of a measure and a Markov kernel couples the measure to the law obtained by averaging the kernel against it. This is the unbundled reconstruction of a joint law from a marginal and a conditional probability kernel.
A composition-product has prescribed marginals μ and ν exactly when averaging its Markov
kernel against μ gives ν.
A finite coupling is reconstructed by composing its source marginal with Mathlib's regular conditional kernel of the second coordinate given the first.
Averaging the conditional kernel of a finite coupling against its source marginal gives its target marginal.
A finite kernel agrees almost everywhere with the regular conditional kernel of a finite coupling exactly when its composition-product with the source marginal reconstructs that coupling. This is the coupling-facing uniqueness theorem for disintegration.
The conditional distribution of the second coordinate given the first reconstructs a finite
coupling from its source marginal. This is the coordinate-map form of
TauCeti.IsCoupling.compProd_condKernel.
The conditional distribution of the second coordinate given the first averages against the source marginal to the target marginal.
For a finite coupling, the conditional distribution of the second coordinate given the first is almost everywhere the same kernel as Mathlib's regular conditional kernel of the joint measure.
A finite coupling concentrated on a set whose sections {y | (x, y) ∈ s} are
μ-almost all subsingletons is deterministic: for μ-almost every x, its conditional kernel
at x is the Dirac mass at the unique point of the section. No measurability of s is
needed.
Two finite couplings with the same source marginal, concentrated on a common set whose
sections are μ-almost all subsingletons, are equal. In particular their target marginals
agree.
The underlying measure of a bundled probability coupling is reconstructed from its source law and regular conditional kernel.
The regular conditional kernel of a bundled probability coupling averages to its prescribed target law.
A finite kernel is a version of the regular conditional kernel of a bundled probability coupling exactly when it reconstructs the coupling from its source law.
The coordinate conditional distribution of a bundled probability coupling reconstructs its underlying joint law.
The coordinate conditional distribution of a bundled probability coupling averages to its target law.
The coordinate conditional distribution and regular conditional kernel of a bundled probability coupling agree almost everywhere under its source law.
A bundled coupling concentrated on a set with almost everywhere subsingleton sections has Dirac conditional laws at points of those sections.
Bundled couplings with the same source and almost everywhere the same uniquely determined partner in a set have equal underlying plan measures.