The optimal uniform gradient step
AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentOptimalStep.optimal_gradient_step · theorem · Teaching coverage
Statement
The balanced positive step satisfies the displayed bound, and its factor is a lower bound for the endpoint envelope at every real step.
All objects and hypotheses
- E is a complete real inner-product space and f:E→ℝ is C² (ContDiff ℝ 2 f). ∇f is the actual Riesz gradient of f; no arbitrary gradient or Hessian field is supplied. Write T_h(x)=x−h∇f(x).
- f is globally α-strongly convex in the StrongConvexOn univ α sense, and for all x,y∈E the upper model f(y)≤f(x)+⟨∇f(x),y−x⟩+(β/2)‖y−x‖² holds. All derivatives and curvature bounds are global.
- 0≤α≤β and β>0; hence α+β>0. The optimality comparison quantifies over every real step h, while the chosen step is positive.
Mathematical proof
1. Balance the two endpoints
Let D=α+β>0 and q=(β−α)/D≥0. At h★=2/D the endpoint values are q and −q. Their maximum absolute value is q, so the preceding actual-gradient bound gives the stated two-point inequality.
Corresponding Lean step
AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentOptimalStep.gradient_step_endpoint_bound; field_simp; abs_neg; abs_of_nonneg; max_self.
2. Prove optimality of this uniform envelope
For any real h, M_h≥1−hα and M_h≥hβ−1. Multiply these inequalities by β≥0 and α≥0 respectively and add. The h terms cancel. Dividing by α+β>0 yields M_h≥q, including negative h. This is envelope minimization, not an objective-by-objective optimal-step theorem.
Corresponding Lean step
le_abs_self; neg_le_abs; mul_le_mul_of_nonneg_left; div_le_iff₀.
Lean statement · optimal_gradient_step
C² actual-gradient map, global lower curvature and quadratic upper model; explicit real parameter domains.
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 optimal_gradient_step {f : E → ℝ} {α β : ℝ}
(hf : ContDiff ℝ 2 f) (hsc : StrongConvexOn univ α f)
(hα : 0 ≤ α) (hβ : 0 < β) (hαβ : α ≤ β)
(hu : ∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + β / 2 * ‖y - x‖ ^ 2)
(x y : E) :
‖(y - (2 / (α + β)) • gradient f y) - (x - (2 / (α + β)) • gradient f x)‖ ≤
((β - α) / (α + β)) * ‖y - x‖ ∧
∀ h : ℝ, (β - α) / (α + β) ≤ max |1 - h * α| |1 - h * β|Lean proof · optimal_gradient_step
Let D=α+β>0 and q=(β−α)/D≥0. At h★=2/D the endpoint values are q and −q. Their maximum absolute value is q, so the preceding actual-gradient bound gives the stated two-point inequality. For any real h, M_h≥1−hα and M_h≥hβ−1. Multiply these inequalities by β≥0 and α≥0 respectively and add. The h terms cancel. Dividing by α+β>0 yields M_h≥q, including negative h. This is envelope minimization, not an objective-by-objective optimal-step theorem.
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 optimal_gradient_step {f : E → ℝ} {α β : ℝ}
(hf : ContDiff ℝ 2 f) (hsc : StrongConvexOn univ α f)
(hα : 0 ≤ α) (hβ : 0 < β) (hαβ : α ≤ β)
(hu : ∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + β / 2 * ‖y - x‖ ^ 2)
(x y : E) :
‖(y - (2 / (α + β)) • gradient f y) - (x - (2 / (α + β)) • gradient f x)‖ ≤
((β - α) / (α + β)) * ‖y - x‖ ∧
∀ h : ℝ, (β - α) / (α + β) ≤ max |1 - h * α| |1 - h * β| := by
have hD : 0 < α + β := add_pos_of_nonneg_of_pos hα hβ
have hq : 0 ≤ (β - α) / (α + β) := div_nonneg (sub_nonneg.mpr hαβ) hD.le
have ha : 1 - 2 / (α + β) * α = (β - α) / (α + β) := by field_simp; ring
have hb : 1 - 2 / (α + β) * β = -((β - α) / (α + β)) := by field_simp; ring
constructor
· have hc := gradient_step_endpoint_bound hf hsc (show 0 ≤ 2 / (α + β) by positivity) hu x y
simpa only [ha, hb, abs_neg, abs_of_nonneg hq, max_self] using hc
· intro h
let M := max |1 - h * α| |1 - h * β|
have ha' : 1 - h * α ≤ M := (le_abs_self _).trans (le_max_left _ _)
have hb' : -(1 - h * β) ≤ M := (neg_le_abs _).trans (le_max_right _ _)
apply (div_le_iff₀ hD).mpr
have h1 := mul_le_mul_of_nonneg_left ha' hβ.le
have h2 := mul_le_mul_of_nonneg_left hb' hα
nlinarith
end AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentOptimalStepScope and omitted-condition boundaries
- The source works in Euclidean space; the Lean theorem extends the same argument to complete real Hilbert spaces using the symmetric Rayleigh norm formula. Completeness supplies the Riesz map and the vector-valued integral.
- C² regularity supplies the actual gradient derivative, Hessian symmetry, and continuity/integrability along the closed line segment. No additional domination, measurability, boundary or supplied spectral hypothesis is assumed.
- These are textbook optimisation edges. No minimizer, N-step convergence, stochastic sampling theorem, oracle lower bound or companion-paper completion is asserted.
- For the source’s condition-number interpretation assume α>0: κ=β/α and q=(κ−1)/(κ+1)<1. At α=0 the extension gives q=1 (nonexpansive) and κ is undefined. At α=β>0 the map has zero pairwise difference; this does not identify a minimizer without further argument.
- The explicit order α≤β preserves the zero-dimensional case, where curvature inequalities alone do not imply this order. The result minimizes the endpoint upper envelope; it does not state that every individual objective has its actual smallest Lipschitz constant at h★.
Source and reuse
ASTIS parents called
Mathlib API called (external library)
- le_abs_self
- neg_le_abs
- mul_le_mul_of_nonneg_left
- div_le_iff₀
Mathematical sources
- Chewi Exercise3.2 — ASTIS-authored paraphrase and complete proof of the curvature-envelope argument.
- Actual quadratic and boundary tests — Equal and unequal moduli, actual gradients, nonexpansive zero-lower-curvature endpoint; no separate theorem credit.
ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.