Riemannian Optimization · Chapter 03

Embedded geometry: first order

Stable source-facing chapter environment inside the shared Samplinglib reader.

Partially formalizedsource mapFull source closure not claimed

Chapter goal

From feasible directions to gradients

Turn smooth embedded geometry into first-order optimization: identify feasible directions, differentiate an objective along them, and use the induced metric to represent its differential by a gradient.

Mathematical knowledge map

Feasible directions
The tangent space describes first-order motion within the embedded manifold. Affine directions are K; for the unit sphere the actual inclusion differential maps Mathlib tangent directions onto the ambient plane x⊥.
Differentiate along the space
Local agreement of extensions gives the same derivative on a true feasible-curve velocity. The sphere adapter now composes the actual inclusion differential with the ambient derivative to construct the true restricted manifold differential. General embedded-manifold tangent/differential and representing-curve adapters remain separate.
Represent by the metric
For the induced pairing, the gradient is the unique ambient tangent vector representing the differential. The sphere adapter tests every ambient tangent direction through the exact range of the inclusion differential. Changing the metric requires a separate adapter; no default chart inner product is substituted.
Project the ambient gradient
Orthogonal projection removes the normal component without changing tangent pairings. The affine lemma supplies the linear restriction prerequisite; the sphere theorem constructs and uniquely characterizes the projection for the actual nonlinear sphere differential.

Current boundary. The curve lemma closes the explicit extension-choice proof edge following Proposition3.35; affine restriction supplies a projection prerequisite; the sphere theorem closes the actual induced-gradient characterization for the unit sphere. General embedded-manifold tangent/differential and extension identification, representing-curve independence/linearity, global induced-metric smoothness and smooth gradient fields remain open. These are scoped partial advances, not completion of either proposition or Chapter3.

Source anchors and shared formal roots

Boumal Chapter3, §3.4 Definition3.34/(3.27), (3.28), Proposition3.35 and following extension-choice verification; §3.8 Definition3.58, (3.36)–(3.38), Definition3.60 and Proposition3.61; 2023 pre-publication edition, annotations through2026-10-08.

This page establishes a stable source route and truth boundary; it does not claim a completed formalization.

Proposition 3.35 and its extension-independence consequence

Nicolas Boumal. Samplinglib attributed restatement. The canonical normed-space lemma generalizes only the selected curve proof edge.

2023 pre-publication edition, annotations through2026-10-08 · §3.4 Definition3.34/(3.27), equation(3.28), Proposition3.35 and following extension-choice verification; printed35–36/PDF51–52 · faithful paraphrase

Complete source statement (Samplinglib restatement)

Let M⊆E and M′⊆E′ be embedded submanifolds of finite-dimensional Euclidean spaces, let F:M→M′ be smooth, and let F̄ be any smooth ambient neighborhood extension. For every x∈M, the manifold differential is DF(x)=D F̄(x)|_{TₓM}. Consequently it is linear, depends on a representing curve only through its base point and velocity, and is independent of the extension: any second extension F̂ gives D F̄(x)[v]=D F̂(x)[v] for v∈TₓM.

M and M′ are embedded submanifolds of finite-dimensional Euclidean spaces; F:M→M′ is smooth.
F̄ and F̂ are smooth neighborhood extensions of the same F.
Each tangent v at x is represented by a smooth feasible curve c with c(0)=x and c′(0)=v.

Source differential restriction

\[DF(x)=D\bar F(x)|_{T_xM}.\]

Selected extension-choice proof edge

\[D\bar F(x)[v]=(\bar F\circ c)\prime(0)=(\widehat F\circ c)\prime(0)=D\widehat F(x)[v],\quad c(0)=x,\ c\prime(0)=v.\]

Read the formalized proofs

Each statement and proof below has its own closed Lean disclosure. Samplinglib parents, Mathlib calls and external mathematical sources are distinguished in each proof.

Samplinglib mathematical lesson

Why the derivative along a feasible curve ignores the extension

AutoSamplingTheory.TechnicalLemmas.Geometry.CurveExtension.fderiv_eq_on_curve_velocity · theorem · Teaching coverage

Read this first

Mathematical statement

Let E and V be real normed spaces, s⊆E, and f,g:E→V. At x=c(t₀), suppose f and g are genuinely differentiable, c has actual velocity v, c(t) lies in s for all t sufficiently near t₀, and f=g locally relative to s at x. Then Df(x)[v]=Dg(x)[v].

\[x=c(t_0),\quad c\prime(t_0)=v,\qquad Df(x)[v]=Dg(x)[v].\]

Lean statement · fderiv_eq_on_curve_velocity

DifferentiableAt certifies both ambient derivatives; HasDerivAt certifies the actual curve velocity. Eventually in 𝓝 means locally near t₀. EventuallyEq in 𝓝[s] x means equality on a relative neighborhood. E→V are total Lean function types, but only their local germs enter this proof.

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 fderiv_eq_on_curve_velocity
    {s : Set E} {f g : E → F} {c : ℝ → E} {t₀ : ℝ} {v : E}
    (hf : DifferentiableAt ℝ f (c t₀))
    (hg : DifferentiableAt ℝ g (c t₀))
    (hc : HasDerivAt c v t₀)
    (hcs : ∀ᶠ t in 𝓝 t₀, c t ∈ s)
    (hfg : f =ᶠ[𝓝[s] (c t₀)] g) :
    fderiv ℝ f (c t₀) v = fderiv ℝ g (c t₀) v

Exact module and namespace context

Proof roadmap

1Pull the agreement back to the curve
A differentiable curve is continuous. Together with local feasibility, continuity sends sufficiently small parameter neighborhoods into relative neighborhoods of x in s. The two image curves therefore agree near t₀. This is a local argument: neither extension needs to agree off the feasible set.
2Differentiate each image curve
Apply the actual chain rule to each genuinely differentiable ambient map and the actual curve derivative. Its velocity is the ambient derivative applied to v. This derives both image derivatives inside the proof.
3Use locality and uniqueness
Locally equal image curves share their derivative at t₀. Transfer the first derivative witness to the second image curve; uniqueness then equates the two velocities. For every source tangent vector represented by a smooth feasible curve, this gives the extension-choice equality. The remaining manifold tangent adapter must be supplied separately.

Full assumptions and notation

All objects and hypotheses

E and V are real normed spaces, possibly infinite-dimensional and incomplete. No chosen Riemannian metric, inner product, Riesz gradient, orthogonal projector or manifold structure is required. This generalizes the finite-dimensional Euclidean source proof ingredient.
Both ambient maps have genuine pointwise Fréchet derivatives at x. Smoothness of the source extensions implies this condition. fderiv is not used to manufacture a derivative when none exists.
c:ℝ→E has a genuine derivative v at t₀ and lies locally in s. Source smooth manifold curves satisfy these weaker local requirements.
The two ambient maps agree on some relative neighborhood of x in s. They need not agree in any open ambient neighborhood. Source neighborhood extensions of the same manifold map supply this equality locally.

Mathematical proof

1. Pull the agreement back to the curve

A differentiable curve is continuous. Together with local feasibility, continuity sends sufficiently small parameter neighborhoods into relative neighborhoods of x in s. The two image curves therefore agree near t₀. This is a local argument: neither extension needs to agree off the feasible set.

\[f(c(t))=g(c(t))\quad\text{for all }t\text{ sufficiently near }t_0.\]

Corresponding Lean step

  have hcts : Tendsto c (𝓝 t₀) (𝓝[s] (c t₀)) :=
    tendsto_nhdsWithin_iff.mpr ⟨hc.continuousAt, hcs⟩
  have hcomp : (f ∘ c) =ᶠ[𝓝 t₀] (g ∘ c) := hfg.comp_tendsto hcts

HasDerivAt.continuousAt and tendsto_nhdsWithin_iff construct the relative-neighborhood limit. Filter.EventuallyEq.comp_tendsto pulls back local equality.

2. Differentiate each image curve

Apply the actual chain rule to each genuinely differentiable ambient map and the actual curve derivative. Its velocity is the ambient derivative applied to v. This derives both image derivatives inside the proof.

\[(f\circ c)\prime(t_0)=Df(x)[v],\qquad (g\circ c)\prime(t_0)=Dg(x)[v].\]

Corresponding Lean step

  have hfc := hf.hasFDerivAt.comp_hasDerivAt t₀ hc
  have hgc := hg.hasFDerivAt.comp_hasDerivAt t₀ hc

DifferentiableAt.hasFDerivAt gives a real derivative witness; HasFDerivAt.comp_hasDerivAt is the Fréchet/one-parameter chain rule.

3. Use locality and uniqueness

Locally equal image curves share their derivative at t₀. Transfer the first derivative witness to the second image curve; uniqueness then equates the two velocities. For every source tangent vector represented by a smooth feasible curve, this gives the extension-choice equality. The remaining manifold tangent adapter must be supplied separately.

\[Df(x)[v]=(f\circ c)\prime(t_0)=(g\circ c)\prime(t_0)=Dg(x)[v].\]

Corresponding Lean step

  exact (hfc.congr_of_eventuallyEq hcomp.symm).unique hgc

HasDerivAt.congr_of_eventuallyEq transfers the witness. HasDerivAt.unique compares two genuine derivatives of one image curve.

Lean verification

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

Lean proof · fderiv_eq_on_curve_velocity

Pull relative equality back by the continuous feasible curve, apply the two genuine chain rules, then compare derivatives by locality and uniqueness.

Download module (.lean)

theorem fderiv_eq_on_curve_velocity
    {s : Set E} {f g : E → F} {c : ℝ → E} {t₀ : ℝ} {v : E}
    (hf : DifferentiableAt ℝ f (c t₀))
    (hg : DifferentiableAt ℝ g (c t₀))
    (hc : HasDerivAt c v t₀)
    (hcs : ∀ᶠ t in 𝓝 t₀, c t ∈ s)
    (hfg : f =ᶠ[𝓝[s] (c t₀)] g) :
    fderiv ℝ f (c t₀) v = fderiv ℝ g (c t₀) v := by
  have hcts : Tendsto c (𝓝 t₀) (𝓝[s] (c t₀)) :=
    tendsto_nhdsWithin_iff.mpr ⟨hc.continuousAt, hcs⟩
  have hcomp : (f ∘ c) =ᶠ[𝓝 t₀] (g ∘ c) := hfg.comp_tendsto hcts
  have hfc := hf.hasFDerivAt.comp_hasDerivAt t₀ hc
  have hgc := hg.hasFDerivAt.comp_hasDerivAt t₀ hc
  exact (hfc.congr_of_eventuallyEq hcomp.symm).unique hgc

end AutoSamplingTheory.TechnicalLemmas.Geometry.CurveExtension

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
Smooth neighborhood extensions between finite-dimensional Euclidean ambient spaces.	Total maps between arbitrary real normed spaces, genuinely differentiable at one point.	generalization	Only pointwise differentiability and local germs are used by the selected source chain-rule edge; no manifold differential identification follows.
Smooth feasible curve c with c(0)=x, c′(0)=v.	Actual HasDerivAt c v t₀ and eventual feasibility in an arbitrary set.	generalization	The argument is local at any parameter and requires only actual differentiability; source smooth feasible curves supply these conditions.
Both extensions agree with F on the manifold where defined.	Relative local agreement f=g in 𝓝[s] (c t₀).	generalization	Ambient open-neighborhood agreement is unnecessary. Source extensions agree on the feasible manifold near x.

This proves the actual nonlinear-curve extension-independence edge. It does not identify the full embedded-manifold differential, prove its tangent-space domain/codomain adapter or complete Proposition3.35/3.61.

Encoder–denoiser: source-reviewed · lean-weakened-conclusion

Detected semantic differences

domains: The real normed-space arbitrary-set local interface genuinely generalizes the selected finite-dimensional smooth curve proof ingredient. It is not a full intrinsic manifold differential generalization. — Independent reviewer classification: domain-clarification; blocking scope: none.
domains: Source maps are defined on open extension neighborhoods, while Lean maps are total. Only their local germs are used; arbitrary outside-neighborhood totalization preserves the pointwise derivative and relative equality. This must not be read as a global smooth extension construction. — Independent reviewer classification: domain-clarification; blocking scope: none.
conclusion: Intrinsic differential restriction, target tangent membership, tangent/curve representation and resulting manifold linearity/curve-choice statements remain absent. This blocks equivalence with the full source Proposition3.35, but does not block the declared proof-edge binding to extension-independence. — Independent reviewer classification: conclusion-correction; blocking scope: full-source-equivalence-only.
domains: Initial reviewed packet claimed no metric was required; normed spaces have their norm-induced metric. Current packet correctly says no chosen Riemannian metric or inner product is required. Exposition-only correction was applied by formalizer during this same review; theorem and proof were unchanged. — Independent reviewer classification: micro-correction; blocking scope: none.

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

Scope and omitted-condition boundaries

This proves the actual nonlinear-curve extension-independence edge. It does not identify the full embedded-manifold differential, prove its tangent-space domain/codomain adapter or complete Proposition3.35/3.61.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

tendsto_nhdsWithin_iff
HasDerivAt.continuousAt
Filter.EventuallyEq.comp_tendsto
DifferentiableAt.hasFDerivAt
HasFDerivAt.comp_hasDerivAt
HasDerivAt.congr_of_eventuallyEq
HasDerivAt.unique

Mathematical sources

Boumal 2023 pre-publication, annotations2026-10-08, §3.4, printed35–36/PDF51–52 — Attributed authored account of the explicit extension-independence verification following Proposition3.35. The preceding definition-based argument is an alternative sufficient route. No book prose or PDF 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.

Which proof obligations and prerequisites are covered?

TODO — not closed by these contributions Identify the actual manifold differential with the ambient derivative restricted to source tangent vectors, including the target tangent adapter.
TODO — not closed by these contributions Derive linearity and independence from the representing feasible curve.
Formalized proof edge; source adapter/review separate Derive equality of two actual ambient derivatives on the velocity of a feasible curve from their local agreement.

Proposition 3.61 · ambient-to-tangent gradient projection

Nicolas Boumal. ASTIS attributed restatement. Affine restriction is a prerequisite; sphere projection is a scoped nonlinear application. Neither completes the general embedded-manifold theorem.

2023 pre-publication edition, annotations through 2026-10-08 · §3.8, Definition3.58 and equations3.36–3.38; Proposition3.61 (3.39), printed42–44 / PDF58–60 · faithful paraphrase

Complete source statement (Samplinglib restatement)

On a Riemannian submanifold of Euclidean space with the induced metric, the gradient of a smooth function is the tangent-space orthogonal projection of the ambient gradient of any smooth neighborhood extension.

Finite-dimensional Euclidean ambient space and embedded submanifold with induced Riemannian metric.
Smooth real-valued f on the manifold and a smooth extension to a neighborhood.

Source projection formula

\[\operatorname{grad}_Mf(x)=P_{T_xM}\operatorname{grad}_E\bar f(x).\]

Read the formalized proofs

Each statement and proof below has its own closed Lean disclosure. Samplinglib parents, Mathlib calls and external mathematical sources are distinguished in each proof.

Samplinglib mathematical lesson

Project the gradient when restricting to an affine subspace

AutoSamplingTheory.TechnicalLemmas.Geometry.AffineGradient.hasGradientAt_affine_restriction · theorem · Teaching coverage

Read this first

Mathematical statement

Let E be a real Hilbert space and K a complete linear subspace with inherited metric. If f has genuine ambient gradient g at a+u, then the affine restriction F_a(v)=f(a+v), v∈K, has genuine gradient P_K g at u.

\[F_a(v)=f(a+v),\qquad \nabla_KF_a(u)=P_K\nabla_Ef(a+u).\]

Lean statement · hasGradientAt_affine_restriction

K is a subtype with its own inherited inner product. HasGradientAt includes genuine differentiability. The result is typed in K; a is a point shift, not part of the gradient. Completeness supplies the Riesz gradient and orthogonal projector.

Download module (.lean)

theorem hasGradientAt_affine_restriction
    (K : Submodule ℝ E) [CompleteSpace K]
    {f : E → ℝ} {a g : E} {u : K}
    (hf : HasGradientAt f g (a + (u : E))) :
    HasGradientAt (fun v : K => f (a + (v : E)))
      (K.orthogonalProjectionOnto g) u

Exact module and namespace context

Proof roadmap

1Differentiate the affine parameterization
For v in the direction space, the chart i_a(v)=a+v has derivative equal to the inclusion K↪E. The shift changes the evaluation point but contributes zero derivative.
2Apply the actual chain rule
The ambient gradient represents Df(a+u). Composing with the chart derivative produces the restriction derivative for every v∈K; this derivative is proved rather than supplied.
3Remove the normal component and identify the gradient
The residual g−P_K g is perpendicular to K. Therefore all tangent pairings agree. With the inherited metric the projected vector represents exactly the restriction derivative, which proves the genuine gradient assertion and hence its uniqueness through the existing gradient API.

Full assumptions and notation

All objects and hypotheses

E is a complete real inner-product space; K is a complete real linear subspace with the inherited inner product. These assumptions generalize the finite-dimensional Euclidean source.
f:E→ℝ, a,g:E and u∈K. The genuine ambient gradient g exists at a+u: HasGradientAt f g (a+u). No totalized derivative is used as a regularity witness.
The restriction is the literal map F_a:K→ℝ, v↦f(a+v). Its gradient is a direction in K, not the affine point a+P_K g.

Mathematical proof

1. Differentiate the affine parameterization

For v in the direction space, the chart i_a(v)=a+v has derivative equal to the inclusion K↪E. The shift changes the evaluation point but contributes zero derivative.

\[Di_a(u)[v]=v,\qquad i_a(u)=a+u.\]

Corresponding Lean step

  have hchart : HasFDerivAt (fun v : K => a + (v : E)) K.subtypeL u := by
    convert (hasFDerivAt_const a u).add K.subtypeL.hasFDerivAt using 1 <;>
      first | rfl | simp only [zero_add]

hchart: derivative of the constant plus the continuous linear inclusion.

2. Apply the actual chain rule

The ambient gradient represents Df(a+u). Composing with the chart derivative produces the restriction derivative for every v∈K; this derivative is proved rather than supplied.

\[DF_a(u)[v]=Df(a+u)[v]=\langle g,v\rangle_E.\]

Corresponding Lean step

  have hcomp := hf.hasFDerivAt.comp u hchart

hf.hasFDerivAt.comp u hchart; the Riesz functional is InnerProductSpace.toDual.

3. Remove the normal component and identify the gradient

The residual g−P_K g is perpendicular to K. Therefore all tangent pairings agree. With the inherited metric the projected vector represents exactly the restriction derivative, which proves the genuine gradient assertion and hence its uniqueness through the existing gradient API.

\[\langle g,v\rangle_E=\langle P_Kg,v\rangle_K\quad(v\in K),\qquad \nabla_KF_a(u)=P_Kg.\]

Corresponding Lean step

  have hdual : (InnerProductSpace.toDual ℝ E g).comp K.subtypeL =
      InnerProductSpace.toDual ℝ K (K.orthogonalProjectionOnto g) := by
    ext v
    simp
  rw [hdual] at hcomp
  exact hasGradientAt_iff_hasFDerivAt.mpr hcomp

hdual uses Submodule.inner_orthogonalProjectionOnto_eq_of_mem_right; hasGradientAt_iff_hasFDerivAt finishes.

Lean verification

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

Lean proof · hasGradientAt_affine_restriction

Compose the genuine ambient derivative with the affine inclusion, then identify its Riesz functional using orthogonal projection. The typeclass conversion only reconciles equivalent submodule structures.

Download module (.lean)

theorem hasGradientAt_affine_restriction
    (K : Submodule ℝ E) [CompleteSpace K]
    {f : E → ℝ} {a g : E} {u : K}
    (hf : HasGradientAt f g (a + (u : E))) :
    HasGradientAt (fun v : K => f (a + (v : E)))
      (K.orthogonalProjectionOnto g) u := by
  have hchart : HasFDerivAt (fun v : K => a + (v : E)) K.subtypeL u := by
    convert (hasFDerivAt_const a u).add K.subtypeL.hasFDerivAt using 1 <;>
      first | rfl | simp only [zero_add]
  have hcomp := hf.hasFDerivAt.comp u hchart
  have hdual : (InnerProductSpace.toDual ℝ E g).comp K.subtypeL =
      InnerProductSpace.toDual ℝ K (K.orthogonalProjectionOnto g) := by
    ext v
    simp
  rw [hdual] at hcomp
  exact hasGradientAt_iff_hasFDerivAt.mpr hcomp

