Recovering a transport map from Dirac conditional laws #
If the conditional laws of the second coordinate of a finite coupling are Dirac for almost every source point, the coupling is the graph plan of a measurable map with the prescribed target law. This turns almost-everywhere singleton conditional transport fibers into a Monge map.
References #
- C. Villani, Optimal Transport: Old and New, Chapter 10, for the passage from Dirac conditional laws of a transport plan to a Monge map.
theorem
TauCeti.IsCoupling.exists_graphPlan_of_ae_exists_condKernel_eq_dirac
{X : Type u}
{Y : Type v}
[MeasurableSpace X]
[MeasurableSpace Y]
[StandardBorelSpace Y]
[Nonempty Y]
{π : MeasureTheory.Measure (X × Y)}
{μ : MeasureTheory.Measure X}
{ν : MeasureTheory.Measure Y}
[MeasureTheory.IsFiniteMeasure π]
(hπ : IsCoupling π μ ν)
(hκ : ∀ᵐ (x : X) ∂μ, ∃ (y : Y), π.condKernel x = MeasureTheory.Measure.dirac y)
:
∃ (T : X → Y), Measurable T ∧ ProbabilityTheory.HasLaw T ν μ ∧ π = graphPlan T μ
A finite coupling with almost everywhere Dirac conditional laws is induced by a measurable transport map.