[RemyDegenne]

This PR adds the self-bounding inequality of Ménard et al. [MDJKLV21, Lemma 13], the inversion of the implicit inequality on the stopping time τ: if τ ≤ C √(τ (A L + B L²)) + D (A L + E L²) with L = log (α τ), α ≥ e, A, B, C, D ≥ 0 and B ≤ E, then τ ≤ C² (A + B) C₁² + (D + 2 √D C) (A + E) C₁² + 1 with C₁ = (8/5) log (11 α² (A + E) (C + √D)²) (Real.le_of_le_sqrt_mul_add), or with (C + D)² in place of (C + √D)² when D ≥ 1 (Real.le_of_le_sqrt_mul_add').

Roadmap: ReinforcementLearning

The target is ReinforcementLearning Layer 19.2 (RF-Express [MDJKLV21, Theorem 1]), the tool "the inversion of the implicit inequality on τ [MDJKLV21, Lemma 13]". The sample-complexity bound of that milestone, τ ≤ (H³SA/ε²)(log(3SAH/δ) + S) C₁ + 1, is obtained by applying this lemma to the inequality on τ that the counting argument produces. After this PR, Layer 19.2 still needs its other tools (counts versus pseudo-counts, the KL-to-Bernstein transport, the variance transfers [MDJKLV21, Lemmas 10–12] and ∑_t u_{t+1}/max(1, U_t) ≤ 4 log(U_{T+1} + 1) [MDJKLV21, Lemma 9]), then the algorithm and its PAC and sample-complexity theorem.

The constant printed in [MDJKLV21, Lemma 13] and [EV26, Lemma 29], C₁ = (8/5) log (11 α² (A + E) (C + D)), is too small. A counterexample, recorded in the module docstring and checked numerically: α = e, B = E = 1, C = 1000, A = D = 10⁻⁶, τ = 4·10⁸ satisfy the hypothesis, while the printed bound gives about 3.27·10⁸. Squaring the factor C + D fixes it. The paper's assumptions A, B, C, D > 0 and B ≥ 1 are dropped, and so is τ ≥ 0.

New declarations:

• LMLExplore/Analysis/SpecialFunctions/Log/SelfBounding.lean (new file): Real.le_mul_sq_of_le_sqrt_mul_add (the quadratic part, for any L ≥ 1 and not only log (α τ): τ ≤ K L² with K = C² (A + B) + (D + 2 √D C) (A + E)), Real.log_le_of_le_sqrt_mul_add (log (α τ) ≤ (8/5) log (4 α K) for τ ≥ 1), Real.le_mul_sq_log_add_one_of_le_sqrt_mul_add (τ ≤ K ((8/5) log M)² + 1 for every M ≥ 4 α K), Real.le_of_le_sqrt_mul_add and Real.le_of_le_sqrt_mul_add'. The bound 4 α K ≤ 11 α² (A + E) (C + √D)² is a private helper of these last two, and 1 ≤ log (α τ) for α ≥ e, τ ≥ 1 is a private helper of the second and third.
• LMLExplore/Analysis/Real/Sqrt.lean: Real.le_add_sqrt_of_sq_le, the root of a quadratic inequality (x² ≤ b x + c with b, c ≥ 0 gives x ≤ b + √c).
• LMLExplore/Analysis/SpecialFunctions/Log/Basic.lean, next to Real.log_div_rpow_le_exp_neg_one: Real.log_le_rpow_div_exp_one_mul (log y ≤ y^γ / (e γ) for y ≥ 0, which is Mathlib's Real.log_le_rpow_div sharpened by the factor e) and Real.log_le_of_le_mul_sq_log (1 ≤ y ≤ M log² y gives log y ≤ (8/5) log (4 M), with no assumption on M).

No declaration is removed or renamed.

Source: this PR ports item R24 of the paper project RemyDegenne/Essakine2026Tight, at commit 73a8c16c42ec1c41f8d38c5d2af232f36c2cff15 (Apache-2.0), files Essakine2026Tight/ForLMLExplore/Analysis/Real/Sqrt.lean, Analysis/SpecialFunctions/Pow/Real.lean and Analysis/SpecialFunctions/Log/SelfBounding.lean. Changes from the source:

• The reduction lemma is generalised from L = log (α τ) to any L ≥ 1.
• The hypothesis 0 ≤ τ is dropped from the final bounds, and y > 0 is relaxed to y ≥ 0 in log_le_rpow_div_exp_one_mul.
• The 1 ≤ log (α τ) helper and the 4 α K bound are now private, and the hypothesis M > 0 of the source's log y ≤ (8/5) log (4 M) is dropped (it follows from the others).
• The two log lemmas go into the existing Log/Basic.lean rather than a new Pow/Real.lean.
• The source's weighted AM–GM lemmas are not ported here, because nothing in this item uses them; they will come with the KL-to-Bernstein item that does.

Local checks (not CI): lake build --iofail green; the local changed-module axiom check found 0 violations in 58 declarations; the local environment lint passed.

Paper: RemyDegenne/Essakine2026Tight
Item: R24

🤖 Prepared with Claude Code

[RemyDegenne]

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

The informal sources [MDJKLV21, Lemma 13] and [EV26, Lemma 29] are credited, but the formalization this PR ports (RemyDegenne/Essakine2026Tight, item R24) is named only in the PR description and in none of the changed files.

• LMLExplore/Analysis/SpecialFunctions/Log/SelfBounding.lean:40 — The file is a port of Essakine2026Tight/ForLMLExplore/Analysis/SpecialFunctions/Log/SelfBounding.lean (per the PR description), but the module docstring credits only the papers, not this prior formalization. Fix: Add to the docstring: 'The statements and proofs are adapted from the formalization in the paper project RemyDegenne/Essakine2026Tight (file ForLMLExplore/Analysis/SpecialFunctions/Log/SelfBounding.lean, by Rémy Degenne, Apache 2.0)', with a brief note on the generalisations.
• LMLExplore/Analysis/SpecialFunctions/Log/Basic.lean:176 — Real.log_le_of_le_mul_sq_log and Real.log_le_rpow_div_exp_one_mul (line 162) are ported from the source's Analysis/SpecialFunctions/Pow/Real.lean, following its proof plan (exponent 3/16, constant 8/5), but they carry no credit. Fix: Credit RemyDegenne/Essakine2026Tight (ForLMLExplore/Analysis/SpecialFunctions/Pow/Real.lean) in these declarations' docstrings or in the module docstring.

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 · 28s · 77.7k in (52.5k cache read, 25.2k cache write) / 2.5k out tokens · reviewing this diff · rubric}

[RemyDegenne]

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

Two hypotheses are stronger than their proofs need: 0 < M in Real.log_le_of_le_mul_sq_log follows from the other hypotheses, and 1 < τ in Real.log_le_of_le_sqrt_mul_add can be weakened to 1 ≤ τ. The rest is at the natural level, with the special cases derived from the general lemmas.

• LMLExplore/Analysis/SpecialFunctions/Log/Basic.lean:177 — hM : 0 < M is redundant: from 1 ≤ y, 0 ≤ log y and y ≤ M * log y ^ 2, the case M ≤ 0 would give y ≤ 0, which contradicts 1 ≤ y. Fix: Drop hM and derive 0 < M inside the proof, as in (hy : 1 ≤ y) (h : y ≤ M * log y ^ 2). Then remove the hK0 proof that log_le_of_le_sqrt_mul_add (SelfBounding.lean:109–111) needs only to supply this argument.
• LMLExplore/Analysis/SpecialFunctions/Log/SelfBounding.lean:101 — hτ : 1 < τ is stronger than needed. The proof uses only hτ.le (for exp 1 ≤ α * τ) and 0 < τ, and both follow from 1 ≤ τ. Fix: Change the hypothesis to (hτ : 1 ≤ τ) and pass h1.le at the call site on line 140.

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 · 32s · 49.5k in (41.8k cache read, 7.7k cache write) / 3.2k out tokens · reviewing this diff · rubric}

