[RemyDegenne]

This pull request adds the quantity a n of EValues Layer 6 and its rate d, with the parts of item 6.1 that need no e-processes.

a n is the maximal expected logarithm, under Q₁ ^ n, of an e-variable for the n-fold products of the members of the null S₁. Its name, maxLogGrowth, is the one Suggested.lean uses. The rate d is named bipolarRate, the term Ram and Ramdas use [RR26, Section 4]. It is defined as the supremum of a n / n over n ≥ 1, and the pull request proves that a n / n converges to it.

No dependency has Fekete's lemma for values in EReal or ℝ≥0∞: Mathlib's Subadditive.tendsto_lim takes real sequences with u n / n bounded below. The pull request therefore adds EReal.tendsto_div_iSup_of_superadditive in LMLExplore/Analysis/Subadditive.lean, the directory of Mathlib's version. It holds for every superadditive sequence of extended reals that takes the value ⊥ at no n ≠ 0, with no bound, and the limit may be ⊤.

Main declarations

LMLExplore/EValues/BipolarRate.lean, namespace ProbabilityTheory:

• maxLogGrowth Q₁ S₁ n: maxUtility (Measure.pi fun _ : Fin n ↦ Q₁) ((fun P ↦ Measure.pi fun _ ↦ P) '' S₁) logUtility.
• bipolarRate Q₁ S₁: ⨆ n, maxLogGrowth Q₁ S₁ (n + 1) / (n + 1).
• maxLogGrowth_add_le: superadditivity [RR26, Lemma 3.2]. The proof splits Fin (m + n) into Fin m ⊕ Fin n and applies Statlib's maxUtility_prod_eq_add (which rests on IsEVar.prod), maxUtility_map_le and maxUtility_anti.
• tendsto_maxLogGrowth_div_bipolarRate: a n / n → d [RR26, Lemma 3.2].
• maxLogGrowth_le_mul_bipolarRate: a n ≤ n * d for n ≠ 0.
• maxLogGrowth_nonneg, bipolarRate_nonneg.
• maxLogGrowth_anti, bipolarRate_anti (@[gcongr]): both are antitone in the null.
• maxLogGrowth_one: a 1 = maxUtility Q₁ S₁ logUtility, on any measurable space, including an empty one.
• maxLogGrowth_le_mul_klDiv, bipolarRate_le_klDiv: a n ≤ n * klDiv Q₁ P and d ≤ klDiv Q₁ P for each P ∈ S₁. These need no hypothesis on the other members of the null.
• bipolarRate_le_iInf_klDiv: d ≤ ⨅ P ∈ S₁, klDiv Q₁ P, with KL_inf valued in ℝ≥0∞ as the roadmap specifies [RR26, proof of Theorem 4.1].

LMLExplore/Analysis/Subadditive.lean:

• EReal.tendsto_div_iSup_of_superadditive: Fekete's lemma for superadditive sequences of extended reals.

Hypotheses

