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

Actual clipped-output exponential mean-error bounds

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ClippedMeanExponential.clipped_mean_exponential · theorem · Teaching coverage

Statement

m, mB and V are measurable. For every x, V(x)>=0 and abs(m(x)-mB(x))<=V(x). The function J(x)=exp(2*ell*V(x))-1 is integrable under q and qhat, with respective integrals at most 2*exp(-K) and 2*exp(2*B-K). The function exp(2*ell*abs(m(x)-mB(x)))-1 is qhat-integrable and its integral is at most 2*exp(2*B-K).

\[\mathbb E_q[e^{2\ell V}-1]\le 2e^{-K},\qquad \mathbb E_{\widehat q}[e^{2\ell V}-1]\le 2e^{2B-K},\qquad \mathbb E_{\widehat q}[e^{2\ell|m-m_B|}-1]\le 2e^{2B-K}.\]

All objects and hypotheses

  • E is a finite-dimensional real inner-product Borel space, d=finrank(E)>0. The actual potential f is differentiable everywhere and its actual gradient is globally beta-Lipschitz. eta,beta,B>0 and ell>=2.
  • Set g=grad f(x_plus), h=x0-eta*g. Assume norm(h-x_plus)<=sqrt(d*eta) and 64*beta^2*(ell*d/B+ell^2)<=1/eta^2. These residual and step assumptions are retained exactly.
  • Let P=(z->sqrt(eta) z)_*stdGaussian(E), U=volume restricted to (0,1], nu=U product P and q=(z->h+sqrt(eta) z)_*stdGaussian(E). For s=(r,z), theta=pi*r/2, gamma=h+sin(theta)(x-h)+cos(theta)z and v=(pi/2)(cos(theta)(x-h)-sin(theta)z), define W(x,s)=<v,g-grad f(gamma)>.
  • Define m(x)=integral W(x,s) dnu(s), mB(x)=integral min(B,max(-B,W(x,s))) dnu(s), V(x)=integral max(abs(W(x,s))-B,0) dnu(s), qhat=q.tilted(mB), and K=min(B^2/(40*beta^2*d*eta^2),B/(8*beta*eta)). All functions and measures are actual definitions, not abstract witnesses.

Mathematical proof

1. Use the actual fixed-time clipping estimate

For each real time r, the parent theorem applies to the actual independent proposal and auxiliary Gaussians. It proves integrability of the nonnegative exponential excess and its uniform bound. Joint measurability follows from the actual Lipschitz gradient and the explicit trigonometric estimator. Integrability of the section integrals follows by domination with the constant bound, so the product integrability criterion proves genuine joint L1 before any use of Fubini.

\[H(r,x,z)=e^{2\ell(|W(x,r,z)|-B)_+}-1\ge0,\quad \int H(r,x,z)\,d(q\otimes P)\le2e^{-K}.\]
Corresponding Lean step

product_bound; actual_time_product; AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.SmoothGradientArcClipping.smooth_gradient_arc_clipping

2. Reorder the independent inputs with a measure-preserving map

Compose the measurable product associator, the swap of the proposal and time coordinates, and the inverse associator. This gives the actual map (x,(r,z)) to (r,(x,z)). Its measure-preserving property transfers joint integrability and the integral exactly, without replacing any marginal distribution or introducing a new independence assumption.

\[T_*(q\otimes(U\otimes P))=U\otimes(q\otimes P),\qquad T(x,(r,z))=(r,(x,z)).\]
Corresponding Lean step

swap_time_preserving; swap_time_integrable; MeasureTheory.Measure.measurePreserving_swap

3. Apply conditional Jensen only after establishing integrability

The program parent proves integrability of the truncation excess for every fixed x. Genuine joint exponential L1 supplies exponential section integrability for q-almost every x. Apply convexity of the exponential on those sections. Measurability of V follows from the measurable parameter integral. The resulting nonnegative Jensen bound dominates J by an integrable section integral, proving outer L1 before integrating the inequality.

