The Kullback–Leibler divergence of composition-products, in integrated form

The chain rule klDiv_compProd_eq_add expresses the conditional divergence as klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η). When the target space of the kernels is countably generated (or the source is countable), the function a ↦ klDiv (κ a) (η a) is measurable (measurable_klDiv_kernel) and the conditional divergence is its integral:

• klDiv_compProd_right_eq_lintegral: klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η) = ∫⁻ a, klDiv (κ a) (η a) ∂μ.

• klDiv_compProd_eq_add_lintegral: klDiv (μ ⊗ₘ κ) (ν ⊗ₘ η) = klDiv μ ν + ∫⁻ a, klDiv (κ a) (η a) ∂μ.

We also record the data processing inequality for the two projections (klDiv_le_compProd, klDiv_comp_le_compProd) and the invariance of the divergence under measurable embeddings (klDiv_map_measurableEmbedding) and measurable equivalences (klDiv_map_measurableEquiv).