Actual bounded Poisson rejection output and full-batch cost

Fan Chen, Sinho Chewi, Jianfeng Lu and Matthew S. Zhang; ASTIS expanded bounded mechanism with explicit parameterization, default output and full-batch cost proof. No author endorsement implied.

Complete source statement (Samplinglib restatement)

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

Actual bounded rejection output and full-batch cost

Read the formalized proofs

Each statement and proof below has its own closed Lean disclosure. Samplinglib parents, Mathlib calls and external mathematical sources are distinguished in each proof.

Samplinglib mathematical lesson

Actual bounded Poisson rejection output and full-batch cost

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PoissonRejection.poisson_rejection_output · theorem · Teaching coverage

Read this first

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

\[R(s)=Q(s)^{w(s,\cdot)}=\mathcal L(\mathrm{out}_s),\quad p_s=\int e^{w(s,x)-B}Q(s)(dx)\ge e^{-2B},\quad\mathbb E C_s=\frac{2B}{p_s}\le2B e^{2B}.\]

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.

Download module (.lean)

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

Exact module and namespace context

Proof roadmap

1Build 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.
2Compute 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.
3Identify 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.
4Prove 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.
5Construct 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).
6Charge 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.
7Derive 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.

Full assumptions and notation

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.

\[\Lambda_s=Q(s)\otimes\operatorname{Poisson}(2B)\otimes\nu^{\mathbb N}\otimes\operatorname{Unif}[0,1].\]

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.

\[\mathbb P(E_s\mid x)=\sum_{n\ge0}\mathbb P(N=n)\left(\frac{B+w(s,x)}{2B}\right)^n=e^{w(s,x)-B}.\]

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.

\[(\pi_X)_*(\Lambda_s|_{E_s})=e^{w(s,\cdot)-B}Q(s),\qquad e^{-2B}\le p_s=\int e^{w(s,x)-B}Q(s)(dx)\le1.\]

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.

\[\mathbb P(\text{first }n\text{ fail})=(1-p_s)^n,\qquad\mathcal L(\mathrm{out}_s)=p_s^{-1}(\pi_X)_*(\Lambda_s|_{E_s}).\]

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

\[R(s,dx)=\frac{e^{w(s,x)-B}}{p_s}Q(s)(dx)=\frac{e^{w(s,x)}}{\int e^{w(s,y)}Q(s)(dy)}Q(s)(dx).\]

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.

\[C=\sum_{n\ge0}\mathbf1_{\{\text{attempts }i<n\text{ fail}\}}N_n,\qquad\mathbb E C=\frac{\mathbb E N}{p_s}=\frac{2B}{p_s}.\]

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.

\[\mathbb E C=2B/p_s\le2B e^{2B}.\]

Corresponding Lean step

hbound; hcost; ENNReal.inv_le_inv

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

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.

Download module (.lean)

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.PoissonRejection

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
The bounded mechanism is stated for a proposal distribution and auxiliary estimator.	A measurable Markov family Q(s) and jointly measurable W((s,x),z), on arbitrary measurable spaces with fixed auxiliary probability law.	generalization	A common parameterized output kernel is proved; parameterization is not attributed as an additional explicit statement of Lemma A.2.
B>0 bounds every estimator realization between -B and B.	Fixed B>0 and \|W\|<=B everywhere.	same	These hypotheses establish factor probabilities and uniform positive acceptance; no clipping step is silently substituted.
Poisson(2B) independent auxiliary samples and a product acceptance probability.	Actual independent proposal, Poisson count, infinite iid auxiliary law, and unit-interval uniform law; only the first N auxiliary coordinates are read.	same	Finite-prefix pushforward and uniform acceptance integration prove the correspondence, including N=0.
Repeat attempts until acceptance.	Actual iid whole-attempt stream and measurable total first-success output with default x0; never-success has measure zero and failure prefixes have probability (1-p)^n.	mathematically-necessary	Explicit default makes a total function; a proved null event removes its effect on the output distribution.
Output density is proportional to exp(mean W) relative to Q, with acceptance at least exp(-2B).	Conditional acceptance, accepted submeasure, exact p and lower bound are public, and the actual output law equals Q.tilted(mean W).	same	Exponential integrability and positive normalization are proved, including the common measurable Markov kernel.
The mechanism repeatedly draws a full Poisson batch of estimators.	Expected full-batch estimator-call count, including the successful batch, equals 2B/p and is at most 2B exp(2B).	source-implicit	The exact expectation is an expanded proof from the actual experiment, not a gradient-cost or shortcircuit-cost claim. Current N is not assumed independent of current acceptance.
Full FORS accuracy and the paper main results require concrete clipped gradient estimators and target/error/initialization conditions.	Those subsequent estimator, clipping, target-identification, Renyi, initialization and gradient-cost obligations are not claimed by this bounded mechanism.	API-limitation	The result is a concrete prerequisite for FORS, not completion of the terminal sampler or either paper main theorem.

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.

Encoder–denoiser: accepted · domain-mismatch

Detected semantic differences

domains: Common measurable Markov family extends the fixed-proposal presentation; fixed auxiliary representation explicit. — Independent reviewer accepted corresponding publication delta 1.
assumptions: Fixed positive B and everywhere bounded W preserve the mechanism. — Independent reviewer accepted corresponding publication delta 2.
objects: Infinite iid randomness supplies exactly the finite auxiliary prefix. — Independent reviewer accepted corresponding publication delta 3.
quantifiers: Explicit default totalizes output on a proved null event. — Independent reviewer accepted corresponding publication delta 4.
conclusion: All conditional, accepted, mass and output identities are exported. — Independent reviewer accepted corresponding publication delta 5.
constant_dependencies: Expected full-batch cost is derived, not a short-circuit or gradient theorem. — Independent reviewer accepted corresponding publication delta 6.
scopes: Concrete FORS estimator, clipping, target, accuracy and gradient-cost consumers remain separate. — Independent reviewer accepted corresponding publication delta 7.

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

Scope 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.

Sources, dependencies, and reuse

Source and reuse

Samplinglib 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.

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.

Actual bounded Poisson rejection output and full-batch cost

Complete source statement (Samplinglib restatement)

Actual bounded rejection output and full-batch cost

Read the formalized proofs

Actual bounded Poisson rejection output and full-batch cost

Mathematical statement

Proof roadmap

All objects and hypotheses

Mathematical proof

1. Build the actual independent attempt

2. Compute conditional acceptance from the event

3. Identify the accepted submeasure and its mass

4. Prove real retries terminate and normalize the output

5. Construct a common Markov kernel and identify the target

6. Charge every full attempt, including the successful one

7. Derive the explicit finite expected cost

Lean verification

Source assumptions versus formal assumptions

Detected semantic differences

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Mathematical sources

Which proof obligations and prerequisites are covered?