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.

theorem InformationTheory.klDiv_eq_iSup_map {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] {β : ℕ → Type u_2} [mβ : (n : ℕ) → MeasurableSpace (β n)] {g : (n : ℕ) → α → β n} (hg : ∀ (n : ℕ), Measurable (g n)) (hmono : Monotone fun (n : ℕ) => MeasurableSpace.comap (g n) (mβ n)) (hsup : ⨆ (n : ℕ), MeasurableSpace.comap (g n) (mβ n) = m0) : klDiv μ ν = ⨆ (n : ℕ), klDiv (MeasureTheory.Measure.map (g n) μ) (MeasureTheory.Measure.map (g n) ν)

The divergence along a generating sequence of maps. If the σ-algebras comap (g n) of measurable maps g n : α → β n increase to the σ-algebra of α, then the divergence of two finite measures is the supremum of the divergences of their images by the g n.

theorem MeasurableSpace.iSup_comap_restrictFin {E : Type u_1} [mE : MeasurableSpace E] : ⨆ (n : ℕ), MeasurableSpace.comap (fun (f : ℕ → E) (i : Fin n) => f ↑i) pi = pi

The σ-algebras of the projections of ℕ → E on the first n coordinates generate the product σ-algebra.