GradientDescentContraction: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

A strongly convex gradient step contracts distances
Gradient descent approaches a global minimizer

ASTIS mathematical exposition

A strongly convex gradient step contracts distances

AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentContraction.gradient_step_contraction · theorem · Teaching coverage

Statement

For every pair x,y, the actual step T satisfies the displayed contraction estimate under the stated global curvature and step conditions.

\[\begin{gathered}T(x)=x-h\nabla f(x),\\r=\sqrt{1-\alpha h},\\f(y)\le f(x)+\langle\nabla f(x),y-x\rangle\\{}+\frac\beta2\|y-x\|^2,\\\|T(y)-T(x)\|\le r\|y-x\|.\end{gathered}\]

All objects and hypotheses

E is a complete real inner-product space, f:E→ℝ is C¹, and all point quantifiers range over E. The gradient is the genuine Riesz representative of its Fréchet derivative.
The real parameters α, β and h are nonnegative and βh≤1.
f is α-strongly convex on all E: the convex chord inequality has the subtraction (α/2)t(1−t)‖y−x‖² for t∈[0,1]. The displayed β quadratic upper model holds for all x,y.
Write T(x)=x−h∇f(x) and r=√(1−αh), with the nonnegative real square root (zero on negative arguments).

Mathematical proof

1. Use the two compiled curvature inequalities

\[\begin{gathered}\alpha\|v\|^2\le p,\quad p\ge0,\\\|d\|^2\le\beta p.\end{gathered}\]

Corresponding Lean step

StrongConvexFirstOrder.gradient_inner_lower_bound_of_strongConvexOn; UniformConvexOn.convexOn; ConvexSmoothGradient.gradient_cocoercive.

2. Expand one actual step

Since h≥0 and βh≤1, multiplying the cocoercivity bound by h² gives h²‖d‖²≤h²βp≤hp. Insert this into the exact squared-norm expansion, then use hp≥αh‖v‖².

\[\begin{gathered}\|v-hd\|^2=\|v\|^2-2hp+h^2\|d\|^2,\\\|v-hd\|^2\le\|v\|^2-hp\\\le(1-\alpha h)\|v\|^2.\end{gathered}\]

Corresponding Lean step

norm_sub_sq_real, inner_smul_right, norm_smul; three mul_le_mul_of_nonneg_left applications and nlinarith.

3. Take a square root without adding compatibility

The squared norm is nonnegative. Taking square roots and factoring the nonnegative factor ‖v‖² yields the asserted distance bound. If 1−αh is negative and v≠0, the squared estimate is impossible; hence no nontrivial negative-coefficient case is hidden.

\[\sqrt{(1-\alpha h)\|v\|^2}=r\|v\|.\]

Corresponding Lean step

Real.le_sqrt_of_sq_le; Real.sqrt_mul' with sq_nonneg; Real.sqrt_sq with norm_nonneg.

Lean statement · gradient_step_contraction

For every pair x,y, the actual step T satisfies the displayed contraction estimate under the stated global curvature and step conditions.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem gradient_step_contraction {f : E → ℝ} {α β h : ℝ}
    (hf : ContDiff ℝ 1 f) (hsc : StrongConvexOn univ α f)
    (hα : 0 ≤ α) (hβ : 0 ≤ β) (hh : 0 ≤ h) (hstep : β * h ≤ 1)
    (hu : ∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + β / 2 * ‖y - x‖ ^ 2)
    (x y : E) :
    ‖(y - h • gradient f y) - (x - h • gradient f x)‖ ≤
      Real.sqrt (1 - α * h) * ‖y - x‖

Exact module and namespace context

Lean proof · gradient_step_contraction

For arbitrary x,y define v=y−x, d=∇f(y)−∇f(x) and p=⟨d,v⟩. Strong convexity with α≥0 supplies convexity and the lower pairing bound. Cocoercivity supplies the upper gradient-square bound. Since h≥0 and βh≤1, multiplying the cocoercivity bound by h² gives h²‖d‖²≤h²βp≤hp. Insert this into the exact squared-norm expansion, then use hp≥αh‖v‖². The squared norm is nonnegative. Taking square roots and factoring the nonnegative factor ‖v‖² yields the asserted distance bound. If 1−αh is negative and v≠0, the squared estimate is impossible; hence no nontrivial negative-coefficient case is hidden.

