GradientDescentOptimalStep: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

The endpoint bound for a gradient update
The optimal uniform gradient step

ASTIS mathematical exposition

The endpoint bound for a gradient update

AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentOptimalStep.gradient_step_endpoint_bound · theorem · Teaching coverage

Statement

Every nonnegative gradient step satisfies the displayed pairwise Lipschitz bound.

\[\forall x,y\in E,\quad\|T_h(y)-T_h(x)\|\le\max\{|1-h\alpha|,|1-h\beta|\}\,\|y-x\|.\]

All objects and hypotheses

E is a complete real inner-product space and f:E→ℝ is C² (ContDiff ℝ 2 f). ∇f is the actual Riesz gradient of f; no arbitrary gradient or Hessian field is supplied. Write T_h(x)=x−h∇f(x).
f is globally α-strongly convex in the StrongConvexOn univ α sense, and for all x,y∈E the upper model f(y)≤f(x)+⟨∇f(x),y−x⟩+(β/2)‖y−x‖² holds. All derivatives and curvature bounds are global.
α,β∈ℝ may be signed; h≥0. The simultaneous global curvature models are assumed, not inferred for incompatible parameters.

Mathematical proof

1. Recover the actual Hessian interval

\[\alpha\|v\|^2\le\langle H_zv,v\rangle=D^2f(z)[v,v]\le\beta\|v\|^2.\]

Corresponding Lean step

StrongConvexFirstOrder.gradient_inner_lower_bound_of_strongConvexOn; ConvexityC2.gradient_mono_iff_fderiv2_lower; SmoothnessEquivalences.upper_model_iff_fderiv2_upper; toDual_symm_apply.

2. Bound the symmetric derivative of the update

Differentiate T_h to obtain A_z=I−hH_z. C² symmetry makes A_z symmetric. Multiplying the Hessian inequalities by h≥0 puts the Rayleigh value of every nonzero vector in [1−hβ,1−hα]. Its absolute value is at most the maximum of the endpoint absolute values. Mathlib’s supremum formula bounds the operator norm; the zero vector is treated separately. In this supremum the Rayleigh quotient is assigned value zero at v=0, including when E is the zero space.

\[\|DT_h(z)\|_{\rm op}=\sup_v\left|\frac{\langle (I-hH_z)v,v\rangle}{\|v\|^2}\right|\le M_h,\quad M_h=\max\{|1-h\alpha|,|1-h\beta|\}.\]

Corresponding Lean step

ContDiffAt.isSymmSndFDerivAt; ContinuousLinearMap.norm_eq_iSup_rayleighQuotient; HasFDerivAt.comp; HasFDerivAt.sub; HasFDerivAt.const_smul.

3. Integrate along the actual segment

Set v=y−x. The derivative of t↦T_h(x+tv) is A_(x+tv)v and is continuous. The vector fundamental theorem of calculus expresses the update difference as its integral over [0,1]. Bound the integral norm by the uniform derivative bound times the segment length.

\[\|T_h(y)-T_h(x)\|=\left\|\int_0^1 A_{x+t(y-x)}(y-x)\,dt\right\|\le\int_0^1 M_h\|y-x\|\,dt=M_h\|y-x\|.\]

Corresponding Lean step

intervalIntegral.integral_eq_sub_of_hasDerivAt; intervalIntegral.norm_integral_le_of_norm_le_const; ContinuousLinearMap.le_opNorm; ContDiff.continuous_fderiv.

Lean statement · gradient_step_endpoint_bound

C² actual-gradient map, global lower curvature and quadratic upper model; explicit real parameter domains.

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_endpoint_bound {f : E → ℝ} {α β h : ℝ}
    (hf : ContDiff ℝ 2 f) (hsc : StrongConvexOn univ α f) (hh : 0 ≤ h)
    (hu : ∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + β / 2 * ‖y - x‖ ^ 2)
    (x y : E) :
    ‖(y - h • gradient f y) - (x - h • gradient f x)‖ ≤
      max |1 - h * α| |1 - h * β| * ‖y - x‖

