Actual clipped-gradient Poisson retry program

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ClippedGradientProgram.clipped_gradient_program · theorem · Teaching coverage

Statement

The actual nu and q are probability measures. W and Wc are jointly measurable in (x,r,z), and m is measurable. For every x, W(x,.) and Wc(x,.) and the excess max(abs(W(x,.))-B,0) are nu-integrable; abs(m(x))<=B and abs(m(x)-(<g,x>-f(x)+C))<=integral max(abs(W(x,a))-B,0) dnu(a). The function exp(m) is q-integrable and exp(-B)<=Z<=exp(B). The first-success output is measurable and its actual rho-pushforward equals q.tilted(m). The never-success event has rho-measure zero. With p_acc=Lambda(accepted), p_acc=ofReal(exp(-B)*Z)>=ofReal(exp(-2B)); the extended-nonnegative expectation of Q is p_acc^(-1)*ofReal(2B), and is at most ofReal(2B*exp(2B)).

All objects and hypotheses

• E is a finite-dimensional real inner-product space with Borel sigma-algebra and explicit second countability. f:E->R is differentiable everywhere and its actual gradient is globally beta-Lipschitz. Fix eta>0, beta>=0, B>0 and x0,x_plus in E. No convexity, positive dimension, center residual or small-step condition is needed for this selected clipped-program result.
• Set g=grad f(x_plus), h=x0-eta*g, P=(z->sqrt(eta) z)_*stdGaussian(E), U=Lebesgue restricted to (0,1], nu=U product P, and q=(z->h+sqrt(eta) z)_*stdGaussian(E). Before choosing x define C=integral f(h+z) dP(z)-<g,h>. The parent mean theorem proves integrability underlying this C.
• For x in E, r in R and z in E, theta=pi*r/2, gamma=h+sin(theta)(x-h)+cos(theta)z, v=(pi/2)(cos(theta)(x-h)-sin(theta)z), W(x,(r,z))=<v,g-grad f(gamma)>. Define Wc=min(B,max(-B,W)), m(x)=integral Wc(x,a) dnu(a), and Z=integral exp(m(x)) dq(x).
• An attempt is p=(x,N,(a_stream,u)), with law Lambda=q product [Poisson(2B) product (nu^N product Uniform[0,1])]; nu^N denotes the infinite iid auxiliary sequence indexed by natural numbers. All these factors are independent. Accept p when u<=product over i<N of (B+Wc(x,a_i))/(2B). The auxiliary time r inside a_i and acceptance uniform u are distinct random inputs.
• Let rho=Lambda^N be the infinite iid sequence of attempts. Output the proposal of the first accepted attempt, using the least natural index; if no attempt succeeds return x0. Define Q(omega)=sum over n>=0 of N_n times the indicator that every i<n failed. This counts all estimator calls in the successful batch as well as failed batches.

Mathematical proof

theorem clipped_gradient_program (f : E → ℝ) (hf : Differentiable ℝ f)
    (eta beta B : ℝ) (heta : 0 < eta) (hbeta : 0 ≤ beta) (hB : 0 < B)
    (hlip : LipschitzWith ⟨beta,hbeta⟩ (gradient f)) (x0 xp : E) :
    let h := x0 - eta • gradient f xp
    let P := (stdGaussian E).map (fun z => Real.sqrt eta • z)
    let U := volume.restrict (Set.Ioc (0 : ℝ) 1)
    let ν := U.prod P
    let q := (stdGaussian E).map (fun z => h + Real.sqrt eta • z)
    let C := (∫ z, f (h+z) ∂P) - inner ℝ (gradient f xp) h
    let W := estimator f h xp
    let Wc := fun p => clip B (W p)
    let m := fun x => ∫ z, Wc (x,z) ∂ν
    let Z := ∫ x, Real.exp (m x) ∂q
    let Λ := attempts q ν B hB
    let ρ := Measure.infinitePi (fun _ : ℕ => Λ)
    IsProbabilityMeasure ν ∧ IsProbabilityMeasure q ∧
      Measurable W ∧ Measurable Wc ∧ Measurable m ∧
      (∀ x, Integrable (fun z => W (x,z)) ν ∧
        Integrable (fun z => Wc (x,z)) ν ∧
        Integrable (fun z => max (|W (x,z)|-B) 0) ν ∧ |m x| ≤ B ∧
        |m x - (inner ℝ (gradient f xp) x - f x + C)| ≤
          ∫ z, max (|W (x,z)|-B) 0 ∂ν) ∧
      Integrable (fun x => Real.exp (m x)) q ∧
      Real.exp (-B) ≤ Z ∧ Z ≤ Real.exp B ∧
      Measurable (output Wc B x0) ∧ ρ.map (output Wc B x0) = q.tilted m ∧
      ρ {ω | ∀ n, ω n ∉ accepted Wc B} = 0 ∧
      Λ (accepted Wc B) = ENNReal.ofReal (Real.exp (-B)*Z) ∧
      ENNReal.ofReal (Real.exp (-2*B)) ≤ Λ (accepted Wc B) ∧
      (∫⁻ ω, queryCount Wc B ω ∂ρ) =
        (ENNReal.ofReal (Real.exp (-B)*Z))⁻¹ * ENNReal.ofReal (2*B) ∧
      (∫⁻ ω, queryCount Wc B ω ∂ρ) ≤ ENNReal.ofReal (2*B*Real.exp (2*B))

