Actual normalized PBPS endpoint-pair sector reversal
AutoSamplingTheory.ExampleCases.ProximalBPS.ActualNormalizedEndpointSector.actual_normalized_endpoint_sector_reversal · theorem · Teaching coverage
Mathematical statement
Let E be a finite-dimensional real inner-product space equipped with its Borel sigma algebra; zero dimension is allowed. Let alpha,beta≥0, eta be real, V:E→R. Assume exactly alpha>0, alpha≤beta, V is C2, alpha||v||^2≤D2V(x)[v,v]≤beta||v||^2 for every x,v, eta>0 and beta*eta≤1. All conclusions hold for every y,r in E, initial phase z0=(x0,p0), integer n≥0 and finite T≥0. Set c=y-eta*grad V(r). For z=(x,p), define Phi_u(z)=(c+cos(u)(x-c)+sqrt(eta)sin(u)p, -sin(u)/sqrt(eta)(x-c)+cos(u)p). Define h_r(x)=grad V(x)-grad V(r), S_r(x,p)=(x,p-[2<p,h_r(x)>/||h_r(x)||^2]h_r(x)) with real division totalized by 0/0=0, lambda_r(x,p)=sqrt(eta)max(0,<p,h_r(x)>), and Lambda_z(u)=integral from0 to u of lambda_r(Phi_s(z)) ds for u≥0, using Lebesgue measure. A tagged record is either live(a,z), with a≥0, or stopped; Hist_n is the type of all n+1 records. Let Delta_n(T) be the strict simplex 0<t1<...<tn<T. Write a0=0, ai=ti (1≤i≤n), a_(n+1)=T. Given t in Delta_n(T), define z_i=S_r(Phi_(a_i-a_(i-1))(z_(i-1))) for1≤i≤n and K_n(t)_j=live(a_j,z_j). The literal Lean nonnegative conversions preserve these nonnegative times. Define qReal_n(t)=product_(i=1)^n [lambda_r(Phi_(a_i-a_(i-1))(z_(i-1))) exp(-Lambda_(z_(i-1))(a_i-a_(i-1)))], q_n=ofReal(qReal_n). For arbitrary histories let readTime(live(a,z))=a and readTime(stopped)=0; d_n(T,h)=max(T-readTime(h_n),0). Put W(live(a,z),u)=ofReal(exp(-Lambda_z(u))) and W(stopped,u)=0. Define rho_n(T,t)=q_n(t) W(K_n(t)_n,d_n(T,K_n(t))). Here ofReal(x) is max(x,0) embedded into extended nonnegative reals; no probability law or normalization is assumed in this deterministic identity. Define Path_T as all phase-valued functions on[0,T]. The total interpolation Psi_n(h)(s) starts at z0 and scans records j=0,...,n in order: a live(a,z) record with a≤s replaces the accumulator by Phi_(max(s-a,0))(z); otherwise it is unchanged. Set Gamma_n(t)=Psi_n(K_n(t)). Define R(x,p)=(x,-p), Vy(x)=V(x)+||x-y||^2/(2 eta), and pi_y=volume_E.tilted(-Vy), that is, the measure with density ofReal(exp(-Vy(x))/integral exp(-Vy) dx). Let gamma=stdGaussian(E), the centered identity-covariance Gaussian. Let m_n,T be the comap of Lebesgue measure on R^n by the inclusion of the strict simplex Prefix_n(T), without a factorial factor or an extra normalization. For every y,r in E, n≥0 and T≥0, let X_n,T=(E times E) times Prefix_n(T), with phase coordinate first. Define the actual terminal phase A(z,t)=Gamma_(y,r,z,n,T,t)(T), endpoint-pair map B(z,t)=(z,A(z,t)), and the density-weighted sector measure sigma_(y,r,n,T)=((pi_y times gamma) times m_n,T).withDensity((z,t) → rho_(y,r,z,n,T)(t)). This uses precisely the actual product of event rates, intervening survivals and terminal survival defined above. Define its pushforward L_(y,r,n,T)=map B sigma_(y,r,n,T), a measure on (E times E) times (E times E). Define J(z0,zT)=(R(zT),R(z0)). Then J is measurable and map J L_(y,r,n,T)=L_(y,r,n,T) for every y,r,n,T. Equivalently J is measure preserving from this actual endpoint-pair measure to itself. Phase normalization, joint measurability, simplex sigma-finiteness and the density conversion are established internally; none is a supplied premise. The word normalized describes the initial phase probability pi_y times gamma; it does not assert that each fixed-count sector has total mass one. The statement does not supply a finite-mass or subprobability bound for sigma or L. The result includes n=0, T=0, dimension-zero E, zero reflection normals and zero rates. For n>0,T=0 the strict simplex is empty. Countable sector assembly, signed bilinear identities, process invariance, restart/Markovness, hypocoercivity, implementation error, expected costs and whole-paper/composition conclusions remain separate.
Lean statement · actual_normalized_endpoint_sector_reversal
Let E be a finite-dimensional real inner-product space equipped with its Borel sigma algebra; zero dimension is allowed. Let alpha,beta>=0, eta be real, V:E->R. Assume exactly alpha>0, alpha<=beta, V is C2, alpha||v||^2<=D2V(x)[v,v]<=beta||v||^2 for every x,v, eta>0 and beta*eta<=1. All conclusions hold for every y,r in E, initial phase z0=(x0,p0), integer n>=0 and finite T>=0. Set c=y-eta*grad V(r). For z=(x,p), define Phi_u(z)=(c+cos(u)(x-c)+sqrt(eta)sin(u)p, -sin(u)/sqrt(eta)(x-c)+cos(u)p). Define h_r(x)=grad V(x)-grad V(r), S_r(x,p)=(x,p-[2<p,h_r(x)>/||h_r(x)||^2]h_r(x)) with real division totalized by 0/0=0, lambda_r(x,p)=sqrt(eta)max(0,<p,h_r(x)>), and Lambda_z(u)=integral from0 to u of lambda_r(Phi_s(z)) ds for u>=0, using Lebesgue measure. A tagged record is either live(a,z), with a>=0, or stopped; Hist_n is the type of all n+1 records. Let Delta_n(T) be the strict simplex 0<t1<...<tn<T. Write a0=0, ai=ti (1<=i<=n), a_(n+1)=T. Given t in Delta_n(T), define z_i=S_r(Phi_(a_i-a_(i-1))(z_(i-1))) for1<=i<=n and K_n(t)_j=live(a_j,z_j). The literal Lean nonnegative conversions preserve these nonnegative times. Define qReal_n(t)=product_(i=1)^n [lambda_r(Phi_(a_i-a_(i-1))(z_(i-1))) exp(-Lambda_(z_(i-1))(a_i-a_(i-1)))], q_n=ofReal(qReal_n). For arbitrary histories let readTime(live(a,z))=a and readTime(stopped)=0; d_n(T,h)=max(T-readTime(h_n),0). Put W(live(a,z),u)=ofReal(exp(-Lambda_z(u))) and W(stopped,u)=0. Define rho_n(T,t)=q_n(t) W(K_n(t)_n,d_n(T,K_n(t))). Here ofReal(x) is max(x,0) embedded into extended nonnegative reals; no probability law or normalization is assumed in this deterministic identity. Define Path_T as all phase-valued functions on[0,T]. The total interpolation Psi_n(h)(s) starts at z0 and scans records j=0,...,n in order: a live(a,z) record with a<=s replaces the accumulator by Phi_(max(s-a,0))(z); otherwise it is unchanged. Set Gamma_n(t)=Psi_n(K_n(t)). Define R(x,p)=(x,-p), Vy(x)=V(x)+||x-y||^2/(2 eta), and pi_y=volume_E.tilted(-Vy), that is, the measure with density ofReal(exp(-Vy(x))/integral exp(-Vy) dx). Let gamma=stdGaussian(E), the centered identity-covariance Gaussian. Let m_n,T be the comap of Lebesgue measure on R^n by the inclusion of the strict simplex Prefix_n(T), without a factorial factor or an extra normalization. For every y,r in E, n>=0 and T>=0, let X_n,T=(E times E) times Prefix_n(T), with phase coordinate first. Define the actual terminal phase A(z,t)=Gamma_(y,r,z,n,T,t)(T), endpoint-pair map B(z,t)=(z,A(z,t)), and the density-weighted sector measure sigma_(y,r,n,T)=((pi_y times gamma) times m_n,T).withDensity((z,t) -> rho_(y,r,z,n,T)(t)). This uses precisely the actual product of event rates, intervening survivals and terminal survival defined above. Define its pushforward L_(y,r,n,T)=map B sigma_(y,r,n,T), a measure on (E times E) times (E times E). Define J(z0,zT)=(R(zT),R(z0)). Then J is measurable and map J L_(y,r,n,T)=L_(y,r,n,T) for every y,r,n,T. Equivalently J is measure preserving from this actual endpoint-pair measure to itself. Phase normalization, joint measurability, simplex sigma-finiteness and the density conversion are established internally; none is a supplied premise. The word normalized describes the initial phase probability pi_y times gamma; it does not assert that each fixed-count sector has total mass one. The statement does not supply a finite-mass or subprobability bound for sigma or L. The result includes n=0, T=0, dimension-zero E, zero reflection normals and zero rates. For n>0,T=0 the strict simplex is empty. Countable sector assembly, signed bilinear identities, process invariance, restart/Markovness, hypocoercivity, implementation error, expected costs and whole-paper/composition conclusions remain separate.
Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.
theorem actual_normalized_endpoint_sector_reversal
{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_normalized_endpoint_sector_statement hα hαβ hV hH hη hβηFull Lean proposition (definition) · actual_normalized_endpoint_sector_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_normalized_endpoint_sector_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 Rec := (ℝ≥0 × (E × E)) ⊕ Unit
let Hist : ℕ → Type _ := fun n => Fin (n + 1) → Rec
let Δ : (n : ℕ) → ℝ≥0 → Set (Fin n → ℝ) := fun n T =>
{t | StrictMono (Fin.cons (0 : ℝ) t) ∧ ∀ i, t i < (T : ℝ)}
let Prefix : (n : ℕ) → ℝ≥0 → Type := fun n T => {t : Fin n → ℝ // t ∈ Δ n T}
let 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 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 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 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 piY : E → Measure E := fun y => (volume : Measure E).tilted (fun x => -Vy y x)
let gamma : Measure E := ProbabilityTheory.stdGaussian E
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 → ℝ))
∀ y r : E, ∀ n : ℕ, ∀ T : ℝ≥0,
let A : (E × E) × Prefix n T → E × E :=
fun q => Γ y r q.1 n T q.2 ⟨T, le_rfl⟩
let B : (E × E) × Prefix n T → (E × E) × (E × E) := fun q => (q.1, A q)
let sigma : Measure ((E × E) × Prefix n T) :=
(((piY y).prod gamma).prod (m n T)).withDensity (fun q => ρ y r q.1 n T q.2)
let L : Measure ((E × E) × (E × E)) := Measure.map B sigma
let J : (E × E) × (E × E) → (E × E) × (E × E) :=
fun p => (R p.2, R p.1)
MeasurePreserving J L L
set_option maxHeartbeats 1600000
set_option maxRecDepth 10000Proof roadmap
- 1Align the two event-time reversal witnesses
In this step only, use zero-based Fin n coordinates i=0,...,n-1; the earlier strict-simplex description uses one-based coordinates. The endpoint reversal and nonnegative weighted substitution each provide a time reversal with the same coordinate formula. Subtype and coordinate extensionality identify them, so one map serves both parents.
- 2Construct the measurable endpoint diagram
Fix y,r using a measurable embedding into the joint parameter domain. The actual terminal map is measurable. Pair it with the initial phase to obtain B; momentum reversal gives measurable J and Theta. The parent endpoint reversal proves B after Theta equals J after B, including the final flow arc.
- 3Recover joint measurability of the actual density
Apply the finite-count path theorem at the same original analytic assumptions and compose its joint density map with the fixed-parameter embedding. This is the actual rho, including terminal survival.
- 4Justify the simplex measure product
Each coordinate inequality is measurable. Express the strict time ordering and terminal bound as finite, hence countable, intersections. Mapping the subtype measure back to Euclidean time space gives restricted Lebesgue measure; sigma-finiteness pulls back along the measurable inclusion.
- 5Identify the normalized phase density
C2 regularity makes the phase Gibbs weight measurable. The existing phase normalization theorem proves that its reciprocal-partition density on phase volume is exactly pi_y times the standard Gaussian. Its positivity and finiteness are supplied by that theorem, not by extra binders here.
- 6Rewrite the actual normalized sector measure
Use the product-with-density identity, justified by simplex sigma-finiteness. Combine the measurable initial phase density with the actual event density; associativity leaves one constant normalizer multiplying the previous unnormalized weight.
- 7Prove preservation of the full normalized sector
Test the pushed-forward measure against every measurable extended-nonnegative F. Rewrite the two density integrals, factor out the constant normalizer and apply the actual unnormalized weighted-sector substitution. Equality of all these integrals proves the full measure identity; no finite integral or cancellation is needed.
- 8Push the reversal to endpoint pairs
Apply composition of measurable pushforwards and the endpoint intertwining. This transports the full normalized-sector identity through B to precisely the declared endpoint-pair measure L.
Full assumptions and notation
All objects and hypotheses
- Finite-dimensional real inner-product Borel E with canonical volume, including dimension zero.
- alpha,beta≥0; alpha>0; alpha≤beta; V is C2; alpha||v||^2≤D2V(x)[v,v]≤beta||v||^2 for every x,v; eta>0; beta*eta≤1.
- Every y,r in E, n≥0 and finite nonnegative T. Literal harmonic flow, totalized reflection, nonnegative event rate, strict time simplex, actual recursively reflected states and interpolated endpoint.
- The actual density is the product of event rates and interval survivals times terminal survival. Initial phase measure is tilted conditional position law times standard Gaussian momentum; no extra normalizer, integrability, measurability, sigma-finiteness or finite-sector-mass hypothesis.
Mathematical proof
1. Align the two event-time reversal witnesses
In this step only, use zero-based Fin n coordinates i=0,...,n-1; the earlier strict-simplex description uses one-based coordinates. The endpoint reversal and nonnegative weighted substitution each provide a time reversal with the same coordinate formula. Subtype and coordinate extensionality identify them, so one map serves both parents.
Corresponding Lean step
obtain ⟨rhoTime, hrho, h97⟩ :=
AutoSamplingTheory.ExampleCases.ProximalBPS.ActualEndpointTimeReversal.actual_endpoint_time_reversal_laws
hα hαβ hV hH hη hβη n T
obtain ⟨rho102, hrho102, h102⟩ :=
AutoSamplingTheory.ExampleCases.ProximalBPS.ActualWeightedSector.actual_weighted_sector_lintegral
hα hαβ hV hH hη hβη n T
have halign : rho102 = rhoTime := by
funext t
apply Subtype.ext
funext i
exact (hrho102 t i).trans (hrho t i).symm
subst rho102
ASTIS completion of the phase-law proportionality. Exact compiled region; every analytic ingredient is derived from the original assumptions.
2. Construct the measurable endpoint diagram
Fix y,r using a measurable embedding into the joint parameter domain. The actual terminal map is measurable. Pair it with the initial phase to obtain B; momentum reversal gives measurable J and Theta. The parent endpoint reversal proves B after Theta equals J after B, including the final flow arc.
Corresponding Lean step
rcases h97 with ⟨hTimeM, hTimeI, hTimeP, hAformula, hAjoint, hAvolume,
hArev, hThetajoint, hThetaI, hThetaP⟩
let Theta : (E × E) × Prefix n T → (E × E) × Prefix n T :=
fun q => (R (A q), rhoTime q.2)
have hemb : Measurable (fun q : (E × E) × Prefix n T => (((y, r), q.1), q.2)) :=
(measurable_const.prodMk measurable_fst).prodMk measurable_snd
have hA : Measurable A := hAjoint.comp hemb
have hB : Measurable B := measurable_fst.prodMk hA
have hR : Measurable R := measurable_fst.prodMk measurable_snd.neg
have hJ : Measurable J := (hR.comp measurable_snd).prodMk (hR.comp measurable_fst)
have hTheta : Measurable Theta := hThetajoint.comp hemb
have hinter (x : (E × E) × Prefix n T) : B (Theta x) = J (B x) := by
apply Prod.ext
· rfl
· exact hArev y r x.1 x.2
ASTIS completion of the phase-law proportionality. Exact compiled region; every analytic ingredient is derived from the original assumptions.
3. Recover joint measurability of the actual density
Apply the finite-count path theorem at the same original analytic assumptions and compose its joint density map with the fixed-parameter embedding. This is the actual rho, including terminal survival.
Corresponding Lean step
obtain ⟨Z, hZ⟩ :=
AutoSamplingTheory.ExampleCases.ProximalBPS.ActualFiniteCountPath.actual_finite_count_path_law
hα hαβ hV hH hη hβη
have hρjoint : Measurable (fun p : ((E × E) × (E × E)) × Prefix n T =>
ρ p.1.1.1 p.1.1.2 p.1.2 n T p.2) := (hZ.2.2.2.2 n T).2.2.1
have hρ := hρjoint.comp hemb
have hρliteral : Measurable (fun x : (E × E) × Prefix n T => ρ y r x.1 n T x.2) := by
simpa only [Function.comp_def] using hρ
ASTIS completion of the phase-law proportionality. Exact compiled region; every analytic ingredient is derived from the original assumptions.
4. Justify the simplex measure product
Each coordinate inequality is measurable. Express the strict time ordering and terminal bound as finite, hence countable, intersections. Mapping the subtype measure back to Euclidean time space gives restricted Lebesgue measure; sigma-finiteness pulls back along the measurable inclusion.
Corresponding Lean step
have hcons (i : Fin (n + 1)) :
Measurable (fun t : Fin n → ℝ => (Fin.cons (0 : ℝ) t : Fin (n + 1) → ℝ) i) := by
induction i using Fin.cases with
| zero => exact measurable_const
| succ i => exact measurable_pi_apply i
have hs : MeasurableSet (Δ n T) := by
change MeasurableSet {t : Fin n → ℝ |
(∀ i j : Fin (n + 1), i < j → (Fin.cons (0 : ℝ) t : Fin (n + 1) → ℝ) i < (Fin.cons (0 : ℝ) t : Fin (n + 1) → ℝ) j) ∧
∀ i : Fin n, t i < (T : ℝ)}
rw [Set.ofPred_and]
apply MeasurableSet.inter
· simpa only [← Set.ofPred_forall] using (MeasurableSet.iInter fun (i : Fin (n + 1)) =>
MeasurableSet.iInter fun (j : Fin (n + 1)) =>
MeasurableSet.iInter fun (_ : i < j) => measurableSet_lt (hcons i) (hcons j))
· simpa only [← Set.ofPred_forall] using (MeasurableSet.iInter fun (i : Fin n) =>
measurableSet_lt (measurable_pi_apply i) (measurable_const (a := (T : ℝ))))
have hmσ : SigmaFinite ((m n T).map (fun t : Prefix n T => t.val)) := by
change SigmaFinite ((Measure.comap (fun t : Prefix n T => t.val)
(volume : Measure (Fin n → ℝ))).map (fun t : Prefix n T => t.val))
rw [map_comap_subtype_coe hs]
infer_instance
letI : SigmaFinite (m n T) := SigmaFinite.of_map (m n T) measurable_subtype_coe.aemeasurable hmσ
ASTIS completion of the phase-law proportionality. Exact compiled region; every analytic ingredient is derived from the original assumptions.
5. Identify the normalized phase density
C2 regularity makes the phase Gibbs weight measurable. The existing phase normalization theorem proves that its reciprocal-partition density on phase volume is exactly pi_y times the standard Gaussian. Its positivity and finiteness are supplied by that theorem, not by extra binders here.
Corresponding Lean step
let U : E × E → ℝ := fun z => V z.1 + ‖z.1 - y‖ ^ 2 / (2 * η) + ‖z.2‖ ^ 2 / 2
let w : E × E → ℝ := fun z => Real.exp (-U z)
let ell : Measure (E × E) := (volume : Measure E).prod (volume : Measure E)
let cNorm : ℝ≥0∞ := (∫⁻ z, ENNReal.ofReal (w z) ∂ell)⁻¹
let W : (E × E) × Prefix n T → ℝ≥0∞ :=
fun x => ENNReal.ofReal (w x.1) * ρ y r x.1 n T x.2
have hU : Continuous U := by
exact ((hV.continuous.comp continuous_fst).add
(((continuous_fst.sub continuous_const).norm.pow 2).div_const (2 * η))).add
((continuous_snd.norm.pow 2).div_const 2)
have hw : Measurable (fun z => ENNReal.ofReal (w z)) :=
ENNReal.measurable_ofReal.comp (Real.continuous_exp.comp hU.neg).measurable
have hW : Measurable W := (hw.comp measurable_fst).mul hρ
have hf : Measurable (fun z => cNorm * ENNReal.ofReal (w z)) := measurable_const.mul hw
have hphase : ell.withDensity (fun z => cNorm * ENNReal.ofReal (w z)) =
(piY y).prod gamma :=
(AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPhaseNormalization.actual_phase_gibbs_normalization
hα hαβ hV hH hη hβη y).2.2.2.2.2.2
ASTIS completion of the phase-law proportionality. Exact compiled region; every analytic ingredient is derived from the original assumptions.
6. Rewrite the actual normalized sector measure
Use the product-with-density identity, justified by simplex sigma-finiteness. Combine the measurable initial phase density with the actual event density; associativity leaves one constant normalizer multiplying the previous unnormalized weight.
Corresponding Lean step
have hsigma : sigma = (ell.prod (m n T)).withDensity (fun x => cNorm * W x) := by
change (((piY y).prod gamma).prod (m n T)).withDensity
(fun x => ρ y r x.1 n T x.2) = _
rw [← hphase, prod_withDensity_left hf,
← withDensity_mul _
(f := fun x : (E × E) × Prefix n T => cNorm * ENNReal.ofReal (w x.1))
(g := fun x => ρ y r x.1 n T x.2) (hf.comp measurable_fst) hρliteral]
congr 1
funext x
exact mul_assoc _ _ _
ASTIS completion of the phase-law proportionality. Exact compiled region; every analytic ingredient is derived from the original assumptions.
7. Prove preservation of the full normalized sector
Test the pushed-forward measure against every measurable extended-nonnegative F. Rewrite the two density integrals, factor out the constant normalizer and apply the actual unnormalized weighted-sector substitution. Equality of all these integrals proves the full measure identity; no finite integral or cancellation is needed.
Corresponding Lean step
have hsector : MeasurePreserving Theta sigma sigma := by
refine ⟨hTheta, ?_⟩
apply Measure.ext_of_lintegral
intro F hF
rw [lintegral_map hF hTheta, hsigma]
rw [lintegral_withDensity_eq_lintegral_mul _
(f := fun x => cNorm * W x) (g := fun x => F (Theta x))
(measurable_const.mul hW) (hF.comp hTheta),
lintegral_withDensity_eq_lintegral_mul _
(f := fun x => cNorm * W x) (g := fun x => F x)
(measurable_const.mul hW) hF]
simp only [Pi.mul_apply, mul_assoc]
rw [lintegral_const_mul cNorm (f := fun x => W x * F (Theta x))
(hW.mul (hF.comp hTheta)),
lintegral_const_mul cNorm (f := fun x => W x * F x) (hW.mul hF)]
exact congrArg (fun a => cNorm * a) (h102 y r F hF)
ASTIS completion of the phase-law proportionality. Exact compiled region; every analytic ingredient is derived from the original assumptions.
8. Push the reversal to endpoint pairs
Apply composition of measurable pushforwards and the endpoint intertwining. This transports the full normalized-sector identity through B to precisely the declared endpoint-pair measure L.
Corresponding Lean step
refine ⟨hJ, ?_⟩
change Measure.map J (Measure.map B sigma) = Measure.map B sigma
rw [Measure.map_map hJ hB]
calc
Measure.map (J ∘ B) sigma = Measure.map (B ∘ Theta) sigma := by
congr 1
funext x
exact (hinter x).symm
_ = Measure.map B (Measure.map Theta sigma) := (Measure.map_map hB hTheta).symm
_ = Measure.map B sigma := by rw [hsector.map_eq]
ASTIS completion of the phase-law proportionality. Exact compiled region; every analytic ingredient is derived from the original assumptions.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · actual_normalized_endpoint_sector_reversal
Align the two event-time reversal witnesses; Construct the measurable endpoint diagram; Recover joint measurability of the actual density; Justify the simplex measure product; Identify the normalized phase density; Rewrite the actual normalized sector measure; Prove preservation of the full normalized sector; Push the reversal to endpoint pairs
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_normalized_endpoint_sector_reversal
{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_normalized_endpoint_sector_statement hα hαβ hV hH hη hβη := by
classical
unfold actual_normalized_endpoint_sector_statement
intro c Φ S rate Λ Rec Hist Δ Prefix zAt K qReal q liveTime d weight Path Ψ Γ ρ R Vy piY gamma m y r n T A B sigma L J
obtain ⟨rhoTime, hrho, h97⟩ :=
AutoSamplingTheory.ExampleCases.ProximalBPS.ActualEndpointTimeReversal.actual_endpoint_time_reversal_laws
hα hαβ hV hH hη hβη n T
obtain ⟨rho102, hrho102, h102⟩ :=
AutoSamplingTheory.ExampleCases.ProximalBPS.ActualWeightedSector.actual_weighted_sector_lintegral
hα hαβ hV hH hη hβη n T
have halign : rho102 = rhoTime := by
funext t
apply Subtype.ext
funext i
exact (hrho102 t i).trans (hrho t i).symm
subst rho102
rcases h97 with ⟨hTimeM, hTimeI, hTimeP, hAformula, hAjoint, hAvolume,
hArev, hThetajoint, hThetaI, hThetaP⟩
let Theta : (E × E) × Prefix n T → (E × E) × Prefix n T :=
fun q => (R (A q), rhoTime q.2)
have hemb : Measurable (fun q : (E × E) × Prefix n T => (((y, r), q.1), q.2)) :=
(measurable_const.prodMk measurable_fst).prodMk measurable_snd
have hA : Measurable A := hAjoint.comp hemb
have hB : Measurable B := measurable_fst.prodMk hA
have hR : Measurable R := measurable_fst.prodMk measurable_snd.neg
have hJ : Measurable J := (hR.comp measurable_snd).prodMk (hR.comp measurable_fst)
have hTheta : Measurable Theta := hThetajoint.comp hemb
have hinter (x : (E × E) × Prefix n T) : B (Theta x) = J (B x) := by
apply Prod.ext
· rfl
· exact hArev y r x.1 x.2
obtain ⟨Z, hZ⟩ :=
AutoSamplingTheory.ExampleCases.ProximalBPS.ActualFiniteCountPath.actual_finite_count_path_law
hα hαβ hV hH hη hβη
have hρjoint : Measurable (fun p : ((E × E) × (E × E)) × Prefix n T =>
ρ p.1.1.1 p.1.1.2 p.1.2 n T p.2) := (hZ.2.2.2.2 n T).2.2.1
have hρ := hρjoint.comp hemb
have hρliteral : Measurable (fun x : (E × E) × Prefix n T => ρ y r x.1 n T x.2) := by
simpa only [Function.comp_def] using hρ
have hcons (i : Fin (n + 1)) :
Measurable (fun t : Fin n → ℝ => (Fin.cons (0 : ℝ) t : Fin (n + 1) → ℝ) i) := by
induction i using Fin.cases with
| zero => exact measurable_const
| succ i => exact measurable_pi_apply i
have hs : MeasurableSet (Δ n T) := by
change MeasurableSet {t : Fin n → ℝ |
(∀ i j : Fin (n + 1), i < j → (Fin.cons (0 : ℝ) t : Fin (n + 1) → ℝ) i < (Fin.cons (0 : ℝ) t : Fin (n + 1) → ℝ) j) ∧
∀ i : Fin n, t i < (T : ℝ)}
rw [Set.ofPred_and]
apply MeasurableSet.inter
· simpa only [← Set.ofPred_forall] using (MeasurableSet.iInter fun (i : Fin (n + 1)) =>
MeasurableSet.iInter fun (j : Fin (n + 1)) =>
MeasurableSet.iInter fun (_ : i < j) => measurableSet_lt (hcons i) (hcons j))
· simpa only [← Set.ofPred_forall] using (MeasurableSet.iInter fun (i : Fin n) =>
measurableSet_lt (measurable_pi_apply i) (measurable_const (a := (T : ℝ))))
have hmσ : SigmaFinite ((m n T).map (fun t : Prefix n T => t.val)) := by
change SigmaFinite ((Measure.comap (fun t : Prefix n T => t.val)
(volume : Measure (Fin n → ℝ))).map (fun t : Prefix n T => t.val))
rw [map_comap_subtype_coe hs]
infer_instance
letI : SigmaFinite (m n T) := SigmaFinite.of_map (m n T) measurable_subtype_coe.aemeasurable hmσ
let U : E × E → ℝ := fun z => V z.1 + ‖z.1 - y‖ ^ 2 / (2 * η) + ‖z.2‖ ^ 2 / 2
let w : E × E → ℝ := fun z => Real.exp (-U z)
let ell : Measure (E × E) := (volume : Measure E).prod (volume : Measure E)
let cNorm : ℝ≥0∞ := (∫⁻ z, ENNReal.ofReal (w z) ∂ell)⁻¹
let W : (E × E) × Prefix n T → ℝ≥0∞ :=
fun x => ENNReal.ofReal (w x.1) * ρ y r x.1 n T x.2
have hU : Continuous U := by
exact ((hV.continuous.comp continuous_fst).add
(((continuous_fst.sub continuous_const).norm.pow 2).div_const (2 * η))).add
((continuous_snd.norm.pow 2).div_const 2)
have hw : Measurable (fun z => ENNReal.ofReal (w z)) :=
ENNReal.measurable_ofReal.comp (Real.continuous_exp.comp hU.neg).measurable
have hW : Measurable W := (hw.comp measurable_fst).mul hρ
have hf : Measurable (fun z => cNorm * ENNReal.ofReal (w z)) := measurable_const.mul hw
have hphase : ell.withDensity (fun z => cNorm * ENNReal.ofReal (w z)) =
(piY y).prod gamma :=
(AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPhaseNormalization.actual_phase_gibbs_normalization
hα hαβ hV hH hη hβη y).2.2.2.2.2.2
have hsigma : sigma = (ell.prod (m n T)).withDensity (fun x => cNorm * W x) := by
change (((piY y).prod gamma).prod (m n T)).withDensity
(fun x => ρ y r x.1 n T x.2) = _
rw [← hphase, prod_withDensity_left hf,
← withDensity_mul _
(f := fun x : (E × E) × Prefix n T => cNorm * ENNReal.ofReal (w x.1))
(g := fun x => ρ y r x.1 n T x.2) (hf.comp measurable_fst) hρliteral]
congr 1
funext x
exact mul_assoc _ _ _
have hsector : MeasurePreserving Theta sigma sigma := by
refine ⟨hTheta, ?_⟩
apply Measure.ext_of_lintegral
intro F hF
rw [lintegral_map hF hTheta, hsigma]
rw [lintegral_withDensity_eq_lintegral_mul _
(f := fun x => cNorm * W x) (g := fun x => F (Theta x))
(measurable_const.mul hW) (hF.comp hTheta),
lintegral_withDensity_eq_lintegral_mul _
(f := fun x => cNorm * W x) (g := fun x => F x)
(measurable_const.mul hW) hF]
simp only [Pi.mul_apply, mul_assoc]
rw [lintegral_const_mul cNorm (f := fun x => W x * F (Theta x))
(hW.mul (hF.comp hTheta)),
lintegral_const_mul cNorm (f := fun x => W x * F x) (hW.mul hF)]
exact congrArg (fun a => cNorm * a) (h102 y r F hF)
refine ⟨hJ, ?_⟩
change Measure.map J (Measure.map B sigma) = Measure.map B sigma
rw [Measure.map_map hJ hB]
calc
Measure.map (J ∘ B) sigma = Measure.map (B ∘ Theta) sigma := by
congr 1
funext x
exact (hinter x).symm
_ = Measure.map B (Measure.map Theta sigma) := (Measure.map_map hB hTheta).symm
_ = Measure.map B sigma := by rw [hsector.map_eq]
#print axioms actual_normalized_endpoint_sector_reversal
end
end AutoSamplingTheory.ExampleCases.ProximalBPS.ActualNormalizedEndpointSectorSource assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| Fixed-count change of variables followed by initial Gibbs averaging. | Exact measure-preserving flipped swap for the actual normalized endpoint-pair sector. | same | ASTIS states the measure identity underlying the source calculation and derives all measurability and normalization ingredients. |
| Finite-dimensional Euclidean phase. | Finite real Hilbert Borel space including rank zero. | generalization | Coordinate-free canonical volume and standard Gaussian retain the formulas. |
| Original six analytic assumptions. | The same six assumptions; no proof ingredient is a supplied premise. | same | The exact presealed proposition is unchanged. |
| Full stationary averaging and invariant process. | Only a fixed-count normalized endpoint-pair measure identity. | unresolved | Actual normalized fixed-count endpoint-pair measure reversal only. Countable assembly, signed bilinear identity, process invariance, Markovness, hypocoercivity, implementation error, actual expected costs and all full paper/composition results remain open. |
Actual normalized fixed-count endpoint-pair measure reversal only. Countable assembly, signed bilinear identity, process invariance, Markovness, hypocoercivity, implementation error, actual expected costs and all full paper/composition results remain open.
Encoder–denoiser: accepted · equivalent-after-elaboration
Detected semantic differences
- domains: Coordinate-free finite real Hilbert Borel presentation includes rank zero. — The actual producers preserve the source formulas and Gaussian/volume conventions; no positive-rank hypothesis is introduced.
- conclusion: Explicit measure-theoretic completion of one normalized endpoint-pair sector. — Current201-226 proves the fixed-sector transport with nonnegative tests, without finite integral or sector-mass assumptions.
- scopes: Later averaging and process conclusions remain explicitly outside this bounded result. — Publication supports only normalized-endpoint-sector; weighted-invariance remains an unresolved obligation. All source regions and red nodes are accounted for.
A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.
Scope and omitted-condition boundaries
- Actual normalized fixed-count endpoint-pair measure reversal only. Countable assembly, signed bilinear identity, process invariance, Markovness, hypocoercivity, implementation error, actual expected costs and all full paper/composition results remain open.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
AutoSamplingTheory.ExampleCases.ProximalBPS.ActualFiniteCountPath.actual_finite_count_path_lawAutoSamplingTheory.ExampleCases.ProximalBPS.ActualEndpointTimeReversal.actual_endpoint_time_reversal_lawsAutoSamplingTheory.ExampleCases.ProximalBPS.ActualWeightedSector.actual_weighted_sector_lintegralAutoSamplingTheory.ExampleCases.ProximalBPS.ActualPhaseNormalization.actual_phase_gibbs_normalization
Mathlib API called (external library)
- MeasurableSet.iInter
- Set.ofPred_forall
- Set.ofPred_and
- map_comap_subtype_coe
- SigmaFinite.of_map
- prod_withDensity_left
- withDensity_mul
- Measure.ext_of_lintegral
- lintegral_map
- lintegral_withDensity_eq_lintegral_mul
- lintegral_const_mul
- Measure.map_map
Mathematical sources
- Appendix A.1 fixed-count change of variables and initial Eq3.1 Gibbs averaging; actual normalized endpoint-pair sector measure reversal. — Actual normalized fixed-count endpoint-pair measure reversal only. Countable assembly, signed bilinear identity, process invariance, Markovness, hypocoercivity, implementation error, actual expected costs and all full paper/composition results 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.