Gradient Descent Linear Convergence (Operator Form)

This file contains reusable gradient-descent convergence theorems.

The main theorems are stated for an operator $g:E\to E$ on a real inner product space. This is the right abstraction boundary for TorchLean:

If $g$ is

• $\mu$-strongly monotone (a.k.a. $\mu$-strongly accretive), and
• L-Lipschitz,

then the fixed-point iteration

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

contracts distances to any root $x^\star$ of $g$, i.e. a point with $g(x^\star)=0$.

For gradients, the usual instantiation is $g=\nabla f$. When $f$ is $\mu$-strongly convex and $L$-smooth, $\nabla f$ is $\mu$-strongly monotone and $L$-Lipschitz. Of these two facts, SmoothStrongConvexBridge proves the strong-monotonicity half from first-order strong convexity; the Lipschitz half is taken as a hypothesis there. This file focuses on the convergence argument itself, keeping the assumptions minimal and reusable. The step-size lemmas at the end of the GD namespace show when the contraction factor q lies in [0, 1).

The final ScalarGD namespace keeps the one-dimensional quadratic facts as a compact reference case: they show the same contraction mechanism in the smallest possible setting and connect plain SGD, L2 regularization, and decoupled weight decay algebraically.

def Optim.GD.q (η μ : ℝ) (L : NNReal) : ℝ

The squared-distance contraction factor from step_norm_sq_le.

