From d6db50cd8afb447460d80900111a0b404fe7e779 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 13:37:35 +0100 Subject: [PATCH 1/6] feat: n observations are worth n times one when one observation attains the smallest relative entropy MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit If `⨅ P ∈ S₁, klDiv Q₁ P ≤ maxLogGrowth Q₁ S₁ 1`, then `maxLogGrowth Q₁ S₁ n = n * maxLogGrowth Q₁ S₁ 1` for every `n ≠ 0` and the bipolar rate is the smallest relative entropy (EValues roadmap, Layer 6.1), with no semicontinuity, convexity or compactness of the null. Also `n * maxLogGrowth Q₁ S₁ 1 ≤ maxLogGrowth Q₁ S₁ n` and `maxLogGrowth Q₁ S₁ 1 ≤ bipolarRate Q₁ S₁`. Co-Authored-By: Claude Fable 5.2 Claude-Session: https://claude.ai/code/session_0196ftMVbgjSJzPQEwdek3kM --- .../EValues/BipolarRate/SingleLetter.lean | 97 +++++++++++++++++++ 1 file changed, 97 insertions(+) create mode 100644 LMLExplore/EValues/BipolarRate/SingleLetter.lean diff --git a/LMLExplore/EValues/BipolarRate/SingleLetter.lean b/LMLExplore/EValues/BipolarRate/SingleLetter.lean new file mode 100644 index 00000000..1021e8f6 --- /dev/null +++ b/LMLExplore/EValues/BipolarRate/SingleLetter.lean @@ -0,0 +1,97 @@ +/- +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 + +/-! +# When one observation attains the smallest relative entropy + +For a probability measure `Q₁` and a null `S₁` on a measurable space, the maximal expected +logarithm `maxLogGrowth Q₁ S₁ n` of an `n`-sample e-variable is at least `n` times that of one +observation, by superadditivity, and at most `n` times the smallest relative entropy from `Q₁` to +the null. If one observation already attains the smallest relative entropy, that is, if +`⨅ P ∈ S₁, klDiv Q₁ P ≤ maxLogGrowth Q₁ S₁ 1`, the three quantities agree: `n` observations are +worth exactly `n` times one, and the bipolar rate is the smallest relative entropy. No +semicontinuity, convexity or compactness of the null is assumed. + +For a weakly compact convex null the hypothesis holds [RR26, Proposition 4.5]. + +## Main statements + +* `ProbabilityTheory.mul_maxLogGrowth_one_le`: `n * maxLogGrowth Q₁ S₁ 1 ≤ maxLogGrowth Q₁ S₁ n`. +* `ProbabilityTheory.maxLogGrowth_one_le_bipolarRate`: the growth of one observation is at most + the bipolar rate. +* `ProbabilityTheory.bipolarRate_eq_iInf_klDiv_of_iInf_klDiv_le_maxLogGrowth_one`: if one + observation attains the smallest relative entropy, the bipolar rate is the smallest relative + entropy. +* `ProbabilityTheory.maxLogGrowth_eq_mul_of_iInf_klDiv_le_maxLogGrowth_one`: and then + `maxLogGrowth Q₁ S₁ n = n * maxLogGrowth Q₁ S₁ 1`. + +## References + +* [RR26] A. Ram and A. Ramdas, *The optimal betting wealth growth rate*, arXiv:2604.25280v1. +-/ + +public section + +open MeasureTheory InformationTheory +open scoped ENNReal + +namespace ProbabilityTheory + +variable {𝓧 : Type*} {m𝓧 : MeasurableSpace 𝓧} {Q₁ : Measure 𝓧} {S₁ : Set (Measure 𝓧)} {n : ℕ} + +/-- The maximal expected logarithm of an `n`-sample e-variable is at least `n` times that of one +observation: superadditivity, iterated. -/ +theorem mul_maxLogGrowth_one_le (Q₁ : Measure 𝓧) [IsProbabilityMeasure Q₁] + (hS₁ : ∀ P ∈ S₁, IsFiniteMeasure P) (n : ℕ) : + n * maxLogGrowth Q₁ S₁ 1 ≤ maxLogGrowth Q₁ S₁ n := by + induction n with + | zero => + rw [Nat.cast_zero, zero_mul] + exact maxLogGrowth_nonneg Q₁ S₁ 0 + | succ n ih => + rw [Nat.cast_add, Nat.cast_one, EReal.right_distrib_of_nonneg (Nat.cast_nonneg' n) zero_le_one, + one_mul] + exact (add_le_add_left ih _).trans (maxLogGrowth_add_le Q₁ hS₁ n 1) + +/-- The maximal expected logarithm of a one-observation e-variable is at most the bipolar +rate. -/ +theorem maxLogGrowth_one_le_bipolarRate (Q₁ : Measure 𝓧) (S₁ : Set (Measure 𝓧)) : + maxLogGrowth Q₁ S₁ 1 ≤ bipolarRate Q₁ S₁ := by + simpa using maxLogGrowth_div_le_bipolarRate Q₁ S₁ one_ne_zero + +/-- If one observation attains the smallest relative entropy from `Q₁` to the null, the bipolar +rate is the maximal expected logarithm of a one-observation e-variable. -/ +theorem bipolarRate_eq_maxLogGrowth_one_of_iInf_klDiv_le (Q₁ : Measure 𝓧) + [IsProbabilityMeasure Q₁] (hS₁ : ∀ P ∈ S₁, IsProbabilityMeasure P) + (h : ((⨅ P ∈ S₁, klDiv Q₁ P : ℝ≥0∞) : EReal) ≤ maxLogGrowth Q₁ S₁ 1) : + bipolarRate Q₁ S₁ = maxLogGrowth Q₁ S₁ 1 := + le_antisymm ((bipolarRate_le_iInf_klDiv Q₁ hS₁).trans h) (maxLogGrowth_one_le_bipolarRate Q₁ S₁) + +/-- If one observation attains the smallest relative entropy from `Q₁` to the null, the bipolar +rate is the smallest relative entropy. -/ +theorem bipolarRate_eq_iInf_klDiv_of_iInf_klDiv_le_maxLogGrowth_one (Q₁ : Measure 𝓧) + [IsProbabilityMeasure Q₁] (hS₁ : ∀ P ∈ S₁, IsProbabilityMeasure P) + (h : ((⨅ P ∈ S₁, klDiv Q₁ P : ℝ≥0∞) : EReal) ≤ maxLogGrowth Q₁ S₁ 1) : + bipolarRate Q₁ S₁ = ((⨅ P ∈ S₁, klDiv Q₁ P : ℝ≥0∞) : EReal) := + le_antisymm (bipolarRate_le_iInf_klDiv Q₁ hS₁) (h.trans (maxLogGrowth_one_le_bipolarRate Q₁ S₁)) + +/-- If one observation attains the smallest relative entropy from `Q₁` to the null, then `n` +observations are worth `n` times one: the maximal expected logarithm of an `n`-sample e-variable +is `n` times that of a one-observation e-variable. The common value may be infinite. -/ +theorem maxLogGrowth_eq_mul_of_iInf_klDiv_le_maxLogGrowth_one (Q₁ : Measure 𝓧) + [IsProbabilityMeasure Q₁] (hS₁ : ∀ P ∈ S₁, IsProbabilityMeasure P) + (h : ((⨅ P ∈ S₁, klDiv Q₁ P : ℝ≥0∞) : EReal) ≤ maxLogGrowth Q₁ S₁ 1) (hn : n ≠ 0) : + maxLogGrowth Q₁ S₁ n = n * maxLogGrowth Q₁ S₁ 1 := by + refine le_antisymm ?_ (mul_maxLogGrowth_one_le Q₁ (fun P hP ↦ ?_) n) + · rw [← bipolarRate_eq_maxLogGrowth_one_of_iInf_klDiv_le Q₁ hS₁ h] + exact maxLogGrowth_le_mul_bipolarRate Q₁ S₁ hn + · have := hS₁ P hP + infer_instance + +end ProbabilityTheory From 363193d5a958e2f8bcef4a43d64ac6faefdf0c6b Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 14:11:33 +0100 Subject: [PATCH 2/6] =?UTF-8?q?fix:=20general=20forms=20under=20bipolarRat?= =?UTF-8?q?e=20=E2=89=A4=20maxLogGrowth=201,=20reuse=20iterated=20superadd?= =?UTF-8?q?itivity,=20cite=20EVR26?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Add `bipolarRate_eq_maxLogGrowth_one_of_le` and `maxLogGrowth_eq_mul_of_bipolarRate_le` (finite measures in the null), and derive the KL-hypothesis forms from them. - Prove `mul_maxLogGrowth_one_le` from `EReal.nsmul_le_of_superadditive`. - State `n ≠ 0` in the docstrings, and credit [EVR26, Note 11, Theorem 9]. Co-Authored-By: Claude Code --- .../EValues/BipolarRate/SingleLetter.lean | 68 ++++++++++++------- 1 file changed, 43 insertions(+), 25 deletions(-) diff --git a/LMLExplore/EValues/BipolarRate/SingleLetter.lean b/LMLExplore/EValues/BipolarRate/SingleLetter.lean index 1021e8f6..c1b880fc 100644 --- a/LMLExplore/EValues/BipolarRate/SingleLetter.lean +++ b/LMLExplore/EValues/BipolarRate/SingleLetter.lean @@ -14,9 +14,11 @@ For a probability measure `Q₁` and a null `S₁` on a measurable space, the ma logarithm `maxLogGrowth Q₁ S₁ n` of an `n`-sample e-variable is at least `n` times that of one observation, by superadditivity, and at most `n` times the smallest relative entropy from `Q₁` to the null. If one observation already attains the smallest relative entropy, that is, if -`⨅ P ∈ S₁, klDiv Q₁ P ≤ maxLogGrowth Q₁ S₁ 1`, the three quantities agree: `n` observations are -worth exactly `n` times one, and the bipolar rate is the smallest relative entropy. No -semicontinuity, convexity or compactness of the null is assumed. +`⨅ P ∈ S₁, klDiv Q₁ P ≤ maxLogGrowth Q₁ S₁ 1`, the three quantities agree: for every `n ≠ 0`, +`n` observations are worth exactly `n` times one, and the bipolar rate is the smallest relative +entropy [EVR26, Note 11, Theorem 9]. No semicontinuity, convexity or compactness of the null is +assumed. Both conclusions already follow from the weaker hypothesis +`bipolarRate Q₁ S₁ ≤ maxLogGrowth Q₁ S₁ 1`, the first for a null of finite measures. For a weakly compact convex null the hypothesis holds [RR26, Proposition 4.5]. @@ -25,14 +27,20 @@ For a weakly compact convex null the hypothesis holds [RR26, Proposition 4.5]. * `ProbabilityTheory.mul_maxLogGrowth_one_le`: `n * maxLogGrowth Q₁ S₁ 1 ≤ maxLogGrowth Q₁ S₁ n`. * `ProbabilityTheory.maxLogGrowth_one_le_bipolarRate`: the growth of one observation is at most the bipolar rate. +* `ProbabilityTheory.bipolarRate_eq_maxLogGrowth_one_of_le`: if the bipolar rate is at most the + growth of one observation, the two are equal. +* `ProbabilityTheory.maxLogGrowth_eq_mul_of_bipolarRate_le`: if the bipolar rate is at most the + growth of one observation, then `maxLogGrowth Q₁ S₁ n = n * maxLogGrowth Q₁ S₁ 1` for `n ≠ 0`. * `ProbabilityTheory.bipolarRate_eq_iInf_klDiv_of_iInf_klDiv_le_maxLogGrowth_one`: if one observation attains the smallest relative entropy, the bipolar rate is the smallest relative - entropy. + entropy [EVR26, Note 11, Theorem 9]. * `ProbabilityTheory.maxLogGrowth_eq_mul_of_iInf_klDiv_le_maxLogGrowth_one`: and then - `maxLogGrowth Q₁ S₁ n = n * maxLogGrowth Q₁ S₁ 1`. + `maxLogGrowth Q₁ S₁ n = n * maxLogGrowth Q₁ S₁ 1` for `n ≠ 0` [EVR26, Note 11, Theorem 9]. ## References +* [EVR26] *Answers to open questions in e-values and anytime-valid inference*, Note 11, and its + Lean library `EValuesResearch`, github.com/RemyDegenne/evalues_research, 2026. * [RR26] A. Ram and A. Ramdas, *The optimal betting wealth growth rate*, arXiv:2604.25280v1. -/ @@ -50,14 +58,11 @@ observation: superadditivity, iterated. -/ theorem mul_maxLogGrowth_one_le (Q₁ : Measure 𝓧) [IsProbabilityMeasure Q₁] (hS₁ : ∀ P ∈ S₁, IsFiniteMeasure P) (n : ℕ) : n * maxLogGrowth Q₁ S₁ 1 ≤ maxLogGrowth Q₁ S₁ n := by - induction n with - | zero => - rw [Nat.cast_zero, zero_mul] - exact maxLogGrowth_nonneg Q₁ S₁ 0 - | succ n ih => - rw [Nat.cast_add, Nat.cast_one, EReal.right_distrib_of_nonneg (Nat.cast_nonneg' n) zero_le_one, - one_mul] - exact (add_le_add_left ih _).trans (maxLogGrowth_add_le Q₁ hS₁ n 1) + cases n with + | zero => simpa using maxLogGrowth_nonneg Q₁ S₁ 0 + | succ q => + simpa [EReal.nsmul_eq_mul] using + EReal.nsmul_le_of_superadditive (maxLogGrowth_add_le Q₁ hS₁) 1 q /-- The maximal expected logarithm of a one-observation e-variable is at most the bipolar rate. -/ @@ -65,33 +70,46 @@ theorem maxLogGrowth_one_le_bipolarRate (Q₁ : Measure 𝓧) (S₁ : Set (Measu maxLogGrowth Q₁ S₁ 1 ≤ bipolarRate Q₁ S₁ := by simpa using maxLogGrowth_div_le_bipolarRate Q₁ S₁ one_ne_zero +/-- If the bipolar rate is at most the maximal expected logarithm of a one-observation +e-variable, the two are equal. -/ +theorem bipolarRate_eq_maxLogGrowth_one_of_le (h : bipolarRate Q₁ S₁ ≤ maxLogGrowth Q₁ S₁ 1) : + bipolarRate Q₁ S₁ = maxLogGrowth Q₁ S₁ 1 := + le_antisymm h (maxLogGrowth_one_le_bipolarRate Q₁ S₁) + +/-- If the bipolar rate is at most the maximal expected logarithm of a one-observation +e-variable, then for `n ≠ 0`, `n` observations are worth `n` times one. -/ +theorem maxLogGrowth_eq_mul_of_bipolarRate_le (Q₁ : Measure 𝓧) [IsProbabilityMeasure Q₁] + (hS₁ : ∀ P ∈ S₁, IsFiniteMeasure P) (h : bipolarRate Q₁ S₁ ≤ maxLogGrowth Q₁ S₁ 1) + (hn : n ≠ 0) : maxLogGrowth Q₁ S₁ n = n * maxLogGrowth Q₁ S₁ 1 := + le_antisymm ((maxLogGrowth_le_mul_bipolarRate Q₁ S₁ hn).trans (by gcongr)) + (mul_maxLogGrowth_one_le Q₁ hS₁ n) + /-- If one observation attains the smallest relative entropy from `Q₁` to the null, the bipolar -rate is the maximal expected logarithm of a one-observation e-variable. -/ +rate is the maximal expected logarithm of a one-observation e-variable +[EVR26, Note 11, Theorem 9]. -/ theorem bipolarRate_eq_maxLogGrowth_one_of_iInf_klDiv_le (Q₁ : Measure 𝓧) [IsProbabilityMeasure Q₁] (hS₁ : ∀ P ∈ S₁, IsProbabilityMeasure P) (h : ((⨅ P ∈ S₁, klDiv Q₁ P : ℝ≥0∞) : EReal) ≤ maxLogGrowth Q₁ S₁ 1) : bipolarRate Q₁ S₁ = maxLogGrowth Q₁ S₁ 1 := - le_antisymm ((bipolarRate_le_iInf_klDiv Q₁ hS₁).trans h) (maxLogGrowth_one_le_bipolarRate Q₁ S₁) + bipolarRate_eq_maxLogGrowth_one_of_le ((bipolarRate_le_iInf_klDiv Q₁ hS₁).trans h) /-- If one observation attains the smallest relative entropy from `Q₁` to the null, the bipolar -rate is the smallest relative entropy. -/ +rate is the smallest relative entropy [EVR26, Note 11, Theorem 9]. -/ theorem bipolarRate_eq_iInf_klDiv_of_iInf_klDiv_le_maxLogGrowth_one (Q₁ : Measure 𝓧) [IsProbabilityMeasure Q₁] (hS₁ : ∀ P ∈ S₁, IsProbabilityMeasure P) (h : ((⨅ P ∈ S₁, klDiv Q₁ P : ℝ≥0∞) : EReal) ≤ maxLogGrowth Q₁ S₁ 1) : bipolarRate Q₁ S₁ = ((⨅ P ∈ S₁, klDiv Q₁ P : ℝ≥0∞) : EReal) := le_antisymm (bipolarRate_le_iInf_klDiv Q₁ hS₁) (h.trans (maxLogGrowth_one_le_bipolarRate Q₁ S₁)) -/-- If one observation attains the smallest relative entropy from `Q₁` to the null, then `n` -observations are worth `n` times one: the maximal expected logarithm of an `n`-sample e-variable -is `n` times that of a one-observation e-variable. The common value may be infinite. -/ +/-- If one observation attains the smallest relative entropy from `Q₁` to the null, then for +`n ≠ 0`, `n` observations are worth `n` times one: the maximal expected logarithm of an `n`-sample +e-variable is `n` times that of a one-observation e-variable. The common value may be infinite +[EVR26, Note 11, Theorem 9]. -/ theorem maxLogGrowth_eq_mul_of_iInf_klDiv_le_maxLogGrowth_one (Q₁ : Measure 𝓧) [IsProbabilityMeasure Q₁] (hS₁ : ∀ P ∈ S₁, IsProbabilityMeasure P) (h : ((⨅ P ∈ S₁, klDiv Q₁ P : ℝ≥0∞) : EReal) ≤ maxLogGrowth Q₁ S₁ 1) (hn : n ≠ 0) : - maxLogGrowth Q₁ S₁ n = n * maxLogGrowth Q₁ S₁ 1 := by - refine le_antisymm ?_ (mul_maxLogGrowth_one_le Q₁ (fun P hP ↦ ?_) n) - · rw [← bipolarRate_eq_maxLogGrowth_one_of_iInf_klDiv_le Q₁ hS₁ h] - exact maxLogGrowth_le_mul_bipolarRate Q₁ S₁ hn - · have := hS₁ P hP - infer_instance + maxLogGrowth Q₁ S₁ n = n * maxLogGrowth Q₁ S₁ 1 := + maxLogGrowth_eq_mul_of_bipolarRate_le Q₁ (fun P hP ↦ have := hS₁ P hP; inferInstance) + ((bipolarRate_le_iInf_klDiv Q₁ hS₁).trans h) hn end ProbabilityTheory From 136dbdfdd118eadfaa36ea174ba4a0f7d9365e03 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 14:29:12 +0100 Subject: [PATCH 3/6] doc: state precisely what the weaker bipolar-rate hypothesis gives Co-Authored-By: Claude Code --- LMLExplore/EValues/BipolarRate/SingleLetter.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/LMLExplore/EValues/BipolarRate/SingleLetter.lean b/LMLExplore/EValues/BipolarRate/SingleLetter.lean index c1b880fc..3638fe58 100644 --- a/LMLExplore/EValues/BipolarRate/SingleLetter.lean +++ b/LMLExplore/EValues/BipolarRate/SingleLetter.lean @@ -17,8 +17,9 @@ the null. If one observation already attains the smallest relative entropy, that `⨅ P ∈ S₁, klDiv Q₁ P ≤ maxLogGrowth Q₁ S₁ 1`, the three quantities agree: for every `n ≠ 0`, `n` observations are worth exactly `n` times one, and the bipolar rate is the smallest relative entropy [EVR26, Note 11, Theorem 9]. No semicontinuity, convexity or compactness of the null is -assumed. Both conclusions already follow from the weaker hypothesis -`bipolarRate Q₁ S₁ ≤ maxLogGrowth Q₁ S₁ 1`, the first for a null of finite measures. +assumed. The weaker hypothesis `bipolarRate Q₁ S₁ ≤ maxLogGrowth Q₁ S₁ 1` already gives +`bipolarRate Q₁ S₁ = maxLogGrowth Q₁ S₁ 1` and, for a null of finite measures, +`maxLogGrowth Q₁ S₁ n = n * maxLogGrowth Q₁ S₁ 1` for `n ≠ 0`. For a weakly compact convex null the hypothesis holds [RR26, Proposition 4.5]. From 225a577dcf6825dff4bd9fc56b41a5dcc9b5fe57 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 15:04:07 +0100 Subject: [PATCH 4/6] refactor: place the general growth bounds next to their neighbours in BipolarRate Move mul_maxLogGrowth_one_le and maxLogGrowth_one_le_bipolarRate into LMLExplore/EValues/BipolarRate.lean, after maxLogGrowth_le_mul_bipolarRate, now that #414 has landed. SingleLetter.lean keeps only the consequences of the single-letter hypotheses. Co-Authored-By: Claude Code --- LMLExplore/EValues/BipolarRate.lean | 20 +++++++++++++++++++ .../EValues/BipolarRate/SingleLetter.lean | 20 ------------------- 2 files changed, 20 insertions(+), 20 deletions(-) diff --git a/LMLExplore/EValues/BipolarRate.lean b/LMLExplore/EValues/BipolarRate.lean index d0719966..723faafa 100644 --- a/LMLExplore/EValues/BipolarRate.lean +++ b/LMLExplore/EValues/BipolarRate.lean @@ -42,6 +42,9 @@ else: no domination, convexity or compactness. the bipolar rate [RR26, Lemma 3.2]. * `ProbabilityTheory.maxLogGrowth_le_mul_bipolarRate`: `maxLogGrowth Q₁ S₁ n ≤ n * bipolarRate Q₁ S₁` for `n ≠ 0`. +* `ProbabilityTheory.mul_maxLogGrowth_one_le`: `n * maxLogGrowth Q₁ S₁ 1 ≤ maxLogGrowth Q₁ S₁ n`. +* `ProbabilityTheory.maxLogGrowth_one_le_bipolarRate`: the growth of one observation is at most + the bipolar rate. * `ProbabilityTheory.maxLogGrowth_anti`, `ProbabilityTheory.bipolarRate_anti`: both are antitone in the null. * `ProbabilityTheory.maxLogGrowth_le_mul_klDiv`, `ProbabilityTheory.bipolarRate_le_iInf_klDiv`: @@ -176,6 +179,23 @@ lemma maxLogGrowth_le_mul_bipolarRate (Q₁ : Measure 𝓧) (S₁ : Set (Measure maxLogGrowth Q₁ S₁ n ≤ n * bipolarRate Q₁ S₁ := bipolarRate_le_iff.1 le_rfl n hn +/-- The maximal expected logarithm of an `n`-sample e-variable is at least `n` times that of one +observation: superadditivity, iterated. -/ +theorem mul_maxLogGrowth_one_le (Q₁ : Measure 𝓧) [IsProbabilityMeasure Q₁] + (hS₁ : ∀ P ∈ S₁, IsFiniteMeasure P) (n : ℕ) : + n * maxLogGrowth Q₁ S₁ 1 ≤ maxLogGrowth Q₁ S₁ n := by + cases n with + | zero => simpa using maxLogGrowth_nonneg Q₁ S₁ 0 + | succ q => + simpa [EReal.nsmul_eq_mul] using + EReal.nsmul_le_of_superadditive (maxLogGrowth_add_le Q₁ hS₁) 1 q + +/-- The maximal expected logarithm of a one-observation e-variable is at most the bipolar +rate. -/ +theorem maxLogGrowth_one_le_bipolarRate (Q₁ : Measure 𝓧) (S₁ : Set (Measure 𝓧)) : + maxLogGrowth Q₁ S₁ 1 ≤ bipolarRate Q₁ S₁ := by + simpa using maxLogGrowth_div_le_bipolarRate Q₁ S₁ one_ne_zero + /-- 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 diff --git a/LMLExplore/EValues/BipolarRate/SingleLetter.lean b/LMLExplore/EValues/BipolarRate/SingleLetter.lean index 3638fe58..2f190451 100644 --- a/LMLExplore/EValues/BipolarRate/SingleLetter.lean +++ b/LMLExplore/EValues/BipolarRate/SingleLetter.lean @@ -25,9 +25,6 @@ For a weakly compact convex null the hypothesis holds [RR26, Proposition 4.5]. ## Main statements -* `ProbabilityTheory.mul_maxLogGrowth_one_le`: `n * maxLogGrowth Q₁ S₁ 1 ≤ maxLogGrowth Q₁ S₁ n`. -* `ProbabilityTheory.maxLogGrowth_one_le_bipolarRate`: the growth of one observation is at most - the bipolar rate. * `ProbabilityTheory.bipolarRate_eq_maxLogGrowth_one_of_le`: if the bipolar rate is at most the growth of one observation, the two are equal. * `ProbabilityTheory.maxLogGrowth_eq_mul_of_bipolarRate_le`: if the bipolar rate is at most the @@ -54,23 +51,6 @@ namespace ProbabilityTheory variable {𝓧 : Type*} {m𝓧 : MeasurableSpace 𝓧} {Q₁ : Measure 𝓧} {S₁ : Set (Measure 𝓧)} {n : ℕ} -/-- The maximal expected logarithm of an `n`-sample e-variable is at least `n` times that of one -observation: superadditivity, iterated. -/ -theorem mul_maxLogGrowth_one_le (Q₁ : Measure 𝓧) [IsProbabilityMeasure Q₁] - (hS₁ : ∀ P ∈ S₁, IsFiniteMeasure P) (n : ℕ) : - n * maxLogGrowth Q₁ S₁ 1 ≤ maxLogGrowth Q₁ S₁ n := by - cases n with - | zero => simpa using maxLogGrowth_nonneg Q₁ S₁ 0 - | succ q => - simpa [EReal.nsmul_eq_mul] using - EReal.nsmul_le_of_superadditive (maxLogGrowth_add_le Q₁ hS₁) 1 q - -/-- The maximal expected logarithm of a one-observation e-variable is at most the bipolar -rate. -/ -theorem maxLogGrowth_one_le_bipolarRate (Q₁ : Measure 𝓧) (S₁ : Set (Measure 𝓧)) : - maxLogGrowth Q₁ S₁ 1 ≤ bipolarRate Q₁ S₁ := by - simpa using maxLogGrowth_div_le_bipolarRate Q₁ S₁ one_ne_zero - /-- If the bipolar rate is at most the maximal expected logarithm of a one-observation e-variable, the two are equal. -/ theorem bipolarRate_eq_maxLogGrowth_one_of_le (h : bipolarRate Q₁ S₁ ≤ maxLogGrowth Q₁ S₁ 1) : From f8046a0c008f40d12e194126f951ebfe58774824 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 15:17:13 +0100 Subject: [PATCH 5/6] fix: import BipolarRate.Basic after its move on main Co-Authored-By: Claude Code --- LMLExplore/EValues/BipolarRate/SingleLetter.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/LMLExplore/EValues/BipolarRate/SingleLetter.lean b/LMLExplore/EValues/BipolarRate/SingleLetter.lean index 2f190451..b122c1da 100644 --- a/LMLExplore/EValues/BipolarRate/SingleLetter.lean +++ b/LMLExplore/EValues/BipolarRate/SingleLetter.lean @@ -5,7 +5,7 @@ Authors: LMLExplore contributors -/ module -public import LMLExplore.EValues.BipolarRate +public import LMLExplore.EValues.BipolarRate.Basic /-! # When one observation attains the smallest relative entropy From f7b3921c782a7cf12633abd5fb5f6be172df4af5 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 15:39:11 +0100 Subject: [PATCH 6/6] doc: state the probability-measure null in the SingleLetter module docstring Co-Authored-By: Claude Code --- .../EValues/BipolarRate/SingleLetter.lean | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/LMLExplore/EValues/BipolarRate/SingleLetter.lean b/LMLExplore/EValues/BipolarRate/SingleLetter.lean index b122c1da..3bf2c1d6 100644 --- a/LMLExplore/EValues/BipolarRate/SingleLetter.lean +++ b/LMLExplore/EValues/BipolarRate/SingleLetter.lean @@ -10,15 +10,15 @@ public import LMLExplore.EValues.BipolarRate.Basic /-! # When one observation attains the smallest relative entropy -For a probability measure `Q₁` and a null `S₁` on a measurable space, the maximal expected -logarithm `maxLogGrowth Q₁ S₁ n` of an `n`-sample e-variable is at least `n` times that of one -observation, by superadditivity, and at most `n` times the smallest relative entropy from `Q₁` to -the null. If one observation already attains the smallest relative entropy, that is, if -`⨅ P ∈ S₁, klDiv Q₁ P ≤ maxLogGrowth Q₁ S₁ 1`, the three quantities agree: for every `n ≠ 0`, -`n` observations are worth exactly `n` times one, and the bipolar rate is the smallest relative -entropy [EVR26, Note 11, Theorem 9]. No semicontinuity, convexity or compactness of the null is -assumed. The weaker hypothesis `bipolarRate Q₁ S₁ ≤ maxLogGrowth Q₁ S₁ 1` already gives -`bipolarRate Q₁ S₁ = maxLogGrowth Q₁ S₁ 1` and, for a null of finite measures, +For a probability measure `Q₁` and a null `S₁` of probability measures on a measurable space, +the maximal expected logarithm `maxLogGrowth Q₁ S₁ n` of an `n`-sample e-variable is at least `n` +times that of one observation, by superadditivity, and at most `n` times the smallest relative +entropy from `Q₁` to the null. If one observation already attains the smallest relative entropy, +that is, if `⨅ P ∈ S₁, klDiv Q₁ P ≤ maxLogGrowth Q₁ S₁ 1`, the three quantities agree: for every +`n ≠ 0`, `n` observations are worth exactly `n` times one, and the bipolar rate is the smallest +relative entropy [EVR26, Note 11, Theorem 9]. No semicontinuity, convexity or compactness of the +null is assumed. The weaker hypothesis `bipolarRate Q₁ S₁ ≤ maxLogGrowth Q₁ S₁ 1` already gives +`bipolarRate Q₁ S₁ = maxLogGrowth Q₁ S₁ 1` for any null and, for a null of finite measures, `maxLogGrowth Q₁ S₁ n = n * maxLogGrowth Q₁ S₁ 1` for `n ≠ 0`. For a weakly compact convex null the hypothesis holds [RR26, Proposition 4.5].