KL divergence between histories

LeanMachineLearning.lean

@@ -1,6 +1,11 @@
 module  -- shake: keep-all --deprecated_module: ignore
 
 public import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.ChainRule
+public import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.CompProd
+public import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.Convex
+public import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.DataProcessing
+public import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.MapSequence
+public import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.Restrict
 public import LeanMachineLearning.ForMathlib.MeasureTheory.Measurable
 public import LeanMachineLearning.ForMathlib.MeasureTheory.MeasurableSpace.Embedding
 public import LeanMachineLearning.ForMathlib.MeasureTheory.Measure.AbsolutelyContinuous
@@ -46,6 +51,7 @@ public import LeanMachineLearning.SequentialLearning.Algorithms.RoundRobin
 public import LeanMachineLearning.SequentialLearning.Algorithms.Uniform
 public import LeanMachineLearning.SequentialLearning.BayesStationaryEnv
 public import LeanMachineLearning.SequentialLearning.Deterministic
+public import LeanMachineLearning.SequentialLearning.DivergenceDecomposition
 public import LeanMachineLearning.SequentialLearning.EvaluationEnv
 public import LeanMachineLearning.SequentialLearning.FeedbackMartingale
 public import LeanMachineLearning.SequentialLearning.FiniteActions

LeanMachineLearning/ForMathlib/InformationTheory/KullbackLeibler/ChainRule.lean

@@ -25,8 +25,10 @@ source is countable), the function `a ↦ klDiv (κ a) (η a)` is measurable
 * `klDiv_compProd_eq_add_lintegral`:
   `klDiv (μ ⊗ₘ κ) (ν ⊗ₘ η) = klDiv μ ν + ∫⁻ a, klDiv (κ a) (η a) ∂μ`.
 
