Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0

Actual PBPS phase-flow defect bound and zero-time stochastic continuity

Fan Chen, Sinho Chewi, Jianfeng Lu and Matthew S. Zhang, arXiv2609.06905v1 Appendix A.1 Ex22 and p6.1-p6.2. Explicit actual measurable phase-flow defect and positive norm-tail probability are ASTIS bounded elaborations of the source smalltime argument; the full L2 strong-continuity consumer is not claimed.

arXiv2609.06905v1 · Chen-Chewi-Lu-Zhang arXiv2609.06905v1 Appendix A.1 Ex22, A1.SS1.SSS0.Px1.p6.1-p6.2; A1.E1 integrated hazard and actual halfopen interpolation A1.SS1.p2.2. Bounded first-event/smalltime prerequisite only. · faithful paraphrase

Complete source statement (Samplinglib restatement)

Let E be any finite-dimensional real inner-product space, including dimension zero, with its Borel measurable structure. Let V:E→ℝ be C². Let α,β be nonnegative reals and η a real number satisfying α>0, α≤β, α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for every x,v∈E, η>0, and βη≤1. Allow arbitrary parameters y,xRef∈E and initial phase z0=(x0,p0)∈E×E. Set c=y−η∇V(xRef). For z=(x,p), define the actual harmonic flow Φ_t(z)=(c+cos(t)(x−c)+√η sin(t)p, −sin(t)(x−c)/√η+cos(t)p), reflection S(z)=(x,p−[2〈p,g(x)〉/‖g(x)‖²]g(x)), residual g(x)=∇V(x)−∇V(xRef), and rate λ(z)=√η max{0,〈p,g(x)〉}. The reflection uses total real division, hence is the identity when g(x)=0. Define Λ(z,t)=∫_0^t λ(Φ_s(z)) ds for finite t≥0 and τ(z,e)=inf{t≥0:Λ(z,t)≥e}, with inf empty=∞. Let P be the actual countable product of rate-one exponential Borel measures on Ω=ℝ^ℕ; let ε_k(sample)=max{sample_k,0} viewed as a nonnegative real. Define active records (T,z) and an absorbing stopped record carrying no phase. Initialize record0=(0,z0). At index k, a stopped record stays stopped; an active record (T,z) becomes stopped if τ(z,ε_k)=∞ and otherwise becomes (T+τ(z,ε_k), S(Φ_{τ(z,ε_k)}(z))). Its event time T_k is the finite time component if active and ∞ if stopped. There exists a total phase map Z:E×E×(E×E)×[0,∞)×Ω→E×E jointly Borel measurable in all displayed parameters, finite physical time t and sample, while V,α,β,η remain fixed. For every parameter triple, every sample, every finite t and any actual covering index n with T_n≤t<T_(n+1), if record_n=inl(a) with a=(s,z), then Z(y,xRef,z0,t,sample)=Φ_(t−s)(z), where subtraction is the NNReal nonnegative subtraction. If no such actual covering index exists, Z(y,xRef,z0,t,sample)=z0. This uncovered value is an explicitly chosen ASTIS total representative convention, not a source state supplied on exceptional inputs. Furthermore, for each fixed deterministic y,xRef,z0, for P-almost every sample simultaneously: for every finite nonnegative t there exist n and an actual finite live record a=(s,z) with T_n≤t<T_(n+1), record_n=inl(a), s≤t, t−s<τ(z,ε_n) and Z(y,xRef,z0,t,sample)=Φ_(t−s)(z); and Z(y,xRef,z0,0,sample)=z0. A stopped record never provides the source phase. An infinite next wait retains the last live harmonic arc for all later finite t and does not trigger the uncovered fallback. The AE event may depend on the fixed parameter triple; no uniform event over all parameters is asserted. Joint measurability permits later measurable parameter evaluation, but per-parameter AE agreement cannot be substituted at arbitrary parameters correlated with sample without a separate law/independence/conditional-kernel argument. For every fixed deterministic y,xRef,z0 and each finite nonnegative t, the phase-flow defect event D_t={sample:Z(y,xRef,z0,t,sample)≠Φ_t(z0)} is measurable and satisfies P(D_t)≤1−exp(−Λ(z0,t)). For every real δ>0, the event A_(δ,t)={sample:δ≤‖Z(y,xRef,z0,t,sample)−z0‖} is measurable for all finite nonnegative t, and P(A_(δ,t)) tends to zero as t tends to zero in the nonnegative real domain, including the value t=0. The phase norm is the literal product norm on E×E, giving its finite-dimensional phase topology; no quantitative norm-distance rate is asserted. This is a bounded ASTIS elaboration of the actual first-event argument in Appendix A.1 Ex22, not a quotation or a proof of the full L² strong-continuity theorem. The inequality uses inclusion in the first-event event, not equality: a bounce or a later return can leave the phase equal to the no-jump flow. All six analytic source hypotheses remain; no first-event law, path, continuity, invariance, nonexplosion, energy or cap certificate is a premise. No uniform parameter limit/nullset or arbitrary correlated random-input substitution is inferred. Full L²/Markov/restart/semigroup/invariance/hypocoercivity/implementation/error/cost/main/composition results remain open.

  • E is any finite-dimensional real inner-product space with its Borel measurable structure, including dimension zero. V is real-valued and C²; α,β are nonnegative reals.
  • Exactly six analytic source hypotheses: α>0; α≤β; V∈C²; for all x,v, α‖v‖²≤D²V(x)[v,v]≤β‖v‖²; η>0; βη≤1. No third or higher derivative bound.
  • Standing E,V,α,β,η are fixed. y,xRef,z0,t,sample are arguments of one jointly Borel map. P and ε are literal canonical definitions; measurability, positive support, recurrence, cover and nonaccumulation are produced dependencies.
  • The deterministic covered-arc characterization and uncovered fallback hold for every sample. Actual all-time agreement and initialization hold on one AE sample event for each fixed parameter triple. No uniform AE event over uncountably many parameter triples and no arbitrary correlated random-parameter law are inferred.
  • A stopped record has no phase and infinite event time; every covering interval has a live finite record. The last infinite-wait live arc remains covered. The initial-phase fallback is an explicitly labelled ASTIS measurable extension only on the uncovered complement; zero-time exceptional bounces need not have source index0 at t0.
  • The new probability estimates and zero-time stochastic continuity quantify each fixed y,xRef,z0. Every real δ>0 is allowed; t tends to zero within NNReal with its ordinary, nonpunctured neighborhood filter. The positive-threshold tail at zero is zero by retained AE initialization.
  • The phase-flow defect can occur only after the first event. Neither equality of the defect and first-event events nor a linear Ct estimate is claimed.

Actual small-time step 1

\[D_t=\{Z_t\ne\Phi_t(z_0)\}\subseteq\{\tau(z_0,\varepsilon_0)\le t\}.\]

Actual small-time step 2

\[P\{t<\tau(z_0,\varepsilon_0)\}=e^{-\Lambda(z_0,t)},\qquad P(D_t)\le1-e^{-\Lambda(z_0,t)}.\]

Actual small-time step 3