theorem Optim.GD.step_dist_sq_le {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (η μ : ℝ) (hη : 0 ≤ η) {L : NNReal} (g : E → E) (hmono : StrongMonotone μ g) (hlip : LipschitzWith L g) {xStar x : E} (hxStar : g xStar = 0) : ‖step η g x - xStar‖ ^ 2 ≤ q η μ L * ‖x - xStar‖ ^ 2

One-step contraction of the squared distance to a root xStar of g.

theorem Optim.GD.dist_sq_iterate_le_of_q_nonneg {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (η μ : ℝ) (hη : 0 ≤ η) {L : NNReal} (g : E → E) (hmono : StrongMonotone μ g) (hlip : LipschitzWith L g) {xStar x : E} (hxStar : g xStar = 0) (hq : 0 ≤ q η μ L) (k : ℕ) : ‖(step η g)^[k] x - xStar‖ ^ 2 ≤ q η μ L ^ k * ‖x - xStar‖ ^ 2

Iterated contraction bound in squared norm.

If $q(\eta,\mu,L)\geq 0$, then after $k$ steps we have

$$ \left\lVert \operatorname{step}_\eta(g)^{\,k}(x)-x^\star\right\rVert^2 \leq q(\eta,\mu,L)^k\lVert x-x^\star\rVert^2. $$

theorem Optim.GD.dist_sq_iterate_le_of_q_lt_one {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (η μ : ℝ) (hη : 0 ≤ η) {L : NNReal} (g : E → E) (hmono : StrongMonotone μ g) (hlip : LipschitzWith L g) {xStar x : E} (hxStar : g xStar = 0) (hq : 0 ≤ q η μ L) (_hq1 : q η μ L < 1) (k : ℕ) : ‖(step η g)^[k] x - xStar‖ ^ 2 ≤ q η μ L ^ k * ‖x - xStar‖ ^ 2

Linear convergence: the squared distance to a root of g decays like q ^ k.

This is dist_sq_iterate_le_of_q_nonneg restated for the regime 0 ≤ q < 1. The extra hypothesis q < 1 is what makes the right-hand side shrink geometrically in k; it is not used by the proof, which is the same iterated contraction. Use q_lt_one_of_mul_sq_lt and q_nonneg_of_le to discharge the two hypotheses on q from a step-size condition.

theorem Optim.GD.q_lt_one_of_mul_sq_lt (η μ : ℝ) (L : NNReal) (hη : 0 < η) (hstep : η * ↑L ^ 2 < 2 * μ) : q η μ L < 1

The contraction factor is strictly below one when 0 < η and η * L ^ 2 < 2 * μ.

Since q - 1 = η * (η * L ^ 2 - 2 * μ), this is exactly the condition for q < 1 once η > 0. For L > 0 it reads η < 2 * μ / L ^ 2; see q_lt_one_of_lt_div.

theorem Optim.GD.q_lt_one_of_lt_div (η μ : ℝ) (L : NNReal) (hL : 0 < ↑L) (hη : 0 < η) (hstep : η < 2 * μ / ↑L ^ 2) : q η μ L < 1

Step-size form of q_lt_one_of_mul_sq_lt: for L > 0, any η with 0 < η < 2 * μ / L ^ 2 gives q η μ L < 1.

theorem Optim.GD.q_nonneg_of_le (η μ : ℝ) (L : NNReal) (hμ : 0 ≤ μ) (hμL : μ ≤ ↑L) : 0 ≤ q η μ L

The contraction factor is nonnegative whenever 0 ≤ μ ≤ L.

This follows from the identity q = (1 - η * μ) ^ 2 + η ^ 2 * (L ^ 2 - μ ^ 2), in which both summands are nonnegative. No sign condition on η is needed.

theorem Optim.GD.StrongMonotone.le_lipschitz {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {μ : ℝ} {L : NNReal} {g : E → E} (hmono : StrongMonotone μ g) (hlip : LipschitzWith L g) {x y : E} (hxy : x ≠ y) : μ ≤ ↑L

A strongly monotone and Lipschitz operator on a space with two distinct points has μ ≤ L.

This is the usual observation that the strong-monotonicity constant can never exceed the Lipschitz constant; it lets q_nonneg_of_le be applied without assuming μ ≤ L separately.

theorem Optim.GD.dist_sq_iterate_le_of_step_size {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (η μ : ℝ) {L : NNReal} (g : E → E) (hmono : StrongMonotone μ g) (hlip : LipschitzWith L g) {xStar x : E} (hxStar : g xStar = 0) (hμ : 0 ≤ μ) (hμL : μ ≤ ↑L) (hη : 0 < η) (hstep : η * ↑L ^ 2 < 2 * μ) (k : ℕ) : ‖(step η g)^[k] x - xStar‖ ^ 2 ≤ q η μ L ^ k * ‖x - xStar‖ ^ 2 ∧ q η μ L < 1

Linear convergence of gradient descent under an explicit step-size condition.

Assuming 0 ≤ μ ≤ L, 0 < η, and η * L ^ 2 < 2 * μ, the contraction factor satisfies 0 ≤ q η μ L < 1 and the iterates converge linearly to any root xStar of g.

theorem Optim.GD.tendsto_iterate_of_q_lt_one {E : Type} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (η μ : ℝ) (hη : 0 ≤ η) {L : NNReal} (g : E → E) (hmono : StrongMonotone μ g) (hlip : LipschitzWith L g) {xStar x : E} (hxStar : g xStar = 0) (hq : 0 ≤ q η μ L) (hq1 : q η μ L < 1) : Filter.Tendsto (fun (k : ℕ) => (step η g)^[k] x) Filter.atTop (nhds xStar)

Gradient-descent iterates tend to a supplied root when the squared-distance factor lies in [0, 1). No completeness assumption is needed: the limit is already given.

Scalar quadratic warm-up

These facts are compact but not merely definitional. They prove algebraic behavior of gradient descent on the one-dimensional quadratic objective

$$ L(x)=\frac12(x-\mathrm{target})^2, $$

whose gradient is $x-\mathrm{target}$. This is the simplest executable bridge from TorchLean's optimizer equations to familiar convergence facts; the Hilbert-space operator theorem above is the reusable version for tensor/vector models.

def Optim.ScalarGD.quadraticGrad {α : Type} [Sub α] (target x : α) : α

Gradient of $\frac12(x-\mathrm{target})^2$.

def Optim.ScalarGD.step {α : Type} [Sub α] [Mul α] (lr target x : α) : α

One scalar gradient-descent step on the quadratic objective.

theorem Optim.ScalarGD.target_fixed {α : Type} [CommRing α] (lr target : α) : step lr target target = target

The optimum is a fixed point of the scalar quadratic gradient-descent update.

theorem Optim.ScalarGD.error_after_step {α : Type} [CommRing α] (lr target x : α) : step lr target x - target = (1 - lr) * (x - target)

One scalar quadratic gradient-descent step multiplies the current error by $1-\mathrm{lr}$.

For ordered fields, this is the usual starting point for contraction proofs when $0<\mathrm{lr}<2$.

def Optim.ScalarGD.stepL2 {α : Type} [Sub α] [Mul α] [Add α] (lr lambda grad x : α) : α

One SGD step with the L2 regularizer $\frac{\lambda}{2}x^2$ adds $\lambda x$ to the gradient.

theorem Optim.ScalarGD.stepL2_eq_decoupledWeightDecay {α : Type} [CommRing α] (lr lambda grad x : α) : stepL2 lr lambda grad x = (1 - lr * lambda) * x - lr * grad

For plain SGD, L2 regularization and decoupled weight decay coincide at the update level.

This scalar statement is the common fact behind the regularization note: adding $\lambda x$ to the gradient produces the same update as multiplying parameters by $1-\mathrm{lr}\lambda$ and then taking the plain gradient step. Adaptive optimizers need separate treatment; AdamW is checked in Optimization.FirstOrder.

theorem Optim.ScalarGD.error_abs_contract_real (lr target x : ℝ) (h0 : 0 < lr) (h2 : lr < 2) (hne : x ≠ target) : |step lr target x - target| < |x - target|

On the one-dimensional quadratic, if $0<\mathrm{lr}<2$, then one GD step contracts the error in absolute value.

This is the scalar version of the operator-level contraction theorem above.