Strong Convexity and Strongly Monotone Gradients

TorchLean's GD convergence theorems are stated at the operator level: $g$ is $\mu$-strongly monotone and $L$-Lipschitz. To apply them to gradient descent on an objective $f$, we instantiate $g=\nabla f$.

Mathlib's gradient f x is total (it returns $0$ if the derivative does not exist), so we assume differentiability and reason through the standard first-order characterization of strong convexity.

Main results:

• firstOrderStrongConvexAt_of_strongConvexOn_univ: StrongConvexOn univ μ f plus differentiability at x gives the first-order inequality at x;
• firstOrderStrongConvex_of_strongConvexOn_univ: with differentiability everywhere, the global first-order premise FirstOrderStrongConvex μ f;
• strongMonotone_gradient_of_firstOrderStrongConvex: the first-order inequality makes ∇ f $\mu$-strongly monotone, which is the hypothesis of GD.step_norm_sq_le;
• dist_sq_iterate_le_of_firstOrderStrongConvex and dist_sq_iterate_le_of_strongConvexOn: linear convergence of gradient descent to a critical point, assuming in addition that ∇ f is Lipschitz.

The smoothness half is not proved here. Nothing in this file derives LipschitzWith L (∇ f) from a second-order or fderiv-level smoothness hypothesis on f; the Lipschitz gradient is taken as an explicit assumption.

def Optim.GD.FirstOrderStrongConvex {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (μ : ℝ) (f : E → ℝ) : Prop

First-order strong convexity with parameter $\mu$, stated using the gradient.

This is the familiar inequality:

$$ f(y)\geq f(x)+\langle\nabla f(x),y-x\rangle +\frac{\mu}{2}\lVert y-x\rVert^2. $$

It is a standard characterization of $\mu$-strong convexity for differentiable functions on Euclidean/Hilbert spaces.

def Optim.GD.FirstOrderStrongConvexAt {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (μ : ℝ) (f : E → ℝ) (x : E) : Prop

First-order strong convexity at a fixed base point x.

This is the same inequality as FirstOrderStrongConvex, but quantified only over $y$. It is the natural statement you get from convex analysis under a DifferentiableAt hypothesis at $x$.

theorem Optim.GD.firstOrderStrongConvexAt_of_strongConvexOn_univ {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (μ : ℝ) {f : E → ℝ} (hsc : StrongConvexOn Set.univ μ f) {x : E} (hdx : DifferentiableAt ℝ f x) : FirstOrderStrongConvexAt μ f x

StrongConvexOn univ μ f plus differentiability at $x$ implies the first-order strong convexity inequality at $x$.

This is the standard convex-analysis “supporting hyperplane” argument applied to $g(z)=f(z)-(\mu/2)\lVert z\rVert^2$, which is convex when $f$ is strongly convex.

theorem Optim.GD.firstOrderStrongConvex_of_strongConvexOn_univ {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (μ : ℝ) {f : E → ℝ} (hsc : StrongConvexOn Set.univ μ f) (hd : Differentiable ℝ f) : FirstOrderStrongConvex μ f

StrongConvexOn univ μ f plus differentiability everywhere gives the global first-order strong convexity inequality, i.e. the premise of strongMonotone_gradient_of_firstOrderStrongConvex.

theorem Optim.GD.strongMonotone_gradient_of_firstOrderStrongConvex {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (μ : ℝ) {f : E → ℝ} (h : FirstOrderStrongConvex μ f) : StrongMonotone μ fun (x : E) => gradient f x

FirstOrderStrongConvex implies the gradient is $\mu$-strongly monotone.

This is the exact operator-side fact needed to use GD.step_norm_sq_le with $g=\nabla f$.

theorem Optim.GD.dist_sq_iterate_le_of_firstOrderStrongConvex {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (η μ : ℝ) {L : NNReal} {f : E → ℝ} (hsc : FirstOrderStrongConvex μ f) (hlip : LipschitzWith L fun (x : E) => gradient f x) {xStar x : E} (hxStar : gradient f xStar = 0) (hμ : 0 ≤ μ) (hμL : μ ≤ ↑L) (hη : 0 < η) (hstep : η * ↑L ^ 2 < 2 * μ) (k : ℕ) : ‖(step η fun (x : E) => gradient f x)^[k] x - xStar‖ ^ 2 ≤ q η μ L ^ k * ‖x - xStar‖ ^ 2 ∧ q η μ L < 1

Linear convergence of gradient descent on a first-order strongly convex objective whose gradient is assumed L-Lipschitz.

With 0 ≤ μ ≤ L, 0 < η, η * L ^ 2 < 2 * μ, and a critical point xStar of f, the iterates of step η (∇ f) satisfy the geometric bound with factor q η μ L < 1. The Lipschitz hypothesis on ∇ f is not derived from smoothness of f in this repository; it must be supplied.

theorem Optim.GD.dist_sq_iterate_le_of_strongConvexOn {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (η μ : ℝ) {L : NNReal} {f : E → ℝ} (hsc : StrongConvexOn Set.univ μ f) (hd : Differentiable ℝ f) (hlip : LipschitzWith L fun (x : E) => gradient f x) {xStar x : E} (hxStar : gradient f xStar = 0) (hμ : 0 ≤ μ) (hμL : μ ≤ ↑L) (hη : 0 < η) (hstep : η * ↑L ^ 2 < 2 * μ) (k : ℕ) : ‖(step η fun (x : E) => gradient f x)^[k] x - xStar‖ ^ 2 ≤ q η μ L ^ k * ‖x - xStar‖ ^ 2 ∧ q η μ L < 1

Linear convergence of gradient descent for a differentiable StrongConvexOn univ μ f objective whose gradient is assumed L-Lipschitz; see dist_sq_iterate_le_of_firstOrderStrongConvex for the step-size regime.