From 09bedb025d257356b6a831f87ce186b4a2adb9e9 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Fri, 13 Nov 2026 10:23:49 +0100 Subject: [PATCH 1/4] feat: the measurable space on kernels, from LML MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Add `Statlib/ForMathlib/Probability/Kernel/MeasurableSpace.lean` with LML's instance `instMeasurableSpaceKernel` (the comap of the coercion to functions), `measurable_kernel_iff` and `Kernel.measurable_const`, and move `Kernel.measurable_eval` and `Kernel.measurable_eval'` there. Remove the instance of `Inference.lean`, which defined the same σ-algebra but is not definitionally equal to LML's, and its `Kernel.measurable_iff` and `Kernel.measurable_of_measurable_eval` (use `measurable_kernel_iff`). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0196ftMV379vy48QfzHBVNvo --- Statlib.lean | 1 + .../Probability/Kernel/MeasurableSpace.lean | 56 +++++++++++++++++++ Statlib/Inference/Inference.lean | 38 ++----------- 3 files changed, 62 insertions(+), 33 deletions(-) create mode 100644 Statlib/ForMathlib/Probability/Kernel/MeasurableSpace.lean diff --git a/Statlib.lean b/Statlib.lean index a5f1af4..3ee4ad5 100644 --- a/Statlib.lean +++ b/Statlib.lean @@ -127,6 +127,7 @@ import Statlib.ForMathlib.Probability.Kernel.Basic import Statlib.ForMathlib.Probability.Kernel.Composition.Lemmas import Statlib.ForMathlib.Probability.Kernel.Composition.MeasureCompProd import Statlib.ForMathlib.Probability.Kernel.Composition.RadonNikodym +import Statlib.ForMathlib.Probability.Kernel.MeasurableSpace import Statlib.ForMathlib.Probability.Kernel.Posterior import Statlib.ForMathlib.Probability.Moments.Variance import Statlib.ForMathlib.Probability.Process.Filtration diff --git a/Statlib/ForMathlib/Probability/Kernel/MeasurableSpace.lean b/Statlib/ForMathlib/Probability/Kernel/MeasurableSpace.lean new file mode 100644 index 0000000..4c390a9 --- /dev/null +++ b/Statlib/ForMathlib/Probability/Kernel/MeasurableSpace.lean @@ -0,0 +1,56 @@ +/- +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.Probability.Kernel.Basic + +/-! +# Measurable space of kernels + +The space of kernels `Kernel 𝓧 𝓨` carries the σ-algebra induced by the coercion to functions +`𝓧 → Measure 𝓨`: the coarsest one for which all the evaluations `κ ↦ κ x` are measurable. + +## Main statements + +* `ProbabilityTheory.measurable_kernel_iff`: a map into a space of kernels is measurable if and only + if all its evaluations are measurable. +* `ProbabilityTheory.Kernel.measurable_eval`: the evaluations `κ ↦ κ x` are measurable. +-/ + +@[expose] public section + +open MeasureTheory + +namespace ProbabilityTheory + +variable {𝓧 𝓨 𝓩 : Type*} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {m𝓩 : MeasurableSpace 𝓩} + +instance instMeasurableSpaceKernel : MeasurableSpace (Kernel 𝓧 𝓨) := + MeasurableSpace.comap (fun κ ↦ (κ : 𝓧 → Measure 𝓨)) inferInstance + +lemma measurable_kernel_iff (f : 𝓧 → Kernel 𝓨 𝓩) : Measurable f ↔ ∀ y, Measurable (f · y) := by + unfold instMeasurableSpaceKernel + rw [measurable_comap_iff, measurable_pi_iff] + simp + +namespace Kernel + +lemma measurable_eval (x : 𝓧) : Measurable fun κ : Kernel 𝓧 𝓨 ↦ κ x := + (measurable_kernel_iff (id : Kernel 𝓧 𝓨 → Kernel 𝓧 𝓨)).1 measurable_id x + +lemma measurable_eval' (x : 𝓧) {s : Set 𝓨} (hs : MeasurableSet s) : + Measurable fun κ : Kernel 𝓧 𝓨 ↦ κ x s := + (Measure.measurable_coe hs).comp (measurable_eval x) + +@[fun_prop] +lemma measurable_const : Measurable (@Kernel.const 𝓧 𝓨 m𝓧 m𝓨) := by + rw [measurable_kernel_iff] + simp only [const_apply] + fun_prop + +end Kernel + +end ProbabilityTheory diff --git a/Statlib/Inference/Inference.lean b/Statlib/Inference/Inference.lean index 30a4c3e..99c0b8b 100644 --- a/Statlib/Inference/Inference.lean +++ b/Statlib/Inference/Inference.lean @@ -7,6 +7,7 @@ Authors: Yongxi Lin module public import Mathlib.Probability.Kernel.Defs +public import Statlib.ForMathlib.Probability.Kernel.MeasurableSpace /-! # Statistical Inference @@ -81,8 +82,8 @@ def HasRateOfConvergence (l : Filter ι) (I : InferenceModelofMeasure ι Ω S X end InferenceModelofMeasure --- In this section, we define a measurable space structure on the space of kernels and a canonical --- map from the space of measures to the space of kernels. +-- In this section, we define a canonical map from the space of measures to the space of kernels, +-- which is measurable (for the σ-algebra `instMeasurableSpaceKernel` on kernels). namespace ProbabilityTheory @@ -92,7 +93,7 @@ namespace Kernel def of_measure (θ Ω : Type*) [MeasurableSpace θ] [mΩ : MeasurableSpace Ω] (μ : Measure Ω) : Kernel θ Ω where toFun := fun _ => μ - measurable' := measurable_const + measurable' := _root_.measurable_const theorem injective_kernel_of_measure (θ Ω : Type*) [MeasurableSpace θ] [hθ : Nonempty θ] [mΩ : MeasurableSpace Ω] : Function.Injective (of_measure θ Ω) := by @@ -100,38 +101,9 @@ theorem injective_kernel_of_measure (θ Ω : Type*) [MeasurableSpace θ] simp_all only [of_measure, mk.injEq] exact congr_fun hμν Classical.ofNonempty -instance instMeasurableSpaceKernel (θ Ω : Type*) [MeasurableSpace θ] [MeasurableSpace Ω] : - MeasurableSpace (Kernel θ Ω) := - ⨆ (t : θ), Measure.instMeasurableSpace.comap fun κ => κ t - -theorem measurable_eval {θ Ω : Type*} [MeasurableSpace θ] - [MeasurableSpace Ω] (t : θ) : - Measurable fun κ : Kernel θ Ω => κ t := - Measurable.of_comap_le <| le_iSup_of_le t <| le_rfl - -theorem measurable_eval' {θ Ω : Type*} [MeasurableSpace θ] - [MeasurableSpace Ω] (t : θ) {s : Set Ω} (hs : MeasurableSet s) : - Measurable fun κ : Kernel θ Ω => κ t s := - (Measure.measurable_coe hs).comp (measurable_eval t) - -theorem measurable_of_measurable_eval {α θ Ω : Type*} [MeasurableSpace α] - [MeasurableSpace θ] [MeasurableSpace Ω] (κ : α → Kernel θ Ω) - (hκ : ∀ t, Measurable fun a => κ a t) : - Measurable κ := by - simp only [measurable_iff_comap_le, instMeasurableSpaceKernel, MeasurableSpace.comap_iSup, - MeasurableSpace.comap_comp] - exact iSup_le fun t => (hκ t).comap_le - -/-- A function into the space of kernels is measurable iff all its evaluation maps are -measurable. -/ -theorem measurable_iff {α θ Ω : Type*} [MeasurableSpace α] - [MeasurableSpace θ] [MeasurableSpace Ω] {κ : α → Kernel θ Ω} : - Measurable κ ↔ ∀ t, Measurable fun a => κ a t := - ⟨fun hκ t => (measurable_eval t).comp hκ, measurable_of_measurable_eval κ⟩ - theorem measurable_kernel_of_measure (θ Ω : Type*) [MeasurableSpace θ] [mΩ : MeasurableSpace Ω] : Measurable (of_measure θ Ω) := - measurable_iff.2 fun _ => measurable_id + (measurable_kernel_iff _).2 fun _ => measurable_id /-- The inverse of the range factorization of the constant-kernel map. -/ noncomputable def inv_rangeFactorization_of_measure (θ Ω : Type*) From 4e3cffad6f241491710863d57cf3d61e0d46ff2f Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Fri, 13 Nov 2026 10:23:49 +0100 Subject: [PATCH 2/4] feat: generalize `rnDeriv_restrict_restrict` and `singularPart_restrict_restrict` MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Assume `μ.HaveLebesgueDecomposition ν` instead of `SigmaFinite μ` (and, for the singular part, no assumption on `ν`). The proofs are unchanged. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0196ftMV379vy48QfzHBVNvo --- .../MeasureTheory/Measure/Decomposition/RadonNikodym.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Statlib/ForMathlib/MeasureTheory/Measure/Decomposition/RadonNikodym.lean b/Statlib/ForMathlib/MeasureTheory/Measure/Decomposition/RadonNikodym.lean index 820be6b..1d2ee5f 100644 --- a/Statlib/ForMathlib/MeasureTheory/Measure/Decomposition/RadonNikodym.lean +++ b/Statlib/ForMathlib/MeasureTheory/Measure/Decomposition/RadonNikodym.lean @@ -48,15 +48,15 @@ lemma singularPart_add_lintegral_rnDeriv (μ ν : Measure α) [μ.HaveLebesgueDe μ.singularPart ν Set.univ + ∫⁻ x, μ.rnDeriv ν x ∂ν = μ Set.univ := by simpa using singularPart_add_setLIntegral_rnDeriv μ ν MeasurableSet.univ -lemma rnDeriv_restrict_restrict (μ ν : Measure α) [SigmaFinite μ] [SigmaFinite ν] - {s : Set α} (hs : MeasurableSet s) : +lemma rnDeriv_restrict_restrict (μ ν : Measure α) [μ.HaveLebesgueDecomposition ν] + [SigmaFinite ν] {s : Set α} (hs : MeasurableSet s) : (μ.restrict s).rnDeriv (ν.restrict s) =ᵐ[ν.restrict s] μ.rnDeriv ν := by refine (eq_rnDeriv (s := (μ.singularPart ν).restrict s) (measurable_rnDeriv μ ν) (((mutuallySingular_singularPart μ ν).restrict s).symm.restrict s).symm ?_).symm conv_lhs => rw [μ.haveLebesgueDecomposition_add ν] rw [restrict_add, restrict_withDensity hs] -lemma singularPart_restrict_restrict (μ ν : Measure α) [SigmaFinite μ] [SigmaFinite ν] +lemma singularPart_restrict_restrict (μ ν : Measure α) [μ.HaveLebesgueDecomposition ν] {s : Set α} (hs : MeasurableSet s) : (μ.restrict s).singularPart (ν.restrict s) = (μ.singularPart ν).restrict s := by refine (eq_singularPart (measurable_rnDeriv μ ν) From f3d31f36a264b967d22088c5ae7acb794386c88e Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Fri, 13 Nov 2026 10:23:49 +0100 Subject: [PATCH 3/4] feat: `klDiv_compProd_left_of_ae`, from LML MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `KL(μ ⊗ₘ κ, ν ⊗ₘ κ) = KL(μ, ν)` when `κ` is a probability measure on a measurable set of full `μ`- and `ν`-measure. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0196ftMV379vy48QfzHBVNvo --- .../KullbackLeibler/ChainRule.lean | 31 +++++++++++++++++++ 1 file changed, 31 insertions(+) diff --git a/Statlib/ForMathlib/InformationTheory/KullbackLeibler/ChainRule.lean b/Statlib/ForMathlib/InformationTheory/KullbackLeibler/ChainRule.lean index 469a835..484d3cc 100644 --- a/Statlib/ForMathlib/InformationTheory/KullbackLeibler/ChainRule.lean +++ b/Statlib/ForMathlib/InformationTheory/KullbackLeibler/ChainRule.lean @@ -32,6 +32,8 @@ measure `μ`. `KL(ρ, μ ⊗ₘ η) = KL(ρ.fst, μ) + KL(ρ, ρ.fst ⊗ₘ η)`. * `InformationTheory.klDiv_prod_eq_klDiv_snd_add`: `KL(ρ, μ × ξ) = KL(ρ.snd, ξ) + KL(ρ, μ × ρ.snd)` for a probability measure `μ`. +* `InformationTheory.klDiv_compProd_left_of_ae`: `KL(μ ⊗ₘ κ, ν ⊗ₘ κ) = KL(μ, ν)` for a kernel `κ` + which is a probability measure on a measurable set of full `μ`- and `ν`-measure. ## Implementation notes @@ -135,4 +137,33 @@ theorem klDiv_prod_eq_klDiv_snd_add (ρ : Measure (α × β)) [IsFiniteMeasure ← Measure.prod_swap (μ := μ), klDiv_map_swap, klDiv_map_swap] at h exact h +/-- `klDiv_compProd_left` for a kernel which is only a probability measure on a measurable set of +full measure for both `μ` and `ν`. -/ +lemma klDiv_compProd_left_of_ae (μ ν : Measure α) [IsFiniteMeasure μ] + [IsFiniteMeasure ν] (κ : Kernel α β) [IsSFiniteKernel κ] {S : Set α} (hS : MeasurableSet S) + (hκ : ∀ a ∈ S, IsProbabilityMeasure (κ a)) (hμ : ∀ᵐ a ∂μ, a ∈ S) (hν : ∀ᵐ a ∂ν, a ∈ S) : + klDiv (μ ⊗ₘ κ) (ν ⊗ₘ κ) = klDiv μ ν := by + classical + rcases isEmpty_or_nonempty β with hβ | ⟨⟨b⟩⟩ + · -- if `β` is empty, then `S` is empty, hence `μ = ν = 0` + have hS_empty (a : α) (ha : a ∈ S) : False := + have := hκ a ha; IsProbabilityMeasure.ne_zero (κ a) (κ a).eq_zero_of_isEmpty + have hμ0 : μ = 0 := ae_eq_bot.1 (Filter.eventually_false_iff_eq_bot.1 (hμ.mono hS_empty)) + have hν0 : ν = 0 := ae_eq_bot.1 (Filter.eventually_false_iff_eq_bot.1 (hν.mono hS_empty)) + simp [hμ0, hν0] + let κ' : Kernel α β := Kernel.piecewise hS κ (Kernel.const α (Measure.dirac b)) + have hκ' : IsMarkovKernel κ' := ⟨fun a ↦ by + by_cases ha : a ∈ S + · simp only [κ', Kernel.piecewise_apply, ha, ite_true] + exact hκ a ha + · simp only [κ', Kernel.piecewise_apply, ha, ite_false, Kernel.const_apply] + infer_instance⟩ + have hμκ : μ ⊗ₘ κ = μ ⊗ₘ κ' := Measure.compProd_congr (by + filter_upwards [hμ] with a ha + simp [κ', Kernel.piecewise_apply, ha]) + have hνκ : ν ⊗ₘ κ = ν ⊗ₘ κ' := Measure.compProd_congr (by + filter_upwards [hν] with a ha + simp [κ', Kernel.piecewise_apply, ha]) + rw [hμκ, hνκ, klDiv_compProd_left] + end InformationTheory From 14b73e82b5b7ce892c6d66c6b56d76c48f916d62 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Fri, 13 Nov 2026 10:23:49 +0100 Subject: [PATCH 4/4] feat: convexity of the KL divergence for finite mixtures, from LML `klDiv_finsetSum_smul_le`, `klDiv_sum_smul_le` and the versions in each argument, proved by induction from `klDiv_add_add_le`. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0196ftMV379vy48QfzHBVNvo --- Statlib/Divergence/KullbackLeibler/Basic.lean | 87 +++++++++++++++++++ 1 file changed, 87 insertions(+) diff --git a/Statlib/Divergence/KullbackLeibler/Basic.lean b/Statlib/Divergence/KullbackLeibler/Basic.lean index 9634b84..b13d107 100644 --- a/Statlib/Divergence/KullbackLeibler/Basic.lean +++ b/Statlib/Divergence/KullbackLeibler/Basic.lean @@ -9,6 +9,8 @@ public import Statlib.Divergence.KullbackLeibler.KLDivFun public import Statlib.Divergence.FDiv.Convex public import Statlib.Divergence.FDiv.Measurable +import Statlib.ForMathlib.InformationTheory.KullbackLeibler.Basic + /-! # Kullback-Leibler divergence @@ -25,6 +27,11 @@ properties of `klDiv` from those of `fDiv`. * `klDiv_add_add_le`: `KL(μ₀ + μ₁, ν₀ + ν₁) ≤ KL(μ₀, ν₀) + KL(μ₁, ν₁)`. * `klDiv_smul_add_smul_le`: **joint convexity** of the Kullback-Leibler divergence, `KL(a • μ₀ + b • μ₁, a • ν₀ + b • ν₁) ≤ a * KL(μ₀, ν₀) + b * KL(μ₁, ν₁)`. +* `klDiv_finsetSum_smul_le`, `klDiv_sum_smul_le`: joint convexity for finite mixtures, + `KL(∑ i, c i • μ i, ∑ i, c i • ν i) ≤ ∑ i, c i * KL(μ i, ν i)`. +* `klDiv_finsetSum_smul_left_le`, `klDiv_sum_smul_left_le`, + `klDiv_finsetSum_smul_right_le`, `klDiv_sum_smul_right_le`: convexity in each argument, for + weights summing to `1`. This file is adapted from the testing-lower-bounds project of Rémy Degenne and Lorenzo Luccioli (https://github.com/RemyDegenne/testing-lower-bounds). @@ -78,4 +85,84 @@ theorem klDiv_smul_add_smul_le (μ₀ μ₁ ν₀ ν₁ : Measure α) [IsFiniteM simp_rw [klDiv_eq_fDiv] exact fDiv_smul_add_smul_le _ _ _ _ a b +section Mixture + +variable {ι : Type*} + +/-- **Joint convexity** of the Kullback-Leibler divergence, for a finite 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)`. -/ +theorem klDiv_finsetSum_smul_le {μ ν : ι → Measure α} [∀ 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 + have h_fin (ρ : ι → Measure α) [∀ i, IsFiniteMeasure (ρ i)] (t : Finset ι) : + IsFiniteMeasure (∑ i ∈ t, (c i : ℝ≥0∞) • ρ i) := + ⟨by simpa using ENNReal.sum_lt_top.mpr fun i _ ↦ + ENNReal.mul_lt_top ENNReal.coe_lt_top (measure_lt_top (ρ i) univ)⟩ + induction s using Finset.induction_on with + | empty => simp + | insert j s hj ih => + have := h_fin μ s + have := h_fin ν s + have := h_fin μ {j} + have := h_fin ν {j} + rw [Finset.sum_insert hj, Finset.sum_insert hj, Finset.sum_insert hj] + calc _ ≤ klDiv ((c j : ℝ≥0∞) • μ j) ((c j : ℝ≥0∞) • ν j) + + klDiv (∑ i ∈ s, (c i : ℝ≥0∞) • μ i) (∑ i ∈ s, (c i : ℝ≥0∞) • ν i) := by + have := klDiv_add_add_le (∑ i ∈ {j}, (c i : ℝ≥0∞) • μ i) + (∑ i ∈ s, (c i : ℝ≥0∞) • μ i) (∑ i ∈ {j}, (c i : ℝ≥0∞) • ν i) + (∑ i ∈ s, (c i : ℝ≥0∞) • ν i) + simpa using this + _ ≤ _ := by + rw [klDiv_smul_same' ENNReal.coe_ne_top] + gcongr + +/-- **Joint convexity** of the Kullback-Leibler divergence, for a finite mixture: 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 klDiv_sum_smul_le [Fintype ι] {μ ν : ι → Measure α} [∀ 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 its first argument**, for a finite mixture +indexed by a `Finset`: for finite measures `μ i`, `ν` and weights `c i ≥ 0` summing to `1`, +`klDiv (∑ i ∈ s, c i • μ i) ν ≤ ∑ i ∈ s, c i * klDiv (μ i) ν`. -/ +theorem klDiv_finsetSum_smul_left_le {μ : ι → Measure α} {ν : Measure α} + [∀ i, IsFiniteMeasure (μ i)] [IsFiniteMeasure ν] {s : Finset ι} {c : ι → ℝ≥0} + (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 weights `c i ≥ 0` summing to `1`, +`klDiv (∑ i, c i • μ i) ν ≤ ∑ i, c i * klDiv (μ i) ν`. -/ +theorem klDiv_sum_smul_left_le [Fintype ι] {μ : ι → Measure α} {ν : Measure α} + [∀ i, IsFiniteMeasure (μ i)] [IsFiniteMeasure ν] {c : ι → ℝ≥0} (hc : ∑ i, c i = 1) : + klDiv (∑ i, (c i : ℝ≥0∞) • μ i) ν ≤ ∑ i, (c i : ℝ≥0∞) * klDiv (μ i) ν := + klDiv_finsetSum_smul_left_le hc + +/-- **Convexity of the Kullback-Leibler divergence in its second argument**, for a finite mixture +indexed by a `Finset`: for finite measures `μ`, `ν i` and weights `c i ≥ 0` summing to `1`, +`klDiv μ (∑ i ∈ s, c i • ν i) ≤ ∑ i ∈ s, c i * klDiv μ (ν i)`. -/ +theorem klDiv_finsetSum_smul_right_le {μ : Measure α} {ν : ι → Measure α} [IsFiniteMeasure μ] + [∀ i, IsFiniteMeasure (ν i)] {s : Finset ι} {c : ι → ℝ≥0} (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 weights `c i ≥ 0` summing to `1`, +`klDiv μ (∑ i, c i • ν i) ≤ ∑ i, c i * klDiv μ (ν i)`. -/ +theorem klDiv_sum_smul_right_le [Fintype ι] {μ : Measure α} {ν : ι → Measure α} + [IsFiniteMeasure μ] [∀ i, IsFiniteMeasure (ν i)] {c : ι → ℝ≥0} (hc : ∑ i, c i = 1) : + klDiv μ (∑ i, (c i : ℝ≥0∞) • ν i) ≤ ∑ i, (c i : ℝ≥0∞) * klDiv μ (ν i) := + klDiv_finsetSum_smul_right_le hc + +end Mixture + end ProbabilityTheory