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

ActualL2Expectation: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

  1. Actual PBPS fixed-time L2 expectation contraction
Samplinglib mathematical lesson

Actual PBPS fixed-time L2 expectation contraction

AutoSamplingTheory.ExampleCases.ProximalBPS.ActualL2Expectation.actual_l2_expectation_contraction · 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. There is no joint measurability or continuity claim for the operator-valued family, no strong-continuity claim, and no assertion of full L2 momentum-flip duality Eq A.3, restart/Markov/semigroup, equality with a separately existential kernel, hypocoercivity, implementation accuracy or actual expected costs. Full papers and actual-input composition remain open.

\[\int|\operatorname{op}_TG|^2\,d\nu_y=\|A_T[G]\|_2^2\le\|[G]\|_2^2=\int|G|^2\,d\nu_y.\]
Lean statement · actual_l2_expectation_contraction

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. There is no joint measurability or continuity claim for the operator-valued family, no strong-continuity claim, and no assertion of full L2 momentum-flip duality Eq A.3, restart/Markov/semigroup, equality with a separately existential kernel, hypocoercivity, implementation accuracy or actual expected costs. Full papers 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.

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

Exact module and namespace context

Full Lean proposition (definition) · actual_l2_expectation_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_expectation_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)

set_option maxHeartbeats 2200000
set_option maxRecDepth 12000

Exact module and namespace context

Proof roadmap

  1. 1Retain the same actual process and all bounded results

    Consume the actual bounded-duality producer once. Preserve its joint measurable process, exact live arcs and fallback, parameterwise clock-almost-sure initialization, fixed-time Gibbs preservation and bounded momentum-flip duality. Every new expectation below uses this same witness.

  2. 2Construct the Hilbert-space averaging contraction

    For a probability input mu times nu and a measure-preserving endpoint, pullback along first projection and endpoint gives L2 isometries B and C. Define the operator internally by A=B* C. Adjoint norm preservation gives ||A||≤1. The adjoint identity and the exact pullback representatives give the displayed product pairing. This proof-local lemma is later instantiated with the actual Gibbs and clock laws, not assumed about the sampler.

  3. 3Prove product and outer integrability before identification

    For arbitrary MemLp input G, endpoint preservation transports L2 to the input product probability, hence to L1. Signed Fubini gives almost-everywhere clock-section integrability and outer L1. The constructed operator output is itself in L2 and therefore L1. These facts precede the uniqueness argument; output expectation L2 has not been assumed.

  4. 4Identify the average through measurable-set indicators

    Test the product pairing against the L2 class of 1_s for each measurable set s. Pullback preserves almost-everywhere changes of both indicator and G representatives. The indicator-weighted product is integrable; signed Fubini equates the two set integrals. L1 set-integral uniqueness then identifies the operator representative with the literal clock expectation almost everywhere.

  5. 5Transfer L2 membership to the actual expectation

    The identified operator representative is L2. Transfer this membership across the proved almost-everywhere equality and use Lp extensionality to certify the exact quotient equality. Together with product Fubini this returns the section L1 and output membership conclusions for arbitrary MemLp representatives.

  6. 6Relate the scalar square integral to the L2 norm

    The canonical toLp representative agrees almost everywhere with the raw function. Substitute this equality in the real inner-product integral; the Hilbert norm identity gives the exact square integral. This converts the operator norm bound into the requested scalar inequality.

  7. 7Prove joint Borel expectation and every bounded section

    For Borel G, compose the jointly measurable actual Z with G and integrate out the clock variable under its probability law. Product-integral measurability gives joint Borel dependence on y,r,z,T. A pointwise finite bound C proves every clock section integrable and the expectation bound, including C=0.

  8. 8Instantiate the construction at the actual probability laws

    Recover nu_y probability from actual Gibbs normalization and P probability from the countable exponential producer. Actual fixed-time endpoint preservation, inherited from the same Z, supplies the input to the proved local averaging construction. Choose one operator for each T; no regularity of the operator-valued family is inferred.

  9. 9Prove the zero-time operator is the identity

    Apply representative identification to the canonical representative of an arbitrary L2 class. The inherited parameterwise clock-almost-sure equality Z_0(z,w)=z makes its clock integral equal to that representative for each z. Lp and continuous-linear-map extensionality imply A_0=id without a uniform parameter-null-set assumption.

  10. 10Return the actual L2 representative and square contraction

    For every T and every MemLp G, return the previously proved section integrability and exact toLp equality. Express both scalar square integrals as L2 norm squares, use the operator bound1, then square the nonnegative norm inequality. This completes the fixed-time result; full L2 momentum-flip duality remains a separate density argument.

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 the same actual process and all bounded results

