Samplinglib mathematical lesson

Actual PBPS finite endpoint and event-time reversal

AutoSamplingTheory.ExampleCases.ProximalBPS.ActualEndpointTimeReversal.actual_endpoint_time_reversal_laws · theorem · Teaching coverage

Read this first

Mathematical statement

Let E be a finite-dimensional real inner-product space with its Borel sigma algebra, including dimension zero. Let V:E→R, alpha,beta≥0 and eta in R. Assume alpha>0, alpha≤beta, V is C2, alpha||v||^2≤D2V(x)[v,v]≤beta||v||^2 for every x,v in E, eta>0 and beta*eta≤1. For y,r in E put c=y-eta grad V(r), h_r(x)=grad V(x)-grad V(r), R(x,p)=(x,-p), Phi_(y,r,u)(x,p)=(c+cos(u)(x-c)+sqrt(eta)sin(u)p, -sin(u)/sqrt(eta)(x-c)+cos(u)p), S_r(x,p)=(x,p-(2<p,h_r(x)>/||h_r(x)||^2)h_r(x)). Real division by zero is zero, so a zero normal gives the identity bounce. Let ell=volume_E tensor volume_E, with canonical Hilbert-space Lebesgue measure. For every integer n≥0 and horizon T≥0, let Delta_n(T) consist of real tuples 0<t_0<...<t_(n-1)<T. Equivalently, prepending 0 produces a strictly increasing tuple and every entry is less than T. Let Prefix_n(T) be this subtype and m_n,T the comap of Lebesgue measure on R^n under its inclusion. This is unnormalized simplex volume. For n=0 the tuple is empty and its zero-dimensional volume is one; for T=0 and n>0 the subtype is empty. Write q_0=0 and q_(j+1)=t_j. Starting at z_0=z, define z_(j+1)=S_r(Phi_(y,r,t_j-q_j)(z_j)) for 0≤j<n. Define records K_j=(q_j,z_j), each embedded in the live branch of (R_nonnegative x (E x E)) plus a cemetery symbol. For a general history of n+1 such records, the path reconstruction Psi at s in [0,T] starts from z and visits records in increasing index order: a live record (a,w) replaces the accumulator by Phi_(y,r,s-a)(w) exactly when a≤s; future records and cemetery records leave it unchanged. Here s-a is nonnegative subtraction. Define Gamma_(y,r,z,t)=Psi(K), the actual finite prescribed path; thus its value at an event is the post-bounce value. Let A_(y,r)(z,t)=Gamma_(y,r,z,t)(T). There exists rho:Prefix_n(T)→Prefix_n(T) with (rho t)_i=T-t_(n-1-i) for every i. It is Borel measurable, involutive, and preserves m_n,T. For all y,r,z,t, the terminal identity is A_(y,r)(z,t)=Phi_(y,r,T-q_n)(z_n). The map (y,r,z,t)→A_(y,r)(z,t) is jointly Borel measurable. For each y,r,t, z→A_(y,r)(z,t) preserves ell. The reversed endpoint satisfies A_(y,r)(R(A_(y,r)(z,t)),rho t)=R(z). Define Theta_(y,r)(z,t)=(R(A_(y,r)(z,t)),rho t). The map (y,r,z,t)→Theta_(y,r)(z,t) is jointly Borel measurable. For each y,r, Theta_(y,r) is an involution and preserves ell tensor m_n,T, in phase-first order. Every measure-preservation assertion includes measurability and equality of pushforward measures. All conclusions include n=0, T=0, zero reflection normals and rank-zero E; measurability, inverses, sigma finiteness and volume identities are proved internally from the six analytic assumptions. This is the finite prescribed endpoint/time change of variables used in the Appendix A.1 reversal argument. It does not assert pointwise time reversal of right-continuous paths at event times. Gibbs-weight balance, stationary averaging and invariant probability laws, Markov properties, hypocoercivity, implementation error, expected oracle costs, main sampling results and actual-input composition remain separate obligations.

