ASTIS mathematical exposition

Actual smooth gradient-arc clipping excess

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

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)_+.\]

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

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

Lean proof · smooth_gradient_arc_clipping

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

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

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.

Source and reuse

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

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