ASTIS mathematical exposition

Actual terminal sampler accuracy and cached gradient costs

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.TerminalSamplerAccuracyCost.terminal_sampler_accuracy_cost · theorem · Teaching coverage

Statement

The output map is measurable and its rho-pushforward equals qhat; the never-accepted event has rho-measure zero. rho,qhat,pi are probability measures, and pi and qhat are mutually absolutely continuous. Both actual real RN ell-power functions are integrable under their denominator measures, and both integrals are strictly positive and at most 1+eps^2. Each explicit logarithmic RN moment divided by ell-1 is at most eps^2. The actual cached gradient count has expected value at most 1+2*exp(2). For every 0<p<=1/2, rho{G_cost>K_G*log(2/p)}<=p, where K_G=2*(exp(1)-1)*(exp(2)+1/log(2))+1+1/log(2). The cost expectation and tail are stated in extended nonnegative reals.

\[I_{\pi\|\widehat\pi}=\int\left(\frac{d\pi}{d\widehat\pi}\right)^\ell d\widehat\pi,\quad I_{\widehat\pi\|\pi}=\int\left(\frac{d\widehat\pi}{d\pi}\right)^\ell d\pi,\quad 0<I_{\cdot\|\cdot}\le1+\varepsilon^2,\quad \frac{\log I_{\cdot\|\cdot}}{\ell-1}\le\varepsilon^2,\quad \widehat\pi=\widehat q.\]

All objects and hypotheses

E is a finite-dimensional real inner-product Borel space with d=finrank(E)>0. f:E->R is differentiable everywhere and its actual gradient is globally beta-Lipschitz. eta,beta>0, ell>=2 and 0<eps<=1/2. Convexity is not used in this fixed smooth dependency.
Given x0 and supplied x_plus, cache g=grad f(x_plus) and set h=x0-eta*g. Assume norm(h-x_plus)<=sqrt(d*eta). Let L=ell+log(1/eps), and assume 64*beta*(sqrt(d*L)+L)<=1/eta. The reference-point construction and its cost are outside this fixed-call input contract.
Let P=(z->sqrt(eta)*z)_*stdGaussian(E), nu=Lebesgue restricted to (0,1] product P, and q=(z->h+sqrt(eta)*z)_*stdGaussian(E). For theta=pi*r/2 define W0(x,r,z)=<(pi/2)*(cos(theta)*(x-h)-sin(theta)*z),g-grad f(h+sin(theta)*(x-h)+cos(theta)*z)>. Set W=min(1,max(-1,W0)), m(x)=integral W(x,a) dnu(a), and qhat=q.tilted(m). First form G=(z->x0+sqrt(eta)*z)_*stdGaussian(E), then pi=G.tilted(-f). The mean m describes a law; the algorithm does not calculate that integral.
One attempt is (x,N,a,u), with independent laws q,Poisson(2),nu^Nat and uniform[0,1]. Accept when u<=product over i<N of (1+W(x,a_i))/2. The full attempt sequence has iid law rho. Output the x-coordinate of the least accepted index, or x0 if no index is accepted. C(omega) sums each batch size N_n whenever all earlier attempts failed, including the successful batch. The specified cached gradient count is G_cost=1+C: one initial evaluation of g and one new gradient evaluation in each W0 call. Random-number generation is not counted as a gradient query.

Mathematical proof

1. Convert the explicit source step condition to the parent parameter bounds

Let a=beta*eta and L=ell+log(1/eps). Positivity of eps and eps<=1/2 give L>=ell>=2. Multiply the inverse-step inequality by positive eta to obtain 64a(sqrt(dL)+L)<=1. Squaring and dropping only nonnegative cross terms gives 4096a^2(dL+L^2)<=1. Since ell<=L, this implies the existing 64-step condition at B=1. Its two separate terms also bound the two positive denominators defining K; no inequality is squared or divided before its sign is established.

\[64\beta^2(\ell d+\ell^2)\le\eta^{-2},\qquad K=\min\!\left\{\frac1{40\beta^2d\eta^2},\frac1{8\beta\eta}\right\}\ge8L.\]

Corresponding Lean step

scaled_parameters; parameter_bounds; Real.sq_sqrt

2. Turn the actual exponential comparison into the requested accuracy

The parent comparison has error 2 exp(2-K) at B=1. Write t=log eps<=0, so log(1/eps)=-t. The preceding K bound, ell>=2 and log2<=1 imply log2+2-K<=2t. Exponentiation and exp(log eps)=eps prove the desired eps-squared bound, retaining the factor2. Consume the actual ClippedRenyiComparison theorem, whose laws are the clipped output tilt and the Gaussian pushforward followed by the potential tilt.

