Basic couplings of measures

A coupling of two measures μ₁ and μ₂ is a measure on their product whose marginals are μ₁ and μ₂. This file provides the carrier-independent coupling API used by the dense graph limit theory: marginal projection rules, measure-preserving projections, integral transfer, coordinate swapping, and the independent and diagonal constructions.

IsCoupling is deliberately a Prop, rather than a structure or typeclass. A coupling is generally not canonical, and consumers such as the cut distance minimize over all witnesses. The product and diagonal measures provide two standard constructions on a common probability carrier; depending on the measure, they may or may not differ.

The declarations live in TauCeti.MeasureTheory because none depends on graphons or cut metrics.

Main definitions

• TauCeti.MeasureTheory.IsCoupling — the predicate that a measure has prescribed marginals;
• TauCeti.MeasureTheory.diagonalCoupling — the pushforward of a measure along the diagonal.

Main results

• isCoupling_prod and isCoupling_diagonalCoupling construct couplings;
• IsCoupling.isProbabilityMeasure and IsCoupling.isFiniteMeasure record that a coupling of probability measures is one;
• IsCoupling.measurePreserving_fst and IsCoupling.measurePreserving_snd expose the marginal projections as measure-preserving maps;
• IsCoupling.integral_comp_fst and IsCoupling.integral_comp_snd transfer integrals depending on one coordinate to the corresponding marginal;
• IsCoupling.swap swaps the coordinates of a coupling;
• isCoupling_map_prodMk builds the graph coupling of two measure-preserving maps out of a common carrier, of which isCoupling_diagonalCoupling is the identity case;
• measurePreserving_diagonal records the diagonal itself as measure preserving.

References

• Roadmap: TauCetiRoadmap/DenseGraphLimits/README.md, Layer 1 — the coupling-primary, cross-carrier cut distance and its IsCoupling input.
• TauCeti/MeasureTheory/OptimalTransport/Gluing.lean — the existing gluing API whose formulation of marginal conditions via Measure.fst and Measure.snd is followed here.

def TauCeti.MeasureTheory.IsCoupling {Ω₁ : Type u_1} {Ω₂ : Type u_2} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] (μ₁ : MeasureTheory.Measure Ω₁) (μ₂ : MeasureTheory.Measure Ω₂) (π : MeasureTheory.Measure (Ω₁ × Ω₂)) : Prop

A coupling of μ₁ and μ₂: a measure on the product whose marginals are μ₁ and μ₂.

Deliberately a Prop rather than a structure or a class: a coupling of two given marginals is not canonical, and the cut distance minimizes over all of them. Use isCoupling_iff to unfold.

Equations

• TauCeti.MeasureTheory.IsCoupling μ₁ μ₂ π = (π.fst = μ₁ ∧ π.snd = μ₂)

theorem TauCeti.MeasureTheory.isCoupling_iff {Ω₁ : Type u_1} {Ω₂ : Type u_2} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] {μ₁ : MeasureTheory.Measure Ω₁} {μ₂ : MeasureTheory.Measure Ω₂} {π : MeasureTheory.Measure (Ω₁ × Ω₂)} : IsCoupling μ₁ μ₂ π ↔ π.fst = μ₁ ∧ π.snd = μ₂

The defining conditions of IsCoupling. The definition's body is not exposed, so this is the lemma downstream modules should rewrite with.

theorem TauCeti.MeasureTheory.IsCoupling.fst_eq {Ω₁ : Type u_1} {Ω₂ : Type u_2} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] {μ₁ : MeasureTheory.Measure Ω₁} {μ₂ : MeasureTheory.Measure Ω₂} {π : MeasureTheory.Measure (Ω₁ × Ω₂)} (hπ : IsCoupling μ₁ μ₂ π) : π.fst = μ₁

The first marginal of a coupling.

