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

GradientDescentComplexity: 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. A logarithmic iteration budget gives distance accuracy
ASTIS mathematical exposition

A logarithmic iteration budget gives distance accuracy

AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentComplexity.distance_le_of_log_bound · theorem · Teaching coverage

Statement

E is a complete real inner-product space; f:E→R is continuously Frechet differentiable. Its gradient is its actual Riesz gradient. Alpha, beta and epsilon are strictly positive. The objective is alpha-strongly convex on E, with the alpha/2 quadratic convention. For every x,y, f(y)<=f(x)+<gradient f(x),y-x>+(beta/2)||y-x||². This is the source smoothness upper model. A global minimizer xstar is supplied. The initial point x0 is arbitrary and N is a natural number, including zero. X_N is exactly N iterations of x ↦ x-beta⁻¹ gradient f(x). Write R=||x0-xstar||. If R>0, assume 2(beta/alpha)log(R/epsilon)<=N. When R=0 no logarithmic threshold is required. Then the actual final iterate has distance at most epsilon from xstar.

\[\begin{gathered}X_N=(\mathrm{id}-\beta^{-1}\nabla f)^N(x_0),\quad R=\|x_0-x_\star\|,\\\bigl(R>0\Rightarrow N\ge2(\beta/\alpha)\log(R/\varepsilon)\bigr)\quad\Longrightarrow\quad\|X_N-x_\star\|\le\varepsilon.\end{gathered}\]

All objects and hypotheses

  • E is a complete real inner-product space; f:E→R is continuously Frechet differentiable. Its gradient is its actual Riesz gradient.
  • Alpha, beta and epsilon are strictly positive. The objective is alpha-strongly convex on E, with the alpha/2 quadratic convention.
  • For every x,y, f(y)<=f(x)+<gradient f(x),y-x>+(beta/2)||y-x||². This is the source smoothness upper model.
  • A global minimizer xstar is supplied. The initial point x0 is arbitrary and N is a natural number, including zero. X_N is exactly N iterations of x ↦ x-beta⁻¹ gradient f(x).
  • Write R=||x0-xstar||. If R>0, assume 2(beta/alpha)log(R/epsilon)<=N. When R=0 no logarithmic threshold is required.

Mathematical proof

1. Use the actual exponential contraction

Apply the existing distance theorem at the positive step h=1/beta. Its first conclusion bounds the actual iterate by the geometric factor; compose it with the second conclusion to obtain the exponential bound.

\[\|X_N-x_\star\|\le e^{-\alpha N/(2\beta)}R.\]
Corresponding Lean step

GradientDescentContraction.gradient_descent_distance_bound; compose its two inequalities with trans.

2. Separate the stationary initial point

If R=0, the exponential bound has zero right-hand side. Thus every iterate has zero distance and meets any positive tolerance. This branch uses neither a real logarithm at zero nor a positive iteration count.

\[R=0\quad\Longrightarrow\quad\|X_N-x_\star\|=0\le\varepsilon.\]
Corresponding Lean step

Case split on the initial norm; simplify the existing bound.

3. Invert the exponential estimate on its positive domain

For R>0, the ratio R/epsilon is positive. Multiply the threshold by alpha/beta>0 and divide by two. The log comparison gives R/epsilon<=exp(alpha N/(2beta)). Multiply by exp(-alpha N/(2beta)) and then by epsilon>0; the two exponential factors cancel. Combining with the first step proves the accuracy bound.

\[\log(R/\varepsilon)\le\frac{\alpha N}{2\beta}\ \Longrightarrow\ \frac R\varepsilon\le e^{\alpha N/(2\beta)}\ \Longrightarrow\ e^{-\alpha N/(2\beta)}R\le\varepsilon.\]
Corresponding Lean step

Real.log_le_iff_le_exp, Real.exp_pos, Real.exp_add and div_le_iff₀; positive alpha and beta justify reciprocal cancellation.

Lean statement · distance_le_of_log_bound

Positive-domain logarithmic budget for actual gradient iterates.

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 distance_le_of_log_bound {f : E → ℝ} {α β ε : ℝ}
    (hf : ContDiff ℝ 1 f) (hsc : StrongConvexOn univ α f)
    (hα : 0 < α) (hβ : 0 < β) (hε : 0 < ε)
    (hu : ∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y-x) + β/2*‖y-x‖^2)
    {xstar : E} (hmin : IsMinOn f univ xstar) (x₀ : E) (N : ℕ)
    (hN : 0 < ‖x₀-xstar‖ → 2 * (β / α) * Real.log (‖x₀-xstar‖ / ε) ≤ (N : ℝ)) :
    ‖(fun x => x - β⁻¹ • gradient f x)^[N] x₀ - xstar‖ ≤ ε

Exact module and namespace context

Lean proof · distance_le_of_log_bound

