AutoSamplingTheory.ExampleCases.ProximalBPS.ActualFiniteFirstEventLaw

Samplinglib mathematical lesson

Actual PBPS finite first-event density and post-bounce law

AutoSamplingTheory.ExampleCases.ProximalBPS.ActualFiniteFirstEventLaw.actual_finite_first_event_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². Let α,β≥0 and η∈ℝ satisfy α>0, α≤β, α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for every x,v∈E, η>0 and βη≤1. Fix arbitrary y,r∈E and z=(x,p)∈E×E. Define c=y−η∇V(r), Φ_s(z)=(c+cos(s)(x−c)+√η sin(s)p, −sin(s)(x−c)/√η+cos(s)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)‖²), and λ_r(x,p)=√η max{0,〈p,g_r(x)〉}. Total real division makes S_r the identity when g_r(x)=0. For t≥0 set Λ_z(t)=∫₀ᵗλ_r(Φ_s(z))ds and τ_z(e)=inf{t≥0:Λ_z(t)≥e}∈[0,∞], with inf empty=∞. Let Ω=ℝ^ℕ, P=⊗_(k≥0)Exp(1), ε_k(sample)=max{sample_k,0}, and U(sample)=τ_z(ε_0(sample)). Thus the authors first threshold is canonical coordinate0, not a supplied clock or law. Set F(sample)=untopD_0(U(sample)), viewed as a real number; it is the finite waiting time when U is finite and zero at infinity. For every finite T≥0 define A_T={sample:0<U(sample)≤T}, d_z(s)=λ_r(Φ_s(z))exp(−Λ_z(max{s,0})), ρ_T=(Lebesgue restricted to (0,T]).withDensity(ofReal(d_z)), and J_z(s)=(max{s,0},S_r(Φ_s(z)))∈[0,∞)×(E×E), for all real s. Then U,F,J_z are Borel measurable. For every finite T, A_T is measurable, F_*(P restricted to A_T)=ρ_T, and (J_z∘F)_*(P restricted to A_T)=(J_z)_*ρ_T. Moreover ρ_T is a finite subprobability measure, ρ_T(ℝ)=1−exp(−Λ_z(T))≤1. For every Borel real h on [0,∞)×(E×E), every M≥0 with |h(a)|≤M for all a, h∈L¹((J_z)_*ρ_T), h∘J_z∘F∈L¹(P restricted to A_T), and s↦h(J_z(s))d_z(s)∈L¹(Lebesgue restricted to (0,T]); their exact integral identity is ∫_(A_T)h(J_z(F(sample)))P(dsample)=∫₀ᵀh(s,S_r(Φ_s(z)))λ_r(Φ_s(z))exp(−Λ_z(s))ds, with the right-hand side understood over (0,T]. All assertions hold for every y,r,z,T, with E,V,α,β,η fixed. Infinity is excluded by A_T before the default finite projection is used; zero thresholds and zero waiting times are excluded by its positive guard and have zero P-mass by the derived survival law at0. The finite-event mass is not renormalized; the missing mass is exp(−Λ_z(T)) and includes waits beyond T and infinite waits. No strict hazard increase, positive rate, almost-sure finite wait, uniform cap, supplied measurability, density or integrability assumption is added. T=0, M=0, rank0, zero normals and flat hazards are included. This is an attributed ASTIS measure-theoretic completion of the actual first-event density factor implicit in the authors AppendixA.1(A.1),(A.2),(A.7), using their actual dynamics and iid clocks. It does not prove the successive conditional factors, full finite-event path expansion, path reversal, invariance, process Markovness, all-L² contraction, mixing, implemented error/cost, actual-input composition or complete main results.

\[\int_{A_T}h(J_z(F(\omega)))\,P(d\omega)=\int_{(0,T]}h(s,S_r\Phi_s z)\ell_z(s)e^{-\Lambda_z(s)}\,ds.\]

Lean statement · actual_finite_first_event_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_first_event_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_first_event_law_statement hα hαβ hV hH hη hβη

Exact module and namespace context

