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).

theorem InformationTheory.klDiv_map_measurableEmbedding {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (μ ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] {f : α → β} (hf : MeasurableEmbedding f) : klDiv (MeasureTheory.Measure.map f μ) (MeasureTheory.Measure.map f ν) = klDiv μ ν

The Kullback–Leibler divergence is invariant under measurable embeddings.

theorem InformationTheory.klDiv_map_measurableEquiv {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (μ ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (e : α ≃ᵐ β) : klDiv (MeasureTheory.Measure.map (⇑e) μ) (MeasureTheory.Measure.map (⇑e) ν) = klDiv μ ν

The Kullback–Leibler divergence is invariant under measurable equivalences.

theorem InformationTheory.klDiv_le_compProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (μ ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (κ η : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel κ] [ProbabilityTheory.IsMarkovKernel η] : klDiv μ ν ≤ klDiv (μ.compProd κ) (ν.compProd η)

Data processing inequality for the first projection: for Markov kernels κ and η, μ and ν are the images of μ ⊗ₘ κ and ν ⊗ₘ η under Prod.fst, hence klDiv μ ν ≤ klDiv (μ ⊗ₘ κ) (ν ⊗ₘ η).

theorem InformationTheory.klDiv_comp_le_compProd {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (μ ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (κ η : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] : klDiv (μ.bind ⇑κ) (ν.bind ⇑η) ≤ klDiv (μ.compProd κ) (ν.compProd η)

Data processing inequality for the second projection: κ ∘ₘ μ and η ∘ₘ ν are the images of μ ⊗ₘ κ and ν ⊗ₘ η under Prod.snd, hence klDiv (κ ∘ₘ μ) (η ∘ₘ ν) ≤ klDiv (μ ⊗ₘ κ) (ν ⊗ₘ η).

theorem InformationTheory.measurable_klDiv_kernel {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace.CountableOrCountablyGenerated α β] (κ η : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] : Measurable fun (a : α) => klDiv (κ a) (η a)

For finite kernels with countably generated target, a ↦ klDiv (κ a) (η a) is measurable.

theorem InformationTheory.klDiv_compProd_right_eq_lintegral {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace.CountableOrCountablyGenerated α β] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (κ η : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] : klDiv (μ.compProd κ) (μ.compProd η) = ∫⁻ (a : α), klDiv (κ a) (η a) ∂μ

Integrated form of the conditional Kullback–Leibler divergence: klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η) = ∫⁻ a, klDiv (κ a) (η a) ∂μ.

theorem InformationTheory.klDiv_compProd_eq_add_lintegral {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSpace.CountableOrCountablyGenerated α β] (μ ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (κ η : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel κ] [ProbabilityTheory.IsMarkovKernel η] : klDiv (μ.compProd κ) (ν.compProd η) = klDiv μ ν + ∫⁻ (a : α), klDiv (κ a) (η a) ∂μ

Chain rule for the Kullback–Leibler divergence, in integrated form: klDiv (μ ⊗ₘ κ) (ν ⊗ₘ η) = klDiv μ ν + ∫⁻ a, klDiv (κ a) (η a) ∂μ.

theorem InformationTheory.klDiv_compProd_left_of_ae {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [Nonempty β] (μ ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] {S : Set α} (hS : MeasurableSet S) (hκ : ∀ a ∈ S, MeasureTheory.IsProbabilityMeasure (κ a)) (hμ : ∀ᵐ (a : α) ∂μ, a ∈ S) (hν : ∀ᵐ (a : α) ∂ν, a ∈ S) : klDiv (μ.compProd κ) (ν.compProd κ) = klDiv μ ν

klDiv_compProd_left for a kernel which is only a probability measure on a measurable set of full measure for both μ and ν.