Samplinglib mathematical lesson

Actual PBPS bounded path functional expansion

AutoSamplingTheory.ExampleCases.ProximalBPS.ActualBoundedPathExpansion.actual_bounded_path_functional_expansion · theorem · Teaching coverage

Read this first

Mathematical statement

Let E be a finite-dimensional real inner-product space with its Borel sigma algebra; rank zero is allowed. Let alpha,beta be nonnegative reals, eta real and V:E→R. Assume alpha>0, alpha≤beta, V is C2, alpha||v||^2≤D2V(x)[v,v]≤beta||v||^2 for all x,v, eta>0 and beta*eta≤1. No additional dynamical, probability, density, integrability or independence hypothesis is supplied. For every y,r in E put c=y-eta grad V(r). Define Phi_u(x,p)=(c+cos(u)(x-c)+sqrt(eta)sin(u)p, -sin(u)/sqrt(eta)(x-c)+cos(u)p). Set h_r(x)=grad V(x)-grad V(r), S_r(x,p)=(x,p-(2<p,h_r(x)>/||h_r(x)||^2)h_r(x)), lambda_r(x,p)=sqrt(eta)max(0,<p,h_r(x)>), and Lambda_z(u)=integral_0^u lambda_r(Phi_s(z))ds for u≥0. Division by zero is totalized by zero, so zero normal leaves the velocity unchanged. The Lebesgue interval integral uses the real time coordinate. Let P be the countable product of unit-rate real exponential probability measures, on real clock streams w; set epsilon_j(w)=max(w_j,0). For each phase z and threshold e≥0 define tau_z(e)=inf{u≥0:Lambda_z(u)≥e}, with value infinity if the set is empty. The source recursion starts with record_0=live(0,z0). From live(a,z), threshold epsilon_j gives stopped if tau_z(epsilon_j)=infinity and otherwise live(a+tau_z(epsilon_j),S_r(Phi_tau(z))); stopped remains stopped. Event time T_j is the time in a live record and infinity in a stopped record. Let I_j(s)={T_j≤s<T_(j+1)}. For n≥0 and T≥0 let Delta_n(T)={0<t1<...<tn<T}. Its measure m_n is the comap of Fin-n product Lebesgue measure under the subtype inclusion. Set a0=0, ai=ti, z_i=S_r(Phi_(a_i-a_(i-1))(z_(i-1))) and K_n(t)_j=live(a_j,z_j), j=0,...,n. For any tagged history h, the total interpolation Psi_n(h)(s), 0≤s≤T, starts from z0 and scans j in increasing order: live(a,z) with a≤s replaces the accumulator by Phi_(max(s-a,0))(z); every other record leaves it unchanged. Let Gamma_n(t)=Psi_n(K_n(t)). In particular a jump time carries the post-reflection phase. Path_T is the set of all phase-valued functions on[0,T], with its coordinate-product sigma algebra; no Skorokhod or supremum-norm Borel identification is asserted. Define the real weight w_n(t)=exp(-integral_0^T lambda_r(Gamma_n(t)(min(max(s,0),T)))ds) times product_(i=1)^n lambda_r(Phi_(a_i-a_(i-1))(z_(i-1))). The clamp is only the real-time extension used by the integral; it agrees with the path coordinate on[0,T]. Every bounce factor uses the incoming phase, and the whole-path integral includes the final no-event arc. Empty products are1; the n=0 simplex is the singleton empty tuple. There exists one phase process Z(y,r,z0,s,w), jointly measurable in all displayed arguments. On every raw stream belonging to I_n(s) whose nth record is live(a,z), its value is exactly Phi_(max(s-a,0))(z). If no covering I_n(s) exists, its value is z0. For every fixed y,r,z0 it equals z0 at time0 P-almost surely. These clauses bind the witness to the literal stopped-clock process, including exceptional raw streams; no arbitrary process with a convenient distribution may replace it. For all deterministic y,r,z0,T, write Z_T(w)(s)=Z(y,r,z0,s,w). For every measurable real F:Path_T→R and every M≥0 such that |F(p)|≤M for every path p, F(Z_T) is P-integrable, every real function t→F(Gamma_n(t))w_n(t) is m_n-integrable, the series sum_n |integral_Delta_n F(Gamma_n(t))w_n(t)dm_n| converges, and integral F(Z_T(w))dP(w)=sum_(n=0)^infinity integral_Delta_n(T) F(Gamma_n(t))w_n(t)dm_n(t). The statement includes n=0,T=0,rank0,zero rates and stopped/infinite waits. Fixed deterministic parameters and horizon precede the almost-sure statements and integration. Coordinate-product measurability and null-input fallback are explicit ASTIS completions. The source all-count bounded-real A7 identity is realized through the probability-mass partition; the printed uniform rate-cap/factorial domination remains a separate source proof route, not an added premise. No unbounded-test or cost transfer, path-space topology equivalence, restart/Markovness, invariance, hypocoercivity, implementation error, main sampling theorem or actual-input composition is claimed.