\[\Theta^2=\mathrm{id},\qquad \Theta_\#(\ell\otimes m_{n,T})=\ell\otimes m_{n,T}.\]

Lean statement · actual_endpoint_time_reversal_laws

Let E be a finite-dimensional real inner-product space with its Borel sigma algebra, including dimension zero. Let V:E->R, alpha,beta>=0 and eta in R. Assume alpha>0, alpha<=beta, V is C2, alpha||v||^2<=D2V(x)[v,v]<=beta||v||^2 for every x,v in E, eta>0 and beta*eta<=1. For y,r in E put c=y-eta grad V(r), h_r(x)=grad V(x)-grad V(r), R(x,p)=(x,-p), Phi_(y,r,u)(x,p)=(c+cos(u)(x-c)+sqrt(eta)sin(u)p, -sin(u)/sqrt(eta)(x-c)+cos(u)p), S_r(x,p)=(x,p-(2<p,h_r(x)>/||h_r(x)||^2)h_r(x)). Real division by zero is zero, so a zero normal gives the identity bounce. Let ell=volume_E tensor volume_E, with canonical Hilbert-space Lebesgue measure. For every integer n>=0 and horizon T>=0, let Delta_n(T) consist of real tuples 0<t_0<...<t_(n-1)<T. Equivalently, prepending 0 produces a strictly increasing tuple and every entry is less than T. Let Prefix_n(T) be this subtype and m_n,T the comap of Lebesgue measure on R^n under its inclusion. This is unnormalized simplex volume. For n=0 the tuple is empty and its zero-dimensional volume is one; for T=0 and n>0 the subtype is empty. Write q_0=0 and q_(j+1)=t_j. Starting at z_0=z, define z_(j+1)=S_r(Phi_(y,r,t_j-q_j)(z_j)) for 0<=j<n. Define records K_j=(q_j,z_j), each embedded in the live branch of (R_nonnegative x (E x E)) plus a cemetery symbol. For a general history of n+1 such records, the path reconstruction Psi at s in [0,T] starts from z and visits records in increasing index order: a live record (a,w) replaces the accumulator by Phi_(y,r,s-a)(w) exactly when a<=s; future records and cemetery records leave it unchanged. Here s-a is nonnegative subtraction. Define Gamma_(y,r,z,t)=Psi(K), the actual finite prescribed path; thus its value at an event is the post-bounce value. Let A_(y,r)(z,t)=Gamma_(y,r,z,t)(T). There exists rho:Prefix_n(T)->Prefix_n(T) with (rho t)_i=T-t_(n-1-i) for every i. It is Borel measurable, involutive, and preserves m_n,T. For all y,r,z,t, the terminal identity is A_(y,r)(z,t)=Phi_(y,r,T-q_n)(z_n). The map (y,r,z,t)->A_(y,r)(z,t) is jointly Borel measurable. For each y,r,t, z->A_(y,r)(z,t) preserves ell. The reversed endpoint satisfies A_(y,r)(R(A_(y,r)(z,t)),rho t)=R(z). Define Theta_(y,r)(z,t)=(R(A_(y,r)(z,t)),rho t). The map (y,r,z,t)->Theta_(y,r)(z,t) is jointly Borel measurable. For each y,r, Theta_(y,r) is an involution and preserves ell tensor m_n,T, in phase-first order. Every measure-preservation assertion includes measurability and equality of pushforward measures. All conclusions include n=0, T=0, zero reflection normals and rank-zero E; measurability, inverses, sigma finiteness and volume identities are proved internally from the six analytic assumptions. This is the finite prescribed endpoint/time change of variables used in the Appendix A.1 reversal argument. It does not assert pointwise time reversal of right-continuous paths at event times. Gibbs-weight balance, stationary averaging and invariant probability laws, Markov properties, hypocoercivity, implementation error, expected oracle costs, main sampling 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_endpoint_time_reversal_laws
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {V : E → ℝ} {α β : ℝ≥0} {η : ℝ}
    (hα : 0 < (α : ℝ)) (hαβ : α ≤ β) (hV : ContDiff ℝ 2 V)
    (hH : ∀ x v : E,
      (α : ℝ) * ‖v‖ ^ 2 ≤ (fderiv ℝ (fderiv ℝ V) x v) v ∧
      (fderiv ℝ (fderiv ℝ V) x v) v ≤ (β : ℝ) * ‖v‖ ^ 2)
    (hη : 0 < η) (hβη : (β : ℝ) * η ≤ 1) : actual_endpoint_time_reversal_statement hα hαβ hV hH hη hβη

Exact module and namespace context

Full Lean proposition (definition) · actual_endpoint_time_reversal_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_endpoint_time_reversal_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 := by
  classical
  exact
    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 Rec := (ℝ≥0 × (E × E)) ⊕ Unit
    let Hist : ℕ → Type _ := fun n => Fin (n + 1) → Rec
    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 Path : ℝ≥0 → Type _ := fun T => {s : ℝ≥0 // s ≤ T} → E × E
    let Ψ : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) → Hist n → Path T :=
      fun y xRef z₀ n T h s =>
        Fin.foldl (n + 1) (fun z j => (h j).elim
          (fun a => if a.1 ≤ s.val then Φ y xRef ((s.val - a.1 : ℝ≥0) : ℝ) a.2 else z)
          (fun _ => z)) z₀
    let Γ : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) → Prefix n T → Path T :=
      fun y xRef z₀ n T t => Ψ y xRef z₀ n T (K y xRef z₀ n T t)
    let R : (E × E) → (E × E) := fun z => (z.1, -z.2)
    let ell : Measure (E × E) := (volume : Measure E).prod (volume : Measure E)
    ∀ n : ℕ, ∀ T : ℝ≥0, ∃ rho : Prefix n T → Prefix n T,
      (∀ t : Prefix n T, ∀ i : Fin n, (rho t).val i = (T : ℝ) - t.val i.rev) ∧
      Measurable rho ∧ Function.Involutive rho ∧ MeasurePreserving rho (m n T) (m n T) ∧
      let A : E → E → (E × E) → Prefix n T → (E × E) :=
        fun y r z t => Γ y r z n T t ⟨T, le_rfl⟩
      let Theta : E → E → ((E × E) × Prefix n T) → ((E × E) × Prefix n T) :=
        fun y r q => (R (A y r q.1 q.2), rho q.2)
      (∀ y r : E, ∀ z : E × E, ∀ t : Prefix n T,
        A y r z t = Φ y r ((T : ℝ) -
          (Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) (Fin.last n))
          (zAt y r z n T t (Fin.last n))) ∧
      Measurable (fun p : ((E × E) × (E × E)) × Prefix n T =>
        A p.1.1.1 p.1.1.2 p.1.2 p.2) ∧
      (∀ y r : E, ∀ t : Prefix n T,
        MeasurePreserving (fun z => A y r z t) ell ell) ∧
      (∀ y r : E, ∀ z : E × E, ∀ t : Prefix n T,
        A y r (R (A y r z t)) (rho t) = R z) ∧
      Measurable (fun p : ((E × E) × (E × E)) × Prefix n T =>
        Theta p.1.1.1 p.1.1.2 (p.1.2, p.2)) ∧
      (∀ y r : E, Function.Involutive (Theta y r)) ∧
      (∀ y r : E, MeasurePreserving (Theta y r) (ell.prod (m n T)) (ell.prod (m n T)))

