Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0

ActualConditionalNextWaitDensity: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

  1. Actual PBPS conditional finite next-wait density
Samplinglib mathematical lesson

Actual PBPS conditional finite next-wait density

AutoSamplingTheory.ExampleCases.ProximalBPS.ActualConditionalNextWaitDensity.actual_conditional_next_wait_density · theorem · Teaching coverage

Read this first

Mathematical statement

Let E be any finite-dimensional real inner-product Borel space, including dimension zero. Let V:E→ℝ be C², α,β≥0 and η∈ℝ with α>0, α≤β, α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for every x,v∈E, η>0 and βη≤1. Fix any deterministic y,r∈E and initial phase z₀∈E×E. Put c=y−η∇V(r), Φ_t(x,p)=(c+cos(t)(x−c)+√η sin(t)p, −sin(t)(x−c)/√η+cos(t)p), g_r(x)=∇V(x)−∇V(r), S_r(x,p)=(x,p−2〈p,g_r(x)〉g_r(x)/‖g_r(x)‖²), λ_r(x,p)=√η max{0,〈p,g_r(x)〉}, Λ_z(t)=∫₀ᵗλ_r(Φ_s(z))ds and τ_z(e)=inf{t≥0:Λ_z(t)≥e}∈[0,∞], with inf empty=∞. Total real division makes S_r the identity at g_r(x)=0. The record space is D=([0,∞)×(E×E))⊕{stopped}, with Borel sum structure. Define next(e,stopped)=stopped; for a live record (T,z), next(e,(T,z))=stopped if τ_z(e)=∞, and otherwise next(e,(T,z))=(T+τ_z(e),S_rΦ_(τ_z(e))(z)). In the Lean definition untopD0 is used only in this non-top branch. Define R₀(e)=live(0,z₀) and R_(j+1)(e)=next(e_j,R_j(e)). Let Ω=ℝ^ℕ with its product Borel structure and P=⊗_(k≥0)Exp(1). Let ε(w)_k=max{w_k,0}; this is an ambient coordinate extension on a P-null nonpositive-clock set, not new source dynamics for negative clocks. For every deterministic depth n≥0 let Hist_n=Drecord^(Fin(n+1)), H_n(w)=(R_j(ε(w)))_(0≤j≤n), and μ_n=(H_n)_*P. Raw w_n is the next unused threshold. Define the total extended wait W(live(T,z),e)=τ_z(max(e,0)), W(stopped,e)=0, and total real observable t(r,e)=real(untopD_0 W(r,e)); these zero defaults outside positive finite waits are proof observables only. Define the finite nonnegative auxiliary real-time density ρ(live(T,z),s)=λ_r(Φ_s z)exp(−Λ_z(max(s,0))) and ρ(stopped,s)=0, embedded into extended nonnegative reals. W and ρ are jointly Borel and ρ is finite everywhere. For every fixed Borel d:Hist_n→[0,∞), each d(h) finite but not necessarily uniformly bounded, set D_d(h,s)=1_{0<s<d(h)}ρ(h_n,s). The extension ρ at nonpositive s is auxiliary and is killed by this strict guard. D_d is jointly Borel. The actual Mathlib kernel K_d=withDensity(const(Hist_n,real Lebesgue),D_d) satisfies K_d(h)=D_d(h,s)ds for every abstract history h and K_d(h,ℝ)≤1; it is a finite subprobability kernel. This equality explicitly identifies the measurable constructor branch rather than its zero fallback. Let B_d={w:0<W(R_n(ε(w)),w_n)<d(H_n(w))}, X_n(w)=(H_n(w),t(R_n(ε(w)),w_n)), and ν_d=D_d(μ_n⊗ds). B_d is Borel, X_n is Borel, (X_n)_*(P restricted to B_d)=ν_d and ν_d(Hist_n×ℝ)≤1. For every jointly Borel F:Hist_n×ℝ→[0,∞], h↦∫_ℝ F(h,s)D_d(h,s)ds is Borel. For every Borel A⊆Hist_n, ∫_{B_d∩{H_n∈A}} F(X_n(w))P(dw)=∫_A[∫_ℝ F(h,s)D_d(h,s)ds]μ_n(dh). No boundedness or integrability assumption on F, no positive μ_n(A), no normalized conditional probability and no finite-wait/provider hypothesis is needed; extended integrals may be infinite. Stopped histories have zero finite kernel, infinite waits fail the finite guard, and missing mass is not renormalized. The cases d(h)=0, n=0, zero hazards, rank zero and unrealizable abstract histories are included. Real Lebesgue time on the strict Ioo(0,d(h)) is exactly the already verified deterministic Ioc density reference restricted further by Iio(d(h)); no open/closed endpoint-mass equivalence or exact strict mass formula is asserted. All conclusions use the six original standing analytic hypotheses. This is attributed ASTIS completion of one finite jump-density factor implicit in Appendix A.1(A.7). Full ordered-time iteration, final survival/path functional assembly, full(A.7), physical-time residual memorylessness/random restart/Markovness, global nonexplosion/invariance/hypocoercivity, implementation/error/unbounded expected cost/main/composition/wholepaper/Goal remain OPEN. Adjacent survival88 is not a false proof prerequisite.

\[\int_{B_d\cap\{H_n\in A\}}F(X_n)\,dP=\int_A\left(\int_{\mathbb R}F(h,s)D_d(h,s)\,ds\right)\mu_n(dh).\]
Lean statement · actual_conditional_next_wait_density

