1.5. ForMathlib.InformationTheory.KullbackLeibler.Convex
From the authors
Convexity of the Kullback–Leibler divergence for mixtures
For finite measures μ i, ν i on Ω and weights c i ≥ 0, the Kullback–Leibler divergence is
convex in the pair of measures:
klDiv (∑ i, c i • μ i) (∑ i, c i • ν i) ≤ ∑ i, c i * klDiv (μ i) (ν i).
The proof combines the data processing inequality with the integral form of the conditional
divergence. Let β := ∑ i, c i • δ i be the measure with weights c on the index set and let
κ, η be the kernels from the index set given by μ and ν. The two mixtures are the
compositions κ ∘ₘ β and η ∘ₘ β, that is, the images of β ⊗ₘ κ and β ⊗ₘ η under the second
projection, so the data processing inequality bounds klDiv (κ ∘ₘ β) (η ∘ₘ β) by the conditional
divergence klDiv (β ⊗ₘ κ) (β ⊗ₘ η), which is ∫⁻ i, klDiv (κ i) (η i) ∂β.
Main statements
-
InformationTheory.klDiv_finsetSum_smul_le,InformationTheory.klDiv_sum_smul_le: convexity ofklDivin the pair of measures, for mixtures indexed by aFinsetand by aFintype; -
InformationTheory.klDiv_smul_add_smul_le: the same statement for two-point mixtures; -
InformationTheory.klDiv_finsetSum_smul_left_le,InformationTheory.klDiv_sum_smul_left_le: convexity ofklDivin its first argument; -
InformationTheory.klDiv_finsetSum_smul_right_le,InformationTheory.klDiv_sum_smul_right_le: convexity ofklDivin its second argument.
Module LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.Convex contains 7 exposed declarations.
-
InformationTheory.klDiv_finsetSum_smul_le -
InformationTheory.klDiv_sum_smul_le -
InformationTheory.klDiv_smul_add_smul_le -
InformationTheory.klDiv_finsetSum_smul_left_le -
InformationTheory.klDiv_sum_smul_left_le -
InformationTheory.klDiv_finsetSum_smul_right_le -
InformationTheory.klDiv_sum_smul_right_le