Gluing two couplings over a shared marginal #
Two couplings sharing their middle marginal — π₁₂ of (μ₁, μ₂) and π₂₃ of (μ₂, μ₃) —
glue to a joint law on Ω₁ × Ω₂ × Ω₃ whose (1,2)-projection is π₁₂, whose
(2,3)-projection is π₂₃, and whose (1,3)-projection is therefore a coupling of
(μ₁, μ₃). This is the measure-theoretic core of the triangle inequality for coupling-defined
distances (Janson, Graphons, cut norm and distance, Lemma 6.5).
The construction is the relative joining — no conditional-weight formulas #
The glued law is relativeFactorCoupling π₁₂ π₂₃ Prod.snd Prod.fst — the relatively
independent joining of the two couplings over their common middle factor — reordered to
Ω₁ × Ω₂ × Ω₃. Both disintegrations are condDistribs, defined almost everywhere under the
middle marginal, so zero-mass middle atoms never produce a division by zero: there is no
hand-written conditional-weight formula to fail there. The regressions below run the middle
through a Dirac mass — every other middle point has measure zero — precisely to exercise that
branch.
The middle coordinate is read off the first component of the joining; the common-factor
identity (the two middle readings agree almost everywhere) is what makes the
(2,3)-projection exact and not merely almost-sure.
Scope #
Everything here is for standard Borel carriers — which includes every finite or countable discrete carrier, the case the step-approximation route consumes. This does not by itself establish the arbitrary-carrier triangle inequality: that requires, separately, stability of the reduction under step approximation, which no statement in this file addresses.
The glued coupling: the relative joining of the two couplings over their common middle marginal, reordered to the triple product.
Equations
- MeasureTheory.gluedCoupling π₁₂ π₂₃ = MeasureTheory.Measure.map (fun (p : (Ω₁ × Ω₂) × Ω₂ × Ω₃) => (p.1.1, p.1.2, p.2.2)) (ProbabilityTheory.relativeFactorCoupling π₁₂ π₂₃ Prod.snd Prod.fst)
Instances For
The (1,2)-projection is the first coupling. Exact.
The (2,3)-projection is the second coupling. Exact — the middle is read off the first
component, and the common-factor identity moves it to the second before map_snd applies.
The first marginal of the (1,3)-projection is μ₁. Exact.
The last marginal of the (1,3)-projection is μ₃. Exact.
The induced outer coupling #
The induced coupling of the outer marginals: forget the shared middle coordinate in the glued triple law.
Equations
- MeasureTheory.gluedOuterCoupling π₁₂ π₂₃ = MeasureTheory.Measure.map (fun (w : Ω₁ × Ω₂ × Ω₃) => (w.1, w.2.2)) (MeasureTheory.gluedCoupling π₁₂ π₂₃)
Instances For
The first marginal of the induced outer coupling is the first marginal of π₁₂. Exact.
The second marginal of the induced outer coupling is the second marginal of π₂₃. Exact.
Zero-mass middle-atom regressions #
The middle marginal is a Dirac mass, so every other middle point is a zero-mass atom; the projections hold regardless, because the construction never divides by a middle weight.
Pushing a coupling through factor maps #
Exact marginal laws for the pushforward of a coupling through a pair of measurable factor maps. Only measurability is assumed — no finiteness of the targets, no positivity of any cell: finite quotients are a later consumer, obtained by instantiating the targets, and zero-mass cells require nothing because nothing here divides.
The pushforward of a coupling through a pair of factor maps is a probability measure.
The first marginal of the pushed coupling is the pushed first marginal. Exact.
The second marginal of the pushed coupling is the pushed second marginal. Exact.