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

Actual PBPS full real-L2 momentum-flip adjoint identity

Chen, Chewi, Lu and Zhang, arXiv:2609.06905v1, Appendix A.1 Eq A.3 and final density extension, with Eq3.1 phase law. Complete attributed mathematical restatement; ASTIS makes the canonical L2 flip and dense-subspace extension explicit. This is not a verbatim standalone theorem quotation.

arXiv2609.06905v1 · Appendix A.1 Eq A.3 (A1.E3 lines3000-3014), density extension (A1.Ex21 lines3210-3227), phase law Eq3.1 lines1411-1422. · 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. Write H=E times E, pi_y=volume_E.tilted(-V_y), gamma=stdGaussian(E), so nu_y=pi_y times gamma. For the same single global actual Z described above, every y,r in E and every finite T>=0, define op_T G(z)=integral G(Z(y,r,z,T,w)) dP(w), a real Bochner integral, and endpoint_T(z,w)=Z(y,r,z,T,w). Then endpoint_T is measurable and its pushforward of nu_y times P is exactly nu_y. For every pair F,G:H->R of Borel measurable functions and finite real bounds C_F,C_G>=0 with |F(z)|<=C_F and |G(z)|<=C_G for all z, both z->F(z)*op_T G(z) and z->G(R(z))*op_T(F composed R)(z) are integrable against nu_y, and their real integrals are equal. Thus integral F(z)*op_T G(z) dnu_y(z) = integral G(R(z))*op_T(F composed R)(z) dnu_y(z). All these conclusions use the same Z, existentially chosen before all centers, references, horizons and observables. Products are phase first, clock input second. No process, kernel, finite mass, signed integrability, momentum symmetry or normalizability is a supplied premise. Dimension zero, T=0, vanishing test bounds, zero bounce rates, infinite waits and raw exceptional fallback remain included. Almost-sure initialization stays parameterwise; no uniform all-parameter null set or pointwise reversed path at jumps is asserted. For every Borel G:H->R, the total real clock expectation (y,r,z,T)->integral G(Z(y,r,z,T,w)) dP(w) is jointly Borel. If C is a finite nonnegative real number and |G(z)|<=C for all z, then for every y,r,z,T the clock section is P-integrable and the absolute value of this expectation is at most C. For every y,r in E there exists a family A indexed by finite nonnegative T, where A_T:L2(nu_y;R)->L2(nu_y;R) is a continuous real linear operator, A_0 is the identity and ||A_T||<=1 for every T. For every real function G with MemLp G 2 nu_y (almost-everywhere strong measurability and finite L2 seminorm), the section w->G(Z(y,r,z,T,w)) is P-integrable for nu_y-almost every z. The literal expectation op_T G belongs to L2(nu_y;R), and A_T[G]=[op_T G]. Thus integral |op_T G|^2 dnu_y <= integral |G|^2 dnu_y. Brackets denote equality classes modulo nu_y-almost-everywhere equality; no pointwise identification of arbitrary L2 representatives is asserted. The operator, section integrability and output L2 membership are conclusions, not supplied premises. These operators use the same single global Z as all inherited path, initialization, invariance and bounded-duality conclusions. The bound1 is exact and independent of dimension, center, reference and horizon. The joint Borel assertion concerns Borel input G; arbitrary MemLp representatives receive the stated almost-everywhere conclusions. In addition, for each y,r the same operator family A has the following property. The literal phase reflection R(x,p)=(x,-p) preserves nu_y. Its canonical pullback J_y on real L2(nu_y) is the linear isometry defined by composition with R; for every L2 class f, (J_y f)(z)=f(R(z)) for nu_y-almost every z, and J_y(J_y f)=f. For every finite nonnegative T, the Hilbert adjoint of that same A_T satisfies A_T*=J_y A_T J_y as an equality of continuous real linear operators. Equivalently its pairing obeys <f,A_T g>=<J_y g,A_T(J_y f)> for all real L2 classes f,g. The pullback and its preservation/involution are proved conclusions; no supplied symmetry, operator relation, integrability or density hypothesis is added. The flip depends only on the displayed R and nu_y; the proof witness hR under y,r does not introduce reference or time dependence into J_y. The identity includes T=0 and rank zero. All representative equalities retain their stated almost-everywhere sense, with no common null set over all parameters or representatives. This is the full fixed-time real-L2 identity of Appendix A.1, Eq A.3, together with the exact inherited process and expectation contract. Strong continuity, restart/Markov/semigroup, complex-L2 extension, a separately existential kernel identification, actual momentum-averaged position operator, hypocoercivity, implementation errors, actual expected costs, actual-input composition and complete papers remain outside this result.

  • 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.
  • A single global actual process is constructed in the conclusion, with the literal joint measurability, arc/fallback and parameterwise almost-sure initialization contracts; every y,r and finite nonnegative T is included.
  • The universal bounded-observable conclusion ranges over measurable real F,G and finite nonnegative C_F,C_G with pointwise absolute-value bounds. These are test domains, not extra assumptions on the sampler.
  • For the L2 conclusion G is any real function with MemLp G 2 nu_y. For joint Borel dependence G is Borel; every-section L1 additionally uses a finite nonnegative pointwise bound. Operator existence, integrability, output membership and bound1 are conclusions.
  • All actual algorithm, clock and Gibbs phase objects are literal. No supplied Z/kernel/operator, integrability, normalizer, momentum symmetry, restart or Markov premise.

