Coupling a factor to a uniform latent (R4 converse piece 3, #107)

The specialization of ProbabilityTheory.relativeFactorCoupling in which the second space is the project's uniform source: given a factor map q : Ω → Z of a probability measure μ, there is a coupling of μ with uniform01 on Ω × ℝ whose second coordinate is uniform, whose first has law μ, in which the latent resolves the factor, and in which the latent tells nothing further about Ω.

This is the narrow randomization step the rankwise recursion needs, and it runs in the direction that Graphon.KernelRandomization does not: that module manufactures a variable with a prescribed law out of a uniform, whereas here a uniform must be manufactured alongside an already-given variable. The only uniform-specific input is Measure.exists_measurable_map_eq_uniform01 (#140), which supplies the coding map f : ℝ → Z matching the two factor laws; everything after that is the generic relative joining.

Contents

• ProbabilityTheory.exists_relativeFactorCoupling_uniform01 — the wrapper: a measurable coding map together with all five properties of the resulting coupling.

theorem ProbabilityTheory.exists_relativeFactorCoupling_uniform01 {Ω : Type u_1} {Z : Type u_2} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] [MeasurableSpace Z] [StandardBorelSpace Z] [Nonempty Z] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] {q : Ω → Z} (hq : Measurable q) : ∃ (f : ℝ → Z), Measurable f ∧ MeasureTheory.IsProbabilityMeasure (relativeFactorCoupling μ MeasureTheory.uniform01 q f) ∧ MeasureTheory.Measure.map Prod.fst (relativeFactorCoupling μ MeasureTheory.uniform01 q f) = μ ∧ MeasureTheory.Measure.map Prod.snd (relativeFactorCoupling μ MeasureTheory.uniform01 q f) = MeasureTheory.uniform01 ∧ q ∘ Prod.fst =ᵐ[relativeFactorCoupling μ MeasureTheory.uniform01 q f] f ∘ Prod.snd ∧ CondIndepFun (MeasurableSpace.comap (q ∘ Prod.fst) inferInstance) ⋯ Prod.fst Prod.snd (relativeFactorCoupling μ MeasureTheory.uniform01 q f)

Every factor of a probability measure can be coupled to a uniform latent. The coding map f comes from the randomization adapter; the coupling is the relatively independent joining of μ and uniform01 over the common Z-factor, and it satisfies, in order: it is a probability measure; its first marginal is μ; its second marginal is uniform01; the latent resolves the factor, q X = f ξ a.s.; and the two coordinates are conditionally independent given the factor read off the first coordinate.

The conditioning σ-algebra is generated by q ∘ Prod.fst, a variable on the coupling space itself, rather than by the disintegration variable the construction integrates out. Conditional independence of the latent from any coarser function of the first coordinate follows by measurable composition.