Accumulated squared-gradient descent
AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentStationarity.gradient_descent_sum_sq_bound · theorem · Teaching coverage
Statement
For every N∈ℕ, actual gradient descent satisfies the cumulative squared-gradient inequality.
All objects and hypotheses
- E is a complete real inner-product space; f:E→ℝ and β,h∈ℝ. Write T(x)=x−h∇f(x), x_k=T^k(x₀), with x₀∈E. T^0 is the identity.
- For every x,y∈E, f(y)≤f(x)+⟨∇f(x),y−x⟩+(β/2)‖y−x‖², and βh≤1. ∇f is the actual Riesz vector of the totalized Fréchet derivative, not a supplied vector field.
- The result is algebraic after this upper model is supplied; no separate C¹ or C² premise is required by the implication. The source smooth Euclidean setting supplies that model. This does not say that an arbitrary function is differentiable or satisfies the model.
- h≥0 and N∈ℕ; neither a minimum nor a lower bound is required.
Mathematical proof
1. Apply descent at every actual iterate
The existing shared descent theorem controls the gradient norm at x_k by the decrease from x_k to x_(k+1). The successor identity connects the abstract iterate to the actual update.
Corresponding Lean step
AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentBasic.gradient_step_descent_of_quadratic_upper_bound; Function.iterate_succ_apply'.
2. Add and telescope
Distribute h/2 over the finite sum, sum the pointwise inequalities, then cancel adjacent objective values with Mathlib’s reversed telescoping identity. No lower bound is needed.
Corresponding Lean step
Finset.mul_sum; Finset.sum_le_sum; Finset.sum_range_sub'.
Lean statement · gradient_descent_sum_sq_bound
Actual gradient iterates, explicit upper model and step/iteration domains.
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_sum_sq_bound {f : E → ℝ} {β h : ℝ}
(hh : 0 ≤ h) (hstep : β * h ≤ 1)
(hu : ∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + β / 2 * ‖y - x‖ ^ 2)
(x₀ : E) (N : ℕ) :
h / 2 * ∑ k ∈ Finset.range N, ‖gradient f ((fun x => x - h • gradient f x)^[k] x₀)‖ ^ 2 ≤
f x₀ - f ((fun x => x - h • gradient f x)^[N] x₀)Lean proof · gradient_descent_sum_sq_bound
The existing shared descent theorem controls the gradient norm at x_k by the decrease from x_k to x_(k+1). The successor identity connects the abstract iterate to the actual update. Distribute h/2 over the finite sum, sum the pointwise inequalities, then cancel adjacent objective values with Mathlib’s reversed telescoping identity. No lower bound is needed.
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_sum_sq_bound {f : E → ℝ} {β h : ℝ}
(hh : 0 ≤ h) (hstep : β * h ≤ 1)
(hu : ∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + β / 2 * ‖y - x‖ ^ 2)
(x₀ : E) (N : ℕ) :
h / 2 * ∑ k ∈ Finset.range N, ‖gradient f ((fun x => x - h • gradient f x)^[k] x₀)‖ ^ 2 ≤
f x₀ - f ((fun x => x - h • gradient f x)^[N] x₀) := by
let T : E → E := fun x => x - h • gradient f x
calc
h / 2 * ∑ k ∈ Finset.range N, ‖gradient f (T^[k] x₀)‖ ^ 2 =
∑ k ∈ Finset.range N, h / 2 * ‖gradient f (T^[k] x₀)‖ ^ 2 := Finset.mul_sum _ _ _
_ ≤ ∑ k ∈ Finset.range N, (f (T^[k] x₀) - f (T^[k + 1] x₀)) := by
apply Finset.sum_le_sum
intro k _
rw [Function.iterate_succ_apply']
have hd := GradientDescentBasic.gradient_step_descent_of_quadratic_upper_bound
hh hstep hu (T^[k] x₀)
change h / 2 * ‖gradient f (T^[k] x₀)‖ ^ 2 ≤ f (T^[k] x₀) - f (T (T^[k] x₀))
dsimp [T] at *
linarith
_ = f x₀ - f (T^[N] x₀) := by
simpa using Finset.sum_range_sub' (fun k => f (T^[k] x₀)) N
/-- Among the first `N` actual gradient iterates, one has small gradient norm.
This is a best-iterate guarantee, not a last-iterate or global optimality guarantee. -/Scope and omitted-condition boundaries
- No convexity, PL inequality, or stochastic oracle is assumed. These are shared textbook optimization results, not companion-paper completion.
- The real parameter β need not be positive in this algebraic model. For source β>0, βh≤1 is equivalent to h≤1/β; β=0 and negative β are explicitly broader model domains, not new reciprocal smoothness claims.
- The source prints only h≤1/β. The normalized theorem additionally needs h>0 and N≥1. For f(t)=t²/2, β=1,x₀=1,z=0,N=1, h=0 or h=−1 makes the Lean-totalized square-root bound equal to 0, although the only tested gradient has norm 1. In ordinary real arithmetic these expressions are undefined. At N=0 the minimum has an empty index set. Proposed domain repairs are separately reviewed; the pinned source wording remains unchanged.
- The unnormalized sum includes h=0 and N=0; both are equality cases. This proof component alone is not the normalized stationary-iterate guarantee.
Source and reuse
ASTIS parents called
Mathlib API called (external library)
- Function.iterate_succ_apply'
- Finset.mul_sum
- Finset.sum_le_sum
- Finset.sum_range_sub'
Mathematical sources
- Chewi Theorem3.7 and its proof — ASTIS-authored source restatement; explicit domain repair, algebraic Hilbert generalization.
- Quadratic objective and endpoint tests — Actual gradients, beta=0 constant objective, and zero-step accumulation; no separate theorem credit.
ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.