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

ActualConditionalNextWaitSurvival: 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 next-wait survival
Samplinglib mathematical lesson

Actual PBPS conditional next-wait survival

AutoSamplingTheory.ExampleCases.ProximalBPS.ActualConditionalNextWaitSurvival.actual_conditional_next_wait_survival · 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 n≥0 let H_n(w)=(R_j(ε(w)))_(0≤j≤n)∈Hist_n=D^(Fin(n+1)), and let μ_n=(H_n)_*P. Thus the last record R_n consumes only raw clocks k<n, and w_n is the next unused clock. Take any Borel function d:Hist_n→[0,∞); each d(h) is finite but the function need not be bounded. Define L(r,u,e) to mean u<τ_z(max(e,0)) when r=live(T,z), and false when r=stopped. Define q(r,u)=exp(−Λ_z(u)) when r=live(T,z), and zero when r=stopped. The event B_d={(h,v)∈Hist_n×ℝ^ℕ:L(h_n,d(h),v_0)} is Borel. The weight q_d(h)=q(h_n,d(h)) is Borel and 0≤q_d(h)≤1 for every history h. For every Borel A⊆Hist_n, P{w:H_n(w)∈A and L(R_n(ε(w)),d(H_n(w)),w_n)}=∫_A q_d(h) μ_n(dh). All conclusions hold for every deterministic y,r,z₀,n and admissible d,A under the same six standing analytic hypotheses. No positivity of μ_n(A), boundedness of d, finite-wait assumption or extra regularity/independence/conditional-law provider is required. Live histories whose next wait is infinite survive every finite d(h); stopped histories have zero weight and no fictitious phase or wait in the statement. The case n=0, null events, zero rates and dimension zero are included. Borel d and A specify admissible deterministic tests rather than additional analytic hypotheses. This is an attributed ASTIS completion of the history-dependent conditional survival ingredient implicit in AppendixA.1(A.7), using the actual recursion. Conditional finite-wait densities, ordered-time disintegration and iteration, final path factor assembly, full(A.7), physical-time residual memorylessness, random stopping/restart/Markovness, reversal, invariance, all-L² contraction, implementation error/cost, main results and actual-input composition remain separate obligations.

