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

Actual PBPS bounded-test integrability and expectation continuity

Fan Chen, Sinho Chewi, Jianfeng Lu and Matthew S. Zhang, arXiv2609.06905v1 AppendixA.1 Ex22 p6.1-p6.2. Bounded continuous real tests and the explicit2M defect estimate are ASTIS elaborations of source compactly supported continuous tests; no full L2 or main-theorem credit.

arXiv2609.06905v1 · Chen-Chewi-Lu-Zhang arXiv2609.06905v1 AppendixA.1 Ex22, A1.SS1.SSS0.Px1.p6.1-p6.2. Explicit ASTIS bounded-continuous extension of source compactly supported continuous test class; pointwise clock-expectation 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. In addition, for this same single phase map Z and each fixed deterministic y,xRef,z0, take any continuous real-valued function f on E×E and any real M≥0 such that |f(z)|≤M for every phase z. For every finite t≥0, the actual sample function f(Z(y,xRef,z0,t,sample)) is Borel measurable and integrable under the same canonical probability measure P. Its expectation obeys |∫ f(Z_t) dP−f(Φ_t(z0))|≤2M[1−exp(−Λ(z0,t))]. Moreover ∫ f(Z_t) dP tends to f(z0) as nonnegative t tends to0 in the ordinary nonpunctured neighborhood filter, including the value at0. The bound is valid for every admissible nonnegative M, including M=0; no uniform limit over parameters or tests is asserted. This bounded-continuous real test class C_b and explicit quantitative2M bound are attributed ASTIS elaborations of the compactly supported continuous test argument in Chen-Chewi-Lu-Zhang AppendixA.1 Ex22 p6.1-p6.2, not quoted source theorems. The proof integrates a bounded discrepancy over the actual phase-flow defect event; it neither identifies that event with the first-event event nor invokes almost-sure convergence from convergence in probability. No unbounded-test expectation or expected oracle cost follows. All six original analytic source conditions and eleven literal actual definitions remain, and no process, probability, integral or limit certificate is a premise. Full outer-state L² strong continuity, invariant law/Jensen/contraction/density, process Markov/restart/semigroup, hypocoercivity, implementation/error/cost/main and actual-input composition remain separate OPEN obligations.

  • 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.
  • The same existential Z precedes every test f and every bound M. Tests are real-valued and continuous on the literal product phase; every M≥0 bounding |f| globally is quantified. This is an explicit ASTIS C_b elaboration of source C_c, not a new dynamics condition.
  • The integral is over the actual iid exponential clock law P for fixed deterministic y,xRef,z0. Boundedness gives integrability; no arbitrary law, probabilistic convergence, integral bound or expectation limit is a public premise.
  • The expectation limit is at ordinary nonpunctured NNReal0 for each fixed test/parameter. No almost-sure sample-path limit, Feller initial-state continuity, outer-state L2 result or unbounded expected-cost transfer is claimed.

Actual bounded-test step 1

\[f(Z_t)\in L^1(P),\qquad f\circ Z_t\text{ measurable}.\]

Actual bounded-test step 2

\[|f(Z_t)-f(\Phi_tz_0)|\le2M\mathbf1_{D_t},\quad D_t=\{Z_t\ne\Phi_tz_0\}.\]

Actual bounded-test step 3

\[|\mathbb E_P f(Z_t)-f(\Phi_tz_0)|\le2M P(D_t)\le2M(1-e^{-\Lambda_t}).\]

Actual bounded-test step 4

\[\mathbb E_P f(Z_t)\longrightarrow f(z_0)\qquad(t\to0,\ t\ge0).\]

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 bounded-test integrability and expectation continuity

AutoSamplingTheory.ExampleCases.ProximalBPS.ActualBoundedTestContinuity.actual_bounded_test_expectation_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. In addition, for this same single phase map Z and each fixed deterministic y,xRef,z0, take any continuous real-valued function f on E×E and any real M≥0 such that |f(z)|≤M for every phase z. For every finite t≥0, the actual sample function f(Z(y,xRef,z0,t,sample)) is Borel measurable and integrable under the same canonical probability measure P. Its expectation obeys |∫ f(Z_t) dP−f(Φ_t(z0))|≤2M[1−exp(−Λ(z0,t))]. Moreover ∫ f(Z_t) dP tends to f(z0) as nonnegative t tends to0 in the ordinary nonpunctured neighborhood filter, including the value at0. The bound is valid for every admissible nonnegative M, including M=0; no uniform limit over parameters or tests is asserted. This bounded-continuous real test class C_b and explicit quantitative2M bound are attributed ASTIS elaborations of the compactly supported continuous test argument in Chen-Chewi-Lu-Zhang AppendixA.1 Ex22 p6.1-p6.2, not quoted source theorems. The proof integrates a bounded discrepancy over the actual phase-flow defect event; it neither identifies that event with the first-event event nor invokes almost-sure convergence from convergence in probability. No unbounded-test expectation or expected oracle cost follows. All six original analytic source conditions and eleven literal actual definitions remain, and no process, probability, integral or limit certificate is a premise. Full outer-state L² strong continuity, invariant law/Jensen/contraction/density, process Markov/restart/semigroup, hypocoercivity, implementation/error/cost/main and actual-input composition remain separate OPEN obligations.

