Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0
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

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.