Randomizing conditionally independent variables #
Conditionally independent random variables can be represented by measurable functions of the conditioning variable, fed by separate independent noise variables. Keeping the noises separate, rather than coding the product conditional law with one noise variable, records the conditional independence in the functional representation. The construction is given both for a pair and for an arbitrary finite family.
This is the conditional randomization step used when a probabilistic factorization is converted into separate latent variables. It combines Mathlib's factorization of a conditionally independent joint law into a product of conditional distributions with measurable randomization of the coordinate kernels. The joint-law identities hold for any finite base measure; when the base measure is a probability measure, the product noise coordinates are independent of one another and of the original sample.
Conversely, codings of conditionally independent variables obtained separately, each jointly with the conditioning variable, can be fed with independent noises to realize their joint law with the conditioning variable; this is done for a pair and for a finite family.
Main results #
ProbabilityTheory.CondIndepFun.exists_independent_coding— conditionally independent random variables are generated from separate independent uniform variables given the conditioning variable.ProbabilityTheory.CondIndepFun.map_prod_prod_eq_of_map_prod_eq— given codings of the two variables, independent noises realize their joint law with the conditioning variable.ProbabilityTheory.iCondIndepFun.exists_independent_coding— the finite-family version, with one independent uniform coordinate per family member.ProbabilityTheory.iCondIndepFun.map_prod_pi_eq_of_map_prod_eq— given codings of each member of a finite family, independent noises realize its joint law with the conditioning variable.
References #
- O. Kallenberg, Foundations of Modern Probability, 3rd ed., Lemma 4.22 and Theorem 8.5.
Conditional independence as a functional representation. If X and Y are conditionally
independent given Z, then their joint law with Z is obtained by keeping Z and applying two
measurable coding functions to separate uniform coordinates. When μ is a probability measure,
the noises are independent both of one another and of the original sample carrying Z.
Gluing conditionally independent codings. Suppose X and Y are conditionally independent
given Z, and each is realized, jointly with Z, by a measurable function of Z and an
independent noise, with laws ρ₁ and ρ₂. Then feeding independent noises into the two codings
realizes the joint law of (Z, X, Y).
Families #
The conditional law of a finite conditionally independent family factors on measurable rectangles into the product of its one-coordinate conditional laws, almost everywhere under the law of the conditioning variable.
Conditional independence as a finite-family functional representation. Suppose each coordinate of a finite conditionally independent family is realized from the conditioning variable and its own noise coordinate, almost everywhere under the law of the conditioning variable. Applying those realizations to a product noise preserves the joint law of the conditioning variable and the whole family.
Gluing conditionally independent codings of a finite family. Suppose a finite family is
conditionally independent given Z, and each coordinate X i is realized, jointly with Z, by a
measurable function of Z and an independent noise with law ρ i. Then feeding independent
noises into the codings realizes the joint law of Z and the whole family.
A finite conditionally independent family has a functional representation by independent uniform noises. Every coordinate is a jointly measurable function of the conditioning variable and its own uniform coordinate, and the resulting family has the same joint law with the conditioning variable as the original family.