Actual full real-L2 flip adjoint identity

\[A_T^*=J A_T J.\]

All L2 pairings

\[\forall f,g\in L^2(\nu_y;\mathbb R),\qquad\langle f,A_Tg\rangle=\langle Jg,A_TJf\rangle.\]

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 PBPS full real-L2 momentum-flip adjoint identity

AutoSamplingTheory.ExampleCases.ProximalBPS.ActualL2FlipDuality.actual_l2_flip_duality · 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. Write H=E times E, pi_y=volume_E.tilted(-V_y), gamma=stdGaussian(E), so nu_y=pi_y times gamma. For the same single global actual Z described above, every y,r in E and every finite T≥0, define op_T G(z)=integral G(Z(y,r,z,T,w)) dP(w), a real Bochner integral, and endpoint_T(z,w)=Z(y,r,z,T,w). Then endpoint_T is measurable and its pushforward of nu_y times P is exactly nu_y. For every pair F,G:H→R of Borel measurable functions and finite real bounds C_F,C_G≥0 with |F(z)|≤C_F and |G(z)|≤C_G for all z, both z→F(z)*op_T G(z) and z→G(R(z))*op_T(F composed R)(z) are integrable against nu_y, and their real integrals are equal. Thus integral F(z)*op_T G(z) dnu_y(z) = integral G(R(z))*op_T(F composed R)(z) dnu_y(z). All these conclusions use the same Z, existentially chosen before all centers, references, horizons and observables. Products are phase first, clock input second. No process, kernel, finite mass, signed integrability, momentum symmetry or normalizability is a supplied premise. Dimension zero, T=0, vanishing test bounds, zero bounce rates, infinite waits and raw exceptional fallback remain included. Almost-sure initialization stays parameterwise; no uniform all-parameter null set or pointwise reversed path at jumps is asserted. For every Borel G:H→R, the total real clock expectation (y,r,z,T)→integral G(Z(y,r,z,T,w)) dP(w) is jointly Borel. If C is a finite nonnegative real number and |G(z)|≤C for all z, then for every y,r,z,T the clock section is P-integrable and the absolute value of this expectation is at most C. For every y,r in E there exists a family A indexed by finite nonnegative T, where A_T:L2(nu_y;R)→L2(nu_y;R) is a continuous real linear operator, A_0 is the identity and ||A_T||≤1 for every T. For every real function G with MemLp G 2 nu_y (almost-everywhere strong measurability and finite L2 seminorm), the section w→G(Z(y,r,z,T,w)) is P-integrable for nu_y-almost every z. The literal expectation op_T G belongs to L2(nu_y;R), and A_T[G]=[op_T G]. Thus integral |op_T G|^2 dnu_y ≤ integral |G|^2 dnu_y. Brackets denote equality classes modulo nu_y-almost-everywhere equality; no pointwise identification of arbitrary L2 representatives is asserted. The operator, section integrability and output L2 membership are conclusions, not supplied premises. These operators use the same single global Z as all inherited path, initialization, invariance and bounded-duality conclusions. The bound1 is exact and independent of dimension, center, reference and horizon. The joint Borel assertion concerns Borel input G; arbitrary MemLp representatives receive the stated almost-everywhere conclusions. In addition, for each y,r the same operator family A has the following property. The literal phase reflection R(x,p)=(x,-p) preserves nu_y. Its canonical pullback J_y on real L2(nu_y) is the linear isometry defined by composition with R; for every L2 class f, (J_y f)(z)=f(R(z)) for nu_y-almost every z, and J_y(J_y f)=f. For every finite nonnegative T, the Hilbert adjoint of that same A_T satisfies A_T*=J_y A_T J_y as an equality of continuous real linear operators. Equivalently its pairing obeys <f,A_T g≥<J_y g,A_T(J_y f)> for all real L2 classes f,g. The pullback and its preservation/involution are proved conclusions; no supplied symmetry, operator relation, integrability or density hypothesis is added. The flip depends only on the displayed R and nu_y; the proof witness hR under y,r does not introduce reference or time dependence into J_y. The identity includes T=0 and rank zero. All representative equalities retain their stated almost-everywhere sense, with no common null set over all parameters or representatives. This is the full fixed-time real-L2 identity of Appendix A.1, Eq A.3, together with the exact inherited process and expectation contract. Strong continuity, restart/Markov/semigroup, complex-L2 extension, a separately existential kernel identification, actual momentum-averaged position operator, hypocoercivity, implementation errors, actual expected costs, actual-input composition and complete papers remain outside this result.

