Gradient Descent: Linear Convergence from Strong Monotonicity + Lipschitz Gradient

This file is a small, “real” optimization-theory module:

It proves a linear convergence bound for the iteration

$$ x_{k+1}=x_k-\eta g(x_k) $$

under two assumptions on g over a real inner product space:

1. $g$ is $\mu$-strongly monotone: $\mu\lVert x-y\rVert^2 \leq \langle x-y, g(x)-g(y)\rangle$.
2. $g$ is $L$-Lipschitz: $\lVert g(x)-g(y)\rVert \leq L\lVert x-y\rVert$.

For gradients of $\mu$-strongly convex and $L$-smooth functions, these are the standard operator-level properties that imply linear convergence of gradient descent with a suitable step size.

This module avoids any heavy Fréchet-derivative setup: it is stated directly in terms of $g$ so it can later be instantiated either by $g=\nabla f$ theorems or by verified gradients of concrete TorchLean models.

def Optim.GD.StrongMonotone {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (μ : ℝ) (g : E → E) : Prop

Strong monotonicity of an operator in a real inner product space.

def Optim.GD.step {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (η : ℝ) (g : E → E) (x : E) : E

One gradient-descent-like step for an operator g.

theorem Optim.GD.step_sub_step {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (η : ℝ) (g : E → E) (x y : E) : step η g x - step η g y = x - y - η • (g x - g y)

Expand the difference of two step applications.

theorem Optim.GD.step_norm_sq_le {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (η μ : ℝ) (hη : 0 ≤ η) {L : NNReal} (g : E → E) (hmono : StrongMonotone μ g) (hlip : LipschitzWith L g) (x y : E) : ‖step η g x - step η g y‖ ^ 2 ≤ (1 - 2 * η * μ + η ^ 2 * ↑L ^ 2) * ‖x - y‖ ^ 2

Key contraction-in-squared-norm inequality.

If $g$ is $\mu$-strongly monotone and $L$-Lipschitz, then $$ \lVert \operatorname{step}_\eta(g,x)-\operatorname{step}_\eta(g,y)\rVert^2 \leq q\lVert x-y\rVert^2, \qquad q=1-2\eta\mu+\eta^2L^2. $$