Gradient descent

TheoremSublinear rate of gradient descent for smooth convex functions#✓fully proved

Let \(E\) be a finite-dimensional real inner product space, let \(L > 0\), and let \(f : E \to \mathbb{R}\) be convex and differentiable with \(L\)-Lipschitz gradient \(\nabla f\). Let \(x^\star \in E\) be a global minimizer of \(f\), let \(0 < \eta \le 1/L\), and let \((x_k)_{k \ge 0}\) be any sequence in \(E\) with \(x_{k+1} = x_k - \eta \nabla f(x_k)\) for all \(k\). Then for every \(k \ge 1\), \(f(x_k) - f(x^\star) \le \|x_0 - x^\star\|^2 / (2 \eta k)\).

Proof: The descent lemma and first-order convexity inequality are proved on affine lines. They bound each objective gap by a difference of squared distances to \(x^\star\); telescoping and the monotonicity of \(f(x_k)\) in \(k\) give the rate, as in L. Vandenberghe, ECE236C lecture notes "Gradient method" (Spring 2022), slides 1.23-1.26.

theorem gradient_descent_convex_sublinear_rate
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
      [FiniteDimensional ℝ E]
    {f : E → ℝ} {L : ℝ} (hL : 0 < L)
    (hconvex : ConvexOn ℝ Set.univ f)
    (hdiff : Differentiable ℝ f)
    (hsmooth : LipschitzWith ⟨L, le_of_lt hL⟩ (gradient f))
    {xstar : E} (hmin : ∀ x, f xstar ≤ f x)
    {η : ℝ} (hη : η ∈ Set.Ioc 0 (1 / L))
    {X : ℕ → E} (hX : ∀ k, X (k + 1) = X k - η • gradient f (X k)) :
    ∀ k : ℕ, 0 < k →
      f (X k) - f xstar ≤ ‖X 0 - xstar‖ ^ 2 / (2 * η * (k : ℝ))

Sources

• Y. Nesterov, Introductory Lectures on Convex Optimization, Section 2.1; https://en.wikipedia.org/wiki/Gradient_descent.

Used by 1

Used byConstant unit steps achieve exponent one

DefinitionGradient descent with a step schedule#✓fully proved

Let \(E\) be a real Hilbert space, \(f : E \to \mathbb{R}\), \(s : \mathbb{N} \to \mathbb{R}\) a sequence of step sizes and \(x_0 \in E\). The gradient descent trajectory of \(f\) from \(x_0\) with steps \(s\) is the sequence \((x_k)_{k \in \mathbb{N}}\) in \(E\) starting at \(x_0\) with \(x_{k+1} = x_k - s_k \nabla f(x_k)\).

Here \(\nabla f(x)\) is taken to be \(0\) at points \(x\) where \(f\) is not differentiable.

noncomputable def gradientDescentTrajectory
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
    (f : E → ℝ) (s : ℕ → ℝ) (x₀ : E) : ℕ → E
  | 0 => x₀
  | k + 1 => gradientDescentTrajectory f s x₀ k -
      s k • gradient f (gradientDescentTrajectory f s x₀ k)

Used by 3

Used byGradient descent with zero step sizes stays put · Uniform last-iterate rate of a step schedule · Constant unit steps achieve exponent one

DefinitionConvex functions with \(1\)-Lipschitz gradient#✓fully proved

A function \(f : E \to \mathbb{R}\) on a real Hilbert space \(E\) is unit-smooth convex if it is convex, differentiable, and its gradient is \(1\)-Lipschitz: \(\lVert \nabla f(x) - \nabla f(y) \rVert \le \lVert x - y \rVert\) for all \(x, y \in E\).

def IsUnitSmoothConvex
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
    (f : E → ℝ) : Prop :=
  ConvexOn ℝ Set.univ f ∧ Differentiable ℝ f ∧ LipschitzWith 1 (gradient f)

Used by 2

Used byUniform last-iterate rate of a step schedule · Constant unit steps achieve exponent one

DefinitionUniform last-iterate rate of a step schedule#✓fully proved

A step schedule \(s : \mathbb{N} \to \mathbb{R}\) achieves a uniform last-iterate rate with exponent \(c \in \mathbb{R}\) if there are a real number \(C > 0\) and an integer \(K \ge 1\) with the following property. For every \(d \in \mathbb{N}\), every convex differentiable function \(f : \mathbb{R}^d \to \mathbb{R}\) whose gradient is \(1\)-Lipschitz for the Euclidean norm, every \(x^\star \in \mathbb{R}^d\) with \(f(x^\star) \le f(x)\) for all \(x\), every \(x_0 \in \mathbb{R}^d\) and every integer \(k \ge K\), the \(k\)-th gradient descent iterate \(x_k\) of \(f\) from \(x_0\) with steps \(s\) satisfies

\[f(x_k) - f(x^\star) \le \frac{C \lVert x_0 - x^\star \rVert^2}{k^c}.\]

The constants \(C\) and \(K\) are chosen before, and do not depend on, \(d\), \(f\), \(x^\star\), \(x_0\) and \(k\).