\[A_T^*=J A_T J.\]
Lean statement · actual_l2_flip_duality

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. Write H=E times E, pi_y=volume_E.tilted(-V_y), gamma=stdGaussian(E), so nu_y=pi_y times gamma. For the same single global actual Z described above, every y,r in E and every finite T>=0, define op_T G(z)=integral G(Z(y,r,z,T,w)) dP(w), a real Bochner integral, and endpoint_T(z,w)=Z(y,r,z,T,w). Then endpoint_T is measurable and its pushforward of nu_y times P is exactly nu_y. For every pair F,G:H->R of Borel measurable functions and finite real bounds C_F,C_G>=0 with |F(z)|<=C_F and |G(z)|<=C_G for all z, both z->F(z)*op_T G(z) and z->G(R(z))*op_T(F composed R)(z) are integrable against nu_y, and their real integrals are equal. Thus integral F(z)*op_T G(z) dnu_y(z) = integral G(R(z))*op_T(F composed R)(z) dnu_y(z). All these conclusions use the same Z, existentially chosen before all centers, references, horizons and observables. Products are phase first, clock input second. No process, kernel, finite mass, signed integrability, momentum symmetry or normalizability is a supplied premise. Dimension zero, T=0, vanishing test bounds, zero bounce rates, infinite waits and raw exceptional fallback remain included. Almost-sure initialization stays parameterwise; no uniform all-parameter null set or pointwise reversed path at jumps is asserted. For every Borel G:H->R, the total real clock expectation (y,r,z,T)->integral G(Z(y,r,z,T,w)) dP(w) is jointly Borel. If C is a finite nonnegative real number and |G(z)|<=C for all z, then for every y,r,z,T the clock section is P-integrable and the absolute value of this expectation is at most C. For every y,r in E there exists a family A indexed by finite nonnegative T, where A_T:L2(nu_y;R)->L2(nu_y;R) is a continuous real linear operator, A_0 is the identity and ||A_T||<=1 for every T. For every real function G with MemLp G 2 nu_y (almost-everywhere strong measurability and finite L2 seminorm), the section w->G(Z(y,r,z,T,w)) is P-integrable for nu_y-almost every z. The literal expectation op_T G belongs to L2(nu_y;R), and A_T[G]=[op_T G]. Thus integral |op_T G|^2 dnu_y <= integral |G|^2 dnu_y. Brackets denote equality classes modulo nu_y-almost-everywhere equality; no pointwise identification of arbitrary L2 representatives is asserted. The operator, section integrability and output L2 membership are conclusions, not supplied premises. These operators use the same single global Z as all inherited path, initialization, invariance and bounded-duality conclusions. The bound1 is exact and independent of dimension, center, reference and horizon. The joint Borel assertion concerns Borel input G; arbitrary MemLp representatives receive the stated almost-everywhere conclusions. In addition, for each y,r the same operator family A has the following property. The literal phase reflection R(x,p)=(x,-p) preserves nu_y. Its canonical pullback J_y on real L2(nu_y) is the linear isometry defined by composition with R; for every L2 class f, (J_y f)(z)=f(R(z)) for nu_y-almost every z, and J_y(J_y f)=f. For every finite nonnegative T, the Hilbert adjoint of that same A_T satisfies A_T*=J_y A_T J_y as an equality of continuous real linear operators. Equivalently its pairing obeys <f,A_T g>=<J_y g,A_T(J_y f)> for all real L2 classes f,g. The pullback and its preservation/involution are proved conclusions; no supplied symmetry, operator relation, integrability or density hypothesis is added. The flip depends only on the displayed R and nu_y; the proof witness hR under y,r does not introduce reference or time dependence into J_y. The identity includes T=0 and rank zero. All representative equalities retain their stated almost-everywhere sense, with no common null set over all parameters or representatives. This is the full fixed-time real-L2 identity of Appendix A.1, Eq A.3, together with the exact inherited process and expectation contract. Strong continuity, restart/Markov/semigroup, complex-L2 extension, a separately existential kernel identification, actual momentum-averaged position operator, hypocoercivity, implementation errors, actual expected costs, actual-input composition and complete papers remain outside this result.

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_l2_flip_duality
    {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_l2_flip_statement hα hαβ hV hH hη hβη

Exact module and namespace context

Full Lean proposition (definition) · actual_l2_flip_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_l2_flip_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 xRef : E, ∀ T : ℝ≥0,
        let op : ((E × E) → ℝ) → (E × E) → ℝ :=
          fun G z => ∫ w, G (Z y xRef z T w) ∂P
        let endpoint : (E × E) × (ℕ → ℝ) → E × E :=
          fun a => Z y xRef a.1 T a.2
        MeasurePreserving endpoint ((nu y).prod P) (nu y) ∧
        ∀ F G : (E × E) → ℝ, ∀ C_F C_G : ℝ,
          Measurable F → Measurable G → 0 ≤ C_F → 0 ≤ C_G →
          (∀ z, |F z| ≤ C_F) → (∀ z, |G z| ≤ C_G) →
          Integrable (fun z => F z * op G z) (nu y) ∧
          Integrable (fun z => G (R z) * op (fun a => F (R a)) z) (nu y) ∧
          (∫ z, F z * op G z ∂nu y) =
            ∫ z, G (R z) * op (fun a => F (R a)) z ∂nu y) ∧
      (∀ G : (E × E) → ℝ, Measurable G →
        Measurable (fun a : ((E × E) × (E × E)) × ℝ≥0 =>
          ∫ w, G (Z a.1.1.1 a.1.1.2 a.1.2 a.2 w) ∂P) ∧
        ∀ C : ℝ, 0 ≤ C → (∀ z, |G z| ≤ C) →
          ∀ y xRef : E, ∀ z : E × E, ∀ T : ℝ≥0,
            Integrable (fun w => G (Z y xRef z T w)) P ∧
            |∫ w, G (Z y xRef z T w) ∂P| ≤ C) ∧
      (∀ y xRef : E,
        ∃ A : ℝ≥0 → (Lp ℝ 2 (nu y) →L[ℝ] Lp ℝ 2 (nu y)),
          A 0 = ContinuousLinearMap.id ℝ (Lp ℝ 2 (nu y)) ∧
          (∀ T : ℝ≥0, ‖A T‖ ≤ 1 ∧
            ∀ G : (E × E) → ℝ, ∀ hG : MemLp G 2 (nu y),
              let opG : (E × E) → ℝ := fun z => ∫ w, G (Z y xRef z T w) ∂P
              (∀ᵐ z ∂nu y, Integrable (fun w => G (Z y xRef z T w)) P) ∧
              (∃ hOp : MemLp opG 2 (nu y), A T (hG.toLp G) = hOp.toLp opG) ∧
              (∫ z, |opG z| ^ 2 ∂nu y) ≤ ∫ z, |G z| ^ 2 ∂nu y) ∧
          ∃ hR : MeasurePreserving R (nu y) (nu y),
            let J : Lp ℝ 2 (nu y) →ₗᵢ[ℝ] Lp ℝ 2 (nu y) :=
              Lp.compMeasurePreservingₗᵢ ℝ R hR
            (∀ f : Lp ℝ 2 (nu y),
              (J f : (E × E) → ℝ) =ᵐ[nu y] fun z => f (R z)) ∧
            (∀ f : Lp ℝ 2 (nu y), J (J f) = f) ∧
            ∀ T : ℝ≥0, (A T).adjoint =
              J.toContinuousLinearMap.comp ((A T).comp J.toContinuousLinearMap))

