Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0
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

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

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

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

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))) := 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

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

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