GradientDescentStationarity: 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.

Accumulated squared-gradient descent
A small-gradient iterate without convexity

Samplinglib mathematical lesson

Accumulated squared-gradient descent

AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentStationarity.gradient_descent_sum_sq_bound · theorem · Teaching coverage

Read this first

Mathematical statement

For every N∈ℕ, actual gradient descent satisfies the cumulative squared-gradient inequality.

\[\frac h2\sum_{k=0}^{N-1}\|\nabla f(T^k x_0)\|^2\le f(x_0)-f(T^N x_0).\]

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.

Download module (.lean)

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₀)

Exact module and namespace context

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.

\[\tfrac h2\|\nabla f(x_k)\|^2\le f(x_k)-f(x_{k+1}).\]

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.

\[\frac h2\sum_{k=0}^{N-1}\|\nabla f(x_k)\|^2\le\sum_{k=0}^{N-1}(f(x_k)-f(x_{k+1}))=f(x_0)-f(x_N).\]

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.

Download module (.lean)

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

Exact module and namespace context

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.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentBasic.gradient_step_descent_of_quadratic_upper_bound

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.

Samplinglib mathematical lesson

A small-gradient iterate without convexity

AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentStationarity.exists_gradient_descent_norm_le · theorem · Teaching coverage

Read this first

Mathematical statement

For every initial point and positive natural iteration count, one of the first N actual gradient iterates satisfies the displayed norm bound.

\[\exists k\in\{0,\ldots,N-1\}:\quad\|\nabla f(T^k x_0)\|\le\sqrt{\frac{2(f(x_0)-f(z))}{Nh}}.\]

Lean statement · exists_gradient_descent_norm_le

Actual gradient iterates, explicit upper model and step/iteration domains.

Download module (.lean)

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))

Exact module and namespace context

Proof roadmap

1Use 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).
2Normalize 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.
3Select 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).

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∈ℕ 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).

\[\frac h2\sum_{k=0}^{N-1}\|\nabla f(x_k)\|^2\le f(x_0)-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.

\[\sum_{k=0}^{N-1}\|\nabla f(x_k)\|^2\le NB,\qquad B=\frac{2(f(x_0)-f(z))}{Nh}.\]

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).

\[\exists k<N:\quad\|\nabla f(x_k)\|^2\le B\quad\Longrightarrow\quad\|\nabla f(x_k)\|\le\sqrt B.\]

Corresponding Lean step

Finset.exists_le_of_sum_le; Finset.mem_range; Real.le_sqrt_of_sq_le.

Lean verification

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

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).

Download module (.lean)

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.GradientDescentStationarity

Exact module and namespace context

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

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentStationarity.gradient_descent_sum_sq_bound

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.

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