Relatively independent joinings over a common factor #
Given two probability spaces carrying a common factor — measurable maps q : Ω → Z and
r : Ξ → Z with the same pushforward — this file builds the canonical coupling of μ and ν
that identifies the two factors and adds nothing else:
relativeFactorCoupling μ ν q r = (condDistrib id q μ ×ₖ condDistrib id r ν) ∘ₘ μ.map q
Both sides are disintegrated over Z and the fibres are then multiplied independently. Nothing
else would do: the independent product μ.prod ν does not satisfy q X = r Ξ, and an arbitrary
coupling with that identity could still let each side see more of the other than the common
factor does.
Main results #
map_condDistrib_id— fibre concentration: the conditional law of a point given its factor value, pushed forward through the factor, is the deterministic identity kernel. This is the whole content of "conditioning onqpins downq", and everything below rests on it.map_fst_relativeFactorCoupling,map_snd_relativeFactorCoupling— the two marginals areμandν(the second under the standing hypothesisν.map r = μ.map q).comp_fst_ae_eq_comp_snd_relativeFactorCoupling— the common-factor identityq ∘ Prod.fst =ᵐ r ∘ Prod.snd.condIndepFun_fst_snd_relativeFactorCoupling— the two coordinates are conditionally independent given the common factor read off the first coordinate.condDistrib_id_map_comap— fibre transport: a measure-preservingTshifting the factor byecarries the disintegration kernel along, so conditioning atzand pushing throughTis conditioning ate z. The commuting squaree ∘ q =ᵐ[μ] q ∘ Tis required only almost everywhere.map_prodMap_relativeFactorCoupling_two_sided— hence a pair of measure-preserving maps shifting the two factors by one and the sameegives a symmetry of the joining, again with both squares required only a.e., each under its own measure. The pushforward identity on the factor law is derived from the commuting square, not assumed, andMeasurableEmbedding esuffices: injectivity is what cancels the pushforward, surjectivity is never used.map_prodMap_relativeFactorCoupling— the degenerate casee = id,U = id, retained because it avoidshr,hqrand the second map, and because its squareq ∘ T = qholds on the nose there. It is deliberately the one statement here that keeps a strict hypothesis.condIndepFun_comp_fst_snd_relativeFactorCoupling— the transfer clause.
Why condition on q ∘ Prod.fst #
The conditioning σ-algebra is MeasurableSpace.comap (q ∘ Prod.fst) inferInstance, generated by a
genuine random variable on the coupling space, not by an auxiliary Z-valued variable that the
composition ∘ₘ has integrated out. Only the former is available to downstream consumers, who see
the coupling and not its construction. The common-factor identity above transfers the statement to
r ∘ Prod.snd whenever that is the more convenient side.
Note that the coupling gives only σ(q ∘ fst) ⊆ σ(snd) modulo the law: the second coordinate may
carry strictly more information than the shared factor, exactly as a uniform U carries more than
1_{U < p}. What the conditional independence excludes is that the surplus says anything about
the first coordinate beyond what the factor already determines.
Fibre concentration #
Fibre concentration. The conditional law of a point given the value of a factor map is
carried by the fibre over that value: pushing condDistrib id q μ forward through q returns
the deterministic identity kernel, almost everywhere for the law of the factor.
The fibre over z carries all of the conditional law given z.
Pointwise form of fibre concentration: conditionally on the factor value z, the factor is
almost surely equal to z.
The coupling #
The relatively independent joining of μ and ν over their common Z-factor. Both sides
are disintegrated over Z — μ along q, ν along r — and the fibres are then multiplied
independently.
Equations
- ProbabilityTheory.relativeFactorCoupling μ ν q r = (MeasureTheory.Measure.map q μ).bind ⇑((ProbabilityTheory.condDistrib id q μ).prod (ProbabilityTheory.condDistrib id r ν))
Instances For
The coupling is a probability measure. Measurability of q is genuinely needed: without it
μ.map q is the zero measure.
The first marginal is μ.
The second marginal is ν, under the standing hypothesis that the two factors have the same
law.
The common-factor identity: the two coordinates agree on the shared factor. Proved from the two fibre-concentration statements, one on each side of the joining — equality of the two factor marginals would not suffice, since it says nothing about the joint law.
The joint law of the common factor and the two coordinates: the factor is a.s. the disintegration variable, so reading it off the first coordinate reconstitutes the outer integration. This is the structural identity behind the conditional independence below.
A symmetry of the first space that fixes the factor is a symmetry of the coupling. If T
preserves μ and satisfies q ∘ T = q, then Prod.map T id preserves the joining: T acts
within the fibres of q, so it leaves each disintegration fibre invariant and never touches the
outer integration.
Fibre transport. If T preserves μ and shifts the factor by e — a commuting square
required only almost everywhere under μ, e ∘ q =ᵐ[μ] q ∘ T — then the disintegration
kernel is carried along: conditioning at z and pushing through T is conditioning at e z.
Two-sided transport of the joining. A pair of measure-preserving maps that shift the two
factors by one and the same e gives a symmetry of the coupling. The two commuting squares are
required only almost everywhere, each under its own measure: e ∘ q =ᵐ[μ] q ∘ T and
e ∘ r =ᵐ[ν] r ∘ U. That is what lets a coding map whose equivariance is itself only a.e. be
supplied directly; demanding strict squares here would make such a coding unusable.
The pushforward identity (μ.map q).map e = μ.map q is derived from the commuting square and
measure preservation, not assumed: taking it as a hypothesis would be redundant and would let a
caller supply an inconsistent pair. MeasurableEmbedding e is what the uniqueness step needs —
it cancels a pushforward along Prod.map e id — and surjectivity is never used.
The two coordinates are conditionally independent given the common factor. The
conditioning σ-algebra is the one generated by q ∘ Prod.fst, a random variable on the coupling
space itself rather than the integrated-out disintegration variable.
The transfer clause. Conditional independence passes to any measurable function of the first coordinate: the second coordinate tells nothing about any reading of the first beyond what the common factor already determines. Stated separately because this — not the marginals and not the common-factor identity — is what rules out the second coordinate secretly encoding the part of the first that the factor leaves unresolved.