Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412
ASTIS mathematical exposition

Convex gradient descent has a normalized final-value bound

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

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}.\]

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

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.

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

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

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.

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

/-- Strongly convex rational rate, and exact inverse-power form on its positive-base domain. -/

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.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

  • strongConvexOn_zero
  • Finset.sum_const
  • Finset.card_range
  • le_div_iff₀

Mathematical sources

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