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

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

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.GradientDescentBasic

Scope 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.