[RemyDegenne]

This PR completes OnlineLearning Layer 1.7, Numerical lemmas [Ora, Lemmas 4.13 and 4.29]. It adds the weighted comparison of a sum with an integral, its square-root and logarithmic corollaries, the explicit solution of the implicit bound x - √(a x + b) ≤ c, and the two quadratic bounds on log (1 + x).

Roadmap: OnlineLearning

New file Analysis/SumIntegralComparisons.lean, named after the Mathlib file whose AntitoneOn.sum_le_integral_of_integrableOn it generalizes:

• AntitoneOn.sum_mul_le_integral_of_integrableOn is Lemma 4.13. Take a t ≥ 0, and f antitone on (c, c + ∑_{t<n} a t] and integrable on [c, c + ∑_{t<n} a t]. Then ∑_{t<n} a t * f (c + ∑_{s≤t} a s) ≤ ∫ x in c..c + ∑_t a t, f x. The hypotheses follow Mathlib's unit-step lemma, which is the case a t = 1. The integrability hypothesis cannot be dropped: for f = x⁻¹ and c = 0 the Bochner integral is 0. Neither c ≥ 0 nor f ≥ 0 from the roadmap statement is needed.
• Real.sum_div_sqrt_le_two_mul_sqrt gives ∑_{t<n} a t / √(∑_{s≤t} a s) ≤ 2 √(∑_t a t). It is derived from the lemma with f x = (√x)⁻¹ and Mathlib's integral_rpow. A term with a zero denominator is 0 by Lean's convention, which matches the roadmap's "terms with a zero denominator omitted".
• Real.sum_div_add_le_log_div gives ∑_{t<n} a t / (c + ∑_{s≤t} a s) ≤ log ((c + ∑_t a t) / c) for c > 0, from the lemma with f x = x⁻¹ and integral_inv_of_pos.

In Analysis/Real/Sqrt.lean:

• Real.le_div_two_add_add_sqrt_of_sub_sqrt_le: for a ≥ 0, x - √(a x + b) ≤ c implies x ≤ a/2 + c + √(a²/4 + b + a c). This is the sharp form of Lemma 4.29.
• Real.le_add_add_sqrt_of_sub_sqrt_le: for a ≥ 0, x ≤ a + c + √(b + a c), the roadmap's form. It follows from the sharp form and Tau Ceti's Real.sqrt_add_le_add_sqrt.
• Only a ≥ 0 is assumed. [Ora] also asks b, c, x ≥ 0, but the proof does not need them. a ≥ 0 cannot be dropped: a = -4, b = -100, c = x = 0 satisfies the hypothesis but not the conclusion.

In Analysis/SpecialFunctions/Log/Basic.lean:

• Real.sub_sq_le_log_one_add: x - x² ≤ log (1 + x) for x ≥ -1/2. [Ora, §13.7] uses it for |x| ≤ 1/2, for coin betting. It fails at x = -0.9.
• Real.log_one_add_le_sub_sq_div_four: log (1 + x) ≤ x - x²/4 for -1 < x ≤ 1 [Ora, Example 7.39, exp-concave losses]. It fails at x = 2.
• Both are proved by monotonicity from the sign of the derivative (monotoneOn_/antitoneOn_of_hasDerivWithinAt_*). The case x ≥ 0 of the lower bound comes from Mathlib's le_log_one_add_of_nonneg. A private helper gives the derivative of log (1 + y) + p y.

New file Analysis/Calculus/MeanValue.lean, named after the Mathlib file whose monotoneOn_of_hasDerivWithinAt_nonneg and antitoneOn_of_hasDerivWithinAt_nonpos it combines:

• LMLExplore.apply_le_apply_of_hasDerivAt_of_nonneg_of_nonpos: if f has derivative f' y at each y between x and x₀, with f' ≥ 0 on (x, x₀) and f' ≤ 0 on (x₀, x), then f x ≤ f x₀. The two log bounds above apply it at x₀ = 0.

Consumers: Layer 2.3 (adaptive rates, the 2√(B ∑‖y_t‖²/m) bound via the square-root sum, and the L⋆ bound for self-bounded losses via Lemma 4.29, which the roadmap item names as "(Layer 1.7)"), Layer 2.4 (AdaGrad), Layer 8 (the logarithmic sum and the upper bound on log (1 + x) for exp-concave losses), and Layer 13 (the lower bound on log (1 + x) for coin betting).

Reuse: I searched Mathlib, Tau Ceti, LML, Statlib and LMLExplore for a weighted sum–integral comparison, for sums a t / √(∑_{s≤t} a s) and a t / (c + ∑_{s≤t} a s), for the implicit bound x - √(a x + b) ≤ c, and for quadratic bounds on log (1 + x). None of them exists. Mathlib has only the unit-step AntitoneOn.sum_le_integral* and le_log_one_add_of_nonneg (2x/(x+2) ≤ log (1 + x)). LMLExplore's Real.le_add_sqrt_of_sq_le and Real.sum_div_sqrt_max_one_le are different statements: one solves a quadratic inequality, the other is the doubling bound with denominators clipped at 1. The proofs reuse sum_integral_adjacent_intervals, integral_mono_on_of_le_Ioo, integral_rpow, intervalIntegrable_rpow', integral_inv_of_pos and Tau Ceti's Real.sqrt_add_le_add_sqrt.

