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

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

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.