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

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

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

AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentContraction.gradient_descent_distance_bound

Mathlib API called (external library)

Real.log_le_iff_le_exp
Real.exp_pos
Real.exp_add
div_le_iff₀

Mathematical sources

Chewi Theorem3.3 following rate paragraph — Exact sufficient count N>=2kappa log(R/epsilon).
Compiled quadratic consumers — Actual quadratic with alpha1,beta2; integer ceiling, zero initial distance and already accurate zero-iteration branches.

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