Actual PBPS event-time nonaccumulation
AutoSamplingTheory.ExampleCases.ProximalBPS.ActualNonaccumulation.actual_fixed_reference_event_time_nonaccumulation · 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. Fix any 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. Then for these fixed y,xRef,z0, for P-almost every sample, simultaneously: (i) for every finite nonnegative horizon t, all sufficiently large k satisfy t<T_k; (ii) for every such t the set {k∈ℕ:T_k≤t} is finite. Initialization index0 is included, and ε_k is source E_(k+1). The result includes both eventual stopping and infinite continuing paths with unbounded event times; it does not assert eventual stopping. It is an actual-input, fixed-reference nonaccumulation conclusion of Appendix A.1 Ex9, with ASTIS total-record and finite-index adapters. The global physical-time process and its additional properties are separate obligations.
Lean statement · actual_fixed_reference_event_time_nonaccumulation
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. Fix any 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. Then for these fixed y,xRef,z0, for P-almost every sample, simultaneously: (i) for every finite nonnegative horizon t, all sufficiently large k satisfy t<T_k; (ii) for every such t the set {k∈ℕ:T_k≤t} is finite. Initialization index0 is included, and ε_k is source E_(k+1). The result includes both eventual stopping and infinite continuing paths with unbounded event times; it does not assert eventual stopping. It is an actual-input, fixed-reference nonaccumulation conclusion of Appendix A.1 Ex9, with ASTIS total-record and finite-index adapters. The global physical-time process and its additional properties are separate 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_fixed_reference_event_time_nonaccumulation
{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_fixed_reference_event_time_nonaccumulation_statement hα hαβ hV hH hη hβηFull Lean proposition (definition) · actual_fixed_reference_event_time_nonaccumulation_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_fixed_reference_event_time_nonaccumulation_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 _ => ⊤)
∀ y xRef : E, ∀ z₀ : E × E, ∀ᵐ sample ∂P,
(∀ t : ℝ≥0, ∀ᶠ n : ℕ in atTop,
(t : WithTop ℝ≥0) < eventTime y xRef z₀ (ε sample) n) ∧
(∀ t : ℝ≥0, {n : ℕ | eventTime y xRef z₀ (ε sample) n ≤ (t : WithTop ℝ≥0)}.Finite)
set_option maxHeartbeats 800000 inProof roadmap
- 1Fix the actual source objects and stopped event times
Use the literal harmonic flow, zero-safe reflection, integrated rate, first hitting time and stopped recursion from the actual finite-prefix theorem. Fix the canonical Exp1 product and its total nonnegative thresholds. The energy H and finite cap C are internal formulas: H(z)=(η⁻¹‖x−c‖²+‖p‖²)/2 and C=√η β√(2H(z0))(√(2ηH(z0))+‖c−xRef‖). They are proved recurrence invariants and bounds, not theorem assumptions.
- 2Join the two actual compiled parents
Apply the finite-recursion theorem to the six analytic source hypotheses. It supplies initialization, monotone times, absorbing stopping, C≥0, the positive-cap increment and zero-cap stopping. Apply the concrete product theorem to obtain a common positive-threshold event and divergent partial sums, with no supplied stochastic witness.
- 3Intersect the two good-input events
For arbitrary fixed y,xRef,z0, intersect the almost-sure all-coordinate positivity and divergent-sum events. Positivity makes every clamped ε_k strictly positive. Extract the cap laws for this actual sample; these facts remain internal to the proof.
- 4Handle zero cap by absorbing stopping
Split on C=0. The initial record is active and ε0>0, so its first update stops. Absorption proves T_(1+k)=∞ for every k. Every finite horizon is therefore exceeded at all indices n≥1. This includes zero-energy and dimension-zero cases.
- 5Sum the actual positive-cap increments
In the other branch C≥0 and C≠0 give C>0. Let cap=toNNReal(C), whose real coercion is C. Starting from S0=T0=0, apply the actual extended-valued increment inequality and induction: S_(n+1)/C=S_n/C+ε_n/C≤T_n+ε_n/C≤T_(n+1). The same inequality remains valid after stopping since times are top.
- 6Use divergent inputs to escape every finite horizon
For any finite t, divergence gives S_n>tC eventually. Because C>0 this implies S_n/C>t. Combine this strict finite inequality, lifted into WithTop NNReal, with the prefix lower bound. This proves finite-horizon escape without requiring eventual equality to infinity.
- 7Turn escape into a finite index set
For each t, choose N such that n≥N implies t<T_n. Any n with T_n≤t must satisfy n<N. The sublevel index set is therefore contained in the finite natural interval [0,N); index0 is retained. Assemble both almost-sure conclusions.
Full assumptions and notation
All objects and hypotheses
- E is finite-dimensional real inner-product with its Borel measurable structure; no positive-dimension restriction. V is C² and α,β≥0.
- The six exact source conditions are α>0; α≤β; V∈C²; for all x,v, α‖v‖²≤D²V(x)[v,v]≤β‖v‖²; η>0; βη≤1. No third or higher derivative condition.
- y,xRef,z0 are arbitrary deterministic parameters. P and ε are literal canonical definitions. No probability, iid, positivity, divergence, cap, energy, waiting-time or recurrence certificate is a public premise.
- Threshold positivity and faithful clamp/raw equality hold simultaneously only almost surely. The all-finite-horizon conclusion is pathwise on the common good-input event for each fixed parameter triple; no uncountable intersection over triples is assumed.
- Stopped records have eventTime=∞ with no phase at infinity. The statement counts indices including index0, not a physical bounce-count expectation. The author direct Exp mean-one strong-law route is distinct from the reused ASTIS bounded-indicator sufficient route.
Mathematical proof
1. Fix the actual source objects and stopped event times
Use the literal harmonic flow, zero-safe reflection, integrated rate, first hitting time and stopped recursion from the actual finite-prefix theorem. Fix the canonical Exp1 product and its total nonnegative thresholds. The energy H and finite cap C are internal formulas: H(z)=(η⁻¹‖x−c‖²+‖p‖²)/2 and C=√η β√(2H(z0))(√(2ηH(z0))+‖c−xRef‖). They are proved recurrence invariants and bounds, not theorem assumptions.
Corresponding Lean step
classical
let P : Measure (ℕ → ℝ) := Measure.infinitePi (fun _ : ℕ => expMeasure (1 : ℝ))
let ε : (ℕ → ℝ) → ℕ → ℝ≥0 := fun sample k => Real.toNNReal (sample k)
let c : E → E → E := fun y xRef => y - η • gradient V xRef
let Φ : E → E → ℝ → (E × E) → (E × E) := fun y xRef t z =>
(c y xRef + Real.cos t • (z.1 - c y xRef) +
(Real.sqrt η * Real.sin t) • z.2,
(-Real.sin t / Real.sqrt η) • (z.1 - c y xRef) + Real.cos t • z.2)
let S : E → (E × E) → (E × E) := fun xRef z =>
(z.1, z.2 - (2 * inner ℝ z.2 (gradient V z.1 - gradient V xRef) /
‖gradient V z.1 - gradient V xRef‖ ^ 2) • (gradient V z.1 - gradient V xRef))
let rate : E → (E × E) → ℝ := fun xRef z =>
Real.sqrt η * max 0 (inner ℝ z.2 (gradient V z.1 - gradient V xRef))
let H : E → E → (E × E) → ℝ := fun y xRef z =>
(η⁻¹ * ‖z.1 - c y xRef‖ ^ 2 + ‖z.2‖ ^ 2) / 2
let C : E → E → (E × E) → ℝ := fun y xRef z =>
Real.sqrt η * (β : ℝ) * Real.sqrt (2 * H y xRef z) *
(Real.sqrt (2 * η * H y xRef z) + ‖c y xRef - 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 _ => ⊤)
change ∀ y xRef : E, ∀ z₀ : E × E, ∀ᵐ sample ∂P,
(∀ t : ℝ≥0, ∀ᶠ n : ℕ in atTop,
(t : WithTop ℝ≥0) < eventTime y xRef z₀ (ε sample) n) ∧
(∀ t : ℝ≥0, {n : ℕ | eventTime y xRef z₀ (ε sample) n ≤ (t : WithTop ℝ≥0)}.Finite)
Exact contiguous compiled proof region; preceding local definitions and facts remain in scope.
2. Join the two actual compiled parents
Apply the finite-recursion theorem to the six analytic source hypotheses. It supplies initialization, monotone times, absorbing stopping, C≥0, the positive-cap increment and zero-cap stopping. Apply the concrete product theorem to obtain a common positive-threshold event and divergent partial sums, with no supplied stochastic witness.
Corresponding Lean step
-- Reuse the actual deterministic recurrence; no cap or recurrence is supplied.
rcases ActualFiniteJumpRecursion.actual_fixed_reference_finite_jump_recursion
hα hαβ hV hH hη hβη with
⟨hinit, _, _, _, _, htime, hstop, _, hcap, _⟩
-- The good event supplies all positive thresholds and divergent actual sums.
rcases AutoSamplingTheory.TechnicalLemmas.Probability.UnitExponentialProduct.unit_exponential_product_laws with
⟨_, _, _, hgood, hdiv⟩
Exact contiguous compiled proof region; preceding local definitions and facts remain in scope.
3. Intersect the two good-input events
For arbitrary fixed y,xRef,z0, intersect the almost-sure all-coordinate positivity and divergent-sum events. Positivity makes every clamped ε_k strictly positive. Extract the cap laws for this actual sample; these facts remain internal to the proof.
Corresponding Lean step
intro y xRef z₀
filter_upwards [hgood, hdiv] with sample hpos hsum
have hepos (k : ℕ) : 0 < ε sample k :=
Real.toNNReal_pos.mpr (hpos k).1
obtain ⟨hC, hinc, hzero⟩ := hcap y xRef z₀ (ε sample)
Exact contiguous compiled proof region; preceding local definitions and facts remain in scope.
4. Handle zero cap by absorbing stopping
Split on C=0. The initial record is active and ε0>0, so its first update stops. Absorption proves T_(1+k)=∞ for every k. Every finite horizon is therefore exceeded at all indices n≥1. This includes zero-energy and dimension-zero cases.
Corresponding Lean step
have hescape : ∀ t : ℝ≥0, ∀ᶠ n : ℕ in atTop,
(t : WithTop ℝ≥0) < eventTime y xRef z₀ (ε sample) n := by
-- Zero cap forces the first positive-threshold update to stop; it absorbs.
by_cases hC0 : C y xRef z₀ = 0
· have hfirst : record y xRef z₀ (ε sample) 1 = Sum.inr () :=
hzero hC0 0 (0, z₀) (hinit y xRef z₀ (ε sample)) (hepos 0)
intro t
filter_upwards [eventually_ge_atTop (1 : ℕ)] with n hn
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hn
have hs : record y xRef z₀ (ε sample) (1 + k) = Sum.inr () :=
hstop y xRef z₀ (ε sample) 1 k hfirst
change (t : WithTop ℝ≥0) < (record y xRef z₀ (ε sample) (1 + k)).elim _ _
rw [hs]
exact WithTop.coe_lt_top t
Exact contiguous compiled proof region; preceding local definitions and facts remain in scope.
5. Sum the actual positive-cap increments
In the other branch C≥0 and C≠0 give C>0. Let cap=toNNReal(C), whose real coercion is C. Starting from S0=T0=0, apply the actual extended-valued increment inequality and induction: S_(n+1)/C=S_n/C+ε_n/C≤T_n+ε_n/C≤T_(n+1). The same inequality remains valid after stopping since times are top.
Corresponding Lean step
-- Positive cap: inductively compare every actual clock with partial sums/C.
· have hCp : 0 < C y xRef z₀ := lt_of_le_of_ne hC (Ne.symm hC0)
let cap : ℝ≥0 := Real.toNNReal (C y xRef z₀)
have hcapcoe : (cap : ℝ) = C y xRef z₀ := Real.coe_toNNReal _ hC
have hcapPos : 0 < cap := Real.toNNReal_pos.mpr hCp
have hbound (n : ℕ) :
(((∑ k ∈ Finset.range n, ε sample k) / cap : ℝ≥0) : WithTop ℝ≥0) ≤
eventTime y xRef z₀ (ε sample) n := by
induction n with
| zero => simpa using (htime y xRef z₀ (ε sample)).1.ge
| succ n ih =>
have hi := hinc hCp n
have hterm : Real.toNNReal ((ε sample n : ℝ) / C y xRef z₀) =
ε sample n / cap := by
rw [Real.toNNReal_div (ε sample n).coe_nonneg, Real.toNNReal_coe]
rw [hterm] at hi
calc
(((∑ k ∈ Finset.range (n + 1), ε sample k) / cap : ℝ≥0) : WithTop ℝ≥0)
= (((∑ k ∈ Finset.range n, ε sample k) / cap : ℝ≥0) : WithTop ℝ≥0) +
((ε sample n / cap : ℝ≥0) : WithTop ℝ≥0) := by
rw [Finset.sum_range_succ, add_div, WithTop.coe_add]
_ ≤ eventTime y xRef z₀ (ε sample) n +
((ε sample n / cap : ℝ≥0) : WithTop ℝ≥0) := add_le_add ih le_rfl
_ ≤ eventTime y xRef z₀ (ε sample) (n + 1) := hi
Exact contiguous compiled proof region; preceding local definitions and facts remain in scope.
6. Use divergent inputs to escape every finite horizon
For any finite t, divergence gives S_n>tC eventually. Because C>0 this implies S_n/C>t. Combine this strict finite inequality, lifted into WithTop NNReal, with the prefix lower bound. This proves finite-horizon escape without requiring eventual equality to infinity.
Corresponding Lean step
intro t
have hs : ∀ᶠ n : ℕ in atTop,
(t : ℝ) * C y xRef z₀ < ∑ k ∈ Finset.range n, (ε sample k : ℝ) :=
hsum.eventually (eventually_gt_atTop ((t : ℝ) * C y xRef z₀))
filter_upwards [hs] with n hn
have ht : t < (∑ k ∈ Finset.range n, ε sample k) / cap := by
apply (NNReal.coe_lt_coe).mp
push_cast
rw [hcapcoe]
exact (lt_div_iff₀ hCp).mpr hn
exact lt_of_lt_of_le (WithTop.coe_lt_coe.mpr ht) (hbound n)
Exact contiguous compiled proof region; preceding local definitions and facts remain in scope.
7. Turn escape into a finite index set
For each t, choose N such that n≥N implies t<T_n. Any n with T_n≤t must satisfy n<N. The sublevel index set is therefore contained in the finite natural interval [0,N); index0 is retained. Assemble both almost-sure conclusions.
Corresponding Lean step
refine ⟨hescape, ?_⟩
-- The bounded-horizon index set is contained in a finite initial interval.
intro t
obtain ⟨N, hN⟩ := eventually_atTop.mp (hescape t)
apply (Set.finite_Iio N).subset
intro n hn
exact lt_of_not_ge (fun hge => (not_lt_of_ge hn) (hN n hge))
Exact contiguous compiled proof region; preceding 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_fixed_reference_event_time_nonaccumulation
Fix the actual source objects and stopped event times; Join the two actual compiled parents; Intersect the two good-input events; Handle zero cap by absorbing stopping; Sum the actual positive-cap increments; Use divergent inputs to escape every finite horizon; Turn escape into a finite index set
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_fixed_reference_event_time_nonaccumulation
{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_fixed_reference_event_time_nonaccumulation_statement hα hαβ hV hH hη hβη := by
classical
let P : Measure (ℕ → ℝ) := Measure.infinitePi (fun _ : ℕ => expMeasure (1 : ℝ))
let ε : (ℕ → ℝ) → ℕ → ℝ≥0 := fun sample k => Real.toNNReal (sample k)
let c : E → E → E := fun y xRef => y - η • gradient V xRef
let Φ : E → E → ℝ → (E × E) → (E × E) := fun y xRef t z =>
(c y xRef + Real.cos t • (z.1 - c y xRef) +
(Real.sqrt η * Real.sin t) • z.2,
(-Real.sin t / Real.sqrt η) • (z.1 - c y xRef) + Real.cos t • z.2)
let S : E → (E × E) → (E × E) := fun xRef z =>
(z.1, z.2 - (2 * inner ℝ z.2 (gradient V z.1 - gradient V xRef) /
‖gradient V z.1 - gradient V xRef‖ ^ 2) • (gradient V z.1 - gradient V xRef))
let rate : E → (E × E) → ℝ := fun xRef z =>
Real.sqrt η * max 0 (inner ℝ z.2 (gradient V z.1 - gradient V xRef))
let H : E → E → (E × E) → ℝ := fun y xRef z =>
(η⁻¹ * ‖z.1 - c y xRef‖ ^ 2 + ‖z.2‖ ^ 2) / 2
let C : E → E → (E × E) → ℝ := fun y xRef z =>
Real.sqrt η * (β : ℝ) * Real.sqrt (2 * H y xRef z) *
(Real.sqrt (2 * η * H y xRef z) + ‖c y xRef - 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 _ => ⊤)
change ∀ y xRef : E, ∀ z₀ : E × E, ∀ᵐ sample ∂P,
(∀ t : ℝ≥0, ∀ᶠ n : ℕ in atTop,
(t : WithTop ℝ≥0) < eventTime y xRef z₀ (ε sample) n) ∧
(∀ t : ℝ≥0, {n : ℕ | eventTime y xRef z₀ (ε sample) n ≤ (t : WithTop ℝ≥0)}.Finite)
-- Reuse the actual deterministic recurrence; no cap or recurrence is supplied.
rcases ActualFiniteJumpRecursion.actual_fixed_reference_finite_jump_recursion
hα hαβ hV hH hη hβη with
⟨hinit, _, _, _, _, htime, hstop, _, hcap, _⟩
-- The good event supplies all positive thresholds and divergent actual sums.
rcases AutoSamplingTheory.TechnicalLemmas.Probability.UnitExponentialProduct.unit_exponential_product_laws with
⟨_, _, _, hgood, hdiv⟩
intro y xRef z₀
filter_upwards [hgood, hdiv] with sample hpos hsum
have hepos (k : ℕ) : 0 < ε sample k :=
Real.toNNReal_pos.mpr (hpos k).1
obtain ⟨hC, hinc, hzero⟩ := hcap y xRef z₀ (ε sample)
have hescape : ∀ t : ℝ≥0, ∀ᶠ n : ℕ in atTop,
(t : WithTop ℝ≥0) < eventTime y xRef z₀ (ε sample) n := by
-- Zero cap forces the first positive-threshold update to stop; it absorbs.
by_cases hC0 : C y xRef z₀ = 0
· have hfirst : record y xRef z₀ (ε sample) 1 = Sum.inr () :=
hzero hC0 0 (0, z₀) (hinit y xRef z₀ (ε sample)) (hepos 0)
intro t
filter_upwards [eventually_ge_atTop (1 : ℕ)] with n hn
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hn
have hs : record y xRef z₀ (ε sample) (1 + k) = Sum.inr () :=
hstop y xRef z₀ (ε sample) 1 k hfirst
change (t : WithTop ℝ≥0) < (record y xRef z₀ (ε sample) (1 + k)).elim _ _
rw [hs]
exact WithTop.coe_lt_top t
-- Positive cap: inductively compare every actual clock with partial sums/C.
· have hCp : 0 < C y xRef z₀ := lt_of_le_of_ne hC (Ne.symm hC0)
let cap : ℝ≥0 := Real.toNNReal (C y xRef z₀)
have hcapcoe : (cap : ℝ) = C y xRef z₀ := Real.coe_toNNReal _ hC
have hcapPos : 0 < cap := Real.toNNReal_pos.mpr hCp
have hbound (n : ℕ) :
(((∑ k ∈ Finset.range n, ε sample k) / cap : ℝ≥0) : WithTop ℝ≥0) ≤
eventTime y xRef z₀ (ε sample) n := by
induction n with
| zero => simpa using (htime y xRef z₀ (ε sample)).1.ge
| succ n ih =>
have hi := hinc hCp n
have hterm : Real.toNNReal ((ε sample n : ℝ) / C y xRef z₀) =
ε sample n / cap := by
rw [Real.toNNReal_div (ε sample n).coe_nonneg, Real.toNNReal_coe]
rw [hterm] at hi
calc
(((∑ k ∈ Finset.range (n + 1), ε sample k) / cap : ℝ≥0) : WithTop ℝ≥0)
= (((∑ k ∈ Finset.range n, ε sample k) / cap : ℝ≥0) : WithTop ℝ≥0) +
((ε sample n / cap : ℝ≥0) : WithTop ℝ≥0) := by
rw [Finset.sum_range_succ, add_div, WithTop.coe_add]
_ ≤ eventTime y xRef z₀ (ε sample) n +
((ε sample n / cap : ℝ≥0) : WithTop ℝ≥0) := add_le_add ih le_rfl
_ ≤ eventTime y xRef z₀ (ε sample) (n + 1) := hi
intro t
have hs : ∀ᶠ n : ℕ in atTop,
(t : ℝ) * C y xRef z₀ < ∑ k ∈ Finset.range n, (ε sample k : ℝ) :=
hsum.eventually (eventually_gt_atTop ((t : ℝ) * C y xRef z₀))
filter_upwards [hs] with n hn
have ht : t < (∑ k ∈ Finset.range n, ε sample k) / cap := by
apply (NNReal.coe_lt_coe).mp
push_cast
rw [hcapcoe]
exact (lt_div_iff₀ hCp).mpr hn
exact lt_of_lt_of_le (WithTop.coe_lt_coe.mpr ht) (hbound n)
refine ⟨hescape, ?_⟩
-- The bounded-horizon index set is contained in a finite initial interval.
intro t
obtain ⟨N, hN⟩ := eventually_atTop.mp (hescape t)
apply (Set.finite_Iio N).subset
intro n hn
exact lt_of_not_ge (fun hge => (not_lt_of_ge hn) (hN n hge))
end
end AutoSamplingTheory.ExampleCases.ProximalBPS.ActualNonaccumulationScope and omitted-condition boundaries
- Only actual fixed-reference recursion nonaccumulation and finite bounded-horizon indices. No global physical-time path existence/uniqueness/measurability, Markov/invariance/kernel/hypocoercivity, PBPS main accuracy/implementation error/expected queries or PBPS-SPHMC composition. Author direct Exp mean-one SLLN remains an alternative open route; ASTIS uses verified bounded-indicator divergence. No merged/stabilized/purified/live/full-paper/Goal credit.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
AutoSamplingTheory.ExampleCases.ProximalBPS.ActualFiniteJumpRecursion.actual_fixed_reference_finite_jump_recursionAutoSamplingTheory.TechnicalLemmas.Probability.UnitExponentialProduct.unit_exponential_product_laws
Mathlib API called (external library)
- Real.toNNReal_pos
- Real.coe_toNNReal
- Real.toNNReal_div
- Real.toNNReal_coe
- NNReal.coe_lt_coe
- Finset.sum_range_succ
- WithTop.coe_add
- WithTop.coe_lt_coe
- WithTop.coe_lt_top
- Filter.eventually_ge_atTop
- Filter.eventually_gt_atTop
- Filter.eventually_atTop
- Set.finite_Iio
Mathematical sources
- arXiv2609.06905v1 Appendix A.1 (A.2), Ex8-Ex9 and following SLLN/nonaccumulation clauses; Algorithm1 actual flow/bounce/rate and standing six analytic conditions. — Only actual fixed-reference recursion nonaccumulation and finite bounded-horizon indices. No global physical-time path existence/uniqueness/measurability, Markov/invariance/kernel/hypocoercivity, PBPS main accuracy/implementation error/expected queries or PBPS-SPHMC composition. Author direct Exp mean-one SLLN remains an alternative open route; ASTIS uses verified bounded-indicator divergence. No merged/stabilized/purified/live/full-paper/Goal credit.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.