\[\Phi_t(z_0)\to z_0,\quad\Lambda(z_0,t)\to0\quad(t\to0,\ t\ge0).\]

Actual small-time step 4

\[\forall\delta>0,\quad P\{\delta\le\|Z_t-z_0\|\}\longrightarrow0.\]

Read the formalized proofs

Each statement and proof below has its own closed Lean disclosure. Samplinglib parents, Mathlib calls and external mathematical sources are distinguished in each proof.

Samplinglib mathematical lesson

Actual PBPS phase-flow defect bound and zero-time stochastic continuity

AutoSamplingTheory.ExampleCases.ProximalBPS.ActualSmallTimeContinuity.actual_small_time_stochastic_continuity · theorem · Teaching coverage

Read this first

Mathematical statement

Let E be any finite-dimensional real inner-product space, including dimension zero, with its Borel measurable structure. Let V:E→ℝ be C². Let α,β be nonnegative reals and η a real number satisfying α>0, α≤β, α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for every x,v∈E, η>0, and βη≤1. Allow arbitrary parameters y,xRef∈E and initial phase z0=(x0,p0)∈E×E. Set c=y−η∇V(xRef). For z=(x,p), define the actual harmonic flow Φ_t(z)=(c+cos(t)(x−c)+√η sin(t)p, −sin(t)(x−c)/√η+cos(t)p), reflection S(z)=(x,p−[2〈p,g(x)〉/‖g(x)‖²]g(x)), residual g(x)=∇V(x)−∇V(xRef), and rate λ(z)=√η max{0,〈p,g(x)〉}. The reflection uses total real division, hence is the identity when g(x)=0. Define Λ(z,t)=∫_0^t λ(Φ_s(z)) ds for finite t≥0 and τ(z,e)=inf{t≥0:Λ(z,t)≥e}, with inf empty=∞. Let P be the actual countable product of rate-one exponential Borel measures on Ω=ℝ^ℕ; let ε_k(sample)=max{sample_k,0} viewed as a nonnegative real. Define active records (T,z) and an absorbing stopped record carrying no phase. Initialize record0=(0,z0). At index k, a stopped record stays stopped; an active record (T,z) becomes stopped if τ(z,ε_k)=∞ and otherwise becomes (T+τ(z,ε_k), S(Φ_{τ(z,ε_k)}(z))). Its event time T_k is the finite time component if active and ∞ if stopped. There exists a total phase map Z:E×E×(E×E)×[0,∞)×Ω→E×E jointly Borel measurable in all displayed parameters, finite physical time t and sample, while V,α,β,η remain fixed. For every parameter triple, every sample, every finite t and any actual covering index n with T_n≤t<T_(n+1), if record_n=inl(a) with a=(s,z), then Z(y,xRef,z0,t,sample)=Φ_(t−s)(z), where subtraction is the NNReal nonnegative subtraction. If no such actual covering index exists, Z(y,xRef,z0,t,sample)=z0. This uncovered value is an explicitly chosen ASTIS total representative convention, not a source state supplied on exceptional inputs. Furthermore, for each fixed deterministic y,xRef,z0, for P-almost every sample simultaneously: for every finite nonnegative t there exist n and an actual finite live record a=(s,z) with T_n≤t<T_(n+1), record_n=inl(a), s≤t, t−s<τ(z,ε_n) and Z(y,xRef,z0,t,sample)=Φ_(t−s)(z); and Z(y,xRef,z0,0,sample)=z0. A stopped record never provides the source phase. An infinite next wait retains the last live harmonic arc for all later finite t and does not trigger the uncovered fallback. The AE event may depend on the fixed parameter triple; no uniform event over all parameters is asserted. Joint measurability permits later measurable parameter evaluation, but per-parameter AE agreement cannot be substituted at arbitrary parameters correlated with sample without a separate law/independence/conditional-kernel argument. For every fixed deterministic y,xRef,z0 and each finite nonnegative t, the phase-flow defect event D_t={sample:Z(y,xRef,z0,t,sample)≠Φ_t(z0)} is measurable and satisfies P(D_t)≤1−exp(−Λ(z0,t)). For every real δ>0, the event A_(δ,t)={sample:δ≤‖Z(y,xRef,z0,t,sample)−z0‖} is measurable for all finite nonnegative t, and P(A_(δ,t)) tends to zero as t tends to zero in the nonnegative real domain, including the value t=0. The phase norm is the literal product norm on E×E, giving its finite-dimensional phase topology; no quantitative norm-distance rate is asserted. This is a bounded ASTIS elaboration of the actual first-event argument in Appendix A.1 Ex22, not a quotation or a proof of the full L² strong-continuity theorem. The inequality uses inclusion in the first-event event, not equality: a bounce or a later return can leave the phase equal to the no-jump flow. All six analytic source hypotheses remain; no first-event law, path, continuity, invariance, nonexplosion, energy or cap certificate is a premise. No uniform parameter limit/nullset or arbitrary correlated random-input substitution is inferred. Full L²/Markov/restart/semigroup/invariance/hypocoercivity/implementation/error/cost/main/composition results remain open.

\[\forall\delta>0,\quad P\{\delta\le\|Z_t-z_0\|\}\longrightarrow0.\]
Lean statement · actual_small_time_stochastic_continuity