Exact module and namespace context

Lean proof · gradient_step_endpoint_bound

Apply the strong-convex first-order gradient monotonicity theorem and its C² Hessian equivalence. The upper-model equivalence gives the opposite inequality. The Riesz map turns D²f(z) into a continuous linear operator H_z with the displayed quadratic form. Differentiate T_h to obtain A_z=I−hH_z. C² symmetry makes A_z symmetric. Multiplying the Hessian inequalities by h≥0 puts the Rayleigh value of every nonzero vector in [1−hβ,1−hα]. Its absolute value is at most the maximum of the endpoint absolute values. Mathlib’s supremum formula bounds the operator norm; the zero vector is treated separately. In this supremum the Rayleigh quotient is assigned value zero at v=0, including when E is the zero space. Set v=y−x. The derivative of t↦T_h(x+tv) is A_(x+tv)v and is continuous. The vector fundamental theorem of calculus expresses the update difference as its integral over [0,1]. Bound the integral norm by the uniform derivative bound times the segment length.

theorem gradient_step_endpoint_bound {f : E → ℝ} {α β h : ℝ}
    (hf : ContDiff ℝ 2 f) (hsc : StrongConvexOn univ α f) (hh : 0 ≤ h)
    (hu : ∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + β / 2 * ‖y - x‖ ^ 2)
    (x y : E) :
    ‖(y - h • gradient f y) - (x - h • gradient f x)‖ ≤
      max |1 - h * α| |1 - h * β| * ‖y - x‖ := by
  let M := max |1 - h * α| |1 - h * β|
  have hM : 0 ≤ M := (abs_nonneg _).trans (le_max_left _ _)
  have hlo := (ConvexityC2.gradient_mono_iff_fderiv2_lower hf).mp (fun a b =>
    StrongConvexFirstOrder.gradient_inner_lower_bound_of_strongConvexOn hsc
      (fun z _ => ((hf.of_le (by norm_num) : ContDiff ℝ 1 f).differentiable_one z).hasGradientAt)
      (mem_univ a) (mem_univ b))
  have hup := (SmoothnessEquivalences.upper_model_iff_fderiv2_upper hf).mp hu
  let R : (E →L[ℝ] ℝ) →L[ℝ] E :=
    { toFun := (toDual ℝ E).symm
      map_add' := (toDual ℝ E).symm.map_add
      map_smul' := by intros; simp
      cont := (toDual ℝ E).symm.continuous }
  let H (z : E) : E →L[ℝ] E := R.comp (fderiv ℝ (fderiv ℝ f) z)
  let A (z : E) : E →L[ℝ] E := ContinuousLinearMap.id ℝ E - h • H z
  let T : E → E := fun z => z - h • gradient f z
  have hfd : ContDiff ℝ 1 (fderiv ℝ f) := hf.fderiv_right (by norm_num)
  have hgrad (z : E) : HasFDerivAt (gradient f) (H z) z :=
    R.hasFDerivAt.comp z (hfd.differentiable_one z).hasFDerivAt
  have hTd (z : E) : HasFDerivAt T (A z) z :=
    (hasFDerivAt_id z).sub ((hgrad z).const_smul h)
  have hT : ContDiff ℝ 1 T := contDiff_id.sub ((R.contDiff.comp hfd).const_smul h)
  have hinner (z v w : E) : inner ℝ (H z v) w = (fderiv ℝ (fderiv ℝ f) z v) w :=
    toDual_symm_apply
  have hsym (z : E) : (A z).IsSymmetric := by
    intro v w
    change inner ℝ (v - h • H z v) w = inner ℝ v (w - h • H z w)
    rw [inner_sub_left, inner_sub_right, real_inner_smul_left, inner_smul_right]
    have hr : inner ℝ v (H z w) = (fderiv ℝ (fderiv ℝ f) z w) v :=
      (real_inner_comm v (H z w)).symm.trans (hinner z w v)
    rw [hinner, hr]
    rw [hf.contDiffAt.isSymmSndFDerivAt (by norm_num) v w]
  have hnorm (z : E) : ‖A z‖ ≤ M := by
    rw [(A z).norm_eq_iSup_rayleighQuotient (hsym z)]
    apply ciSup_le
    intro v
    change |inner ℝ (A z v) v / ‖v‖ ^ 2| ≤ M
    by_cases hv : v = 0
    · simp [hv]
      exact hM
    · simp only [abs_div, abs_pow, abs_norm]
      apply (div_le_iff₀ (sq_pos_of_pos (norm_pos_iff.mpr hv))).mpr
      change |inner ℝ (v - h • H z v) v| ≤ M * ‖v‖ ^ 2
      rw [inner_sub_left, real_inner_smul_left, real_inner_self_eq_norm_sq, hinner]
      have hl := mul_le_mul_of_nonneg_left (hlo z v) hh
      have hu' := mul_le_mul_of_nonneg_left (hup z v) hh
      have hleft : 1 - h * α ≤ M := (le_abs_self _).trans (le_max_left _ _)
      have hright : -(1 - h * β) ≤ M := (neg_le_abs _).trans (le_max_right _ _)
      have hleft' := mul_le_mul_of_nonneg_right hleft (sq_nonneg ‖v‖)
      have hright' := mul_le_mul_of_nonneg_right hright (sq_nonneg ‖v‖)
      exact abs_le.mpr ⟨by nlinarith, by nlinarith⟩
  let v := y - x
  have hpath (t : ℝ) : HasDerivAt (fun s : ℝ => T (x + s • v)) (A (x + t • v) v) t := by
    convert (hTd (x + t • v)).comp_hasDerivAt t
      (((hasDerivAt_id t).smul_const v).const_add x) using 1 <;> simp [Function.comp_def]
  have hc : Continuous (fun t : ℝ => A (x + t • v) v) := by
    have hA : A = fderiv ℝ T := funext (fun z => (hTd z).fderiv.symm)
    rw [hA]
    exact ((hT.continuous_fderiv (by norm_num)).comp
      (continuous_const.add (continuous_id.smul continuous_const))).clm_apply continuous_const
  have hFTC : (∫ t : ℝ in 0..1, A (x + t • v) v) = T y - T x := by
    simpa [v] using intervalIntegral.integral_eq_sub_of_hasDerivAt
      (fun t _ => hpath t) (hc.intervalIntegrable 0 1)
  change ‖T y - T x‖ ≤ M * ‖v‖
  rw [← hFTC]
  simpa using intervalIntegral.norm_integral_le_of_norm_le_const (a := (0 : ℝ)) (b := 1)
    (fun t _ => ((A (x + t • v)).le_opNorm v).trans
      (mul_le_mul_of_nonneg_right (hnorm _) (norm_nonneg v)))

