feat: the bipolar rate equals the smallest relative entropy to the null under lower semicontinuity [RR26, Theorem 4.1]

LMLExplore/EValues/BipolarRate.lean

@@ -47,6 +47,11 @@ else: no domination, convexity or compactness.
 * `ProbabilityTheory.maxLogGrowth_le_mul_klDiv`, `ProbabilityTheory.bipolarRate_le_iInf_klDiv`:
   the bipolar rate is at most the smallest relative entropy from `Q₁` to the null
   [RR26, proof of Theorem 4.1].
+* `ProbabilityTheory.le_bipolarRate_of_tendsto`: a lower bound on the bipolar rate from real lower
+  bounds on `maxLogGrowth Q₁ S₁ (n + 1)` whose quotients by `n + 1` converge.
+* `ProbabilityTheory.le_maxLogGrowth_of_ofReal_exp_mul_le_one`: the lower bound on the growth of
+  `m` observations given by the e-variable `1/2 + (1/2) e ^ t 1_A`, valid when
+  `e ^ t P ^ m (A) ≤ 1` for every member `P` of the null.
 
 ## References
 
@@ -224,4 +229,70 @@ theorem bipolarRate_le_iInf_klDiv (Q₁ : Measure 𝓧) [IsProbabilityMeasure Q
   rw [← EReal.toENNReal_coe (x := klDiv Q₁ P)]
   exact EReal.toENNReal_le_toENNReal (bipolarRate_le_klDiv Q₁ hP)
 
+/-- A real lower bound on the growth of `n + 1` observations, divided by `n + 1`, that converges
+to `L` gives the lower bound `L` on the bipolar rate. -/
+lemma le_bipolarRate_of_tendsto {r : ℕ → ℝ} {L : ℝ}
+    (hr : ∀ n, (r n : EReal) ≤ maxLogGrowth Q₁ S₁ (n + 1))
+    (hlim : Tendsto (fun n : ℕ ↦ r n / (n + 1)) atTop (𝓝 L)) :
+    (L : EReal) ≤ bipolarRate Q₁ S₁ := by
+  refine le_of_tendsto' (EReal.tendsto_coe.2 hlim) fun n ↦ ?_
+  have h : ((r n / (n + 1) : ℝ) : EReal) = (r n : EReal) / ((n + 1 : ℕ) : EReal) := by
+    rw [EReal.coe_div]
+    norm_cast
+  rw [h]
+  exact (EReal.div_le_div_right_of_nonneg (by positivity) (hr n)).trans
+    (maxLogGrowth_div_le_bipolarRate Q₁ S₁ n.succ_ne_zero)
+
+/-- The e-variable `1/2 + (1/2) e ^ t 1_A` on `m` observations, valid when `e ^ t P ^ m (A) ≤ 1`
+for every member `P` of the null, gives the lower bound `t Q ^ m (A) - log 2` on the growth of `m`
+observations. -/
+lemma le_maxLogGrowth_of_ofReal_exp_mul_le_one (Q : Measure 𝓧) [IsProbabilityMeasure Q]
+    {S : Set (Measure 𝓧)} (hS : ∀ P ∈ S, IsProbabilityMeasure P) {m : ℕ}
+    {A : Set (Fin m → 𝓧)} (hA : MeasurableSet A) {t : ℝ}
+    (hP : ∀ P ∈ S, ENNReal.ofReal (Real.exp t) * (Measure.pi fun _ : Fin m ↦ P) A ≤ 1) :
+    ((t * (Measure.pi fun _ : Fin m ↦ Q).real A - Real.log 2 : ℝ) : EReal) ≤
+      maxLogGrowth Q S m := by
+  set Qm := Measure.pi fun _ : Fin m ↦ Q
+  set b := ENNReal.ofReal (Real.exp t)
+  set X : (Fin m → 𝓧) → ℝ≥0∞ := fun x ↦ 2⁻¹ + 2⁻¹ * A.indicator (fun _ ↦ b) x
+  have hXm : Measurable X := measurable_const.add (measurable_const.mul
+    (measurable_const.indicator hA))
+  have hX : IsEVar X ((fun P ↦ Measure.pi fun _ : Fin m ↦ P) '' S) := by
+    refine IsEVar.of_lintegral_le_one ?_ hXm ?_
+    · rintro _ ⟨P, hP, rfl⟩
+      have := hS P hP
+      infer_instance
+    · rintro _ ⟨P, hPS, rfl⟩
+      have := hS P hPS
+      calc ∫⁻ x, X x ∂(Measure.pi fun _ : Fin m ↦ P)
+      _ = 2⁻¹ + 2⁻¹ * (b * (Measure.pi fun _ : Fin m ↦ P) A) := by
+        simp [X, lintegral_add_right _ ((measurable_const.indicator hA).const_mul _),
+          lintegral_const_mul _ (measurable_const.indicator hA), lintegral_indicator_const hA]
+      _ ≤ 2⁻¹ + 2⁻¹ * 1 := by gcongr; exact hP P hPS
+      _ = 1 := by rw [mul_one, ENNReal.inv_two_add_inv_two]
+  set g : (Fin m → 𝓧) → ℝ := fun x ↦ A.indicator (fun _ ↦ t) x - Real.log 2
+  have hg (x : Fin m → 𝓧) : ENNReal.ofReal (Real.exp (g x)) ≤ X x := by
+    by_cases hx : x ∈ A
+    · simp only [g, X, Set.indicator_of_mem hx]
+      rw [Real.exp_sub, Real.exp_log two_pos, ENNReal.ofReal_div_of_pos two_pos,
+        ENNReal.ofReal_ofNat, div_eq_mul_inv, mul_comm]
+      exact le_add_self
+    · simp only [g, X, Set.indicator_of_notMem hx, zero_sub, Real.exp_neg, Real.exp_log two_pos,
+        mul_zero, add_zero]
+      rw [ENNReal.ofReal_inv_of_pos two_pos, ENNReal.ofReal_ofNat]
+  have hgi : Integrable g Qm := ((integrable_const t).indicator hA).sub (integrable_const _)
+  calc ((t * Qm.real A - Real.log 2 : ℝ) : EReal)
+  _ = ∫ᵉ x, (g x : EReal) ∂Qm := by
+    rw [eintegral_eq_integral hgi]
+    simp [g, integral_sub ((integrable_const t).indicator hA) (integrable_const _),
+      integral_indicator_const _ hA, mul_comm]
+  _ ≤ ∫ᵉ x, (logUtility ∘ X) x ∂Qm := eintegral_mono fun x ↦ by
+    calc (g x : EReal)
+    _ = ENNReal.log (ENNReal.ofReal (Real.exp (g x))) := by
+      rw [ENNReal.log_ofReal_of_pos (Real.exp_pos _), Real.log_exp]
+    _ ≤ (logUtility ∘ X) x := ENNReal.log_monotone (hg x)
+  _ ≤ maxLogGrowth Q S m := by
+    rw [maxLogGrowth_def]
+    exact hX.eintegral_le_maxUtility _ _
+
 end ProbabilityTheory

LMLExplore/EValues/BipolarRate/Semicontinuity.lean

@@ -0,0 +1,109 @@
+/-
+Copyright (c) 2026 LMLExplore contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: LMLExplore contributors
+-/
+module
+
+public import LMLExplore.EValues.BipolarRate
+public import LMLExplore.Probability.LargeDeviations.EmpiricalAverage
+
+/-!
+# The bipolar rate equals the smallest relative entropy under lower semicontinuity
+
+The bipolar rate `bipolarRate Q S` of a probability measure `Q` against an i.i.d. null `S` is at
+most the smallest relative entropy `⨅ P ∈ S, klDiv Q P` from `Q` to the null
+(`ProbabilityTheory.bipolarRate_le_iInf_klDiv`). This file proves that they are equal when the
+smallest relative entropy to the null, as a function of the law, is lower semicontinuous at `Q`
+for the topology generated by the integrals of bounded measurable functions [RR26, Theorem 4.1].
+That topology is finer than the topology of weak convergence, so lower semicontinuity for weak
+convergence, which [RR26] assumes on a Polish space, is a special case; no topology on the
+sample space is needed here.
+
+The semicontinuity is stated with neighbourhoods: for every `c` below the smallest relative
+entropy from `Q` to `S`, there are finitely many bounded measurable functions `f i` and `ε > 0`
+such that every probability measure `R` whose integrals of the `f i` are within `ε` of those of
+`Q` is at relative entropy at least `c` from every member of `S`.
+
+## Main statements
+
+* `ProbabilityTheory.bipolarRate_eq_iInf_klDiv_of_forall_exists_forall_le`: the bipolar rate
+  equals the smallest relative entropy to the null under the semicontinuity above.
+
+## Implementation notes
+
+The lower bound is a Sanov-type argument with blocks of length one. The probability under `P ^ m`
+of the event `A` that the empirical averages of the test functions lie in the neighbourhood is at
+most `exp (- m c)` (`ProbabilityTheory.ofReal_exp_mul_measure_pi_le_one`, Csiszár's conditioning
+argument [Csi84]): condition `P ^ m` on that event, and use the superadditivity of the relative
+entropy over the coordinates and its convexity. The mixture `1/2 + (1/2) exp (m c) 1_A` is then an
+`m`-sample e-variable, whose expected logarithm under `Q ^ m` is at least `m c Q ^ m (A) - log 2`
+(`ProbabilityTheory.le_maxLogGrowth_of_ofReal_exp_mul_le_one`); the weak law of large numbers
+under `Q ^ m`, from Chebyshev's inequality, gives `Q ^ m (A) ≥ 1 - D / m` for a constant `D`, so
+this is at least `m c - O(1)`.
+
+## References
+
+* [RR26] A. Ram and A. Ramdas, *The optimal betting wealth growth rate*, arXiv:2604.25280v1.
+* [Csi84] I. Csiszár, *Sanov property, generalized I-projection and a conditional limit theorem*,
+  Ann. Probab. 12 (1984), 768–793.
+-/
+
+public section
+
+open MeasureTheory InformationTheory Filter
+open scoped ENNReal NNReal Topology
+
+namespace ProbabilityTheory
+
+variable {𝓧 : Type*} {m𝓧 : MeasurableSpace 𝓧}
+
+/-- If the smallest relative entropy to `S` is lower semicontinuous at `Q` for the topology of
+integrals of bounded measurable functions, in the sense of neighbourhoods, then the bipolar rate
+of `Q` against `S` equals the smallest relative entropy from `Q` to `S` [RR26, Theorem 4.1]. The
+test functions need only be bounded, by any constant, and measurable: no topology on `𝓧` is
+used, and lower semicontinuity for weak convergence is a special case. -/
+theorem bipolarRate_eq_iInf_klDiv_of_forall_exists_forall_le (Q : Measure 𝓧)
+    [IsProbabilityMeasure Q] (S : Set (Measure 𝓧)) (hS : ∀ P ∈ S, IsProbabilityMeasure P)
+    (h : ∀ c : ℝ≥0∞, c < ⨅ P ∈ S, klDiv Q P →
+      ∃ (k : ℕ) (f : Fin k → 𝓧 → ℝ) (ε : ℝ), 0 < ε ∧ (∀ i, Measurable (f i)) ∧
+        (∀ i, ∃ C, ∀ x, |f i x| ≤ C) ∧ ∀ R : Measure 𝓧, IsProbabilityMeasure R →
+          (∀ i, |∫ x, f i x ∂R - ∫ x, f i x ∂Q| ≤ ε) → c ≤ ⨅ P ∈ S, klDiv R P) :
+    bipolarRate Q S = (⨅ P ∈ S, klDiv Q P : ℝ≥0∞) := by
+  refine le_antisymm (bipolarRate_le_iInf_klDiv Q hS)
+    (le_of_forall_lt_imp_le_of_dense fun c hc ↦ ?_)
+  rcases le_or_gt c 0 with hc0 | hc0
+  · exact hc0.trans (bipolarRate_nonneg Q S)
+  obtain ⟨c, rfl⟩ : ∃ r : ℝ, (r : EReal) = c :=
+    ⟨c.toReal, EReal.coe_toReal hc.ne_top (ne_bot_of_gt hc0)⟩
+  have hc0' : 0 < c := by exact_mod_cast hc0
+  have hcE : ((ENNReal.ofReal c : ℝ≥0∞) : EReal) = c := by
+    rw [EReal.coe_ennreal_ofReal, max_eq_left hc0'.le]
+  obtain ⟨k, f, ε, hε, hfm, hfC, hU⟩ :=
+    h (ENNReal.ofReal c) (EReal.coe_ennreal_lt_coe_ennreal_iff.1 (hcE ▸ hc))
+  choose C hC using hfC
+  have hfL (i : Fin k) : MemLp (f i) 2 Q :=
+    .of_bound (hfm i).aestronglyMeasurable (C i) (.of_forall fun x ↦ (hC i x).trans' (by simp))
+  set D := ∑ i, Var[f i; Q] / ε ^ 2
+  refine le_bipolarRate_of_tendsto (r := fun n ↦ (n + 1) * c * (1 - D / (n + 1)) - Real.log 2)
+    (fun n ↦ ?_) ?_
+  · -- the e-variable `1/2 + (1/2) exp ((n + 1) c) 1_A`, with the law of large numbers under `Q`
+    have hsan (P : Measure 𝓧) (hP : P ∈ S) :=
+      have := hS P hP
+      ofReal_exp_mul_measure_pi_le_one hfm hC hc0'.le
+        (fun R hR hRf ↦ (hU R hR hRf).trans (iInf₂_le P hP)) (m := n + 1) n.succ_ne_zero
+    refine le_trans ?_ (le_maxLogGrowth_of_ofReal_exp_mul_le_one Q hS
+      (measurableSet_setOf_forall_abs_sum_div_sub_le hfm _ ε (n + 1)) hsan)
+    have h := one_sub_div_le_measureReal_pi_forall_abs_sum_div_sub_le hfL hε n.succ_ne_zero
+    refine EReal.coe_le_coe_iff.2 ?_
+    have hn1 : ((n + 1 : ℕ) : ℝ) = (n : ℝ) + 1 := by push_cast; ring
+    rw [hn1] at h ⊢
+    gcongr
+  · have h0 := tendsto_one_div_add_atTop_nhds_zero_nat (𝕜 := ℝ)
+    have h1 := (tendsto_const_nhds (x := c)).sub (h0.const_mul (c * D + Real.log 2))
+    rw [mul_zero, sub_zero] at h1
+    refine h1.congr fun n ↦ ?_
+    field_simp
+    ring
+
+end ProbabilityTheory

LMLExplore/InformationTheory/KullbackLeibler/Cond.lean

@@ -0,0 +1,54 @@
+/-
+Copyright (c) 2026 LMLExplore contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: LMLExplore contributors
+-/
+module
+
+public import Mathlib.InformationTheory.KullbackLeibler.Basic
+public import Mathlib.Probability.ConditionalProbability
+public import Statlib.EValues.RIPr
+
+/-!
+# The relative entropy from a conditional law
+
+The relative entropy from the law `μ[|A]`, the probability measure `μ` conditioned on the event
+`A`, to `μ` is at most `log (1 / μ A)`. The proof uses Statlib's variational form of the relative
+entropy, the maximal expected logarithm of an e-variable for the singleton null
+(`maxUtility_singleton_eq_klDiv`), and Jensen's inequality: an e-variable for `μ` has integral at
+most `1 / μ A` under `μ[|A]`.
+
+## Main statements
+
+* `InformationTheory.klDiv_cond_le`: `klDiv (μ[|A]) μ ≤ log (1 / μ A)`.
+-/
+
+public section
+
+open MeasureTheory ProbabilityTheory
+open scoped ENNReal
+
+namespace InformationTheory
+
+variable {𝓧 : Type*} {m𝓧 : MeasurableSpace 𝓧}
+
+/-- The relative entropy from the law `μ` conditioned on `A` to `μ` is at most `log (1 / μ A)`. -/
+lemma klDiv_cond_le {μ : Measure 𝓧} [IsProbabilityMeasure μ] {A : Set 𝓧} (hμA : μ A ≠ 0) :
+    ((klDiv (μ[|A]) μ : ℝ≥0∞) : EReal) ≤ ENNReal.log (μ A)⁻¹ := by
+  have := cond_isProbabilityMeasure hμA
+  rw [← maxUtility_singleton_eq_klDiv]
+  refine iSup₂_le fun X hX ↦ ?_
+  calc ∫ᵉ x, (logUtility ∘ X) x ∂μ[|A]
+  _ ≤ logUtility (∫⁻ x, X x ∂μ[|A]) :=
+    Utility.eintegral_le_map logUtility hX.measurable.aemeasurable
+  _ ≤ ENNReal.log (μ A)⁻¹ := by
+    refine ENNReal.log_monotone ?_
+    rw [ProbabilityTheory.cond, lintegral_smul_measure, smul_eq_mul]
+    calc (μ A)⁻¹ * ∫⁻ x, X x ∂μ.restrict A
+    _ ≤ (μ A)⁻¹ * 1 := by
+      gcongr
+      exact (setLIntegral_le_lintegral A X).trans
+        ((hX.lintegral_le_measure_univ μ rfl).trans_eq measure_univ)
+    _ = (μ A)⁻¹ := mul_one _
+
+end InformationTheory

LMLExplore/InformationTheory/KullbackLeibler/Pi.lean

@@ -0,0 +1,114 @@
+/-
+Copyright (c) 2026 LMLExplore contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: LMLExplore contributors
+-/
+module
+
+public import Mathlib.InformationTheory.KullbackLeibler.Basic
+public import Statlib.EValues.Product
+public import Statlib.EValues.RIPr
+public import Statlib.ForMathlib.InformationTheory.KullbackLeibler.DataProcessing
+
+/-!
+# Superadditivity of the relative entropy over the marginals of a product
+
+The relative entropy from a law to a product law is at least the sum of the relative entropies of
+its marginals to the factors. For two factors, this is the value of Statlib's
+`maxUtility_fst_add_maxUtility_snd_le` for singleton nulls, where the maximal expected logarithm
+of an e-variable is the relative entropy (`maxUtility_singleton_eq_klDiv`); for finitely many
+factors, it follows by induction on the number of coordinates, after enumerating them.
+
+## Main statements
+
+* `InformationTheory.klDiv_fst_add_klDiv_snd_le`: the relative entropy to a product law is at
+  least the sum of the relative entropies of the two marginals.
+* `InformationTheory.sum_klDiv_map_eval_le`: the relative entropy from a law on a finite product
+  `∀ i, 𝓧 i` to a product law `Measure.pi P` is at least the sum of the relative entropies of its
+  marginals to the factors `P i`.
+-/
+
+public section
+
+open MeasureTheory ProbabilityTheory
+
+namespace InformationTheory
+
+variable {𝓧 𝓨 : Type*} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨}
+
+/-- The relative entropy to a product law is at least the sum of the relative entropies of the
+two marginals. -/
+lemma klDiv_fst_add_klDiv_snd_le (R : Measure (𝓧 × 𝓨)) [IsProbabilityMeasure R] (P : Measure 𝓧)
+    (P' : Measure 𝓨) [IsProbabilityMeasure P] [IsProbabilityMeasure P'] :
+    klDiv R.fst P + klDiv R.snd P' ≤ klDiv R (P.prod P') := by
+  have h := maxUtility_fst_add_maxUtility_snd_le R (S := {P}) (T := {P'})
+    (fun μ hμ ↦ by rw [Set.mem_singleton_iff.1 hμ]; infer_instance)
+    (fun μ hμ ↦ by rw [Set.mem_singleton_iff.1 hμ]; infer_instance)
+  rwa [Set.image2_singleton, maxUtility_singleton_eq_klDiv, maxUtility_singleton_eq_klDiv,
+    maxUtility_singleton_eq_klDiv, ← EReal.coe_ennreal_add,
+    EReal.coe_ennreal_le_coe_ennreal_iff] at h
+
+/-- The case of `Fin n` of `sum_klDiv_map_eval_le`, by induction on `n`. -/
+private lemma sum_klDiv_map_eval_le_fin {n : ℕ} {𝓧 : Fin n → Type*} [∀ j, MeasurableSpace (𝓧 j)]
+    (P : ∀ j, Measure (𝓧 j)) [∀ j, IsProbabilityMeasure (P j)] (μ : Measure (∀ j, 𝓧 j))
+    [IsProbabilityMeasure μ] :
+    ∑ j, klDiv (μ.map fun x ↦ x j) (P j) ≤ klDiv μ (Measure.pi P) := by
+  induction n with
+  | zero => simp
+  | succ n ih =>
+    set e := MeasurableEquiv.piFinSuccAbove 𝓧 0
+    set R := μ.map e
+    set P' := Measure.pi fun j : Fin n ↦ P ((0 : Fin (n + 1)).succAbove j)
+    -- `e` splits off the first coordinate and carries `Measure.pi P` to a product law
+    have hKL : klDiv R ((P 0).prod P') = klDiv μ (Measure.pi P) := by
+      rw [← (measurePreserving_piFinSuccAbove P 0).map_eq]
+      exact klDiv_map_measurableEmbedding _ _ e.measurableEmbedding
+    have hfst : R.fst = μ.map fun x ↦ x 0 := by
+      -- the first component of `e x` is `x 0` by definition of `piFinSuccAbove`
+      have h : Prod.fst ∘ e = fun x ↦ x 0 := rfl
+      rw [Measure.fst, Measure.map_map measurable_fst e.measurable, h]
+    have hmarg (j : Fin n) :
+        R.snd.map (fun x ↦ x j) = μ.map fun x ↦ x ((0 : Fin (n + 1)).succAbove j) := by
+      -- the second component of `e x` is `x ∘ succAbove 0` by definition of `piFinSuccAbove`
+      have h : ((fun x ↦ x j) ∘ Prod.snd) ∘ e = fun x ↦ x ((0 : Fin (n + 1)).succAbove j) := rfl
+      rw [Measure.snd, Measure.map_map (measurable_pi_apply j) measurable_snd,
+        Measure.map_map ((measurable_pi_apply j).comp measurable_snd) e.measurable, h]
+    calc ∑ j, klDiv (μ.map fun x ↦ x j) (P j)
+    _ = klDiv R.fst (P 0) +
+        ∑ j : Fin n, klDiv (R.snd.map fun x ↦ x j) (P ((0 : Fin (n + 1)).succAbove j)) := by
+      rw [Fin.sum_univ_succAbove _ 0, hfst]
+      simp_rw [hmarg]
+    _ ≤ klDiv R.fst (P 0) + klDiv R.snd P' := by
+      gcongr
+      exact ih _ R.snd
+    _ ≤ klDiv R ((P 0).prod P') := klDiv_fst_add_klDiv_snd_le R _ _
+    _ = klDiv μ (Measure.pi P) := hKL
+
+/-- The relative entropy from a law on a finite product `∀ i, 𝓧 i` to a product law
+`Measure.pi P` is at least the sum of the relative entropies of its marginals to the factors
+`P i`. -/
+lemma sum_klDiv_map_eval_le {ι : Type*} [Fintype ι] {𝓧 : ι → Type*}
+    [∀ i, MeasurableSpace (𝓧 i)] (P : ∀ i, Measure (𝓧 i)) [∀ i, IsProbabilityMeasure (P i)]
+    (μ : Measure (∀ i, 𝓧 i)) [IsProbabilityMeasure μ] :
+    ∑ i, klDiv (μ.map fun x ↦ x i) (P i) ≤ klDiv μ (Measure.pi P) := by
+  -- transport to `Fin n` along an enumeration of `ι`
+  set e := (Fintype.equivFin ι).symm
+  set ψ := MeasurableEquiv.piCongrLeft 𝓧 e
+  set ν := μ.map ψ.symm
+  have hν : ν.map ψ = μ := by
+    rw [Measure.map_map ψ.measurable ψ.symm.measurable, ψ.self_comp_symm, Measure.map_id]
+  have hKL : klDiv ν (Measure.pi fun a ↦ P (e a)) = klDiv μ (Measure.pi P) := by
+    rw [← (measurePreserving_piCongrLeft P e).map_eq, ← klDiv_map_measurableEmbedding _ _
+      ψ.measurableEmbedding, hν]
+  have hmarg (a : Fin (Fintype.card ι)) : ν.map (fun x ↦ x a) = μ.map fun x ↦ x (e a) := by
+    -- `ψ.symm x a = x (e a)` by definition of `piCongrLeft`
+    have h : (fun x ↦ x a) ∘ ψ.symm = fun x ↦ x (e a) := rfl
+    rw [Measure.map_map (measurable_pi_apply a) ψ.symm.measurable, h]
+  calc ∑ i, klDiv (μ.map fun x ↦ x i) (P i)
+  _ = ∑ a, klDiv (ν.map fun x ↦ x a) (P (e a)) := by
+    rw [← e.sum_comp]
+    simp_rw [hmarg]
+  _ ≤ klDiv ν (Measure.pi fun a ↦ P (e a)) := sum_klDiv_map_eval_le_fin _ ν
+  _ = klDiv μ (Measure.pi P) := hKL
+
+end InformationTheory