[RemyDegenne]

This PR adds the logarithmic sum bound of RF-Express [MDJKLV21, Lemma 9] to LMLExplore/Analysis/SpecialFunctions/Log/Basic.lean. If 0 ≤ u k ≤ max 1 (U k) for every k < n, where U k = ∑_{i < k} u i, then ∑_{k < n} u k / max 1 (U k) ≤ 3 log (U n + 1) (Real.sum_div_max_one_le_three_mul_log). Real.sum_div_max_one_le_four_mul_log is the statement exactly as the roadmap and the source give it, for u k ∈ [0, 1] and with the constant 4. The proof telescopes the one-step bound u / max 1 U ≤ 3 (log (U + u + 1) - log (U + 1)), which follows from 1 - x⁻¹ ≤ log x (Mathlib's Real.one_sub_inv_le_log_of_pos) together with U + u + 1 ≤ 3 max 1 U.

Target: ReinforcementLearning, Layer 19.2 (RF-Express [MDJKLV21, Theorem 1]), tool bullet "$\sum_t u_{t+1}/\max(1,U_t)\le4\log(U_{T+1}+1)$ [MDJKLV21, Lemma 9]". On indexing: the source writes U_t = ∑_{l=1}^t u_l and sums over t = 0, …, T. Re-indexing from 0 (u k = u_{k+1}, n = T + 1) gives exactly the Lean statement. I checked this against the text of Lemma 9 in arXiv:2007.13442. This is the version with the 0-based indices. The hypotheses are weakened from u k ≤ 1 to u k ≤ max 1 (U k), the same hypotheses as the neighbouring doubling bound Real.sum_div_sqrt_max_one_le (LMLExplore/Analysis/Real/Sqrt.lean), and the same proof gives the constant 3. The one-step bound is private, as in that sibling. I add the new statements at the end of the file and at the end of its docstring list, so they don't overlap with the edits that the open PR #287 makes to the same file.

After this PR, the last open tools of Layer 19.2 are in open PRs: counts versus pseudo-counts in #292, the KL-to-Bernstein transport and variance transfers in #291, and the implicit-inequality inversion in #287. What remains for the milestone is the RF-Express algorithm itself, on the Layer 7.7 and Layer 14 infrastructure (statesEnv, episodic counts and stream models), and its PAC and sample-complexity theorems.

Source: this is adapted from the paper project RemyDegenne/Essakine2026Tight at commit 9c77165d56f81c1db7a9835068356bb14886a3be (Apache 2.0), file Essakine2026Tight/ForLMLExplore/Analysis/SpecialFunctions/Log/Basic.lean (Real.sum_div_max_one_le_three_mul_log, Real.sum_div_max_one_le_four_mul_log, stated there for u k ∈ [0, 1]). The paper is [EV26, Lemma 28], and the constant 3 follows that project's notes/paper-errata.md E19. The code credits the source and its reference [MDJKLV21]. No public declaration is removed or renamed.

Roadmap: ReinforcementLearning

Paper: RemyDegenne/Essakine2026Tight
Item: R25

🤖 Prepared with Claude Code