diff --git a/LMLExplore/EValues/BipolarRate.lean b/LMLExplore/EValues/BipolarRate.lean
index f2ca48fd..d0719966 100644
--- a/LMLExplore/EValues/BipolarRate.lean
+++ b/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
diff --git a/LMLExplore/EValues/BipolarRate/Semicontinuity.lean b/LMLExplore/EValues/BipolarRate/Semicontinuity.lean
new file mode 100644
index 00000000..a0218f90
--- /dev/null
+++ b/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
diff --git a/LMLExplore/InformationTheory/KullbackLeibler/Cond.lean b/LMLExplore/InformationTheory/KullbackLeibler/Cond.lean
new file mode 100644
index 00000000..472436ed
--- /dev/null
+++ b/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
diff --git a/LMLExplore/InformationTheory/KullbackLeibler/Pi.lean b/LMLExplore/InformationTheory/KullbackLeibler/Pi.lean
new file mode 100644
index 00000000..c666957f
--- /dev/null
+++ b/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
diff --git a/LMLExplore/Probability/LargeDeviations/EmpiricalAverage.lean b/LMLExplore/Probability/LargeDeviations/EmpiricalAverage.lean
new file mode 100644
index 00000000..fe276416
--- /dev/null
+++ b/LMLExplore/Probability/LargeDeviations/EmpiricalAverage.lean
@@ -0,0 +1,232 @@
+/-
+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.InformationTheory.KullbackLeibler.Cond
+public import LMLExplore.InformationTheory.KullbackLeibler.Pi
+public import Mathlib.Probability.Moments.Variance
+public import Statlib.Divergence.KullbackLeibler.Basic
+public import Statlib.ForMathlib.MeasureTheory.Integral.Pi
+
+/-!
+# Empirical averages of functions under product laws
+
+For finitely many measurable functions `f i` on `𝓧` and `m` observations `x : Fin m → 𝓧`,
+this file bounds the probability, under an i.i.d. law `P ^ m`, that the empirical averages
+`(∑ j, f i (x j)) / m` lie within `ε` of given values `a i`, from both sides.
+
+* From above, for bounded `f i`, by a Sanov-type bound with blocks of length one: if every law
+  whose integrals of the `f i` are within `ε` of the `a i` is at relative entropy at least `c`
+  from `P`, the probability is at most `exp (- m c)`. This is Csiszár's argument for Sanov's
+  upper bound on a convex set [Csi84]: condition `P ^ m` on the event, whose relative entropy to
+  `P ^ m` is at most `log (1 / P ^ m (A))` (`InformationTheory.klDiv_cond_le`), and bound it from
+  below by the superadditivity of the relative entropy over the coordinates
+  (`InformationTheory.sum_klDiv_map_eval_le`) and its convexity, at the average of the marginals
+  of the conditioned law, which is in the neighbourhood.
+* From below, for square-integrable `f i` whose means under `P` are the `a i`, by the weak law of
+  large numbers from Chebyshev's inequality.
+
+## Main statements
+
+* `ProbabilityTheory.ofReal_exp_mul_measure_pi_le_one`: the Sanov-type bound.
+* `ProbabilityTheory.measure_pi_lt_abs_sum_div_sub_le`: the weak law of large numbers for a
+  square-integrable function `g`, `P ^ m (|(∑ j, g (x j)) / m - mean| > ε) ≤ Var[g] / (m ε ^ 2)`.
+* `ProbabilityTheory.one_sub_div_le_measureReal_pi_forall_abs_sum_div_sub_le`: the weak law of
+  large numbers for finitely many square-integrable functions at once.
+
+## References
+
+* [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
+
+namespace ProbabilityTheory
+
+variable {𝓧 : Type*} {m𝓧 : MeasurableSpace 𝓧}
+
+/-- The tuples whose empirical averages of the measurable functions `f i` are within `ε` of the
+`a i` form a measurable set. -/
+lemma measurableSet_setOf_forall_abs_sum_div_sub_le {k : ℕ} {f : Fin k → 𝓧 → ℝ}
+    (hf : ∀ i, Measurable (f i)) (a : Fin k → ℝ) (ε : ℝ) (m : ℕ) :
+    MeasurableSet {x : Fin m → 𝓧 | ∀ i, |(∑ j, f i (x j)) / m - a i| ≤ ε} := by
+  simp only [Set.ofPred_forall]
+  exact MeasurableSet.iInter fun i ↦ measurableSet_le (continuous_abs.measurable.comp
+    (((Finset.measurable_sum _ fun j _ ↦ (hf i).comp (measurable_pi_apply j)).div_const _).sub_const
+      _)) measurable_const
+
+/-- A measurable function `g` bounded by `C` in absolute value, evaluated at one coordinate, is
+integrable against every finite measure on `ι → 𝓧`. -/
+lemma integrable_comp_eval_of_abs_le {g : 𝓧 → ℝ} (hg : Measurable g) {C : ℝ}
+    (hgC : ∀ x, |g x| ≤ C) {ι : Type*} (μ : Measure (ι → 𝓧)) [IsFiniteMeasure μ] (j : ι) :
+    Integrable (fun x ↦ g (x j)) μ :=
+  .of_bound (hg.comp (measurable_pi_apply j)).aestronglyMeasurable C (.of_forall fun _ ↦ hgC _)
+
+/-- The average of the marginals of a probability measure on `Fin m → 𝓧`, for `m ≠ 0`, is a
+probability measure. -/
+lemma isProbabilityMeasure_sum_smul_map_eval {m : ℕ} (hm : m ≠ 0) (μ : Measure (Fin m → 𝓧))
+    [IsProbabilityMeasure μ] :
+    IsProbabilityMeasure (∑ j : Fin m, (((m : ℝ≥0)⁻¹ : ℝ≥0) : ℝ≥0∞) • μ.map fun x ↦ x j) :=
+  ⟨by simp [ENNReal.coe_inv, hm, ENNReal.mul_inv_cancel]⟩
+
+/-- The integral against the average of the marginals of `μ` is the integral of the empirical
+average against `μ`. -/
+lemma integral_sum_smul_map_eval {m : ℕ} (μ : Measure (Fin m → 𝓧))
+    [IsProbabilityMeasure μ] {g : 𝓧 → ℝ} (hg : Measurable g) {C : ℝ} (hgC : ∀ x, |g x| ≤ C) :
+    ∫ x, g x ∂(∑ j : Fin m, (((m : ℝ≥0)⁻¹ : ℝ≥0) : ℝ≥0∞) • μ.map fun x ↦ x j) =
+      ∫ x, (∑ j, g (x j)) / m ∂μ := by
+  have hgj := integrable_comp_eval_of_abs_le hg hgC μ
+  rw [integral_finsetSum_measure fun j _ ↦ ((integrable_map_measure hg.aestronglyMeasurable
+    (measurable_pi_apply j).aemeasurable).2 (hgj j)).smul_measure ENNReal.coe_ne_top]
+  have hj (j : Fin m) : ∫ x, g x ∂(μ.map fun x ↦ x j) = ∫ x, g (x j) ∂μ :=
+    integral_map (measurable_pi_apply j).aemeasurable hg.aestronglyMeasurable
+  simp_rw [integral_smul_measure, hj]
+  rw [integral_div, integral_finsetSum _ fun j _ ↦ hgj j]
+  simp [div_eq_inv_mul, Finset.mul_sum]
+
+/-- If the empirical average of a bounded measurable function `g` is almost surely within `ε` of
+`a` under `μ`, then so is the integral of `g` against the average of the marginals of `μ`. -/
+lemma abs_integral_sum_smul_map_eval_sub_le {m : ℕ} (μ : Measure (Fin m → 𝓧))
+    [IsProbabilityMeasure μ] {g : 𝓧 → ℝ} (hg : Measurable g) {C : ℝ} (hgC : ∀ x, |g x| ≤ C)
+    {a ε : ℝ} (hμ : ∀ᵐ x ∂μ, |(∑ j, g (x j)) / m - a| ≤ ε) :
+    |∫ x, g x ∂(∑ j : Fin m, (((m : ℝ≥0)⁻¹ : ℝ≥0) : ℝ≥0∞) • μ.map fun x ↦ x j) - a| ≤ ε := by
+  rw [integral_sum_smul_map_eval μ hg hgC]
+  have hint : Integrable (fun x : Fin m → 𝓧 ↦ (∑ j, g (x j)) / m) μ :=
+    (integrable_finsetSum _ fun j _ ↦ integrable_comp_eval_of_abs_le hg hgC μ j).div_const _
+  have heq : ∫ x, (∑ j, g (x j)) / m ∂μ - a = ∫ x, ((∑ j, g (x j)) / m - a) ∂μ := by
+    rw [integral_sub hint (integrable_const _), integral_const, probReal_univ, one_smul]
+  rw [heq, ← Real.norm_eq_abs]
+  refine (norm_integral_le_of_norm_le_const (C := ε) ?_).trans (by simp)
+  simpa only [Real.norm_eq_abs] using hμ
+
+/-- **Sanov-type bound** [Csi84]. If every law `R` whose integrals of the bounded functions `f i`
+are within `ε` of `a i` is at relative entropy at least `c ≥ 0` from `P`, then the probability
+under `P ^ m` that the empirical averages of the `f i` are within `ε` of the `a i` is at most
+`exp (- m c)`. -/
+lemma ofReal_exp_mul_measure_pi_le_one {k : ℕ} {f : Fin k → 𝓧 → ℝ} (hf : ∀ i, Measurable (f i))
+    {C : Fin k → ℝ} (hfC : ∀ i x, |f i x| ≤ C i) {a : Fin k → ℝ} {ε c : ℝ} (hc : 0 ≤ c)
+    {P : Measure 𝓧} [IsProbabilityMeasure P]
+    (hU : ∀ R : Measure 𝓧, IsProbabilityMeasure R → (∀ i, |∫ x, f i x ∂R - a i| ≤ ε) →
+      ENNReal.ofReal c ≤ klDiv R P) {m : ℕ} (hm : m ≠ 0) :
+    ENNReal.ofReal (Real.exp (m * c)) *
+      (Measure.pi fun _ : Fin m ↦ P) {x | ∀ i, |(∑ j, f i (x j)) / m - a i| ≤ ε} ≤ 1 := by
+  set A := {x : Fin m → 𝓧 | ∀ i, |(∑ j, f i (x j)) / m - a i| ≤ ε}
+  set Pm := Measure.pi fun _ : Fin m ↦ P
+  have hA : MeasurableSet A := measurableSet_setOf_forall_abs_sum_div_sub_le hf a ε m
+  rcases eq_or_ne (Pm A) 0 with h0 | h0
+  · simp [h0]
+  -- the law `μ` of `m` observations conditioned on the event, and the average `R` of its marginals
+  set μ := Pm[|A]
+  have : IsProbabilityMeasure μ := cond_isProbabilityMeasure h0
+  set w : Fin m → ℝ≥0 := fun _ ↦ (m : ℝ≥0)⁻¹
+  have hw : ∑ j, w j = 1 := by
+    simp [w, hm]
+  set R := ∑ j, (w j : ℝ≥0∞) • μ.map fun x ↦ x j
+  have hR : IsProbabilityMeasure R := isProbabilityMeasure_sum_smul_map_eval hm μ
+  have hRU (i : Fin k) : |∫ x, f i x ∂R - a i| ≤ ε := by
+    refine abs_integral_sum_smul_map_eval_sub_le μ (hf i) (hfC i) ?_
+    filter_upwards [ae_cond_mem hA] with x hx
+    exact hx i
+  -- `R` is in the neighbourhood, so by convexity and superadditivity over the coordinates the
+  -- relative entropy from `μ` to `P ^ m` is at least `m c`
+  have h1 : (m : ℝ≥0∞) * ENNReal.ofReal c ≤ klDiv μ Pm := by
+    calc (m : ℝ≥0∞) * ENNReal.ofReal c
+    _ ≤ m * klDiv R P := by gcongr; exact hU R hR hRU
+    _ ≤ m * ∑ j, (w j : ℝ≥0∞) * klDiv (μ.map fun x ↦ x j) P := by
+      gcongr
+      exact klDiv_sum_smul_left_le hw
+    _ = ∑ j, klDiv (μ.map fun x ↦ x j) P := by
+      simp [w, Finset.mul_sum, ← mul_assoc, ENNReal.coe_inv, hm, ENNReal.mul_inv_cancel]
+    _ ≤ klDiv μ Pm := sum_klDiv_map_eval_le (fun _ ↦ P) μ
+  -- the relative entropy from `μ` to `P ^ m` is at most `log (1 / P ^ m (A))`: take logarithms
+  have h2 : ((m * c : ℝ) : EReal) ≤ ENNReal.log (Pm A)⁻¹ := by
+    calc ((m * c : ℝ) : EReal)
+    _ = (((m : ℝ≥0∞) * ENNReal.ofReal c : ℝ≥0∞) : EReal) := by
+      simp [← ENNReal.ofReal_natCast, ← ENNReal.ofReal_mul, EReal.coe_ennreal_ofReal,
+        max_eq_left (mul_nonneg (Nat.cast_nonneg m) hc)]
+    _ ≤ (klDiv μ Pm : EReal) := EReal.coe_ennreal_le_coe_ennreal_iff.2 h1
+    _ ≤ ENNReal.log (Pm A)⁻¹ := klDiv_cond_le h0
+  -- take exponentials
+  refine ENNReal.le_inv_iff_mul_le.1 (ENNReal.log_le_log_iff.1 ?_)
+  simpa [ENNReal.log_ofReal_of_pos (Real.exp_pos _)] using h2
+
+/-- **Weak law of large numbers**, by Chebyshev's inequality: the probability that the empirical
+average of a square-integrable function `g` deviates by more than `ε` from its mean is at most
+`Var[g; Q] / (m ε ^ 2)`. -/
+lemma measure_pi_lt_abs_sum_div_sub_le {g : 𝓧 → ℝ} {Q : Measure 𝓧} [IsProbabilityMeasure Q]
+    (hg : MemLp g 2 Q) {ε : ℝ} (hε : 0 < ε) {m : ℕ} (hm : m ≠ 0) :
+    (Measure.pi fun _ : Fin m ↦ Q) {x | ε < |(∑ j, g (x j)) / m - ∫ y, g y ∂Q|} ≤
+      ENNReal.ofReal (Var[g; Q] / (m * ε ^ 2)) := by
+  set Qm := Measure.pi fun _ : Fin m ↦ Q
+  set X : (Fin m → 𝓧) → ℝ := ∑ j : Fin m, fun x ↦ g (x j) with hX_def
+  have hm' : (0 : ℝ) < m := Nat.cast_pos.2 (Nat.pos_of_ne_zero hm)
+  have hgL (j : Fin m) : MemLp (fun x : Fin m → 𝓧 ↦ g (x j)) 2 Qm :=
+    hg.comp_measurePreserving (measurePreserving_eval (fun _ : Fin m ↦ Q) j)
+  have hXL : MemLp X 2 Qm := memLp_finsetSum' _ fun j _ ↦ hgL j
+  have hEX : ∫ x, X x ∂Qm = m * ∫ y, g y ∂Q := by
+    have hj (j : Fin m) : ∫ x, g (x j) ∂Qm = ∫ y, g y ∂Q := by
+      have h := (measurePreserving_eval (fun _ : Fin m ↦ Q) j).map_eq
+      rw [← integral_map (measurable_pi_apply j).aemeasurable (h ▸ hg.aestronglyMeasurable), h]
+    simp [X, integral_finsetSum _ fun j _ ↦ (hgL j).integrable one_le_two, hj]
+  have hVar : Var[X; Qm] = m * Var[g; Q] := by
+    rw [hX_def, variance_sum_pi (μ := fun _ : Fin m ↦ Q) (X := fun _ ↦ g) fun _ ↦ hg]
+    simp
+  calc Qm {x | ε < |(∑ j, g (x j)) / m - ∫ y, g y ∂Q|}
+  _ ≤ Qm {x | m * ε ≤ |X x - ∫ x, X x ∂Qm|} := by
+    refine measure_mono fun x hx ↦ ?_
+    simp only [Set.mem_ofPred_eq] at hx ⊢
+    have h : (∑ j, g (x j)) / m - ∫ y, g y ∂Q = (X x - ∫ x, X x ∂Qm) / m := by
+      rw [hEX, hX_def, Finset.sum_apply]
+      field_simp
+    rw [h, abs_div, abs_of_pos hm', lt_div_iff₀ hm'] at hx
+    linarith
+  _ ≤ ENNReal.ofReal (Var[X; Qm] / (m * ε) ^ 2) :=
+    meas_ge_le_variance_div_sq hXL (by positivity)
+  _ = ENNReal.ofReal (Var[g; Q] / (m * ε ^ 2)) := by
+    rw [hVar]
+    congr 1
+    field_simp
+
+/-- **Weak law of large numbers** for finitely many square-integrable functions `f i`: with
+probability at least `1 - (∑ i, Var[f i; Q] / ε ^ 2) / m` under `Q ^ m`, the empirical averages of
+all the `f i` are within `ε` of their means. -/
+lemma one_sub_div_le_measureReal_pi_forall_abs_sum_div_sub_le {k : ℕ} {f : Fin k → 𝓧 → ℝ}
+    {Q : Measure 𝓧} [IsProbabilityMeasure Q] (hf : ∀ i, MemLp (f i) 2 Q) {ε : ℝ} (hε : 0 < ε)
+    {m : ℕ} (hm : m ≠ 0) :
+    1 - (∑ i, Var[f i; Q] / ε ^ 2) / m ≤
+      (Measure.pi fun _ : Fin m ↦ Q).real
+        {x | ∀ i, |(∑ j, f i (x j)) / m - ∫ y, f i y ∂Q| ≤ ε} := by
+  set Qm := Measure.pi fun _ : Fin m ↦ Q
+  set A := {x : Fin m → 𝓧 | ∀ i, |(∑ j, f i (x j)) / m - ∫ y, f i y ∂Q| ≤ ε}
+  have hcompl : Aᶜ = ⋃ i, {x : Fin m → 𝓧 | ε < |(∑ j, f i (x j)) / m - ∫ y, f i y ∂Q|} := by
+    ext x
+    simp [A]
+  have hle : Qm Aᶜ ≤ ENNReal.ofReal ((∑ i, Var[f i; Q] / ε ^ 2) / m) := by
+    rw [hcompl]
+    refine (measure_iUnion_fintype_le _ _).trans ?_
+    calc ∑ i, Qm {x : Fin m → 𝓧 | ε < |(∑ j, f i (x j)) / m - ∫ y, f i y ∂Q|}
+    _ ≤ ∑ i, ENNReal.ofReal (Var[f i; Q] / (m * ε ^ 2)) :=
+      Finset.sum_le_sum fun i _ ↦ measure_pi_lt_abs_sum_div_sub_le (hf i) hε hm
+    _ = ENNReal.ofReal ((∑ i, Var[f i; Q] / ε ^ 2) / m) := by
+      rw [← ENNReal.ofReal_sum_of_nonneg fun i _ ↦
+        div_nonneg (variance_nonneg _ _) (by positivity)]
+      congr 1
+      simp only [Finset.sum_div]
+      refine Finset.sum_congr rfl fun i _ ↦ ?_
+      field_simp
+  have h := ENNReal.toReal_le_of_le_ofReal
+    (div_nonneg (Finset.sum_nonneg fun i _ ↦ div_nonneg (variance_nonneg _ _) (by positivity))
+      (Nat.cast_nonneg _)) hle
+  rw [← measureReal_def] at h
+  have hu : 1 ≤ Qm.real A + Qm.real Aᶜ := by
+    simpa using measureReal_union_le (μ := Qm) A Aᶜ
+  linarith
+
+end ProbabilityTheory