When P ≪ volume and Q ≪ volume, the log-likelihood ratio llr P Q splits, P-a.e., into the difference of the two volume-densities' logarithms: llr P Q x = log (P-density x) − log (Q-density x) for P-a.e. x, where P-density x := (P.rnDeriv volume x).toReal.

This is rnDeriv P Q = rnDeriv P volume / rnDeriv Q volume (a.e.) under the chain rule, pushed through Real.log. @audit:ok

Per-fiber density expansion (sub-gap (b)). For P Q : Measure ℝ with P ≪ volume, Q ≪ volume, equal total mass P univ = Q univ, the real-valued Kullback-Leibler divergence expands into minus the differential entropy of P and a cross-entropy term:

(klDiv P Q).toReal = − differentialEntropy P − ∫ x, (P.rnDeriv volume x).toReal · log ((Q.rnDeriv volume x).toReal) ∂volume.

differentialEntropy P = − ∫ p log p and the cross-term is ∫ p log q, so this is ∫ p log p − ∫ p log q = ∫ p log (p/q) = ∫ llr P Q ∂P.

The cross-term integrability Integrable (fun x ↦ (P.rnDeriv volume x).toReal · log ((Q.rnDeriv volume x).toReal)) volume is a regularity precondition (the term may otherwise be non-integrable). @audit:ok

Per-fiber balance in ℝ≥0∞: the sum of the differential entropy positive part A, KL divergence, and cross-entropy positive part Cpos equals the sum of the negative parts B and Cneg. A subtraction-free identity used by the assembler via lintegral_add. @audit:ok

Fubini + condDistrib marginal identification (sub-gap (c), measure-level core). For X : Ω → ℝ, Z : Ω → α measurable and g : ℝ → ℝ integrable against μ.map X, averaging the X-fiber integral of g over the law μ.map Z of Z returns the μ.map X integral:

∫ z, (∫ x, g x ∂(condDistrib X Z μ z)) ∂(μ.map Z) = ∫ x, g x ∂(μ.map X).

Proof route: compProd_map_condDistrib identifies (μ.map Z) ⊗ₘ condDistrib X Z μ with μ.map (fun ω ↦ (Z ω, X ω)); Measure.integral_compProd (Fubini, on fun p ↦ g p.2) opens the joint integral into the iterated fiber integral; and integral_map reduces the joint integral to ∫ x, g x ∂(μ.map X) via the second projection. @audit:ok

The density-form wrapper of sub-gap (c), packaging the cross-entropy shape the assembly consumes. With g := fun x ↦ Real.log ((μ.map X).rnDeriv volume x).toReal and the per-fiber density rewrite ∫ x, g x ∂(κ z) = ∫ x, (κ z -density x) · g x ∂volume (needs κ z ≪ volume a.e. z), the μ.map Z-average of the fiber cross-integral equals the marginal cross-integral against μ.map X's own density:

∫ z, (∫ x, (κ z -density x) · log (qX x) ∂volume) ∂(μ.map Z) = ∫ x, (qX x) · log (qX x) ∂volume, where qX x := ((μ.map X).rnDeriv volume x).toReal.

hX_ac (μ.map X ≪ volume), hκ_ac (each fiber condDistrib X Z μ z ≪ volume, a.e. z) and h_logq_int (integrability of log qX against μ.map X) are regularity preconditions inherited from the disintegration / sub-gap (a) finiteness. @audit:ok

ℝ≥0∞ Fubini + condDistrib marginal identification (crux ② core). ℝ≥0∞ mirror of integral_condDistrib_marginal_eq: for X : Ω → ℝ, Z : Ω → α measurable and g : ℝ → ℝ≥0∞ measurable, averaging the X-fiber lintegral of g over μ.map Z returns the μ.map X lintegral:

∫⁻ z, (∫⁻ x, g x ∂(condDistrib X Z μ z)) ∂(μ.map Z) = ∫⁻ x, g x ∂(μ.map X).

ℝ≥0∞ Tonelli (Measure.lintegral_compProd) is unconditional, so unlike the ∫/Bochner sibling no integrability hypothesis is needed — just measurability hg.

Proof route: compProd_map_condDistrib identifies (μ.map Z) ⊗ₘ condDistrib X Z μ with μ.map (fun ω ↦ (Z ω, X ω)); Measure.lintegral_compProd (Tonelli on fun p ↦ g p.2) opens the joint lintegral into the iterated fiber lintegral; and lintegral_map reduces the joint lintegral to ∫⁻ x, g x ∂(μ.map X) via the second projection. @audit:ok

ℝ≥0∞ cross-term marginal collapse (crux ② core, sign-parametrized). ℝ≥0∞ mirror of integral_condDistrib_density_marginal_eq: the μ.map Z-average of the fiber cross-lintegral ∫⁻ x, ofReal (sign (pz_x · log qX_x)) ∂volume (where pz_x := (condDistrib X Z μ z -density x), qX_x := (μ.map X -density x), log qX_x := Real.log qX_x) collapses to the marginal cross-lintegral against the μ.map X density.

hsign_hom (sign (a * b) = a * sign b) lets the pz-factor commute out of sign, so ofReal (pz · sign (log qX)) = ofReal pz · ofReal (sign (log qX)) (ofReal_mul, pz ≥ 0) and the pz = (κz)-density factor is absorbed via lintegral_rnDeriv_mul. The assembly instantiates sign := id (positive part) and sign := Neg.neg (negative part). ofReal clips negatives to 0, so the two instantiations split the signed cross-term into its ℝ≥0∞ positive/negative parts.

All hypotheses are regularity preconditions (measurability, absolute continuity, homogeneity of sign); the marginal collapse is the conclusion. @audit:ok