Actual smooth gradient-arc clipping excess

ASTIS mathematical restatement and exposition of the actual smooth gradient-estimator clipping bound, used as a dependency of Fan Chen, Sinho Chewi, Jianfeng Lu and Matthew S. Zhang, Smoothed Picard Hamiltonian Monte Carlo. The prior proof-supported factor2 moment is used without silently repairing the differing printed Claim1 log formula.

Complete source statement (Samplinglib restatement)

W_r and F_r are measurable, F_r is integrable under the actual input law mu, and its integral is at most 2 exp(-min(B^2/(40 beta^2 d eta^2),B/(8 beta eta))).

Actual clipping-excess moment

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

Actual smooth gradient-arc clipping excess

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.SmoothGradientArcClipping.smooth_gradient_arc_clipping · theorem · Teaching coverage

Read this first

Mathematical statement

W_r and F_r are measurable, F_r is integrable under the actual input law mu, and its integral is at most 2 exp(-min(B^2/(40 beta^2 d eta^2),B/(8 beta eta))).

\[\mathbb E_\mu\!\left[e^{2\ell\tau_B(W_r)}-1\right]\le2\exp\!\left[-\min\!\left\{\frac{B^2}{40\beta^2d\eta^2},\frac{B}{8\beta\eta}\right\}\right],\quad\tau_B(w)=(|w|-B)_+.\]

Lean statement · smooth_gradient_arc_clipping

Actual fixed-time gradient clipping-excess measurability, integrability and explicit source two-scale exponential bound.

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 smooth_gradient_arc_clipping (f : E → ℝ) (hf : Differentiable ℝ f)
    (eta beta B ell : ℝ) (heta : 0 < eta) (hbeta : 0 < beta) (hB : 0 < B)
    (hell : 2 ≤ ell) (hd : 0 < (Module.finrank ℝ E : ℝ))
    (hlip : LipschitzWith ⟨beta,hbeta.le⟩ (gradient f)) (h xp : E) (r : ℝ)
    (hcenter : ‖h-xp‖ ≤ Real.sqrt ((Module.finrank ℝ E : ℝ)*eta))
    (hstep : 64*beta^2*(ell*(Module.finrank ℝ E : ℝ)/B+ell^2) ≤ 1/eta^2) :
    let mu := ((stdGaussian E).map (fun z : E => h+Real.sqrt eta • z)).prod
      ((stdGaussian E).map (fun z : E => Real.sqrt eta • z))
    let W := fun p : E × E => inner ℝ (clipVelocity h r p)
      (gradient f xp-gradient f (clipArc h r p))
    let F := fun p : E × E => Real.exp (2*ell*max (|W p|-B) 0)-1
    Measurable W ∧ Measurable F ∧ Integrable F mu ∧
    (∫ p, F p ∂mu) ≤ 2*Real.exp (-min
      (B^2/(40*beta^2*(Module.finrank ℝ E : ℝ)*eta^2)) (B/(8*beta*eta)))

Exact module and namespace context

Proof roadmap

1Choose a parameter that lies in both required ranges
Let A=beta^2 d eta^2 and choose lambda as the minimum below. Multiply the step-size inequality by the positive eta^2. Its two nonnegative terms imply 8 beta eta ell≤1 and 64 beta^2 ell d eta^2≤B. These give 2ell below each cap, hence below their minimum. The first cap also ensures the previously proved moment theorem applies.
2Dominate the clipping excess pointwise
If abs(w)≤B, the excess is zero. Otherwise tau_B(w)=abs(w)-B≥0; since 2ell≤lambda, increasing the exponent and dropping the subtractive one gives the displayed bound. The left side is nonnegative because ell and tau_B are nonnegative.
3Apply the moment theorem to the same actual estimator
The gradient is continuous by its Lipschitz hypothesis, so the explicit arc formula makes W_r measurable. Invoke the actual smooth gradient-arc moment theorem with the chosen lambda. Its source center condition is exactly the present one; definitional equality identifies the same velocity, gradient difference and original independent Gaussian product input. No new independence or exponential-integrability premise is assumed.
4Establish integrability before comparing expectations
The right-hand side of the pointwise inequality is an integrable constant multiple of the proved moment integrand. Measurability and nonnegative domination establish integrability of F_r first. Integral monotonicity and the constant-multiple identity then yield the exponential bound.
5Recover the two explicit source scales
The second cap implies 20A lambda≤B. Multiplying by nonnegative lambda gives 10A lambda^2-B lambda≤-B lambda/2. Multiplication by positive B/2 commutes with the minimum; cancellation of the strictly positive denominators gives precisely the two scales. Exponential monotonicity finishes the claim.