Let E be any finite-dimensional real inner-product space, including dimension zero, with its Borel measurable structure. Let V:E→ℝ be C². Let α,β be nonnegative reals and η a real number satisfying α>0, α≤β, α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for every x,v∈E, η>0, and βη≤1. Allow arbitrary parameters y,xRef∈E and initial phase z0=(x0,p0)∈E×E. Set c=y−η∇V(xRef). For z=(x,p), define the actual harmonic flow Φ_t(z)=(c+cos(t)(x−c)+√η sin(t)p, −sin(t)(x−c)/√η+cos(t)p), reflection S(z)=(x,p−[2〈p,g(x)〉/‖g(x)‖²]g(x)), residual g(x)=∇V(x)−∇V(xRef), and rate λ(z)=√η max{0,〈p,g(x)〉}. The reflection uses total real division, hence is the identity when g(x)=0. Define Λ(z,t)=∫_0^t λ(Φ_s(z)) ds for finite t≥0 and τ(z,e)=inf{t≥0:Λ(z,t)≥e}, with inf empty=∞. Let P be the actual countable product of rate-one exponential Borel measures on Ω=ℝ^ℕ; let ε_k(sample)=max{sample_k,0} viewed as a nonnegative real. Define active records (T,z) and an absorbing stopped record carrying no phase. Initialize record0=(0,z0). At index k, a stopped record stays stopped; an active record (T,z) becomes stopped if τ(z,ε_k)=∞ and otherwise becomes (T+τ(z,ε_k), S(Φ_{τ(z,ε_k)}(z))). Its event time T_k is the finite time component if active and ∞ if stopped. There exists a total phase map Z:E×E×(E×E)×[0,∞)×Ω→E×E jointly Borel measurable in all displayed parameters, finite physical time t and sample, while V,α,β,η remain fixed. For every parameter triple, every sample, every finite t and any actual covering index n with T_n≤t<T_(n+1), if record_n=inl(a) with a=(s,z), then Z(y,xRef,z0,t,sample)=Φ_(t−s)(z), where subtraction is the NNReal nonnegative subtraction. If no such actual covering index exists, Z(y,xRef,z0,t,sample)=z0. This uncovered value is an explicitly chosen ASTIS total representative convention, not a source state supplied on exceptional inputs. Furthermore, for each fixed deterministic y,xRef,z0, for P-almost every sample simultaneously: for every finite nonnegative t there exist n and an actual finite live record a=(s,z) with T_n≤t<T_(n+1), record_n=inl(a), s≤t, t−s<τ(z,ε_n) and Z(y,xRef,z0,t,sample)=Φ_(t−s)(z); and Z(y,xRef,z0,0,sample)=z0. A stopped record never provides the source phase. An infinite next wait retains the last live harmonic arc for all later finite t and does not trigger the uncovered fallback. The AE event may depend on the fixed parameter triple; no uniform event over all parameters is asserted. Joint measurability permits later measurable parameter evaluation, but per-parameter AE agreement cannot be substituted at arbitrary parameters correlated with sample without a separate law/independence/conditional-kernel argument. For every fixed deterministic y,xRef,z0 and each finite nonnegative t, the phase-flow defect event D_t={sample:Z(y,xRef,z0,t,sample)≠Φ_t(z0)} is measurable and satisfies P(D_t)≤1−exp(−Λ(z0,t)). For every real δ>0, the event A_(δ,t)={sample:δ≤‖Z(y,xRef,z0,t,sample)−z0‖} is measurable for all finite nonnegative t, and P(A_(δ,t)) tends to zero as t tends to zero in the nonnegative real domain, including the value t=0. The phase norm is the literal product norm on E×E, giving its finite-dimensional phase topology; no quantitative norm-distance rate is asserted. This is a bounded ASTIS elaboration of the actual first-event argument in Appendix A.1 Ex22, not a quotation or a proof of the full L² strong-continuity theorem. The inequality uses inclusion in the first-event event, not equality: a bounce or a later return can leave the phase equal to the no-jump flow. All six analytic source hypotheses remain; no first-event law, path, continuity, invariance, nonexplosion, energy or cap certificate is a premise. No uniform parameter limit/nullset or arbitrary correlated random-input substitution is inferred. Full L²/Markov/restart/semigroup/invariance/hypocoercivity/implementation/error/cost/main/composition results remain open.

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_small_time_stochastic_continuity
    {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_small_time_stochastic_continuity_statement hα hαβ hV hH hη hβη

Exact module and namespace context

Full Lean proposition (definition) · actual_small_time_stochastic_continuity_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.

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)
private def actual_small_time_stochastic_continuity_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 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 eventTime : E → E → (E × E) → (ℕ → ℝ≥0) → ℕ → WithTop ℝ≥0 :=
      fun y xRef z₀ e n => (record y xRef z₀ e n).elim
        (fun a => (a.1 : WithTop ℝ≥0)) (fun _ => ⊤)
    ∃ 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, ∀ sample : ℕ → ℝ, ∀ t : ℝ≥0,
        ∀ n : ℕ, ∀ a : ℝ≥0 × (E × E),
          eventTime y xRef z₀ (ε sample) n ≤ (t : WithTop ℝ≥0) →
          (t : WithTop ℝ≥0) < eventTime y xRef z₀ (ε sample) (n + 1) →
          record y xRef z₀ (ε sample) n = Sum.inl a →
          Z y xRef z₀ t sample = Φ y xRef ((t - a.1 : ℝ≥0) : ℝ) a.2) ∧
      (∀ y xRef : E, ∀ z₀ : E × E, ∀ sample : ℕ → ℝ, ∀ t : ℝ≥0,
        (¬ ∃ n : ℕ, eventTime y xRef z₀ (ε sample) n ≤ (t : WithTop ℝ≥0) ∧
          (t : WithTop ℝ≥0) < eventTime y xRef z₀ (ε sample) (n + 1)) →
          Z y xRef z₀ t sample = z₀) ∧
      (∀ y xRef : E, ∀ z₀ : E × E, ∀ᵐ sample ∂P,
        (∀ t : ℝ≥0, ∃ n : ℕ, ∃ a : ℝ≥0 × (E × E),
          eventTime y xRef z₀ (ε sample) n ≤ (t : WithTop ℝ≥0) ∧
          (t : WithTop ℝ≥0) < eventTime y xRef z₀ (ε sample) (n + 1) ∧
          record y xRef z₀ (ε sample) n = Sum.inl a ∧ a.1 ≤ t ∧
          ((t - a.1 : ℝ≥0) : WithTop ℝ≥0) < τ y xRef a.2 (ε sample n) ∧
          Z y xRef z₀ t sample = Φ y xRef ((t - a.1 : ℝ≥0) : ℝ) a.2) ∧
        Z y xRef z₀ 0 sample = z₀)
 ∧
      (∀ y xRef : E, ∀ z₀ : E × E,
        (∀ t : ℝ≥0,
          MeasurableSet {sample : ℕ → ℝ |
            Z y xRef z₀ t sample ≠ Φ y xRef (t : ℝ) z₀} ∧
          P.real {sample : ℕ → ℝ |
            Z y xRef z₀ t sample ≠ Φ y xRef (t : ℝ) z₀} ≤
              1 - Real.exp (-Λ y xRef z₀ t)) ∧
        (∀ δ : ℝ, 0 < δ →
          (∀ t : ℝ≥0, MeasurableSet {sample : ℕ → ℝ |
            δ ≤ ‖Z y xRef z₀ t sample - z₀‖}) ∧
          Tendsto (fun t : ℝ≥0 => P.real {sample : ℕ → ℝ |
            δ ≤ ‖Z y xRef z₀ t sample - z₀‖}) (𝓝 0) (𝓝 0)))


set_option maxHeartbeats 1600000 in

Exact module and namespace context