Consume the actual bounded-duality producer once. Preserve its joint measurable process, exact live arcs and fallback, parameterwise clock-almost-sure initialization, fixed-time Gibbs preservation and bounded momentum-flip duality. Every new expectation below uses this same witness.

\[Z\text{ fixed globally};\quad (Z_T)_*(\nu_y\otimes P)=\nu_y;\quad Z_0(z,w)=z\quad P\text{-a.e.}\]
Corresponding Lean step
  obtain ⟨Z, hZm, hZa, hZf, hZ0, h106⟩ :=
    AutoSamplingTheory.ExampleCases.ProximalBPS.ActualBoundedGibbsDuality.actual_bounded_gibbs_duality
      hα hαβ hV hH hη hβη

ASTIS completion of actual fixed-time L2 averaging. Exact compiled region; original six analytic assumptions and same global process are unchanged.

2. Construct the Hilbert-space averaging contraction

For a probability input mu times nu and a measure-preserving endpoint, pullback along first projection and endpoint gives L2 isometries B and C. Define the operator internally by A=B* C. Adjoint norm preservation gives ||A||≤1. The adjoint identity and the exact pullback representatives give the displayed product pairing. This proof-local lemma is later instantiated with the actual Gibbs and clock laws, not assumed about the sampler.

\[Bf(z,w)=f(z),\quad Cg(z,w)=g(Z_T(z,w)),\quad A=B^*C,\quad\|A\|\le1,\quad\langle f,Ag\rangle=\int f(z)g(Z_T(z,w))\,d(\mu\otimes\nu).\]
Corresponding Lean step
  have hpair_core
      (μ : Measure (E × E)) (ν : Measure (ℕ → ℝ)) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
      (Z : (E × E) × (ℕ → ℝ) → (E × E)) (hZ : MeasurePreserving Z (μ.prod ν) μ) :
      ∃ A : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ, ‖A‖ ≤ 1 ∧
        ∀ f g : Lp ℝ 2 μ,
          ⟪f, A g⟫_ℝ = ∫ p : (E × E) × (ℕ → ℝ), f p.1 * g (Z p) ∂μ.prod ν := by
    have hfst : MeasurePreserving Prod.fst (μ.prod ν) μ := by
      refine ⟨measurable_fst, ?_⟩
      simp only [Measure.map_fst_prod, measure_univ, one_smul]
    let B : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 (μ.prod ν) :=
      (Lp.compMeasurePreservingₗᵢ ℝ Prod.fst hfst).toContinuousLinearMap
    let C : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 (μ.prod ν) :=
      (Lp.compMeasurePreservingₗᵢ ℝ Z hZ).toContinuousLinearMap
    let A : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ := B.adjoint.comp C
    have hB : ‖B‖ ≤ 1 := LinearIsometry.norm_toContinuousLinearMap_le _
    have hC : ‖C‖ ≤ 1 := LinearIsometry.norm_toContinuousLinearMap_le _
    refine ⟨A, ?_, ?_⟩
    · calc
        ‖A‖ ≤ ‖B.adjoint‖ * ‖C‖ := ContinuousLinearMap.opNorm_comp_le _ _
        _ = ‖B‖ * ‖C‖ := by rw [ContinuousLinearMap.adjoint.norm_map]
        _ ≤ 1 * 1 := mul_le_mul hB hC (norm_nonneg _) zero_le_one
        _ = 1 := one_mul 1
    · intro f g
      change ⟪f, B.adjoint (C g)⟫_ℝ = _
      rw [ContinuousLinearMap.adjoint_inner_right, L2.inner_def]
      have hb : (B f : (E × E) × (ℕ → ℝ) → ℝ) =ᵐ[μ.prod ν] (fun p => f p.1) :=
        Lp.coeFn_compMeasurePreserving f hfst
      have hc : (C g : (E × E) × (ℕ → ℝ) → ℝ) =ᵐ[μ.prod ν] (fun p => g (Z p)) :=
        Lp.coeFn_compMeasurePreserving g hZ
      apply integral_congr_ae
      filter_upwards [hb, hc] with p hp hq
      rw [hp, hq]
      simp [RCLike.inner_apply, mul_comm]

ASTIS completion of actual fixed-time L2 averaging. Exact compiled region; original six analytic assumptions and same global process are unchanged.

3. Prove product and outer integrability before identification

For arbitrary MemLp input G, endpoint preservation transports L2 to the input product probability, hence to L1. Signed Fubini gives almost-everywhere clock-section integrability and outer L1. The constructed operator output is itself in L2 and therefore L1. These facts precede the uniqueness argument; output expectation L2 has not been assumed.