\[\mathbb E_P f(Z_t)\longrightarrow f(z_0)\qquad(t\to0,\ t\ge0).\]
Lean statement · actual_bounded_test_expectation_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. In addition, for this same single phase map Z and each fixed deterministic y,xRef,z0, take any continuous real-valued function f on E×E and any real M≥0 such that |f(z)|≤M for every phase z. For every finite t≥0, the actual sample function f(Z(y,xRef,z0,t,sample)) is Borel measurable and integrable under the same canonical probability measure P. Its expectation obeys |∫ f(Z_t) dP−f(Φ_t(z0))|≤2M[1−exp(−Λ(z0,t))]. Moreover ∫ f(Z_t) dP tends to f(z0) as nonnegative t tends to0 in the ordinary nonpunctured neighborhood filter, including the value at0. The bound is valid for every admissible nonnegative M, including M=0; no uniform limit over parameters or tests is asserted. This bounded-continuous real test class C_b and explicit quantitative2M bound are attributed ASTIS elaborations of the compactly supported continuous test argument in Chen-Chewi-Lu-Zhang AppendixA.1 Ex22 p6.1-p6.2, not quoted source theorems. The proof integrates a bounded discrepancy over the actual phase-flow defect event; it neither identifies that event with the first-event event nor invokes almost-sure convergence from convergence in probability. No unbounded-test expectation or expected oracle cost follows. All six original analytic source conditions and eleven literal actual definitions remain, and no process, probability, integral or limit certificate is a premise. Full outer-state L² strong continuity, invariant law/Jensen/contraction/density, process Markov/restart/semigroup, hypocoercivity, implementation/error/cost/main and actual-input composition remain separate OPEN obligations.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)
theorem actual_bounded_test_expectation_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_bounded_test_expectation_continuity_statement hα hαβ hV hH hη hβη

Exact module and namespace context

Full Lean proposition (definition) · actual_bounded_test_expectation_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_bounded_test_expectation_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)))

 ∧
      (∀ y xRef : E, ∀ z₀ : E × E,
        ∀ f : (E × E) → ℝ, Continuous f →
        ∀ M : ℝ, 0 ≤ M → (∀ z : E × E, |f z| ≤ M) →
          (∀ t : ℝ≥0,
            Measurable (fun sample : ℕ → ℝ => f (Z y xRef z₀ t sample)) ∧
            Integrable (fun sample : ℕ → ℝ => f (Z y xRef z₀ t sample)) P ∧
            |(∫ sample, f (Z y xRef z₀ t sample) ∂P) -
                f (Φ y xRef (t : ℝ) z₀)| ≤
              2 * M * (1 - Real.exp (-Λ y xRef z₀ t))) ∧
          Tendsto (fun t : ℝ≥0 => ∫ sample, f (Z y xRef z₀ t sample) ∂P)
            (𝓝 0) (𝓝 (f z₀)))


set_option maxHeartbeats 1600000 in

Exact module and namespace context