\[\mathbb E[F(Z_T)]=\sum_{n=0}^{\infty}\int_{\Delta_n(T)}F(\Gamma_n(t))e^{-\int_0^T\lambda(\Gamma_n(t)(s))ds}\prod_{i=1}^{n}\lambda(z_{i-})\,dm_n(t).\]

Lean statement · actual_bounded_path_functional_expansion

Let E be a finite-dimensional real inner-product space with its Borel sigma algebra; rank zero is allowed. Let alpha,beta be nonnegative reals, eta real and V:E->R. Assume alpha>0, alpha<=beta, V is C2, alpha||v||^2<=D2V(x)[v,v]<=beta||v||^2 for all x,v, eta>0 and beta*eta<=1. No additional dynamical, probability, density, integrability or independence hypothesis is supplied. For every y,r in E put c=y-eta grad V(r). Define Phi_u(x,p)=(c+cos(u)(x-c)+sqrt(eta)sin(u)p, -sin(u)/sqrt(eta)(x-c)+cos(u)p). Set h_r(x)=grad V(x)-grad V(r), S_r(x,p)=(x,p-(2<p,h_r(x)>/||h_r(x)||^2)h_r(x)), lambda_r(x,p)=sqrt(eta)max(0,<p,h_r(x)>), and Lambda_z(u)=integral_0^u lambda_r(Phi_s(z))ds for u>=0. Division by zero is totalized by zero, so zero normal leaves the velocity unchanged. The Lebesgue interval integral uses the real time coordinate. Let P be the countable product of unit-rate real exponential probability measures, on real clock streams w; set epsilon_j(w)=max(w_j,0). For each phase z and threshold e>=0 define tau_z(e)=inf{u>=0:Lambda_z(u)>=e}, with value infinity if the set is empty. The source recursion starts with record_0=live(0,z0). From live(a,z), threshold epsilon_j gives stopped if tau_z(epsilon_j)=infinity and otherwise live(a+tau_z(epsilon_j),S_r(Phi_tau(z))); stopped remains stopped. Event time T_j is the time in a live record and infinity in a stopped record. Let I_j(s)={T_j<=s<T_(j+1)}. For n>=0 and T>=0 let Delta_n(T)={0<t1<...<tn<T}. Its measure m_n is the comap of Fin-n product Lebesgue measure under the subtype inclusion. Set a0=0, ai=ti, z_i=S_r(Phi_(a_i-a_(i-1))(z_(i-1))) and K_n(t)_j=live(a_j,z_j), j=0,...,n. For any tagged history h, the total interpolation Psi_n(h)(s), 0<=s<=T, starts from z0 and scans j in increasing order: live(a,z) with a<=s replaces the accumulator by Phi_(max(s-a,0))(z); every other record leaves it unchanged. Let Gamma_n(t)=Psi_n(K_n(t)). In particular a jump time carries the post-reflection phase. Path_T is the set of all phase-valued functions on[0,T], with its coordinate-product sigma algebra; no Skorokhod or supremum-norm Borel identification is asserted. Define the real weight w_n(t)=exp(-integral_0^T lambda_r(Gamma_n(t)(min(max(s,0),T)))ds) times product_(i=1)^n lambda_r(Phi_(a_i-a_(i-1))(z_(i-1))). The clamp is only the real-time extension used by the integral; it agrees with the path coordinate on[0,T]. Every bounce factor uses the incoming phase, and the whole-path integral includes the final no-event arc. Empty products are1; the n=0 simplex is the singleton empty tuple. There exists one phase process Z(y,r,z0,s,w), jointly measurable in all displayed arguments. On every raw stream belonging to I_n(s) whose nth record is live(a,z), its value is exactly Phi_(max(s-a,0))(z). If no covering I_n(s) exists, its value is z0. For every fixed y,r,z0 it equals z0 at time0 P-almost surely. These clauses bind the witness to the literal stopped-clock process, including exceptional raw streams; no arbitrary process with a convenient distribution may replace it. For all deterministic y,r,z0,T, write Z_T(w)(s)=Z(y,r,z0,s,w). For every measurable real F:Path_T->R and every M>=0 such that |F(p)|<=M for every path p, F(Z_T) is P-integrable, every real function t->F(Gamma_n(t))w_n(t) is m_n-integrable, the series sum_n |integral_Delta_n F(Gamma_n(t))w_n(t)dm_n| converges, and integral F(Z_T(w))dP(w)=sum_(n=0)^infinity integral_Delta_n(T) F(Gamma_n(t))w_n(t)dm_n(t). The statement includes n=0,T=0,rank0,zero rates and stopped/infinite waits. Fixed deterministic parameters and horizon precede the almost-sure statements and integration. Coordinate-product measurability and null-input fallback are explicit ASTIS completions. The source all-count bounded-real A7 identity is realized through the probability-mass partition; the printed uniform rate-cap/factorial domination remains a separate source proof route, not an added premise. No unbounded-test or cost transfer, path-space topology equivalence, restart/Markovness, invariance, hypocoercivity, implementation error, main sampling theorem or actual-input composition is claimed.

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_bounded_path_functional_expansion
    {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_bounded_path_statement hα hαβ hV hH hη hβη

Exact module and namespace context

Full Lean proposition (definition) · actual_bounded_path_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 noncomputable def actual_bounded_path_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 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 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 eventTime : E → E → (E × E) → (ℕ → ℝ) → ℕ → WithTop ℝ≥0 :=
      fun y xRef z₀ w j => (record y xRef z₀ (ε w) j).elim
        (fun a => (a.1 : WithTop ℝ≥0)) (fun _ => ⊤)
    let I : E → E → (E × E) → ℝ≥0 → ℕ → Set (ℕ → ℝ) :=
      fun y xRef z₀ T n => {w | eventTime y xRef z₀ w n ≤ (T : WithTop ℝ≥0) ∧
        (T : WithTop ℝ≥0) < eventTime y xRef z₀ w (n + 1)}
    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 wgt : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) → Prefix n T → ℝ :=
      fun y xRef z₀ n T t =>
        Real.exp (-(∫ s in (0 : ℝ)..(T : ℝ),
          rate xRef (Γ y xRef z₀ n T t ⟨min (Real.toNNReal s) T, min_le_right _ _⟩))) *
        ∏ 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))
    ∃ Z : E → E → (E × E) → ℝ≥0 → (ℕ → ℝ) → (E × E),
      Measurable (fun a : ((E × E) × (E × E)) × ℝ≥0 × (ℕ → ℝ) =>
        Z a.1.1.1 a.1.1.2 a.1.2 a.2.1 a.2.2) ∧
      (∀ y xRef : E, ∀ z₀ : E × E, ∀ w : ℕ → ℝ, ∀ s : ℝ≥0,
        ∀ n : ℕ, ∀ a : ℝ≥0 × (E × E), w ∈ I y xRef z₀ s n →
          record y xRef z₀ (ε w) n = Sum.inl a →
          Z y xRef z₀ s w = Φ y xRef ((s - a.1 : ℝ≥0) : ℝ) a.2) ∧
      (∀ y xRef : E, ∀ z₀ : E × E, ∀ w : ℕ → ℝ, ∀ s : ℝ≥0,
        (¬ ∃ n, w ∈ I y xRef z₀ s n) → Z y xRef z₀ s w = z₀) ∧
      (∀ y xRef : E, ∀ z₀ : E × E, ∀ᵐ w ∂P, Z y xRef z₀ 0 w = z₀) ∧
      (∀ y xRef : E, ∀ z₀ : E × E, ∀ T : ℝ≥0,
        let ZT : (ℕ → ℝ) → Path T := fun u s => Z y xRef z₀ s.val u
        ∀ F : Path T → ℝ, Measurable F → ∀ M : ℝ, 0 ≤ M →
          (∀ p : Path T, |F p| ≤ M) →
          Integrable (fun u => F (ZT u)) P ∧
          (∀ n : ℕ, Integrable (fun t : Prefix n T =>
            F (Γ y xRef z₀ n T t) * wgt y xRef z₀ n T t) (m n T)) ∧
          Summable (fun n : ℕ => |∫ t : Prefix n T,
            F (Γ y xRef z₀ n T t) * wgt y xRef z₀ n T t ∂m n T|) ∧
          (∫ u, F (ZT u) ∂P) = ∑' n : ℕ, ∫ t : Prefix n T,
            F (Γ y xRef z₀ n T t) * wgt y xRef z₀ n T t ∂m n T)

