[RemyDegenne]

This PR adds the Bernoulli maximal inequality [DLB17, Lemma F.4], [EV26, Lemma 20]. If X i is ℱ (i + 1)-measurable with values in [0, 1] almost surely and P i is a version of E[X i | ℱ i], then for every δ > 0, ℙ(∃ n, ∑_{i < n} X i < (1/2) ∑_{i < n} P i - log (1 / δ)) ≤ δ (LMLExplore.measure_exists_sum_lt_half_mul_sum_sub_le). This is the "counts versus pseudo-counts" tool n ≥ n̄/2 - log(3SAH/δ) that ReinforcementLearning Layer 19.2 (RF-Express [MDJKLV21, Theorem 1]) lists among the tools to prove. Its instance at the visits of a step–state–action pair, at confidence δ/(3SAH), gives the counts event of that analysis. The other Layer 19.2 tools are either in flight (KL-to-Bernstein transport and variance transfers #291, the self-bounding inequality #287) or still to port (the logarithmic sum bound). After this PR, the milestone still needs the logarithmic sum bound, the threshold β from Layer 3.4, and the RF-Express algorithm with its PAC and sample-complexity theorem on statesEnv (Layer 7.7).

The new file LMLExplore/Probability/Martingale/BernoulliMaximal.lean (160 lines) adds:

• LMLExplore.condExp_exp_condExp_div_two_sub_le_one: the one-step bound E[exp (E[X | m] / 2 - X) | m] ≤ 1 for X measurable with values in [0, 1] a.s. It is proved from the chord exp (-x) ≤ 1 - (1 - e⁻¹) x on [0, 1] (Mathlib's convexOn_exp), the pull-out property, and 1 - e⁻¹ ≥ 1/2 (Mathlib's Real.exp_neg_one_lt_half).
• LMLExplore.measure_exists_sum_lt_half_mul_sum_sub_le: the time-uniform inequality. It goes through LMLExplore's LMLExplore.supermartingale_exp_sum_of_condExp_exp_le_one and Ville's inequality MeasureTheory.Supermartingale.measure_exists_le_le.

LMLExplore's fixed-η Freedman inequality LMLExplore.measure_exists_mul_sum_condExp_sq_add_log_div_le_sum_le, applied to P i - X i with η = 1/2, gives only - 2 log (1 / δ). The sharper constant needs the dedicated one-step bound above.

This PR ports Essakine2026Tight/ForLMLExplore/Probability/Martingale/Ville.lean from RemyDegenne/Essakine2026Tight at commit 9c77165d56f81c1db7a9835068356bb14886a3be (Apache 2.0, author Rémy Degenne). It generalizes and re-proves that material as follows:

• The source assumes X i ∈ {0, 1} everywhere, together with P i ∈ [0, 1] and ℱ i-strong measurability of P i. Here X i ∈ [0, 1] holds only almost surely, and P i is any version of the conditional mean. Its range and measurability are then derived rather than assumed, and the convexity chord replaces the {0, 1} identity.
• The declarations are in the LMLExplore namespace, next to Freedman's inequality, rather than in MeasureTheory.
• The one-step lemma is renamed from condExp_exp_sub_le_one to condExp_exp_condExp_div_two_sub_le_one, to name its conclusion.

No declaration is removed or renamed on main.

Roadmap: ReinforcementLearning

Paper: RemyDegenne/Essakine2026Tight
Item: R12

🤖 Prepared with Claude Code

[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	Both new statements faithfully formalize the one-step bound E[exp(E[X|m]/2 − X)|m] ≤ 1 and the time-uniform Bernoulli maximal inequality [DLB17, Lemma F.4] with W = log(1/δ); the hypotheses are weaker than the source's and no vacuity, mis-indexing, or content moved into hypotheses was found.
✅	reuse	approved	claude/claude-opus-5-5	The one-step bound and the time-uniform Bernoulli maximal inequality are new; the PR now uses the existing chord lemma, Mathlib's integrability lemmas, the supermartingale lemma and Ville's inequality.
✅	scope	approved	claude/claude-opus-5-5	The Bernoulli maximal inequality is the 'counts versus pseudo-counts' tool listed explicitly under ReinforcementLearning Layer 19, item 2 (RF-Express), so it directly advances a named roadmap target. The PR is one new file with the one-step bound and the time-uniform inequality, with no unrelated material bundled.
✅	attribution	approved	claude/claude-opus-5-5	The file now credits its ported formal source (RemyDegenne/Essakine2026Tight, ForLMLExplore/Probability/Martingale/Ville.lean, by Rémy Degenne, Apache 2.0) in the module docstring and author line, along with the informal sources [DLB17, Lemma F.4] and [EV26, Lemma 20]; the prior finding is resolved.
✅	api-design	approved	claude/claude-opus-5-5	The public surface is the roadmap-targeted Bernoulli maximal inequality plus its one-step bound; the only private helper is an integrability step specific to this proof, and the chord bound is reused from KLChernoff rather than duplicated. No definitions, so no characteristic API or annotations are needed, and there are no compatibility artifacts.
✅	generality	approved	claude/claude-opus-5-5	Both statements sit at the natural level: hypotheses follow the library's Freedman and supermartingale conventions, the [0, 1] range and conditional-mean version are needed only almost surely, and δ > 0 is the only condition on δ. The supermartingale step reuses supermartingale_exp_sum_of_condExp_exp_le_one, and the dedicated one-step bound is justified because Freedman gives only the weaker 2·log(1/δ) constant.
✅	placement	approved	claude/claude-opus-5-5	The new file sits in Probability/Martingale/ next to the supermartingale constructor (Basic.lean) and Ville's inequality (Ville.lean) it uses, and both declarations are general rather than roadmap-specific. Every import supplies a lemma the proofs use (exp_mul_le_one_sub_add_mul_exp from KLChernoff, condExp_mul_of_stronglyMeasurable_left from PullOut, exp_neg_one_lt_half from ExponentialBounds), and there is no broad import Mathlib.
✅	naming	approved	claude/claude-opus-5-5	condExp_exp_condExp_div_two_sub_le_one and measure_exists_sum_lt_half_mul_sum_sub_le describe their conclusions and match the patterns of adjacent declarations (condExp_exp_mul_sub_mul_condExp_sq_le_one, measure_exists_le_mul_sum_sub_mul_sum_condExp_sq_le in Freedman.lean, measure_exists_card_mul_add_le_sum_le in ExponentialTail.lean). The PR adds no notation, and all material sits in the LMLExplore namespace with no dot-notation candidates.
✅	documentation	approved	claude/claude-opus-5-5	Module and declaration docstrings accurately describe the statements and their use, with no roadmap or process narrative; the claim that fixed-η Freedman gives 2 log(1/δ) checks out against Freedman.lean:264 with η = 1/2.
✅	proof-quality	approved	claude/claude-opus-5-5	Prior findings are resolved: the chord step reuses exp_mul_le_one_sub_add_mul_exp, the duplicated |X| ≤ 1 derivation is gone via Integrable.of_mem_Icc, and the Pi defeq is replaced by simpa. The remaining proofs are commented, under 50 lines each, and free of undocumented change/show or brittle rewrite chains.

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

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

[prevostad]

🟡 reuse — request_changes claude/claude-opus-5-5

The two main results are new and reuse existing building blocks (the KLChernoff chord lemma, the exponential-supermartingale criterion, Ville's inequality), but a private integrability helper re-derives Mathlib's integrable_exp_mul_of_le.

• LMLExplore/Probability/Martingale/BernoulliMaximal.lean:68 — The private integrable_exp_condExp_div_two_sub rebuilds integrability by hand (.of_bound plus ae_bdd_abs_condExp_of_ae_bdd_abs plus the exp (1/2) bound), but Mathlib's ProbabilityTheory.integrable_exp_mul_of_le already gives it with t = 1, b = 1/2. Fix: Remove the helper. At both uses, write by simpa using integrable_exp_mul_of_le 1 (1 / 2) zero_le_one (((stronglyMeasurable_condExp.mono hm).measurable.div_const 2).sub hX).aemeasurable (by filter_upwards [hX01, condExp_le-bound] ...), discharging C/2 - X ≤ 1/2 from μ[X|m] ≤ 1 (e.g. via condExp_mono against the constant 1, or the existing ae_bdd_abs_condExp_of_ae_bdd_abs). This is the same pattern as Freedman.lean:119.

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 · 42s · 323.3k in (279.4k cache read, 43.9k cache write) / 4.2k out tokens · reviewing this diff · rubric}

[RemyDegenne]

Addressed in e973ab3: integrable_exp_condExp_div_two_sub no longer rebuilds integrability by hand (.of_bound + the exp (1/2) norm bound are gone). It is now one call to Mathlib's ProbabilityTheory.integrable_exp_mul_of_le 1 (1 / 2) zero_le_one …, with only the C / 2 - X ≤ 1 / 2 bound discharged, exactly the pattern of Freedman.lean:119. I kept the private helper and did not inline it at its two uses (the pull-out in condExp_exp_condExp_div_two_sub_le_one and the supermartingale step in measure_exists_sum_lt_half_mul_sum_sub_le). Inlining would copy the measurability term and the bound proof twice, and the previous proof-quality round flagged exactly that kind of duplication. Freedman.lean also keeps its own private wrapper around integrable_exp_mul_of_le for the same reason.

[prevostad]

🟡 attribution — request_changes claude/claude-opus-5-5

The docstring credits DLB17, EV26 and Rémy Degenne's Essakine2026Tight source file, but the file's copyright and Authors header leaves out the source author. Every other file in the repo ported from Degenne's work names him there.

• LMLExplore/Probability/Martingale/BernoulliMaximal.lean:2 — Lines 2 and 4 give the copyright and authorship to 'LMLExplore contributors', but the file is adapted from Rémy Degenne's Apache 2.0 Essakine2026Tight/.../Ville.lean. This is the only file in the repo with that header. Fix: Change line 2 to Copyright (c) 2026 Rémy Degenne. All rights reserved. and line 4 to Authors: Rémy Degenne, as in the sibling ports Ville.lean, Freedman.lean and Basic.lean.

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 · 19s · 86.1k in (75.6k cache read, 10.5k cache write) / 1.7k out tokens · reviewing this diff · rubric}

[prevostad]

AI review — changes requested

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.

	rubric	state	judge	summary
♻️	correctness	stale (re-run pending) (approved in @RemyDegenne's review of 1263b27)	—
🟡	reuse	changes requested	claude/claude-opus-5-5	The two main results are new and reuse existing building blocks (the KLChernoff chord lemma, the exponential-supermartingale criterion, Ville's inequality), but a private integrability helper re-derives Mathlib's integrable_exp_mul_of_le.
♻️	scope	stale (re-run pending) (approved in @RemyDegenne's review of 1263b27)	—
🟡	attribution	changes requested	claude/claude-opus-5-5	The docstring credits DLB17, EV26 and Rémy Degenne's Essakine2026Tight source file, but the file's copyright and Authors header leaves out the source author. Every other file in the repo ported from Degenne's work names him there.
♻️	api-design	stale (re-run pending) (approved in @RemyDegenne's review of 1263b27)	—
♻️	generality	stale (re-run pending) (approved in @RemyDegenne's review of 1263b27)	—
♻️	placement	stale (re-run pending) (approved in @RemyDegenne's review of 1263b27)	—
♻️	naming	stale (re-run pending) (approved in @RemyDegenne's review of 1263b27)	—
♻️	documentation	stale (re-run pending) (approved in @RemyDegenne's review of 1263b27)	—
✅	proof-quality	approved	claude/claude-opus-5-5	All three prior proof-quality findings are resolved in 187630d: the chord now uses the existing exp_mul_le_one_sub_add_mul_exp, the duplicated |X| ≤ 1 derivation is replaced by Mathlib's Integrable.of_mem_Icc, and hC no longer relies on implicit Pi defeq. The remaining proofs are short, commented, and use no change/show or brittle rewrite chains.

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

_{Reviewing this diff at head 187630d. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $0.57.}