A small-gradient iterate without convexity
AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentStationarity.exists_gradient_descent_norm_le · theorem · Teaching coverage
Statement
For every initial point and positive natural iteration count, one of the first N actual gradient iterates satisfies the displayed norm bound.
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∈ℕ with N≥1. z∈E is a supplied global minimizer: f(z)≤f(x) for all x∈E.
Mathematical proof
1. Use the true objective lower bound
The supplied global minimizer z gives f(z)≤f(x_N). Apply accumulated descent to replace the final objective value by f(z).
Corresponding Lean step
AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentStationarity.gradient_descent_sum_sq_bound; IsMinOn.
2. Normalize with positive denominators
Let B=2(f(x₀)−f(z))/(Nh). Since h>0 and N>0, multiplication by h/2 preserves and reflects order; (h/2)NB is exactly the initial gap. Hence the sum is at most NB.
Corresponding Lean step
Nat.cast_pos; field_simp; Finset.sum_const; Finset.card_range; mul_le_mul_iff_right₀.
3. Select a small term and take a square root
A nonempty finite sum bounded by the sum of the constant B has a term at most B. Convert that squared-norm bound to a norm bound with Mathlib’s square-root lemma. The witness is one of x₀,…,x_(N−1).
Corresponding Lean step
Finset.exists_le_of_sum_le; Finset.mem_range; Real.le_sqrt_of_sq_le.
Lean statement · exists_gradient_descent_norm_le
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 exists_gradient_descent_norm_le {f : E → ℝ} {β h : ℝ} {z : E}
(hz : IsMinOn f univ z) (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 : ℕ} (hN : 0 < N) :
∃ k ∈ Finset.range N,
‖gradient f ((fun x => x - h • gradient f x)^[k] x₀)‖ ≤
Real.sqrt (2 * (f x₀ - f z) / ((N : ℝ) * h))Lean proof · exists_gradient_descent_norm_le
The supplied global minimizer z gives f(z)≤f(x_N). Apply accumulated descent to replace the final objective value by f(z). Let B=2(f(x₀)−f(z))/(Nh). Since h>0 and N>0, multiplication by h/2 preserves and reflects order; (h/2)NB is exactly the initial gap. Hence the sum is at most NB. A nonempty finite sum bounded by the sum of the constant B has a term at most B. Convert that squared-norm bound to a norm bound with Mathlib’s square-root lemma. The witness is one of x₀,…,x_(N−1).
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 exists_gradient_descent_norm_le {f : E → ℝ} {β h : ℝ} {z : E}
(hz : IsMinOn f univ z) (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 : ℕ} (hN : 0 < N) :
∃ k ∈ Finset.range N,
‖gradient f ((fun x => x - h • gradient f x)^[k] x₀)‖ ≤
Real.sqrt (2 * (f x₀ - f z) / ((N : ℝ) * h)) := by
let T : E → E := fun x => x - h • gradient f x
let B : ℝ := 2 * (f x₀ - f z) / ((N : ℝ) * h)
have hNr : 0 < (N : ℝ) := by exact_mod_cast hN
have hd := gradient_descent_sum_sq_bound hh.le hstep hu x₀ N
have hzN : f z ≤ f (T^[N] x₀) := hz (mem_univ _)
have hsum : (∑ k ∈ Finset.range N, ‖gradient f (T^[k] x₀)‖ ^ 2) ≤
∑ _k ∈ Finset.range N, B := by
have hb : h / 2 * ((N : ℝ) * B) = f x₀ - f z := by
dsimp [B]
field_simp
simp only [Finset.sum_const, Finset.card_range, nsmul_eq_mul]
apply (mul_le_mul_iff_right₀ (show 0 < h / 2 by positivity)).mp
change h / 2 * (∑ k ∈ Finset.range N, ‖gradient f (T^[k] x₀)‖ ^ 2) ≤
h / 2 * ((N : ℝ) * B)
rw [hb]
change h / 2 * (∑ k ∈ Finset.range N, ‖gradient f (T^[k] x₀)‖ ^ 2) ≤
f x₀ - f (T^[N] x₀) at hd
linarith
obtain ⟨k, hk, hkle⟩ := Finset.exists_le_of_sum_le ⟨0, Finset.mem_range.mpr hN⟩ hsum
refine ⟨k, hk, ?_⟩
exact Real.le_sqrt_of_sq_le hkle
end AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentStationarityScope 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 existential witness is equivalent to the finite-minimum upper bound on this nonempty index set. No last-iterate guarantee, convergence of the entire sequence, exact stationary point, or global optimality is concluded.
- The minimizer is supplied, not constructed. At h=1/β with β>0, the formula gives the source O(βΔ₀/ε²) stationarity scaling; no separate stopping algorithm or oracle-complexity theorem is claimed.
Source and reuse
ASTIS parents called
Mathlib API called (external library)
- Finset.exists_le_of_sum_le
- Finset.sum_const
- Finset.card_range
- mul_le_mul_iff_right₀
- Real.le_sqrt_of_sq_le
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.