\[G\in L^2(\mu)\Rightarrow G\circ Z_T\in L^2(\mu\otimes\nu)\subset L^1;\qquad z\mapsto\int G(Z_T(z,w))\,d\nu(w)\in L^1(\mu).\]
Corresponding Lean step
  have haverage_core
      (μ : Measure (E × E)) (ν : Measure (ℕ → ℝ)) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
      (Z : (E × E) × (ℕ → ℝ) → (E × E)) (hZ : MeasurePreserving Z (μ.prod ν) μ) :
      ∃ A : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ, ‖A‖ ≤ 1 ∧
        ∀ G : (E × E) → ℝ, ∀ hG : MemLp G 2 μ,
          (∀ᵐ x ∂μ, Integrable (fun w => G (Z (x, w))) ν) ∧
          ∃ hOp : MemLp (fun x => ∫ w, G (Z (x, w)) ∂ν) 2 μ,
            A (hG.toLp G) = hOp.toLp (fun x => ∫ w, G (Z (x, w)) ∂ν) := by
    classical
    obtain ⟨A, hA, hpair⟩ := hpair_core μ ν Z hZ
    refine ⟨A, hA, ?_⟩
    intro G hG
    have hfst : MeasurePreserving Prod.fst (μ.prod ν) μ := by
      refine ⟨measurable_fst, ?_⟩
      simp only [Measure.map_fst_prod, measure_univ, one_smul]
    have hprod : Integrable (fun p : (E × E) × (ℕ → ℝ) => G (Z p)) (μ.prod ν) :=
      (hG.comp_measurePreserving hZ).integrable (by norm_num)
    have hop : Integrable (fun x => ∫ w, G (Z (x, w)) ∂ν) μ := hprod.integral_prod_left
    have hAg : Integrable (A (hG.toLp G) : (E × E) → ℝ) μ :=
      (Lp.memLp (A (hG.toLp G))).integrable (by norm_num)

ASTIS completion of actual fixed-time L2 averaging. Exact compiled region; original six analytic assumptions and same global process are unchanged.

4. Identify the average through measurable-set indicators

Test the product pairing against the L2 class of 1_s for each measurable set s. Pullback preserves almost-everywhere changes of both indicator and G representatives. The indicator-weighted product is integrable; signed Fubini equates the two set integrals. L1 set-integral uniqueness then identifies the operator representative with the literal clock expectation almost everywhere.

