ASTIS mathematical exposition

Exact evolution of a quadratic eigenmode

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

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

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 statement · quadratic_eigenmode

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_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

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.

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.

Source and reuse

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

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