Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412

SmoothGradientArcClipping: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

  1. Actual smooth gradient-arc clipping excess
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.

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))) := 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

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

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