\[\int_s A[G]\,d\mu=\langle1_s,A[G]\rangle=\int1_s(z)G(Z_T(z,w))\,d(\mu\otimes\nu)=\int_s\operatorname{op}_TG\,d\mu.\]
Corresponding Lean step
    have heq : (A (hG.toLp G) : (E × E) → ℝ) =ᵐ[μ] (fun x => ∫ w, G (Z (x, w)) ∂ν) := by
      apply Integrable.ae_eq_of_forall_setIntegral_eq _ _ hAg hop
      intro s hs hms
      let i : Lp ℝ 2 μ := indicatorConstLp 2 hs hms.ne (1 : ℝ)
      have hi : (i : (E × E) → ℝ) =ᵐ[μ] s.indicator (fun _ => (1 : ℝ)) := indicatorConstLp_coeFn
      have hi' := hfst.quasiMeasurePreserving.ae_eq hi
      have hg' := hZ.quasiMeasurePreserving.ae_eq hG.coeFn_toLp
      let H : (E × E) × (ℕ → ℝ) → ℝ := fun p => (s.indicator (fun _ => (1 : ℝ)) p.1) * G (Z p)
      have hH : Integrable H (μ.prod ν) := by
        have hfun : H = (Prod.fst ⁻¹' s).indicator (fun p : (E × E) × (ℕ → ℝ) => G (Z p)) := by
          funext p
          by_cases hp : p.1 ∈ s <;> simp [H, Set.indicator, hp]
        rw [hfun]
        exact hprod.indicator (hs.preimage measurable_fst)
      calc
        (∫ x in s, A (hG.toLp G) x ∂μ) = ⟪i, A (hG.toLp G)⟫_ℝ :=
          (L2.inner_indicatorConstLp_one hs hms.ne _).symm
        _ = ∫ p : (E × E) × (ℕ → ℝ), i p.1 * (hG.toLp G) (Z p) ∂μ.prod ν := hpair i (hG.toLp G)
        _ = ∫ p : (E × E) × (ℕ → ℝ), H p ∂μ.prod ν := by
          apply integral_congr_ae
          filter_upwards [hi', hg'] with p hp hq
          change i p.1 = s.indicator (fun _ => (1 : ℝ)) p.1 at hp
          change (hG.toLp G) (Z p) = G (Z p) at hq
          dsimp only [H]
          rw [hp, hq]
        _ = ∫ x, ∫ w, H (x, w) ∂ν ∂μ := integral_prod H hH
        _ = ∫ x, s.indicator (fun _ => (1 : ℝ)) x * (∫ w, G (Z (x, w)) ∂ν) ∂μ := by
          simp only [H, integral_const_mul]
        _ = ∫ x in s, (∫ w, G (Z (x, w)) ∂ν) ∂μ := by
          rw [← integral_indicator hs]
          congr 1
          funext x
          by_cases hx : x ∈ s <;> simp [Set.indicator, hx]

ASTIS completion of actual fixed-time L2 averaging. Exact compiled region; original six analytic assumptions and same global process are unchanged.

5. Transfer L2 membership to the actual expectation

The identified operator representative is L2. Transfer this membership across the proved almost-everywhere equality and use Lp extensionality to certify the exact quotient equality. Together with product Fubini this returns the section L1 and output membership conclusions for arbitrary MemLp representatives.

\[\operatorname{op}_TG=A[G]\quad\mu\text{-a.e.}\quad\Rightarrow\quad\operatorname{op}_TG\in L^2(\mu),\quad[\operatorname{op}_TG]=A[G].\]
Corresponding Lean step
    have hOp : MemLp (fun x => ∫ w, G (Z (x, w)) ∂ν) 2 μ := MemLp.ae_eq heq (Lp.memLp (A (hG.toLp G)))
    refine ⟨hprod.prod_right_ae, hOp, ?_⟩
    apply Lp.ext
    exact heq.trans hOp.coeFn_toLp.symm

ASTIS completion of actual fixed-time L2 averaging. Exact compiled region; original six analytic assumptions and same global process are unchanged.

6. Relate the scalar square integral to the L2 norm

The canonical toLp representative agrees almost everywhere with the raw function. Substitute this equality in the real inner-product integral; the Hilbert norm identity gives the exact square integral. This converts the operator norm bound into the requested scalar inequality.

\[\int |G|^2\,d\mu=\langle[G],[G]\rangle=\|[G]\|_2^2.\]
Corresponding Lean step
  have hsquare_core
      (μ : Measure (E × E)) (G : (E × E) → ℝ) (hG : MemLp G 2 μ) :
      (∫ x, |G x| ^ 2 ∂μ) = ‖hG.toLp G‖ ^ 2 := by
    calc
      (∫ x, |G x| ^ 2 ∂μ) = ∫ x, ⟪(hG.toLp G) x, (hG.toLp G) x⟫_ℝ ∂μ := by
        apply integral_congr_ae
        filter_upwards [hG.coeFn_toLp] with x hx
        rw [hx]
        simp [RCLike.inner_apply, sq_abs, pow_two]
      _ = ⟪hG.toLp G, hG.toLp G⟫_ℝ := rfl
      _ = ‖hG.toLp G‖ ^ 2 := real_inner_self_eq_norm_sq _

ASTIS completion of actual fixed-time L2 averaging. Exact compiled region; original six analytic assumptions and same global process are unchanged.

7. Prove joint Borel expectation and every bounded section

For Borel G, compose the jointly measurable actual Z with G and integrate out the clock variable under its probability law. Product-integral measurability gives joint Borel dependence on y,r,z,T. A pointwise finite bound C proves every clock section integrable and the expectation bound, including C=0.

\[(y,r,z,T)\mapsto\int G(Z(y,r,z,T,w))\,dP(w)\text{ is Borel};\quad |G|\le C\Rightarrow |\operatorname{op}_TG|\le C.\]
Corresponding Lean step
  refine ⟨Z, hZm, hZa, hZf, hZ0, h106, ?_, ?_⟩
  · letI : IsProbabilityMeasure P :=
      AutoSamplingTheory.TechnicalLemmas.Probability.UnitExponentialProduct.unit_exponential_product_laws.1
    intro G hG
    constructor
    · have hmap : Measurable (fun a : (((E × E) × (E × E)) × ℝ≥0) × (ℕ → ℝ) =>
          G (Z a.1.1.1.1 a.1.1.1.2 a.1.1.2 a.1.2 a.2)) :=
        hG.comp (hZm.comp (measurable_fst.fst.prodMk
          (measurable_fst.snd.prodMk measurable_snd)))
      exact hmap.stronglyMeasurable.integral_prod_right.measurable
    · intro C hC hbound y xRef z T
      have hemb : Measurable (fun w : ℕ → ℝ => (((y, xRef), z), T, w)) :=
        measurable_const.prodMk (measurable_const.prodMk measurable_id)
      have hm : Measurable (fun w => G (Z y xRef z T w)) := hG.comp (hZm.comp hemb)
      have hb : ∀ᵐ w ∂P, ‖G (Z y xRef z T w)‖ ≤ C :=
        Filter.Eventually.of_forall fun w => by simpa only [Real.norm_eq_abs] using hbound (Z y xRef z T w)
      refine ⟨Integrable.of_bound hm.aestronglyMeasurable C hb, ?_⟩
      simpa using norm_integral_le_of_norm_le_const hb

ASTIS completion of actual fixed-time L2 averaging. Exact compiled region; original six analytic assumptions and same global process are unchanged.

8. Instantiate the construction at the actual probability laws

Recover nu_y probability from actual Gibbs normalization and P probability from the countable exponential producer. Actual fixed-time endpoint preservation, inherited from the same Z, supplies the input to the proved local averaging construction. Choose one operator for each T; no regularity of the operator-valued family is inferred.

\[\mu=\nu_y,\quad\nu=P,\quad(Z_T)_*(\nu_y\otimes P)=\nu_y\Rightarrow\exists(A_T)_{T\ge0}\text{ with }\|A_T\|\le1.\]
Corresponding Lean step
  · intro y xRef
    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 hfor : ∀ T : ℝ≥0,
        ∃ L : Lp ℝ 2 (nu y) →L[ℝ] Lp ℝ 2 (nu y), ‖L‖ ≤ 1 ∧
          ∀ G : (E × E) → ℝ, ∀ hG : MemLp G 2 (nu y),
            (∀ᵐ z ∂nu y, Integrable (fun w => G (Z y xRef z T w)) P) ∧
            ∃ hOp : MemLp (fun z => ∫ w, G (Z y xRef z T w) ∂P) 2 (nu y),
              L (hG.toLp G) = hOp.toLp (fun z => ∫ w, G (Z y xRef z T w) ∂P) := by
      intro T
      exact haverage_core (nu y) P (fun a => Z y xRef a.1 T a.2) (h106 y xRef T).1
    choose L hL hrep using hfor

ASTIS completion of actual fixed-time L2 averaging. Exact compiled region; original six analytic assumptions and same global process are unchanged.

9. Prove the zero-time operator is the identity

Apply representative identification to the canonical representative of an arbitrary L2 class. The inherited parameterwise clock-almost-sure equality Z_0(z,w)=z makes its clock integral equal to that representative for each z. Lp and continuous-linear-map extensionality imply A_0=id without a uniform parameter-null-set assumption.

\[\int f(Z_0(z,w))\,dP(w)=f(z)\quad\Rightarrow\quad A_0[f]=[f],\qquad A_0=\mathrm{id}.\]
Corresponding Lean step
    refine ⟨L, ?_, ?_⟩
    · apply ContinuousLinearMap.ext
      intro f
      obtain ⟨_, hm, he⟩ := hrep 0 (f : (E × E) → ℝ) (Lp.memLp f)
      rw [Lp.toLp_coeFn] at he
      apply Lp.ext
      change (L 0 f : (E × E) → ℝ) =ᵐ[nu y] (f : (E × E) → ℝ)
      have hpoint : ∀ z, (∫ w, f (Z y xRef z 0 w) ∂P) = f z := by
        intro z
        exact integral_eq_const ((hZ0 y xRef z).mono (fun w hw => congrArg f hw))
      rw [he]
      exact hm.coeFn_toLp.trans (Filter.Eventually.of_forall hpoint)

ASTIS completion of actual fixed-time L2 averaging. Exact compiled region; original six analytic assumptions and same global process are unchanged.

10. Return the actual L2 representative and square contraction

For every T and every MemLp G, return the previously proved section integrability and exact toLp equality. Express both scalar square integrals as L2 norm squares, use the operator bound1, then square the nonnegative norm inequality. This completes the fixed-time result; full L2 momentum-flip duality remains a separate density argument.

\[\int|\operatorname{op}_TG|^2\,d\nu_y=\|A_T[G]\|_2^2\le\|[G]\|_2^2=\int|G|^2\,d\nu_y.\]
Corresponding Lean step
    · intro T
      refine ⟨hL T, ?_⟩
      intro G hG opG
      obtain ⟨hsec, hOp, he⟩ := hrep T G hG
      refine ⟨hsec, ⟨hOp, he⟩, ?_⟩
      rw [hsquare_core (nu y) opG hOp, hsquare_core (nu y) G hG, ← he]
      have hn : ‖L T (hG.toLp G)‖ ≤ ‖hG.toLp G‖ :=
        (ContinuousLinearMap.le_opNorm (L T) (hG.toLp G)).trans
          (mul_le_of_le_one_left (norm_nonneg _) (hL T))
      nlinarith [norm_nonneg (L T (hG.toLp G)), norm_nonneg (hG.toLp G)]

ASTIS completion of actual fixed-time L2 averaging. 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_expectation_contraction

Retain the same actual process and all bounded results; Construct the Hilbert-space averaging contraction; Prove product and outer integrability before identification; Identify the average through measurable-set indicators; Transfer L2 membership to the actual expectation; Relate the scalar square integral to the L2 norm; Prove joint Borel expectation and every bounded section; Instantiate the construction at the actual probability laws; Prove the zero-time operator is the identity; Return the actual L2 representative and square contraction

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_expectation_contraction
    {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_expectation_statement hα hαβ hV hH hη hβη := by
  classical
  unfold actual_l2_expectation_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⟩ :=
    AutoSamplingTheory.ExampleCases.ProximalBPS.ActualBoundedGibbsDuality.actual_bounded_gibbs_duality
      hα hαβ hV hH hη hβη
  have hpair_core
      (μ : Measure (E × E)) (ν : Measure (ℕ → ℝ)) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
      (Z : (E × E) × (ℕ → ℝ) → (E × E)) (hZ : MeasurePreserving Z (μ.prod ν) μ) :
      ∃ A : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ, ‖A‖ ≤ 1 ∧
        ∀ f g : Lp ℝ 2 μ,
          ⟪f, A g⟫_ℝ = ∫ p : (E × E) × (ℕ → ℝ), f p.1 * g (Z p) ∂μ.prod ν := by
    have hfst : MeasurePreserving Prod.fst (μ.prod ν) μ := by
      refine ⟨measurable_fst, ?_⟩
      simp only [Measure.map_fst_prod, measure_univ, one_smul]
    let B : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 (μ.prod ν) :=
      (Lp.compMeasurePreservingₗᵢ ℝ Prod.fst hfst).toContinuousLinearMap
    let C : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 (μ.prod ν) :=
      (Lp.compMeasurePreservingₗᵢ ℝ Z hZ).toContinuousLinearMap
    let A : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ := B.adjoint.comp C
    have hB : ‖B‖ ≤ 1 := LinearIsometry.norm_toContinuousLinearMap_le _
    have hC : ‖C‖ ≤ 1 := LinearIsometry.norm_toContinuousLinearMap_le _
    refine ⟨A, ?_, ?_⟩
    · calc
        ‖A‖ ≤ ‖B.adjoint‖ * ‖C‖ := ContinuousLinearMap.opNorm_comp_le _ _
        _ = ‖B‖ * ‖C‖ := by rw [ContinuousLinearMap.adjoint.norm_map]
        _ ≤ 1 * 1 := mul_le_mul hB hC (norm_nonneg _) zero_le_one
        _ = 1 := one_mul 1
    · intro f g
      change ⟪f, B.adjoint (C g)⟫_ℝ = _
      rw [ContinuousLinearMap.adjoint_inner_right, L2.inner_def]
      have hb : (B f : (E × E) × (ℕ → ℝ) → ℝ) =ᵐ[μ.prod ν] (fun p => f p.1) :=
        Lp.coeFn_compMeasurePreserving f hfst
      have hc : (C g : (E × E) × (ℕ → ℝ) → ℝ) =ᵐ[μ.prod ν] (fun p => g (Z p)) :=
        Lp.coeFn_compMeasurePreserving g hZ
      apply integral_congr_ae
      filter_upwards [hb, hc] with p hp hq
      rw [hp, hq]
      simp [RCLike.inner_apply, mul_comm]
  have haverage_core
      (μ : Measure (E × E)) (ν : Measure (ℕ → ℝ)) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
      (Z : (E × E) × (ℕ → ℝ) → (E × E)) (hZ : MeasurePreserving Z (μ.prod ν) μ) :
      ∃ A : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ, ‖A‖ ≤ 1 ∧
        ∀ G : (E × E) → ℝ, ∀ hG : MemLp G 2 μ,
          (∀ᵐ x ∂μ, Integrable (fun w => G (Z (x, w))) ν) ∧
          ∃ hOp : MemLp (fun x => ∫ w, G (Z (x, w)) ∂ν) 2 μ,
            A (hG.toLp G) = hOp.toLp (fun x => ∫ w, G (Z (x, w)) ∂ν) := by
    classical
    obtain ⟨A, hA, hpair⟩ := hpair_core μ ν Z hZ
    refine ⟨A, hA, ?_⟩
    intro G hG
    have hfst : MeasurePreserving Prod.fst (μ.prod ν) μ := by
      refine ⟨measurable_fst, ?_⟩
      simp only [Measure.map_fst_prod, measure_univ, one_smul]
    have hprod : Integrable (fun p : (E × E) × (ℕ → ℝ) => G (Z p)) (μ.prod ν) :=
      (hG.comp_measurePreserving hZ).integrable (by norm_num)
    have hop : Integrable (fun x => ∫ w, G (Z (x, w)) ∂ν) μ := hprod.integral_prod_left
    have hAg : Integrable (A (hG.toLp G) : (E × E) → ℝ) μ :=
      (Lp.memLp (A (hG.toLp G))).integrable (by norm_num)
    have heq : (A (hG.toLp G) : (E × E) → ℝ) =ᵐ[μ] (fun x => ∫ w, G (Z (x, w)) ∂ν) := by
      apply Integrable.ae_eq_of_forall_setIntegral_eq _ _ hAg hop
      intro s hs hms
      let i : Lp ℝ 2 μ := indicatorConstLp 2 hs hms.ne (1 : ℝ)
      have hi : (i : (E × E) → ℝ) =ᵐ[μ] s.indicator (fun _ => (1 : ℝ)) := indicatorConstLp_coeFn
      have hi' := hfst.quasiMeasurePreserving.ae_eq hi
      have hg' := hZ.quasiMeasurePreserving.ae_eq hG.coeFn_toLp
      let H : (E × E) × (ℕ → ℝ) → ℝ := fun p => (s.indicator (fun _ => (1 : ℝ)) p.1) * G (Z p)
      have hH : Integrable H (μ.prod ν) := by
        have hfun : H = (Prod.fst ⁻¹' s).indicator (fun p : (E × E) × (ℕ → ℝ) => G (Z p)) := by
          funext p
          by_cases hp : p.1 ∈ s <;> simp [H, Set.indicator, hp]
        rw [hfun]
        exact hprod.indicator (hs.preimage measurable_fst)
      calc
        (∫ x in s, A (hG.toLp G) x ∂μ) = ⟪i, A (hG.toLp G)⟫_ℝ :=
          (L2.inner_indicatorConstLp_one hs hms.ne _).symm
        _ = ∫ p : (E × E) × (ℕ → ℝ), i p.1 * (hG.toLp G) (Z p) ∂μ.prod ν := hpair i (hG.toLp G)
        _ = ∫ p : (E × E) × (ℕ → ℝ), H p ∂μ.prod ν := by
          apply integral_congr_ae
          filter_upwards [hi', hg'] with p hp hq
          change i p.1 = s.indicator (fun _ => (1 : ℝ)) p.1 at hp
          change (hG.toLp G) (Z p) = G (Z p) at hq
          dsimp only [H]
          rw [hp, hq]
        _ = ∫ x, ∫ w, H (x, w) ∂ν ∂μ := integral_prod H hH
        _ = ∫ x, s.indicator (fun _ => (1 : ℝ)) x * (∫ w, G (Z (x, w)) ∂ν) ∂μ := by
          simp only [H, integral_const_mul]
        _ = ∫ x in s, (∫ w, G (Z (x, w)) ∂ν) ∂μ := by
          rw [← integral_indicator hs]
          congr 1
          funext x
          by_cases hx : x ∈ s <;> simp [Set.indicator, hx]
    have hOp : MemLp (fun x => ∫ w, G (Z (x, w)) ∂ν) 2 μ := MemLp.ae_eq heq (Lp.memLp (A (hG.toLp G)))
    refine ⟨hprod.prod_right_ae, hOp, ?_⟩
    apply Lp.ext
    exact heq.trans hOp.coeFn_toLp.symm
  have hsquare_core
      (μ : Measure (E × E)) (G : (E × E) → ℝ) (hG : MemLp G 2 μ) :
      (∫ x, |G x| ^ 2 ∂μ) = ‖hG.toLp G‖ ^ 2 := by
    calc
      (∫ x, |G x| ^ 2 ∂μ) = ∫ x, ⟪(hG.toLp G) x, (hG.toLp G) x⟫_ℝ ∂μ := by
        apply integral_congr_ae
        filter_upwards [hG.coeFn_toLp] with x hx
        rw [hx]
        simp [RCLike.inner_apply, sq_abs, pow_two]
      _ = ⟪hG.toLp G, hG.toLp G⟫_ℝ := rfl
      _ = ‖hG.toLp G‖ ^ 2 := real_inner_self_eq_norm_sq _
  refine ⟨Z, hZm, hZa, hZf, hZ0, h106, ?_, ?_⟩
  · letI : IsProbabilityMeasure P :=
      AutoSamplingTheory.TechnicalLemmas.Probability.UnitExponentialProduct.unit_exponential_product_laws.1
    intro G hG
    constructor
    · have hmap : Measurable (fun a : (((E × E) × (E × E)) × ℝ≥0) × (ℕ → ℝ) =>
          G (Z a.1.1.1.1 a.1.1.1.2 a.1.1.2 a.1.2 a.2)) :=
        hG.comp (hZm.comp (measurable_fst.fst.prodMk
          (measurable_fst.snd.prodMk measurable_snd)))
      exact hmap.stronglyMeasurable.integral_prod_right.measurable
    · intro C hC hbound y xRef z T
      have hemb : Measurable (fun w : ℕ → ℝ => (((y, xRef), z), T, w)) :=
        measurable_const.prodMk (measurable_const.prodMk measurable_id)
      have hm : Measurable (fun w => G (Z y xRef z T w)) := hG.comp (hZm.comp hemb)
      have hb : ∀ᵐ w ∂P, ‖G (Z y xRef z T w)‖ ≤ C :=
        Filter.Eventually.of_forall fun w => by simpa only [Real.norm_eq_abs] using hbound (Z y xRef z T w)
      refine ⟨Integrable.of_bound hm.aestronglyMeasurable C hb, ?_⟩
      simpa using norm_integral_le_of_norm_le_const hb
  · intro y xRef
    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 hfor : ∀ T : ℝ≥0,
        ∃ L : Lp ℝ 2 (nu y) →L[ℝ] Lp ℝ 2 (nu y), ‖L‖ ≤ 1 ∧
          ∀ G : (E × E) → ℝ, ∀ hG : MemLp G 2 (nu y),
            (∀ᵐ z ∂nu y, Integrable (fun w => G (Z y xRef z T w)) P) ∧
            ∃ hOp : MemLp (fun z => ∫ w, G (Z y xRef z T w) ∂P) 2 (nu y),
              L (hG.toLp G) = hOp.toLp (fun z => ∫ w, G (Z y xRef z T w) ∂P) := by
      intro T
      exact haverage_core (nu y) P (fun a => Z y xRef a.1 T a.2) (h106 y xRef T).1
    choose L hL hrep using hfor
    refine ⟨L, ?_, ?_⟩
    · apply ContinuousLinearMap.ext
      intro f
      obtain ⟨_, hm, he⟩ := hrep 0 (f : (E × E) → ℝ) (Lp.memLp f)
      rw [Lp.toLp_coeFn] at he
      apply Lp.ext
      change (L 0 f : (E × E) → ℝ) =ᵐ[nu y] (f : (E × E) → ℝ)
      have hpoint : ∀ z, (∫ w, f (Z y xRef z 0 w) ∂P) = f z := by
        intro z
        exact integral_eq_const ((hZ0 y xRef z).mono (fun w hw => congrArg f hw))
      rw [he]
      exact hm.coeFn_toLp.trans (Filter.Eventually.of_forall hpoint)
    · intro T
      refine ⟨hL T, ?_⟩
      intro G hG opG
      obtain ⟨hsec, hOp, he⟩ := hrep T G hG
      refine ⟨hsec, ⟨hOp, he⟩, ?_⟩
      rw [hsquare_core (nu y) opG hOp, hsquare_core (nu y) G hG, ← he]
      have hn : ‖L T (hG.toLp G)‖ ≤ ‖hG.toLp G‖ :=
        (ContinuousLinearMap.le_opNorm (L T) (hG.toLp G)).trans
          (mul_le_of_le_one_left (norm_nonneg _) (hL T))
      nlinarith [norm_nonneg (L T (hG.toLp G)), norm_nonneg (hG.toLp G)]

#print axioms actual_l2_expectation_contraction
end
end AutoSamplingTheory.ExampleCases.ProximalBPS.ActualL2Expectation

Exact module and namespace context

Scope and omitted-condition boundaries
  • Fixed-time real L2 expectation contraction with inherited106 bounded duality/invariance. Full A.3 identity, strong continuity, restart/Markov/semigroup, separate kernel-witness identification, 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)

  • StronglyMeasurable.integral_prod_right
  • Integrable.of_bound
  • norm_integral_le_of_norm_le_const
  • Lp.compMeasurePreservingₗᵢ
  • Lp.coeFn_compMeasurePreserving
  • ContinuousLinearMap.adjoint_inner_right
  • ContinuousLinearMap.opNorm_comp_le
  • LinearIsometry.norm_toContinuousLinearMap_le
  • MemLp.integrable
  • Integrable.prod_right_ae
  • Integrable.integral_prod_left
  • L2.inner_indicatorConstLp_one
  • integral_prod
  • Integrable.ae_eq_of_forall_setIntegral_eq
  • memLp_congr_ae
  • Lp.ext
  • integral_eq_const
  • Lp.toLp_coeFn

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.