Proof roadmap

  1. 1Keep the same actual probability input and deterministic flow

    Use the literal rate-one exponential product P, harmonic flow about c=y−η∇V(xRef), residual rate and integrated hazard. The full sealed statement also retains the actual reflection, stopped recurrence and physical-phase conventions.

  2. 2Consume the actual phase and its defect bound

    The already verified actual smalltime theorem supplies one jointly Borel Z and every covered/fallback/common-AE/init/defect/tail property. Retain them all. Existing hazard, harmonic-flow and exponential-product producers supply continuity, initial values and probability normalization internally; none is a new public premise.

  3. 3Prove bounded test measurability and integrability

    Restrict joint Z to each deterministic tuple and time. Continuous f is Borel, so f(Z_t) is measurable. Its absolute value is bounded by the same constant M on the entire sample space. Because P is a probability, that constant is integrable, yielding actual L1 integrability for every finite time.

  4. 4Localize the test discrepancy to the measurable defect

    On D_t use the triangle inequality and the two global test bounds to get2M. Outside D_t the actual phase equals the free-flow phase, so their test values agree exactly. The constant indicator is integrable on P. This argument holds for each raw sample and allows ineffective jumps or later returns.

  5. 5Integrate and apply the actual first-event probability bound

    Bound the norm of the integral by the integral of2M times the defect indicator. Both test integrals exist, so subtraction commutes with integration; probability normalization integrates the constant free-flow value. The indicator integral is2M P(D_t). Multiplication by2M≥0 preserves the already proved actual defect bound.

  6. 6Use deterministic test-flow and hazard continuity

    Return all finite-time measurable/integrable estimates. Restrict the actual joint flow and hazard continuity to the fixed tuple. Since Φ0z0=z0 and f is continuous, f(Φ_tz0) tends f(z0). The integrated hazard is continuous at0.

  7. 7Make the quantitative error vanish

    Continuity of the exponential and Λ0=0 give q_t=1−exp(−Λ_t)→0. Multiplication by the fixed finite constant2M preserves this zero limit. No source energy cap, moment bound or almost-sure convergence is needed.

  8. 8Squeeze the expectation difference and recover the initial value

    The absolute expectation difference is between0 and the vanishing quantitative bound. Hence the signed difference tends0. Add the independently proved deterministic test-flow limit; subtraction cancels to give the actual clock expectation limit at0. This closes only the pointwise expectation ingredient before the source outer-state L2 argument.

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.
  • The same existential Z precedes every test f and every bound M. Tests are real-valued and continuous on the literal product phase; every M≥0 bounding |f| globally is quantified. This is an explicit ASTIS C_b elaboration of source C_c, not a new dynamics condition.
  • The integral is over the actual iid exponential clock law P for fixed deterministic y,xRef,z0. Boundedness gives integrability; no arbitrary law, probabilistic convergence, integral bound or expectation limit is a public premise.
  • The expectation limit is at ordinary nonpunctured NNReal0 for each fixed test/parameter. No almost-sure sample-path limit, Feller initial-state continuity, outer-state L2 result or unbounded expected-cost transfer is claimed.

Mathematical proof

1. Keep the same actual probability input and deterministic flow

Use the literal rate-one exponential product P, harmonic flow about c=y−η∇V(xRef), residual rate and integrated hazard. The full sealed statement also retains the actual reflection, stopped recurrence and physical-phase conventions.

\[P=\bigotimes_{k\ge0}\operatorname{Exp}(1),\quad\Lambda_t=\int_0^t\lambda(\Phi_sz_0)\,ds.\]
Corresponding Lean step
  classical
  let P : Measure (ℕ → ℝ) := Measure.infinitePi (fun _ : ℕ => expMeasure (1 : ℝ))
  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 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)

Exact contiguous compiled proof region; prior local definitions and facts remain in scope.

2. Consume the actual phase and its defect bound

The already verified actual smalltime theorem supplies one jointly Borel Z and every covered/fallback/common-AE/init/defect/tail property. Retain them all. Existing hazard, harmonic-flow and exponential-product producers supply continuity, initial values and probability normalization internally; none is a new public premise.

\[P(D_t)\le1-e^{-\Lambda_t},\quad\Lambda_0=0,\quad\Phi_0z_0=z_0.\]
Corresponding Lean step
  obtain ⟨Z, hZM, hcovered, hfallback, hAE, hshort⟩ :=
    ActualSmallTimeContinuity.actual_small_time_stochastic_continuity
      hα hαβ hV hH hη hβη
  have hclock := ActualHazardClock.actual_integrated_hazard_clock_laws
    hα hαβ hV hH hη hβη
  have hΛC := hclock.1
  have hΛbasic := hclock.2.2.2.1
  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
  let : IsProbabilityMeasure P := hinput.1
  refine ⟨Z, hZM, hcovered, hfallback, hAE, hshort, ?_⟩
  intro y xRef z₀ f hf M hM hbound

Exact contiguous compiled proof region; prior local definitions and facts remain in scope.

3. Prove bounded test measurability and integrability

Restrict joint Z to each deterministic tuple and time. Continuous f is Borel, so f(Z_t) is measurable. Its absolute value is bounded by the same constant M on the entire sample space. Because P is a probability, that constant is integrable, yielding actual L1 integrability for every finite time.