end AutoSamplingTheory.TechnicalLemmas.Geometry.AffineGradient

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
Finite Euclidean ambient and tangent subspaces.	Complete real Hilbert E and complete linear subspace K.	generalization	The pairing mechanism works for complete subspaces; finite-dimensional source instances satisfy completeness. This is not a nonlinear tangent adapter.
Smooth function and smooth neighborhood extension.	Pointwise genuine HasGradientAt for f:E→ℝ; literal affine restriction.	generalization	One-point differentiability suffices for this library node. The source requires independent nonlinear extension/differential semantics.
Induced metric and tangent gradient.	Inherited inner product on K and gradient typed in K.	same	The chosen subspace metric is exactly inherited. No arbitrary Riemannian metric identification is claimed.

This is the linear/affine restriction prerequisite for Boumal §3.8. Arbitrary embedded-manifold tangent identification, differential restriction, extension semantics and smooth gradient fields remain open; Proposition 3.61 and Chapter 3 are not complete.

Encoder–denoiser: source-reviewed · domain-mismatch

Detected semantic differences

objects: Fixed affine restriction and ambient pointwise gradient do not formalize arbitrary nonlinear embedded M or its intrinsic differential/gradient. This blocks full-source equivalence while leaving declared affine prerequisite valid. — Independent domain-clarification; blocking scope full-source-equivalence-only. See actual runs/20261012-andi-sphere-gradient/affine-source-semantic-review.json
domains: Complete Hilbert ambient/subspace and pointwise HasGradientAt generalize finite Euclidean smoothness, while total literal affine pullback specializes geometry. Both changes are explicitly disclosed rather than proposed source repairs. — Independent domain-clarification; blocking scope none. See actual runs/20261012-andi-sphere-gradient/affine-source-semantic-review.json
quantifiers: For every smooth extension of one fixed intrinsic f is absent from this affine statement. General tangent/differential identification and extension semantics remain unbound source obligations. — Independent quantifier-clarification; blocking scope full-source-equivalence-only. See actual runs/20261012-andi-sphere-gradient/affine-source-semantic-review.json
scopes: The separate unit-sphere characterization obligation is mathematically compatible with the source specialization, and does not change affine supports=[affine-gradient]. This review neither certifies the sphere Lean declaration nor closes generic nonlinear/smooth-field obligations. — Independent domain-clarification; blocking scope none. See actual runs/20261012-andi-sphere-gradient/affine-source-semantic-review.json

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

Scope and omitted-condition boundaries

This is the linear/affine restriction prerequisite for Boumal §3.8. Arbitrary embedded-manifold tangent identification, differential restriction, extension semantics and smooth gradient fields remain open; Proposition 3.61 and Chapter 3 are not complete.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

HasGradientAt.hasFDerivAt
HasFDerivAt.comp
hasFDerivAt_const
HasFDerivAt.add
ContinuousLinearMap.hasFDerivAt
Submodule.inner_orthogonalProjectionOnto_eq_of_mem_right
hasGradientAt_iff_hasFDerivAt

Mathematical sources

Boumal 2023, annotation revision 2026-10-08, §3.8 — Authored account of the affine restriction mechanism underlying Definition3.58 and equations3.36–3.38; no reproduction of book prose. Pre-publication PDF is personal-use-only; do not bundle the PDF.

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

The induced gradient on the sphere is a projection

AutoSamplingTheory.TechnicalLemmas.Geometry.SphereGradient.sphere_gradient_characterization · theorem · Teaching coverage

Read this first

Mathematical statement

Let E be a finite-dimensional real inner-product space of dimension n+1 and let x be on its unit sphere. If the ambient objective f has genuine gradient g at x, its restriction F to the sphere has a unique ambient tangent representative of its actual manifold differential. That representative is the orthogonal projection of g onto T=x⊥. The pairing uses the actual inclusion derivative Aₓ, so it specifies the induced metric rather than a default chart inner product.

\[T=(\mathbb R x)^\perp,\quad A_x=D\iota(x),\quad F=f\circ\iota,\qquad DF(x)[w]=\langle A_xw,z\rangle_E\ \forall w\ \Longleftrightarrow\ z=P_Tg\quad(z\in T).\]

Lean statement · sphere_gradient_characterization

TangentSpace (𝓡 n) x is the actual Mathlib tangent type for the unit sphere. mvfderiv is the true vector/scalar-valued manifold differential. z is in the ambient orthogonal tangent subspace; all w are quantified. The conclusion is a characterization, so it supplies existence by setting z=P_Tg and uniqueness for any candidate.

Download module (.lean)

theorem sphere_gradient_characterization
    (n : ℕ) [Fact (Module.finrank ℝ E = n + 1)]
    (x : sphere (0 : E) 1) {f : E → ℝ} {g : E}
    (hf : HasGradientAt f g (x : E)) :
    ∀ z : (ℝ ∙ (x : E))ᗮ,
      ((∀ w : TangentSpace (𝓡 n) x,
        mvfderiv (𝓡 n) (fun y : sphere (0 : E) 1 => f (y : E)) x w =
          ⟪mvfderiv (𝓡 n) ((↑) : sphere (0 : E) 1 → E) x w, (z : E)⟫_ℝ) ↔
        z = (ℝ ∙ (x : E))ᗮ.orthogonalProjectionOnto g)

Exact module and namespace context

Proof roadmap

1Identify actual tangent directions
The sphere inclusion is differentiable. Its differential Aₓ has range exactly the ambient plane T orthogonal to x. Thus every actual chart tangent direction maps into T, and every vector in T has a preimage. The companion injectivity theorem makes the pullback of the ambient pairing positive definite; the present ambient-representative proof uses the exact range.
2Differentiate the actual restricted objective
Apply the manifold chain rule to F=f∘ι. The ambient gradient is a genuine derivative witness, so evaluating the result at w gives the ambient pairing with its true direction Aₓw. Explicit vector-space tangent identification reconciles target types; it changes neither the differential nor the metric.
3Remove the normal component
For each w, Aₓw belongs to T. Orthogonal projection changes g only by a vector perpendicular to T, so it preserves this pairing. The projected vector is already typed in T, furnishing an actual candidate gradient representative.
4Prove uniqueness on the whole tangent plane
Suppose a tangent candidate z has the same differential pairings for every chart direction. Given any v in T, use the exact-range identity to choose w with Aₓw=v. The two candidates pair equally with every v in T. Nondegeneracy of its inherited inner product gives z=P_Tg. Conversely, the projected candidate satisfies all pairings by the preceding step.

Full assumptions and notation

All objects and hypotheses

E is a finite-dimensional real inner-product space; dim E=n+1 and n may be0. Finite dimension supplies completeness and closedness of the tangent subspace, so no extra analytical premise is added.
x lies on the unit sphere, and f:E→ℝ has a genuine gradient g at x. Source smoothness implies this pointwise HasGradientAt witness; the theorem explicitly allows weaker pointwise regularity.
F is the literal restriction y↦f(y). Source maps on an ambient open neighborhood can be represented by their local germs, but arbitrary smooth extension construction is not proved.
Mathlib chart tangent directions are sent into the ambient tangent plane by the actual derivative Aₓ of the sphere inclusion. Its exact range is proved by Mathlib and used internally, not assumed. The induced pairing is ⟨Aₓw,Aₓw′⟩E; no default chart norm/inner product is identified with it.

Mathematical proof

1. Identify actual tangent directions

The sphere inclusion is differentiable. Its differential Aₓ has range exactly the ambient plane T orthogonal to x. Thus every actual chart tangent direction maps into T, and every vector in T has a preimage. The companion injectivity theorem makes the pullback of the ambient pairing positive definite; the present ambient-representative proof uses the exact range.

\[\operatorname{range} A_x=T=(\mathbb R x)^\perp,\qquad \langle w,w\prime\rangle_x=\langle A_xw,A_xw\prime\rangle_E.\]

Corresponding Lean step

  let K := (ℝ ∙ (x : E))ᗮ
  let A := mvfderiv (𝓡 n) ((↑) : sphere (0 : E) 1 → E) x
  have hA : A.range = K := range_mvfderiv_subtypeVal x
  have hco := (contMDiff_coe_sphere (n := n) (m := 1) x).mdifferentiableAt one_ne_zero

contMDiff_coe_sphere gives actual differentiability; range_mvfderiv_subtypeVal supplies both directions of the tangent identification. injective_mvfderiv_subtypeVal_sphere is background for interpreting the induced metric, not a call in this proof.

2. Differentiate the actual restricted objective

Apply the manifold chain rule to F=f∘ι. The ambient gradient is a genuine derivative witness, so evaluating the result at w gives the ambient pairing with its true direction Aₓw. Explicit vector-space tangent identification reconciles target types; it changes neither the differential nor the metric.

\[DF(x)[w]=Df(x)[A_xw]=\langle g,A_xw\rangle_E=\langle A_xw,g\rangle_E.\]

Corresponding Lean step

  have hd : ∀ w : TangentSpace (𝓡 n) x,
      mvfderiv (𝓡 n) (fun y : sphere (0 : E) 1 => f (y : E)) x w =
        ⟪A w, g⟫_ℝ := by
    intro w
    have hchain := mvfderiv_comp x hf.differentiableAt.mdifferentiableAt hco
    change mvfderiv (𝓡 n) (f ∘ ((↑) : sphere (0 : E) 1 → E)) x w = _
    rw [hchain]
    convert! (hf.fderiv_apply (y := A w)) using 1 <;>
      simp [A, mvfderiv, NormedSpace.fromTangentSpace, real_inner_comm] <;> rfl

mvfderiv_comp and HasGradientAt.fderiv_apply provide the mathematical equalities. NormedSpace.fromTangentSpace is the explicit trivial-vector-space tangent identification; convert/rfl only reconciles its identity map.

3. Remove the normal component

For each w, Aₓw belongs to T. Orthogonal projection changes g only by a vector perpendicular to T, so it preserves this pairing. The projected vector is already typed in T, furnishing an actual candidate gradient representative.

\[\langle A_xw,g\rangle_E=\langle A_xw,P_Tg\rangle_E.\]

Corresponding Lean step

  have hp : ∀ w : TangentSpace (𝓡 n) x,
      mvfderiv (𝓡 n) (fun y : sphere (0 : E) 1 => f (y : E)) x w =
        ⟪A w, (K.orthogonalProjectionOnto g : E)⟫_ℝ := by
    intro w
    have hw : A w ∈ K := hA ▸ (show A w ∈ A.range from ⟨w, rfl⟩)
    rw [hd w]
    exact (K.inner_orthogonalProjectionOnto_eq_of_mem_left ⟨A w, hw⟩ g).symm

Submodule.inner_orthogonalProjectionOnto_eq_of_mem_left applies to the proved tangent membership. No differential equality for the candidate is supplied as a premise.

4. Prove uniqueness on the whole tangent plane

Suppose a tangent candidate z has the same differential pairings for every chart direction. Given any v in T, use the exact-range identity to choose w with Aₓw=v. The two candidates pair equally with every v in T. Nondegeneracy of its inherited inner product gives z=P_Tg. Conversely, the projected candidate satisfies all pairings by the preceding step.

\[\forall v\in T,\ \langle v,z\rangle_E=\langle v,P_Tg\rangle_E\quad\Longrightarrow\quad z=P_Tg.\]

Corresponding Lean step

  intro z
  constructor
  · intro hz
    apply ext_inner_left ℝ
    intro v
    have hv : (v : E) ∈ A.range := hA.symm ▸ v.property
    obtain ⟨w, hw⟩ := hv
    change ⟪(v : E), (z : E)⟫_ℝ = ⟪(v : E), (K.orthogonalProjectionOnto g : E)⟫_ℝ
    rw [← hw]
    exact (hz w).symm.trans (hp w)
  · rintro rfl
    exact hp

Range surjectivity supplies each test direction; ext_inner_left proves uniqueness in the ambient tangent subspace. This constructs the candidate and proves its characterization before defining any chosen gradient object.

Lean verification

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

Lean proof · sphere_gradient_characterization

Use the actual sphere inclusion and manifold chain rule, remove the normal component with projection, then test every ambient tangent direction through the exact range. No project-owned gradient definition or fallback semantics are introduced.

Download module (.lean)

theorem sphere_gradient_characterization
    (n : ℕ) [Fact (Module.finrank ℝ E = n + 1)]
    (x : sphere (0 : E) 1) {f : E → ℝ} {g : E}
    (hf : HasGradientAt f g (x : E)) :
    ∀ z : (ℝ ∙ (x : E))ᗮ,
      ((∀ w : TangentSpace (𝓡 n) x,
        mvfderiv (𝓡 n) (fun y : sphere (0 : E) 1 => f (y : E)) x w =
          ⟪mvfderiv (𝓡 n) ((↑) : sphere (0 : E) 1 → E) x w, (z : E)⟫_ℝ) ↔
        z = (ℝ ∙ (x : E))ᗮ.orthogonalProjectionOnto g) := by
  let K := (ℝ ∙ (x : E))ᗮ
  let A := mvfderiv (𝓡 n) ((↑) : sphere (0 : E) 1 → E) x
  have hA : A.range = K := range_mvfderiv_subtypeVal x
  have hco := (contMDiff_coe_sphere (n := n) (m := 1) x).mdifferentiableAt one_ne_zero
  have hd : ∀ w : TangentSpace (𝓡 n) x,
      mvfderiv (𝓡 n) (fun y : sphere (0 : E) 1 => f (y : E)) x w =
        ⟪A w, g⟫_ℝ := by
    intro w
    have hchain := mvfderiv_comp x hf.differentiableAt.mdifferentiableAt hco
    change mvfderiv (𝓡 n) (f ∘ ((↑) : sphere (0 : E) 1 → E)) x w = _
    rw [hchain]
    convert! (hf.fderiv_apply (y := A w)) using 1 <;>
      simp [A, mvfderiv, NormedSpace.fromTangentSpace, real_inner_comm] <;> rfl
  have hp : ∀ w : TangentSpace (𝓡 n) x,
      mvfderiv (𝓡 n) (fun y : sphere (0 : E) 1 => f (y : E)) x w =
        ⟪A w, (K.orthogonalProjectionOnto g : E)⟫_ℝ := by
    intro w
    have hw : A w ∈ K := hA ▸ (show A w ∈ A.range from ⟨w, rfl⟩)
    rw [hd w]
    exact (K.inner_orthogonalProjectionOnto_eq_of_mem_left ⟨A w, hw⟩ g).symm
  intro z
  constructor
  · intro hz
    apply ext_inner_left ℝ
    intro v
    have hv : (v : E) ∈ A.range := hA.symm ▸ v.property
    obtain ⟨w, hw⟩ := hv
    change ⟪(v : E), (z : E)⟫_ℝ = ⟪(v : E), (K.orthogonalProjectionOnto g : E)⟫_ℝ
    rw [← hw]
    exact (hz w).symm.trans (hp w)
  · rintro rfl
    exact hp

end AutoSamplingTheory.TechnicalLemmas.Geometry.SphereGradient

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
Smooth objective and neighborhood extension.	Actual pointwise ambient HasGradientAt f g; literal restriction of total f.	generalization	Only the actual derivative at x is used; no smooth extension construction or global smooth-field conclusion.
General Riemannian submanifold with induced Euclidean metric.	Unit sphere with actual Mathlib inclusion differential and ambient tangent-subspace pairing.	API-limitation	This source-present sphere specialization explicitly discharges the nonlinear adapter here; it does not stand for all embedded submanifolds or a default chart metric.
Finite Euclidean space and tangent vector at x.	FiniteDimensional real inner-product E, finrank=n+1, x:sphere0E1, candidate z:x⊥ and chart tangent w transported by the true inclusion derivative.	same	Dimension and carrier typing match the sphere application; exact range and differentiability are proof dependencies, not added premises.

Unit-sphere specialization with true Mathlib manifold differential and ambient tangent representation using actual inclusion derivative; pointwise ambient HasGradientAt generalizes smoothness. No general embedded-manifold theorem, chosen default chart metric identification, global smooth field, general neighborhood extension construction or Rayleigh quotient computation. No global Riemannian metric typeclass or smooth-field construction is certified by the pointwise pairing.

Encoder–denoiser: source-reviewed · domain-mismatch

Detected semantic differences

domains: The complete original source ranges over arbitrary induced-metric Riemannian submanifolds; the reconstructed theorem handles only the unit sphere. This blocks full-source equivalence, while it is intentional and accepted for the separate sphere binding. — Independent geometry-specialization; blocking scope full-source-equivalence-only. See actual runs/20261012-andi-sphere-gradient/source-semantic-review.json
quantifiers: The universal arbitrary-M source conclusion is absent. General nonlinear-differential obligation remains open; source sphere application quantifiers are preserved. — Independent scope-restriction; blocking scope full-source-equivalence-only. See actual runs/20261012-andi-sphere-gradient/source-semantic-review.json
assumptions: Pointwise ambient HasGradientAt is weaker than smooth source data. Correct for local characterization and explicitly disclosed; it does not certify source smoothness or smooth field. — Independent generalization; blocking scope informational-no-selected-binding-block. See actual runs/20261012-andi-sphere-gradient/source-semantic-review.json
scopes: The source names a general gradient vector field; Lean constructs only a local sphere ambient representative. Global metric/gradient-field and general well-definedness construction are not discharged. This is a full-source fidelity boundary, not a mathematical defect in the sphere theorem. — Independent scope-restriction; blocking scope full-source-equivalence-only. See actual runs/20261012-andi-sphere-gradient/source-semantic-review.json
objects: Source embedded tangent v corresponds to A_x w, the actual inclusion differential applied to an abstract chart tangent direction. Exact range gives all source directions; injectivity supports induced pullback metric interpretation. Candidate z is ambient tangent, not identified with abstract tangent by an unstated equality. — Independent explicit-elaboration; blocking scope informational-no-selected-binding-block. See actual runs/20261012-andi-sphere-gradient/source-semantic-review.json
domains: Lean f is total; a source neighborhood extension gives the same local instance by taking a total function agreeing on its open domain and arbitrary outside. No smooth extension construction/global smooth total map is claimed. — Independent local-germ-representation; blocking scope informational-no-selected-binding-block. See actual runs/20261012-andi-sphere-gradient/source-semantic-review.json

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

Scope and omitted-condition boundaries

Unit-sphere specialization with true Mathlib manifold differential and ambient tangent representation using actual inclusion derivative; pointwise ambient HasGradientAt generalizes smoothness. No general embedded-manifold theorem, chosen default chart metric identification, global smooth field, general neighborhood extension construction or Rayleigh quotient computation. No global Riemannian metric typeclass or smooth-field construction is certified by the pointwise pairing.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

range_mvfderiv_subtypeVal
contMDiff_coe_sphere
ContMDiffAt.mdifferentiableAt
HasGradientAt.differentiableAt
DifferentiableAt.mdifferentiableAt
mvfderiv_comp
HasGradientAt.fderiv_apply
NormedSpace.fromTangentSpace
Submodule.inner_orthogonalProjectionOnto_eq_of_mem_left
ext_inner_left

Mathematical sources

Boumal2023, annotations2026-10-08, §§3.7–3.8; printed41–44/PDF57–60 — ASTIS-authored sphere specialization of Definition3.58 and Proposition3.61, using the inherited metric in Example3.56/3.62. No book prose or source PDF is 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.

Which proof obligations and prerequisites are covered?

Independently verified prerequisite Canonical gradient under linear/affine restriction with inherited metric.
TODO — not closed by these contributions Actual nonlinear tangent/differential and extension-independence adapter.
TODO — not closed by these contributions Smoothness of the resulting manifold gradient field.
Formalized proof edge; source adapter/review separate Unit-sphere specialization: use the actual manifold differential and inclusion derivative to construct and uniquely characterize its ambient induced-gradient representative.

Example 3.62 · Rayleigh gradient and critical eigenvectors

Nicolas Boumal. ASTIS-authored restatement of the sphere application and its two stationarity directions; no source text/PDF redistributed.

2023 pre-publication edition, annotations through 2026-10-08 · Boumal2023 pre-publication annotations through2026-10-08, §3.8 Example3.62 and(3.40), printed44/PDF60; §3.4 Example3.36 printed36/PDF52; induced metric/gradient conventions §§3.7–3.8 · faithful paraphrase

Complete source statement (Samplinglib restatement)

For a real symmetric matrix A, let F(x)=xᵀAx on the unit sphere with the metric induced by the Euclidean inner product. The chosen smooth ambient quadratic extension has gradient2Ax. The tangent projector sends u to u−⟨x,u⟩x, so the sphere gradient is2(Ax−⟨x,Ax⟩x). Its vanishing is equivalent to Ax=⟨x,Ax⟩x; thus the stationary unit vectors are exactly eigenvectors of A, and every unit eigenvector is stationary.

