Strong Convexity and Strongly Monotone Gradients

TorchLean's GD convergence theorems are stated at the operator level:

• $g$ is $\mu$-strongly monotone, and
• $g$ is $L$-Lipschitz.

To apply them to gradient descent on an objective $f$, we need to instantiate $g=\nabla f$.

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

This file provides the key local bridge lemma:

If $f$ satisfies the first-order strong convexity inequality (using the gradient), then $\nabla f$ is $\mu$-strongly monotone in the sense needed by GDLinearConvergence.

This file provides a concrete bridge from mathlib's StrongConvexOn definition to a first-order inequality, under a DifferentiableAt assumption at the base point x.

The pointwise theorem gives the first-order inequality at one differentiability point. To obtain global strong monotonicity, the first-order inequality must hold at every base point. A strong-convexity hypothesis together with differentiability everywhere provides that global premise.

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. The closing theorem dist_sq_iterate_le_of_firstOrderStrongConvex assembles the pieces that are proved: first-order strong convexity gives strong monotonicity of ∇ f, and together with an assumed Lipschitz gradient and a step-size condition this yields linear convergence of gradient descent to a critical point.

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