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

Actual normalized PBPS countable endpoint law

Chen, Chewi, Lu and Zhang, arXiv:2609.06905v1, Appendix A.1 A7 and Gibbs averaging before A8, with Eq3.1 normalization. Complete attributed mathematical restatement of the selected measure-assembly step. Joint measurable representatives and explicit measure identities are ASTIS completion; this is not a verbatim standalone theorem quotation.

arXiv2609.06905v1 · Appendix A.1 A7, initial Gibbs averaging and nonnegative Tonelli before A8: actual normalized countable endpoint-pair law assembly and reversal. · faithful paraphrase

Complete source statement (Samplinglib restatement)

Let E be any finite-dimensional real inner-product Borel space, including dimension zero. Let V:E→ℝ be C², α,β≥0 and η∈ℝ with α>0, α≤β, α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for every x,v∈E, η>0 and βη≤1. The following literal constructions are made for all y,r∈E and initial phases z₀∈E×E; the existential process witness below is global in these parameters. Put c=y−η∇V(r), Φ_t(x,p)=(c+cos(t)(x−c)+√η sin(t)p, −sin(t)(x−c)/√η+cos(t)p), g_r(x)=∇V(x)−∇V(r), S_r(x,p)=(x,p−2〈p,g_r(x)〉g_r(x)/‖g_r(x)‖²), λ_r(x,p)=√η max{0,〈p,g_r(x)〉}, Λ_z(t)=∫₀ᵗλ_r(Φ_s(z))ds and τ_z(e)=inf{t≥0:Λ_z(t)≥e}∈[0,∞], with inf empty=∞. Total real division makes S_r the identity at g_r(x)=0. The record space is D=([0,∞)×(E×E))⊕{stopped}, with Borel sum structure. Define next(e,stopped)=stopped; for a live record (T,z), next(e,(T,z))=stopped if τ_z(e)=∞, and otherwise next(e,(T,z))=(T+τ_z(e),S_rΦ_(τ_z(e))(z)). In the Lean definition untopD0 is used only in this non-top branch. Define R₀(e)=live(0,z₀) and R_(j+1)(e)=next(e_j,R_j(e)). Let Ω=ℝ^ℕ with its product Borel structure and P=⊗_(k≥0)Exp(1). Let ε(w)_k=max{w_k,0}; this is an ambient coordinate extension on a P-null nonpositive-clock set, not new source dynamics for negative clocks. Write T_j(w)=a for a live record R_j(ε(w))=live(a,z), and T_j(w)=∞ for a stopped record. Define I_n(T)={T_n≤T<T_(n+1)}, and the total selector N(T,w)=min{n:w∈I_n(T)} when such an n exists, and 0 otherwise. For n≥0 let Hist_n=D^(Fin(n+1)) and H_n(w)_j=R_j(ε(w)). Write readTime(live(a,z))=a and readTime(stopped)=0. The abstract guard A_n(T) consists of histories all of whose records are live, whose read times are strictly increasing and whose positive-index read times are strictly below T; it does not constrain record0 itself. Actual H_n starts at live(0,z₀). For h∈Hist_n set d_n(T,h)=max{T−readTime(h_n),0}. Define survival(live(a,z),u,e) to mean u<τ_z(max{e,0}); on stopped it is false. Define W(live(a,z),u)=exp(−Λ_z(u)); on stopped W=0. Put C_n(T)={w:H_n(w)∈A_n(T), survival(R_n(ε(w)),d_n(T,H_n(w)),w_n)}. For a fixed finite T≥0 let Path_T be all functions from [0,T] into E×E, with its coordinate-product sigma algebra. On every history, including unrealizable ones, define Ψ_n(T,h)(s) by starting at z₀ and visiting j=0,…,n in increasing order: a live record (a,z) with a≤s replaces the current value by Φ_(s−a)(z), and an ineligible live or stopped record leaves it unchanged. All elapsed times in this total definition use nonnegative subtraction. Define Δ_n(T)={t∈ℝ^n:0<t₁<⋯<t_n<T}, and let m_n be the comap of product Lebesgue measure to this subtype, without normalization. For t∈Δ_n(T), put s₀=0,s_i=t_i, z₀ equal to the prescribed initial phase and z_i=S_rΦ_(s_i−s_(i−1))(z_(i−1)). Set K_n(t)_j=live(s_j,z_j), Γ_n(T,t)=Ψ_n(T,K_n(t)), q_n(t)=ofReal(∏_(i=1)^n λ_r(Φ_(s_i−s_(i−1))(z_(i−1)))exp[−Λ_(z_(i−1))(s_i−s_(i−1))]), and ρ_n(T,t)=q_n(t)W(K_n(t)_n,d_n(T,K_n(t))). The literal toNNReal conversions agree with these nonnegative simplex times. There exists one actual phase representative Z(y,r,z₀,t,w), jointly Borel in all deterministic parameters, finite time and raw input, with the following properties. On every raw covering interval T_n(w)≤s<T_(n+1)(w), if R_n(ε(w))=live(a,z), then Z(s,w)=Φ_(s−a)(z). If no interval covers s, Z(s,w)=z₀. For each fixed parameter tuple, Z(0,w)=z₀ almost surely. Put R(x,p)=(x,-p), V_y(x)=V(x)+||x-y||^2/(2 eta), and nu_y=(volume_E.tilted(-V_y)) times stdGaussian(E), in position/momentum order. Here tilted(-V_y) has density ofReal(exp(-V_y(x))/integral exp(-V_y) dx), and stdGaussian is the centered identity-covariance Gaussian. Normalizability is a consequence, not a premise. For the same single actual Z described above, every y,r in E and every finite T>=0, define for each n in Nat the map B_n(z,t)=(z,Gamma_(y,r,z,n,T,t)(T)), the measure sigma_n=(nu_y times m_n,T).withDensity((z,t)->rho_(y,r,z,n,T)(t)), and L_n=map B_n sigma_n on (E times E) times (E times E). Define M_Z(z,w)=(z,Z(y,r,z,T,w)), Q=map M_Z (nu_y times P), and J(z0,zT)=(R(zT),R(z0)). Every product uses initial phase first, and Q is the actual endpoint-pair law of the specified clock process. Then simultaneously Q=Measure.sum(n in Nat -> L_n), Q is a probability measure, and J is measurable with map J Q=Q. The sum includes every nonnegative integer without a cap. There is no assumption that a fixed-count sector has mass one. Joint measurability, simplex sigma-finiteness, measurable initial-phase sector integrals, countable exchange, and probability of the input measures are internal dependencies, not supplied hypotheses. In particular no joint-in-initial-state measurability of N is assumed: the count partition is taken at each fixed initial state before nonnegative integration against nu_y. The conclusion includes n=0 in the sum, T=0, dimension zero, zero rates and infinite waits with the explicit raw exceptional fallback above. At T=0 the actual initialization is almost sure; no pointwise all-clock initialization or jumpwise reversed-path equality is added. Arbitrary nonnegative measurable test functions may have infinite integrals during assembly. Signed bilinear duality, marginal phase invariance, restart/Markovness, hypocoercivity, implementation error, unbounded expected oracle cost and complete paper/composition results remain separate obligations.

  • Finite-dimensional real inner-product Borel E with canonical volume, 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.
  • The actual global process is existentially constructed, with joint measurability, literal arc/fallback characterization and almost-sure initialization. Every y,r and finite nonnegative T is included, and all n in Nat are summed.
  • All harmonic flow, totalized reflection, exponential clocks, strict simplex, actual event density, conditional Gibbs initial phase and endpoint measures are the displayed definitions. No supplied process, normalizer, integrability, joint count-measurability, cap or finite-sector-probability premise.

