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

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.

  1. Convex gradient descent has a normalized final-value bound
  2. Strongly convex gradient descent has rational and inverse-power rates
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.

ASTIS mathematical exposition

Strongly convex gradient descent has rational and inverse-power rates

AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentRates.strongly_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 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}\]

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

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. 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 statement · strongly_convex_value_le

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

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

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.

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

Source and reuse

ASTIS parents called

Mathlib API called (external library)

  • geom_sum_mul_neg
  • pow_lt_one₀
  • pow_pos
  • zpow_neg
  • zpow_natCast
  • 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.