diff --git a/.github/workflows/update.yml b/.github/workflows/update.yml
index 1783e52a..2ce72c83 100644
--- a/.github/workflows/update.yml
+++ b/.github/workflows/update.yml
@@ -6,7 +6,10 @@ on:
   workflow_dispatch:
 
 jobs:
-  bump:
+  # LML gets Mathlib through Statlib: bumping Statlib to its latest `main` commit also moves Mathlib
+  # (and Mathlib's dependencies) to the commits that Statlib pins. Statlib keeps itself close to
+  # Mathlib master with its own updater, and the incompatibilities with Mathlib are tracked there.
+  bump-statlib:
     runs-on: ubuntu-latest
     permissions:
       contents: write
@@ -14,26 +17,46 @@ jobs:
     steps:
       - uses: actions/checkout@v7
 
-      - name: Bump to latest mathlib
+      - name: Install Lean
+        uses: leanprover/lean-action@fe408643ea7367d8c0404a8be3975bb145f5fb64 # v1.7.0
+        with:
+          auto-config: false
+          use-mathlib-cache: false
+
+      - name: Bump Statlib
         id: bump
-        uses: leanprover-community/downstream-reports/.github/actions/bump-to-latest@main
+        run: |
+          rev() { jq -r --arg name "$1" '.packages[] | select(.name == $name) | .rev' lake-manifest.json; }
+          old=$(rev Statlib)
+          lake update Statlib
+          new=$(rev Statlib)
+          if [ "$old" = "$new" ]; then
+            echo "Statlib is already at its latest commit ${new:0:7}."
+            echo "updated=false" >> "$GITHUB_OUTPUT"
+            exit 0
+          fi
+          mathlib=$(rev mathlib)
+          {
+            echo "updated=true"
+            echo "title=chore: bump Statlib to ${new:0:7} (Mathlib ${mathlib:0:7})"
+          } >> "$GITHUB_OUTPUT"
+
+      # Pull requests opened by this workflow do not trigger the Build workflow, so the bump is
+      # checked here, and opened only if LML and its tutorial build without warnings.
+      - name: Build
+        if: steps.bump.outputs.updated == 'true'
+        run: |
+          lake exe cache get
+          lake build --wfail LeanMachineLearning LMLTutorial
 
       - name: Open or update PR
         if: steps.bump.outputs.updated == 'true'
         uses: leanprover-community/downstream-reports/.github/actions/open-bump-pr@main
         with:
-          title:          ${{ steps.bump.outputs.pr-title }}
-          message:        ${{ steps.bump.outputs.bump-description }}
-          commit-message: ${{ steps.bump.outputs.commit-message }}
-
-  open-issue:
-    runs-on: ubuntu-latest
-    permissions:
-      issues: write
-      contents: write
-      pull-requests: write
-    steps:
-      - uses: actions/checkout@v7
-
-      - name: Open or update incompatibility issue and PR
-        uses: leanprover-community/downstream-reports/.github/actions/track-incompatibility@main
+          branch:         statlib-bump
+          title:          ${{ steps.bump.outputs.title }}
+          commit-message: ${{ steps.bump.outputs.title }}
+          body: >
+            Bumps Statlib to its latest `main` commit. LML gets Mathlib through Statlib, so Mathlib
+            moves to the commit that Statlib pins. `lake build --wfail LeanMachineLearning
+            LMLTutorial` passed in the workflow run that opened this pull request.
diff --git a/LMLTutorial/Pages/Martingales.lean b/LMLTutorial/Pages/Martingales.lean
index c7c93e58..fc9cb193 100644
--- a/LMLTutorial/Pages/Martingales.lean
+++ b/LMLTutorial/Pages/Martingales.lean
@@ -91,7 +91,7 @@ This is the Mathlib lemma `Submartingale.ae_tendsto_limitProcess`.
 
 ```lean
 example {Y : ℕ → Ω → ℝ} (hY : Submartingale Y 𝓕 P)
-    {R : ℝ≥0} (hbdd : ∀ n, eLpNorm (Y n) 1 P ≤ R) :
+    (hbdd : ⨆ n, eLpNorm (Y n) 1 P < ∞) :
     ∀ᵐ ω ∂P, Tendsto (Y · ω) atTop (𝓝 (𝓕.limitProcess Y P ω)) :=
   hY.ae_tendsto_limitProcess hbdd
 ```
diff --git a/LeanMachineLearning.lean b/LeanMachineLearning.lean
index 668d1294..54e9d8c9 100644
--- a/LeanMachineLearning.lean
+++ b/LeanMachineLearning.lean
@@ -6,9 +6,7 @@ public import LeanMachineLearning.ForMathlib.Analysis.Convex.Integral
 public import LeanMachineLearning.ForMathlib.Analysis.Convex.Subgradient.Basic
 public import LeanMachineLearning.ForMathlib.Analysis.Convex.Subgradient.Deriv
 public import LeanMachineLearning.ForMathlib.Basic.Unique
-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
@@ -46,7 +44,6 @@ public import LeanMachineLearning.ForMathlib.Probability.Kernel.Composition.Meas
 public import LeanMachineLearning.ForMathlib.Probability.Kernel.Composition.WithDensity
 public import LeanMachineLearning.ForMathlib.Probability.Kernel.CondDistrib
 public import LeanMachineLearning.ForMathlib.Probability.Kernel.IonescuTulcea.Traj
-public import LeanMachineLearning.ForMathlib.Probability.Kernel.MeasurableSpace
 public import LeanMachineLearning.ForMathlib.Probability.Kernel.RadonNikodym
 public import LeanMachineLearning.ForMathlib.Probability.Kernel.Sigma
 public import LeanMachineLearning.ForMathlib.Probability.Moments.SubExponential