Actual countable law

\[\int F\,dQ=\int\sum_nD_n\,d\nu_y=\sum_n\int D_n\,d\nu_y=\sum_n\int F\,dL_n=\int F\,d\!\left(\sum_nL_n\right).\]

Endpoint-pair reversal

\[J_*Q=J_*\!\left(\sum_n L_n\right)=\sum_nJ_*L_n=\sum_nL_n=Q.\]

Read the formalized proofs

Each statement and proof below has its own closed Lean disclosure. Samplinglib parents, Mathlib calls and external mathematical sources are distinguished in each proof.

Samplinglib mathematical lesson

Actual normalized PBPS countable endpoint law

AutoSamplingTheory.ExampleCases.ProximalBPS.ActualCountableEndpointLaw.actual_countable_endpoint_law · theorem · Teaching coverage

Read this first

Mathematical statement

Let E be any finite-dimensional real inner-product Borel space, including dimension zero. Let V:E→ℝ be C², α,β≥0 and η∈ℝ with α>0, α≤β, α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for every x,v∈E, η>0 and βη≤1. The following literal constructions are made for all y,r∈E and initial phases z₀∈E×E; the existential process witness below is global in these parameters. Put c=y−η∇V(r), Φ_t(x,p)=(c+cos(t)(x−c)+√η sin(t)p, −sin(t)(x−c)/√η+cos(t)p), g_r(x)=∇V(x)−∇V(r), S_r(x,p)=(x,p−2〈p,g_r(x)〉g_r(x)/‖g_r(x)‖²), λ_r(x,p)=√η max{0,〈p,g_r(x)〉}, Λ_z(t)=∫₀ᵗλ_r(Φ_s(z))ds and τ_z(e)=inf{t≥0:Λ_z(t)≥e}∈[0,∞], with inf empty=∞. Total real division makes S_r the identity at g_r(x)=0. The record space is D=([0,∞)×(E×E))⊕{stopped}, with Borel sum structure. Define next(e,stopped)=stopped; for a live record (T,z), next(e,(T,z))=stopped if τ_z(e)=∞, and otherwise next(e,(T,z))=(T+τ_z(e),S_rΦ_(τ_z(e))(z)). In the Lean definition untopD0 is used only in this non-top branch. Define R₀(e)=live(0,z₀) and R_(j+1)(e)=next(e_j,R_j(e)). Let Ω=ℝ^ℕ with its product Borel structure and P=⊗_(k≥0)Exp(1). Let ε(w)_k=max{w_k,0}; this is an ambient coordinate extension on a P-null nonpositive-clock set, not new source dynamics for negative clocks. Write T_j(w)=a for a live record R_j(ε(w))=live(a,z), and T_j(w)=∞ for a stopped record. Define I_n(T)={T_n≤T<T_(n+1)}, and the total selector N(T,w)=min{n:w∈I_n(T)} when such an n exists, and 0 otherwise. For n≥0 let Hist_n=D^(Fin(n+1)) and H_n(w)_j=R_j(ε(w)). Write readTime(live(a,z))=a and readTime(stopped)=0. The abstract guard A_n(T) consists of histories all of whose records are live, whose read times are strictly increasing and whose positive-index read times are strictly below T; it does not constrain record0 itself. Actual H_n starts at live(0,z₀). For h∈Hist_n set d_n(T,h)=max{T−readTime(h_n),0}. Define survival(live(a,z),u,e) to mean u<τ_z(max{e,0}); on stopped it is false. Define W(live(a,z),u)=exp(−Λ_z(u)); on stopped W=0. Put C_n(T)={w:H_n(w)∈A_n(T), survival(R_n(ε(w)),d_n(T,H_n(w)),w_n)}. For a fixed finite T≥0 let Path_T be all functions from [0,T] into E×E, with its coordinate-product sigma algebra. On every history, including unrealizable ones, define Ψ_n(T,h)(s) by starting at z₀ and visiting j=0,…,n in increasing order: a live record (a,z) with a≤s replaces the current value by Φ_(s−a)(z), and an ineligible live or stopped record leaves it unchanged. All elapsed times in this total definition use nonnegative subtraction. Define Δ_n(T)={t∈ℝ^n:0<t₁<⋯<t_n<T}, and let m_n be the comap of product Lebesgue measure to this subtype, without normalization. For t∈Δ_n(T), put s₀=0,s_i=t_i, z₀ equal to the prescribed initial phase and z_i=S_rΦ_(s_i−s_(i−1))(z_(i−1)). Set K_n(t)_j=live(s_j,z_j), Γ_n(T,t)=Ψ_n(T,K_n(t)), q_n(t)=ofReal(∏_(i=1)^n λ_r(Φ_(s_i−s_(i−1))(z_(i−1)))exp[−Λ_(z_(i−1))(s_i−s_(i−1))]), and ρ_n(T,t)=q_n(t)W(K_n(t)_n,d_n(T,K_n(t))). The literal toNNReal conversions agree with these nonnegative simplex times. There exists one actual phase representative Z(y,r,z₀,t,w), jointly Borel in all deterministic parameters, finite time and raw input, with the following properties. On every raw covering interval T_n(w)≤s<T_(n+1)(w), if R_n(ε(w))=live(a,z), then Z(s,w)=Φ_(s−a)(z). If no interval covers s, Z(s,w)=z₀. For each fixed parameter tuple, Z(0,w)=z₀ almost surely. Put R(x,p)=(x,-p), V_y(x)=V(x)+||x-y||^2/(2 eta), and nu_y=(volume_E.tilted(-V_y)) times stdGaussian(E), in position/momentum order. Here tilted(-V_y) has density ofReal(exp(-V_y(x))/integral exp(-V_y) dx), and stdGaussian is the centered identity-covariance Gaussian. Normalizability is a consequence, not a premise. For the same single actual Z described above, every y,r in E and every finite T≥0, define for each n in Nat the map B_n(z,t)=(z,Gamma_(y,r,z,n,T,t)(T)), the measure sigma_n=(nu_y times m_n,T).withDensity((z,t)→rho_(y,r,z,n,T)(t)), and L_n=map B_n sigma_n on (E times E) times (E times E). Define M_Z(z,w)=(z,Z(y,r,z,T,w)), Q=map M_Z (nu_y times P), and J(z0,zT)=(R(zT),R(z0)). Every product uses initial phase first, and Q is the actual endpoint-pair law of the specified clock process. Then simultaneously Q=Measure.sum(n in Nat → L_n), Q is a probability measure, and J is measurable with map J Q=Q. The sum includes every nonnegative integer without a cap. There is no assumption that a fixed-count sector has mass one. Joint measurability, simplex sigma-finiteness, measurable initial-phase sector integrals, countable exchange, and probability of the input measures are internal dependencies, not supplied hypotheses. In particular no joint-in-initial-state measurability of N is assumed: the count partition is taken at each fixed initial state before nonnegative integration against nu_y. The conclusion includes n=0 in the sum, T=0, dimension zero, zero rates and infinite waits with the explicit raw exceptional fallback above. At T=0 the actual initialization is almost sure; no pointwise all-clock initialization or jumpwise reversed-path equality is added. Arbitrary nonnegative measurable test functions may have infinite integrals during assembly. Signed bilinear duality, marginal phase invariance, restart/Markovness, hypocoercivity, implementation error, unbounded expected oracle cost and complete paper/composition results remain separate obligations.