Exact module and namespace context

Proof roadmap

1Reverse the ordered time simplex
Set rho(t)_i=T-t_(n-1-i). Reversal reverses index order and subtraction reverses inequalities, so strict ordering is preserved. The original upper bound gives positivity, and the original positivity gives the new upper bound T. Applying the formula twice restores every coordinate. On R^n this map is a coordinate permutation composed with coordinatewise reflection and translation, each preserving Lebesgue measure. Its invariant measurable simplex therefore inherits preservation of the exact comap measure m. This includes the unique empty tuple.
2Cancel a finite reversed sequence
For updates f_i and a map C satisfying f_i(C(f_i(x)))=C(x), process f_0 through f_(n-1), then apply C and process the updates in reverse order. Induction removes the outer matching pair and leaves C(x). A second finite induction identifies a fold with a prescribed sequence whenever its initial value and one-step recurrences agree. These algebraic statements will be applied to the actual flow and bounce.
3Express the endpoint as a finite word of gaps
Append T and prepend 0 to define gaps g_0=t_0, g_j=t_j-t_(j-1), g_n=T-t_(n-1). Reversing the tuple reverses the n+1 gaps exactly. The recursive post-bounce states give the terminal map Phi_(g_n) S Phi_(g_(n-1)) ... S Phi_(g_0). Equivalently start from S(z) and fold f_i=Phi_(g_i) composed with S through i=0,...,n. The first pair of bounces cancels because S is involutive. For n=0 this is just Phi_T(z).
4Derive the inverse endpoint and its fiber volume
Take C=S composed with R. The identities S^2=R^2=id, RS=SR and R Phi_u R=Phi_(-u), together with the inverse-flow law, imply f_i C f_i=C. Apply reversed-word cancellation and use the reversed-gap identity. The result is A_(rho t)(R A_t(z))=R(z). Separately, finite induction shows a composition of volume-preserving updates preserves volume; since S and each Phi_u preserve ell, so does A_t.
5Connect the finite word to the actual path at T
The verified ordered-prefix theorem supplies measurability of Delta. The verified finite-count path theorem supplies joint measurability of Gamma and its last-interval formula. Evaluating the measurable function-valued path at T preserves measurability. For n>0 the last event is strictly before T; for n=0 its grid point is zero and T≥0. There is no later record than the final index. Thus the interval formula yields Gamma(T)=Phi_(T-q_n)(z_n), exactly the finite word above. This connection uses the actual live/cemetery history and the original six analytic assumptions.
6Assemble the jointly measurable preserving involution
Reuse the actual phase-volume theorem for every flow, bounce and reversal identity; no such identity is an extra public premise. The terminal-data connection gives the measurable endpoint A and its fiber-volume and reversal laws. Hence Theta(z,t)=(R A_t(z),rho t) is jointly measurable and Theta^2(z,t)=(R R z,rho^2 t)=(z,t). The simplex inclusion pushes m to restricted ambient Lebesgue measure, establishing sigma finiteness. In time-first order, apply the measurable skew-product theorem to rho and the ell-preserving fibers z→R A_t(z); swap coordinates before and after to obtain preservation of ell tensor m in the stated phase-first order. This finishes the endpoint change of variables; weighting by Gibbs densities is a later edge.