Apply the existing distance theorem at the positive step h=1/beta. Its first conclusion bounds the actual iterate by the geometric factor; compose it with the second conclusion to obtain the exponential bound. If R=0, the exponential bound has zero right-hand side. Thus every iterate has zero distance and meets any positive tolerance. This branch uses neither a real logarithm at zero nor a positive iteration count. For R>0, the ratio R/epsilon is positive. Multiply the threshold by alpha/beta>0 and divide by two. The log comparison gives R/epsilon<=exp(alpha N/(2beta)). Multiply by exp(-alpha N/(2beta)) and then by epsilon>0; the two exponential factors cancel. Combining with the first step proves the accuracy 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 distance_le_of_log_bound {f : E → ℝ} {α β ε : ℝ}
    (hf : ContDiff ℝ 1 f) (hsc : StrongConvexOn univ α f)
    (hα : 0 < α) (hβ : 0 < β) (hε : 0 < ε)
    (hu : ∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y-x) + β/2*‖y-x‖^2)
    {xstar : E} (hmin : IsMinOn f univ xstar) (x₀ : E) (N : ℕ)
    (hN : 0 < ‖x₀-xstar‖ → 2 * (β / α) * Real.log (‖x₀-xstar‖ / ε) ≤ (N : ℝ)) :
    ‖(fun x => x - β⁻¹ • gradient f x)^[N] x₀ - xstar‖ ≤ ε := by
  have hi := GradientDescentContraction.gradient_descent_distance_bound hf hsc
    hα.le hβ.le (inv_nonneg.mpr hβ.le) (by simp [ne_of_gt hβ]) hu hmin x₀ N
  have he := hi.1.trans hi.2
  by_cases hR : ‖x₀-xstar‖ = 0
  · simpa [hR] using he.trans (by simpa [hR] using hε.le)
  · have hRp : 0 < ‖x₀-xstar‖ := lt_of_le_of_ne (norm_nonneg _) (Ne.symm hR)
    have ht := mul_le_mul_of_nonneg_left (hN hRp) (div_nonneg hα.le hβ.le)
    have hc : (α / β) * (2 * (β / α) * Real.log (‖x₀-xstar‖ / ε)) =
        2 * Real.log (‖x₀-xstar‖ / ε) := by field_simp
    rw [hc] at ht
    have hl : Real.log (‖x₀-xstar‖ / ε) ≤ α * β⁻¹ * N / 2 := by
      rw [div_eq_mul_inv α β] at ht
      nlinarith [ht]
    have hex := (Real.log_le_iff_le_exp (div_pos hRp hε)).mp hl
    have hb : Real.exp (-(α * β⁻¹ * N) / 2) * ‖x₀-xstar‖ ≤ ε := by
      have hm := mul_le_mul_of_nonneg_left hex (le_of_lt (Real.exp_pos (-(α * β⁻¹ * N) / 2)))
      have hid : Real.exp (-(α * β⁻¹ * N) / 2) * Real.exp (α * β⁻¹ * N / 2) = 1 := by
        rw [← Real.exp_add]; ring_nf; exact Real.exp_zero
      rw [hid] at hm
      have hh := (div_le_iff₀ hε).mp (show (Real.exp (-(α * β⁻¹ * N) / 2) * ‖x₀-xstar‖) / ε ≤ 1 by simpa [mul_div_assoc] using hm)
      simpa using hh
    exact he.trans hb

end AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentComplexity

Exact module and namespace context

Scope and omitted-condition boundaries

  • This closes the logarithmic-complexity obligation of Theorem3.3 by integrating the existing actual-iterate contraction; it does not reprove that contraction. Earlier binding-local statements that exclude complexity retain their historical scope.
  • C1 on a complete real Hilbert space generalizes the source C2 Euclidean setting. The explicit quadratic upper model is sufficient; no Hessian or finite dimension is used.
  • The source condition number is beta/alpha. Alpha<=beta is not needed as an additional hypothesis: the parent theorem handles a singleton space too. On the ordinary nontrivial source setting the usual compatible-modulus regime is recovered.
  • Positive moduli and positive accuracy expose the denominator and logarithm domains. R=0 is treated without log0; for 0<R<=epsilon the threshold is nonpositive, so N=0 is allowed.
  • The sufficient integer budget can be the natural ceiling of the real threshold when R>0, and zero when R=0. The compiled quadratic consumer also uses Lean totalized log0 inside its ceiling expression; its zero-radius proof is independent of that expression. No minimality or lower complexity bound is claimed.
  • A minimizer is assumed, not constructed. No full Table1, Chapter3 exercises, Riemannian or stochastic convergence, or companion-paper result is claimed.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

  • Real.log_le_iff_le_exp
  • Real.exp_pos
  • Real.exp_add
  • div_le_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.