GradientDescentValue: mathematical reading route

Put g=∇f(x) and s=T(x)=x−hg. Apply the upper model at x,s. Since h≥0 and βh≤1, βh²‖g‖²≤h‖g‖². This proves the source Lemma3.1 descent estimate using the canonical shared descent interface. The compiled first-order support theorem follows from the source chord definition and the genuine gradient, supplied by C¹ differentiability. Set v=x−z and g=∇f(x). No minimum condition on z enters. Multiply each function inequality by 2h≥0 and insert the exact squared-distance expansion. The h²‖g‖² terms cancel. This gives the stated one-step energy inequality even when the comparator gap is negative.

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_energy_bound {f : E → ℝ} {α β h : ℝ}
    (hf : ContDiff ℝ 1 f) (hsc : StrongConvexOn univ α f)
    (hh : 0 ≤ h) (hstep : β * h ≤ 1)
    (hu : ∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + β / 2 * ‖y - x‖ ^ 2)
    (x z : E) :
    ‖x - h • gradient f x - z‖ ^ 2 + 2 * h * (f (x - h • gradient f x) - f z) ≤
      (1 - α * h) * ‖x - z‖ ^ 2 := by
  have hl := StrongConvexFirstOrder.firstOrder_lower_bound_of_strongConvexOn
    hsc (fun w _ => (hf.differentiable_one w).hasGradientAt) (mem_univ x) (mem_univ z)
  have hd := GradientDescentBasic.gradient_step_descent_of_quadratic_upper_bound hh hstep hu x
  have hn : z - x = -(x - z) := by abel
  rw [hn, inner_neg_right, norm_neg] at hl
  have hl' := mul_le_mul_of_nonneg_left hl (by positivity : 0 ≤ 2 * h)
  have hd' := mul_le_mul_of_nonneg_left hd (by positivity : 0 ≤ 2 * h)
  rw [show x - h • gradient f x - z = (x - z) - h • gradient f x by abel,
    norm_sub_sq_real, inner_smul_right, real_inner_comm (gradient f x),
    norm_smul, Real.norm_eq_abs, mul_pow, sq_abs]
  nlinarith

/-- Weighted final function gap for actual gradient-descent iterates. The
coefficient domain is explicit and includes both zero and one. -/

Exact module and namespace context

Define x_n=T^n(x₀), u_n=‖x_n−z‖², g_n=f(x_n)−f(z), and q=1−αh≥0. The one-step energy inequality gives the recurrence, and shared descent gives g_(n+1)≤g_n. The gaps themselves need not be nonnegative. Apply Mathlib’s recurrence theorem with constant coefficient q and forcing −2h g_(n+1). This theorem permits signed forcing. Constant products become powers; no inverse of q is introduced, so q=0 is admitted. For k<N, monotonicity gives g_N≤g_(k+1). Multiply by the nonpositive coefficient −2h and then the nonnegative weight q^(N−1−k). Sum, discard u_N≥0, and reverse the finite index. Write S_N=Σ_(k=0)^(N−1)q^k and R=‖x₀−z‖. This proves the final bound also for N=0.

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_descent_weighted_value_bound {f : E → ℝ} {α β h : ℝ}
    (hf : ContDiff ℝ 1 f) (hsc : StrongConvexOn univ α f)
    (hh : 0 ≤ h) (hstep : β * h ≤ 1) (hcoeff : α * h ≤ 1)
    (hu : ∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + β / 2 * ‖y - x‖ ^ 2)
    (x₀ z : E) (N : ℕ) :
    2 * h * (∑ k ∈ range N, (1 - α * h) ^ k) *
        (f ((fun x => x - h • gradient f x)^[N] x₀) - f z) ≤
      (1 - α * h) ^ N * ‖x₀ - z‖ ^ 2 := by
  let T : E → E := fun x => x - h • gradient f x
  let X : ℕ → E := fun n => T^[n] x₀
  let q : ℝ := 1 - α * h
  have hq : 0 ≤ q := sub_nonneg.mpr hcoeff
  have hX (n : ℕ) : X (n + 1) = T (X n) := Function.iterate_succ_apply' _ _ _
  have hm : Antitone (fun n => f (X n)) := by
    apply antitone_nat_of_succ_le
    intro n
    have hd := GradientDescentBasic.gradient_step_descent_of_quadratic_upper_bound hh hstep hu (X n)
    rw [hX]
    dsimp [T]
    have : 0 ≤ h / 2 * ‖gradient f (X n)‖ ^ 2 := by positivity
    linarith
  have hr (n : ℕ) (_ : 0 ≤ n) :
      ‖X (n + 1) - z‖ ^ 2 ≤ q * ‖X n - z‖ ^ 2 + (-2 * h * (f (X (n + 1)) - f z)) := by
    have he := gradient_step_energy_bound hf hsc hh hstep hu (X n) z
    rw [hX]
    dsimp [T, q]
    linarith
  have hg := discrete_gronwall_prod_general (u := fun n => ‖X n - z‖ ^ 2)
    (b := fun n => -2 * h * (f (X (n + 1)) - f z)) (c := fun _ => q) hr (fun _ _ => hq) (Nat.zero_le N)
  simp only [Finset.prod_const, Nat.card_Ico, Nat.Ico_zero_eq_range, Finset.card_range] at hg
  have hs : ∑ k ∈ range N, (-2 * h * (f (X (k + 1)) - f z)) * q ^ (N - (k + 1)) ≤
      ∑ k ∈ range N, (-2 * h * (f (X N) - f z)) * q ^ (N - (k + 1)) := by
    apply sum_le_sum
    intro k hk
    have hm' := hm (by have := mem_range.mp hk; omega : k + 1 ≤ N)
    apply mul_le_mul_of_nonneg_right _ (pow_nonneg hq _)
    have hh' : 0 ≤ 2 * h := by positivity
    nlinarith
  have hsum : (∑ k ∈ range N, q ^ (N - (k + 1))) = ∑ k ∈ range N, q ^ k := by
    rw [← sum_range_reflect (fun k => q ^ k) N]
    apply sum_congr rfl
    intro k _
    congr 1
    omega
  rw [← mul_sum, hsum] at hs
  have hu0 : X 0 = x₀ := rfl
  rw [hu0] at hg
  have huN := sq_nonneg ‖X N - z‖
  change 2 * h * (∑ k ∈ range N, q ^ k) * (f (X N) - f z) ≤ q ^ N * ‖x₀ - z‖ ^ 2
  nlinarith

end AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentValue

Exact module and namespace context