\[f(Z_t)\in L^1(P),\qquad f\circ Z_t\text{ 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)
    exact hZM.comp hargs
  have hfM (t : ℝ≥0) : Measurable (fun sample : ℕ → ℝ => f (Z y xRef z₀ t sample)) :=
    hf.measurable.comp (hZtM t)
  have hfi (t : ℝ≥0) : Integrable (fun sample : ℕ → ℝ => f (Z y xRef z₀ t sample)) P := by
    apply Integrable.of_bound (hfM t).aestronglyMeasurable M
    exact Filter.Eventually.of_forall fun sample => by
      simpa only [Real.norm_eq_abs] using hbound (Z y xRef z₀ t sample)

Exact contiguous compiled proof region; prior local definitions and facts remain in scope.

4. Localize the test discrepancy to the measurable defect

On D_t use the triangle inequality and the two global test bounds to get2M. Outside D_t the actual phase equals the free-flow phase, so their test values agree exactly. The constant indicator is integrable on P. This argument holds for each raw sample and allows ineffective jumps or later returns.

\[|f(Z_t)-f(\Phi_tz_0)|\le2M\mathbf1_{D_t},\quad D_t=\{Z_t\ne\Phi_tz_0\}.\]
Corresponding Lean step
  have hestimate (t : ℝ≥0) :
      |(∫ sample, f (Z y xRef z₀ t sample) ∂P) - f (Φ y xRef (t : ℝ) z₀)| ≤
        2 * M * (1 - Real.exp (-Λ y xRef z₀ t)) := by
    let D : Set (ℕ → ℝ) := {sample | Z y xRef z₀ t sample ≠ Φ y xRef (t : ℝ) z₀}
    have hDM : MeasurableSet D := ((hshort y xRef z₀).1 t).1
    have hbi : Integrable (D.indicator (fun _ : ℕ → ℝ => 2 * M)) P :=
      (integrable_const (2 * M)).indicator hDM
    have hpoint (sample : ℕ → ℝ) :
        ‖f (Z y xRef z₀ t sample) - f (Φ y xRef (t : ℝ) z₀)‖ ≤
          D.indicator (fun _ : ℕ → ℝ => 2 * M) sample := by
      by_cases hd : sample ∈ D
      · rw [Set.indicator_of_mem hd]
        calc
          ‖f (Z y xRef z₀ t sample) - f (Φ y xRef (t : ℝ) z₀)‖ ≤
              ‖f (Z y xRef z₀ t sample)‖ + ‖f (Φ y xRef (t : ℝ) z₀)‖ := norm_sub_le _ _
          _ ≤ M + M := add_le_add
            (by simpa only [Real.norm_eq_abs] using hbound (Z y xRef z₀ t sample))
            (by simpa only [Real.norm_eq_abs] using hbound (Φ y xRef (t : ℝ) z₀))
          _ = 2 * M := by ring
      · have he : Z y xRef z₀ t sample = Φ y xRef (t : ℝ) z₀ := not_ne_iff.mp hd
        simp only [Set.indicator_of_notMem hd, he, sub_self, norm_zero, le_refl]

Exact contiguous compiled proof region; prior local definitions and facts remain in scope.

5. Integrate and apply the actual first-event probability bound

Bound the norm of the integral by the integral of2M times the defect indicator. Both test integrals exist, so subtraction commutes with integration; probability normalization integrates the constant free-flow value. The indicator integral is2M P(D_t). Multiplication by2M≥0 preserves the already proved actual defect bound.

\[|\mathbb E_P f(Z_t)-f(\Phi_tz_0)|\le2M P(D_t)\le2M(1-e^{-\Lambda_t}).\]
Corresponding Lean step
    have hnorm := norm_integral_le_of_norm_le hbi (Filter.Eventually.of_forall hpoint)
    have hdiff : (∫ sample, f (Z y xRef z₀ t sample) - f (Φ y xRef (t : ℝ) z₀) ∂P) =
        (∫ sample, f (Z y xRef z₀ t sample) ∂P) - f (Φ y xRef (t : ℝ) z₀) := by
      rw [integral_sub (hfi t) (integrable_const _)]
      simp only [integral_const, probReal_univ, one_smul]
    calc
      |(∫ sample, f (Z y xRef z₀ t sample) ∂P) - f (Φ y xRef (t : ℝ) z₀)| =
          ‖∫ sample, f (Z y xRef z₀ t sample) - f (Φ y xRef (t : ℝ) z₀) ∂P‖ := by
        rw [hdiff, Real.norm_eq_abs]
      _ ≤ ∫ sample, D.indicator (fun _ : ℕ → ℝ => 2 * M) sample ∂P := hnorm
      _ = 2 * M * P.real D := by
        rw [integral_indicator_const _ hDM, smul_eq_mul, mul_comm]
      _ ≤ 2 * M * (1 - Real.exp (-Λ y xRef z₀ t)) :=
        mul_le_mul_of_nonneg_left (((hshort y xRef z₀).1 t).2) (by positivity)

Exact contiguous compiled proof region; prior local definitions and facts remain in scope.

6. Use deterministic test-flow and hazard continuity

Return all finite-time measurable/integrable estimates. Restrict the actual joint flow and hazard continuity to the fixed tuple. Since Φ0z0=z0 and f is continuous, f(Φ_tz0) tends f(z0). The integrated hazard is continuous at0.

\[f(\Phi_tz_0)\to f(z_0),\qquad\Lambda_t\to\Lambda_0=0.\]
Corresponding Lean step
  refine ⟨fun t => ⟨hfM t, hfi t, hestimate t⟩, ?_⟩
  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)
    exact hΦC.comp hargs
  have hφlimit : Tendsto (fun t : ℝ≥0 => f (Φ y xRef (t : ℝ) z₀))
      (𝓝 0) (𝓝 (f z₀)) := by
    have hzero : Φ y xRef 0 z₀ = z₀ := hΦ0 y xRef z₀
    have hc : Continuous (fun t : ℝ≥0 => f (Φ y xRef (t : ℝ) z₀)) := hf.comp hφ
    simpa only [NNReal.coe_zero, hzero] using hc.tendsto (0 : ℝ≥0)
  have hLambdaCont : Continuous (Λ y xRef z₀) := by
    have hargs : Continuous (fun t : ℝ≥0 => (((y, xRef), z₀), t)) :=
      continuous_const.prodMk continuous_id
    exact hΛC.comp hargs