[RemyDegenne]

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

The module and declaration docstrings are accurate, and the counterexample to the printed constant holds when recomputed; one docstring overclaims by calling a bound "sharp" when nothing establishes that.

• LMLExplore/Analysis/SpecialFunctions/Log/SelfBounding.lean:120 — The docstring of Real.le_mul_sq_log_add_one_of_le_sqrt_mul_add calls it "The self-bounding inequality, sharp form". Nothing shows the bound K ((8/5) log M)² + 1 is tight; it is only the general form, with M free, that the two main theorems specialise. Fix: Replace "sharp form" with "general form" (or "for any M ≥ 4 α K").

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 · 24s · 73.8k in (68k cache read, 5.8k cache write) / 2.1k out tokens · reviewing this diff · rubric}

[RemyDegenne]

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

The proofs are readable and robust, but SelfBounding.lean writes out the same block twice: deriving 1 ≤ log(α τ), getting τ ≤ K L² and proving 0 < K.

• LMLExplore/Analysis/SpecialFunctions/Log/SelfBounding.lean:130 — le_mul_sq_log_add_one_of_le_sqrt_mul_add repeats the steps of log_le_of_le_sqrt_mul_add (lines 104-111): the 1 ≤ log (α τ) derivation via le_log_iff_exp_le (mul_pos hα0 …), the call to le_mul_sq_of_le_sqrt_mul_add, and the by_contra! hK; nlinarith proof of 0 < K. The 'inlined one-liner' is used twice, so it is not a one-off. Fix: Restore a public helper giving 1 ≤ log (α * τ) from exp 1 ≤ α and 1 < τ, and factor τ ≤ K L² ∧ 0 < K (for τ > 1) into one lemma used by both theorems.

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 · 35s · 49.2k in (42.1k cache read, 7.1k cache write) / 3.2k out tokens · reviewing this diff · rubric}