/-- The step `2/(α+β)` gives the sharp uniform curvature-envelope contraction.
Its factor minimizes the endpoint max-envelope over every real step.
The `α=0` boundary is nonexpansive, and `α=β` is retained. -/

Exact module and namespace context

Scope and omitted-condition boundaries

The source works in Euclidean space; the Lean theorem extends the same argument to complete real Hilbert spaces using the symmetric Rayleigh norm formula. Completeness supplies the Riesz map and the vector-valued integral.
C² regularity supplies the actual gradient derivative, Hessian symmetry, and continuity/integrability along the closed line segment. No additional domination, measurability, boundary or supplied spectral hypothesis is assumed.
These are textbook optimisation edges. No minimizer, N-step convergence, stochastic sampling theorem, oracle lower bound or companion-paper completion is asserted.
This is the Exercise3.2 derivative/integral proof component before step selection. It does not by itself assert contraction: M_h can exceed one. It includes h=0 and allows signed curvature bounds.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

toDual_symm_apply
ContDiffAt.isSymmSndFDerivAt
ContinuousLinearMap.norm_eq_iSup_rayleighQuotient
intervalIntegral.integral_eq_sub_of_hasDerivAt
intervalIntegral.norm_integral_le_of_norm_le_const
ContinuousLinearMap.le_opNorm

