AutoSamplingTheory.ExampleCases.ProximalBPS.ActualFiniteHistoryTailLaw

Samplinglib mathematical lesson

Actual PBPS finite history and unused-clock tail law

AutoSamplingTheory.ExampleCases.ProximalBPS.ActualFiniteHistoryTailLaw.actual_finite_history_tail_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 n≥0 define H_n(w)=(R_j(ε(w)))_(0≤j≤n)∈D^(Fin(n+1)), Y_n(w)_k=w_(n+k), and F_n=σ(w↦w_k:k<n). Then H_n and Y_n are measurable for the ambient product Borel structures. If w,w′ agree for all k<n, then H_n(w)=H_n(w′), for all real sequences w,w′, including the ambient extension. Moreover H_n is F_n-measurable. The entire countable unused raw tail has law (Y_n)_*P=P and is independent of H_n. Its joint law is (H_n,Y_n)_*P=(H_n)_*P⊗P. For every measurable A⊆D^(Fin(n+1)), (Y_n)_*(P restricted to H_n⁻¹(A))=P(H_n⁻¹(A))·P. All conclusions hold for every y,r,z₀,n with the standing analytic parameters fixed. The last identity is unnormalized and includes P(H_n⁻¹(A))=0; no division by a point-history probability or regular conditional distribution is claimed. At n=0 the history is constant and Y₀ is the identity. Tagged stopped histories are retained without assigning a phase at infinity. The tail starts at raw coordinate n, which represents the source E_(n+1). No measurability, causality, independence or law provider is assumed. This is an attributed ASTIS completion of the deterministic-depth unused-input probability bridge implicit in AppendixA.1(A.7), using the authors actual recursion and independent clock model. Conditional random-hazard next-wait survival, conditional finite-event densities/final survival/iteration, 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.

\[(Y_n)_*(P|_{H_n^{-1}(A)})=P(H_n^{-1}(A))\,P.\]

Lean statement · actual_finite_history_tail_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_finite_history_tail_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_finite_history_tail_law_statement hα hαβ hV hH hη hβη

Exact module and namespace context