def GradientDescentUniformRate (s : ℕ → ℝ) (c : ℝ) : Prop :=
  ∃ C : ℝ, 0 < C ∧ ∃ K : ℕ, 0 < K ∧
    ∀ (d : ℕ) (f : EuclideanSpace ℝ (Fin d) → ℝ), IsUnitSmoothConvex f →
      ∀ xstar : EuclideanSpace ℝ (Fin d), (∀ x, f xstar ≤ f x) →
        ∀ x₀ : EuclideanSpace ℝ (Fin d), ∀ k : ℕ, K ≤ k →
          f (gradientDescentTrajectory f s x₀ k) - f xstar ≤
            C * ‖x₀ - xstar‖ ^ 2 / (k : ℝ) ^ c

Uses 2 · Used by 3

Statement usesConvex functions with \(1\)-Lipschitz gradient · Gradient descent with a step schedule

Used byThe gradient descent exponent · Constant unit steps achieve exponent one · The gradient descent exponent is at least one

DefinitionThe gradient descent exponent#✓fully proved

The gradient descent exponent is the supremum, in the extended reals \([-\infty, +\infty]\), of the set of real numbers \(c\) such that some step schedule \(s : \mathbb{N} \to \mathbb{R}\) achieves a uniform last-iterate rate with exponent \(c\). In particular, it is \(-\infty\) if there is no such \(c\), and \(+\infty\) if these exponents are unbounded above.

noncomputable def gradientDescentExponent : EReal :=
  sSup {r | ∃ c : ℝ, r = (c : EReal) ∧ ∃ s : ℕ → ℝ, GradientDescentUniformRate s c}

Sources

• OptimizationProblems, constants/35a.md (constant C35).

Uses 1 · Used by 1

Statement usesUniform last-iterate rate of a step schedule

Used byThe gradient descent exponent is at least one

DefinitionSilver ratio#✓fully proved

The silver ratio is the real number \(\rho = 1 + \sqrt{2}\).

It is the ratio used by the stepsize-hedging (silver) step schedule.

noncomputable def gradientDescentSilverRatio : ℝ := 1 + Real.sqrt 2

Used by 2

Used bySilver exponent · Silver step schedule

DefinitionSilver exponent#✓fully proved

The silver exponent is \(\log_2 \rho = \log \rho / \log 2\), where \(\rho = 1 + \sqrt{2}\) is the silver ratio.

It is the catalogue's proposed optimal value of the gradient descent exponent.

noncomputable def silverGradientDescentExponent : ℝ :=
  Real.log gradientDescentSilverRatio / Real.log 2

Uses 1

Statement usesSilver ratio

DefinitionSilver step schedule#✓fully proved

The silver step schedule is the sequence \(s_t = 1 + \rho^{\nu_2(t + 1) - 1}\) for \(t \in \mathbb{N}\), where \(\rho = 1 + \sqrt{2}\) is the silver ratio and \(\nu_2(n)\) is the exponent of \(2\) in the prime factorization of \(n\).

The exponent \(\nu_2(t + 1) - 1\) is an integer and equals \(-1\) for even \(t\), where \(s_t = 1 + \rho^{-1} = \sqrt{2}\).

noncomputable def silverGradientDescentSchedule (t : ℕ) : ℝ :=
  1 + gradientDescentSilverRatio ^ ((padicValNat 2 (t + 1) : ℤ) - 1)

Uses 1

Statement usesSilver ratio

TheoremConstant unit steps achieve exponent one#✓fully proved

The step schedule with every step size equal to \(1\) achieves a uniform last-iterate rate with exponent \(1\).

This follows from the fixed-step descent theorem; it is a lower bound for the gradient descent exponent, not its conjectured optimal value.

theorem gradientDescentUniformRate_one : GradientDescentUniformRate (fun _ => 1) 1

Uses 4 · Used by 1

Statement usesUniform last-iterate rate of a step schedule

Proof usesConvex functions with \(1\)-Lipschitz gradient · Sublinear rate of gradient descent for smooth convex functions · Gradient descent with a step schedule

Used byThe gradient descent exponent is at least one

TheoremThe gradient descent exponent is at least one#✓fully proved

The gradient descent exponent is at least \(1\).

theorem one_le_gradientDescentExponent : (1 : EReal) ≤ gradientDescentExponent

Uses 3

Statement usesThe gradient descent exponent

Proof usesUniform last-iterate rate of a step schedule · Constant unit steps achieve exponent one

TheoremGradient descent with zero step sizes stays put#✓fully proved

Let \(E\) be a real Hilbert space, \(f : E \to \mathbb{R}\) and \(x_0 \in E\). If every step size is \(0\), then for every \(k \in \mathbb{N}\) the \(k\)-th gradient descent iterate of \(f\) from \(x_0\) equals \(x_0\).

@[simp] theorem gradientDescentTrajectory_zeroSchedule
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
    (f : E → ℝ) (x₀ : E) (k : ℕ) :
    gradientDescentTrajectory f (fun _ => 0) x₀ k = x₀

Uses 1

Statement usesGradient descent with a step schedule

11 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.