Accumulated squared-gradient descent
AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentStationarity.gradient_descent_sum_sq_bound · theorem · Teaching coverage
Mathematical statement
For every N∈ℕ, actual gradient descent satisfies the cumulative squared-gradient inequality.
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₀)Proof roadmap
- 1Apply 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.
- 2Add 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.
Full assumptions and notation
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 verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
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₀)) NScope 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.
Sources, dependencies, and reuse
Source and reuse
Samplinglib 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.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.