Proof roadmap

  1. 1Retain the literal actual process definitions

    Use the source harmonic flow, reflection, integrated hazard, stopped finite recurrence and canonical exponential product. The initial record is live at0; an infinite next wait retains its last physical arc.

  2. 2Consume the actual measurable phase and hazard producers

    The actual physical phase theorem supplies a jointly Borel Z and all covered/fallback/common-AE properties. The hazard theorem supplies continuity, zero initial hazard and the exact firstwait survival law. The harmonic flow and exponential product are existing verified dependencies, not new premises.

  3. 3Make the actual phase-flow defect measurable

    Fix the deterministic parameters. Pull joint Z measurability back along the sample coordinate and take the complement of equality with the constant no-jump phase. This proves measurability on the entire sample space, including exceptional raw inputs.

  4. 4Transport the firstwait survival law to the actual product input

    The first wait is the measurable actual inverse-hazard map of the clamped zeroth real coordinate. That coordinate has exactly Exp(1) law. Composition of pushforwards therefore gives the same firstwait law as the existing hazard producer, and its strict survival probability is the exponential formula.

  5. 5Identify the actual first live arc

    Directly unfold the initialized first record in the finite and infinite wait cases. Its event time equals the actual first wait. Therefore t below that wait lies in the initial half-open interval, and the deterministic covered-arc characterization gives Z_t=Φ_t(z0), for every raw sample. The at-event endpoint is outside this no-event case.

  6. 6Bound the phase-flow defect by first-event probability

    The previous equality gives D_t contained in the complement of strict firstwait survival. Real probability monotonicity and the measurable-complement identity give the exact displayed upper bound. This is only an inclusion, allowing ineffective bounces and returns.

  7. 7Expose every positive-threshold measurable tail

    Return the measurable defect bounds and fix δ>0. The norm of the measurable phase difference is measurable, so the closed threshold event A_(δ,t) is measurable at each t. No moment/integrability claim is needed for this probability event.

  8. 8Use the continuous no-jump flow and hazard at zero

    The already proved joint flow and hazard continuity restrict to fixed parameters. Φ0=z0 makes the deterministic phase distance tend to0; hence it is eventually below any δ>0. Λ0=0 and exponential continuity make 1−exp(−Λ_t) tend to0. The optional linear energy-cap route is unnecessary.

  9. 9Squeeze the actual phase tail to zero

    When the deterministic no-jump distance is below δ, a phase at distance at least δ must differ from that no-jump phase. Thus the tail probability is eventually between0 and the already proved defect bound. The probability squeeze proves zero-time stochastic continuity in the nonnegative time topology. This closes only the pointwise smalltime ingredient of source Ex22.

Full assumptions and notation

All objects and hypotheses

  • E is any finite-dimensional real inner-product space with its Borel measurable structure, including dimension zero. V is real-valued and C²; α,β are nonnegative reals.
  • Exactly six analytic source hypotheses: α>0; α≤β; V∈C²; for all x,v, α‖v‖²≤D²V(x)[v,v]≤β‖v‖²; η>0; βη≤1. No third or higher derivative bound.
  • Standing E,V,α,β,η are fixed. y,xRef,z0,t,sample are arguments of one jointly Borel map. P and ε are literal canonical definitions; measurability, positive support, recurrence, cover and nonaccumulation are produced dependencies.
  • The deterministic covered-arc characterization and uncovered fallback hold for every sample. Actual all-time agreement and initialization hold on one AE sample event for each fixed parameter triple. No uniform AE event over uncountably many parameter triples and no arbitrary correlated random-parameter law are inferred.
  • A stopped record has no phase and infinite event time; every covering interval has a live finite record. The last infinite-wait live arc remains covered. The initial-phase fallback is an explicitly labelled ASTIS measurable extension only on the uncovered complement; zero-time exceptional bounces need not have source index0 at t0.
  • The new probability estimates and zero-time stochastic continuity quantify each fixed y,xRef,z0. Every real δ>0 is allowed; t tends to zero within NNReal with its ordinary, nonpunctured neighborhood filter. The positive-threshold tail at zero is zero by retained AE initialization.
  • The phase-flow defect can occur only after the first event. Neither equality of the defect and first-event events nor a linear Ct estimate is claimed.

Mathematical proof

1. Retain the literal actual process definitions

Use the source harmonic flow, reflection, integrated hazard, stopped finite recurrence and canonical exponential product. The initial record is live at0; an infinite next wait retains its last physical arc.

\[\operatorname{record}_0=\mathrm{inl}(0,z_0),\qquad P=\bigotimes_{k\ge0}\operatorname{Exp}(1).\]
Corresponding Lean step
  classical
  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 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 eventTime : E → E → (E × E) → (ℕ → ℝ≥0) → ℕ → WithTop ℝ≥0 :=
    fun y xRef z₀ e n => (record y xRef z₀ e n).elim
      (fun a => (a.1 : WithTop ℝ≥0)) (fun _ => ⊤)

Exact contiguous compiled proof region; preceding local definitions and facts stay in scope.

2. Consume the actual measurable phase and hazard producers

The actual physical phase theorem supplies a jointly Borel Z and all covered/fallback/common-AE properties. The hazard theorem supplies continuity, zero initial hazard and the exact firstwait survival law. The harmonic flow and exponential product are existing verified dependencies, not new premises.

\[Z\text{ jointly Borel},\quad\Lambda_0=0,\quad\Phi_0(z_0)=z_0.\]
Corresponding Lean step
  obtain ⟨Z, hZM, hcovered, hfallback, hAE⟩ :=
    ActualPhysicalTimeMeasurability.actual_physical_time_measurable_phase
      hα hαβ hV hH hη hβη
  rcases ActualHazardClock.actual_integrated_hazard_clock_laws
    hα hαβ hV hH hη hβη with
    ⟨hΛC, _, _, hΛbasic, _, _, hτM, hW, _, _⟩
  have hflow := ActualHarmonicFlow.actual_harmonic_flow_laws hα hαβ hV hH hη hβη
  have hΦC := hflow.1
  have hΦ0 := hflow.2.2.1
  have hinput :=
    AutoSamplingTheory.TechnicalLemmas.Probability.UnitExponentialProduct.unit_exponential_product_laws
  letI : IsProbabilityMeasure P := hinput.1
  refine ⟨Z, hZM, hcovered, hfallback, hAE, ?_⟩
  intro y xRef z₀

Exact contiguous compiled proof region; preceding local definitions and facts stay in scope.

3. Make the actual phase-flow defect measurable

Fix the deterministic parameters. Pull joint Z measurability back along the sample coordinate and take the complement of equality with the constant no-jump phase. This proves measurability on the entire sample space, including exceptional raw inputs.

\[D_t=\{Z_t\ne\Phi_t(z_0)\}\text{ is measurable}.\]
Corresponding Lean step
  have hZtM (t : ℝ≥0) : Measurable (Z y xRef z₀ t) := by
    have hargs : Measurable (fun sample : ℕ → ℝ => (((y, xRef), z₀), t, sample)) :=
      measurable_const.prodMk (measurable_const.prodMk measurable_id)
    have hc := hZM.comp hargs
    exact hc
  have hdefectM (t : ℝ≥0) :
      MeasurableSet {sample : ℕ → ℝ | Z y xRef z₀ t sample ≠ Φ y xRef (t : ℝ) z₀} :=
    (measurableSet_eq_fun (hZtM t) measurable_const).compl

Exact contiguous compiled proof region; preceding local definitions and facts stay in scope.

4. Transport the firstwait survival law to the actual product input

The first wait is the measurable actual inverse-hazard map of the clamped zeroth real coordinate. That coordinate has exactly Exp(1) law. Composition of pushforwards therefore gives the same firstwait law as the existing hazard producer, and its strict survival probability is the exponential formula.