Mathematical sources

Chewi Exercise3.2 — ASTIS-authored paraphrase and complete proof of the curvature-envelope argument.
Actual quadratic and boundary tests — Equal and unequal moduli, actual gradients, nonexpansive zero-lower-curvature endpoint; no separate theorem credit.

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

ASTIS mathematical exposition

The optimal uniform gradient step

AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentOptimalStep.optimal_gradient_step · theorem · Teaching coverage

Statement

The balanced positive step satisfies the displayed bound, and its factor is a lower bound for the endpoint envelope at every real step.

\[h_\star=\frac2{\alpha+\beta},\quad q=\frac{\beta-\alpha}{\alpha+\beta}:\qquad\|T_{h_\star}(y)-T_{h_\star}(x)\|\le q\|y-x\|,\quad\forall h\in\mathbb R,\ q\le\max\{|1-h\alpha|,|1-h\beta|\}.\]

All objects and hypotheses

E is a complete real inner-product space and f:E→ℝ is C² (ContDiff ℝ 2 f). ∇f is the actual Riesz gradient of f; no arbitrary gradient or Hessian field is supplied. Write T_h(x)=x−h∇f(x).
f is globally α-strongly convex in the StrongConvexOn univ α sense, and for all x,y∈E the upper model f(y)≤f(x)+⟨∇f(x),y−x⟩+(β/2)‖y−x‖² holds. All derivatives and curvature bounds are global.
0≤α≤β and β>0; hence α+β>0. The optimality comparison quantifies over every real step h, while the chosen step is positive.

Mathematical proof

1. Balance the two endpoints

Let D=α+β>0 and q=(β−α)/D≥0. At h★=2/D the endpoint values are q and −q. Their maximum absolute value is q, so the preceding actual-gradient bound gives the stated two-point inequality.

\[1-h_\star\alpha=q,\quad 1-h_\star\beta=-q,\qquad\|T_{h_\star}(y)-T_{h_\star}(x)\|\le q\|y-x\|.\]

Corresponding Lean step

AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentOptimalStep.gradient_step_endpoint_bound; field_simp; abs_neg; abs_of_nonneg; max_self.

2. Prove optimality of this uniform envelope

For any real h, M_h≥1−hα and M_h≥hβ−1. Multiply these inequalities by β≥0 and α≥0 respectively and add. The h terms cancel. Dividing by α+β>0 yields M_h≥q, including negative h. This is envelope minimization, not an objective-by-objective optimal-step theorem.

\[(\alpha+\beta)M_h\ge\beta(1-h\alpha)+\alpha(h\beta-1)=\beta-\alpha\quad\Longrightarrow\quad M_h\ge q.\]

Corresponding Lean step

le_abs_self; neg_le_abs; mul_le_mul_of_nonneg_left; div_le_iff₀.

Lean statement · optimal_gradient_step

C² actual-gradient map, global lower curvature and quadratic upper model; explicit real parameter domains.

theorem optimal_gradient_step {f : E → ℝ} {α β : ℝ}
    (hf : ContDiff ℝ 2 f) (hsc : StrongConvexOn univ α f)
    (hα : 0 ≤ α) (hβ : 0 < β) (hαβ : α ≤ β)
    (hu : ∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + β / 2 * ‖y - x‖ ^ 2)
    (x y : E) :
    ‖(y - (2 / (α + β)) • gradient f y) - (x - (2 / (α + β)) • gradient f x)‖ ≤
        ((β - α) / (α + β)) * ‖y - x‖ ∧
      ∀ h : ℝ, (β - α) / (α + β) ≤ max |1 - h * α| |1 - h * β|

Exact module and namespace context

Lean proof · optimal_gradient_step

