Shared descent for an actual gradient step
AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentBasic.gradient_step_descent_of_quadratic_upper_bound · theorem · Teaching coverage
Statement
Every actual gradient update obeys the displayed decrease under the global quadratic upper model and nonnegative admissible step.
All objects and hypotheses
- E is a complete real inner-product space; f:E→ℝ; α,β,h are real scalars, with h≥0 and βh≤1. The descent lemma does not use α.
- The displayed quadratic upper model holds for every x,y∈E. ∇f is Lean’s actual gradient (the Riesz representative of the totalized Fréchet derivative), not a supplied vector field.
- These are algebraic consequences of the model. No separate C¹ or C² premise is needed once the model is supplied; no claim that every arbitrary function satisfies it. The source C² Euclidean setting is a specialization.
- For every x,y: f(y)≤f(x)+⟨∇f(x),y−x⟩+(β/2)‖y−x‖².
Mathematical proof
1. Insert the actual update into the upper model
Write g=∇f(x), T(x)=x−hg. The displacement is −hg; inner-product and norm identities evaluate the model exactly.
Corresponding Lean step
inner_neg_right; inner_smul_right; real_inner_self_eq_norm_sq; norm_neg; norm_smul; sq_abs.
2. Use the step restriction with its sign
Multiply βh≤1 by h‖g‖²≥0. Substituting the result leaves half of the linear decrease.
Corresponding Lean step
mul_nonneg; sq_nonneg; mul_le_mul_of_nonneg_right; nlinarith.
Lean statement · gradient_step_descent_of_quadratic_upper_bound
Actual gradient update and the global upper-model decrease.
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 gradient_step_descent_of_quadratic_upper_bound {f : E → ℝ} {β h : ℝ}
(hh : 0 ≤ h) (hstep : β * h ≤ 1)
(hu : ∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + β / 2 * ‖y - x‖ ^ 2)
(x : E) : f (x - h • gradient f x) - f x ≤ -(h / 2) * ‖gradient f x‖ ^ 2Lean proof · gradient_step_descent_of_quadratic_upper_bound
Write g=∇f(x), T(x)=x−hg. The displacement is −hg; inner-product and norm identities evaluate the model exactly. Multiply βh≤1 by h‖g‖²≥0. Substituting the result leaves half of the linear decrease.
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 gradient_step_descent_of_quadratic_upper_bound {f : E → ℝ} {β h : ℝ}
(hh : 0 ≤ h) (hstep : β * h ≤ 1)
(hu : ∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + β / 2 * ‖y - x‖ ^ 2)
(x : E) : f (x - h • gradient f x) - f x ≤ -(h / 2) * ‖gradient f x‖ ^ 2 := by
have hu' := hu x (x - h • gradient f x)
have he : x - h • gradient f x - x = -(h • gradient f x) := by abel
rw [he, inner_neg_right, inner_smul_right, real_inner_self_eq_norm_sq,
norm_neg, norm_smul, Real.norm_eq_abs, mul_pow, sq_abs] at hu'
have hs := mul_le_mul_of_nonneg_right hstep (mul_nonneg hh (sq_nonneg ‖gradient f x‖))
nlinarith
end AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentBasicScope and omitted-condition boundaries
- This is shared optimization textbook work, not progress on the companion papers. No convexity, optimizer-existence proof or smoothness-to-upper-model theorem is claimed.
- The source prints only h≤1/β. The explicit h≥0 is necessary: for f(t)=t²/2, β=1,h=−1,x=1, descent would assert 3/2≤1/2. The reciprocal and product step restrictions agree when β>0; signed β and β=0 here are algebraic extensions.
Source and reuse
ASTIS parents called
Mathlib API called (external library)
- inner_neg_right; inner_smul_right; real_inner_self_eq_norm_sq
- norm_neg; norm_smul; sq_abs; mul_le_mul_of_nonneg_right
Mathematical sources
- Chewi Lemma3.1 — ASTIS source restatement; explicit nonnegative-step repair and algebraic Hilbert generalizations.
- Pinned Optlib convex_lipschitz — Inspected adjacent descent result needs positive step and Lipschitz gradient; external reference, no code port.
- Actual quadratic and negative-coefficient constant-objective tests — Compiled tests, 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.