Samplinglib mathematical lesson

Actual PBPS ordered finite-prefix law

AutoSamplingTheory.ExampleCases.ProximalBPS.ActualOrderedPrefix.actual_ordered_prefix_law · 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 finite n≥0 and finite horizon T≥0, let Hist_n=D^(Fin(n+1)) and H_n(w)=(R_j(ε(w)))_(0≤j≤n). Write rtime(live(a,z))=a and rtime(stopped)=0. Define the measurable ordered simplex Δ_n(T)={t∈ℝ^n:0<t_1<⋯<t_n<T}; its subtype carries m_n, the comap of product Lebesgue volume along inclusion. For t∈Δ_n(T), put s_0=0,s_i=t_i, z_0=z₀ and z_i=S_rΦ_(s_i−s_(i−1))(z_(i−1)) for 1≤i≤n. Define K_n(t)_j=live(s_j,z_j). Define qReal_n(t)=∏_(i=1)^n [λ_r(Φ_(s_i−s_(i−1))(z_(i−1))) exp(−Λ_(z_(i−1))(s_i−s_(i−1)))] and q_n=ofReal(qReal_n). Here the literal Lean definitions use toNNReal on times and elapsed times; these agree with the displayed nonnegative values on the simplex. Let A_n(T) be the abstract-history set in which all n+1 records are live, their read times are strictly increasing, and each postinitial read time is below T. A_n(T) does not itself constrain the initial record time. Set B_n(T)=H_n^(-1)(A_n(T)) and obs_n(w)_i=rtime(H_n(w)_(i+1)); actual H_n(w)_0 is always live(0,z₀). Then Δ_n(T) and A_n(T) are Borel. For fixed n,T, K_n and q_n are jointly Borel in (y,r,z₀,t). For every y,r,z₀, H_n,obs_n and B_n(T) are Borel, and qReal_n(t)≥0 for every simplex point. For every raw w∈B_n(T), there exists t∈Δ_n(T) with t=obs_n(w) and H_n(w)=K_n(t), as complete tagged histories. The exact unnormalized law is (H_n)_*(P restricted to B_n(T))=(K_n)_*(q_n m_n). For every Borel F:Hist_n→[0,∞], ∫_(B_n(T))F(H_n(w))P(dw)=∫_(Δ_n(T))F(K_n(t))q_n(t)m_n(dt). Moreover ∫q_n dm_n=P(B_n(T))≤1. This includes n=0,T=0, zero hazard and extended-valued tests; there is no boundedness, integrability or positive-event-mass assumption. This is the strict first-n-prefix law, without a final survival factor, and is not a raw exact-n event-count law. It is an attributed ASTIS completion of the finite ordered iteration ingredient implicit in Appendix A.1(A.7), with joint Borel construction from Appendix A.2. The dimension-zero and ENNReal-test extensions are explicit ASTIS extensions. Terminal survival, endpoint/count identification, the full path-functional A.7 expansion, restart/Markovness, invariance, hypocoercivity, implementation errors, expected costs and full paper/composition remain outside this result.

\[\int_{B_n(T)}F(H_n)\,dP=\int_{\Delta_n(T)}F(K_n(s))q_n(s)\,dm_n(s).\]

