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

Rayleigh objective: remove the radial part of 2Ax
Sphere stationary points are exactly unit eigenvectors

Samplinglib mathematical lesson

Rayleigh objective: remove the radial part of 2Ax

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

Read this first

Mathematical statement

For a symmetric linear operator A on a finite-dimensional real Euclidean space, let F(x)=⟨x,Ax⟩ on the unit sphere. With its induced metric, the unique ambient tangent vector representing the genuine sphere differential is Gₓ=2(Ax−⟨x,Ax⟩x). More explicitly, every z in x⊥ represents that differential against every actual tangent direction exactly when z=Gₓ.

\[\begin{gathered}F(x)=\langle x,Ax\rangle,\quad T_xS=x^\perp,\quad J_x=D\iota(x),\\ DF(x)[w]=\langle J_xw,z\rangle\ \forall w\ \Longleftrightarrow\ z=G_x\quad(z\in x^\perp),\\ G_x=2(Ax-\langle x,Ax\rangle x).\end{gathered}\]

Lean statement · sphere_rayleigh_characterization

All source data are quantified. z is typed in the ambient tangent plane x⊥, w in the actual Mathlib TangentSpace. The inclusion differential Jₓ transports w into the ambient space for the exact induced pairing. The iff yields the explicit unique representative; it is not a definition of a new gradient field.

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_characterization
    (n : ℕ) [Fact (Module.finrank ℝ E = n + 1)]
    (A : E →L[ℝ] E) (hA : A.IsSymmetric) (x : sphere (0 : E) 1) :
    ∀ z : (ℝ ∙ (x : E))ᗮ,
      ((∀ w : TangentSpace (𝓡 n) x,
        mvfderiv (𝓡 n) (fun y : sphere (0 : E) 1 => ⟪(y : E), A (y : E)⟫_ℝ) x w =
          ⟪mvfderiv (𝓡 n) ((↑) : sphere (0 : E) 1 → E) x w, (z : E)⟫_ℝ) ↔
        (z : E) = (2 : ℝ) • (A (x : E) - ⟪(x : E), A (x : E)⟫_ℝ • (x : E)))

Exact module and namespace context

Proof roadmap

1Differentiate the symmetric quadratic
Expand q(x+tv). Symmetry makes the two first-order cross terms equal, giving Dq(x)[v]=2⟨Ax,v⟩ and hence the genuine ambient gradient 2Ax. The implementation reuses Mathlib’s derivative, proves that its quadratic is literally q, and identifies its linear functional with the gradient dual. No gradient witness is supplied by the reader.
2Project onto the actual tangent plane
Because x is a unit vector, the projection onto its normal line sends u to ⟨x,u⟩x. Subtracting this normal component gives the projection onto x⊥. Apply this to 2Ax and use bilinearity to obtain the displayed vector Gₓ. In particular Gₓ is tangent: ⟨x,Gₓ⟩=2(⟨x,Ax⟩−⟨x,Ax⟩‖x‖²)=0.
3Use the induced differential characterization
The existing genuine-sphere theorem applies to the actual ambient gradient just proved. The inclusion chain rule and its exact tangent range are already established in that parent: the restricted differential pairs with a tangent candidate precisely when it is the orthogonal projection. Replacing that projection by Gₓ gives the claimed formula and uniqueness. Existence uses the projected vector in x⊥, not an assumed solution.

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. Differentiate the symmetric quadratic

Expand q(x+tv). Symmetry makes the two first-order cross terms equal, giving Dq(x)[v]=2⟨Ax,v⟩ and hence the genuine ambient gradient 2Ax. The implementation reuses Mathlib’s derivative, proves that its quadratic is literally q, and identifies its linear functional with the gradient dual. No gradient witness is supplied by the reader.

\[q(x+tv)=q(x)+2t\langle Ax,v\rangle+t^2q(v),\qquad Dq(x)[v]=2\langle Ax,v\rangle,\quad \nabla q(x)=2Ax.\]

Corresponding Lean step

  have hx : ‖(x : E)‖ = 1 := mem_sphere_zero_iff_norm.mp x.property
  have hg : HasGradientAt (fun y : E => ⟪y, A y⟫_ℝ) ((2 : ℝ) • A (x : E)) (x : E) := by
    apply hasGradientAt_iff_hasFDerivAt.mpr
    have hraw := (hA.hasStrictFDerivAt_reApplyInnerSelf (x : E)).hasFDerivAt
    have hfun : (fun y : E => ⟪y, A y⟫_ℝ) = A.reApplyInnerSelf := by
      funext y
      simp [ContinuousLinearMap.reApplyInnerSelf_apply, real_inner_comm]
    have hlin : toDual ℝ E ((2 : ℝ) • A (x : E)) =
        (2 : ℕ) • innerSL ℝ (A (x : E)) := by
      ext v
      simp [toDual_apply_apply, two_smul]
    rw [hfun, hlin]
    exact hraw

The strict derivative API writes its coefficient as natural-number addition twice; two_smul identifies it with multiplication by the real scalar2. This is an API adapter, not a change of normalization.

2. Project onto the actual tangent plane

Because x is a unit vector, the projection onto its normal line sends u to ⟨x,u⟩x. Subtracting this normal component gives the projection onto x⊥. Apply this to 2Ax and use bilinearity to obtain the displayed vector Gₓ. In particular Gₓ is tangent: ⟨x,Gₓ⟩=2(⟨x,Ax⟩−⟨x,Ax⟩‖x‖²)=0.

\[P_{x^\perp}u=u-\langle x,u\rangle x,\qquad P_{x^\perp}(2Ax)=2(Ax-\langle x,Ax\rangle x).\]

