[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.
• 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: Real.one_le_log_mul (1 ≤ log (x y) for x ≥ e and y ≥ 1, next to Real.one_le_log_natCast_of_three_le), and, 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 4 α K bound is now private, the 1 ≤ log (α τ) helper is the public Real.one_le_log_mul in Log/Basic.lean, and the hypothesis M > 0 of the source's log y ≤ (8/5) log (4 M) is dropped (it follows from the others).
• The 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 59 declarations; the local environment lint passed.

Paper: RemyDegenne/Essakine2026Tight
Item: R24

🤖 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	The statements match [MDJKLV21, Lemma 13] with a correctly repaired constant, and the counterexample to the published constant checks out (hypothesis ≈4.16e8 ≥ τ = 4e8, published bound ≈3.27e8). The helper lemmas are true as stated, the dropped hypotheses (M > 0, τ ≥ 0, positivity, B ≥ 1) really are unnecessary, and the degenerate cases are handled without vacuity.
✅	reuse	approved	claude/claude-opus-5-5	No existing Mathlib or LMLExplore declaration covers the quadratic-root lemma, the e-sharpened log/rpow bound, the inversion of y ≤ M log² y, one_le_log_mul or the self-bounding inequality; Mathlib has only the weaker Real.log_le_rpow_div and the linear-term-free Real.le_sqrt_of_sq_le. The proofs reuse existing API, and the primed variant and private helper are derived from the general lemmas without being proved again.
✅	scope	approved	claude/claude-opus-5-5	The PR proves the RF-Express tool 'the inversion of the implicit inequality on τ [MDJKLV21, Lemma 13]', listed at ReinforcementLearning/README.md:1668, and its sqrt and log helpers are all used by that proof, so it is one topic. No other RF-Express tool has merged yet, so this is not side work around a stalled target.
✅	attribution	approved	claude/claude-opus-5-5	Every adapted declaration credits the ported formalization RemyDegenne/Essakine2026Tight with its source file, and SelfBounding.lean cites [MDJKLV21, Lemma 13] and [EV26, Lemma 29] with full references, including where the constant is corrected. The roadmap is credited only in the PR description's Roadmap line.
✅	api-design	approved	claude/claude-opus-5-5	The new general lemmas (le_add_sqrt_of_sq_le, one_le_log_mul, log_le_rpow_div_exp_one_mul, log_le_of_le_mul_sq_log) are public in their natural files and do not duplicate Mathlib (only log_le_rpow_div and le_sqrt_of_sq_le exist there); the only private lemma is a step specific to this file's constant K, and there are no definitions, shims or annotations to judge.
✅	generality	approved	claude/claude-opus-5-5	Each hypothesis is needed and matches Mathlib convention: dropping 0 ≤ b in le_add_sqrt_of_sq_le (b=-1, c=1, x=0.6) or 1 ≤ y in log_le_of_le_mul_sq_log (y=e^-10, M=e^-10/100) gives counterexamples. The quadratic step holds for any L ≥ 1, and both final bounds are short corollaries of the general M ≥ 4αK theorem, with no repeated proofs.
✅	placement	approved	claude/claude-opus-5-5	Each new declaration sits in its natural home: the quadratic-root lemma in Real/Sqrt, the log bounds next to their siblings in Log/Basic, and the generic self-bounding results in a new file inside the existing Log/ directory. Every import of SelfBounding.lean is used, including ExponentialBounds for exp_one_gt_d9, which Log/Basic imports non-publicly.
✅	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), with no collisions in the code or Mathlib; no notation is introduced.
✅	documentation	approved	claude/claude-opus-5-5	Module and declaration docstrings are accurate and do not overclaim; the prior finding is resolved because the docstring now says le_of_le_sqrt_mul_add' needs D ≥ 1, which the paper does not assume. The counterexample to the printed constant holds when recomputed.
✅	proof-quality	approved	claude/claude-opus-5-5	Proofs are short and robust, with comments on the non-obvious nlinarith/linear_combination steps and no goal-changing change/show or undocumented defeq. The reusable steps (le_add_sqrt_of_sq_le, one_le_log_mul, log_le_rpow_div_exp_one_mul, the private 4 α K bound) are already factored out.

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

_{Reviewing this diff at head 280e59e. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $4.05.}