\[P\{t<\tau(z_0,\varepsilon_0)\}=e^{-\Lambda(z_0,t)}.\]
Corresponding Lean step
  let w : (ℕ → ℝ) → WithTop ℝ≥0 := fun sample => τ y xRef z₀ (ε sample 0)
  let g : ℝ → WithTop ℝ≥0 := fun e => τ y xRef z₀ (Real.toNNReal e)
  have hgM : Measurable g := by
    have hargs : Measurable (fun e : ℝ => ((y, xRef), z₀, Real.toNNReal e)) :=
      measurable_const.prodMk (measurable_const.prodMk measurable_real_toNNReal)
    have hc := hτM.comp hargs
    exact hc
  have hwM : Measurable w := hgM.comp (measurable_pi_apply 0)
  have hwlaw : P.map w = (expMeasure (1 : ℝ)).map g := by
    calc
      P.map w = (P.map (fun sample : ℕ → ℝ => sample 0)).map g :=
        (Measure.map_map hgM (measurable_pi_apply 0)).symm
      _ = (expMeasure (1 : ℝ)).map g := by rw [(hinput.2.1 0).2.2]
  have hsurvival (t : ℝ≥0) :
      P.real {sample : ℕ → ℝ | (t : WithTop ℝ≥0) < w sample} =
        Real.exp (-Λ y xRef z₀ t) := by
    calc
      P.real {sample : ℕ → ℝ | (t : WithTop ℝ≥0) < w sample} =
          (P.map w).real (Set.Ioi (t : WithTop ℝ≥0)) :=
        (map_measureReal_apply hwM measurableSet_Ioi).symm
      _ = Real.exp (-Λ y xRef z₀ t) := by
        rw [hwlaw]
        exact (hW y xRef z₀).2 t

Exact contiguous compiled proof region; preceding local definitions and facts stay in scope.

5. Identify the actual first live arc

Directly unfold the initialized first record in the finite and infinite wait cases. Its event time equals the actual first wait. Therefore t below that wait lies in the initial half-open interval, and the deterministic covered-arc characterization gives Z_t=Φ_t(z0), for every raw sample. The at-event endpoint is outside this no-event case.

\[D_t=\{Z_t\ne\Phi_t(z_0)\}\subseteq\{\tau(z_0,\varepsilon_0)\le t\}.\]
Corresponding Lean step
  have hfirst (sample : ℕ → ℝ) :
      eventTime y xRef z₀ (ε sample) 1 = w sample := by
    change (if τ y xRef z₀ (ε sample 0) = ⊤ then Sum.inr () else
      Sum.inl (0 + (τ y xRef z₀ (ε sample 0)).untopD 0,
        S xRef (Φ y xRef (((τ y xRef z₀ (ε sample 0)).untopD 0 : ℝ≥0) : ℝ) z₀))).elim
          (fun a => (a.1 : WithTop ℝ≥0)) (fun _ => ⊤) = τ y xRef z₀ (ε sample 0)
    cases hc : τ y xRef z₀ (ε sample 0) using WithTop.recTopCoe with
    | top => rfl
    | coe s => simp only [WithTop.coe_ne_top, if_false, WithTop.untopD_coe,
        zero_add, Sum.elim_inl]
  have hnoevent (t : ℝ≥0) (sample : ℕ → ℝ)
      (ht : (t : WithTop ℝ≥0) < w sample) :
      Z y xRef z₀ t sample = Φ y xRef (t : ℝ) z₀ := by
    have he := hcovered y xRef z₀ sample t 0 (0, z₀)
      (show eventTime y xRef z₀ (ε sample) 0 ≤ (t : WithTop ℝ≥0) from
        show (0 : WithTop ℝ≥0) ≤ (t : WithTop ℝ≥0) from bot_le)
      (by change (t : WithTop ℝ≥0) < eventTime y xRef z₀ (ε sample) 1
          rw [hfirst sample]; exact ht) rfl
    simpa only [tsub_zero] using he

Exact contiguous compiled proof region; preceding local definitions and facts stay in scope.

6. Bound the phase-flow defect by first-event probability

The previous equality gives D_t contained in the complement of strict firstwait survival. Real probability monotonicity and the measurable-complement identity give the exact displayed upper bound. This is only an inclusion, allowing ineffective bounces and returns.

\[P\{t<\tau(z_0,\varepsilon_0)\}=e^{-\Lambda(z_0,t)},\qquad P(D_t)\le1-e^{-\Lambda(z_0,t)}.\]
Corresponding Lean step
  have hbound (t : ℝ≥0) :
      P.real {sample : ℕ → ℝ | Z y xRef z₀ t sample ≠ Φ y xRef (t : ℝ) z₀} ≤
        1 - Real.exp (-Λ y xRef z₀ t) := by
    have hsub : {sample : ℕ → ℝ | Z y xRef z₀ t sample ≠ Φ y xRef (t : ℝ) z₀} ⊆
        {sample : ℕ → ℝ | (t : WithTop ℝ≥0) < w sample}ᶜ := by
      intro sample hs ht
      exact hs (hnoevent t sample ht)
    calc
      P.real {sample : ℕ → ℝ | Z y xRef z₀ t sample ≠ Φ y xRef (t : ℝ) z₀} ≤
          P.real {sample : ℕ → ℝ | (t : WithTop ℝ≥0) < w sample}ᶜ := measureReal_mono hsub
      _ = 1 - Real.exp (-Λ y xRef z₀ t) := by
        have hsM : MeasurableSet {sample : ℕ → ℝ | (t : WithTop ℝ≥0) < w sample} :=
          measurableSet_Ioi.preimage hwM
        rw [measureReal_compl hsM, probReal_univ, hsurvival]

Exact contiguous compiled proof region; preceding local definitions and facts stay in scope.

7. Expose every positive-threshold measurable tail

Return the measurable defect bounds and fix δ>0. The norm of the measurable phase difference is measurable, so the closed threshold event A_(δ,t) is measurable at each t. No moment/integrability claim is needed for this probability event.

\[A_{\delta,t}=\{\delta\le\|Z_t-z_0\|\}\text{ is measurable}.\]
Corresponding Lean step
  refine ⟨fun t => ⟨hdefectM t, hbound t⟩, ?_⟩
  intro δ hδ
  have htailM (t : ℝ≥0) :
      MeasurableSet {sample : ℕ → ℝ | δ ≤ ‖Z y xRef z₀ t sample - z₀‖} :=
    measurableSet_le measurable_const (((hZtM t).sub measurable_const).norm)
  refine ⟨htailM, ?_⟩

Exact contiguous compiled proof region; preceding local definitions and facts stay in scope.

8. Use the continuous no-jump flow and hazard at zero

The already proved joint flow and hazard continuity restrict to fixed parameters. Φ0=z0 makes the deterministic phase distance tend to0; hence it is eventually below any δ>0. Λ0=0 and exponential continuity make 1−exp(−Λ_t) tend to0. The optional linear energy-cap route is unnecessary.

