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

Convex gradient descent has a normalized final-value bound
Strongly convex gradient descent has rational and inverse-power rates

Samplinglib mathematical lesson

Convex gradient descent has a normalized final-value bound

AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentRates.convex_value_le · theorem · Teaching coverage

Read this first

Mathematical statement

E is a complete real inner-product space and f:E→R is C1. The gradient is the genuine Riesz gradient of f. For all x,y, f(y)≤f(x)+<gradient f(x),y-x>+(beta/2)||y-x||². The step satisfies h>0 and beta*h≤1; N is a positive natural number. x0 and z are arbitrary points; X_N is exactly N iterations of x ↦ x-h gradient f(x) starting at x0. No minimizer is required for the comparator bound. f is convex on the whole space. No positivity assumption on beta is needed beyond the upper model and admissible step. The following bound holds for the actual final iterate.

\[X_N=(\mathrm{id}-h\nabla f)^N(x_0),\qquad f(X_N)-f(z)\le\frac{\|x_0-z\|^2}{2hN}.\]

Lean statement · convex_value_le

Convex gradient descent has a normalized final-value bound.

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 convex_value_le {f : E → ℝ} {β h : ℝ} (hf : ContDiff ℝ 1 f)
    (hc : ConvexOn ℝ univ f) (hh : 0 < h) (hstep : β * h ≤ 1)
    (hu : ∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + β / 2 * ‖y - x‖ ^ 2)
    (x₀ z : E) {N : ℕ} (hN : 0 < N) :
    f ((fun x => x - h • gradient f x)^[N] x₀) - f z ≤ ‖x₀ - z‖ ^ 2 / (2 * h * N)

Exact module and namespace context

Proof roadmap

1Reuse the actual-iterate energy estimate
Write q=1-alpha h, R=||x0-z|| and e_N=f(X_N)-f(z). The existing weighted theorem already derives objective descent and the forced recurrence for the actual gradient iterates. Invoke it directly; its conclusion also allows negative comparator gaps.
2Evaluate the zero-curvature sum
For a convex objective set alpha=0, hence q=1. Every summand equals one and there are exactly N summands. Thus the weighted estimate becomes 2hN e_N≤R².
3Divide on the positive domain
Since h>0 and N>0, the coefficient 2hN is positive. Dividing preserves the inequality. With beta>0, substituting h=1/beta gives exactly beta R²/(2N), the source prescribed-step convex rate. This substitution is exercised by a compiled consumer test.

Full assumptions and notation

All objects and hypotheses

E is a complete real inner-product space and f:E→R is C1. The gradient is the genuine Riesz gradient of f.
For all x,y, f(y)≤f(x)+<gradient f(x),y-x>+(beta/2)||y-x||². The step satisfies h>0 and beta*h≤1; N is a positive natural number.
x0 and z are arbitrary points; X_N is exactly N iterations of x ↦ x-h gradient f(x) starting at x0. No minimizer is required for the comparator bound.
f is convex on the whole space. No positivity assumption on beta is needed beyond the upper model and admissible step.

Mathematical proof

1. Reuse the actual-iterate energy estimate

\[2h\Bigl(\sum_{k=0}^{N-1}q^k\Bigr)e_N\le q^N R^2.\]

Corresponding Lean step

GradientDescentValue.gradient_descent_weighted_value_bound.

2. Evaluate the zero-curvature sum

For a convex objective set alpha=0, hence q=1. Every summand equals one and there are exactly N summands. Thus the weighted estimate becomes 2hN e_N≤R².

\[\alpha=0:\quad q=1,\qquad\sum_{k=0}^{N-1}q^k=N,\qquad2hNe_N\le R^2.\]

Corresponding Lean step

strongConvexOn_zero; Finset.sum_const, card_range, one_pow and nsmul_eq_mul.

3. Divide on the positive domain

Since h>0 and N>0, the coefficient 2hN is positive. Dividing preserves the inequality. With beta>0, substituting h=1/beta gives exactly beta R²/(2N), the source prescribed-step convex rate. This substitution is exercised by a compiled consumer test.

\[e_N\le\frac{R^2}{2hN};\qquad h=1/\beta\Longrightarrow e_N\le\frac{\beta R^2}{2N}.\]

Corresponding Lean step

le_div_iff₀; Tests.Shared.GradientDescentRates verifies the reciprocal-step specialization.

Lean verification

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

Lean proof · convex_value_le

