Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0

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.

  1. A strongly convex gradient step contracts distances
  2. Gradient descent approaches a global minimizer
Samplinglib mathematical lesson

A strongly convex gradient step contracts distances

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

Read this first

Mathematical 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}\]
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.

Download module (.lean)
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

Proof roadmap

  1. 1Use the two compiled curvature inequalities

    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.

  2. 2Expand 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‖².

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

Full assumptions and notation

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

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.

\[\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 verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

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.

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.

Download module (.lean)
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

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.
Sources, dependencies, and reuse

Source and reuse

Samplinglib 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

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

Samplinglib mathematical lesson

Gradient descent approaches a global minimizer

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

Read this first

Mathematical 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}\]
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.

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.

Download module (.lean)
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

Proof roadmap

  1. 1Derive the fixed point from the actual minimum

    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.

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

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

Full assumptions and notation

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

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.

\[\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 verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

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.

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.

Download module (.lean)
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.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

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

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