Actual PBPS integrated hazard and first exponential clock

Fan Chen, Sinho Chewi, Jianfeng Lu and Matthew S. Zhang, arXiv:2609.06905v1, Algorithm1 and AppendixA.1 equation(A.1), Ex1–8. ASTIS supplies omitted continuous-first-crossing and measure details. Recursive equation(A.2) and the full Proposition3.1 stochastic construction remain later consumers.

arXiv2609.06905v1 · arXiv2609.06905v1 Algorithm1, Proposition3.1, AppendixA.1 equation(A.1), Ex1-8; one-segment prerequisites for recursive equation(A.2). · faithful paraphrase

Complete source statement (Samplinglib restatement)

Let E be a finite-dimensional real inner-product Borel space, including rank zero. Let V:E→ℝ be C², let α,β≥0 satisfy 0<α≤β and α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for all x,v, and let η>0 with βη≤1. For arbitrary y,xRef and z=(x,p), define c=y−η∇V(xRef), Φ_t(z)=(c+cos(t)(x−c)+√η sin(t)p, −sin(t)(x−c)/√η+cos(t)p), λ(xRef,(u,q))=√η max(0,⟨q,∇V(u)−∇V(xRef)⟩), H(z)=(η⁻¹‖x−c‖²+‖p‖²)/2, and C(z)=√η β√(2H(z))(√(2ηH(z))+‖c−xRef‖). For t≥0 put Λ_z(t)=∫₀ᵗλ(xRef,Φ_s(z))ds and τ_z(e)=inf{t≥0:Λ_z(t)≥e}, returning ∞ when this set is empty. Let W_z be the pushforward of Exp(1) on ℝ by e↦τ_z(max(e,0)). Then: (1) Λ is jointly continuous in y,xRef,z,t; (2) Λ is jointly Borel; (3) the actual orbit rate is integrable on every finite [0,t]; (4) Λ_z(0)=0, Λ_z(t)≥0 and Λ_z is nondecreasing; (5) for every e,t≥0, τ_z(e)≤t iff e≤Λ_z(t); (6) τ_z(e)=∞ iff Λ_z(t)<e for every finite t, finite τ_z(e) satisfies Λ_z(τ_z(e))=e, e>0 implies τ_z(e)>0, and τ_z(0)=0; (7) τ is jointly Borel in y,xRef,z,e; (8) W_z is a probability measure on [0,∞] and W_z((t,∞])=exp(−Λ_z(t)) for every finite t; (9) C(z)≥0 and Λ_z(t)≤C(z)t; (10) C(z)>0 implies max(e/C(z),0)≤τ_z(e), while C(z)=0 and e>0 imply τ_z(e)=∞. Every conclusion is derived for the actual flow and rate using their compiled laws. No unbounded-hazard or almost-sure finite-wait assumption is made. This is one flow-segment clock law used by AppendixA.1(A.1) and the future recursion(A.2). Recursive paths, nonexplosion, Markov memorylessness, invariance, terminal sampling kernels, main bounds and query costs remain open.

E is a finite-dimensional real inner-product space with its compatible norm and Borel measurable structure; product spaces use product structures. Rank zero is allowed.
V:E→ℝ is C² on all E. The nonnegative α,β satisfy 0<α and α≤β, and α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for every x,v∈E.
η is real, η>0 and βη≤1. These are exactly the six original analytic callers. Flow/rate continuity, integrability, hazard monotonicity, an arbitrary cap, positivity of energy and finiteness of a random wait are never supplied as callers.
All y,xRef∈E, initial phase z=(x,p)∈E×E, continuous nonnegative times t and thresholds e≥0 are arbitrary. The eight c,Φ,λ,H,C,Λ,τ,W definitions below are the literal definitions.
τ takes values in [0,∞], with τ=∞ when no finite cumulative-hazard crossing exists. e=0 is included and gives τ=0. The finite-hitting identity has an explicit τ≠∞ guard.
W is the actual pushforward of the unit-rate real exponential measure under e↦τ(toNNReal e); its measurability and probability normalization are conclusions. The waiting lower bound assumes C>0 only in its own implication; the C=0,e>0 branch gives τ=∞.