\[2e^{2-K}=e^{\log2+2-K}\le e^{2\log\varepsilon}=\varepsilon^2,\qquad I_{\pi\|\widehat\pi},I_{\widehat\pi\|\pi}\le1+\varepsilon^2.\]

Corresponding Lean step

accuracy_error; terminal_sampler_accuracy_cost; AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ClippedRenyiComparison.clipped_renyi_comparison; Real.exp_log

3. Prove strict positivity before taking logarithms

For I(mu||nu), the actual reverse absolute continuity nu<<mu gives positivity of dmu/dnu nu-almost everywhere. Its nu-almost-everywhere finiteness is checked separately before conversion to real values. Every real power of a positive real is positive. Thus the support of the integrable RN-power function has the full probability mass of nu, proving I>0. Repeat with the two actual laws exchanged; no conclusion relies on toReal(infinity) or a totalized nonintegrable integral.

\[0<\frac{d\mu}{d\nu}<\infty\quad\nu\text{-a.e.},\qquad \nu\!\left(\operatorname{supp}((\operatorname{toReal}(d\mu/d\nu))^\ell)\right)=1,\qquad I_{\mu\|\nu}>0.\]

Corresponding Lean step

rn_moment_positive; MeasureTheory.Measure.rnDeriv_pos'; MeasureTheory.Measure.rnDeriv_ne_top; ENNReal.toReal_pos; MeasureTheory.integral_pos_iff_support_of_nonneg_ae

4. Obtain the explicit logarithmic RN-moment bound

For each positive actual moment I, apply log I<=I-1 and the previous moment upper bound. Since ell-1>=1 and eps^2>=0, division by the positive denominator yields log I/(ell-1)<=eps^2. The proof neither assumes a moment lower bound of one nor uses log at zero. These are the usual explicit expressions on this actual mutually absolutely continuous probability pair; a separate named divergence API is not claimed.

\[\log I\le I-1\le\varepsilon^2\le(\ell-1)\varepsilon^2,\qquad \frac{\log I}{\ell-1}\le\varepsilon^2.\]

Corresponding Lean step

logarithmic_accuracy; Real.log_le_sub_one_of_pos; terminal_sampler_accuracy_cost

5. Identify the actual cached-gradient probability program

Cache g once and use it both in the proposal center and in the actual arc estimator. Each attempt samples the proposal, Poisson count, independent auxiliary sequence and independent acceptance uniform. The product acceptance test uses only the first N auxiliary samples. The output is the first accepted proposal with a defined fallback. Match these concrete definitions with ClippedGradientProgram; its output measurability, exact pushforward and null never-accepted event transfer by definition equality. Product probability laws establish that the actual attempt sequence rho is a probability. No integral of m is performed by this algorithm.

\[\Lambda=q\otimes\operatorname{Poisson}(2)\otimes\nu^{\mathbb N}\otimes U_{[0,1]},\quad \rho=\Lambda^{\mathbb N},\quad \rho\circ\operatorname{out}^{-1}=q.\mathrm{tilted}(m)=\widehat\pi.\]

Corresponding Lean step

cachedEstimator; Attempt; attemptLaw; accepted; output; actual_program; AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ClippedGradientProgram.clipped_gradient_program

6. Charge the cached gradient and every consumed batch

The full-batch estimator cost includes the successful batch: a batch is charged precisely when all earlier attempts failed. Each estimator call uses the already cached g and one new gradient evaluation at its arc point. Under this stated execution convention G_cost=1+C. Apply the parent actual full-batch expected-cost bound at B=1. Nonnegative integration adds the initial unit charge using rho being a probability; there is no transport of an unbounded cost from a nearby law.

\[C(\omega)=\sum_{n\ge0}N_n\mathbf1\{\text{all }i<n\text{ failed}\},\quad G_{\rm cost}=1+C,\quad \mathbb E_\rho G_{\rm cost}\le1+2e^2.\]

Corresponding Lean step

queryCount; cached_expected_cost; actual_program; MeasureTheory.lintegral_add_left

7. Reuse the same-program tail and absorb the initial charge

Instantiate PoissonQueryTail with a constant proposal kernel at the fixed input and the same clipped estimator. Its attempt law, acceptance event and total cost are definitionally the ones above. This gives the estimator tail with K1=2(e-1)(e^2+1/log2)+1. Since log(2/p)>=log2>0, the extra initial unit is bounded by log(2/p)/log2. A pointwise event inclusion transfers the tail to G_cost with K_G=K1+1/log2. This does not assume independence between stopping time and batch size, and does not inherit the unchecked external tail-constant substitution.

