Couplings of two measures

A coupling, or transport plan, of a measure μ on X and a measure ν on Y is a measure π on X × Y whose two marginals are μ and ν. It is the primitive object of optimal transport: the primal transport problem minimises a cost over the couplings of two fixed measures, so every statement about that problem is a statement about the set defined here.

Nothing in this file needs a topology, a metric, a density, or a normalisation, and the two factors may be different measurable spaces. The relation is therefore stated for arbitrary measures, and the probability case is packaged separately as a subtype of MeasureTheory.ProbabilityMeasure (X × Y).

Main definitions

• TauCeti.IsCoupling π μ ν — the plan-first coupling relation: π.fst = μ and π.snd = ν;
• TauCeti.Coupling μ ν — couplings of two probability measures, bundled as a subtype of MeasureTheory.ProbabilityMeasure (X × Y);
• TauCeti.Coupling.prod — the independent coupling, and with it TauCeti.Coupling.instNonempty.

Main statements

• TauCeti.IsCoupling.measure_prod_univ and TauCeti.IsCoupling.measure_univ_prod — the marginal formulas on measurable cylinders, with the converse TauCeti.isCoupling_of_measure_prod_univ_of_measure_univ_prod;
• TauCeti.IsCoupling.measurePreserving_fst, TauCeti.IsCoupling.measurePreserving_snd, TauCeti.IsCoupling.integral_comp_fst, and TauCeti.IsCoupling.integral_comp_snd — projection and integral-transfer forms of the marginal conditions;
• TauCeti.IsCoupling.smul, TauCeti.IsCoupling.add, TauCeti.IsCoupling.sum and TauCeti.isCoupling_zero — the relation is compatible with the additive and scalar structure of measures, which is what mixtures of transport problems use;
• TauCeti.IsCoupling.sub_add — replacing a finite part of a coupling by a measure with the same two marginals keeps the coupling property, which is how a plan is perturbed locally;
• TauCeti.IsCoupling.prodProdProdComm — exchanging the two middle coordinates of a product of two couplings couples the two product measures;
• TauCeti.IsCoupling.map_prod — a coupling run alongside an independent sample, with measurable maps applied to both coordinates, couples the two pushed-forward products;
• TauCeti.exists_isCoupling_iff — a finite measure and any other measure admit a coupling exactly when they have the same total mass, the witness being their normalised product;
• TauCeti.isCoupling_sum_map_pi — pairing the source of each of finitely many independent samples with the target of a permuted one preserves both total marginals;
• TauCeti.isCoupling_map_swap_iff and TauCeti.isCoupling_map_prodMap_iff — invariance of the relation under the coordinate swap and under measurable equivalences of the two factors;
• TauCeti.isCoupling_toMeasure_iff — the coupling condition on bundled probability measures, as the pair of equations for the two marginal pushforwards;
• TauCeti.IsCoupling.eq_map_prodMk — a coupling out of a Dirac measure is the pushforward of its target along y ↦ (x, y), so it is unique; IsCoupling.eq_dirac specialises this to a pair of Dirac measures.

Implementation notes

The argument order IsCoupling π μ ν takes the plan first, so that a hypothesis hπ : IsCoupling π μ ν supports dot notation such as hπ.swap and hπ.map. This convention, and the choice to state the relation for raw measures rather than only for bundled probability measures, follow Joseph K. Miller's Apache-2.0 Vlasov.IsCoupling (https://github.com/Hydrodynamical/Vlasov_Meanfield_Formalization), the closest existing Lean development of the same relation; no code is taken from it. The bundled subtype mirrors TauCeti.MultiCoupling, the multi-marginal analogue already in this repository.

The declarations sit in the bare TauCeti namespace rather than in TauCeti.Measure: scripts/lint-dot-notation.py rejects a new declaration under TauCeti.<Mathlib type namespace> that takes an explicit argument of that type, because π.IsCoupling μ ν would not elaborate there anyway. Dot notation on hπ works under either namespace; the bare namespace is forced by the lint rule and matches TauCeti.MultiCoupling.

This is Layer 0, item 1 of the optimal-transport roadmap.