Lean statement · actual_ordered_prefix_law

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_ordered_prefix_law
    {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_ordered_prefix_statement hα hαβ hV hH hη hβη

Exact module and namespace context

Full Lean proposition (definition) · actual_ordered_prefix_statement

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

Download module (.lean)

private def actual_ordered_prefix_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 Rec := (ℝ≥0 × (E × E)) ⊕ Unit
    let Hist : ℕ → Type _ := fun n => Fin (n + 1) → Rec
    let readTime : Rec → ℝ := fun r => match r with
      | Sum.inl q => (q.1 : ℝ)
      | Sum.inr _ => 0
    let Δ : (n : ℕ) → ℝ≥0 → Set (Fin n → ℝ) := fun n T =>
      {t | StrictMono (Fin.cons (0 : ℝ) t) ∧ ∀ i, t i < (T : ℝ)}
    let Prefix : (n : ℕ) → ℝ≥0 → Type := fun n T => {t : Fin n → ℝ // t ∈ Δ n T}
    let m : (n : ℕ) → (T : ℝ≥0) → Measure (Prefix n T) := fun n T =>
      Measure.comap (fun t : Prefix n T => t.val) (volume : Measure (Fin n → ℝ))
    let zAt : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) →
        Prefix n T → Fin (n + 1) → (E × E) := fun y xRef z₀ n T t =>
      Fin.induction z₀ (fun i z =>
        S xRef (Φ y xRef (t.val i - (Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) i.castSucc) z))
    let K : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) →
        Prefix n T → Hist n := fun y xRef z₀ n T t j =>
      Sum.inl (Real.toNNReal ((Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) j), zAt y xRef z₀ n T t j)
    let qReal : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) →
        Prefix n T → ℝ := fun y xRef z₀ n T t =>
      ∏ i : Fin n,
        rate xRef (Φ y xRef (t.val i - (Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) i.castSucc)
          (zAt y xRef z₀ n T t i.castSucc)) *
        Real.exp (-Λ y xRef (zAt y xRef z₀ n T t i.castSucc)
          (Real.toNNReal (t.val i - (Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) i.castSucc)))
    let q : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) →
        Prefix n T → ℝ≥0∞ := fun y xRef z₀ n T t =>
      ENNReal.ofReal (qReal y xRef z₀ n T t)
    let A : (n : ℕ) → ℝ≥0 → Set (Hist n) := fun n T =>
      {h | (∀ j, ∃ a : ℝ≥0 × (E × E), h j = Sum.inl a) ∧
        StrictMono (fun j => readTime (h j)) ∧
        ∀ i : Fin n, readTime (h i.succ) < (T : ℝ)}
    ∀ n : ℕ, ∀ T : ℝ≥0,
      MeasurableSet (Δ n T) ∧ MeasurableSet (A n T) ∧
      Measurable (fun p : ((E × E) × (E × E)) × Prefix n T =>
        K p.1.1.1 p.1.1.2 p.1.2 n T p.2) ∧
      Measurable (fun p : ((E × E) × (E × E)) × Prefix n T =>
        q p.1.1.1 p.1.1.2 p.1.2 n T p.2) ∧
      (∀ y xRef : E, ∀ z₀ : E × E,
        let H : (ℕ → ℝ) → Hist n := history y xRef z₀ n
        let B : Set (ℕ → ℝ) := H ⁻¹' A n T
        let obs : (ℕ → ℝ) → Fin n → ℝ := fun w i => readTime (H w i.succ)
        Measurable H ∧ MeasurableSet B ∧ Measurable obs ∧
        (∀ t : Prefix n T, 0 ≤ qReal y xRef z₀ n T t) ∧
        (∀ w ∈ B, ∃ t : Prefix n T, t.val = obs w ∧ H w = K y xRef z₀ n T t) ∧
        Measure.map H (P.restrict B) =
          Measure.map (K y xRef z₀ n T) ((m n T).withDensity (q y xRef z₀ n T)) ∧
        (∀ F : Hist n → ℝ≥0∞, Measurable F →
          (∫⁻ w in B, F (H w) ∂P) =
            ∫⁻ t : Prefix n T, F (K y xRef z₀ n T t) * q y xRef z₀ n T t ∂m n T) ∧
        (∫⁻ t : Prefix n T, q y xRef z₀ n T t ∂m n T) = P B ∧
        P B ≤ 1)


set_option maxHeartbeats 2400000 in

Exact module and namespace context

Proof roadmap