Exact contiguous compiled proof region; prior local definitions and facts remain in scope.

7. Make the quantitative error vanish

Continuity of the exponential and Λ0=0 give q_t=1−exp(−Λ_t)→0. Multiplication by the fixed finite constant2M preserves this zero limit. No source energy cap, moment bound or almost-sure convergence is needed.

\[2M(1-e^{-\Lambda_t})\longrightarrow0.\]
Corresponding Lean step
  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)
  have hscaled : Tendsto (fun t : ℝ≥0 => 2 * M * (1 - Real.exp (-Λ y xRef z₀ t)))
      (𝓝 0) (𝓝 0) := by
    simpa only [mul_zero] using
      (show Tendsto (fun _ : ℝ≥0 => 2 * M) (𝓝 0) (𝓝 (2 * M)) from
        tendsto_const_nhds).mul hbzero

Exact contiguous compiled proof region; prior local definitions and facts remain in scope.

8. Squeeze the expectation difference and recover the initial value

The absolute expectation difference is between0 and the vanishing quantitative bound. Hence the signed difference tends0. Add the independently proved deterministic test-flow limit; subtraction cancels to give the actual clock expectation limit at0. This closes only the pointwise expectation ingredient before the source outer-state L2 argument.

\[\mathbb E_P f(Z_t)\longrightarrow f(z_0)\qquad(t\to0,\ t\ge0).\]
Corresponding Lean step
  have habs : Tendsto (fun t : ℝ≥0 =>
      |(∫ sample, f (Z y xRef z₀ t sample) ∂P) - f (Φ y xRef (t : ℝ) z₀)|)
      (𝓝 0) (𝓝 0) :=
    tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds hscaled
      (fun _ => abs_nonneg _) hestimate
  have hdiffzero : Tendsto (fun t : ℝ≥0 =>
      (∫ sample, f (Z y xRef z₀ t sample) ∂P) - f (Φ y xRef (t : ℝ) z₀))
      (𝓝 0) (𝓝 0) := by
    apply tendsto_zero_iff_norm_tendsto_zero.mpr
    simpa only [Real.norm_eq_abs] using habs
  simpa only [sub_add_cancel, zero_add] using hdiffzero.add hφlimit

Exact contiguous compiled proof region; prior local definitions and facts remain 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_bounded_test_expectation_continuity

