PL descent gives the final-value rate

AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentPL.gradient_descent_pl_value_bound · theorem · Teaching coverage

Statement

For every initial point x₀ and N∈ℕ, actual gradient iterates obey the displayed PL value bound about a supplied global minimizer.

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‖².
• z∈E is a global minimizer: f(z)≤f(x) for all x. The displayed PL model holds globally, in the normalization 2α(f(x)−f(z))≤‖∇f(x)‖².
• x₀∈E and N∈ℕ are arbitrary; T⁰ is the identity. No convexity or nonnegative-coefficient premise is supplied.

Mathematical proof

theorem gradient_descent_pl_value_bound {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)

theorem gradient_descent_pl_value_bound {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
  let T : E → E := fun x => x - h • gradient f x
  let q : ℝ := 1 - α * h
  have hnonneg (x : E) : 0 ≤ f x - f z := sub_nonneg.mpr (hz (mem_univ x))
  have hrec (x : E) : f (T x) - f z ≤ q * (f x - f z) := by
    have hd := GradientDescentBasic.gradient_step_descent_of_quadratic_upper_bound hh hstep hu x
    have hp := mul_le_mul_of_nonneg_left (hpl x) (show 0 ≤ h / 2 by positivity)
    dsimp [T, q]
    nlinarith
  by_cases hq : 0 ≤ q
  · have hr := le_geom (u := fun n => f (T^[n] x₀) - f z) hq N (by
      intro k _
      rw [Function.iterate_succ_apply']
      exact hrec _)
    exact hr
  · have hzero (x : E) : f x - f z = 0 := by
      have hc : q * (f x - f z) ≥ 0 := (hnonneg (T x)).trans (hrec x)
      have hneg : q < 0 := lt_of_not_ge hq
      have hx := hnonneg x
      nlinarith
    change f (T^[N] x₀) - f z ≤ q ^ N * (f x₀ - f z)
    rw [hzero, hzero, mul_zero]

end AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentPL

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.
• The supplied z satisfies f(z)≤f(x) for every x. This preserves the source attainment convention; no minimizer is constructed.
• The formula permits signed α. A positive PL modulus α>0 and positive h give q<1; in the ordinary branch 0≤q<1 this is geometric decay. The theorem adds no αh≤1 restriction; negative q is necessarily a zero-gap degeneracy. h=0 and N=0 yield equality.
• Theorem3.6 has its own missing-step counterexample: f(t)=t²/2, α=β=1,h=−1,x₀=1,N=1 gives final gap 2 but proposed upper bound 1. Its source repair remains distinct from the actual compiled theorem.