[RemyDegenne]

This PR adds s-smoothness on a set and the descent lemma, the first bullet of OnlineLearning Layer 1.3 (Smoothness and self-bounded functions, [Ora, Definition 4.22]). The new file is LMLExplore/Analysis/Convex/Smooth.lean (189 lines).

• LMLExplore.SmoothOn V s f is the roadmap's definition exactly: f is differentiable on an open set containing V, and fderiv ℝ f is s-Lipschitz on V for the operator norm (LipschitzOnWith s (fderiv ℝ f) V, s : ℝ≥0). Its API is SmoothOn.differentiableAt, SmoothOn.mono, SmoothOn.weaken, and the @[simp] characterisation smoothOn_univ : SmoothOn univ s f ↔ Differentiable ℝ f ∧ LipschitzWith s (fderiv ℝ f), which is the form the "smooth on E" items of 1.3 and 1.4 use.
• Convex.norm_bregDiv_le_mul_norm_sub_sq: on a convex K, for any family f' of derivatives of f within K that is s-Lipschitz on K, ‖bregDiv f y x (f' x)‖ ≤ s / 2 * ‖y - x‖ ^ 2 for x, y ∈ K [Nes18, Lemma 1.2.3]. It is stated for F-valued f, as Mathlib's mean value inequalities are. Asking only for derivatives within K covers sets with empty interior, such as the simplex in α → ℝ. The proof restricts the remainder to the segment and applies Mathlib's image_norm_le_of_norm_deriv_right_le_deriv_boundary.
• Convex.bregDiv_le_mul_norm_sub_sq is the one-sided descent lemma for real f in the same setting.
• SmoothOn.norm_bregDiv_le_mul_norm_sub_sq and SmoothOn.bregDiv_le_mul_norm_sub_sq give the roadmap's statement for s-smooth f on a convex V, with fderiv. With F = ℝ the norm form is the roadmap's |f y - f x - f'(x)(y - x)| ≤ s/2 ‖y - x‖², since bregDiv f y x J = f y - f x - J (y - x) by definition.

Layer 1.3's other bullets remain after this PR: the gradient bound ‖f'(x)‖² ≤ 2s(f(x) - inf f), self-bounded functions, and their two implications. ReinforcementLearning 5.2 also consumes the descent lemma ("The descent lemma for L-smooth functions is the OnlineLearning roadmap's Layer 1.3").

On naming: Mathlib has open PRs leanprover-community/mathlib4#39574 and #43429 (neither is in the pinned Mathlib). There, LipschitzSmoothOnWith is a different predicate, the quadratic Taylor-remainder bound itself, and the descent lemma is the implication from a Lipschitz fderivWithin to it. The roadmap defines s-smoothness through a Lipschitz derivative, so this PR gives that predicate its own name, SmoothOn. Reusing LipschitzSmoothOnWith for a different meaning would make a later upstream adoption a rewrite instead of a deletion. The docstrings say that this is optimisation smoothness, not ContDiff. The conclusions use LMLExplore's bregDiv, as the neighbouring StrongConvexOn.mul_norm_sub_sq_le_bregDiv does.

The descent-lemma proof and its within-K form are adapted from the paper project RemyDegenne/Schlisselberg2026Hidden, file Schlisselberg2026Hidden/ForLMLExplore/Analysis/Convex/Smooth.lean, commit b08c8189133af6a5a8578c04ff6ae061acbdec60, Apache-2.0. The adaptation adds the roadmap's definition and its API, uses LipschitzOnWith, generalises to F-valued functions, and uses AffineMap.lineMap. The file credits [Nes18], [Ora] and [SSKM26] (Schlisselberg, Sherman, Koren and Mansour, arXiv:2511.22283v2, whose Lemma 22 and Theorem 2 use the within-set form).

This PR removes or renames no public declaration.

Roadmap: OnlineLearning