theorem gradient_step_contraction {f : E → ℝ} {α β h : ℝ}
    (hf : ContDiff ℝ 1 f) (hsc : StrongConvexOn univ α f)
    (hα : 0 ≤ α) (hβ : 0 ≤ β) (hh : 0 ≤ h) (hstep : β * h ≤ 1)
    (hu : ∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + β / 2 * ‖y - x‖ ^ 2)
    (x y : E) :
    ‖(y - h • gradient f y) - (x - h • gradient f x)‖ ≤
      Real.sqrt (1 - α * h) * ‖y - x‖ := by
  have hc : ConvexOn ℝ univ f := hsc.convexOn (by intro r; positivity)
  have hm := StrongConvexFirstOrder.gradient_inner_lower_bound_of_strongConvexOn
    hsc (fun z _ => (hf.differentiable_one z).hasGradientAt) (mem_univ x) (mem_univ y)
  have hg := ConvexSmoothGradient.gradient_cocoercive hf hc hβ hu x y
  have hp : 0 ≤ inner ℝ (gradient f y - gradient f x) (y - x) :=
    le_trans (mul_nonneg hα (sq_nonneg _)) hm
  have hg' := mul_le_mul_of_nonneg_left hg (sq_nonneg h)
  have hs := mul_le_mul_of_nonneg_left hstep (mul_nonneg hh hp)
  have hm' := mul_le_mul_of_nonneg_left hm hh
  have hv : (y - h • gradient f y) - (x - h • gradient f x) =
      (y - x) - h • (gradient f y - gradient f x) := by rw [smul_sub]; abel
  have hb : ‖(y - h • gradient f y) - (x - h • gradient f x)‖ ^ 2 ≤
      (1 - α * h) * ‖y - x‖ ^ 2 := by
    rw [hv, norm_sub_sq_real, inner_smul_right,
      real_inner_comm (gradient f y - gradient f x), norm_smul,
      Real.norm_eq_abs, mul_pow, sq_abs]
    nlinarith
  simpa only [Real.sqrt_mul' _ (sq_nonneg _), Real.sqrt_sq (norm_nonneg _)] using
    Real.le_sqrt_of_sq_le hb

/-- The actual Nth gradient-descent iterate has geometric, then exponential,
distance control about a supplied global minimizer. -/

Exact module and namespace context

Scope and omitted-condition boundaries

C¹ on a complete real inner-product space is an explicit extension of the section’s C² Euclidean setting. The source reciprocal restriction is recovered for β>0; the division-free statement also includes β=0 and h=0. If 1−αh<0, the squared bound forces every pairwise distance to vanish, so the norm result remains valid on a singleton space without an unjustified α≤β assumption. No constrained-domain, Riemannian or stochastic method is covered; this is shared optimization background, not companion-paper progress.
The source prints h≤1/β without stating h≥0. Nonnegative step is essential: f(t)=t²/2, α=β=1 and h=−1 gives T(t)=2t, contradicting the claimed factor √2 for distinct points. The reciprocal formula additionally needs β>0. The stray gradient before y−x in the middle proof display is a transcription typo, resolved by the preceding expansion and Proposition1.6.
The source specializes to h=1/β and κ=β/α. For 0<α≤β, r^N=(1−1/κ)^(N/2) and the exponential factor is exp(−N/(2κ)). This unit does not formalize the subsequent logarithmic iteration-complexity statement or the improved step of Exercise3.2.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

UniformConvexOn.convexOn; ContDiff.differentiable_one; DifferentiableAt.hasGradientAt
norm_sub_sq_real; inner_smul_right; norm_smul; mul_le_mul_of_nonneg_left; Real.le_sqrt_of_sq_le; Real.sqrt_mul'; Real.sqrt_sq

Mathematical sources

Sinho Chewi, Theorem3.3 and its proof — ASTIS-authored restatement and proof explanation; necessary step condition exposed.
Pinned Optlib gradient_method_strong_convex — Related stronger interpolation route, Apache-2.0; external reference only, not an imported dependency.
Reciprocal step, one-step termination and zero-modulus consumers — Compiled calls of the actual new interfaces.

ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.

ASTIS mathematical exposition

Gradient descent approaches a global minimizer

AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentContraction.gradient_descent_distance_bound · theorem · Teaching coverage

Statement

For any actual global minimizer x⋆, any initial point x₀ and every natural N (including zero), the actual Nth iterate satisfies the geometric and exponential distance estimates.

\[\begin{gathered}T(x)=x-h\nabla f(x),\\r=\sqrt{1-\alpha h},\quad R=\|x_0-x_\star\|,\\f(y)\le f(x)+\langle\nabla f(x),y-x\rangle\\{}+\frac\beta2\|y-x\|^2,\\\|T^N(x_0)-x_\star\|\le r^N R,\\r^N R\le e^{-\alpha hN/2}R.\end{gathered}\]

All objects and hypotheses

E is a complete real inner-product space, f:E→ℝ is C¹, and all point quantifiers range over E. The gradient is the genuine Riesz representative of its Fréchet derivative.
The real parameters α, β and h are nonnegative and βh≤1.
f is α-strongly convex on all E: the convex chord inequality has the subtraction (α/2)t(1−t)‖y−x‖² for t∈[0,1]. The displayed β quadratic upper model holds for all x,y.
Write T(x)=x−h∇f(x) and r=√(1−αh), with the nonnegative real square root (zero on negative arguments).
x⋆ is a supplied global minimizer: f(x⋆)≤f(y) for every y∈E. N is a natural number, T^N denotes function iteration (T⁰ is the identity), and R=‖x₀−x⋆‖. No minimizer existence theorem is claimed.

Mathematical proof

1. Derive the fixed point from the actual minimum

\[\nabla f(x_\star)=0,\qquad T(x_\star)=x_\star.\]

Corresponding Lean step

IsMinOn.isLocalMin with Filter.univ_mem; IsLocalMin.fderiv_eq_zero; gradient and map_zero simplification.

2. Iterate the Lipschitz map

The single-step result means T is r-Lipschitz. Its Nth iterate is r^N-Lipschitz, and x⋆ stays fixed under every iterate. Apply the iterated bound to x₀ and x⋆. N=0 is included.

\[\|T^N(x_0)-x_\star\|\le r^N R.\]

Corresponding Lean step

gradient_step_contraction; lipschitzWith_iff_norm_sub_le; Real.toNNReal; LipschitzWith.iterate.dist_le_mul; Function.IsFixedPt.iterate.

3. Compare with the exponential

The real inequality 1−a≤e^(−a), applied with a=αh, implies r≤e^(−αh/2). Both sides are nonnegative, so taking natural powers and multiplying by R≥0 preserves order. The exponential product identity gives the final formula.

\[\begin{gathered}1-\alpha h\le e^{-\alpha h},\\r\le e^{-\alpha h/2},\\r^NR\le e^{-\alpha hN/2}R.\end{gathered}\]

Corresponding Lean step

Real.add_one_le_exp; Real.sqrt_le_left; Real.exp_add; pow_le_pow_left₀; Real.exp_nat_mul.

Lean statement · gradient_descent_distance_bound

For any actual global minimizer x⋆, any initial point x₀ and every natural N (including zero), the actual Nth iterate satisfies the geometric and exponential distance estimates.

theorem gradient_descent_distance_bound {f : E → ℝ} {α β h : ℝ}
    (hf : ContDiff ℝ 1 f) (hsc : StrongConvexOn univ α f)
    (hα : 0 ≤ α) (hβ : 0 ≤ β) (hh : 0 ≤ h) (hstep : β * h ≤ 1)
    (hu : ∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + β / 2 * ‖y - x‖ ^ 2)
    {xstar : E} (hmin : IsMinOn f univ xstar) (x₀ : E) (N : ℕ) :
    ‖(fun x => x - h • gradient f x)^[N] x₀ - xstar‖ ≤
        Real.sqrt (1 - α * h) ^ N * ‖x₀ - xstar‖ ∧
      Real.sqrt (1 - α * h) ^ N * ‖x₀ - xstar‖ ≤
        Real.exp (-(α * h * N) / 2) * ‖x₀ - xstar‖

Exact module and namespace context

Lean proof · gradient_descent_distance_bound

Write x⋆ for the supplied global minimizer, x₀ for the initial point, N∈ℕ for the iteration count, R=‖x₀−x⋆‖, T(x)=x−h∇f(x), and r=√(1−αh). A global minimum on the whole space is a local minimum. Fermat’s theorem sets its Fréchet derivative to zero, so the Riesz gradient vanishes. The single-step result means T is r-Lipschitz. Its Nth iterate is r^N-Lipschitz, and x⋆ stays fixed under every iterate. Apply the iterated bound to x₀ and x⋆. N=0 is included. The real inequality 1−a≤e^(−a), applied with a=αh, implies r≤e^(−αh/2). Both sides are nonnegative, so taking natural powers and multiplying by R≥0 preserves order. The exponential product identity gives the final formula.

theorem gradient_descent_distance_bound {f : E → ℝ} {α β h : ℝ}
    (hf : ContDiff ℝ 1 f) (hsc : StrongConvexOn univ α f)
    (hα : 0 ≤ α) (hβ : 0 ≤ β) (hh : 0 ≤ h) (hstep : β * h ≤ 1)
    (hu : ∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + β / 2 * ‖y - x‖ ^ 2)
    {xstar : E} (hmin : IsMinOn f univ xstar) (x₀ : E) (N : ℕ) :
    ‖(fun x => x - h • gradient f x)^[N] x₀ - xstar‖ ≤
        Real.sqrt (1 - α * h) ^ N * ‖x₀ - xstar‖ ∧
      Real.sqrt (1 - α * h) ^ N * ‖x₀ - xstar‖ ≤
        Real.exp (-(α * h * N) / 2) * ‖x₀ - xstar‖ := by
  let T : E → E := fun x => x - h • gradient f x
  have hg : gradient f xstar = 0 := by
    simp [gradient, (hmin.isLocalMin Filter.univ_mem).fderiv_eq_zero]
  have hfix : Function.IsFixedPt T xstar := by simp [Function.IsFixedPt, T, hg]
  have hl : LipschitzWith (Real.toNNReal (Real.sqrt (1 - α * h))) T := by
    rw [lipschitzWith_iff_norm_sub_le]
    intro x y
    simpa only [Real.coe_toNNReal _ (Real.sqrt_nonneg _)] using
      gradient_step_contraction hf hsc hα hβ hh hstep hu y x
  constructor
  · have hi := (hl.iterate N).dist_le_mul x₀ xstar
    simpa only [dist_eq_norm, (hfix.iterate N).eq, NNReal.coe_pow, Real.coe_toNNReal _ (Real.sqrt_nonneg _), T] using hi
  · have he : Real.sqrt (1 - α * h) ≤ Real.exp (-(α * h) / 2) := by
      apply (Real.sqrt_le_left (Real.exp_nonneg _)).mpr
      have hx := Real.add_one_le_exp (-(α * h))
      rw [pow_two, ← Real.exp_add, show -(α * h) / 2 + -(α * h) / 2 = -(α * h) by ring]
      simpa only [sub_eq_add_neg, add_comm] using hx
    have hp := pow_le_pow_left₀ (Real.sqrt_nonneg _) he N
    have hr := mul_le_mul_of_nonneg_right hp (norm_nonneg (x₀ - xstar))
    rw [← Real.exp_nat_mul, show (N : ℝ) * (-(α * h) / 2) =
      -(α * h * N) / 2 by ring] at hr
    exact hr

end AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentContraction

Exact module and namespace context

Scope and omitted-condition boundaries

C¹ on a complete real inner-product space is an explicit extension of the section’s C² Euclidean setting. The source reciprocal restriction is recovered for β>0; the division-free statement also includes β=0 and h=0. If 1−αh<0, the squared bound forces every pairwise distance to vanish, so the norm result remains valid on a singleton space without an unjustified α≤β assumption. No constrained-domain, Riemannian or stochastic method is covered; this is shared optimization background, not companion-paper progress.
The source prints h≤1/β without stating h≥0. Nonnegative step is essential: f(t)=t²/2, α=β=1 and h=−1 gives T(t)=2t, contradicting the claimed factor √2 for distinct points. The reciprocal formula additionally needs β>0. The stray gradient before y−x in the middle proof display is a transcription typo, resolved by the preceding expansion and Proposition1.6.
The source specializes to h=1/β and κ=β/α. For 0<α≤β, r^N=(1−1/κ)^(N/2) and the exponential factor is exp(−N/(2κ)). This unit does not formalize the subsequent logarithmic iteration-complexity statement or the improved step of Exercise3.2.

Source and reuse

ASTIS parents called

AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentContraction.gradient_step_contraction

Mathlib API called (external library)

IsMinOn.isLocalMin; IsLocalMin.fderiv_eq_zero; gradient
lipschitzWith_iff_norm_sub_le; LipschitzWith.iterate; LipschitzWith.dist_le_mul; Function.IsFixedPt.iterate
Real.sqrt_le_left; Real.add_one_le_exp; Real.exp_add; pow_le_pow_left₀; Real.exp_nat_mul

Mathematical sources

Sinho Chewi, Theorem3.3 and its proof — ASTIS-authored restatement and proof explanation; necessary step condition exposed.
Pinned Optlib gradient_method_strong_convex — Related stronger interpolation route, Apache-2.0; external reference only, not an imported dependency.
Reciprocal step, one-step termination and zero-modulus consumers — Compiled calls of the actual new interfaces.

ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.