Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0

AffineGradient: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

  1. Project the gradient when restricting to an affine subspace
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.

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

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

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

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

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

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.