\[\rho\{C>K_1\log(2/p)\}\le p,\quad \{1+C>(K_1+1/\log2)\log(2/p)\}\subseteq\{C>K_1\log(2/p)\}.\]

Corresponding Lean step

cached_cost_tail; actual_program; AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PoissonQueryTail.poisson_query_tail; ProbabilityTheory.Kernel.const

8. Return the actual fixed-call accuracy and cost contract

Assemble the actual output-law equality and probability/termination results with both RN-power integrability statements, strict moment positivity, two moment bounds, two logarithmic bounds, expected cached gradient cost and the universally quantified p-tail. These are eighteen public conjuncts. The internal K and step inequalities are proof dependencies, not extra public conclusions. The supplied-reference, positive-parameter and fixed-call scope stays explicit for the later recursive consumer.

\[\rho\{\text{never accepts}\}=0,\quad \frac{\log I_{\pi\|\widehat\pi}}{\ell-1},\frac{\log I_{\widehat\pi\|\pi}}{\ell-1}\le\varepsilon^2,\quad \rho\{G_{\rm cost}>K_G\log(2/p)\}\le p.\]

Corresponding Lean step

terminal_sampler_accuracy_cost; actual_program; logarithmic_accuracy

Lean statement · terminal_sampler_accuracy_cost

Eighteen actual output, probability, termination, RN L1/positivity/moment/log accuracy, expected cached gradient and universal p-tail conclusions.

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 terminal_sampler_accuracy_cost (f : E → ℝ) (hf : Differentiable ℝ f)
    (eta beta ell eps : ℝ) (heta : 0 < eta) (hb : 0 < beta)
    (he : 2 ≤ ell) (hep : 0 < eps) (heps : eps ≤ 1/2)
    (hd : 0 < (Module.finrank ℝ E : ℝ))
    (hlip : LipschitzWith ⟨beta,hb.le⟩ (gradient f)) (x0 xp : E)
    (hcenter : ‖(x0-eta • gradient f xp)-xp‖ ≤ Real.sqrt ((Module.finrank ℝ E : ℝ)*eta))
    (hstep : 64*beta*(Real.sqrt ((Module.finrank ℝ E : ℝ)*(ell+Real.log (1/eps)))+
      (ell+Real.log (1/eps))) ≤ 1/eta) :
    let g := gradient f xp
    let h := x0-eta • g
    let P := (stdGaussian E).map (fun z => Real.sqrt eta • z)
    let nu := (volume.restrict (Set.Ioc (0 : ℝ) 1)).prod P
    let q := (stdGaussian E).map (fun z => h+Real.sqrt eta • z)
    let W := fun p => min 1 (max (-1) (cachedEstimator f h g p))
    let m := fun x => ∫ z, W (x,z) ∂nu
    let rho := Measure.infinitePi (fun _ : ℕ => attemptLaw q nu 1 (by norm_num))
    let qhat := q.tilted m
    let pi := ((stdGaussian E).map (fun z => x0+Real.sqrt eta • z)).tilted (fun x => -f x)
    Measurable (output W 1 x0) ∧ rho.map (output W 1 x0) = qhat ∧
      rho {omega | ∀ n, omega n ∉ accepted W 1} = 0 ∧
      IsProbabilityMeasure rho ∧ IsProbabilityMeasure qhat ∧ IsProbabilityMeasure pi ∧
      pi ≪ qhat ∧ qhat ≪ pi ∧
      Integrable (fun x => (pi.rnDeriv qhat x).toReal^ell) qhat ∧
      Integrable (fun x => (qhat.rnDeriv pi x).toReal^ell) pi ∧
      0 < (∫ x, (pi.rnDeriv qhat x).toReal^ell ∂qhat) ∧
      0 < (∫ x, (qhat.rnDeriv pi x).toReal^ell ∂pi) ∧
      (∫ x, (pi.rnDeriv qhat x).toReal^ell ∂qhat) ≤ 1+eps^2 ∧
      (∫ x, (qhat.rnDeriv pi x).toReal^ell ∂pi) ≤ 1+eps^2 ∧
      Real.log (∫ x, (pi.rnDeriv qhat x).toReal^ell ∂qhat)/(ell-1) ≤ eps^2 ∧
      Real.log (∫ x, (qhat.rnDeriv pi x).toReal^ell ∂pi)/(ell-1) ≤ eps^2 ∧
      (∫⁻ omega, 1+queryCount W 1 omega ∂rho) ≤ ENNReal.ofReal (1+2*Real.exp 2) ∧
      ∀ p : ℝ, 0 < p → p ≤ 1/2 →
        rho {omega | ENNReal.ofReal
          ((2*(Real.exp 1-1)*(Real.exp 2+1/Real.log 2)+1+1/Real.log 2)*
            Real.log (2/p)) < 1+queryCount W 1 omega} ≤ ENNReal.ofReal p

