Actual PBPS bounded Gibbs duality and fixed-time invariance
AutoSamplingTheory.ExampleCases.ProximalBPS.ActualBoundedGibbsDuality.actual_bounded_gibbs_duality · theorem · Teaching coverage
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. The phase-invariance conclusion is fixed-time stationarity of the actual output under Gibbs initialization. It does not assert Markov/restart, Chapman-Kolmogorov, an L2 operator/domain identity, identification with a different existential kernel witness, hypocoercivity, implementation accuracy or actual expected oracle costs. Full paper results and actual-input composition remain open.
Lean statement · actual_bounded_gibbs_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. The phase-invariance conclusion is fixed-time stationarity of the actual output under Gibbs initialization. It does not assert Markov/restart, Chapman-Kolmogorov, an L2 operator/domain identity, identification with a different existential kernel witness, hypocoercivity, implementation accuracy or actual expected oracle costs. Full paper results and actual-input composition remain open.
Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.
theorem actual_bounded_gibbs_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_bounded_gibbs_duality_statement hα hαβ hV hH hη hβηFull Lean proposition (definition) · actual_bounded_gibbs_duality_statement
This literal definition stores the complete proposition asserted above. It supplies no mathematical proof or additional hypothesis; the theorem proof must establish its value.
Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.
private def actual_bounded_gibbs_duality_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)
set_option maxHeartbeats 1800000
set_option maxRecDepth 10000Proof roadmap
- 1Keep the same global actual process
Consume the actual countable endpoint-law producer once. Retain the exact joint measurability, live-arc, raw fallback and parameterwise almost-sure initialization of its single global Z. All subsequent maps and test integrals use this witness.
- 2Recover the actual probability laws and endpoint reversal
Write H=E×E, pi_y=volume_E.tilted(-V_y), gamma=stdGaussian(E), and nu_y=pi_y times gamma. The normalization and clock producers prove that nu_y and P are probability measures. Joint Z makes endpoint and M measurable. The countable-law producer gives probability of Q and J-preservation; these are internal dependencies.
- 3Prove momentum-flip symmetry of the actual phase law
Negation is a linear isometry of E, so it preserves the standard Gaussian, including dimension zero. Product pushforward leaves the tilted position factor unchanged and negates only the momentum factor. Thus the literal R is measurable and preserves nu_y.
- 4Identify the actual fixed-time Gibbs marginal
The initial marginal of Q is nu_y because P has mass one. Compose the preserving maps M, J, first projection and R. Since R is an involution, R composed fst composed J is the second projection; the resulting map is the actual endpoint. This is the explicitly recorded direct-marginal implementation of the source stationarity consequence. The printed F=1 argument follows from the bounded identity proved below.
- 5Derive product integrability from the observable bounds
Fix arbitrary measurable real F,G with finite nonnegative bounds C_F,C_G. Their actual-input product H_FG(z,w)=F(z)G(Z_T(z,w)) is measurable and bounded by C_F C_G. The input product is probability, so this bound proves honest real Bochner integrability without any integrability premise.
- 6Use signed Fubini and pushforward for the test identity
Product integrability yields integrability of the inner integral. Pull F(z) through the clock integral, then apply signed Fubini. The measurable pushforward M identifies the resulting integral with the endpoint-pair test under Q. This proves both the outer L1 conclusion and its exact integral representation.
- 7Apply the same integrability argument to the flipped tests
Apply the already proved test identity first to F,G and then to G composed R,F composed R. Measurability of R and the original pointwise bounds give all required hypotheses. Both displayed outer integrals are therefore integrable, including when either bound vanishes.
- 8Transfer endpoint reversal to bounded signed duality
Use the measurable map J and J_*Q=Q in the real integral-map identity for F(a)G(b). After the flipped swap the integrand is F(Rb)G(Ra); commute the real factors and combine the two test representations. No unbounded observable or L2 extension is inferred.
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.
- All actual algorithm, clock and Gibbs phase objects are defined literally; no supplied Z/kernel, integrability, normalizer, momentum symmetry, restart or Markov premise.
Mathematical proof
1. Keep the same global actual process
Consume the actual countable endpoint-law producer once. Retain the exact joint measurability, live-arc, raw fallback and parameterwise almost-sure initialization of its single global Z. All subsequent maps and test integrals use this witness.
Corresponding Lean step
obtain ⟨Z, hZm, hZa, hZf, hZ0, h105⟩ :=
AutoSamplingTheory.ExampleCases.ProximalBPS.ActualCountableEndpointLaw.actual_countable_endpoint_law
hα hαβ hV hH hη hβη
refine ⟨Z, hZm, hZa, hZf, hZ0, ?_⟩
intro y r T op endpoint
ASTIS completion of bounded signed averaging and fixed-time stationarity. Exact compiled region; the original six analytic assumptions are unchanged.
2. Recover the actual probability laws and endpoint reversal
Write H=E×E, pi_y=volume_E.tilted(-V_y), gamma=stdGaussian(E), and nu_y=pi_y times gamma. The normalization and clock producers prove that nu_y and P are probability measures. Joint Z makes endpoint and M measurable. The countable-law producer gives probability of Q and J-preservation; these are internal dependencies.
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 hemb : Measurable (fun a : (E × E) × (ℕ → ℝ) => (((y, r), a.1), T, a.2)) :=
(measurable_const.prodMk measurable_fst).prodMk (measurable_const.prodMk measurable_snd)
have he : Measurable endpoint := hZm.comp hemb
let M : (E × E) × (ℕ → ℝ) → (E × E) × (E × E) := fun a => (a.1, endpoint a)
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 a => (R a.2, R a.1)
have hM : Measurable M := measurable_fst.prodMk he
have hJ : MeasurePreserving J Q Q := (h105 y r T).2.2
letI : IsProbabilityMeasure Q := (h105 y r T).2.1
ASTIS completion of bounded signed averaging and fixed-time stationarity. Exact compiled region; the original six analytic assumptions are unchanged.
3. Prove momentum-flip symmetry of the actual phase law
Negation is a linear isometry of E, so it preserves the standard Gaussian, including dimension zero. Product pushforward leaves the tilted position factor unchanged and negates only the momentum factor. Thus the literal R is measurable and preserves 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 completion of bounded signed averaging and fixed-time stationarity. Exact compiled region; the original six analytic assumptions are unchanged.
4. Identify the actual fixed-time Gibbs marginal
The initial marginal of Q is nu_y because P has mass one. Compose the preserving maps M, J, first projection and R. Since R is an involution, R composed fst composed J is the second projection; the resulting map is the actual endpoint. This is the explicitly recorded direct-marginal implementation of the source stationarity consequence. The printed F=1 argument follows from the bounded identity proved below.
Corresponding Lean step
have hMP : MeasurePreserving M ((nu y).prod P) Q := ⟨hM, rfl⟩
have hfst : MeasurePreserving Prod.fst Q (nu y) := by
refine ⟨measurable_fst, ?_⟩
change Measure.map Prod.fst (Measure.map M ((nu y).prod P)) = nu y
rw [Measure.map_map measurable_fst hM]
change Measure.map Prod.fst ((nu y).prod P) = nu y
simp only [Measure.map_fst_prod, measure_univ, one_smul]
have hinvariant : MeasurePreserving endpoint ((nu y).prod P) (nu y) := by
have h := hR.comp ((hfst.comp hJ).comp hMP)
simpa only [Function.comp_def, M, J, R, neg_neg] using h
refine ⟨hinvariant, ?_⟩
ASTIS completion of bounded signed averaging and fixed-time stationarity. Exact compiled region; the original six analytic assumptions are unchanged.
5. Derive product integrability from the observable bounds
Fix arbitrary measurable real F,G with finite nonnegative bounds C_F,C_G. Their actual-input product H_FG(z,w)=F(z)G(Z_T(z,w)) is measurable and bounded by C_F C_G. The input product is probability, so this bound proves honest real Bochner integrability without any integrability premise.
Corresponding Lean step
have htest (F G : (E × E) → ℝ) (CF CG : ℝ)
(hF : Measurable F) (hG : Measurable G) (hCF : 0 ≤ CF) (hCG : 0 ≤ CG)
(hFb : ∀ z, |F z| ≤ CF) (hGb : ∀ z, |G z| ≤ CG) :
Integrable (fun z => F z * op G z) (nu y) ∧
(∫ z, F z * op G z ∂nu y) = ∫ a, F a.1 * G a.2 ∂Q := by
let H : (E × E) × (ℕ → ℝ) → ℝ := fun a => F a.1 * G (endpoint a)
have hHm : Measurable H := (hF.comp measurable_fst).mul (hG.comp he)
have hHi : Integrable H ((nu y).prod P) :=
Integrable.of_bound hHm.aestronglyMeasurable (CF * CG)
(Filter.Eventually.of_forall fun a => by
change |F a.1 * G (endpoint a)| ≤ CF * CG
rw [abs_mul]
exact mul_le_mul (hFb a.1) (hGb (endpoint a)) (abs_nonneg _) hCF)
ASTIS completion of bounded signed averaging and fixed-time stationarity. Exact compiled region; the original six analytic assumptions are unchanged.
6. Use signed Fubini and pushforward for the test identity
Product integrability yields integrability of the inner integral. Pull F(z) through the clock integral, then apply signed Fubini. The measurable pushforward M identifies the resulting integral with the endpoint-pair test under Q. This proves both the outer L1 conclusion and its exact integral representation.
Corresponding Lean step
have houter : Integrable (fun z => F z * op G z) (nu y) := by
simpa only [H, endpoint, integral_const_mul] using hHi.integral_prod_left
refine ⟨houter, ?_⟩
have hpair : Measurable (fun a : (E × E) × (E × E) => F a.1 * G a.2) :=
(hF.comp measurable_fst).mul (hG.comp measurable_snd)
calc
(∫ z, F z * op G z ∂nu y) = ∫ a, H a ∂((nu y).prod P) := by
rw [integral_prod H hHi]
simp only [H, endpoint, op, integral_const_mul]
_ = ∫ a, F a.1 * G a.2 ∂Q :=
(integral_map hM.aemeasurable hpair.aestronglyMeasurable).symm
ASTIS completion of bounded signed averaging and fixed-time stationarity. Exact compiled region; the original six analytic assumptions are unchanged.
7. Apply the same integrability argument to the flipped tests
Apply the already proved test identity first to F,G and then to G composed R,F composed R. Measurability of R and the original pointwise bounds give all required hypotheses. Both displayed outer integrals are therefore integrable, including when either bound vanishes.
Corresponding Lean step
intro F G CF CG hF hG hCF hCG hFb hGb
have hleft := htest F G CF CG hF hG hCF hCG hFb hGb
have hright := htest (fun z => G (R z)) (fun z => F (R z)) CG CF
(hG.comp hRm) (hF.comp hRm) hCG hCF (fun z => hGb (R z)) (fun z => hFb (R z))
refine ⟨hleft.1, hright.1, ?_⟩
rw [hleft.2, hright.2]
have hpair : Measurable (fun a : (E × E) × (E × E) => F a.1 * G a.2) :=
(hF.comp measurable_fst).mul (hG.comp measurable_snd)
ASTIS completion of bounded signed averaging and fixed-time stationarity. Exact compiled region; the original six analytic assumptions are unchanged.
8. Transfer endpoint reversal to bounded signed duality
Use the measurable map J and J_*Q=Q in the real integral-map identity for F(a)G(b). After the flipped swap the integrand is F(Rb)G(Ra); commute the real factors and combine the two test representations. No unbounded observable or L2 extension is inferred.
Corresponding Lean step
calc
(∫ a, F a.1 * G a.2 ∂Q) = ∫ a, F (J a).1 * G (J a).2 ∂Q := by
conv_lhs => rw [← hJ.map_eq]
exact integral_map hJ.measurable.aemeasurable hpair.aestronglyMeasurable
_ = ∫ a, G (R a.1) * F (R a.2) ∂Q := by
apply integral_congr_ae
exact Filter.Eventually.of_forall fun a => mul_comm _ _
ASTIS completion of bounded signed averaging and fixed-time stationarity. 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_bounded_gibbs_duality
Keep the same global actual process; Recover the actual probability laws and endpoint reversal; Prove momentum-flip symmetry of the actual phase law; Identify the actual fixed-time Gibbs marginal; Derive product integrability from the observable bounds; Use signed Fubini and pushforward for the test identity; Apply the same integrability argument to the flipped tests; Transfer endpoint reversal to bounded signed duality
Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.
theorem actual_bounded_gibbs_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_bounded_gibbs_duality_statement hα hαβ hV hH hη hβη := by
classical
unfold actual_bounded_gibbs_duality_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, h105⟩ :=
AutoSamplingTheory.ExampleCases.ProximalBPS.ActualCountableEndpointLaw.actual_countable_endpoint_law
hα hαβ hV hH hη hβη
refine ⟨Z, hZm, hZa, hZf, hZ0, ?_⟩
intro y r T op endpoint
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 hemb : Measurable (fun a : (E × E) × (ℕ → ℝ) => (((y, r), a.1), T, a.2)) :=
(measurable_const.prodMk measurable_fst).prodMk (measurable_const.prodMk measurable_snd)
have he : Measurable endpoint := hZm.comp hemb
let M : (E × E) × (ℕ → ℝ) → (E × E) × (E × E) := fun a => (a.1, endpoint a)
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 a => (R a.2, R a.1)
have hM : Measurable M := measurable_fst.prodMk he
have hJ : MeasurePreserving J Q Q := (h105 y r T).2.2
letI : IsProbabilityMeasure Q := (h105 y r T).2.1
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]
have hMP : MeasurePreserving M ((nu y).prod P) Q := ⟨hM, rfl⟩
have hfst : MeasurePreserving Prod.fst Q (nu y) := by
refine ⟨measurable_fst, ?_⟩
change Measure.map Prod.fst (Measure.map M ((nu y).prod P)) = nu y
rw [Measure.map_map measurable_fst hM]
change Measure.map Prod.fst ((nu y).prod P) = nu y
simp only [Measure.map_fst_prod, measure_univ, one_smul]
have hinvariant : MeasurePreserving endpoint ((nu y).prod P) (nu y) := by
have h := hR.comp ((hfst.comp hJ).comp hMP)
simpa only [Function.comp_def, M, J, R, neg_neg] using h
refine ⟨hinvariant, ?_⟩
have htest (F G : (E × E) → ℝ) (CF CG : ℝ)
(hF : Measurable F) (hG : Measurable G) (hCF : 0 ≤ CF) (hCG : 0 ≤ CG)
(hFb : ∀ z, |F z| ≤ CF) (hGb : ∀ z, |G z| ≤ CG) :
Integrable (fun z => F z * op G z) (nu y) ∧
(∫ z, F z * op G z ∂nu y) = ∫ a, F a.1 * G a.2 ∂Q := by
let H : (E × E) × (ℕ → ℝ) → ℝ := fun a => F a.1 * G (endpoint a)
have hHm : Measurable H := (hF.comp measurable_fst).mul (hG.comp he)
have hHi : Integrable H ((nu y).prod P) :=
Integrable.of_bound hHm.aestronglyMeasurable (CF * CG)
(Filter.Eventually.of_forall fun a => by
change |F a.1 * G (endpoint a)| ≤ CF * CG
rw [abs_mul]
exact mul_le_mul (hFb a.1) (hGb (endpoint a)) (abs_nonneg _) hCF)
have houter : Integrable (fun z => F z * op G z) (nu y) := by
simpa only [H, endpoint, integral_const_mul] using hHi.integral_prod_left
refine ⟨houter, ?_⟩
have hpair : Measurable (fun a : (E × E) × (E × E) => F a.1 * G a.2) :=
(hF.comp measurable_fst).mul (hG.comp measurable_snd)
calc
(∫ z, F z * op G z ∂nu y) = ∫ a, H a ∂((nu y).prod P) := by
rw [integral_prod H hHi]
simp only [H, endpoint, op, integral_const_mul]
_ = ∫ a, F a.1 * G a.2 ∂Q :=
(integral_map hM.aemeasurable hpair.aestronglyMeasurable).symm
intro F G CF CG hF hG hCF hCG hFb hGb
have hleft := htest F G CF CG hF hG hCF hCG hFb hGb
have hright := htest (fun z => G (R z)) (fun z => F (R z)) CG CF
(hG.comp hRm) (hF.comp hRm) hCG hCF (fun z => hGb (R z)) (fun z => hFb (R z))
refine ⟨hleft.1, hright.1, ?_⟩
rw [hleft.2, hright.2]
have hpair : Measurable (fun a : (E × E) × (E × E) => F a.1 * G a.2) :=
(hF.comp measurable_fst).mul (hG.comp measurable_snd)
calc
(∫ a, F a.1 * G a.2 ∂Q) = ∫ a, F (J a).1 * G (J a).2 ∂Q := by
conv_lhs => rw [← hJ.map_eq]
exact integral_map hJ.measurable.aemeasurable hpair.aestronglyMeasurable
_ = ∫ a, G (R a.1) * F (R a.2) ∂Q := by
apply integral_congr_ae
exact Filter.Eventually.of_forall fun a => mul_comm _ _
#print axioms actual_bounded_gibbs_duality
end
end AutoSamplingTheory.ExampleCases.ProximalBPS.ActualBoundedGibbsDualitySource assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| Bounded signed bilinear identity and Gibbs stationarity in Appendix A.1. | Both real outer integrals are integrable, have the stated flipped equality, and the same actual endpoint preserves nu_y. | same | Signed Fubini and momentum symmetry are proved internally. |
| Finite-dimensional Euclidean phase. | Finite real inner-product Borel space including rank zero. | generalization | Coordinate-free canonical volume and Gaussian preserve the formulas. |
| Printed F=1 marginal consequence. | Equivalent direct first/second marginal argument through actual endpoint reversal, with full bounded duality also proved. | same | Selected route explicitly allowed in the independently reviewed source graph; exact implementation selection is recorded. |
| L2 operator and later sampler results. | Fixed-time stationarity and bounded real-test duality only. | unresolved | Bounded signed Gibbs duality and fixed-time actual phase invariance only. L2 operator/domain identity, restart/Markovness, kernel-witness identification, hypocoercivity, simulation errors, actual expected costs, composition and all four full papers remain open. |
Bounded signed Gibbs duality and fixed-time actual phase invariance only. L2 operator/domain identity, restart/Markovness, kernel-witness identification, hypocoercivity, simulation errors, actual expected costs, composition and all four full papers remain open.
Encoder–denoiser: accepted · equivalent-after-elaboration
Detected semantic differences
- domains: Explicit coordinate-free finite-dimensional and rank-zero elaboration. — All exact volume/Gaussian/flow conventions retained; original six conditions unchanged and no dimension-positive premise.
- conclusion: Expose signed L1 obligations and actual endpoint measure equality. — Internal finite-probability bound, signed Fubini and actual endpoint law discharge all obligations; no extra public premise.
- scopes: Use separately admitted equivalent direct-marginal route for the fixed-time consequence. — Independent one-edge route overlay preserves source alternative and exact header. No Markov/L2 extension credited.
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
- Bounded signed Gibbs duality and fixed-time actual phase invariance only. L2 operator/domain identity, restart/Markovness, kernel-witness identification, hypocoercivity, simulation errors, actual expected costs, composition and all four full papers remain open.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
AutoSamplingTheory.ExampleCases.ProximalBPS.ActualCountableEndpointLaw.actual_countable_endpoint_lawAutoSamplingTheory.ExampleCases.ProximalBPS.ActualPhaseNormalization.actual_phase_gibbs_normalizationAutoSamplingTheory.TechnicalLemmas.Probability.UnitExponentialProduct.unit_exponential_product_laws
Mathlib API called (external library)
- stdGaussian_map
- Measure.map_prod_map
- Measure.map_map
- Measure.map_fst_prod
- MeasurePreserving.comp
- Integrable.of_bound
- Integrable.integral_prod_left
- integral_const_mul
- integral_prod
- integral_map
Mathematical sources
- Appendix A.1 final bounded signed bilinear identity (A8 averaging) and F=1 fixed-time Gibbs stationarity. — Bounded signed Gibbs duality and fixed-time actual phase invariance only. L2 operator/domain identity, restart/Markovness, kernel-witness identification, hypocoercivity, simulation errors, actual expected costs, composition and all four full papers remain open.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.