Write q=1-alpha h, R=||x0-z|| and e_N=f(X_N)-f(z). The existing weighted theorem already derives objective descent and the forced recurrence for the actual gradient iterates. Invoke it directly; its conclusion also allows negative comparator gaps. For a convex objective set alpha=0, hence q=1. Every summand equals one and there are exactly N summands. Thus the weighted estimate becomes 2hN e_N<=R². Since h>0 and N>0, the coefficient 2hN is positive. Dividing preserves the inequality. With beta>0, substituting h=1/beta gives exactly beta R²/(2N), the source prescribed-step convex rate. This substitution is exercised by a compiled consumer test.

Download module (.lean)

theorem convex_value_le {f : E → ℝ} {β h : ℝ} (hf : ContDiff ℝ 1 f)
    (hc : ConvexOn ℝ univ f) (hh : 0 < h) (hstep : β * h ≤ 1)
    (hu : ∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + β / 2 * ‖y - x‖ ^ 2)
    (x₀ z : E) {N : ℕ} (hN : 0 < N) :
    f ((fun x => x - h • gradient f x)^[N] x₀) - f z ≤ ‖x₀ - z‖ ^ 2 / (2 * h * N) := by
  have he := gradient_descent_weighted_value_bound hf
    (strongConvexOn_zero.mpr hc) hh.le hstep (by norm_num : (0 : ℝ) * h ≤ 1) hu x₀ z N
  simp only [zero_mul, sub_zero, one_pow, sum_const, card_range, nsmul_eq_mul,
    mul_one, one_mul] at he
  apply (le_div_iff₀ (by positivity : 0 < 2 * h * (N : ℝ))).mpr
  nlinarith [he]

Exact module and namespace context

Scope and omitted-condition boundaries

These are public integrations of the existing weighted theorem and previously compiled test normalizations. The new representation edge is the exact inverse-power equality; no new descent or recurrence proof is claimed.
C1 on a complete real Hilbert space and arbitrary comparator generalize the C2 Euclidean minimizer-based source rate. Source smoothness is represented by its global quadratic upper model. The condition beta*h≤1 agrees with h≤1/beta when beta>0.
Finite normalized bounds require h>0 and N>0. No real-valued normalized h=0 or N=0 assertion, analytic alpha-to-zero limit, iteration-complexity theorem, minimum existence, Riemannian or stochastic result is claimed.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentValue.gradient_descent_weighted_value_bound

Mathlib API called (external library)

strongConvexOn_zero
Finset.sum_const
Finset.card_range
le_div_iff₀

Mathematical sources

Chewi Theorem3.4 — Normalized source rate and weighted proof; endpoint interpretation explicitly separated.
Previously compiled normalization proofs — The convex and strong rational algebra existed as test consumers before this public interface.
Public interface consumer tests — Actual unit quadratic, arbitrary comparators, positive and zero geometric base, reciprocal step and singular inverse-power counterexample.

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

Strongly convex gradient descent has rational and inverse-power rates

AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentRates.strongly_convex_value_le · theorem · Teaching coverage

Read this first

Mathematical statement

E is a complete real inner-product space and f:E→R is C1. The gradient is the genuine Riesz gradient of f. For all x,y, f(y)≤f(x)+<gradient f(x),y-x>+(beta/2)||y-x||². The step satisfies h>0 and beta*h≤1; N is a positive natural number. x0 and z are arbitrary points; X_N is exactly N iterations of x ↦ x-h gradient f(x) starting at x0. No minimizer is required for the comparator bound. f is alpha-strongly convex on the whole space with normalization alpha/2; alpha>0 and alpha*h≤1. The rational bound includes q=1-alpha*h=0; the second, conditional inverse-power bound additionally requires alpha*h<1. The following bound holds for the actual final iterate.

\[\begin{gathered}q=1-\alpha h\in[0,1),\qquad f(X_N)-f(z)\le\frac{\alpha q^N\|x_0-z\|^2}{2(1-q^N)},\\q>0\Longrightarrow f(X_N)-f(z)\le\frac{\alpha}{2(q^{-N}-1)}\|x_0-z\|^2.\end{gathered}\]

Lean statement · strongly_convex_value_le

Strongly convex gradient descent has rational and inverse-power rates.

Download module (.lean)