Full assumptions and notation

All objects and hypotheses

E is a finite-dimensional real inner product space with its Borel measurable structure and positive real dimension d=finrank(E). The real-valued function f is differentiable everywhere, and its actual gradient is beta-Lipschitz.
eta,beta,B>0, ell≥2, and 64 beta^2(ell*d/B+ell^2)≤1/eta^2. All denominators in the conclusion are strictly positive.
h,x_plus in E satisfy norm(h-x_plus)≤sqrt(d eta). The independent input law is mu=N(h,eta I) product N(0,eta I), represented by the affine pushforwards of standard Gaussian.
For a fixed real r, theta=pi*r/2, gamma_r(x,z)=h+sin(theta)(x-h)+cos(theta)z, v_r(x,z)=(pi/2)(cos(theta)(x-h)-sin(theta)z), W_r=<v_r,grad f(x_plus)-grad f(gamma_r)>, tau_B(w)=max(abs(w)-B,0), and F_r=exp(2ell*tau_B(W_r))-1.

Mathematical proof

1. Choose a parameter that lies in both required ranges

Let A=beta^2 d eta^2 and choose lambda as the minimum below. Multiply the step-size inequality by the positive eta^2. Its two nonnegative terms imply 8 beta eta ell≤1 and 64 beta^2 ell d eta^2≤B. These give 2ell below each cap, hence below their minimum. The first cap also ensures the previously proved moment theorem applies.

\[\lambda=\min\!\left\{\frac1{4\beta\eta},\frac B{20A}\right\}\ge2\ell,\qquad12\beta^2\eta^2\lambda^2\le1.\]

Corresponding Lean step

clipping_parameter_lower; clipping_parameter_bounds

2. Dominate the clipping excess pointwise

If abs(w)≤B, the excess is zero. Otherwise tau_B(w)=abs(w)-B≥0; since 2ell≤lambda, increasing the exponent and dropping the subtractive one gives the displayed bound. The left side is nonnegative because ell and tau_B are nonnegative.

\[0\le e^{2\ell\tau_B(w)}-1\le e^{-\lambda B}e^{\lambda|w|}.\]

Corresponding Lean step

clipping_exp_domination

3. Apply the moment theorem to the same actual estimator

The gradient is continuous by its Lipschitz hypothesis, so the explicit arc formula makes W_r measurable. Invoke the actual smooth gradient-arc moment theorem with the chosen lambda. Its source center condition is exactly the present one; definitional equality identifies the same velocity, gradient difference and original independent Gaussian product input. No new independence or exponential-integrability premise is assumed.

\[\mathbb E_\mu e^{\lambda|W_r|}\le2e^{10A\lambda^2},\qquad e^{\lambda|W_r|}\in L^1(\mu).\]

Corresponding Lean step

smooth_gradient_arc_clipping; SmoothGradientArcMoment.smooth_gradient_arc_moment

4. Establish integrability before comparing expectations

The right-hand side of the pointwise inequality is an integrable constant multiple of the proved moment integrand. Measurability and nonnegative domination establish integrability of F_r first. Integral monotonicity and the constant-multiple identity then yield the exponential bound.

\[\mathbb E_\mu F_r\le e^{-\lambda B}\mathbb E_\mu e^{\lambda|W_r|}\le2e^{10A\lambda^2-B\lambda}.\]

Corresponding Lean step

clipping_integral_domination; Integrable.mono'; integral_mono; integral_const_mul

5. Recover the two explicit source scales

The second cap implies 20A lambda≤B. Multiplying by nonnegative lambda gives 10A lambda^2-B lambda≤-B lambda/2. Multiplication by positive B/2 commutes with the minimum; cancellation of the strictly positive denominators gives precisely the two scales. Exponential monotonicity finishes the claim.

\[10A\lambda^2-B\lambda\le-\frac{B\lambda}{2}=-\min\!\left\{\frac{B^2}{40A},\frac B{8\beta\eta}\right\}.\]

Corresponding Lean step

clipping_parameter_bounds; mul_min_of_nonneg; min_div_div_right; Real.exp_le_exp