1Build the Borel geometry and a nonnegative density
The simplex is a finite intersection of strict inequalities between coordinate maps. Reading a live time and returning zero on the stopped tag is Borel; the live tag is a measurable summand. Thus the complete-history guard is Borel. Reuse the actual harmonic-flow, reflection/rate and integrated-hazard theorems. Finite induction through the bounce-after-flow update makes every prescribed state jointly Borel in y,r,z₀ and time coordinates. Pair with the nonnegative time coordinates to obtain K; finite products and exp/ofReal give q. Each rate is √η times a nonnegative positive part and each exponential is positive, so every factor and the real finite product are nonnegative.
2Recover the complete prescribed history from each actual strict prefix
Take w in B_n and read its postinitial times into s. The actual zeroth record is live(0,z₀); the guard supplies strict increase and s_i<T, hence s lies in the simplex. Induct over records. A live successor excludes an infinite clock by the literal stopped recursion. Its time is the previous live time plus the finite wait, so that wait equals s_i−s_(i−1). The recursive state is therefore exactly S_rΦ_(s_i−s_(i−1))z_(i−1). Nonnegative clocks make the toNNReal representatives agree. Every time, state and tag is preserved, proving H_n(w)=K_n(s) pointwise, rather than merely identifying a final marginal.
3Start the probability induction at zero events
For n=0 the complete history is the single initial live record. The guard and zero-dimensional simplex are universal, even when T=0. The empty density product equals one. The subtype comap has mass one: push its inclusion forward to restricted zero-dimensional product volume and use the empty product of masses. The canonical exponential product is a probability measure. Both sides of the test identity are therefore F(live(0,z₀)), including F=∞. No positive horizon or finite test assumption is introduced.
4Split exactly the next strict-prefix event
A length n+2 history is the old length n+1 history followed by its last record. Strict monotonicity splits into old strict monotonicity and one final strict comparison; the cap splits into the old cap and the final time below T. All-live status splits in the same way. The old last record is live because it belongs to the old guard. Applying this finite-tuple identity to the literal record sequence gives the displayed event equality on every raw input. Stopped or zero-wait transitions cannot enter the strict next-event part; no almost-everywhere count interpretation is used.
5Use the actual one-step probability law inside the old guard
Apply the previously verified absolute-event-time theorem at constant horizon T and its full next-history test (h_next,u)↦F(h_next). It produces the Borel inner function J_F. Localize its unnormalized law to A_n(T), the old Borel guard. The event equality just proved changes its left side to B_(n+1)(T). Pull the right integral against the old history pushforward back to canonical P. This gives the actual recurrence, using the law of the real exponential-clock recursion. No conditional density or recurrence is assumed as a new source premise.
6Disintegrate the ordered simplex with its actual subtype measure
Appending u to s belongs to Δ_(n+1)(T) exactly when s lies in Δ_n(T) and s_n<u<T. Fixed Mathlib proves that inserting the last real coordinate preserves product Lebesgue volume. Pull back the simplex indicator and apply nonnegative Tonelli to obtain the iterated integral. For a Borel function defined only on the simplex subtype, extend it measurably to the ambient finite product using the measurable inclusion. It agrees on the subtype; all integrals are restricted there, so outside values have no effect. The comap integral formula transfers the resulting equality back to the dependent simplex and interval subtypes. The argument includes empty domains and infinite integrals.
7Identify the appended history and factor the density
Finite induction shows that appending a last time leaves every earlier state unchanged and adds state S_rΦ_(u−s_n)z_n. Since s_n≥0 and u>s_n, toNNReal(s_n)+toNNReal(u−s_n)=toNNReal(u); therefore absolute append equals K_(n+1)(s,u) as a complete history. Split the finite product at its last index to get q_(n+1)=q_n times the next pre-bounce rate and elapsed survival. The real product is already nonnegative, so ofReal preserves this multiplication. These private algebraic inputs are instantiated by the actual flow, reflection, rate and hazard in the induction.
8Close the all-n probability induction for every nonnegative test
Assume the test identity at n. Apply it to the Borel J_F produced by the actual recurrence. The resulting integrand is J_F(K_n(s))q_n(s). At K_n(s), the next-event density is the indicator of s_n<u<T times ρ(z_n,u−s_n). Move the finite nonnegative scalar q_n(s)=ofReal(qReal_n(s)) inside the nonnegative integral, restrict to that open interval, and use the exact append and product identities. The result is F(K_(n+1)(s,u))q_(n+1)(s,u). The subtype Tonelli equality turns the two integrals into the integral over Δ_(n+1). Joint Borel K and q ensure the composed test is Borel. Together with the zero-event base this proves the formula for every n, without boundedness or integrability.
9Recover the measure equality and the exact missing mass
Compare both pushforward measures against every Borel ENNReal test. The map-integral formula and the withDensity formula turn their integrals into the identity just proved; measure extensionality gives equality. Taking F=1 gives ∫q_n dm_n=P(B_n(T)), and the canonical probability normalization gives P(B_n(T))≤1. This mass is not renormalized. The private all-test input is supplied by the actual all-n induction, not by a public hypothesis.
10Assemble the sealed statement and retain its source boundary
Keep the literal definitions and the six original analytic hypotheses. Assemble the joint Borel conclusions, derive actual H_n from the existing next-event theorem and obs_n by Borel coordinate projection, use the pointwise reconstruction, and pass the proved all-n tests to measure extensionality. The result is the complete strict-prefix statement displayed above. A final no-further-event survival term, exact-count/path identification and summing full path terms are separate remaining source steps; this theorem makes no invariance, mixing or expected-cost claim.

