Bench / optimisation

sogb-029 · public-dev · editorial and formal status separate

Chewi Optimization Exercise 3.2: the balanced gradient step

Optimisation · natural-language: L3 (author-assigned; calibration pending)

Numbered textbook exercise · Lectures on Optimization · Exercise 3.2

Original exercise, all requested parts and exact Lean scope

Sinho Chewi · arXiv:2605.07006v1 · printed p.23 / PDF p.23

Original source page · Numbered exercise directory

original faithful mathematical restatement; not reproduced source prose

Original exercise · faithful ASTIS restatement

For an \(α\)-convex and \(β\)-smooth \(C^{2}\) Euclidean objective, apply the fundamental theorem of calculus to \(T_{h}=id-h\nabla f\) along the segment between two points. Bound the eigenvalues of \(DT_{h}\) to obtain its operator norm bound and show that \(h=2/(α+β)\) minimizes the resulting bound. The resulting factor is \((κ-1)/(κ+1)\), where \(κ=β/α\), improving the preceding gradient-descent estimate.

The surrounding section works with \(C^{2}\) Euclidean objectives, an \(α\)-strong-convexity lower bound and \(β\)-smoothness upper bound.

The condition-number contraction formula is used in the positive-curvature regime \(0<α\le β\); \(κ=β/α\). Step h is a nonnegative gradient-descent step in the derivative-bound argument.

Requested parts and owned answers

Derive the endpoint Lipschitz bound from the actual Hessian and segment integral
AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentOptimalStep.gradient_step_endpoint_bound
Select the balanced step and prove minimality of its curvature envelope
AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentOptimalStep.optimal_gradient_step

Chapter 3 explicitly assumes \(C^{2}\) regularity. The condition-number interpretation uses \(0<α\le β\) and \(κ=β/α\).

The owned APIs generalize Euclidean space to complete real Hilbert spaces, and retain signed-modulus or \(α=0\) intermediate extensions. Those are disclosed API generalizations, not changes to the source exercise.

The answer minimizes a uniform curvature-endpoint bound, not the actual optimal Lipschitz constant of each objective.

Remaining formal boundary

The source's informal large-condition-number iteration-complexity comparison is contextual commentary, not an output of the two named owned declarations.

The finite-dimensional eigenvalue presentation and \(κ\) notation are explained in the mathematical answer; the actual owned proofs use the symmetric Rayleigh norm formula and the equivalent \((β-α)/(α+β)\) expression. No separate eigenvalue-list or asymptotic-complexity declaration is claimed.

No current aggregate owned-answer build receipt is recorded in this build. This is owned core-answer reuse, not a new proof, an equivalent Lean challenge or full textbook certification.

The source has an arXiv non-exclusive distribution grant. No blanket source-text/solution-manual ML reuse license is inferred; only original mathematical restatement, original solutions and bibliographic correspondence enter the Bench. The PDF/render stays outside ML exports.

Why this difficulty?

Solve a real numbered textbook exercise by combining the actual Hessian interval, a genuine derivative/segment integral and a two-endpoint scalar minimax argument. Distinguish a uniform class bound from an objective-specific optimum. This is a multi-step graduate-course proof, not a research-level difficulty or model-calibration claim.

Editorial review and exact formal-coverage boundary

AI editorial review accepted after a separately reviewed correction. This is not canonical theorem publication, full Lean coverage or empirical difficulty calibration.

There is still no aligned fixed Lean QA view for this exercise. Existing owned-answer declarations and the displayed supporting module are not converted into an aligned challenge or whole-exercise formalization by this rubric repair.
This independent audit recomputes content/context hashes and checks the scoring mathematics; it does not run Lean or issue a new compiler, source-theorem or publication certificate.
The unchanged coverage boundary does not add separate compiled eigenvalue-list, condition-number-notation, loose-curvature-label example, minimizer, iterate-convergence or asymptotic-complexity claims. Source commentary and broader API specializations retain their existing disclosed status.

