AutoSamplingTheory.ExampleCases.ProximalBPS.ActualHazardClock

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

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.

\[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