\[J_*Q=J_*\!\left(\sum_n L_n\right)=\sum_nJ_*L_n=\sum_nL_n=Q.\]
Lean statement · actual_countable_endpoint_law

Let E be any finite-dimensional real inner-product Borel space, including dimension zero. Let V:E→ℝ be C², α,β≥0 and η∈ℝ with α>0, α≤β, α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for every x,v∈E, η>0 and βη≤1. The following literal constructions are made for all y,r∈E and initial phases z₀∈E×E; the existential process witness below is global in these parameters. Put c=y−η∇V(r), Φ_t(x,p)=(c+cos(t)(x−c)+√η sin(t)p, −sin(t)(x−c)/√η+cos(t)p), g_r(x)=∇V(x)−∇V(r), S_r(x,p)=(x,p−2〈p,g_r(x)〉g_r(x)/‖g_r(x)‖²), λ_r(x,p)=√η max{0,〈p,g_r(x)〉}, Λ_z(t)=∫₀ᵗλ_r(Φ_s(z))ds and τ_z(e)=inf{t≥0:Λ_z(t)≥e}∈[0,∞], with inf empty=∞. Total real division makes S_r the identity at g_r(x)=0. The record space is D=([0,∞)×(E×E))⊕{stopped}, with Borel sum structure. Define next(e,stopped)=stopped; for a live record (T,z), next(e,(T,z))=stopped if τ_z(e)=∞, and otherwise next(e,(T,z))=(T+τ_z(e),S_rΦ_(τ_z(e))(z)). In the Lean definition untopD0 is used only in this non-top branch. Define R₀(e)=live(0,z₀) and R_(j+1)(e)=next(e_j,R_j(e)). Let Ω=ℝ^ℕ with its product Borel structure and P=⊗_(k≥0)Exp(1). Let ε(w)_k=max{w_k,0}; this is an ambient coordinate extension on a P-null nonpositive-clock set, not new source dynamics for negative clocks. Write T_j(w)=a for a live record R_j(ε(w))=live(a,z), and T_j(w)=∞ for a stopped record. Define I_n(T)={T_n≤T<T_(n+1)}, and the total selector N(T,w)=min{n:w∈I_n(T)} when such an n exists, and 0 otherwise. For n≥0 let Hist_n=D^(Fin(n+1)) and H_n(w)_j=R_j(ε(w)). Write readTime(live(a,z))=a and readTime(stopped)=0. The abstract guard A_n(T) consists of histories all of whose records are live, whose read times are strictly increasing and whose positive-index read times are strictly below T; it does not constrain record0 itself. Actual H_n starts at live(0,z₀). For h∈Hist_n set d_n(T,h)=max{T−readTime(h_n),0}. Define survival(live(a,z),u,e) to mean u<τ_z(max{e,0}); on stopped it is false. Define W(live(a,z),u)=exp(−Λ_z(u)); on stopped W=0. Put C_n(T)={w:H_n(w)∈A_n(T), survival(R_n(ε(w)),d_n(T,H_n(w)),w_n)}. For a fixed finite T≥0 let Path_T be all functions from [0,T] into E×E, with its coordinate-product sigma algebra. On every history, including unrealizable ones, define Ψ_n(T,h)(s) by starting at z₀ and visiting j=0,…,n in increasing order: a live record (a,z) with a≤s replaces the current value by Φ_(s−a)(z), and an ineligible live or stopped record leaves it unchanged. All elapsed times in this total definition use nonnegative subtraction. Define Δ_n(T)={t∈ℝ^n:0<t₁<⋯<t_n<T}, and let m_n be the comap of product Lebesgue measure to this subtype, without normalization. For t∈Δ_n(T), put s₀=0,s_i=t_i, z₀ equal to the prescribed initial phase and z_i=S_rΦ_(s_i−s_(i−1))(z_(i−1)). Set K_n(t)_j=live(s_j,z_j), Γ_n(T,t)=Ψ_n(T,K_n(t)), q_n(t)=ofReal(∏_(i=1)^n λ_r(Φ_(s_i−s_(i−1))(z_(i−1)))exp[−Λ_(z_(i−1))(s_i−s_(i−1))]), and ρ_n(T,t)=q_n(t)W(K_n(t)_n,d_n(T,K_n(t))). The literal toNNReal conversions agree with these nonnegative simplex times. There exists one actual phase representative Z(y,r,z₀,t,w), jointly Borel in all deterministic parameters, finite time and raw input, with the following properties. On every raw covering interval T_n(w)≤s<T_(n+1)(w), if R_n(ε(w))=live(a,z), then Z(s,w)=Φ_(s−a)(z). If no interval covers s, Z(s,w)=z₀. For each fixed parameter tuple, Z(0,w)=z₀ almost surely. Put R(x,p)=(x,-p), V_y(x)=V(x)+||x-y||^2/(2 eta), and nu_y=(volume_E.tilted(-V_y)) times stdGaussian(E), in position/momentum order. Here tilted(-V_y) has density ofReal(exp(-V_y(x))/integral exp(-V_y) dx), and stdGaussian is the centered identity-covariance Gaussian. Normalizability is a consequence, not a premise. For the same single actual Z described above, every y,r in E and every finite T>=0, define for each n in Nat the map B_n(z,t)=(z,Gamma_(y,r,z,n,T,t)(T)), the measure sigma_n=(nu_y times m_n,T).withDensity((z,t)->rho_(y,r,z,n,T)(t)), and L_n=map B_n sigma_n on (E times E) times (E times E). Define M_Z(z,w)=(z,Z(y,r,z,T,w)), Q=map M_Z (nu_y times P), and J(z0,zT)=(R(zT),R(z0)). Every product uses initial phase first, and Q is the actual endpoint-pair law of the specified clock process. Then simultaneously Q=Measure.sum(n in Nat -> L_n), Q is a probability measure, and J is measurable with map J Q=Q. The sum includes every nonnegative integer without a cap. There is no assumption that a fixed-count sector has mass one. Joint measurability, simplex sigma-finiteness, measurable initial-phase sector integrals, countable exchange, and probability of the input measures are internal dependencies, not supplied hypotheses. In particular no joint-in-initial-state measurability of N is assumed: the count partition is taken at each fixed initial state before nonnegative integration against nu_y. The conclusion includes n=0 in the sum, T=0, dimension zero, zero rates and infinite waits with the explicit raw exceptional fallback above. At T=0 the actual initialization is almost sure; no pointwise all-clock initialization or jumpwise reversed-path equality is added. Arbitrary nonnegative measurable test functions may have infinite integrals during assembly. Signed bilinear duality, marginal phase invariance, restart/Markovness, hypocoercivity, implementation error, unbounded expected oracle cost and complete paper/composition results remain 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.

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