theorem strongly_convex_value_le {f : E → ℝ} {α β h : ℝ} (hf : ContDiff ℝ 1 f)
    (hsc : StrongConvexOn univ α f) (hα : 0 < α) (hh : 0 < h) (hstep : β * h ≤ 1)
    (hcoeff : α * h ≤ 1)
    (hu : ∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + β / 2 * ‖y - x‖ ^ 2)
    (x₀ z : E) {N : ℕ} (hN : 0 < N) :
    f ((fun x => x - h • gradient f x)^[N] x₀) - f z ≤
      α * (1 - α * h) ^ N * ‖x₀ - z‖ ^ 2 / (2 * (1 - (1 - α * h) ^ N)) ∧
    (α * h < 1 → f ((fun x => x - h • gradient f x)^[N] x₀) - f z ≤
      α / (2 * ((1 - α * h) ^ (-(N : ℤ)) - 1)) * ‖x₀ - z‖ ^ 2)

Exact module and namespace context

Proof roadmap

1Reuse the actual-iterate energy estimate
Write q=1-alpha h, R=||x0-z|| and e_N=f(X_N)-f(z). The existing weighted theorem already derives objective descent and the forced recurrence for the actual gradient iterates. Invoke it directly; its conclusion also allows negative comparator gaps.
2Normalize the geometric sum without inverting q
Positive alpha and h with alpha h≤1 give 0≤q<1. For N>0, q^N<1. The finite geometric identity, multiplied by 2, yields 2alpha h sum(q^k)=2(1-q^N). Multiply the weighted estimate by positive alpha and divide by positive 2(1-q^N). This rational form remains valid at q=0.
3Recover the source inverse-power expression
Under the additional strict inequality alpha h<1, q>0 and q^N>0. Integer negative powers equal inverse positive powers. Multiplying numerator and denominator by q^N proves the exact displayed equality. At q=0 only the preceding rational conclusion applies; the negative-power formula is undefined in ordinary real arithmetic.

Full assumptions and notation

All objects and hypotheses

E is a complete real inner-product space and f:E→R is C1. The gradient is the genuine Riesz gradient of f.
For all x,y, f(y)≤f(x)+<gradient f(x),y-x>+(beta/2)||y-x||². The step satisfies h>0 and beta*h≤1; N is a positive natural number.
x0 and z are arbitrary points; X_N is exactly N iterations of x ↦ x-h gradient f(x) starting at x0. No minimizer is required for the comparator bound.
f is alpha-strongly convex on the whole space with normalization alpha/2; alpha>0 and alpha*h≤1.
The rational bound includes q=1-alpha*h=0; the second, conditional inverse-power bound additionally requires alpha*h<1.

Mathematical proof

1. Reuse the actual-iterate energy estimate

\[2h\Bigl(\sum_{k=0}^{N-1}q^k\Bigr)e_N\le q^N R^2.\]

Corresponding Lean step

GradientDescentValue.gradient_descent_weighted_value_bound.

2. Normalize the geometric sum without inverting q

Positive alpha and h with alpha h≤1 give 0≤q<1. For N>0, q^N<1. The finite geometric identity, multiplied by 2, yields 2alpha h sum(q^k)=2(1-q^N). Multiply the weighted estimate by positive alpha and divide by positive 2(1-q^N). This rational form remains valid at q=0.

\[2\alpha h\sum_{k=0}^{N-1}q^k=2(1-q^N)>0,\qquad e_N\le\frac{\alpha q^N R^2}{2(1-q^N)}.\]

Corresponding Lean step

geom_sum_mul_neg, pow_lt_one₀, mul_le_mul_of_nonneg_left and le_div_iff₀.

3. Recover the source inverse-power expression

Under the additional strict inequality alpha h<1, q>0 and q^N>0. Integer negative powers equal inverse positive powers. Multiplying numerator and denominator by q^N proves the exact displayed equality. At q=0 only the preceding rational conclusion applies; the negative-power formula is undefined in ordinary real arithmetic.

\[0<q<1:\quad\frac{\alpha q^N R^2}{2(1-q^N)}=\frac{\alpha}{2(q^{-N}-1)}R^2.\]

Corresponding Lean step

zpow_neg, zpow_natCast, pow_pos and field_simp. The positive q^N fact discharges inverse cancellation.

Lean verification

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

Lean proof · strongly_convex_value_le

Write q=1-alpha h, R=||x0-z|| and e_N=f(X_N)-f(z). The existing weighted theorem already derives objective descent and the forced recurrence for the actual gradient iterates. Invoke it directly; its conclusion also allows negative comparator gaps. Positive alpha and h with alpha h<=1 give 0<=q<1. For N>0, q^N<1. The finite geometric identity, multiplied by 2, yields 2alpha h sum(q^k)=2(1-q^N). Multiply the weighted estimate by positive alpha and divide by positive 2(1-q^N). This rational form remains valid at q=0. Under the additional strict inequality alpha h<1, q>0 and q^N>0. Integer negative powers equal inverse positive powers. Multiplying numerator and denominator by q^N proves the exact displayed equality. At q=0 only the preceding rational conclusion applies; the negative-power formula is undefined in ordinary real arithmetic.