No public declaration is removed or renamed.

What remains: Layer 1.7 is complete. Items 1.2–1.6 of Layer 1 remain, and Layer 2.3 can now be built on these lemmas.

Local checks only (CI verifies the pushed PR): scope: scoped: against 34d96f1b8f111131d1e459ccaf61245f0e5ea285. local-axioms: checked 4 changed module(s), 74 declaration(s); 0 violation(s). The source guards, the whole-library lake build --iofail, the module-system audit, the header check and the environment lint (checked 4 changed module(s), 74 declarations; 14 environment linters) passed, and the verify script exited 0.

🤖 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	All six new statements match roadmap item OnlineLearning 1.7 [Ora, Lemmas 4.13, 4.29] with the same or weaker hypotheses, and none is vacuous. Edge cases (zero denominators, A = 0, x ≤ c and b + ac < 0 in the implicit bound, the endpoints of the log ranges) and the derivative signs all check out.
✅	reuse	approved	claude/claude-opus-5-5	No Mathlib or LMLExplore declaration covers the variable-step weighted sum–integral comparison, its square-root and log corollaries, the implicit bound x - √(a x + b) ≤ c, or the quadratic log (1 + x) bounds; Mathlib's sum_*le_integral* lemmas, including sum_mul_Ico_le_integral_of_monotone_antitone, all use integer steps. The proofs reuse sum_integral_adjacent_intervals, integral_mono_on_of_le_Ioo, integral_rpow, integral_inv_of_pos, le_log_one_add_of_nonneg and monotoneOn_/antitoneOn_of_hasDerivWithinAt_*.
✅	scope	approved	claude/claude-opus-5-5	Every new declaration matches a bullet of OnlineLearning Layer 1.7, Numerical lemmas (roadmap README.md:363-371), and the MeanValue helper is a direct prerequisite of the two log bounds. The PR completes that one item as a single unit.
✅	attribution	approved	claude/claude-opus-5-5	Every changed file with sourced material cites [Ora] (arXiv:1912.13213v10), and each new theorem's docstring names its Ora location (Lemma 4.13, Lemma 4.29, Example 7.39, §13.7). The weighted comparison names the Mathlib unit-step lemma it generalizes, and MeanValue.lean names the Mathlib monotonicity lemmas it combines.
✅	api-design	approved	claude/claude-opus-5-5	The public surface is the Layer 1.7 targets, the sharp form of Lemma 4.29, the weighted sum–integral comparison and a general mean-value comparison lemma in its own calculus file; the only private helper is log-specific proof glue. No definitions, exposed bodies, compatibility artifacts or missing annotations.
✅	generality	approved	claude/claude-opus-5-5	The weighted sum–integral comparison, its square-root and logarithmic corollaries, the implicit square-root bound and the log bounds are stated at the natural level, and the corollaries are derived from the general lemma. The earlier finding is fixed: the mean-value lemma now takes ContinuousOn on the segment and a derivative only on the open interval, like Mathlib's monotoneOn_of_hasDerivWithinAt_nonneg.
✅	placement	approved	claude/claude-opus-5-5	Each new declaration sits in a topical home that mirrors Mathlib: the sum–integral comparison and its two corollaries go in Analysis/SumIntegralComparisons.lean, the derivative-sign lemma in Analysis/Calculus/MeanValue.lean, and the sqrt and log bounds in their existing files. The new imports (TauCeti.Analysis.SpecialFunctions.Sqrt, LMLExplore.Analysis.Calculus.MeanValue, Mathlib.Analysis.SpecialFunctions.Integrals.Basic) are each used and specific, and no flat sibling-prefix clash is introduced.
✅	naming	approved	claude/claude-opus-5-5	New names describe their conclusions in standard Mathlib terminology, matching AntitoneOn.sum_le_integral_of_integrableOn and the adjacent Real.le_add_sqrt_of_sq_le/Real.sum_div_sqrt_max_one_le, and sit in the correct AntitoneOn/Real/LMLExplore namespaces. No notation is introduced.
✅	documentation	approved	claude/claude-opus-5-5	Each new file has a module docstring giving its content and mathematical purpose, and every public theorem's docstring matches its statement; the Mathlib cross-references (AntitoneOn.sum_le_integral_of_integrableOn with Ioc antitonicity and Icc integrability) check out against the source. No docstring overclaims or contains process narrative.
✅	proof-quality	approved	claude/claude-opus-5-5	The shared derivative-sign argument is in the reusable apply_le_apply_of_hasDerivAt_of_nonneg_of_nonpos, and the other proofs are short, commented and closed by linarith/nlinarith/field_simp/simp. The show terms only state facts passed to rw or le_sqrt_of_sq_le, and no proof relies on undocumented definitional equality.

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

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