Full assumptions and notation

All objects and hypotheses

Finite-dimensional real inner-product Borel E, including rank zero.
alpha,beta≥0; alpha>0; alpha≤beta; V is C2; alpha||v||^2≤D2V(x)[v,v]≤beta||v||^2 for all x,v; eta>0; beta*eta≤1.
All n≥0, T≥0, y,r,z and strictly ordered event tuples; zero events and zero normals are included.
The exact unnormalized simplex comap m and phase-first product ell tensor m are fixed definitions. Measurability, sigma finiteness, inverses and volume preservation are proved dependencies or conclusions.

Mathematical proof

1. Reverse the ordered time simplex

Set rho(t)_i=T-t_(n-1-i). Reversal reverses index order and subtraction reverses inequalities, so strict ordering is preserved. The original upper bound gives positivity, and the original positivity gives the new upper bound T. Applying the formula twice restores every coordinate. On R^n this map is a coordinate permutation composed with coordinatewise reflection and translation, each preserving Lebesgue measure. Its invariant measurable simplex therefore inherits preservation of the exact comap measure m. This includes the unique empty tuple.

\[\rho(t)_i=T-t_{n-1-i},\quad \rho^2=\mathrm{id},\quad \rho_\#m_{n,T}=m_{n,T}.\]

Corresponding Lean step

private def delta (n : ℕ) (T : ℝ) : Set (Fin n → ℝ) :=
  {t | StrictMono (Fin.cons (0 : ℝ) t) ∧ ∀ i, t i < T}
private def reverseTime {n : ℕ} (T : ℝ) (t : Fin n → ℝ) : Fin n → ℝ :=
  fun i => T - t i.rev

private theorem reverseTime_involutive (n : ℕ) (T : ℝ) :
    Function.Involutive (reverseTime (n := n) T) := by
  intro t; funext i
  simp [reverseTime]

private theorem reverseTime_mem {n : ℕ} {T : ℝ} {t : Fin n → ℝ}
    (ht : t ∈ delta n T) : reverseTime T t ∈ delta n T := by
  obtain ⟨hpos, hmono⟩ := Fin.strictMono_cons.mp ht.1
  refine ⟨Fin.strictMono_cons.mpr ⟨?_, ?_⟩, ?_⟩
  · intro i
    exact sub_pos.mpr (ht.2 i.rev)
  · intro i j hij
    exact sub_lt_sub_left (hmono (Fin.rev_lt_rev.mpr hij)) T
  · intro i
    exact sub_lt_self T (hpos i.rev)

private theorem reverseTime_measurable (n : ℕ) (T : ℝ) :
    Measurable (reverseTime (n := n) T) := by
  apply measurable_pi_lambda
  intro i
  exact measurable_const.sub (measurable_pi_apply i.rev)

private theorem reverseTime_volume (n : ℕ) (T : ℝ) :
    MeasurePreserving (reverseTime (n := n) T) volume volume := by
  have hp := volume_measurePreserving_piCongrLeft (fun _ : Fin n => ℝ) Fin.revPerm
  have heq : (fun t : Fin n → ℝ => fun i : Fin n => t i.rev) =
      MeasurableEquiv.piCongrLeft (fun _ : Fin n => ℝ) Fin.revPerm := by
    funext t i
    symm
    simpa only [Fin.revPerm_apply, Fin.rev_rev] using
      (MeasurableEquiv.piCongrLeft_apply_apply (β := fun _ : Fin n => ℝ) Fin.revPerm t i.rev)
  rw [← heq] at hp
  have hc : MeasurePreserving (fun t : Fin n → ℝ => fun i => T - t i) volume volume :=
    volume_preserving_pi (fun _ : Fin n => (volume : Measure ℝ).measurePreserving_sub_left T)
  exact hc.comp hp

private def rho (n : ℕ) (T : ℝ) (t : delta n T) : delta n T :=
  ⟨reverseTime T t.val, reverseTime_mem t.property⟩

private theorem rho_measurable (n : ℕ) (T : ℝ) : Measurable (rho n T) :=
  ((reverseTime_measurable n T).comp measurable_subtype_coe).subtype_mk

private theorem rho_involutive (n : ℕ) (T : ℝ) : Function.Involutive (rho n T) := by
  intro t; apply Subtype.ext
  exact reverseTime_involutive n T t.val

private theorem rho_volume (n : ℕ) (T : ℝ) (hs : MeasurableSet (delta n T)) :
    MeasurePreserving (rho n T) (Measure.comap Subtype.val volume)
      (Measure.comap Subtype.val volume) := by
  have he : reverseTime (n := n) T ⁻¹' delta n T = delta n T := by
    ext t
    constructor
    · intro ht
      have hh := reverseTime_mem ht
      simpa only [reverseTime_involutive n T t] using hh
    · exact reverseTime_mem
  have hr := (reverseTime_volume n T).restrict_preimage hs
  rw [he] at hr
  have hcoe := measurePreserving_subtype_coe (μa := (volume : Measure (Fin n → ℝ))) hs
  refine ⟨rho_measurable n T, ?_⟩
  apply (MeasurableEmbedding.subtype_coe hs).map_injective
  rw [Measure.map_map measurable_subtype_coe (rho_measurable n T)]
  exact (hr.comp hcoe).map_eq.trans hcoe.map_eq.symm



/-- Cancellation of a finite word against its reverse under a common reversing map. -/