set_option maxHeartbeats 2200000
set_option maxRecDepth 12000

Exact module and namespace context

Proof roadmap

  1. 1Retain one actual process and the same expectation family

    Invoke the previous actual expectation theorem once. Carry its global process, live arcs, fallback, initialization, invariant phase law, bounded duality, Borel expectation and every L2 contraction conclusion. Fix y,r and use precisely its family A; the proof never chooses another path or operator.

  2. 2Preserve the actual phase law under momentum reflection

    The centered Gaussian is invariant under the linear isometry p↦−p. The position coordinate is unchanged. Apply the product-map identity to the actual tilted position measure and Gaussian. Mathlib supplies finite-factor instances for tilted and Gaussian measures, so no extra probability or integrability assumption enters this argument.

  3. 3Construct the canonical involutive L2 isometry

    Use the measure-preserving pullback J on L2 classes. Its canonical representative equals f∘R almost everywhere. Transport that equality through R and use R(Rz)=z; Lp extensionality proves J²=I. The linear-isometry type itself certifies norm preservation.

  4. 4Expose the inherited actual expectation representative

    For a MemLp raw function G, take the existing quotient identity for A_T[G]. Its output toLp representative equals the literal clock expectation almost everywhere. This uses the existing same-Z identity and does not assume a new integral formula.

  5. 5Choose simple representatives and match every pullback class

    Each L2 simple class has a measurable finite-range representative F with its own MemLp witness. Identify [F] with f. Measure preservation transports MemLp to F∘R and transports representative equalities. Consequently Jf=[F∘R], Jg agrees with G∘R, and both operator representatives match their actual expectations.

  6. 6Apply the bounded signed duality to these representatives

    Finite range supplies finite norm bounds C_F and C_G; replace them by max(C,0) for the inherited nonnegative-bound contract. Apply the actual bounded signed identity to F,G. Substitute the proved representative equalities into the L2 inner-product integrals, obtaining the pairing identity for the two simple classes.

  7. 7Extend both arguments by L2 density

    L2 simple classes form a dense subset. Both pairings are continuous jointly in (f,g), since the inner product, A_T and J are continuous. Their equality set is closed and contains every pair of simple classes; the two-variable dense-range induction therefore proves equality for all real L2 classes.

  8. 8Identify the Hilbert adjoint

    By the adjoint defining relation and the full pairing identity, <A_T* f,g≥<Jg,A_TJf>. The isometry and involution move J across the inner product; real symmetry turns this into <JA_TJf,g>. Inner-product extensionality for each f, followed by operator extensionality, gives the claimed equality of the same operators.

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.
  • A single global actual process is constructed in the conclusion, with the literal joint measurability, arc/fallback and parameterwise almost-sure initialization contracts; every y,r and finite nonnegative T is included.
  • The universal bounded-observable conclusion ranges over measurable real F,G and finite nonnegative C_F,C_G with pointwise absolute-value bounds. These are test domains, not extra assumptions on the sampler.
  • For the L2 conclusion G is any real function with MemLp G 2 nu_y. For joint Borel dependence G is Borel; every-section L1 additionally uses a finite nonnegative pointwise bound. Operator existence, integrability, output membership and bound1 are conclusions.
  • All actual algorithm, clock and Gibbs phase objects are literal. No supplied Z/kernel/operator, integrability, normalizer, momentum symmetry, restart or Markov premise.

Mathematical proof

1. Retain one actual process and the same expectation family

Invoke the previous actual expectation theorem once. Carry its global process, live arcs, fallback, initialization, invariant phase law, bounded duality, Borel expectation and every L2 contraction conclusion. Fix y,r and use precisely its family A; the proof never chooses another path or operator.

\[Z\text{ fixed};\quad A_T[G]=[\operatorname{op}_TG],\quad A_0=I,\quad\|A_T\|\le1.\]
Corresponding Lean step
  obtain ⟨Z, hZm, hZa, hZf, hZ0, h106, hBorel, h107⟩ :=
    AutoSamplingTheory.ExampleCases.ProximalBPS.ActualL2Expectation.actual_l2_expectation_contraction
      hα hαβ hV hH hη hβη
  refine ⟨Z, hZm, hZa, hZf, hZ0, h106, hBorel, ?_⟩
  intro y xRef
  obtain ⟨L, hL0, hL⟩ := h107 y xRef
  refine ⟨L, hL0, hL, ?_⟩