Keep the same actual probability input and deterministic flow; Consume the actual phase and its defect bound; Prove bounded test measurability and integrability; Localize the test discrepancy to the measurable defect; Integrate and apply the actual first-event probability bound; Use deterministic test-flow and hazard continuity; Make the quantitative error vanish; Squeeze the expectation difference and recover the initial 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)
theorem actual_bounded_test_expectation_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_bounded_test_expectation_continuity_statement hα hαβ hV hH hη hβη := by
  classical
  let P : Measure (ℕ → ℝ) := Measure.infinitePi (fun _ : ℕ => expMeasure (1 : ℝ))
  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 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)
  obtain ⟨Z, hZM, hcovered, hfallback, hAE, hshort⟩ :=
    ActualSmallTimeContinuity.actual_small_time_stochastic_continuity
      hα hαβ hV hH hη hβη
  have hclock := ActualHazardClock.actual_integrated_hazard_clock_laws
    hα hαβ hV hH hη hβη
  have hΛC := hclock.1
  have hΛbasic := hclock.2.2.2.1
  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
  let : IsProbabilityMeasure P := hinput.1
  refine ⟨Z, hZM, hcovered, hfallback, hAE, hshort, ?_⟩
  intro y xRef z₀ f hf M hM hbound
  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)
    exact hZM.comp hargs
  have hfM (t : ℝ≥0) : Measurable (fun sample : ℕ → ℝ => f (Z y xRef z₀ t sample)) :=
    hf.measurable.comp (hZtM t)
  have hfi (t : ℝ≥0) : Integrable (fun sample : ℕ → ℝ => f (Z y xRef z₀ t sample)) P := by
    apply Integrable.of_bound (hfM t).aestronglyMeasurable M
    exact Filter.Eventually.of_forall fun sample => by
      simpa only [Real.norm_eq_abs] using hbound (Z y xRef z₀ t sample)
  have hestimate (t : ℝ≥0) :
      |(∫ sample, f (Z y xRef z₀ t sample) ∂P) - f (Φ y xRef (t : ℝ) z₀)| ≤
        2 * M * (1 - Real.exp (-Λ y xRef z₀ t)) := by
    let D : Set (ℕ → ℝ) := {sample | Z y xRef z₀ t sample ≠ Φ y xRef (t : ℝ) z₀}
    have hDM : MeasurableSet D := ((hshort y xRef z₀).1 t).1
    have hbi : Integrable (D.indicator (fun _ : ℕ → ℝ => 2 * M)) P :=
      (integrable_const (2 * M)).indicator hDM
    have hpoint (sample : ℕ → ℝ) :
        ‖f (Z y xRef z₀ t sample) - f (Φ y xRef (t : ℝ) z₀)‖ ≤
          D.indicator (fun _ : ℕ → ℝ => 2 * M) sample := by
      by_cases hd : sample ∈ D
      · rw [Set.indicator_of_mem hd]
        calc
          ‖f (Z y xRef z₀ t sample) - f (Φ y xRef (t : ℝ) z₀)‖ ≤
              ‖f (Z y xRef z₀ t sample)‖ + ‖f (Φ y xRef (t : ℝ) z₀)‖ := norm_sub_le _ _
          _ ≤ M + M := add_le_add
            (by simpa only [Real.norm_eq_abs] using hbound (Z y xRef z₀ t sample))
            (by simpa only [Real.norm_eq_abs] using hbound (Φ y xRef (t : ℝ) z₀))
          _ = 2 * M := by ring
      · have he : Z y xRef z₀ t sample = Φ y xRef (t : ℝ) z₀ := not_ne_iff.mp hd
        simp only [Set.indicator_of_notMem hd, he, sub_self, norm_zero, le_refl]
    have hnorm := norm_integral_le_of_norm_le hbi (Filter.Eventually.of_forall hpoint)
    have hdiff : (∫ sample, f (Z y xRef z₀ t sample) - f (Φ y xRef (t : ℝ) z₀) ∂P) =
        (∫ sample, f (Z y xRef z₀ t sample) ∂P) - f (Φ y xRef (t : ℝ) z₀) := by
      rw [integral_sub (hfi t) (integrable_const _)]
      simp only [integral_const, probReal_univ, one_smul]
    calc
      |(∫ sample, f (Z y xRef z₀ t sample) ∂P) - f (Φ y xRef (t : ℝ) z₀)| =
          ‖∫ sample, f (Z y xRef z₀ t sample) - f (Φ y xRef (t : ℝ) z₀) ∂P‖ := by
        rw [hdiff, Real.norm_eq_abs]
      _ ≤ ∫ sample, D.indicator (fun _ : ℕ → ℝ => 2 * M) sample ∂P := hnorm
      _ = 2 * M * P.real D := by
        rw [integral_indicator_const _ hDM, smul_eq_mul, mul_comm]
      _ ≤ 2 * M * (1 - Real.exp (-Λ y xRef z₀ t)) :=
        mul_le_mul_of_nonneg_left (((hshort y xRef z₀).1 t).2) (by positivity)
  refine ⟨fun t => ⟨hfM t, hfi t, hestimate t⟩, ?_⟩
  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)
    exact hΦC.comp hargs
  have hφlimit : Tendsto (fun t : ℝ≥0 => f (Φ y xRef (t : ℝ) z₀))
      (𝓝 0) (𝓝 (f z₀)) := by
    have hzero : Φ y xRef 0 z₀ = z₀ := hΦ0 y xRef z₀
    have hc : Continuous (fun t : ℝ≥0 => f (Φ y xRef (t : ℝ) z₀)) := hf.comp hφ
    simpa only [NNReal.coe_zero, hzero] using hc.tendsto (0 : ℝ≥0)
  have hLambdaCont : Continuous (Λ y xRef z₀) := by
    have hargs : Continuous (fun t : ℝ≥0 => (((y, xRef), z₀), t)) :=
      continuous_const.prodMk continuous_id
    exact hΛC.comp hargs
  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)
  have hscaled : Tendsto (fun t : ℝ≥0 => 2 * M * (1 - Real.exp (-Λ y xRef z₀ t)))
      (𝓝 0) (𝓝 0) := by
    simpa only [mul_zero] using
      (show Tendsto (fun _ : ℝ≥0 => 2 * M) (𝓝 0) (𝓝 (2 * M)) from
        tendsto_const_nhds).mul hbzero
  have habs : Tendsto (fun t : ℝ≥0 =>
      |(∫ sample, f (Z y xRef z₀ t sample) ∂P) - f (Φ y xRef (t : ℝ) z₀)|)
      (𝓝 0) (𝓝 0) :=
    tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds hscaled
      (fun _ => abs_nonneg _) hestimate
  have hdiffzero : Tendsto (fun t : ℝ≥0 =>
      (∫ sample, f (Z y xRef z₀ t sample) ∂P) - f (Φ y xRef (t : ℝ) z₀))
      (𝓝 0) (𝓝 0) := by
    apply tendsto_zero_iff_norm_tendsto_zero.mpr
    simpa only [Real.norm_eq_abs] using habs
  simpa only [sub_add_cancel, zero_add] using hdiffzero.add hφlimit

