feat: the maximal expected logarithm of n-sample e-variables, its superadditivity and the bipolar rate

LMLExplore/Analysis/Subadditive.lean

@@ -0,0 +1,137 @@
+/-
+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.Analysis.SpecificLimits.Basic
+public import Mathlib.Topology.Instances.EReal.Lemmas
+
+/-!
+# Fekete's lemma for superadditive sequences of extended reals
+
+Mathlib's `Subadditive.tendsto_lim` is Fekete's lemma for a subadditive sequence `u : ℕ → ℝ`
+with `u n / n` bounded below. This file proves it for a superadditive sequence of extended reals,
+`u m + u n ≤ u (m + n)`, that takes the value `⊥` at no `n ≠ 0`, with no boundedness assumption:
+`u n / n` tends to its supremum over `n ≥ 1`, which may be `⊤`.
+
+## Main statements
+
+* `EReal.tendsto_div_iSup_of_superadditive`: Fekete's lemma for superadditive sequences of
+  extended reals.
+* `EReal.nsmul_le_of_superadditive`, `EReal.nsmul_add_nsmul_le_of_superadditive`: iterated
+  superadditivity.
+* `EReal.eq_top_of_superadditive`: a value `⊤` carries forward to every later index.
+
+## Implementation notes
+
+The supremum `d` bounds `u n / n` for `n ≥ 1`. Conversely, for `m ≥ 1` and `n = q m + s` with
+`q ≥ 1` and `s < m`, superadditivity gives `u n ≥ q u m + s u 1`. If `u m` is finite, so is `u 1`,
+and this lower bound is `n u m / m` up to a constant, so that `u n / n` is eventually above any
+`L < u m / m`. If `u m = ⊤`, then `u n = ⊤` for every `n ≥ m`.
+-/
+
+public section
+
+open Filter Topology
+
+namespace EReal
+
+variable {u : ℕ → EReal}
+
+/-- Superadditivity iterated: `(q + 1) • u m ≤ u ((q + 1) * m)`. -/
+lemma nsmul_le_of_superadditive (h : ∀ m n, u m + u n ≤ u (m + n)) (m q : ℕ) :
+    (q + 1) • u m ≤ u ((q + 1) * m) := by
+  induction q with
+  | zero => simp
+  | succ q ih =>
+    calc (q + 1 + 1) • u m = (q + 1) • u m + u m := succ_nsmul _ _
+    _ ≤ u ((q + 1) * m) + u m := by gcongr
+    _ ≤ u ((q + 1) * m + m) := h _ _
+    _ = u ((q + 1 + 1) * m) := by congr 1; ring
+
+/-- Superadditivity iterated: `(q + 1) • u m + s • u 1 ≤ u ((q + 1) * m + s)`. -/
+lemma nsmul_add_nsmul_le_of_superadditive (h : ∀ m n, u m + u n ≤ u (m + n))
+    (m q s : ℕ) : (q + 1) • u m + s • u 1 ≤ u ((q + 1) * m + s) := by
+  cases s with
+  | zero => simpa using nsmul_le_of_superadditive h m q
+  | succ s =>
+    calc (q + 1) • u m + (s + 1) • u 1 ≤ u ((q + 1) * m) + u ((s + 1) * 1) :=
+        add_le_add (nsmul_le_of_superadditive h m q) (nsmul_le_of_superadditive h 1 s)
+    _ ≤ u ((q + 1) * m + (s + 1)) := by rw [mul_one]; exact h _ _
+
+/-- A value `⊤` of a superadditive sequence that takes the value `⊥` at no `n ≠ 0` carries
+forward: if `u j = ⊤` and `j ≤ n`, then `u n = ⊤`. -/
+lemma eq_top_of_superadditive (hu : ∀ n ≠ 0, u n ≠ ⊥)
+    (h : ∀ m n, u m + u n ≤ u (m + n)) {j n : ℕ} (hjt : u j = ⊤) (hjn : j ≤ n) : u n = ⊤ := by
+  rcases hjn.eq_or_lt with rfl | hjn
+  · exact hjt
+  refine eq_top_iff.2 ?_
+  calc ⊤ = u j + u (n - j) := by rw [hjt, top_add_of_ne_bot (hu _ (by omega))]
+  _ ≤ u (j + (n - j)) := h _ _
+  _ = u n := by rw [Nat.add_sub_cancel' hjn.le]
+
+/-- The real inequality behind Fekete's lemma: if `n = (q + 1) m + s` with `s ≤ m`, then
+`(r / m - C / n) n ≤ (q + 1) r + s a` for `C = m |a - r / m|`. -/
+private lemma _root_.Real.fekete_bound {m n q s : ℕ} {r a : ℝ} (hm : (0 : ℝ) < m)
+    (hn : (0 : ℝ) < n) (hn_eq : (q + 1) * m + s = n) (hs : s ≤ m) :
+    (r / m - m * |a - r / m| / n) * n ≤ (q + 1) * r + s * a := by
+  have hn_real : (n : ℝ) = (q + 1) * m + s := by exact_mod_cast hn_eq.symm
+  have hs_real : (s : ℝ) ≤ m := by exact_mod_cast hs
+  have h_eq : (r / m - m * |a - r / m| / n) * n = (q + 1) * r + s * (r / m) - m * |a - r / m| := by
+    rw [sub_mul, div_mul_cancel₀ _ hn.ne', hn_real]
+    field_simp
+  rw [h_eq]
+  nlinarith [mul_le_mul_of_nonneg_right hs_real (abs_nonneg (a - r / m)),
+    mul_le_mul_of_nonneg_left (neg_abs_le (a - r / m)) (Nat.cast_nonneg (α := ℝ) s)]
+
+/-- **Fekete's lemma** for superadditive sequences of extended reals: if
+`u m + u n ≤ u (m + n)` for all `m, n` and `u n ≠ ⊥` for `n ≠ 0`, then `u n / n` tends to the
+supremum of `u n / n` over `n ≥ 1`. The limit may be `⊤`. -/
+theorem tendsto_div_iSup_of_superadditive (hu : ∀ n ≠ 0, u n ≠ ⊥)
+    (h : ∀ m n, u m + u n ≤ u (m + n)) :
+    Tendsto (fun n : ℕ ↦ u n / n) atTop (𝓝 (⨆ n : ℕ, u (n + 1) / ((n + 1 : ℕ) : EReal))) := by
+  have h_pos {n : ℕ} (hn : n ≠ 0) : (0 : EReal) < n := by exact_mod_cast Nat.pos_of_ne_zero hn
+  refine tendsto_order.2 ⟨fun L hL ↦ ?_, fun L hL ↦ ?_⟩
+  swap
+  · filter_upwards [eventually_ne_atTop 0] with n hn
+    obtain ⟨k, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hn
+    exact (le_iSup (fun k : ℕ ↦ u (k + 1) / ((k + 1 : ℕ) : EReal)) k).trans_lt hL
+  obtain ⟨k, hk⟩ := lt_iSup_iff.1 hL
+  -- the case `u (k + 1) = ⊤`: `u n / n = ⊤` for `n ≥ k + 1`
+  by_cases hkt : u (k + 1) = ⊤
+  · filter_upwards [eventually_ge_atTop (k + 1)] with n hn
+    rw [eq_top_of_superadditive hu h hkt hn,
+      top_div_of_pos_ne_top (h_pos (by omega)) (natCast_ne_top n)]
+    exact hk.trans_le le_top
+  -- otherwise `u (k + 1)` and `u 1` are real
+  have h1t : u 1 ≠ ⊤ := fun h1 ↦ hkt (eq_top_of_superadditive hu h h1 (by omega))
+  obtain ⟨r, hr⟩ : ∃ r : ℝ, u (k + 1) = r := ⟨_, (EReal.coe_toReal hkt (hu _ k.succ_ne_zero)).symm⟩
+  obtain ⟨a, ha⟩ : ∃ a : ℝ, u 1 = a := ⟨_, (EReal.coe_toReal h1t (hu _ one_ne_zero)).symm⟩
+  set m : ℕ := k + 1
+  have hm0 : (0 : ℝ) < m := by positivity
+  obtain ⟨x, hLx, hx⟩ := lt_iff_exists_real_btwn.1 hk
+  rw [hr] at hx
+  have hx : x < r / m := EReal.coe_lt_coe_iff.1 (hx.trans_eq (EReal.coe_div r m).symm)
+  -- the real lower bound `r / m - C / n` of `u n / n` tends to `r / m > x`
+  have h_lim : Tendsto (fun n : ℕ ↦ r / m - m * |a - r / m| / n) atTop (𝓝 (r / m)) := by
+    simpa using (tendsto_const_nhds (x := r / m)).sub
+      (_root_.tendsto_const_div_atTop_nhds_zero_nat (m * |a - r / m|))
+  filter_upwards [eventually_ge_atTop m, h_lim.eventually (lt_mem_nhds hx)] with n hnm hxn
+  have hn0 : n ≠ 0 := by omega
+  refine hLx.trans (lt_of_lt_of_le (EReal.coe_lt_coe_iff.2 hxn) ?_)
+  rw [le_div_iff_mul_le (h_pos hn0) (natCast_ne_top n)]
+  -- write `n = (q + 1) * m + s` with `s < m`
+  obtain ⟨q, hq⟩ : ∃ q, n / m = q + 1 :=
+    Nat.exists_eq_succ_of_ne_zero (Nat.div_pos hnm (by omega)).ne'
+  have hn_eq : (q + 1) * m + n % m = n := by rw [← hq, Nat.div_add_mod']
+  have key := nsmul_add_nsmul_le_of_superadditive h m q (n % m)
+  rw [hn_eq, hr, ha] at key
+  refine le_trans ?_ key
+  have := Real.fekete_bound (r := r) (a := a) hm0 (by exact_mod_cast Nat.pos_of_ne_zero hn0)
+    hn_eq (Nat.mod_lt _ (by omega)).le
+  simp only [nsmul_eq_mul]
+  exact_mod_cast this
+
+end EReal

LMLExplore/EValues/BipolarRate.lean

@@ -0,0 +1,227 @@
+/-
+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.Analysis.Subadditive
+public import LMLExplore.EValues.DPI
+public import Statlib.Divergence.KullbackLeibler.CondKL
+public import Statlib.EValues.Product
+public import Statlib.EValues.RIPr
+
+/-!
+# The optimal growth rate of e-variables against an i.i.d. null
+
+For a law `Q₁` on `𝓧` (the alternative) and a set `S₁` of laws on `𝓧` (the null), the
+`n`-sample e-variables are the e-variables for the `n`-fold products `P ^ n` of the members `P`
+of `S₁`. Their maximal expected logarithm under `Q₁ ^ n`, `maxLogGrowth Q₁ S₁ n`, is Statlib's
+`maxUtility` with `logUtility`, which Statlib's duality
+(`maxUtility_eq_iInf_klIntegral_effectiveSet`) writes as the reverse information projection of
+`Q₁ ^ n` onto the effective null of the `n`-sample null. It is superadditive in `n`, so that
+`maxLogGrowth Q₁ S₁ n / n` converges to its supremum, the bipolar rate `bipolarRate Q₁ S₁`: the
+optimal growth rate of the evidence against the i.i.d. null, per observation. It is at most the
+smallest relative entropy `⨅ P ∈ S₁, klDiv Q₁ P` from `Q₁` to the null, and can be smaller
+(Ram and Ramdas, Proposition 5.4).
+
+The statements assume that `Q₁` is a probability measure and that the members of the null are
+finite measures (probability measures for the comparison with the relative entropy), and nothing
+else: no domination, convexity or compactness.
+
+## Main definitions
+
+* `ProbabilityTheory.maxLogGrowth Q₁ S₁ n`: the maximal expected logarithm, under the `n`-fold
+  product of `Q₁`, of the e-variables for the `n`-fold products of the members of `S₁`.
+* `ProbabilityTheory.bipolarRate Q₁ S₁`: the supremum over `n ≥ 1` of `maxLogGrowth Q₁ S₁ n / n`.
+
+## Main statements
+
+* `ProbabilityTheory.maxLogGrowth_add_le`: `maxLogGrowth Q₁ S₁` is superadditive [RR26, Lemma 3.2].
+* `ProbabilityTheory.tendsto_maxLogGrowth_div_bipolarRate`: `maxLogGrowth Q₁ S₁ n / n` tends to
+  the bipolar rate [RR26, Lemma 3.2].
+* `ProbabilityTheory.maxLogGrowth_le_mul_bipolarRate`:
+  `maxLogGrowth Q₁ S₁ n ≤ n * bipolarRate Q₁ S₁` for `n ≠ 0`.
+* `ProbabilityTheory.maxLogGrowth_anti`, `ProbabilityTheory.bipolarRate_anti`: both are antitone
+  in the null.
+* `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].
+
+## References
+
+* [RR26] A. Ram and A. Ramdas, *The optimal betting wealth growth rate*, arXiv:2604.25280v1.
+-/
+
+public section
+
+open MeasureTheory Filter InformationTheory
+open scoped ENNReal Topology
+
+namespace ProbabilityTheory
+
+variable {𝓧 : Type*} {m𝓧 : MeasurableSpace 𝓧} {Q₁ P : Measure 𝓧} {S₁ T₁ : Set (Measure 𝓧)}
+  {n : ℕ}
+
+/-- The maximal expected logarithm of an `n`-sample e-variable for the i.i.d. laws of `S₁`, under
+the `n`-fold product of `Q₁`: the supremum of `∫ᵉ x, log (E x) ∂Q₁ ^ n` over the functions
+`E : (Fin n → 𝓧) → ℝ≥0∞` that are e-variables for `{P ^ n | P ∈ S₁}`. -/
+noncomputable def maxLogGrowth (Q₁ : Measure 𝓧) (S₁ : Set (Measure 𝓧)) (n : ℕ) : EReal :=
+  maxUtility (Measure.pi fun _ : Fin n ↦ Q₁) ((fun P ↦ Measure.pi fun _ : Fin n ↦ P) '' S₁)
+    logUtility
+
+/-- The bipolar rate of `Q₁` against the i.i.d. null generated by `S₁`: the supremum over `n ≥ 1`
+of the maximal expected logarithm of an `n`-sample e-variable, divided by `n`. It is also the limit
+of these normalized values [RR26, Lemma 3.2] (`tendsto_maxLogGrowth_div_bipolarRate`), and Ram
+and Ramdas show that it is the optimal growth rate of e-processes against the null. -/
+noncomputable def bipolarRate (Q₁ : Measure 𝓧) (S₁ : Set (Measure 𝓧)) : EReal :=
+  ⨆ n : ℕ, maxLogGrowth Q₁ S₁ (n + 1) / ((n + 1 : ℕ) : EReal)
+
+lemma maxLogGrowth_def (Q₁ : Measure 𝓧) (S₁ : Set (Measure 𝓧)) (n : ℕ) :
+    maxLogGrowth Q₁ S₁ n = maxUtility (Measure.pi fun _ : Fin n ↦ Q₁)
+      ((fun P ↦ Measure.pi fun _ : Fin n ↦ P) '' S₁) logUtility :=
+  (rfl)
+
+lemma bipolarRate_def (Q₁ : Measure 𝓧) (S₁ : Set (Measure 𝓧)) :
+    bipolarRate Q₁ S₁ = ⨆ n : ℕ, maxLogGrowth Q₁ S₁ (n + 1) / ((n + 1 : ℕ) : EReal) :=
+  (rfl)
+
+/-- The maximal expected logarithm of an `n`-sample e-variable is nonnegative, as the constant `1`
+is an e-variable. -/
+lemma maxLogGrowth_nonneg (Q₁ : Measure 𝓧) (S₁ : Set (Measure 𝓧)) (n : ℕ) :
+    0 ≤ maxLogGrowth Q₁ S₁ n :=
+  maxUtility_nonneg _
+
+/-- The normalized maximal expected logarithm of an `n`-sample e-variable is at most the bipolar
+rate, for `n ≠ 0`. -/
+lemma maxLogGrowth_div_le_bipolarRate (Q₁ : Measure 𝓧) (S₁ : Set (Measure 𝓧)) (hn : n ≠ 0) :
+    maxLogGrowth Q₁ S₁ n / n ≤ bipolarRate Q₁ S₁ := by
+  obtain ⟨k, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hn
+  exact le_iSup (fun k : ℕ ↦ maxLogGrowth Q₁ S₁ (k + 1) / ((k + 1 : ℕ) : EReal)) k
+
+/-- The bipolar rate is at most `c` if and only if `maxLogGrowth Q₁ S₁ n ≤ n * c` for every
+`n ≠ 0`. -/
+lemma bipolarRate_le_iff {c : EReal} :
+    bipolarRate Q₁ S₁ ≤ c ↔ ∀ n ≠ 0, maxLogGrowth Q₁ S₁ n ≤ n * c := by
+  have h (n : ℕ) (hn : n ≠ 0) : maxLogGrowth Q₁ S₁ n / n ≤ c ↔ maxLogGrowth Q₁ S₁ n ≤ n * c :=
+    EReal.div_le_iff_le_mul (by exact_mod_cast Nat.pos_of_ne_zero hn) (EReal.natCast_ne_top _)
+  refine ⟨fun hc n hn ↦ (h n hn).1 ((maxLogGrowth_div_le_bipolarRate Q₁ S₁ hn).trans hc),
+    fun hc ↦ ?_⟩
+  exact iSup_le fun n ↦ (h _ n.succ_ne_zero).2 (hc _ n.succ_ne_zero)
+
+/-- The maximal expected logarithm of an `n`-sample e-variable is antitone in the null. -/
+@[gcongr]
+lemma maxLogGrowth_anti (h : S₁ ⊆ T₁) : maxLogGrowth Q₁ T₁ n ≤ maxLogGrowth Q₁ S₁ n :=
+  maxUtility_anti (Set.image_mono h)
+
+/-- With one observation, `maxLogGrowth` is the maximal expected logarithm of an e-variable. -/
+@[simp]
+lemma maxLogGrowth_one (Q₁ : Measure 𝓧) (S₁ : Set (Measure 𝓧)) :
+    maxLogGrowth Q₁ S₁ 1 = maxUtility Q₁ S₁ logUtility := by
+  rcases isEmpty_or_nonempty 𝓧 with h𝓧 | h𝓧
+  · -- on an empty space every measure is `0`, and both sides vanish
+    rw [maxLogGrowth_def, Measure.eq_zero_of_isEmpty (Measure.pi fun _ : Fin 1 ↦ Q₁),
+      Measure.eq_zero_of_isEmpty Q₁, maxUtility_zero_measure, maxUtility_zero_measure]
+  set e := (MeasurableEquiv.funUnique (Fin 1) 𝓧).symm
+  have h_map (P : Measure 𝓧) : P.map e = Measure.pi fun _ : Fin 1 ↦ P :=
+    (measurePreserving_funUnique P (Fin 1)).symm.map_eq
+  rw [← e.measurableEmbedding.maxUtility_map_eq, h_map, maxLogGrowth_def]
+  congr 1
+  ext μ
+  simp only [Set.mem_image, Set.mem_ofPred_eq, h_map]
+
+/-- **Superadditivity** of the maximal expected logarithm of e-variables for an i.i.d. null
+[RR26, Lemma 3.2]: the product of an `m`-sample e-variable and an `n`-sample e-variable, on
+disjoint blocks of observations, is an `m + n`-sample e-variable (Statlib's `IsEVar.prod`, through
+`maxUtility_prod_eq_add`). -/
+theorem maxLogGrowth_add_le (Q₁ : Measure 𝓧) [IsProbabilityMeasure Q₁]
+    (hS₁ : ∀ P ∈ S₁, IsFiniteMeasure P) (m n : ℕ) :
+    maxLogGrowth Q₁ S₁ m + maxLogGrowth Q₁ S₁ n ≤ maxLogGrowth Q₁ S₁ (m + n) := by
+  -- split the first `m + n` observations into the first `m` and the last `n`
+  let e : (Fin (m + n) → 𝓧) ≃ᵐ (Fin m → 𝓧) × (Fin n → 𝓧) :=
+    (MeasurableEquiv.piCongrLeft (fun _ ↦ 𝓧) finSumFinEquiv).symm.trans
+      (MeasurableEquiv.sumPiEquivProdPi fun _ ↦ 𝓧)
+  have h_map (P : Measure 𝓧) [SigmaFinite P] :
+      (Measure.pi fun _ : Fin (m + n) ↦ P).map e =
+        (Measure.pi fun _ : Fin m ↦ P).prod (Measure.pi fun _ : Fin n ↦ P) :=
+    ((measurePreserving_sumPiEquivProdPi fun _ ↦ P).comp
+      ((measurePreserving_piCongrLeft (fun _ ↦ P) finSumFinEquiv).symm _)).map_eq
+  have h_fin (k : ℕ) :
+      ∀ μ ∈ (fun P ↦ Measure.pi fun _ : Fin k ↦ P) '' S₁, IsFiniteMeasure μ := by
+    rintro _ ⟨P, hP, rfl⟩
+    have := hS₁ P hP
+    infer_instance
+  calc maxLogGrowth Q₁ S₁ m + maxLogGrowth Q₁ S₁ n
+  _ = maxUtility ((Measure.pi fun _ : Fin m ↦ Q₁).prod (Measure.pi fun _ : Fin n ↦ Q₁))
+      (Set.image2 Measure.prod ((fun P ↦ Measure.pi fun _ : Fin m ↦ P) '' S₁)
+        ((fun P ↦ Measure.pi fun _ : Fin n ↦ P) '' S₁)) logUtility :=
+    by rw [maxLogGrowth_def, maxLogGrowth_def, maxUtility_prod_eq_add _ _ (h_fin m) (h_fin n)]
+  _ ≤ maxUtility ((Measure.pi fun _ : Fin (m + n) ↦ Q₁).map e)
+      {μ.map e | μ ∈ (fun P ↦ Measure.pi fun _ : Fin (m + n) ↦ P) '' S₁} logUtility := by
+    rw [h_map]
+    refine maxUtility_anti ?_
+    rintro _ ⟨_, ⟨P, hP, rfl⟩, rfl⟩
+    have := hS₁ P hP
+    exact ⟨_, ⟨P, hP, rfl⟩, _, ⟨P, hP, rfl⟩, (h_map P).symm⟩
+  _ ≤ maxLogGrowth Q₁ S₁ (m + n) := by rw [maxLogGrowth_def]; exact maxUtility_map_le _ e.measurable
+
+/-- The maximal expected logarithm of an `n`-sample e-variable is at most `n` times the bipolar
+rate, for `n ≠ 0`. -/
+lemma maxLogGrowth_le_mul_bipolarRate (Q₁ : Measure 𝓧) (S₁ : Set (Measure 𝓧)) (hn : n ≠ 0) :
+    maxLogGrowth Q₁ S₁ n ≤ n * bipolarRate Q₁ S₁ :=
+  bipolarRate_le_iff.1 le_rfl n hn
+
+/-- The bipolar rate is nonnegative. -/
+lemma bipolarRate_nonneg (Q₁ : Measure 𝓧) (S₁ : Set (Measure 𝓧)) : 0 ≤ bipolarRate Q₁ S₁ :=
+  (EReal.div_nonneg (maxLogGrowth_nonneg _ _ _) (by positivity)).trans
+    (maxLogGrowth_div_le_bipolarRate Q₁ S₁ one_ne_zero)
+
+/-- The bipolar rate is antitone in the null. -/
+@[gcongr]
+lemma bipolarRate_anti (h : S₁ ⊆ T₁) : bipolarRate Q₁ T₁ ≤ bipolarRate Q₁ S₁ :=
+  bipolarRate_le_iff.2 fun _ hn ↦ (maxLogGrowth_anti h).trans
+    (maxLogGrowth_le_mul_bipolarRate Q₁ S₁ hn)
+
+/-- **Fekete's lemma** for the maximal expected logarithm of e-variables for an i.i.d. null:
+`maxLogGrowth Q₁ S₁ n / n` tends to its supremum, the bipolar rate [RR26, Lemma 3.2]. The limit
+may be `⊤`. -/
+theorem tendsto_maxLogGrowth_div_bipolarRate (Q₁ : Measure 𝓧) [IsProbabilityMeasure Q₁]
+    (hS₁ : ∀ P ∈ S₁, IsFiniteMeasure P) :
+    Tendsto (fun n : ℕ ↦ maxLogGrowth Q₁ S₁ n / n) atTop (𝓝 (bipolarRate Q₁ S₁)) :=
+  bipolarRate_def Q₁ S₁ ▸ EReal.tendsto_div_iSup_of_superadditive
+    (fun _ _ ↦ ne_bot_of_le_ne_bot EReal.zero_ne_bot (maxLogGrowth_nonneg _ _ _))
+    (maxLogGrowth_add_le Q₁ hS₁)
+
+/-- The maximal expected logarithm of an `n`-sample e-variable is at most `n` times the relative
+entropy from `Q₁` to any member `P` of the null: this is its value for the null `{P}`, by Statlib's
+`maxUtility_singleton_eq_klDiv` and the tensorization of the relative entropy
+[RR26, proof of Theorem 4.1]. -/
+lemma maxLogGrowth_le_mul_klDiv (Q₁ : Measure 𝓧) [IsProbabilityMeasure Q₁] (hP : P ∈ S₁)
+    [IsProbabilityMeasure P] (n : ℕ) :
+    maxLogGrowth Q₁ S₁ n ≤ n * (klDiv Q₁ P : EReal) := by
+  calc maxLogGrowth Q₁ S₁ n
+  _ ≤ maxUtility (Measure.pi fun _ : Fin n ↦ Q₁) {Measure.pi fun _ : Fin n ↦ P} logUtility :=
+    maxUtility_anti (Set.singleton_subset_iff.2 ⟨P, hP, rfl⟩)
+  _ = n * (klDiv Q₁ P : EReal) := by
+    rw [maxUtility_singleton_eq_klDiv, klDiv_pi_const]
+    simp
+
+/-- The bipolar rate is at most the relative entropy from `Q₁` to any member of the null. -/
+lemma bipolarRate_le_klDiv (Q₁ : Measure 𝓧) [IsProbabilityMeasure Q₁] (hP : P ∈ S₁)
+    [IsProbabilityMeasure P] :
+    bipolarRate Q₁ S₁ ≤ klDiv Q₁ P :=
+  bipolarRate_le_iff.2 fun n _ ↦ maxLogGrowth_le_mul_klDiv Q₁ hP n
+
+/-- The bipolar rate is at most the smallest relative entropy from `Q₁` to the null,
+$\mathrm{KL}_{\inf}(Q_1,\mathcal P_1)$ [RR26, proof of Theorem 4.1]. The inequality can be
+strict. -/
+theorem bipolarRate_le_iInf_klDiv (Q₁ : Measure 𝓧) [IsProbabilityMeasure Q₁]
+    (hS₁ : ∀ P ∈ S₁, IsProbabilityMeasure P) :
+    bipolarRate Q₁ S₁ ≤ (⨅ P ∈ S₁, klDiv Q₁ P : ℝ≥0∞) := by
+  rw [← EReal.coe_toENNReal (bipolarRate_nonneg Q₁ S₁), EReal.coe_ennreal_le_coe_ennreal_iff]
+  refine le_iInf₂ fun P hP ↦ ?_
+  have := hS₁ P hP
+  rw [← EReal.toENNReal_coe (x := klDiv Q₁ P)]
+  exact EReal.toENNReal_le_toENNReal (bipolarRate_le_klDiv Q₁ hP)
+
+end ProbabilityTheory