Actual bounded Poisson rejection output and full-batch cost
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PoissonRejection.poisson_rejection_output · theorem · Teaching coverage
Statement
Let Q be a Markov proposal kernel from a measurable parameter space S to a measurable space X, let nu be a fixed probability measure on auxiliary space A, and let W((s,x),z) be jointly measurable with |W|<=B for a fixed B>0. Fix a default x0. An attempt independently draws x from Q(s), N from Poisson(2B), an infinite iid nu sequence z, and U uniform on [0,1], and accepts when U is at most the product over i<N of (B+W((s,x),z_i))/(2B). Let Lambda_s be this actual product law, E_s its acceptance event, and p_s=Lambda_s(E_s). On an iid sequence of whole attempts, return the proposal at the first success, using x0 only on never-success, and charge N for every attempt whose predecessors all failed. There is a measurable Markov kernel R whose fiber is both the actual output law and Q(s) exponentially tilted by w(s,x)=integral W((s,x),z) nu(dz). Conditional acceptance is exp(w-B), the projected accepted submeasure is exp(w-B)Q(s), and p_s is its total mass with p_s>=exp(-2B). Never-success has measure zero; the first n attempts all fail with probability (1-p_s)^n. The expected total full-batch charge equals 2B/p_s and is at most 2B exp(2B).
All objects and hypotheses
- S, X and A are arbitrary measurable spaces; Q:S->X is a Markov kernel.
- nu is a fixed probability measure on A, and B is a fixed real number with B>0.
- W:((S times X) times A)->Real is jointly measurable and satisfies |W((s,x),z)|<=B for every s,x,z.
- A fixed x0 in X defines the output on the never-success event.
- Each attempt draws independently from the displayed proposal/Poisson/infinite auxiliary/uniform product. Each retry is an independent whole attempt. Cost is the full N estimator calls for every attempt reached.
Mathematical proof
1. Build the actual independent attempt
Use the product of the proposal law, Poisson law, auxiliary infinite product and unit-interval Lebesgue restriction. Infinite-product finite-coordinate pushforward identifies the first N auxiliary draws with the finite product law. Variable N is measurable by countable discrete stratification. The empty product at N=0 is one, so that branch accepts and makes zero estimator calls.
Corresponding Lean step
attemptLaw; iid_prefix_law; measurable_accepted
2. Compute conditional acceptance from the event
Every factor lies in [0,1], so integrating the actual event U<=product gives the product itself. Finite product integration gives t^n, where t=(B+w)/(2B). The Poisson generating series then gives exp(2B(t-1))=exp(w-B). Bounded measurability supplies the integrability needed for the real-to-nonnegative-integral conversions.
Corresponding Lean step
finite_uniform_acceptance; poisson_power_integral; actual_poisson_acceptance
3. Identify the accepted submeasure and its mass
For every measurable proposal event, restrict the whole attempt law to acceptance and project to the proposal. Fubini and conditional acceptance give the exact weighted submeasure. Since -B<=w<=B, its density lies between exp(-2B) and one. Thus its mass p is strictly positive and finite; positivity is derived, not assumed.
Corresponding Lean step
actual_accepted_proposal; bounded_estimator_mean; bounded_acceptance_mass; ha; hp
4. Prove real retries terminate and normalize the output
A failure prefix followed by an attempt in any measurable set F is an actual finite cylinder, with mass q^n Lambda(F), q=1-p. Taking F inside acceptance gives disjoint first-success events. Never-success is contained in every failure prefix and has mass zero because q^n tends to zero. The total firstOutput is measurable using measurable existence, Nat.find, and its explicit default branch. Summing the first-success events gives the normalized accepted proposal law.
Corresponding Lean step
first_hit_submeasure; never_hit_null; measurable_firstOutput; firstOutput_law
5. Construct a common Markov kernel and identify the target
Parameter integration makes w jointly measurable, and kernel integration makes p measurable. Construct Q.withDensity with the actual normalized density and verify unit mass in every fiber. This is a common measurable kernel, not merely separate fiberwise existence. Boundedness establishes exponential integrability, allowing the constant exp(-B) to cancel in the real normalization and identify the result with Q(s).tilted(w).
Corresponding Lean step
normalized_density_kernel; bounded_estimator_output_kernel; normalized_exp_tilt; hReq
6. Charge every full attempt, including the successful one
Define total charge as the sum of N_n multiplied by the indicator that all earlier attempts failed. The current count may correlate with current acceptance. The finite-cylinder identity instead gives the current attempt law restricted only by preceding failure as q^n Lambda. Tonelli therefore yields E C=(sum q^n) E N. The actual Poisson expectation is proved from its mass series, including rate zero, and product integration gives E N=2B for the full attempt law.
Corresponding Lean step
surviving_current_law; totalCost; expected_totalCost; poisson_nat_mean; attempt_count_mean
7. Derive the explicit finite expected cost
Invert the proved positive acceptance lower bound and multiply by the nonnegative per-attempt mean. This is a direct expectation calculation for the actual attempt stream and does not transfer unbounded costs through a distributional approximation.
Corresponding Lean step
hbound; hcost; ENNReal.inv_le_inv
Lean statement · poisson_rejection_output
Actual bounded Poisson rejection output, conditional and accepted laws, stopping, parameterized Markov kernel and full-batch expected 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_rejection_output {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) :
let Λ := fun s => attemptLaw (Q s) ν (⟨2 * B, by positivity⟩ : ℝ≥0)
let E := fun s => accepted (fun p : X × A => W ((s,p.1),p.2)) B
let ρ := fun s => Measure.infinitePi (fun _ : ℕ => Λ s)
let out := fun s => firstOutput (E s) Prod.fst x₀
∃ R : Kernel S X, IsMarkovKernel R ∧ ∀ s,
Measurable (out s) ∧ (ρ s).map (out s) = R s ∧
R s = (Q s).tilted (fun x => ∫ z, W ((s,x),z) ∂ν) ∧
(∀ x, ((poissonMeasure (⟨2 * B, by positivity⟩ : ℝ≥0)).prod
((Measure.infinitePi (fun _ : ℕ => ν)).prod unitUniform))
{p : ℕ × ((ℕ → A) × ℝ) |
p.2.2 ≤ ∏ i : Fin p.1, (B + W ((s,x),p.2.1 i.val)) / (2 * B)} =
ENNReal.ofReal (Real.exp ((∫ z, W ((s,x),z) ∂ν) - B))) ∧
((Λ s).restrict (E s)).map Prod.fst = (Q s).withDensity
(fun x => ENNReal.ofReal (Real.exp ((∫ z, W ((s,x),z) ∂ν) - B))) ∧
Λ s (E s) = (∫⁻ x, ENNReal.ofReal (Real.exp ((∫ z, W ((s,x),z) ∂ν) - B)) ∂Q s) ∧
ρ s {ω | ∀ n, ω n ∉ E s} = 0 ∧
(∀ n, ρ s {ω | ∀ i < n, ω i ∉ E s} = (1 - Λ s (E s))^n) ∧
ENNReal.ofReal (Real.exp (-2 * B)) ≤ Λ s (E s) ∧
(∫⁻ ω, totalCost (E s) (fun p => (p.2.1 : ℝ≥0∞)) ω ∂ρ s) =
(Λ s (E s))⁻¹ * ENNReal.ofReal (2 * B) ∧
(∫⁻ ω, totalCost (E s) (fun p => (p.2.1 : ℝ≥0∞)) ω ∂ρ s) ≤
ENNReal.ofReal (2 * B * Real.exp (2 * B))Lean proof · poisson_rejection_output
Actual product attempts; finite-prefix and uniform acceptance integration; Poisson generating series; first-hit cylinders and countable output decomposition; normalized density kernel; actual nonnegative accumulated 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_rejection_output {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) :
let Λ := fun s => attemptLaw (Q s) ν (⟨2 * B, by positivity⟩ : ℝ≥0)
let E := fun s => accepted (fun p : X × A => W ((s,p.1),p.2)) B
let ρ := fun s => Measure.infinitePi (fun _ : ℕ => Λ s)
let out := fun s => firstOutput (E s) Prod.fst x₀
∃ R : Kernel S X, IsMarkovKernel R ∧ ∀ s,
Measurable (out s) ∧ (ρ s).map (out s) = R s ∧
R s = (Q s).tilted (fun x => ∫ z, W ((s,x),z) ∂ν) ∧
(∀ x, ((poissonMeasure (⟨2 * B, by positivity⟩ : ℝ≥0)).prod
((Measure.infinitePi (fun _ : ℕ => ν)).prod unitUniform))
{p : ℕ × ((ℕ → A) × ℝ) |
p.2.2 ≤ ∏ i : Fin p.1, (B + W ((s,x),p.2.1 i.val)) / (2 * B)} =
ENNReal.ofReal (Real.exp ((∫ z, W ((s,x),z) ∂ν) - B))) ∧
((Λ s).restrict (E s)).map Prod.fst = (Q s).withDensity
(fun x => ENNReal.ofReal (Real.exp ((∫ z, W ((s,x),z) ∂ν) - B))) ∧
Λ s (E s) = (∫⁻ x, ENNReal.ofReal (Real.exp ((∫ z, W ((s,x),z) ∂ν) - B)) ∂Q s) ∧
ρ s {ω | ∀ n, ω n ∉ E s} = 0 ∧
(∀ n, ρ s {ω | ∀ i < n, ω i ∉ E s} = (1 - Λ s (E s))^n) ∧
ENNReal.ofReal (Real.exp (-2 * B)) ≤ Λ s (E s) ∧
(∫⁻ ω, totalCost (E s) (fun p => (p.2.1 : ℝ≥0∞)) ω ∂ρ s) =
(Λ s (E s))⁻¹ * ENNReal.ofReal (2 * B) ∧
(∫⁻ ω, totalCost (E s) (fun p => (p.2.1 : ℝ≥0∞)) ω ∂ρ s) ≤
ENNReal.ofReal (2 * B * Real.exp (2 * B)) := by
dsimp only
let r : ℝ≥0 := ⟨2 * B, by positivity⟩
let Λ := fun s => attemptLaw (Q s) ν r
let E := fun s => accepted (fun p : X × A => W ((s,p.1),p.2)) B
obtain ⟨R, hR, hReq⟩ := bounded_estimator_output_kernel Q ν W hW B hb
refine ⟨R, hR, ?_⟩
intro s
have hWs : Measurable (fun p : X × A => W ((s,p.1),p.2)) := hW.comp (by fun_prop)
have hE : MeasurableSet (E s) := measurable_accepted _ hWs B
have ha := actual_accepted_proposal (Q s) ν _ hWs B hB (hb s)
change ((Λ s).restrict (E s)).map Prod.fst =
(Q s).withDensity (fun x => ENNReal.ofReal (Real.exp ((∫ z, W ((s,x),z) ∂ν) - B))) at ha
have hp : Λ s (E s) =
∫⁻ x, ENNReal.ofReal (Real.exp ((∫ z, W ((s,x),z) ∂ν) - B)) ∂Q s := by
have ht := congrArg (fun μ : Measure X => μ Set.univ) ha
simpa [Measure.map_apply measurable_fst MeasurableSet.univ,
withDensity_apply, Λ, E, attemptLaw, accepted, r] using ht
have hbound := bounded_acceptance_mass (Q s)
(fun x => ∫ z, W ((s,x),z) ∂ν) B (fun x =>
(bounded_estimator_mean ν _ (hW.comp (by fun_prop)) B (hb s x)).2)
have hpos : 0 < Λ s (E s) := by
rw [hp]
exact lt_of_lt_of_le (ENNReal.ofReal_pos.mpr (Real.exp_pos _)) hbound.1
have hcost : (∫⁻ ω, totalCost (E s)
(fun p => (p.2.1 : ℝ≥0∞)) ω ∂Measure.infinitePi (fun _ : ℕ => Λ s)) =
(Λ s (E s))⁻¹ * ENNReal.ofReal (2 * B) := by
rw [expected_totalCost (Λ s) (E s) hE _ (by fun_prop),
attempt_count_mean]
congr 1
exact (ENNReal.ofReal_coe_nnreal (p := r)).symm
refine ⟨measurable_firstOutput _ hE _ measurable_fst x₀, ?_, ?_, ?_, ha, hp,
never_hit_null (Λ s) (E s) hE hpos, ?_, ?_, hcost, ?_⟩
· rw [firstOutput_law (Λ s) (E s) hE hpos _ measurable_fst x₀,
ha, hp, hReq s]
· rw [hReq s]
apply normalized_exp_tilt
· exact hWs.stronglyMeasurable.integral_prod_right'.measurable
· intro x
exact (bounded_estimator_mean ν _
(hW.comp (by fun_prop)) B (hb s x)).2.2
· intro x
exact actual_poisson_acceptance ν _ (hW.comp (by fun_prop)) B hB (hb s x)
· intro n
rw [failure_prefix_probability (Λ s) (E s) hE n,
prob_compl_eq_one_sub hE]
· rw [hp]
exact hbound.1
· rw [hcost]
calc
_ ≤ (ENNReal.ofReal (Real.exp (-2 * B)))⁻¹ * ENNReal.ofReal (2 * B) :=
mul_le_mul' (ENNReal.inv_le_inv.mpr (by rw [hp]; exact hbound.1)) le_rfl
_ = _ := by
rw [← ENNReal.ofReal_inv_of_pos (Real.exp_pos _),
← ENNReal.ofReal_mul (by positivity), ← Real.exp_neg]
congr 1
ring_nf
end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PoissonRejectionScope and omitted-condition boundaries
- Fixed B>0 and a fixed auxiliary probability law are explicit. W is jointly measurable and bounded everywhere by B. Cost counts full-batch auxiliary estimator calls, including the successful attempt; it is not automatically a gradient-query cost or the cost of an early-shortcircuit implementation. No clipping theorem, gradient-arc estimator, target log-weight identification, Renyi accuracy, initialization or complete FORS guarantee is established. The common output kernel is measurable in s and each output function is measurable in its attempt stream; joint measurability of the entire parameterized random-stream construction is not an additional public conclusion.
Source and reuse
ASTIS parents called
Mathlib API called (external library)
- MeasureTheory.Measure.infinitePi
- MeasureTheory.Measure.map_infinitePi_infinitePi_of_inj
- ProbabilityTheory.poissonMeasure
- ProbabilityTheory.integral_poissonMeasure
- MeasureTheory.integral_fintype_prod_eq_pow
- ProbabilityTheory.Kernel.withDensity
- MeasureTheory.Measure.tilted
- MeasureTheory.lintegral_tsum
Mathematical sources
- SPHMC v1 Appendix A.1, Lemma A.2 — The bounded Poisson acceptance mechanism underlying FORS.
- Poisson rejection mechanism, Algorithm 1 — Independent auxiliary draws and repeated acceptance; the present theorem assumes already bounded W.
ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.