/- SamplingOptimisationGeometryBench public-dev reference.
   Reuses the existing project proof; retain LICENSE and NOTICE. -/
import AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentBasic
import Mathlib.Analysis.SpecificLimits.Basic

open Set
open scoped RealInnerProductSpace
open AutoSamplingTheory.TechnicalLemmas.Analysis
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]

example {f : E → ℝ} {α β h : ℝ} {z : E}
    (hz : IsMinOn f univ z) (hh : 0 ≤ h) (hstep : β * h ≤ 1)
    (hu : ∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + β / 2 * ‖y - x‖ ^ 2)
    (hpl : ∀ x, 2 * α * (f x - f z) ≤ ‖gradient f x‖ ^ 2)
    (x₀ : E) (N : ℕ) :
    f ((fun x => x - h • gradient f x)^[N] x₀) - f z ≤
      (1 - α * h) ^ N * (f x₀ - f z) := by
  -- Replace this comment with your proof.