Randomizing probability measures and kernels by uniform variables #

A probability measure on a standard Borel space is the law of a measurable function of a single uniform variable, and the function can be chosen to depend measurably on the measure. Packaging that choice once gives a coding map

unitIntervalCoding α : ProbabilityMeasure α → I → α

which is jointly measurable and satisfies volume.map (unitIntervalCoding α P) = P for every P. Feeding it independent uniform variables therefore realizes any product P^{⊗ι} as the law of a coordinatewise transform of uniform noise, which is map_infinitePi_volume_unitIntervalCoding.

This is the "isolation of randomness" step: a random probability measure ν and an independent uniform sequence ϑ together generate a sample from ν, with all the randomness of the sample carried by ϑ. It is what turns a conditional-distribution statement into a functional representation.

The conditional form starts from a Markov kernel κ : Kernel β α. Mathlib provides a jointly measurable realization f : β → I → α of each conditional law κ b; this file proves that the skew map (b, u) ↦ (b, f b u) sends μ.prod volume to the composition-product μ ⊗ₘ κ. Applying this to the conditional kernel of a joint law gives a functional representation of the pair by its first coordinate and a fresh independent uniform variable. This is the conditional randomization step used when a probabilistic representation is converted into latent variables.

Main definitions #

TauCeti.Probability.unitIntervalCoding — the coding map above.

Main results #

TauCeti.Probability.map_volume_unitIntervalCoding — the coding map transports the uniform law on I to its parameter.
TauCeti.Probability.map_infinitePi_volume_unitIntervalCoding — applying it coordinatewise to i.i.d. uniform noise produces the ι-fold power of the parameter for an arbitrary index type.
TauCeti.Probability.exists_measurable_map_prod_volume_eq_compProd — a Markov kernel and a base measure are jointly realized from the base point and independent uniform noise.
TauCeti.Probability.exists_measurable_map_prod_volume_eq — every finite joint law has such a conditional functional representation.
TauCeti.Probability.exists_measurable_map_prod_volume_eq_map_prodMk — the random-variable form, using fresh uniform noise on the original probability space.
TauCeti.Probability.measurable_pi_uncurry_prod — coordinatewise coding of a parameter and a family of noises is jointly measurable.
TauCeti.Probability.map_prod_infinitePi_eq_of_ae_map_eq — coordinatewise realizations fed by independent noises have a joint law determined by their almost-everywhere fibre laws.
TauCeti.Probability.ae_map_eq_of_map_prod_eq — conversely, realizations with the same joint law with the base point have almost everywhere equal fibre laws.

Implementation #

Mathlib's ProbabilityTheory.Kernel.exists_measurable_map_eq_unitInterval supplies the coding for an arbitrary Markov kernel into a standard Borel space; the content here is applying it to the tautological kernel, so that the parameter space is the space of probability measures itself and no further choice has to be threaded through downstream statements. unitIntervalCoding is therefore a choice: it has no properties beyond the two recorded below, and consumers should use those rather than unfold it. The conditional results apply Mathlib's general kernel realization to an arbitrary Markov kernel, identify the resulting skew-product law by the product-measure integral formula, and use Mathlib's Measure.condKernel disintegration for the joint-law forms.

References #

O. Kallenberg, Foundations of Modern Probability, 3rd ed., Lemma 4.22.
O. Kallenberg, Foundations of Modern Probability, 3rd ed., Theorem 8.5, for disintegration.