Full Lean proposition (definition) · actual_finite_history_tail_law_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_finite_history_tail_law_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 tail : ℕ → (ℕ → ℝ) → (ℕ → ℝ) := fun n w k => w (n + k)
    let past : ℕ → MeasurableSpace (ℕ → ℝ) := fun n =>
      ⨆ k ∈ Set.Iio n, MeasurableSpace.comap (fun w : ℕ → ℝ => w k) inferInstance
    ∀ y xRef : E, ∀ z₀ : E × E, ∀ n : ℕ,
      Measurable (history y xRef z₀ n) ∧ Measurable (tail n) ∧
      (∀ (w w' : ℕ → ℝ), (∀ k < n, w k = w' k) →
        history y xRef z₀ n w = history y xRef z₀ n w') ∧
      Measurable[past n] (history y xRef z₀ n) ∧
      Measure.map (tail n) P = P ∧
      IndepFun (history y xRef z₀ n) (tail n) P ∧
      Measure.map (fun w => (history y xRef z₀ n w, tail n w)) P =
        (Measure.map (history y xRef z₀ n) P).prod P ∧
      (∀ A : Set (Fin (n + 1) → ((ℝ≥0 × (E × E)) ⊕ Unit)), MeasurableSet A →
        Measure.map (tail n) (P.restrict (history y xRef z₀ n ⁻¹' A)) =
          (P (history y xRef z₀ n ⁻¹' A)) • P)


set_option maxHeartbeats 1600000 in

Exact module and namespace context

Proof roadmap

1Keep the actual recursion and consume its existing producers
Retain the literal harmonic flow, reflection, intensity, stopped crossing time and tagged recursion. The already compiled finite-recursion theorem supplies joint Borel measurability of each R_j; the canonical exponential-product theorem supplies probability and mutual independence of raw coordinate clocks. No independence or regularity certificate is requested from the caller.
2Prove finite-prefix causality and ambient measurability
Induct on m. R₀ is constant. The step R_(m+1) uses only e_m and R_m, so agreement below m+1 gives agreement at the step and by induction at the previous record. For each j≤n, agreement below n therefore gives the same record and hence the same history. Measurable coordinate clipping composed with the existing joint-measurable recursion gives ambient H_n measurability; coordinate reindexing gives ambient Y_n measurability.
3Expose the consumed-prefix measurable input
For this proof only, define ē_k(w)=ε_k(w) when k<n and zero otherwise. Each used coordinate is F_n-measurable by inclusion of its generated sigma algebra into F_n. Clipping is Borel; unused coordinates are constant. Thus the full clipped/truncated sequence is F_n-measurable. This auxiliary sequence proves a factorization of H_n; it does not replace P or alter the actual algorithm.
4Derive history measurability in the past sigma algebra
For every j∈Fin(n+1), the two threshold streams ē(w) and ε(w) agree below j. Causality makes the resulting jth records identical. Compose the existing jointly measurable R_j with deterministic parameters and ē, and use this equality. Coordinatewise product measurability now proves H_n is F_n-measurable, including the live/stopped tag. The smaller domain sigma algebra is explicit; ambient measurability alone would not suffice.
5Separate the independent past and unused future
Put G_n=σ(w↦w_k:k≥n). Every coordinate of Y_n belongs to this sigma algebra. Mutual independence of all raw coordinate functions, together with their ambient measurability, gives independence of the generated sigma algebras for disjoint index sets [0,n) and [n,∞). The existing Mathlib theorem extends cylinder independence to the whole generated sigma algebras. Independence descends along the inclusions generated by H_n and Y_n. Hence H_n and the full countable tail are independent.
6Identify the unchanged tail and restricted laws
The injection k↦n+k reindexes identical Exp(1) factors, so the infinite-product pushforward is P. Independence and measurability identify the joint pushforward with the product of its two marginals. Finally, for any Borel tail event B, evaluate the restricted pushforward as P(Y_n∈B and H_n∈A); independence makes this P(H_n∈A)P(Y_n∈B), and the tail law replaces the last factor by P(B). Equality on every Borel B proves the unnormalized measure identity. No positivity, point-event normalization or conditional kernel existence is used.

Full assumptions and notation

All objects and hypotheses

E is finite-dimensional over ℝ with inner product and Borel measurable structure; rank zero is included. V:E→ℝ is C².
The six analytic hypotheses are α>0, α≤β, V∈C², the pointwise α/β Hessian bounds for every x,v, η>0, and βη≤1. α,β are nonnegative.
y,r,z₀ and n are deterministic and universally quantified. No random initial state or stopping index is included.
P, ε, all eight actual recursion definitions, H_n,Y_n and F_n are literal definitions. Measurability, prefix causality, independence and distributional identities are conclusions.
A is any Borel history event, with no positive-probability assumption. The restricted law is unnormalized. Zero rates, zero normals, infinite waits and stopped branches are allowed.

Mathematical proof

1. Keep the actual recursion and consume its existing producers

Retain the literal harmonic flow, reflection, intensity, stopped crossing time and tagged recursion. The already compiled finite-recursion theorem supplies joint Borel measurability of each R_j; the canonical exponential-product theorem supplies probability and mutual independence of raw coordinate clocks. No independence or regularity certificate is requested from the caller.

\[R_0=\operatorname{live}(0,z_0),\quad R_{j+1}=\operatorname{next}(\epsilon_j,R_j),\quad H_n=(R_0,\ldots,R_n),\quad Y_n(w)=(w_{n+k})_{k\ge0}.\]

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 tail : ℕ → (ℕ → ℝ) → (ℕ → ℝ) := fun n w k => w (n + k)
  let past : ℕ → MeasurableSpace (ℕ → ℝ) := fun n =>
    ⨆ k ∈ Set.Iio n, MeasurableSpace.comap (fun w : ℕ → ℝ => w k) inferInstance
  change
  ∀ y xRef : E, ∀ z₀ : E × E, ∀ n : ℕ,
      Measurable (history y xRef z₀ n) ∧ Measurable (tail n) ∧
      (∀ (w w' : ℕ → ℝ), (∀ k < n, w k = w' k) →
        history y xRef z₀ n w = history y xRef z₀ n w') ∧
      Measurable[past n] (history y xRef z₀ n) ∧
      Measure.map (tail n) P = P ∧
      IndepFun (history y xRef z₀ n) (tail n) P ∧
      Measure.map (fun w => (history y xRef z₀ n w, tail n w)) P =
        (Measure.map (history y xRef z₀ n) P).prod P ∧
      (∀ A : Set (Fin (n + 1) → ((ℝ≥0 × (E × E)) ⊕ Unit)), MeasurableSet A →
        Measure.map (tail n) (P.restrict (history y xRef z₀ n ⁻¹' A)) =
          (P (history y xRef z₀ n ⁻¹' A)) • P)

  have hrec := ActualFiniteJumpRecursion.actual_fixed_reference_finite_jump_recursion
    hα hαβ hV hH hη hβη
  have hR (j : ℕ) : Measurable (fun a : (E × E) × (E × E) × (ℕ → ℝ≥0) =>
      record a.1.1 a.1.2 a.2.1 a.2.2 j) := hrec.2.2.2.1 j
  have hinput := AutoSamplingTheory.TechnicalLemmas.Probability.UnitExponentialProduct.unit_exponential_product_laws
  letI : IsProbabilityMeasure P := hinput.1
  letI : IsProbabilityMeasure (expMeasure (1 : ℝ)) :=
    isProbabilityMeasure_expMeasure zero_lt_one
  have hclock : iIndepFun (fun k (w : ℕ → ℝ) => w k) P := hinput.2.2.1
  intro y xRef z₀ n