Full assumptions and notation

All objects and hypotheses

Finite-dimensional real inner-product Borel space E, including the explicitly disclosed rank-zero extension.
α,β≥0; exactly six analytic assumptions: α>0, α≤β, V is C², α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for all x,v, η>0, βη≤1.
Every deterministic n≥0, finite T≥0 and y,r,z₀ are universally quantified. The exponential product P, clipped coordinates, stopped recursion, complete histories, simplex and reference measure are literal definitions.
Tests F are arbitrary Borel Hist_n→[0,∞], with no boundedness, integrability or positive-event-mass requirement.
All joint measurability, pointwise reconstruction, nonnegativity, density law and mass bounds are proved conclusions; no law, independence, normalization or density provider is an additional public premise.

Mathematical proof

1. Build the Borel geometry and a nonnegative density

The simplex is a finite intersection of strict inequalities between coordinate maps. Reading a live time and returning zero on the stopped tag is Borel; the live tag is a measurable summand. Thus the complete-history guard is Borel. Reuse the actual harmonic-flow, reflection/rate and integrated-hazard theorems. Finite induction through the bounce-after-flow update makes every prescribed state jointly Borel in y,r,z₀ and time coordinates. Pair with the nonnegative time coordinates to obtain K; finite products and exp/ofReal give q. Each rate is √η times a nonnegative positive part and each exponential is positive, so every factor and the real finite product are nonnegative.

\[\Delta_n(T)=\{0<s_1<\cdots<s_n<T\},\quad s_0=0,\quad z_i=S_r\Phi_{s_i-s_{i-1}}z_{i-1},\quad K_n(s)_i=\operatorname{live}(s_i,z_i).\qquad K_n,q_n\text{ jointly Borel},\quad q_n^{\rm real}\ge0.\]

Corresponding Lean step

private theorem measurable_cons_zero (n : ℕ) (j : Fin (n + 1)) :
    Measurable (fun t : Fin n → ℝ => (Fin.cons (0 : ℝ) t : Fin (n + 1) → ℝ) j) := by
  induction j using Fin.cases with
  | zero => simpa only [Fin.cons_zero] using (measurable_const : Measurable (fun _ : Fin n → ℝ => (0 : ℝ)))
  | succ i => simpa only [Fin.cons_succ] using (measurable_pi_apply i : Measurable (fun t : Fin n → ℝ => t i))

private theorem simplex_measurable (n : ℕ) (T : ℝ≥0) :
    MeasurableSet {t : Fin n → ℝ |
      StrictMono (Fin.cons (0 : ℝ) t) ∧ ∀ i, t i < (T : ℝ)} := by
  simp only [StrictMono, Set.ofPred_and, Set.ofPred_forall]
  apply MeasurableSet.inter
  · exact MeasurableSet.iInter fun i => MeasurableSet.iInter fun j =>
      MeasurableSet.iInter fun _ => measurableSet_lt (measurable_cons_zero n i) (measurable_cons_zero n j)
  · exact MeasurableSet.iInter fun i => measurableSet_lt (measurable_pi_apply i) measurable_const