References

• TauCeti/MeasureTheory/Measure/Coupling/Basic.lean is the formal source for the measure-preserving projection and integral-transfer declarations and proofs adapted here to the plan-first TauCeti.IsCoupling interface.
• C. Villani, Optimal Transport: Old and New, Grundlehren 338, 2009, Chapter 1 ("Couplings and changes of variables"), Definition 1.1, which is this relation for two probability measures. TauCeti.IsCoupling states it for arbitrary measures, so the probability case is the bundled TauCeti.Coupling.

structure TauCeti.IsCoupling {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] (π : MeasureTheory.Measure (X × Y)) (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) : Prop

IsCoupling π μ ν says that the measure π on X × Y is a coupling, or transport plan, of μ and ν: its first marginal is μ and its second marginal is ν.

• fst_eq : π.fst = μ

  The first marginal of a coupling is the prescribed source measure.

• snd_eq : π.snd = ν

  The second marginal of a coupling is the prescribed target measure.

theorem TauCeti.IsCoupling.measurePreserving_fst {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {π : MeasureTheory.Measure (X × Y)} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} (hπ : IsCoupling π μ ν) : MeasureTheory.MeasurePreserving Prod.fst π μ

The first projection out of a coupling is measure preserving.

theorem TauCeti.IsCoupling.measurePreserving_snd {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {π : MeasureTheory.Measure (X × Y)} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} (hπ : IsCoupling π μ ν) : MeasureTheory.MeasurePreserving Prod.snd π ν

The second projection out of a coupling is measure preserving.