• Q₁ is a probability measure.
• For superadditivity and the limit, the members of S₁ are finite measures (IsFiniteMeasure, as in Statlib's maxUtility_prod_eq_add). They do not need to be probability measures.
• The comparison with KL_inf takes probability measures.
• There is no domination, convexity or compactness assumption anywhere.

Roadmap item 6.1: covered

• Superadditivity of a, from Statlib's IsEVar.prod [RR26, Lemma 3.2], so that a n / n converges to its supremum d.
• d ≤ KL_inf(Q₁, S₁).

Roadmap item 6.1: left for later pull requests

• Blockwise e-processes [RR26, Definitions 2.3–2.5].
• The bound limsup (1/n) ∫ᵉ log W n ≤ d for every e-process and every blockwise e-process [RR26, Lemma 3.3].
• That products of numeraires over blocks attain every rate below d [RR26, Theorem 3.5].
• d = KL_inf under weak lower semicontinuity, the almost sure growth of block test supermartingales, Propositions 4.5, 5.4 and 7.1.
• The sequential null of Layer 4.5.
• The almost sure bound for every e-process [WSJ26, Proposition 2.2].

Checks run locally

• lake build LMLExplore.Analysis.Subadditive, lake build LMLExplore.EValues.BipolarRate, and then the full lake build: no warnings.
• Mathlib's default environment linters (#lint in LMLExplore) on the new modules, docBlame included: no findings.
• lake exe axioms: duplicate and axiom audit, no duplicates, only the three standard axioms.
• lake exe module-system.
• Through tauceti-tools script: check_source_options.py, check-imports.py, lint-dot-notation.py and lint-style.sh (headers and text linters).

Nothing is removed or renamed.

Roadmap: EValues
Paper: RemyDegenne/evalues_research
Item: R7

🤖 Generated with Claude Code

https://claude.ai/code/session_0196ftMVbgjSJzPQEwdek3kM

[RemyDegenne]

🟡 api-design — request_changes claude/claude-opus-5-5

The characteristic API of maxLogGrowth/bipolarRate is complete with hidden bodies and (rfl) def lemmas, but a general maxUtility lemma is in the wrong file, general superadditivity steps are hidden as private, and one name does not follow the naming convention.

• LMLExplore/EValues/BipolarRate.lean:90 — maxUtility_zero_measure is a general fact about Statlib's maxUtility (any Ω, T, U) with no dependence on i.i.d. nulls or the bipolar rate, placed in the bipolar-rate file. Fix: Move it to a general maxUtility companion module under LMLExplore/EValues/ that BipolarRate.lean imports, keeping it public and @[simp].
• LMLExplore/Analysis/Subadditive.lean:59 — eq_top_of_superadditive is general infrastructure for superadditive ℕ → EReal sequences, but it is private. The same applies to the iterate (q + 1) • u m ≤ u ((q + 1) * m), now a local have h_mul inside the private nsmul_add_nsmul_le_of_superadditive (line 41). Fix: Make EReal.eq_top_of_superadditive public. Extract h_mul as a public EReal.nsmul_le_of_superadditive (and expose nsmul_add_nsmul_le_of_superadditive if it stays separate). Keep only Real.fekete_bound private.
• LMLExplore/EValues/BipolarRate.lean:105 — div_le_bipolarRate drops the subject of its statement maxLogGrowth Q₁ S₁ n / n ≤ bipolarRate Q₁ S₁, so it reads like a generic division lemma. Fix: Rename it to maxLogGrowth_div_le_bipolarRate and update its uses in bipolarRate_le_iff and bipolarRate_nonneg.

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

_{claude/claude-opus-5-5 · 40s · 119.7k in (87.3k cache read, 32.4k cache write) / 3.7k out tokens · reviewing this diff · rubric · ⚠️ rubrics checkout differs from published main}

[RemyDegenne]

🟡 proof-quality — request_changes claude/claude-opus-5-5

The proofs work, but the Fekete proof is about 60 lines with reusable facts buried inside it, and several steps move coercions by hand with brittle rewrite chains.

• LMLExplore/Analysis/Subadditive.lean:67 — h_top (a ⊤ value at j ≠ 0 carries forward to every n ≥ j) and the closing real inequality n r / m - C ≤ (q + 1) r + s a (lines 112–121) are separate facts buried in a 60-line proof. Fix: Make h_top a private lemma (eq_top_of_superadditive). Make the arithmetic bound a private real lemma stated in terms of q, s, m, r, a. The main proof then keeps only the filter argument.
• LMLExplore/Analysis/Subadditive.lean:110 — Coercions are moved by hand: rw [hn_eq, hr, ha, ← EReal.coe_nsmul, ← EReal.coe_nsmul, ← EReal.coe_add] at key. Lines 92 and 104 do the same with rw [hr, ← EReal.coe_natCast, ← EReal.coe_div, EReal.coe_lt_coe_iff] and rw [le_div_iff_mul_le …, ← EReal.coe_natCast, ← EReal.coe_mul]. These chains break when Mathlib renames lemmas. Fix: After substituting hr/ha, use norm_cast/push_cast (or exact_mod_cast) to move between EReal and ℝ.
• LMLExplore/EValues/BipolarRate.lean:94 — maxLogGrowth_one defines h0 : maxUtility 0 T logUtility = 0 as a local have. That is a general fact about maxUtility, not something specific to this proof. Fix: Extract it as a standalone @[simp] lemma maxUtility_zero_measure and use it in the empty-space branch.
• LMLExplore/EValues/BipolarRate.lean:186 — maxLogGrowth_le_mul_klDiv closes its goal with a five-step rewrite chain rw [maxUtility_singleton_eq_klDiv, klDiv_pi_const, Fintype.card_fin, EReal.coe_ennreal_mul, ENNReal.toEReal_natCast], which is brittle. Fix: Use rw [maxUtility_singleton_eq_klDiv, klDiv_pi_const] followed by simp/push_cast. Fintype.card_fin and the ENNReal→EReal cast lemmas are simp/norm_cast lemmas.

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

_{claude/claude-opus-5-5 · 25s · 47.3k in (41.8k cache read, 5.4k cache write) / 2.5k out tokens · reviewing this diff · rubric · ⚠️ rubrics checkout differs from published main}

[RemyDegenne]

AI review — approved

Each rubric is judged independently by multiple review agents; the PR merges only once every rubric is green — any rubric that is not green (changes requested, blocked, errored, stale, or not yet run) blocks the merge. See the rubrics.

⚠️ This review ran from a rubrics checkout that differs from the published rubrics (out of date, pinned, or locally edited), so its findings may reflect different rules.

	rubric	state	judge	summary
✅	correctness	approved	claude/claude-opus-5-5	maxLogGrowth matches the roadmap's Suggested.lean definition, bipolarRate is RR26's rate d, and the superadditivity, Fekete limit and KL_inf bound state the intended results with assumptions that are no stronger than the roadmap's.
✅	reuse	approved	claude/claude-opus-5-5	The extended-real Fekete lemma, the iterated-superadditivity helpers and the bipolar-rate API have no counterpart in Mathlib or LMLExplore (Mathlib's Subadditive.tendsto_lim covers only bounded-below real sequences), and the proofs build on existing Mathlib and Statlib pieces (measure-preserving equivalences, maxUtility_prod_eq_add, maxUtility_map_le, maxUtility_singleton_eq_klDiv). Statlib's source was not available, so I could not check whether maxUtility_zero_measure already exists there.
✅	scope	approved	claude/claude-opus-5-5	New material directly advances EValues roadmap item 6.1 (superadditivity of a, convergence of a n / n to d, and d ≤ KL_inf), with Fekete's lemma for EReal and one maxUtility helper as proximate prerequisites; the PR is a single coherent topic.
✅	attribution	approved	claude/claude-opus-5-5	The central informal source [RR26] (Ram and Ramdas, arXiv:2604.25280v1, matching the roadmap's bibliography) is cited at Lemma 3.2, Theorem 4.1 and Proposition 5.4. The EReal Fekete lemma names Fekete and Mathlib's Subadditive.tendsto_lim, and its standard proof needs no further credit.
✅	api-design	approved	claude/claude-opus-5-5	The definitions hide their bodies behind (rfl) *_def lemmas, bipolarRate is characterized by its upper-bound iff and lower bound, and the gcongr/simp annotations are appropriate. The general Fekete and maxUtility results are public in reasonable homes, and there is no compatibility surface.
✅	generality	approved	claude/claude-opus-5-5	Statements sit at the natural level: the EReal Fekete lemma is stated for general superadditive sequences without boundedness, monotonicity/nonnegativity lemmas carry no hypotheses, and superadditivity only assumes finite null members; KL comparisons are derived from one general per-member lemma rather than duplicated.
✅	placement	approved	claude/claude-opus-5-5	Fekete's lemma for EReal sits in LMLExplore/Analysis/Subadditive.lean, matching Mathlib's Mathlib.Analysis.Subadditive, the maxUtility companion lemma sits at the path mirroring Statlib's EValues/DPI, and the Layer 6 material joins the existing EValues/ directory. No import is evidently unused or overly broad.
✅	naming	approved	claude/claude-opus-5-5	New names describe their conclusions in standard Mathlib terminology, match the roadmap's maxLogGrowth/maxLogGrowth_add_le stand-ins, and no notation is introduced.
✅	documentation	approved	claude/claude-opus-5-5	Module docstrings and declaration docstrings are present, accurate to the statements (hypotheses, possible ⊤ limit, n ≠ 0 conditions), and free of roadmap/process narrative.
✅	proof-quality	approved	claude/claude-opus-5-5	The proofs are short and use explicit _def lemmas, with no undocumented change or show manipulation; the roughly 45-line Fekete proof has comments explaining its case split. Iterated superadditivity and the real bound are factored out as lemmas, and the remaining one-off steps are reasonably robust.

♻️ = approved on an earlier commit, re-run before merge.

_{Reviewing this diff at head f52778c. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $1.30.}