Lean verification

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

Lean proof · smooth_gradient_arc_clipping

Source parameter caps, pointwise nonnegative domination, actual parent MGF, integrable comparison and exact minimum algebra.

Download module (.lean)

theorem smooth_gradient_arc_clipping (f : E → ℝ) (hf : Differentiable ℝ f)
    (eta beta B ell : ℝ) (heta : 0 < eta) (hbeta : 0 < beta) (hB : 0 < B)
    (hell : 2 ≤ ell) (hd : 0 < (Module.finrank ℝ E : ℝ))
    (hlip : LipschitzWith ⟨beta,hbeta.le⟩ (gradient f)) (h xp : E) (r : ℝ)
    (hcenter : ‖h-xp‖ ≤ Real.sqrt ((Module.finrank ℝ E : ℝ)*eta))
    (hstep : 64*beta^2*(ell*(Module.finrank ℝ E : ℝ)/B+ell^2) ≤ 1/eta^2) :
    let mu := ((stdGaussian E).map (fun z : E => h+Real.sqrt eta • z)).prod
      ((stdGaussian E).map (fun z : E => Real.sqrt eta • z))
    let W := fun p : E × E => inner ℝ (clipVelocity h r p)
      (gradient f xp-gradient f (clipArc h r p))
    let F := fun p : E × E => Real.exp (2*ell*max (|W p|-B) 0)-1
    Measurable W ∧ Measurable F ∧ Integrable F mu ∧
    (∫ p, F p ∂mu) ≤ 2*Real.exp (-min
      (B^2/(40*beta^2*(Module.finrank ℝ E : ℝ)*eta^2)) (B/(8*beta*eta))) := by
  let d := (Module.finrank ℝ E : ℝ)
  let lam := min (1/(4*beta*eta)) (B/(20*beta^2*d*eta^2))
  let mu := ((stdGaussian E).map (fun z : E => h+Real.sqrt eta • z)).prod
      ((stdGaussian E).map (fun z : E => Real.sqrt eta • z))
  let W := fun p : E × E => inner ℝ (clipVelocity h r p)
      (gradient f xp-gradient f (clipArc h r p))
  have hell0 : 0 ≤ ell := by linarith
  obtain ⟨hl,hll,hrange,he⟩ := clipping_parameter_bounds eta beta B ell d heta hbeta hB hell0 hd hstep
  change 0 ≤ lam at hl
  change 2*ell ≤ lam at hll
  change 12*beta^2*eta^2*lam^2 ≤ 1 at hrange
  have hW : Measurable W := by
    have hg := hlip.continuous.measurable
    dsimp [W,clipVelocity,clipArc]
    fun_prop
  obtain ⟨_,_,hi,hv,_⟩ :=
    AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.SmoothGradientArcMoment.smooth_gradient_arc_moment
      f hf eta beta lam heta hbeta.le hl hlip h xp r hcenter hrange
  change Integrable (fun p => Real.exp (lam*|W p|)) mu at hi
  change (∫ p, Real.exp (lam*|W p|) ∂mu) ≤ 2*Real.exp (10*d*eta^2*lam^2*beta^2) at hv
  obtain ⟨hI,hv'⟩ := clipping_integral_domination mu W hW B ell lam hell0 hll hi
  refine ⟨hW, ?_, hI, hv'.trans ?_⟩
  · change Measurable (fun p => Real.exp (2*ell*max (|W p|-B) 0)-1)
    fun_prop
  · calc
      _ ≤ Real.exp (-lam*B)*(2*Real.exp (10*d*eta^2*lam^2*beta^2)) :=
        mul_le_mul_of_nonneg_left hv (Real.exp_nonneg _)
      _ = 2*Real.exp (10*d*eta^2*lam^2*beta^2-B*lam) := by
        rw [← mul_assoc, mul_comm (Real.exp (-lam*B)) 2, mul_assoc, ← Real.exp_add]
        congr 2
        ring
      _ ≤ _ := by
        apply mul_le_mul_of_nonneg_left _ (by norm_num : (0 : ℝ) ≤ 2)
        exact Real.exp_le_exp.mpr he