Exact module and namespace context

Lean proof · terminal_sampler_accuracy_cost

Explicit parameter algebra, actual RN positivity before log, identical first-success probability program, actual cached count, and independently proved same-program Poisson tail.

theorem terminal_sampler_accuracy_cost (f : E → ℝ) (hf : Differentiable ℝ f)
    (eta beta ell eps : ℝ) (heta : 0 < eta) (hb : 0 < beta)
    (he : 2 ≤ ell) (hep : 0 < eps) (heps : eps ≤ 1/2)
    (hd : 0 < (Module.finrank ℝ E : ℝ))
    (hlip : LipschitzWith ⟨beta,hb.le⟩ (gradient f)) (x0 xp : E)
    (hcenter : ‖(x0-eta • gradient f xp)-xp‖ ≤ Real.sqrt ((Module.finrank ℝ E : ℝ)*eta))
    (hstep : 64*beta*(Real.sqrt ((Module.finrank ℝ E : ℝ)*(ell+Real.log (1/eps)))+
      (ell+Real.log (1/eps))) ≤ 1/eta) :
    let g := gradient f xp
    let h := x0-eta • g
    let P := (stdGaussian E).map (fun z => Real.sqrt eta • z)
    let nu := (volume.restrict (Set.Ioc (0 : ℝ) 1)).prod P
    let q := (stdGaussian E).map (fun z => h+Real.sqrt eta • z)
    let W := fun p => min 1 (max (-1) (cachedEstimator f h g p))
    let m := fun x => ∫ z, W (x,z) ∂nu
    let rho := Measure.infinitePi (fun _ : ℕ => attemptLaw q nu 1 (by norm_num))
    let qhat := q.tilted m
    let pi := ((stdGaussian E).map (fun z => x0+Real.sqrt eta • z)).tilted (fun x => -f x)
    Measurable (output W 1 x0) ∧ rho.map (output W 1 x0) = qhat ∧
      rho {omega | ∀ n, omega n ∉ accepted W 1} = 0 ∧
      IsProbabilityMeasure rho ∧ IsProbabilityMeasure qhat ∧ IsProbabilityMeasure pi ∧
      pi ≪ qhat ∧ qhat ≪ pi ∧
      Integrable (fun x => (pi.rnDeriv qhat x).toReal^ell) qhat ∧
      Integrable (fun x => (qhat.rnDeriv pi x).toReal^ell) pi ∧
      0 < (∫ x, (pi.rnDeriv qhat x).toReal^ell ∂qhat) ∧
      0 < (∫ x, (qhat.rnDeriv pi x).toReal^ell ∂pi) ∧
      (∫ x, (pi.rnDeriv qhat x).toReal^ell ∂qhat) ≤ 1+eps^2 ∧
      (∫ x, (qhat.rnDeriv pi x).toReal^ell ∂pi) ≤ 1+eps^2 ∧
      Real.log (∫ x, (pi.rnDeriv qhat x).toReal^ell ∂qhat)/(ell-1) ≤ eps^2 ∧
      Real.log (∫ x, (qhat.rnDeriv pi x).toReal^ell ∂pi)/(ell-1) ≤ eps^2 ∧
      (∫⁻ omega, 1+queryCount W 1 omega ∂rho) ≤ ENNReal.ofReal (1+2*Real.exp 2) ∧
      ∀ p : ℝ, 0 < p → p ≤ 1/2 →
        rho {omega | ENNReal.ofReal
          ((2*(Real.exp 1-1)*(Real.exp 2+1/Real.log 2)+1+1/Real.log 2)*
            Real.log (2/p)) < 1+queryCount W 1 omega} ≤ ENNReal.ofReal p := by
  let g := gradient f xp
  let h := x0-eta • g
  let P := (stdGaussian E).map (fun z => Real.sqrt eta • z)
  let nu := (volume.restrict (Set.Ioc (0 : ℝ) 1)).prod P
  let q := (stdGaussian E).map (fun z => h+Real.sqrt eta • z)
  let W := fun p => min 1 (max (-1) (cachedEstimator f h g p))
  let m := fun x => ∫ z, W (x,z) ∂nu
  let rho := Measure.infinitePi (fun _ : ℕ => attemptLaw q nu 1 (by norm_num))
  let qhat := q.tilted m
  let pi := ((stdGaussian E).map (fun z => x0+Real.sqrt eta • z)).tilted (fun x => -f x)
  let K := min (1/(40*beta^2*(Module.finrank ℝ E : ℝ)*eta^2)) (1/(8*beta*eta))
  obtain ⟨hs,hK⟩ := parameter_bounds eta beta _ ell eps heta hb hd he hep heps hstep
  have herr := accuracy_error ell eps K he hep heps hK
  have hc := AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ClippedRenyiComparison.clipped_renyi_comparison
    f hf eta beta 1 ell heta hb (by norm_num) he hd hlip x0 xp hcenter
    (by simpa only [div_one] using hs)
  rcases hc with ⟨hpi,hqh,hpq,hqp,hfi,hri,hfb,hrb,_,_⟩
  have : IsProbabilityMeasure pi := hpi
  have : IsProbabilityMeasure qhat := hqh
  have hfi' : Integrable (fun x => (pi.rnDeriv qhat x).toReal^ell) qhat := hfi
  have hri' : Integrable (fun x => (qhat.rnDeriv pi x).toReal^ell) pi := hri
  have hfb' : (∫ x, (pi.rnDeriv qhat x).toReal^ell ∂qhat)-1 ≤ 2*Real.exp (2-K) := by
    change (∫ x, (pi.rnDeriv qhat x).toReal^ell ∂qhat)-1 ≤
      2*Real.exp (2*1-min (1^2/(40*beta^2*(Module.finrank ℝ E : ℝ)*eta^2)) (1/(8*beta*eta))) at hfb
    simpa only [one_pow,mul_one] using hfb
  have hrb' : (∫ x, (qhat.rnDeriv pi x).toReal^ell ∂pi)-1 ≤ 2*Real.exp (2-K) := by
    change (∫ x, (qhat.rnDeriv pi x).toReal^ell ∂pi)-1 ≤
      2*Real.exp (2*1-min (1^2/(40*beta^2*(Module.finrank ℝ E : ℝ)*eta^2)) (1/(8*beta*eta))) at hrb
    simpa only [one_pow,mul_one] using hrb
  have hfbound : (∫ x, (pi.rnDeriv qhat x).toReal^ell ∂qhat) ≤ 1+eps^2 := by linarith
  have hrbound : (∫ x, (qhat.rnDeriv pi x).toReal^ell ∂pi) ≤ 1+eps^2 := by linarith
  obtain ⟨hfp,hfl⟩ := logarithmic_accuracy pi qhat hqp ell eps he hfi' hfbound
  obtain ⟨hrp,hrl⟩ := logarithmic_accuracy qhat pi hpq ell eps he hri' hrbound
  obtain ⟨hprob,ho,hlaw,hnever,hcost,htail⟩ := actual_program f hf eta beta heta hb hlip x0 xp
  exact ⟨ho,hlaw,hnever,hprob,hqh,hpi,hpq,hqp,hfi',hri',hfp,hrp,hfbound,hrbound,hfl,hrl,hcost,htail⟩

