The same Gaussian derivative is bounded and Lipschitz on the closed unit ball
Mathematical statement
Let E be a finite-dimensional real inner-product normed space with its Borel measurable structure, let γ be its centered standard Gaussian law with identity covariance, and let p be any finite real polynomial. For every ambient weight w and direction v, the actual functions f_w(x)=p(⟨w,x⟩) and d_{w,v}(x)=p′(⟨w,x⟩)⟨v,x⟩ belong to L²(γ). There exist simultaneous membership witnesses and a field of continuous real linear maps D(w):E→L²(γ), with D(w)v=[d_{w,v}], such that the actual feature-class map Φ(w)=[f_w] is fully Fréchet differentiable with derivative D(w) at every ambient w. There also exist strictly positive real constants M₁,M₂ such that ‖D(w)‖op≤M₁ for every ‖w‖≤1 and ‖D(u)−D(w)‖op≤M₂‖u−w‖ whenever both weights lie in the closed unit ball. The constants may depend on p and the ambient space; no dimension-independent rate is asserted. All memberships, derivatives and bounds are produced.
Lean statement · actual_gaussian_polynomial_ridge_L2_derivative_bounds
Let E be a finite-dimensional real inner-product normed space with its Borel measurable structure, let γ be its centered standard Gaussian law with identity covariance, and let p be any finite real polynomial. For every ambient weight w and direction v, the actual functions f_w(x)=p(⟨w,x⟩) and d_{w,v}(x)=p′(⟨w,x⟩)⟨v,x⟩ belong to L²(γ). There exist simultaneous membership witnesses and a field of continuous real linear maps D(w):E→L²(γ), with D(w)v=[d_{w,v}], such that the actual feature-class map Φ(w)=[f_w] is fully Fréchet differentiable with derivative D(w) at every ambient w. There also exist strictly positive real constants M₁,M₂ such that ‖D(w)‖op≤M₁ for every ‖w‖≤1 and ‖D(u)−D(w)‖op≤M₂‖u−w‖ whenever both weights lie in the closed unit ball. The constants may depend on p and the ambient space; no dimension-independent rate is asserted. All memberships, derivatives and bounds are produced.
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.
theorem actual_gaussian_polynomial_ridge_L2_derivative_bounds
{E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
[FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
(p : Polynomial ℝ) :
let γ := ProbabilityTheory.stdGaussian E
let f : E → E → ℝ := fun w x => p.eval ⟪w,x⟫_ℝ
let df : E → E → E → ℝ := fun w v x => p.derivative.eval ⟪w,x⟫_ℝ * ⟪v,x⟫_ℝ
∃ hf : ∀ w, MemLp (f w) 2 γ,
∃ hdf : ∀ w v, MemLp (df w v) 2 γ,
∃ D : E → E →L[ℝ] Lp ℝ 2 γ,
(∀ w v, D w v = (hdf w v).toLp (df w v)) ∧
(∀ w, HasFDerivAt (fun u => (hf u).toLp (f u)) (D w) w) ∧
∃ M₁ M₂ : ℝ, 0 < M₁ ∧ 0 < M₂ ∧
(∀ w : E, ‖w‖ ≤ 1 → ‖D w‖ ≤ M₁) ∧
∀ w u : E, ‖w‖ ≤ 1 → ‖u‖ ≤ 1 → ‖D u - D w‖ ≤ M₂ * ‖u-w‖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
- The only mathematical data are E with its finite-dimensional real inner-product and Borel structures, and a finite real polynomial p.
- The returned operator estimates apply to the same derivative field in the ambient derivative conclusion; both endpoint weights in the difference estimate satisfy norm at most one.
Mathematical proof
1. Reuse the actual ambient derivative
Call the preceding producer to obtain feature memberships, derivative memberships, representation and full Fréchet differentiability together. The following bounds concern this same D.
Corresponding Lean step
dsimp only
obtain ⟨hf,hdf,D,hD,hDiff⟩ := actual_gaussian_polynomial_ridge_L2_frechet_derivative (E := E) p
exact ⟨hf,hdf,D,hD,hDiff,produced_operator_bounds p hdf D hD⟩
Literal implementation excerpt from AutoSamplingTheory/TechnicalLemmas/Probability/GaussianPolynomialDifferentiation.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. Produce first and second polynomial envelopes
Gaussian radial moments supply B,C∈L² uniformly on the closed unit ball, with radial factors of orders one and two respectively.
Corresponding Lean step
obtain ⟨B,hB,hB0,hBound⟩ := polynomial_radial_envelope (E := E) p.derivative 1 (by norm_num) 1
obtain ⟨C,hC,hC0,hBound2⟩ := polynomial_radial_envelope (E := E) p.derivative.derivative 1 (by norm_num) 2
let b := hB.toLp B
let c := hC.toLp C
Literal implementation excerpt from AutoSamplingTheory/TechnicalLemmas/Probability/GaussianPolynomialDifferentiation.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.
3. Bound every directional operator value
The first envelope and Cauchy–Schwarz for the scalar inner product give an almost-everywhere domination of D(w)v. The L² order estimate yields the operator norm bound.
Corresponding Lean step
have hnorm (w : E) (hw : ‖w‖ ≤ 1) (v : E) : ‖D w v‖ ≤ ‖v‖ * ‖b‖ := by
apply Lp.norm_le_mul_norm_of_ae_le_mul
rw [hD w v]
filter_upwards [(hdf w v).coeFn_toLp,hB.coeFn_toLp] with x hv hBx
rw [hv]
change ‖p.derivative.eval ⟪w,x⟫_ℝ * ⟪v,x⟫_ℝ‖ ≤ ‖v‖ * ‖hB.toLp B x‖
rw [hBx,Real.norm_of_nonneg (hB0 x),norm_mul]
calc
‖p.derivative.eval ⟪w,x⟫_ℝ‖ * ‖⟪v,x⟫_ℝ‖ ≤
‖p.derivative.eval ⟪w,x⟫_ℝ‖ * (‖v‖*‖x‖) :=
mul_le_mul_of_nonneg_left (norm_inner_le_norm (𝕜 := ℝ) v x) (norm_nonneg _)
_ = ‖v‖ * (‖p.derivative.eval ⟪w,x⟫_ℝ‖ * ‖x‖) := by ring
_ ≤ ‖v‖ * B x := mul_le_mul_of_nonneg_left
(by simpa only [pow_one] using hBound w hw x) (norm_nonneg _)
Literal implementation excerpt from AutoSamplingTheory/TechnicalLemmas/Probability/GaussianPolynomialDifferentiation.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.
4. Apply a scalar mean-value theorem inside the convex ball
Differentiate the p′ directional expression. Convexity keeps the interpolation between u and w inside the same ball, so the second envelope controls its increment.
Corresponding Lean step
have hinc (w u : E) (hw : ‖w‖ ≤ 1) (hu : ‖u‖ ≤ 1) (v x : E) :
‖p.derivative.eval ⟪u,x⟫_ℝ * ⟪v,x⟫_ℝ -
p.derivative.eval ⟪w,x⟫_ℝ * ⟪v,x⟫_ℝ‖ ≤ (‖v‖ * C x) * ‖u-w‖ := by
let d := fun z : E => ⟪v,x⟫_ℝ • (p.derivative.derivative.eval ⟪z,x⟫_ℝ • innerSL ℝ x)
have hd (z : E) : HasFDerivAt (fun q : E =>
p.derivative.eval ⟪q,x⟫_ℝ * ⟪v,x⟫_ℝ) (d z) z := by
convert (pointwise_ridge_hasFDerivAt p.derivative z x).const_smul ⟪v,x⟫_ℝ using 1 <;>
(first | rfl | (ext q; simp [d,Pi.smul_apply,smul_eq_mul,mul_comm]))
apply (convex_closedBall (0 : E) 1).norm_image_sub_le_of_norm_hasFDerivWithin_le
(fun z _ => (hd z).hasFDerivWithinAt) ?_
(by simpa [Metric.mem_closedBall,dist_zero_right] using hw)
(by simpa [Metric.mem_closedBall,dist_zero_right] using hu)
intro z hz
have hz' : ‖z‖ ≤ 1 := by simpa [Metric.mem_closedBall,dist_zero_right] using hz
dsimp only [d]
rw [norm_smul,norm_smul,innerSL_apply_norm]
calc
‖⟪v,x⟫_ℝ‖ * (‖p.derivative.derivative.eval ⟪z,x⟫_ℝ‖ * ‖x‖) ≤
(‖v‖ * ‖x‖) * (‖p.derivative.derivative.eval ⟪z,x⟫_ℝ‖ * ‖x‖) :=
mul_le_mul_of_nonneg_right (norm_inner_le_norm (𝕜 := ℝ) v x) (by positivity)
_ = ‖v‖ * (‖p.derivative.derivative.eval ⟪z,x⟫_ℝ‖ * ‖x‖^2) := by ring
_ ≤ ‖v‖ * C x := mul_le_mul_of_nonneg_left (hBound2 z hz' x) (norm_nonneg _)
Literal implementation excerpt from AutoSamplingTheory/TechnicalLemmas/Probability/GaussianPolynomialDifferentiation.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.
5. Pass to operator norms with positive witnesses
Actual-class subtraction and L² domination give the difference bound for every v. Take the operator norm and choose M₁=‖[B]‖₂+1 and M₂=‖[C]‖₂+1 to retain strict positivity even for constant or zero p.
Corresponding Lean step
have hdiff (w u : E) (hw : ‖w‖ ≤ 1) (hu : ‖u‖ ≤ 1) (v : E) :
‖(D u-D w) v‖ ≤ (‖u-w‖*‖v‖) * ‖c‖ := by
apply Lp.norm_le_mul_norm_of_ae_le_mul
have hdu := (hdf u v).coeFn_toLp
have hdw := (hdf w v).coeFn_toLp
rw [← hD u v] at hdu
rw [← hD w v] at hdw
filter_upwards [Lp.coeFn_sub (D u v) (D w v),hdu,hdw,hC.coeFn_toLp]
with x hsub hux hwx hCx
change ‖(D u v - D w v) x‖ ≤ (‖u-w‖*‖v‖) * ‖hC.toLp C x‖
rw [hsub]
simp only [Pi.sub_apply]
rw [hux,hwx,hCx,Real.norm_of_nonneg (hC0 x)]
exact (hinc w u hw hu v x).trans_eq (by ring)
have hOp (w : E) (hw : ‖w‖ ≤ 1) : ‖D w‖ ≤ ‖b‖ := by
apply ContinuousLinearMap.opNorm_le_bound _ (norm_nonneg _)
intro v
simpa only [mul_comm] using hnorm w hw v
have hOpDiff (w u : E) (hw : ‖w‖ ≤ 1) (hu : ‖u‖ ≤ 1) :
‖D u-D w‖ ≤ ‖c‖ * ‖u-w‖ := by
apply ContinuousLinearMap.opNorm_le_bound _ (by positivity)
intro v
exact (hdiff w u hw hu v).trans_eq (by ring)
refine ⟨‖b‖+1,‖c‖+1,by positivity,by positivity,?_,?_⟩
· intro w hw
exact (hOp w hw).trans (by linarith)
· intro w u hw hu
exact (hOpDiff w u hw hu).trans
(mul_le_mul_of_nonneg_right (by linarith : ‖c‖ ≤ ‖c‖+1) (norm_nonneg _))
Literal implementation excerpt from AutoSamplingTheory/TechnicalLemmas/Probability/GaussianPolynomialDifferentiation.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.
Lean verification
Lean proof · actual_gaussian_polynomial_ridge_L2_derivative_bounds
The displayed formula proof explains the mathematical route; the exact Lean is folded adjacent.
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.
theorem actual_gaussian_polynomial_ridge_L2_derivative_bounds
{E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
[FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
(p : Polynomial ℝ) :
let γ := ProbabilityTheory.stdGaussian E
let f : E → E → ℝ := fun w x => p.eval ⟪w,x⟫_ℝ
let df : E → E → E → ℝ := fun w v x => p.derivative.eval ⟪w,x⟫_ℝ * ⟪v,x⟫_ℝ
∃ hf : ∀ w, MemLp (f w) 2 γ,
∃ hdf : ∀ w v, MemLp (df w v) 2 γ,
∃ D : E → E →L[ℝ] Lp ℝ 2 γ,
(∀ w v, D w v = (hdf w v).toLp (df w v)) ∧
(∀ w, HasFDerivAt (fun u => (hf u).toLp (f u)) (D w) w) ∧
∃ M₁ M₂ : ℝ, 0 < M₁ ∧ 0 < M₂ ∧
(∀ w : E, ‖w‖ ≤ 1 → ‖D w‖ ≤ M₁) ∧
∀ w u : E, ‖w‖ ≤ 1 → ‖u‖ ≤ 1 → ‖D u - D w‖ ≤ M₂ * ‖u-w‖ := by
dsimp only
obtain ⟨hf,hdf,D,hD,hDiff⟩ := actual_gaussian_polynomial_ridge_L2_frechet_derivative (E := E) p
exact ⟨hf,hdf,D,hD,hDiff,produced_operator_bounds p hdf D hD⟩
end AutoSamplingTheory.TechnicalLemmas.Probability.GaussianPolynomialDifferentiationScope and omitted-condition boundaries
- The p′′ envelope is a proved estimate, not an assumed bound on a second feature derivative.
- This theorem makes no global-in-weight uniform bound, sharp constant, dimension-independent estimate, second Fréchet derivative or manifold-gradient assertion.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
Mathlib API called (external library)
- Pinned Mathlib Gaussian norm moments and actual L² quotient 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.