Content-bound review status and evidence hashes · Independent reports and frozen inputs. Historical rejected wording is audit material, not training gold.

Assumptions and conventions

This is an original faithful reformulation of Sinho Chewi, Lectures on Optimization, arXiv:2605.07006v1, Chapter 3, Exercise 3.2, printed/PDF p.23. The chapter explicitly works with \(C^{2}\) functions; the condition-number regime uses \(0<α\le β\).
Let \(f:\mathbb{R}^{d}\to \mathbb{R}\) be \(C^{2}\) and globally \(α\)-convex and \(β\)-smooth, with the quadratic-model normalization \(α/2\) and \(β/2\). Equivalently under this regularity, \(αI\preceq \nabla ^{2}f(z)\preceq βI\) for every z. The order \(α\le β\) is explicit rather than inferred in a zero-dimensional space.
For \(h\ge 0\) define \(T_{h}(x)=x-h\nabla f(x)\), and write \(κ=β/α\). No minimizer or iterate convergence hypothesis is supplied. The target is a pairwise one-step bound and the optimal uniform curvature-endpoint envelope.

Natural-language question

Solve Exercise 3.2 in the positive-curvature regime. Use the genuine derivative of \(T_{h}\), bound its eigenvalues and operator norm, then justify the vector fundamental theorem of calculus along the segment from x to y. Find the step minimizing the resulting endpoint bound and obtain the factor \((κ-1)/(κ+1)\). Prove minimality of that bound, not merely the value at a proposed step, and explain what is—and is not—being optimized.

Reference mathematical proof

\(C^{2}\) regularity makes the actual Hessian \(H(z)=\nabla ^{2}f(z)\) symmetric and continuous. The convexity/smoothness models yield \(αI\preceq H(z)\preceq βI\). These are genuine derivative statements, not an interpretation of the fallback value of a totalized derivative. They also ensure continuous segment derivatives for the upcoming integral.
The actual derivative is \(DT_{h}(z)=I-hH(z)\). For \(h\ge 0\) and any eigenvalue \(λ\) of H(z), \(α\le λ\le β\) gives \[1-h\beta\le1-h\lambda\le1-h\alpha.\] Since the derivative is symmetric, its operator norm is bounded by \[M(h):=\max\{|1-h\alpha|,|1-h\beta|\}.\] In finite dimensions this follows from orthogonal diagonalization. The existing Hilbert-space Lean proof uses the equivalent symmetric Rayleigh-quotient norm bound rather than constructing an eigenvalue list.
Put \(v=y-x\) and \(z(t)=x+tv\). The chain rule gives \(dT_{h}(z(t))/dt=DT_{h}(z(t))v\). This derivative is continuous on [0,1], so it is Bochner integrable and the vector FTC applies: \[T_h(y)-T_h(x)=\int_0^1DT_h(x+tv)v\,dt.\] Taking norms and using the uniform operator bound yields \[\|T_h(y)-T_h(x)\|\le M(h)\|y-x\|.\] The case \(x=y\) is included; no division by \(\|y-x\|\) is needed.
Because \(α+β>0\), take \(h★=2/(α+β)\) and \(q=(β-α)/(α+β)\ge 0\). Direct algebra gives \[\begin{gathered}1-h_\star\alpha=q,\\1-h_\star\beta=-q.\end{gathered}\] Thus \(M(h★)=q\), and the preceding estimate proves the pairwise bound at that step.
To show global optimality of the endpoint envelope, fix any real h and let \(M=M(h)\). The elementary inequalities \(1-hα\le M\) and \(hβ-1\le M\) can be multiplied by the nonnegative weights \(β\) and \(α\). Their sum gives \[\beta-\alpha=\beta(1-h\alpha)+\alpha(h\beta-1)\le(\alpha+\beta)M.\] Divide by \(α+β>0\) to obtain \(q\le M(h)\). Hence h★ achieves the smallest endpoint bound, even when the scalar comparison is made over every real h; in particular it is optimal among nonnegative steps.
Since \(α>0\), \(κ=β/α\) is well-defined and \(κ\ge 1\). Dividing numerator and denominator of q by \(α\) gives \[\begin{gathered}q=\frac{\kappa-1}{\kappa+1},\\\|T_{h_\star}(y)-T_{h_\star}(x)\|\le\frac{\kappa-1}{\kappa+1}\|y-x\|.\end{gathered}\] Also \(q<1\), so this is a contraction in the stated source regime. When \(α=β>0\) it gives \(q=0\) and a constant update map, without needing a minimizer premise.
The optimization concerns the uniform bound derived from the curvature interval, not the actual best step for each individual objective. For example, if \(f(x)=β\|x\|^{2}/2\) and \(0<α<β\) is a valid but loose lower label, the individual map vanishes at \(h=1/β\), whereas the balanced endpoint envelope still has \(q>0\). This does not contradict the minimax result for the supplied class of curvature bounds.
The owned endpoint theorem permits signed moduli and the optimal-step theorem permits \(α=0\), both on complete real Hilbert spaces. Those are disclosed generalizations. At \(α=0\) the latter is only nonexpansive and \(κ\) is not formed. The present exercise uses their positive-curvature Euclidean specialization. Its source's informal \(large-κ\) iteration-complexity remark, separate eigenvalue-list output and the explanatory loose-label example are not additional compiled claims of these two declarations.