Exact module and namespace context

Full Lean proposition (definition) · actual_countable_endpoint_statement

This literal definition stores the complete proposition asserted above. It supplies no mathematical proof or additional hypothesis; the theorem proof must establish its value.

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

Download module (.lean)
private def actual_countable_endpoint_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 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 P : Measure (ℕ → ℝ) := Measure.infinitePi (fun _ : ℕ => expMeasure (1 : ℝ))
    let ε : (ℕ → ℝ) → ℕ → ℝ≥0 := fun w k => Real.toNNReal (w k)
    let history : E → E → (E × E) → (n : ℕ) → (ℕ → ℝ) →
        (Fin (n + 1) → ((ℝ≥0 × (E × E)) ⊕ Unit)) :=
      fun y xRef z₀ n w j => record y xRef z₀ (ε w) j.val
    let Rec := (ℝ≥0 × (E × E)) ⊕ Unit
    let Hist : ℕ → Type _ := fun n => Fin (n + 1) → Rec
    let readTime : Rec → ℝ := fun r => match r with
      | Sum.inl q => (q.1 : ℝ)
      | Sum.inr _ => 0
    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 qReal : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) →
        Prefix n T → ℝ := fun y xRef z₀ n T t =>
      ∏ i : Fin n,
        rate xRef (Φ y xRef (t.val i - (Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) i.castSucc)
          (zAt y xRef z₀ n T t i.castSucc)) *
        Real.exp (-Λ y xRef (zAt y xRef z₀ n T t i.castSucc)
          (Real.toNNReal (t.val i - (Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) i.castSucc)))
    let q : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) →
        Prefix n T → ℝ≥0∞ := fun y xRef z₀ n T t =>
      ENNReal.ofReal (qReal y xRef z₀ n T t)
    let A : (n : ℕ) → ℝ≥0 → Set (Hist n) := fun n T =>
      {h | (∀ j, ∃ a : ℝ≥0 × (E × E), h j = Sum.inl a) ∧
        StrictMono (fun j => readTime (h j)) ∧
        ∀ i : Fin n, readTime (h i.succ) < (T : ℝ)}
    let eventTime : E → E → (E × E) → (ℕ → ℝ) → ℕ → WithTop ℝ≥0 :=
      fun y xRef z₀ w j => (record y xRef z₀ (ε w) j).elim
        (fun a => (a.1 : WithTop ℝ≥0)) (fun _ => ⊤)
    let I : E → E → (E × E) → ℝ≥0 → ℕ → Set (ℕ → ℝ) :=
      fun y xRef z₀ T n => {w | eventTime y xRef z₀ w n ≤ (T : WithTop ℝ≥0) ∧
        (T : WithTop ℝ≥0) < eventTime y xRef z₀ w (n + 1)}
    let N : E → E → (E × E) → ℝ≥0 → (ℕ → ℝ) → ℕ := fun y xRef z₀ T w =>
      if h : ∃ n, w ∈ I y xRef z₀ T n then Nat.find h else 0
    let liveTime : Rec → ℝ≥0 := fun r => r.elim Prod.fst (fun _ => 0)
    let d : (n : ℕ) → ℝ≥0 → Hist n → ℝ≥0 :=
      fun n T h => T - liveTime (h ⟨n, Nat.lt_succ_self n⟩)
    let survival : E → E → Rec → ℝ≥0 → ℝ → Prop :=
      fun y xRef r u e => r.elim
        (fun a => (u : WithTop ℝ≥0) < τ y xRef a.2 (Real.toNNReal e)) (fun _ => False)
    let weight : E → E → Rec → ℝ≥0 → ℝ≥0∞ :=
      fun y xRef r u => r.elim
        (fun a => ENNReal.ofReal (Real.exp (-Λ y xRef a.2 u))) (fun _ => 0)
    let C : E → E → (E × E) → (n : ℕ) → ℝ≥0 → Set (ℕ → ℝ) :=
      fun y xRef z₀ n T => {w | history y xRef z₀ n w ∈ A n T ∧
        survival y xRef (record y xRef z₀ (ε w) n) (d n T (history y xRef z₀ n w)) (w n)}
    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 ρ : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) → Prefix n T → ℝ≥0∞ :=
      fun y xRef z₀ n T t => q y xRef z₀ n T t *
        weight y xRef ((K y xRef z₀ n T t) ⟨n, Nat.lt_succ_self n⟩)
          (d n T (K y xRef z₀ n T t))
    let R : E × E → E × E := fun z => (z.1, -z.2)
    let Vy : E → E → ℝ := fun y x => V x + ‖x - y‖ ^ 2 / (2 * η)
    let nu : E → Measure (E × E) := fun y =>
      ((volume : Measure E).tilted (fun x => -Vy y x)).prod
        (ProbabilityTheory.stdGaussian E)
    ∃ 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, ∀ w : ℕ → ℝ, ∀ s : ℝ≥0,
        ∀ n : ℕ, ∀ a : ℝ≥0 × (E × E), w ∈ I y xRef z₀ s n →
          record y xRef z₀ (ε w) n = Sum.inl a →
          Z y xRef z₀ s w = Φ y xRef ((s - a.1 : ℝ≥0) : ℝ) a.2) ∧
      (∀ y xRef : E, ∀ z₀ : E × E, ∀ w : ℕ → ℝ, ∀ s : ℝ≥0,
        (¬ ∃ n, w ∈ I y xRef z₀ s n) → Z y xRef z₀ s w = z₀) ∧
      (∀ y xRef : E, ∀ z₀ : E × E, ∀ᵐ w ∂P, Z y xRef z₀ 0 w = z₀) ∧
      (∀ y r : E, ∀ T : ℝ≥0,
        let B : (n : ℕ) → (E × E) × Prefix n T → (E × E) × (E × E) :=
          fun n q => (q.1, Γ y r q.1 n T q.2 ⟨T, le_rfl⟩)
        let sigma : (n : ℕ) → Measure ((E × E) × Prefix n T) := fun n =>
          ((nu y).prod (m n T)).withDensity (fun q => ρ y r q.1 n T q.2)
        let L : ℕ → Measure ((E × E) × (E × E)) := fun n => Measure.map (B n) (sigma n)
        let M : (E × E) × (ℕ → ℝ) → (E × E) × (E × E) :=
          fun q => (q.1, Z y r q.1 T q.2)
        let Q : Measure ((E × E) × (E × E)) := Measure.map M ((nu y).prod P)
        let J : (E × E) × (E × E) → (E × E) × (E × E) :=
          fun q => (R q.2, R q.1)
        Q = Measure.sum L ∧ IsProbabilityMeasure Q ∧ MeasurePreserving J Q Q)


set_option maxHeartbeats 1600000
set_option maxRecDepth 10000