end
end AutoSamplingTheory.ExampleCases.ProximalBPS.ActualBoundedTestContinuity

Exact module and namespace context

Source assumptions versus formal assumptions

SourceActual LeanDifference kindWhy it matters
Original six analytic hypotheses, literal actual phase and source compactly supported continuous test class.Same six dynamics binders and all actual82 clauses; quantify continuous real f and every admissible global nonnegative bound M.source-implicitExplicit mathematically valid ASTIS C_b extension of C_c, independently reviewed before StatementSeal.
First-event argument and continuous free flow supply pointwise expectation convergence.Derive actual test measurability/integrability, explicit2M defect expectation estimate and nonpunctured zero-time expectation limit.source-implicitActual82 and existing integral floors consumed internally; no probability or limit premise.
Full L2 conclusion uses invariant law/Jensen, outer DCT, density and contractivity.Only fixed-state clock expectation prerequisite; all full operators/global boundaries remain open.unresolvedNo AS convergence inferred from probability convergence; no unbounded-test or cost assertion.

Retains actual82 full joint measurability/covered/fallback/fixed-parameter commonAE/init/defect/smalltime clauses and literal eleven definitions. Quantifies all continuous real f and all global nonnegative bounds M. No unbounded-test expectation, arbitrary correlated input substitution, uniform parameter event/limit, AS path convergence, outer-state L2, invariance/Jensen/density, process Markov/restart/semigroup/hypocoercivity/implementation/error/cost/composition/main or actual reader visual/main/PURIFIED/live credit.

Encoder–denoiser: accepted · equivalent-after-elaboration