\[\Phi_t(z_0)\to z_0,\quad\Lambda(z_0,t)\to0\quad(t\to0,\ t\ge0).\]
Corresponding Lean step
  have hφ : Continuous (fun t : ℝ≥0 => Φ y xRef (t : ℝ) z₀) := by
    have hargs : Continuous (fun t : ℝ≥0 => ((y, xRef), (t : ℝ), z₀)) :=
      continuous_const.prodMk (continuous_subtype_val.prodMk continuous_const)
    have hc := hΦC.comp hargs
    exact hc
  have hLambdaCont : Continuous (Λ y xRef z₀) := by
    have hargs : Continuous (fun t : ℝ≥0 => (((y, xRef), z₀), t)) :=
      continuous_const.prodMk continuous_id
    have hc := hΛC.comp hargs
    exact hc
  have hnorm : Tendsto (fun t : ℝ≥0 => ‖Φ y xRef (t : ℝ) z₀ - z₀‖) (𝓝 0) (𝓝 0) := by
    have hzero : Φ y xRef 0 z₀ = z₀ := hΦ0 y xRef z₀
    have hc : Continuous (fun t : ℝ≥0 => ‖Φ y xRef (t : ℝ) z₀ - z₀‖) :=
      (hφ.sub continuous_const).norm
    simpa only [NNReal.coe_zero, hzero, sub_self, norm_zero] using
      hc.tendsto (0 : ℝ≥0)
  have hsmall : ∀ᶠ t : ℝ≥0 in 𝓝 0, ‖Φ y xRef (t : ℝ) z₀ - z₀‖ < δ :=
    (tendsto_order.1 hnorm).2 δ hδ
  have hbzero : Tendsto (fun t : ℝ≥0 => 1 - Real.exp (-Λ y xRef z₀ t))
      (𝓝 0) (𝓝 0) := by
    have hzero : Λ y xRef z₀ 0 = 0 := (hΛbasic y xRef z₀).1
    have he : Tendsto (fun t : ℝ≥0 => Real.exp (-Λ y xRef z₀ t)) (𝓝 0)
        (𝓝 (Real.exp (-Λ y xRef z₀ 0))) :=
      (Real.continuous_exp.tendsto _).comp ((hLambdaCont.tendsto 0).neg)
    simpa only [hzero, neg_zero, Real.exp_zero, sub_self] using
      (show Tendsto (fun t : ℝ≥0 => 1 - Real.exp (-Λ y xRef z₀ t)) (𝓝 0)
        (𝓝 (1 - Real.exp (-Λ y xRef z₀ 0))) from tendsto_const_nhds.sub he)

Exact contiguous compiled proof region; preceding local definitions and facts stay in scope.

9. Squeeze the actual phase tail to zero

When the deterministic no-jump distance is below δ, a phase at distance at least δ must differ from that no-jump phase. Thus the tail probability is eventually between0 and the already proved defect bound. The probability squeeze proves zero-time stochastic continuity in the nonnegative time topology. This closes only the pointwise smalltime ingredient of source Ex22.

\[\forall\delta>0,\quad P\{\delta\le\|Z_t-z_0\|\}\longrightarrow0.\]
Corresponding Lean step
  apply tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds hbzero
  · exact Filter.Eventually.of_forall fun _ => measureReal_nonneg
  · filter_upwards [hsmall] with t ht
    apply (measureReal_mono (show
      {sample : ℕ → ℝ | δ ≤ ‖Z y xRef z₀ t sample - z₀‖} ⊆
      {sample : ℕ → ℝ | Z y xRef z₀ t sample ≠ Φ y xRef (t : ℝ) z₀} from ?_)).trans (hbound t)
    intro sample hs he
    change δ ≤ ‖Z y xRef z₀ t sample - z₀‖ at hs
    rw [he] at hs
    exact (not_le.mpr ht) hs

Exact contiguous compiled proof region; preceding local definitions and facts stay in scope.

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · actual_small_time_stochastic_continuity