Exact module and namespace context

Proof roadmap

1Use the actual path and bound its observable
Reuse the same jointly measurable Z from the actual finite-count law, keeping its raw covered-arc formula, uncovered fallback and almost-sure initialization. Fix y,r,z0,T. Coordinate measurability makes Z_T measurable, hence F composed with Z_T is measurable. The canonical exponential input has probability1, and the bound |F|≤M makes its absolute integral finite. This derives integrability without assuming any path-law density.
2Identify each finite-sector weight
For a fixed n, reuse measurable actual history, prescribed history K_n, interpolation Gamma_n and density rho_n. The already verified prescribed-path identity gives rho_n=ofReal(w_n), with its whole-hazard integral and all incoming bounce rates. Each rate is sqrt(eta) times a nonnegative part, so w_n≥0. Thus rho_n is finite pointwise and rho_n.toReal=w_n; zero rates require no division.
3Transport a signed integral through the finite-count joint law
Restrict P to the measurable event N(T)=n. Its joint history/path pushforward equals the pushforward of m_n.withDensity(rho_n) under (K_n,Gamma_n). The measurable test (h,p)→F(p) transfers integrability through these two pushforwards. Because rho_n is measurable and finite, the withDensity conversion identifies both integrability and integral with the real product F(Gamma_n)rho_n.toReal. Replace the latter by F(Gamma_n)w_n. The signed integral is therefore justified before summation.
4Sum the measurable count partition
For any measurable natural-valued N, the sets {N=n} are measurable and pairwise disjoint and their union is the whole sample space. Countable additivity of integrals for an integrable real function gives an unconditional HasSum: the limit over all finite subsets of counts equals the whole-space integral. This unconditional real summability implies absolute summability. Apply it to F(Z_T), whose absolute integrability was derived above. This realizes the probability-partition route in the source graph without a supplied rate-cap hypothesis.
5Assemble the complete bounded-real expansion
For each n, apply the signed-sector lemma to the actual finite-count law and to integrability restricted from P. The measurable count from that same law partitions every raw stream, with its specified total convention. Substitute the proved sector integral identities into the absolutely convergent count sum. This simultaneously gives every weighted-sector integrability, the absolute series and the exact expectation identity for all bounded coordinate-measurable real F. No event-time endpoint convention or process representative is changed.

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 every x,v; eta>0; beta*eta≤1.
Every deterministic y,r,z0 and finite T≥0.
F is real-valued and measurable for the coordinate-product path sigma, with a global nonnegative bound M on |F|.
All process existence, joint measurability, sector laws, integrability and summability are conclusions or internally consumed proved dependencies, never added provider premises.

