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.
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.
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.
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.
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.
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_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‖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.
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.GradientDescentContractionScope 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)
- 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.