Actual PBPS path reversal and survival-integral substitution
AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPrescribedPathReversal.actual_prescribed_path_reversal_and_survival · theorem · Teaching coverage
Mathematical statement
Let E be a finite-dimensional real inner-product space with its Borel sigma algebra, including dimension zero. Let V:E→R, alpha,beta≥0 and eta in R. Assume alpha>0, alpha≤beta, V is C2, alpha||v||^2≤D2V(x)[v,v]≤beta||v||^2 for every x,v in E, eta>0 and beta*eta≤1. For y,r in E put c=y-eta grad V(r), h_r(x)=grad V(x)-grad V(r), R(x,p)=(x,-p), Phi_(y,r,u)(x,p)=(c+cos(u)(x-c)+sqrt(eta)sin(u)p, -sin(u)/sqrt(eta)(x-c)+cos(u)p), S_r(x,p)=(x,p-(2<p,h_r(x)>/||h_r(x)||^2)h_r(x)). Real division by zero is zero, so a zero normal gives the identity bounce. Let ell=volume_E tensor volume_E, with canonical Hilbert-space Lebesgue measure. For every integer n≥0 and horizon T≥0, let Delta_n(T) consist of real tuples 0<t_0<...<t_(n-1)<T. Equivalently, prepending 0 produces a strictly increasing tuple and every entry is less than T. Let Prefix_n(T) be this subtype and m_n,T the comap of Lebesgue measure on R^n under its inclusion. This is unnormalized simplex volume. For n=0 the tuple is empty and its zero-dimensional volume is one; for T=0 and n>0 the subtype is empty. Write q_0=0 and q_(j+1)=t_j. Starting at z_0=z, define z_(j+1)=S_r(Phi_(y,r,t_j-q_j)(z_j)) for 0≤j<n. Define records K_j=(q_j,z_j), each embedded in the live branch of (R_nonnegative x (E x E)) plus a cemetery symbol. For a general history of n+1 such records, the path reconstruction Psi at s in [0,T] starts from z and visits records in increasing index order: a live record (a,w) replaces the accumulator by Phi_(y,r,s-a)(w) exactly when a≤s; future records and cemetery records leave it unchanged. Here s-a is nonnegative subtraction. Define Gamma_(y,r,z,t)=Psi(K), the actual finite prescribed path; thus its value at an event is the post-bounce value. Let A_(y,r)(z,t)=Gamma_(y,r,z,t)(T). Define R(x,p)=(x,-p) and lambda_r(x,p)=sqrt(eta) max(0,<p,grad V(x)-grad V(r)>). For every finite n≥0 and T≥0 there exists rho:Prefix(n,T)→Prefix(n,T), with (rho(t))_i=T-t_(n-1-i). This witness is produced, not assumed. For every y,r,z and t in Prefix(n,T), let A=Gamma(y,r,z,n,T,t)(T) be the actual terminal state. Define gamma(s)=Gamma(y,r,z,n,T,t)(min(max(s,0),T)) and barGamma(s)=Gamma(y,r,R(A),n,T,rho(t))(min(max(s,0),T)). Here Gamma is precisely the prescribed finite-recursion path defined above, including its right-continuous event convention. For every real s with 0≤s≤T and s different from every internal reversed event time (rho(t))_i, barGamma(s)=R(gamma(T-s)). Both real functions s→lambda_r(barGamma(s)) and s→lambda_r(R(gamma(s))) are interval integrable against real Lebesgue measure on [0,T]. Their integrals agree: integral_0^T lambda_r(barGamma(s)) ds = integral_0^T lambda_r(R(gamma(s))) ds. The state identity includes both endpoints 0,T; only the finite internal event set is excluded. It asserts no pointwise identity at genuine jumps or outside the closed horizon. The functions are defined on all real times by clamping solely to express interval integrability and integration. The conclusion includes n=0, T=0, rank-zero spaces, zero normals and zero rates; when T=0 and n>0 the strict event subtype is empty. The exact unnormalized simplex measure m is retained in the literal interface but unused in this deterministic path and scalar integral result. The only analytic premises are the original six assumptions. The reversed intermediate states, actual arc formula, flow group and momentum-conjugacy laws, and integrability of the actual reversed path rate are discharged using proved actual producers. This is the off-event trajectory and survival-substitution component of Appendix A.1. Weighted density matching, invariant probability, restart/Markovness, hypocoercivity, implementation error, actual expected costs, main results and PBPS/SPHMC composition remain separate.
Lean statement · actual_prescribed_path_reversal_and_survival
Let E be a finite-dimensional real inner-product space with its Borel sigma algebra, including dimension zero. Let V:E->R, alpha,beta>=0 and eta in R. Assume alpha>0, alpha<=beta, V is C2, alpha||v||^2<=D2V(x)[v,v]<=beta||v||^2 for every x,v in E, eta>0 and beta*eta<=1. For y,r in E put c=y-eta grad V(r), h_r(x)=grad V(x)-grad V(r), R(x,p)=(x,-p), Phi_(y,r,u)(x,p)=(c+cos(u)(x-c)+sqrt(eta)sin(u)p, -sin(u)/sqrt(eta)(x-c)+cos(u)p), S_r(x,p)=(x,p-(2<p,h_r(x)>/||h_r(x)||^2)h_r(x)). Real division by zero is zero, so a zero normal gives the identity bounce. Let ell=volume_E tensor volume_E, with canonical Hilbert-space Lebesgue measure. For every integer n>=0 and horizon T>=0, let Delta_n(T) consist of real tuples 0<t_0<...<t_(n-1)<T. Equivalently, prepending 0 produces a strictly increasing tuple and every entry is less than T. Let Prefix_n(T) be this subtype and m_n,T the comap of Lebesgue measure on R^n under its inclusion. This is unnormalized simplex volume. For n=0 the tuple is empty and its zero-dimensional volume is one; for T=0 and n>0 the subtype is empty. Write q_0=0 and q_(j+1)=t_j. Starting at z_0=z, define z_(j+1)=S_r(Phi_(y,r,t_j-q_j)(z_j)) for 0<=j<n. Define records K_j=(q_j,z_j), each embedded in the live branch of (R_nonnegative x (E x E)) plus a cemetery symbol. For a general history of n+1 such records, the path reconstruction Psi at s in [0,T] starts from z and visits records in increasing index order: a live record (a,w) replaces the accumulator by Phi_(y,r,s-a)(w) exactly when a<=s; future records and cemetery records leave it unchanged. Here s-a is nonnegative subtraction. Define Gamma_(y,r,z,t)=Psi(K), the actual finite prescribed path; thus its value at an event is the post-bounce value. Let A_(y,r)(z,t)=Gamma_(y,r,z,t)(T). Define R(x,p)=(x,-p) and lambda_r(x,p)=sqrt(eta) max(0,<p,grad V(x)-grad V(r)>). For every finite n>=0 and T>=0 there exists rho:Prefix(n,T)->Prefix(n,T), with (rho(t))_i=T-t_(n-1-i). This witness is produced, not assumed. For every y,r,z and t in Prefix(n,T), let A=Gamma(y,r,z,n,T,t)(T) be the actual terminal state. Define gamma(s)=Gamma(y,r,z,n,T,t)(min(max(s,0),T)) and barGamma(s)=Gamma(y,r,R(A),n,T,rho(t))(min(max(s,0),T)). Here Gamma is precisely the prescribed finite-recursion path defined above, including its right-continuous event convention. For every real s with 0<=s<=T and s different from every internal reversed event time (rho(t))_i, barGamma(s)=R(gamma(T-s)). Both real functions s->lambda_r(barGamma(s)) and s->lambda_r(R(gamma(s))) are interval integrable against real Lebesgue measure on [0,T]. Their integrals agree: integral_0^T lambda_r(barGamma(s)) ds = integral_0^T lambda_r(R(gamma(s))) ds. The state identity includes both endpoints 0,T; only the finite internal event set is excluded. It asserts no pointwise identity at genuine jumps or outside the closed horizon. The functions are defined on all real times by clamping solely to express interval integrability and integration. The conclusion includes n=0, T=0, rank-zero spaces, zero normals and zero rates; when T=0 and n>0 the strict event subtype is empty. The exact unnormalized simplex measure m is retained in the literal interface but unused in this deterministic path and scalar integral result. The only analytic premises are the original six assumptions. The reversed intermediate states, actual arc formula, flow group and momentum-conjugacy laws, and integrability of the actual reversed path rate are discharged using proved actual producers. This is the off-event trajectory and survival-substitution component of Appendix A.1. Weighted density matching, invariant probability, restart/Markovness, hypocoercivity, implementation error, actual expected costs, main results and PBPS/SPHMC composition remain separate.
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_prescribed_path_reversal_and_survival
{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_prescribed_path_reversal_statement hα hαβ hV hH hη hβηFull Lean proposition (definition) · actual_prescribed_path_reversal_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_prescribed_path_reversal_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 := by
classical
exact
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 Rec := (ℝ≥0 × (E × E)) ⊕ Unit
let Hist : ℕ → Type _ := fun n => Fin (n + 1) → Rec
let Δ : (n : ℕ) → ℝ≥0 → Set (Fin n → ℝ) := fun n T =>
{t | StrictMono (Fin.cons (0 : ℝ) t) ∧ ∀ i, t i < (T : ℝ)}
let Prefix : (n : ℕ) → ℝ≥0 → Type := fun n T => {t : Fin n → ℝ // t ∈ Δ n T}
let m : (n : ℕ) → (T : ℝ≥0) → Measure (Prefix n T) := fun n T =>
Measure.comap (fun t : Prefix n T => t.val) (volume : Measure (Fin n → ℝ))
let zAt : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) →
Prefix n T → Fin (n + 1) → (E × E) := fun y xRef z₀ n T t =>
Fin.induction z₀ (fun i z =>
S xRef (Φ y xRef (t.val i - (Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) i.castSucc) z))
let K : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) →
Prefix n T → Hist n := fun y xRef z₀ n T t j =>
Sum.inl (Real.toNNReal ((Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) j), zAt y xRef z₀ n T t j)
let Path : ℝ≥0 → Type _ := fun T => {s : ℝ≥0 // s ≤ T} → E × E
let Ψ : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) → Hist n → Path T :=
fun y xRef z₀ n T h s =>
Fin.foldl (n + 1) (fun z j => (h j).elim
(fun a => if a.1 ≤ s.val then Φ y xRef ((s.val - a.1 : ℝ≥0) : ℝ) a.2 else z)
(fun _ => z)) z₀
let Γ : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) → Prefix n T → Path T :=
fun y xRef z₀ n T t => Ψ y xRef z₀ n T (K y xRef z₀ n T t)
let R : E × E → E × E := fun z => (z.1, -z.2)
let rate : E → E × E → ℝ := fun r z =>
Real.sqrt η * max 0 (inner ℝ z.2 (gradient V z.1 - gradient V r))
∀ n : ℕ, ∀ T : ℝ≥0, ∃ rho : Prefix n T → Prefix n T,
(∀ t : Prefix n T, ∀ i : Fin n, (rho t).val i = (T : ℝ) - t.val i.rev) ∧
∀ y r : E, ∀ z : E × E, ∀ t : Prefix n T,
let A : E × E := Γ y r z n T t ⟨T, le_rfl⟩
let gamma : ℝ → E × E := fun s =>
Γ y r z n T t ⟨min (Real.toNNReal s) T, min_le_right _ _⟩
let barGamma : ℝ → E × E := fun s =>
Γ y r (R A) n T (rho t) ⟨min (Real.toNNReal s) T, min_le_right _ _⟩
(∀ s : ℝ, 0 ≤ s → s ≤ (T : ℝ) →
(∀ i : Fin n, s ≠ (rho t).val i) →
barGamma s = R (gamma ((T : ℝ) - s))) ∧
IntervalIntegrable (fun s => rate r (barGamma s)) volume 0 (T : ℝ) ∧
IntervalIntegrable (fun s => rate r (R (gamma s))) volume 0 (T : ℝ) ∧
(∫ s in (0 : ℝ)..(T : ℝ), rate r (barGamma s)) =
∫ s in (0 : ℝ)..(T : ℝ), rate r (R (gamma s))Proof roadmap
- 1Select the last active finite arc
The finite set of grid indices whose start is at most s contains index zero when s≥0. Its maximum j has a_j≤s, while every later grid start is strictly greater than s. This finite maximum gives an explicit active index without a continuity or regularity assumption.
- 2Reverse each open arc, including the horizon endpoints
For the selected reversed arc j, use the grid equations b_j=T-a_(n+1-j) and b_(j+1)=T-a_(n-j). If s is not an internal reversed event, T-s lies in original arc n-j; the first and last arcs handle s=0,T explicitly. The paired reversed post-state is R of the original next arrival. Momentum conjugacy R Phi_u R=Phi_(-u) and the flow group reduce the two remaining times to the same point. The identity need not hold at a genuine internal jump.
- 3Remove the finite exceptional set and reflect time
A finite subset of the real line has zero Lebesgue measure. Thus g(s)=f(T-s) almost everywhere on the integration interval. Transfer integrability from g to the reflected f, then apply the affine substitution u=T-s and reverse the endpoints to obtain integrability of f and equality of the integrals. The proof includes T=0 and requires no bounded-rate assumption.
- 4Obtain the actual states and match the two finite grids
Apply the actual finite-state reversal theorem to obtain one rho together with its coordinate equation and paired states. Use that same witness in both grids and the reversed trajectory. Prepending zero and appending T proves both reflected-grid equations, including the endpoint cases. Strict event ordering proves original-grid monotonicity.
- 5Identify the actual interpolated path on each active arc
The actual finite-count path law supplies the active-arc interpolation formula for the literal prescribed path. For 0≤s≤T, the clamp min(max(s,0),T) equals s. Consequently the original and reversed trajectories satisfy exactly the arc premises of the private path lemma, including both endpoints.
- 6Discharge reversal and survival premises with actual producers
The actual harmonic flow gives its group law; the phase-reversal theorem gives momentum involution and conjugacy. Apply the private arc lemma to the actual post-states and paths. The actual prescribed-density theorem gives interval integrability of the rate along the reversed actual path. Finally apply the finite-null-set substitution with f(s)=lambda_r(R gamma(s)) and g(s)=lambda_r(barGamma(s)). These are proved dependencies, never additional public hypotheses.
Full assumptions and notation
All objects and hypotheses
- Finite-dimensional real inner-product Borel E, including rank zero.
- alpha,beta≥0; alpha>0; alpha≤beta; V is C2; alpha||v||^2≤D2V(x)[v,v]≤beta||v||^2 for every x,v; eta>0; beta*eta≤1.
- Every finite n≥0 and T≥0; rho is produced on the strict event subtype; then every y,r,z,t is quantified. No positive rate or nonzero-normal assumption.
- Literal actual flow, reflection, finite state recursion and right-continuous interpolated path; no supplied reversal, arc or integrability hypothesis.
Mathematical proof
1. Select the last active finite arc
The finite set of grid indices whose start is at most s contains index zero when s≥0. Its maximum j has a_j≤s, while every later grid start is strictly greater than s. This finite maximum gives an explicit active index without a continuity or regularity assumption.
Corresponding Lean step
private theorem active_arc (n : ℕ) (a : Fin (n+1) → ℝ) (ha : a 0 = 0)
(s : ℝ) (hs : 0 ≤ s) :
∃ j, a j ≤ s ∧ ∀ k, j < k → s < a k := by
let q : Finset (Fin (n+1)) := Finset.univ.filter (fun j => a j ≤ s)
have hq : q.Nonempty := ⟨0, by simp [q, ha, hs]⟩
refine ⟨q.max' hq, (Finset.mem_filter.mp (Finset.max'_mem q hq)).2, ?_⟩
intro k hk
by_contra h
have hm : k ∈ q := by simp [q, le_of_not_gt h]
exact (not_le_of_gt hk) (Finset.le_max' q k hm)
Exact compiled region. Generic helper premises are internal and discharged by actual PBPS producers in the public proof.
2. Reverse each open arc, including the horizon endpoints
For the selected reversed arc j, use the grid equations b_j=T-a_(n+1-j) and b_(j+1)=T-a_(n-j). If s is not an internal reversed event, T-s lies in original arc n-j; the first and last arcs handle s=0,T explicitly. The paired reversed post-state is R of the original next arrival. Momentum conjugacy R Phi_u R=Phi_(-u) and the flow group reduce the two remaining times to the same point. The identity need not hold at a genuine internal jump.
Corresponding Lean step
private theorem path_reversal {X : Type*} (n : ℕ) (T : ℝ)
(a b : Fin (n+2) → ℝ) (ha : Monotone a)
(hb0 : b 0 = 0) (hbT : b (Fin.last (n+1)) = T)
(hbl : ∀ j : Fin (n+1), b j.castSucc = T - a j.rev.succ)
(hbr : ∀ j : Fin (n+1), b j.succ = T - a j.rev.castSucc)
(Φ : ℝ → X → X) (R : X → X) (hR : Function.Involutive R)
(hgroup : ∀ u v x, Φ (u+v) x = Φ u (Φ v x))
(hrev : ∀ u x, R (Φ u (R x)) = Φ (-u) x)
(post barPost : Fin (n+1) → X) (f g : ℝ → X)
(hstate : ∀ j, barPost j =
R (Φ (a j.rev.succ - a j.rev.castSucc) (post j.rev)))
(hf : ∀ s, 0 ≤ s → s ≤ T → ∀ j : Fin (n+1),
a j.castSucc ≤ s → (∀ k, j < k → s < a k.castSucc) →
f s = Φ (s-a j.castSucc) (post j))
(hg : ∀ s, 0 ≤ s → s ≤ T → ∀ j : Fin (n+1),
b j.castSucc ≤ s → (∀ k, j < k → s < b k.castSucc) →
g s = Φ (s-b j.castSucc) (barPost j)) :
∀ s, 0 ≤ s → s ≤ T → (∀ i : Fin n, s ≠ b i.succ.castSucc) →
g s = R (f (T-s)) := by
intro s hs0 hsT hne
obtain ⟨j, hj, hjafter⟩ := active_arc n (fun j => b j.castSucc) (by simpa using hb0) s hs0
have hnext : s ≤ b j.succ := by
induction j using Fin.lastCases with
| last => simpa only [Fin.succ_last, hbT] using hsT
| cast i =>
simpa only [Fin.succ_castSucc] using (hjafter i.succ Fin.castSucc_lt_succ).le
have hstart : a j.rev.castSucc ≤ T-s := by
rw [hbr] at hnext
linarith
have hafter : ∀ k : Fin (n+1), j.rev < k → T-s < a k.castSucc := by
intro k hk
have hstrict : b j.castSucc < s := by
induction j using Fin.cases with
| zero => simpa only [Fin.rev_zero, not_lt_of_ge (Fin.le_last k)] using hk
| succ i => exact lt_of_le_of_ne hj (hne i).symm
have hidx : j.rev.succ ≤ k.castSucc := by
exact_mod_cast hk
have ham := ha hidx
rw [hbl] at hstrict
linarith
have hRR (x : X) : R (R x) = x := hR x
have hc (u : ℝ) (x : X) : Φ u (R x) = R (Φ (-u) x) := by
simpa only [hRR] using congrArg R (hrev u x)
rw [hg s hs0 hsT j hj hjafter,
hf (T-s) (sub_nonneg.mpr hsT) (by linarith) j.rev hstart hafter,
hstate, hc, ← hgroup]
congr 2
rw [hbl]
ring
Exact compiled region. Generic helper premises are internal and discharged by actual PBPS producers in the public proof.
3. Remove the finite exceptional set and reflect time
A finite subset of the real line has zero Lebesgue measure. Thus g(s)=f(T-s) almost everywhere on the integration interval. Transfer integrability from g to the reflected f, then apply the affine substitution u=T-s and reverse the endpoints to obtain integrability of f and equality of the integrals. The proof includes T=0 and requires no bounded-rate assumption.
Corresponding Lean step
private theorem scalar_reflection (T : ℝ) (hT : 0 ≤ T) (f g : ℝ → ℝ)
(N : Set ℝ) (hN : N.Finite)
(he : ∀ s ∈ Icc 0 T, s ∉ N → g s = f (T-s))
(hg : IntervalIntegrable g volume 0 T) :
IntervalIntegrable f volume 0 T ∧
(∫ s in (0 : ℝ)..T, g s) = ∫ s in (0 : ℝ)..T, f s := by
have hae : g =ᵐ[volume.restrict (Ι (0 : ℝ) T)] (fun s => f (T-s)) := by
filter_upwards [ae_restrict_mem measurableSet_uIoc,
hN.countable.ae_notMem (volume.restrict (Ι (0 : ℝ) T))] with s hs hn
rw [uIoc_of_le hT] at hs
exact he s ⟨hs.1.le, hs.2⟩ hn
have hi : IntervalIntegrable (fun s => f (T-s)) volume 0 T := hg.congr_ae hae
have hf : IntervalIntegrable f volume 0 T := by
simpa using (hi.comp_sub_left T).symm
refine ⟨hf, ?_⟩
rw [intervalIntegral.integral_congr_ae_restrict hae]
simpa using intervalIntegral.integral_comp_sub_left f T (a := (0 : ℝ)) (b := T)
Exact compiled region. Generic helper premises are internal and discharged by actual PBPS producers in the public proof.
4. Obtain the actual states and match the two finite grids
Apply the actual finite-state reversal theorem to obtain one rho together with its coordinate equation and paired states. Use that same witness in both grids and the reversed trajectory. Prepending zero and appending T proves both reflected-grid equations, including the endpoint cases. Strict event ordering proves original-grid monotonicity.
Corresponding Lean step
theorem actual_prescribed_path_reversal_and_survival
{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_prescribed_path_reversal_statement hα hαβ hV hH hη hβη := by
classical
unfold actual_prescribed_path_reversal_statement
intro c Φ S Rec Hist Δ Prefix m zAt K Path Ψ Γ R rate n T
obtain ⟨rho, hrho, h99⟩ :=
AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPrescribedStateReversal.actual_prescribed_state_reversal_and_rate_product
hα hαβ hV hH hη hβη n T
refine ⟨rho, hrho, ?_⟩
intro y r z t A gamma barGamma
let grid : Fin (n+2) → ℝ := Fin.snoc (Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n+1) → ℝ) (T : ℝ)
let barGrid : Fin (n+2) → ℝ := Fin.snoc (Fin.cons (0 : ℝ) (rho t).val) (T : ℝ)
let post := zAt y r z n T t
let barPost := zAt y r (R A) n T (rho t)
have hpair : ∀ j : Fin (n+1), barPost j =
R (Φ y r (grid j.rev.succ-grid j.rev.castSucc) (post j.rev)) :=
fun j => ((h99 y r z t).1 j).1
have hbl (j : Fin (n+1)) : barGrid j.castSucc = (T : ℝ) - grid j.rev.succ := by
induction j using Fin.cases with
| zero => simp [grid, barGrid]
| succ i => simp only [grid, barGrid, Fin.rev_succ, Fin.succ_castSucc,
Fin.snoc_castSucc, Fin.cons_succ, hrho]
have hbr (j : Fin (n+1)) : barGrid j.succ = (T : ℝ) - grid j.rev.castSucc := by
induction j using Fin.lastCases with
| last => simp [grid, barGrid]
| cast i => simp only [grid, barGrid, Fin.rev_castSucc, Fin.succ_castSucc,
Fin.snoc_castSucc, Fin.cons_succ, hrho]
have hgrid : Monotone grid := by
have htT : ∀ j : Fin (n+1), (Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n+1) → ℝ) j ≤ (T : ℝ) := by
intro j
refine Fin.cases ?_ (fun i => ?_) j
· simpa using T.coe_nonneg
· exact (t.property.2 i).le
intro i j hij
induction i using Fin.lastCases with
| last =>
have hj : j = Fin.last (n+1) := le_antisymm (Fin.le_last j) hij
subst j
exact le_rfl
| cast i =>
induction j using Fin.lastCases with
| last => simpa [grid] using htT i
| cast j => simpa [grid] using t.property.1.monotone (show i ≤ j from hij)
Exact compiled region. Generic helper premises are internal and discharged by actual PBPS producers in the public proof.
5. Identify the actual interpolated path on each active arc
The actual finite-count path law supplies the active-arc interpolation formula for the literal prescribed path. For 0≤s≤T, the clamp min(max(s,0),T) equals s. Consequently the original and reversed trajectories satisfy exactly the arc premises of the private path lemma, including both endpoints.
Corresponding Lean step
obtain ⟨Z, _, _, _, _, hlaw⟩ :=
AutoSamplingTheory.ExampleCases.ProximalBPS.ActualFiniteCountPath.actual_finite_count_path_law
hα hαβ hV hH hη hβη
have harc (w : E × E) (u : Prefix n T) (s : ℝ) (hs0 : 0 ≤ s) (hsT : s ≤ (T : ℝ))
(j : Fin (n+1)) (hj : (Fin.cons (0 : ℝ) (u.val : Fin n → ℝ) : Fin (n+1) → ℝ) j ≤ s)
(hn : ∀ k : Fin (n+1), j < k → s < (Fin.cons (0 : ℝ) (u.val : Fin n → ℝ) : Fin (n+1) → ℝ) k) :
Γ y r w n T u ⟨min (Real.toNNReal s) T, min_le_right _ _⟩ =
Φ y r (s - (Fin.cons (0 : ℝ) (u.val : Fin n → ℝ) : Fin (n+1) → ℝ) j) (zAt y r w n T u j) := by
have hclip : min (Real.toNNReal s) T = Real.toNNReal s :=
min_eq_left (by exact_mod_cast (Real.toNNReal_le_iff_le_coe).2 hsT)
have hcoe : ((min (Real.toNNReal s) T : ℝ≥0) : ℝ) = s := by
rw [hclip, Real.coe_toNNReal s hs0]
have hp := ((hlaw n T).2.2.2 y r w).2.2.2.2.1
u ⟨min (Real.toNNReal s) T, min_le_right _ _⟩ j
(by simpa only [hcoe] using hj) (by simpa only [hcoe] using hn)
change Γ y r w n T u ⟨min (Real.toNNReal s) T, min_le_right _ _⟩ =
Φ y r (((min (Real.toNNReal s) T : ℝ≥0) : ℝ) - (Fin.cons (0 : ℝ) (u.val : Fin n → ℝ) : Fin (n+1) → ℝ) j)
(zAt y r w n T u j) at hp
simpa only [hcoe] using hp
Exact compiled region. Generic helper premises are internal and discharged by actual PBPS producers in the public proof.
6. Discharge reversal and survival premises with actual producers
The actual harmonic flow gives its group law; the phase-reversal theorem gives momentum involution and conjugacy. Apply the private arc lemma to the actual post-states and paths. The actual prescribed-density theorem gives interval integrability of the rate along the reversed actual path. Finally apply the finite-null-set substitution with f(s)=lambda_r(R gamma(s)) and g(s)=lambda_r(barGamma(s)). These are proved dependencies, never additional public hypotheses.
Corresponding Lean step
obtain ⟨_, _, _, hgroup, _⟩ :=
AutoSamplingTheory.ExampleCases.ProximalBPS.ActualHarmonicFlow.actual_harmonic_flow_laws
hα hαβ hV hH hη hβη
obtain ⟨_, _, _, _, _, _, _, _, hR, hrev, _⟩ :=
AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPhaseReversalVolume.actual_phase_reversal_volume_laws
hα hαβ hV hH hη hβη
have hoff : ∀ s : ℝ, 0 ≤ s → s ≤ (T : ℝ) →
(∀ i : Fin n, s ≠ (rho t).val i) → barGamma s = R (gamma ((T : ℝ)-s)) := by
have hp := path_reversal n (T : ℝ) grid barGrid hgrid
(by simp [barGrid]) (by simp [barGrid]) hbl hbr (Φ y r) R hR
(hgroup y r) (hrev y r) post barPost gamma barGamma hpair
(fun s hs0 hsT j hj hn => by
simpa only [gamma, grid, post, Fin.snoc_castSucc] using
harc z t s hs0 hsT j (by simpa only [grid, Fin.snoc_castSucc] using hj)
(by simpa only [grid, Fin.snoc_castSucc] using hn))
(fun s hs0 hsT j hj hn => by
simpa only [barGamma, barGrid, barPost, Fin.snoc_castSucc] using
harc (R A) (rho t) s hs0 hsT j (by simpa only [barGrid, Fin.snoc_castSucc] using hj)
(by simpa only [barGrid, Fin.snoc_castSucc] using hn))
intro s hs0 hsT hn
exact hp s hs0 hsT (by simpa only [barGrid, Fin.snoc_castSucc, Fin.cons_succ] using hn)
have hi : IntervalIntegrable (fun s => rate r (barGamma s)) volume 0 (T : ℝ) :=
(AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPrescribedPathDensity.actual_prescribed_path_density_rewrite
hα hαβ hV hH hη hβη y r (R A) n T (rho t)).1
have hs := scalar_reflection (T : ℝ) T.coe_nonneg
(fun s => rate r (R (gamma s))) (fun s => rate r (barGamma s))
(Set.range (rho t).val) (Set.finite_range _) (by
intro s hs hn
exact congrArg (rate r) (hoff s hs.1 hs.2 (fun i he => hn ⟨i, he.symm⟩))) hi
exact ⟨hoff, hi, hs⟩
Exact compiled region. Generic helper premises are internal and discharged by actual PBPS producers in the public proof.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · actual_prescribed_path_reversal_and_survival
Select the last active finite arc; Reverse each open arc, including the horizon endpoints; Remove the finite exceptional set and reflect time; Obtain the actual states and match the two finite grids; Identify the actual interpolated path on each active arc; Discharge reversal and survival premises with actual producers
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_prescribed_path_reversal_and_survival
{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_prescribed_path_reversal_statement hα hαβ hV hH hη hβη := by
classical
unfold actual_prescribed_path_reversal_statement
intro c Φ S Rec Hist Δ Prefix m zAt K Path Ψ Γ R rate n T
obtain ⟨rho, hrho, h99⟩ :=
AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPrescribedStateReversal.actual_prescribed_state_reversal_and_rate_product
hα hαβ hV hH hη hβη n T
refine ⟨rho, hrho, ?_⟩
intro y r z t A gamma barGamma
let grid : Fin (n+2) → ℝ := Fin.snoc (Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n+1) → ℝ) (T : ℝ)
let barGrid : Fin (n+2) → ℝ := Fin.snoc (Fin.cons (0 : ℝ) (rho t).val) (T : ℝ)
let post := zAt y r z n T t
let barPost := zAt y r (R A) n T (rho t)
have hpair : ∀ j : Fin (n+1), barPost j =
R (Φ y r (grid j.rev.succ-grid j.rev.castSucc) (post j.rev)) :=
fun j => ((h99 y r z t).1 j).1
have hbl (j : Fin (n+1)) : barGrid j.castSucc = (T : ℝ) - grid j.rev.succ := by
induction j using Fin.cases with
| zero => simp [grid, barGrid]
| succ i => simp only [grid, barGrid, Fin.rev_succ, Fin.succ_castSucc,
Fin.snoc_castSucc, Fin.cons_succ, hrho]
have hbr (j : Fin (n+1)) : barGrid j.succ = (T : ℝ) - grid j.rev.castSucc := by
induction j using Fin.lastCases with
| last => simp [grid, barGrid]
| cast i => simp only [grid, barGrid, Fin.rev_castSucc, Fin.succ_castSucc,
Fin.snoc_castSucc, Fin.cons_succ, hrho]
have hgrid : Monotone grid := by
have htT : ∀ j : Fin (n+1), (Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n+1) → ℝ) j ≤ (T : ℝ) := by
intro j
refine Fin.cases ?_ (fun i => ?_) j
· simpa using T.coe_nonneg
· exact (t.property.2 i).le
intro i j hij
induction i using Fin.lastCases with
| last =>
have hj : j = Fin.last (n+1) := le_antisymm (Fin.le_last j) hij
subst j
exact le_rfl
| cast i =>
induction j using Fin.lastCases with
| last => simpa [grid] using htT i
| cast j => simpa [grid] using t.property.1.monotone (show i ≤ j from hij)
obtain ⟨Z, _, _, _, _, hlaw⟩ :=
AutoSamplingTheory.ExampleCases.ProximalBPS.ActualFiniteCountPath.actual_finite_count_path_law
hα hαβ hV hH hη hβη
have harc (w : E × E) (u : Prefix n T) (s : ℝ) (hs0 : 0 ≤ s) (hsT : s ≤ (T : ℝ))
(j : Fin (n+1)) (hj : (Fin.cons (0 : ℝ) (u.val : Fin n → ℝ) : Fin (n+1) → ℝ) j ≤ s)
(hn : ∀ k : Fin (n+1), j < k → s < (Fin.cons (0 : ℝ) (u.val : Fin n → ℝ) : Fin (n+1) → ℝ) k) :
Γ y r w n T u ⟨min (Real.toNNReal s) T, min_le_right _ _⟩ =
Φ y r (s - (Fin.cons (0 : ℝ) (u.val : Fin n → ℝ) : Fin (n+1) → ℝ) j) (zAt y r w n T u j) := by
have hclip : min (Real.toNNReal s) T = Real.toNNReal s :=
min_eq_left (by exact_mod_cast (Real.toNNReal_le_iff_le_coe).2 hsT)
have hcoe : ((min (Real.toNNReal s) T : ℝ≥0) : ℝ) = s := by
rw [hclip, Real.coe_toNNReal s hs0]
have hp := ((hlaw n T).2.2.2 y r w).2.2.2.2.1
u ⟨min (Real.toNNReal s) T, min_le_right _ _⟩ j
(by simpa only [hcoe] using hj) (by simpa only [hcoe] using hn)
change Γ y r w n T u ⟨min (Real.toNNReal s) T, min_le_right _ _⟩ =
Φ y r (((min (Real.toNNReal s) T : ℝ≥0) : ℝ) - (Fin.cons (0 : ℝ) (u.val : Fin n → ℝ) : Fin (n+1) → ℝ) j)
(zAt y r w n T u j) at hp
simpa only [hcoe] using hp
obtain ⟨_, _, _, hgroup, _⟩ :=
AutoSamplingTheory.ExampleCases.ProximalBPS.ActualHarmonicFlow.actual_harmonic_flow_laws
hα hαβ hV hH hη hβη
obtain ⟨_, _, _, _, _, _, _, _, hR, hrev, _⟩ :=
AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPhaseReversalVolume.actual_phase_reversal_volume_laws
hα hαβ hV hH hη hβη
have hoff : ∀ s : ℝ, 0 ≤ s → s ≤ (T : ℝ) →
(∀ i : Fin n, s ≠ (rho t).val i) → barGamma s = R (gamma ((T : ℝ)-s)) := by
have hp := path_reversal n (T : ℝ) grid barGrid hgrid
(by simp [barGrid]) (by simp [barGrid]) hbl hbr (Φ y r) R hR
(hgroup y r) (hrev y r) post barPost gamma barGamma hpair
(fun s hs0 hsT j hj hn => by
simpa only [gamma, grid, post, Fin.snoc_castSucc] using
harc z t s hs0 hsT j (by simpa only [grid, Fin.snoc_castSucc] using hj)
(by simpa only [grid, Fin.snoc_castSucc] using hn))
(fun s hs0 hsT j hj hn => by
simpa only [barGamma, barGrid, barPost, Fin.snoc_castSucc] using
harc (R A) (rho t) s hs0 hsT j (by simpa only [barGrid, Fin.snoc_castSucc] using hj)
(by simpa only [barGrid, Fin.snoc_castSucc] using hn))
intro s hs0 hsT hn
exact hp s hs0 hsT (by simpa only [barGrid, Fin.snoc_castSucc, Fin.cons_succ] using hn)
have hi : IntervalIntegrable (fun s => rate r (barGamma s)) volume 0 (T : ℝ) :=
(AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPrescribedPathDensity.actual_prescribed_path_density_rewrite
hα hαβ hV hH hη hβη y r (R A) n T (rho t)).1
have hs := scalar_reflection (T : ℝ) T.coe_nonneg
(fun s => rate r (R (gamma s))) (fun s => rate r (barGamma s))
(Set.range (rho t).val) (Set.finite_range _) (by
intro s hs hn
exact congrArg (rate r) (hoff s hs.1 hs.2 (fun i he => hn ⟨i, he.symm⟩))) hi
exact ⟨hoff, hi, hs⟩
#print axioms actual_prescribed_path_reversal_and_survival
end
end AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPrescribedPathReversalScope and omitted-condition boundaries
- No all-time equality at genuine jumps or outside closed horizon; no weighted density/sector, invariant probability, restart/Markovness, hypocoercivity, implementation error, expected cost, main theorem or composition.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPrescribedStateReversal.actual_prescribed_state_reversal_and_rate_productAutoSamplingTheory.ExampleCases.ProximalBPS.ActualFiniteCountPath.actual_finite_count_path_lawAutoSamplingTheory.ExampleCases.ProximalBPS.ActualPhaseReversalVolume.actual_phase_reversal_volume_lawsAutoSamplingTheory.ExampleCases.ProximalBPS.ActualHarmonicFlow.actual_harmonic_flow_lawsAutoSamplingTheory.ExampleCases.ProximalBPS.ActualPrescribedPathDensity.actual_prescribed_path_density_rewrite
Mathlib API called (external library)
- Finset.max'
- Fin.lastCases
- Fin.snoc_castSucc
- Fin.cons_succ
- Set.Countable.ae_notMem
- IntervalIntegrable.congr_ae
- IntervalIntegrable.comp_sub_left
- intervalIntegral.integral_congr_ae_restrict
- intervalIntegral.integral_comp_sub_left
Mathematical sources
- Appendix A.1 actual prescribed trajectories and A8 off-event reversal, survival integral matching — No all-time equality at genuine jumps or outside closed horizon; no weighted density/sector, invariant probability, restart/Markovness, hypocoercivity, implementation error, expected cost, main theorem or composition.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.