ASTIS expansion of the source dense-subspace extension for full real-L2 flip duality. Exact compiled region; original six analytic assumptions and same global process are unchanged.

2. Preserve the actual phase law under momentum reflection

The centered Gaussian is invariant under the linear isometry p↦−p. The position coordinate is unchanged. Apply the product-map identity to the actual tilted position measure and Gaussian. Mathlib supplies finite-factor instances for tilted and Gaussian measures, so no extra probability or integrability assumption enters this argument.

\[R(x,p)=(x,-p),\qquad R_*\bigl(\pi_y\otimes\gamma\bigr)=\pi_y\otimes\gamma=\nu_y.\]
Corresponding Lean step
  have hRm : Measurable R := by dsimp [R]; fun_prop
  have hneg : Measure.map (fun p : E => -p) (stdGaussian E) = stdGaussian E := by
    simpa using (stdGaussian_map (LinearIsometryEquiv.neg ℝ (E := E)))
  have hR : MeasurePreserving R (nu y) (nu y) := by
    refine ⟨hRm, ?_⟩
    change Measure.map (Prod.map id (fun p : E => -p))
      (((volume : Measure E).tilted (fun x => -Vy y x)).prod (stdGaussian E)) = _
    rw [← Measure.map_prod_map _ _ measurable_id (by fun_prop), hneg, Measure.map_id]

ASTIS expansion of the source dense-subspace extension for full real-L2 flip duality. Exact compiled region; original six analytic assumptions and same global process are unchanged.

3. Construct the canonical involutive L2 isometry

Use the measure-preserving pullback J on L2 classes. Its canonical representative equals f∘R almost everywhere. Transport that equality through R and use R(Rz)=z; Lp extensionality proves J²=I. The linear-isometry type itself certifies norm preservation.

\[Jf=f\circ R\quad\nu_y\text{-a.e.},\qquad\|Jf\|_2=\|f\|_2,\qquad J^2=I.\]
Corresponding Lean step
  refine ⟨hR, ?_⟩
  intro J
  have hJrep (f : Lp ℝ 2 (nu y)) :
      (J f : (E × E) → ℝ) =ᵐ[nu y] fun z => f (R z) :=
    Lp.coeFn_compMeasurePreserving f hR
  have hJJ (f : Lp ℝ 2 (nu y)) : J (J f) = f := by
    apply Lp.ext
    filter_upwards [hJrep (J f), hR.quasiMeasurePreserving.ae_eq_comp (hJrep f)] with z hz hz'
    simpa only [Function.comp_def, R, neg_neg] using hz.trans hz'
  refine ⟨hJrep, hJJ, ?_⟩
  intro T

ASTIS expansion of the source dense-subspace extension for full real-L2 flip duality. Exact compiled region; original six analytic assumptions and same global process are unchanged.

4. Expose the inherited actual expectation representative

For a MemLp raw function G, take the existing quotient identity for A_T[G]. Its output toLp representative equals the literal clock expectation almost everywhere. This uses the existing same-Z identity and does not assume a new integral formula.

\[A_T[G](z)=\int G(Z(y,r,z,T,w))\,dP(w)\quad\nu_y\text{-a.e.}\]
Corresponding Lean step
  have hrep (G : (E × E) → ℝ) (hG : MemLp G 2 (nu y)) :
      (L T (hG.toLp G) : (E × E) → ℝ) =ᵐ[nu y]
        fun z => ∫ w, G (Z y xRef z T w) ∂P := by
    obtain ⟨_, ⟨hOp, he⟩, _⟩ := (hL T).2 G hG
    rw [he]
    exact hOp.coeFn_toLp

ASTIS expansion of the source dense-subspace extension for full real-L2 flip duality. Exact compiled region; original six analytic assumptions and same global process are unchanged.

5. Choose simple representatives and match every pullback class

Each L2 simple class has a measurable finite-range representative F with its own MemLp witness. Identify [F] with f. Measure preservation transports MemLp to F∘R and transports representative equalities. Consequently Jf=[F∘R], Jg agrees with G∘R, and both operator representatives match their actual expectations.

\[[F]=f,\quad[G]=g,\quad[F\circ R]=Jf,\quad Jg=G\circ R\ \nu_y\text{-a.e.}\]
Corresponding Lean step
  have hsimple (f g : Lp.simpleFunc ℝ 2 (nu y)) :
      ⟪(f : Lp ℝ 2 (nu y)), L T g⟫_ℝ = ⟪J g, L T (J f)⟫_ℝ := by
    let F := Lp.simpleFunc.toSimpleFunc f
    let G := Lp.simpleFunc.toSimpleFunc g
    have hF : MemLp F 2 (nu y) := Lp.simpleFunc.memLp f
    have hG : MemLp G 2 (nu y) := Lp.simpleFunc.memLp g
    have hFrep : (f : (E × E) → ℝ) =ᵐ[nu y] F :=
      (Lp.simpleFunc.toSimpleFunc_eq_toFun f).symm
    have hGrep : (g : (E × E) → ℝ) =ᵐ[nu y] G :=
      (Lp.simpleFunc.toSimpleFunc_eq_toFun g).symm
    have hFto : hF.toLp F = (f : Lp ℝ 2 (nu y)) := by
      apply Lp.ext
      exact hF.coeFn_toLp.trans hFrep.symm
    have hGto : hG.toLp G = (g : Lp ℝ 2 (nu y)) := by
      apply Lp.ext
      exact hG.coeFn_toLp.trans hGrep.symm
    have hFR : MemLp (fun z => F (R z)) 2 (nu y) := hF.comp_measurePreserving hR
    have hJfto : J f = hFR.toLp (fun z => F (R z)) := by
      apply Lp.ext
      exact ((hJrep f).trans (hR.quasiMeasurePreserving.ae_eq_comp hFrep)).trans
        hFR.coeFn_toLp.symm
    have hJg : (J g : (E × E) → ℝ) =ᵐ[nu y] fun z => G (R z) :=
      (hJrep g).trans (hR.quasiMeasurePreserving.ae_eq_comp hGrep)
    have hLg := hrep G hG
    rw [hGto] at hLg
    have hLJf := hrep (fun z => F (R z)) hFR
    rw [← hJfto] at hLJf

