From 3969fb888763cff987c68ad083fe3ef4473c80a7 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 14 Nov 2026 23:24:17 +0100 Subject: [PATCH 1/3] =?UTF-8?q?feat:=20adaptive=20learning=20rates,=20self?= =?UTF-8?q?-bounded=20functions=20and=20L=E2=8B=86=20bounds?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Mirror descent with the adaptive learning rates sqrt(m B / sum_{s<=t} ||y_s||^2) has regret at most 2 sqrt(B sum ||y_t||^2 / m); projected online subgradient descent with D / sqrt(2 sum ||g_s||^2) has regret at most D sqrt(2 sum ||g_t||^2) [Ora, Theorem 4.14]; and for losses with ||g_t||^2 <= 2 s f_t(a_t), in particular nonnegative s-self-bounded losses, the L⋆ bound 4 s D^2 + 2 D sqrt(s sum f_t u) [Ora, Theorem 4.30]. Adds self-bounded functions (SelfBoundedOn), the gradient bound for smooth functions bounded below, and their self-boundedness. Co-Authored-By: Claude Code --- LMLExplore/Analysis/Convex/Smooth.lean | 95 +++++- LMLExplore/OnlineLearning/AdaptiveRate.lean | 293 +++++++++++++++++++ LMLExplore/OnlineLearning/MirrorDescent.lean | 9 + 3 files changed, 396 insertions(+), 1 deletion(-) create mode 100644 LMLExplore/OnlineLearning/AdaptiveRate.lean diff --git a/LMLExplore/Analysis/Convex/Smooth.lean b/LMLExplore/Analysis/Convex/Smooth.lean index cad68a7f..814459af 100644 --- a/LMLExplore/Analysis/Convex/Smooth.lean +++ b/LMLExplore/Analysis/Convex/Smooth.lean @@ -6,14 +6,16 @@ Authors: LMLExplore contributors module public import LeanMachineLearning.ForMathlib.Analysis.Convex.Bregman.Basic +public import LeanMachineLearning.ForMathlib.Analysis.Convex.Subgradient.Deriv public import Mathlib.Analysis.Calculus.MeanValue +import Mathlib.Algebra.QuadraticDiscriminant import Mathlib.Analysis.Calculus.Deriv.AffineMap import Mathlib.Analysis.Calculus.Deriv.Comp import Mathlib.Analysis.Calculus.Deriv.Pow import Mathlib.Analysis.Normed.Affine.AddTorsor /-! -# Smooth functions and the descent lemma +# Smooth functions, the descent lemma and self-bounded functions A function `f : E → F` on a real normed space is `s`-smooth on a set `V`, in the sense of convex optimization [Ora, Definition 4.22], if it is differentiable on an open set containing `V` and its @@ -29,6 +31,13 @@ The bound is first proved for a derivative within the set at its points, with no it. This covers sets with empty interior, such as the simplex in `α → ℝ`, on which the inexact mirror descent analysis of [SSKM26, Lemma 22, Theorem 2] uses it. +A function bounded below that is `s`-smooth on the whole space has small gradients near its +infimum: `‖f' x‖ ^ 2 ≤ 2 * s * (f x - inf f)`. +Functions with this property for all their subgradients within a set are called **self-bounded** +[Ora, Definition 4.26]; for nonnegative losses it bounds the squared gradients by the losses +themselves, which turns regret bounds in `∑ t, ‖g t‖ ^ 2` into `L⋆` bounds in the losses of the +best comparator [Ora, Theorem 4.30]. + The proof of `Convex.norm_bregDiv_le_mul_norm_sub_sq` and its within-set form are adapted from the formalization in the paper project RemyDegenne/Schlisselberg2026Hidden (, file @@ -39,6 +48,8 @@ formalization in the paper project RemyDegenne/Schlisselberg2026Hidden * `LMLExplore.SmoothOn V s f`: `f` is differentiable on an open set containing `V` and `fderiv ℝ f` is `s`-Lipschitz on `V`. +* `LMLExplore.SelfBoundedOn V s f`: `f` is bounded below on `V` and every subgradient `g` within + `V` at `x ∈ V` satisfies `‖g‖ ^ 2 ≤ 2 * s * (f x - inf_V f)`. ## Main statements @@ -50,6 +61,11 @@ formalization in the paper project RemyDegenne/Schlisselberg2026Hidden `|D_f(y, x)| ≤ s / 2 * ‖y - x‖ ^ 2`. * `LMLExplore.SmoothOn.bregDiv_le_mul_norm_sub_sq`: the descent lemma for an `s`-smooth real function on a convex set. +* `LMLExplore.SmoothOn.norm_fderiv_sq_le`: for `f` `s`-smooth on the whole space and bounded + below, `‖fderiv ℝ f x‖ ^ 2 ≤ 2 * s * (f x - ⨅ y, f y)`. +* `LMLExplore.SmoothOn.selfBoundedOn_univ`: such a function is `s`-self-bounded. +* `LMLExplore.SelfBoundedOn.norm_sq_le_of_nonneg`: a nonnegative `s`-self-bounded function has + `‖g‖ ^ 2 ≤ 2 * s * f x` for its subgradients `g` at `x`. ## References @@ -196,6 +212,83 @@ theorem smoothOn_univ {f : E → F} : lipschitzOnWith_univ.mp hf.lipschitzOnWith⟩, fun ⟨hd, hl⟩ ↦ ⟨?_, hl.lipschitzOnWith⟩⟩ exact ⟨univ, isOpen_univ, subset_rfl, hd.differentiableOn⟩ +/-- **The gradient of a smooth function bounded below.** If `f` is `s`-smooth +on the whole space and bounded below, then `‖fderiv ℝ f x‖ ^ 2 ≤ 2 * s * (f x - ⨅ y, f y)` at +every `x`, where `‖fderiv ℝ f x‖` is the dual norm. -/ +theorem SmoothOn.norm_fderiv_sq_le {f : E → ℝ} (hf : SmoothOn univ s f) + (hbdd : BddBelow (range f)) (x : E) : + ‖fderiv ℝ f x‖ ^ 2 ≤ 2 * s * (f x - ⨅ y, f y) := by + set c := 2 * s * (f x - ⨅ y, f y) + have hc : 0 ≤ c := by positivity [sub_nonneg.mpr (ciInf_le hbdd x)] + -- along each direction `v`, the descent lemma bounds `f` above by a quadratic in the step `r`, + -- which stays above the infimum of `f`: its discriminant is nonpositive + have h_dir (v : E) : (fderiv ℝ f x v) ^ 2 ≤ c * ‖v‖ ^ 2 := by + have h_quad (r : ℝ) : 0 ≤ s / 2 * ‖v‖ ^ 2 * (r * r) + fderiv ℝ f x v * r + + (f x - ⨅ y, f y) := by + have h_desc := hf.bregDiv_le_mul_norm_sub_sq convex_univ (mem_univ x) (mem_univ (x + r • v)) + have h_inf := ciInf_le hbdd (x + r • v) + simp only [bregDiv, add_sub_cancel_left, map_smul, smul_eq_mul, norm_smul, Real.norm_eq_abs, + mul_pow, sq_abs] at h_desc + nlinarith + have := discrim_le_zero h_quad + simp only [discrim, c] at this ⊢ + linarith + -- hence `|fderiv ℝ f x v| ≤ √c * ‖v‖` for every `v`, which bounds the operator norm + have h_norm : ‖fderiv ℝ f x‖ ≤ √c := by + refine ContinuousLinearMap.opNorm_le_bound _ (Real.sqrt_nonneg c) fun v ↦ ?_ + rw [Real.norm_eq_abs, ← Real.sqrt_sq (norm_nonneg v), ← Real.sqrt_mul hc] + exact Real.abs_le_sqrt (h_dir v) + exact (Real.le_sqrt (norm_nonneg _) hc).mp h_norm + +/-- A function `f : E → ℝ` is **`s`-self-bounded within `V`** [Ora, Definition 4.26] if it is +bounded below on `V` and every subgradient `g` of `f` within `V` at a point `x ∈ V` satisfies +`‖g‖ ^ 2 ≤ 2 * s * (f x - inf_V f)`, where `‖g‖` is the dual norm and `inf_V f = sInf (f '' V)`. +Subgradients are those of LML's `HasSubgradientWithinAt`. For a nonnegative function the bound +gives `‖g‖ ^ 2 ≤ 2 * s * f x` (`SelfBoundedOn.norm_sq_le_of_nonneg`), which is how it enters the +`L⋆` regret bounds of online learning [Ora, Theorem 4.30]. -/ +structure SelfBoundedOn (V : Set E) (s : ℝ≥0) (f : E → ℝ) : Prop where + /-- `f` is bounded below on `V`. -/ + bddBelow : BddBelow (f '' V) + /-- The squared dual norm of every subgradient within `V` at `x ∈ V` is at most + `2 * s * (f x - inf_V f)`. -/ + norm_sq_le : ∀ x ∈ V, ∀ g : E →L[ℝ] ℝ, HasSubgradientWithinAt f g V x → + ‖g‖ ^ 2 ≤ 2 * s * (f x - sInf (f '' V)) + +namespace SelfBoundedOn + +variable {f : E → ℝ} + +/-- An `s`-self-bounded function within `V` is `t`-self-bounded for every `t ≥ s`. -/ +protected theorem weaken (hf : SelfBoundedOn V s f) (hst : s ≤ t) : SelfBoundedOn V t f where + bddBelow := hf.bddBelow + norm_sq_le x hx g hg := by + have h_inf : sInf (f '' V) ≤ f x := csInf_le hf.bddBelow (mem_image_of_mem f hx) + calc ‖g‖ ^ 2 ≤ 2 * s * (f x - sInf (f '' V)) := hf.norm_sq_le x hx g hg + _ ≤ 2 * t * (f x - sInf (f '' V)) := by gcongr + +/-- For an `s`-self-bounded function within `V` that is nonnegative on `V`, every subgradient `g` +within `V` at `x ∈ V` satisfies `‖g‖ ^ 2 ≤ 2 * s * f x`. -/ +theorem norm_sq_le_of_nonneg (hf : SelfBoundedOn V s f) (hf0 : ∀ y ∈ V, 0 ≤ f y) (hx : x ∈ V) + {g : E →L[ℝ] ℝ} (hg : HasSubgradientWithinAt f g V x) : ‖g‖ ^ 2 ≤ 2 * s * f x := by + have h_inf : 0 ≤ sInf (f '' V) := + le_csInf (image_nonempty.mpr ⟨x, hx⟩) (forall_mem_image.mpr hf0) + nlinarith [hf.norm_sq_le x hx g hg, mul_nonneg (NNReal.coe_nonneg s) h_inf] + +end SelfBoundedOn + +/-- **Smooth functions are self-bounded** [Ora, Remark 4.27]. If `f` is `s`-smooth +on the whole space and bounded below, then it is `s`-self-bounded within the whole space: its only +subgradient at `x` is its derivative, whose squared norm is at most `2 * s * (f x - ⨅ y, f y)`. +No convexity is needed. -/ +theorem SmoothOn.selfBoundedOn_univ {f : E → ℝ} (hf : SmoothOn univ s f) + (hbdd : BddBelow (range f)) : SelfBoundedOn univ s f where + bddBelow := by rwa [image_univ] + norm_sq_le x _ g hg := by + rw [(hf.differentiableAt (mem_univ x)).hasFDerivAt.eq_of_hasSubgradientWithinAt + Filter.univ_mem hg, image_univ] + -- `⨅ y, f y` is by definition `sInf (range f)` + exact hf.norm_fderiv_sq_le hbdd x + end LMLExplore /-- On an open set `V`, a function is `s`-smooth if and only if it is differentiable on `V` and its diff --git a/LMLExplore/OnlineLearning/AdaptiveRate.lean b/LMLExplore/OnlineLearning/AdaptiveRate.lean new file mode 100644 index 00000000..037d2077 --- /dev/null +++ b/LMLExplore/OnlineLearning/AdaptiveRate.lean @@ -0,0 +1,293 @@ +/- +Copyright (c) 2026 LMLExplore contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: LMLExplore contributors +-/ +module + +public import LMLExplore.Analysis.Convex.Smooth +public import LMLExplore.Analysis.SumIntegralComparisons +public import LMLExplore.OnlineLearning.SubgradientDescent + +/-! +# Adaptive learning rates and `L⋆` bounds + +The regret bound of mirror descent with nonincreasing learning rates `η t` and an `m`-strongly +convex potential `F` is `B / η (n - 1) + ∑ t < n, η t / (2 m) * ‖y t‖ ^ 2`, where `B` bounds the +Bregman divergences `D_F(u, a t)` from the plays to the comparator. The learning rate that +balances the two terms after `n` rounds depends on the losses to come. The **adaptive learning +rates** [Ora, Section 4.2, Theorem 4.14] +`η t = √(m B / ∑ s ≤ t, ‖y s‖ ^ 2)` +use instead the losses observed so far, the loss of the current round included, and give the +regret bound `2 √(B ∑ t < n, ‖y t‖ ^ 2 / m)` against every comparator, at every horizon, with no +bound on the losses known in advance. While the losses observed so far all vanish, the learning +rate is `√(m B / 0) = 0` with Lean's division, and the step for the learning rate `0` is a +Bregman projection of the current play: the algorithm makes no step, as in [Ora]. + +For projected online subgradient descent with plays at distance at most `D` from the +comparator, as on a set of diameter `D`, the potential `‖·‖ ^ 2 / 2` with `B = D ^ 2 / 2` gives +the rates `η t = D / √(2 ∑ s ≤ t, ‖g s‖ ^ 2)` and the regret bound +`D √(2 ∑ t < n, ‖g t‖ ^ 2)` [Ora, Theorem 4.14]. When the squared norms of the subgradients are +controlled by the losses, `‖g t‖ ^ 2 ≤ 2 s f t (a t)`, as for nonnegative `s`-self-bounded losses +(`LMLExplore.SelfBoundedOn`), the regret is in turn controlled by the cumulative loss of the +comparator `u`: it is at most `4 s D ^ 2 + 2 D √(s ∑ t < n, f t u)` [Ora, Theorem 4.30]. This +**`L⋆` bound** is constant when the comparator has zero cumulative loss. + +## Main statements + +* `mirrorDescent_regret_le_two_mul_sqrt`: mirror descent with an `m`-strongly convex potential and + the adaptive learning rates has regret at most `2 √(B ∑ t < n, ‖y t‖ ^ 2 / m)`. +* `onlineSubgradientDescent_regret_le_mul_sqrt_sum`: [Ora, Theorem 4.14] projected online + subgradient descent with the adaptive learning rates, with plays at distance at most `D` from the + comparator, has regret at most `D √(2 ∑ t < n, ‖g t‖ ^ 2)`. +* `onlineSubgradientDescent_regret_le_of_norm_sq_le`: [Ora, Theorem 4.30] the `L⋆` bound + `4 s D ^ 2 + 2 D √(s ∑ t < n, f t u)` for losses with `‖g t‖ ^ 2 ≤ 2 s f t (a t)`. +* `onlineSubgradientDescent_regret_le_of_selfBoundedOn`: its form for nonnegative `s`-self-bounded + losses. + +## References + +* [Ora] F. Orabona, *Online learning: a modern introduction using convex optimization*, + arXiv:1912.13213v10, 2026. +-/ + +public section + +open Finset +open scoped NNReal + +namespace LMLExplore.OnlineLearning + +variable {n : ℕ} + +section NormedSpace + +variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {K : Set E} {F : E → ℝ} {u : E} + +/-- The case of `mirrorDescent_regret_le_two_mul_sqrt` with `B > 0` and a first round `t₀ < n` +with a nonzero loss. From `t₀` on, the adaptive learning rates are positive and nonincreasing; +before `t₀` the losses vanish, so that the steps are also steps for the learning rate of `t₀`, +and the bound of mirror descent with nonincreasing learning rates applies. -/ +private theorem mirrorDescent_regret_le_two_mul_sqrt_of_ne_zero {m B : ℝ} + (hF : StrongConvexOn K m F) (hm : 0 < m) (hB : 0 < B) (y : ℕ → E →L[ℝ] ℝ) (a : ℕ → E) + (F' : ℕ → E →L[ℝ] ℝ) (ha0K : a 0 ∈ K) {t₀ : ℕ} (ht₀n : t₀ < n) (hyt₀ : y t₀ ≠ 0) + (hy_lt : ∀ t < t₀, y t = 0) + (ha : ∀ t < n, IsMirrorDescentStep K F (√(m * B / ∑ s ∈ range (t + 1), ‖y s‖ ^ 2)) (y t) + (a t) (F' t) (a (t + 1))) + (hF' : ∀ t ≤ n, HasFDerivWithinAt F (F' t) K (a t)) + (hBu : ∀ t < n, bregDiv F u (a t) (F' t) ≤ B) (hu : u ∈ K) : + ∑ t ∈ range n, y t (a t - u) ≤ 2 * √(B * (∑ t ∈ range n, ‖y t‖ ^ 2) / m) := by + set S : ℕ → ℝ := fun t ↦ ∑ s ∈ range (t + 1), ‖y s‖ ^ 2 with hS_def + set A := ∑ t ∈ range n, ‖y t‖ ^ 2 with hA_def + have hS_mono : Monotone S := fun s t hst ↦ + sum_le_sum_of_subset_of_nonneg (range_subset_range.mpr (by omega)) fun _ _ _ ↦ sq_nonneg _ + have hS_pos (t : ℕ) (ht : t₀ ≤ t) : 0 < S t := + calc 0 < ‖y t₀‖ ^ 2 := pow_pos (norm_pos_iff.mpr hyt₀) 2 + _ ≤ S t := single_le_sum (f := fun s ↦ ‖y s‖ ^ 2) (fun _ _ ↦ sq_nonneg _) + (mem_range.mpr (by omega)) + -- the learning rate of round `t` is `r / √(S t)`, with `r = √(m B)` + set r := √(m * B) with hr_def + have hr : 0 < r := Real.sqrt_pos.mpr (mul_pos hm hB) + have hr_sq : r ^ 2 = m * B := Real.sq_sqrt (mul_pos hm hB).le + have h_rate (t : ℕ) : √(m * B / S t) = r / √(S t) := Real.sqrt_div' _ (by positivity) + -- the learning rates frozen at round `t₀` before it are positive and nonincreasing + set η : ℕ → ℝ := fun t ↦ r / √(S (max t t₀)) with hη_def + have hη (t : ℕ) : 0 < η t := div_pos hr (Real.sqrt_pos.mpr (hS_pos _ (le_max_right _ _))) + have hη_anti : Antitone η := fun s t hst ↦ + div_le_div_of_nonneg_left hr.le (Real.sqrt_pos.mpr (hS_pos _ (le_max_right _ _))) + (Real.sqrt_le_sqrt (hS_mono (max_le_max hst le_rfl))) + have ha' (t : ℕ) (ht : t < n) : + IsMirrorDescentStep K F (η t) (y t) (a t) (F' t) (a (t + 1)) := by + have h_step := ha t ht + rcases lt_or_ge t t₀ with htt | htt + · rw [hy_lt t htt] at h_step ⊢ + exact isMirrorDescentStep_zero_iff.mpr (isMirrorDescentStep_zero_iff.mp h_step) + · simp only [hη_def, max_eq_left htt, ← h_rate] + exact h_step + have h := mirrorDescent_regret_le_of_strongConvexOn_of_antitone hF hm hη hη_anti y a F' ha0K ha' + hF' hB.le hBu hu + -- the first term is `B √A / r`, and the stability terms add up to at most `r √A / m` + have h_first : B / η (n - 1) = B * √A / r := by + have hn : 0 < n := (Nat.zero_le t₀).trans_lt ht₀n + have hSn : S (n - 1) = A := by simp only [hS_def, hA_def, Nat.sub_add_cancel hn] + simp only [hη_def, max_eq_left (Nat.le_sub_one_of_lt ht₀n), hSn, div_div_eq_mul_div] + have h_term (t : ℕ) (ht : t ∈ range n) : + η t / (2 * m) * ‖y t‖ ^ 2 = r / (2 * m) * (‖y t‖ ^ 2 / √(S t)) := by + rcases lt_or_ge t t₀ with htt | htt + · simp [hy_lt t htt] + · simp only [hη_def, max_eq_left htt] + ring + have h_stab : ∑ t ∈ range n, η t / (2 * m) * ‖y t‖ ^ 2 ≤ r * √A / m := by + rw [sum_congr rfl h_term, ← mul_sum] + calc r / (2 * m) * ∑ t ∈ range n, ‖y t‖ ^ 2 / √(S t) ≤ r / (2 * m) * (2 * √A) := + mul_le_mul_of_nonneg_left (Real.sum_div_sqrt_le_two_mul_sqrt fun _ _ ↦ sq_nonneg _) + (by positivity) + _ = r * √A / m := by field_simp + -- and `B √A / r = r √A / m = √(B A / m)`, as `r ^ 2 = m B` + have h_B : B * √A / r = r * √A / m := by + rw [div_eq_div_iff hr.ne' hm.ne'] + linear_combination (-√A) * hr_sq + have h_sqrt : √(B * A / m) = r * √A / m := by + have hA : 0 ≤ A := sum_nonneg fun _ _ ↦ sq_nonneg _ + rw [show B * A / m = (r * √A / m) ^ 2 by + rw [div_pow, mul_pow, hr_sq, Real.sq_sqrt hA] + field_simp] + exact Real.sqrt_sq (by positivity) + rw [h_sqrt] + linarith + +/-- **Mirror descent with adaptive learning rates**, the form of [Ora, Theorem 4.14] for mirror +descent with a strongly convex potential. Let `F` be `m`-strongly +convex on `K`, with `m > 0`. Let `a 0 ∈ K` and let each `a (t + 1)`, for `t < n`, be a mirror +descent step on `K` from `a t` with derivative `F' t`, for the loss `y t` and the learning rate +`η t = √(m B / ∑ s ≤ t, ‖y s‖ ^ 2)`, where `F` has derivative `F' t` within `K` at `a t` for +`t ≤ n`. If `B` bounds the Bregman divergences `D_F(u, a t)` for `t < n`, then for every `u ∈ K`, +`∑ t < n, y t (a t - u) ≤ 2 √(B ∑ t < n, ‖y t‖ ^ 2 / m)`, +where `‖y t‖` is the dual norm. While the losses observed so far vanish, the learning rate is `0` +and the step is a Bregman projection of `a t`, so that the algorithm stays at `a t`. -/ +theorem mirrorDescent_regret_le_two_mul_sqrt {m B : ℝ} (hF : StrongConvexOn K m F) (hm : 0 < m) + (y : ℕ → E →L[ℝ] ℝ) (a : ℕ → E) (F' : ℕ → E →L[ℝ] ℝ) (ha0K : a 0 ∈ K) + (ha : ∀ t < n, IsMirrorDescentStep K F (√(m * B / ∑ s ∈ range (t + 1), ‖y s‖ ^ 2)) (y t) + (a t) (F' t) (a (t + 1))) + (hF' : ∀ t ≤ n, HasFDerivWithinAt F (F' t) K (a t)) + (hBu : ∀ t < n, bregDiv F u (a t) (F' t) ≤ B) (hu : u ∈ K) : + ∑ t ∈ range n, y t (a t - u) ≤ 2 * √(B * (∑ t ∈ range n, ‖y t‖ ^ 2) / m) := by + have h_mem := mem_of_isMirrorDescentStep ha0K ha + rcases n.eq_zero_or_pos with rfl | hn + · simp + -- `B ≥ 0`, as the Bregman divergences of a convex function are nonnegative + have hB : 0 ≤ B := ((hF' 0 hn.le).hasSubgradientWithinAt + (strongConvexOn_zero.mp (hF.mono hm.le)) ha0K u hu).trans (hBu 0 hn) + -- if every loss vanishes, so does the regret + by_cases hy : ∀ t < n, y t = 0 + · rw [sum_eq_zero fun t ht ↦ by simp [hy t (mem_range.mp ht)]] + positivity + push Not at hy + rcases hB.eq_or_lt with hB0 | hB0 + · -- if `B = 0`, every play is the comparator, by strong convexity + refine (sum_eq_zero fun t ht ↦ ?_).le.trans (by positivity) + have ht := mem_range.mp ht + have h_lower := hF.mul_norm_sub_sq_le_bregDiv (h_mem t ht.le) hu (hF' t ht.le) + have h_sq : ‖u - a t‖ ^ 2 = 0 := by nlinarith [hBu t ht, sq_nonneg ‖u - a t‖] + rw [sq_eq_zero_iff, norm_eq_zero, sub_eq_zero] at h_sq + simp [h_sq] + -- otherwise, let `t₀` be the first round with a nonzero loss + classical + refine mirrorDescent_regret_le_two_mul_sqrt_of_ne_zero hF hm hB0 y a F' ha0K + (Nat.find_spec hy).1 (Nat.find_spec hy).2 (fun t ht ↦ ?_) ha hF' hBu hu + by_contra h + exact Nat.find_min hy ht ⟨ht.trans (Nat.find_spec hy).1, h⟩ + +end NormedSpace + +section InnerProductSpace + +variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {K : Set E} {u : E} + +/-- **Projected online subgradient descent with adaptive learning rates** [Ora, Theorem 4.14]. +Let `K` be convex, and let `g t` be a subgradient of the loss `f t` within `K` at `a t`, for +`t < n`. Let `a 0 ∈ K` and let each `a (t + 1)` be a point of `K` nearest to `a t - η t • g t`, for +the learning rate `η t = D / √(2 ∑ s ≤ t, ‖g s‖ ^ 2)`. If `‖u - a t‖ ≤ D` for `t < n`, for +instance if `u ∈ K` and `K` has diameter at most `D`, then +`regret f a u n ≤ D √(2 ∑ t < n, ‖g t‖ ^ 2)`. +The learning rates need neither the horizon nor a bound on the subgradients. While the +subgradients observed so far vanish, the learning rate is `0` and the algorithm stays at `a t`. -/ +theorem onlineSubgradientDescent_regret_le_mul_sqrt_sum (hK : Convex ℝ K) {D : ℝ} + (f : ℕ → E → ℝ) (g a : ℕ → E) + (hg : ∀ t < n, HasSubgradientWithinAt (f t) (innerSL ℝ (g t)) K (a t)) (ha0 : a 0 ∈ K) + (ha : ∀ t < n, a (t + 1) ∈ K ∧ IsMinOn + (fun b ↦ ‖b - (a t - (D / √(2 * ∑ s ∈ range (t + 1), ‖g s‖ ^ 2)) • g t)‖) K (a (t + 1))) + (hD : ∀ t < n, ‖u - a t‖ ≤ D) (hu : u ∈ K) : + regret f a u n ≤ D * √(2 * ∑ t ∈ range n, ‖g t‖ ^ 2) := by + rcases n.eq_zero_or_pos with rfl | hn + · simp [regret_def] + have hD0 : 0 ≤ D := (norm_nonneg _).trans (hD 0 hn) + -- the learning rates are those of `mirrorDescent_regret_le_two_mul_sqrt` for the potential + -- `‖·‖ ^ 2 / 2`, with `m = 1` and `B = D ^ 2 / 2` + have h_rate (S : ℝ) (hS : 0 ≤ S) : √(1 * (D ^ 2 / 2) / S) = D / √(2 * S) := by + rw [show 1 * (D ^ 2 / 2) / S = D ^ 2 / (2 * S) by ring, Real.sqrt_div' _ (by positivity), + Real.sqrt_sq hD0] + have ha' (t : ℕ) (ht : t < n) : IsMirrorDescentStep K (fun b : E ↦ ‖b‖ ^ 2 / 2) + (√(1 * (D ^ 2 / 2) / ∑ s ∈ range (t + 1), ‖innerSL ℝ (g s)‖ ^ 2)) (innerSL ℝ (g t)) (a t) + (innerSL ℝ (a t)) (a (t + 1)) := by + simp only [innerSL_apply_norm] + rw [h_rate _ (sum_nonneg fun _ _ ↦ sq_nonneg _)] + exact isMirrorDescentStep_norm_sq_div_two_iff.mpr (ha t ht) + have hBu (t : ℕ) (ht : t < n) : + bregDiv (fun b : E ↦ ‖b‖ ^ 2 / 2) u (a t) (innerSL ℝ (a t)) ≤ D ^ 2 / 2 := by + rw [bregDiv_norm_sq_div_two] + gcongr + exact hD t ht + have h := mirrorDescent_regret_le_two_mul_sqrt (strongConvexOn_norm_sq_div_two hK) one_pos + (fun t ↦ innerSL ℝ (g t)) a (fun t ↦ innerSL ℝ (a t)) ha0 ha' + (fun t _ ↦ (hasFDerivAt_norm_sq_div_two _).hasFDerivWithinAt) hBu hu + simp only [innerSL_apply_norm] at h + rw [regret_def] + refine (sum_sub_le_sum_apply_sub_of_hasSubgradientWithinAt f _ a hg hu).trans (h.trans_eq ?_) + rw [div_one, show D ^ 2 / 2 * ∑ t ∈ range n, ‖g t‖ ^ 2 = + (D / 2) ^ 2 * (2 * ∑ t ∈ range n, ‖g t‖ ^ 2) by ring, Real.sqrt_mul (sq_nonneg _), + Real.sqrt_sq (by positivity)] + ring + +/-- **The `L⋆` bound of projected online subgradient descent** [Ora, Theorem 4.30]. Under the +assumptions of `onlineSubgradientDescent_regret_le_mul_sqrt_sum`, if moreover the subgradients +satisfy `‖g t‖ ^ 2 ≤ 2 s f t (a t)` for `t < n`, then +`regret f a u n ≤ 4 s D ^ 2 + 2 D √(s ∑ t < n, f t u)`. +The bound depends on the cumulative loss of the comparator, and not on the number of rounds. -/ +theorem onlineSubgradientDescent_regret_le_of_norm_sq_le (hK : Convex ℝ K) {D : ℝ} {s : ℝ≥0} + (f : ℕ → E → ℝ) (g a : ℕ → E) + (hg : ∀ t < n, HasSubgradientWithinAt (f t) (innerSL ℝ (g t)) K (a t)) + (hgf : ∀ t < n, ‖g t‖ ^ 2 ≤ 2 * s * f t (a t)) (ha0 : a 0 ∈ K) + (ha : ∀ t < n, a (t + 1) ∈ K ∧ IsMinOn + (fun b ↦ ‖b - (a t - (D / √(2 * ∑ s ∈ range (t + 1), ‖g s‖ ^ 2)) • g t)‖) K (a (t + 1))) + (hD : ∀ t < n, ‖u - a t‖ ≤ D) (hu : u ∈ K) : + regret f a u n ≤ 4 * s * D ^ 2 + 2 * D * √(s * ∑ t ∈ range n, f t u) := by + rcases n.eq_zero_or_pos with rfl | hn + · simp only [regret_def, range_zero, sum_empty, mul_zero, Real.sqrt_zero, add_zero] + positivity + have hD0 : 0 ≤ D := (norm_nonneg _).trans (hD 0 hn) + set L := ∑ t ∈ range n, f t (a t) + set U := ∑ t ∈ range n, f t u + have h_reg : regret f a u n = L - U := by rw [regret_def, sum_sub_distrib] + have h := onlineSubgradientDescent_regret_le_mul_sqrt_sum hK f g a hg ha0 ha hD hu + -- the squared subgradients add up to at most `2 s L`, so that `L - U ≤ √(4 s D ^ 2 L)` + have h_sum : 2 * ∑ t ∈ range n, ‖g t‖ ^ 2 ≤ 4 * s * L := by + have := sum_le_sum fun t ht ↦ hgf t (mem_range.mp ht) + rw [← mul_sum] at this + linarith + have h_imp : L - √(4 * s * D ^ 2 * L + 0) ≤ U := by + have h_le : D * √(2 * ∑ t ∈ range n, ‖g t‖ ^ 2) ≤ √(4 * s * D ^ 2 * L + 0) := by + rw [add_zero, show 4 * s * D ^ 2 * L = D ^ 2 * (4 * s * L) by ring, + Real.sqrt_mul (sq_nonneg _), Real.sqrt_sq hD0] + exact mul_le_mul_of_nonneg_left (Real.sqrt_le_sqrt h_sum) hD0 + linarith + -- solving for `L` gives `L ≤ 4 s D ^ 2 + U + √(4 s D ^ 2 U)` + have h_sol := Real.le_add_add_sqrt_of_sub_sqrt_le (by positivity) h_imp + rw [zero_add, show 4 * s * D ^ 2 * U = (2 * D) ^ 2 * (s * U) by ring, + Real.sqrt_mul (sq_nonneg _), Real.sqrt_sq (by positivity)] at h_sol + rw [h_reg] + linarith + +/-- **The `L⋆` bound for self-bounded losses** [Ora, Theorem 4.30]. Let `K` be convex, and let the +losses `f t` be nonnegative and `s`-self-bounded within `K`, with a subgradient `g t` within `K` +at `a t`, for `t < n`. Let `a 0 ∈ K` and let each `a (t + 1)` be a point of `K` nearest to +`a t - η t • g t`, for the learning rate `η t = D / √(2 ∑ s ≤ t, ‖g s‖ ^ 2)`. If `u ∈ K` and +`‖u - a t‖ ≤ D` for `t < n`, as on a set of diameter at most `D`, then +`regret f a u n ≤ 4 s D ^ 2 + 2 D √(s ∑ t < n, f t u)`. -/ +theorem onlineSubgradientDescent_regret_le_of_selfBoundedOn (hK : Convex ℝ K) {D : ℝ} + {s : ℝ≥0} (f : ℕ → E → ℝ) (g a : ℕ → E) + (hf : ∀ t < n, SelfBoundedOn K s (f t)) (hf0 : ∀ t < n, ∀ x ∈ K, 0 ≤ f t x) + (hg : ∀ t < n, HasSubgradientWithinAt (f t) (innerSL ℝ (g t)) K (a t)) (ha0 : a 0 ∈ K) + (ha : ∀ t < n, a (t + 1) ∈ K ∧ IsMinOn + (fun b ↦ ‖b - (a t - (D / √(2 * ∑ s ∈ range (t + 1), ‖g s‖ ^ 2)) • g t)‖) K (a (t + 1))) + (hD : ∀ t < n, ‖u - a t‖ ≤ D) (hu : u ∈ K) : + regret f a u n ≤ 4 * s * D ^ 2 + 2 * D * √(s * ∑ t ∈ range n, f t u) := by + have h_mem := mem_of_isMirrorDescentStep (η := fun t ↦ D / √(2 * ∑ s ∈ range (t + 1), ‖g s‖ ^ 2)) + ha0 fun t ht ↦ isMirrorDescentStep_norm_sq_div_two_iff.mpr (ha t ht) + refine onlineSubgradientDescent_regret_le_of_norm_sq_le hK f g a hg (fun t ht ↦ ?_) ha0 ha hD hu + have := (hf t ht).norm_sq_le_of_nonneg (hf0 t ht) (h_mem t ht.le) (hg t ht) + rwa [innerSL_apply_norm] at this + +end InnerProductSpace + +end LMLExplore.OnlineLearning diff --git a/LMLExplore/OnlineLearning/MirrorDescent.lean b/LMLExplore/OnlineLearning/MirrorDescent.lean index e14ba9cd..d9e8ee4f 100644 --- a/LMLExplore/OnlineLearning/MirrorDescent.lean +++ b/LMLExplore/OnlineLearning/MirrorDescent.lean @@ -40,6 +40,8 @@ of losses, in particular for losses chosen adaptively from the past plays. ## Main statements +* `isMirrorDescentStep_zero_iff`: a step for the zero loss is a Bregman projection of the + current play, whatever the learning rate. * `isMirrorDescentStep_iff_isMinOn_bregDiv`: the second stage of the two-step form [LS, (28.8)]. If `G = F' - η y`, the steps from `a` are the Bregman projections onto `K` of any point `b` with derivative `G`. @@ -111,6 +113,13 @@ structure IsMirrorDescentStep (K : Set E) (F : E → ℝ) (η : ℝ) (y : E →L /-- The step minimizes the mirror descent objective over `K`. -/ isMinOn : IsMinOn (fun b ↦ η * y b + bregDiv F b a F') K x +/-- A mirror descent step for the zero loss is a Bregman projection of `a` onto `K`, whatever the +learning rate: a point of `K` minimizing `b ↦ D_F(b, a)` over `K`. -/ +@[simp] +theorem isMirrorDescentStep_zero_iff {a x : E} {F' : E →L[ℝ] ℝ} : + IsMirrorDescentStep K F η 0 a F' x ↔ x ∈ K ∧ IsMinOn (fun b ↦ bregDiv F b a F') K x := + ⟨fun h ↦ ⟨h.mem, by simpa using h.isMinOn⟩, fun ⟨hx, h⟩ ↦ ⟨hx, by simpa using h⟩⟩ + section TwoStep variable {y F' G : E →L[ℝ] ℝ} From 00415001ffadba9a6e5e0fc1476e2abcf939928d Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 09:58:35 +0100 Subject: [PATCH 2/3] refactor: reuse the two-step lemma and split the rate arithmetic MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Prove `isMirrorDescentStep_zero_iff` as an instance of `isMirrorDescentStep_iff_isMinOn_bregDiv` (moved after the `TwoStep` section), and move the closing identity `B √A / r + r √A / m = 2 √(B A / m)` of `mirrorDescent_regret_le_two_mul_sqrt_of_ne_zero` into a private lemma. Co-Authored-By: Claude Code --- LMLExplore/OnlineLearning/AdaptiveRate.lean | 29 ++++++++++++-------- LMLExplore/OnlineLearning/MirrorDescent.lean | 18 ++++++------ 2 files changed, 26 insertions(+), 21 deletions(-) diff --git a/LMLExplore/OnlineLearning/AdaptiveRate.lean b/LMLExplore/OnlineLearning/AdaptiveRate.lean index 037d2077..adf8a77d 100644 --- a/LMLExplore/OnlineLearning/AdaptiveRate.lean +++ b/LMLExplore/OnlineLearning/AdaptiveRate.lean @@ -64,6 +64,22 @@ section NormedSpace variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {K : Set E} {F : E → ℝ} {u : E} +/-- The two terms of the regret bound balance at the adaptive learning rates: if `r ^ 2 = m B`, +then `B √A / r + r √A / m = 2 √(B A / m)`. -/ +private lemma mul_sqrt_div_add_mul_sqrt_div_eq {r m B A : ℝ} (hr : 0 < r) (hm : 0 < m) + (hr_sq : r ^ 2 = m * B) (hA : 0 ≤ A) : + B * √A / r + r * √A / m = 2 * √(B * A / m) := by + have h_B : B * √A / r = r * √A / m := by + rw [div_eq_div_iff hr.ne' hm.ne'] + linear_combination (-√A) * hr_sq + have h_sqrt : √(B * A / m) = r * √A / m := by + rw [show B * A / m = (r * √A / m) ^ 2 by + rw [div_pow, mul_pow, hr_sq, Real.sq_sqrt hA] + field_simp] + exact Real.sqrt_sq (by positivity) + rw [h_B, h_sqrt] + ring + /-- The case of `mirrorDescent_regret_le_two_mul_sqrt` with `B > 0` and a first round `t₀ < n` with a nonzero loss. From `t₀` on, the adaptive learning rates are positive and nonincreasing; before `t₀` the losses vanish, so that the steps are also steps for the learning rate of `t₀`, @@ -123,18 +139,7 @@ private theorem mirrorDescent_regret_le_two_mul_sqrt_of_ne_zero {m B : ℝ} mul_le_mul_of_nonneg_left (Real.sum_div_sqrt_le_two_mul_sqrt fun _ _ ↦ sq_nonneg _) (by positivity) _ = r * √A / m := by field_simp - -- and `B √A / r = r √A / m = √(B A / m)`, as `r ^ 2 = m B` - have h_B : B * √A / r = r * √A / m := by - rw [div_eq_div_iff hr.ne' hm.ne'] - linear_combination (-√A) * hr_sq - have h_sqrt : √(B * A / m) = r * √A / m := by - have hA : 0 ≤ A := sum_nonneg fun _ _ ↦ sq_nonneg _ - rw [show B * A / m = (r * √A / m) ^ 2 by - rw [div_pow, mul_pow, hr_sq, Real.sq_sqrt hA] - field_simp] - exact Real.sqrt_sq (by positivity) - rw [h_sqrt] - linarith + linarith [mul_sqrt_div_add_mul_sqrt_div_eq hr hm hr_sq (sum_nonneg fun _ _ ↦ sq_nonneg _ : 0 ≤ A)] /-- **Mirror descent with adaptive learning rates**, the form of [Ora, Theorem 4.14] for mirror descent with a strongly convex potential. Let `F` be `m`-strongly diff --git a/LMLExplore/OnlineLearning/MirrorDescent.lean b/LMLExplore/OnlineLearning/MirrorDescent.lean index d9e8ee4f..b7e3fcbc 100644 --- a/LMLExplore/OnlineLearning/MirrorDescent.lean +++ b/LMLExplore/OnlineLearning/MirrorDescent.lean @@ -40,14 +40,14 @@ of losses, in particular for losses chosen adaptively from the past plays. ## Main statements -* `isMirrorDescentStep_zero_iff`: a step for the zero loss is a Bregman projection of the - current play, whatever the learning rate. * `isMirrorDescentStep_iff_isMinOn_bregDiv`: the second stage of the two-step form [LS, (28.8)]. If `G = F' - η y`, the steps from `a` are the Bregman projections onto `K` of any point `b` with derivative `G`. * `isMinOn_mul_apply_add_bregDiv_of_hasFDerivWithinAt`: the first stage [LS, (28.7), (28.9)]. For `F` convex on `D`, a point `b ∈ D` where `F` has derivative `F' - η y` minimizes the objective of the step over `D`. +* `isMirrorDescentStep_zero_iff`: a step for the zero loss is a Bregman projection of the + current play, whatever the learning rate. * `exists_isMirrorDescentStep`: on a nonempty compact set, with a potential continuous on it, mirror descent steps exist. * `exists_isMirrorDescentStep_of_strongConvexOn`: in finite dimension, on a nonempty closed set @@ -113,13 +113,6 @@ structure IsMirrorDescentStep (K : Set E) (F : E → ℝ) (η : ℝ) (y : E →L /-- The step minimizes the mirror descent objective over `K`. -/ isMinOn : IsMinOn (fun b ↦ η * y b + bregDiv F b a F') K x -/-- A mirror descent step for the zero loss is a Bregman projection of `a` onto `K`, whatever the -learning rate: a point of `K` minimizing `b ↦ D_F(b, a)` over `K`. -/ -@[simp] -theorem isMirrorDescentStep_zero_iff {a x : E} {F' : E →L[ℝ] ℝ} : - IsMirrorDescentStep K F η 0 a F' x ↔ x ∈ K ∧ IsMinOn (fun b ↦ bregDiv F b a F') K x := - ⟨fun h ↦ ⟨h.mem, by simpa using h.isMinOn⟩, fun ⟨hx, h⟩ ↦ ⟨hx, by simpa using h⟩⟩ - section TwoStep variable {y F' G : E →L[ℝ] ℝ} @@ -160,6 +153,13 @@ theorem isMinOn_mul_apply_add_bregDiv_of_hasFDerivWithinAt (hG : G = F' - η • end TwoStep +/-- A mirror descent step for the zero loss is a Bregman projection of `a` onto `K`, whatever the +learning rate: a point of `K` minimizing `b ↦ D_F(b, a)` over `K`. -/ +@[simp] +theorem isMirrorDescentStep_zero_iff {a x : E} {F' : E →L[ℝ] ℝ} : + IsMirrorDescentStep K F η 0 a F' x ↔ x ∈ K ∧ IsMinOn (fun b ↦ bregDiv F b a F') K x := + isMirrorDescentStep_iff_isMinOn_bregDiv (by simp) a a x + /-- **The stability term is largest at the unconstrained step.** Let `F` be convex on `D`, let `η > 0`, and let `x ∈ D` be a point where `F` has derivative `J - η y` within `D`. Then for every `b ∈ D`, `y (a - b) - D_F(b, a) / η ≤ y (a - x) - D_F(x, a) / η`, where the Bregman divergences From 19077557a1de67b0fc5f49d7a1efeb5d4959374e Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 10:32:28 +0100 Subject: [PATCH 3/3] =?UTF-8?q?refactor:=20reuse=20Real.sqrt=5Fsq=5Fmul=20?= =?UTF-8?q?and=20sInf=5Frange=20in=20the=20L=E2=8B=86=20proofs?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Rewrite `√(c ^ 2 * X)` with Tau Ceti's `Real.sqrt_sq_mul` instead of the repeated `sqrt_mul`/`sqrt_sq` chain, and close `SmoothOn.selfBoundedOn_univ` through `sInf_range` rather than the definitional unfolding of `iInf`. Co-Authored-By: Claude Code --- LMLExplore/Analysis/Convex/Smooth.lean | 3 +-- LMLExplore/OnlineLearning/AdaptiveRate.lean | 9 +++++---- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/LMLExplore/Analysis/Convex/Smooth.lean b/LMLExplore/Analysis/Convex/Smooth.lean index 814459af..51aaa054 100644 --- a/LMLExplore/Analysis/Convex/Smooth.lean +++ b/LMLExplore/Analysis/Convex/Smooth.lean @@ -285,8 +285,7 @@ theorem SmoothOn.selfBoundedOn_univ {f : E → ℝ} (hf : SmoothOn univ s f) bddBelow := by rwa [image_univ] norm_sq_le x _ g hg := by rw [(hf.differentiableAt (mem_univ x)).hasFDerivAt.eq_of_hasSubgradientWithinAt - Filter.univ_mem hg, image_univ] - -- `⨅ y, f y` is by definition `sInf (range f)` + Filter.univ_mem hg, image_univ, sInf_range] exact hf.norm_fderiv_sq_le hbdd x end LMLExplore diff --git a/LMLExplore/OnlineLearning/AdaptiveRate.lean b/LMLExplore/OnlineLearning/AdaptiveRate.lean index adf8a77d..06211d30 100644 --- a/LMLExplore/OnlineLearning/AdaptiveRate.lean +++ b/LMLExplore/OnlineLearning/AdaptiveRate.lean @@ -8,6 +8,7 @@ module public import LMLExplore.Analysis.Convex.Smooth public import LMLExplore.Analysis.SumIntegralComparisons public import LMLExplore.OnlineLearning.SubgradientDescent +import TauCeti.Analysis.Real.Sqrt /-! # Adaptive learning rates and `L⋆` bounds @@ -230,8 +231,8 @@ theorem onlineSubgradientDescent_regret_le_mul_sqrt_sum (hK : Convex ℝ K) {D : rw [regret_def] refine (sum_sub_le_sum_apply_sub_of_hasSubgradientWithinAt f _ a hg hu).trans (h.trans_eq ?_) rw [div_one, show D ^ 2 / 2 * ∑ t ∈ range n, ‖g t‖ ^ 2 = - (D / 2) ^ 2 * (2 * ∑ t ∈ range n, ‖g t‖ ^ 2) by ring, Real.sqrt_mul (sq_nonneg _), - Real.sqrt_sq (by positivity)] + (D / 2) ^ 2 * (2 * ∑ t ∈ range n, ‖g t‖ ^ 2) by ring, Real.sqrt_sq_mul, + abs_of_nonneg (by positivity)] ring /-- **The `L⋆` bound of projected online subgradient descent** [Ora, Theorem 4.30]. Under the @@ -263,13 +264,13 @@ theorem onlineSubgradientDescent_regret_le_of_norm_sq_le (hK : Convex ℝ K) {D have h_imp : L - √(4 * s * D ^ 2 * L + 0) ≤ U := by have h_le : D * √(2 * ∑ t ∈ range n, ‖g t‖ ^ 2) ≤ √(4 * s * D ^ 2 * L + 0) := by rw [add_zero, show 4 * s * D ^ 2 * L = D ^ 2 * (4 * s * L) by ring, - Real.sqrt_mul (sq_nonneg _), Real.sqrt_sq hD0] + Real.sqrt_sq_mul, abs_of_nonneg hD0] exact mul_le_mul_of_nonneg_left (Real.sqrt_le_sqrt h_sum) hD0 linarith -- solving for `L` gives `L ≤ 4 s D ^ 2 + U + √(4 s D ^ 2 U)` have h_sol := Real.le_add_add_sqrt_of_sub_sqrt_le (by positivity) h_imp rw [zero_add, show 4 * s * D ^ 2 * U = (2 * D) ^ 2 * (s * U) by ring, - Real.sqrt_mul (sq_nonneg _), Real.sqrt_sq (by positivity)] at h_sol + Real.sqrt_sq_mul, abs_of_nonneg (by positivity)] at h_sol rw [h_reg] linarith