Finite-dimensional real Euclidean space, real symmetric matrix A and a unit vector x.
Unit sphere with the metric induced by the ambient inner product; F(x)=xᵀAx, the sphere restriction of the smooth quadratic extension.

Unit tangent projector and gradient

\[P_xu=u-\langle x,u\rangle x,\qquad \operatorname{grad}_S F(x)=2(Ax-\langle x,Ax\rangle x).\]

Both directions of stationarity

\[\operatorname{grad}_S F(x)=0\ \Longleftrightarrow\ Ax=\langle x,Ax\rangle x\ \Longleftrightarrow\ x\text{ is a unit eigenvector of }A.\]

Read the formalized proofs

Each statement and proof below has its own closed Lean disclosure. Samplinglib parents, Mathlib calls and external mathematical sources are distinguished in each proof.

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.

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

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
Real symmetric matrix in a finite Euclidean space.	FiniteDimensional real inner-product E and continuous-linear A with A.IsSymmetric; dim E=n+1.	same	Coordinate-free representation in orthonormal coordinates; finite-dimensional continuity and sphere chart dimension are typing facts, not extra analytical restrictions.
Unit sphere with induced metric; smooth quadratic restriction.	Literal restriction y↦⟨y,Ay⟩; actual mvfderiv paired through the actual inclusion derivative.	same	The quadratic derivative is produced internally from symmetry; the induced pairing retains the source metric and actual tangent directions.
The induced sphere gradient is the tangent projection of the ambient quadratic gradient, with explicit formula2(Ax−⟨x,Ax⟩x).	Every ambient tangent candidate z represents the true restricted differential through the actual inclusion derivative iff z equals the explicit Rayleigh vector.	same	The canonical parent proves the genuine restricted differential and unique induced tangent representative. Explicit unit projection gives this representative; no stationary/eigenvector conclusion is attributed to this declaration.

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.

Encoder–denoiser: source-reviewed · equivalent-after-elaboration

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

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

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
Real symmetric matrix in a finite Euclidean space.	FiniteDimensional real inner-product E and continuous-linear A with A.IsSymmetric; dim E=n+1.	same	Coordinate-free representation in orthonormal coordinates; finite-dimensional continuity and sphere chart dimension are typing facts, not extra analytical restrictions.
Unit sphere with induced metric; smooth quadratic restriction.	Literal restriction y↦⟨y,Ay⟩; actual mvfderiv paired through the actual inclusion derivative.	same	The quadratic derivative is produced internally from symmetry; the induced pairing retains the source metric and actual tangent directions.
Stationary gradient zero and eigenvector equation.	Zero actual differential and Module.End.HasEigenvector, whose nonzero condition is derived from unit norm.	same	The explicit candidate characterization equates differential vanishing with zero projected representative. Unit normalization identifies every converse eigenvalue. No positivity or nonzero-eigenvalue premise is added.

Encoder–denoiser: source-reviewed · equivalent-after-elaboration

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

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.

Which proof obligations and prerequisites are covered?

Formalized proof edge; source adapter/review separate Construct the actual restricted differential and its unique induced tangent representative, with explicit formula2(Ax−⟨x,Ax⟩x).
Formalized proof edge; source adapter/review separate Zero actual differential iff the Rayleigh-coefficient equation iff actual unit eigenvectorhood, including the converse.

Library supplement: Hilbert feature tangent-gradient estimates

An original reusable mathematics supplement placed by subject. It is not a theorem claim about the primary textbook or a complete stochastic/statistical model.

Samplinglib original feature differentiation and transport supplement v1, 2026-10-21 · Complete authored units 2 and their formula proof steps in the immutable declaration lesson (historical source) · licensed original

Complete source statement and conditions

The adjacent complete statements, assumptions and formula proofs describe the exact generic results; the optional Lean is initially folded.

E,H are complete real inner-product normed spaces. F and D have the explicit actual full ambient Fréchet derivative relation.
M₁,M₂ are nonnegative; uniform derivative and operator Lipschitz bounds are explicit inputs on the closed unit ball. The tangent and joint field bounds require unit endpoint weights.

A Hilbert feature potential has a controlled tangent Riesz field

\[G_r(w)=2P_wD(w)^*r,\quad P_wz=z-\langle z,w\rangle w,\quad \|G_r(w)-G_q(u)\|\le2M_1\|r-q\|+2(M_2+2M_1)\|q\|\|w-u\|.\]

Read the formalized proofs

Each statement and proof below has its own closed Lean disclosure. Samplinglib parents, Mathlib calls and external mathematical sources are distinguished in each proof.

Samplinglib mathematical lesson

A Hilbert feature potential has a controlled tangent Riesz field

Read this first

Mathematical statement

Let E,H be complete real inner-product normed spaces. Let F:E→H be a map, and let each D(w):E→H be a continuous real linear map satisfying the actual ambient identity DF(w)=D(w) for every w. Suppose M₁,M₂≥0, ‖D(w)‖op≤M₁ on the closed unit ball, and ‖D(w)−D(u)‖op≤M₂‖w−u‖ there. For r∈H define V_r(w)=2⟨r,F(w)⟩ and G_r(w)=2(D(w)*r−⟨D(w)*r,w⟩w), where * is the Hilbert adjoint. At every ambient w, V_r has derivative 2⟨D(w)*r,·⟩. At every unit w, G_r(w) is tangent, satisfies ⟨G_r(w),v⟩=2⟨r,D(w)v⟩ for every v perpendicular to w, and has norm at most 2M₁‖r‖. For all r,q and unit w,u, its joint increment is bounded by 2M₁‖r−q‖+2(M₂+2M₁)‖q‖‖w−u‖.

\[G_r(w)=2P_wD(w)^*r,\quad P_wz=z-\langle z,w\rangle w,\quad \|G_r(w)-G_q(u)\|\le2M_1\|r-q\|+2(M_2+2M_1)\|q\|\|w-u\|.\]

Lean statement · quadratic_feature_potential_tangent_gradient

Let E,H be complete real inner-product normed spaces. Let F:E→H and D(w):E→H be continuous real linear maps satisfying the actual ambient identity DF(w)=D(w) for every w. Suppose M₁,M₂≥0, ‖D(w)‖op≤M₁ on the closed unit ball, and ‖D(w)−D(u)‖op≤M₂‖w−u‖ there. For r∈H define V_r(w)=2⟨r,F(w)⟩ and G_r(w)=2(D(w)*r−⟨D(w)*r,w⟩w), where * is the Hilbert adjoint. At every ambient w, V_r has derivative 2⟨D(w)*r,·⟩. At every unit w, G_r(w) is tangent, satisfies ⟨G_r(w),v⟩=2⟨r,D(w)v⟩ for every v perpendicular to w, and has norm at most 2M₁‖r‖. For all r,q and unit w,u, its joint increment is bounded by 2M₁‖r−q‖+2(M₂+2M₁)‖q‖‖w−u‖.

Download module (.lean)

