[RemyDegenne]

This PR adds OnlineLearning Layer 2.4, AdaGrad [Ora, Algorithm 4.1, Theorem 4.32, Definition 4.33], the last open item of the milestone "Layer 2: Online subgradient descent beyond √n". As the roadmap asks, AdaGrad is built as the coordinatewise product of learners (Layer 0.2, OnlineLearner.pi), and its bound comes from item 3 in dimension one (onlineSubgradientDescent_regret_le_mul_sqrt_sum, #398). After this PR, every item of Layer 2 has been stated and proved, so nothing is left on this milestone. (The guessing-game completion check of Layer 2 is already covered by onlineSubgradientDescent_regret_sq_sub_le_one_add_log.)

Roadmap: OnlineLearning

In LMLExplore/OnlineLearning/AdaptiveRate.lean, next to the adaptive-rate results it uses (new section AdaGrad; the module docstring and title are updated):

• OnlineLearner.adaGradIcc l r h x₀ : OnlineLearner C ℝ ℝ is AdaGrad in dimension one, that is, projected online subgradient descent on [l, r] with the rates (r - l) / √(2 ∑ s ≤ t, g s ^ 2) of [Ora, Theorem 4.14]. Its first play is projIcc l r h x₀, so no membership hypothesis is needed. Its API: run_adaGradIcc_zero (simp), run_adaGradIcc_succ (the update), run_adaGradIcc_mem, run_adaGradIcc_const_mul (scale-free), and hasRegretBound_adaGradIcc, which bounds the regret for linear losses x ↦ g t * x by (r - l) √(2 ∑ t < n, g t ^ 2). The history recursion is a private helper adaGradIccPlay; users only need the run lemmas.
• OnlineLearner.adaGrad l r h x₀ : OnlineLearner C (α → ℝ) (α → ℝ) is pi of the adaGradIcc (l a) (r a). Its API: run_adaGrad (reduction to coordinates), run_adaGrad_zero (simp), run_adaGrad_succ (the coordinatewise update of Algorithm 4.1), run_adaGrad_mem (plays in the box), and run_adaGrad_mul, the roadmap's coordinatewise scale-freeness: multiplying each coordinate of every feedback by a positive constant k a leaves the plays unchanged.
• hasRegretBound_adaGrad is Theorem 4.32 for linear losses x ↦ ∑ a, g t a * x a: the bound is √2 ∑ a, (r a - l a) √(∑ t < n, g t a ^ 2) against every u in the box. It is derived from HasRegretBound.pi and hasRegretBound_adaGradIcc.
• regret_run_adaGrad_le is Theorem 4.32 for convex losses: if ∑ a, g t a • proj a is a subgradient of f t within the box at each play, the regret of f has the same bound. The feedback is arbitrary, so the bound also holds for closed-loop (adaptive) feedback.

New file LMLExplore/Algebra/Order/Interval/Set/ProjIcc.lean, general infrastructure that AdaGrad's projection step needs:

• Set.isMinOn_abs_sub_projIcc: in a linearly ordered additive group, projIcc a b h x minimizes y ↦ |y - x| over Icc a b. Mathlib has the 1-Lipschitz bound Set.abs_projIcc_sub_projIcc, but not the nearest-point property.

No public declaration is removed or renamed.

Reuse: I grepped Mathlib, Tau Ceti, LML and Statlib at the pinned versions, and LMLExplore/, for AdaGrad/adaGrad (no hits). I also grepped for projIcc together with abs/dist/IsMinOn. The only related lemma is Mathlib's Set.abs_projIcc_sub_projIcc, which is a contraction bound, not the nearest-point property. The proofs reuse the merged onlineSubgradientDescent_regret_le_mul_sqrt_sum, OnlineLearner.pi/HasRegretBound.pi/run_pi, sum_sub_le_sum_apply_sub_of_hasSubgradientWithinAt, LML's hasSubgradientWithinAt_linear and Tau Ceti's Real.sqrt_sq_mul. Sources cited in the file: [Ora] and the original AdaGrad paper [DHS11] (Duchi, Hazan and Singer, JMLR 2011).

Local checks only (CI verifies the pushed PR): scope: scoped: against 7142c37d5e5dacc0509d1da87594fe25c9d6e0f5. local-axioms: checked 2 changed module(s), 56 declaration(s); 0 violation(s). The whole-library lake build --iofail, the source guards, the module-system audit, the header check and the environment lint (2 changed modules, 56 declarations, 14 environment linters) all 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	AdaGrad's definitions, update rule, scale-freeness and regret bounds (linear and convex) faithfully formalize [Ora, Algorithm 4.1, Theorem 4.32, Definition 4.33] and roadmap Layer 2.4, with no vacuous hypotheses or placeholders. The projIcc nearest-point lemma is correctly stated.
✅	reuse	approved	claude/claude-opus-5-5	New material (nearest-point property of projIcc, AdaGrad learners and bounds) has no existing counterpart in Mathlib or LMLExplore, and the proofs reuse the located product-learner, adaptive-OSD and subgradient-linearization lemmas.
✅	scope	approved	claude/claude-opus-5-5	The PR delivers OnlineLearning Layer 2.4 (AdaGrad: box regret bound via pi plus item 3 in dimension one, and coordinatewise scale-freeness) as the roadmap specifies, together with the projIcc nearest-point lemma its projection step needs. It is a single coherent topic that delivers the target itself.
✅	attribution	approved	claude/claude-opus-5-5	AdaGrad is credited in the code to [Ora] (Algorithm 4.1, Theorems 4.14/4.32, Definition 4.33) and to the original paper [DHS11], with full reference entries; the roadmap is credited only in the PR description. The projIcc nearest-point lemma is routine and needs no attribution.
✅	api-design	approved	claude/claude-opus-5-5	The new public surface (adaGradIcc/adaGrad with their run, membership, scale-freeness and regret lemmas, plus the relocated general lemma Set.isMinOn_abs_sub_projIcc) is minimal, covers roadmap item 2.4, and keeps only the file-specific recursion private. Its simp annotations are well-placed and there is no compatibility surface.
✅	generality	approved	claude/claude-opus-5-5	The new nearest-point lemma is stated for linearly ordered additive groups, the natural level, and Mathlib only has the contraction bound for projIcc. The AdaGrad box results are derived from the interval results through pi, and the convex-loss bound from the linear one, with no duplicated special-case proofs and no unused or too-strong assumptions.
✅	placement	approved	claude/claude-opus-5-5	The nearest-point lemma for projIcc sits in a fitting generic Algebra/Order/Interval/Set/ProjIcc.lean, and AdaGrad sits next to the adaptive-rate subgradient-descent result it is built on. All new imports are used, and none is broad.
✅	naming	approved	claude/claude-opus-5-5	New names describe their conclusions in standard terminology and match adjacent precedent (run_pi, regret_run_sum_le, hasRegretBound_*); no notation is introduced.
✅	documentation	approved	claude/claude-opus-5-5	The new module and every new public declaration have accurate docstrings that describe the mathematics without overclaiming or process narrative. The references to Ora Theorem 4.14 and to closedLoopFeedback resolve to existing material in the repo.
✅	proof-quality	approved	claude/claude-opus-5-5	Proofs are short and built from the merged regret and product lemmas, with no undocumented definitional-equality manipulation or brittle rewrite chains of material length. The one non-obvious step, congr 3; field_simp in run_adaGradIcc_const_mul, is commented and confined.

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

_{Reviewing this diff at head 8823def. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $1.23.}