Actual PBPS bounded-test outer square-integral continuity
AutoSamplingTheory.ExampleCases.ProximalBPS.ActualOuterBoundedL2Continuity.actual_outer_bounded_l2_continuity · theorem · Teaching coverage
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. In addition, define the exact conditional position probability q_y=volume.tilted(x↦−V(x)−‖x−y‖²/(2η)) and the initial phase probability ν_y=q_y⊗N(0,I_E). Both probability normalizations are conclusions derived from the same six analytic hypotheses. For each fixed y,xRef, each continuous real f:E×E→ℝ and every M≥0 with |f(z)|≤M for all z, define the actual clock expectation A_t f(z)=∫_Ω f(Z(y,xRef,z,t,sample))P(dsample). For every finite t≥0, A_t f is Borel measurable in z; z↦(A_t f(z)−f(z))² is ν_y-integrable and obeys the pointwise bound (A_t f(z)−f(z))²≤4M² for every phase z. Moreover ∫(A_t f(z)−f(z))²ν_y(dz)→0 as t→0 in the ordinary nonpunctured neighborhood filter on nonnegative reals. The same single existential actual phase Z is used for every test, bound and initial state. These outputs hold for every deterministic y and xRef without any phase-invariance premise. This is the bounded continuous real test subclass, an attributed ASTIS extension of the authors compactly supported continuous test ingredient in AppendixA.1 Ex22 p6.2. It is not the general L² equivalence-class operator theorem. Full invariant-law and AE-representative semantics, contraction/Jensen, C_c density and extension to every L² test, restart/Markov/semigroup, hypocoercivity, implementation/error/unbounded cost, actual-input composition and full main results remain separate OPEN obligations.
Lean statement · actual_outer_bounded_l2_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. In addition, define the exact conditional position probability q_y=volume.tilted(x↦−V(x)−‖x−y‖²/(2η)) and the initial phase probability ν_y=q_y⊗N(0,I_E). Both probability normalizations are conclusions derived from the same six analytic hypotheses. For each fixed y,xRef, each continuous real f:E×E→ℝ and every M≥0 with |f(z)|≤M for all z, define the actual clock expectation A_t f(z)=∫_Ω f(Z(y,xRef,z,t,sample))P(dsample). For every finite t≥0, A_t f is Borel measurable in z; z↦(A_t f(z)−f(z))² is ν_y-integrable and obeys the pointwise bound (A_t f(z)−f(z))²≤4M² for every phase z. Moreover ∫(A_t f(z)−f(z))²ν_y(dz)→0 as t→0 in the ordinary nonpunctured neighborhood filter on nonnegative reals. The same single existential actual phase Z is used for every test, bound and initial state. These outputs hold for every deterministic y and xRef without any phase-invariance premise. This is the bounded continuous real test subclass, an attributed ASTIS extension of the authors compactly supported continuous test ingredient in AppendixA.1 Ex22 p6.2. It is not the general L² equivalence-class operator theorem. Full invariant-law and AE-representative semantics, contraction/Jensen, C_c density and extension to every L² test, restart/Markov/semigroup, hypocoercivity, implementation/error/unbounded cost, actual-input composition and full main results 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.
theorem actual_outer_bounded_l2_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_outer_bounded_l2_continuity_statement hα hαβ hV hH hη hβηFull Lean proposition (definition) · actual_outer_bounded_l2_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.
private def actual_outer_bounded_l2_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₀)))
∧
(let q : E → Measure E := fun y =>
(volume : Measure E).tilted (fun x => -V x - ‖x - y‖ ^ 2 / (2 * η))
let ν : E → Measure (E × E) := fun y => (q y).prod (stdGaussian E)
(∀ y : E, IsProbabilityMeasure (q y) ∧ IsProbabilityMeasure (ν y)) ∧
(∀ y xRef : E, ∀ f : (E × E) → ℝ, Continuous f →
∀ M : ℝ, 0 ≤ M → (∀ z : E × E, |f z| ≤ M) →
let A : ℝ≥0 → (E × E) → ℝ := fun t z₀ =>
∫ sample, f (Z y xRef z₀ t sample) ∂P
(∀ t : ℝ≥0, Measurable (A t) ∧
Integrable (fun z₀ : E × E => (A t z₀ - f z₀) ^ 2) (ν y) ∧
(∀ z₀ : E × E, (A t z₀ - f z₀) ^ 2 ≤ 4 * M ^ 2)) ∧
Tendsto (fun t : ℝ≥0 =>
∫ z₀, (A t z₀ - f z₀) ^ 2 ∂(ν y)) (𝓝 0) (𝓝 0)))
set_option maxHeartbeats 1600000 inProof roadmap
- 1Retain one actual phase and define the exact initial law
Keep the canonical exponential clock probability and define q_y by its literal quadratic Gibbs tilt, with ν_y its standard-Gaussian momentum product. Consume the verified actual83 phase, retaining all eleven algorithm definitions, joint measurability, covered and fallback behavior, fixed-parameter common-AE initialization, defect/tail estimates and bounded-test expectation limit.
- 2Derive conditional position normalization internally
Strong convexity and C² regularity imply a positive finite Gibbs normalizer via the existing augmentation theorem. Therefore μ=volume.tilted(−V) is a probability. The existing Gaussian conditional-kernel producer is Markov; its exact iterated-tilt identity equals q_y after adding the two exponents. Hence q_y is a probability for every y, rather than a zero-totalized tilt accepted by assumption.
- 3Normalize the actual phase and clock inputs
The product of q_y and the standard Gaussian is a probability. The actual infinite exponential product is a probability by its existing compiled producer. Return the unchanged actual83 clauses and the new probability outputs, then fix y,xRef,f and its arbitrary admissible M before defining A.
- 4Prove measurable dependence of the clock expectation on the initial phase
For fixed time, insert (y,xRef,z,t,sample) into the jointly Borel actual phase map and compose with continuous f. The existing Mathlib parameter-integral theorem makes the integral over P a strongly measurable, hence Borel measurable, function of z. Integrability is already supplied for every initial state by actual83.
- 5Bound the expectation and its squared discrepancy
The norm of an integral is at most the integral of the norm. Since |f|≤M and P has total mass one, |A_tf(z)|≤M. Together with |f(z)|≤M this gives −2M≤A_tf(z)−f(z)≤2M. Multiplying the two nonnegative factors 2M±(A_tf−f) proves the exact4M² square bound, including M=0.
- 6Make the square difference integrable under the exact phase law
State measurability of A and f gives measurability of their squared difference. Its norm is the same nonnegative square, bounded by4M² for every state. This constant is integrable under the already derived probability ν_y, yielding square integrability for every finite time. No invariant-law hypothesis is needed.
- 7Apply the actual pointwise expectation limit at every initial phase
The verified actual83 theorem gives A_tf(z)→f(z) for every fixed z, in the ordinary NNReal neighborhood filter at zero. Subtracting the constant f(z) and squaring gives (A_tf(z)−f(z))²→0 for every z. This is convergence of clock expectations, without asserting almost-sure convergence of sample paths.
- 8Integrate the pointwise limit by finite-probability dominated convergence
Use Mathlib filter dominated convergence with the exact outer law ν_y. Every finite-time integrand is measurable,4M² dominates it for every t and z, that constant is integrable, and the pointwise limit is zero everywhere. The integral of zero is zero. This closes the bounded-test outer square-integral ingredient only; source all-L2 extension still needs invariant-law, contraction and density edges.
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.
- For every deterministic y, q_y is the exact quadratic Gibbs tilt under volume and ν_y=q_y.prod(stdGaussian E). Their probability laws are derived internally from the original assumptions, not supplied as public normalization or invariance premises.
- For fixed y,xRef and f,M, the new conclusions concern state measurability and outer square integrability/convergence under this exact ν_y. The clock input is the same independent canonical P; neither y nor xRef is randomized or substituted through a correlated law.
- All-L2 equivalence-class well-definedness, invariant law, contraction and density are excluded. The bounded-test argument uses the finite probability ν_y and an explicit4M² integrable constant, not invariance or a TV transfer for unbounded quantities.
Mathematical proof
1. Retain one actual phase and define the exact initial law
Keep the canonical exponential clock probability and define q_y by its literal quadratic Gibbs tilt, with ν_y its standard-Gaussian momentum product. Consume the verified actual83 phase, retaining all eleven algorithm definitions, joint measurability, covered and fallback behavior, fixed-parameter common-AE initialization, defect/tail estimates and bounded-test expectation limit.
Corresponding Lean step
classical
let P : Measure (ℕ → ℝ) := Measure.infinitePi (fun _ : ℕ => expMeasure (1 : ℝ))
let q : E → Measure E := fun y =>
(volume : Measure E).tilted (fun x => -V x - ‖x - y‖ ^ 2 / (2 * η))
let ν : E → Measure (E × E) := fun y => (q y).prod (stdGaussian E)
obtain ⟨Z, hZM, hcovered, hfallback, hAE, hshort, htest⟩ :=
ActualBoundedTestContinuity.actual_bounded_test_expectation_continuity
hα hαβ hV hH hη hβη
Exact contiguous compiled proof region; prior local definitions and facts remain in scope.
2. Derive conditional position normalization internally
Strong convexity and C² regularity imply a positive finite Gibbs normalizer via the existing augmentation theorem. Therefore μ=volume.tilted(−V) is a probability. The existing Gaussian conditional-kernel producer is Markov; its exact iterated-tilt identity equals q_y after adding the two exponents. Hence q_y is a probability for every y, rather than a zero-totalized tilt accepted by assumption.
Corresponding Lean step
have hZV := (GibbsAugmentation.normalized_augmentation_density
hα hV (fun x v => (hH x v).1) hη).1
have hi : Integrable (fun x : E => Real.exp (-V x)) (volume : Measure E) :=
Integrable.of_integral_ne_zero hZV.ne'
let μ : Measure E := (volume : Measure E).tilted (fun x => -V x)
letI : IsProbabilityMeasure μ := isProbabilityMeasure_tilted hi
obtain ⟨R, hR, hRy, _⟩ :=
AutoSamplingTheory.TechnicalLemmas.Probability.GaussianConditionalKernel.exists_tilted_isCondKernel μ hη
letI : IsMarkovKernel R := hR
have hRq (y : E) : R y = q y := by
rw [hRy y, show μ = (volume : Measure E).tilted (fun x => -V x) from rfl,
tilted_tilted hi]
congr 1
funext z
dsimp only [Pi.add_apply]
ring
have hqprob (y : E) : IsProbabilityMeasure (q y) := by
rw [← hRq y]
infer_instance
Exact contiguous compiled proof region; prior local definitions and facts remain in scope.
3. Normalize the actual phase and clock inputs
The product of q_y and the standard Gaussian is a probability. The actual infinite exponential product is a probability by its existing compiled producer. Return the unchanged actual83 clauses and the new probability outputs, then fix y,xRef,f and its arbitrary admissible M before defining A.
Corresponding Lean step
have hνprob (y : E) : IsProbabilityMeasure (ν y) := by
letI := hqprob y
dsimp only [ν]
infer_instance
letI : IsProbabilityMeasure P :=
AutoSamplingTheory.TechnicalLemmas.Probability.UnitExponentialProduct.unit_exponential_product_laws.1
refine ⟨Z, hZM, hcovered, hfallback, hAE, hshort, htest, ?_⟩
refine ⟨fun y => ⟨hqprob y, hνprob y⟩, ?_⟩
intro y xRef f hf M hM hbound
letI := hνprob y
let A : ℝ≥0 → (E × E) → ℝ := fun t z₀ => ∫ sample, f (Z y xRef z₀ t sample) ∂P
Exact contiguous compiled proof region; prior local definitions and facts remain in scope.
4. Prove measurable dependence of the clock expectation on the initial phase
For fixed time, insert (y,xRef,z,t,sample) into the jointly Borel actual phase map and compose with continuous f. The existing Mathlib parameter-integral theorem makes the integral over P a strongly measurable, hence Borel measurable, function of z. Integrability is already supplied for every initial state by actual83.
Corresponding Lean step
have hAM (t : ℝ≥0) : Measurable (A t) := by
have hargs : Measurable (fun a : (E × E) × (ℕ → ℝ) =>
(((y, xRef), a.1), t, a.2)) :=
(measurable_const.prodMk measurable_fst).prodMk (measurable_const.prodMk measurable_snd)
exact ((hf.measurable.comp (hZM.comp hargs)).stronglyMeasurable.integral_prod_right').measurable
Exact contiguous compiled proof region; prior local definitions and facts remain in scope.
5. Bound the expectation and its squared discrepancy
The norm of an integral is at most the integral of the norm. Since |f|≤M and P has total mass one, |A_tf(z)|≤M. Together with |f(z)|≤M this gives −2M≤A_tf(z)−f(z)≤2M. Multiplying the two nonnegative factors 2M±(A_tf−f) proves the exact4M² square bound, including M=0.
Corresponding Lean step
have hAbound (t : ℝ≥0) (z₀ : E × E) : |A t z₀| ≤ M := by
have hb : ∀ᵐ sample ∂P, ‖f (Z y xRef z₀ t sample)‖ ≤ M :=
Filter.Eventually.of_forall fun sample => by
simpa only [Real.norm_eq_abs] using hbound (Z y xRef z₀ t sample)
simpa only [A, Real.norm_eq_abs, probReal_univ, mul_one] using
norm_integral_le_of_norm_le_const hb
have hsquare (t : ℝ≥0) (z₀ : E × E) : (A t z₀ - f z₀) ^ 2 ≤ 4 * M ^ 2 := by
have ha := (abs_le.mp (hAbound t z₀))
have hb := (abs_le.mp (hbound z₀))
nlinarith [sq_nonneg (A t z₀ - f z₀ - 2 * M),
mul_nonneg (show 0 ≤ 2 * M - (A t z₀ - f z₀) by linarith)
(show 0 ≤ 2 * M + (A t z₀ - f z₀) by linarith)]
Exact contiguous compiled proof region; prior local definitions and facts remain in scope.
6. Make the square difference integrable under the exact phase law
State measurability of A and f gives measurability of their squared difference. Its norm is the same nonnegative square, bounded by4M² for every state. This constant is integrable under the already derived probability ν_y, yielding square integrability for every finite time. No invariant-law hypothesis is needed.
Corresponding Lean step
have hsM (t : ℝ≥0) : Measurable (fun z₀ : E × E => (A t z₀ - f z₀) ^ 2) :=
((hAM t).sub hf.measurable).pow_const 2
have hsi (t : ℝ≥0) : Integrable (fun z₀ : E × E => (A t z₀ - f z₀) ^ 2) (ν y) := by
apply Integrable.of_bound (hsM t).aestronglyMeasurable (4 * M ^ 2)
exact Filter.Eventually.of_forall fun z₀ => by
simpa only [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg (A t z₀ - f z₀))] using hsquare t z₀
refine ⟨fun t => ⟨hAM t, hsi t, hsquare t⟩, ?_⟩
Exact contiguous compiled proof region; prior local definitions and facts remain in scope.
7. Apply the actual pointwise expectation limit at every initial phase
The verified actual83 theorem gives A_tf(z)→f(z) for every fixed z, in the ordinary NNReal neighborhood filter at zero. Subtracting the constant f(z) and squaring gives (A_tf(z)−f(z))²→0 for every z. This is convergence of clock expectations, without asserting almost-sure convergence of sample paths.
Corresponding Lean step
have hlimit (z₀ : E × E) : Tendsto (fun t : ℝ≥0 => (A t z₀ - f z₀) ^ 2)
(𝓝 0) (𝓝 0) := by
have ht : Tendsto (fun t : ℝ≥0 => A t z₀) (𝓝 0) (𝓝 (f z₀)) :=
(htest y xRef z₀ f hf M hM hbound).2
have hc : Tendsto (fun _ : ℝ≥0 => f z₀) (𝓝 0) (𝓝 (f z₀)) := tendsto_const_nhds
simpa only [sub_self, zero_pow (by decide : 2 ≠ 0)] using
(ht.sub hc).pow 2
Exact contiguous compiled proof region; prior local definitions and facts remain in scope.
8. Integrate the pointwise limit by finite-probability dominated convergence
Use Mathlib filter dominated convergence with the exact outer law ν_y. Every finite-time integrand is measurable,4M² dominates it for every t and z, that constant is integrable, and the pointwise limit is zero everywhere. The integral of zero is zero. This closes the bounded-test outer square-integral ingredient only; source all-L2 extension still needs invariant-law, contraction and density edges.
Corresponding Lean step
have hDCT := tendsto_integral_filter_of_dominated_convergence (μ := ν y)
(F := fun t : ℝ≥0 => fun z₀ : E × E => (A t z₀ - f z₀) ^ 2)
(f := fun _ : E × E => (0 : ℝ)) (fun _ : E × E => 4 * M ^ 2)
(Filter.Eventually.of_forall fun t => (hsM t).aestronglyMeasurable)
(Filter.Eventually.of_forall fun t => Filter.Eventually.of_forall fun z₀ => by
simpa only [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg (A t z₀ - f z₀))] using hsquare t z₀)
(integrable_const _) (Filter.Eventually.of_forall hlimit)
simpa only [integral_zero] using hDCT
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_outer_bounded_l2_continuity
Retain one actual phase and define the exact initial law; Derive conditional position normalization internally; Normalize the actual phase and clock inputs; Prove measurable dependence of the clock expectation on the initial phase; Bound the expectation and its squared discrepancy; Make the square difference integrable under the exact phase law; Apply the actual pointwise expectation limit at every initial phase; Integrate the pointwise limit by finite-probability dominated convergence
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.
theorem actual_outer_bounded_l2_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_outer_bounded_l2_continuity_statement hα hαβ hV hH hη hβη := by
classical
let P : Measure (ℕ → ℝ) := Measure.infinitePi (fun _ : ℕ => expMeasure (1 : ℝ))
let q : E → Measure E := fun y =>
(volume : Measure E).tilted (fun x => -V x - ‖x - y‖ ^ 2 / (2 * η))
let ν : E → Measure (E × E) := fun y => (q y).prod (stdGaussian E)
obtain ⟨Z, hZM, hcovered, hfallback, hAE, hshort, htest⟩ :=
ActualBoundedTestContinuity.actual_bounded_test_expectation_continuity
hα hαβ hV hH hη hβη
have hZV := (GibbsAugmentation.normalized_augmentation_density
hα hV (fun x v => (hH x v).1) hη).1
have hi : Integrable (fun x : E => Real.exp (-V x)) (volume : Measure E) :=
Integrable.of_integral_ne_zero hZV.ne'
let μ : Measure E := (volume : Measure E).tilted (fun x => -V x)
letI : IsProbabilityMeasure μ := isProbabilityMeasure_tilted hi
obtain ⟨R, hR, hRy, _⟩ :=
AutoSamplingTheory.TechnicalLemmas.Probability.GaussianConditionalKernel.exists_tilted_isCondKernel μ hη
letI : IsMarkovKernel R := hR
have hRq (y : E) : R y = q y := by
rw [hRy y, show μ = (volume : Measure E).tilted (fun x => -V x) from rfl,
tilted_tilted hi]
congr 1
funext z
dsimp only [Pi.add_apply]
ring
have hqprob (y : E) : IsProbabilityMeasure (q y) := by
rw [← hRq y]
infer_instance
have hνprob (y : E) : IsProbabilityMeasure (ν y) := by
letI := hqprob y
dsimp only [ν]
infer_instance
letI : IsProbabilityMeasure P :=
AutoSamplingTheory.TechnicalLemmas.Probability.UnitExponentialProduct.unit_exponential_product_laws.1
refine ⟨Z, hZM, hcovered, hfallback, hAE, hshort, htest, ?_⟩
refine ⟨fun y => ⟨hqprob y, hνprob y⟩, ?_⟩
intro y xRef f hf M hM hbound
letI := hνprob y
let A : ℝ≥0 → (E × E) → ℝ := fun t z₀ => ∫ sample, f (Z y xRef z₀ t sample) ∂P
have hAM (t : ℝ≥0) : Measurable (A t) := by
have hargs : Measurable (fun a : (E × E) × (ℕ → ℝ) =>
(((y, xRef), a.1), t, a.2)) :=
(measurable_const.prodMk measurable_fst).prodMk (measurable_const.prodMk measurable_snd)
exact ((hf.measurable.comp (hZM.comp hargs)).stronglyMeasurable.integral_prod_right').measurable
have hAbound (t : ℝ≥0) (z₀ : E × E) : |A t z₀| ≤ M := by
have hb : ∀ᵐ sample ∂P, ‖f (Z y xRef z₀ t sample)‖ ≤ M :=
Filter.Eventually.of_forall fun sample => by
simpa only [Real.norm_eq_abs] using hbound (Z y xRef z₀ t sample)
simpa only [A, Real.norm_eq_abs, probReal_univ, mul_one] using
norm_integral_le_of_norm_le_const hb
have hsquare (t : ℝ≥0) (z₀ : E × E) : (A t z₀ - f z₀) ^ 2 ≤ 4 * M ^ 2 := by
have ha := (abs_le.mp (hAbound t z₀))
have hb := (abs_le.mp (hbound z₀))
nlinarith [sq_nonneg (A t z₀ - f z₀ - 2 * M),
mul_nonneg (show 0 ≤ 2 * M - (A t z₀ - f z₀) by linarith)
(show 0 ≤ 2 * M + (A t z₀ - f z₀) by linarith)]
have hsM (t : ℝ≥0) : Measurable (fun z₀ : E × E => (A t z₀ - f z₀) ^ 2) :=
((hAM t).sub hf.measurable).pow_const 2
have hsi (t : ℝ≥0) : Integrable (fun z₀ : E × E => (A t z₀ - f z₀) ^ 2) (ν y) := by
apply Integrable.of_bound (hsM t).aestronglyMeasurable (4 * M ^ 2)
exact Filter.Eventually.of_forall fun z₀ => by
simpa only [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg (A t z₀ - f z₀))] using hsquare t z₀
refine ⟨fun t => ⟨hAM t, hsi t, hsquare t⟩, ?_⟩
have hlimit (z₀ : E × E) : Tendsto (fun t : ℝ≥0 => (A t z₀ - f z₀) ^ 2)
(𝓝 0) (𝓝 0) := by
have ht : Tendsto (fun t : ℝ≥0 => A t z₀) (𝓝 0) (𝓝 (f z₀)) :=
(htest y xRef z₀ f hf M hM hbound).2
have hc : Tendsto (fun _ : ℝ≥0 => f z₀) (𝓝 0) (𝓝 (f z₀)) := tendsto_const_nhds
simpa only [sub_self, zero_pow (by decide : 2 ≠ 0)] using
(ht.sub hc).pow 2
have hDCT := tendsto_integral_filter_of_dominated_convergence (μ := ν y)
(F := fun t : ℝ≥0 => fun z₀ : E × E => (A t z₀ - f z₀) ^ 2)
(f := fun _ : E × E => (0 : ℝ)) (fun _ : E × E => 4 * M ^ 2)
(Filter.Eventually.of_forall fun t => (hsM t).aestronglyMeasurable)
(Filter.Eventually.of_forall fun t => Filter.Eventually.of_forall fun z₀ => by
simpa only [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg (A t z₀ - f z₀))] using hsquare t z₀)
(integrable_const _) (Filter.Eventually.of_forall hlimit)
simpa only [integral_zero] using hDCT
end
end AutoSamplingTheory.ExampleCases.ProximalBPS.ActualOuterBoundedL2ContinuityScope and omitted-condition boundaries
- Retains actual83 full joint measurable physical phase, covered/fallback/commonAE/init/defect/smalltime/test clauses and literal eleven definitions. Exact q_y=volume.tilted(-V-quadratic), nu_y=q_y.prod(stdGaussian) probability derived internally. Fixed y and xRef; actual independent Exp1 clock expectation, state measurability,4M2 domination and bounded-test outer square-integral zero-time limit. No invariant-law, contraction or density premise. All-L2 AE operator/Jensen/contraction/density, phase invariance, restart/Markov/semigroup/hypocoercivity, implementation/error/unbounded cost/composition/main/PURIFIED/live/whole-Goal remain OPEN.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
AutoSamplingTheory.ExampleCases.ProximalBPS.ActualBoundedTestContinuity.actual_bounded_test_expectation_continuityAutoSamplingTheory.ExampleCases.ProximalBPS.GibbsAugmentation.normalized_augmentation_densityAutoSamplingTheory.TechnicalLemmas.Probability.GaussianConditionalKernel.exists_tilted_isCondKernelAutoSamplingTheory.TechnicalLemmas.Probability.UnitExponentialProduct.unit_exponential_product_laws
Mathlib API called (external library)
- isProbabilityMeasure_tilted
- Integrable.of_integral_ne_zero
- tilted_tilted
- StronglyMeasurable.integral_prod_right'
- norm_integral_le_of_norm_le_const
- Integrable.of_bound
- integrable_const
- tendsto_integral_filter_of_dominated_convergence
Mathematical sources
- Chen-Chewi-Lu-Zhang arXiv2609.06905v1 AppendixA.1 Ex22 p6.1-p6.2. ASTIS explicit bounded-continuous extension of the source compactly supported continuous test class; bounded outer square-integral ingredient only. — Retains actual83 full joint measurable physical phase, covered/fallback/commonAE/init/defect/smalltime/test clauses and literal eleven definitions. Exact q_y=volume.tilted(-V-quadratic), nu_y=q_y.prod(stdGaussian) probability derived internally. Fixed y and xRef; actual independent Exp1 clock expectation, state measurability,4M2 domination and bounded-test outer square-integral zero-time limit. No invariant-law, contraction or density premise. All-L2 AE operator/Jensen/contraction/density, phase invariance, restart/Markov/semigroup/hypocoercivity, implementation/error/unbounded cost/composition/main/PURIFIED/live/whole-Goal remain OPEN.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.