private def readTime {Z : Type*} (r : (ℝ≥0 × Z) ⊕ Unit) : ℝ :=
  match r with
  | Sum.inl q => q.1
  | Sum.inr _ => 0

private theorem readTime_measurable {Z : Type*} [MeasurableSpace Z] :
    Measurable (@readTime Z) := by
  apply Measurable.sumElim
  · exact measurable_coe_nnreal_real.comp measurable_fst
  · exact measurable_const

private theorem live_measurable {Z : Type*} [MeasurableSpace Z] :
    MeasurableSet {r : (ℝ≥0 × Z) ⊕ Unit | ∃ a, r = Sum.inl a} := by
  have heq : {r : (ℝ≥0 × Z) ⊕ Unit | ∃ a, r = Sum.inl a} = Set.range Sum.inl := by
    ext r
    simp only [Set.mem_ofPred_eq, Set.mem_range, eq_comm]
  rw [heq]
  exact measurableSet_range_inl

private theorem history_guard_measurable {Z : Type*} [MeasurableSpace Z] (n : ℕ) (T : ℝ≥0) :
    MeasurableSet {h : Fin (n + 1) → ((ℝ≥0 × Z) ⊕ Unit) |
      (∀ j, ∃ a : ℝ≥0 × Z, h j = Sum.inl a) ∧
      StrictMono (fun j => readTime (h j)) ∧
      ∀ i : Fin n, readTime (h i.succ) < (T : ℝ)} := by
  simp only [StrictMono, Set.ofPred_and, Set.ofPred_forall]
  apply MeasurableSet.inter
  · exact MeasurableSet.iInter fun j => live_measurable.preimage (measurable_pi_apply j)
  · apply MeasurableSet.inter
    · exact MeasurableSet.iInter fun i => MeasurableSet.iInter fun j =>
        MeasurableSet.iInter fun _ => measurableSet_lt
          (readTime_measurable.comp (measurable_pi_apply i))
          (readTime_measurable.comp (measurable_pi_apply j))
    · exact MeasurableSet.iInter fun i => measurableSet_lt
        (readTime_measurable.comp (measurable_pi_apply i.succ)) measurable_const


