[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.

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 3 changed module(s), 72 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 3 changed module(s), 72 declarations; 14 environment linters) passed, and the verify script exited 0.

🤖 Prepared with Claude Code

[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.

⚠️ 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] under the same or weaker hypotheses; the extra integrability hypothesis is necessary for the Bochner integral, and the edge cases (zero denominators, n = 0, a < 0, endpoints of the log ranges) behave correctly.
✅	reuse	approved	claude/claude-opus-5-5	No existing Mathlib or LMLExplore declaration covers the weighted sum–integral comparison, its square-root and logarithmic corollaries, the implicit square-root bound, or the quadratic log (1 + x) bounds: Mathlib has only the unit-step AntitoneOn.sum_le_integral* (Mathlib/Analysis/SumIntegralComparisons.lean:116), and Real.le_add_sqrt_of_sq_le needs b + a c ≥ 0, which the new lemma does not assume. The proofs reuse the appropriate library lemmas; the Tau Ceti sources were not in the checkout, so Real.sqrt_add_le_add_sqrt and the absence of Tau Ceti duplicates could not be checked.
✅	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 PR completes that item as one unit with no unrelated material.
✅	attribution	approved	claude/claude-opus-5-5	Each changed file adds an [Ora] reference, and each new theorem's docstring names its source (Lemma 4.13, Lemma 4.29, Example 7.39 or §13.7). The weighted comparison credits the Mathlib unit-step lemma it generalizes, and no other uncredited source was found.
🟡	api-design	changes requested	claude/claude-opus-5-5	The public surface is the Layer 1.7 targets plus the sharp form of Lemma 4.29 and the weighted integral comparison, and it is well-named and has no definitions or exposed bodies. One general mean-value monotonicity lemma is hidden as private in the log file instead of being made public in a calculus file.
✅	generality	approved	claude/claude-opus-5-5	The weighted sum–integral comparison keeps Mathlib's unit-step hypotheses and drops the roadmap's unneeded sign conditions, and both corollaries are derived from it. The implicit bound and the two log bounds assume only what is needed: a ≥ 0 is shown necessary, and the log ranges are the natural cutoffs.
✅	placement	approved	claude/claude-opus-5-5	Each new declaration is in its topical home: the weighted sum–integral comparison and its corollaries are in a new Analysis/SumIntegralComparisons.lean mirroring Mathlib, and the sqrt and log lemmas are in their existing files. The previously unused Mathlib.Analysis.SumIntegralComparisons import is gone, and the new non-public TauCeti import is used by sqrt_add_le_add_sqrt.
✅	naming	approved	claude/claude-opus-5-5	Names describe conclusions in standard Mathlib terminology and follow Mathlib's AntitoneOn.sum_le_integral_of_integrableOn and the adjacent Real.* lemmas; declarations sit in the correct AntitoneOn/Real namespaces. No notation is introduced.
🟡	documentation	changes requested	claude/claude-opus-5-5	The docstrings are accurate and mathematically motivated, except that the new file's module docstring states the weighted sum–integral comparison without the integrability hypothesis, which makes the statement false. Add the hypothesis to that sentence.
✅	proof-quality	approved	claude/claude-opus-5-5	The repeated derivative-sign argument now lives in the shared helper le_apply_zero_of_hasDerivAt, and the non-terminal simp calls now use simp only with explicit lemmas, so both prior findings are resolved. The remaining proofs are short, use robust automation and have comments, with no undocumented defeq manipulation.

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

_{Reviewing this diff at head 145910c. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $2.31.}

[RemyDegenne]

🟡 api-design — request_changes claude/claude-opus-5-5

The public surface is the Layer 1.7 targets plus the sharp form of Lemma 4.29 and the weighted integral comparison, and it is well-named and has no definitions or exposed bodies. One general mean-value monotonicity lemma is hidden as private in the log file instead of being made public in a calculus file.

• LMLExplore/Analysis/SpecialFunctions/Log/Basic.lean:108 — le_apply_zero_of_hasDerivAt is general one-variable calculus infrastructure: if f' ≥ 0 on (x, 0) and f' ≤ 0 on (0, x), then f x ≤ f 0. Its statement uses only HasDerivAt, Set.uIcc and Set.Ioo, and its proof never uses log, yet it is private in the log file. Fix: Generalize the point 0 to an arbitrary x₀ (f x ≤ f x₀) and make it public in a calculus file mirroring Mathlib, e.g. LMLExplore/Analysis/Calculus/MeanValue.lean, or send it upstream. Keep hasDerivAt_log_one_add_add private, since it only serves this file.

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 · 80.9k in (71.5k cache read, 9.4k cache write) / 2k out tokens · reviewing this diff · rubric · ⚠️ rubrics checkout differs from published main}

[RemyDegenne]

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

The docstrings are accurate and mathematically motivated, except that the new file's module docstring states the weighted sum–integral comparison without the integrability hypothesis, which makes the statement false. Add the hypothesis to that sentence.

• LMLExplore/Analysis/SumIntegralComparisons.lean:15 — The module overview says 'for f antitone on (c, c + ∑ a t] and a t ≥ 0, ∑ a t f(c + ∑_{s≤t} a s) ≤ ∫ f', leaving out integrability on [c, c + ∑ a t]. Without it the claim is false, so the overview promises more than the theorem proves. Fix: Change it to 'for f antitone on (c, c + ∑_{t < n} a t] and integrable on [c, c + ∑_{t < n} a t], and a t ≥ 0, ...', matching the theorem's 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 · 22s · 48.6k in (41.9k cache read, 6.7k cache write) / 2.1k out tokens · reviewing this diff · rubric · ⚠️ rubrics checkout differs from published main}