Download module (.lean)

theorem strongly_convex_value_le {f : E → ℝ} {α β h : ℝ} (hf : ContDiff ℝ 1 f)
    (hsc : StrongConvexOn univ α f) (hα : 0 < α) (hh : 0 < h) (hstep : β * h ≤ 1)
    (hcoeff : α * h ≤ 1)
    (hu : ∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + β / 2 * ‖y - x‖ ^ 2)
    (x₀ z : E) {N : ℕ} (hN : 0 < N) :
    f ((fun x => x - h • gradient f x)^[N] x₀) - f z ≤
      α * (1 - α * h) ^ N * ‖x₀ - z‖ ^ 2 / (2 * (1 - (1 - α * h) ^ N)) ∧
    (α * h < 1 → f ((fun x => x - h • gradient f x)^[N] x₀) - f z ≤
      α / (2 * ((1 - α * h) ^ (-(N : ℤ)) - 1)) * ‖x₀ - z‖ ^ 2) := by
  have hq : 0 ≤ 1 - α * h := by linarith
  have hqlt : 1 - α * h < 1 := by nlinarith
  have he := gradient_descent_weighted_value_bound hf hsc hh.le hstep (by linarith) hu x₀ z N
  have hs := geom_sum_mul_neg (1 - α * h) N
  have hp : (1 - α * h) ^ N < 1 := pow_lt_one₀ hq hqlt (Nat.ne_of_gt hN)
  have hr : f ((fun x => x - h • gradient f x)^[N] x₀) - f z ≤
      α * (1 - α * h) ^ N * ‖x₀ - z‖ ^ 2 / (2 * (1 - (1 - α * h) ^ N)) := by
    apply (le_div_iff₀ (by positivity : 0 < 2 * (1 - (1 - α * h) ^ N))).mpr
    have hem := mul_le_mul_of_nonneg_left he hα.le
    have hid : α * (2 * h * ∑ k ∈ range N, (1 - α * h) ^ k) =
        2 * (1 - (1 - α * h) ^ N) := by nlinarith [hs]
    rw [← mul_assoc, hid] at hem
    nlinarith [hem]
  refine ⟨hr, ?_⟩
  intro hstrict
  have hqp : 0 < (1 - α * h) ^ N := pow_pos (by linarith) N
  have heq : α * (1 - α * h) ^ N * ‖x₀ - z‖ ^ 2 /
      (2 * (1 - (1 - α * h) ^ N)) =
      α / (2 * ((1 - α * h) ^ (-(N : ℤ)) - 1)) * ‖x₀ - z‖ ^ 2 := by
    rw [zpow_neg, zpow_natCast]
    field_simp
  rwa [heq] at hr

end AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentRates

Exact module and namespace context

Scope and omitted-condition boundaries

These are public integrations of the existing weighted theorem and previously compiled test normalizations. The new representation edge is the exact inverse-power equality; no new descent or recurrence proof is claimed.
C1 on a complete real Hilbert space and arbitrary comparator generalize the C2 Euclidean minimizer-based source rate. Source smoothness is represented by its global quadratic upper model. The condition beta*h≤1 agrees with h≤1/beta when beta>0.
Finite normalized bounds require h>0 and N>0. No real-valued normalized h=0 or N=0 assertion, analytic alpha-to-zero limit, iteration-complexity theorem, minimum existence, Riemannian or stochastic result is claimed.
The rational coefficient equals zero at q=0 and N>0. With an actual minimizing comparator it forces exact objective optimality. This does not make the source inverse-power expression meaningful at zero.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentValue.gradient_descent_weighted_value_bound

Mathlib API called (external library)

geom_sum_mul_neg
pow_lt_one₀
pow_pos
zpow_neg
zpow_natCast
le_div_iff₀

Mathematical sources

Chewi Theorem3.4 — Normalized source rate and weighted proof; endpoint interpretation explicitly separated.
Previously compiled normalization proofs — The convex and strong rational algebra existed as test consumers before this public interface.
Public interface consumer tests — Actual unit quadratic, arbitrary comparators, positive and zero geometric base, reciprocal step and singular inverse-power counterexample.

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