Samplinglib mathematical lesson

Sphere stationary points are exactly unit eigenvectors

AutoSamplingTheory.TechnicalLemmas.Geometry.SphereRayleigh.sphere_rayleigh_stationary_iff · theorem · Teaching coverage

Read this first

Mathematical statement

For the same symmetric quadratic on the induced unit sphere, the genuine manifold differential at x is zero exactly when Ax=⟨x,Ax⟩x, and exactly when x is an eigenvector of A. If Ax=μx, the unit norm forces μ=⟨x,Ax⟩. Zero or negative eigenvalues are allowed.

\[\begin{gathered}DF(x)=0\ \Longleftrightarrow\ Ax=\langle x,Ax\rangle x\ \Longleftrightarrow\ \exists\mu\in\mathbb R:\ Ax=\mu x,\ x\ne0,\\ Ax=\mu x\Rightarrow\mu=\langle x,Ax\rangle.\end{gathered}\]

Lean statement · sphere_rayleigh_stationary_iff

The first conjunct identifies a zero continuous-linear-map differential with the Rayleigh equation. The second conjunct identifies it with an existential actual Module.End.HasEigenvector. All x on the unit sphere are quantified, and no nonzero-eigenvalue premise is present.

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 sphere_rayleigh_stationary_iff
    (n : ℕ) [Fact (Module.finrank ℝ E = n + 1)]
    (A : E →L[ℝ] E) (hA : A.IsSymmetric) (x : sphere (0 : E) 1) :
    (mvfderiv (𝓡 n) (fun y : sphere (0 : E) 1 => ⟪(y : E), A (y : E)⟫_ℝ) x = 0 ↔
      A (x : E) = ⟪(x : E), A (x : E)⟫_ℝ • (x : E)) ∧
    (mvfderiv (𝓡 n) (fun y : sphere (0 : E) 1 => ⟪(y : E), A (y : E)⟫_ℝ) x = 0 ↔
      ∃ μ : ℝ, Module.End.HasEigenvector A.toLinearMap μ (x : E))

Exact module and namespace context

Proof roadmap

1Turn zero differential into zero projected gradient
A continuous linear differential is zero exactly when it vanishes on every tangent direction. The first theorem at the candidate z=0 says that these vanishing pairings hold precisely when Gₓ=0. This explicitly implements the source-derived bridge from differential stationarity to induced-gradient stationarity. Cancel the nonzero real scalar2 and rearrange the difference.
2A stationary unit vector is an eigenvector
The preceding equality puts x in the eigenspace with eigenvalue ⟨x,Ax⟩. Unit membership proves x≠0, so this is genuine eigenvectorhood in the library sense rather than the equation alone, which would also hold at zero.
3Every unit eigenvector is stationary
Conversely, suppose Ax=μx. Pair with x to get ⟨x,Ax⟩=μ‖x‖²=μ. Thus the eigenvector equation is exactly the Rayleigh-coefficient equation, and the first equivalence gives DF(x)=0. This proves the converse for any real eigenvalue, including zero and negative values.

Full assumptions and notation

All objects and hypotheses

E is a finite-dimensional real inner-product space of dimension n+1. In orthonormal coordinates A is the source real symmetric matrix; its continuous-linear-map representation adds no regularity assumption in finite dimension.
A is symmetric, not necessarily positive, positive definite or invertible. x has norm one. Nonzeroness of x and the Rayleigh eigenvalue identity are derived internally, not added hypotheses.
The objective is the literal sphere restriction F(x)=⟨x,Ax⟩ of the smooth quadratic q(y)=⟨y,Ay⟩. The ambient quotient is defined only for y≠0; its equality with this restriction uses ‖x‖=1. No derivative of an off-domain totalized quotient is used.
The metric is the ambient-induced one. The actual inclusion derivative Jₓ maps abstract chart directions into x⊥. Pairings with Jₓw express this induced metric explicitly; no default chart inner product is identified with it.
n may be zero. The claims are pointwise, with every x and every tangent test direction quantified. They neither construct a global gradient-field object nor claim a convergence or extremal-eigenvalue theorem.

Mathematical proof

1. Turn zero differential into zero projected gradient

A continuous linear differential is zero exactly when it vanishes on every tangent direction. The first theorem at the candidate z=0 says that these vanishing pairings hold precisely when Gₓ=0. This explicitly implements the source-derived bridge from differential stationarity to induced-gradient stationarity. Cancel the nonzero real scalar2 and rearrange the difference.