theorem quadratic_feature_potential_tangent_gradient
    {E H : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
    [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
    (F : E → H) (D : E → E →L[ℝ] H)
    (hF : ∀ w, HasFDerivAt F (D w) w)
    (M₁ M₂ : ℝ) (hM₁ : 0 ≤ M₁) (hM₂ : 0 ≤ M₂)
    (hBound : ∀ w : E, ‖w‖ ≤ 1 → ‖D w‖ ≤ M₁)
    (hLip : ∀ w u : E, ‖w‖ ≤ 1 → ‖u‖ ≤ 1 → ‖D w-D u‖ ≤ M₂*‖w-u‖) :
    let V : H → E → ℝ := fun r w => 2 * ⟪r,F w⟫_ℝ
    let G : H → E → E := fun r w =>
      (2 : ℝ) • ((D w).adjoint r - ⟪(D w).adjoint r,w⟫_ℝ • w)
    (∀ r w, HasFDerivAt (V r) ((2 : ℝ) • innerSL ℝ ((D w).adjoint r)) w) ∧
    (∀ r w, ‖w‖ = 1 →
      ⟪w,G r w⟫_ℝ = 0 ∧
      (∀ v, ⟪w,v⟫_ℝ = 0 → ⟪G r w,v⟫_ℝ = 2 * ⟪r,D w v⟫_ℝ) ∧
      ‖G r w‖ ≤ 2 * M₁ * ‖r‖) ∧
    ∀ r q w u, ‖w‖ = 1 → ‖u‖ = 1 →
      ‖G r w-G q u‖ ≤ 2 * M₁ * ‖r-q‖ +
        2 * (M₂+2*M₁) * ‖q‖ * ‖w-u‖

Exact module and namespace context

Read the complete claim and its hypotheses first, then open the numbered mathematical proof steps. Each step has an optional fold containing literal Lean implementation excerpts; the full theorem and module context remain available below.

Full assumptions and notation

All objects and hypotheses

E,H are complete real inner-product normed spaces. F and D have the explicit actual full ambient Fréchet derivative relation.
M₁,M₂ are nonnegative; uniform derivative and operator Lipschitz bounds are explicit inputs on the closed unit ball. The tangent and joint field bounds require unit endpoint weights.

Mathematical proof

Open a step to read its argument and formula.

1. Control the orthogonal projection

For unit w, expand the squared norm of P_wz. Subtracting a nonnegative squared normal component proves contraction.

\[\|P_wz\|^2=\|z\|^2-\langle z,w\rangle^2\le\|z\|^2.\]

Corresponding Lean step

private theorem P_norm_le {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    (w z : E) (hw : ‖w‖ = 1) : ‖P w z‖ ≤ ‖z‖ := by
  have hsq : ‖P w z‖^2 = ‖z‖^2 - ⟪z,w⟫_ℝ^2 := by
    simp only [P,norm_sub_sq_real,inner_smul_right,norm_smul,hw,mul_one,
      Real.norm_eq_abs,sq_abs]
    ring
  nlinarith [sq_nonneg ⟪z,w⟫_ℝ,norm_nonneg (P w z),norm_nonneg z]

Literal implementation excerpt from AutoSamplingTheory/TechnicalLemmas/Geometry/QuadraticFeatureTangentGradient.lean. Local names retain their surrounding theorem context; the complete theorem and exact module context are folded below. These excerpts are presentation, not extra theorem premises.

2. Control projection movement

Rewrite the projection difference into one change of vector direction and one change of its inner product. Cauchy–Schwarz and unit norms bound both terms.

\[(P_w-P_u)z=\langle z,u\rangle(u-w)+\langle z,u-w\rangle w,\qquad \|(P_w-P_u)z\|\le2\|z\|\|w-u\|.\]

Corresponding Lean step

private theorem P_point_lip {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    (w u z : E) (hw : ‖w‖ = 1) (hu : ‖u‖ = 1) :
    ‖P w z-P u z‖ ≤ 2 * ‖z‖ * ‖w-u‖ := by
  have he : P w z-P u z = ⟪z,u⟫_ℝ • (u-w) + ⟪z,u-w⟫_ℝ • w := by
    simp only [P,inner_sub_right,smul_sub,sub_smul]
    abel
  rw [he]
  calc
    ‖⟪z,u⟫_ℝ • (u-w) + ⟪z,u-w⟫_ℝ • w‖ ≤
        ‖⟪z,u⟫_ℝ • (u-w)‖ + ‖⟪z,u-w⟫_ℝ • w‖ := norm_add_le _ _
    _ = ‖⟪z,u⟫_ℝ‖ * ‖u-w‖ + ‖⟪z,u-w⟫_ℝ‖ * ‖w‖ := by simp only [norm_smul]
    _ ≤ (‖z‖*‖u‖)*‖u-w‖ + (‖z‖*‖u-w‖)*‖w‖ := by
      gcongr <;> exact norm_inner_le_norm _ _
    _ = 2 * ‖z‖ * ‖w-u‖ := by rw [hw,hu,norm_sub_rev u w];ring

3. Differentiate the scalar potential

The chain rule for the bounded residual functional and the adjoint identity give the full ambient derivative. Projecting its representing vector removes only the normal part, which pairs to zero against every tangent direction.

\[DV_r(w)v=2\langle r,D(w)v\rangle=2\langle D(w)^*r,v\rangle,\quad \langle w,G_r(w)\rangle=0.\]

Corresponding Lean step

  · intro r w
    have he : (innerSL ℝ r).comp (D w) = innerSL ℝ ((D w).adjoint r) := by
      ext v
      simpa only [ContinuousLinearMap.comp_apply,innerSL_apply_apply] using
        ((D w).adjoint_inner_left v r).symm
    have h := (innerSL ℝ r).hasFDerivAt.comp w (hF w)
    rw [he] at h
    convert h.const_smul (2 : ℝ) using 1 <;>
      (first | rfl | (ext q; simp [Pi.smul_apply,smul_eq_mul,innerSL_apply_apply]))
  · intro r w hw
    refine ⟨?_,?_,?_⟩
    · simp only [inner_smul_right,inner_sub_right,inner_smul_right,real_inner_self_eq_norm_sq,hw]
      rw [real_inner_comm w ((D w).adjoint r)]
      ring
    · intro v hv
      simp only [real_inner_smul_left,inner_sub_left,real_inner_smul_left,hv,mul_zero,
        sub_zero,ContinuousLinearMap.adjoint_inner_left]

4. Bound the tangent field

Adjoints preserve operator norms; the projection is contractive. Multiplication by two gives the asserted residual-dependent bound.

\[\|G_r(w)\|\le2\|D(w)^*r\|\le2M_1\|r\|.\]

Corresponding Lean step

  have hAdj (w : E) (hw : ‖w‖ ≤ 1) (r : H) :
      ‖(D w).adjoint r‖ ≤ M₁ * ‖r‖ := by
    have h := (D w).adjoint.le_opNorm r
    rw [ContinuousLinearMap.adjoint.norm_map] at h
    exact h.trans (mul_le_mul_of_nonneg_right (hBound w hw) (norm_nonneg _))

    · change ‖(2 : ℝ) • P w ((D w).adjoint r)‖ ≤ _
      rw [norm_smul,Real.norm_of_nonneg (by norm_num : (0:ℝ) ≤ 2)]
      exact (mul_le_mul_of_nonneg_left ((P_norm_le _ _ hw).trans (hAdj w hw.le r))
        (by norm_num : (0:ℝ) ≤ 2)).trans_eq (by ring)

5. Separate residual and location changes

At a fixed w use linearity in r. For the fixed q location change, split the derivative-adjoint increment and the projection increment; combine the previous estimates.

\[G_r(w)-G_q(u)=2P_wD(w)^*(r-q)+2P_w(D(w)^*-D(u)^*)q+2(P_w-P_u)D(u)^*q.\]

Corresponding Lean step

  have hAdjDiff (w u : E) (hw : ‖w‖ ≤ 1) (hu : ‖u‖ ≤ 1) (q : H) :
      ‖((D w).adjoint-(D u).adjoint) q‖ ≤ (M₂*‖w-u‖)*‖q‖ := by
    have h := ((D w).adjoint-(D u).adjoint).le_opNorm q
    rw [← map_sub,ContinuousLinearMap.adjoint.norm_map] at h
    simpa only [map_sub] using h.trans (mul_le_mul_of_nonneg_right (hLip w u hw hu) (norm_nonneg _))
  have hFixed (q : H) (w u : E) (hw : ‖w‖ = 1) (hu : ‖u‖ = 1) :
      ‖P w ((D w).adjoint q) - P u ((D u).adjoint q)‖ ≤
        (M₂+2*M₁) * ‖q‖ * ‖w-u‖ := by
    have he : P w ((D w).adjoint q) - P u ((D u).adjoint q) =
        P w (((D w).adjoint-(D u).adjoint) q) +
          (P w ((D u).adjoint q) - P u ((D u).adjoint q)) := by
      rw [ContinuousLinearMap.sub_apply,P_sub]
      abel
    rw [he]
    calc
      ‖P w (((D w).adjoint-(D u).adjoint) q) +
          (P w ((D u).adjoint q) - P u ((D u).adjoint q))‖ ≤
        ‖P w (((D w).adjoint-(D u).adjoint) q)‖ +
          ‖P w ((D u).adjoint q) - P u ((D u).adjoint q)‖ := norm_add_le _ _
      _ ≤ ‖((D w).adjoint-(D u).adjoint) q‖ + 2 * ‖(D u).adjoint q‖ * ‖w-u‖ :=
        add_le_add (P_norm_le _ _ hw) (P_point_lip _ _ _ hw hu)
      _ ≤ (M₂*‖w-u‖)*‖q‖ + 2 * (M₁*‖q‖) * ‖w-u‖ := by
        gcongr
        · exact hAdjDiff w u hw.le hu.le q
        · exact hAdj u hu.le q
      _ = (M₂+2*M₁)*‖q‖*‖w-u‖ := by ring

  · intro r q w u hw hu
    change ‖(2 : ℝ) • P w ((D w).adjoint r) - (2 : ℝ) • P u ((D u).adjoint q)‖ ≤ _
    rw [← smul_sub,norm_smul,Real.norm_of_nonneg (by norm_num : (0:ℝ) ≤ 2)]
    have he : P w ((D w).adjoint r) - P u ((D u).adjoint q) =
        P w ((D w).adjoint (r-q)) +
          (P w ((D w).adjoint q) - P u ((D u).adjoint q)) := by
      rw [map_sub,P_sub]
      abel
    have hn : ‖P w ((D w).adjoint r) - P u ((D u).adjoint q)‖ ≤
        M₁*‖r-q‖ + (M₂+2*M₁)*‖q‖*‖w-u‖ := by
      rw [he]
      exact (norm_add_le _ _).trans (add_le_add
        ((P_norm_le _ _ hw).trans (hAdj w hw.le (r-q))) (hFixed q w u hw hu))
    exact (mul_le_mul_of_nonneg_left hn (by norm_num : (0:ℝ) ≤ 2)).trans_eq (by ring)

Lean verification

Lean proof · quadratic_feature_potential_tangent_gradient

The displayed formula proof explains the mathematical route; the exact Lean is folded adjacent.

Download module (.lean)

theorem quadratic_feature_potential_tangent_gradient
    {E H : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
    [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
    (F : E → H) (D : E → E →L[ℝ] H)
    (hF : ∀ w, HasFDerivAt F (D w) w)
    (M₁ M₂ : ℝ) (hM₁ : 0 ≤ M₁) (hM₂ : 0 ≤ M₂)
    (hBound : ∀ w : E, ‖w‖ ≤ 1 → ‖D w‖ ≤ M₁)
    (hLip : ∀ w u : E, ‖w‖ ≤ 1 → ‖u‖ ≤ 1 → ‖D w-D u‖ ≤ M₂*‖w-u‖) :
    let V : H → E → ℝ := fun r w => 2 * ⟪r,F w⟫_ℝ
    let G : H → E → E := fun r w =>
      (2 : ℝ) • ((D w).adjoint r - ⟪(D w).adjoint r,w⟫_ℝ • w)
    (∀ r w, HasFDerivAt (V r) ((2 : ℝ) • innerSL ℝ ((D w).adjoint r)) w) ∧
    (∀ r w, ‖w‖ = 1 →
      ⟪w,G r w⟫_ℝ = 0 ∧
      (∀ v, ⟪w,v⟫_ℝ = 0 → ⟪G r w,v⟫_ℝ = 2 * ⟪r,D w v⟫_ℝ) ∧
      ‖G r w‖ ≤ 2 * M₁ * ‖r‖) ∧
    ∀ r q w u, ‖w‖ = 1 → ‖u‖ = 1 →
      ‖G r w-G q u‖ ≤ 2 * M₁ * ‖r-q‖ +
        2 * (M₂+2*M₁) * ‖q‖ * ‖w-u‖ := by
  dsimp only
  have hAdj (w : E) (hw : ‖w‖ ≤ 1) (r : H) :
      ‖(D w).adjoint r‖ ≤ M₁ * ‖r‖ := by
    have h := (D w).adjoint.le_opNorm r
    rw [ContinuousLinearMap.adjoint.norm_map] at h
    exact h.trans (mul_le_mul_of_nonneg_right (hBound w hw) (norm_nonneg _))
  have hAdjDiff (w u : E) (hw : ‖w‖ ≤ 1) (hu : ‖u‖ ≤ 1) (q : H) :
      ‖((D w).adjoint-(D u).adjoint) q‖ ≤ (M₂*‖w-u‖)*‖q‖ := by
    have h := ((D w).adjoint-(D u).adjoint).le_opNorm q
    rw [← map_sub,ContinuousLinearMap.adjoint.norm_map] at h
    simpa only [map_sub] using h.trans (mul_le_mul_of_nonneg_right (hLip w u hw hu) (norm_nonneg _))
  have hFixed (q : H) (w u : E) (hw : ‖w‖ = 1) (hu : ‖u‖ = 1) :
      ‖P w ((D w).adjoint q) - P u ((D u).adjoint q)‖ ≤
        (M₂+2*M₁) * ‖q‖ * ‖w-u‖ := by
    have he : P w ((D w).adjoint q) - P u ((D u).adjoint q) =
        P w (((D w).adjoint-(D u).adjoint) q) +
          (P w ((D u).adjoint q) - P u ((D u).adjoint q)) := by
      rw [ContinuousLinearMap.sub_apply,P_sub]
      abel
    rw [he]
    calc
      ‖P w (((D w).adjoint-(D u).adjoint) q) +
          (P w ((D u).adjoint q) - P u ((D u).adjoint q))‖ ≤
        ‖P w (((D w).adjoint-(D u).adjoint) q)‖ +
          ‖P w ((D u).adjoint q) - P u ((D u).adjoint q)‖ := norm_add_le _ _
      _ ≤ ‖((D w).adjoint-(D u).adjoint) q‖ + 2 * ‖(D u).adjoint q‖ * ‖w-u‖ :=
        add_le_add (P_norm_le _ _ hw) (P_point_lip _ _ _ hw hu)
      _ ≤ (M₂*‖w-u‖)*‖q‖ + 2 * (M₁*‖q‖) * ‖w-u‖ := by
        gcongr
        · exact hAdjDiff w u hw.le hu.le q
        · exact hAdj u hu.le q
      _ = (M₂+2*M₁)*‖q‖*‖w-u‖ := by ring
  refine ⟨?_,?_,?_⟩
  · intro r w
    have he : (innerSL ℝ r).comp (D w) = innerSL ℝ ((D w).adjoint r) := by
      ext v
      simpa only [ContinuousLinearMap.comp_apply,innerSL_apply_apply] using
        ((D w).adjoint_inner_left v r).symm
    have h := (innerSL ℝ r).hasFDerivAt.comp w (hF w)
    rw [he] at h
    convert h.const_smul (2 : ℝ) using 1 <;>
      (first | rfl | (ext q; simp [Pi.smul_apply,smul_eq_mul,innerSL_apply_apply]))
  · intro r w hw
    refine ⟨?_,?_,?_⟩
    · simp only [inner_smul_right,inner_sub_right,inner_smul_right,real_inner_self_eq_norm_sq,hw]
      rw [real_inner_comm w ((D w).adjoint r)]
      ring
    · intro v hv
      simp only [real_inner_smul_left,inner_sub_left,real_inner_smul_left,hv,mul_zero,
        sub_zero,ContinuousLinearMap.adjoint_inner_left]
    · change ‖(2 : ℝ) • P w ((D w).adjoint r)‖ ≤ _
      rw [norm_smul,Real.norm_of_nonneg (by norm_num : (0:ℝ) ≤ 2)]
      exact (mul_le_mul_of_nonneg_left ((P_norm_le _ _ hw).trans (hAdj w hw.le r))
        (by norm_num : (0:ℝ) ≤ 2)).trans_eq (by ring)
  · intro r q w u hw hu
    change ‖(2 : ℝ) • P w ((D w).adjoint r) - (2 : ℝ) • P u ((D u).adjoint q)‖ ≤ _
    rw [← smul_sub,norm_smul,Real.norm_of_nonneg (by norm_num : (0:ℝ) ≤ 2)]
    have he : P w ((D w).adjoint r) - P u ((D u).adjoint q) =
        P w ((D w).adjoint (r-q)) +
          (P w ((D w).adjoint q) - P u ((D u).adjoint q)) := by
      rw [map_sub,P_sub]
      abel
    have hn : ‖P w ((D w).adjoint r) - P u ((D u).adjoint q)‖ ≤
        M₁*‖r-q‖ + (M₂+2*M₁)*‖q‖*‖w-u‖ := by
      rw [he]
      exact (norm_add_le _ _).trans (add_le_add
        ((P_norm_le _ _ hw).trans (hAdj w hw.le (r-q))) (hFixed q w u hw hu))
    exact (mul_le_mul_of_nonneg_left hn (by norm_num : (0:ℝ) ≤ 2)).trans_eq (by ring)

end AutoSamplingTheory.TechnicalLemmas.Geometry.QuadraticFeatureTangentGradient

Exact module and namespace context

Source correspondence and review

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
Let E,H be complete real inner-product normed spaces. Let F:E→H be a map, and let each D(w):E→H be a continuous real linear map satisfying the actual ambient identity DF(w)=D(w) for every w. Suppose M₁,M₂≥0, ‖D(w)‖op≤M₁ on the closed unit ball, and ‖D(w)−D(u)‖op≤M₂‖w−u‖ there. For r∈H define V_r(w)=2⟨r,F(w)⟩ and G_r(w)=2(D(w)r−⟨D(w)r,w⟩w), where * is the Hilbert adjoint. At every ambient w, V_r has derivative 2⟨D(w)*r,·⟩. At every unit w, G_r(w) is tangent, satisfies ⟨G_r(w),v⟩=2⟨r,D(w)v⟩ for every v perpendicular to w, and has norm at most 2M₁‖r‖. For all r,q and unit w,u, its joint increment is bounded by 2M₁‖r−q‖+2(M₂+2M₁)‖q‖‖w−u‖.	The exact adjacent signature preserves all displayed structures, generic inputs, actual function classes, measures, derivative and cost scopes.	same	For Gaussian features, moments and derivatives are produced. For generic tangent and transport interfaces the exact analytic and feature/cost premises remain explicit; no model instance or unspecified gradient/Wasserstein identification is claimed.

D, its actual derivative identity and the two operator bounds are explicit generic hypotheses; a concrete feature model must produce them separately.; The conclusion is a tangent Riesz representation. Equality with a chosen manifold-gradient API, a geodesic-distance or law-Wasserstein estimate, and a uniform residual bound are separate obligations.

Encoder–denoiser: accepted · equivalent-after-elaboration

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

Scope and omitted-condition boundaries

D, its actual derivative identity and the two operator bounds are explicit generic hypotheses; a concrete feature model must produce them separately.
The conclusion is a tangent Riesz representation. Equality with a chosen manifold-gradient API, a geodesic-distance or law-Wasserstein estimate, and a uniform residual bound are separate obligations.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Pinned Mathlib adjoint and Hilbert Fréchet calculus

Mathematical sources

Samplinglib original feature differentiation and transport supplement v1 (2026-10-21) (historical source) — Original generic mathematical supplement from the cited pinned library prerequisites; no primary-textbook theorem or statistical convergence 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.

Which proof obligations and prerequisites are covered?

Formalized proof edge; source adapter/review separate A Hilbert feature potential has a controlled tangent Riesz field

Explicit geodesics and exponential maps on the unit sphere

Nicolas Boumal for the geometric route; Samplinglib supplies the ambient Hilbert-space formulas and explicit fourth-order analytic bounds.

An Introduction to Optimization on Smooth Manifolds, 2023 · sphere geometry, geodesics, and the Riemannian exponential map · faithful paraphrase

Complete source statement (Samplinglib restatement)

In a real inner-product space, the standard trigonometric curve gives the signed unit-sphere geodesic. It is smooth, agrees with the ambient exponential formula at nonnegative time, preserves unit norm for tangent increments, and has explicit derivatives and uniform bounds through order four.

The ambient space is a real normed additive commutative group with an inner product.
Norm preservation assumes a unit base point and an orthogonal tangent increment.
The displayed closed derivative bundle assumes nonzero velocity; zero velocity is the constant curve.

ambient exponential

\[\operatorname{Exp}_w(z)=\cos(\|z\|)w+\operatorname{sinc}(\|z\|)z\]

derivative envelope

\[\|\gamma^{(q)}(t)\|\le2\|z\|^q,\qquad q=1,2,3,4\]

Read the formalized proofs

Each statement and proof below has its own closed Lean disclosure. Samplinglib parents, Mathlib calls and external mathematical sources are distinguished in each proof.

Samplinglib mathematical lesson

The ambient exponential map of the unit sphere

AutoSamplingTheory.TechnicalLemmas.Geometry.UnitSphere.unitSphereExp · def · Teaching coverage

Read this first

Mathematical statement

The sphere exponential formula combines the base direction with a sinc-scaled increment.

\[\operatorname{Exp}_w(z)=\cos(\|z\|)w+\operatorname{sinc}(\|z\|)z\]

Lean statement · unitSphereExp

Lean defines a total ambient-space map.

Download module (.lean)

noncomputable def unitSphereExp (w z : E) : E

Exact module and namespace context

Proof roadmap

1Rotate in the span of w and z
Cosine weights the base direction and sine-over-radius weights the increment.

Full assumptions and notation

All objects and hypotheses

E is a real inner-product space.
w and z are ambient vectors.
sinc supplies the continuous value at z=0.

Construction and meaning

1. Rotate in the span of w and z

Cosine weights the base direction and sine-over-radius weights the increment.

\[\cos r\,w+\frac{\sin r}{r}z,\quad r=\|z\|\]

Corresponding Lean step

Real.sinc makes this a total formula.

Lean verification

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

Lean construction · unitSphereExp

The later norm theorem states the exact tangency conditions for sphere membership.

Download module (.lean)

noncomputable def unitSphereExp (w z : E) : E :=
  Real.cos ‖z‖ • w + Real.sinc ‖z‖ • z

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
The textbook route states the standard finite-dimensional formula in ordinary mathematical notation.	The declaration exposes exactly the algebraic, differentiability, unit-norm, orthogonality, or bounded-input hypotheses used by its proof.	source-implicit	Lean records domain and regularity conditions that textbook prose normally leaves in the surrounding context.

Without unit length and tangency, unit norm is not asserted.

Encoder–denoiser: accepted · exact

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

Scope and omitted-condition boundaries

Without unit length and tangency, unit norm is not asserted.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

No direct Mathlib call recorded; see the Samplinglib parents.

Mathematical sources

Samplinglib compiled source — Exact statement and proof.

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

A signed great-circle parameterization

AutoSamplingTheory.TechnicalLemmas.Geometry.UnitSphere.unitSphereGeodesic · def · Teaching coverage

Read this first

Mathematical statement

The curve uses cos(t‖z‖) and sin(t‖z‖)/‖z‖, with a constant zero-velocity branch.

\[\gamma_{w,z}(t)=\begin{cases}w,&z=0,\\\cos(t\|z\|)w+\frac{\sin(t\|z\|)}{\|z\|}z,&z\ne0.\end{cases}\]

Lean statement · unitSphereGeodesic

The signed parameterization avoids the absolute value introduced by ‖t • z‖.

Download module (.lean)

noncomputable def unitSphereGeodesic (w z : E) (t : ℝ) : E

Exact module and namespace context

Proof roadmap

1Choose the removable branch
Zero velocity gives the constant curve; nonzero velocity gives the signed trigonometric formula.

Full assumptions and notation

All objects and hypotheses

E is a real inner-product space.
t may be negative, zero, or positive.
The zero-velocity branch is explicit.

Construction and meaning

1. Choose the removable branch

Zero velocity gives the constant curve; nonzero velocity gives the signed trigonometric formula.

\[z=0\Rightarrow\gamma(t)=w\]

Corresponding Lean step

Lean uses an if ‖z‖ = 0 branch.

Lean verification

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

Lean construction · unitSphereGeodesic

Subsequent theorems prove its smoothness and relation to the exponential formula.

Download module (.lean)

noncomputable def unitSphereGeodesic (w z : E) (t : ℝ) : E :=
  if ‖z‖ = 0 then w
  else Real.cos (t * ‖z‖) • w +
    (Real.sin (t * ‖z‖) / ‖z‖) • z

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
The textbook route states the standard finite-dimensional formula in ordinary mathematical notation.	The declaration exposes exactly the algebraic, differentiability, unit-norm, orthogonality, or bounded-input hypotheses used by its proof.	source-implicit	Lean records domain and regularity conditions that textbook prose normally leaves in the surrounding context.

w need not be unit and z need not be tangent for the definition.

Encoder–denoiser: accepted · exact

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

Scope and omitted-condition boundaries

w need not be unit and z need not be tangent for the definition.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

No direct Mathlib call recorded; see the Samplinglib parents.

Mathematical sources

Samplinglib compiled source — Exact statement and proof.

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

Signed sphere geodesics are smooth

AutoSamplingTheory.TechnicalLemmas.Geometry.UnitSphere.unitSphereGeodesic_contDiff · theorem · Teaching coverage

Read this first

Mathematical statement

For fixed base point and velocity, the signed great-circle curve is continuously differentiable to every requested finite order.

\[\gamma_{w,z}\in C^n(\mathbb R;E)\]

Lean statement · unitSphereGeodesic_contDiff

The theorem returns `ContDiff ℝ n`.

Download module (.lean)

theorem unitSphereGeodesic_contDiff (w z : E) (n : WithTop ℕ∞) :
    ContDiff ℝ n (unitSphereGeodesic w z)

Exact module and namespace context

Proof roadmap

1Split on zero velocity
The zero branch is constant; in the nonzero branch all scalar trigonometric operations are smooth.

Full assumptions and notation

All objects and hypotheses

E is a real inner-product space.
No unit-length or tangency assumption is needed.
n is any Mathlib differentiability order.

Mathematical proof

1. Split on zero velocity

The zero branch is constant; in the nonzero branch all scalar trigonometric operations are smooth.

\[z=0\Rightarrow\gamma(t)=w;\quad z\ne0\Rightarrow\gamma(t)=\cos(tr)w+\frac{\sin(tr)}r z\]

Corresponding Lean step

fun_prop proves both branches after the case split.

Lean verification

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

Lean proof · unitSphereGeodesic_contDiff

The only case split handles the removable zero-velocity denominator.

Download module (.lean)

theorem unitSphereGeodesic_contDiff (w z : E) (n : WithTop ℕ∞) :
    ContDiff ℝ n (unitSphereGeodesic w z) := by
  by_cases hz : ‖z‖ = 0
  · have hgeo : unitSphereGeodesic w z = fun _ : ℝ => w := by
      funext t
      simp [unitSphereGeodesic, hz]
    rw [hgeo]
    fun_prop
  · unfold unitSphereGeodesic
    simp only [hz, ↓reduceIte]
    fun_prop

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
The textbook route states the standard finite-dimensional formula in ordinary mathematical notation.	The declaration exposes exactly the algebraic, differentiability, unit-norm, orthogonality, or bounded-input hypotheses used by its proof.	source-implicit	Lean records domain and regularity conditions that textbook prose normally leaves in the surrounding context.

Smoothness alone does not imply the curve lies on a sphere.

Encoder–denoiser: accepted · exact

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

Scope and omitted-condition boundaries

Smoothness alone does not imply the curve lies on a sphere.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

No direct Mathlib call recorded; see the Samplinglib parents.

Mathematical sources

Samplinglib compiled source — Exact statement and proof.

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

The exponential formula is continuous in its increment

AutoSamplingTheory.TechnicalLemmas.Geometry.UnitSphere.unitSphereExp_continuous · theorem · Teaching coverage

Read this first

Mathematical statement

For a fixed base point, the ambient sphere exponential formula depends continuously on z.

\[z_n\to z\Longrightarrow\operatorname{Exp}_w(z_n)\to\operatorname{Exp}_w(z)\]

Lean statement · unitSphereExp_continuous

The conclusion is ordinary topological continuity.

Download module (.lean)

theorem unitSphereExp_continuous (w : E) : Continuous (unitSphereExp w)

Exact module and namespace context

Proof roadmap

1Compose continuous operations
The norm, cosine, sinc, scalar multiplication, and addition are continuous.

Full assumptions and notation

All objects and hypotheses

E is a real inner-product space.
w is fixed.
No tangency premise is needed.

Mathematical proof

1. Compose continuous operations

The norm, cosine, sinc, scalar multiplication, and addition are continuous.

\[z\mapsto\cos(\|z\|)w+\operatorname{sinc}(\|z\|)z\]

Corresponding Lean step

After unfolding, fun_prop applies Mathlib's continuity rules.

Lean verification

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

Lean proof · unitSphereExp_continuous

The proof is a direct closure argument.

Download module (.lean)

theorem unitSphereExp_continuous (w : E) : Continuous (unitSphereExp w) := by
  unfold unitSphereExp
  fun_prop

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
The textbook route states the standard finite-dimensional formula in ordinary mathematical notation.	The declaration exposes exactly the algebraic, differentiability, unit-norm, orthogonality, or bounded-input hypotheses used by its proof.	source-implicit	Lean records domain and regularity conditions that textbook prose normally leaves in the surrounding context.

Joint differentiability in both arguments is not claimed.

Encoder–denoiser: accepted · exact

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

Scope and omitted-condition boundaries

Joint differentiability in both arguments is not claimed.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

No direct Mathlib call recorded; see the Samplinglib parents.

Mathematical sources

Samplinglib compiled source — Exact statement and proof.

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

Forward exponential steps equal the signed geodesic

AutoSamplingTheory.TechnicalLemmas.Geometry.UnitSphere.unitSphereExp_smul_eq_unitSphereGeodesic · theorem · Teaching coverage

Read this first

Mathematical statement

For nonnegative time, exponentiating the scaled increment tz equals the signed geodesic at t.

\[t\ge0\Longrightarrow\operatorname{Exp}_w(tz)=\gamma_{w,z}(t)\]

Lean statement · unitSphereExp_smul_eq_unitSphereGeodesic

The nonnegative-time hypothesis is visible.

Download module (.lean)

theorem unitSphereExp_smul_eq_unitSphereGeodesic
    (w z : E) {t : ℝ} (ht : 0 ≤ t) :
    unitSphereExp w (t • z) = unitSphereGeodesic w z t

Exact module and namespace context

Proof roadmap

1Handle degenerate cases
When t=0 or z=0, both sides reduce to w.
2Rewrite the scaled norm
Nonnegative t gives ‖tz‖=t‖z‖.
3Expand sinc and cancel t
For nonzero t‖z‖, sinc becomes sine divided by its argument.

Full assumptions and notation

All objects and hypotheses

t is nonnegative.
Zero time and zero velocity are allowed.
w and z are arbitrary ambient vectors.

Mathematical proof

1. Handle degenerate cases

When t=0 or z=0, both sides reduce to w.

\[t=0\text{ or }z=0\Rightarrow\operatorname{Exp}_w(tz)=w\]

Corresponding Lean step

Lean discharges both branches by simplification.

2. Rewrite the scaled norm

Nonnegative t gives ‖tz‖=t‖z‖.

\[\|tz\|=t\|z\|\]

Corresponding Lean step

norm_smul and abs_of_nonneg prove the equality.

3. Expand sinc and cancel t

For nonzero t‖z‖, sinc becomes sine divided by its argument.

\[\operatorname{sinc}(t\|z\|)(tz)=\frac{\sin(t\|z\|)}{\|z\|}z\]

Corresponding Lean step

Real.sinc_of_ne_zero and field simplification finish.

Lean verification

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

Lean proof · unitSphereExp_smul_eq_unitSphereGeodesic

All denominator and zero cases are handled explicitly.

Download module (.lean)

theorem unitSphereExp_smul_eq_unitSphereGeodesic
    (w z : E) {t : ℝ} (ht : 0 ≤ t) :
    unitSphereExp w (t • z) = unitSphereGeodesic w z t := by
  by_cases hz : z = 0
  · subst z
    simp [unitSphereExp, unitSphereGeodesic]
  by_cases ht0 : t = 0
  · subst t
    simp [unitSphereExp, unitSphereGeodesic]
  have hr : ‖z‖ ≠ 0 := norm_ne_zero_iff.mpr hz
  have htne : t ≠ 0 := ht0
  have hnorm : ‖t • z‖ = t * ‖z‖ := by
    rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg ht]
  rw [unitSphereExp, unitSphereGeodesic, if_neg hr, hnorm,
    Real.sinc_of_ne_zero (mul_ne_zero htne hr)]
  congr 1
  rw [smul_smul]
  congr 1
  field_simp [htne, hr]

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
The textbook route states the standard finite-dimensional formula in ordinary mathematical notation.	The declaration exposes exactly the algebraic, differentiability, unit-norm, orthogonality, or bounded-input hypotheses used by its proof.	source-implicit	Lean records domain and regularity conditions that textbook prose normally leaves in the surrounding context.

The same equality is not claimed for negative t because the exponential formula uses ‖tz‖.

Encoder–denoiser: accepted · exact

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

Scope and omitted-condition boundaries

The same equality is not claimed for negative t because the exponential formula uses ‖tz‖.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

No direct Mathlib call recorded; see the Samplinglib parents.

Mathematical sources

Samplinglib compiled source — Exact statement and proof.

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

A fourth-order certificate for sphere geodesics

AutoSamplingTheory.TechnicalLemmas.Geometry.UnitSphere.unitSphereGeodesic_derivatives_and_bounds · theorem · Teaching coverage

Read this first

Mathematical statement

At a unit base point and nonzero velocity, the first four derivatives have explicit formulas and satisfy ‖γ^(q)(t)‖≤2‖z‖^q for q=1,2,3,4.

\[\|\gamma_{w,z}^{(q)}(t)\|\le2\|z\|^q\quad(q=1,2,3,4)\]

Lean statement · unitSphereGeodesic_derivatives_and_bounds

Consumers receive exact `HasDerivAt` witnesses as well as estimates.

Download module (.lean)

theorem unitSphereGeodesic_derivatives_and_bounds
    {w z : E} (hw : ‖w‖ = 1) (hz : z ≠ 0) (t : ℝ) :
    (HasDerivAt (unitSphereGeodesic w z)
        ((-(‖z‖ * Real.sin (t * ‖z‖))) • w +
          Real.cos (t * ‖z‖) • z) t ∧
      HasDerivAt
        (fun s : ℝ =>
          (-(‖z‖ * Real.sin (s * ‖z‖))) • w +
            Real.cos (s * ‖z‖) • z)
        ((-(‖z‖ ^ (2 : ℕ) * Real.cos (t * ‖z‖))) • w +
          (-(‖z‖ * Real.sin (t * ‖z‖))) • z) t ∧
      HasDerivAt
        (fun s : ℝ =>
          (-(‖z‖ ^ (2 : ℕ) * Real.cos (s * ‖z‖))) • w +
            (-(‖z‖ * Real.sin (s * ‖z‖))) • z)
        ((‖z‖ ^ (3 : ℕ) * Real.sin (t * ‖z‖)) • w +
          (-(‖z‖ ^ (2 : ℕ) * Real.cos (t * ‖z‖))) • z) t ∧
      HasDerivAt
        (fun s : ℝ =>
          (‖z‖ ^ (3 : ℕ) * Real.sin (s * ‖z‖)) • w +
            (-(‖z‖ ^ (2 : ℕ) * Real.cos (s * ‖z‖))) • z)
        ((‖z‖ ^ (4 : ℕ) * Real.cos (t * ‖z‖)) • w +
          (‖z‖ ^ (3 : ℕ) * Real.sin (t * ‖z‖)) • z) t) ∧
    (‖(-(‖z‖ * Real.sin (t * ‖z‖))) • w +
          Real.cos (t * ‖z‖) • z‖ ≤ 2 * ‖z‖ ∧
      ‖(-(‖z‖ ^ (2 : ℕ) * Real.cos (t * ‖z‖))) • w +
          (-(‖z‖ * Real.sin (t * ‖z‖))) • z‖ ≤
        2 * ‖z‖ ^ (2 : ℕ) ∧
      ‖(‖z‖ ^ (3 : ℕ) * Real.sin (t * ‖z‖)) • w +
          (-(‖z‖ ^ (2 : ℕ) * Real.cos (t * ‖z‖))) • z‖ ≤
        2 * ‖z‖ ^ (3 : ℕ) ∧
      ‖(‖z‖ ^ (4 : ℕ) * Real.cos (t * ‖z‖)) • w +
          (‖z‖ ^ (3 : ℕ) * Real.sin (t * ‖z‖)) • z‖ ≤
        2 * ‖z‖ ^ (4 : ℕ))

Exact module and namespace context

Proof roadmap

1Differentiate four times
Sine and cosine alternate and each differentiation contributes one power of ‖z‖.
2Bound the two components
Use the triangle inequality, ‖w‖=1, and |sin|,|cos|≤1.
3Return one reusable certificate
The public theorem packages four exact derivative witnesses and four bounds.

Full assumptions and notation

All objects and hypotheses

E is any real inner-product space.
‖w‖=1.
z≠0 selects the displayed closed form.
No finite-dimensional or probabilistic hypothesis is used.

Mathematical proof

1. Differentiate four times

Sine and cosine alternate and each differentiation contributes one power of ‖z‖.

\[\gamma'(t)=-r\sin(tr)w+\cos(tr)z,\quad\gamma''(t)=-r^2\cos(tr)w-r\sin(tr)z,\ldots\]

Corresponding Lean step

Private HasDerivAt lemmas prove every displayed derivative.

2. Bound the two components

Use the triangle inequality, ‖w‖=1, and |sin|,|cos|≤1.

\[\|a(t)w+b(t)z\|\le2\|z\|^q\]

Corresponding Lean step

Private norm lemmas prove all four uniform envelopes.

3. Return one reusable certificate

The public theorem packages four exact derivative witnesses and four bounds.

\[(\gamma',\gamma'',\gamma^{(3)},\gamma^{(4)})\text{ and }(2r,2r^2,2r^3,2r^4)\]

Corresponding Lean step

Conjunction introduction assembles the reviewed helpers.

Lean verification

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

Lean proof · unitSphereGeodesic_derivatives_and_bounds

All analytic helpers live in the same module and compile with the public theorem.

Download module (.lean)

theorem unitSphereGeodesic_derivatives_and_bounds
    {w z : E} (hw : ‖w‖ = 1) (hz : z ≠ 0) (t : ℝ) :
    (HasDerivAt (unitSphereGeodesic w z)
        ((-(‖z‖ * Real.sin (t * ‖z‖))) • w +
          Real.cos (t * ‖z‖) • z) t ∧
      HasDerivAt
        (fun s : ℝ =>
          (-(‖z‖ * Real.sin (s * ‖z‖))) • w +
            Real.cos (s * ‖z‖) • z)
        ((-(‖z‖ ^ (2 : ℕ) * Real.cos (t * ‖z‖))) • w +
          (-(‖z‖ * Real.sin (t * ‖z‖))) • z) t ∧
      HasDerivAt
        (fun s : ℝ =>
          (-(‖z‖ ^ (2 : ℕ) * Real.cos (s * ‖z‖))) • w +
            (-(‖z‖ * Real.sin (s * ‖z‖))) • z)
        ((‖z‖ ^ (3 : ℕ) * Real.sin (t * ‖z‖)) • w +
          (-(‖z‖ ^ (2 : ℕ) * Real.cos (t * ‖z‖))) • z) t ∧
      HasDerivAt
        (fun s : ℝ =>
          (‖z‖ ^ (3 : ℕ) * Real.sin (s * ‖z‖)) • w +
            (-(‖z‖ ^ (2 : ℕ) * Real.cos (s * ‖z‖))) • z)
        ((‖z‖ ^ (4 : ℕ) * Real.cos (t * ‖z‖)) • w +
          (‖z‖ ^ (3 : ℕ) * Real.sin (t * ‖z‖)) • z) t) ∧
    (‖(-(‖z‖ * Real.sin (t * ‖z‖))) • w +
          Real.cos (t * ‖z‖) • z‖ ≤ 2 * ‖z‖ ∧
      ‖(-(‖z‖ ^ (2 : ℕ) * Real.cos (t * ‖z‖))) • w +
          (-(‖z‖ * Real.sin (t * ‖z‖))) • z‖ ≤
        2 * ‖z‖ ^ (2 : ℕ) ∧
      ‖(‖z‖ ^ (3 : ℕ) * Real.sin (t * ‖z‖)) • w +
          (-(‖z‖ ^ (2 : ℕ) * Real.cos (t * ‖z‖))) • z‖ ≤
        2 * ‖z‖ ^ (3 : ℕ) ∧
      ‖(‖z‖ ^ (4 : ℕ) * Real.cos (t * ‖z‖)) • w +
          (‖z‖ ^ (3 : ℕ) * Real.sin (t * ‖z‖)) • z‖ ≤
        2 * ‖z‖ ^ (4 : ℕ)) := by
  constructor
  · exact ⟨unitSphereGeodesic_hasDerivAt w hz t,
      unitSphereGeodesic_velocity_hasDerivAt w z t,
      unitSphereGeodesic_acceleration_hasDerivAt w z t,
      unitSphereGeodesic_jerk_hasDerivAt w z t⟩
  · exact ⟨unitSphereGeodesic_first_derivative_norm_le hw t,
      unitSphereGeodesic_second_derivative_norm_le hw t,
      unitSphereGeodesic_third_derivative_norm_le hw t,
      unitSphereGeodesic_fourth_derivative_norm_le hw t⟩

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
The textbook route states the standard finite-dimensional formula in ordinary mathematical notation.	The declaration exposes exactly the algebraic, differentiability, unit-norm, orthogonality, or bounded-input hypotheses used by its proof.	source-implicit	Lean records domain and regularity conditions that textbook prose normally leaves in the surrounding context.

The constant 2 is a simple uniform envelope, not an optimality claim.

Encoder–denoiser: accepted · exact

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

Scope and omitted-condition boundaries

The constant 2 is a simple uniform envelope, not an optimality claim.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

No direct Mathlib call recorded; see the Samplinglib parents.

Mathematical sources

Samplinglib compiled source — Exact statement and proof.

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

Tangent exponential steps remain on the unit sphere

AutoSamplingTheory.TechnicalLemmas.Geometry.UnitSphere.unitSphereExp_norm_eq_one · theorem · Teaching coverage

Read this first

Mathematical statement

A unit base point and an orthogonal increment produce an exponential-map value with exactly unit norm.

\[\|w\|=1,\ \langle w,z\rangle=0\Longrightarrow\|\operatorname{Exp}_w(z)\|=1\]

Lean statement · unitSphereExp_norm_eq_one

The theorem gives exact feasibility, not an asymptotic estimate.

Download module (.lean)

theorem unitSphereExp_norm_eq_one
    {w z : E}
    (hw : ‖w‖ = 1)
    (htan : ⟪w, z⟫_ℝ = 0) :
    ‖unitSphereExp w z‖ = 1

Exact module and namespace context

Proof roadmap

1Handle zero increment
At z=0, the exponential formula is w.
2Use orthogonality
The cosine and sinc components have zero cross inner product.
3Apply Pythagoras and trigonometry
The two squared norms are cos²r and sin²r.
4Use nonnegativity of norm
A nonnegative real with square one equals one.

Full assumptions and notation

All objects and hypotheses

E is a real inner-product space.
‖w‖=1.
⟪w,z⟫=0.
z=0 is allowed.

Mathematical proof

1. Handle zero increment

At z=0, the exponential formula is w.

\[z=0\Rightarrow\operatorname{Exp}_w(z)=w\]

Corresponding Lean step

Simplification uses the unit-norm premise.

2. Use orthogonality

The cosine and sinc components have zero cross inner product.

\[\langle\cos(r)w,\operatorname{sinc}(r)z\rangle=0\]

Corresponding Lean step

Inner-product scalar rules reduce this to ⟪w,z⟫=0.

3. Apply Pythagoras and trigonometry

The two squared norms are cos²r and sin²r.

\[\|\operatorname{Exp}_w(z)\|^2=\cos^2r+\sin^2r=1\]

Corresponding Lean step

norm_add_sq_real, Real.sinc_of_ne_zero, and Real.sin_sq_add_cos_sq prove the identity.

4. Use nonnegativity of norm

A nonnegative real with square one equals one.

\[x\ge0,\ x^2=1\Rightarrow x=1\]

Corresponding Lean step

Nonlinear arithmetic closes the final scalar step.

Lean verification

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

Lean proof · unitSphereExp_norm_eq_one

The proof is the orthogonal norm identity plus sin²+cos²=1.

Download module (.lean)

theorem unitSphereExp_norm_eq_one
    {w z : E}
    (hw : ‖w‖ = 1)
    (htan : ⟪w, z⟫_ℝ = 0) :
    ‖unitSphereExp w z‖ = 1 := by
  by_cases hz : z = 0
  · subst z
    simp [unitSphereExp, hw]
  · have hr : ‖z‖ ≠ 0 := norm_ne_zero_iff.mpr hz
    have hcross :
        ⟪Real.cos ‖z‖ • w, Real.sinc ‖z‖ • z⟫_ℝ = 0 := by
      simp [real_inner_smul_left, real_inner_smul_right, htan]
    have hpyth :
        ‖unitSphereExp w z‖ ^ (2 : ℕ) =
          ‖Real.cos ‖z‖ • w‖ ^ (2 : ℕ) +
          ‖Real.sinc ‖z‖ • z‖ ^ (2 : ℕ) := by
      rw [unitSphereExp, norm_add_sq_real, hcross]
      ring
    have hfirst :
        ‖Real.cos ‖z‖ • w‖ ^ (2 : ℕ) =
          Real.cos ‖z‖ ^ (2 : ℕ) := by
      simp [norm_smul, hw, sq_abs]
    have hsinc :
        Real.sinc ‖z‖ = Real.sin ‖z‖ / ‖z‖ :=
      Real.sinc_of_ne_zero hr
    have hsecond :
        ‖Real.sinc ‖z‖ • z‖ ^ (2 : ℕ) =
          Real.sin ‖z‖ ^ (2 : ℕ) := by
      rw [norm_smul, Real.norm_eq_abs, hsinc]
      have hrpos : 0 < ‖z‖ := norm_pos_iff.mpr hz
      rw [abs_div, abs_of_pos hrpos]
      rw [div_mul_cancel₀ _ hr]
      exact sq_abs (Real.sin ‖z‖)
    have hsq : ‖unitSphereExp w z‖ ^ (2 : ℕ) = 1 := by
      rw [hpyth, hfirst, hsecond]
      nlinarith [Real.sin_sq_add_cos_sq ‖z‖]
    have hnonneg : 0 ≤ ‖unitSphereExp w z‖ := norm_nonneg _
    nlinarith


end

end AutoSamplingTheory.TechnicalLemmas.Geometry.UnitSphere

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
The textbook route states the standard finite-dimensional formula in ordinary mathematical notation.	The declaration exposes exactly the algebraic, differentiability, unit-norm, orthogonality, or bounded-input hypotheses used by its proof.	source-implicit	Lean records domain and regularity conditions that textbook prose normally leaves in the surrounding context.

No algorithmic convergence theorem is included.

Encoder–denoiser: accepted · exact

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

Scope and omitted-condition boundaries

No algorithmic convergence theorem is included.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

No direct Mathlib call recorded; see the Samplinglib parents.

Mathematical sources

Samplinglib compiled source — Exact statement and proof.

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

Which proof obligations and prerequisites are covered?

Independently verified prerequisite Define the exponential formula and signed geodesic
Independently verified prerequisite Prove smoothness and continuity
Independently verified prerequisite Identify forward geodesic time with scaled exponential input
Independently verified prerequisite Verify exact derivatives and bounds through order four
Independently verified prerequisite Prove that tangent increments remain on the unit sphere

Second-order necessary conditions on the unit sphere

The standard second-order necessary condition and sphere restriction are textbook calculus/Riemannian optimization; Samplinglib supplies the Lean bridge to Mathlib total derivatives and explicit trace hypotheses.

An Introduction to Optimization on Smooth Manifolds, 2023; Mathlib v4.33.0 · second-order necessary optimality conditions and unit-sphere exponential curves · faithful paraphrase

Complete source statement (Samplinglib restatement)

A continuous real function has nonnegative double derivative at a local minimum and nonpositive double derivative at a local maximum. On the unit sphere, restricting a global extremum to tangent exponential curves yields the corresponding sign for every supplied Hessian diagonal, hence for its finite trace.

Scalar extrema use continuity at the extremum and Mathlib’s total deriv (deriv f).
Sphere extrema use a unit base point, tangent directions, continuity along each exponential curve, exact diagonal identities, and a finite trace identity.
No PDE or model-specific coefficient occurs.

scalar necessary condition

\[x\text{ local min}\Rightarrow f^{\prime\prime}(x)\ge0,\qquad x\text{ local max}\Rightarrow f^{\prime\prime}(x)\le0\]

sphere trace sign

\[\Delta f(w)=\sum_i (f\circ\operatorname{Exp}_w(tz_i))^{\prime\prime}(0)\gtreqless0\]

Read the formalized proofs

Each statement and proof below has its own closed Lean disclosure. Samplinglib parents, Mathlib calls and external mathematical sources are distinguished in each proof.

Samplinglib mathematical lesson

Second derivative at a local minimum

AutoSamplingTheory.TechnicalLemmas.Geometry.SphereSecondOrder.IsLocalMin.deriv_deriv_nonneg_of_continuousAt · theorem · Teaching coverage

Read this first

Mathematical statement

For a real function continuous at a local minimum, the second derivative represented by deriv (deriv f) is nonnegative.

\[x\text{ local min of }f,\ f\text{ continuous at }x\Longrightarrow (\operatorname{deriv}\operatorname{deriv}f)(x)\ge0\]

Lean statement · deriv_deriv_nonneg_of_continuousAt

The Lean theorem states the displayed necessary sign with every continuity, tangency, diagonal, and trace premise explicit.

Download module (.lean)

theorem IsLocalMin.deriv_deriv_nonneg_of_continuousAt
    {f : ℝ → ℝ} {x : ℝ} (hmin : IsLocalMin f x)
    (hc : ContinuousAt f x) :
    0 ≤ deriv (deriv f) x

Exact module and namespace context

Proof roadmap

1Rule out a negative second derivative
If the second derivative were negative, Mathlib’s strict second-derivative test would also make x a local maximum.
2Combine the two local inequalities
A point that is both a local minimum and a local maximum has a neighborhood on which f is constant.
3Differentiate the local equality twice
The derivative is locally zero, hence its derivative at x is zero, contradicting strict negativity.

Full assumptions and notation

All objects and hypotheses

f is a real-valued function on the real line.
x is a local minimum of f.
f is continuous at x; Mathlib deriv is total and equals zero at nondifferentiable points.

Mathematical proof

1. Rule out a negative second derivative

If the second derivative were negative, Mathlib’s strict second-derivative test would also make x a local maximum.

\[f^{\prime\prime}(x)<0\Longrightarrow x\text{ is a local maximum}\]

Corresponding Lean step

Use isLocalMax_of_deriv_deriv_neg, with Fermat’s identity at the local minimum.

2. Combine the two local inequalities

A point that is both a local minimum and a local maximum has a neighborhood on which f is constant.

\[f(x)\le f(y)\le f(x)\Longrightarrow f(y)=f(x)\]

Corresponding Lean step

Intersect the two neighborhood filters and apply antisymmetry.

3. Differentiate the local equality twice

The derivative is locally zero, hence its derivative at x is zero, contradicting strict negativity.

\[f\equiv f(x)\text{ locally}\Longrightarrow f^\prime\equiv0\text{ locally}\Longrightarrow f^{\prime\prime}(x)=0\]

Corresponding Lean step

Filter.EventuallyEq.deriv and deriv_eq transport the local equality.

Lean verification

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

Lean proof · deriv_deriv_nonneg_of_continuousAt

The proof reduces a forbidden strict sign to simultaneous local minimum and maximum, or restricts the sphere extremum to feasible exponential curves and sums the scalar signs.

Download module (.lean)

theorem IsLocalMin.deriv_deriv_nonneg_of_continuousAt
    {f : ℝ → ℝ} {x : ℝ} (hmin : IsLocalMin f x)
    (hc : ContinuousAt f x) :
    0 ≤ deriv (deriv f) x := by
  by_contra hnonneg
  have hneg : deriv (deriv f) x < 0 := lt_of_not_ge hnonneg
  have hmax : IsLocalMax f x :=
    isLocalMax_of_deriv_deriv_neg hneg hmin.deriv_eq_zero hc
  have hconst : f =ᶠ[𝓝 x] fun _ : ℝ => f x := by
    filter_upwards [hmin, hmax] with y hymin hymax
    exact le_antisymm hymax hymin
  have hderiv : deriv f =ᶠ[𝓝 x] fun _ : ℝ => 0 := by
    simpa using hconst.deriv
  have hzero : deriv (deriv f) x = 0 := by
    calc
      deriv (deriv f) x = deriv (fun _ : ℝ => 0) x := hderiv.deriv_eq
      _ = 0 := by simp
  linarith

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
The classical textbook statement assumes an ordinary second derivative at the extremum.	The scalar result is stated for Mathlib’s total expression deriv (deriv f), with continuity at the extremum. If either derivative is unavailable, Mathlib supplies zero.	generalization	The proof shows the non-strict sign for the totalized expression on a larger domain; the public lesson and boundary do not reinterpret it as existence of a classical second derivative.
Textbook sphere statements are usually finite-dimensional.	The geometric trace theorem works in any real inner-product space for an explicitly finite family of tangent directions.	generalization	The proof uses only tangent exponential curves and a finite sum.

This uses Mathlib’s total deriv; it does not assert existence of a classical second derivative beyond that representation.

Encoder–denoiser: accepted · equivalent-after-elaboration

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

Scope and omitted-condition boundaries

This uses Mathlib’s total deriv; it does not assert existence of a classical second derivative beyond that representation.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

isLocalMax_of_deriv_deriv_neg
isLocalMin_of_deriv_deriv_pos
Filter.EventuallyEq.deriv

Mathematical sources

Samplinglib compiled source — Exact statement and proof.

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

Second derivative at a local maximum

AutoSamplingTheory.TechnicalLemmas.Geometry.SphereSecondOrder.IsLocalMax.deriv_deriv_nonpos_of_continuousAt · theorem · Teaching coverage

Read this first

Mathematical statement

For a real function continuous at a local maximum, the second derivative represented by deriv (deriv f) is nonpositive.

\[x\text{ local max of }f,\ f\text{ continuous at }x\Longrightarrow (\operatorname{deriv}\operatorname{deriv}f)(x)\le0\]

Lean statement · deriv_deriv_nonpos_of_continuousAt

The Lean theorem states the displayed necessary sign with every continuity, tangency, diagonal, and trace premise explicit.

Download module (.lean)

theorem IsLocalMax.deriv_deriv_nonpos_of_continuousAt
    {f : ℝ → ℝ} {x : ℝ} (hmax : IsLocalMax f x)
    (hc : ContinuousAt f x) :
    deriv (deriv f) x ≤ 0

Exact module and namespace context

Proof roadmap

1Rule out a positive second derivative
A positive second derivative and Fermat’s identity would make x a local minimum.
2Force local constancy
The local minimum and maximum inequalities agree, so f equals f(x) near x.
3Contradict strict positivity
Differentiating the local constant germ twice gives second derivative zero.

Full assumptions and notation

All objects and hypotheses

f is a real-valued function on the real line.
x is a local maximum of f.
f is continuous at x; Mathlib deriv is total and equals zero at nondifferentiable points.

Mathematical proof

1. Rule out a positive second derivative

A positive second derivative and Fermat’s identity would make x a local minimum.

\[f^{\prime\prime}(x)>0\Longrightarrow x\text{ is a local minimum}\]

Corresponding Lean step

Use isLocalMin_of_deriv_deriv_pos.

2. Force local constancy

The local minimum and maximum inequalities agree, so f equals f(x) near x.

\[f(y)=f(x)\text{ near }x\]

Corresponding Lean step

Intersect the two filters and apply order antisymmetry.

3. Contradict strict positivity

Differentiating the local constant germ twice gives second derivative zero.

\[f^{\prime\prime}(x)=0\]

Corresponding Lean step

Use the congruence theorem for deriv twice.

Lean verification

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

Lean proof · deriv_deriv_nonpos_of_continuousAt

The proof reduces a forbidden strict sign to simultaneous local minimum and maximum, or restricts the sphere extremum to feasible exponential curves and sums the scalar signs.

Download module (.lean)

theorem IsLocalMax.deriv_deriv_nonpos_of_continuousAt
    {f : ℝ → ℝ} {x : ℝ} (hmax : IsLocalMax f x)
    (hc : ContinuousAt f x) :
    deriv (deriv f) x ≤ 0 := by
  by_contra hnonpos
  have hpos : 0 < deriv (deriv f) x := lt_of_not_ge hnonpos
  have hmin : IsLocalMin f x :=
    isLocalMin_of_deriv_deriv_pos hpos hmax.deriv_eq_zero hc
  have hconst : f =ᶠ[𝓝 x] fun _ : ℝ => f x := by
    filter_upwards [hmin, hmax] with y hymin hymax
    exact le_antisymm hymax hymin
  have hderiv : deriv f =ᶠ[𝓝 x] fun _ : ℝ => 0 := by
    simpa using hconst.deriv
  have hzero : deriv (deriv f) x = 0 := by
    calc
      deriv (deriv f) x = deriv (fun _ : ℝ => 0) x := hderiv.deriv_eq
      _ = 0 := by simp
  linarith

variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]

open AutoSamplingTheory.TechnicalLemmas.Geometry.UnitSphere

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
The classical textbook statement assumes an ordinary second derivative at the extremum.	The scalar result is stated for Mathlib’s total expression deriv (deriv f), with continuity at the extremum. If either derivative is unavailable, Mathlib supplies zero.	generalization	The proof shows the non-strict sign for the totalized expression on a larger domain; the public lesson and boundary do not reinterpret it as existence of a classical second derivative.
Textbook sphere statements are usually finite-dimensional.	The geometric trace theorem works in any real inner-product space for an explicitly finite family of tangent directions.	generalization	The proof uses only tangent exponential curves and a finite sum.

This is a necessary non-strict sign condition, not a sufficient test for an extremum.

Encoder–denoiser: accepted · equivalent-after-elaboration

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

Scope and omitted-condition boundaries

This is a necessary non-strict sign condition, not a sufficient test for an extremum.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

isLocalMax_of_deriv_deriv_neg
isLocalMin_of_deriv_deriv_pos
Filter.EventuallyEq.deriv

Mathematical sources

Samplinglib compiled source — Exact statement and proof.

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

Nonnegative Laplacian at a unit-sphere minimum

AutoSamplingTheory.TechnicalLemmas.Geometry.SphereSecondOrder.unitSphere_isMinOn_laplacian_nonneg · theorem · Teaching coverage

Read this first

Mathematical statement

At a global minimum on the unit sphere, a finite trace of tangent exponential-curve second derivatives is nonnegative.

\[\Delta f(w)=\sum_i \frac{d^2}{dt^2}f(\operatorname{Exp}_w(tz_i))\big|_{t=0}\ge0\]

Lean statement · unitSphere_isMinOn_laplacian_nonneg

The Lean theorem states the displayed necessary sign with every continuity, tangency, diagonal, and trace premise explicit.

Download module (.lean)

theorem unitSphere_isMinOn_laplacian_nonneg
    {ι : Type*} [Fintype ι] {f : E → ℝ} {w : E}
    (directions : ι → E) (diagonal : ι → ℝ) (laplacian : ℝ)
    (hw : ‖w‖ = 1)
    (htangent : ∀ i, ⟪w, directions i⟫_ℝ = 0)
    (hmin : IsMinOn f (Metric.sphere (0 : E) 1) w)
    (hcontinuous : ∀ i, ContinuousAt
      (fun t : ℝ => f (unitSphereExp w (t • directions i))) 0)
    (hdiagonal : ∀ i, diagonal i =
      deriv (deriv (fun t : ℝ =>
        f (unitSphereExp w (t • directions i)))) 0)
    (htrace : laplacian = ∑ i, diagonal i) :
    0 ≤ laplacian

Exact module and namespace context

Proof roadmap

1Keep every curve on the sphere
Unit norm and tangency make Exp_w(t z_i) a sphere point for every real t.
2Restrict the minimum to each curve
The global sphere minimum becomes a local minimum of every scalar curve at t=0.
3Sum the directional signs
The real second-order necessary condition makes every diagonal entry nonnegative; a finite sum preserves the sign.

Full assumptions and notation

All objects and hypotheses

E is a real inner-product space and the index type is finite.
w has unit norm and every direction z_i is tangent at w.
f has a global minimum on the unit sphere at w.
Each exponential-curve restriction is continuous at zero; diagonal entries equal its Mathlib double derivative and the Laplacian equals their finite sum.

Mathematical proof

1. Keep every curve on the sphere

Unit norm and tangency make Exp_w(t z_i) a sphere point for every real t.

\[\|\operatorname{Exp}_w(tz_i)\|=1\]

Corresponding Lean step

Apply unitSphereExp_norm_eq_one after scaling the tangent direction.

2. Restrict the minimum to each curve

The global sphere minimum becomes a local minimum of every scalar curve at t=0.

\[f(w)\le f(\operatorname{Exp}_w(tz_i))\]

Corresponding Lean step

Build an IsLocalMin from the global IsMinOn inequality.

3. Sum the directional signs

The real second-order necessary condition makes every diagonal entry nonnegative; a finite sum preserves the sign.

\[0\le h_i\ \forall i\Longrightarrow0\le\sum_i h_i=\Delta f(w)\]

Corresponding Lean step

Rewrite each diagonal identity and use Finset.sum_nonneg.

Lean verification

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

Lean proof · unitSphere_isMinOn_laplacian_nonneg

The proof reduces a forbidden strict sign to simultaneous local minimum and maximum, or restricts the sphere extremum to feasible exponential curves and sums the scalar signs.

Download module (.lean)

theorem unitSphere_isMinOn_laplacian_nonneg
    {ι : Type*} [Fintype ι] {f : E → ℝ} {w : E}
    (directions : ι → E) (diagonal : ι → ℝ) (laplacian : ℝ)
    (hw : ‖w‖ = 1)
    (htangent : ∀ i, ⟪w, directions i⟫_ℝ = 0)
    (hmin : IsMinOn f (Metric.sphere (0 : E) 1) w)
    (hcontinuous : ∀ i, ContinuousAt
      (fun t : ℝ => f (unitSphereExp w (t • directions i))) 0)
    (hdiagonal : ∀ i, diagonal i =
      deriv (deriv (fun t : ℝ =>
        f (unitSphereExp w (t • directions i)))) 0)
    (htrace : laplacian = ∑ i, diagonal i) :
    0 ≤ laplacian := by
  rw [htrace]
  exact Finset.sum_nonneg fun i _ => by
    rw [hdiagonal i]
    exact unitSphere_isMinOn_expCurve_deriv_deriv_nonneg
      hw (htangent i) hmin (hcontinuous i)

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
The classical textbook statement assumes an ordinary second derivative at the extremum.	The scalar result is stated for Mathlib’s total expression deriv (deriv f), with continuity at the extremum. If either derivative is unavailable, Mathlib supplies zero.	generalization	The proof shows the non-strict sign for the totalized expression on a larger domain; the public lesson and boundary do not reinterpret it as existence of a classical second derivative.
Textbook sphere statements are usually finite-dimensional.	The geometric trace theorem works in any real inner-product space for an explicitly finite family of tangent directions.	generalization	The proof uses only tangent exponential curves and a finite sum.

The theorem requires the supplied diagonal/trace identities; it does not construct a tangent orthonormal frame or identify a differential operator with the Laplace–Beltrami operator.

Encoder–denoiser: accepted · equivalent-after-elaboration

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

Scope and omitted-condition boundaries

The theorem requires the supplied diagonal/trace identities; it does not construct a tangent orthonormal frame or identify a differential operator with the Laplace–Beltrami operator.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

AutoSamplingTheory.TechnicalLemmas.Geometry.UnitSphere.unitSphereExp_norm_eq_one

Mathlib API called (external library)

isLocalMax_of_deriv_deriv_neg
isLocalMin_of_deriv_deriv_pos
Filter.EventuallyEq.deriv

Mathematical sources

Samplinglib compiled source — Exact statement and proof.

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

Nonpositive Laplacian at a unit-sphere maximum

AutoSamplingTheory.TechnicalLemmas.Geometry.SphereSecondOrder.unitSphere_isMaxOn_laplacian_nonpos · theorem · Teaching coverage

Read this first

Mathematical statement

At a global maximum on the unit sphere, a finite trace of tangent exponential-curve second derivatives is nonpositive.

\[\Delta f(w)=\sum_i \frac{d^2}{dt^2}f(\operatorname{Exp}_w(tz_i))\big|_{t=0}\le0\]

Lean statement · unitSphere_isMaxOn_laplacian_nonpos

The Lean theorem states the displayed necessary sign with every continuity, tangency, diagonal, and trace premise explicit.

Download module (.lean)

theorem unitSphere_isMaxOn_laplacian_nonpos
    {ι : Type*} [Fintype ι] {f : E → ℝ} {w : E}
    (directions : ι → E) (diagonal : ι → ℝ) (laplacian : ℝ)
    (hw : ‖w‖ = 1)
    (htangent : ∀ i, ⟪w, directions i⟫_ℝ = 0)
    (hmax : IsMaxOn f (Metric.sphere (0 : E) 1) w)
    (hcontinuous : ∀ i, ContinuousAt
      (fun t : ℝ => f (unitSphereExp w (t • directions i))) 0)
    (hdiagonal : ∀ i, diagonal i =
      deriv (deriv (fun t : ℝ =>
        f (unitSphereExp w (t • directions i)))) 0)
    (htrace : laplacian = ∑ i, diagonal i) :
    laplacian ≤ 0

Exact module and namespace context

Proof roadmap

1Preserve feasibility along tangent curves
Every scaled tangent direction remains orthogonal to the unit base point, so the exponential curve stays on the sphere.
2Restrict the maximum to one dimension
The sphere maximum is a local maximum at zero along each exponential curve.
3Take the finite trace
Every directional double derivative is nonpositive, and their finite sum is the supplied Laplacian.

Full assumptions and notation

All objects and hypotheses

E is a real inner-product space and the index type is finite.
w has unit norm and every direction z_i is tangent at w.
f has a global maximum on the unit sphere at w.
Each exponential-curve restriction is continuous at zero; diagonal entries equal its Mathlib double derivative and the Laplacian equals their finite sum.

Mathematical proof

1. Preserve feasibility along tangent curves

Every scaled tangent direction remains orthogonal to the unit base point, so the exponential curve stays on the sphere.

\[\|\operatorname{Exp}_w(tz_i)\|=1\]

Corresponding Lean step

Use the public unit-sphere norm theorem.

2. Restrict the maximum to one dimension

The sphere maximum is a local maximum at zero along each exponential curve.

\[f(\operatorname{Exp}_w(tz_i))\le f(w)\]

Corresponding Lean step

Specialize IsMaxOn to the feasible curve.

3. Take the finite trace

Every directional double derivative is nonpositive, and their finite sum is the supplied Laplacian.

\[h_i\le0\ \forall i\Longrightarrow\sum_i h_i=\Delta f(w)\le0\]

Corresponding Lean step

Rewrite and use Finset.sum_nonpos.

Lean verification

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

Lean proof · unitSphere_isMaxOn_laplacian_nonpos

The proof reduces a forbidden strict sign to simultaneous local minimum and maximum, or restricts the sphere extremum to feasible exponential curves and sums the scalar signs.

Download module (.lean)

theorem unitSphere_isMaxOn_laplacian_nonpos
    {ι : Type*} [Fintype ι] {f : E → ℝ} {w : E}
    (directions : ι → E) (diagonal : ι → ℝ) (laplacian : ℝ)
    (hw : ‖w‖ = 1)
    (htangent : ∀ i, ⟪w, directions i⟫_ℝ = 0)
    (hmax : IsMaxOn f (Metric.sphere (0 : E) 1) w)
    (hcontinuous : ∀ i, ContinuousAt
      (fun t : ℝ => f (unitSphereExp w (t • directions i))) 0)
    (hdiagonal : ∀ i, diagonal i =
      deriv (deriv (fun t : ℝ =>
        f (unitSphereExp w (t • directions i)))) 0)
    (htrace : laplacian = ∑ i, diagonal i) :
    laplacian ≤ 0 := by
  rw [htrace]
  exact Finset.sum_nonpos fun i _ => by
    rw [hdiagonal i]
    exact unitSphere_isMaxOn_expCurve_deriv_deriv_nonpos
      hw (htangent i) hmax (hcontinuous i)

end

end AutoSamplingTheory.TechnicalLemmas.Geometry.SphereSecondOrder

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
The classical textbook statement assumes an ordinary second derivative at the extremum.	The scalar result is stated for Mathlib’s total expression deriv (deriv f), with continuity at the extremum. If either derivative is unavailable, Mathlib supplies zero.	generalization	The proof shows the non-strict sign for the totalized expression on a larger domain; the public lesson and boundary do not reinterpret it as existence of a classical second derivative.
Textbook sphere statements are usually finite-dimensional.	The geometric trace theorem works in any real inner-product space for an explicitly finite family of tangent directions.	generalization	The proof uses only tangent exponential curves and a finite sum.

No parabolic PDE, density evolution, or maximum-principle time argument is included.

Encoder–denoiser: accepted · equivalent-after-elaboration

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

Scope and omitted-condition boundaries

No parabolic PDE, density evolution, or maximum-principle time argument is included.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

AutoSamplingTheory.TechnicalLemmas.Geometry.UnitSphere.unitSphereExp_norm_eq_one

Mathlib API called (external library)

isLocalMax_of_deriv_deriv_neg
isLocalMin_of_deriv_deriv_pos
Filter.EventuallyEq.deriv

Mathematical sources

Samplinglib compiled source — Exact statement and proof.

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

Which proof obligations and prerequisites are covered?

Independently verified prerequisite Second derivative at a local minimum
Independently verified prerequisite Second derivative at a local maximum
Independently verified prerequisite Nonnegative Laplacian at a unit-sphere minimum
Independently verified prerequisite Nonpositive Laplacian at a unit-sphere maximum

Library supplement: Angular geometry on the actual unit sphere

Original generic mathematics supplement, not a theorem attributed to the primary textbook or a statistical paper.

Samplinglib original sphere geometry and feature-law supplement v1, 2026-10-23 · Complete authored units[0] and its formula proof, pinned source commit 3212f7eb462e2d2237d0a57c6f1f425a82169cff (historical source) · licensed original

Complete source statement and conditions

Let E be a finite-dimensional real inner-product space with its Borel measurable structure, and let S be its literal unit-norm subtype. The actual angular cost c(u,v)=arccos(inner(u,v)) is jointly continuous and measurable on S×S. For every pair it lies between zero and pi, equals Mathlib's unoriented vector angle, dominates the ambient chord norm, vanishes exactly on the diagonal, and is symmetric. It satisfies the triangle inequality. These are explicit properties of the angular cost; no inherited chord-distance instance is replaced, no path-length geodesic-distance identification or Wasserstein theorem is included, and no sphere nonemptiness or positive dimension is assumed.

E is a finite-dimensional real inner-product normed space with its Borel measurable structure.
S is exactly the unit-norm subtype and c(u,v)=arccos(inner(u,v)). Neither positive dimension nor a point of S is assumed.

Angular geometry on the actual unit sphere

\[c(u,v)=\arccos\langle u,v\rangle,\quad 0\le c\le\pi,\quad \|u-v\|\le c(u,v),\quad c(u,w)\le c(u,v)+c(v,w).\]

Read the formalized proofs

Each statement and proof below has its own closed Lean disclosure. Samplinglib parents, Mathlib calls and external mathematical sources are distinguished in each proof.

Samplinglib mathematical lesson

Angular geometry on the actual unit sphere

Read this first

Mathematical statement

\[c(u,v)=\arccos\langle u,v\rangle,\quad 0\le c\le\pi,\quad \|u-v\|\le c(u,v),\quad c(u,w)\le c(u,v)+c(v,w).\]

Lean statement · unit_sphere_angular_cost_properties

Download module (.lean)

theorem unit_sphere_angular_cost_properties
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] :
    let S := {w : E // ‖w‖ = 1}
    let c : S × S → ℝ := fun z => Real.arccos ⟪z.1.1,z.2.1⟫_ℝ
    Continuous c ∧ Measurable c ∧
      (∀ u v : S, 0 ≤ c (u,v) ∧ c (u,v) ≤ Real.pi ∧
        c (u,v) = InnerProductGeometry.angle u.1 v.1 ∧
        ‖u.1-v.1‖ ≤ c (u,v) ∧
        (c (u,v) = 0 ↔ u = v) ∧ c (u,v) = c (v,u)) ∧
      ∀ u v w : S, c (u,w) ≤ c (u,v)+c (v,w)

Exact module and namespace context

Read the complete mathematical statement and visible assumptions, then expand the numbered formula proof. Exact Lean remains optional and initially folded.

Full assumptions and notation

All objects and hypotheses

E is a finite-dimensional real inner-product normed space with its Borel measurable structure.
S is exactly the unit-norm subtype and c(u,v)=arccos(inner(u,v)). Neither positive dimension nor a point of S is assumed.

Mathematical proof

Open a step to read its argument and formula.

1. Identify the angle

Unit norms cancel the denominator in the vector-angle definition, so the literal arccos cost is the existing unoriented angle. Continuity follows from continuous subtype coercions, the inner product and arccos; finite dimension supplies second countability for the measurable product.

\[c(u,v)=\operatorname{angle}(u,v),\qquad c\in C(S\times S;\mathbb R).\]

Corresponding Lean step

  have heq (u v : {w : E // ‖w‖ = 1}) :
      Real.arccos ⟪u.1,v.1⟫_ℝ = InnerProductGeometry.angle u.1 v.1 := by
    simp [InnerProductGeometry.angle,u.property,v.property]
  have hc : Continuous (fun z : {w : E // ‖w‖ = 1} × {w : E // ‖w‖ = 1} =>
      Real.arccos ⟪z.1.1,z.2.1⟫_ℝ) := by fun_prop

Literal module excerpt. Local names retain the surrounding theorem context, available with the complete folded theorem; these are proof ingredients, not extra public premises.

2. Compare a chord with its angle

Set θ=c(u,v)=angle(u,v). For unit endpoints, expand the squared chord norm. The half-angle identity and sin squared bounded by its argument squared yield the chord estimate; both norms and the angle are nonnegative.

\[\|u-v\|^2=2-2\cos\theta=4\sin^2(\theta/2)\le\theta^2.\]

Corresponding Lean step

private theorem chord_le_angle
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    (u v : E) (hu : ‖u‖ = 1) (hv : ‖v‖ = 1) :
    ‖u-v‖ ≤ InnerProductGeometry.angle u v := by
  let θ := InnerProductGeometry.angle u v
  have hθ : 0 ≤ θ := InnerProductGeometry.angle_nonneg u v
  have hc : Real.cos θ = ⟪u,v⟫_ℝ := by
    simpa [θ,hu,hv] using InnerProductGeometry.cos_angle u v
  have heq : ‖u-v‖^2 = 2-2*Real.cos θ := by
    rw [norm_sub_sq_real,hu,hv,hc]
    ring
  have hh := Real.sin_sq_eq_half_sub (θ/2)
  have htwo : 2*(θ/2) = θ := by ring
  rw [htwo] at hh
  have hs := Real.sin_sq_le_sq (x := θ/2)
  change ‖u-v‖ ≤ θ
  nlinarith [norm_nonneg (u-v)]

Literal module excerpt. Local names retain the surrounding theorem context, available with the complete folded theorem; these are proof ingredients, not extra public premises.

3. Separate points and record the range

The principal arccos lies in [0,pi]. A zero cost forces zero chord, hence equal subtype points. Conversely every unit vector is nonzero and has zero angle with itself. Inner-product symmetry supplies cost symmetry.

\[0\le c(u,v)\le\pi,\quad c(u,v)=0\iff u=v,\quad c(u,v)=c(v,u).\]

Corresponding Lean step

    refine ⟨Real.arccos_nonneg _,Real.arccos_le_pi _,heq u v,hchord,?_,?_⟩
    · constructor
      · intro hz
        apply Subtype.ext
        apply sub_eq_zero.mp
        apply norm_eq_zero.mp
        exact le_antisymm (by simpa only [hz] using hchord) (norm_nonneg _)
      · rintro rfl
        rw [heq]
        apply InnerProductGeometry.angle_self
        intro hz
        have hh := u.property
        rw [hz,norm_zero] at hh
        norm_num at hh
    · rw [heq,heq,InnerProductGeometry.angle_comm]

Literal module excerpt. Local names retain the surrounding theorem context, available with the complete folded theorem; these are proof ingredients, not extra public premises.

4. Use the vector-angle triangle inequality

Replace each literal cost by its angle expression and apply the existing vector-angle triangle inequality. This is an angular-cost fact; it does not identify an intrinsic path-length metric, particularly on the disconnected two-point sphere.

\[c(u,w)=\operatorname{angle}(u,w)\le\operatorname{angle}(u,v)+\operatorname{angle}(v,w).\]

Corresponding Lean step

  · intro u v w
    rw [heq,heq,heq]
    exact InnerProductGeometry.angle_le_angle_add_angle u.1 v.1 w.1

Literal module excerpt. Local names retain the surrounding theorem context, available with the complete folded theorem; these are proof ingredients, not extra public premises.

Lean verification

Lean proof · unit_sphere_angular_cost_properties

The formula steps explain the proof; optional folds contain literal Lean excerpts and the full checked theorem.

Download module (.lean)

theorem unit_sphere_angular_cost_properties
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] :
    let S := {w : E // ‖w‖ = 1}
    let c : S × S → ℝ := fun z => Real.arccos ⟪z.1.1,z.2.1⟫_ℝ
    Continuous c ∧ Measurable c ∧
      (∀ u v : S, 0 ≤ c (u,v) ∧ c (u,v) ≤ Real.pi ∧
        c (u,v) = InnerProductGeometry.angle u.1 v.1 ∧
        ‖u.1-v.1‖ ≤ c (u,v) ∧
        (c (u,v) = 0 ↔ u = v) ∧ c (u,v) = c (v,u)) ∧
      ∀ u v w : S, c (u,w) ≤ c (u,v)+c (v,w) := by
  dsimp only
  letI : SecondCountableTopology E := inferInstance
  have heq (u v : {w : E // ‖w‖ = 1}) :
      Real.arccos ⟪u.1,v.1⟫_ℝ = InnerProductGeometry.angle u.1 v.1 := by
    simp [InnerProductGeometry.angle,u.property,v.property]
  have hc : Continuous (fun z : {w : E // ‖w‖ = 1} × {w : E // ‖w‖ = 1} =>
      Real.arccos ⟪z.1.1,z.2.1⟫_ℝ) := by fun_prop
  refine ⟨hc,hc.measurable,?_,?_⟩
  · intro u v
    have hchord : ‖u.1-v.1‖ ≤ Real.arccos ⟪u.1,v.1⟫_ℝ := by
      rw [heq]
      exact chord_le_angle u.1 v.1 u.property v.property
    refine ⟨Real.arccos_nonneg _,Real.arccos_le_pi _,heq u v,hchord,?_,?_⟩
    · constructor
      · intro hz
        apply Subtype.ext
        apply sub_eq_zero.mp
        apply norm_eq_zero.mp
        exact le_antisymm (by simpa only [hz] using hchord) (norm_nonneg _)
      · rintro rfl
        rw [heq]
        apply InnerProductGeometry.angle_self
        intro hz
        have hh := u.property
        rw [hz,norm_zero] at hh
        norm_num at hh
    · rw [heq,heq,InnerProductGeometry.angle_comm]
  · intro u v w
    rw [heq,heq,heq]
    exact InnerProductGeometry.angle_le_angle_add_angle u.1 v.1 w.1

end AutoSamplingTheory.TechnicalLemmas.Geometry.UnitSphereAngularCost

Exact module and namespace context

Source correspondence and review

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
Let E be a finite-dimensional real inner-product space with its Borel measurable structure, and let S be its literal unit-norm subtype. The actual angular cost c(u,v)=arccos(inner(u,v)) is jointly continuous and measurable on S×S. For every pair it lies between zero and pi, equals Mathlib's unoriented vector angle, dominates the ambient chord norm, vanishes exactly on the diagonal, and is symmetric. It satisfies the triangle inequality. These are explicit properties of the angular cost; no inherited chord-distance instance is replaced, no path-length geodesic-distance identification or Wasserstein theorem is included, and no sphere nonemptiness or positive dimension is assumed.	The signature preserves the finite-dimensional real/Borel carrier, actual unit-norm subtype and arccos inner-product cost. Continuity, measurability, range, angle/chord relations, separation, symmetry and triangle are conclusions; no probability law or transport object is part of this theorem.	same	Ambient derivatives/operator bounds are explicit generic inputs only to the feature-law result; all feature-integrability/residual/cost estimates are derived. Angular geometry supplies properties of the actual cost. No intrinsic-path/manifold/Wasserstein API identification or chosen statistical instance is claimed.

Explicit cost properties only. The inherited subtype distance is still the ambient chord distance; no metric instance is changed.; No intrinsic path-length identity, installed manifold API, Wasserstein theorem or statistical model is certified. In dimension one the two-point sphere has finite angular cost but no internal path between its two points.

Encoder–denoiser: accepted · equivalent-after-elaboration

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

Scope and omitted-condition boundaries

Explicit cost properties only. The inherited subtype distance is still the ambient chord distance; no metric instance is changed.
No intrinsic path-length identity, installed manifold API, Wasserstein theorem or statistical model is certified. In dimension one the two-point sphere has finite angular cost but no internal path between its two points.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

InnerProductGeometry.angle_le_angle_add_angle
InnerProductGeometry.cos_angle
Real.sin_sq_eq_half_sub
Real.sin_sq_le_sq

Mathematical sources

Samplinglib original sphere geometry and feature-law supplement v1 (2026-10-23) (historical source) — Original generic canonical-library mathematics placed by subject; no primary-textbook theorem, concrete statistical model or whole chapter 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.

Which proof obligations and prerequisites are covered?

Formalized proof edge; source adapter/review separate Angular geometry on the actual unit sphere

Library supplement: Uniform gradients of quadratic feature-law potentials

Original generic mathematics supplement, not a theorem attributed to the primary textbook or a statistical paper.

Samplinglib original sphere geometry and feature-law supplement v1, 2026-10-23 · Complete authored units[1] and its formula proof, pinned source commit 3212f7eb462e2d2237d0a57c6f1f425a82169cff (historical source) · licensed original

Complete source statement and conditions

Let E be a finite-dimensional real inner-product normed space with its Borel measurable structure and H a complete real inner-product normed space. Let F:E→H have actual ambient Frechet derivative D(w):E→H for every w. Assume nonnegative M1,M2, an operator bound norm(D(w))<=M1 on the closed unit ball and an operator-Lipschitz bound norm(D(w)-D(u))<=M2 norm(w-u) there. Fix y in H. On the actual unit-norm subtype S define K(w)=F(w), angular cost c(u,v)=arccos(inner(u,v)), the actual Bochner mean m(mu)=integral K dmu, V_mu(w)=2 inner(m(mu)-y,F(w)), and G_mu(w)=2P_w D(w)^*(m(mu)-y) with the explicit projection P_w z=z−⟨z,w⟩w, which projects onto w-perpendicular when norm(w)=1. Let Q(mu,nu) be the literal extended nonnegative infimum of the quadratic angular cost over all actual couplings. There exist C1,C2>0, independent of probability laws and unit weights, such that for every actual parameter probability K is integrable, V_mu has the displayed ambient gradient 2D(w)^*(m(mu)-y) at every ambient w, and its projected G_mu is tangent and uniformly bounded by C1 at every unit weight. For every two actual parameter probabilities Q is finite and norm(G_mu(w)-G_nu(u))<=C2*(sqrt(Q).toReal+c(w,u)). Feature boundedness, strong measurability, feature Lipschitz control and residual budgets are derived inside the proof rather than assumed; the returned conclusions are feature integrability, actual ambient gradient, tangency/uniform bound, finite transport cost and the joint sensitivity estimate. The constants may depend on the displayed feature/derivative data, E,H and y. This is a generic feature-law theorem, not a concrete Gaussian scalar-data potential, installed manifold-gradient/Wasserstein API or intrinsic path-length theorem.

E is finite-dimensional real Hilbert with Borel structure; H is a complete real inner-product normed space, with no separability assumption.
F:E→H has actual full ambient Frechet derivative D(w) at every w. M1,M2≥0 bound the derivative operator norm and its operator Lipschitz increment on the closed unit ball.
y is fixed. S is the literal unit-norm subtype; m is the actual Bochner integral, c the literal arccos cost, and Q the infimum of angular squared cost over all actual couplings.

Uniform gradients of quadratic feature-law potentials

\[P_wz=z-\langle z,w\rangle w,\quad V_\mu(w)=2\langle m_\mu-y,F(w)\rangle,\quad G_\mu(w)=2P_wD(w)^*(m_\mu-y),\quad \|G_\mu(w)-G_\nu(u)\|\le C_2\bigl(Q(\mu,\nu)^{1/2}+c(w,u)\bigr).\]

Read the formalized proofs

Each statement and proof below has its own closed Lean disclosure. Samplinglib parents, Mathlib calls and external mathematical sources are distinguished in each proof.

Samplinglib mathematical lesson

Uniform gradients of quadratic feature-law potentials

Read this first

Mathematical statement

\[P_wz=z-\langle z,w\rangle w,\quad V_\mu(w)=2\langle m_\mu-y,F(w)\rangle,\quad G_\mu(w)=2P_wD(w)^*(m_\mu-y),\quad \|G_\mu(w)-G_\nu(u)\|\le C_2\bigl(Q(\mu,\nu)^{1/2}+c(w,u)\bigr).\]

Lean statement · quadratic_feature_law_gradient_angular_transport_control

Download module (.lean)

theorem quadratic_feature_law_gradient_angular_transport_control
    {E H : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
    (F : E → H) (D : E → E →L[ℝ] H)
    (hF : ∀ w, HasFDerivAt F (D w) w)
    (M₁ M₂ : ℝ) (hM₁ : 0 ≤ M₁) (hM₂ : 0 ≤ M₂)
    (hBound : ∀ w : E, ‖w‖ ≤ 1 → ‖D w‖ ≤ M₁)
    (hLip : ∀ w u : E, ‖w‖ ≤ 1 → ‖u‖ ≤ 1 → ‖D w-D u‖ ≤ M₂*‖w-u‖)
    (y : H) :
    let S := {w : E // ‖w‖ = 1}
    let K : S → H := fun w => F w.1
    let c : S × S → ℝ := fun z => Real.arccos ⟪z.1.1,z.2.1⟫_ℝ
    let m : Measure S → H := fun μ => ∫ w, K w ∂μ
    let V : Measure S → E → ℝ := fun μ w => 2 * ⟪m μ-y,F w⟫_ℝ
    let G : Measure S → E → E := fun μ w =>
      (2 : ℝ) • ((D w).adjoint (m μ-y) - ⟪(D w).adjoint (m μ-y),w⟫_ℝ • w)
    let Q : Measure S → Measure S → ℝ≥0∞ := fun μ ν =>
      AutoSamplingTheory.TechnicalLemmas.Measure.Transport.transportCost
        (fun z => ENNReal.ofReal ((c z)^2)) μ ν
    ∃ C₁ C₂ : ℝ, 0 < C₁ ∧ 0 < C₂ ∧
      (∀ μ : Measure S, IsProbabilityMeasure μ →
        Integrable K μ ∧
        (∀ w : E, HasGradientAt (V μ) ((2 : ℝ) • (D w).adjoint (m μ-y)) w) ∧
        ∀ w : S, ⟪w.1,G μ w.1⟫_ℝ = 0 ∧ ‖G μ w.1‖ ≤ C₁) ∧
      ∀ μ ν : Measure S, IsProbabilityMeasure μ → IsProbabilityMeasure ν →
        Q μ ν ≠ ∞ ∧ ∀ w u : S,
          ‖G μ w.1-G ν u.1‖ ≤
            C₂ * ((Q μ ν ^ (1 / 2 : ℝ)).toReal + c (w,u))

Exact module and namespace context

Read the complete mathematical statement and visible assumptions, then expand the numbered formula proof. Exact Lean remains optional and initially folded.

Full assumptions and notation

All objects and hypotheses

E is finite-dimensional real Hilbert with Borel structure; H is a complete real inner-product normed space, with no separability assumption.
F:E→H has actual full ambient Frechet derivative D(w) at every w. M1,M2≥0 bound the derivative operator norm and its operator Lipschitz increment on the closed unit ball.
y is fixed. S is the literal unit-norm subtype; m is the actual Bochner integral, c the literal arccos cost, and Q the infimum of angular squared cost over all actual couplings.

Mathematical proof

Open a step to read its argument and formula.

1. Produce feature continuity and chord control

Differentiability gives continuity. The convex mean-value bound on the closed unit ball produces the M1 chord Lipschitz estimate. Continuity on a second-countable domain yields strong measurability of the feature restriction even when H is not separable.

\[\|F(w)-F(u)\|\le M_1\|w-u\|\quad(\|w\|,\|u\|\le1).\]

Corresponding Lean step

  have hFc : Continuous F := continuous_iff_continuousAt.mpr fun w => (hF w).continuousAt
  have hKsm : StronglyMeasurable K := (hFc.comp continuous_subtype_val).stronglyMeasurable
  have hChord (w u : E) (hw : ‖w‖ ≤ 1) (hu : ‖u‖ ≤ 1) :
      ‖F w-F u‖ ≤ M₁*‖w-u‖ := by
    apply (convex_closedBall (0 : E) 1).norm_image_sub_le_of_norm_hasFDerivWithin_le
      (fun z _ => (hF z).hasFDerivWithinAt) ?_
      (by simpa [Metric.mem_closedBall,dist_zero_right] using hu)
      (by simpa [Metric.mem_closedBall,dist_zero_right] using hw)
    intro z hz
    exact hBound z (by simpa [Metric.mem_closedBall,dist_zero_right] using hz)

Literal module excerpt. Local names retain the surrounding theorem context, available with the complete folded theorem; these are proof ingredients, not extra public premises.

2. Produce one uniform feature bound

Compare every unit feature with F(0), using the previous estimate and the norm triangle inequality. The extra one makes B a convenient positive budget. This budget is an internal consequence, not a new premise.

\[B=\|F(0)\|+M_1+1,\qquad\|F(w)\|\le B\quad(w\in S).\]

Corresponding Lean step

  let B := ‖F (0:E)‖+M₁+1
  have hB : 0 ≤ B := by dsimp [B]; positivity
  have hKb (w : S) : ‖K w‖ ≤ B := by
    have hb := hChord w.1 0 w.property.le (by simp)
    have hn := norm_add_le (F w.1-F 0) (F 0)
    rw [sub_add_cancel] at hn
    simp only [sub_zero,w.property,mul_one] at hb
    change ‖F w.1‖ ≤ B
    dsimp [B]
    linarith

Literal module excerpt. Local names retain the surrounding theorem context, available with the complete folded theorem; these are proof ingredients, not extra public premises.

3. Pass from chords to angular cost

The canonical angular-geometry result supplies measurability, nonnegativity, the pi upper bound and chord domination. Consequently K is M1 Lipschitz with respect to the actual angular cost.

\[\|K(w)-K(u)\|\le M_1c(w,u),\qquad 0\le c(w,u)\le\pi.\]

Corresponding Lean step

  have hAng := AutoSamplingTheory.TechnicalLemmas.Geometry.UnitSphereAngularCost.unit_sphere_angular_cost_properties (E := E)
  change Continuous c ∧ Measurable c ∧
    (∀ u v : S, 0 ≤ c (u,v) ∧ c (u,v) ≤ Real.pi ∧
      c (u,v) = InnerProductGeometry.angle u.1 v.1 ∧ ‖u.1-v.1‖ ≤ c (u,v) ∧
      (c (u,v) = 0 ↔ u = v) ∧ c (u,v) = c (v,u)) ∧
    ∀ u v w : S, c (u,w) ≤ c (u,v)+c (v,w) at hAng
  have hc0 (z : S × S) : 0 ≤ c z := (hAng.2.2.1 z.1 z.2).1
  have hcB (z : S × S) : c z ≤ Real.pi := (hAng.2.2.1 z.1 z.2).2.1
  have hKlip (w u : S) : ‖K w-K u‖ ≤ M₁*c (w,u) :=
    (hChord w.1 u.1 w.property.le u.property.le).trans
      (mul_le_mul_of_nonneg_left (hAng.2.2.1 w u).2.2.2.1 hM₁)

Literal module excerpt. Local names retain the surrounding theorem context, available with the complete folded theorem; these are proof ingredients, not extra public premises.

4. Control actual means over all couplings

Apply bounded Bochner transport to actual probability laws, not chosen optimal couplings. It produces integrability, finite Q, the mean difference estimate and the residual budget R0=B+norm(y).

\[\|m_\mu-m_\nu\|\le M_1\sqrt{Q(\mu,\nu)},\qquad\|m_\mu-y\|\le R_0.\]

Corresponding Lean step

  have hMean (μ ν : Measure S) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] :=
    AutoSamplingTheory.TechnicalLemmas.Measure.BochnerMeanTransport.bounded_bochner_mean_quadratic_transport_control
      K hKsm B Real.pi M₁ hB Real.pi_pos.le hM₁ hKb c hAng.2.1 hc0 hcB hKlip μ ν
  have hTangent :=
    AutoSamplingTheory.TechnicalLemmas.Geometry.QuadraticFeatureTangentGradient.quadratic_feature_potential_tangent_gradient
      F D hF M₁ M₂ hM₁ hM₂ hBound hLip
  let R₀ := B+‖y‖
  have hR₀ : 0 ≤ R₀ := add_nonneg hB (norm_nonneg y)
  have hResidual (μ : Measure S) [IsProbabilityMeasure μ] : ‖m μ-y‖ ≤ R₀ :=
    ((hMean μ μ).2.2.2.2 y).1

Literal module excerpt. Local names retain the surrounding theorem context, available with the complete folded theorem; these are proof ingredients, not extra public premises.

5. Identify the full ambient gradient

For fixed residual r=m_mu-y the canonical scalar-potential derivative is 2 inner(D(w)*r,·). The real Riesz identification turns it into HasGradientAt, at every ambient weight rather than only unit points.

\[\nabla V_\mu(w)=2D(w)^*(m_\mu-y).\]

Corresponding Lean step

  have hGrad (μ : Measure S) (w : E) :
      HasGradientAt (V μ) ((2 : ℝ) • (D w).adjoint (m μ-y)) w := by
    rw [hasGradientAt_iff_hasFDerivAt]
    have he : InnerProductSpace.toDual ℝ E ((2 : ℝ) • (D w).adjoint (m μ-y)) =
        (2 : ℝ) • innerSL ℝ ((D w).adjoint (m μ-y)) := by
      ext v
      simp [InnerProductSpace.toDual_apply_apply,innerSL_apply_apply]
    rw [he]
    exact hTangent.1 (m μ-y) w

Literal module excerpt. Local names retain the surrounding theorem context, available with the complete folded theorem; these are proof ingredients, not extra public premises.

6. Choose constants before the laws

Projection contraction gives the pointwise bound, while R0 is independent of the parameter law. Choose strictly positive C1,C2 before quantifying over all laws and weights. The constants are not claimed dimension free.

\[C_1=2M_1R_0+1,\quad C_2=2M_1^2+2(M_2+2M_1)R_0+1.\]

Corresponding Lean step

  let A := 2*M₁^2
  let B₂ := 2*(M₂+2*M₁)*R₀
  have hA : 0 ≤ A := by dsimp [A]; positivity
  have hB₂ : 0 ≤ B₂ := by dsimp [B₂]; positivity
  refine ⟨2*M₁*R₀+1,A+B₂+1,by positivity,by positivity,?_,?_⟩
  · intro μ hμ
    let : IsProbabilityMeasure μ := hμ
    refine ⟨(hMean μ μ).1,hGrad μ,?_⟩
    intro w
    have ht := hTangent.2.1 (m μ-y) w.1 w.property
    refine ⟨ht.1,?_⟩
    exact ht.2.2.trans ((mul_le_mul_of_nonneg_left (hResidual μ) (by positivity)).trans (by linarith))

Literal module excerpt. Local names retain the surrounding theorem context, available with the complete folded theorem; these are proof ingredients, not extra public premises.

7. Combine law and point movement

Use the tangent-field joint estimate, substitute the actual mean sensitivity and residual budget, and dominate the chord by the angle. All costs are finite before applying toReal; the sum of the two coefficients plus one yields a single constant.

\[\|G_\mu(w)-G_\nu(u)\|\le2M_1^2\sqrt Q+2(M_2+2M_1)R_0c(w,u)\le C_2(\sqrt Q+c(w,u)).\]

Corresponding Lean step

  · intro μ ν hμ hν
    let : IsProbabilityMeasure μ := hμ
    let : IsProbabilityMeasure ν := hν
    refine ⟨(hMean μ ν).2.2.1,?_⟩
    intro w u
    have hm : ‖(m μ-y)-(m ν-y)‖ ≤ M₁*(Q μ ν ^ (1 / 2 : ℝ)).toReal := by
      simpa only [sub_sub_sub_cancel_right] using (hMean μ ν).2.2.2.1
    have hr := hResidual ν
    have ht := hTangent.2.2 (m μ-y) (m ν-y) w.1 u.1 w.property u.property
    have hpoint := (hAng.2.2.1 w u).2.2.2.1
    have ht' : ‖G μ w.1-G ν u.1‖ ≤
        A*(Q μ ν ^ (1 / 2 : ℝ)).toReal+B₂*c (w,u) := by
      calc
        _ ≤ 2*M₁*‖(m μ-y)-(m ν-y)‖+
            2*(M₂+2*M₁)*‖m ν-y‖*‖w.1-u.1‖ := ht
        _ ≤ 2*M₁*(M₁*(Q μ ν ^ (1 / 2 : ℝ)).toReal)+
            2*(M₂+2*M₁)*R₀*c (w,u) := by
          gcongr
        _ = _ := by dsimp [A,B₂]; ring
    apply ht'.trans
    have hs : 0 ≤ (Q μ ν ^ (1 / 2 : ℝ)).toReal := ENNReal.toReal_nonneg
    have hc := hc0 (w,u)
    nlinarith [mul_nonneg hA hc,mul_nonneg hB₂ hs]

Literal module excerpt. Local names retain the surrounding theorem context, available with the complete folded theorem; these are proof ingredients, not extra public premises.

Lean verification

Lean proof · quadratic_feature_law_gradient_angular_transport_control

The formula steps explain the proof; optional folds contain literal Lean excerpts and the full checked theorem.

Download module (.lean)

theorem quadratic_feature_law_gradient_angular_transport_control
    {E H : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
    (F : E → H) (D : E → E →L[ℝ] H)
    (hF : ∀ w, HasFDerivAt F (D w) w)
    (M₁ M₂ : ℝ) (hM₁ : 0 ≤ M₁) (hM₂ : 0 ≤ M₂)
    (hBound : ∀ w : E, ‖w‖ ≤ 1 → ‖D w‖ ≤ M₁)
    (hLip : ∀ w u : E, ‖w‖ ≤ 1 → ‖u‖ ≤ 1 → ‖D w-D u‖ ≤ M₂*‖w-u‖)
    (y : H) :
    let S := {w : E // ‖w‖ = 1}
    let K : S → H := fun w => F w.1
    let c : S × S → ℝ := fun z => Real.arccos ⟪z.1.1,z.2.1⟫_ℝ
    let m : Measure S → H := fun μ => ∫ w, K w ∂μ
    let V : Measure S → E → ℝ := fun μ w => 2 * ⟪m μ-y,F w⟫_ℝ
    let G : Measure S → E → E := fun μ w =>
      (2 : ℝ) • ((D w).adjoint (m μ-y) - ⟪(D w).adjoint (m μ-y),w⟫_ℝ • w)
    let Q : Measure S → Measure S → ℝ≥0∞ := fun μ ν =>
      AutoSamplingTheory.TechnicalLemmas.Measure.Transport.transportCost
        (fun z => ENNReal.ofReal ((c z)^2)) μ ν
    ∃ C₁ C₂ : ℝ, 0 < C₁ ∧ 0 < C₂ ∧
      (∀ μ : Measure S, IsProbabilityMeasure μ →
        Integrable K μ ∧
        (∀ w : E, HasGradientAt (V μ) ((2 : ℝ) • (D w).adjoint (m μ-y)) w) ∧
        ∀ w : S, ⟪w.1,G μ w.1⟫_ℝ = 0 ∧ ‖G μ w.1‖ ≤ C₁) ∧
      ∀ μ ν : Measure S, IsProbabilityMeasure μ → IsProbabilityMeasure ν →
        Q μ ν ≠ ∞ ∧ ∀ w u : S,
          ‖G μ w.1-G ν u.1‖ ≤
            C₂ * ((Q μ ν ^ (1 / 2 : ℝ)).toReal + c (w,u)) := by
  let : SecondCountableTopology E := inferInstance
  let S := {w : E // ‖w‖ = 1}
  let K : S → H := fun w => F w.1
  let c : S × S → ℝ := fun z => Real.arccos ⟪z.1.1,z.2.1⟫_ℝ
  let m : Measure S → H := fun μ => ∫ w, K w ∂μ
  let V : Measure S → E → ℝ := fun μ w => 2 * ⟪m μ-y,F w⟫_ℝ
  let G : Measure S → E → E := fun μ w =>
    (2 : ℝ) • ((D w).adjoint (m μ-y) - ⟪(D w).adjoint (m μ-y),w⟫_ℝ • w)
  let Q : Measure S → Measure S → ℝ≥0∞ := fun μ ν =>
    AutoSamplingTheory.TechnicalLemmas.Measure.Transport.transportCost
      (fun z => ENNReal.ofReal ((c z)^2)) μ ν
  change ∃ C₁ C₂ : ℝ, 0 < C₁ ∧ 0 < C₂ ∧
    (∀ μ : Measure S, IsProbabilityMeasure μ →
      Integrable K μ ∧
      (∀ w : E, HasGradientAt (V μ) ((2 : ℝ) • (D w).adjoint (m μ-y)) w) ∧
      ∀ w : S, ⟪w.1,G μ w.1⟫_ℝ = 0 ∧ ‖G μ w.1‖ ≤ C₁) ∧
    ∀ μ ν : Measure S, IsProbabilityMeasure μ → IsProbabilityMeasure ν →
      Q μ ν ≠ ∞ ∧ ∀ w u : S,
        ‖G μ w.1-G ν u.1‖ ≤ C₂ * ((Q μ ν ^ (1 / 2 : ℝ)).toReal + c (w,u))
  have hFc : Continuous F := continuous_iff_continuousAt.mpr fun w => (hF w).continuousAt
  have hKsm : StronglyMeasurable K := (hFc.comp continuous_subtype_val).stronglyMeasurable
  have hChord (w u : E) (hw : ‖w‖ ≤ 1) (hu : ‖u‖ ≤ 1) :
      ‖F w-F u‖ ≤ M₁*‖w-u‖ := by
    apply (convex_closedBall (0 : E) 1).norm_image_sub_le_of_norm_hasFDerivWithin_le
      (fun z _ => (hF z).hasFDerivWithinAt) ?_
      (by simpa [Metric.mem_closedBall,dist_zero_right] using hu)
      (by simpa [Metric.mem_closedBall,dist_zero_right] using hw)
    intro z hz
    exact hBound z (by simpa [Metric.mem_closedBall,dist_zero_right] using hz)
  let B := ‖F (0:E)‖+M₁+1
  have hB : 0 ≤ B := by dsimp [B]; positivity
  have hKb (w : S) : ‖K w‖ ≤ B := by
    have hb := hChord w.1 0 w.property.le (by simp)
    have hn := norm_add_le (F w.1-F 0) (F 0)
    rw [sub_add_cancel] at hn
    simp only [sub_zero,w.property,mul_one] at hb
    change ‖F w.1‖ ≤ B
    dsimp [B]
    linarith
  have hAng := AutoSamplingTheory.TechnicalLemmas.Geometry.UnitSphereAngularCost.unit_sphere_angular_cost_properties (E := E)
  change Continuous c ∧ Measurable c ∧
    (∀ u v : S, 0 ≤ c (u,v) ∧ c (u,v) ≤ Real.pi ∧
      c (u,v) = InnerProductGeometry.angle u.1 v.1 ∧ ‖u.1-v.1‖ ≤ c (u,v) ∧
      (c (u,v) = 0 ↔ u = v) ∧ c (u,v) = c (v,u)) ∧
    ∀ u v w : S, c (u,w) ≤ c (u,v)+c (v,w) at hAng
  have hc0 (z : S × S) : 0 ≤ c z := (hAng.2.2.1 z.1 z.2).1
  have hcB (z : S × S) : c z ≤ Real.pi := (hAng.2.2.1 z.1 z.2).2.1
  have hKlip (w u : S) : ‖K w-K u‖ ≤ M₁*c (w,u) :=
    (hChord w.1 u.1 w.property.le u.property.le).trans
      (mul_le_mul_of_nonneg_left (hAng.2.2.1 w u).2.2.2.1 hM₁)
  have hMean (μ ν : Measure S) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] :=
    AutoSamplingTheory.TechnicalLemmas.Measure.BochnerMeanTransport.bounded_bochner_mean_quadratic_transport_control
      K hKsm B Real.pi M₁ hB Real.pi_pos.le hM₁ hKb c hAng.2.1 hc0 hcB hKlip μ ν
  have hTangent :=
    AutoSamplingTheory.TechnicalLemmas.Geometry.QuadraticFeatureTangentGradient.quadratic_feature_potential_tangent_gradient
      F D hF M₁ M₂ hM₁ hM₂ hBound hLip
  let R₀ := B+‖y‖
  have hR₀ : 0 ≤ R₀ := add_nonneg hB (norm_nonneg y)
  have hResidual (μ : Measure S) [IsProbabilityMeasure μ] : ‖m μ-y‖ ≤ R₀ :=
    ((hMean μ μ).2.2.2.2 y).1
  have hGrad (μ : Measure S) (w : E) :
      HasGradientAt (V μ) ((2 : ℝ) • (D w).adjoint (m μ-y)) w := by
    rw [hasGradientAt_iff_hasFDerivAt]
    have he : InnerProductSpace.toDual ℝ E ((2 : ℝ) • (D w).adjoint (m μ-y)) =
        (2 : ℝ) • innerSL ℝ ((D w).adjoint (m μ-y)) := by
      ext v
      simp [InnerProductSpace.toDual_apply_apply,innerSL_apply_apply]
    rw [he]
    exact hTangent.1 (m μ-y) w
  let A := 2*M₁^2
  let B₂ := 2*(M₂+2*M₁)*R₀
  have hA : 0 ≤ A := by dsimp [A]; positivity
  have hB₂ : 0 ≤ B₂ := by dsimp [B₂]; positivity
  refine ⟨2*M₁*R₀+1,A+B₂+1,by positivity,by positivity,?_,?_⟩
  · intro μ hμ
    let : IsProbabilityMeasure μ := hμ
    refine ⟨(hMean μ μ).1,hGrad μ,?_⟩
    intro w
    have ht := hTangent.2.1 (m μ-y) w.1 w.property
    refine ⟨ht.1,?_⟩
    exact ht.2.2.trans ((mul_le_mul_of_nonneg_left (hResidual μ) (by positivity)).trans (by linarith))
  · intro μ ν hμ hν
    let : IsProbabilityMeasure μ := hμ
    let : IsProbabilityMeasure ν := hν
    refine ⟨(hMean μ ν).2.2.1,?_⟩
    intro w u
    have hm : ‖(m μ-y)-(m ν-y)‖ ≤ M₁*(Q μ ν ^ (1 / 2 : ℝ)).toReal := by
      simpa only [sub_sub_sub_cancel_right] using (hMean μ ν).2.2.2.1
    have hr := hResidual ν
    have ht := hTangent.2.2 (m μ-y) (m ν-y) w.1 u.1 w.property u.property
    have hpoint := (hAng.2.2.1 w u).2.2.2.1
    have ht' : ‖G μ w.1-G ν u.1‖ ≤
        A*(Q μ ν ^ (1 / 2 : ℝ)).toReal+B₂*c (w,u) := by
      calc
        _ ≤ 2*M₁*‖(m μ-y)-(m ν-y)‖+
            2*(M₂+2*M₁)*‖m ν-y‖*‖w.1-u.1‖ := ht
        _ ≤ 2*M₁*(M₁*(Q μ ν ^ (1 / 2 : ℝ)).toReal)+
            2*(M₂+2*M₁)*R₀*c (w,u) := by
          gcongr
        _ = _ := by dsimp [A,B₂]; ring
    apply ht'.trans
    have hs : 0 ≤ (Q μ ν ^ (1 / 2 : ℝ)).toReal := ENNReal.toReal_nonneg
    have hc := hc0 (w,u)
    nlinarith [mul_nonneg hA hc,mul_nonneg hB₂ hs]

end AutoSamplingTheory.TechnicalLemmas.Geometry.QuadraticFeatureLawGradient

Exact module and namespace context

Source correspondence and review

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
Let E be a finite-dimensional real inner-product normed space with its Borel measurable structure and H a complete real inner-product normed space. Let F:E→H have actual ambient Frechet derivative D(w):E→H for every w. Assume nonnegative M1,M2, an operator bound norm(D(w))<=M1 on the closed unit ball and an operator-Lipschitz bound norm(D(w)-D(u))<=M2 norm(w-u) there. Fix y in H. On the actual unit-norm subtype S define K(w)=F(w), angular cost c(u,v)=arccos(inner(u,v)), the actual Bochner mean m(mu)=integral K dmu, V_mu(w)=2 inner(m(mu)-y,F(w)), and G_mu(w)=2P_w D(w)^(m(mu)-y) with the explicit projection P_w z=z−⟨z,w⟩w, which projects onto w-perpendicular when norm(w)=1. Let Q(mu,nu) be the literal extended nonnegative infimum of the quadratic angular cost over all actual couplings. There exist C1,C2>0, independent of probability laws and unit weights, such that for every actual parameter probability K is integrable, V_mu has the displayed ambient gradient 2D(w)^(m(mu)-y) at every ambient w, and its projected G_mu is tangent and uniformly bounded by C1 at every unit weight. For every two actual parameter probabilities Q is finite and norm(G_mu(w)-G_nu(u))<=C2*(sqrt(Q).toReal+c(w,u)). Feature boundedness, strong measurability, feature Lipschitz control and residual budgets are derived inside the proof rather than assumed; the returned conclusions are feature integrability, actual ambient gradient, tangency/uniform bound, finite transport cost and the joint sensitivity estimate. The constants may depend on the displayed feature/derivative data, E,H and y. This is a generic feature-law theorem, not a concrete Gaussian scalar-data potential, installed manifold-gradient/Wasserstein API or intrinsic path-length theorem.	The exact adjacent signature retains the full displayed carrier and analytic data, actual Bochner law means, angular cost, extended all-coupling infimum and constant quantifier order.	same	Ambient derivatives/operator bounds are explicit generic inputs only to the feature-law result; all feature-integrability/residual/cost estimates are derived. Angular geometry supplies properties of the actual cost. No intrinsic-path/manifold/Wasserstein API identification or chosen statistical instance is claimed.

F and D plus their actual derivative/operator bounds remain explicit generic inputs. A specific model must produce them and identify its literal scalar potential with this Hilbert potential.; Angular all-coupling cost, tangent projection and actual ambient gradient are explicit. Identification with a chosen Riemannian-gradient/Wasserstein API or intrinsic path-length convention remains separate.; Auxiliary feature bounds, strong measurability and residual estimates are derived internally; they are not separately returned conjuncts. Constants may depend on E,H,F,D,M1,M2,y.

Encoder–denoiser: accepted · equivalent-after-elaboration

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

Scope and omitted-condition boundaries

F and D plus their actual derivative/operator bounds remain explicit generic inputs. A specific model must produce them and identify its literal scalar potential with this Hilbert potential.
Angular all-coupling cost, tangent projection and actual ambient gradient are explicit. Identification with a chosen Riemannian-gradient/Wasserstein API or intrinsic path-length convention remains separate.
Auxiliary feature bounds, strong measurability and residual estimates are derived internally; they are not separately returned conjuncts. Constants may depend on E,H,F,D,M1,M2,y.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le
Continuous.stronglyMeasurable
hasGradientAt_iff_hasFDerivAt
InnerProductSpace.toDual_apply_apply

Mathematical sources

Samplinglib original sphere geometry and feature-law supplement v1 (2026-10-23) (historical source) — Original generic canonical-library mathematics placed by subject; no primary-textbook theorem, concrete statistical model or whole chapter 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.

Which proof obligations and prerequisites are covered?

Formalized proof edge; source adapter/review separate Uniform gradients of quadratic feature-law potentials

Embedded geometry: first order

From feasible directions to gradients

Mathematical knowledge map

Feasible directions

Differentiate along the space

Represent by the metric

Project the ambient gradient

Proposition 3.35 and its extension-independence consequence

Complete source statement (Samplinglib restatement)

Source differential restriction

Selected extension-choice proof edge

Read the formalized proofs

Why the derivative along a feasible curve ignores the extension

Mathematical statement

Proof roadmap

All objects and hypotheses

Mathematical proof

1. Pull the agreement back to the curve

2. Differentiate each image curve

3. Use locality and uniqueness

Lean verification

Source assumptions versus formal assumptions

Detected semantic differences

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Mathematical sources

Which proof obligations and prerequisites are covered?

Proposition 3.61 · ambient-to-tangent gradient projection

Complete source statement (Samplinglib restatement)

Source projection formula

Read the formalized proofs

Project the gradient when restricting to an affine subspace

Mathematical statement

Proof roadmap

All objects and hypotheses

Mathematical proof

1. Differentiate the affine parameterization

2. Apply the actual chain rule

3. Remove the normal component and identify the gradient

Lean verification

Source assumptions versus formal assumptions

Detected semantic differences

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Mathematical sources

The induced gradient on the sphere is a projection

Mathematical statement

Proof roadmap

All objects and hypotheses

Mathematical proof

1. Identify actual tangent directions

2. Differentiate the actual restricted objective

3. Remove the normal component

4. Prove uniqueness on the whole tangent plane

Lean verification

Source assumptions versus formal assumptions

Detected semantic differences

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Mathematical sources

Which proof obligations and prerequisites are covered?

Example 3.62 · Rayleigh gradient and critical eigenvectors

Complete source statement (Samplinglib restatement)

Unit tangent projector and gradient

Both directions of stationarity

Read the formalized proofs

Rayleigh objective: remove the radial part of 2Ax

Mathematical statement

Proof roadmap

All objects and hypotheses

Mathematical proof

1. Differentiate the symmetric quadratic

2. Project onto the actual tangent plane

3. Use the induced differential characterization

Lean verification

Source assumptions versus formal assumptions

Source and reuse