Exact module and namespace context

Proof roadmap

  1. 1Select the same actual global process

    Use the existing actual finite-count path law once. Retain its single jointly measurable Z and its arc, fallback and almost-sure zero-time formulas for the entire theorem. No fresh abstract process replaces it.

  2. 2Establish the actual endpoint probability

    Write H=E×E, pi_y=volume_E.tilted(-V_y), and gamma=stdGaussian(E). The phase normalization theorem identifies the initial product law and proves it is probability. The unit-exponential product theorem supplies probability, hence sigma-finiteness, of P. Joint measurability of Z makes the actual endpoint map M measurable; its pushforward Q has mass one.

  3. 3Retain joint endpoint and density measurability

    Fix y,r with a measurable embedding and evaluate the jointly measurable prescribed path at T. Pairing with z yields B_n. The same actual finite-count theorem supplies the actual density rho, including terminal survival.

  4. 4Justify integration over each time simplex

    Express strict ordering and the terminal bound through measurable coordinate inequalities. The subtype measure maps to Lebesgue measure restricted to the simplex, so it is sigma-finite for every n, including n=0.

  5. 5Make the sector integrals measurable in the initial phase

    To identify measures, fix any measurable extended-nonnegative F. Joint measurability of B_n and rho and sigma-finiteness of m give measurable parameter integrals D_n(z). No finite-integral or signed domination premise is used.

  6. 6Partition the actual clock input by its finite count

    For each fixed initial z, the Nat-valued total count has measurable disjoint fibers whose union is all clock inputs. Apply the actual finite-count test identity on each fiber using the terminal evaluation test. This gives a nonnegative countable expansion for the same Z. No joint-in-z count measurability is needed.

  7. 7Average and identify the full countable measure

    Integrate the fixed-initial identity against nu_y. Nonnegative Tonelli on nu_y times P and on nu_y times m_n,T, together with measurable D_n and countable monotone summation, turns each term into the integral against L_n. Equality on every measurable extended-nonnegative F proves Q=sum L_n; infinite test integrals are allowed.

  8. 8Assemble the common endpoint reversal

    Apply the reviewed normalized endpoint reversal to each n using the same literal J. Global measurability permits pushforward to commute with the countable sum. Combine with the actual-law equality and its already established probability.

Full assumptions and notation

All objects and hypotheses

  • Finite-dimensional real inner-product Borel E with canonical volume, 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.
  • The actual global process is existentially constructed, with joint measurability, literal arc/fallback characterization and almost-sure initialization. Every y,r and finite nonnegative T is included, and all n in Nat are summed.
  • All harmonic flow, totalized reflection, exponential clocks, strict simplex, actual event density, conditional Gibbs initial phase and endpoint measures are the displayed definitions. No supplied process, normalizer, integrability, joint count-measurability, cap or finite-sector-probability premise.

Mathematical proof

1. Select the same actual global process

Use the existing actual finite-count path law once. Retain its single jointly measurable Z and its arc, fallback and almost-sure zero-time formulas for the entire theorem. No fresh abstract process replaces it.

\[Z(y,r,z,s,w)=\Phi_{s-a}(b)\quad\text{on each live covering arc }(a,b);\qquad Z(y,r,z,0,w)=z\ \ P\text{-a.e.}\]
Corresponding Lean step
  obtain ⟨Z, hZm, hZa, hZf, hZ0, h93⟩ :=
    AutoSamplingTheory.ExampleCases.ProximalBPS.ActualFiniteCountPath.actual_finite_count_path_law
      hα hαβ hV hH hη hβη
  refine ⟨Z, hZm, hZa, hZf, hZ0, ?_⟩
  intro y r T B sigma L M Q J

ASTIS completion of the countable initial-phase averaging step. Exact compiled region; the original six analytic assumptions are unchanged.

2. Establish the actual endpoint probability

Write H=E×E, pi_y=volume_E.tilted(-V_y), and gamma=stdGaussian(E). The phase normalization theorem identifies the initial product law and proves it is probability. The unit-exponential product theorem supplies probability, hence sigma-finiteness, of P. Joint measurability of Z makes the actual endpoint map M measurable; its pushforward Q has mass one.

\[\nu_y=\pi_y\otimes\gamma,\quad M(z,w)=(z,Z(y,r,z,T,w)),\quad Q=M_*(\nu_y\otimes P),\quad Q(H\times H)=1.\]
Corresponding Lean step
  have h103 := AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPhaseNormalization.actual_phase_gibbs_normalization
    hα hαβ hV hH hη hβη y
  letI : IsProbabilityMeasure (nu y) := by
    have hp := h103.2.2.2.2.2.1
    rw [h103.2.2.2.2.2.2] at hp
    exact hp
  letI : IsProbabilityMeasure P :=
    AutoSamplingTheory.TechnicalLemmas.Probability.UnitExponentialProduct.unit_exponential_product_laws.1
  have hembZ : Measurable (fun q : (E × E) × (ℕ → ℝ) => (((y, r), q.1), T, q.2)) :=
    (measurable_const.prodMk measurable_fst).prodMk (measurable_const.prodMk measurable_snd)
  have hZend := hZm.comp hembZ
  have hM : Measurable M := measurable_fst.prodMk hZend
  have hQ : IsProbabilityMeasure Q := Measure.isProbabilityMeasure_map hM.aemeasurable

ASTIS completion of the countable initial-phase averaging step. Exact compiled region; the original six analytic assumptions are unchanged.

3. Retain joint endpoint and density measurability

Fix y,r with a measurable embedding and evaluate the jointly measurable prescribed path at T. Pairing with z yields B_n. The same actual finite-count theorem supplies the actual density rho, including terminal survival.