theorem TauCeti.MeasureTheory.IsCoupling.snd_eq {Ω₁ : Type u_1} {Ω₂ : Type u_2} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] {μ₁ : MeasureTheory.Measure Ω₁} {μ₂ : MeasureTheory.Measure Ω₂} {π : MeasureTheory.Measure (Ω₁ × Ω₂)} (hπ : IsCoupling μ₁ μ₂ π) : π.snd = μ₂

The second marginal of a coupling.

theorem TauCeti.MeasureTheory.IsCoupling.measurePreserving_fst {Ω₁ : Type u_1} {Ω₂ : Type u_2} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] {μ₁ : MeasureTheory.Measure Ω₁} {μ₂ : MeasureTheory.Measure Ω₂} {π : MeasureTheory.Measure (Ω₁ × Ω₂)} (hπ : IsCoupling μ₁ μ₂ π) : MeasureTheory.MeasurePreserving Prod.fst π μ₁

The first projection out of a coupling is measure preserving. This is the marginal condition in the form the integral transfer below consumes, and the form the measure-preserving-map picture of the cut distance is stated in.

theorem TauCeti.MeasureTheory.IsCoupling.measurePreserving_snd {Ω₁ : Type u_1} {Ω₂ : Type u_2} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] {μ₁ : MeasureTheory.Measure Ω₁} {μ₂ : MeasureTheory.Measure Ω₂} {π : MeasureTheory.Measure (Ω₁ × Ω₂)} (hπ : IsCoupling μ₁ μ₂ π) : MeasureTheory.MeasurePreserving Prod.snd π μ₂

The second projection out of a coupling is measure preserving.

theorem TauCeti.MeasureTheory.IsCoupling.isProbabilityMeasure {Ω₁ : Type u_1} {Ω₂ : Type u_2} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] {μ₁ : MeasureTheory.Measure Ω₁} {μ₂ : MeasureTheory.Measure Ω₂} {π : MeasureTheory.Measure (Ω₁ × Ω₂)} [MeasureTheory.IsProbabilityMeasure μ₁] (hπ : IsCoupling μ₁ μ₂ π) : MeasureTheory.IsProbabilityMeasure π

A coupling of probability measures is itself a probability measure.

theorem TauCeti.MeasureTheory.IsCoupling.isFiniteMeasure {Ω₁ : Type u_1} {Ω₂ : Type u_2} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] {μ₁ : MeasureTheory.Measure Ω₁} {μ₂ : MeasureTheory.Measure Ω₂} {π : MeasureTheory.Measure (Ω₁ × Ω₂)} [MeasureTheory.IsFiniteMeasure μ₁] (hπ : IsCoupling μ₁ μ₂ π) : MeasureTheory.IsFiniteMeasure π

A coupling whose first marginal is finite is a finite measure.

This weakening is what an existentially quantified coupling has to supply by hand: a consumer such as the cut norm asks for IsFiniteMeasure, and a witness bound by an existential cannot provide an instance by unification, so it passes this term explicitly.

theorem TauCeti.MeasureTheory.isCoupling_prod {Ω₁ : Type u_1} {Ω₂ : Type u_2} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] (μ₁ : MeasureTheory.Measure Ω₁) (μ₂ : MeasureTheory.Measure Ω₂) [MeasureTheory.IsProbabilityMeasure μ₁] [MeasureTheory.IsProbabilityMeasure μ₂] : IsCoupling μ₁ μ₂ (μ₁.prod μ₂)

The independent coupling: the product measure couples its two factors.

theorem TauCeti.MeasureTheory.IsCoupling.swap {Ω₁ : Type u_1} {Ω₂ : Type u_2} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] {μ₁ : MeasureTheory.Measure Ω₁} {μ₂ : MeasureTheory.Measure Ω₂} {π : MeasureTheory.Measure (Ω₁ × Ω₂)} (hπ : IsCoupling μ₁ μ₂ π) : IsCoupling μ₂ μ₁ (MeasureTheory.Measure.map Prod.swap π)

Swapping the two coordinates of a coupling of μ₁ and μ₂ gives a coupling of μ₂ and μ₁.