Paper: RemyDegenne/Schlisselberg2026Hidden
Item: R8

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

	rubric	state	judge	summary
✅	correctness	approved	claude/claude-opus-5-5	SmoothOn matches the roadmap's s-smoothness (differentiable on an open set containing V, fderiv s-Lipschitz on V; operator norm equals dual norm for F = ℝ), and the F = ℝ norm form is exactly the roadmap's two-sided descent lemma, with bregDiv's argument order pinned by h_one. The within-K version holds under its stated hypotheses, and no statement is vacuous or carries its conclusion in its assumptions.
✅	reuse	approved	claude/claude-opus-5-5	No Mathlib or LMLExplore declaration provides a Lipschitz-derivative smoothness predicate or the quadratic Taylor-remainder bound; the nearest LMLExplore results (Convex.exists_mem_segment_bregDiv_eq, ConvexOn.exists_mem_segment_apply_sub_sub_bregDiv_div_le) need second derivatives. The proof reuses Mathlib's image_norm_le_of_norm_deriv_right_le_deriv_boundary and hasDerivWithinAt_lineMap, and the corollaries are one-line specialisations stating the roadmap's items.
✅	scope	approved	claude/claude-opus-5-5	Adds the roadmap's s-smoothness definition and the descent lemma, which are the heading and first bullet of OnlineLearning Layer 1.3 (README.md:323-329); ReinforcementLearning 5.2 also uses the descent lemma. It is one coherent topic, and nothing on main duplicates it.
✅	attribution	approved	claude/claude-opus-5-5	The module docstring now credits the adapted formalization (RemyDegenne/Schlisselberg2026Hidden, file, commit, Apache-2.0), along with [Nes18], [Ora] and [SSKM26]. No central source is left uncredited, and the roadmap is not credited in the file.
✅	api-design	approved	claude/claude-opus-5-5	SmoothOn now has the API that characterises it: elimination lemmas, mono/weaken, the @[simp] lemma smoothOn_univ, and the new IsOpen.smoothOn_iff, which resolves the earlier finding. The surface is minimal, carries no free data, and leaves no compatibility layer behind.
✅	generality	approved	claude/claude-opus-5-5	The general within-set, F-valued Taylor-remainder bound is proved once, and the real, one-sided and SmoothOn forms are one-line corollaries. SmoothOn matches the roadmap's definition with no unused or too-strong hypotheses.
✅	placement	approved	claude/claude-opus-5-5	LMLExplore/Analysis/Convex/Smooth.lean is where the OnlineLearning roadmap puts smoothness (LMLExplore/Analysis/Convex/ for strong convexity, smoothness, ...), duplicates no existing predicate, and leaves no flat sibling-prefix clash. Every import supplies a lemma the proofs use (image_norm_le_of_norm_deriv_right_le_deriv_boundary, hasDerivWithinAt_lineMap, hasDerivAt_pow, dist_lineMap_left, the derivative of f ∘ lineMap, bregDiv), and none is broad.
✅	naming	approved	claude/claude-opus-5-5	Theorem names describe their conclusions consistently with the adjacent StrongConvexOn.mul_norm_sub_sq_le_bregDiv, Convex.*/IsOpen.* dot-notation placement is correct, and LMLExplore.SmoothOn does not collide with any pinned Mathlib declaration. No notation is introduced.
✅	documentation	approved	claude/claude-opus-5-5	The module docstring and every public declaration are documented accurately, and no docstring promises more than its statement delivers. The file contains no roadmap-layer or PR-process narrative; the provenance paragraph is a source credit.
✅	proof-quality	approved	claude/claude-opus-5-5	The descent-lemma proof is under 50 lines, its stages (restrict to the segment, bound the derivative, compare with the quadratic) are commented, and it uses no change/show and relies on no undocumented definitional equality. The smoothness API proofs are one-liners or short structure builds.

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

_{Reviewing this diff at head 9a64c1b. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $2.16.}