Retain the literal actual process definitions; Consume the actual measurable phase and hazard producers; Make the actual phase-flow defect measurable; Transport the firstwait survival law to the actual product input; Identify the actual first live arc; Bound the phase-flow defect by first-event probability; Expose every positive-threshold measurable tail; Use the continuous no-jump flow and hazard at zero; Squeeze the actual phase tail to zero

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_small_time_stochastic_continuity
    {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_small_time_stochastic_continuity_statement hα hαβ hV hH hη hβη := by
  classical
  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 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 eventTime : E → E → (E × E) → (ℕ → ℝ≥0) → ℕ → WithTop ℝ≥0 :=
    fun y xRef z₀ e n => (record y xRef z₀ e n).elim
      (fun a => (a.1 : WithTop ℝ≥0)) (fun _ => ⊤)
  obtain ⟨Z, hZM, hcovered, hfallback, hAE⟩ :=
    ActualPhysicalTimeMeasurability.actual_physical_time_measurable_phase
      hα hαβ hV hH hη hβη
  rcases ActualHazardClock.actual_integrated_hazard_clock_laws
    hα hαβ hV hH hη hβη with
    ⟨hΛC, _, _, hΛbasic, _, _, hτM, hW, _, _⟩
  have hflow := ActualHarmonicFlow.actual_harmonic_flow_laws hα hαβ hV hH hη hβη
  have hΦC := hflow.1
  have hΦ0 := hflow.2.2.1
  have hinput :=
    AutoSamplingTheory.TechnicalLemmas.Probability.UnitExponentialProduct.unit_exponential_product_laws
  letI : IsProbabilityMeasure P := hinput.1
  refine ⟨Z, hZM, hcovered, hfallback, hAE, ?_⟩
  intro y xRef z₀
  have hZtM (t : ℝ≥0) : Measurable (Z y xRef z₀ t) := by
    have hargs : Measurable (fun sample : ℕ → ℝ => (((y, xRef), z₀), t, sample)) :=
      measurable_const.prodMk (measurable_const.prodMk measurable_id)
    have hc := hZM.comp hargs
    exact hc
  have hdefectM (t : ℝ≥0) :
      MeasurableSet {sample : ℕ → ℝ | Z y xRef z₀ t sample ≠ Φ y xRef (t : ℝ) z₀} :=
    (measurableSet_eq_fun (hZtM t) measurable_const).compl
  let w : (ℕ → ℝ) → WithTop ℝ≥0 := fun sample => τ y xRef z₀ (ε sample 0)
  let g : ℝ → WithTop ℝ≥0 := fun e => τ y xRef z₀ (Real.toNNReal e)
  have hgM : Measurable g := by
    have hargs : Measurable (fun e : ℝ => ((y, xRef), z₀, Real.toNNReal e)) :=
      measurable_const.prodMk (measurable_const.prodMk measurable_real_toNNReal)
    have hc := hτM.comp hargs
    exact hc
  have hwM : Measurable w := hgM.comp (measurable_pi_apply 0)
  have hwlaw : P.map w = (expMeasure (1 : ℝ)).map g := by
    calc
      P.map w = (P.map (fun sample : ℕ → ℝ => sample 0)).map g :=
        (Measure.map_map hgM (measurable_pi_apply 0)).symm
      _ = (expMeasure (1 : ℝ)).map g := by rw [(hinput.2.1 0).2.2]
  have hsurvival (t : ℝ≥0) :
      P.real {sample : ℕ → ℝ | (t : WithTop ℝ≥0) < w sample} =
        Real.exp (-Λ y xRef z₀ t) := by
    calc
      P.real {sample : ℕ → ℝ | (t : WithTop ℝ≥0) < w sample} =
          (P.map w).real (Set.Ioi (t : WithTop ℝ≥0)) :=
        (map_measureReal_apply hwM measurableSet_Ioi).symm
      _ = Real.exp (-Λ y xRef z₀ t) := by
        rw [hwlaw]
        exact (hW y xRef z₀).2 t
  have hfirst (sample : ℕ → ℝ) :
      eventTime y xRef z₀ (ε sample) 1 = w sample := by
    change (if τ y xRef z₀ (ε sample 0) = ⊤ then Sum.inr () else
      Sum.inl (0 + (τ y xRef z₀ (ε sample 0)).untopD 0,
        S xRef (Φ y xRef (((τ y xRef z₀ (ε sample 0)).untopD 0 : ℝ≥0) : ℝ) z₀))).elim
          (fun a => (a.1 : WithTop ℝ≥0)) (fun _ => ⊤) = τ y xRef z₀ (ε sample 0)
    cases hc : τ y xRef z₀ (ε sample 0) using WithTop.recTopCoe with
    | top => rfl
    | coe s => simp only [WithTop.coe_ne_top, if_false, WithTop.untopD_coe,
        zero_add, Sum.elim_inl]
  have hnoevent (t : ℝ≥0) (sample : ℕ → ℝ)
      (ht : (t : WithTop ℝ≥0) < w sample) :
      Z y xRef z₀ t sample = Φ y xRef (t : ℝ) z₀ := by
    have he := hcovered y xRef z₀ sample t 0 (0, z₀)
      (show eventTime y xRef z₀ (ε sample) 0 ≤ (t : WithTop ℝ≥0) from
        show (0 : WithTop ℝ≥0) ≤ (t : WithTop ℝ≥0) from bot_le)
      (by change (t : WithTop ℝ≥0) < eventTime y xRef z₀ (ε sample) 1
          rw [hfirst sample]; exact ht) rfl
    simpa only [tsub_zero] using he
  have hbound (t : ℝ≥0) :
      P.real {sample : ℕ → ℝ | Z y xRef z₀ t sample ≠ Φ y xRef (t : ℝ) z₀} ≤
        1 - Real.exp (-Λ y xRef z₀ t) := by
    have hsub : {sample : ℕ → ℝ | Z y xRef z₀ t sample ≠ Φ y xRef (t : ℝ) z₀} ⊆
        {sample : ℕ → ℝ | (t : WithTop ℝ≥0) < w sample}ᶜ := by
      intro sample hs ht
      exact hs (hnoevent t sample ht)
    calc
      P.real {sample : ℕ → ℝ | Z y xRef z₀ t sample ≠ Φ y xRef (t : ℝ) z₀} ≤
          P.real {sample : ℕ → ℝ | (t : WithTop ℝ≥0) < w sample}ᶜ := measureReal_mono hsub
      _ = 1 - Real.exp (-Λ y xRef z₀ t) := by
        have hsM : MeasurableSet {sample : ℕ → ℝ | (t : WithTop ℝ≥0) < w sample} :=
          measurableSet_Ioi.preimage hwM
        rw [measureReal_compl hsM, probReal_univ, hsurvival]
  refine ⟨fun t => ⟨hdefectM t, hbound t⟩, ?_⟩
  intro δ hδ
  have htailM (t : ℝ≥0) :
      MeasurableSet {sample : ℕ → ℝ | δ ≤ ‖Z y xRef z₀ t sample - z₀‖} :=
    measurableSet_le measurable_const (((hZtM t).sub measurable_const).norm)
  refine ⟨htailM, ?_⟩
  have hφ : Continuous (fun t : ℝ≥0 => Φ y xRef (t : ℝ) z₀) := by
    have hargs : Continuous (fun t : ℝ≥0 => ((y, xRef), (t : ℝ), z₀)) :=
      continuous_const.prodMk (continuous_subtype_val.prodMk continuous_const)
    have hc := hΦC.comp hargs
    exact hc
  have hLambdaCont : Continuous (Λ y xRef z₀) := by
    have hargs : Continuous (fun t : ℝ≥0 => (((y, xRef), z₀), t)) :=
      continuous_const.prodMk continuous_id
    have hc := hΛC.comp hargs
    exact hc
  have hnorm : Tendsto (fun t : ℝ≥0 => ‖Φ y xRef (t : ℝ) z₀ - z₀‖) (𝓝 0) (𝓝 0) := by
    have hzero : Φ y xRef 0 z₀ = z₀ := hΦ0 y xRef z₀
    have hc : Continuous (fun t : ℝ≥0 => ‖Φ y xRef (t : ℝ) z₀ - z₀‖) :=
      (hφ.sub continuous_const).norm
    simpa only [NNReal.coe_zero, hzero, sub_self, norm_zero] using
      hc.tendsto (0 : ℝ≥0)
  have hsmall : ∀ᶠ t : ℝ≥0 in 𝓝 0, ‖Φ y xRef (t : ℝ) z₀ - z₀‖ < δ :=
    (tendsto_order.1 hnorm).2 δ hδ
  have hbzero : Tendsto (fun t : ℝ≥0 => 1 - Real.exp (-Λ y xRef z₀ t))
      (𝓝 0) (𝓝 0) := by
    have hzero : Λ y xRef z₀ 0 = 0 := (hΛbasic y xRef z₀).1
    have he : Tendsto (fun t : ℝ≥0 => Real.exp (-Λ y xRef z₀ t)) (𝓝 0)
        (𝓝 (Real.exp (-Λ y xRef z₀ 0))) :=
      (Real.continuous_exp.tendsto _).comp ((hLambdaCont.tendsto 0).neg)
    simpa only [hzero, neg_zero, Real.exp_zero, sub_self] using
      (show Tendsto (fun t : ℝ≥0 => 1 - Real.exp (-Λ y xRef z₀ t)) (𝓝 0)
        (𝓝 (1 - Real.exp (-Λ y xRef z₀ 0))) from tendsto_const_nhds.sub he)
  apply tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds hbzero
  · exact Filter.Eventually.of_forall fun _ => measureReal_nonneg
  · filter_upwards [hsmall] with t ht
    apply (measureReal_mono (show
      {sample : ℕ → ℝ | δ ≤ ‖Z y xRef z₀ t sample - z₀‖} ⊆
      {sample : ℕ → ℝ | Z y xRef z₀ t sample ≠ Φ y xRef (t : ℝ) z₀} from ?_)).trans (hbound t)
    intro sample hs he
    change δ ≤ ‖Z y xRef z₀ t sample - z₀‖ at hs
    rw [he] at hs
    exact (not_le.mpr ht) hs

end
end AutoSamplingTheory.ExampleCases.ProximalBPS.ActualSmallTimeContinuity

Exact module and namespace context

Source assumptions versus formal assumptions

SourceActual LeanDifference kindWhy it matters
Six original analytic hypotheses and actual physical process.Same six source standing binders and literal actual recurrence; retain all jointly measurable realization clauses.sameSealed exact header and independent source/topology audit.
Ex22 first-event probability tends to0; deterministic flow continuous at0.Measurable actual phase-flow defect <= first-event probability, then every positive norm-tail tends to0 in NNReal.source-implicitExplicit actual-input integration; nonpunctured zero includes AE initialization, no quantitative phase norm rate.
Full L2 strong continuity uses invariance/Jensen, DCT, density and contractivity.Only fixed-initial-phase stochastic continuity; all full process/L2 consumers remain open.unresolvedBounded prerequisite, no source full-theorem credit.

Actual phase-flow defect bound and zero-time stochastic continuity for fixed V/alpha/beta/eta,y,xRef,z0 under actual exponential product, retaining all physical-phase realization clauses. No uniform parameter nullset/limit or arbitrary correlated substitution. Full L2 strong continuity/Markov/restart/semigroup/invariance/hypocoercivity/implementation/main/cost/composition and actual reader visual/main/PURIFIED/live remain OPEN.

Encoder–denoiser: accepted · equivalent-after-elaboration

Detected semantic differences

  • objects: Exp product coordinate0 realizes source E1; measurable clamp has actual Exp input law. Source initial record is live, not stopped; G82-05 title ACK removes wording ambiguity without topology change. — Native independent review D82-01 in E:/Samplinglib/runs/20261007-companion-priority/pbps-actual-small-time-continuity82/fresh-source82/source-review.result82.json, exact current module and nine BODY regions bound by run 90f6416500e968bdc387c0c42143f4c67472e4af3a5cddfd9df08454ec021948.
  • domains: Intrinsic finite-dimensional Borel carrier/rank0 and literal product norm preserve phase topology. NNReal finite time is distinct from extended wait. — Native independent review D82-02 in E:/Samplinglib/runs/20261007-companion-priority/pbps-actual-small-time-continuity82/fresh-source82/source-review.result82.json, exact current module and nine BODY regions bound by run 90f6416500e968bdc387c0c42143f4c67472e4af3a5cddfd9df08454ec021948.
  • quantifiers: Nonpunctured NNReal nhds0 extends source t-downarrow0 legitimately. Positive-delta tail at0 has probability0, derivable from hbound0 plus Phi0=id and retained AE initialization. No uniformparameter or arbitrary correlated input claim. — Native independent review D82-03 in E:/Samplinglib/runs/20261007-companion-priority/pbps-actual-small-time-continuity82/fresh-source82/source-review.result82.json, exact current module and nine BODY regions bound by run 90f6416500e968bdc387c0c42143f4c67472e4af3a5cddfd9df08454ec021948.
  • assumptions: Six exact source binders retained; actual probability/measurability/firstwait/phase facts are produced dependencies, not public source premises. — Native independent review D82-04 in E:/Samplinglib/runs/20261007-companion-priority/pbps-actual-small-time-continuity82/fresh-source82/source-review.result82.json, exact current module and nine BODY regions bound by run 90f6416500e968bdc387c0c42143f4c67472e4af3a5cddfd9df08454ec021948.
  • conclusion: Source firstevent survival gives actual phase-flow defect upper bound via firstarc agreement. This is a strict bounded prerequisite, not a fullL2 theorem or event-equality claim. — Native independent review D82-05 in E:/Samplinglib/runs/20261007-companion-priority/pbps-actual-small-time-continuity82/fresh-source82/source-review.result82.json, exact current module and nine BODY regions bound by run 90f6416500e968bdc387c0c42143f4c67472e4af3a5cddfd9df08454ec021948.
  • scopes: E82-14 optional cap Ct OR route is unused; E82-13 Lambda continuity suffices. Bounded-test expectation/G82-11, fullL2/G82-12 and global/path/restart/G82-13 remain OPEN. — Native independent review D82-06 in E:/Samplinglib/runs/20261007-companion-priority/pbps-actual-small-time-continuity82/fresh-source82/source-review.result82.json, exact current module and nine BODY regions bound by run 90f6416500e968bdc387c0c42143f4c67472e4af3a5cddfd9df08454ec021948.
  • scopes: Zero thresholds exceptional under actual Exp input; firstwaittop keeps last live arc, stopped dummy no phase, uncovered z0 distinct from source failed-limit zero. Deterministic noevent agreement holds every raw sequence on its first live interval. — Native independent review D82-07 in E:/Samplinglib/runs/20261007-companion-priority/pbps-actual-small-time-continuity82/fresh-source82/source-review.result82.json, exact current module and nine BODY regions bound by run 90f6416500e968bdc387c0c42143f4c67472e4af3a5cddfd9df08454ec021948.
  • constant_dependencies: All eta/Exp1/clockindex/hazard signs retained; no quantitative norm-distance constant, Ct or time rescaling added. — Native independent review D82-08 in E:/Samplinglib/runs/20261007-companion-priority/pbps-actual-small-time-continuity82/fresh-source82/source-review.result82.json, exact current module and nine BODY regions bound by run 90f6416500e968bdc387c0c42143f4c67472e4af3a5cddfd9df08454ec021948.
  • scopes: Independent step4 formula overlay adopted exactly: survival only at step4, firstarc agreement step5, defect bound step6. Nine formula/BODY regions now agree in dependency order; no mathematical change. — Native independent review D82-09 in E:/Samplinglib/runs/20261007-companion-priority/pbps-actual-small-time-continuity82/fresh-source82/source-review.result82.json, exact current module and nine BODY regions bound by run 90f6416500e968bdc387c0c42143f4c67472e4af3a5cddfd9df08454ec021948.
  • scopes: One module docstring line corrected; exact reverse replacement regenerates predecessor RAW a5d0303..., proving all statement/BODY bytes and line count unchanged. Final module RAW f2bbb2a4... bound. — Native independent review D82-10 in E:/Samplinglib/runs/20261007-companion-priority/pbps-actual-small-time-continuity82/fresh-source82/source-review.result82.json, exact current module and nine BODY regions bound by run 90f6416500e968bdc387c0c42143f4c67472e4af3a5cddfd9df08454ec021948.

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

Scope and omitted-condition boundaries
  • Actual phase-flow defect bound and zero-time stochastic continuity for fixed V/alpha/beta/eta,y,xRef,z0 under actual exponential product, retaining all physical-phase realization clauses. No uniform parameter nullset/limit or arbitrary correlated substitution. Full L2 strong continuity/Markov/restart/semigroup/invariance/hypocoercivity/implementation/main/cost/composition and actual reader visual/main/PURIFIED/live remain OPEN.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

  • Measure.map_map
  • map_measureReal_apply
  • measureReal_compl
  • measureReal_mono
  • probReal_univ
  • measurableSet_eq_fun
  • measurableSet_le
  • Continuous.comp
  • Continuous.tendsto
  • Real.continuous_exp
  • tendsto_order
  • tendsto_of_tendsto_of_tendsto_of_le_of_le'

Mathematical sources

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.

Which proof obligations and prerequisites are covered?

  • Formalized proof edge; source adapter/review separate Actual phase-flow defect bound and fixed-parameter zero-time stochastic continuity
  • TODO — not closed by these contributions Full L2/Markov/semigroup/invariance and main/implementation/cost/composition