The Kullback–Leibler divergence along a generating sequence of maps

Let μ, ν be finite measures on α and g n : α → β n be measurable maps whose σ-algebras comap (g n) increase to the σ-algebra of α (for instance the projections of a sequence space on its first n coordinates). Then the divergence of μ and ν is the supremum of the divergences of their images by the g n: klDiv μ ν = ⨆ n, klDiv (μ.map (g n)) (ν.map (g n)) (klDiv_eq_iSup_map).

The inequality ≥ is the data-processing inequality. For ≤, if μ ≪ ν the divergences of the images are the integrals of klFun of the conditional expectations of the density ∂μ/∂ν given comap (g n) (klDiv_map_eq_lintegral_klFun_condExp), which converge almost everywhere to the density by Lévy's upward theorem, and Fatou's lemma concludes. If μ is not absolutely continuous with respect to ν, a set A with ν A = 0 < μ A is approximated by comap (g n)-measurable sets B n (again by Lévy's upward theorem, applied to the indicator of A under μ + ν), and the lower bound μ B * log (μ B / ν B) + ν B - μ B ≤ klDiv on B n shows that the divergences of the images tend to infinity.

The sequence space case is MeasurableSpace.iSup_comap_restrictFin: the σ-algebras of the projections on the first n coordinates generate the product σ-algebra of ℕ → E.