[RemyDegenne]

This pull request proves that no e-process for an i.i.d. null grows faster than the bipolar rate in expectation [RR26, Lemma 3.3]. It adds one new file, LMLExplore/EValues/BipolarRate/EProcess.lean, moves LMLExplore/EValues/BipolarRate.lean to LMLExplore/EValues/BipolarRate/Basic.lean next to it, and adds the general initial-segment API (initSeg and its lemmas, which do not depend on e-values) to the existing LMLExplore/MeasureTheory/MeasurableSpace/Constructions.lean and LMLExplore/Probability/ProductMeasure.lean.

Setting

The observations are the coordinates of ℕ → 𝓧. The null is the set of i.i.d. laws Measure.infinitePi fun _ ↦ P, P ∈ S₁, with S₁ a set of probability measures, and the alternative is the i.i.d. law of a probability measure Q₁. E-processes are taken in Mathlib's Filtration.piLE, whose σ-algebra at time n is generated by the observations 0, …, n. So the value of an e-process at time n is a function of n + 1 observations, and the statements are indexed accordingly.

Main declarations

• In LMLExplore/MeasureTheory/MeasurableSpace/Constructions.lean, namespace MeasureTheory: initSeg n, with initSeg_apply, measurable_initSeg, dependsOn_initSeg, dependsOn_comp_initSeg and exists_measurable_eq_comp_initSeg: the first n observations of a sequence as a function on Fin n; it and any function of it depend only on the first n coordinates; conversely a measurable function that depends on the first n coordinates factors through it. In LMLExplore/Probability/ProductMeasure.lean: measurePreserving_initSeg, under an i.i.d. law it has the product law. The inline re-derivations of this fact in Measure.infinitePi_fin_mem_and_forall_add_mem and in hasLaw_arm_fin_streamMeasure (LMLExplore/SequentialLearning/SumRewards.lean) now use it.
• exists_isEVar_eq_comp_initSeg: a function of the first n observations with expectation at most one under the i.i.d. laws of the null is an n-sample e-variable composed with initSeg n.
• eintegral_log_le_maxLogGrowth_of_dependsOn: such a function has expected logarithm at most maxLogGrowth Q₁ S₁ n under the i.i.d. law of Q₁.
• IsEProcess.eintegral_log_le_maxLogGrowth: for an e-process E, ∫ᵉ log (E n) ≤ maxLogGrowth Q₁ S₁ (n + 1).
• IsEProcess.eintegral_log_le_mul_bipolarRate: ∫ᵉ log (E n) ≤ (n + 1) * bipolarRate Q₁ S₁.
• IsEProcess.eintegral_log_div_le_bipolarRate and IsEProcess.limsup_eintegral_log_div_le_bipolarRate: the expected logarithm per observation seen is at most the bipolar rate at every time, and so is its limsup [RR26, Lemma 3.3].

Roadmap coverage (EValues, Layer 6, item 1)

Covered: in the second bullet, "every e-process W has limsup (1/n) ∫ᵉ log (W n) ∂Q ≤ d per observation, since W n is an e-variable of the observations it has seen". The bound is proved at every time, not only in the limit.

Left for later pull requests:

• blockwise e-processes and the same bound for them [RR26, Definitions 2.3–2.5];
• products over blocks of numeraires attaining every rate below d [RR26, Theorem 3.5];
• d = KL_inf under lower semicontinuity, the strictness example, the sequential null and the almost sure bound;
• items 2 and 3 of Layer 6. The lower bound on expected stopping times of item 3 will use initSeg (from ProductMeasure.lean) and eintegral_log_le_maxLogGrowth_of_dependsOn.

This pull request shares no content with the open #399 and #402.

Removed or renamed

• Module LMLExplore.EValues.BipolarRate is renamed to LMLExplore.EValues.BipolarRate.Basic (no declaration renamed). Downstream imports of LMLExplore.EValues.BipolarRate should import LMLExplore.EValues.BipolarRate.Basic instead.

Notes for reviewers

• The division is by n + 1, the number of observations that Filtration.piLE n knows, not by the time n. With this normalization the bound holds at every time and the limsup statement is a one-line consequence.
• exists_measurable_eq_comp_initSeg extends a finite sequence by a constant, which needs Nonempty 𝓧; the theorems get it from the probability measure Q₁. Mathlib's factorization lemmas through Filtration.piLE go to Finset.Iic n → 𝓧, while maxLogGrowth is indexed by Fin n.
• The hypotheses ask for probability measures in the null because the null consists of i.i.d. laws on ℕ → 𝓧 (Measure.infinitePi).

Roadmap: EValues
Paper: RemyDegenne/evalues_research
Item: R34

