LeanMachineLearning

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 of klDiv in the pair of measures, for mixtures indexed by a Finset and by a Fintype;

  • 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 of klDiv in its first argument;

  • InformationTheory.klDiv_finsetSum_smul_right_le, InformationTheory.klDiv_sum_smul_right_le: convexity of klDiv in its second argument.

Module LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.Convex contains 7 exposed declarations.