Actual Poisson rejection query tails with explicit constants

Mathematical statement

Under the displayed measurable bounded-estimator experiment, the actual full-batch query count satisfies P(C>2B(e-1)m+L)≤delta and P(C>K(B)L)≤delta, where K(B)=2B(e-1)(exp(2B)+1/log(2))+1. Acceptance probability is derived from the actual parent program and is not an extra hypothesis. The first inequality retains the integer ceiling; the second is an explicit single-log bound for fixed B. Both hold for every B>0, including arbitrarily small B, and every 0<delta<1.

theorem poisson_query_tail {S X A : Type*}
    [MeasurableSpace S] [MeasurableSpace X] [MeasurableSpace A]
    (Q : Kernel S X) [IsMarkovKernel Q] (ν : Measure A) [IsProbabilityMeasure ν]
    (W : (S × X) × A → ℝ) (hW : Measurable W)
    (B : ℝ) (hB : 0 < B) (hb : ∀ s x z, |W ((s,x),z)| ≤ B) (x₀ : X)
    (s : S) (δ : ℝ) (hδ : 0 < δ) (hδ1 : δ < 1) :
    let Λ := attemptLaw (Q s) ν (⟨2 * B, by positivity⟩ : ℝ≥0)
    let E := accepted (fun p : X × A => W ((s,p.1),p.2)) B
    let ρ := Measure.infinitePi (fun _ : ℕ => Λ)
    let C := totalCost E (fun p => (p.2.1 : ℝ≥0∞))
    let L := Real.log (2 / δ)
    let m := ⌈Real.exp (2 * B) * L⌉₊
    ρ {ω | ENNReal.ofReal (2 * B * (Real.exp 1 - 1) * m + L) < C ω} ≤ ENNReal.ofReal δ ∧
    ρ {ω | ENNReal.ofReal
      ((2 * B * (Real.exp 1 - 1) * (Real.exp (2 * B) + 1 / Real.log 2) + 1) * L) < C ω}
        ≤ ENNReal.ofReal δ

Proof roadmap

1. 1Use the same actual program and its proved acceptance probability

   The existing production theorem supplies p_s≥exp(-2B) for the actual acceptance event under the actual four-coordinate attempt law. Definitional equality aligns both definitions. Mapping the attempt to its N coordinate gives Poisson(2B); measurability follows from product coordinates and finite products on each discrete N stratum.

2. 2Compare the stopped cost to a deterministic prefix on each path

   If any attempt j<m succeeds, every charged term at index n≥m vanishes because the earlier-success predicate is false. Therefore C is at most S_m=sum_{n<m}N_n on this event. A large stopped cost thus requires either all m attempts to fail or a large fixed-prefix sum. This comparison uses no stopping-time/count independence.

3. 3Integrate the actual Poisson exponential moment

   First prove integrability of exp(N) using the convergent exponential series weighted by the Poisson mass. The true count law then gives E exp(N)=exp(2B(e-1)). The finite-coordinate pushforward of the iid stream is the finite product measure, so product integration gives E exp(S_m)=exp(2Bm(e-1)).

4. 4Apply exponential Markov to the fixed prefix

   Exponentiation sends S_m>2Bm(e-1)+L into an event where exp(S_m) exceeds the corresponding positive threshold. Markov and the exact exponential moment cancel the Poisson contribution, leaving exp(-L). All conversions to extended nonnegative integrals have integrability or positivity witnesses.

5. 5Budget the probability of all preceding failures

   The actual iid cylinder law gives failure probability (1-p_s)^m. For a=exp(-2B), the inequality 1-p_s≤exp(-a) follows from p_s≥a and 1-a≤exp(-a). The ceiling choice ensures a*m≥L. The failure term is therefore at most exp(-L). Probability finiteness is established before taking real parts.

6. 6Combine both events at the requested failure tolerance

   The union bound gives at most 2exp(-L). With L=log(2/delta), this equals delta. The nonnegative total cost is left as its full infinite sum, so the bound covers all paths, including any never-success path; it is not a theorem only about attempt counts.

7. 7Expose the single-log coefficient and its dependence on B

   Because 0<delta<1, L≥log(2)>0. Thus m≤exp(2B)L+1≤(exp(2B)+1/log(2))L. The resulting larger threshold K(B)L has a smaller exceedance event. K depends on B: converting this to a universal terminal gradient-cost statement still needs a uniform B bound and the concrete per-estimator gradient cost.