theorem clipped_gradient_program (f : E → ℝ) (hf : Differentiable ℝ f)
    (eta beta B : ℝ) (heta : 0 < eta) (hbeta : 0 ≤ beta) (hB : 0 < B)
    (hlip : LipschitzWith ⟨beta,hbeta⟩ (gradient f)) (x0 xp : E) :
    let h := x0 - eta • gradient f xp
    let P := (stdGaussian E).map (fun z => Real.sqrt eta • z)
    let U := volume.restrict (Set.Ioc (0 : ℝ) 1)
    let ν := U.prod P
    let q := (stdGaussian E).map (fun z => h + Real.sqrt eta • z)
    let C := (∫ z, f (h+z) ∂P) - inner ℝ (gradient f xp) h
    let W := estimator f h xp
    let Wc := fun p => clip B (W p)
    let m := fun x => ∫ z, Wc (x,z) ∂ν
    let Z := ∫ x, Real.exp (m x) ∂q
    let Λ := attempts q ν B hB
    let ρ := Measure.infinitePi (fun _ : ℕ => Λ)
    IsProbabilityMeasure ν ∧ IsProbabilityMeasure q ∧
      Measurable W ∧ Measurable Wc ∧ Measurable m ∧
      (∀ x, Integrable (fun z => W (x,z)) ν ∧
        Integrable (fun z => Wc (x,z)) ν ∧
        Integrable (fun z => max (|W (x,z)|-B) 0) ν ∧ |m x| ≤ B ∧
        |m x - (inner ℝ (gradient f xp) x - f x + C)| ≤
          ∫ z, max (|W (x,z)|-B) 0 ∂ν) ∧
      Integrable (fun x => Real.exp (m x)) q ∧
      Real.exp (-B) ≤ Z ∧ Z ≤ Real.exp B ∧
      Measurable (output Wc B x0) ∧ ρ.map (output Wc B x0) = q.tilted m ∧
      ρ {ω | ∀ n, ω n ∉ accepted Wc B} = 0 ∧
      Λ (accepted Wc B) = ENNReal.ofReal (Real.exp (-B)*Z) ∧
      ENNReal.ofReal (Real.exp (-2*B)) ≤ Λ (accepted Wc B) ∧
      (∫⁻ ω, queryCount Wc B ω ∂ρ) =
        (ENNReal.ofReal (Real.exp (-B)*Z))⁻¹ * ENNReal.ofReal (2*B) ∧
      (∫⁻ ω, queryCount Wc B ω ∂ρ) ≤ ENNReal.ofReal (2*B*Real.exp (2*B)) := by
  dsimp only
  let h := x0 - eta • gradient f xp
  let P := (stdGaussian E).map (fun z => Real.sqrt eta • z)
  let ν := (volume.restrict (Set.Ioc (0 : ℝ) 1)).prod P
  let q := (stdGaussian E).map (fun z => h + Real.sqrt eta • z)
  let W := estimator f h xp
  let Wc := fun p => clip B (W p)
  obtain ⟨hν, hw, hc, hm, hx⟩ := actual_clipped_input f hf eta beta B heta hbeta hB hlip x0 xp
  let : IsProbabilityMeasure ν := hν
  have hq : Measurable (fun z : E => h + Real.sqrt eta • z) := by fun_prop
  let : IsProbabilityMeasure q := Measure.isProbabilityMeasure_map hq.aemeasurable
  obtain ⟨hi, hzlow, hzup⟩ := clipped_normalizer q _ hm B (fun x => (hx x).2.2.2.1)
  have hr := actual_retry q ν Wc hc B hB (fun x z => clip_bounds B (W (x,z)) hB.le) x0
  exact ⟨hν, inferInstance, hw, hc, hm, hx, hi, hzlow, hzup, hr⟩

end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ClippedGradientProgram

Scope and omitted-condition boundaries

• This is a fixed-parameter actual clipped program, including its true-input estimator count. Coordinate-free spaces, zero dimension and beta=0 are disclosed extensions. The output law is the normalized clipped tilt; the ideal Gibbs/RGO law, positive finite ideal normalization, normalized Renyi accuracy, adaptive eta/x0/x_plus kernel and initialization remain separate. Potential L1 for C is supplied by the parent proof, not separately returned as a public conjunct here. No separate RN bound is asserted. Cost counts complete batches of estimator calls, including success; reference-gradient preparation, full gradient-oracle accounting and random-number cost are not proved. An arbitrary B>0 bound 2B exp(2B) is not a uniform constant-cost theorem; source parameter and accuracy conditions are still required. Neither companion paper is complete.