\[e^{2\ell V(x)}-1\le\int\!\left(e^{2\ell(|W(x,s)|-B)_+}-1\right)d\nu(s)\quad(q\text{-a.e. }x).\]
Corresponding Lean step

exponential_mean_bound; integrated_exponential_mean; actual_proposal_bound; convexOn_exp.map_integral_le

4. Identify the actual means and the pointwise truncation error

GradientArcMean identifies the untruncated mean with the actual affine potential expression using a single constant chosen independently of x. ClippedGradientProgram proves the corresponding error estimate and measurability for the actual clipped mean. Substituting the common mean identity gives the pointwise bound for every x. Nonnegativity of V comes from its nonnegative integrand.

\[m(x)=\langle g,x\rangle-f(x)+C,\qquad 0\le V(x),\qquad |m(x)-m_B(x)|\le V(x).\]
Corresponding Lean step

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.GradientArcMean.gradient_arc_mean; AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ClippedGradientProgram.clipped_gradient_program

5. Bound the actual clipped density using its positive normalizer

The program parent gives abs(mB)<=B and ZB>=exp(-B)>0. Thus the actual clipped density w=exp(mB)/ZB is nonnegative, measurable and at most exp(2B). Dominate w*J by exp(2B)*J to prove weighted integrability first. The withDensity equivalence then gives J integrability under qhat, and integration of the density bound yields the clipped-output estimate. No closeness metric is used to transport this unbounded function.

\[Z_B=\int e^{m_B}\,dq\ge e^{-B}>0,\qquad 0\le\frac{e^{m_B(x)}}{Z_B}\le e^{2B},\qquad \int J\,d\widehat q\le e^{2B}\int J\,dq.\]
Corresponding Lean step

clipped_density_transfer; MeasureTheory.integrable_withDensity_iff_integrable_smul'; MeasureTheory.integral_withDensity_eq_integral_toReal_smul

6. Dominate the true mean error under the clipped output law

Since ell>=2, monotonicity of the exponential and the pointwise mean-error bound dominate the nonnegative true-error exponential by J. Its measurability and this domination prove its integrability under the actual clipped output law. Integrating gives the same bound, retaining the prefactor 2. Normalized comparison with the ideal law is a subsequent theorem obligation.

\[0\le e^{2\ell|m-m_B|}-1\le e^{2\ell V}-1,\qquad \int(e^{2\ell|m-m_B|}-1)\,d\widehat q\le2e^{2B-K}.\]
Corresponding Lean step

clipped_mean_exponential; MeasureTheory.Integrable.mono'; MeasureTheory.integral_mono

Lean statement · clipped_mean_exponential

Three measurable actual means/excess functions, pointwise nonnegative excess and mean-error bound, three outer exponential L1 statements and three explicit integral bounds.

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 clipped_mean_exponential (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)) (x0 xp : E)
    (hcenter : ‖(x0-eta • gradient f xp)-xp‖ ≤ Real.sqrt ((Module.finrank ℝ E : ℝ)*eta))
    (hstep : 64*beta^2*(ell*(Module.finrank ℝ E : ℝ)/B+ell^2) ≤ 1/eta^2) :
    let h := x0-eta • gradient f xp
    let q := (stdGaussian E).map (fun z => h+Real.sqrt eta • z)
    let P := (stdGaussian E).map (fun z => Real.sqrt eta • z)
    let nu := (volume.restrict (Set.Ioc (0 : ℝ) 1)).prod P
    let m := fun x => ∫ a, estimator f h xp (x,a) ∂nu
    let mB := fun x => ∫ a, min B (max (-B) (estimator f h xp (x,a))) ∂nu
    let V := fun x => ∫ a, max (|estimator f h xp (x,a)|-B) 0 ∂nu
    let qhat := q.tilted mB
    let K := min (B^2/(40*beta^2*(Module.finrank ℝ E : ℝ)*eta^2)) (B/(8*beta*eta))
    Measurable m ∧ Measurable mB ∧ Measurable V ∧
      (∀ x, 0 ≤ V x ∧ |m x-mB x| ≤ V x) ∧
      Integrable (fun x => Real.exp (2*ell*V x)-1) q ∧
      (∫ x, Real.exp (2*ell*V x)-1 ∂q) ≤ 2*Real.exp (-K) ∧
      Integrable (fun x => Real.exp (2*ell*V x)-1) qhat ∧
      (∫ x, Real.exp (2*ell*V x)-1 ∂qhat) ≤ 2*Real.exp (2*B-K) ∧
      Integrable (fun x => Real.exp (2*ell*|m x-mB x|)-1) qhat ∧
      (∫ x, Real.exp (2*ell*|m x-mB x|)-1 ∂qhat) ≤ 2*Real.exp (2*B-K)

