QuadraticGradientDescent: 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.

Exact gradient descent on a quadratic
Exact evolution of a quadratic eigenmode

Samplinglib mathematical lesson

Exact gradient descent on a quadratic

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

Read this first

Mathematical 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.\]

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.

Download module (.lean)

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

Proof roadmap

1Differentiate the actual objective
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.
2Identify 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.

Full assumptions and notation

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 verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

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.

Download module (.lean)

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

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.

Sources, dependencies, and reuse

Source and reuse

Samplinglib 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.

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

Samplinglib mathematical lesson

Exact evolution of a quadratic eigenmode

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

Read this first

Mathematical statement

The supplied eigenmode evolves by a scalar geometric factor, with the displayed exact norm and objective-value identities.

\[Hx=\mu x,\quad z=T_h^N(x):\quad z=(1-h\mu)^Nx,\quad\|z\|=|1-h\mu|^N\|x\|,\quad f(z)=(1-h\mu)^{2N}f(x).\]

Lean statement · quadratic_eigenmode

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

Download module (.lean)

theorem quadratic_eigenmode (H : E →L[ℝ] E) (hH : H.IsSymmetric)
    {μ : ℝ} {x : E} (hx : H x = μ • x) (h : ℝ) (N : ℕ) :
    let f := fun z : E => inner ℝ z (H z) / 2
    let z := (fun y => y - h • gradient f y)^[N] x
    z = (1 - h * μ) ^ N • x ∧
      ‖z‖ = |1 - h * μ| ^ N * ‖x‖ ∧
      f z = (1 - h * μ) ^ (2 * N) * f x

Exact module and namespace context

Proof roadmap

1Transport the supplied mode to the update operator
The given relation Hx=μx implies (I−hH)x=(1−hμ)x. If x=0, every power identity is immediate. Otherwise this is a genuine nonzero eigenvector of I−hH, so Mathlib’s eigenvector power theorem applies. No eigenvector is constructed.
2Read the exact norm and value
Take norms of the scalar multiple and use homogeneity. The quadratic is homogeneous of degree two, so its value is multiplied by the square of the trajectory scalar. The absolute value is essential when the update changes sign.

Full assumptions and notation

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.
μ∈ℝ and Hx=μx is supplied for the initial point. x=0 is allowed as an algebraic mode relation; a genuine eigenvector requires x≠0.

Mathematical proof

1. Transport the supplied mode to the update operator

\[(I-hH)x=(1-h\mu)x\quad\Longrightarrow\quad (I-hH)^Nx=(1-h\mu)^Nx.\]

Corresponding Lean step

AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticGradientDescent.quadratic_gradient_iterate; Module.End.mem_eigenspace_iff; Module.End.HasEigenvector.pow_apply; ContinuousLinearMap.toLinearMap_pow.

2. Read the exact norm and value

Take norms of the scalar multiple and use homogeneity. The quadratic is homogeneous of degree two, so its value is multiplied by the square of the trajectory scalar. The absolute value is essential when the update changes sign.

\[\|c x\|=|c|\|x\|,\qquad f(cx)=c^2f(x),\qquad c=(1-h\mu)^N.\]

Corresponding Lean step

norm_smul; Real.norm_eq_abs; map_smul; inner_smul_left; inner_smul_right; pow_mul.

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · quadratic_eigenmode

The given relation Hx=μx implies (I−hH)x=(1−hμ)x. If x=0, every power identity is immediate. Otherwise this is a genuine nonzero eigenvector of I−hH, so Mathlib’s eigenvector power theorem applies. No eigenvector is constructed. Take norms of the scalar multiple and use homogeneity. The quadratic is homogeneous of degree two, so its value is multiplied by the square of the trajectory scalar. The absolute value is essential when the update changes sign.

Download module (.lean)

theorem quadratic_eigenmode (H : E →L[ℝ] E) (hH : H.IsSymmetric)
    {μ : ℝ} {x : E} (hx : H x = μ • x) (h : ℝ) (N : ℕ) :
    let f := fun z : E => inner ℝ z (H z) / 2
    let z := (fun y => y - h • gradient f y)^[N] x
    z = (1 - h * μ) ^ N • x ∧
      ‖z‖ = |1 - h * μ| ^ N * ‖x‖ ∧
      f z = (1 - h * μ) ^ (2 * N) * f x := by
  let f := fun z : E => inner ℝ z (H z) / 2
  let A : E →L[ℝ] E := 1 - h • H
  have hAx : A x = (1 - h * μ) • x := by
    simp only [A, sub_apply, one_apply_eq_self,
      smul_apply, hx, smul_smul, sub_smul, one_smul]
  have hp : (A ^ N) x = (1 - h * μ) ^ N • x := by
    by_cases hz : x = 0
    · simp [hz]
    · have he : Module.End.HasEigenvector A.toLinearMap (1 - h * μ) x :=
        ⟨Module.End.mem_eigenspace_iff.mpr hAx, hz⟩
      have ht := congrArg (fun K : E →ₗ[ℝ] E => K x) (ContinuousLinearMap.toLinearMap_pow A N)
      convert ht.trans (he.pow_apply N) using 1; rfl
  have hi := (quadratic_gradient_iterate H hH h N x).trans hp
  change _ = _ ∧ _ = _ ∧ f _ = _ * f x
  rw [hi]
  refine ⟨rfl, ?_, ?_⟩
  · simp [norm_smul, Real.norm_eq_abs]
  · simp only [f, map_smul, inner_smul_left, inner_smul_right, RCLike.conj_to_real]
    rw [Nat.mul_comm 2 N, pow_mul]
    ring

end AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticGradientDescent

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.
To use this as a sharpness witness, supply a nonzero endpoint eigenvector and the appropriate positive curvature bounds. At h=2/(α+β), modes μ=α or μ=β give |1−hμ|=(β−α)/(α+β). The concrete diagonal-matrix tests realize both endpoints for α=1,β=3; this is not a general spectral existence theorem.
N=0 gives the initial point and value even when 1−hμ=0; the zero-th power is one. A zero mode vector yields zero throughout. For arbitrary Hilbert operators, neither endpoint eigenvectors nor a diagonalizing eigenbasis are asserted.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticGradientDescent.quadratic_gradient_iterate

Mathlib API called (external library)

Module.End.mem_eigenspace_iff
Module.End.HasEigenvector.pow_apply
ContinuousLinearMap.toLinearMap_pow
norm_smul
inner_smul_left
inner_smul_right
pow_mul

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.

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