Actual harmonic orbit

\[c=y-\eta\nabla V(x_{\rm ref}),\quad\Phi_t(x,p)=\bigl(c+\cos t(x-c)+\sqrt\eta\sin t\,p,-\tfrac{\sin t}{\sqrt\eta}(x-c)+\cos t\,p\bigr).\]

Actual rate, energy and majorant

\[\lambda(x_{\rm ref},(x,p))=\sqrt\eta\max\{0,\langle p,\nabla V(x)-\nabla V(x_{\rm ref})\rangle\},\quad H(z)=\tfrac12(\eta^{-1}\|x-c\|^2+\|p\|^2),\quad C(z)=\sqrt\eta\,\beta\sqrt{2H(z)}\bigl(\sqrt{2\eta H(z)}+\|c-x_{\rm ref}\|\bigr).\]

Continuous cumulative hazard and first crossing

\[\Lambda_z(t)=\int_0^t\lambda(x_{\rm ref},\Phi_s z)\,ds,\quad\tau_z(e)=\inf\{t\ge0:\Lambda_z(t)\ge e\}\in[0,\infty],\quad\inf\varnothing=\infty.\]

Actual exponential law and waiting bound

\[W_z=(e\mapsto\tau_z(\max\{e,0\}))_\#\operatorname{Exp}(1),\quad W_z((t,\infty])=e^{-\Lambda_z(t)},\quad\Lambda_z(t)\le C(z)t,\quad\tau_z(e)\ge e/C(z)\ (C(z)>0).\]

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 PBPS integrated hazard and first exponential clock

AutoSamplingTheory.ExampleCases.ProximalBPS.ActualHazardClock.actual_integrated_hazard_clock_laws · theorem · Teaching coverage

Read this first

Mathematical statement

\[c=y-\eta\nabla V(x_{\rm ref}),\quad\Phi_t(x,p)=\bigl(c+\cos t(x-c)+\sqrt\eta\sin t\,p,-\tfrac{\sin t}{\sqrt\eta}(x-c)+\cos t\,p\bigr).\quad \lambda(x_{\rm ref},(x,p))=\sqrt\eta\max\{0,\langle p,\nabla V(x)-\nabla V(x_{\rm ref})\rangle\},\quad H(z)=\tfrac12(\eta^{-1}\|x-c\|^2+\|p\|^2),\quad C(z)=\sqrt\eta\,\beta\sqrt{2H(z)}\bigl(\sqrt{2\eta H(z)}+\|c-x_{\rm ref}\|\bigr).\quad \Lambda_z(t)=\int_0^t\lambda(x_{\rm ref},\Phi_s z)\,ds,\quad\tau_z(e)=\inf\{t\ge0:\Lambda_z(t)\ge e\}\in[0,\infty],\quad\inf\varnothing=\infty.\quad W_z=(e\mapsto\tau_z(\max\{e,0\}))_\#\operatorname{Exp}(1),\quad W_z((t,\infty])=e^{-\Lambda_z(t)},\quad\Lambda_z(t)\le C(z)t,\quad\tau_z(e)\ge e/C(z)\ (C(z)>0).\]

Lean statement · actual_integrated_hazard_clock_laws

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 actual_integrated_hazard_clock_laws
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {V : E → ℝ} {α β : ℝ≥0} {η : ℝ}
    (hα : 0 < (α : ℝ)) (hαβ : α ≤ β) (hV : ContDiff ℝ 2 V)
    (hH : ∀ x v : E,
      (α : ℝ) * ‖v‖ ^ 2 ≤ (fderiv ℝ (fderiv ℝ V) x v) v ∧
      (fderiv ℝ (fderiv ℝ V) x v) v ≤ (β : ℝ) * ‖v‖ ^ 2)
    (hη : 0 < η) (hβη : (β : ℝ) * η ≤ 1) :
    actual_integrated_hazard_clock_statement hα hαβ hV hH hη hβη

Exact module and namespace context

Full Lean proposition (definition) · actual_integrated_hazard_clock_statement

This literal definition stores the complete proposition asserted above. It supplies no mathematical proof or additional hypothesis; the theorem proof must establish its value.

Download module (.lean)

private def actual_integrated_hazard_clock_statement
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {V : E → ℝ} {α β : ℝ≥0} {η : ℝ}
    (hα : 0 < (α : ℝ)) (hαβ : α ≤ β) (hV : ContDiff ℝ 2 V)
    (hH : ∀ x v : E,
      (α : ℝ) * ‖v‖ ^ 2 ≤ (fderiv ℝ (fderiv ℝ V) x v) v ∧
      (fderiv ℝ (fderiv ℝ V) x v) v ≤ (β : ℝ) * ‖v‖ ^ 2)
    (hη : 0 < η) (hβη : (β : ℝ) * η ≤ 1) : Prop :=
    let c : E → E → E := fun y xRef => y - η • gradient V xRef
    let Φ : E → E → ℝ → (E × E) → (E × E) := fun y xRef t z =>
      (c y xRef + Real.cos t • (z.1 - c y xRef) +
          (Real.sqrt η * Real.sin t) • z.2,
       (-Real.sin t / Real.sqrt η) • (z.1 - c y xRef) + Real.cos t • z.2)
    let rate : E → (E × E) → ℝ := fun xRef z =>
      Real.sqrt η * max 0 (inner ℝ z.2 (gradient V z.1 - gradient V xRef))
    let H : E → E → (E × E) → ℝ := fun y xRef z =>
      (η⁻¹ * ‖z.1 - c y xRef‖ ^ 2 + ‖z.2‖ ^ 2) / 2
    let C : E → E → (E × E) → ℝ := fun y xRef z =>
      Real.sqrt η * (β : ℝ) * Real.sqrt (2 * H y xRef z) *
        (Real.sqrt (2 * η * H y xRef z) + ‖c y xRef - xRef‖)
    let Λ : E → E → (E × E) → ℝ≥0 → ℝ := fun y xRef z t =>
      ∫ s in (0 : ℝ)..(t : ℝ), rate xRef (Φ y xRef s z)
    let τ : E → E → (E × E) → ℝ≥0 → WithTop ℝ≥0 := fun y xRef z e =>
      MeasureTheory.hittingAfter
        (fun t : ℝ≥0 => fun a : (E × E) × (E × E) × ℝ≥0 =>
          Λ a.1.1 a.1.2 a.2.1 t - (a.2.2 : ℝ))
        (Set.Ici (0 : ℝ)) 0 ((y, xRef), z, e)
    let W : E → E → (E × E) → Measure (WithTop ℝ≥0) := fun y xRef z =>
      Measure.map (fun e : ℝ => τ y xRef z (Real.toNNReal e))
        (ProbabilityTheory.expMeasure (1 : ℝ))
    Continuous (fun a : ((E × E) × (E × E)) × ℝ≥0 =>
      Λ a.1.1.1 a.1.1.2 a.1.2 a.2) ∧
    Measurable (fun a : ((E × E) × (E × E)) × ℝ≥0 =>
      Λ a.1.1.1 a.1.1.2 a.1.2 a.2) ∧
    (∀ y xRef : E, ∀ z : E × E, ∀ t : ℝ≥0,
      IntervalIntegrable (fun s : ℝ => rate xRef (Φ y xRef s z)) volume 0 (t : ℝ)) ∧
    (∀ y xRef : E, ∀ z : E × E,
      Λ y xRef z 0 = 0 ∧ (∀ t : ℝ≥0, 0 ≤ Λ y xRef z t) ∧
      Monotone (Λ y xRef z)) ∧
    (∀ y xRef : E, ∀ z : E × E, ∀ e t : ℝ≥0,
      τ y xRef z e ≤ (t : WithTop ℝ≥0) ↔ (e : ℝ) ≤ Λ y xRef z t) ∧
    (∀ y xRef : E, ∀ z : E × E, ∀ e : ℝ≥0,
      (τ y xRef z e = ⊤ ↔ ∀ t : ℝ≥0, Λ y xRef z t < (e : ℝ)) ∧
      (τ y xRef z e ≠ ⊤ → Λ y xRef z (τ y xRef z e).untopA = (e : ℝ)) ∧
      (0 < e → (0 : WithTop ℝ≥0) < τ y xRef z e) ∧ τ y xRef z 0 = 0) ∧
    Measurable (fun a : (E × E) × (E × E) × ℝ≥0 =>
      τ a.1.1 a.1.2 a.2.1 a.2.2) ∧
    (∀ y xRef : E, ∀ z : E × E, IsProbabilityMeasure (W y xRef z) ∧
      ∀ t : ℝ≥0, (W y xRef z).real (Set.Ioi (t : WithTop ℝ≥0)) =
        Real.exp (-Λ y xRef z t)) ∧
    (∀ y xRef : E, ∀ z : E × E, 0 ≤ C y xRef z ∧
      ∀ t : ℝ≥0, Λ y xRef z t ≤ C y xRef z * (t : ℝ)) ∧
    (∀ y xRef : E, ∀ z : E × E, ∀ e : ℝ≥0,
      (0 < C y xRef z →
        (Real.toNNReal ((e : ℝ) / C y xRef z) : WithTop ℝ≥0) ≤ τ y xRef z e) ∧
      (C y xRef z = 0 → 0 < e → τ y xRef z e = ⊤))

set_option maxHeartbeats 800000 in

Exact module and namespace context

Proof roadmap

1Reuse the actual flow, rate and conserved-energy bound
Take joint flow continuity and exact H conservation from the compiled harmonic-flow theorem, and rate continuity/nonnegativity and the same-energy-layer bound from the compiled bounce/rate theorem. Substitute Φ_s(z) into that bound and use H(Φ_s(z))=H(z). Positivity of the displayed factors proves C(z)≥0.
2Construct the continuous cumulative hazard
The actual joint orbit rate is continuous. The parameter-dependent primitive theorem with real Lebesgue measure gives joint continuity of its integral up to t; restricting the endpoint to NNReal preserves continuity and Borel measurability. For each fixed phase, direct trigonometric continuity of Φ and continuity of λ prove interval integrability on every finite real interval.
3Derive monotonicity and the integrated cap
The empty interval gives Λ(0)=0. Nonnegativity of the actual integrand gives Λ(t)≥0. Integral monotonicity on nested nonnegative intervals gives Λ(s)≤Λ(t) when s≤t. Integrating the same actual pointwise bound C(z) gives Λ(t)≤C(z)t. Collect these facts in the private helper; no integral or cap certificate becomes a public caller.
4Identify the exact finite-time crossing event
Reuse the proved primitive facts with their folded local types. The set A_e={s≥0:e≤Λ(s)} is closed by continuity. If A_e is nonempty, its infimum belongs to A_e because it is bounded below; monotonicity gives inf A_e≤t iff e≤Λ(t). If it is empty, τ=∞ and both sides are false. This is a closed-set argument on continuous NNReal time.
5Prove the first crossing has the exact threshold value
For finite τ=q, the crossing event gives e≤Λ(q). If Λ(q)>e, continuity on [0,q], Λ(0)=0 and e≥0 yield s≤q with Λ(s)=e by the intermediate value theorem. Strictness forces s<q, while the crossing equivalence forces q≤s, a contradiction. At time zero the same event proves e>0⇒τ>0 and τ(0)=0.
6Prove the first clock is jointly Borel
The target extended time is generated by closed lower intervals. The preimage of Iic(∞) is the whole space. For finite t, the crossing event identifies the preimage as {e≤Λ_z(t)}, a Borel inequality between the threshold coordinate and the jointly Borel cumulative hazard. This proves joint measurability, including infinite waiting.
7Push forward the actual unit exponential law
The unit-rate exponential measure is a probability measure. Its map e↦τ_z(toNNReal e) is measurable by composing the jointly Borel clock with fixed parameters and the measurable nonnegative-part map. Hence its pushforward W_z is a probability measure. The finite-time event and Λ_z(t)≥0 identify the strict survival preimage exactly with {e>Λ_z(t)} on ℝ.
8Evaluate the strict survival probability
Apply the measurable pushforward formula to Ioi(t). The preimage from the preceding block is Ioi(Λ_z(t)). Take the complement of Iic and use the exact Exp(1) CDF, 1−exp(−u) for u≥0, obtaining exp(−Λ_z(t)). Possible mass at infinite waiting is retained by the interval (t,∞].
9Extract the extended waiting lower bound and zero-cap branch
If C(z)>0 and τ is finite, the exact threshold identity and integrated cap give e=Λ_z(τ)≤C(z)τ, so e/C(z)≤τ. If τ=∞ the extended inequality is automatic. If C(z)=0 and e>0, every Λ_z(t)≤0<e; the no-hit equivalence gives τ=∞. Collect all ten conclusion groups, preserving the finite-hit guards.

Full assumptions and notation

All objects and hypotheses

E is a finite-dimensional real inner-product space with its compatible norm and Borel measurable structure; product spaces use product structures. Rank zero is allowed.
V:E→ℝ is C² on all E. The nonnegative α,β satisfy 0<α and α≤β, and α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for every x,v∈E.
η is real, η>0 and βη≤1. These are exactly the six original analytic callers. Flow/rate continuity, integrability, hazard monotonicity, an arbitrary cap, positivity of energy and finiteness of a random wait are never supplied as callers.
All y,xRef∈E, initial phase z=(x,p)∈E×E, continuous nonnegative times t and thresholds e≥0 are arbitrary. The eight c,Φ,λ,H,C,Λ,τ,W definitions below are the literal definitions.
τ takes values in [0,∞], with τ=∞ when no finite cumulative-hazard crossing exists. e=0 is included and gives τ=0. The finite-hitting identity has an explicit τ≠∞ guard.
W is the actual pushforward of the unit-rate real exponential measure under e↦τ(toNNReal e); its measurability and probability normalization are conclusions. The waiting lower bound assumes C>0 only in its own implication; the C=0,e>0 branch gives τ=∞.

Mathematical proof

1. Reuse the actual flow, rate and conserved-energy bound

Take joint flow continuity and exact H conservation from the compiled harmonic-flow theorem, and rate continuity/nonnegativity and the same-energy-layer bound from the compiled bounce/rate theorem. Substitute Φ_s(z) into that bound and use H(Φ_s(z))=H(z). Positivity of the displayed factors proves C(z)≥0.

\[\lambda(x_{\rm ref},\Phi_s z)\ge0,\quad H(\Phi_s z)=H(z),\quad\lambda(x_{\rm ref},\Phi_s z)\le C(z),\quad C(z)\ge0.\]

Corresponding Lean step

  have hf := ActualHarmonicFlow.actual_harmonic_flow_laws hα hαβ hV hH hη hβη
  have hb := ActualBounceRate.actual_bounce_rate_energy_laws hα hαβ hV hH hη hβη
  have hΦ : Continuous (fun a : (E × E) × ℝ × (E × E) =>
      Φ a.1.1 a.1.2 a.2.1 a.2.2) := hf.1
  have hrate : Continuous (fun a : E × (E × E) => rate a.1 a.2) := hb.2.1
  have hrate0 (xRef : E) (z : E × E) : 0 ≤ rate xRef z :=
    (hb.2.2.2.2.2.2.2.1 xRef z).1
  have henergy (y xRef : E) (s : ℝ) (z : E × E) :
      H y xRef (Φ y xRef s z) = H y xRef z := hf.2.2.2.2.2.2.2.1 y xRef s z
  have hcap (y xRef : E) (z : E × E) (s : ℝ) :
      rate xRef (Φ y xRef s z) ≤ C y xRef z :=
    (hb.2.2.2.2.2.2.2.2.2 y xRef z).2 (Φ y xRef s z) (henergy y xRef s z) |>.2.2
  have hC (y xRef : E) (z : E × E) : 0 ≤ C y xRef z := by
    dsimp [C]
    positivity