end
end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.SmoothGradientArcClipping

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
Smooth s=1 Euclidean case with positive dimension and beta.	Finite-dimensional real inner-product Borel space with positive finrank and beta.	generalization	Basis-independent domain retains the source positive-denominator conditions; zero-dimensional and zero-beta cases are not asserted.
For each r in [0,1].	For each real r.	generalization	The actual parent arc moment holds for all real angles. No random-time integration conclusion is added.
Source center h=x0-eta grad f(x_plus) with residual at most sqrt(d eta).	Arbitrary h,x_plus satisfying exactly this residual bound.	generalization	Only the distance bound enters the moment. Center/reference construction remains a later consumer.
Positive eta,beta,B,d; ell>=2 in the surrounding theorem; 1/eta^2>=64 beta^2(ell*d/B+ell^2).	Exactly these inequalities, with d=finrank(E), differentiable f and its actual beta-Lipschitz gradient.	same	No assumed MGF or integrability premise; source parameter range proves the needed moment and clipping comparisons.
Expectation of exp(2ell tau_B(W))-1 bounded by2 exp(-min(B²/(40 beta² d eta²),B/(8 beta eta))).	Same actual input, clipping excess max(abs(W)-B,0) and constants; W and excess integrand measurable, integrand integrable.	source-implicit	All analytic obligations for the actual expectation are proved explicitly before comparison.
Claim2 feeds Eq18 and normalized terminal approximation, later using B=Theta(1).	Fixed-time clipping-excess moment for arbitrary B>0 under the displayed step condition.	same	This is the selected proof edge only. Joint time measurability, target mean, target law, Renyi accuracy and cost remain separate; arbitrary B does not assert uniform cost.

This is the fixed-r smooth Claim 2 clipping-excess moment for the actual estimator. The finite-dimensional inner-product domain and all-real r are disclosed extensions; positive dimension and beta are retained. Constructing h=x0-eta grad f(x_plus), joint time measurability and averaging over random uniform time, unclipped mean identification, the clipped target law, normalized Renyi accuracy, initialization and actual query costs remain separate. Arbitrary B>0 does not imply a uniform constant-cost statement; later source use sets B=Theta(1). The parent factor2 moment is used, without silently repairing printed Claim 1.

Encoder–denoiser: accepted · domain-mismatch

Detected semantic differences

domains: Positive-dimensional coordinate-free domain; positivity preserved. — Independent formal source review accepted this disclosed difference.
quantifiers: All-real r supported by parent; random-time averaging not asserted. — Independent formal source review accepted this disclosed difference.
quantifiers: Arbitrary residual-controlled center; source center construction deferred. — Independent formal source review accepted this disclosed difference.
assumptions: Positive parameters, ell and step retained without assumed MGF or integrability. — Independent formal source review accepted this disclosed difference.
conclusion: Actual measurability and integrability proved; bound unchanged. — Independent formal source review accepted this disclosed difference.
scopes: Selected Claim2 only; arbitrary B does not imply uniform constant cost. — Independent formal source review accepted this disclosed difference.

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 fixed-r smooth Claim 2 clipping-excess moment for the actual estimator. The finite-dimensional inner-product domain and all-real r are disclosed extensions; positive dimension and beta are retained. Constructing h=x0-eta grad f(x_plus), joint time measurability and averaging over random uniform time, unclipped mean identification, the clipped target law, normalized Renyi accuracy, initialization and actual query costs remain separate. Arbitrary B>0 does not imply a uniform constant-cost statement; later source use sets B=Theta(1). The parent factor2 moment is used, without silently repairing printed Claim 1.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.SmoothGradientArcMoment.smooth_gradient_arc_moment

Mathlib API called (external library)

MeasureTheory.Integrable.mono'
MeasureTheory.integral_mono
MeasureTheory.integral_const_mul
mul_min_of_nonneg
min_div_div_right
Real.exp_le_exp

Mathematical sources

Appendix D.1 Claim 2, smooth s=1 — Explicit clipping-excess exponential bound for the actual gradient estimator.
SPHMC Appendix A.4(2) — Terminal gradient-estimator approximation consumer.

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

Actual smooth gradient-arc clipping excess

Complete source statement (Samplinglib restatement)

Actual clipping-excess moment

Read the formalized proofs

Actual smooth gradient-arc clipping excess

Mathematical statement

Proof roadmap

All objects and hypotheses

Mathematical proof

1. Choose a parameter that lies in both required ranges

2. Dominate the clipping excess pointwise

3. Apply the moment theorem to the same actual estimator

4. Establish integrability before comparing expectations

5. Recover the two explicit source scales

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?