How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Conditional density formula
Statement
Let and be sigma-finite measure spaces. Let a joint probability on have nonnegative product-measurable density relative to . A fixed probability on is supplied. Put
Then K is an everywhere probability kernel from T to E. If is the second marginal of , then and
For any random elements X,Y with joint law , is a regular conditional distribution of X given . These event identities require no AC. If interpreted with the library's conditional-expectation class existence convention, assume AC. Neither zero nor infinite marginal-density fibres are normalized by the displayed quotient.
Facts & Assumptions
Given: The hypotheses and conventions in the statement.
Probability-kernel sections must have mass one at every source point and measurable evaluations. Measure kernel and probability kernel.
Nonnegative product-measurable functions on the stated sigma-finite spaces have measurable section integrals and equal iterated integrals. Tonelli's theorem for nonnegative measurable functions on a sigma-finite product.
Each nonnegative measurable section density defines a measure. The indefinite integral of a nonnegative measurable function is a measure.
All conditioning-event identities characterize a supplied RCD. Regular conditional distribution.
Bounded measurable functions of Y integrate against its marginal. Change of variables for expectation.
AC is only for the inherited conditional-class existence notation, not for the density construction with supplied rho. The Axiom of Choice.
Integrating against a density measure equals integrating the product. Integrating against a density agrees with integrating the product.
Proof
By [F2], m is measurable and . For each measurable B, apply [F2] to to obtain . Put and . Then . Also for all , so ; the nonnegative integral over this measurable null set is zero, even though m is infinite there, giving . Therefore is measurable and has full marginal mass. No finite value of m at each point follows from total integrability.
For , let . Tonelli applied to makes measurable. It satisfies everywhere. On D both are finite and the denominator is positive, so is a measurable real function there; reciprocal and multiplication are continuous on this finite positive domain. Pasting the constant off D proves measurable evaluations of K. For each , [F2] ensures that is measurable and [F3] makes a measure of mass m(y); dividing by this finite positive number gives a probability. Off D, K is the supplied probability . This proves [F1], including the empty-event and whole-target evaluations.
For measurable A,B, the contribution of to the K-integral under is zero because and . On D the density conversion [F7] and give On Z, since ; on I its integral is zero because I is -null. Thus the last integral is , which equals by [F2]. All cancellation was restricted to finite positive m.
If X,Y have joint law , [F5] applied to the bounded measurable function converts step 3.1 into The collection of inverse images is already a sigma-algebra and is exactly . These are therefore all required conditioning events. Measurability and probability sections follow from step 2.1 under composition with Y, so [F4] proves the RCD assertion. The proof selected no points, versions or exhaustion: the sigma-finite measures, product density and filler probability are supplied. [F6] is required only when using the library conditional-class existence convention.
Depends on
- Measure kernel and probability kernel
- Tonelli's theorem for nonnegative measurable functions on a sigma-finite product
- The indefinite integral of a nonnegative measurable function is a measure
- Regular conditional distribution
- Change of variables for expectation
- The Axiom of Choice
- Integrating against a density agrees with integrating the product
Used by
Dependency tree · two levels
31 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Durrett, Probability: Theory and Examples, fifth edition (standard reference, not scraped)
- Varadhan, Probability Theory, Chapter 4 (standard reference, not scraped)