Actual clipped-gradient Poisson retry program

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

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

Proof roadmap

1. 1Use the source center and actual independent inputs

   Substitute h=x0-eta grad f(x_plus) in the already proved path-mean theorem. Its constant C is fixed before every x. Continuity of the actual gradient and the explicit sine/cosine path proves measurability jointly in x and both auxiliary variables. Clipping is a continuous min/max operation. The scaled and translated Gaussian pushforwards and uniform-time product are genuine probability laws.

2. 2Prove the exact clipping loss before integrating

   Split a real estimator value into the three regions below -B, within [-B,B], and above B. The resulting identities give both the everywhere bound on the clipped value and the exact positive-excess loss. These are pointwise real inequalities, independent of any probability approximation.

3. 3Control the actual mean by an integrable excess

   Bound the measurable clipped estimator by the integrable constant B. The parent gives actual unclipped L1. Hence their difference and its absolute value are integrable, and the exact clipping identity proves excess integrability. Only then subtract their integrals and apply the absolute-integral inequality. Integrating -B≤Wc≤B proves the mean bound. Substituting the parent identity retains the same C.

4. 4Normalize the clipped law with proved bounds

   Measurable parameter integration makes m measurable. Its bound implies exp(-B)≤exp(m(x))≤exp(B). The upper constant is integrable under actual probability q, so exp(m) is integrable. Integrating the two pointwise bounds establishes a strictly positive finite Z. This argument normalizes only the clipped target; it uses no unproved exponential-integrability assumption for the ideal potential.

5. 5Identify the same actual first-success program

   Instantiate the established Poisson rejection theorem with the constant proposal kernel q and the actual clipped W. Expand the attempt, acceptance, first-output and cost definitions and check definitional equality with the parent program. Each attempt draws independent proposal, Poisson count, auxiliary stream and acceptance uniform. The first-success output uses the least accepted index and the explicit null-event default x0. The inherited law identifies the actual pushforward as the clipped exponential tilt, rather than merely constructing an abstract comparison law.

6. 6Compute acceptance using the finite clipped normalizer

   The actual parent program gives acceptance mass as the integral of exp(m-B). Its integrability follows from that of exp(m). Nonnegativity justifies converting the real integral to the extended-nonnegative integral; constant factor extraction then gives exp(-B)Z. The same-program lower acceptance bound is exp(-2B).

7. 7Charge the successful batch under the actual input law

   At index n, charge its full Poisson count whenever all earlier attempts failed; current acceptance is not assumed independent of that count. The parent theorem already proves the resulting stopped-sum expectation for these iid attempts. Substitute the actual acceptance mass. The bound uses its positive lower bound and remains attached to rho throughout. This is an estimator-call count; translating it into complete oracle accounting and a uniform constant bound requires later work.