🤖 Generated with Claude Code

https://claude.ai/code/session_0196ftMVbgjSJzPQEwdek3kM

[RemyDegenne]

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

Proofs are short and mostly robust, but one calc step closes by a bare rfl that unfolds the bundled logUtility to ENNReal.log, which is an undocumented definitional equality across a wrapper.

• LMLExplore/EValues/BipolarRate/EProcess.lean:134 — After rw [... eintegral_map ...], the goal ∫ᵉ ω, ENNReal.log ((G ∘ initSeg n) ω) = ∫ᵉ ω, (logUtility ∘ G) (initSeg n ω) is closed by rfl, which only works by unfolding the bundled logUtility (it has a .measurable field) into ENNReal.log. This undocumented defeq will break if logUtility's representation changes. Fix: Replace rfl with a rewrite by the coercion/apply lemma for logUtility (e.g. simp [Function.comp_def, logUtility_apply]), adding that lemma upstream if it is missing; or state the calc's middle term with ENNReal.log ∘ G and convert once through the named lemma.

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 · 41s · 130.2k in (120.1k cache read, 10k cache write) / 2.6k 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	The statements faithfully formalize RR26 Lemma 3.3: piLE n knows n+1 observations, the null transfers correctly to Measure.pi images matching maxLogGrowth, and the limsup bound follows soundly from the bound at every time. No vacuity, placeholders or over-strong assumptions found.
✅	reuse	approved	claude/claude-opus-5-5	Both inline re-derivations of the product law of the first n coordinates now use measurePreserving_initSeg, so last round's findings are resolved. The new initSeg API and the e-process bounds add material not found in Mathlib (whose frestrictLe maps to Finset.Iic and whose Measurable.exists_eq_measurable_comp needs a standard Borel target) and build on the existing maxLogGrowth_le_mul_bipolarRate, IsEVar.eintegral_le_maxUtility and Measurable.dependsOn_of_piLE.
✅	scope	approved	claude/claude-opus-5-5	The PR proves the e-process limsup bound of EValues Layer 6 item 1 [RR26, Lemma 3.3] (README:884-887), with the initSeg API as a direct prerequisite and a file move that places the new file. The edits in ProductMeasure, SumRewards and StaticAllocation replace in-place copies of the same fact, so the PR is one coherent unit.
✅	attribution	approved	claude/claude-opus-5-5	The central informal source [RR26, Lemma 3.3] is cited in the module docstring, in the theorem docstrings and in a full References entry in EProcess.lean; the initSeg helper API is routine and follows no particular source.
✅	api-design	approved	claude/claude-opus-5-5	initSeg is a hidden-body definition placed in a general home, with complete characteristic API (initSeg_def by (rfl), @[simp] initSeg_apply, @[fun_prop] measurable_initSeg, dependence and factorization lemmas) and no Mathlib duplicate. The module rename leaves no shim, and the inline re-derivations in-repo now use the new API.
✅	generality	approved	claude/claude-opus-5-5	The statements are at the right level: initSeg and its factorization lemma are generic and reused by existing proofs, every hypothesis is used, and the bipolar-rate bounds are proved once and then specialized (maxLogGrowth → n+1 times the rate → per observation → limsup) without duplicated proofs.
✅	placement	approved	claude/claude-opus-5-5	The generic initial-segment API is in Constructions.lean and ProductMeasure.lean, the e-value results are in the new BipolarRate/EProcess.lean, and the BipolarRate/Basic.lean rename updates every in-repo import and leaves no old path behind. Every import in the diff is used.
✅	naming	approved	claude/claude-opus-5-5	Names describe their conclusions in the library's existing terms (eintegral_log_le_maxLogGrowth, measurePreserving_initSeg, exists_measurable_eq_comp_initSeg, IsEProcess.*), no name claims more than its statement proves, and no notation is added. MeasureTheory.initSeg does not clash with Mathlib's Finset.initSeg (Colex) and duplicates no Mathlib name.
✅	documentation	approved	claude/claude-opus-5-5	The new module and every new public declaration are documented accurately, with no docstring promising more than its statement; the updated module docstrings in Constructions.lean and ProductMeasure.lean list the new initSeg API, and no reference to the renamed module path remains.
✅	proof-quality	approved	claude/claude-opus-5-5	Proofs are short, use explicit unfolding lemmas (initSeg_def, initSeg_apply) instead of hidden defeq, and the inline re-derivations in ProductMeasure.lean and SumRewards.lean are now handled by the reusable measurePreserving_initSeg. The only rfl that depends on defeq (ProductMeasure.lean:77) is pre-existing and carries a comment explaining it.

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

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