Full Lean proposition (definition) · actual_finite_first_event_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_first_event_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 P : Measure (ℕ → ℝ) := Measure.infinitePi (fun _ : ℕ => expMeasure (1 : ℝ))
    let ε : (ℕ → ℝ) → ℕ → ℝ≥0 := fun sample k => Real.toNNReal (sample k)
    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 U : E → E → (E × E) → (ℕ → ℝ) → WithTop ℝ≥0 :=
      fun y xRef z sample => τ y xRef z (ε sample 0)
    let F : E → E → (E × E) → (ℕ → ℝ) → ℝ :=
      fun y xRef z sample => ((U y xRef z sample).untopD 0 : ℝ≥0)
    let A : E → E → (E × E) → ℝ≥0 → Set (ℕ → ℝ) :=
      fun y xRef z T => {sample | (0 : WithTop ℝ≥0) < U y xRef z sample ∧
        U y xRef z sample ≤ (T : WithTop ℝ≥0)}
    let d : E → E → (E × E) → ℝ → ℝ := fun y xRef z s =>
      rate xRef (Φ y xRef s z) * Real.exp (-Λ y xRef z (Real.toNNReal s))
    let ρ : E → E → (E × E) → ℝ≥0 → Measure ℝ := fun y xRef z T =>
      (volume.restrict (Set.Ioc (0 : ℝ) (T : ℝ))).withDensity
        (fun s => ENNReal.ofReal (d y xRef z s))
    let J : E → E → (E × E) → ℝ → (ℝ≥0 × (E × E)) :=
      fun y xRef z s => (Real.toNNReal s, S xRef (Φ y xRef s z))
    ∀ y xRef : E, ∀ z : E × E,
      Measurable (U y xRef z) ∧ Measurable (F y xRef z) ∧
      Measurable (J y xRef z) ∧
      (∀ T : ℝ≥0,
        MeasurableSet (A y xRef z T) ∧
        Measure.map (F y xRef z) (P.restrict (A y xRef z T)) = ρ y xRef z T ∧
        Measure.map (fun sample => J y xRef z (F y xRef z sample))
          (P.restrict (A y xRef z T)) = Measure.map (J y xRef z) (ρ y xRef z T) ∧
        IsFiniteMeasure (ρ y xRef z T) ∧
        (ρ y xRef z T).real Set.univ = 1 - Real.exp (-Λ y xRef z T) ∧
        ρ y xRef z T Set.univ ≤ 1 ∧
        (∀ h : (ℝ≥0 × (E × E)) → ℝ, Measurable h →
          ∀ M : ℝ, 0 ≤ M → (∀ a, |h a| ≤ M) →
            Integrable h (Measure.map (J y xRef z) (ρ y xRef z T)) ∧
            Integrable (fun sample => h (J y xRef z (F y xRef z sample)))
              (P.restrict (A y xRef z T)) ∧
            Integrable (fun s => h (J y xRef z s) * d y xRef z s)
              (volume.restrict (Set.Ioc (0 : ℝ) (T : ℝ))) ∧
            (∫ sample, h (J y xRef z (F y xRef z sample))
                ∂P.restrict (A y xRef z T)) =
              ∫ s, h (J y xRef z s) * d y xRef z s
                ∂volume.restrict (Set.Ioc (0 : ℝ) (T : ℝ))))

-- Internal FTC ingredient of the sealed finite-density anchor; not the public result.

Exact module and namespace context

Proof roadmap

1Key lemma: integrate the first-event density
For any continuous real function l, put L(s)=∫₀ˢl(u)du. The fundamental theorem gives L′=l. The chain rule yields (1−exp(−L))′=l exp(−L). The derivative is continuous, so integrating from0 to t≥0 gives the endpoint difference; L(0)=0 removes the lower endpoint. Nonnegativity is not needed for this identity; the actual nonnegative rate will supply it for the measure.
2Key lemma: turn the integral into finite density mass
Now assume l(s)≥0 for every real s. The exponential is positive and the density continuous, hence integrable on every bounded (0,t]. The integral of ofReal(density) equals ofReal of its real integral. Evaluating withDensity on the whole line and using the preceding identity gives the exact ENNReal mass, including t=0.
3Key lemma: determine the density CDF on a finite window
For a≥0 and t≥0, intersect the window (0,t] with (−∞,a]. This is (0,min(t,a)]. Restriction composition and the previous mass formula give the left-half-line mass. This step uses only measurable interval identities and preserves the finite-window cutoff.
4Key lemma: compute the positive finite clock mass
For a measurable extended nonnegative wait U under a probability measure, assume the already derived survival P(U>t)=exp(−L(t)) and L(0)=0. Then P(U>0)=1. The event 0<U≤t is {U>0} minus its measurable subset {U>t}; finite-measure subtraction gives mass1−exp(−L(t)). This includes infinite waits correctly in the subtracted tail.
5Key lemma: the projected clock has the same CDF
On 0<U≤t the wait is finite. For a≥0, the preimage of (−∞,a] under untopD0 intersected with that event equals {0<U≤min(t,toNNReal(a))}. The proof splits U=∞ and finite U explicitly; the infinite case cannot satisfy either finite cutoff. Pushforward evaluation, restriction and the preceding mass formula give the CDF. The zero default outside the restricted event never creates an atom.
6Retain the actual definitions and consume their compiled producers
Use the literal actual clocks, flow, zero-normal-safe reflection, nonnegative rate, stopped hazard clock, positive finite event, density and mark. Consume the actual hazard/flow/bounce producers with exactly the six original analytic assumptions. UnitExponentialProduct supplies P probability. These are internal proof dependencies, not premises supplied by the theorem caller.
7Derive actual rate continuity, clock law and Borel mark
The compiled jointly continuous harmonic flow and bounce-rate continuity give the continuous free-arc rate l(s)≥0 for all real s. The jointly measurable stopped clock composed with real threshold truncation and coordinate0 gives U; untopD0 and inclusion give F. The compiled Borel reflection composed with the flow gives J. Map composition identifies U under P with the Exp(1) stopped-clock law, hence P(U>t)=exp(−Λ(t)). Joint continuity of Λ and truncation also give continuous nonnegative d.
8Identify the actual finite density and its entire measure
Fix T. A_T is the intersection of two Borel clock events. On (0,T], toNNReal(s) has real value s, so the literal d agrees almost everywhere on this support with l(s)exp(−∫₀ˢl). For a≥0, the two CDF lemmas agree after converting min(T,toNNReal(a)) to min(T,a). For a<0, F is nonnegative and (0,T] has empty intersection with (−∞,a], so both masses vanish. The left pushforward is finite; equality on every left half-line therefore identifies the whole measures.
9Map the same finite law through the actual post-bounce mark
The equality with the restricted-clock pushforward proves ρ finite. Borel J and measurable map composition then give the marked law using the very same J, F and restricted P. Evaluating the density on the whole line gives1−exp(−Λ(T)); Λ(T)≥0 makes this a nonnegative number and positivity of exp makes it at most1. No division by that mass occurs.
10Derive all three integrability statements
For any displayed Borel h with |h|≤M, finiteness of the marked measure gives h∈L¹; the measurable composed clock test is bounded under the finite restriction of P and is also L¹. The same bound gives h∘J∈L¹(ρ). The withDensity integrability equivalence transfers this last fact to (ofReal(d)).toReal·h∘J under restricted Lebesgue measure. Since d≥0 and ofReal(d)<∞, that function is exactly h(J(s))d(s). Thus weighted integrability is derived, including M=0.
11Transfer the bounded-test integral exactly
Rewrite the marked law as the measurable pushforward of restricted P and apply the Bochner integral-map identity. Apply integral-map once more through J to integrate h∘J under ρ. Finally the withDensity integral identity and nonnegative d replace the ENNReal weight by its real value. This yields the stated weighted finite-event integral. Successive conditional factors and the final-survival/path expansion require additional proofs.