Detected semantic differences

  • objects: Index0 real exponential coordinate realizes source E1, clamp is AE actual positive clock. Literal stopped records and source physical phase retained. — Native independent review D83-01 in E:/Samplinglib/runs/20261007-companion-priority/pbps-actual-bounded-test-continuity83/independent-source83/source-review.result83.json, exact current module and eight BODY regions bound by run 73d075e64435455e0863bffafaf6534de4feb1ab4abfd5c7f5d0dab0d537ccdd.
  • domains: Intrinsic Borel/rank0/product phase and NNReal finite time preserve source phase topology; source C_c extended explicitly to bounded continuous real C_b tests. — Native independent review D83-02 in E:/Samplinglib/runs/20261007-companion-priority/pbps-actual-bounded-test-continuity83/independent-source83/source-review.result83.json, exact current module and eight BODY regions bound by run 73d075e64435455e0863bffafaf6534de4feb1ab4abfd5c7f5d0dab0d537ccdd.
  • quantifiers: One Z before all tests/bounds; every admissible M>=0 globalbound quantified. Fixedparams AEallfinite/init retained; no uniformparams nullset or arbitrary correlated random-parameter substitution. — Native independent review D83-03 in E:/Samplinglib/runs/20261007-companion-priority/pbps-actual-bounded-test-continuity83/independent-source83/source-review.result83.json, exact current module and eight BODY regions bound by run 73d075e64435455e0863bffafaf6534de4feb1ab4abfd5c7f5d0dab0d537ccdd.
  • assumptions: Continuity and boundedness of f define the tested class, not added potential/trajectory hypotheses. All six source dynamics binders exact. — Native independent review D83-04 in E:/Samplinglib/runs/20261007-companion-priority/pbps-actual-bounded-test-continuity83/independent-source83/source-review.result83.json, exact current module and eight BODY regions bound by run 73d075e64435455e0863bffafaf6534de4feb1ab4abfd5c7f5d0dab0d537ccdd.
  • conclusion: Pointwise expectation convergence is genuine implicit ingredient between Ex22 rare-first-event/flow control and outer-state DCT, now derived from actual inputs. — Native independent review D83-05 in E:/Samplinglib/runs/20261007-companion-priority/pbps-actual-bounded-test-continuity83/independent-source83/source-review.result83.json, exact current module and eight BODY regions bound by run 73d075e64435455e0863bffafaf6534de4feb1ab4abfd5c7f5d0dab0d537ccdd.
  • constant_dependencies: Explicit2M estimate follows bounded discrepancy on phase-flow defect. Defect is only contained in first-event event; no equality, Ct cap or moment rate asserted. — Native independent review D83-06 in E:/Samplinglib/runs/20261007-companion-priority/pbps-actual-bounded-test-continuity83/independent-source83/source-review.result83.json, exact current module and eight BODY regions bound by run 73d075e64435455e0863bffafaf6534de4feb1ab4abfd5c7f5d0dab0d537ccdd.
  • scopes: Uncovered fallbackz0 is labelled ASTIS representative vs source failed-limitzero; fixedparams null exceptions ignored by integrals. Last infinite-wait arc remains live and covered; stopped dummy never phase. — Native independent review D83-07 in E:/Samplinglib/runs/20261007-companion-priority/pbps-actual-bounded-test-continuity83/independent-source83/source-review.result83.json, exact current module and eight BODY regions bound by run 73d075e64435455e0863bffafaf6534de4feb1ab4abfd5c7f5d0dab0d537ccdd.
  • scopes: Preferred complete integrated-defect route used. E29/E30 AND inside optional epsilon/delta route, whole branch OR with preferred route. No probability->AS DCT shortcut. — Native independent review D83-08 in E:/Samplinglib/runs/20261007-companion-priority/pbps-actual-bounded-test-continuity83/independent-source83/source-review.result83.json, exact current module and eight BODY regions bound by run 73d075e64435455e0863bffafaf6534de4feb1ab4abfd5c7f5d0dab0d537ccdd.
  • scopes: Fullouter L2/invariance/Jensen/density/operator laws/Markov/restart/main/cost/composition remainOPEN; E28 dependency_edge=false association is not theorem implication. — Native independent review D83-09 in E:/Samplinglib/runs/20261007-companion-priority/pbps-actual-bounded-test-continuity83/independent-source83/source-review.result83.json, exact current module and eight BODY regions bound by run 73d075e64435455e0863bffafaf6534de4feb1ab4abfd5c7f5d0dab0d537ccdd.
  • quantifiers: Ordinary NNReal nhds0 includes0; actual AEinit and Phi0=id make actual expectation0=f(z0), quantitativeq0=0 compatible even raw zero thresholds exceptional. — Native independent review D83-10 in E:/Samplinglib/runs/20261007-companion-priority/pbps-actual-bounded-test-continuity83/independent-source83/source-review.result83.json, exact current module and eight BODY regions bound by run 73d075e64435455e0863bffafaf6534de4feb1ab4abfd5c7f5d0dab0d537ccdd.

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
  • Retains actual82 full joint measurability/covered/fallback/fixed-parameter commonAE/init/defect/smalltime clauses and literal eleven definitions. Quantifies all continuous real f and all global nonnegative bounds M. No unbounded-test expectation, arbitrary correlated input substitution, uniform parameter event/limit, AS path convergence, outer-state L2, invariance/Jensen/density, process Markov/restart/semigroup/hypocoercivity/implementation/error/cost/composition/main or actual reader visual/main/PURIFIED/live credit.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

  • Integrable.of_bound
  • Integrable.indicator
  • norm_sub_le
  • norm_integral_le_of_norm_le
  • integral_sub
  • integral_const
  • probReal_univ
  • integral_indicator_const
  • mul_le_mul_of_nonneg_left
  • Continuous.comp
  • Continuous.tendsto
  • Real.continuous_exp
  • tendsto_of_tendsto_of_tendsto_of_le_of_le
  • tendsto_zero_iff_norm_tendsto_zero

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 bounded-test L1/2M estimate and zero-time expectation limit
  • TODO — not closed by these contributions Full outerL2/Markov/semigroup/invariance/main/implementation/cost/composition