\[(z,t)\mapsto B_n(z,t),\qquad (z,t)\mapsto\rho_{y,r,z,n,T}(t)\quad\text{are measurable}.\]
Corresponding Lean step
  have hB (n : ℕ) : Measurable (B n) := by
    have hemb : Measurable (fun q : (E × E) × Prefix n T => (((y, r), q.1), q.2)) :=
      (measurable_const.prodMk measurable_fst).prodMk measurable_snd
    have hp := (h93 n T).2.1.comp hemb
    have he := (measurable_pi_apply (⟨T, le_rfl⟩ : {s : ℝ≥0 // s ≤ T})).comp hp
    exact measurable_fst.prodMk he
  have hρ (n : ℕ) : Measurable (fun q : (E × E) × Prefix n T => ρ y r q.1 n T q.2) := by
    have hemb : Measurable (fun q : (E × E) × Prefix n T => (((y, r), q.1), q.2)) :=
      (measurable_const.prodMk measurable_fst).prodMk measurable_snd
    have h := (h93 n T).2.2.1.comp hemb
    simpa only [Function.comp_def] using h

ASTIS completion of the countable initial-phase averaging step. Exact compiled region; the original six analytic assumptions are unchanged.

4. Justify integration over each time simplex

Express strict ordering and the terminal bound through measurable coordinate inequalities. The subtype measure maps to Lebesgue measure restricted to the simplex, so it is sigma-finite for every n, including n=0.

\[\Delta_n(T)=\{0<t_1<\cdots<t_n<T\},\quad\iota_*m_{n,T}=dt|_{\Delta_n(T)},\quad m_{n,T}\text{ sigma-finite}.\]
Corresponding Lean step
  have hm (n : ℕ) : SigmaFinite (m n T) := by
    have hcons (i : Fin (n + 1)) :
        Measurable (fun t : Fin n → ℝ => (Fin.cons (0 : ℝ) t : Fin (n + 1) → ℝ) i) := by
      induction i using Fin.cases with
      | zero => exact measurable_const
      | succ i => exact measurable_pi_apply i
    have hs : MeasurableSet (Δ n T) := by
      change MeasurableSet {t : Fin n → ℝ |
        (∀ i j : Fin (n + 1), i < j → (Fin.cons (0 : ℝ) t : Fin (n + 1) → ℝ) i < (Fin.cons (0 : ℝ) t : Fin (n + 1) → ℝ) j) ∧
        ∀ i : Fin n, t i < (T : ℝ)}
      rw [Set.ofPred_and]
      apply MeasurableSet.inter
      · simpa only [← Set.ofPred_forall] using (MeasurableSet.iInter fun (i : Fin (n + 1)) =>
          MeasurableSet.iInter fun (j : Fin (n + 1)) =>
          MeasurableSet.iInter fun (_ : i < j) => measurableSet_lt (hcons i) (hcons j))
      · simpa only [← Set.ofPred_forall] using (MeasurableSet.iInter fun (i : Fin n) =>
          measurableSet_lt (measurable_pi_apply i) (measurable_const (a := (T : ℝ))))
    have hmσ : SigmaFinite ((m n T).map (fun t : Prefix n T => t.val)) := by
      change SigmaFinite ((Measure.comap (fun t : Prefix n T => t.val)
        (volume : Measure (Fin n → ℝ))).map (fun t : Prefix n T => t.val))
      rw [map_comap_subtype_coe hs]
      infer_instance
    exact SigmaFinite.of_map (m n T) measurable_subtype_coe.aemeasurable hmσ

ASTIS completion of the countable initial-phase averaging step. Exact compiled region; the original six analytic assumptions are unchanged.

5. Make the sector integrals measurable in the initial phase

To identify measures, fix any measurable extended-nonnegative F. Joint measurability of B_n and rho and sigma-finiteness of m give measurable parameter integrals D_n(z). No finite-integral or signed domination premise is used.

\[D_n(z)=\int_{\Delta_n(T)}F(B_n(z,t))\rho_{y,r,z,n,T}(t)\,m_{n,T}(dt).\]
Corresponding Lean step
  have hsum : Q = Measure.sum L := by
    apply Measure.ext_of_lintegral
    intro F hF
    let D : ℕ → (E × E) → ℝ≥0∞ := fun n z =>
      ∫⁻ t : Prefix n T, F (B n (z, t)) * ρ y r z n T t ∂m n T
    have hD (n : ℕ) : Measurable (D n) := by
      letI := hm n
      exact ((hF.comp (hB n)).mul (hρ n)).lintegral_prod_right'

ASTIS completion of the countable initial-phase averaging step. Exact compiled region; the original six analytic assumptions are unchanged.

6. Partition the actual clock input by its finite count

For each fixed initial z, the Nat-valued total count has measurable disjoint fibers whose union is all clock inputs. Apply the actual finite-count test identity on each fiber using the terminal evaluation test. This gives a nonnegative countable expansion for the same Z. No joint-in-z count measurability is needed.

\[\int F(z,Z_T(w))\,P(dw)=\sum_{n\ge0}\int_{\{N(T)=n\}}F(z,Z_T(w))\,P(dw)=\sum_{n\ge0}D_n(z).\]
Corresponding Lean step
    have hz (z : E × E) :
        (∫⁻ w, F (z, Z y r z T w) ∂P) = ∑' n, D n z := by
      have hN : Measurable (N y r z T) := ((h93 0 T).2.2.2 y r z).2.2.1
      have hsets (n : ℕ) : MeasurableSet {w | N y r z T w = n} :=
        (measurableSet_singleton n).preimage hN
      have hdis : Pairwise (fun i j : ℕ => Disjoint {w | N y r z T w = i} {w | N y r z T w = j}) := by
        intro i j hij
        exact Set.disjoint_left.mpr (fun w hi hj => hij (hi.symm.trans hj))
      have hu : (⋃ n : ℕ, {w | N y r z T w = n}) = Set.univ := by
        ext w
        simp
      calc
        (∫⁻ w, F (z, Z y r z T w) ∂P) =
            ∑' n, ∫⁻ w in {w | N y r z T w = n}, F (z, Z y r z T w) ∂P := by
          simpa only [hu, Measure.restrict_univ] using
            (lintegral_iUnion hsets hdis (fun w => F (z, Z y r z T w)))
        _ = ∑' n, D n z := by
          apply tsum_congr
          intro n
          rcases (h93 n T).2.2.2 y r z with
            ⟨hH, hZT, hNN, hC, hGamma, hactual, hAE, hdisjoint, hcover, hlaw, hint, hmass, hbound⟩
          exact hint (fun hp => F (z, hp.2 ⟨T, le_rfl⟩))
            (hF.comp (measurable_const.prodMk ((measurable_pi_apply (⟨T, le_rfl⟩ : {s : ℝ≥0 // s ≤ T})).comp measurable_snd)))

ASTIS completion of the countable initial-phase averaging step. Exact compiled region; the original six analytic assumptions are unchanged.

7. Average and identify the full countable measure

Integrate the fixed-initial identity against nu_y. Nonnegative Tonelli on nu_y times P and on nu_y times m_n,T, together with measurable D_n and countable monotone summation, turns each term into the integral against L_n. Equality on every measurable extended-nonnegative F proves Q=sum L_n; infinite test integrals are allowed.

\[\int F\,dQ=\int\sum_nD_n\,d\nu_y=\sum_n\int D_n\,d\nu_y=\sum_n\int F\,dL_n=\int F\,d\!\left(\sum_nL_n\right).\]
Corresponding Lean step
    calc
      (∫⁻ x, F x ∂Q) = ∫⁻ z, ∫⁻ w, F (z, Z y r z T w) ∂P ∂nu y := by
        change (∫⁻ x, F x ∂Measure.map M ((nu y).prod P)) = _
        rw [lintegral_map hF hM]
        exact lintegral_prod (f := fun x => F (M x)) (hF.comp hM).aemeasurable
      _ = ∫⁻ z, ∑' n, D n z ∂nu y := lintegral_congr hz
      _ = ∑' n, ∫⁻ z, D n z ∂nu y := lintegral_tsum (fun n => (hD n).aemeasurable)
      _ = ∑' n, ∫⁻ x, F x ∂L n := by
        apply tsum_congr
        intro n
        letI := hm n
        change (∫⁻ z, ∫⁻ t : Prefix n T, F (B n (z, t)) * ρ y r z n T t ∂m n T ∂nu y) =
          ∫⁻ x, F x ∂Measure.map (B n) (sigma n)
        rw [lintegral_map hF (hB n)]
        change _ = ∫⁻ x, F (B n x) ∂(((nu y).prod (m n T)).withDensity (fun x => ρ y r x.1 n T x.2))
        rw [lintegral_withDensity_eq_lintegral_mul _
          (f := fun x : (E × E) × Prefix n T => ρ y r x.1 n T x.2)
          (g := fun x => F (B n x)) (hρ n) (hF.comp (hB n))]
        simp only [Pi.mul_apply]
        rw [lintegral_prod (f := fun x : (E × E) × Prefix n T =>
          ρ y r x.1 n T x.2 * F (B n x)) ((hρ n).mul (hF.comp (hB n))).aemeasurable]
        apply lintegral_congr
        intro z
        apply lintegral_congr
        intro t
        exact mul_comm _ _
      _ = ∫⁻ x, F x ∂Measure.sum L := (lintegral_sum_measure F L).symm

ASTIS completion of the countable initial-phase averaging step. Exact compiled region; the original six analytic assumptions are unchanged.

8. Assemble the common endpoint reversal

Apply the reviewed normalized endpoint reversal to each n using the same literal J. Global measurability permits pushforward to commute with the countable sum. Combine with the actual-law equality and its already established probability.

\[J_*Q=J_*\!\left(\sum_n L_n\right)=\sum_nJ_*L_n=\sum_nL_n=Q.\]
Corresponding Lean step
  have hsector (n : ℕ) : MeasurePreserving J (L n) (L n) :=
    AutoSamplingTheory.ExampleCases.ProximalBPS.ActualNormalizedEndpointSector.actual_normalized_endpoint_sector_reversal
      hα hαβ hV hH hη hβη y r n T
  refine ⟨hsum, hQ, (hsector 0).measurable, ?_⟩
  rw [hsum, Measure.map_sum (hsector 0).measurable.aemeasurable]
  congr 1
  funext n
  exact (hsector n).map_eq

ASTIS completion of the countable initial-phase averaging step. Exact compiled region; the original six analytic assumptions are unchanged.

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · actual_countable_endpoint_law

Select the same actual global process; Establish the actual endpoint probability; Retain joint endpoint and density measurability; Justify integration over each time simplex; Make the sector integrals measurable in the initial phase; Partition the actual clock input by its finite count; Average and identify the full countable measure; Assemble the common endpoint reversal

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

Download module (.lean)
theorem actual_countable_endpoint_law
    {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_countable_endpoint_statement hα hαβ hV hH hη hβη := by
  classical
  unfold actual_countable_endpoint_statement
  intro c Φ S rate Λ τ next record P ε history Rec Hist readTime Δ Prefix m zAt K qReal q A eventTime I N liveTime d survival weight C Path Ψ Γ ρ R Vy nu
  obtain ⟨Z, hZm, hZa, hZf, hZ0, h93⟩ :=
    AutoSamplingTheory.ExampleCases.ProximalBPS.ActualFiniteCountPath.actual_finite_count_path_law
      hα hαβ hV hH hη hβη
  refine ⟨Z, hZm, hZa, hZf, hZ0, ?_⟩
  intro y r T B sigma L M Q J
  have h103 := AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPhaseNormalization.actual_phase_gibbs_normalization
    hα hαβ hV hH hη hβη y
  letI : IsProbabilityMeasure (nu y) := by
    have hp := h103.2.2.2.2.2.1
    rw [h103.2.2.2.2.2.2] at hp
    exact hp
  letI : IsProbabilityMeasure P :=
    AutoSamplingTheory.TechnicalLemmas.Probability.UnitExponentialProduct.unit_exponential_product_laws.1
  have hembZ : Measurable (fun q : (E × E) × (ℕ → ℝ) => (((y, r), q.1), T, q.2)) :=
    (measurable_const.prodMk measurable_fst).prodMk (measurable_const.prodMk measurable_snd)
  have hZend := hZm.comp hembZ
  have hM : Measurable M := measurable_fst.prodMk hZend
  have hQ : IsProbabilityMeasure Q := Measure.isProbabilityMeasure_map hM.aemeasurable
  have hB (n : ℕ) : Measurable (B n) := by
    have hemb : Measurable (fun q : (E × E) × Prefix n T => (((y, r), q.1), q.2)) :=
      (measurable_const.prodMk measurable_fst).prodMk measurable_snd
    have hp := (h93 n T).2.1.comp hemb
    have he := (measurable_pi_apply (⟨T, le_rfl⟩ : {s : ℝ≥0 // s ≤ T})).comp hp
    exact measurable_fst.prodMk he
  have hρ (n : ℕ) : Measurable (fun q : (E × E) × Prefix n T => ρ y r q.1 n T q.2) := by
    have hemb : Measurable (fun q : (E × E) × Prefix n T => (((y, r), q.1), q.2)) :=
      (measurable_const.prodMk measurable_fst).prodMk measurable_snd
    have h := (h93 n T).2.2.1.comp hemb
    simpa only [Function.comp_def] using h
  have hm (n : ℕ) : SigmaFinite (m n T) := by
    have hcons (i : Fin (n + 1)) :
        Measurable (fun t : Fin n → ℝ => (Fin.cons (0 : ℝ) t : Fin (n + 1) → ℝ) i) := by
      induction i using Fin.cases with
      | zero => exact measurable_const
      | succ i => exact measurable_pi_apply i
    have hs : MeasurableSet (Δ n T) := by
      change MeasurableSet {t : Fin n → ℝ |
        (∀ i j : Fin (n + 1), i < j → (Fin.cons (0 : ℝ) t : Fin (n + 1) → ℝ) i < (Fin.cons (0 : ℝ) t : Fin (n + 1) → ℝ) j) ∧
        ∀ i : Fin n, t i < (T : ℝ)}
      rw [Set.ofPred_and]
      apply MeasurableSet.inter
      · simpa only [← Set.ofPred_forall] using (MeasurableSet.iInter fun (i : Fin (n + 1)) =>
          MeasurableSet.iInter fun (j : Fin (n + 1)) =>
          MeasurableSet.iInter fun (_ : i < j) => measurableSet_lt (hcons i) (hcons j))
      · simpa only [← Set.ofPred_forall] using (MeasurableSet.iInter fun (i : Fin n) =>
          measurableSet_lt (measurable_pi_apply i) (measurable_const (a := (T : ℝ))))
    have hmσ : SigmaFinite ((m n T).map (fun t : Prefix n T => t.val)) := by
      change SigmaFinite ((Measure.comap (fun t : Prefix n T => t.val)
        (volume : Measure (Fin n → ℝ))).map (fun t : Prefix n T => t.val))
      rw [map_comap_subtype_coe hs]
      infer_instance
    exact SigmaFinite.of_map (m n T) measurable_subtype_coe.aemeasurable hmσ
  have hsum : Q = Measure.sum L := by
    apply Measure.ext_of_lintegral
    intro F hF
    let D : ℕ → (E × E) → ℝ≥0∞ := fun n z =>
      ∫⁻ t : Prefix n T, F (B n (z, t)) * ρ y r z n T t ∂m n T
    have hD (n : ℕ) : Measurable (D n) := by
      letI := hm n
      exact ((hF.comp (hB n)).mul (hρ n)).lintegral_prod_right'
    have hz (z : E × E) :
        (∫⁻ w, F (z, Z y r z T w) ∂P) = ∑' n, D n z := by
      have hN : Measurable (N y r z T) := ((h93 0 T).2.2.2 y r z).2.2.1
      have hsets (n : ℕ) : MeasurableSet {w | N y r z T w = n} :=
        (measurableSet_singleton n).preimage hN
      have hdis : Pairwise (fun i j : ℕ => Disjoint {w | N y r z T w = i} {w | N y r z T w = j}) := by
        intro i j hij
        exact Set.disjoint_left.mpr (fun w hi hj => hij (hi.symm.trans hj))
      have hu : (⋃ n : ℕ, {w | N y r z T w = n}) = Set.univ := by
        ext w
        simp
      calc
        (∫⁻ w, F (z, Z y r z T w) ∂P) =
            ∑' n, ∫⁻ w in {w | N y r z T w = n}, F (z, Z y r z T w) ∂P := by
          simpa only [hu, Measure.restrict_univ] using
            (lintegral_iUnion hsets hdis (fun w => F (z, Z y r z T w)))
        _ = ∑' n, D n z := by
          apply tsum_congr
          intro n
          rcases (h93 n T).2.2.2 y r z with
            ⟨hH, hZT, hNN, hC, hGamma, hactual, hAE, hdisjoint, hcover, hlaw, hint, hmass, hbound⟩
          exact hint (fun hp => F (z, hp.2 ⟨T, le_rfl⟩))
            (hF.comp (measurable_const.prodMk ((measurable_pi_apply (⟨T, le_rfl⟩ : {s : ℝ≥0 // s ≤ T})).comp measurable_snd)))
    calc
      (∫⁻ x, F x ∂Q) = ∫⁻ z, ∫⁻ w, F (z, Z y r z T w) ∂P ∂nu y := by
        change (∫⁻ x, F x ∂Measure.map M ((nu y).prod P)) = _
        rw [lintegral_map hF hM]
        exact lintegral_prod (f := fun x => F (M x)) (hF.comp hM).aemeasurable
      _ = ∫⁻ z, ∑' n, D n z ∂nu y := lintegral_congr hz
      _ = ∑' n, ∫⁻ z, D n z ∂nu y := lintegral_tsum (fun n => (hD n).aemeasurable)
      _ = ∑' n, ∫⁻ x, F x ∂L n := by
        apply tsum_congr
        intro n
        letI := hm n
        change (∫⁻ z, ∫⁻ t : Prefix n T, F (B n (z, t)) * ρ y r z n T t ∂m n T ∂nu y) =
          ∫⁻ x, F x ∂Measure.map (B n) (sigma n)
        rw [lintegral_map hF (hB n)]
        change _ = ∫⁻ x, F (B n x) ∂(((nu y).prod (m n T)).withDensity (fun x => ρ y r x.1 n T x.2))
        rw [lintegral_withDensity_eq_lintegral_mul _
          (f := fun x : (E × E) × Prefix n T => ρ y r x.1 n T x.2)
          (g := fun x => F (B n x)) (hρ n) (hF.comp (hB n))]
        simp only [Pi.mul_apply]
        rw [lintegral_prod (f := fun x : (E × E) × Prefix n T =>
          ρ y r x.1 n T x.2 * F (B n x)) ((hρ n).mul (hF.comp (hB n))).aemeasurable]
        apply lintegral_congr
        intro z
        apply lintegral_congr
        intro t
        exact mul_comm _ _
      _ = ∫⁻ x, F x ∂Measure.sum L := (lintegral_sum_measure F L).symm
  have hsector (n : ℕ) : MeasurePreserving J (L n) (L n) :=
    AutoSamplingTheory.ExampleCases.ProximalBPS.ActualNormalizedEndpointSector.actual_normalized_endpoint_sector_reversal
      hα hαβ hV hH hη hβη y r n T
  refine ⟨hsum, hQ, (hsector 0).measurable, ?_⟩
  rw [hsum, Measure.map_sum (hsector 0).measurable.aemeasurable]
  congr 1
  funext n
  exact (hsector n).map_eq

#print axioms actual_countable_endpoint_law
end
end AutoSamplingTheory.ExampleCases.ProximalBPS.ActualCountableEndpointLaw

Exact module and namespace context

Source assumptions versus formal assumptions

SourceActual LeanDifference kindWhy it matters
A7 finite-count expansion followed by initial Gibbs averaging and nonnegative Tonelli.Actual endpoint probability Q equals the all-Nat sector sum and is preserved by J.sameASTIS exposes the measure identity of the source averaging step with all ingredients derived.
Finite-dimensional Euclidean phase.Finite real Hilbert Borel space including rank zero.generalizationCoordinate-free canonical volume and Gaussian preserve the formulas.
Original six analytic assumptions.Same six assumptions, with one actual global process in the conclusion.sameUnchanged presealed literal proposition.
Signed duality and invariant process arguments.Countable endpoint-law assembly and reversal only.unresolvedActual normalized countable endpoint law, probability and endpoint reversal only. Signed bilinear averaging, phase marginal invariance, restart/Markovness, hypocoercivity, implementation errors, expected costs, full composition and four full papers remain open.

Actual normalized countable endpoint law, probability and endpoint reversal only. Signed bilinear averaging, phase marginal invariance, restart/Markovness, hypocoercivity, implementation errors, expected costs, full composition and four full papers remain open.

Encoder–denoiser: accepted · equivalent-after-elaboration

Detected semantic differences

  • domains: Finite-dimensional Hilbert and totalized raw-clock/path conventions elaborate the Euclidean source calculation, including rank zero and exceptional inputs. — Actual clock probability law and exact process contract preserve source almost-sure dynamics; no source binder strengthened.
  • conclusion: Nonnegative averaging is packaged as equality of actual endpoint measures, plus probability and flipped-swap preservation of that same law. — Measurable ENNReal tests and countable Tonelli prove measure equality; probability uses actual103 and actual clock law, not fixed-sector104 alone.
  • scopes: The selected source slice ends before signed bilinear duality and marginal invariance. — Current public triple, blind reconstruction and all eight authored steps agree on this boundary.

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

Scope and omitted-condition boundaries
  • Actual normalized countable endpoint law, probability and endpoint reversal only. Signed bilinear averaging, phase marginal invariance, restart/Markovness, hypocoercivity, implementation errors, expected costs, full composition and four full papers remain open.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

  • Measurable.lintegral_prod_right'
  • Measure.isProbabilityMeasure_map
  • map_comap_subtype_coe
  • SigmaFinite.of_map
  • Measure.ext_of_lintegral
  • lintegral_iUnion
  • lintegral_tsum
  • lintegral_prod
  • lintegral_map
  • lintegral_withDensity_eq_lintegral_mul
  • lintegral_sum_measure
  • Measure.map_sum

Mathematical sources

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.

Which proof obligations and prerequisites are covered?

  • Formalized proof edge; source adapter/review separate Actual normalized countable endpoint law
  • TODO — not closed by these contributions Normalized averaging and invariant process law