Exact module and namespace context

Lean proof · clipped_mean_exponential

Actual product L1, measure-preserving reordering, conditional Jensen, actual mean identity, positive clipped normalizer and density domination.

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 clipped_mean_exponential (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)) (x0 xp : E)
    (hcenter : ‖(x0-eta • gradient f xp)-xp‖ ≤ Real.sqrt ((Module.finrank ℝ E : ℝ)*eta))
    (hstep : 64*beta^2*(ell*(Module.finrank ℝ E : ℝ)/B+ell^2) ≤ 1/eta^2) :
    let h := x0-eta • gradient f xp
    let q := (stdGaussian E).map (fun z => h+Real.sqrt eta • z)
    let P := (stdGaussian E).map (fun z => Real.sqrt eta • z)
    let nu := (volume.restrict (Set.Ioc (0 : ℝ) 1)).prod P
    let m := fun x => ∫ a, estimator f h xp (x,a) ∂nu
    let mB := fun x => ∫ a, min B (max (-B) (estimator f h xp (x,a))) ∂nu
    let V := fun x => ∫ a, max (|estimator f h xp (x,a)|-B) 0 ∂nu
    let qhat := q.tilted mB
    let K := min (B^2/(40*beta^2*(Module.finrank ℝ E : ℝ)*eta^2)) (B/(8*beta*eta))
    Measurable m ∧ Measurable mB ∧ Measurable V ∧
      (∀ x, 0 ≤ V x ∧ |m x-mB x| ≤ V x) ∧
      Integrable (fun x => Real.exp (2*ell*V x)-1) q ∧
      (∫ x, Real.exp (2*ell*V x)-1 ∂q) ≤ 2*Real.exp (-K) ∧
      Integrable (fun x => Real.exp (2*ell*V x)-1) qhat ∧
      (∫ x, Real.exp (2*ell*V x)-1 ∂qhat) ≤ 2*Real.exp (2*B-K) ∧
      Integrable (fun x => Real.exp (2*ell*|m x-mB x|)-1) qhat ∧
      (∫ x, Real.exp (2*ell*|m x-mB x|)-1 ∂qhat) ≤ 2*Real.exp (2*B-K) := by
  let h := x0-eta • gradient f xp
  let q := (stdGaussian E).map (fun z => h+Real.sqrt eta • z)
  let P := (stdGaussian E).map (fun z => Real.sqrt eta • z)
  let nu := (volume.restrict (Set.Ioc (0 : ℝ) 1)).prod P
  let m := fun x => ∫ a, estimator f h xp (x,a) ∂nu
  let mB := fun x => ∫ a, min B (max (-B) (estimator f h xp (x,a))) ∂nu
  let V := fun x => ∫ a, max (|estimator f h xp (x,a)|-B) 0 ∂nu
  let K := min (B^2/(40*beta^2*(Module.finrank ℝ E : ℝ)*eta^2)) (B/(8*beta*eta))
  have hp := AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ClippedGradientProgram.clipped_gradient_program
    f hf eta beta B heta hbeta.le hB hlip x0 xp
  have hmB : Measurable mB := hp.2.2.2.2.1
  have hx := hp.2.2.2.2.2.1
  have hmean := AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.GradientArcMean.gradient_arc_mean
    f hf eta beta heta hbeta.le hlip h xp
  let C := (∫ z, f (h+z) ∂P)-inner ℝ (gradient f xp) h
  have hme (x : E) : m x = inner ℝ (gradient f xp) x-f x+C :=
    (hmean.2.2.2 x).2.2.2
  have hm : Measurable m := by
    have heq : m = fun x => inner ℝ (gradient f xp) x-f x+C := funext hme
    rw [heq]
    exact ((by fun_prop : Measurable (fun x => inner ℝ (gradient f xp) x)).sub
      hf.continuous.measurable).add_const C
  have herr (x : E) : |m x-mB x| ≤ V x := by
    rw [abs_sub_comm, hme]
    exact (hx x).2.2.2.2
  have hv := actual_proposal_bound f hf eta beta B ell heta hbeta hB hell hd hlip x0 xp hcenter hstep
  have hV : Measurable V := hv.1
  have he : 0 ≤ 2*ell := by linarith
  have hJpos (x : E) : 0 ≤ Real.exp (2*ell*V x)-1 :=
    sub_nonneg.mpr (Real.one_le_exp_iff.mpr (mul_nonneg he (hv.2.1 x)))
  have ht := clipped_density_transfer q mB (fun x => Real.exp (2*ell*V x)-1)
    hmB (by fun_prop) hJpos hv.2.2.1 B (fun x => (abs_le.mp ((hx x).2.2.2.1)).2)
      hp.2.2.2.2.2.2.2.1
  have hbound : (∫ x, Real.exp (2*ell*V x)-1 ∂q.tilted mB) ≤ 2*Real.exp (2*B-K) := by
    calc
      _ ≤ Real.exp (2*B)*(2*Real.exp (-K)) :=
        ht.2.trans (mul_le_mul_of_nonneg_left hv.2.2.2 (Real.exp_nonneg _))
      _ = _ := by
        rw [← mul_assoc, mul_comm (Real.exp (2*B)) 2, mul_assoc, ← Real.exp_add]
        congr 2
  have hpoint (x : E) : Real.exp (2*ell*|m x-mB x|)-1 ≤ Real.exp (2*ell*V x)-1 := by
    exact sub_le_sub_right (Real.exp_le_exp.mpr (mul_le_mul_of_nonneg_left (herr x) he)) 1
  have hEpos (x : E) : 0 ≤ Real.exp (2*ell*|m x-mB x|)-1 :=
    sub_nonneg.mpr (Real.one_le_exp_iff.mpr (mul_nonneg he (abs_nonneg _)))
  have hEi : Integrable (fun x => Real.exp (2*ell*|m x-mB x|)-1) (q.tilted mB) := by
    apply ht.1.mono' (by fun_prop)
    exact Filter.Eventually.of_forall (fun x => by
      simpa only [Real.norm_eq_abs, abs_of_nonneg (hEpos x)] using hpoint x)
  exact ⟨hm, hmB, hV, fun x => ⟨hv.2.1 x, herr x⟩, hv.2.2.1, hv.2.2.2,
    ht.1, hbound, hEi, (integral_mono hEi ht.1 hpoint).trans hbound⟩

end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ClippedMeanExponential

Exact module and namespace context

Scope and omitted-condition boundaries

  • This proves three exponential-minus-one integrability statements and their explicit bounds under the actual proposal and actual clipped tilt. ClippedGradientProgram already identifies qhat with the actual program output; this theorem does not repeat its pushforward equality. It does not assert normalized Radon-Nikodym power identities, a Renyi divergence bound, an ideal-target equality, a joint adaptive kernel, initialization or query cost. The factor 2 is retained and no logarithmic estimate is claimed. Neither full companion paper is complete.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

  • convexOn_exp.map_integral_le
  • MeasureTheory.integrable_prod_iff
  • MeasureTheory.integrable_withDensity_iff_integrable_smul'
  • MeasureTheory.integral_mono

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.