Let E be any finite-dimensional real inner-product Borel space, including dimension zero. Let V:E→ℝ be C², α,β≥0 and η∈ℝ with α>0, α≤β, α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for every x,v∈E, η>0 and βη≤1. Fix any deterministic y,r∈E and initial phase z₀∈E×E. Put c=y−η∇V(r), Φ_t(x,p)=(c+cos(t)(x−c)+√η sin(t)p, −sin(t)(x−c)/√η+cos(t)p), g_r(x)=∇V(x)−∇V(r), S_r(x,p)=(x,p−2〈p,g_r(x)〉g_r(x)/‖g_r(x)‖²), λ_r(x,p)=√η max{0,〈p,g_r(x)〉}, Λ_z(t)=∫₀ᵗλ_r(Φ_s(z))ds and τ_z(e)=inf{t≥0:Λ_z(t)≥e}∈[0,∞], with inf empty=∞. Total real division makes S_r the identity at g_r(x)=0. The record space is D=([0,∞)×(E×E))⊕{stopped}, with Borel sum structure. Define next(e,stopped)=stopped; for a live record (T,z), next(e,(T,z))=stopped if τ_z(e)=∞, and otherwise next(e,(T,z))=(T+τ_z(e),S_rΦ_(τ_z(e))(z)). In the Lean definition untopD0 is used only in this non-top branch. Define R₀(e)=live(0,z₀) and R_(j+1)(e)=next(e_j,R_j(e)). Let Ω=ℝ^ℕ with its product Borel structure and P=⊗_(k≥0)Exp(1). Let ε(w)_k=max{w_k,0}; this is an ambient coordinate extension on a P-null nonpositive-clock set, not new source dynamics for negative clocks. For every deterministic depth n≥0 let Hist_n=Drecord^(Fin(n+1)), H_n(w)=(R_j(ε(w)))_(0≤j≤n), and μ_n=(H_n)_*P. Raw w_n is the next unused threshold. Define the total extended wait W(live(T,z),e)=τ_z(max(e,0)), W(stopped,e)=0, and total real observable t(r,e)=real(untopD_0 W(r,e)); these zero defaults outside positive finite waits are proof observables only. Define the finite nonnegative auxiliary real-time density ρ(live(T,z),s)=λ_r(Φ_s z)exp(−Λ_z(max(s,0))) and ρ(stopped,s)=0, embedded into extended nonnegative reals. W and ρ are jointly Borel and ρ is finite everywhere. For every fixed Borel d:Hist_n→[0,∞), each d(h) finite but not necessarily uniformly bounded, set D_d(h,s)=1_{0<s<d(h)}ρ(h_n,s). The extension ρ at nonpositive s is auxiliary and is killed by this strict guard. D_d is jointly Borel. The actual Mathlib kernel K_d=withDensity(const(Hist_n,real Lebesgue),D_d) satisfies K_d(h)=D_d(h,s)ds for every abstract history h and K_d(h,ℝ)≤1; it is a finite subprobability kernel. This equality explicitly identifies the measurable constructor branch rather than its zero fallback. Let B_d={w:0<W(R_n(ε(w)),w_n)<d(H_n(w))}, X_n(w)=(H_n(w),t(R_n(ε(w)),w_n)), and ν_d=D_d(μ_n⊗ds). B_d is Borel, X_n is Borel, (X_n)_*(P restricted to B_d)=ν_d and ν_d(Hist_n×ℝ)≤1. For every jointly Borel F:Hist_n×ℝ→[0,∞], h↦∫_ℝ F(h,s)D_d(h,s)ds is Borel. For every Borel A⊆Hist_n, ∫_{B_d∩{H_n∈A}} F(X_n(w))P(dw)=∫_A[∫_ℝ F(h,s)D_d(h,s)ds]μ_n(dh). No boundedness or integrability assumption on F, no positive μ_n(A), no normalized conditional probability and no finite-wait/provider hypothesis is needed; extended integrals may be infinite. Stopped histories have zero finite kernel, infinite waits fail the finite guard, and missing mass is not renormalized. The cases d(h)=0, n=0, zero hazards, rank zero and unrealizable abstract histories are included. Real Lebesgue time on the strict Ioo(0,d(h)) is exactly the already verified deterministic Ioc density reference restricted further by Iio(d(h)); no open/closed endpoint-mass equivalence or exact strict mass formula is asserted. All conclusions use the six original standing analytic hypotheses. This is attributed ASTIS completion of one finite jump-density factor implicit in Appendix A.1(A.7). Full ordered-time iteration, final survival/path functional assembly, full(A.7), physical-time residual memorylessness/random restart/Markovness, global nonexplosion/invariance/hypocoercivity, implementation/error/unbounded expected cost/main/composition/wholepaper/Goal remain OPEN. Adjacent survival88 is not a false proof prerequisite.

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_conditional_next_wait_density
    {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_conditional_next_wait_density_statement hα hαβ hV hH hη hβη

Exact module and namespace context

Full Lean proposition (definition) · actual_conditional_next_wait_density_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.

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)
private def actual_conditional_next_wait_density_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 S : E → (E × E) → (E × E) := fun xRef z =>
      (z.1, z.2 - (2 * inner ℝ z.2 (gradient V z.1 - gradient V xRef) /
        ‖gradient V z.1 - gradient V xRef‖ ^ 2) • (gradient V z.1 - gradient V xRef))
    let rate : E → (E × E) → ℝ := fun xRef z =>
      Real.sqrt η * max 0 (inner ℝ z.2 (gradient V z.1 - gradient V 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 next : E → E → ℝ≥0 → ((ℝ≥0 × (E × E)) ⊕ Unit) →
        ((ℝ≥0 × (E × E)) ⊕ Unit) := fun y xRef e r =>
      match r with
      | Sum.inr _ => Sum.inr ()
      | Sum.inl a =>
        if τ y xRef a.2 e = ⊤ then Sum.inr () else
          Sum.inl (a.1 + (τ y xRef a.2 e).untopD 0,
            S xRef (Φ y xRef (((τ y xRef a.2 e).untopD 0 : ℝ≥0) : ℝ) a.2))
    let record : E → E → (E × E) → (ℕ → ℝ≥0) → ℕ →
        ((ℝ≥0 × (E × E)) ⊕ Unit) := fun y xRef z₀ e n =>
      Nat.rec (Sum.inl (0, z₀)) (fun k r => next y xRef (e k) r) n
    let P : Measure (ℕ → ℝ) := Measure.infinitePi (fun _ : ℕ => expMeasure (1 : ℝ))
    let ε : (ℕ → ℝ) → ℕ → ℝ≥0 := fun w k => Real.toNNReal (w k)
    let history : E → E → (E × E) → (n : ℕ) → (ℕ → ℝ) →
        (Fin (n + 1) → ((ℝ≥0 × (E × E)) ⊕ Unit)) :=
      fun y xRef z₀ n w j => record y xRef z₀ (ε w) j.val
    let waitObs : E → E → (((ℝ≥0 × (E × E)) ⊕ Unit) × ℝ) → WithTop ℝ≥0 :=
      fun y xRef q => match q.1 with
        | Sum.inl a => τ y xRef a.2 (Real.toNNReal q.2)
        | Sum.inr _ => 0
    let timeObs : E → E → (((ℝ≥0 × (E × E)) ⊕ Unit) × ℝ) → ℝ :=
      fun y xRef q => ((waitObs y xRef q).untopD 0 : ℝ≥0)
    let density : E → E → (((ℝ≥0 × (E × E)) ⊕ Unit) × ℝ) → ℝ≥0∞ :=
      fun y xRef q => match q.1 with
        | Sum.inl a => ENNReal.ofReal (rate xRef (Φ y xRef q.2 a.2) *
            Real.exp (-Λ y xRef a.2 (Real.toNNReal q.2)))
        | Sum.inr _ => 0
    ∀ y xRef : E, ∀ z₀ : E × E, ∀ n : ℕ,
      Measurable (waitObs y xRef) ∧ Measurable (density y xRef) ∧
      (∀ q, density y xRef q ≠ ⊤) ∧
      (∀ d : (Fin (n + 1) → ((ℝ≥0 × (E × E)) ⊕ Unit)) → ℝ≥0,
        Measurable d →
        let Hist := Fin (n + 1) → ((ℝ≥0 × (E × E)) ⊕ Unit)
        let last : Fin (n + 1) := ⟨n, Nat.lt_succ_self n⟩
        let H : (ℕ → ℝ) → Hist := history y xRef z₀ n
        let μ : Measure Hist := Measure.map H P
        let D : Hist → ℝ → ℝ≥0∞ := fun h s =>
          if 0 < s ∧ s < (d h : ℝ) then density y xRef (h last, s) else 0
        let K : Kernel Hist ℝ := (Kernel.const Hist (volume : Measure ℝ)).withDensity D
        let B : Set (ℕ → ℝ) := {w |
          (0 : WithTop ℝ≥0) < waitObs y xRef (record y xRef z₀ (ε w) n, w n) ∧
          waitObs y xRef (record y xRef z₀ (ε w) n, w n) <
            ((d (H w) : ℝ≥0) : WithTop ℝ≥0)}
        let X : (ℕ → ℝ) → Hist × ℝ := fun w =>
          (H w, timeObs y xRef (record y xRef z₀ (ε w) n, w n))
        let ν : Measure (Hist × ℝ) := (μ.prod (volume : Measure ℝ)).withDensity
          (fun p => D p.1 p.2)
        Measurable (Function.uncurry D) ∧
        (∀ h, K h = (volume : Measure ℝ).withDensity (D h)) ∧
        IsFiniteKernel K ∧ (∀ h, K h Set.univ ≤ 1) ∧
        MeasurableSet B ∧ Measurable X ∧
        Measure.map X (P.restrict B) = ν ∧ ν Set.univ ≤ 1 ∧
        (∀ F : Hist × ℝ → ℝ≥0∞, Measurable F →
          Measurable (fun h => ∫⁻ s : ℝ, F (h, s) * D h s) ∧
          (∀ A : Set Hist, MeasurableSet A →
            (∫⁻ w in B ∩ H ⁻¹' A, F (X w) ∂P) =
              ∫⁻ h in A, (∫⁻ s : ℝ, F (h, s) * D h s) ∂μ)))


set_option maxHeartbeats 1600000 in

Exact module and namespace context

Proof roadmap

  1. 1Retain actual definitions and derive joint Borel observables

    Keep the literal harmonic flow, zero-normal identity reflection, intensity, integrated hazard, first ≥ crossing, stopped recursion, Exp1 product and full finite history. Consume the verified hazard/clock, flow and rate producers; the exponential-product theorem supplies P probability internally. Distribute the record sum across raw clock/time. On live records compose joint crossing and density maps, while stopped records use zero. Coerce untopD0 for the total Borel real observer. Multiplication, exp and ofReal give jointly Borel finite density. Density at nonpositive real times and defaults at stopped/infinite waits are auxiliary total extensions, used only through the strict positive finite guards below.

  2. 2Construct actual histories, strict guards and the genuine kernel

    Fix any Borel finite-valued d, possibly unbounded across histories. Define H, unchanged raw tail Y, μ, guarded D, canonical density kernel K, product event Q, actual event B and pair X. The verified history theorem gives Borel H,Y and (H,Y)_*P=μ⊗P. The last-history and tail0 projections yield Borel W,G,Q and actual B,X. The guard 0<s<d(h) is jointly Borel, hence uncurry D is Borel. Mathlib withDensity_apply then proves K(h)=volume.withDensity(D(h,·)) for every abstract history: this identifies the intended measurable branch, ruling out its zero fallback.

  3. 3Restrict each deterministic fiber to strict positive finite waits

    A stopped last record gives an empty positive-wait event and zero density. For a live state z, producer86 gives f_*(P|A)=ρ_T with T=d(h), A={0<U≤T}, and ρ_T the density on Ioc(0,T). Restrict BOTH measures by Iio(T). Its pullback intersects A exactly in 0<U<T: top cannot satisfy the finite bound; finite waits compare via explicit NNReal/WithTop/real coercions. Restrict-map and restrict-withDensity give density on Ioc(0,T)∩Iio(T)=Ioo(0,T), namely D(h,s)ds. This restricts an equality; it never equates open/closed endpoint masses or assumes no finite atoms.

  4. 4Derive a uniform kernel mass bound internally

    For every fixed abstract history, the density measure is the pushforward of P restricted to the strict finite event. Its mass on all real times is that event probability, at most1. The proved fiber equality transfers this bound to K(h,ℝ), including stopped records, d(h)=0 and unrealizable histories. C=1 supplies IsFiniteKernel. This bounds mass, not the pointwise density; no finite-wait guarantee, integrability provider or normalization is used.

  5. 5Identify the actual joint finite measure

    For arbitrary Borel C⊆Hist×ℝ, pull the actual restricted pushforward back through G(H,Y). L=G⁻¹(C)∩Q is Borel. Replace the joint history/tail law by μ⊗P and apply product-measure sections. The strict fixed-history fiber law replaces each section by D(h,s)ds. Nonnegative product integration gives ∫_C D d(μ⊗ds)=ν(C). Equality for all Borel C proves the joint map law. Total mass is at most1 because ν is a restricted pushforward of the actual probability P.

  6. 6Integrate every nonnegative joint test on every history event

    Jointly Borel F gives jointly Borel F·D; nonnegative parameter integration makes its time integral Borel in h, allowing infinity. For arbitrary Borel A multiply F by the indicator of the first-coordinate event. Restrict/map nonnegative integration and the proved joint measure identity give its ν integral. The density formula and Tonelli yield ∫μ∫ds 1_A(h)F(h,s)D(h,s). The indicator formula gives the displayed history-restricted identity, including null A. No boundedness, integrability, positive conditioning probability, conditional representative or normalization enters.

Full assumptions and notation

All objects and hypotheses

  • E is finite-dimensional over ℝ with inner product and its Borel structure, including rank zero. V:E→ℝ is C².
  • The six standing hypotheses are α>0, α≤β, V∈C², α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for every x,v, η>0 and βη≤1; α,β≥0.
  • y,r,z₀ and n are deterministic and universally quantified. Actual stopped recursion and raw independent Exp1 product P are literal definitions.
  • d:Hist_n→NNReal is any fixed Borel finite-valued function, with no global bound; F:Hist_n×ℝ→ENNReal is jointly Borel, with no boundedness/integrability premise; A is any Borel history event, including μ_n(A)=0. These classify deterministic tests.
  • Joint measurability, density, unused-clock independence, kernel finite mass, no-atom estimates or conditional distributions are not supplied as premises. Strict finite component excludes stopped/infinite waits without normalization.

Mathematical proof

1. Retain actual definitions and derive joint Borel observables

Keep the literal harmonic flow, zero-normal identity reflection, intensity, integrated hazard, first ≥ crossing, stopped recursion, Exp1 product and full finite history. Consume the verified hazard/clock, flow and rate producers; the exponential-product theorem supplies P probability internally. Distribute the record sum across raw clock/time. On live records compose joint crossing and density maps, while stopped records use zero. Coerce untopD0 for the total Borel real observer. Multiplication, exp and ofReal give jointly Borel finite density. Density at nonpositive real times and defaults at stopped/infinite waits are auxiliary total extensions, used only through the strict positive finite guards below.

\[W,\ t,\ \rho\ \text{jointly Borel},\qquad\rho<\infty.\]
Corresponding Lean step
  classical
  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 S : E → (E × E) → (E × E) := fun xRef z =>
    (z.1, z.2 - (2 * inner ℝ z.2 (gradient V z.1 - gradient V xRef) /
      ‖gradient V z.1 - gradient V xRef‖ ^ 2) • (gradient V z.1 - gradient V xRef))
  let rate : E → (E × E) → ℝ := fun xRef z =>
    Real.sqrt η * max 0 (inner ℝ z.2 (gradient V z.1 - gradient V 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 next : E → E → ℝ≥0 → ((ℝ≥0 × (E × E)) ⊕ Unit) →
      ((ℝ≥0 × (E × E)) ⊕ Unit) := fun y xRef e r =>
    match r with
    | Sum.inr _ => Sum.inr ()
    | Sum.inl a =>
      if τ y xRef a.2 e = ⊤ then Sum.inr () else
        Sum.inl (a.1 + (τ y xRef a.2 e).untopD 0,
          S xRef (Φ y xRef (((τ y xRef a.2 e).untopD 0 : ℝ≥0) : ℝ) a.2))
  let record : E → E → (E × E) → (ℕ → ℝ≥0) → ℕ →
      ((ℝ≥0 × (E × E)) ⊕ Unit) := fun y xRef z₀ e n =>
    Nat.rec (Sum.inl (0, z₀)) (fun k r => next y xRef (e k) r) n
  let P : Measure (ℕ → ℝ) := Measure.infinitePi (fun _ : ℕ => expMeasure (1 : ℝ))
  let ε : (ℕ → ℝ) → ℕ → ℝ≥0 := fun w k => Real.toNNReal (w k)
  let history : E → E → (E × E) → (n : ℕ) → (ℕ → ℝ) →
      (Fin (n + 1) → ((ℝ≥0 × (E × E)) ⊕ Unit)) :=
    fun y xRef z₀ n w j => record y xRef z₀ (ε w) j.val
  let waitObs : E → E → (((ℝ≥0 × (E × E)) ⊕ Unit) × ℝ) → WithTop ℝ≥0 :=
    fun y xRef q => match q.1 with
      | Sum.inl a => τ y xRef a.2 (Real.toNNReal q.2)
      | Sum.inr _ => 0
  let timeObs : E → E → (((ℝ≥0 × (E × E)) ⊕ Unit) × ℝ) → ℝ :=
    fun y xRef q => ((waitObs y xRef q).untopD 0 : ℝ≥0)
  let density : E → E → (((ℝ≥0 × (E × E)) ⊕ Unit) × ℝ) → ℝ≥0∞ :=
    fun y xRef q => match q.1 with
      | Sum.inl a => ENNReal.ofReal (rate xRef (Φ y xRef q.2 a.2) *
          Real.exp (-Λ y xRef a.2 (Real.toNNReal q.2)))
      | Sum.inr _ => 0
  change
  ∀ y xRef : E, ∀ z₀ : E × E, ∀ n : ℕ,
    Measurable (waitObs y xRef) ∧ Measurable (density y xRef) ∧
    (∀ q, density y xRef q ≠ ⊤) ∧
    (∀ d : (Fin (n + 1) → ((ℝ≥0 × (E × E)) ⊕ Unit)) → ℝ≥0,
      Measurable d →
      let Hist := Fin (n + 1) → ((ℝ≥0 × (E × E)) ⊕ Unit)
      let last : Fin (n + 1) := ⟨n, Nat.lt_succ_self n⟩
      let H : (ℕ → ℝ) → Hist := history y xRef z₀ n
      let μ : Measure Hist := Measure.map H P
      let D : Hist → ℝ → ℝ≥0∞ := fun h s =>
        if 0 < s ∧ s < (d h : ℝ) then density y xRef (h last, s) else 0
      let K : Kernel Hist ℝ := (Kernel.const Hist (volume : Measure ℝ)).withDensity D
      let B : Set (ℕ → ℝ) := {w |
        (0 : WithTop ℝ≥0) < waitObs y xRef (record y xRef z₀ (ε w) n, w n) ∧
        waitObs y xRef (record y xRef z₀ (ε w) n, w n) <
          ((d (H w) : ℝ≥0) : WithTop ℝ≥0)}
      let X : (ℕ → ℝ) → Hist × ℝ := fun w =>
        (H w, timeObs y xRef (record y xRef z₀ (ε w) n, w n))
      let ν : Measure (Hist × ℝ) := (μ.prod (volume : Measure ℝ)).withDensity
        (fun p => D p.1 p.2)
      Measurable (Function.uncurry D) ∧
      (∀ h, K h = (volume : Measure ℝ).withDensity (D h)) ∧
      IsFiniteKernel K ∧ (∀ h, K h Set.univ ≤ 1) ∧
      MeasurableSet B ∧ Measurable X ∧
      Measure.map X (P.restrict B) = ν ∧ ν Set.univ ≤ 1 ∧
      (∀ F : Hist × ℝ → ℝ≥0∞, Measurable F →
        Measurable (fun h => ∫⁻ s : ℝ, F (h, s) * D h s) ∧
        (∀ A : Set Hist, MeasurableSet A →
          (∫⁻ w in B ∩ H ⁻¹' A, F (X w) ∂P) =
            ∫⁻ h in A, (∫⁻ s : ℝ, F (h, s) * D h s) ∂μ)))

  have hc := ActualHazardClock.actual_integrated_hazard_clock_laws hα hαβ hV hH hη hβη
  have hτ : Measurable (fun a : (E × E) × (E × E) × ℝ≥0 =>
      τ a.1.1 a.1.2 a.2.1 a.2.2) := hc.2.2.2.2.2.2.1
  have hΛ : Measurable (fun a : ((E × E) × (E × E)) × ℝ≥0 =>
      Λ a.1.1.1 a.1.1.2 a.1.2 a.2) := hc.2.1
  have hf := ActualHarmonicFlow.actual_harmonic_flow_laws hα hαβ hV hH hη hβη
  have hr := ActualBounceRate.actual_bounce_rate_energy_laws hα hαβ hV hH hη hβη
  have hi := AutoSamplingTheory.TechnicalLemmas.Probability.UnitExponentialProduct.unit_exponential_product_laws
  letI : IsProbabilityMeasure P := hi.1
  intro y xRef z₀ n
  let Rec := (ℝ≥0 × (E × E)) ⊕ Unit
  let Hist := Fin (n + 1) → Rec
  let last : Fin (n + 1) := ⟨n, Nat.lt_succ_self n⟩
  -- Total clock and density observables are jointly Borel, including stopped0.
  have hw : Measurable (waitObs y xRef) := by
    let e := MeasurableEquiv.sumProdDistrib (ℝ≥0 × (E × E)) Unit ℝ
    have hl : Measurable (fun q : (ℝ≥0 × (E × E)) × ℝ =>
        τ y xRef q.1.2 (Real.toNNReal q.2)) :=
      hτ.comp (f := fun q : (ℝ≥0 × (E × E)) × ℝ =>
        ((y, xRef), q.1.2, Real.toNNReal q.2))
        (measurable_const.prodMk (measurable_fst.snd.prodMk
          (measurable_real_toNNReal.comp measurable_snd)))
    have heq : waitObs y xRef = (Sum.elim
        (fun q : (ℝ≥0 × (E × E)) × ℝ => τ y xRef q.1.2 (Real.toNNReal q.2))
        (fun _ : Unit × ℝ => (0 : WithTop ℝ≥0))) ∘ e := by
      funext q; rcases q with ⟨a | a, t⟩ <;> rfl
    rw [heq]
    exact (hl.sumElim (measurable_const : Measurable
      (fun _ : Unit × ℝ => (0 : WithTop ℝ≥0)))).comp e.measurable
  have ht : Measurable (timeObs y xRef) :=
    measurable_subtype_coe.comp (hw.untopD 0)
  have hρ : Measurable (density y xRef) := by
    let e := MeasurableEquiv.sumProdDistrib (ℝ≥0 × (E × E)) Unit ℝ
    have hφ : Measurable (fun q : (ℝ≥0 × (E × E)) × ℝ => Φ y xRef q.2 q.1.2) :=
      hf.1.measurable.comp (f := fun q : (ℝ≥0 × (E × E)) × ℝ =>
        ((y, xRef), q.2, q.1.2))
        (measurable_const.prodMk (measurable_snd.prodMk measurable_fst.snd))
    have hl : Measurable (fun q : (ℝ≥0 × (E × E)) × ℝ =>
        ENNReal.ofReal (rate xRef (Φ y xRef q.2 q.1.2) *
          Real.exp (-Λ y xRef q.1.2 (Real.toNNReal q.2)))) := by
      have hrateArgs : Measurable (fun q : (ℝ≥0 × (E × E)) × ℝ =>
          (xRef, Φ y xRef q.2 q.1.2)) :=
        (measurable_const : Measurable
          (fun _ : (ℝ≥0 × (E × E)) × ℝ => xRef)).prodMk hφ
      have hrate : Measurable (fun q : (ℝ≥0 × (E × E)) × ℝ =>
          rate xRef (Φ y xRef q.2 q.1.2)) := hr.2.1.measurable.comp hrateArgs
      have hΛArgs : Measurable (fun q : (ℝ≥0 × (E × E)) × ℝ =>
          (((y, xRef), q.1.2), Real.toNNReal q.2)) :=
        (((measurable_const : Measurable
          (fun _ : (ℝ≥0 × (E × E)) × ℝ => (y, xRef))).prodMk
          measurable_fst.snd).prodMk (measurable_real_toNNReal.comp measurable_snd))
      have hhazard : Measurable (fun q : (ℝ≥0 × (E × E)) × ℝ =>
          Λ y xRef q.1.2 (Real.toNNReal q.2)) := hΛ.comp hΛArgs
      exact (hrate.mul hhazard.neg.exp).ennreal_ofReal
    have heq : density y xRef = (Sum.elim
        (fun q : (ℝ≥0 × (E × E)) × ℝ => ENNReal.ofReal
          (rate xRef (Φ y xRef q.2 q.1.2) *
            Real.exp (-Λ y xRef q.1.2 (Real.toNNReal q.2))))
        (fun _ : Unit × ℝ => (0 : ℝ≥0∞))) ∘ e := by
      funext q; rcases q with ⟨a | a, t⟩ <;> rfl
    rw [heq]
    exact (hl.sumElim (measurable_const : Measurable
      (fun _ : Unit × ℝ => (0 : ℝ≥0∞)))).comp e.measurable
  have hρfin (q : Rec × ℝ) : density y xRef q ≠ ⊤ := by
    rcases q with ⟨a | a, t⟩
    · exact ENNReal.ofReal_ne_top
    · exact ENNReal.zero_ne_top

Exact contiguous compiled BODY region; every mathematical ingredient is derived internally.

2. Construct actual histories, strict guards and the genuine kernel

Fix any Borel finite-valued d, possibly unbounded across histories. Define H, unchanged raw tail Y, μ, guarded D, canonical density kernel K, product event Q, actual event B and pair X. The verified history theorem gives Borel H,Y and (H,Y)_*P=μ⊗P. The last-history and tail0 projections yield Borel W,G,Q and actual B,X. The guard 0<s<d(h) is jointly Borel, hence uncurry D is Borel. Mathlib withDensity_apply then proves K(h)=volume.withDensity(D(h,·)) for every abstract history: this identifies the intended measurable branch, ruling out its zero fallback.

\[K_d(h,ds)=D_d(h,s)\,ds,\quad \nu_d(dh,ds)=\mu_n(dh)D_d(h,s)\,ds.\]
Corresponding Lean step
  refine ⟨hw, hρ, hρfin, ?_⟩
  intro d hd
  let H : (ℕ → ℝ) → Hist := history y xRef z₀ n
  let Y : (ℕ → ℝ) → (ℕ → ℝ) := fun w k => w (n + k)
  let μ : Measure Hist := Measure.map H P
  let D : Hist → ℝ → ℝ≥0∞ := fun h s =>
    if 0 < s ∧ s < (d h : ℝ) then density y xRef (h last, s) else 0
  let K : Kernel Hist ℝ := (Kernel.const Hist (volume : Measure ℝ)).withDensity D
  let W : Hist × (ℕ → ℝ) → WithTop ℝ≥0 :=
    fun p => waitObs y xRef (p.1 last, p.2 0)
  let Q : Set (Hist × (ℕ → ℝ)) := {p |
    (0 : WithTop ℝ≥0) < W p ∧ W p < ((d p.1 : ℝ≥0) : WithTop ℝ≥0)}
  let G : Hist × (ℕ → ℝ) → Hist × ℝ :=
    fun p => (p.1, timeObs y xRef (p.1 last, p.2 0))
  let B : Set (ℕ → ℝ) := {w |
    (0 : WithTop ℝ≥0) < waitObs y xRef (record y xRef z₀ (ε w) n, w n) ∧
    waitObs y xRef (record y xRef z₀ (ε w) n, w n) <
      ((d (H w) : ℝ≥0) : WithTop ℝ≥0)}
  let X : (ℕ → ℝ) → Hist × ℝ := fun w =>
    (H w, timeObs y xRef (record y xRef z₀ (ε w) n, w n))
  let ν : Measure (Hist × ℝ) := (μ.prod (volume : Measure ℝ)).withDensity
    (fun p => D p.1 p.2)
  have hp := ActualFiniteHistoryTailLaw.actual_finite_history_tail_law
    hα hαβ hV hH hη hβη y xRef z₀ n
  have hHm : Measurable H := hp.1
  have hY : Measurable Y := hp.2.1
  have hjoint : Measure.map (fun w => (H w, Y w)) P = μ.prod P := hp.2.2.2.2.2.2.1
  letI : IsProbabilityMeasure μ := Measure.isProbabilityMeasure_map hHm.aemeasurable
  have hargs : Measurable (fun p : Hist × (ℕ → ℝ) => (p.1 last, p.2 0)) :=
    ((measurable_pi_apply last).comp measurable_fst).prodMk
      ((measurable_pi_apply 0).comp measurable_snd)
  have hW : Measurable W := hw.comp hargs
  have hQ : MeasurableSet Q :=
    (measurableSet_lt measurable_const hW).inter
      (measurableSet_lt hW (WithTop.measurable_coe.comp (hd.comp measurable_fst)))
  have hG : Measurable G := measurable_fst.prodMk (ht.comp hargs)
  have hXeq : X = G ∘ (fun w => (H w, Y w)) := rfl
  have hBeq : B = (fun w => (H w, Y w)) ⁻¹' Q := rfl
  have hB : MeasurableSet B := hBeq ▸ hQ.preimage (hHm.prodMk hY)
  have hX : Measurable X := hXeq ▸ hG.comp (hHm.prodMk hY)
  have hD : Measurable (Function.uncurry D) := by
    have hguard : MeasurableSet {p : Hist × ℝ | 0 < p.2 ∧ p.2 < (d p.1 : ℝ)} :=
      (measurableSet_lt measurable_const measurable_snd).inter
        (measurableSet_lt measurable_snd (measurable_subtype_coe.comp (hd.comp measurable_fst)))
    exact (hρ.comp (((measurable_pi_apply last).comp measurable_fst).prodMk
      measurable_snd)).piecewise hguard measurable_const
  have hK (h : Hist) : K h = (volume : Measure ℝ).withDensity (D h) :=
    Kernel.withDensity_apply _ hD h

Exact contiguous compiled BODY region; every mathematical ingredient is derived internally.

3. Restrict each deterministic fiber to strict positive finite waits

A stopped last record gives an empty positive-wait event and zero density. For a live state z, producer86 gives f_*(P|A)=ρ_T with T=d(h), A={0<U≤T}, and ρ_T the density on Ioc(0,T). Restrict BOTH measures by Iio(T). Its pullback intersects A exactly in 0<U<T: top cannot satisfy the finite bound; finite waits compare via explicit NNReal/WithTop/real coercions. Restrict-map and restrict-withDensity give density on Ioc(0,T)∩Iio(T)=Ioo(0,T), namely D(h,s)ds. This restricts an equality; it never equates open/closed endpoint masses or assumes no finite atoms.

\[f_*(P|_{\{0<U\le T\}})|_{(-\infty,T)}=f_*(P|_{\{0<U<T\}})=\mathbf1_{(0,T)}(s)\rho_z(s)\,ds.\]
Corresponding Lean step
  -- Restrict the deterministic Ioc law by Iio: strict endpoints on BOTH sides.
  have hfiber (h : Hist) :
      Measure.map (fun w : ℕ → ℝ => timeObs y xRef (h last, w 0))
        (P.restrict {w | (h, w) ∈ Q}) = (volume : Measure ℝ).withDensity (D h) := by
    cases ha : h last with
    | inr a =>
      simp [Q, W, waitObs, timeObs, density, D, ha]
    | inl a =>
      let U : (ℕ → ℝ) → WithTop ℝ≥0 := fun w => τ y xRef a.2 (ε w 0)
      let f : (ℕ → ℝ) → ℝ := fun w => ((U w).untopD 0 : ℝ≥0)
      let A : Set (ℕ → ℝ) := {w | (0 : WithTop ℝ≥0) < U w ∧
        U w ≤ ((d h : ℝ≥0) : WithTop ℝ≥0)}
      let ρ : Measure ℝ := (volume.restrict (Set.Ioc (0 : ℝ) (d h : ℝ))).withDensity
        (fun s => density y xRef (Sum.inl a, s))
      have hfirst := ActualFiniteFirstEventLaw.actual_finite_first_event_law
        hα hαβ hV hH hη hβη y xRef a.2
      have hfm : Measurable f := hfirst.2.1
      have hclosed : Measure.map f (P.restrict A) = ρ := (hfirst.2.2.2 (d h)).2.1
      have hset : A ∩ f ⁻¹' Set.Iio (d h : ℝ) = {w | (h, w) ∈ Q} := by
        ext w
        simp only [Set.mem_inter_iff, A, Set.mem_ofPred_eq, Set.mem_preimage,
          Set.mem_Iio, Q, W, waitObs, ha]
        change ((0 : WithTop ℝ≥0) < U w ∧ U w ≤ ↑(d h)) ∧
          (((U w).untopD 0 : ℝ≥0) : ℝ) < (d h : ℝ) ↔
            (0 : WithTop ℝ≥0) < U w ∧ U w < ↑(d h)
        cases hu : U w using WithTop.recTopCoe with
        | top =>
          simp only [WithTop.not_top_le_coe, and_false, false_and]
          exact iff_of_false id (fun hs => (not_lt_of_ge le_top) hs.2)
        | coe s =>
          have hz : (0 : WithTop ℝ≥0) < (s : WithTop ℝ≥0) ↔ 0 < s := by
            have hz0 : ((0 : ℝ≥0) : WithTop ℝ≥0) < (s : WithTop ℝ≥0) ↔
                (0 : ℝ≥0) < s := WithTop.coe_lt_coe
            simpa only [WithTop.coe_zero] using hz0
          simp only [WithTop.untopD_coe, WithTop.coe_le_coe,
            WithTop.coe_lt_coe, NNReal.coe_lt_coe, hz]
          exact ⟨fun v => ⟨v.1.1, v.2⟩, fun v => ⟨⟨v.1, v.2.le⟩, v.2⟩⟩
      have hstrict : Measure.map f (P.restrict {w | (h, w) ∈ Q}) = ρ.restrict (Set.Iio (d h : ℝ)) := by
        rw [← hclosed, Measure.restrict_map hfm measurableSet_Iio,
          Measure.restrict_restrict (measurableSet_Iio.preimage hfm), Set.inter_comm, hset]
      simp only [timeObs, waitObs, ha]
      change Measure.map f (P.restrict {w | (h, w) ∈ Q}) = _
      rw [hstrict]
      dsimp only [ρ]
      rw [restrict_withDensity measurableSet_Iio,
        Measure.restrict_restrict measurableSet_Iio]
      have hinterval : Set.Iio (d h : ℝ) ∩ Set.Ioc (0 : ℝ) (d h : ℝ) =
          Set.Ioo (0 : ℝ) (d h : ℝ) := by ext s; simp; grind
      rw [hinterval, ← withDensity_indicator measurableSet_Ioo]
      congr 1
      funext s
      simp [D, ha, Set.indicator, Set.mem_Ioo]

Exact contiguous compiled BODY region; every mathematical ingredient is derived internally.

4. Derive a uniform kernel mass bound internally

For every fixed abstract history, the density measure is the pushforward of P restricted to the strict finite event. Its mass on all real times is that event probability, at most1. The proved fiber equality transfers this bound to K(h,ℝ), including stopped records, d(h)=0 and unrealizable histories. C=1 supplies IsFiniteKernel. This bounds mass, not the pointwise density; no finite-wait guarantee, integrability provider or normalization is used.

\[K_d(h,\mathbb R)=P\{v:0<W(h_n,v_0)<d(h)\}\le1.\]
Corresponding Lean step
  have hmass (h : Hist) : K h Set.univ ≤ 1 := by
    rw [hK, ← hfiber]
    have hfm : Measurable (fun w : ℕ → ℝ => timeObs y xRef (h last, w 0)) :=
      ht.comp (measurable_const.prodMk (measurable_pi_apply 0))
    rw [Measure.map_apply hfm MeasurableSet.univ, Set.preimage_univ,
      Measure.restrict_apply MeasurableSet.univ, Set.univ_inter]
    exact prob_le_one
  have hfinite : IsFiniteKernel K := ⟨⟨1, ENNReal.one_lt_top, hmass⟩⟩

Exact contiguous compiled BODY region; every mathematical ingredient is derived internally.

5. Identify the actual joint finite measure

For arbitrary Borel C⊆Hist×ℝ, pull the actual restricted pushforward back through G(H,Y). L=G⁻¹(C)∩Q is Borel. Replace the joint history/tail law by μ⊗P and apply product-measure sections. The strict fixed-history fiber law replaces each section by D(h,s)ds. Nonnegative product integration gives ∫_C D d(μ⊗ds)=ν(C). Equality for all Borel C proves the joint map law. Total mass is at most1 because ν is a restricted pushforward of the actual probability P.

\[(X_n)_*(P|_{B_d})=\nu_d,\qquad B_d=\{0<W_n<d(H_n)\}.\]
Corresponding Lean step
  -- The actual complete history and unchanged unused tail have the product law.
  have hmap : Measure.map X (P.restrict B) = ν := by
    apply Measure.ext
    intro C hC
    let L : Set (Hist × (ℕ → ℝ)) := G ⁻¹' C ∩ Q
    have hL : MeasurableSet L := (hC.preimage hG).inter hQ
    calc
      Measure.map X (P.restrict B) C =
          (Measure.map (fun w => (H w, Y w)) P) L := by
        rw [Measure.map_apply hX hC, Measure.restrict_apply (hC.preimage hX),
          Measure.map_apply (hHm.prodMk hY) hL]
        rfl
      _ = (μ.prod P) L := by rw [hjoint]
      _ = ∫⁻ h : Hist, P {w : ℕ → ℝ | (h, w) ∈ L} ∂μ := Measure.prod_apply hL
      _ = ∫⁻ h : Hist, ((volume : Measure ℝ).withDensity (D h))
          ((fun s : ℝ => (h, s)) ⁻¹' C) ∂μ := by
        apply lintegral_congr
        intro h
        have hs : MeasurableSet ((fun s : ℝ => (h, s)) ⁻¹' C) :=
          hC.preimage (measurable_const.prodMk measurable_id)
        have htm : Measurable (fun w : ℕ → ℝ => timeObs y xRef (h last, w 0)) :=
          ht.comp (measurable_const.prodMk (measurable_pi_apply 0))
        rw [← hfiber, Measure.map_apply htm hs,
          Measure.restrict_apply (hs.preimage htm)]
        rfl
      _ = ∫⁻ h : Hist, (∫⁻ s : ℝ, C.indicator (fun p => D p.1 p.2) (h, s)) ∂μ := by
        apply lintegral_congr
        intro h
        have hs : MeasurableSet ((fun s : ℝ => (h, s)) ⁻¹' C) :=
          hC.preimage (measurable_const.prodMk measurable_id)
        rw [withDensity_apply _ hs, ← lintegral_indicator hs]
        rfl
      _ = ∫⁻ p in C, D p.1 p.2 ∂μ.prod (volume : Measure ℝ) := by
        exact (lintegral_prod (C.indicator (Function.uncurry D))
          (hD.indicator hC).aemeasurable).symm.trans (lintegral_indicator hC _)
      _ = ν C := (withDensity_apply _ hC).symm
  have hνmass : ν Set.univ ≤ 1 := by
    rw [← hmap, Measure.map_apply hX MeasurableSet.univ, Set.preimage_univ,
      Measure.restrict_apply MeasurableSet.univ, Set.univ_inter]
    exact prob_le_one

Exact contiguous compiled BODY region; every mathematical ingredient is derived internally.

6. Integrate every nonnegative joint test on every history event

Jointly Borel F gives jointly Borel F·D; nonnegative parameter integration makes its time integral Borel in h, allowing infinity. For arbitrary Borel A multiply F by the indicator of the first-coordinate event. Restrict/map nonnegative integration and the proved joint measure identity give its ν integral. The density formula and Tonelli yield ∫μ∫ds 1_A(h)F(h,s)D(h,s). The indicator formula gives the displayed history-restricted identity, including null A. No boundedness, integrability, positive conditioning probability, conditional representative or normalization enters.

\[\int_{B_d\cap\{H_n\in A\}}F(X_n)\,dP=\int_A\left(\int_{\mathbb R}F(h,s)D_d(h,s)\,ds\right)\mu_n(dh).\]
Corresponding Lean step
  refine ⟨hD, hK, hfinite, hmass, hB, hX, hmap, hνmass, ?_⟩
  intro F hF
  have hFD : Measurable (fun p : Hist × ℝ => F p * D p.1 p.2) := hF.mul hD
  refine ⟨hFD.lintegral_prod_right', ?_⟩
  intro A hA
  let f : Hist × ℝ → ℝ≥0∞ := (Prod.fst ⁻¹' A).indicator F
  have hm : Measurable f := hF.indicator (hA.preimage measurable_fst)
  calc
    (∫⁻ w in B ∩ H ⁻¹' A, F (X w) ∂P) =
        ∫⁻ w in B, f (X w) ∂P := by
      rw [Set.inter_comm B, ← Measure.restrict_restrict (hA.preimage hHm),
        ← lintegral_indicator (hA.preimage hHm)]
      apply lintegral_congr
      intro w
      simp [f, X, Set.indicator, and_comm]
    _ = ∫⁻ p, f p ∂ν := by rw [← hmap, lintegral_map hm hX]
    _ = ∫⁻ p : Hist × ℝ, f p * D p.1 p.2 ∂μ.prod (volume : Measure ℝ) := by
      change (∫⁻ p, f p ∂(μ.prod (volume : Measure ℝ)).withDensity (Function.uncurry D)) = _
      exact (lintegral_withDensity_eq_lintegral_mul _ hD hm).trans
        (lintegral_congr fun p => mul_comm _ _)
    _ = ∫⁻ h : Hist, (∫⁻ s : ℝ, f (h, s) * D h s) ∂μ :=
      lintegral_prod _ (hm.mul hD).aemeasurable
    _ = ∫⁻ h in A, (∫⁻ s : ℝ, F (h, s) * D h s) ∂μ := by
      rw [← lintegral_indicator hA]
      apply lintegral_congr
      intro h
      by_cases ha : h ∈ A
      · rw [Set.indicator_of_mem ha]
        apply lintegral_congr; intro s; simp [f, ha]
      · simp [f, ha]

Exact contiguous compiled BODY region; every mathematical ingredient is derived internally.

Lean verification

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

Lean proof · actual_conditional_next_wait_density

Retain actual definitions and derive joint Borel observables; Construct actual histories, strict guards and the genuine kernel; Restrict each deterministic fiber to strict positive finite waits; Derive a uniform kernel mass bound internally; Identify the actual joint finite measure; Integrate every nonnegative joint test on every history event

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_conditional_next_wait_density
    {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_conditional_next_wait_density_statement hα hαβ hV hH hη hβη := by
  classical
  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 S : E → (E × E) → (E × E) := fun xRef z =>
    (z.1, z.2 - (2 * inner ℝ z.2 (gradient V z.1 - gradient V xRef) /
      ‖gradient V z.1 - gradient V xRef‖ ^ 2) • (gradient V z.1 - gradient V xRef))
  let rate : E → (E × E) → ℝ := fun xRef z =>
    Real.sqrt η * max 0 (inner ℝ z.2 (gradient V z.1 - gradient V 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 next : E → E → ℝ≥0 → ((ℝ≥0 × (E × E)) ⊕ Unit) →
      ((ℝ≥0 × (E × E)) ⊕ Unit) := fun y xRef e r =>
    match r with
    | Sum.inr _ => Sum.inr ()
    | Sum.inl a =>
      if τ y xRef a.2 e = ⊤ then Sum.inr () else
        Sum.inl (a.1 + (τ y xRef a.2 e).untopD 0,
          S xRef (Φ y xRef (((τ y xRef a.2 e).untopD 0 : ℝ≥0) : ℝ) a.2))
  let record : E → E → (E × E) → (ℕ → ℝ≥0) → ℕ →
      ((ℝ≥0 × (E × E)) ⊕ Unit) := fun y xRef z₀ e n =>
    Nat.rec (Sum.inl (0, z₀)) (fun k r => next y xRef (e k) r) n
  let P : Measure (ℕ → ℝ) := Measure.infinitePi (fun _ : ℕ => expMeasure (1 : ℝ))
  let ε : (ℕ → ℝ) → ℕ → ℝ≥0 := fun w k => Real.toNNReal (w k)
  let history : E → E → (E × E) → (n : ℕ) → (ℕ → ℝ) →
      (Fin (n + 1) → ((ℝ≥0 × (E × E)) ⊕ Unit)) :=
    fun y xRef z₀ n w j => record y xRef z₀ (ε w) j.val
  let waitObs : E → E → (((ℝ≥0 × (E × E)) ⊕ Unit) × ℝ) → WithTop ℝ≥0 :=
    fun y xRef q => match q.1 with
      | Sum.inl a => τ y xRef a.2 (Real.toNNReal q.2)
      | Sum.inr _ => 0
  let timeObs : E → E → (((ℝ≥0 × (E × E)) ⊕ Unit) × ℝ) → ℝ :=
    fun y xRef q => ((waitObs y xRef q).untopD 0 : ℝ≥0)
  let density : E → E → (((ℝ≥0 × (E × E)) ⊕ Unit) × ℝ) → ℝ≥0∞ :=
    fun y xRef q => match q.1 with
      | Sum.inl a => ENNReal.ofReal (rate xRef (Φ y xRef q.2 a.2) *
          Real.exp (-Λ y xRef a.2 (Real.toNNReal q.2)))
      | Sum.inr _ => 0
  change
  ∀ y xRef : E, ∀ z₀ : E × E, ∀ n : ℕ,
    Measurable (waitObs y xRef) ∧ Measurable (density y xRef) ∧
    (∀ q, density y xRef q ≠ ⊤) ∧
    (∀ d : (Fin (n + 1) → ((ℝ≥0 × (E × E)) ⊕ Unit)) → ℝ≥0,
      Measurable d →
      let Hist := Fin (n + 1) → ((ℝ≥0 × (E × E)) ⊕ Unit)
      let last : Fin (n + 1) := ⟨n, Nat.lt_succ_self n⟩
      let H : (ℕ → ℝ) → Hist := history y xRef z₀ n
      let μ : Measure Hist := Measure.map H P
      let D : Hist → ℝ → ℝ≥0∞ := fun h s =>
        if 0 < s ∧ s < (d h : ℝ) then density y xRef (h last, s) else 0
      let K : Kernel Hist ℝ := (Kernel.const Hist (volume : Measure ℝ)).withDensity D
      let B : Set (ℕ → ℝ) := {w |
        (0 : WithTop ℝ≥0) < waitObs y xRef (record y xRef z₀ (ε w) n, w n) ∧
        waitObs y xRef (record y xRef z₀ (ε w) n, w n) <
          ((d (H w) : ℝ≥0) : WithTop ℝ≥0)}
      let X : (ℕ → ℝ) → Hist × ℝ := fun w =>
        (H w, timeObs y xRef (record y xRef z₀ (ε w) n, w n))
      let ν : Measure (Hist × ℝ) := (μ.prod (volume : Measure ℝ)).withDensity
        (fun p => D p.1 p.2)
      Measurable (Function.uncurry D) ∧
      (∀ h, K h = (volume : Measure ℝ).withDensity (D h)) ∧
      IsFiniteKernel K ∧ (∀ h, K h Set.univ ≤ 1) ∧
      MeasurableSet B ∧ Measurable X ∧
      Measure.map X (P.restrict B) = ν ∧ ν Set.univ ≤ 1 ∧
      (∀ F : Hist × ℝ → ℝ≥0∞, Measurable F →
        Measurable (fun h => ∫⁻ s : ℝ, F (h, s) * D h s) ∧
        (∀ A : Set Hist, MeasurableSet A →
          (∫⁻ w in B ∩ H ⁻¹' A, F (X w) ∂P) =
            ∫⁻ h in A, (∫⁻ s : ℝ, F (h, s) * D h s) ∂μ)))

  have hc := ActualHazardClock.actual_integrated_hazard_clock_laws hα hαβ hV hH hη hβη
  have hτ : Measurable (fun a : (E × E) × (E × E) × ℝ≥0 =>
      τ a.1.1 a.1.2 a.2.1 a.2.2) := hc.2.2.2.2.2.2.1
  have hΛ : Measurable (fun a : ((E × E) × (E × E)) × ℝ≥0 =>
      Λ a.1.1.1 a.1.1.2 a.1.2 a.2) := hc.2.1
  have hf := ActualHarmonicFlow.actual_harmonic_flow_laws hα hαβ hV hH hη hβη
  have hr := ActualBounceRate.actual_bounce_rate_energy_laws hα hαβ hV hH hη hβη
  have hi := AutoSamplingTheory.TechnicalLemmas.Probability.UnitExponentialProduct.unit_exponential_product_laws
  letI : IsProbabilityMeasure P := hi.1
  intro y xRef z₀ n
  let Rec := (ℝ≥0 × (E × E)) ⊕ Unit
  let Hist := Fin (n + 1) → Rec
  let last : Fin (n + 1) := ⟨n, Nat.lt_succ_self n⟩
  -- Total clock and density observables are jointly Borel, including stopped0.
  have hw : Measurable (waitObs y xRef) := by
    let e := MeasurableEquiv.sumProdDistrib (ℝ≥0 × (E × E)) Unit ℝ
    have hl : Measurable (fun q : (ℝ≥0 × (E × E)) × ℝ =>
        τ y xRef q.1.2 (Real.toNNReal q.2)) :=
      hτ.comp (f := fun q : (ℝ≥0 × (E × E)) × ℝ =>
        ((y, xRef), q.1.2, Real.toNNReal q.2))
        (measurable_const.prodMk (measurable_fst.snd.prodMk
          (measurable_real_toNNReal.comp measurable_snd)))
    have heq : waitObs y xRef = (Sum.elim
        (fun q : (ℝ≥0 × (E × E)) × ℝ => τ y xRef q.1.2 (Real.toNNReal q.2))
        (fun _ : Unit × ℝ => (0 : WithTop ℝ≥0))) ∘ e := by
      funext q; rcases q with ⟨a | a, t⟩ <;> rfl
    rw [heq]
    exact (hl.sumElim (measurable_const : Measurable
      (fun _ : Unit × ℝ => (0 : WithTop ℝ≥0)))).comp e.measurable
  have ht : Measurable (timeObs y xRef) :=
    measurable_subtype_coe.comp (hw.untopD 0)
  have hρ : Measurable (density y xRef) := by
    let e := MeasurableEquiv.sumProdDistrib (ℝ≥0 × (E × E)) Unit ℝ
    have hφ : Measurable (fun q : (ℝ≥0 × (E × E)) × ℝ => Φ y xRef q.2 q.1.2) :=
      hf.1.measurable.comp (f := fun q : (ℝ≥0 × (E × E)) × ℝ =>
        ((y, xRef), q.2, q.1.2))
        (measurable_const.prodMk (measurable_snd.prodMk measurable_fst.snd))
    have hl : Measurable (fun q : (ℝ≥0 × (E × E)) × ℝ =>
        ENNReal.ofReal (rate xRef (Φ y xRef q.2 q.1.2) *
          Real.exp (-Λ y xRef q.1.2 (Real.toNNReal q.2)))) := by
      have hrateArgs : Measurable (fun q : (ℝ≥0 × (E × E)) × ℝ =>
          (xRef, Φ y xRef q.2 q.1.2)) :=
        (measurable_const : Measurable
          (fun _ : (ℝ≥0 × (E × E)) × ℝ => xRef)).prodMk hφ
      have hrate : Measurable (fun q : (ℝ≥0 × (E × E)) × ℝ =>
          rate xRef (Φ y xRef q.2 q.1.2)) := hr.2.1.measurable.comp hrateArgs
      have hΛArgs : Measurable (fun q : (ℝ≥0 × (E × E)) × ℝ =>
          (((y, xRef), q.1.2), Real.toNNReal q.2)) :=
        (((measurable_const : Measurable
          (fun _ : (ℝ≥0 × (E × E)) × ℝ => (y, xRef))).prodMk
          measurable_fst.snd).prodMk (measurable_real_toNNReal.comp measurable_snd))
      have hhazard : Measurable (fun q : (ℝ≥0 × (E × E)) × ℝ =>
          Λ y xRef q.1.2 (Real.toNNReal q.2)) := hΛ.comp hΛArgs
      exact (hrate.mul hhazard.neg.exp).ennreal_ofReal
    have heq : density y xRef = (Sum.elim
        (fun q : (ℝ≥0 × (E × E)) × ℝ => ENNReal.ofReal
          (rate xRef (Φ y xRef q.2 q.1.2) *
            Real.exp (-Λ y xRef q.1.2 (Real.toNNReal q.2))))
        (fun _ : Unit × ℝ => (0 : ℝ≥0∞))) ∘ e := by
      funext q; rcases q with ⟨a | a, t⟩ <;> rfl
    rw [heq]
    exact (hl.sumElim (measurable_const : Measurable
      (fun _ : Unit × ℝ => (0 : ℝ≥0∞)))).comp e.measurable
  have hρfin (q : Rec × ℝ) : density y xRef q ≠ ⊤ := by
    rcases q with ⟨a | a, t⟩
    · exact ENNReal.ofReal_ne_top
    · exact ENNReal.zero_ne_top
  refine ⟨hw, hρ, hρfin, ?_⟩
  intro d hd
  let H : (ℕ → ℝ) → Hist := history y xRef z₀ n
  let Y : (ℕ → ℝ) → (ℕ → ℝ) := fun w k => w (n + k)
  let μ : Measure Hist := Measure.map H P
  let D : Hist → ℝ → ℝ≥0∞ := fun h s =>
    if 0 < s ∧ s < (d h : ℝ) then density y xRef (h last, s) else 0
  let K : Kernel Hist ℝ := (Kernel.const Hist (volume : Measure ℝ)).withDensity D
  let W : Hist × (ℕ → ℝ) → WithTop ℝ≥0 :=
    fun p => waitObs y xRef (p.1 last, p.2 0)
  let Q : Set (Hist × (ℕ → ℝ)) := {p |
    (0 : WithTop ℝ≥0) < W p ∧ W p < ((d p.1 : ℝ≥0) : WithTop ℝ≥0)}
  let G : Hist × (ℕ → ℝ) → Hist × ℝ :=
    fun p => (p.1, timeObs y xRef (p.1 last, p.2 0))
  let B : Set (ℕ → ℝ) := {w |
    (0 : WithTop ℝ≥0) < waitObs y xRef (record y xRef z₀ (ε w) n, w n) ∧
    waitObs y xRef (record y xRef z₀ (ε w) n, w n) <
      ((d (H w) : ℝ≥0) : WithTop ℝ≥0)}
  let X : (ℕ → ℝ) → Hist × ℝ := fun w =>
    (H w, timeObs y xRef (record y xRef z₀ (ε w) n, w n))
  let ν : Measure (Hist × ℝ) := (μ.prod (volume : Measure ℝ)).withDensity
    (fun p => D p.1 p.2)
  have hp := ActualFiniteHistoryTailLaw.actual_finite_history_tail_law
    hα hαβ hV hH hη hβη y xRef z₀ n
  have hHm : Measurable H := hp.1
  have hY : Measurable Y := hp.2.1
  have hjoint : Measure.map (fun w => (H w, Y w)) P = μ.prod P := hp.2.2.2.2.2.2.1
  letI : IsProbabilityMeasure μ := Measure.isProbabilityMeasure_map hHm.aemeasurable
  have hargs : Measurable (fun p : Hist × (ℕ → ℝ) => (p.1 last, p.2 0)) :=
    ((measurable_pi_apply last).comp measurable_fst).prodMk
      ((measurable_pi_apply 0).comp measurable_snd)
  have hW : Measurable W := hw.comp hargs
  have hQ : MeasurableSet Q :=
    (measurableSet_lt measurable_const hW).inter
      (measurableSet_lt hW (WithTop.measurable_coe.comp (hd.comp measurable_fst)))
  have hG : Measurable G := measurable_fst.prodMk (ht.comp hargs)
  have hXeq : X = G ∘ (fun w => (H w, Y w)) := rfl
  have hBeq : B = (fun w => (H w, Y w)) ⁻¹' Q := rfl
  have hB : MeasurableSet B := hBeq ▸ hQ.preimage (hHm.prodMk hY)
  have hX : Measurable X := hXeq ▸ hG.comp (hHm.prodMk hY)
  have hD : Measurable (Function.uncurry D) := by
    have hguard : MeasurableSet {p : Hist × ℝ | 0 < p.2 ∧ p.2 < (d p.1 : ℝ)} :=
      (measurableSet_lt measurable_const measurable_snd).inter
        (measurableSet_lt measurable_snd (measurable_subtype_coe.comp (hd.comp measurable_fst)))
    exact (hρ.comp (((measurable_pi_apply last).comp measurable_fst).prodMk
      measurable_snd)).piecewise hguard measurable_const
  have hK (h : Hist) : K h = (volume : Measure ℝ).withDensity (D h) :=
    Kernel.withDensity_apply _ hD h
  -- Restrict the deterministic Ioc law by Iio: strict endpoints on BOTH sides.
  have hfiber (h : Hist) :
      Measure.map (fun w : ℕ → ℝ => timeObs y xRef (h last, w 0))
        (P.restrict {w | (h, w) ∈ Q}) = (volume : Measure ℝ).withDensity (D h) := by
    cases ha : h last with
    | inr a =>
      simp [Q, W, waitObs, timeObs, density, D, ha]
    | inl a =>
      let U : (ℕ → ℝ) → WithTop ℝ≥0 := fun w => τ y xRef a.2 (ε w 0)
      let f : (ℕ → ℝ) → ℝ := fun w => ((U w).untopD 0 : ℝ≥0)
      let A : Set (ℕ → ℝ) := {w | (0 : WithTop ℝ≥0) < U w ∧
        U w ≤ ((d h : ℝ≥0) : WithTop ℝ≥0)}
      let ρ : Measure ℝ := (volume.restrict (Set.Ioc (0 : ℝ) (d h : ℝ))).withDensity
        (fun s => density y xRef (Sum.inl a, s))
      have hfirst := ActualFiniteFirstEventLaw.actual_finite_first_event_law
        hα hαβ hV hH hη hβη y xRef a.2
      have hfm : Measurable f := hfirst.2.1
      have hclosed : Measure.map f (P.restrict A) = ρ := (hfirst.2.2.2 (d h)).2.1
      have hset : A ∩ f ⁻¹' Set.Iio (d h : ℝ) = {w | (h, w) ∈ Q} := by
        ext w
        simp only [Set.mem_inter_iff, A, Set.mem_ofPred_eq, Set.mem_preimage,
          Set.mem_Iio, Q, W, waitObs, ha]
        change ((0 : WithTop ℝ≥0) < U w ∧ U w ≤ ↑(d h)) ∧
          (((U w).untopD 0 : ℝ≥0) : ℝ) < (d h : ℝ) ↔
            (0 : WithTop ℝ≥0) < U w ∧ U w < ↑(d h)
        cases hu : U w using WithTop.recTopCoe with
        | top =>
          simp only [WithTop.not_top_le_coe, and_false, false_and]
          exact iff_of_false id (fun hs => (not_lt_of_ge le_top) hs.2)
        | coe s =>
          have hz : (0 : WithTop ℝ≥0) < (s : WithTop ℝ≥0) ↔ 0 < s := by
            have hz0 : ((0 : ℝ≥0) : WithTop ℝ≥0) < (s : WithTop ℝ≥0) ↔
                (0 : ℝ≥0) < s := WithTop.coe_lt_coe
            simpa only [WithTop.coe_zero] using hz0
          simp only [WithTop.untopD_coe, WithTop.coe_le_coe,
            WithTop.coe_lt_coe, NNReal.coe_lt_coe, hz]
          exact ⟨fun v => ⟨v.1.1, v.2⟩, fun v => ⟨⟨v.1, v.2.le⟩, v.2⟩⟩
      have hstrict : Measure.map f (P.restrict {w | (h, w) ∈ Q}) = ρ.restrict (Set.Iio (d h : ℝ)) := by
        rw [← hclosed, Measure.restrict_map hfm measurableSet_Iio,
          Measure.restrict_restrict (measurableSet_Iio.preimage hfm), Set.inter_comm, hset]
      simp only [timeObs, waitObs, ha]
      change Measure.map f (P.restrict {w | (h, w) ∈ Q}) = _
      rw [hstrict]
      dsimp only [ρ]
      rw [restrict_withDensity measurableSet_Iio,
        Measure.restrict_restrict measurableSet_Iio]
      have hinterval : Set.Iio (d h : ℝ) ∩ Set.Ioc (0 : ℝ) (d h : ℝ) =
          Set.Ioo (0 : ℝ) (d h : ℝ) := by ext s; simp; grind
      rw [hinterval, ← withDensity_indicator measurableSet_Ioo]
      congr 1
      funext s
      simp [D, ha, Set.indicator, Set.mem_Ioo]
  have hmass (h : Hist) : K h Set.univ ≤ 1 := by
    rw [hK, ← hfiber]
    have hfm : Measurable (fun w : ℕ → ℝ => timeObs y xRef (h last, w 0)) :=
      ht.comp (measurable_const.prodMk (measurable_pi_apply 0))
    rw [Measure.map_apply hfm MeasurableSet.univ, Set.preimage_univ,
      Measure.restrict_apply MeasurableSet.univ, Set.univ_inter]
    exact prob_le_one
  have hfinite : IsFiniteKernel K := ⟨⟨1, ENNReal.one_lt_top, hmass⟩⟩
  -- The actual complete history and unchanged unused tail have the product law.
  have hmap : Measure.map X (P.restrict B) = ν := by
    apply Measure.ext
    intro C hC
    let L : Set (Hist × (ℕ → ℝ)) := G ⁻¹' C ∩ Q
    have hL : MeasurableSet L := (hC.preimage hG).inter hQ
    calc
      Measure.map X (P.restrict B) C =
          (Measure.map (fun w => (H w, Y w)) P) L := by
        rw [Measure.map_apply hX hC, Measure.restrict_apply (hC.preimage hX),
          Measure.map_apply (hHm.prodMk hY) hL]
        rfl
      _ = (μ.prod P) L := by rw [hjoint]
      _ = ∫⁻ h : Hist, P {w : ℕ → ℝ | (h, w) ∈ L} ∂μ := Measure.prod_apply hL
      _ = ∫⁻ h : Hist, ((volume : Measure ℝ).withDensity (D h))
          ((fun s : ℝ => (h, s)) ⁻¹' C) ∂μ := by
        apply lintegral_congr
        intro h
        have hs : MeasurableSet ((fun s : ℝ => (h, s)) ⁻¹' C) :=
          hC.preimage (measurable_const.prodMk measurable_id)
        have htm : Measurable (fun w : ℕ → ℝ => timeObs y xRef (h last, w 0)) :=
          ht.comp (measurable_const.prodMk (measurable_pi_apply 0))
        rw [← hfiber, Measure.map_apply htm hs,
          Measure.restrict_apply (hs.preimage htm)]
        rfl
      _ = ∫⁻ h : Hist, (∫⁻ s : ℝ, C.indicator (fun p => D p.1 p.2) (h, s)) ∂μ := by
        apply lintegral_congr
        intro h
        have hs : MeasurableSet ((fun s : ℝ => (h, s)) ⁻¹' C) :=
          hC.preimage (measurable_const.prodMk measurable_id)
        rw [withDensity_apply _ hs, ← lintegral_indicator hs]
        rfl
      _ = ∫⁻ p in C, D p.1 p.2 ∂μ.prod (volume : Measure ℝ) := by
        exact (lintegral_prod (C.indicator (Function.uncurry D))
          (hD.indicator hC).aemeasurable).symm.trans (lintegral_indicator hC _)
      _ = ν C := (withDensity_apply _ hC).symm
  have hνmass : ν Set.univ ≤ 1 := by
    rw [← hmap, Measure.map_apply hX MeasurableSet.univ, Set.preimage_univ,
      Measure.restrict_apply MeasurableSet.univ, Set.univ_inter]
    exact prob_le_one
  refine ⟨hD, hK, hfinite, hmass, hB, hX, hmap, hνmass, ?_⟩
  intro F hF
  have hFD : Measurable (fun p : Hist × ℝ => F p * D p.1 p.2) := hF.mul hD
  refine ⟨hFD.lintegral_prod_right', ?_⟩
  intro A hA
  let f : Hist × ℝ → ℝ≥0∞ := (Prod.fst ⁻¹' A).indicator F
  have hm : Measurable f := hF.indicator (hA.preimage measurable_fst)
  calc
    (∫⁻ w in B ∩ H ⁻¹' A, F (X w) ∂P) =
        ∫⁻ w in B, f (X w) ∂P := by
      rw [Set.inter_comm B, ← Measure.restrict_restrict (hA.preimage hHm),
        ← lintegral_indicator (hA.preimage hHm)]
      apply lintegral_congr
      intro w
      simp [f, X, Set.indicator, and_comm]
    _ = ∫⁻ p, f p ∂ν := by rw [← hmap, lintegral_map hm hX]
    _ = ∫⁻ p : Hist × ℝ, f p * D p.1 p.2 ∂μ.prod (volume : Measure ℝ) := by
      change (∫⁻ p, f p ∂(μ.prod (volume : Measure ℝ)).withDensity (Function.uncurry D)) = _
      exact (lintegral_withDensity_eq_lintegral_mul _ hD hm).trans
        (lintegral_congr fun p => mul_comm _ _)
    _ = ∫⁻ h : Hist, (∫⁻ s : ℝ, f (h, s) * D h s) ∂μ :=
      lintegral_prod _ (hm.mul hD).aemeasurable
    _ = ∫⁻ h in A, (∫⁻ s : ℝ, F (h, s) * D h s) ∂μ := by
      rw [← lintegral_indicator hA]
      apply lintegral_congr
      intro h
      by_cases ha : h ∈ A
      · rw [Set.indicator_of_mem ha]
        apply lintegral_congr; intro s; simp [f, ha]
      · simp [f, ha]

end
end AutoSamplingTheory.ExampleCases.ProximalBPS.ActualConditionalNextWaitDensity

Exact module and namespace context

Scope and omitted-condition boundaries
  • Original six analytic hypotheses unchanged. Fixed deterministic depth n, complete stopped actual history, raw unused Exp1 coordinate n. Fixed Borel finite-valued cutoff d may be unbounded across histories. Strict positive finite wait guard 0<tau<d(H), no endpoint-mass equivalence or no-atom premise. Real Lebesgue time on Ioo is the existing86 Ioc density measure restricted by Iio. Stopped histories have zero kernel; infinity mass is retained outside this finite component without normalization. All abstract histories, null A, n0, rank0, d0 and all jointly Borel ENNReal tests included. Only density component of S87-I5 closes if proved; ordered-time iteration, final survival/path factor, full A7/global G86-11, physical-time residual memorylessness/random restart/Markovness, nonexplosion/invariance/hypocoercivity/implementation/errors/unbounded costs/main/composition/wholepaper/Goal remain OPEN. Survival88 is adjacent, not a fabricated AND parent.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

  • Kernel.withDensity
  • Kernel.withDensity_apply
  • IsFiniteKernel
  • MeasurableEquiv.sumProdDistrib
  • Measurable.sumElim
  • WithTop.measurable_coe
  • Measurable.untopD
  • Measure.restrict_map
  • Measure.restrict_restrict
  • restrict_withDensity
  • withDensity_indicator
  • Measure.map_apply
  • Measure.prod_apply
  • lintegral_prod
  • Measurable.lintegral_prod_right'
  • lintegral_withDensity_eq_lintegral_mul
  • lintegral_map
  • lintegral_indicator

Mathematical sources

  • Chen-Chewi-Lu-Zhang arXiv2609.06905v1 Appendix A.1 (A.1),(A.2),(A.7) strict ordered-event density factor and Appendix A.2 joint Borel recursion; attributed ASTIS source-implicit completion. — Original six analytic hypotheses unchanged. Fixed deterministic depth n, complete stopped actual history, raw unused Exp1 coordinate n. Fixed Borel finite-valued cutoff d may be unbounded across histories. Strict positive finite wait guard 0<tau<d(H), no endpoint-mass equivalence or no-atom premise. Real Lebesgue time on Ioo is the existing86 Ioc density measure restricted by Iio. Stopped histories have zero kernel; infinity mass is retained outside this finite component without normalization. All abstract histories, null A, n0, rank0, d0 and all jointly Borel ENNReal tests included. Only density component of S87-I5 closes if proved; ordered-time iteration, final survival/path factor, full A7/global G86-11, physical-time residual memorylessness/random restart/Markovness, nonexplosion/invariance/hypocoercivity/implementation/errors/unbounded costs/main/composition/wholepaper/Goal remain OPEN. Survival88 is adjacent, not a fabricated AND parent.

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