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.

theorem InformationTheory.klDiv_finsetSum_smul_le {Ω : Type u_1} {ι : Type u_2} {mΩ : MeasurableSpace Ω} {μ ν : ι → MeasureTheory.Measure Ω} [∀ (i : ι), MeasureTheory.IsFiniteMeasure (μ i)] [∀ (i : ι), MeasureTheory.IsFiniteMeasure (ν i)] (s : Finset ι) (c : ι → NNReal) : klDiv (∑ i ∈ s, ↑(c i) • μ i) (∑ i ∈ s, ↑(c i) • ν i) ≤ ∑ i ∈ s, ↑(c i) * klDiv (μ i) (ν i)

Convexity of the Kullback–Leibler divergence in the pair of measures, for a mixture indexed by a Finset: for finite measures μ i, ν i and weights c i ≥ 0, klDiv (∑ i ∈ s, c i • μ i) (∑ i ∈ s, c i • ν i) ≤ ∑ i ∈ s, c i * klDiv (μ i) (ν i). Weights summing to 1 give the convexity of klDiv; no such hypothesis is needed here, since klDiv is positively homogeneous.

theorem InformationTheory.klDiv_sum_smul_le {Ω : Type u_1} {ι : Type u_2} {mΩ : MeasurableSpace Ω} {μ ν : ι → MeasureTheory.Measure Ω} [Fintype ι] [∀ (i : ι), MeasureTheory.IsFiniteMeasure (μ i)] [∀ (i : ι), MeasureTheory.IsFiniteMeasure (ν i)] (c : ι → NNReal) : klDiv (∑ i : ι, ↑(c i) • μ i) (∑ i : ι, ↑(c i) • ν i) ≤ ∑ i : ι, ↑(c i) * klDiv (μ i) (ν i)

Convexity of the Kullback–Leibler divergence in the pair of measures: for finite measures μ i, ν i and weights c i ≥ 0, klDiv (∑ i, c i • μ i) (∑ i, c i • ν i) ≤ ∑ i, c i * klDiv (μ i) (ν i).

theorem InformationTheory.klDiv_smul_add_smul_le {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (μ₀ μ₁ ν₀ ν₁ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ₀] [MeasureTheory.IsFiniteMeasure μ₁] [MeasureTheory.IsFiniteMeasure ν₀] [MeasureTheory.IsFiniteMeasure ν₁] (a b : NNReal) : klDiv (↑a • μ₀ + ↑b • μ₁) (↑a • ν₀ + ↑b • ν₁) ≤ ↑a * klDiv μ₀ ν₀ + ↑b * klDiv μ₁ ν₁

Convexity of the Kullback–Leibler divergence in the pair of measures, for a two-point mixture: for finite measures μ₀, μ₁, ν₀, ν₁ and weights a, b ≥ 0, klDiv (a • μ₀ + b • μ₁) (a • ν₀ + b • ν₁) ≤ a * klDiv μ₀ ν₀ + b * klDiv μ₁ ν₁.

theorem InformationTheory.klDiv_finsetSum_smul_left_le {Ω : Type u_1} {ι : Type u_2} {mΩ : MeasurableSpace Ω} {μ : ι → MeasureTheory.Measure Ω} {ν : MeasureTheory.Measure Ω} {c : ι → NNReal} [∀ (i : ι), MeasureTheory.IsFiniteMeasure (μ i)] [MeasureTheory.IsFiniteMeasure ν] {s : Finset ι} (hc : ∑ i ∈ s, c i = 1) : klDiv (∑ i ∈ s, ↑(c i) • μ i) ν ≤ ∑ i ∈ s, ↑(c i) * klDiv (μ i) ν

Convexity of the Kullback–Leibler divergence in its first argument, for a finite mixture indexed by a Finset: for finite measures μ i, ν and nonnegative weights c i summing to 1, klDiv (∑ i ∈ s, c i • μ i) ν ≤ ∑ i ∈ s, c i * klDiv (μ i) ν.

theorem InformationTheory.klDiv_sum_smul_left_le {Ω : Type u_1} {ι : Type u_2} {mΩ : MeasurableSpace Ω} {μ : ι → MeasureTheory.Measure Ω} {ν : MeasureTheory.Measure Ω} {c : ι → NNReal} [Fintype ι] [∀ (i : ι), MeasureTheory.IsFiniteMeasure (μ i)] [MeasureTheory.IsFiniteMeasure ν] (hc : ∑ i : ι, c i = 1) : klDiv (∑ i : ι, ↑(c i) • μ i) ν ≤ ∑ i : ι, ↑(c i) * klDiv (μ i) ν

Convexity of the Kullback–Leibler divergence in its first argument: for finite measures μ i, ν and nonnegative weights c i summing to 1, klDiv (∑ i, c i • μ i) ν ≤ ∑ i, c i * klDiv (μ i) ν.

theorem InformationTheory.klDiv_finsetSum_smul_right_le {Ω : Type u_1} {ι : Type u_2} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ν : ι → MeasureTheory.Measure Ω} {c : ι → NNReal} [MeasureTheory.IsFiniteMeasure μ] [∀ (i : ι), MeasureTheory.IsFiniteMeasure (ν i)] {s : Finset ι} (hc : ∑ i ∈ s, c i = 1) : klDiv μ (∑ i ∈ s, ↑(c i) • ν i) ≤ ∑ i ∈ s, ↑(c i) * klDiv μ (ν i)

Convexity of the Kullback–Leibler divergence in its second argument, for a finite mixture indexed by a Finset: for finite measures μ, ν i and nonnegative weights c i summing to 1, klDiv μ (∑ i ∈ s, c i • ν i) ≤ ∑ i ∈ s, c i * klDiv μ (ν i).

theorem InformationTheory.klDiv_sum_smul_right_le {Ω : Type u_1} {ι : Type u_2} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ν : ι → MeasureTheory.Measure Ω} {c : ι → NNReal} [Fintype ι] [MeasureTheory.IsFiniteMeasure μ] [∀ (i : ι), MeasureTheory.IsFiniteMeasure (ν i)] (hc : ∑ i : ι, c i = 1) : klDiv μ (∑ i : ι, ↑(c i) • ν i) ≤ ∑ i : ι, ↑(c i) * klDiv μ (ν i)

Convexity of the Kullback–Leibler divergence in its second argument: for finite measures μ, ν i and nonnegative weights c i summing to 1, klDiv μ (∑ i, c i • ν i) ≤ ∑ i, c i * klDiv μ (ν i).