end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.TerminalSamplerAccuracyCost

Exact module and namespace context

Scope and omitted-condition boundaries

Eighteen public conjuncts bind the actual first-success probability program to both accuracy directions and the specified cached gradient count. This is a probability program with an explicit cost random variable, not a formally verified compiler, evaluator or hardware trace. The supplied reference point is not constructed and finding it is not charged; its one cached gradient evaluation is charged. Positive beta and dimension are retained; zero-beta/zero-dimensional cases remain separate. The explicit logarithmic RN expressions are proved, but no complete named Renyi API is asserted. The chosen denominator-measure powers follow B.12/D.1 despite inconsistent printed B.7/section1.3 notation. The below-order-two B.12 intermediate proof gap and the external tail proof final constant substitution are not silently imported or claimed repaired. The tail uses the independently proved local PoissonQueryTail on the same actual law/event/cost. No joint input-parameter kernel, outer recursion, initialization construction, PBPS composition or complete paper result is asserted; no unbounded cost is transferred by TV or Renyi closeness.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

MeasureTheory.Measure.rnDeriv_pos'
MeasureTheory.Measure.rnDeriv_ne_top
MeasureTheory.integral_pos_iff_support_of_nonneg_ae
Real.log_le_sub_one_of_pos
MeasureTheory.lintegral_add_left

Mathematical sources

SPHMC Theorem A.4(2) — Fixed-call terminal sampler accuracy and gradient cost; supplied reference.
Smooth D.1, B.12 and Appendix C — Actual smooth estimator and normalized comparison; source discrepancies disclosed.

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