[RemyDegenne]

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	approved	claude/claude-opus-5-5	The statements match [MDJKLV21, Lemma 13] with a correctly repaired constant; the counterexample to the printed constant checks out numerically, and the edge cases (K = 0, A + E = 0, τ ≤ 1, negative τ) and the helper bounds are all sound.
✅	reuse	approved	claude/claude-opus-5-5	No existing Mathlib or LMLExplore declaration covers the new quadratic-root lemma, the e-sharpened log/rpow bound, the inversion of y ≤ M log² y or the self-bounding inequality; the existing lemmas these build on are reused where they apply.
✅	scope	approved	claude/claude-opus-5-5	The PR proves the tool "the inversion of the implicit inequality on τ [MDJKLV21, Lemma 13]", which ReinforcementLearning Layer 19.2 lists explicitly; the square-root and log helpers are used by the main proof, so it is one topic.
🟡	attribution	changes requested	claude/claude-opus-5-5	The informal sources [MDJKLV21, Lemma 13] and [EV26, Lemma 29] are credited, but the formalization this PR ports (RemyDegenne/Essakine2026Tight, item R24) is named only in the PR description and in none of the changed files.
✅	api-design	approved	claude/claude-opus-5-5	The public surface is minimal and well placed: the general quadratic-root and log/rpow lemmas are public in their canonical files, and the only private helper is specific to the constant K of this argument. The PR adds no definitions or annotations, and leaves no compatibility surface.
🟡	generality	changes requested	claude/claude-opus-5-5	Two hypotheses are stronger than their proofs need: 0 < M in Real.log_le_of_le_mul_sq_log follows from the other hypotheses, and 1 < τ in Real.log_le_of_le_sqrt_mul_add can be weakened to 1 ≤ τ. The rest is at the natural level, with the special cases derived from the general lemmas.
✅	placement	approved	claude/claude-opus-5-5	The quadratic-root lemma, the log bounds and the self-bounding file each sit in the existing file or directory that matches their topic and dependencies. The only new import, Mathlib.Analysis.Complex.ExponentialBounds, is needed for exp_one_gt_d9.
✅	naming	approved	claude/claude-opus-5-5	New names describe their conclusions in standard Mathlib terminology, consistent with Real.log_le_rpow_div and adjacent Real lemmas; no notation is introduced.
🟡	documentation	changes requested	claude/claude-opus-5-5	The module and declaration docstrings are accurate, and the counterexample to the printed constant holds when recomputed; one docstring overclaims by calling a bound "sharp" when nothing establishes that.
🟡	proof-quality	changes requested	claude/claude-opus-5-5	The proofs are readable and robust, but SelfBounding.lean writes out the same block twice: deriving 1 ≤ log(α τ), getting τ ≤ K L² and proving 0 < K.

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

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