private theorem ordered_prefix_borel_data
    {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) :
    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 Rec := (ℝ≥0 × (E × E)) ⊕ Unit
    let Hist : ℕ → Type _ := fun n => Fin (n + 1) → Rec
    let readTime : Rec → ℝ := fun r => match r with
      | Sum.inl q => (q.1 : ℝ)
      | Sum.inr _ => 0
    let Δ : (n : ℕ) → ℝ≥0 → Set (Fin n → ℝ) := fun n T =>
      {t | StrictMono (Fin.cons (0 : ℝ) t) ∧ ∀ i, t i < (T : ℝ)}
    let Prefix : (n : ℕ) → ℝ≥0 → Type := fun n T => {t : Fin n → ℝ // t ∈ Δ n T}
    let m : (n : ℕ) → (T : ℝ≥0) → Measure (Prefix n T) := fun n T =>
      Measure.comap (fun t : Prefix n T => t.val) (volume : Measure (Fin n → ℝ))
    let zAt : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) →
        Prefix n T → Fin (n + 1) → (E × E) := fun y xRef z₀ n T t =>
      Fin.induction z₀ (fun i z =>
        S xRef (Φ y xRef (t.val i - (Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) i.castSucc) z))
    let K : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) →
        Prefix n T → Hist n := fun y xRef z₀ n T t j =>
      Sum.inl (Real.toNNReal ((Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) j), zAt y xRef z₀ n T t j)
    let qReal : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) →
        Prefix n T → ℝ := fun y xRef z₀ n T t =>
      ∏ i : Fin n,
        rate xRef (Φ y xRef (t.val i - (Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) i.castSucc)
          (zAt y xRef z₀ n T t i.castSucc)) *
        Real.exp (-Λ y xRef (zAt y xRef z₀ n T t i.castSucc)
          (Real.toNNReal (t.val i - (Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) i.castSucc)))
    let q : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) →
        Prefix n T → ℝ≥0∞ := fun y xRef z₀ n T t =>
      ENNReal.ofReal (qReal y xRef z₀ n T t)
    let A : (n : ℕ) → ℝ≥0 → Set (Hist n) := fun n T =>
      {h | (∀ j, ∃ a : ℝ≥0 × (E × E), h j = Sum.inl a) ∧
        StrictMono (fun j => readTime (h j)) ∧
        ∀ i : Fin n, readTime (h i.succ) < (T : ℝ)}
    ∀ n : ℕ, ∀ T : ℝ≥0,
      MeasurableSet (Δ n T) ∧ MeasurableSet (A n T) ∧
      Measurable (fun p : ((E × E) × (E × E)) × Prefix n T =>
        K p.1.1.1 p.1.1.2 p.1.2 n T p.2) ∧
      Measurable (fun p : ((E × E) × (E × E)) × Prefix n T =>
        q p.1.1.1 p.1.1.2 p.1.2 n T p.2) ∧
      (∀ y xRef : E, ∀ z₀ : E × E, ∀ t : Prefix n T, 0 ≤ qReal y xRef z₀ n T t) := 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 Rec := (ℝ≥0 × (E × E)) ⊕ Unit
  let Hist : ℕ → Type _ := fun n => Fin (n + 1) → Rec
  let readTime : Rec → ℝ := fun r => match r with
    | Sum.inl q => (q.1 : ℝ)
    | Sum.inr _ => 0
  let Δ : (n : ℕ) → ℝ≥0 → Set (Fin n → ℝ) := fun n T =>
    {t | StrictMono (Fin.cons (0 : ℝ) t) ∧ ∀ i, t i < (T : ℝ)}
  let Prefix : (n : ℕ) → ℝ≥0 → Type := fun n T => {t : Fin n → ℝ // t ∈ Δ n T}
  let m : (n : ℕ) → (T : ℝ≥0) → Measure (Prefix n T) := fun n T =>
    Measure.comap (fun t : Prefix n T => t.val) (volume : Measure (Fin n → ℝ))
  let zAt : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) →
      Prefix n T → Fin (n + 1) → (E × E) := fun y xRef z₀ n T t =>
    Fin.induction z₀ (fun i z =>
      S xRef (Φ y xRef (t.val i - (Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) i.castSucc) z))
  let K : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) →
      Prefix n T → Hist n := fun y xRef z₀ n T t j =>
    Sum.inl (Real.toNNReal ((Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) j), zAt y xRef z₀ n T t j)
  let qReal : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) →
      Prefix n T → ℝ := fun y xRef z₀ n T t =>
    ∏ i : Fin n,
      rate xRef (Φ y xRef (t.val i - (Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) i.castSucc)
        (zAt y xRef z₀ n T t i.castSucc)) *
      Real.exp (-Λ y xRef (zAt y xRef z₀ n T t i.castSucc)
        (Real.toNNReal (t.val i - (Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) i.castSucc)))
  let q : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) →
      Prefix n T → ℝ≥0∞ := fun y xRef z₀ n T t =>
    ENNReal.ofReal (qReal y xRef z₀ n T t)
  let A : (n : ℕ) → ℝ≥0 → Set (Hist n) := fun n T =>
    {h | (∀ j, ∃ a : ℝ≥0 × (E × E), h j = Sum.inl a) ∧
      StrictMono (fun j => readTime (h j)) ∧
      ∀ i : Fin n, readTime (h i.succ) < (T : ℝ)}
  change ∀ n : ℕ, ∀ T : ℝ≥0,
      MeasurableSet (Δ n T) ∧ MeasurableSet (A n T) ∧
      Measurable (fun p : ((E × E) × (E × E)) × Prefix n T =>
        K p.1.1.1 p.1.1.2 p.1.2 n T p.2) ∧
      Measurable (fun p : ((E × E) × (E × E)) × Prefix n T =>
        q p.1.1.1 p.1.1.2 p.1.2 n T p.2) ∧
      (∀ y xRef : E, ∀ z₀ : E × E, ∀ t : Prefix n T, 0 ≤ qReal y xRef z₀ n T t)
  have hΦ : Measurable (fun a : (E × E) × ℝ × (E × E) =>
      Φ a.1.1 a.1.2 a.2.1 a.2.2) :=
    (AutoSamplingTheory.ExampleCases.ProximalBPS.ActualHarmonicFlow.actual_harmonic_flow_laws
      hα hαβ hV hH hη hβη).2.1
  have hb := AutoSamplingTheory.ExampleCases.ProximalBPS.ActualBounceRate.actual_bounce_rate_energy_laws
    hα hαβ hV hH hη hβη
  have hS : Measurable (fun a : E × (E × E) => S a.1 a.2) := hb.1
  have hr : Measurable (fun a : E × (E × E) => rate a.1 a.2) := hb.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) :=
    (AutoSamplingTheory.ExampleCases.ProximalBPS.ActualHazardClock.actual_integrated_hazard_clock_laws
      hα hαβ hV hH hη hβη).2.1
  intro n T
  have hd (i : Fin n) : Measurable (fun p : ((E × E) × (E × E)) × Prefix n T =>
      p.2.val i - (Fin.cons (0 : ℝ) (p.2.val : Fin n → ℝ) : Fin (n+1) → ℝ) i.castSucc) :=
    ((measurable_pi_apply i).comp measurable_snd.subtype_val).sub
      ((measurable_cons_zero n i.castSucc).comp measurable_snd.subtype_val)
  have hz (j : Fin (n + 1)) :
      Measurable (fun p : ((E × E) × (E × E)) × Prefix n T =>
        zAt p.1.1.1 p.1.1.2 p.1.2 n T p.2 j) := by
    induction j using Fin.induction with
    | zero => simpa only [zAt, Fin.induction_zero] using
        (measurable_fst.snd : Measurable (fun p : ((E × E) × (E × E)) × Prefix n T => p.1.2))
    | succ i ih =>
      change Measurable (fun p : ((E × E) × (E × E)) × Prefix n T =>
        S p.1.1.2 (Φ p.1.1.1 p.1.1.2
          (p.2.val i - (Fin.cons (0 : ℝ) (p.2.val : Fin n → ℝ) : Fin (n+1) → ℝ) i.castSucc)
          (zAt p.1.1.1 p.1.1.2 p.1.2 n T p.2 i.castSucc)))
      exact hS.comp (measurable_fst.fst.snd.prodMk
        (hΦ.comp (measurable_fst.fst.prodMk ((hd i).prodMk ih))))
  have hf (i : Fin n) : Measurable (fun p : ((E × E) × (E × E)) × Prefix n T =>
      Φ p.1.1.1 p.1.1.2
        (p.2.val i - (Fin.cons (0 : ℝ) (p.2.val : Fin n → ℝ) : Fin (n+1) → ℝ) i.castSucc)
        (zAt p.1.1.1 p.1.1.2 p.1.2 n T p.2 i.castSucc)) :=
    hΦ.comp (measurable_fst.fst.prodMk ((hd i).prodMk (hz i.castSucc)))
  have hread : readTime = @AutoSamplingTheory.ExampleCases.ProximalBPS.ActualOrderedPrefix.readTime (E × E) := by
    funext r
    cases r <;> rfl
  refine ⟨simplex_measurable n T, ?_, ?_, ?_, ?_⟩
  · simpa only [A, hread] using
      (history_guard_measurable (Z := E × E) n T)
  · apply measurable_pi_lambda
    intro j
    exact measurable_inl.comp (((measurable_cons_zero n j).comp
      measurable_snd.subtype_val).real_toNNReal.prodMk (hz j))
  · apply Measurable.ennreal_ofReal
    apply Finset.measurable_prod
    intro i _
    exact (hr.comp (measurable_fst.fst.snd.prodMk (hf i))).mul
      ((hΛ.comp ((measurable_fst.fst.prodMk (hz i.castSucc)).prodMk
        (hd i).real_toNNReal)).neg.exp)
  · intro y xRef z₀ t
    apply Finset.prod_nonneg
    intro i _
    exact mul_nonneg (mul_nonneg (Real.sqrt_nonneg η) (le_max_left 0 _))
      (Real.exp_pos _).le