Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412
ASTIS mathematical exposition

One gradient step controls comparator energy

AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentValue.gradient_step_energy_bound · theorem · Teaching coverage

Statement

For every x,z, one actual gradient step obeys the displayed distance-plus-function energy bound.

\[\begin{gathered}T(x)=x-h\nabla f(x),\\f(y)\le f(x)+\langle\nabla f(x),y-x\rangle+\frac\beta2\|y-x\|^2.\\\|T(x)-z\|^2+2h(f(T(x))-f(z))\\\le(1-\alpha h)\|x-z\|^2.\end{gathered}\]

All objects and hypotheses

  • E is a complete real inner-product space and f:E→ℝ is C¹ globally. Its gradient is the actual Riesz representative of its Fréchet derivative.
  • α,β,h are real numbers; h≥0 and βh≤1. No separate nonnegative-modulus assumption is needed by these two inequalities.
  • f is globally α-strongly convex in the chord sense with subtraction (α/2)t(1−t)‖y−x‖². The β quadratic upper model displayed below holds for every x,y in E.
  • T(x)=x−h∇f(x). The comparator z is arbitrary, so f(x)−f(z) may be negative. No minimizer is assumed or constructed.

Mathematical proof

1. Compute descent for the actual gradient step

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.

\[\begin{gathered}f(s)-f(x)\le-h\|g\|^2+\tfrac\beta2h^2\|g\|^2,\\f(s)-f(x)\le-\tfrac h2\|g\|^2.\end{gathered}\]
Corresponding Lean step

AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentBasic.gradient_step_descent_of_quadratic_upper_bound; inner_smul_right, real_inner_self_eq_norm_sq, norm_smul, mul_le_mul_of_nonneg_right.

2. Use strong first-order support at an arbitrary comparator

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.

\[f(z)\ge f(x)-\langle g,v\rangle+\tfrac\alpha2\|v\|^2.\]
Corresponding Lean step

StrongConvexFirstOrder.firstOrder_lower_bound_of_strongConvexOn; ContDiff.differentiable_one; DifferentiableAt.hasGradientAt.

3. Expand and cancel the gradient square

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.

\[\begin{gathered}\|v-hg\|^2=\|v\|^2-2h\langle g,v\rangle+h^2\|g\|^2,\\\|T(x)-z\|^2+2h(f(T(x))-f(z))\\\le(1-\alpha h)\|v\|^2.\end{gathered}\]
Corresponding Lean step

norm_sub_sq_real; inner_smul_right; real_inner_comm; norm_smul; two nonnegative multiplications and nlinarith.

Lean statement · gradient_step_energy_bound

Actual-gradient one-step arbitrary-comparator energy bound.

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

Exact module and namespace context

Lean proof · gradient_step_energy_bound

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

Scope and omitted-condition boundaries

  • This is shared optimization textbook mathematics, not companion-paper progress. C¹ on a complete real Hilbert space generalizes the section’s C² Euclidean setting. Signed α and β are explicit extensions of the nonnegative source moduli; no reciprocal of either is used. The actual comparator formulation is justified by source (3.3).
  • The source prints h≤1/β without h≥0. The latter is essential: f(t)=t²/2, α=0, β=1, x=0, z=1 and h=−1 meet the printed upper restriction, but (3.3) would assert 2≤1. The division-free βh≤1 presentation includes β=0; it agrees with the printed reciprocal restriction only for β>0.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

  • ContDiff.differentiable_one; DifferentiableAt.hasGradientAt
  • norm_sub_sq_real; inner_smul_right; real_inner_self_eq_norm_sq; norm_smul

Mathematical sources

ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.