ASTIS expansion of the source dense-subspace extension for full real-L2 flip duality. Exact compiled region; original six analytic assumptions and same global process are unchanged.

6. Apply the bounded signed duality to these representatives

Finite range supplies finite norm bounds C_F and C_G; replace them by max(C,0) for the inherited nonnegative-bound contract. Apply the actual bounded signed identity to F,G. Substitute the proved representative equalities into the L2 inner-product integrals, obtaining the pairing identity for the two simple classes.

\[\langle f,A_Tg\rangle=\int F\operatorname{op}_TG\,d\nu_y=\int(G\circ R)\operatorname{op}_T(F\circ R)\,d\nu_y=\langle Jg,A_TJf\rangle.\]
Corresponding Lean step
    obtain ⟨CF, hCF⟩ := F.exists_forall_norm_le
    obtain ⟨CG, hCG⟩ := G.exists_forall_norm_le
    have hBF : ∀ z, |F z| ≤ max CF 0 := by
      intro z
      exact le_trans (by simpa only [Real.norm_eq_abs] using hCF z) (le_max_left _ _)
    have hBG : ∀ z, |G z| ≤ max CG 0 := by
      intro z
      exact le_trans (by simpa only [Real.norm_eq_abs] using hCG z) (le_max_left _ _)
    have hd := ((h106 y xRef T).2 F G (max CF 0) (max CG 0)
      F.measurable G.measurable (le_max_right _ _) (le_max_right _ _) hBF hBG).2.2
    calc
      ⟪(f : Lp ℝ 2 (nu y)), L T g⟫_ℝ =
          ∫ z, F z * (∫ w, G (Z y xRef z T w) ∂P) ∂nu y := by
        rw [L2.inner_def]
        apply integral_congr_ae
        filter_upwards [hFrep, hLg] with z hz hz'
        simp only [RCLike.inner_apply, conj_trivial, hz, hz', mul_comm]
      _ = ∫ z, G (R z) * (∫ w, F (R (Z y xRef z T w)) ∂P) ∂nu y := hd
      _ = ⟪J g, L T (J f)⟫_ℝ := by
        rw [L2.inner_def]
        apply integral_congr_ae
        filter_upwards [hJg, hLJf] with z hz hz'
        simp only [RCLike.inner_apply, conj_trivial, hz, hz', mul_comm]

ASTIS expansion of the source dense-subspace extension for full real-L2 flip duality. Exact compiled region; original six analytic assumptions and same global process are unchanged.

7. Extend both arguments by L2 density

L2 simple classes form a dense subset. Both pairings are continuous jointly in (f,g), since the inner product, A_T and J are continuous. Their equality set is closed and contains every pair of simple classes; the two-variable dense-range induction therefore proves equality for all real L2 classes.

\[\forall f,g\in L^2(\nu_y;\mathbb R),\qquad\langle f,A_Tg\rangle=\langle Jg,A_TJf\rangle.\]
Corresponding Lean step
  have hpair (f g : Lp ℝ 2 (nu y)) :
      ⟪f, L T g⟫_ℝ = ⟪J g, L T (J f)⟫_ℝ := by
    apply (Lp.simpleFunc.denseRange (E := ℝ) (μ := nu y) (p := 2) (by norm_num)).induction_on₂
      (p := fun f g => ⟪f, L T g⟫_ℝ = ⟪J g, L T (J f)⟫_ℝ) _ hsimple f g
    exact isClosed_eq (continuous_fst.inner ((L T).continuous.comp continuous_snd))
      ((J.continuous.comp continuous_snd).inner
        ((L T).continuous.comp (J.continuous.comp continuous_fst)))

ASTIS expansion of the source dense-subspace extension for full real-L2 flip duality. Exact compiled region; original six analytic assumptions and same global process are unchanged.

8. Identify the Hilbert adjoint

By the adjoint defining relation and the full pairing identity, <A_T* f,g≥<Jg,A_TJf>. The isometry and involution move J across the inner product; real symmetry turns this into <JA_TJf,g>. Inner-product extensionality for each f, followed by operator extensionality, gives the claimed equality of the same operators.

\[A_T^*=J A_T J.\]
Corresponding Lean step
  apply ContinuousLinearMap.ext
  intro f
  apply ext_inner_right ℝ
  intro g
  calc
    ⟪(L T).adjoint f, g⟫_ℝ = ⟪f, L T g⟫_ℝ := (L T).adjoint_inner_left g f
    _ = ⟪J g, L T (J f)⟫_ℝ := hpair f g
    _ = ⟪g, J (L T (J f))⟫_ℝ := by
      rw [← J.inner_map_map g (J (L T (J f))), hJJ]
    _ = ⟪J (L T (J f)), g⟫_ℝ := real_inner_comm _ _

ASTIS expansion of the source dense-subspace extension for full real-L2 flip duality. Exact compiled region; original six analytic assumptions and same global process 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_l2_flip_duality

Retain one actual process and the same expectation family; Preserve the actual phase law under momentum reflection; Construct the canonical involutive L2 isometry; Expose the inherited actual expectation representative; Choose simple representatives and match every pullback class; Apply the bounded signed duality to these representatives; Extend both arguments by L2 density; Identify the Hilbert adjoint

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_l2_flip_duality
    {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_l2_flip_statement hα hαβ hV hH hη hβη := by
  classical
  unfold actual_l2_flip_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, h106, hBorel, h107⟩ :=
    AutoSamplingTheory.ExampleCases.ProximalBPS.ActualL2Expectation.actual_l2_expectation_contraction
      hα hαβ hV hH hη hβη
  refine ⟨Z, hZm, hZa, hZf, hZ0, h106, hBorel, ?_⟩
  intro y xRef
  obtain ⟨L, hL0, hL⟩ := h107 y xRef
  refine ⟨L, hL0, hL, ?_⟩
  have hRm : Measurable R := by dsimp [R]; fun_prop
  have hneg : Measure.map (fun p : E => -p) (stdGaussian E) = stdGaussian E := by
    simpa using (stdGaussian_map (LinearIsometryEquiv.neg ℝ (E := E)))
  have hR : MeasurePreserving R (nu y) (nu y) := by
    refine ⟨hRm, ?_⟩
    change Measure.map (Prod.map id (fun p : E => -p))
      (((volume : Measure E).tilted (fun x => -Vy y x)).prod (stdGaussian E)) = _
    rw [← Measure.map_prod_map _ _ measurable_id (by fun_prop), hneg, Measure.map_id]
  refine ⟨hR, ?_⟩
  intro J
  have hJrep (f : Lp ℝ 2 (nu y)) :
      (J f : (E × E) → ℝ) =ᵐ[nu y] fun z => f (R z) :=
    Lp.coeFn_compMeasurePreserving f hR
  have hJJ (f : Lp ℝ 2 (nu y)) : J (J f) = f := by
    apply Lp.ext
    filter_upwards [hJrep (J f), hR.quasiMeasurePreserving.ae_eq_comp (hJrep f)] with z hz hz'
    simpa only [Function.comp_def, R, neg_neg] using hz.trans hz'
  refine ⟨hJrep, hJJ, ?_⟩
  intro T
  have hrep (G : (E × E) → ℝ) (hG : MemLp G 2 (nu y)) :
      (L T (hG.toLp G) : (E × E) → ℝ) =ᵐ[nu y]
        fun z => ∫ w, G (Z y xRef z T w) ∂P := by
    obtain ⟨_, ⟨hOp, he⟩, _⟩ := (hL T).2 G hG
    rw [he]
    exact hOp.coeFn_toLp
  have hsimple (f g : Lp.simpleFunc ℝ 2 (nu y)) :
      ⟪(f : Lp ℝ 2 (nu y)), L T g⟫_ℝ = ⟪J g, L T (J f)⟫_ℝ := by
    let F := Lp.simpleFunc.toSimpleFunc f
    let G := Lp.simpleFunc.toSimpleFunc g
    have hF : MemLp F 2 (nu y) := Lp.simpleFunc.memLp f
    have hG : MemLp G 2 (nu y) := Lp.simpleFunc.memLp g
    have hFrep : (f : (E × E) → ℝ) =ᵐ[nu y] F :=
      (Lp.simpleFunc.toSimpleFunc_eq_toFun f).symm
    have hGrep : (g : (E × E) → ℝ) =ᵐ[nu y] G :=
      (Lp.simpleFunc.toSimpleFunc_eq_toFun g).symm
    have hFto : hF.toLp F = (f : Lp ℝ 2 (nu y)) := by
      apply Lp.ext
      exact hF.coeFn_toLp.trans hFrep.symm
    have hGto : hG.toLp G = (g : Lp ℝ 2 (nu y)) := by
      apply Lp.ext
      exact hG.coeFn_toLp.trans hGrep.symm
    have hFR : MemLp (fun z => F (R z)) 2 (nu y) := hF.comp_measurePreserving hR
    have hJfto : J f = hFR.toLp (fun z => F (R z)) := by
      apply Lp.ext
      exact ((hJrep f).trans (hR.quasiMeasurePreserving.ae_eq_comp hFrep)).trans
        hFR.coeFn_toLp.symm
    have hJg : (J g : (E × E) → ℝ) =ᵐ[nu y] fun z => G (R z) :=
      (hJrep g).trans (hR.quasiMeasurePreserving.ae_eq_comp hGrep)
    have hLg := hrep G hG
    rw [hGto] at hLg
    have hLJf := hrep (fun z => F (R z)) hFR
    rw [← hJfto] at hLJf
    obtain ⟨CF, hCF⟩ := F.exists_forall_norm_le
    obtain ⟨CG, hCG⟩ := G.exists_forall_norm_le
    have hBF : ∀ z, |F z| ≤ max CF 0 := by
      intro z
      exact le_trans (by simpa only [Real.norm_eq_abs] using hCF z) (le_max_left _ _)
    have hBG : ∀ z, |G z| ≤ max CG 0 := by
      intro z
      exact le_trans (by simpa only [Real.norm_eq_abs] using hCG z) (le_max_left _ _)
    have hd := ((h106 y xRef T).2 F G (max CF 0) (max CG 0)
      F.measurable G.measurable (le_max_right _ _) (le_max_right _ _) hBF hBG).2.2
    calc
      ⟪(f : Lp ℝ 2 (nu y)), L T g⟫_ℝ =
          ∫ z, F z * (∫ w, G (Z y xRef z T w) ∂P) ∂nu y := by
        rw [L2.inner_def]
        apply integral_congr_ae
        filter_upwards [hFrep, hLg] with z hz hz'
        simp only [RCLike.inner_apply, conj_trivial, hz, hz', mul_comm]
      _ = ∫ z, G (R z) * (∫ w, F (R (Z y xRef z T w)) ∂P) ∂nu y := hd
      _ = ⟪J g, L T (J f)⟫_ℝ := by
        rw [L2.inner_def]
        apply integral_congr_ae
        filter_upwards [hJg, hLJf] with z hz hz'
        simp only [RCLike.inner_apply, conj_trivial, hz, hz', mul_comm]
  have hpair (f g : Lp ℝ 2 (nu y)) :
      ⟪f, L T g⟫_ℝ = ⟪J g, L T (J f)⟫_ℝ := by
    apply (Lp.simpleFunc.denseRange (E := ℝ) (μ := nu y) (p := 2) (by norm_num)).induction_on₂
      (p := fun f g => ⟪f, L T g⟫_ℝ = ⟪J g, L T (J f)⟫_ℝ) _ hsimple f g
    exact isClosed_eq (continuous_fst.inner ((L T).continuous.comp continuous_snd))
      ((J.continuous.comp continuous_snd).inner
        ((L T).continuous.comp (J.continuous.comp continuous_fst)))
  apply ContinuousLinearMap.ext
  intro f
  apply ext_inner_right ℝ
  intro g
  calc
    ⟪(L T).adjoint f, g⟫_ℝ = ⟪f, L T g⟫_ℝ := (L T).adjoint_inner_left g f
    _ = ⟪J g, L T (J f)⟫_ℝ := hpair f g
    _ = ⟪g, J (L T (J f))⟫_ℝ := by
      rw [← J.inner_map_map g (J (L T (J f))), hJJ]
    _ = ⟪J (L T (J f)), g⟫_ℝ := real_inner_comm _ _

#print axioms actual_l2_flip_duality
end
end AutoSamplingTheory.ExampleCases.ProximalBPS.ActualL2FlipDuality

Exact module and namespace context

Source assumptions versus formal assumptions

SourceActual LeanDifference kindWhy it matters
Appendix A.1 Eq A.3 and its dense-subspace extension.Full same-process real-L2 adjoint equals canonical momentum-flip conjugation, retaining all107 conclusions.sameCanonical flip, simple representatives, continuous density and adjoint uniqueness are internal dependencies.
Finite-dimensional Euclidean phase.Finite real inner-product Borel space including rank zero.generalizationCanonical volume/Gaussian formulation preserves the source formulas.
Later process and sampler properties.Fixed-time real-L2 Eq A.3 is closed; semigroup, strong continuity and later sampler results remain open.unresolvedFull fixed-time real L2 flip adjoint identity with all107 conclusions. Strong continuity, restart/Markov/semigroup, separate kernel-witness identification, momentum-averaged position operator, hypocoercivity, implementation errors, actual expected costs, composition and all four full papers remain open.

Full fixed-time real L2 flip adjoint identity with all107 conclusions. Strong continuity, restart/Markov/semigroup, separate kernel-witness identification, momentum-averaged position operator, hypocoercivity, implementation errors, actual expected costs, composition and all four full papers remain open.

Encoder–denoiser: accepted · equivalent-after-elaboration

Detected semantic differences

  • domains: Explicit real Hilbert/Borel realization includes rank zero; complex-L2 is outside the accepted boundary. — Header/Prop ambient telescope and publication explicit realL2 boundary
  • conclusion: ASTIS exposes the canonical flip and dense-subspace extension as derived outputs/internal proofs; no source ingredient becomes a premise. — Source-first expectation and exact194–285 proof coverage
  • scopes: Actual total raw-path and AE quotient contracts remain explicit; source fixed-time identity grants no restart/semigroup or whole-paper completion. — Fresh blind reconstruction scopes and exactProp outputs

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
  • Full fixed-time real L2 flip adjoint identity with all107 conclusions. Strong continuity, restart/Markov/semigroup, separate kernel-witness identification, momentum-averaged position operator, hypocoercivity, implementation errors, actual expected costs, composition and all four full papers remain open.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

  • stdGaussian_map
  • Measure.map_prod_map
  • Lp.compMeasurePreservingₗᵢ
  • Lp.coeFn_compMeasurePreserving
  • Measure.QuasiMeasurePreserving.ae_eq_comp
  • Lp.simpleFunc.toSimpleFunc
  • Lp.simpleFunc.memLp
  • SimpleFunc.exists_forall_norm_le
  • Lp.simpleFunc.denseRange
  • DenseRange.induction_on₂
  • L2.inner_def
  • isClosed_eq
  • LinearIsometry.inner_map_map
  • ContinuousLinearMap.adjoint_inner_left
  • ext_inner_right
  • Lp.ext

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 Full actual real-L2 momentum-flip identity