\[DF(x)=0\ \Longleftrightarrow\ DF(x)[w]=0\ \forall w\ \Longleftrightarrow\ 0=2(Ax-\langle x,Ax\rangle x)\ \Longleftrightarrow\ Ax=\langle x,Ax\rangle x.\]

Corresponding Lean step

  have hx : ‖(x : E)‖ = 1 := mem_sphere_zero_iff_norm.mp x.property
  have hxne : (x : E) ≠ 0 := by
    intro hz
    simp [hz] at hx
  have hzero := sphere_rayleigh_characterization n A hA x 0
  have hd :
      mvfderiv (𝓡 n) (fun y : sphere (0 : E) 1 => ⟪(y : E), A (y : E)⟫_ℝ) x = 0 ↔
        A (x : E) = ⟪(x : E), A (x : E)⟫_ℝ • (x : E) := by
    have he :
        mvfderiv (𝓡 n) (fun y : sphere (0 : E) 1 => ⟪(y : E), A (y : E)⟫_ℝ) x = 0 ↔
          ∀ w : TangentSpace (𝓡 n) x,
            mvfderiv (𝓡 n) (fun y : sphere (0 : E) 1 => ⟪(y : E), A (y : E)⟫_ℝ) x w = 0 := by
      constructor
      · intro h w
        rw [h]
        rfl
      · intro h
        ext w
        exact h w
    rw [he]
    have hs : (0 : E) = (2 : ℝ) •
        (A (x : E) - ⟪(x : E), A (x : E)⟫_ℝ • (x : E)) ↔
          A (x : E) = ⟪(x : E), A (x : E)⟫_ℝ • (x : E) := by
      rw [eq_comm, smul_eq_zero, sub_eq_zero]
      simp
    have hpair :
        (∀ w : TangentSpace (𝓡 n) x,
          mvfderiv (𝓡 n) (fun y : sphere (0 : E) 1 => ⟪(y : E), A (y : E)⟫_ℝ) x w = 0) ↔
          (0 : E) = (2 : ℝ) • (A (x : E) - ⟪(x : E), A (x : E)⟫_ℝ • (x : E)) := by
      simpa only [Submodule.coe_zero, inner_zero_right] using hzero
    exact hpair.trans hs

The proof uses extensionality of the actual differential, not an arbitrary supplied pairing identity. The characterization tests every chart direction through the canonical induced pairing. Norm one gives x≠0 internally.

2. A stationary unit vector is an eigenvector

The preceding equality puts x in the eigenspace with eigenvalue ⟨x,Ax⟩. Unit membership proves x≠0, so this is genuine eigenvectorhood in the library sense rather than the equation alone, which would also hold at zero.

\[Ax=\langle x,Ax\rangle x,\quad\|x\|=1\Rightarrow x\ne0,\qquad x\in E_{\langle x,Ax\rangle}(A)\setminus\{0\}.\]

Corresponding Lean step

  refine ⟨hd, ?_⟩
  constructor
  · intro h
    exact ⟨⟪(x : E), A (x : E)⟫_ℝ,
      Module.End.mem_eigenspace_iff.mpr (hd.mp h), hxne⟩

Module.End.mem_eigenspace_iff supplies eigenspace membership; HasEigenvector includes the proved nonzeroness. No spectral existence theorem or positivity assumption is needed.

3. Every unit eigenvector is stationary

Conversely, suppose Ax=μx. Pair with x to get ⟨x,Ax⟩=μ‖x‖²=μ. Thus the eigenvector equation is exactly the Rayleigh-coefficient equation, and the first equivalence gives DF(x)=0. This proves the converse for any real eigenvalue, including zero and negative values.

\[\langle x,Ax\rangle=\langle x,\mu x\rangle=\mu\|x\|^2=\mu,\qquad Ax=\langle x,Ax\rangle x\Rightarrow DF(x)=0.\]

Corresponding Lean step

  · rintro ⟨μ, hμ⟩
    have hAx : A (x : E) = μ • (x : E) := hμ.apply_eq_smul
    have hcoef : ⟪(x : E), A (x : E)⟫_ℝ = μ := by
      rw [hAx, inner_smul_right]
      simp [hx]
    apply hd.mpr
    rw [hcoef]
    exact hAx

HasEigenvector.apply_eq_smul gives the actual eigenvalue equation. The coefficient identity uses the source unit norm; it is not added as a theorem hypothesis.

Lean verification

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

Lean proof · sphere_rayleigh_stationary_iff

Evaluate the genuine gradient characterization at zero; derive the coefficient equation; construct the actual eigenvector and prove the converse by unit normalization.

