Samplinglib mathematical lesson

Uniform gradients of quadratic feature-law potentials

Read this first

Mathematical statement

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.

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

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.

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