\[P\{H_n\in A,\ L(R_n,d(H_n),w_n)\}=\int_A q(h_n,d(h))\,\mu_n(dh).\]
Lean statement · actual_conditional_next_wait_survival

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 n≥0 let H_n(w)=(R_j(ε(w)))_(0≤j≤n)∈Hist_n=D^(Fin(n+1)), and let μ_n=(H_n)_*P. Thus the last record R_n consumes only raw clocks k<n, and w_n is the next unused clock. Take any Borel function d:Hist_n→[0,∞); each d(h) is finite but the function need not be bounded. Define L(r,u,e) to mean u<τ_z(max(e,0)) when r=live(T,z), and false when r=stopped. Define q(r,u)=exp(−Λ_z(u)) when r=live(T,z), and zero when r=stopped. The event B_d={(h,v)∈Hist_n×ℝ^ℕ:L(h_n,d(h),v_0)} is Borel. The weight q_d(h)=q(h_n,d(h)) is Borel and 0≤q_d(h)≤1 for every history h. For every Borel A⊆Hist_n, P{w:H_n(w)∈A and L(R_n(ε(w)),d(H_n(w)),w_n)}=∫_A q_d(h) μ_n(dh). All conclusions hold for every deterministic y,r,z₀,n and admissible d,A under the same six standing analytic hypotheses. No positivity of μ_n(A), boundedness of d, finite-wait assumption or extra regularity/independence/conditional-law provider is required. Live histories whose next wait is infinite survive every finite d(h); stopped histories have zero weight and no fictitious phase or wait in the statement. The case n=0, null events, zero rates and dimension zero are included. Borel d and A specify admissible deterministic tests rather than additional analytic hypotheses. This is an attributed ASTIS completion of the history-dependent conditional survival ingredient implicit in AppendixA.1(A.7), using the actual recursion. Conditional finite-wait densities, ordered-time disintegration and iteration, final path factor assembly, full(A.7), physical-time residual memorylessness, random stopping/restart/Markovness, reversal, invariance, all-L² contraction, implementation error/cost, main results and actual-input composition remain separate obligations.

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_survival
    {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_survival_statement hα hαβ hV hH hη hβη

Exact module and namespace context

Full Lean proposition (definition) · actual_conditional_next_wait_survival_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_survival_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 liveSurvival : E → E → ((ℝ≥0 × (E × E)) ⊕ Unit) → ℝ≥0 → ℝ → Prop :=
      fun y xRef r u e => match r with
        | Sum.inl a => (u : WithTop ℝ≥0) < τ y xRef a.2 (Real.toNNReal e)
        | Sum.inr _ => False
    let survivalWeight : E → E → ((ℝ≥0 × (E × E)) ⊕ Unit) → ℝ≥0 → ℝ≥0∞ :=
      fun y xRef r u => match r with
        | Sum.inl a => ENNReal.ofReal (Real.exp (-Λ y xRef a.2 u))
        | Sum.inr _ => 0
    ∀ y xRef : E, ∀ z₀ : E × E, ∀ n : ℕ,
      ∀ d : (Fin (n + 1) → ((ℝ≥0 × (E × E)) ⊕ Unit)) → ℝ≥0,
      Measurable d →
      MeasurableSet {p : (Fin (n + 1) → ((ℝ≥0 × (E × E)) ⊕ Unit)) × (ℕ → ℝ) |
        liveSurvival y xRef (p.1 ⟨n, Nat.lt_succ_self n⟩) (d p.1) (p.2 0)} ∧
      Measurable (fun h : Fin (n + 1) → ((ℝ≥0 × (E × E)) ⊕ Unit) =>
        survivalWeight y xRef (h ⟨n, Nat.lt_succ_self n⟩) (d h)) ∧
      (∀ h : Fin (n + 1) → ((ℝ≥0 × (E × E)) ⊕ Unit),
        survivalWeight y xRef (h ⟨n, Nat.lt_succ_self n⟩) (d h) ≤ 1) ∧
      (∀ A : Set (Fin (n + 1) → ((ℝ≥0 × (E × E)) ⊕ Unit)), MeasurableSet A →
        P {w : ℕ → ℝ | history y xRef z₀ n w ∈ A ∧
          liveSurvival y xRef (record y xRef z₀ (ε w) n)
            (d (history y xRef z₀ n w)) (w n)} =
        ∫⁻ h in A, survivalWeight y xRef (h ⟨n, Nat.lt_succ_self n⟩) (d h)
          ∂(Measure.map (history y xRef z₀ n) P))


set_option maxHeartbeats 1000000 in

Exact module and namespace context

Proof roadmap

  1. 1Keep actual definitions and consume verified producers

    Retain the actual flow, reflection, intensity, integrated hazard, infinity-guarded crossing recursion and independent Exp(1) input. The existing hazard-clock theorem supplies joint Borel Λ and τ, nonnegative Λ and deterministic-state survival. The exponential-product theorem supplies P probability and each coordinate law. The finite-history theorem supplies Borel H_n,Y_n and their exact joint law μ_n⊗P. Its raw tail Y_n starts at n, hence Y_n(w)_0=w_n. None of these ingredients is an added premise.

  2. 2Derive the joint survival event measurability

    Distribute the Borel record sum across the raw clock coordinate. On live records the wait observable is the composition of the joint Borel τ with the phase projection and e↦max(e,0); on the stopped summand use the zero observable solely for this proof. Since u≥0, u<0 is false, so this auxiliary observable gives exactly L, never a new stopped phase or algorithm transition. Compose with the Borel last-history projection, d and tail coordinate0. Strict comparison in [0,∞] is Borel, proving B_d is Borel.

  3. 3Derive the Borel bounded survival weight

    Distribute the record sum across duration. On the live summand joint Borel Λ followed by x↦exp(−x) and inclusion into the extended nonnegative reals is Borel; on the stopped summand the weight is zero. Compose with h↦(h_n,d(h)). Nonnegativity Λ_z(u)≥0 gives exp(−Λ_z(u))≤1. Thus every q_d(h) lies in [0,1], even when d as a function is unbounded. This bound is derived internally.

  4. 4Evaluate each fixed-history survival fiber

    Fix a history h. For a stopped last record the fiber is empty and its P-measure is zero. For a live last record z, push raw coordinate0 forward under P to Exp(1), then push that law through e↦τ_z(max(e,0)). The existing hazard-clock theorem identifies the real probability of (d(h),∞] with exp(−Λ_z(d(h))). Its pushed law is a probability measure, so conversion to an extended nonnegative measure loses no mass. This is a pointwise identity for every fixed h and its d(h), not substitution into separate almost-everywhere statements indexed by fixed times.

  5. 5Integrate over the actual history law without normalization

    For Borel A let C={(h,v):h∈A and (h,v)∈B_d}, a Borel product-space event. Its pullback under (H_n,Y_n) is exactly the desired actual-clock event. Replace the pushforward by μ_n⊗P and apply the product-measure section formula. The section has mass q_d(h) on A and zero off A. Its integral is the integral of the indicator of A times q_d, hence ∫_A q_d dμ_n. No division by μ_n(A), regular conditional distribution or bounded duration assumption 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 original analytic hypotheses are α>0, α≤β, V∈C², α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for every x,v, η>0, and βη≤1; α,β≥0.
  • y,r,z₀ and event depth n are deterministic and universally quantified. P and the actual stopped recursion are literal definitions.
  • d is any Borel finite-valued nonnegative duration function of the whole finite history; A is any Borel history event. These classify test objects. d may be unbounded and μ_n(A) may vanish.
  • No state measurability, independence, regular conditional law, density or integrability estimate is supplied as a premise. Stopped records are guarded; live infinite waits and zero rates are permitted.

Mathematical proof

1. Keep actual definitions and consume verified producers

Retain the actual flow, reflection, intensity, integrated hazard, infinity-guarded crossing recursion and independent Exp(1) input. The existing hazard-clock theorem supplies joint Borel Λ and τ, nonnegative Λ and deterministic-state survival. The exponential-product theorem supplies P probability and each coordinate law. The finite-history theorem supplies Borel H_n,Y_n and their exact joint law μ_n⊗P. Its raw tail Y_n starts at n, hence Y_n(w)_0=w_n. None of these ingredients is an added premise.

\[(H_n,Y_n)_*P=\mu_n\otimes P,\qquad Y_n(w)_0=w_n.\]
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 liveSurvival : E → E → ((ℝ≥0 × (E × E)) ⊕ Unit) → ℝ≥0 → ℝ → Prop :=
    fun y xRef r u e => match r with
      | Sum.inl a => (u : WithTop ℝ≥0) < τ y xRef a.2 (Real.toNNReal e)
      | Sum.inr _ => False
  let survivalWeight : E → E → ((ℝ≥0 × (E × E)) ⊕ Unit) → ℝ≥0 → ℝ≥0∞ :=
    fun y xRef r u => match r with
      | Sum.inl a => ENNReal.ofReal (Real.exp (-Λ y xRef a.2 u))
      | Sum.inr _ => 0
  change
  ∀ y xRef : E, ∀ z₀ : E × E, ∀ n : ℕ,
    ∀ d : (Fin (n + 1) → ((ℝ≥0 × (E × E)) ⊕ Unit)) → ℝ≥0,
    Measurable d →
    MeasurableSet {p : (Fin (n + 1) → ((ℝ≥0 × (E × E)) ⊕ Unit)) × (ℕ → ℝ) |
      liveSurvival y xRef (p.1 ⟨n, Nat.lt_succ_self n⟩) (d p.1) (p.2 0)} ∧
    Measurable (fun h : Fin (n + 1) → ((ℝ≥0 × (E × E)) ⊕ Unit) =>
      survivalWeight y xRef (h ⟨n, Nat.lt_succ_self n⟩) (d h)) ∧
    (∀ h : Fin (n + 1) → ((ℝ≥0 × (E × E)) ⊕ Unit),
      survivalWeight y xRef (h ⟨n, Nat.lt_succ_self n⟩) (d h) ≤ 1) ∧
    (∀ A : Set (Fin (n + 1) → ((ℝ≥0 × (E × E)) ⊕ Unit)), MeasurableSet A →
      P {w : ℕ → ℝ | history y xRef z₀ n w ∈ A ∧
        liveSurvival y xRef (record y xRef z₀ (ε w) n)
          (d (history y xRef z₀ n w)) (w n)} =
      ∫⁻ h in A, survivalWeight y xRef (h ⟨n, Nat.lt_succ_self n⟩) (d h)
        ∂(Measure.map (history y xRef z₀ n) P))

  have hh := ActualHazardClock.actual_integrated_hazard_clock_laws hα hαβ hV hH hη hβη
  rcases hh with ⟨hΛc, hΛm, hInt, hΛpos, hcross, hfinite, hτm, hSurv, hcap, hfloor⟩
  have hτtyped : Measurable (fun a : (E × E) × (E × E) × ℝ≥0 =>
      τ a.1.1 a.1.2 a.2.1 a.2.2) := hτm
  have hΛtyped : Measurable (fun a : ((E × E) × (E × E)) × ℝ≥0 =>
      Λ a.1.1.1 a.1.1.2 a.1.2 a.2) := hΛm
  have hi := AutoSamplingTheory.TechnicalLemmas.Probability.UnitExponentialProduct.unit_exponential_product_laws
  letI : IsProbabilityMeasure P := hi.1
  letI : IsProbabilityMeasure (expMeasure (1 : ℝ)) :=
    isProbabilityMeasure_expMeasure zero_lt_one
  intro y xRef z₀ n d hd
  let D := ((ℝ≥0 × (E × E)) ⊕ Unit)
  let Hist := Fin (n + 1) → D
  let last : Fin (n + 1) := ⟨n, Nat.lt_succ_self n⟩
  let H : (ℕ → ℝ) → Hist := history y xRef z₀ n
  let Y : (ℕ → ℝ) → (ℕ → ℝ) := fun w k => w (n + k)
  have hp := ActualFiniteHistoryTailLaw.actual_finite_history_tail_law
    hα hαβ hV hH hη hβη y xRef z₀ n
  have hH : Measurable H := hp.1
  have hY : Measurable Y := hp.2.1
  have hjoint : Measure.map (fun w => (H w, Y w)) P =
      (Measure.map H P).prod P := hp.2.2.2.2.2.2.1

Exact contiguous compiled BODY region; all proof ingredients are derived, not added source premises.

2. Derive the joint survival event measurability

Distribute the Borel record sum across the raw clock coordinate. On live records the wait observable is the composition of the joint Borel τ with the phase projection and e↦max(e,0); on the stopped summand use the zero observable solely for this proof. Since u≥0, u<0 is false, so this auxiliary observable gives exactly L, never a new stopped phase or algorithm transition. Compose with the Borel last-history projection, d and tail coordinate0. Strict comparison in [0,∞] is Borel, proving B_d is Borel.

\[L(r,u,e)\iff u<\operatorname{waitObs}(r,e),\qquad u\ge0.\]
Corresponding Lean step
  -- A stopped record has no next wait. The following zero-valued observable
  -- is only used under a strict nonnegative-duration comparison, hence false.
  let waitObs : D × ℝ → WithTop ℝ≥0 := fun q => match q.1 with
    | Sum.inl a => τ y xRef a.2 (Real.toNNReal q.2)
    | Sum.inr _ => 0
  have hwait : Measurable waitObs := 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τtyped.comp (f := 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 heq : waitObs = (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 hwaitEq (r : D) (u : ℝ≥0) (e : ℝ) :
      liveSurvival y xRef r u e ↔ (u : WithTop ℝ≥0) < waitObs (r, e) := by
    cases r with
    | inl a => rfl
    | inr a =>
      simp only [liveSurvival, waitObs, false_iff]
      exact not_lt.mpr (WithTop.coe_le_coe.mpr (show (0 : ℝ≥0) ≤ u from zero_le))
  let B : Set (Hist × (ℕ → ℝ)) := {p |
    liveSurvival y xRef (p.1 last) (d p.1) (p.2 0)}
  have hB : MeasurableSet B := by
    have hm := measurableSet_lt (WithTop.measurable_coe.comp (hd.comp measurable_fst))
      (hwait.comp (f := fun p : Hist × (ℕ → ℝ) => (p.1 last, p.2 0))
        (((measurable_pi_apply last).comp measurable_fst).prodMk
        ((measurable_pi_apply 0).comp measurable_snd)))
    simpa only [B, hwaitEq, Function.comp_def] using hm

Exact contiguous compiled BODY region; all proof ingredients are derived, not added source premises.

3. Derive the Borel bounded survival weight

Distribute the record sum across duration. On the live summand joint Borel Λ followed by x↦exp(−x) and inclusion into the extended nonnegative reals is Borel; on the stopped summand the weight is zero. Compose with h↦(h_n,d(h)). Nonnegativity Λ_z(u)≥0 gives exp(−Λ_z(u))≤1. Thus every q_d(h) lies in [0,1], even when d as a function is unbounded. This bound is derived internally.

\[\Lambda_z(u)\ge0\Longrightarrow0\le e^{-\Lambda_z(u)}\le1.\]
Corresponding Lean step
  -- Joint Borel hazard gives a Borel exponential weight, including dead records.
  let weightObs : D × ℝ≥0 → ℝ≥0∞ := fun q => match q.1 with
    | Sum.inl a => ENNReal.ofReal (Real.exp (-Λ y xRef a.2 q.2))
    | Sum.inr _ => 0
  have hweightObs : Measurable weightObs := by
    let e := MeasurableEquiv.sumProdDistrib (ℝ≥0 × (E × E)) Unit ℝ≥0
    have hl : Measurable (fun q : (ℝ≥0 × (E × E)) × ℝ≥0 =>
        ENNReal.ofReal (Real.exp (-Λ y xRef q.1.2 q.2))) := by
      exact (hΛtyped.comp (f := fun q : (ℝ≥0 × (E × E)) × ℝ≥0 =>
        (((y, xRef), q.1.2), q.2)) (((measurable_const : Measurable
        (fun _ : (ℝ≥0 × (E × E)) × ℝ≥0 => (y, xRef))).prodMk
          measurable_fst.snd).prodMk measurable_snd)).neg.exp.ennreal_ofReal
    have heq : weightObs = (Sum.elim
        (fun q : (ℝ≥0 × (E × E)) × ℝ≥0 =>
          ENNReal.ofReal (Real.exp (-Λ y xRef q.1.2 q.2)))
        (fun _ : Unit × ℝ≥0 => (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 : ℝ≥0∞)))).comp e.measurable
  let weight : Hist → ℝ≥0∞ := fun h => survivalWeight y xRef (h last) (d h)
  have hw : Measurable weight :=
    hweightObs.comp ((measurable_pi_apply last).prodMk hd)
  have hbound (h : Hist) : weight h ≤ 1 := by
    change survivalWeight y xRef (h last) (d h) ≤ 1
    cases h last with
    | inr a => simp [survivalWeight]
    | inl a =>
      change ENNReal.ofReal (Real.exp (-Λ y xRef a.2 (d h))) ≤ 1
      exact ENNReal.ofReal_le_one.mpr
        (Real.exp_le_one_iff.mpr (neg_nonpos.mpr ((hΛpos y xRef a.2).2.1 (d h))))

Exact contiguous compiled BODY region; all proof ingredients are derived, not added source premises.

4. Evaluate each fixed-history survival fiber

Fix a history h. For a stopped last record the fiber is empty and its P-measure is zero. For a live last record z, push raw coordinate0 forward under P to Exp(1), then push that law through e↦τ_z(max(e,0)). The existing hazard-clock theorem identifies the real probability of (d(h),∞] with exp(−Λ_z(d(h))). Its pushed law is a probability measure, so conversion to an extended nonnegative measure loses no mass. This is a pointwise identity for every fixed h and its d(h), not substitution into separate almost-everywhere statements indexed by fixed times.

\[P\{v:L(h_n,d(h),v_0)\}=q_d(h)\quad\text{for every }h.\]
Corresponding Lean step
  -- For every fixed live history, integrate only its independent next clock.
  have hfiber (h : Hist) : P {w : ℕ → ℝ |
      liveSurvival y xRef (h last) (d h) (w 0)} = weight h := by
    cases hr : h last with
    | inr a => simp [liveSurvival, weight, survivalWeight, hr]
    | inl a =>
      let z := a.2
      let f : ℝ → WithTop ℝ≥0 := fun e => τ y xRef z (Real.toNNReal e)
      have hf : Measurable f := hτtyped.comp (f := fun e : ℝ =>
        ((y, xRef), z, Real.toNNReal e))
        ((measurable_const : Measurable (fun _ : ℝ => (y, xRef))).prodMk
          ((measurable_const : Measurable (fun _ : ℝ => z)).prodMk
            measurable_real_toNNReal))
      have hs := hSurv y xRef z
      letI : IsProbabilityMeasure (Measure.map f (expMeasure (1 : ℝ))) := hs.1
      have ht : Measure.map f (expMeasure (1 : ℝ))
          (Set.Ioi ((d h : ℝ≥0) : WithTop ℝ≥0)) =
          ENNReal.ofReal (Real.exp (-Λ y xRef z (d h))) := by
        rw [← ofReal_measureReal, hs.2 (d h)]
      calc
        P {w : ℕ → ℝ | liveSurvival y xRef (Sum.inl a) (d h) (w 0)} =
            (Measure.map (fun w : ℕ → ℝ => w 0) P)
              (f ⁻¹' Set.Ioi ((d h : ℝ≥0) : WithTop ℝ≥0)) := by
          rw [Measure.map_apply (measurable_pi_apply 0)
            (measurableSet_Ioi.preimage hf)]
          simp only [liveSurvival, hr, f, z]
          rfl
        _ = (expMeasure (1 : ℝ)) (f ⁻¹' Set.Ioi ((d h : ℝ≥0) : WithTop ℝ≥0)) := by
          rw [(hi.2.1 0).2.2]
        _ = Measure.map f (expMeasure (1 : ℝ))
            (Set.Ioi ((d h : ℝ≥0) : WithTop ℝ≥0)) :=
          (Measure.map_apply hf measurableSet_Ioi).symm
        _ = weight h := by simpa only [weight, survivalWeight, hr, z] using ht

Exact contiguous compiled BODY region; all proof ingredients are derived, not added source premises.

5. Integrate over the actual history law without normalization

For Borel A let C={(h,v):h∈A and (h,v)∈B_d}, a Borel product-space event. Its pullback under (H_n,Y_n) is exactly the desired actual-clock event. Replace the pushforward by μ_n⊗P and apply the product-measure section formula. The section has mass q_d(h) on A and zero off A. Its integral is the integral of the indicator of A times q_d, hence ∫_A q_d dμ_n. No division by μ_n(A), regular conditional distribution or bounded duration assumption enters.

\[P\{H_n\in A,\ L(R_n,d(H_n),w_n)\}=\int_A q(h_n,d(h))\,\mu_n(dh).\]
Corresponding Lean step
  refine ⟨hB, hw, hbound, ?_⟩
  intro A hA
  let C : Set (Hist × (ℕ → ℝ)) := {p | p.1 ∈ A ∧ p ∈ B}
  have hC : MeasurableSet C := (hA.preimage measurable_fst).inter hB
  calc
    P {w : ℕ → ℝ | H w ∈ A ∧ liveSurvival y xRef
        (record y xRef z₀ (ε w) n) (d (H w)) (w n)} =
        (Measure.map (fun w => (H w, Y w)) P) C := by
      rw [Measure.map_apply (hH.prodMk hY) hC]
      rfl
    _ = ((Measure.map H P).prod P) C := by rw [hjoint]
    _ = ∫⁻ h : Hist, P {w : ℕ → ℝ | (h, w) ∈ C} ∂Measure.map H P :=
      Measure.prod_apply hC
    _ = ∫⁻ h : Hist, A.indicator weight h ∂Measure.map H P := by
      apply lintegral_congr
      intro h
      by_cases ha : h ∈ A
      · simpa only [C, B, Set.mem_setOf_eq, ha, true_and,
          Set.indicator_of_mem ha] using hfiber h
      · simp only [C, Set.mem_setOf_eq, ha, false_and, Set.setOf_false,
          measure_empty, Set.indicator_of_notMem ha]
    _ = ∫⁻ h in A, survivalWeight y xRef (h last) (d h) ∂Measure.map H P :=
      lintegral_indicator hA weight

Exact contiguous compiled BODY region; all proof ingredients are derived, not added source premises.

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_survival

Keep actual definitions and consume verified producers; Derive the joint survival event measurability; Derive the Borel bounded survival weight; Evaluate each fixed-history survival fiber; Integrate over the actual history law without normalization

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_survival
    {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_survival_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 liveSurvival : E → E → ((ℝ≥0 × (E × E)) ⊕ Unit) → ℝ≥0 → ℝ → Prop :=
    fun y xRef r u e => match r with
      | Sum.inl a => (u : WithTop ℝ≥0) < τ y xRef a.2 (Real.toNNReal e)
      | Sum.inr _ => False
  let survivalWeight : E → E → ((ℝ≥0 × (E × E)) ⊕ Unit) → ℝ≥0 → ℝ≥0∞ :=
    fun y xRef r u => match r with
      | Sum.inl a => ENNReal.ofReal (Real.exp (-Λ y xRef a.2 u))
      | Sum.inr _ => 0
  change
  ∀ y xRef : E, ∀ z₀ : E × E, ∀ n : ℕ,
    ∀ d : (Fin (n + 1) → ((ℝ≥0 × (E × E)) ⊕ Unit)) → ℝ≥0,
    Measurable d →
    MeasurableSet {p : (Fin (n + 1) → ((ℝ≥0 × (E × E)) ⊕ Unit)) × (ℕ → ℝ) |
      liveSurvival y xRef (p.1 ⟨n, Nat.lt_succ_self n⟩) (d p.1) (p.2 0)} ∧
    Measurable (fun h : Fin (n + 1) → ((ℝ≥0 × (E × E)) ⊕ Unit) =>
      survivalWeight y xRef (h ⟨n, Nat.lt_succ_self n⟩) (d h)) ∧
    (∀ h : Fin (n + 1) → ((ℝ≥0 × (E × E)) ⊕ Unit),
      survivalWeight y xRef (h ⟨n, Nat.lt_succ_self n⟩) (d h) ≤ 1) ∧
    (∀ A : Set (Fin (n + 1) → ((ℝ≥0 × (E × E)) ⊕ Unit)), MeasurableSet A →
      P {w : ℕ → ℝ | history y xRef z₀ n w ∈ A ∧
        liveSurvival y xRef (record y xRef z₀ (ε w) n)
          (d (history y xRef z₀ n w)) (w n)} =
      ∫⁻ h in A, survivalWeight y xRef (h ⟨n, Nat.lt_succ_self n⟩) (d h)
        ∂(Measure.map (history y xRef z₀ n) P))

  have hh := ActualHazardClock.actual_integrated_hazard_clock_laws hα hαβ hV hH hη hβη
  rcases hh with ⟨hΛc, hΛm, hInt, hΛpos, hcross, hfinite, hτm, hSurv, hcap, hfloor⟩
  have hτtyped : Measurable (fun a : (E × E) × (E × E) × ℝ≥0 =>
      τ a.1.1 a.1.2 a.2.1 a.2.2) := hτm
  have hΛtyped : Measurable (fun a : ((E × E) × (E × E)) × ℝ≥0 =>
      Λ a.1.1.1 a.1.1.2 a.1.2 a.2) := hΛm
  have hi := AutoSamplingTheory.TechnicalLemmas.Probability.UnitExponentialProduct.unit_exponential_product_laws
  letI : IsProbabilityMeasure P := hi.1
  letI : IsProbabilityMeasure (expMeasure (1 : ℝ)) :=
    isProbabilityMeasure_expMeasure zero_lt_one
  intro y xRef z₀ n d hd
  let D := ((ℝ≥0 × (E × E)) ⊕ Unit)
  let Hist := Fin (n + 1) → D
  let last : Fin (n + 1) := ⟨n, Nat.lt_succ_self n⟩
  let H : (ℕ → ℝ) → Hist := history y xRef z₀ n
  let Y : (ℕ → ℝ) → (ℕ → ℝ) := fun w k => w (n + k)
  have hp := ActualFiniteHistoryTailLaw.actual_finite_history_tail_law
    hα hαβ hV hH hη hβη y xRef z₀ n
  have hH : Measurable H := hp.1
  have hY : Measurable Y := hp.2.1
  have hjoint : Measure.map (fun w => (H w, Y w)) P =
      (Measure.map H P).prod P := hp.2.2.2.2.2.2.1
  -- A stopped record has no next wait. The following zero-valued observable
  -- is only used under a strict nonnegative-duration comparison, hence false.
  let waitObs : D × ℝ → WithTop ℝ≥0 := fun q => match q.1 with
    | Sum.inl a => τ y xRef a.2 (Real.toNNReal q.2)
    | Sum.inr _ => 0
  have hwait : Measurable waitObs := 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τtyped.comp (f := 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 heq : waitObs = (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 hwaitEq (r : D) (u : ℝ≥0) (e : ℝ) :
      liveSurvival y xRef r u e ↔ (u : WithTop ℝ≥0) < waitObs (r, e) := by
    cases r with
    | inl a => rfl
    | inr a =>
      simp only [liveSurvival, waitObs, false_iff]
      exact not_lt.mpr (WithTop.coe_le_coe.mpr (show (0 : ℝ≥0) ≤ u from zero_le))
  let B : Set (Hist × (ℕ → ℝ)) := {p |
    liveSurvival y xRef (p.1 last) (d p.1) (p.2 0)}
  have hB : MeasurableSet B := by
    have hm := measurableSet_lt (WithTop.measurable_coe.comp (hd.comp measurable_fst))
      (hwait.comp (f := fun p : Hist × (ℕ → ℝ) => (p.1 last, p.2 0))
        (((measurable_pi_apply last).comp measurable_fst).prodMk
        ((measurable_pi_apply 0).comp measurable_snd)))
    simpa only [B, hwaitEq, Function.comp_def] using hm
  -- Joint Borel hazard gives a Borel exponential weight, including dead records.
  let weightObs : D × ℝ≥0 → ℝ≥0∞ := fun q => match q.1 with
    | Sum.inl a => ENNReal.ofReal (Real.exp (-Λ y xRef a.2 q.2))
    | Sum.inr _ => 0
  have hweightObs : Measurable weightObs := by
    let e := MeasurableEquiv.sumProdDistrib (ℝ≥0 × (E × E)) Unit ℝ≥0
    have hl : Measurable (fun q : (ℝ≥0 × (E × E)) × ℝ≥0 =>
        ENNReal.ofReal (Real.exp (-Λ y xRef q.1.2 q.2))) := by
      exact (hΛtyped.comp (f := fun q : (ℝ≥0 × (E × E)) × ℝ≥0 =>
        (((y, xRef), q.1.2), q.2)) (((measurable_const : Measurable
        (fun _ : (ℝ≥0 × (E × E)) × ℝ≥0 => (y, xRef))).prodMk
          measurable_fst.snd).prodMk measurable_snd)).neg.exp.ennreal_ofReal
    have heq : weightObs = (Sum.elim
        (fun q : (ℝ≥0 × (E × E)) × ℝ≥0 =>
          ENNReal.ofReal (Real.exp (-Λ y xRef q.1.2 q.2)))
        (fun _ : Unit × ℝ≥0 => (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 : ℝ≥0∞)))).comp e.measurable
  let weight : Hist → ℝ≥0∞ := fun h => survivalWeight y xRef (h last) (d h)
  have hw : Measurable weight :=
    hweightObs.comp ((measurable_pi_apply last).prodMk hd)
  have hbound (h : Hist) : weight h ≤ 1 := by
    change survivalWeight y xRef (h last) (d h) ≤ 1
    cases h last with
    | inr a => simp [survivalWeight]
    | inl a =>
      change ENNReal.ofReal (Real.exp (-Λ y xRef a.2 (d h))) ≤ 1
      exact ENNReal.ofReal_le_one.mpr
        (Real.exp_le_one_iff.mpr (neg_nonpos.mpr ((hΛpos y xRef a.2).2.1 (d h))))
  -- For every fixed live history, integrate only its independent next clock.
  have hfiber (h : Hist) : P {w : ℕ → ℝ |
      liveSurvival y xRef (h last) (d h) (w 0)} = weight h := by
    cases hr : h last with
    | inr a => simp [liveSurvival, weight, survivalWeight, hr]
    | inl a =>
      let z := a.2
      let f : ℝ → WithTop ℝ≥0 := fun e => τ y xRef z (Real.toNNReal e)
      have hf : Measurable f := hτtyped.comp (f := fun e : ℝ =>
        ((y, xRef), z, Real.toNNReal e))
        ((measurable_const : Measurable (fun _ : ℝ => (y, xRef))).prodMk
          ((measurable_const : Measurable (fun _ : ℝ => z)).prodMk
            measurable_real_toNNReal))
      have hs := hSurv y xRef z
      letI : IsProbabilityMeasure (Measure.map f (expMeasure (1 : ℝ))) := hs.1
      have ht : Measure.map f (expMeasure (1 : ℝ))
          (Set.Ioi ((d h : ℝ≥0) : WithTop ℝ≥0)) =
          ENNReal.ofReal (Real.exp (-Λ y xRef z (d h))) := by
        rw [← ofReal_measureReal, hs.2 (d h)]
      calc
        P {w : ℕ → ℝ | liveSurvival y xRef (Sum.inl a) (d h) (w 0)} =
            (Measure.map (fun w : ℕ → ℝ => w 0) P)
              (f ⁻¹' Set.Ioi ((d h : ℝ≥0) : WithTop ℝ≥0)) := by
          rw [Measure.map_apply (measurable_pi_apply 0)
            (measurableSet_Ioi.preimage hf)]
          simp only [liveSurvival, hr, f, z]
          rfl
        _ = (expMeasure (1 : ℝ)) (f ⁻¹' Set.Ioi ((d h : ℝ≥0) : WithTop ℝ≥0)) := by
          rw [(hi.2.1 0).2.2]
        _ = Measure.map f (expMeasure (1 : ℝ))
            (Set.Ioi ((d h : ℝ≥0) : WithTop ℝ≥0)) :=
          (Measure.map_apply hf measurableSet_Ioi).symm
        _ = weight h := by simpa only [weight, survivalWeight, hr, z] using ht
  refine ⟨hB, hw, hbound, ?_⟩
  intro A hA
  let C : Set (Hist × (ℕ → ℝ)) := {p | p.1 ∈ A ∧ p ∈ B}
  have hC : MeasurableSet C := (hA.preimage measurable_fst).inter hB
  calc
    P {w : ℕ → ℝ | H w ∈ A ∧ liveSurvival y xRef
        (record y xRef z₀ (ε w) n) (d (H w)) (w n)} =
        (Measure.map (fun w => (H w, Y w)) P) C := by
      rw [Measure.map_apply (hH.prodMk hY) hC]
      rfl
    _ = ((Measure.map H P).prod P) C := by rw [hjoint]
    _ = ∫⁻ h : Hist, P {w : ℕ → ℝ | (h, w) ∈ C} ∂Measure.map H P :=
      Measure.prod_apply hC
    _ = ∫⁻ h : Hist, A.indicator weight h ∂Measure.map H P := by
      apply lintegral_congr
      intro h
      by_cases ha : h ∈ A
      · simpa only [C, B, Set.mem_setOf_eq, ha, true_and,
          Set.indicator_of_mem ha] using hfiber h
      · simp only [C, Set.mem_setOf_eq, ha, false_and, Set.setOf_false,
          measure_empty, Set.indicator_of_notMem ha]
    _ = ∫⁻ h in A, survivalWeight y xRef (h last) (d h) ∂Measure.map H P :=
      lintegral_indicator hA weight

end
end AutoSamplingTheory.ExampleCases.ProximalBPS.ActualConditionalNextWaitSurvival

Exact module and namespace context

Scope and omitted-condition boundaries
  • Same six original analytic hypotheses and literal stopped actual recursion. Deterministic event depth n; Borel finite-valued duration d of complete history and Borel event A are admissible test objects, not extra analytic hypotheses or probability/regularity providers. Stopped histories have zero survival weight; live infinite waits survive every finite duration. Unnormalized identity includes null A, n0, rank0 and unbounded duration functions. Only S87-I4 closes when proved; S87-I5 conditional finite-wait density, ordered-time iteration, final factor assembly, fullA7, physical-time residual restart/Markovness/invariance/nonexplosion/hypocoercivity/implementation/cost/main/composition/wholepaper/Goal remain OPEN. No proof credit at seal.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

  • MeasurableEquiv.sumProdDistrib
  • Measurable.sumElim
  • measurableSet_lt
  • WithTop.measurable_coe
  • measurable_pi_apply
  • Measurable.ennreal_ofReal
  • Real.exp_le_one_iff
  • ENNReal.ofReal_le_one
  • ofReal_measureReal
  • Measure.map_apply
  • Measure.prod_apply
  • lintegral_congr
  • lintegral_indicator

Mathematical sources

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