-We also record the invariance of the divergence under measurable embeddings
-(`klDiv_map_measurableEmbedding`) and measurable equivalences (`klDiv_map_measurableEquiv`).
+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`).
 -/
 
 @[expose] public section
@@ -56,6 +58,25 @@ lemma klDiv_map_measurableEquiv (μ ν : Measure α) [IsFiniteMeasure μ] [IsFin
     klDiv (μ.map e) (ν.map e) = klDiv μ ν :=
   klDiv_map_measurableEmbedding μ ν e.measurableEmbedding
 
+/-- **Data processing inequality** for the first projection: for Markov kernels `κ` and `η`,
+`μ` and `ν` are the images of `μ ⊗ₘ κ` and `ν ⊗ₘ η` under `Prod.fst`, hence
+`klDiv μ ν ≤ klDiv (μ ⊗ₘ κ) (ν ⊗ₘ η)`. -/
+lemma klDiv_le_compProd (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν]
+    (κ η : Kernel α β) [IsMarkovKernel κ] [IsMarkovKernel η] :
+    klDiv μ ν ≤ klDiv (μ ⊗ₘ κ) (ν ⊗ₘ η) := by
+  conv_lhs => rw [← Measure.fst_compProd μ κ, ← Measure.fst_compProd ν η]
+  rw [Measure.fst, Measure.fst]
+  exact klDiv_map_le _ _ measurable_fst
+
+/-- **Data processing inequality** for the second projection: `κ ∘ₘ μ` and `η ∘ₘ ν` are the images
+of `μ ⊗ₘ κ` and `ν ⊗ₘ η` under `Prod.snd`, hence
+`klDiv (κ ∘ₘ μ) (η ∘ₘ ν) ≤ klDiv (μ ⊗ₘ κ) (ν ⊗ₘ η)`. -/
+lemma klDiv_comp_le_compProd (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν]
+    (κ η : Kernel α β) [IsFiniteKernel κ] [IsFiniteKernel η] :
+    klDiv (κ ∘ₘ μ) (η ∘ₘ ν) ≤ klDiv (μ ⊗ₘ κ) (ν ⊗ₘ η) := by
+  rw [← Measure.snd_compProd μ κ, ← Measure.snd_compProd ν η, Measure.snd, Measure.snd]
+  exact klDiv_map_le _ _ measurable_snd
+
 section kernel
 
 variable [MeasurableSpace.CountableOrCountablyGenerated α β] {κ η : Kernel α β} [IsFiniteKernel κ]

LeanMachineLearning/ForMathlib/InformationTheory/KullbackLeibler/CompProd.lean

@@ -0,0 +1,113 @@
+/-
+Copyright (c) 2026 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
+module
+
+public import Mathlib.InformationTheory.KullbackLeibler.Basic
+
+/-! # Lemmas about the Kullback-Leibler divergence of the images of two measures by a measurable map
+-/
+
+@[expose] public section
+
+open MeasureTheory ProbabilityTheory Set
+open scoped ENNReal NNReal
+
+namespace InformationTheory
+
+variable {α β γ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
+  {mγ : MeasurableSpace γ} {μ ν : Measure α} [IsFiniteMeasure μ] [IsFiniteMeasure ν]
+
+/-- Transporting `μ ⊗ₘ η.comap f` along `f` in the first coordinate gives `μ.map f ⊗ₘ η`. -/
+lemma _root_.MeasureTheory.Measure.map_compProd_comap (μ : Measure α) [SFinite μ]
+    (η : Kernel β γ) [IsSFiniteKernel η] {f : α → β} (hf : Measurable f) :
+    (μ ⊗ₘ η.comap f hf).map (fun p : α × γ ↦ (f p.1, p.2)) = μ.map f ⊗ₘ η := by
+  ext s hs
+  rw [Measure.map_apply (by fun_prop) hs, Measure.compProd_apply (hs.preimage (by fun_prop)),
+    Measure.compProd_apply hs, lintegral_map (Kernel.measurable_kernel_prodMk_left hs) hf]
+  rfl
+
+omit [IsFiniteMeasure ν] in
+lemma _root_.MeasureTheory.Measure.map_withDensity_comp
+    {f : β → ℝ≥0∞} (hf : Measurable f) {g : α → β} (hg : Measurable g) :
+    (ν.withDensity (f ∘ g)).map g = (ν.map g).withDensity f := by
+  ext s hs
+  rw [Measure.map_apply hg hs, withDensity_apply _ (hg hs), withDensity_apply _ hs,
+    ← lintegral_indicator hs, ← lintegral_indicator (hg hs), lintegral_map (hf.indicator hs) hg]
+  rfl
+
+lemma klDiv_withDensity_comp_map {f : β → ℝ≥0∞} (hf : Measurable f) {g : α → β} (hg : Measurable g)
+    [IsFiniteMeasure (ν.withDensity (f ∘ g))] :
+    klDiv ((ν.withDensity (f ∘ g)).map g) (ν.map g) = klDiv (ν.withDensity (f ∘ g)) ν := by
+  have hac : ν.withDensity (f ∘ g) ≪ ν := withDensity_absolutelyContinuous ν (f ∘ g)
+  have h_rnDeriv : ((ν.withDensity (f ∘ g)).map g).rnDeriv (ν.map g) =ᵐ[ν.map g] f := by
+    rw [Measure.map_withDensity_comp hf hg]
+    exact Measure.rnDeriv_withDensity _ hf
+  have hmeas : Measurable fun x : β ↦
+      ENNReal.ofReal (klFun (((ν.withDensity (f ∘ g)).map g).rnDeriv (ν.map g) x).toReal) :=
+    (measurable_klFun.comp (Measure.measurable_rnDeriv _ _).ennreal_toReal).ennreal_ofReal
+  rw [klDiv_eq_lintegral_klFun_of_ac (hac.map hg), klDiv_eq_lintegral_klFun_of_ac hac,
+    lintegral_map hmeas hg]
+  refine lintegral_congr_ae ?_
+  filter_upwards [Measure.rnDeriv_withDensity ν (hf.comp hg),
+    ae_of_ae_map hg.aemeasurable h_rnDeriv] with x hx1 hx2
+  rw [hx1, hx2]
+  rfl
+
+/-- If `μ` has density `f ∘ g` with respect to `ν`, then the divergence of the images by `g` is
+the divergence of `μ` and `ν`: `g` is a sufficient statistic. -/
+lemma klDiv_map_of_eq_withDensity_comp {f : β → ℝ≥0∞} (hf : Measurable f) {g : α → β}
+    (hg : Measurable g) (hμ : μ = ν.withDensity (f ∘ g)) :
+    klDiv (μ.map g) (ν.map g) = klDiv μ ν := by
+  rw [hμ]
+  have : IsFiniteMeasure (ν.withDensity (f ∘ g)) := by rw [← hμ]; infer_instance
+  exact klDiv_withDensity_comp_map hf hg
+
+/-- The conditional divergence of two kernels which depend on the conditioning variable only
+through a statistic `f` is the conditional divergence given `f`. -/
+lemma klDiv_compProd_comap (μ : Measure α) [IsFiniteMeasure μ] (κ η : Kernel β γ)
+    [IsFiniteKernel κ] [IsFiniteKernel η] {f : α → β} (hf : Measurable f) :
+    klDiv (μ ⊗ₘ κ.comap f hf) (μ ⊗ₘ η.comap f hf) = klDiv (μ.map f ⊗ₘ κ) (μ.map f ⊗ₘ η) := by
+  have hg : Measurable fun p : α × γ ↦ (f p.1, p.2) := by fun_prop
+  by_cases hac : μ.map f ⊗ₘ κ ≪ μ.map f ⊗ₘ η
+  swap
+  · rw [klDiv_of_not_ac hac, klDiv_of_not_ac]
+    refine fun h ↦ hac ?_
+    have := h.map hg
+    rwa [Measure.map_compProd_comap, Measure.map_compProd_comap] at this
+  let D := (μ.map f ⊗ₘ κ).rnDeriv (μ.map f ⊗ₘ η)
+  have hD : Measurable D := Measure.measurable_rnDeriv _ _
+  have hDκ : μ.map f ⊗ₘ κ = (μ.map f ⊗ₘ η).withDensity D :=
+    (Measure.withDensity_rnDeriv_eq _ _ hac).symm
+  -- for every measurable `t`, the sections of the density integrate to `κ (f a) t`, `μ`-a.e.
+  have h_sect {t : Set γ} (ht : MeasurableSet t) :
+      ∀ᵐ a ∂μ, ∫⁻ c in t, D (f a, c) ∂(η (f a)) = κ (f a) t := by
+    refine ae_of_ae_map (p := fun b ↦ ∫⁻ c in t, D (b, c) ∂(η b) = κ b t) hf.aemeasurable ?_
+    refine ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite
+      (Measurable.setLIntegral_kernel_prod_right (f := fun b c ↦ D (b, c)) hD ht)
+      (Kernel.measurable_coe κ ht) fun u hu _ ↦ ?_
+    have h1 := congrArg (fun ρ : Measure (β × γ) ↦ ρ (u ×ˢ t)) hDκ
+    rw [Measure.compProd_apply_prod hu ht, withDensity_apply _ (hu.prod ht),
+      Measure.setLIntegral_compProd hD hu ht] at h1
+    exact h1.symm
+  have h_rect s t (hs : MeasurableSet s) (ht : MeasurableSet t) :
+      (μ ⊗ₘ κ.comap f hf) (s ×ˢ t) =
+        ((μ ⊗ₘ η.comap f hf).withDensity (D ∘ fun p ↦ (f p.1, p.2))) (s ×ˢ t) := by
+    rw [Measure.compProd_apply_prod hs ht, withDensity_apply _ (hs.prod ht),
+      Measure.setLIntegral_compProd (hD.comp hg) hs ht]
+    refine setLIntegral_congr_fun_ae hs ?_
+    filter_upwards [h_sect ht] with a ha _
+    simp only [Kernel.comap_apply, Function.comp_apply]
+    exact ha.symm
+  have key : μ ⊗ₘ κ.comap f hf =
+      (μ ⊗ₘ η.comap f hf).withDensity (D ∘ fun p ↦ (f p.1, p.2)) := by
+    refine ext_of_generate_finite _ generateFrom_prod.symm isPiSystem_prod ?_ ?_
+    · rintro _ ⟨s, hs, t, ht, rfl⟩
+      exact h_rect s t hs ht
+    · simpa using h_rect Set.univ Set.univ MeasurableSet.univ MeasurableSet.univ
+  rw [← Measure.map_compProd_comap μ κ hf, ← Measure.map_compProd_comap μ η hf,
+    klDiv_map_of_eq_withDensity_comp hD hg key]
+
+end InformationTheory

LeanMachineLearning/ForMathlib/InformationTheory/KullbackLeibler/Convex.lean

@@ -0,0 +1,174 @@
+/-
+Copyright (c) 2026 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
+module
+
+public import Mathlib.InformationTheory.KullbackLeibler.Basic
+
+import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.ChainRule
+
+/-!
+# 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.
+-/
+
+@[expose] public section
+
+open Real MeasureTheory ProbabilityTheory Set
+open scoped ENNReal NNReal
+
+namespace InformationTheory
+
+variable {Ω ι : Type*} {mΩ : MeasurableSpace Ω}
+
+section pair
+
+variable {μ ν : ι → Measure Ω}
+
+/-- **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. -/
+lemma klDiv_finsetSum_smul_le [∀ i, IsFiniteMeasure (μ i)]
+    [∀ i, IsFiniteMeasure (ν i)] (s : Finset ι) (c : ι → ℝ≥0) :
+    klDiv (∑ i ∈ s, (c i : ℝ≥0∞) • μ i) (∑ i ∈ s, (c i : ℝ≥0∞) • ν i)
+      ≤ ∑ i ∈ s, (c i : ℝ≥0∞) * klDiv (μ i) (ν i) := by
+  classical
+  -- the index set, with the discrete measurable structure
+  let _ : MeasurableSpace s := ⊤
+  have : MeasurableSingletonClass s := ⟨fun _ ↦ trivial⟩
+  -- the measure with weights `c` on the index set
+  set β : Measure s := ∑ i : s, (c i : ℝ≥0∞) • Measure.dirac i with hβ_def
+  have hβ_lintegral (f : s → ℝ≥0∞) : ∫⁻ i, f i ∂β = ∑ i : s, (c i : ℝ≥0∞) * f i := by
+    simp only [hβ_def, lintegral_finsetSum_measure, lintegral_smul_measure, lintegral_dirac,
+      smul_eq_mul]
+  have : IsFiniteMeasure β := ⟨by
+    simpa using (hβ_lintegral 1).trans_lt (ENNReal.sum_lt_top.mpr fun i _ ↦ by simp)⟩
+  -- the kernels from the index set given by the two families of measures
+  set κ : Kernel s Ω := Kernel.ofFunOfCountable fun i ↦ μ i
+  set η : Kernel s Ω := Kernel.ofFunOfCountable fun i ↦ ν i
+  have hκ_apply (i : s) : κ i = μ i := rfl
+  have hη_apply (i : s) : η i = ν i := rfl
+  have h_fin (ρ : Kernel s Ω) (ρ' : ι → Measure Ω) [∀ i, IsFiniteMeasure (ρ' i)]
+      (hρ : ∀ i : s, ρ i = ρ' i) : IsFiniteKernel ρ :=
+    ⟨∑ i : s, ρ' i univ, ENNReal.sum_lt_top.mpr fun i _ ↦ measure_lt_top _ _, fun i ↦ by
+      rw [hρ i]
+      exact Finset.single_le_sum (f := fun j : s ↦ ρ' j univ) (fun _ _ ↦ bot_le)
+        (Finset.mem_univ i)⟩
+  have : IsFiniteKernel κ := h_fin κ μ hκ_apply
+  have : IsFiniteKernel η := h_fin η ν hη_apply
+  -- composing a kernel with `β` gives the corresponding mixture
+  have h_comp (ρ : Kernel s Ω) (ρ' : ι → Measure Ω) (hρ : ∀ i : s, ρ i = ρ' i) :
+      ρ ∘ₘ β = ∑ i ∈ s, (c i : ℝ≥0∞) • ρ' i := by
+    ext t ht
+    rw [Measure.bind_apply ht ρ.aemeasurable, hβ_lintegral, Measure.finsetSum_apply,
+      ← Finset.sum_coe_sort s]
+    exact Finset.sum_congr rfl fun i _ ↦ by rw [hρ i, Measure.smul_apply, smul_eq_mul]
+  calc klDiv (∑ i ∈ s, (c i : ℝ≥0∞) • μ i) (∑ i ∈ s, (c i : ℝ≥0∞) • ν i)
+  _ = klDiv (κ ∘ₘ β) (η ∘ₘ β) := by rw [h_comp κ μ hκ_apply, h_comp η ν hη_apply]
+  -- data processing inequality for the second projection
+  _ ≤ klDiv (β ⊗ₘ κ) (β ⊗ₘ η) := klDiv_comp_le_compProd β β κ η
+  -- integral form of the conditional divergence
+  _ = ∫⁻ i, klDiv (κ i) (η i) ∂β := klDiv_compProd_right_eq_lintegral β κ η
+  _ = ∑ i ∈ s, (c i : ℝ≥0∞) * klDiv (μ i) (ν i) := by
+      rw [hβ_lintegral]
+      simp_rw [hκ_apply, hη_apply]
+      exact Finset.sum_coe_sort s fun i ↦ (c i : ℝ≥0∞) * 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)`. -/
+lemma klDiv_sum_smul_le [Fintype ι] [∀ i, IsFiniteMeasure (μ i)]
+    [∀ i, IsFiniteMeasure (ν i)] (c : ι → ℝ≥0) :
+    klDiv (∑ i, (c i : ℝ≥0∞) • μ i) (∑ i, (c i : ℝ≥0∞) • ν i)
+      ≤ ∑ i, (c i : ℝ≥0∞) * klDiv (μ i) (ν i) :=
+  klDiv_finsetSum_smul_le Finset.univ c
+
+/-- **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 μ₁ ν₁`. -/
+lemma klDiv_smul_add_smul_le (μ₀ μ₁ ν₀ ν₁ : Measure Ω) [IsFiniteMeasure μ₀] [IsFiniteMeasure μ₁]
+    [IsFiniteMeasure ν₀] [IsFiniteMeasure ν₁] (a b : ℝ≥0) :
+    klDiv ((a : ℝ≥0∞) • μ₀ + (b : ℝ≥0∞) • μ₁) ((a : ℝ≥0∞) • ν₀ + (b : ℝ≥0∞) • ν₁)
+      ≤ (a : ℝ≥0∞) * klDiv μ₀ ν₀ + (b : ℝ≥0∞) * klDiv μ₁ ν₁ := by
+  have : ∀ x : Bool, IsFiniteMeasure (bif x then μ₁ else μ₀) := fun x ↦ by
+    cases x <;> assumption
+  have : ∀ x : Bool, IsFiniteMeasure (bif x then ν₁ else ν₀) := fun x ↦ by
+    cases x <;> assumption
+  have h := klDiv_sum_smul_le (μ := fun x ↦ bif x then μ₁ else μ₀)
+    (ν := fun x ↦ bif x then ν₁ else ν₀) (fun x ↦ bif x then b else a)
+  simpa [Fintype.sum_bool, add_comm] using h
+
+end pair
+
+section firstArgument
+
+variable {μ : ι → Measure Ω} {ν : Measure Ω} {c : ι → ℝ≥0}
+
+/-- **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) ν`. -/
+lemma klDiv_finsetSum_smul_left_le [∀ i, IsFiniteMeasure (μ i)] [IsFiniteMeasure ν]
+    {s : Finset ι} (hc : ∑ i ∈ s, c i = 1) :
+    klDiv (∑ i ∈ s, (c i : ℝ≥0∞) • μ i) ν ≤ ∑ i ∈ s, (c i : ℝ≥0∞) * klDiv (μ i) ν := by
+  have h := klDiv_finsetSum_smul_le (μ := μ) (ν := fun _ ↦ ν) s c
+  rwa [← Finset.sum_smul, ← ENNReal.ofNNReal_finsetSum, hc, ENNReal.coe_one, one_smul] at h
+
+/-- **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) ν`. -/
+lemma klDiv_sum_smul_left_le [Fintype ι] [∀ i, IsFiniteMeasure (μ i)] [IsFiniteMeasure ν]
+    (hc : ∑ i, c i = 1) :
+    klDiv (∑ i, (c i : ℝ≥0∞) • μ i) ν ≤ ∑ i, (c i : ℝ≥0∞) * klDiv (μ i) ν :=
+  klDiv_finsetSum_smul_left_le hc
+
+end firstArgument
+
+section secondArgument
+
+variable {μ : Measure Ω} {ν : ι → Measure Ω} {c : ι → ℝ≥0}
+
+/-- **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)`. -/
+lemma klDiv_finsetSum_smul_right_le [IsFiniteMeasure μ] [∀ i, IsFiniteMeasure (ν i)]
+    {s : Finset ι} (hc : ∑ i ∈ s, c i = 1) :
+    klDiv μ (∑ i ∈ s, (c i : ℝ≥0∞) • ν i) ≤ ∑ i ∈ s, (c i : ℝ≥0∞) * klDiv μ (ν i) := by
+  have h := klDiv_finsetSum_smul_le (μ := fun _ ↦ μ) (ν := ν) s c
+  rwa [← Finset.sum_smul, ← ENNReal.ofNNReal_finsetSum, hc, ENNReal.coe_one, one_smul] at h
+
+/-- **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)`. -/
+lemma klDiv_sum_smul_right_le [Fintype ι] [IsFiniteMeasure μ] [∀ i, IsFiniteMeasure (ν i)]
+    (hc : ∑ i, c i = 1) :
+    klDiv μ (∑ i, (c i : ℝ≥0∞) • ν i) ≤ ∑ i, (c i : ℝ≥0∞) * klDiv μ (ν i) :=
+  klDiv_finsetSum_smul_right_le hc
+
+end secondArgument
+
+end InformationTheory