Full assumptions and notation

All objects and hypotheses

E is a finite-dimensional real inner-product Borel space, including dimension zero. V:E→ℝ is real-valued and C².
The six original analytic hypotheses are α>0; α≤β; V∈C²; α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for every x,v; η>0; βη≤1. α,β are nonnegative. No higher derivative bound is assumed.
Standing E,V,α,β,η are fixed. Every deterministic y,r,z and finite T≥0 is allowed. P is the canonical countable product of real rate-one exponential measures; U uses ε_0. All fourteen P,ε,c,Φ,S,λ,Λ,τ,U,F,A,d,ρ,J definitions are literal.
F defaults to0 at U=∞; the actual law uses the restriction 0<U≤T first. No conditioning normalization, guaranteed finite wait or strict hazard increase is imposed. Zero normal reflection is the identity; flat hazard, T=0 and rank0 are allowed.
Tests are all Borel real h on nonnegative time×full phase, with every M≥0 satisfying a global absolute bound. The three displayed L¹ facts are conclusions. M=0 is included. No unbounded expectation or oracle-cost transfer follows.

Mathematical proof

1. Key lemma: integrate the first-event density

For any continuous real function l, put L(s)=∫₀ˢl(u)du. The fundamental theorem gives L′=l. The chain rule yields (1−exp(−L))′=l exp(−L). The derivative is continuous, so integrating from0 to t≥0 gives the endpoint difference; L(0)=0 removes the lower endpoint. Nonnegativity is not needed for this identity; the actual nonnegative rate will supply it for the measure.

\[\int_{(0,t]}l(s)e^{-L(s)}ds=1-e^{-L(t)}.\]

Corresponding Lean step

private theorem first_density_setIntegral
    (l : ℝ → ℝ) (hl : Continuous l) (t : ℝ) (ht : 0 ≤ t) :
    (∫ s in Set.Ioc 0 t, l s * Real.exp (-(∫ u in (0 : ℝ)..s, l u))) =
      1 - Real.exp (-(∫ u in (0 : ℝ)..t, l u)) := by
  let L : ℝ → ℝ := fun s => ∫ u in (0 : ℝ)..s, l u
  have hL (s : ℝ) : HasDerivAt L (l s) s :=
    intervalIntegral.integral_hasDerivAt_right (hl.intervalIntegrable _ _)
      hl.stronglyMeasurable.stronglyMeasurableAtFilter hl.continuousAt
  have hcL : Continuous L := continuous_iff_continuousAt.mpr fun s => (hL s).continuousAt
  have hd (s : ℝ) :
      HasDerivAt (fun s => 1 - Real.exp (-L s))
        (l s * Real.exp (-L s)) s := by
    simpa only [Pi.neg_apply, mul_neg, neg_mul, neg_neg, mul_comm]
      using (hL s).neg.exp.const_sub 1
  have hdC : Continuous (fun s => l s * Real.exp (-L s)) :=
    hl.mul hcL.neg.rexp
  have hf := intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le ht
    ((continuous_const.sub hcL.neg.rexp).continuousOn)
    (fun s _ => hd s) (hdC.intervalIntegrable _ _)
  rw [intervalIntegral.integral_of_le ht] at hf
  simpa [L] using hf