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.
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.
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.
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.
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)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.GradientDescentRatesScope 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
- 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.
ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.