Let D=α+β>0 and q=(β−α)/D≥0. At h★=2/D the endpoint values are q and −q. Their maximum absolute value is q, so the preceding actual-gradient bound gives the stated two-point inequality. For any real h, M_h≥1−hα and M_h≥hβ−1. Multiply these inequalities by β≥0 and α≥0 respectively and add. The h terms cancel. Dividing by α+β>0 yields M_h≥q, including negative h. This is envelope minimization, not an objective-by-objective optimal-step theorem.

theorem optimal_gradient_step {f : E → ℝ} {α β : ℝ}
    (hf : ContDiff ℝ 2 f) (hsc : StrongConvexOn univ α f)
    (hα : 0 ≤ α) (hβ : 0 < β) (hαβ : α ≤ β)
    (hu : ∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + β / 2 * ‖y - x‖ ^ 2)
    (x y : E) :
    ‖(y - (2 / (α + β)) • gradient f y) - (x - (2 / (α + β)) • gradient f x)‖ ≤
        ((β - α) / (α + β)) * ‖y - x‖ ∧
      ∀ h : ℝ, (β - α) / (α + β) ≤ max |1 - h * α| |1 - h * β| := by
  have hD : 0 < α + β := add_pos_of_nonneg_of_pos hα hβ
  have hq : 0 ≤ (β - α) / (α + β) := div_nonneg (sub_nonneg.mpr hαβ) hD.le
  have ha : 1 - 2 / (α + β) * α = (β - α) / (α + β) := by field_simp; ring
  have hb : 1 - 2 / (α + β) * β = -((β - α) / (α + β)) := by field_simp; ring
  constructor
  · have hc := gradient_step_endpoint_bound hf hsc (show 0 ≤ 2 / (α + β) by positivity) hu x y
    simpa only [ha, hb, abs_neg, abs_of_nonneg hq, max_self] using hc
  · intro h
    let M := max |1 - h * α| |1 - h * β|
    have ha' : 1 - h * α ≤ M := (le_abs_self _).trans (le_max_left _ _)
    have hb' : -(1 - h * β) ≤ M := (neg_le_abs _).trans (le_max_right _ _)
    apply (div_le_iff₀ hD).mpr
    have h1 := mul_le_mul_of_nonneg_left ha' hβ.le
    have h2 := mul_le_mul_of_nonneg_left hb' hα
    nlinarith

end AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentOptimalStep

Exact module and namespace context

Scope and omitted-condition boundaries

The source works in Euclidean space; the Lean theorem extends the same argument to complete real Hilbert spaces using the symmetric Rayleigh norm formula. Completeness supplies the Riesz map and the vector-valued integral.
C² regularity supplies the actual gradient derivative, Hessian symmetry, and continuity/integrability along the closed line segment. No additional domination, measurability, boundary or supplied spectral hypothesis is assumed.
These are textbook optimisation edges. No minimizer, N-step convergence, stochastic sampling theorem, oracle lower bound or companion-paper completion is asserted.
For the source’s condition-number interpretation assume α>0: κ=β/α and q=(κ−1)/(κ+1)<1. At α=0 the extension gives q=1 (nonexpansive) and κ is undefined. At α=β>0 the map has zero pairwise difference; this does not identify a minimizer without further argument.
The explicit order α≤β preserves the zero-dimensional case, where curvature inequalities alone do not imply this order. The result minimizes the endpoint upper envelope; it does not state that every individual objective has its actual smallest Lipschitz constant at h★.

Source and reuse

ASTIS parents called

AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentOptimalStep.gradient_step_endpoint_bound

Mathlib API called (external library)

le_abs_self
neg_le_abs
mul_le_mul_of_nonneg_left
div_le_iff₀

Mathematical sources

Chewi Exercise3.2 — ASTIS-authored paraphrase and complete proof of the curvature-envelope argument.
Actual quadratic and boundary tests — Equal and unequal moduli, actual gradients, nonexpansive zero-lower-curvature endpoint; no separate theorem credit.

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