Corresponding Lean step

  let K := (ℝ ∙ (x : E))ᗮ
  have hproj (u : E) : (K.orthogonalProjectionOnto u : E) =
      u - ⟪(x : E), u⟫_ℝ • (x : E) := by
    change (ℝ ∙ (x : E))ᗮ.starProjection u = _
    rw [Submodule.starProjection_orthogonal_val,
      Submodule.starProjection_unit_singleton ℝ hx]
  have hp : (K.orthogonalProjectionOnto ((2 : ℝ) • A (x : E)) : E) =
      (2 : ℝ) • (A (x : E) - ⟪(x : E), A (x : E)⟫_ℝ • (x : E)) := by
    rw [hproj]
    simp [inner_smul_right, smul_sub, smul_smul]

Submodule.starProjection_orthogonal_val and starProjection_unit_singleton supply the exact projection formula. The local hproj holds for every ambient u and covers source equation3.40; no duplicate public projection lemma is introduced.

3. Use the induced differential characterization

The existing genuine-sphere theorem applies to the actual ambient gradient just proved. The inclusion chain rule and its exact tangent range are already established in that parent: the restricted differential pairs with a tangent candidate precisely when it is the orthogonal projection. Replacing that projection by Gₓ gives the claimed formula and uniqueness. Existence uses the projected vector in x⊥, not an assumed solution.

\[\begin{gathered}DF(x)[w]=Dq(x)[J_xw]=\langle J_xw,2Ax\rangle=\langle J_xw,G_x\rangle,\\ z\text{ represents }DF(x)\ \Longleftrightarrow\ z=G_x.\end{gathered}\]

Corresponding Lean step

  intro z
  rw [SphereGradient.sphere_gradient_characterization n x hg z]
  constructor
  · intro hz
    exact (congrArg (fun v : K => (v : E)) hz).trans hp
  · intro hz
    apply Subtype.ext
    exact hz.trans hp.symm

The canonical SphereGradient.sphere_gradient_characterization supplies the true nonlinear differential and uniqueness. Subtype.ext and congrArg only move the already tangent projection between its subtype and ambient representation.

Lean verification

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

Lean proof · sphere_rayleigh_characterization

Produce the true quadratic derivative, compute the unit tangent projection and apply the existing canonical sphere differential theorem.

Download module (.lean)

theorem sphere_rayleigh_characterization
    (n : ℕ) [Fact (Module.finrank ℝ E = n + 1)]
    (A : E →L[ℝ] E) (hA : A.IsSymmetric) (x : sphere (0 : E) 1) :
    ∀ z : (ℝ ∙ (x : E))ᗮ,
      ((∀ w : TangentSpace (𝓡 n) x,
        mvfderiv (𝓡 n) (fun y : sphere (0 : E) 1 => ⟪(y : E), A (y : E)⟫_ℝ) x w =
          ⟪mvfderiv (𝓡 n) ((↑) : sphere (0 : E) 1 → E) x w, (z : E)⟫_ℝ) ↔
        (z : E) = (2 : ℝ) • (A (x : E) - ⟪(x : E), A (x : E)⟫_ℝ • (x : E))) := by
  have hx : ‖(x : E)‖ = 1 := mem_sphere_zero_iff_norm.mp x.property
  have hg : HasGradientAt (fun y : E => ⟪y, A y⟫_ℝ) ((2 : ℝ) • A (x : E)) (x : E) := by
    apply hasGradientAt_iff_hasFDerivAt.mpr
    have hraw := (hA.hasStrictFDerivAt_reApplyInnerSelf (x : E)).hasFDerivAt
    have hfun : (fun y : E => ⟪y, A y⟫_ℝ) = A.reApplyInnerSelf := by
      funext y
      simp [ContinuousLinearMap.reApplyInnerSelf_apply, real_inner_comm]
    have hlin : toDual ℝ E ((2 : ℝ) • A (x : E)) =
        (2 : ℕ) • innerSL ℝ (A (x : E)) := by
      ext v
      simp [toDual_apply_apply, two_smul]
    rw [hfun, hlin]
    exact hraw
  let K := (ℝ ∙ (x : E))ᗮ
  have hproj (u : E) : (K.orthogonalProjectionOnto u : E) =
      u - ⟪(x : E), u⟫_ℝ • (x : E) := by
    change (ℝ ∙ (x : E))ᗮ.starProjection u = _
    rw [Submodule.starProjection_orthogonal_val,
      Submodule.starProjection_unit_singleton ℝ hx]
  have hp : (K.orthogonalProjectionOnto ((2 : ℝ) • A (x : E)) : E) =
      (2 : ℝ) • (A (x : E) - ⟪(x : E), A (x : E)⟫_ℝ • (x : E)) := by
    rw [hproj]
    simp [inner_smul_right, smul_sub, smul_smul]
  intro z
  rw [SphereGradient.sphere_gradient_characterization n x hg z]
  constructor
  · intro hz
    exact (congrArg (fun v : K => (v : E)) hz).trans hp
  · intro hz
    apply Subtype.ext
    exact hz.trans hp.symm

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.SphereGradient.sphere_gradient_characterization

Mathlib API called (external library)

LinearMap.IsSymmetric.hasStrictFDerivAt_reApplyInnerSelf
HasStrictFDerivAt.hasFDerivAt
hasGradientAt_iff_hasFDerivAt
ContinuousLinearMap.reApplyInnerSelf_apply
InnerProductSpace.toDual_apply_apply
two_smul
Submodule.starProjection_orthogonal_val
Submodule.starProjection_unit_singleton
mem_sphere_zero_iff_norm
inner_smul_right
Subtype.ext
congrArg

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.

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.

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.