Owned Lean answer and proof-step correspondence

This numbered exercise reuses the two actual owned answers in the full source module. The endpoint proof derives Hessian bounds from the existing convexity/smoothness APIs, constructs the Riesz Hessian and genuine update derivative, proves symmetry, bounds its Rayleigh quotients including the zero-vector case, and applies the vector segment FTC with internally established continuity/integrability. The optimal-step proof balances the endpoints and proves their global scalar lower bound. The separate trusted module probe compiles/imports and checks transitive axioms of these named answers; it is not a new theorem or a fixed Lean reconstruction challenge. The optional code is the exact existing module. No target is smuggled into a challenge, and no terminal call is counted as a substantive new leaf.

Supporting library Lean (not an aligned QA task)

import AutoSamplingTheory.TechnicalLemmas.Analysis.SmoothnessEquivalences
import Mathlib.Analysis.Calculus.FDeriv.Symmetric
import Mathlib.Analysis.InnerProductSpace.Rayleigh

/-!
# Optimal constant step for a gradient map

Chewi arXiv:2605.07006v1 Exercise 3.2. Genuine C² regularity supplies Hessian
symmetry and affine-segment integrability. The Rayleigh norm formula implements
the source spectral bound on a complete real Hilbert space. The endpoint
max-envelope is minimized at 2/(α+β); this is a uniform curvature bound, not
an assertion of an optimal step for every individual objective.
-/

namespace AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentOptimalStep

open Set InnerProductSpace MeasureTheory
open scoped RealInnerProductSpace

variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]

set_option backward.isDefEq.respectTransparency false in
/-- Actual gradient maps satisfy the endpoint spectral bound for nonnegative steps.
The curvature moduli may be signed; all Hessians are derived from the C² objective. -/
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. -/
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

Download exact supporting module · Uses the project toolchain and its listed imports; not a standalone replacement QA proof.

Assessment rubric · 4 points

Obtains the actual symmetric update derivative and the correct endpoint eigenvalue/operator-norm bound, keeping the chapter's \(C^{2}\) and compatible curvature assumptions explicit. (1 point)
Checks the continuous segment derivative/integrability and applies vector FTC and the norm bound to every x,y without a hidden minimizer or nonzero-displacement premise. (1 point)
Finds h*=2/(alpha+beta), verifies \(M(h*)=q\), proves \(q\le M(h)\) for every admissible \(h\ge 0\) (a stronger all-real comparison also qualifies), justifies any divisions and sign-sensitive steps, and derives exactly (kappa-1)/(kappa+1). Equivalent valid minimax arguments receive credit. (1 point)
Correctly interprets uniform-envelope optimality, handles equal curvatures and the condition-number regime, and does not promote the disclosed \(Hilbert/α=0\) extensions or commentary into stronger source/iterate claims. Equivalent valid proofs of the requested obligations receive credit. (1 point)