diff --git a/LeanMachineLearning/ForMathlib/InformationTheory/KullbackLeibler/ChainRule.lean b/LeanMachineLearning/ForMathlib/InformationTheory/KullbackLeibler/ChainRule.lean
deleted file mode 100644
index 63212eb2..00000000
--- a/LeanMachineLearning/ForMathlib/InformationTheory/KullbackLeibler/ChainRule.lean
+++ /dev/null
@@ -1,136 +0,0 @@
-/-
-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.ChainRule
-public import Mathlib.InformationTheory.KullbackLeibler.DataProcessing
-public import Mathlib.Probability.Kernel.Composition.RadonNikodym
-
-import LeanMachineLearning.ForMathlib.Probability.Kernel.Composition.Lemmas
-import LeanMachineLearning.ForMathlib.Probability.Kernel.Composition.MapComap
-import Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous
-
-/-!
-# The Kullback–Leibler divergence of composition-products, in integrated form
-
-The chain rule `klDiv_compProd_eq_add` expresses the conditional divergence as
-`klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)`. When the target space of the kernels is countably generated (or the
-source is countable), the function `a ↦ klDiv (κ a) (η a)` is measurable
-(`measurable_klDiv_kernel`) and the conditional divergence is its integral.
-
-## Main statements
-
-* `klDiv_compProd_right_eq_lintegral`: `klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η) = ∫⁻ a, klDiv (κ a) (η a) ∂μ`.
-* `klDiv_compProd_eq_add_lintegral`:
-  `klDiv (μ ⊗ₘ κ) (ν ⊗ₘ η) = klDiv μ ν + ∫⁻ a, klDiv (κ a) (η a) ∂μ`.
--/
-
-@[expose] public section
-
-open MeasureTheory ProbabilityTheory
-open scoped ENNReal
-
-namespace InformationTheory
-
-variable {α β γ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
-
-section kernel
-
-variable [MeasurableSpace.CountableOrCountablyGenerated α β]
-
-/-- For finite kernels with countably generated target, `a ↦ klDiv (κ a) (η a)` is measurable. -/
-lemma measurable_klDiv_kernel (κ η : Kernel α β) [IsFiniteKernel κ] [IsFiniteKernel η] :
-    Measurable fun a ↦ klDiv (κ a) (η a) := by
-  classical
-  have h_meas : Measurable fun a ↦
-      ∫⁻ b, ENNReal.ofReal (klFun (κ.rnDeriv η a b).toReal) ∂(η a) :=
-    Measurable.lintegral_kernel_prod_right
-      ((measurable_klFun.comp (Kernel.measurable_rnDeriv κ η).ennreal_toReal).ennreal_ofReal)
-  have h_eq : ∀ a, klDiv (κ a) (η a) = if κ a ≪ η a then
-      ∫⁻ b, ENNReal.ofReal (klFun (κ.rnDeriv η a b).toReal) ∂(η a) else ∞ := by
-    intro a
-    split_ifs with hac
-    · rw [klDiv_eq_lintegral_klFun_of_ac hac]
-      refine lintegral_congr_ae ?_
-      filter_upwards [Kernel.rnDeriv_eq_rnDeriv_measure (κ := κ) (η := η) (a := a)] with b hb
-      rw [hb]
-    · exact klDiv_of_not_ac hac
-  simp_rw [h_eq]
-  exact Measurable.ite (Kernel.measurableSet_absolutelyContinuous κ η) h_meas measurable_const
-
-/-- Integrated form of the conditional Kullback–Leibler divergence:
-`klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η) = ∫⁻ a, klDiv (κ a) (η a) ∂μ`. -/
-lemma klDiv_compProd_right_eq_lintegral (μ : Measure α) [IsFiniteMeasure μ] (κ η : Kernel α β)
-    [IsFiniteKernel κ] [IsFiniteKernel η] :
-    klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η) = ∫⁻ a, klDiv (κ a) (η a) ∂μ := by
-  by_cases h_ac : μ ⊗ₘ κ ≪ μ ⊗ₘ η
-  · rw [klDiv_eq_lintegral_klFun_of_ac h_ac]
-    have h_ae := Measure.absolutelyContinuous_compProd_right_iff.mp h_ac
-    calc ∫⁻ p, ENNReal.ofReal (klFun ((μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) p).toReal) ∂(μ ⊗ₘ η)
-        = ∫⁻ p, ENNReal.ofReal (klFun (κ.rnDeriv η p.1 p.2).toReal) ∂(μ ⊗ₘ η) := by
-          refine lintegral_congr_ae ?_
-          filter_upwards [rnDeriv_measure_compProd_right μ κ η] with p hp
-          rw [hp]
-      _ = ∫⁻ a, ∫⁻ b, ENNReal.ofReal (klFun (κ.rnDeriv η a b).toReal) ∂(η a) ∂μ :=
-          Measure.lintegral_compProd
-            ((measurable_klFun.comp (Kernel.measurable_rnDeriv κ η).ennreal_toReal).ennreal_ofReal)
-      _ = ∫⁻ a, klDiv (κ a) (η a) ∂μ := by
-          refine lintegral_congr_ae ?_
-          filter_upwards [h_ae] with a ha
-          rw [klDiv_eq_lintegral_klFun_of_ac ha]
-          refine lintegral_congr_ae ?_
-          filter_upwards [Kernel.rnDeriv_eq_rnDeriv_measure (κ := κ) (η := η) (a := a)] with b hb
-          rw [hb]
-  · rw [klDiv_of_not_ac h_ac, Measure.absolutelyContinuous_compProd_right_iff, ae_iff] at *
-    symm
-    rw [eq_top_iff]
-    calc (∞ : ℝ≥0∞) = ∫⁻ _ in {a | ¬ κ a ≪ η a}, ∞ ∂μ := by
-          rw [setLIntegral_const, ENNReal.top_mul h_ac]
-      _ ≤ ∫⁻ a in {a | ¬ κ a ≪ η a}, klDiv (κ a) (η a) ∂μ :=
-          setLIntegral_mono' (Kernel.measurableSet_absolutelyContinuous κ η).compl
-            fun a ha ↦ by rw [klDiv_of_not_ac ha]
-      _ ≤ ∫⁻ a, klDiv (κ a) (η a) ∂μ := setLIntegral_le_lintegral _ _
-
-/-- **Chain rule** for the Kullback–Leibler divergence, in integrated form:
-`klDiv (μ ⊗ₘ κ) (ν ⊗ₘ η) = klDiv μ ν + ∫⁻ a, klDiv (κ a) (η a) ∂μ`. -/
-lemma klDiv_compProd_eq_add_lintegral (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν]
-    (κ η : Kernel α β) [IsMarkovKernel κ] [IsMarkovKernel η] :
-    klDiv (μ ⊗ₘ κ) (ν ⊗ₘ η) = klDiv μ ν + ∫⁻ a, klDiv (κ a) (η a) ∂μ := by
-  rw [klDiv_compProd_eq_add, klDiv_compProd_right_eq_lintegral]
-
-omit [MeasurableSpace.CountableOrCountablyGenerated α β] in
-/-- `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 kernel
-
-end InformationTheory
diff --git a/LeanMachineLearning/ForMathlib/InformationTheory/KullbackLeibler/Convex.lean b/LeanMachineLearning/ForMathlib/InformationTheory/KullbackLeibler/Convex.lean
deleted file mode 100644
index 44918b88..00000000
--- a/LeanMachineLearning/ForMathlib/InformationTheory/KullbackLeibler/Convex.lean
+++ /dev/null
@@ -1,175 +0,0 @@
-/-
-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
-import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.DataProcessing
-
-/-!
-# 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, sum_apply,
-      ← Finset.sum_coe_sort s]
-    exact Finset.sum_congr rfl fun i _ ↦ by rw [hρ i, 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
diff --git a/LeanMachineLearning/ForMathlib/InformationTheory/KullbackLeibler/DataProcessing.lean b/LeanMachineLearning/ForMathlib/InformationTheory/KullbackLeibler/DataProcessing.lean
index b3de4794..b8580395 100644
--- a/LeanMachineLearning/ForMathlib/InformationTheory/KullbackLeibler/DataProcessing.lean
+++ b/LeanMachineLearning/ForMathlib/InformationTheory/KullbackLeibler/DataProcessing.lean
@@ -6,6 +6,7 @@ Authors: Rémy Degenne
 module
 
 public import Mathlib.InformationTheory.KullbackLeibler.DataProcessing
+public import Statlib.ForMathlib.InformationTheory.KullbackLeibler.DataProcessing
 
 import Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
 
@@ -19,10 +20,11 @@ conditional expectation of the density `∂μ/∂ν` given `g`
 
 * `klDiv_map_eq_lintegral_klFun_condExp`: the divergence of the images by a measurable map, as
   the integral of `klFun` of the conditional expectation of the density.
-* `klDiv_map_measurableEmbedding`, `klDiv_map_measurableEquiv`: the divergence is invariant under
-  measurable embeddings and measurable equivalences.
-* `klDiv_le_compProd`, `klDiv_comp_le_compProd`: data processing inequalities for the two
-  projections of `μ ⊗ₘ κ` and `ν ⊗ₘ η`.
+* `klDiv_map_measurableEquiv`: the divergence is invariant under measurable equivalences.
+
+Invariance under measurable embeddings (`klDiv_map_measurableEmbedding`) and the data processing
+inequalities for the two projections of `μ ⊗ₘ κ` and `ν ⊗ₘ η` (`le_klDiv_compProd`,
+`klDiv_comp_le_compProd`) are in Statlib.
 -/
 
 @[expose] public section
@@ -58,43 +60,12 @@ end CondExp
 
 section Map
 
-/-- The Kullback–Leibler divergence is invariant under measurable embeddings. -/
-lemma klDiv_map_measurableEmbedding (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν]
-    {f : α → β} (hf : MeasurableEmbedding f) :
-    klDiv (μ.map f) (ν.map f) = klDiv μ ν := by
-  refine le_antisymm (klDiv_map_le μ ν hf.measurable) ?_
-  rcases isEmpty_or_nonempty α with hα | hα
-  · simp [μ.eq_zero_of_isEmpty, ν.eq_zero_of_isEmpty]
-  have h := klDiv_map_le (μ.map f) (ν.map f) hf.measurable_invFun
-  rwa [Measure.map_map hf.measurable_invFun hf.measurable,
-    Measure.map_map hf.measurable_invFun hf.measurable, hf.leftInverse_invFun.comp_eq_id,
-    Measure.map_id, Measure.map_id] at h
-
 /-- The Kullback–Leibler divergence is invariant under measurable equivalences. -/
 lemma klDiv_map_measurableEquiv (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν]
     (e : α ≃ᵐ β) :
     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
-
 end Map
 
 end InformationTheory
diff --git a/LeanMachineLearning/ForMathlib/InformationTheory/KullbackLeibler/MapSequence.lean b/LeanMachineLearning/ForMathlib/InformationTheory/KullbackLeibler/MapSequence.lean
index 95411aee..0ce61f2c 100644
--- a/LeanMachineLearning/ForMathlib/InformationTheory/KullbackLeibler/MapSequence.lean
+++ b/LeanMachineLearning/ForMathlib/InformationTheory/KullbackLeibler/MapSequence.lean
@@ -5,10 +5,10 @@ Authors: Rémy Degenne
 -/
 module
 
-public import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.DataProcessing
-public import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.Restrict
-public import Mathlib.MeasureTheory.Integral.Indicator
-public import Mathlib.Probability.Martingale.Convergence
+public import Mathlib.InformationTheory.KullbackLeibler.DataProcessing
+
+import Statlib.Divergence.FDiv.TrimApprox
+import Statlib.Divergence.KullbackLeibler.Basic
 
 /-!
 # The Kullback–Leibler divergence along a generating sequence of maps
@@ -25,14 +25,9 @@ divergences of their images by the `g n`:
 
 ## Implementation notes
 
-The inequality `≥` is the data-processing inequality. For `≤`, if `μ ≪ ν` the divergences of
-the images are the integrals of `klFun` of the conditional expectations of the density `∂μ/∂ν`
-given `comap (g n)` (`klDiv_map_eq_lintegral_klFun_condExp`), which converge almost everywhere
-to the density by Lévy's upward theorem, and Fatou's lemma concludes. If `μ` is not absolutely
-continuous with respect to `ν`, a set `A` with `ν A = 0 < μ A` is approximated by
-`comap (g n)`-measurable sets `B n` (again by Lévy's upward theorem, applied to the indicator of
-`A` under `μ + ν`), and the lower bound `μ B * log (μ B / ν B) + ν B - μ B ≤ klDiv` on `B n`
-shows that the divergences of the images tend to infinity.
+The inequality `≥` is the data-processing inequality. For `≤`, the divergences of the images
+converge to `klDiv μ ν`: this is Statlib's `tendsto_fDiv_map_of_iSup_comap_eq` for the
+f-divergence `fDiv klDivFun`, which is `klDiv` (`klDiv_eq_fDiv`).
 -/
 
 @[expose] public section
@@ -53,130 +48,9 @@ lemma klDiv_eq_iSup_map {β : ℕ → Type*} [mβ : ∀ n, MeasurableSpace (β n
     (hmono : Monotone fun n ↦ (mβ n).comap (g n))
     (hsup : ⨆ n, (mβ n).comap (g n) = m0) :
     klDiv μ ν = ⨆ n, klDiv (μ.map (g n)) (ν.map (g n)) := by
-  let ℱ : Filtration ℕ m0 := ⟨fun n ↦ (mβ n).comap (g n), hmono, fun n ↦ (hg n).comap_le⟩
-  have hℱ : ∀ n, ℱ n = (mβ n).comap (g n) := fun _ ↦ rfl
-  have hℱ_sup : (⨆ n, ℱ n) = m0 := hsup
   refine le_antisymm ?_ (iSup_le fun n ↦ klDiv_map_le μ ν (hg n))
-  by_cases hμν : μ ≪ ν
-  · -- Lévy's upward theorem and Fatou's lemma
-    let f : α → ℝ := fun x ↦ (μ.rnDeriv ν x).toReal
-    have hf_int : Integrable f ν := Measure.integrable_toReal_rnDeriv
-    have hf_meas : StronglyMeasurable[⨆ n, ℱ n] f :=
-      (Measure.measurable_rnDeriv μ ν).ennreal_toReal.stronglyMeasurable.mono hℱ_sup.symm.le
-    have hlim := hf_int.tendsto_ae_condExp (ℱ := ℱ) hf_meas
-    have hmeas : ∀ n, Measurable fun x ↦ ENNReal.ofReal (klFun ((ν[f | ℱ n]) x)) := fun n ↦
-      (measurable_klFun.comp
-        ((stronglyMeasurable_condExp (m := ℱ n)).measurable.mono (ℱ.le n) le_rfl)).ennreal_ofReal
-    calc klDiv μ ν = ∫⁻ x, ENNReal.ofReal (klFun (f x)) ∂ν := klDiv_eq_lintegral_klFun_of_ac hμν
-      _ = ∫⁻ x, liminf (fun n ↦ ENNReal.ofReal (klFun ((ν[f | ℱ n]) x))) atTop ∂ν := by
-          refine lintegral_congr_ae ?_
-          filter_upwards [hlim] with x hx
-          exact ((ENNReal.continuous_ofReal.tendsto _).comp
-            ((continuous_klFun.tendsto _).comp hx)).liminf_eq.symm
-      _ ≤ liminf (fun n ↦ ∫⁻ x, ENNReal.ofReal (klFun ((ν[f | ℱ n]) x)) ∂ν) atTop :=
-          lintegral_liminf_le hmeas
-      _ ≤ ⨆ n, ∫⁻ x, ENNReal.ofReal (klFun ((ν[f | ℱ n]) x)) ∂ν :=
-          le_trans liminf_le_limsup limsup_le_iSup
-      _ = ⨆ n, klDiv (μ.map (g n)) (ν.map (g n)) :=
-          iSup_congr fun n ↦ (klDiv_map_eq_lintegral_klFun_condExp hμν (hg n)).symm
-  · -- the divergences of the images tend to infinity
-    rw [klDiv_of_not_ac hμν, top_le_iff, iSup_eq_top]
-    obtain ⟨A, hA, hνA, hμA⟩ : ∃ A, MeasurableSet A ∧ ν A = 0 ∧ μ A ≠ 0 := by
-      by_contra! h
-      exact hμν (Measure.AbsolutelyContinuous.mk fun A hA hνA ↦ h A hA hνA)
-    -- approximation of `A` by `comap (g n)`-measurable sets, by Lévy's upward theorem
-    let ρ : Measure α := μ + ν
-    let φ : α → ℝ := A.indicator fun _ ↦ (1 : ℝ)
-    have hφ_int : Integrable φ ρ := (integrable_const (1 : ℝ)).indicator hA
-    have hφ_meas : StronglyMeasurable[⨆ n, ℱ n] φ :=
-      (measurable_const.indicator hA).stronglyMeasurable.mono hℱ_sup.symm.le
-    have hlim := hφ_int.tendsto_ae_condExp (ℱ := ℱ) hφ_meas
-    set B : ℕ → Set α := fun n ↦ {x | (2⁻¹ : ℝ) < (ρ[φ | ℱ n]) x} with hB
-    have hB_meas : ∀ n, MeasurableSet[ℱ n] (B n) := fun n ↦ by
-      have : B n = (ρ[φ | ℱ n]) ⁻¹' Set.Ioi 2⁻¹ := by ext; simp [hB]
-      rw [this]
-      exact (stronglyMeasurable_condExp (m := ℱ n)).measurable measurableSet_Ioi
-    have hB_meas0 : ∀ n, MeasurableSet (B n) := fun n ↦ ℱ.le n _ (hB_meas n)
-    have hB_lim : ∀ᵐ x ∂ρ, ∀ᶠ n in atTop, x ∈ B n ↔ x ∈ A := by
-      filter_upwards [hlim] with x hx
-      by_cases hxA : x ∈ A
-      · have h1 : Tendsto (fun n ↦ (ρ[φ | ℱ n]) x) atTop (𝓝 1) := by simpa [φ, hxA] using hx
-        filter_upwards [h1.eventually (lt_mem_nhds (by norm_num : (2⁻¹ : ℝ) < 1))] with n hn
-        simp [hB, hn, hxA]
-      · have h0 : Tendsto (fun n ↦ (ρ[φ | ℱ n]) x) atTop (𝓝 0) := by simpa [φ, hxA] using hx
-        filter_upwards [h0.eventually (gt_mem_nhds (by norm_num : (0 : ℝ) < 2⁻¹))] with n hn
-        simp [hB, hxA, hn.le]
-    have hμB : Tendsto (fun n ↦ μ (B n)) atTop (𝓝 (μ A)) :=
-      tendsto_measure_of_ae_tendsto_indicator atTop hA hB_meas0 MeasurableSet.univ
-        (measure_ne_top μ _) (Eventually.of_forall fun _ ↦ Set.subset_univ _)
-        (ae_add_measure_iff.1 hB_lim).1
-    have hνB : Tendsto (fun n ↦ ν (B n)) atTop (𝓝 0) := by
-      rw [← hνA]
-      exact tendsto_measure_of_ae_tendsto_indicator atTop hA hB_meas0 MeasurableSet.univ
-        (measure_ne_top ν _) (Eventually.of_forall fun _ ↦ Set.subset_univ _)
-        (ae_add_measure_iff.1 hB_lim).2
-    -- lower bounds on the divergences of the images
-    have hBC : ∀ n, ∃ C : Set (β n), MeasurableSet C ∧ g n ⁻¹' C = B n := fun n ↦
-      MeasurableSpace.measurableSet_comap.1 (hB_meas n)
-    have hkey n : ENNReal.ofReal (μ.real (B n) * Real.log (μ.real (B n) / ν.real (B n)) +
-        ν.real (B n) - μ.real (B n)) ≤ klDiv (μ.map (g n)) (ν.map (g n)) := by
-      obtain ⟨C, hC, hCB⟩ := hBC n
-      refine le_trans ?_ (klDiv_restrict_le hC)
-      have := mul_log_le_klDiv ((μ.map (g n)).restrict C) ((ν.map (g n)).restrict C)
-      simpa only [measureReal_def, Measure.restrict_apply_univ, Measure.map_apply (hg n) hC, hCB]
-        using this
-    have hkey' n (h0 : ν (B n) = 0) (hpos : μ (B n) ≠ 0) :
-        klDiv (μ.map (g n)) (ν.map (g n)) = ⊤ := by
-      obtain ⟨C, hC, hCB⟩ := hBC n
-      refine klDiv_of_not_ac fun hac ↦ hpos ?_
-      have := hac (show (ν.map (g n)) C = 0 by rw [Measure.map_apply (hg n) hC, hCB, h0])
-      rwa [Measure.map_apply (hg n) hC, hCB] at this
-    -- conclusion
-    intro K hK
-    set a : ℝ := μ.real A with ha_def
-    have ha : 0 < a := ENNReal.toReal_pos hμA (measure_ne_top μ A)
-    set δ : ℝ := Real.exp (-(2 / a) * (K.toReal + 2)) with hδ_def
-    have hδ : 0 < δ := Real.exp_pos _
-    have hδ1 : δ ≤ 1 := by
-      rw [hδ_def, Real.exp_le_one_iff]
-      have : 0 ≤ K.toReal + 2 := by positivity
-      nlinarith [div_pos (by norm_num : (0 : ℝ) < 2) ha]
-    have hμB' : Tendsto (fun n ↦ μ.real (B n)) atTop (𝓝 a) :=
-      (ENNReal.tendsto_toReal (measure_ne_top μ A)).comp hμB
-    have hνB' : Tendsto (fun n ↦ ν.real (B n)) atTop (𝓝 0) := by
-      have := (ENNReal.tendsto_toReal ENNReal.zero_ne_top).comp hνB
-      simpa [Function.comp_def, measureReal_def] using this
-    have h_ev : ∀ᶠ n in atTop, a / 2 ≤ μ.real (B n) ∧ ν.real (B n) ≤ δ :=
-      (hμB'.eventually (le_mem_nhds (by linarith))).and (hνB'.eventually (ge_mem_nhds hδ))
-    obtain ⟨n, hna, hnδ⟩ := h_ev.exists
-    refine ⟨n, ?_⟩
-    by_cases h0 : ν (B n) = 0
-    · rw [hkey' n h0 (fun h ↦ by simp [measureReal_def, h] at hna; linarith)]
-      exact hK
-    · have hνpos : 0 < ν.real (B n) := ENNReal.toReal_pos h0 (measure_ne_top ν _)
-      have hμpos : 0 < μ.real (B n) := by linarith
-      refine lt_of_lt_of_le ?_ (hkey n)
-      rw [← ENNReal.ofReal_toReal hK.ne, ENNReal.ofReal_lt_ofReal_iff_of_nonneg
-        ENNReal.toReal_nonneg]
-      -- `x log (x / y) + y - x ≥ -1 - x log y ≥ -1 + (a / 2) (-log δ) = K.toReal + 1`
-      have h1 : μ.real (B n) - 1 ≤ μ.real (B n) * Real.log (μ.real (B n)) := by
-        have := Real.one_sub_inv_le_log_of_pos hμpos
-        calc μ.real (B n) - 1 = μ.real (B n) * (1 - (μ.real (B n))⁻¹) := by
-              field_simp
-          _ ≤ _ := by gcongr
-      have h2 : Real.log (ν.real (B n)) ≤ Real.log δ := Real.log_le_log hνpos hnδ
-      have h3 : Real.log δ = -(2 / a) * (K.toReal + 2) := by rw [hδ_def, Real.log_exp]
-      have h4 : (a / 2) * (-Real.log δ) = K.toReal + 2 := by
-        rw [h3]
-        field_simp
-      have h5 : (a / 2) * (-Real.log (ν.real (B n))) ≤
-          μ.real (B n) * (-Real.log (ν.real (B n))) := by
-        have hlog : 0 ≤ -Real.log (ν.real (B n)) := by
-          have := Real.log_nonpos hνpos.le (hnδ.trans hδ1)
-          linarith
-        exact mul_le_mul_of_nonneg_right hna hlog
-      rw [Real.log_div hμpos.ne' hνpos.ne']
-      nlinarith [mul_le_mul_of_nonneg_left (neg_le_neg h2) (by positivity : (0 : ℝ) ≤ a / 2),
-        measureReal_nonneg (μ := ν) (s := B n)]
+  have h := tendsto_fDiv_map_of_iSup_comap_eq (f := klDivFun) (μ := μ) (ν := ν) hg hmono hsup
+  simp_rw [← klDiv_eq_fDiv] at h
+  exact le_of_tendsto' h fun n ↦ le_iSup (fun n ↦ klDiv (μ.map (g n)) (ν.map (g n))) n
 
 end InformationTheory
diff --git a/LeanMachineLearning/ForMathlib/InformationTheory/KullbackLeibler/Restrict.lean b/LeanMachineLearning/ForMathlib/InformationTheory/KullbackLeibler/Restrict.lean
index 1da60cd8..37878f25 100644
--- a/LeanMachineLearning/ForMathlib/InformationTheory/KullbackLeibler/Restrict.lean
+++ b/LeanMachineLearning/ForMathlib/InformationTheory/KullbackLeibler/Restrict.lean
@@ -8,6 +8,9 @@ module
 public import LeanMachineLearning.ForMathlib.MeasureTheory.Measure.Decomposition.Lebesgue
 public import Mathlib.InformationTheory.KullbackLeibler.Basic
 
+import Statlib.Divergence.KullbackLeibler.Basic
+import Statlib.ForMathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
+
 /-!
 # The Kullback–Leibler divergence of restrictions of measures
 
@@ -51,16 +54,8 @@ lemma klDiv_restrict_of_ac (hμν : μ.restrict s ≪ ν.restrict s) (hs : Measu
 /-- The divergence is the sum of the divergences of the restrictions to a measurable set and to
 its complement. -/
 lemma klDiv_restrict_add_restrict_compl (hs : MeasurableSet s) :
-    klDiv (μ.restrict s) (ν.restrict s) + klDiv (μ.restrict sᶜ) (ν.restrict sᶜ) = klDiv μ ν := by
-  by_cases hμν : μ ≪ ν
-  · rw [klDiv_restrict_of_ac (hμν.restrict s) hs, klDiv_restrict_of_ac (hμν.restrict sᶜ) hs.compl,
-      klDiv_eq_lintegral_klFun_of_ac hμν, lintegral_add_compl _ hs]
-  · rw [klDiv_of_not_ac hμν, ENNReal.add_eq_top]
-    by_contra! h
-    refine hμν ?_
-    rw [← Measure.restrict_add_restrict_compl (μ := μ) hs,
-      ← Measure.restrict_add_restrict_compl (μ := ν) hs]
-    exact (klDiv_ne_top_iff.1 h.1).1.add (klDiv_ne_top_iff.1 h.2).1
+    klDiv (μ.restrict s) (ν.restrict s) + klDiv (μ.restrict sᶜ) (ν.restrict sᶜ) = klDiv μ ν :=
+  (ProbabilityTheory.klDiv_eq_klDiv_restrict_add_klDiv_restrict_compl μ ν hs).symm
 
 /-- Restricting both measures to a measurable set does not increase the divergence. -/
 lemma klDiv_restrict_le (hs : MeasurableSet s) :
diff --git a/LeanMachineLearning/ForMathlib/MeasureTheory/Measure/Decomposition/Lebesgue.lean b/LeanMachineLearning/ForMathlib/MeasureTheory/Measure/Decomposition/Lebesgue.lean
index e93a8f66..fed3ff92 100644
--- a/LeanMachineLearning/ForMathlib/MeasureTheory/Measure/Decomposition/Lebesgue.lean
+++ b/LeanMachineLearning/ForMathlib/MeasureTheory/Measure/Decomposition/Lebesgue.lean
@@ -13,8 +13,6 @@ public import Mathlib.MeasureTheory.Measure.SubFinite
 
 ## Main statements
 
-* `Measure.rnDeriv_restrict_restrict`: the Radon-Nikodym derivative of `μ.restrict s` with
-  respect to `ν.restrict s` is `μ.rnDeriv ν`, `ν.restrict s`-almost everywhere.
 * `Measure.sub_apply_eq_rnDeriv_add_singularPart`: for finite measures,
   `(μ - ν) s = ν.withDensity (μ.rnDeriv ν - 1) s + μ.singularPart ν s`.
 -/
@@ -27,15 +25,6 @@ namespace MeasureTheory.Measure
 
 variable {α : Type*} {mα : MeasurableSpace α} {μ ν : Measure α}
 
-/-- The Radon–Nikodym derivative of `μ.restrict s` with respect to `ν.restrict s` is the
-Radon–Nikodym derivative of `μ` with respect to `ν`, `ν.restrict s`-almost everywhere. -/
-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).mono le_rfl restrict_le_self) ?_).symm
-  rw [← restrict_withDensity hs, ← restrict_add, ← haveLebesgueDecomposition_add μ ν]
-
 lemma sub_apply_eq_rnDeriv_add_singularPart [IsFiniteMeasure μ] [IsFiniteMeasure ν] (s : Set α) :
     (μ - ν) s = ν.withDensity (fun a ↦ μ.rnDeriv ν a - 1) s + μ.singularPart ν s := by
   have hμ : μ = ν.withDensity (fun a ↦ μ.rnDeriv ν a) + μ.singularPart ν := by
diff --git a/LeanMachineLearning/ForMathlib/Probability/Kernel/MeasurableSpace.lean b/LeanMachineLearning/ForMathlib/Probability/Kernel/MeasurableSpace.lean
deleted file mode 100644
index a984f069..00000000
--- a/LeanMachineLearning/ForMathlib/Probability/Kernel/MeasurableSpace.lean
+++ /dev/null
@@ -1,37 +0,0 @@
-/-
-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
-
--/
-
-@[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
-
-@[fun_prop]
-lemma Kernel.measurable_const : Measurable (@Kernel.const 𝓧 𝓨 m𝓧 m𝓨) := by
-  rw [measurable_kernel_iff]
-  simp only [const_apply]
-  fun_prop
-
-end ProbabilityTheory
diff --git a/LeanMachineLearning/ForMathlib/Probability/Moments/SubExponential.lean b/LeanMachineLearning/ForMathlib/Probability/Moments/SubExponential.lean
index accf5f51..0259e2c6 100644
--- a/LeanMachineLearning/ForMathlib/Probability/Moments/SubExponential.lean
+++ b/LeanMachineLearning/ForMathlib/Probability/Moments/SubExponential.lean
@@ -146,11 +146,11 @@ lemma ae_forall_memLp_exp_mul (h : HasSubexponentialMGF X V b κ ν) (p : ℝ≥
     continuous_exp.comp_aestronglyMeasurable (hm.const_mul t)
   by_cases hp : p = 0
   · simp [hp, hmeas]
-  rw [memLp_iff, eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top (mod_cast hp) (by simp) hmeas,
+  rw [memLp_iff, eLpNorm_lt_top_iff_lintegral_rpow_eNorm_lt_top (mod_cast hp) (by simp) hmeas,
     ENNReal.coe_toReal]
   have hf := (hi (p * t) ht).lintegral_lt_top
   convert! hf using 3 with ω
-  rw [enorm_eq_ofReal (by positivity), ENNReal.ofReal_rpow_of_nonneg (by positivity),
+  rw [eNorm_eq_ofReal (by positivity), ENNReal.ofReal_rpow_of_nonneg (by positivity),
     ← exp_mul, mul_comm, ← mul_assoc]
   positivity
 
@@ -161,12 +161,12 @@ lemma memLp_exp_mul (h : HasSubexponentialMGF X V b κ ν) {t : ℝ} (p : ℝ≥
     continuous_exp.comp_aestronglyMeasurable (h.aestronglyMeasurable.const_mul t)
   by_cases hp0 : p = 0
   · simp [hp0, hmeas]
-  rw [memLp_iff, eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top (mod_cast hp0) (by simp) hmeas]
+  rw [memLp_iff, eLpNorm_lt_top_iff_lintegral_rpow_eNorm_lt_top (mod_cast hp0) (by simp) hmeas]
   simp only [ENNReal.coe_toReal]
   have h' := (h.integrable_exp_mul (p * t) ht).2
   rw [hasFiniteIntegral_def] at h'
   convert! h' using 3 with ω
-  rw [enorm_eq_ofReal (by positivity), enorm_eq_ofReal (by positivity),
+  rw [eNorm_eq_ofReal (by positivity), eNorm_eq_ofReal (by positivity),
     ENNReal.ofReal_rpow_of_nonneg (by positivity), ← exp_mul, mul_comm, ← mul_assoc]
   positivity
 
diff --git a/LeanMachineLearning/SequentialLearning/Algorithm.lean b/LeanMachineLearning/SequentialLearning/Algorithm.lean
index 956fe1cf..443f199f 100644
--- a/LeanMachineLearning/SequentialLearning/Algorithm.lean
+++ b/LeanMachineLearning/SequentialLearning/Algorithm.lean
@@ -9,7 +9,7 @@ public import LeanMachineLearning.ForMathlib.Basic.Unique
 public import LeanMachineLearning.ForMathlib.MeasureTheory.MeasurableSpace.Basic
 public import LeanMachineLearning.ForMathlib.MeasureTheory.MeasurableSpace.Instances
 public import LeanMachineLearning.ForMathlib.Probability.Kernel.IonescuTulcea.Traj
-public import LeanMachineLearning.ForMathlib.Probability.Kernel.MeasurableSpace
+public import Statlib.ForMathlib.Probability.Kernel.MeasurableSpace
 
 /-!
 # Algorithms and environments
diff --git a/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling/Tendsto.lean b/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling/Tendsto.lean
index c0408d5c..f1a2d6fa 100644
--- a/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling/Tendsto.lean
+++ b/LeanMachineLearning/SequentialLearning/Algorithms/RandomSampling/Tendsto.lean
@@ -209,7 +209,6 @@ lemma feedback_tendsto_any_const_eval [PseudoMetricSpace 𝓨] [BorelSpace 𝓨]
   refine measure_congr ?_
   let g : ((Iic n) → 𝓨) → ℝ := fun r ↦ (fun i ↦ dist (r i) (f a)).min
   filter_upwards [comp_feedback_ae_eq_eval h g] with ω hω
-  simp only [eq_iff_iff]
   simp [g, hω]
 
 variable {R : ℕ → Ω → ℝ} {f : 𝓐 → ℝ} (hfc : Continuous f) {a : 𝓐}
diff --git a/LeanMachineLearning/SequentialLearning/DivergenceDecomposition.lean b/LeanMachineLearning/SequentialLearning/DivergenceDecomposition.lean
index 75ae3aff..174d3914 100644
--- a/LeanMachineLearning/SequentialLearning/DivergenceDecomposition.lean
+++ b/LeanMachineLearning/SequentialLearning/DivergenceDecomposition.lean
@@ -5,12 +5,12 @@ Authors: Rémy Degenne
 -/
 module
 
-public import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.ChainRule
 public import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.CompProd
 public import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.MapSequence
 public import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.Restrict
 public import LeanMachineLearning.ForMathlib.MeasureTheory.MeasurableSpace.Constructions
 public import LeanMachineLearning.SequentialLearning.StationaryEnv
+public import Statlib.Divergence.KullbackLeibler.CondKL
 
 /-!
 # The divergence decomposition
@@ -148,8 +148,8 @@ lemma IsAlgEnvSeq.klDiv_map_history_bandit [MeasurableSpace.CountablyGenerated 
       ∑ t ∈ range M, ∫⁻ ω, klDiv (κ (A t ω)) (κ' (A t ω)) ∂P := by
   rw [h.klDiv_map_history_compProd_bandit h']
   refine sum_congr rfl fun t _ ↦ ?_
-  rw [klDiv_compProd_right_eq_lintegral,
-    lintegral_map (measurable_klDiv_kernel κ κ') (h.measurable_action t)]
+  rw [← condKL, condKL_eq_lintegral,
+    lintegral_map (measurable_klDiv κ κ') (h.measurable_action t)]
 
 /-- **Divergence decomposition** for trajectories of a single algorithm against two stationary
 bandit environments. -/
@@ -171,8 +171,8 @@ lemma IsAlgEnvSeq.klDiv_map_trajectory_bandit [MeasurableSpace.CountablyGenerate
       ∑' t : ℕ, ∫⁻ ω, klDiv (κ (A t ω)) (κ' (A t ω)) ∂P := by
   rw [h.klDiv_map_trajectory_compProd_bandit h']
   refine tsum_congr fun t ↦ ?_
-  rw [klDiv_compProd_right_eq_lintegral,
-    lintegral_map (measurable_klDiv_kernel κ κ') (h.measurable_action t)]
+  rw [← condKL, condKL_eq_lintegral,
+    lintegral_map (measurable_klDiv κ κ') (h.measurable_action t)]
 
 end Bandit
 
diff --git a/lake-manifest.json b/lake-manifest.json
index 07ddf6f5..4f263d69 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,36 +1,86 @@
 {"version": "1.3.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover-community/mathlib4",
+ [{"url": "https://github.com/leanprover/verso",
    "type": "git",
    "subDir": null,
-   "scope": "leanprover-community",
-   "rev": "6135ffb78e8bcd3fcc8ec02f3f82ea0b0737358b",
-   "name": "mathlib",
+   "scope": "",
+   "rev": "71a2035b44e7f54a797ce799fd1b03cdd3a44684",
+   "name": "verso",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "6135ffb78e8bcd3fcc8ec02f3f82ea0b0737358b",
+   "inputRev": "v4.36.0-rc2",
    "inherited": false,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/verso",
+  {"url": "https://github.com/stat-lib/statlib",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "71a2035b44e7f54a797ce799fd1b03cdd3a44684",
-   "name": "verso",
+   "rev": "af3496983daa5d0e4cc18bb05f91f07885db94b1",
+   "name": "Statlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.36.0-rc2",
+   "inputRev": "main",
    "inherited": false,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "c09cb1e4f1e6e1c231a1175a12b681b075054a1b",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/illuminate",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "758bff3509b8e90ca82e37aa5de81de3c9e70fc0",
+   "name": "illuminate",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
-   "scope": "leanprover-community",
+   "scope": "",
    "rev": "129d1ba9a16bc0660f46c79e9fb041ef5d5d80de",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
+  {"url": "https://github.com/acmepjz/md4lean",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "31907cc18f48a95384f99cee5582c00fb39e0f67",
+   "name": "MD4Lean",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/subverso",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "892d6dc520270b5fb8c1291dd1b131e8c16255ed",
+   "name": "subverso",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/mathlib4",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "2ddf59c8f14245864e6c0ed227a2dab76b9efea2",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "2ddf59c8f14245864e6c0ed227a2dab76b9efea2",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/LeanSearchClient",
    "type": "git",
    "subDir": null,
@@ -45,7 +95,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b8cc5dd0a36233b88a6ed5a7dbf1207d09338c60",
+   "rev": "e5d5639bedc7feecfbcb98e30b3bf26463d9f722",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,52 +135,12 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "08a1d53cd0bbb78442973b751c8e6f98e75b12be",
+   "rev": "4af7237d146261353907b06a01b6f3fc06cfa067",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover/lean4-cli",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover",
-   "rev": "c09cb1e4f1e6e1c231a1175a12b681b075054a1b",
-   "name": "Cli",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.36.0-rc2",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover/illuminate",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "758bff3509b8e90ca82e37aa5de81de3c9e70fc0",
-   "name": "illuminate",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/acmepjz/md4lean",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "31907cc18f48a95384f99cee5582c00fb39e0f67",
-   "name": "MD4Lean",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/subverso",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "892d6dc520270b5fb8c1291dd1b131e8c16255ed",
-   "name": "subverso",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"}],
+   "configFile": "lakefile.toml"}],
  "name": "LeanMachineLearning",
  "lakeDir": ".lake",
  "fixedToolchain": false}
diff --git a/lakefile.toml b/lakefile.toml
index ba75e333..9199f075 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -9,16 +9,19 @@ relaxedAutoImplicit = false
 # Enable all mathlib linters: automatically matches what mathlib uses.
 weak.linter.mathlibStandardSet = true
 
+# Mathlib comes through Statlib, at the commit Statlib pins. Statlib is required before Verso:
+# Lake gives precedence to later requires for shared dependencies, so Verso's `subverso` pin wins
+# over Statlib's.
+[[require]]
+name = "Statlib"
+git = "https://github.com/stat-lib/statlib"
+rev = "main"
+
 [[require]]
 name = "verso"
 git = "https://github.com/leanprover/verso"
 rev = "v4.36.0-rc2"
 
-[[require]]
-name = "mathlib"
-scope = "leanprover-community"
-rev = "6135ffb78e8bcd3fcc8ec02f3f82ea0b0737358b"
-
 [[lean_lib]]
 name = "LeanMachineLearning"