ActualBoundedTestContinuity: mathematical reading route

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.

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βη

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

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.