Owned Lean core answers · no fixed reconstruction challenge

Supporting library Lean (not an aligned QA task)

import AutoSamplingTheory.TechnicalLemmas.Analysis.SmoothnessEquivalences
import Mathlib.Analysis.Calculus.FDeriv.Symmetric
import Mathlib.Analysis.InnerProductSpace.Rayleigh

/-!
# Optimal constant step for a gradient map

Chewi arXiv:2605.07006v1 Exercise 3.2. Genuine C² regularity supplies Hessian
symmetry and affine-segment integrability. The Rayleigh norm formula implements
the source spectral bound on a complete real Hilbert space. The endpoint
max-envelope is minimized at 2/(α+β); this is a uniform curvature bound, not
an assertion of an optimal step for every individual objective.
-/

namespace AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentOptimalStep

open Set InnerProductSpace MeasureTheory
open scoped RealInnerProductSpace

variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]

set_option backward.isDefEq.respectTransparency false in
/-- Actual gradient maps satisfy the endpoint spectral bound for nonnegative steps.
The curvature moduli may be signed; all Hessians are derived from the C² objective. -/
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. -/
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

Download exact supporting module · Uses the project toolchain and its listed imports; not a standalone replacement QA proof.

Named owned core answers and their exact domain are separate from full explanatory coverage or a fixed reconstruction challenge.

What this does—and does not—verify

A real source-numbered exercise with a complete authored mathematical reference answer and two existing compiled owned core-answer declarations. There is no separately aligned fixed Lean QA here. The Lean APIs are broader than the source domain and use the equivalent Rayleigh formulation; their exact differences and unformalized context remain visible. No new production declaration, wrapper, Registry credit, full textbook completion, standalone eigenvalue-list theorem, iterate complexity or source-commentary formalization is claimed.

Existing library mathematics reused; no new mathematical leaf or paper-completion credit. The editorial panel records the exact current review scope and remaining unformalized explanation.

Sources, graph location and dependencies

Sinho Chewi, Lectures on Optimization, arXiv:2605.07006v1, Chapter 3 Exercise 3.2, printed/PDF p.23. This original mathematical reformulation and solution use the canonical publication item chewi-opt-v1-exercise-3-2 and its two actual part bindings, rather than copying textbook prose or renaming an unrelated original QA. The primary PDF is hash-pinned and its relevant page was visually inspected; the arXiv distribution grant is not treated as a blanket ML-text license. Existing ASTIS-owned answers, source audits, tests and graph placement are reused with their scope disclosed. This public exercise and all variants/subparts share one family; public availability is not evidence of an unseen test.

Exact local source and full context · Locate the existing Lean declaration

AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentOptimalStep.optimal_gradient_step

ASTIS formal support (not an equivalent QA)

AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentOptimalStep.gradient_step_endpoint_bound
AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexityC2.gradient_mono_iff_fderiv2_lower
AutoSamplingTheory.TechnicalLemmas.Analysis.SmoothnessEquivalences.upper_model_iff_fderiv2_upper

Mathlib facts / definitions

ContinuousLinearMap.norm_eq_iSup_rayleighQuotient
intervalIntegral.integral_eq_sub_of_hasDerivAt
intervalIntegral.norm_integral_le_of_norm_le_const

Additional source-bound support (not full QA certification)

AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentOptimalStep.gradient_step_endpoint_bound · LF source SHA-256: 856f336591e9cd23a69b827d5c438ec70628e530974c4b63981e6b13cd77dc83

Binding SHA-256: 9d9f361a44b9b4cbd33ff6379d61f64ca7b45805e410c4021af25e64ba6013c8