Mathematical proof

1. Use the actual path and bound its observable

Reuse the same jointly measurable Z from the actual finite-count law, keeping its raw covered-arc formula, uncovered fallback and almost-sure initialization. Fix y,r,z0,T. Coordinate measurability makes Z_T measurable, hence F composed with Z_T is measurable. The canonical exponential input has probability1, and the bound |F|≤M makes its absolute integral finite. This derives integrability without assuming any path-law density.

\[\int |F(Z_T)|\,dP\le M P(\Omega)=M.\]

Corresponding Lean step

  obtain ⟨Z, hZM, hZarc, hZfallback, hZzero, hAll⟩ :=
    ActualFiniteCountPath.actual_finite_count_path_law hα hαβ hV hH hη hβη
  refine ⟨Z, hZM, hZarc, hZfallback, hZzero, ?_⟩
  intro y xRef z₀ T
  let ZT : (ℕ → ℝ) → Path T := fun u s => Z y xRef z₀ s.val u
  dsimp only
  intro F hF M hM hbound
  letI : IsProbabilityMeasure P :=
    AutoSamplingTheory.TechnicalLemmas.Probability.UnitExponentialProduct.unit_exponential_product_laws.1
  have hbase := (hAll 0 T).2.2.2 y xRef z₀
  have hZT : Measurable ZT := hbase.2.1
  have hN : Measurable (N y xRef z₀ T) := hbase.2.2.1
  have hi : Integrable (fun u => F (ZT u)) P :=
    ⟨(hF.comp hZT).aestronglyMeasurable,
      HasFiniteIntegral.of_bounded (Filter.Eventually.of_forall
        (fun u => by simpa only [Real.norm_eq_abs] using hbound (ZT u)))⟩