theorem TauCeti.IsCoupling.integrable_comp_fst {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {π : MeasureTheory.Measure (X × Y)} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {ε : Type u_2} [TopologicalSpace ε] [ContinuousENorm ε] (hπ : IsCoupling π μ ν) {f : X → ε} (hf : MeasureTheory.Integrable f μ) : MeasureTheory.Integrable (fun (p : X × Y) => f p.1) π

An integrable function of the first marginal remains integrable after composition with the first projection from a coupling.

theorem TauCeti.IsCoupling.integrable_comp_snd {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {π : MeasureTheory.Measure (X × Y)} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {ε : Type u_2} [TopologicalSpace ε] [ContinuousENorm ε] (hπ : IsCoupling π μ ν) {f : Y → ε} (hf : MeasureTheory.Integrable f ν) : MeasureTheory.Integrable (fun (p : X × Y) => f p.2) π

An integrable function of the second marginal remains integrable after composition with the second projection from a coupling.

theorem TauCeti.IsCoupling.integrable_add_split {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {π : MeasureTheory.Measure (X × Y)} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {ε : Type u_2} [TopologicalSpace ε] [ESeminormedAddMonoid ε] [ContinuousAdd ε] (hπ : IsCoupling π μ ν) {f : X → ε} {g : Y → ε} (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g ν) : MeasureTheory.Integrable (fun (p : X × Y) => f p.1 + g p.2) π

The sum of two integrable marginal functions is integrable against every coupling.

theorem TauCeti.IsCoupling.integral_comp_fst {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {π : MeasureTheory.Measure (X × Y)} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (hπ : IsCoupling π μ ν) {f : X → E} (hf : MeasureTheory.AEStronglyMeasurable f μ) : ∫ (p : X × Y), f p.1 ∂π = ∫ (x : X), f x ∂μ

A function of the first coordinate integrates against a coupling as it does against the first marginal.

theorem TauCeti.IsCoupling.integral_comp_snd {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {π : MeasureTheory.Measure (X × Y)} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (hπ : IsCoupling π μ ν) {f : Y → E} (hf : MeasureTheory.AEStronglyMeasurable f ν) : ∫ (p : X × Y), f p.2 ∂π = ∫ (y : Y), f y ∂ν

A function of the second coordinate integrates against a coupling as it does against the second marginal.

theorem TauCeti.IsCoupling.measure_prod_univ {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {π : MeasureTheory.Measure (X × Y)} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} (hπ : IsCoupling π μ ν) {s : Set X} (hs : MeasurableSet s) : π (s ×ˢ Set.univ) = μ s

A coupling gives the measurable cylinder s ×ˢ univ the source mass of s.

theorem TauCeti.IsCoupling.measure_univ_prod {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {π : MeasureTheory.Measure (X × Y)} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} (hπ : IsCoupling π μ ν) {t : Set Y} (ht : MeasurableSet t) : π (Set.univ ×ˢ t) = ν t

A coupling gives the measurable cylinder univ ×ˢ t the target mass of t.

theorem TauCeti.IsCoupling.measure_univ_left {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {π : MeasureTheory.Measure (X × Y)} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} (hπ : IsCoupling π μ ν) : μ Set.univ = π Set.univ

The source measure of a coupling has the total mass of the coupling.

theorem TauCeti.IsCoupling.measure_univ_right {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {π : MeasureTheory.Measure (X × Y)} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} (hπ : IsCoupling π μ ν) : ν Set.univ = π Set.univ

The target measure of a coupling has the total mass of the coupling.

theorem TauCeti.IsCoupling.measure_univ_eq {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {π : MeasureTheory.Measure (X × Y)} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} (hπ : IsCoupling π μ ν) : μ Set.univ = ν Set.univ

Coupled measures have equal total mass. Measures of different total mass are therefore not coupled by anything.

theorem TauCeti.IsCoupling.isFiniteMeasure {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {π : MeasureTheory.Measure (X × Y)} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [MeasureTheory.IsFiniteMeasure μ] (hπ : IsCoupling π μ ν) : MeasureTheory.IsFiniteMeasure π

A coupling of a finite measure is finite.

theorem TauCeti.IsCoupling.isProbabilityMeasure {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {π : MeasureTheory.Measure (X × Y)} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [MeasureTheory.IsProbabilityMeasure μ] (hπ : IsCoupling π μ ν) : MeasureTheory.IsProbabilityMeasure π

A coupling of a probability measure is a probability measure.

theorem TauCeti.IsCoupling.isFiniteMeasure_of_right {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {π : MeasureTheory.Measure (X × Y)} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [MeasureTheory.IsFiniteMeasure ν] (hπ : IsCoupling π μ ν) : MeasureTheory.IsFiniteMeasure π

A coupling with a finite target measure is finite.

theorem TauCeti.IsCoupling.isProbabilityMeasure_of_right {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {π : MeasureTheory.Measure (X × Y)} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [MeasureTheory.IsProbabilityMeasure ν] (hπ : IsCoupling π μ ν) : MeasureTheory.IsProbabilityMeasure π

A coupling with a probability target measure is a probability measure.

theorem TauCeti.IsCoupling.isProbabilityMeasure_right {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {π : MeasureTheory.Measure (X × Y)} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [MeasureTheory.IsProbabilityMeasure μ] (hπ : IsCoupling π μ ν) : MeasureTheory.IsProbabilityMeasure ν

The target of a coupling of a probability measure is a probability measure.

theorem TauCeti.IsCoupling.swap {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {π : MeasureTheory.Measure (X × Y)} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} (hπ : IsCoupling π μ ν) : IsCoupling (MeasureTheory.Measure.map Prod.swap π) ν μ

Exchanging the two coordinates of a coupling of μ and ν gives a coupling of ν and μ.

theorem TauCeti.IsCoupling.map {X : Type u} {Y : Type v} {X' : Type w} {Y' : Type u_1} [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace X'] [MeasurableSpace Y'] {π : MeasureTheory.Measure (X × Y)} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} (hπ : IsCoupling π μ ν) {f : X → X'} {g : Y → Y'} (hf : Measurable f) (hg : Measurable g) : IsCoupling (MeasureTheory.Measure.map (Prod.map f g) π) (MeasureTheory.Measure.map f μ) (MeasureTheory.Measure.map g ν)

Pushing a coupling forward coordinatewise along measurable maps couples the two pushforwards.

theorem TauCeti.IsCoupling.smul {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {π : MeasureTheory.Measure (X × Y)} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} (hπ : IsCoupling π μ ν) (c : ENNReal) : IsCoupling (c • π) (c • μ) (c • ν)

Scaling a coupling scales both of its marginals by the same factor.

theorem TauCeti.IsCoupling.add {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {π : MeasureTheory.Measure (X × Y)} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {σ : MeasureTheory.Measure (X × Y)} {μ' : MeasureTheory.Measure X} {ν' : MeasureTheory.Measure Y} (hπ : IsCoupling π μ ν) (hσ : IsCoupling σ μ' ν') : IsCoupling (π + σ) (μ + μ') (ν + ν')

The sum of a coupling of μ, ν and a coupling of μ', ν' couples μ + μ' and ν + ν'.

theorem TauCeti.IsCoupling.smul_add_smul {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {π : MeasureTheory.Measure (X × Y)} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {σ : MeasureTheory.Measure (X × Y)} (hπ : IsCoupling π μ ν) (hσ : IsCoupling σ μ ν) {a b : NNReal} (hab : a + b = 1) : IsCoupling (a • π + b • σ) μ ν

A convex combination of two couplings of μ and ν is again a coupling of μ and ν.

theorem TauCeti.IsCoupling.sum {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {ι : Type u_2} {πs : ι → MeasureTheory.Measure (X × Y)} {μs : ι → MeasureTheory.Measure X} {νs : ι → MeasureTheory.Measure Y} (h : ∀ (i : ι), IsCoupling (πs i) (μs i) (νs i)) : IsCoupling (MeasureTheory.Measure.sum πs) (MeasureTheory.Measure.sum μs) (MeasureTheory.Measure.sum νs)

The sum of a family of couplings couples the sums of the two families of marginals.

theorem TauCeti.IsCoupling.sub_add {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {π : MeasureTheory.Measure (X × Y)} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {κ κ' : MeasureTheory.Measure (X × Y)} [MeasureTheory.IsFiniteMeasure κ] (hπ : IsCoupling π μ ν) (hκ : κ ≤ π) (hκ' : IsCoupling κ' κ.fst κ.snd) : IsCoupling (π - κ + κ') μ ν

Rerouting part of a coupling. Removing a finite part κ ≤ π of a coupling and putting back any measure κ' with the same two marginals as κ gives again a coupling of the same pair.

theorem TauCeti.IsCoupling.map_left {X : Type u} {Y : Type v} {X' : Type w} [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace X'] {π : MeasureTheory.Measure (X × Y)} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} (hπ : IsCoupling π μ ν) {f : X → X'} (hf : Measurable f) : IsCoupling (MeasureTheory.Measure.map (Prod.map f id) π) (MeasureTheory.Measure.map f μ) ν

Pushing a coupling forward along a measurable map of the source alone.

theorem TauCeti.IsCoupling.map_right {X : Type u} {Y : Type v} {Y' : Type u_1} [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace Y'] {π : MeasureTheory.Measure (X × Y)} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} (hπ : IsCoupling π μ ν) {g : Y → Y'} (hg : Measurable g) : IsCoupling (MeasureTheory.Measure.map (Prod.map id g) π) μ (MeasureTheory.Measure.map g ν)

Pushing a coupling forward along a measurable map of the target alone.

theorem TauCeti.IsCoupling.prodProdProdComm {X : Type u} {Y : Type v} {X' : Type w} {Y' : Type u_1} [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace X'] [MeasurableSpace Y'] {π : MeasureTheory.Measure (X × Y)} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {π' : MeasureTheory.Measure (X' × Y')} {μ' : MeasureTheory.Measure X'} {ν' : MeasureTheory.Measure Y'} [MeasureTheory.SFinite π] [MeasureTheory.SFinite π'] (hπ : IsCoupling π μ ν) (hπ' : IsCoupling π' μ' ν') : IsCoupling (MeasureTheory.Measure.map (fun (w : (X × Y) × X' × Y') => ((w.1.1, w.2.1), w.1.2, w.2.2)) (π.prod π')) (μ.prod μ') (ν.prod ν')

Rearranging a product of plans. Exchanging the two middle coordinates of the product of a coupling of μ, ν and a coupling of μ', ν' gives a coupling of μ ⊗ μ' and ν ⊗ ν'.

theorem TauCeti.IsCoupling.map_prod {X : Type u} {Y : Type v} {X' : Type w} {Y' : Type u_1} [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace X'] [MeasurableSpace Y'] {π : MeasureTheory.Measure (X × Y)} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {H : Type u_2} [MeasurableSpace H] (hπ : IsCoupling π μ ν) [MeasureTheory.SFinite π] (η : MeasureTheory.Measure H) [MeasureTheory.SFinite η] {f : X × H → X'} {g : Y × H → Y'} (hf : Measurable f) (hg : Measurable g) : IsCoupling (MeasureTheory.Measure.map (fun (w : (X × Y) × H) => (f (w.1.1, w.2), g (w.1.2, w.2))) (π.prod η)) (MeasureTheory.Measure.map f (μ.prod η)) (MeasureTheory.Measure.map g (ν.prod η))

Running a coupling alongside an independent sample. If π couples μ and ν, then sampling (x, y) ∼ π and an independent z ∼ η and applying f (·, z) and g (·, z) to the two coordinates couples the pushforwards of μ ⊗ η along f and of ν ⊗ η along g.

theorem TauCeti.isCoupling_of_measure_prod_univ_of_measure_univ_prod {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {π : MeasureTheory.Measure (X × Y)} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} (hs : ∀ (s : Set X), MeasurableSet s → π (s ×ˢ Set.univ) = μ s) (ht : ∀ (t : Set Y), MeasurableSet t → π (Set.univ ×ˢ t) = ν t) : IsCoupling π μ ν

The converse of TauCeti.IsCoupling.measure_prod_univ and TauCeti.IsCoupling.measure_univ_prod: the coupling relation can be checked on measurable cylinders, one for each factor.

@[simp]

theorem TauCeti.isCoupling_map_swap_iff {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {π : MeasureTheory.Measure (X × Y)} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} : IsCoupling (MeasureTheory.Measure.map Prod.swap π) ν μ ↔ IsCoupling π μ ν

The coupling relation is invariant under exchanging the two coordinates.

@[simp]

theorem TauCeti.isCoupling_map_prodMap_iff {X : Type u} {Y : Type v} {X' : Type w} {Y' : Type u_1} [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace X'] [MeasurableSpace Y'] {π : MeasureTheory.Measure (X × Y)} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} (e : X ≃ᵐ X') (f : Y ≃ᵐ Y') : IsCoupling (MeasureTheory.Measure.map (Prod.map ⇑e ⇑f) π) (MeasureTheory.Measure.map (⇑e) μ) (MeasureTheory.Measure.map (⇑f) ν) ↔ IsCoupling π μ ν

The coupling relation is invariant under measurable equivalences of the two factors.

@[simp]

theorem TauCeti.isCoupling_zero {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] : IsCoupling 0 0 0

The zero measure couples the two zero measures.

@[simp]

theorem TauCeti.isCoupling_prod {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] : IsCoupling (μ.prod ν) μ ν

The product measure couples two probability measures, so probability measures always have a coupling.

theorem TauCeti.isCoupling_inv_smul_prod {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [MeasureTheory.IsFiniteMeasure μ] (h : μ Set.univ = ν Set.univ) : IsCoupling ((μ Set.univ)⁻¹ • μ.prod ν) μ ν

A finite measure and a measure of equal total mass are coupled by their normalised product. The equality makes the second measure finite. The statement includes the zero measures, where the normalising factor is ∞ and the plan is 0.

theorem TauCeti.exists_isCoupling_iff {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [MeasureTheory.IsFiniteMeasure μ] : (∃ (π : MeasureTheory.Measure (X × Y)), IsCoupling π μ ν) ↔ μ Set.univ = ν Set.univ

A finite measure and any measure admit a coupling exactly when they have the same total mass.

theorem TauCeti.isCoupling_sum_map_pi {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {n : ℕ} (ρ : Fin n → MeasureTheory.Measure (X × Y)) [∀ (i : Fin n), MeasureTheory.IsProbabilityMeasure (ρ i)] (σ : Equiv.Perm (Fin n)) : IsCoupling (MeasureTheory.Measure.sum fun (i : Fin n) => MeasureTheory.Measure.map (fun (w : Fin n → X × Y) => ((w i).1, (w (σ i)).2)) (MeasureTheory.Measure.pi ρ)) (MeasureTheory.Measure.sum ρ).fst (MeasureTheory.Measure.sum ρ).snd

Draw independent samples w i ∼ ρ i of pairs and pair the source of w i with the target of w (σ i). Summed over i, the laws of these permuted pairs have the same two marginals as ∑ i, ρ i.

@[simp]

theorem TauCeti.isCoupling_map_prodMk {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] (x : X) (ν : MeasureTheory.Measure Y) [MeasureTheory.IsProbabilityMeasure ν] : IsCoupling (MeasureTheory.Measure.map (Prod.mk x) ν) (MeasureTheory.Measure.dirac x) ν

A Dirac measure and a probability measure are coupled by the pushforward of the latter along y ↦ (x, y).

@[simp]

theorem TauCeti.isCoupling_dirac_dirac {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] (x : X) (y : Y) : IsCoupling (MeasureTheory.Measure.dirac (x, y)) (MeasureTheory.Measure.dirac x) (MeasureTheory.Measure.dirac y)

Two Dirac measures are coupled by the Dirac measure at the pair.

theorem TauCeti.IsCoupling.eq_map_prodMk {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {π : MeasureTheory.Measure (X × Y)} {ν : MeasureTheory.Measure Y} {x : X} (hπ : IsCoupling π (MeasureTheory.Measure.dirac x) ν) : π = MeasureTheory.Measure.map (Prod.mk x) ν

A plan whose source marginal is a Dirac measure is the pushforward of its target marginal along y ↦ (x, y). Together with TauCeti.isCoupling_map_prodMk this says that a Dirac source has exactly one coupling with each probability target.

theorem TauCeti.IsCoupling.eq_dirac {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {π : MeasureTheory.Measure (X × Y)} {x : X} {y : Y} (hπ : IsCoupling π (MeasureTheory.Measure.dirac x) (MeasureTheory.Measure.dirac y)) : π = MeasureTheory.Measure.dirac (x, y)

Two Dirac measures have exactly one coupling, the Dirac measure at the pair.

@[simp]

theorem TauCeti.isCoupling_toMeasure_iff {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.ProbabilityMeasure X} {ν : MeasureTheory.ProbabilityMeasure Y} {π : MeasureTheory.ProbabilityMeasure (X × Y)} : IsCoupling ↑π ↑μ ↑ν ↔ π.map Prod.fst = μ ∧ π.map Prod.snd = ν

Being a coupling, read on bundled probability measures: the two marginal pushforwards are the prescribed marginals. This is the form in which the coupling condition is a pair of preimages of points under the marginal maps.

@[reducible, inline]

abbrev TauCeti.Coupling {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] (μ : MeasureTheory.ProbabilityMeasure X) (ν : MeasureTheory.ProbabilityMeasure Y) : Type (max u v)

Couplings of two probability measures, bundled as a subtype of the probability measures on the product. The unbundled relation TauCeti.IsCoupling is the one to use for raw measures; this type is the domain over which the probability transport problem is optimised.

Equations

• TauCeti.Coupling μ ν = { π : MeasureTheory.ProbabilityMeasure (X × Y) // TauCeti.IsCoupling ↑π ↑μ ↑ν }

theorem TauCeti.Coupling.ext {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.ProbabilityMeasure X} {ν : MeasureTheory.ProbabilityMeasure Y} {π σ : Coupling μ ν} (h : ↑↑π = ↑↑σ) : π = σ

Two bundled couplings are equal when their underlying measures are equal.

theorem TauCeti.Coupling.ext_iff {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.ProbabilityMeasure X} {ν : MeasureTheory.ProbabilityMeasure Y} {π σ : Coupling μ ν} : π = σ ↔ ↑↑π = ↑↑σ

noncomputable def TauCeti.Coupling.prod {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] (μ : MeasureTheory.ProbabilityMeasure X) (ν : MeasureTheory.ProbabilityMeasure Y) : Coupling μ ν

The independent coupling of two probability measures: their product.

Equations

• TauCeti.Coupling.prod μ ν = ⟨μ.prod ν, ⋯⟩

@[simp]

theorem TauCeti.Coupling.coe_prod {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] (μ : MeasureTheory.ProbabilityMeasure X) (ν : MeasureTheory.ProbabilityMeasure Y) : ↑(prod μ ν) = μ.prod ν

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

instance TauCeti.Coupling.instNonempty {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.ProbabilityMeasure X} {ν : MeasureTheory.ProbabilityMeasure Y} : Nonempty (Coupling μ ν)

Any two probability measures are coupled, by their product.

noncomputable def TauCeti.Coupling.fst {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.ProbabilityMeasure X} {ν : MeasureTheory.ProbabilityMeasure Y} (π : Coupling μ ν) : MeasureTheory.ProbabilityMeasure X

The first marginal of a bundled coupling.

Equations

• π.fst = (↑π).map Prod.fst

noncomputable def TauCeti.Coupling.snd {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.ProbabilityMeasure X} {ν : MeasureTheory.ProbabilityMeasure Y} (π : Coupling μ ν) : MeasureTheory.ProbabilityMeasure Y

The second marginal of a bundled coupling.

Equations

• π.snd = (↑π).map Prod.snd

theorem TauCeti.Coupling.coe_fst {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.ProbabilityMeasure X} {ν : MeasureTheory.ProbabilityMeasure Y} (π : Coupling μ ν) : ↑π.fst = MeasureTheory.Measure.map Prod.fst ↑↑π

The underlying measure of the first marginal is the pushforward along the first projection. This is not a simp lemma: simp rewrites π.fst to μ via fst_eq instead.

theorem TauCeti.Coupling.coe_snd {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.ProbabilityMeasure X} {ν : MeasureTheory.ProbabilityMeasure Y} (π : Coupling μ ν) : ↑π.snd = MeasureTheory.Measure.map Prod.snd ↑↑π

The underlying measure of the second marginal is the pushforward along the second projection. This is not a simp lemma: simp rewrites π.snd to ν via snd_eq instead.

@[simp]

theorem TauCeti.Coupling.fst_eq {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.ProbabilityMeasure X} {ν : MeasureTheory.ProbabilityMeasure Y} (π : Coupling μ ν) : π.fst = μ

The first marginal of a bundled coupling is its prescribed source.

@[simp]

theorem TauCeti.Coupling.snd_eq {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.ProbabilityMeasure X} {ν : MeasureTheory.ProbabilityMeasure Y} (π : Coupling μ ν) : π.snd = ν

The second marginal of a bundled coupling is its prescribed target.

noncomputable def TauCeti.Coupling.swap {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.ProbabilityMeasure X} {ν : MeasureTheory.ProbabilityMeasure Y} (π : Coupling μ ν) : Coupling ν μ

Exchanging the two coordinates of a bundled coupling.

Equations

• π.swap = ⟨(↑π).map Prod.swap, ⋯⟩

@[simp]

theorem TauCeti.Coupling.coe_swap {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.ProbabilityMeasure X} {ν : MeasureTheory.ProbabilityMeasure Y} (π : Coupling μ ν) : ↑π.swap = (↑π).map Prod.swap

The underlying probability measure of the exchanged coupling is the pushforward along the coordinate swap.

@[simp]

theorem TauCeti.Coupling.swap_swap {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.ProbabilityMeasure X} {ν : MeasureTheory.ProbabilityMeasure Y} (π : Coupling μ ν) : π.swap.swap = π

Exchanging the coordinates twice is the identity.

@[simp]

theorem TauCeti.Coupling.swap_prod {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] (μ : MeasureTheory.ProbabilityMeasure X) (ν : MeasureTheory.ProbabilityMeasure Y) : (prod μ ν).swap = prod ν μ

Exchanging the coordinates of the independent coupling gives the independent coupling of the exchanged pair.