theorem TauCeti.MeasureTheory.IsCoupling.integral_comp_fst {Ω₁ : Type u_1} {Ω₂ : Type u_2} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] {μ₁ : MeasureTheory.Measure Ω₁} {μ₂ : MeasureTheory.Measure Ω₂} {π : MeasureTheory.Measure (Ω₁ × Ω₂)} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] (hπ : IsCoupling μ₁ μ₂ π) {f : Ω₁ → E} (hf : MeasureTheory.AEStronglyMeasurable f μ₁) : ∫ (p : Ω₁ × Ω₂), f p.1 ∂π = ∫ (x : Ω₁), f x ∂μ₁

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

theorem TauCeti.MeasureTheory.IsCoupling.integral_comp_snd {Ω₁ : Type u_1} {Ω₂ : Type u_2} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] {μ₁ : MeasureTheory.Measure Ω₁} {μ₂ : MeasureTheory.Measure Ω₂} {π : MeasureTheory.Measure (Ω₁ × Ω₂)} {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] (hπ : IsCoupling μ₁ μ₂ π) {f : Ω₂ → E} (hf : MeasureTheory.AEStronglyMeasurable f μ₂) : ∫ (p : Ω₁ × Ω₂), f p.2 ∂π = ∫ (x : Ω₂), f x ∂μ₂

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

theorem TauCeti.MeasureTheory.isCoupling_map_prodMk {Ω₁ : Type u_1} {Ω₂ : Type u_2} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] {μ₁ : MeasureTheory.Measure Ω₁} {μ₂ : MeasureTheory.Measure Ω₂} {Ω : Type u_3} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {f : Ω → Ω₁} {g : Ω → Ω₂} (hf : MeasureTheory.MeasurePreserving f μ μ₁) (hg : MeasureTheory.MeasurePreserving g μ μ₂) : IsCoupling μ₁ μ₂ (MeasureTheory.Measure.map (fun (x : Ω) => (f x, g x)) μ)

The graph coupling of two measure-preserving maps out of a common carrier: pushing μ forward along x ↦ (f x, g x) couples μ₁ and μ₂.

This is the coupling a common-carrier comparison of two objects contributes to a coupling infimum, and it is where the measure-preserving-map picture enters the coupling-primary one. The diagonal coupling below is the case f = g = id.

noncomputable def TauCeti.MeasureTheory.diagonalCoupling {Ω : Type u_3} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) : MeasureTheory.Measure (Ω × Ω)

The diagonal coupling of a measure with itself: the pushforward of μ along x ↦ (x, x).

Equations

• TauCeti.MeasureTheory.diagonalCoupling μ = MeasureTheory.Measure.map (fun (x : Ω) => (x, x)) μ

theorem TauCeti.MeasureTheory.diagonalCoupling_apply {Ω : Type u_3} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) {s : Set (Ω × Ω)} (hs : MeasurableSet s) : (diagonalCoupling μ) s = μ {x : Ω | (x, x) ∈ s}

The diagonal coupling of a measurable set is the measure of its diagonal slice.

theorem TauCeti.MeasureTheory.measurePreserving_diagonal {Ω : Type u_3} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) : MeasureTheory.MeasurePreserving (fun (x : Ω) => (x, x)) μ (diagonalCoupling μ)

The diagonal is measure preserving onto the diagonal coupling.

This is the defining pushforward, packaged for the transport lemmas that ask for a MeasurePreserving hypothesis. It is stated here because diagonalCoupling is not reducible outside this module, so a caller cannot supply the pushforward identity by rfl.

theorem TauCeti.MeasureTheory.isCoupling_diagonalCoupling {Ω : Type u_3} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) : IsCoupling μ μ (diagonalCoupling μ)

The diagonal coupling is a coupling of μ with itself: the graph coupling of the identity with itself.

instance TauCeti.MeasureTheory.instIsProbabilityMeasureDiagonalCoupling {Ω : Type u_3} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] : MeasureTheory.IsProbabilityMeasure (diagonalCoupling μ)

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