AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentBasic

- Actual gradient-step descent from a global quadratic upper model. Includes a zero step and signed upper-model coefficient.

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

AutoSamplingTheory/TechnicalLemmas/Analysis/GradientDescentBasic.lean:23published source at 0e31a3cda412Open detailed card