ASTIS mathematical exposition

Exact gradient descent on a quadratic

AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticGradientDescent.quadratic_gradient_iterate · theorem · Teaching coverage

Statement

For every natural iteration count, the actual gradient-descent trajectory equals the indicated operator power.

\[T_h^N(x)=(I-hH)^N x,\qquad f(x)=\tfrac12\langle x,Hx\rangle.\]

All objects and hypotheses

E is a complete real inner-product space. H:E→E is a continuous linear operator symmetric in the sense ⟨Hx,y⟩=⟨x,Hy⟩ for every x,y.
Define the actual centered objective f(x)=⟨x,Hx⟩/2 and its actual gradient update T_h(x)=x−h∇f(x). h∈ℝ is constant across steps, N∈ℕ, and the initial point x∈E is arbitrary.

Mathematical proof

1. Differentiate the actual objective

\[Df(x)[v]=\tfrac12\bigl(\langle x,Hv\rangle+\langle v,Hx\rangle\bigr)=\langle Hx,v\rangle,\qquad\nabla f(x)=Hx.\]

Corresponding Lean step

HasFDerivAt.inner; HasFDerivAt.const_mul; LinearMap.IsSymmetric.apply_clm; hasGradientAt_iff_hasFDerivAt; HasGradientAt.gradient.

2. Identify every update and its iterates

Substitute the computed gradient into T_h. The update is the continuous linear endomorphism I−hH. Reuse Mathlib’s identity equating endomorphism powers with function iteration; the zero-th power is the identity.

\[T_h=I-hH\quad\Longrightarrow\quad T_h^N(x)=(I-hH)^Nx.\]

Corresponding Lean step

FunLike.coe_pow_eq_iterate; congrFun.

Lean statement · quadratic_gradient_iterate

Actual quadratic and actual gradient iteration; symmetric continuous linear H on complete real Hilbert E, real h, natural N.

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 quadratic_gradient_iterate (H : E →L[ℝ] E) (hH : H.IsSymmetric)
    (h : ℝ) (N : ℕ) (x : E) :
    let f := fun z : E => inner ℝ z (H z) / 2
    (fun z => z - h • gradient f z)^[N] x = ((1 - h • H) ^ N) x

Exact module and namespace context

Lean proof · quadratic_gradient_iterate

The product rule for the inner product gives half the sum of two linear terms. Symmetry moves H between arguments, and real inner-product symmetry identifies both terms. This is the continuous linear functional represented by Hx, so uniqueness of the Riesz gradient yields ∇f(x)=Hx. Substitute the computed gradient into T_h. The update is the continuous linear endomorphism I−hH. Reuse Mathlib’s identity equating endomorphism powers with function iteration; the zero-th power is the identity.

theorem quadratic_gradient_iterate (H : E →L[ℝ] E) (hH : H.IsSymmetric)
    (h : ℝ) (N : ℕ) (x : E) :
    let f := fun z : E => inner ℝ z (H z) / 2
    (fun z => z - h • gradient f z)^[N] x = ((1 - h • H) ^ N) x := by
  let f := fun z : E => inner ℝ z (H z) / 2
  have hg (z : E) : gradient f z = H z := by
    have hraw := ((hasFDerivAt_id z).inner ℝ H.hasFDerivAt).const_mul (1 / 2 : ℝ)
    have hlin : (1 / 2 : ℝ) •
        ((fderivInnerCLM ℝ (z, H z)).comp ((ContinuousLinearMap.id ℝ E).prod H)) =
        toDual ℝ E (H z) := by
      ext v
      change (1 / 2 : ℝ) * (inner ℝ z (H v) + inner ℝ v (H z)) = inner ℝ (H z) v
      rw [← hH.apply_clm z v, (real_inner_comm v (H z)).symm]
      ring
    have hd : HasFDerivAt f (toDual ℝ E (H z)) z := by
      convert hraw using 1 <;> first | rfl | exact hlin.symm | (ext v; simp only [f, id_eq]; ring)
    exact (hasGradientAt_iff_hasFDerivAt.mpr hd).gradient
  change (fun z => z - h • gradient f z)^[N] x = _
  simp_rw [hg]
  exact congrFun (FunLike.coe_pow_eq_iterate (1 - h • H) N).symm x

/-- A supplied eigenmode gives exact iterates, distances to zero and quadratic values.
No existence of an eigenvector or stability of the chosen step is assumed. -/

Exact module and namespace context

Scope and omitted-condition boundaries

The source assumes a positive-definite symmetric matrix on Euclidean space. These exact identities extend to bounded symmetric operators on complete real Hilbert spaces, including signed or zero operators and the zero-dimensional space.
Positivity and a stability condition on h are unnecessary for identities. The theorem does not assert convergence for arbitrary h or indefinite H. The quadratic is smooth by bounded bilinear calculus; symmetry, not a supplied gradient equality, gives its true gradient.
This is a bounded Exercise3.3 proof component. Assessment of every Section3 bound, spectral decomposition/existence, complexity lower bounds, accelerated methods and companion-paper completion remain outside its conclusions.
The formula covers every initial point, without choosing an eigenbasis. The source matrix-power notation is instantiated by a continuous linear map on Euclidean space.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

HasFDerivAt.inner
HasFDerivAt.const_mul
LinearMap.IsSymmetric.apply_clm
HasGradientAt.gradient
FunLike.coe_pow_eq_iterate

Mathematical sources

Chewi Exercise3.3 — ASTIS-authored derivation of exact quadratic iterations; remaining sharpness analysis stays separate.
Diagonal endpoint and unstable-step tests — Actual diagonal spectrum 1,3 at balanced step, and scalar unit quadratic at unstable step3; no standalone 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.