Actual Poisson rejection query tails with explicit constants
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PoissonQueryTail.poisson_query_tail · theorem · Teaching coverage
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.
All objects and hypotheses
- S, X and A are arbitrary measurable spaces. Q:S->X is a Markov kernel and nu is a fixed probability law on A.
- B>0 is fixed across parameters. W:((S times X) times A)->Real is jointly measurable and |W((s,x),z)|<=B for every s,x,z.
- A default x0:X is supplied for the parent output construction; the cost bound does not depend on its value.
- At each parameter s an attempt independently draws x~Q(s), N~Poisson(2B), an infinite iid auxiliary sequence z~nu^ℕ, of which only the first N entries are read, and U~Uniform[0,1]. It accepts when U<=product_{i<N}(B+W((s,x),z_i))/(2B). Whole attempts are iid.
- C is the extended nonnegative sum of N_n over all attempts n whose preceding attempts failed, including the first successful batch. On never-success it is the sum over every batch.
- For every parameter s and failure tolerance 0<delta<1, set L=log(2/delta) and m=ceil(exp(2B)L).
Mathematical proof
1. Use 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.
Corresponding Lean step
poisson_rejection_output; actual_attempt_count_law; measurable_accepted
2. Compare 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.
Corresponding Lean step
totalCost_le_prefix; cost_tail_subset
3. Integrate 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)).
Corresponding Lean step
poisson_exponential_integrable; poisson_exponential_moment; fixed_prefix_exponential_moment
4. Apply 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.
Corresponding Lean step
fixed_prefix_chernoff; fixed_prefix_chernoff_shift
5. Budget 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.
Corresponding Lean step
failure_power_exponential_bound; poisson_tail_budget
6. Combine 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.
Corresponding Lean step
full_batch_cost_tail; full_batch_cost_tail_of_budget; delta_log_budget; full_batch_cost_delta_tail
7. Expose 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.
Corresponding Lean step
ceil_threshold_le_single_log; measure_mono
Lean statement · poisson_query_tail
Two explicit high-probability bounds for the same actual full-batch Poisson rejection cost.
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 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 δLean proof · poisson_query_tail
Actual parent acceptance bound, coordinate law, pathwise prefix truncation, Poisson exponential series, iid product moment, exponential Markov, failure budget and ceiling comparison.
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 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 δ := by
dsimp only
let r : ℝ≥0 := ⟨2 * B, by positivity⟩
let Λ := attemptLaw (Q s) ν r
let E := accepted (fun p : X × A => W ((s,p.1),p.2)) B
have hE : MeasurableSet E := measurable_accepted _ (hW.comp (by fun_prop)) B
have hlaw : Λ.map (fun p => p.2.1) = poissonMeasure r :=
actual_attempt_count_law (Q s) ν r
obtain ⟨R, hR, hs⟩ :=
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PoissonRejection.poisson_rejection_output
Q ν W hW B hB hb x₀
obtain ⟨_, _, _, _, _, _, _, _, haccept, _, _⟩ := hs s
change ENNReal.ofReal (Real.exp (-2 * B)) ≤ Λ E at haccept
have ht := full_batch_cost_delta_tail Λ E hE
(fun p => p.2.1) (by fun_prop) B hB hlaw haccept δ hδ hδ1
refine ⟨ht, ?_⟩
have hlog : Real.log 2 ≤ Real.log (2 / δ) := by
apply Real.log_le_log (by norm_num)
apply (le_div_iff₀ hδ).2
linarith
have hc := ceil_threshold_le_single_log B (Real.log (2 / δ)) hB.le hlog
refine (measure_mono (fun ω hω => ?_)).trans ht
exact lt_of_le_of_lt (ENNReal.ofReal_le_ofReal hc) hω
end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PoissonQueryTailScope and omitted-condition boundaries
- Counts full-batch estimator evaluations, including the successful batch, not automatically gradient queries or wall-clock time. A universal terminal-state constant requires uniform control of B and a separate cost account for each estimator call and other work. Actual clipped gradient estimators, target log-weight identification, Renyi error, reference points and initialization remain separate. This independently derived supporting inequality does not assert or silently repair the unrestricted printed 3B exp(2B) log(2/delta) threshold in external Theorem 2.3.
Source and reuse
ASTIS parents called
Mathlib API called (external library)
- MeasureTheory.Measure.infinitePi
- ProbabilityTheory.poissonMeasure
- MeasureTheory.meas_ge_le_lintegral_div
- MeasureTheory.integral_fintype_prod_eq_pow
- Nat.le_ceil
- Nat.ceil_lt_add_one
Mathematical sources
- SPHMC v1 Appendix A.1 and Theorem A.4(2) — Bounded rejection mechanism and the terminal routine consumer requiring a single-log cost tail; the present supporting bound is an independent ASTIS derivation.
- Poisson rejection Algorithm 1 and Theorem 2.3 — Actual full Poisson batches. The unrestricted printed tail formula is not asserted here; its small-B discrepancy remains explicit.
ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.