Download module (.lean)

theorem sphere_rayleigh_stationary_iff
    (n : ℕ) [Fact (Module.finrank ℝ E = n + 1)]
    (A : E →L[ℝ] E) (hA : A.IsSymmetric) (x : sphere (0 : E) 1) :
    (mvfderiv (𝓡 n) (fun y : sphere (0 : E) 1 => ⟪(y : E), A (y : E)⟫_ℝ) x = 0 ↔
      A (x : E) = ⟪(x : E), A (x : E)⟫_ℝ • (x : E)) ∧
    (mvfderiv (𝓡 n) (fun y : sphere (0 : E) 1 => ⟪(y : E), A (y : E)⟫_ℝ) x = 0 ↔
      ∃ μ : ℝ, Module.End.HasEigenvector A.toLinearMap μ (x : E)) := by
  have hx : ‖(x : E)‖ = 1 := mem_sphere_zero_iff_norm.mp x.property
  have hxne : (x : E) ≠ 0 := by
    intro hz
    simp [hz] at hx
  have hzero := sphere_rayleigh_characterization n A hA x 0
  have hd :
      mvfderiv (𝓡 n) (fun y : sphere (0 : E) 1 => ⟪(y : E), A (y : E)⟫_ℝ) x = 0 ↔
        A (x : E) = ⟪(x : E), A (x : E)⟫_ℝ • (x : E) := by
    have he :
        mvfderiv (𝓡 n) (fun y : sphere (0 : E) 1 => ⟪(y : E), A (y : E)⟫_ℝ) x = 0 ↔
          ∀ w : TangentSpace (𝓡 n) x,
            mvfderiv (𝓡 n) (fun y : sphere (0 : E) 1 => ⟪(y : E), A (y : E)⟫_ℝ) x w = 0 := by
      constructor
      · intro h w
        rw [h]
        rfl
      · intro h
        ext w
        exact h w
    rw [he]
    have hs : (0 : E) = (2 : ℝ) •
        (A (x : E) - ⟪(x : E), A (x : E)⟫_ℝ • (x : E)) ↔
          A (x : E) = ⟪(x : E), A (x : E)⟫_ℝ • (x : E) := by
      rw [eq_comm, smul_eq_zero, sub_eq_zero]
      simp
    have hpair :
        (∀ w : TangentSpace (𝓡 n) x,
          mvfderiv (𝓡 n) (fun y : sphere (0 : E) 1 => ⟪(y : E), A (y : E)⟫_ℝ) x w = 0) ↔
          (0 : E) = (2 : ℝ) • (A (x : E) - ⟪(x : E), A (x : E)⟫_ℝ • (x : E)) := by
      simpa only [Submodule.coe_zero, inner_zero_right] using hzero
    exact hpair.trans hs
  refine ⟨hd, ?_⟩
  constructor
  · intro h
    exact ⟨⟪(x : E), A (x : E)⟫_ℝ,
      Module.End.mem_eigenspace_iff.mpr (hd.mp h), hxne⟩
  · rintro ⟨μ, hμ⟩
    have hAx : A (x : E) = μ • (x : E) := hμ.apply_eq_smul
    have hcoef : ⟪(x : E), A (x : E)⟫_ℝ = μ := by
      rw [hAx, inner_smul_right]
      simp [hx]
    apply hd.mpr
    rw [hcoef]
    exact hAx

end AutoSamplingTheory.TechnicalLemmas.Geometry.SphereRayleigh

Exact module and namespace context

Scope and omitted-condition boundaries

Pointwise Example3.62 gradient formula and both critical/eigenvector conditions, using the genuine sphere differential and actual inclusion-induced pairing. Finite Euclidean symmetric matrices are represented coordinate-independently by continuous symmetric linear maps. No default chart-metric identification, global Riemannian bundle/gradient-field construction, extremal eigenvalue theorem, algorithm or convergence rate, arbitrary radius, general Prop3.61 or chapter completion.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

AutoSamplingTheory.TechnicalLemmas.Geometry.SphereRayleigh.sphere_rayleigh_characterization

Mathlib API called (external library)

mem_sphere_zero_iff_norm
Module.End.mem_eigenspace_iff
Module.End.HasEigenvector.apply_eq_smul
inner_smul_right
smul_eq_zero
sub_eq_zero

Mathematical sources

Boumal2023, annotations2026-10-08, Example3.62/(3.40), printed44/PDF60; Example3.36 printed36/PDF52 — ASTIS-authored explanation of the sphere quadratic application; no source PDF or book prose bundled.

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