feat: kernel measurable space and KL generalizations from LML

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

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

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

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 μ ν)

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

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,46 +93,17 @@ 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
   refine fun μ ν hμν => ?_
   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*)