Actual PBPS phase-volume preservation and reversal
AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPhaseReversalVolume.actual_phase_reversal_volume_laws · theorem · Teaching coverage
Mathematical statement
Let E be a finite-dimensional real inner-product space equipped with its Borel sigma algebra, including dimension zero. Let V:E→R, alpha,beta≥0 and eta in R. Assume alpha>0, alpha≤beta, V is C2, alpha||v||^2≤D2V(x)[v,v]≤beta||v||^2 for every x,v in E, eta>0 and beta*eta≤1. These are the six original analytic assumptions; there is no supplied volume, measurability, inverse-map or integral identity premise. For every y,r in E put c(y,r)=y-eta grad V(r), h(r,x)=grad V(x)-grad V(r), B(n,p)=p-(2<p,n>/||n||^2)n and S_r(x,p)=(x,B(h(r,x),p)). Put R(x,p)=(x,-p) and Phi_(y,r,u)(x,p)=(c+cos(u)(x-c)+sqrt(eta)sin(u)p, -sin(u)/sqrt(eta)(x-c)+cos(u)p), lambda_r(x,p)=sqrt(eta)max(0,<p,h(r,x)>), ell=volume_E tensor volume_E. Volume_E is the canonical Hilbert-space Lebesgue/Haar volume. Division by zero in B is totalized by zero, hence B(0,p)=p; no nonzero-normal hypothesis is imposed. The map ((y,r),(u,z))→Phi_(y,r,u)(z) is jointly Borel measurable on (E x E) x R x (E x E); (r,z)→S_r(z) and (r,z)→lambda_r(z) are jointly Borel measurable. For every y,r,u, Phi_(y,r,u) preserves ell. For every r, S_r preserves ell, and R preserves ell. Preservation means a measurable map whose pushforward of ell equals ell. For every y,r,u,z, both Phi_(y,r,-u)(Phi_(y,r,u)(z))=z and Phi_(y,r,u)(Phi_(y,r,-u)(z))=z. For every r,z, S_r(S_r(z))=z; for every z, R(R(z))=z. For every y,r,u,z, R(Phi_(y,r,u)(R(z)))=Phi_(y,r,-u)(z). For every r,z, R(S_r(z))=S_r(R(z)) and lambda_r(R(S_r(z)))=lambda_r(z). Finally, for every r and real-valued F on E x E that is Bochner integrable with respect to ell, F composed with S_r is ell-integrable and integral F(S_r(z)) d ell(z)=integral F(z) d ell(z). These assertions include all real times u, zero normals and rank zero. They assert phase product-volume preservation, not preservation of the unscaled phase-space norm. The real integrable-test clause is the A6 change-of-variables consequence. The elementary phase reversal laws supply dependencies for later prescribed-path reversal; they assert no pointwise reversal of a right-continuous path at its jumps, no stationary/Gibbs invariant law, Markov semigroup, hypocoercivity, implementation error, expected oracle cost, main sampling theorem or actual-input composition.
Lean statement · actual_phase_reversal_volume_laws
Let E be a finite-dimensional real inner-product space equipped with its Borel sigma algebra, including dimension zero. Let V:E->R, alpha,beta>=0 and eta in R. Assume alpha>0, alpha<=beta, V is C2, alpha||v||^2<=D2V(x)[v,v]<=beta||v||^2 for every x,v in E, eta>0 and beta*eta<=1. These are the six original analytic assumptions; there is no supplied volume, measurability, inverse-map or integral identity premise. For every y,r in E put c(y,r)=y-eta grad V(r), h(r,x)=grad V(x)-grad V(r), B(n,p)=p-(2<p,n>/||n||^2)n and S_r(x,p)=(x,B(h(r,x),p)). Put R(x,p)=(x,-p) and Phi_(y,r,u)(x,p)=(c+cos(u)(x-c)+sqrt(eta)sin(u)p, -sin(u)/sqrt(eta)(x-c)+cos(u)p), lambda_r(x,p)=sqrt(eta)max(0,<p,h(r,x)>), ell=volume_E tensor volume_E. Volume_E is the canonical Hilbert-space Lebesgue/Haar volume. Division by zero in B is totalized by zero, hence B(0,p)=p; no nonzero-normal hypothesis is imposed. The map ((y,r),(u,z))->Phi_(y,r,u)(z) is jointly Borel measurable on (E x E) x R x (E x E); (r,z)->S_r(z) and (r,z)->lambda_r(z) are jointly Borel measurable. For every y,r,u, Phi_(y,r,u) preserves ell. For every r, S_r preserves ell, and R preserves ell. Preservation means a measurable map whose pushforward of ell equals ell. For every y,r,u,z, both Phi_(y,r,-u)(Phi_(y,r,u)(z))=z and Phi_(y,r,u)(Phi_(y,r,-u)(z))=z. For every r,z, S_r(S_r(z))=z; for every z, R(R(z))=z. For every y,r,u,z, R(Phi_(y,r,u)(R(z)))=Phi_(y,r,-u)(z). For every r,z, R(S_r(z))=S_r(R(z)) and lambda_r(R(S_r(z)))=lambda_r(z). Finally, for every r and real-valued F on E x E that is Bochner integrable with respect to ell, F composed with S_r is ell-integrable and integral F(S_r(z)) d ell(z)=integral F(z) d ell(z). These assertions include all real times u, zero normals and rank zero. They assert phase product-volume preservation, not preservation of the unscaled phase-space norm. The real integrable-test clause is the A6 change-of-variables consequence. The elementary phase reversal laws supply dependencies for later prescribed-path reversal; they assert no pointwise reversal of a right-continuous path at its jumps, no stationary/Gibbs invariant law, Markov semigroup, hypocoercivity, implementation error, expected oracle cost, main sampling theorem or actual-input composition.
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_phase_reversal_volume_laws
{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_phase_reversal_volume_statement hα hαβ hV hH hη hβηFull Lean proposition (definition) · actual_phase_reversal_volume_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_phase_reversal_volume_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 :=
let c : E → E → E := fun y r => y - η • gradient V r
let h : E → E → E := fun r x => gradient V x - gradient V r
let B : E → E → E := fun n p => p - (2 * inner ℝ p n / ‖n‖ ^ 2) • n
let S : E → (E × E) → (E × E) := fun r z => (z.1, B (h r z.1) z.2)
let R : (E × E) → (E × E) := fun z => (z.1, -z.2)
let Φ : E → E → ℝ → (E × E) → (E × E) := fun y r u z =>
(c y r + Real.cos u • (z.1 - c y r) + (Real.sqrt η * Real.sin u) • z.2,
(-Real.sin u / Real.sqrt η) • (z.1 - c y r) + Real.cos u • z.2)
let rate : E → (E × E) → ℝ := fun r z =>
Real.sqrt η * max 0 (inner ℝ z.2 (h r z.1))
let ell : Measure (E × E) := (volume : Measure E).prod (volume : Measure E)
Measurable (fun a : (E × E) × ℝ × (E × E) => Φ a.1.1 a.1.2 a.2.1 a.2.2) ∧
Measurable (fun a : E × (E × E) => S a.1 a.2) ∧
Measurable (fun a : E × (E × E) => rate a.1 a.2) ∧
(∀ y r : E, ∀ u : ℝ, MeasurePreserving (Φ y r u) ell ell) ∧
(∀ r : E, MeasurePreserving (S r) ell ell) ∧
MeasurePreserving R ell ell ∧
(∀ y r : E, ∀ u : ℝ, ∀ z : E × E,
Φ y r (-u) (Φ y r u z) = z ∧ Φ y r u (Φ y r (-u) z) = z) ∧
(∀ r : E, ∀ z : E × E, S r (S r z) = z) ∧
(∀ z : E × E, R (R z) = z) ∧
(∀ y r : E, ∀ u : ℝ, ∀ z : E × E, R (Φ y r u (R z)) = Φ y r (-u) z) ∧
(∀ r : E, ∀ z : E × E, R (S r z) = S r (R z)) ∧
(∀ r : E, ∀ z : E × E, rate r (R (S r z)) = rate r z) ∧
(∀ r : E, ∀ F : (E × E) → ℝ, Integrable F ell →
Integrable (fun z => F (S r z)) ell ∧
(∫ z, F (S r z) ∂ell) = ∫ z, F z ∂ell)
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
[FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]Proof roadmap
- 1Preserve product volume under elementary shears
For L_a(x,p)=(x,p+a x), each fixed-x momentum map is a translation and preserves volume_E. Joint measurability and the skew-product theorem therefore preserve ell. Swapping coordinates before and after L_a gives U_a(x,p)=(x+a p,p), also volume preserving. Negation on both coordinates is a product of linear isometries, so it preserves ell as well. These are the elementary maps used below.
- 2Identify every bounce fiber with an orthogonal reflection
For fixed n, the literal formula B(n,p) equals reflection in the orthogonal complement of span(n). In finite dimension this reflection is a linear isometry equivalence, hence preserves canonical volume_E. If n=0, its orthogonal complement is all E and the formula is the identity, so this proof requires no division by a nonzero norm. This is a fiber statement; joint Borel measurability of the state-dependent bounce is supplied separately by the verified bounce theorem.
- 3Factor the linear harmonic matrix into three shears
Suppose a^2-bc=1 and 1+a is nonzero. Set k=b/(1+a). The determinant identity gives ck=a-1, while k(1+a)=b. Expanding U_k composed with L_c composed with U_k gives diagonal coefficients 1+ck=a and upper-right coefficient 2k+k^2 c=k(1+a)=b; its lower-left coefficient is c. Composition of these three preserved-volume maps proves the matrix map preserves ell, without choosing coordinates or assuming positive dimension.
- 4Cover every harmonic time and restore the center
Use a=cos(u), b=sqrt(eta)sin(u), c=-sin(u)/sqrt(eta). Since eta>0, sqrt(eta) is nonzero, and sin^2(u)+cos^2(u)=1 gives a^2-bc=1. If 1+cos(u) is nonzero, apply the shear factorization. Otherwise cos(u)=-1 and the same trigonometric identity forces sin(u)=0, so the linear map is simultaneous negation. Finally translate x by minus the center, apply the linear map, and translate back. Position translations preserve ell, giving the exact affine Phi for all u.
- 5Assemble actual joint Borel maps and phase-volume laws
Reuse the verified actual harmonic-flow theorem for joint Borel measurability and both inverse-flow identities, and the actual bounce theorem for joint Borel rate/bounce maps and the bounce involution. For each fixed reference r, combine measurable S_r with volume preservation of its momentum reflection at every x through the skew-product theorem. This proves S_r preserves ell. Momentum reversal is identity on x times momentum negation and also preserves ell. The affine proof above supplies flow volume preservation.
- 6Check reversal and rate pairing with the actual formulas
Momentum negation is involutive. Substitute the flow formula and use cos(-u)=cos(u), sin(-u)=-sin(u) to obtain R Phi_u R=Phi_(-u). Reflection is linear in momentum, including n=0, so R S_r=S_r R. The verified reflection identity <B(n,p),n≥-<p,n> shows that the additional momentum negation in R S_r restores the inner product; applying the same positive-part rate formula gives lambda_r(R S_r z)=lambda_r(z). These are phase identities, not path reversal assertions at jump values.
- 7Derive the full real integrable-test identity
Fix r and an ell-integrable real F. Measure preservation transports integrability to F composed with S_r. The measurable involution S_r is a measurable equivalence, and its pushforward identity supplies change of variables for the real integral. Thus both integrability and the exact A6 equality follow from the proved phase map. Integrability of F specifies the test class; volume preservation and invertibility are conclusions already proved inside this theorem.
Full assumptions and notation
All objects and hypotheses
- Finite-dimensional real inner-product Borel E, 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.
- All y,r in E and all real times u; all phase points, including zero reflection normals.
- A6 test class: each real F is Bochner integrable against the explicitly defined product volume ell.
- Measurability, volume preservation, inverse identities and integrability after bounce are proved conclusions, not supplied provider assumptions.
Mathematical proof
1. Preserve product volume under elementary shears
For L_a(x,p)=(x,p+a x), each fixed-x momentum map is a translation and preserves volume_E. Joint measurability and the skew-product theorem therefore preserve ell. Swapping coordinates before and after L_a gives U_a(x,p)=(x+a p,p), also volume preserving. Negation on both coordinates is a product of linear isometries, so it preserves ell as well. These are the elementary maps used below.
Corresponding Lean step
private theorem lower_shear (a : ℝ) :
MeasurePreserving (fun z : E × E => (z.1, z.2 + a • z.1))
((volume : Measure E).prod volume) ((volume : Measure E).prod volume) := by
exact (MeasurePreserving.id (volume : Measure E)).skew_product
(measurable_snd.add (measurable_fst.const_smul a))
(Filter.Eventually.of_forall fun x => (measurePreserving_add_right volume (a • x)).map_eq)
private theorem upper_shear (a : ℝ) :
MeasurePreserving (fun z : E × E => (z.1 + a • z.2, z.2))
((volume : Measure E).prod volume) ((volume : Measure E).prod volume) := by
simpa only [Function.comp_def, Prod.swap_prod_mk, Prod.fst_swap, Prod.snd_swap] using
(Measure.measurePreserving_swap.comp (lower_shear (E := E) a)).comp Measure.measurePreserving_swap
private theorem negate_phase :
MeasurePreserving (fun z : E × E => (-z.1, -z.2))
((volume : Measure E).prod volume) ((volume : Measure E).prod volume) := by
exact (LinearIsometryEquiv.neg ℝ).measurePreserving.prod
(LinearIsometryEquiv.neg ℝ).measurePreserving
Exact compiled proof region; all private volume and algebra premises are discharged internally in the public theorem.
2. Identify every bounce fiber with an orthogonal reflection
For fixed n, the literal formula B(n,p) equals reflection in the orthogonal complement of span(n). In finite dimension this reflection is a linear isometry equivalence, hence preserves canonical volume_E. If n=0, its orthogonal complement is all E and the formula is the identity, so this proof requires no division by a nonzero norm. This is a fiber statement; joint Borel measurability of the state-dependent bounce is supplied separately by the verified bounce theorem.
Corresponding Lean step
private theorem reflect_fiber (n : E) :
MeasurePreserving (fun p : E => p - (2 * inner ℝ p n / ‖n‖ ^ 2) • n)
volume volume := by
let : CompleteSpace E := FiniteDimensional.complete ℝ E
have heq : (fun p : E => p - (2 * inner ℝ p n / ‖n‖ ^ 2) • n) =
(fun p => (ℝ ∙ n)ᗮ.reflection p) := by
funext p
rw [Submodule.reflection_orthogonal_apply, Submodule.reflection_singleton_apply]
simp only [two_smul, neg_sub, div_eq_mul_inv, mul_smul]
rw [real_inner_comm n p]
module
rw [heq]
exact ((ℝ ∙ n)ᗮ.reflection).measurePreserving
Exact compiled proof region; all private volume and algebra premises are discharged internally in the public theorem.
3. Factor the linear harmonic matrix into three shears
Suppose a^2-bc=1 and 1+a is nonzero. Set k=b/(1+a). The determinant identity gives ck=a-1, while k(1+a)=b. Expanding U_k composed with L_c composed with U_k gives diagonal coefficients 1+ck=a and upper-right coefficient 2k+k^2 c=k(1+a)=b; its lower-left coefficient is c. Composition of these three preserved-volume maps proves the matrix map preserves ell, without choosing coordinates or assuming positive dimension.
Corresponding Lean step
private theorem area_matrix (a b c : ℝ) (hd : a * a - b * c = 1)
(ha : 1 + a ≠ 0) :
MeasurePreserving (fun z : E × E => (a • z.1 + b • z.2, c • z.1 + a • z.2))
((volume : Measure E).prod volume) ((volume : Measure E).prod volume) := by
let k : ℝ := b / (1 + a)
have hk : c * k = a - 1 := by
dsimp [k]
rw [← mul_div_assoc]
apply (div_eq_iff ha).2
nlinarith [hd]
have hb : k * (1 + a) = b := by dsimp [k]; exact div_mul_cancel₀ b ha
have heq : (fun z : E × E => (a • z.1 + b • z.2, c • z.1 + a • z.2)) =
(fun z : E × E => (z.1 + k • z.2, z.2)) ∘
(fun z : E × E => (z.1, z.2 + c • z.1)) ∘
(fun z : E × E => (z.1 + k • z.2, z.2)) := by
funext z
apply Prod.ext <;> dsimp only [Function.comp_def] <;> match_scalars <;>
nlinarith [hk, hb, congrArg (fun x : ℝ => k * x) hk]
rw [heq]
exact (upper_shear k).comp ((lower_shear c).comp (upper_shear k))
Exact compiled proof region; all private volume and algebra premises are discharged internally in the public theorem.
4. Cover every harmonic time and restore the center
Use a=cos(u), b=sqrt(eta)sin(u), c=-sin(u)/sqrt(eta). Since eta>0, sqrt(eta) is nonzero, and sin^2(u)+cos^2(u)=1 gives a^2-bc=1. If 1+cos(u) is nonzero, apply the shear factorization. Otherwise cos(u)=-1 and the same trigonometric identity forces sin(u)=0, so the linear map is simultaneous negation. Finally translate x by minus the center, apply the linear map, and translate back. Position translations preserve ell, giving the exact affine Phi for all u.
Corresponding Lean step
private theorem harmonic_linear (η u : ℝ) (hη : 0 < η) :
MeasurePreserving (fun z : E × E =>
(Real.cos u • z.1 + (Real.sqrt η * Real.sin u) • z.2,
(-Real.sin u / Real.sqrt η) • z.1 + Real.cos u • z.2))
((volume : Measure E).prod volume) ((volume : Measure E).prod volume) := by
have hr : Real.sqrt η ≠ 0 := ne_of_gt (Real.sqrt_pos.mpr hη)
by_cases ha : 1 + Real.cos u = 0
· have hc : Real.cos u = -1 := by linarith
have hs : Real.sin u = 0 := by nlinarith [Real.sin_sq_add_cos_sq u, sq_nonneg (Real.sin u)]
simpa only [hc, hs, mul_zero, neg_zero, zero_div, zero_smul, add_zero, zero_add,
neg_one_smul] using (negate_phase (E := E))
· apply area_matrix _ _ _ _ ha
field_simp [hr]
nlinarith [Real.sin_sq_add_cos_sq u]
private theorem translate_position (d : E) :
MeasurePreserving (fun z : E × E => (d + z.1, z.2))
((volume : Measure E).prod volume) ((volume : Measure E).prod volume) := by
exact (measurePreserving_add_left volume d).prod (MeasurePreserving.id volume)
private theorem harmonic_affine (η u : ℝ) (hη : 0 < η) (d : E) :
MeasurePreserving (fun z : E × E =>
(d + Real.cos u • (z.1 - d) + (Real.sqrt η * Real.sin u) • z.2,
(-Real.sin u / Real.sqrt η) • (z.1 - d) + Real.cos u • z.2))
((volume : Measure E).prod volume) ((volume : Measure E).prod volume) := by
have heq : (fun z : E × E =>
(d + Real.cos u • (z.1 - d) + (Real.sqrt η * Real.sin u) • z.2,
(-Real.sin u / Real.sqrt η) • (z.1 - d) + Real.cos u • z.2)) =
(fun z : E × E => (d + z.1, z.2)) ∘
(fun z : E × E => (Real.cos u • z.1 + (Real.sqrt η * Real.sin u) • z.2,
(-Real.sin u / Real.sqrt η) • z.1 + Real.cos u • z.2)) ∘
(fun z : E × E => (-d + z.1, z.2)) := by
funext z
apply Prod.ext <;> dsimp only [Function.comp_def] <;> module
rw [heq]
exact (translate_position d).comp ((harmonic_linear η u hη).comp (translate_position (-d)))
Exact compiled proof region; all private volume and algebra premises are discharged internally in the public theorem.
5. Assemble actual joint Borel maps and phase-volume laws
Reuse the verified actual harmonic-flow theorem for joint Borel measurability and both inverse-flow identities, and the actual bounce theorem for joint Borel rate/bounce maps and the bounce involution. For each fixed reference r, combine measurable S_r with volume preservation of its momentum reflection at every x through the skew-product theorem. This proves S_r preserves ell. Momentum reversal is identity on x times momentum negation and also preserves ell. The affine proof above supplies flow volume preservation.
Corresponding Lean step
have hf := AutoSamplingTheory.ExampleCases.ProximalBPS.ActualHarmonicFlow.actual_harmonic_flow_laws
hα hαβ hV hH hη hβη
have hb := AutoSamplingTheory.ExampleCases.ProximalBPS.ActualBounceRate.actual_bounce_rate_energy_laws
hα hαβ hV hH hη hβη
have hSm : Measurable (fun a : E × (E × E) => S a.1 a.2) := hb.1
have hSi (r : E) : Function.Involutive (S r) := fun z => (hb.2.2.2.2.2.1 r z).2
have hSmp (r : E) : MeasurePreserving (S r) ell ell := by
exact (MeasurePreserving.id (volume : Measure E)).skew_product
(hSm.comp (measurable_const.prodMk measurable_id)).snd
(Filter.Eventually.of_forall fun x => (reflect_fiber (h r x)).map_eq)
refine ⟨hf.2.1, hSm, hb.2.2.1, ?_, hSmp, ?_, hf.2.2.2.2.1, hSi, ?_, ?_, ?_, ?_, ?_⟩
· intro y r u
exact harmonic_affine η u hη (c y r)
· exact (MeasurePreserving.id (volume : Measure E)).prod
(LinearIsometryEquiv.neg ℝ).measurePreserving
Exact compiled proof region; all private volume and algebra premises are discharged internally in the public theorem.
6. Check reversal and rate pairing with the actual formulas
Momentum negation is involutive. Substitute the flow formula and use cos(-u)=cos(u), sin(-u)=-sin(u) to obtain R Phi_u R=Phi_(-u). Reflection is linear in momentum, including n=0, so R S_r=S_r R. The verified reflection identity <B(n,p),n≥-<p,n> shows that the additional momentum negation in R S_r restores the inner product; applying the same positive-part rate formula gives lambda_r(R S_r z)=lambda_r(z). These are phase identities, not path reversal assertions at jump values.
Corresponding Lean step
· intro z
simp [R]
· intro y r u z
apply Prod.ext <;> dsimp [R, Φ] <;>
simp only [Real.cos_neg, Real.sin_neg, neg_neg, neg_div] <;> module
· intro r z
apply Prod.ext
· rfl
· dsimp [R, S, B]
simp only [inner_neg_left, mul_neg, neg_div, neg_smul]
module
· intro r z
have hflip : inner ℝ (B (h r z.1) z.2) (h r z.1) = -inner ℝ z.2 (h r z.1) :=
(hb.2.2.2.2.1 (h r z.1) z.2).2.2
dsimp [rate, R, S]
rw [inner_neg_left, hflip, neg_neg]
Exact compiled proof region; all private volume and algebra premises are discharged internally in the public theorem.
7. Derive the full real integrable-test identity
Fix r and an ell-integrable real F. Measure preservation transports integrability to F composed with S_r. The measurable involution S_r is a measurable equivalence, and its pushforward identity supplies change of variables for the real integral. Thus both integrability and the exact A6 equality follow from the proved phase map. Integrability of F specifies the test class; volume preservation and invertibility are conclusions already proved inside this theorem.
Corresponding Lean step
· intro r F hF
refine ⟨(hSmp r).integrable_comp_of_integrable hF, ?_⟩
exact (hSmp r).integral_comp
(MeasurableEquiv.ofInvolutive (S r) (hSi r) (hSmp r).measurable).measurableEmbedding F
Exact compiled proof region; all private volume and algebra premises are discharged internally in the public theorem.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · actual_phase_reversal_volume_laws
Preserve product volume under elementary shears; Identify every bounce fiber with an orthogonal reflection; Factor the linear harmonic matrix into three shears; Cover every harmonic time and restore the center; Assemble actual joint Borel maps and phase-volume laws; Check reversal and rate pairing with the actual formulas; Derive the full real integrable-test identity
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_phase_reversal_volume_laws
{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_phase_reversal_volume_statement hα hαβ hV hH hη hβη := by
let c : E → E → E := fun y r => y - η • gradient V r
let h : E → E → E := fun r x => gradient V x - gradient V r
let B : E → E → E := fun n p => p - (2 * inner ℝ p n / ‖n‖ ^ 2) • n
let S : E → (E × E) → (E × E) := fun r z => (z.1, B (h r z.1) z.2)
let R : (E × E) → (E × E) := fun z => (z.1, -z.2)
let Φ : E → E → ℝ → (E × E) → (E × E) := fun y r u z =>
(c y r + Real.cos u • (z.1 - c y r) + (Real.sqrt η * Real.sin u) • z.2,
(-Real.sin u / Real.sqrt η) • (z.1 - c y r) + Real.cos u • z.2)
let rate : E → (E × E) → ℝ := fun r z =>
Real.sqrt η * max 0 (inner ℝ z.2 (h r z.1))
let ell : Measure (E × E) := (volume : Measure E).prod (volume : Measure E)
change
Measurable (fun a : (E × E) × ℝ × (E × E) => Φ a.1.1 a.1.2 a.2.1 a.2.2) ∧
Measurable (fun a : E × (E × E) => S a.1 a.2) ∧
Measurable (fun a : E × (E × E) => rate a.1 a.2) ∧
(∀ y r : E, ∀ u : ℝ, MeasurePreserving (Φ y r u) ell ell) ∧
(∀ r : E, MeasurePreserving (S r) ell ell) ∧
MeasurePreserving R ell ell ∧
(∀ y r : E, ∀ u : ℝ, ∀ z : E × E,
Φ y r (-u) (Φ y r u z) = z ∧ Φ y r u (Φ y r (-u) z) = z) ∧
(∀ r : E, ∀ z : E × E, S r (S r z) = z) ∧
(∀ z : E × E, R (R z) = z) ∧
(∀ y r : E, ∀ u : ℝ, ∀ z : E × E, R (Φ y r u (R z)) = Φ y r (-u) z) ∧
(∀ r : E, ∀ z : E × E, R (S r z) = S r (R z)) ∧
(∀ r : E, ∀ z : E × E, rate r (R (S r z)) = rate r z) ∧
(∀ r : E, ∀ F : (E × E) → ℝ, Integrable F ell →
Integrable (fun z => F (S r z)) ell ∧
(∫ z, F (S r z) ∂ell) = ∫ z, F z ∂ell)
have hf := AutoSamplingTheory.ExampleCases.ProximalBPS.ActualHarmonicFlow.actual_harmonic_flow_laws
hα hαβ hV hH hη hβη
have hb := AutoSamplingTheory.ExampleCases.ProximalBPS.ActualBounceRate.actual_bounce_rate_energy_laws
hα hαβ hV hH hη hβη
have hSm : Measurable (fun a : E × (E × E) => S a.1 a.2) := hb.1
have hSi (r : E) : Function.Involutive (S r) := fun z => (hb.2.2.2.2.2.1 r z).2
have hSmp (r : E) : MeasurePreserving (S r) ell ell := by
exact (MeasurePreserving.id (volume : Measure E)).skew_product
(hSm.comp (measurable_const.prodMk measurable_id)).snd
(Filter.Eventually.of_forall fun x => (reflect_fiber (h r x)).map_eq)
refine ⟨hf.2.1, hSm, hb.2.2.1, ?_, hSmp, ?_, hf.2.2.2.2.1, hSi, ?_, ?_, ?_, ?_, ?_⟩
· intro y r u
exact harmonic_affine η u hη (c y r)
· exact (MeasurePreserving.id (volume : Measure E)).prod
(LinearIsometryEquiv.neg ℝ).measurePreserving
· intro z
simp [R]
· intro y r u z
apply Prod.ext <;> dsimp [R, Φ] <;>
simp only [Real.cos_neg, Real.sin_neg, neg_neg, neg_div] <;> module
· intro r z
apply Prod.ext
· rfl
· dsimp [R, S, B]
simp only [inner_neg_left, mul_neg, neg_div, neg_smul]
module
· intro r z
have hflip : inner ℝ (B (h r z.1) z.2) (h r z.1) = -inner ℝ z.2 (h r z.1) :=
(hb.2.2.2.2.1 (h r z.1) z.2).2.2
dsimp [rate, R, S]
rw [inner_neg_left, hflip, neg_neg]
· intro r F hF
refine ⟨(hSmp r).integrable_comp_of_integrable hF, ?_⟩
exact (hSmp r).integral_comp
(MeasurableEquiv.ofInvolutive (S r) (hSi r) (hSmp r).measurable).measurableEmbedding F
end
end AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPhaseReversalVolumeSource assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| A6 bounce change of variables and harmonic flow/reversal mechanics. | Explicit product-volume preservation, joint Borel maps, phase inverses and real integrable-test identity. | source-implicit | ASTIS expands implicit measurability and zero-case obligations; no additional provider assumption. |
| Finite-dimensional Euclidean phase calculations. | Finite-dimensional real Hilbert Borel E, including rank zero; exact sqrt(eta) scaling and literal reflection. | generalization | Coordinate-free equivalent mechanism; rank zero and zero normals covered. |
| Original analytic assumptions for the sampler. | All six assumptions retained; individual algebra/volume identities need fewer assumptions. | same | No assertion of necessity of every assumption; existing actual parents reused. |
| Later stationary path reversal and main sampling results. | Only elementary phase-volume/reversal identities. | unresolved | Prescribed endpoint/time reversal, stationary averaging, invariance, Markovness, errors, costs and composition remain separate obligations. |
No false unscaled harmonic isometry; no naive pointwise time reversal at right-continuous jump values; no stationary law, semigroup, hypocoercivity, unbounded cost or main/composition result.
Encoder–denoiser: accepted · equivalent-after-elaboration
Detected semantic differences
- domains: Finite Hilbert Borel representation with explicit rank-zero completion; zero-normal formula matches source R0=I. — Finite Hilbert Borel representation with explicit rank-zero completion; zero-normal formula matches source R0=I.
- conclusion: Positive-jump source equality extends by literal reflection/negation to every state, including zero rates. — Positive-jump source equality extends by literal reflection/negation to every state, including zero rates.
- scopes: Joint Borel and transported real Bochner integrability expose and discharge source change-of-variables obligations. — Joint Borel and transported real Bochner integrability expose and discharge source change-of-variables obligations.
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
- No false unscaled harmonic isometry; no naive pointwise time reversal at right-continuous jump values; no stationary law, semigroup, hypocoercivity, unbounded cost or main/composition result.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
AutoSamplingTheory.ExampleCases.ProximalBPS.ActualHarmonicFlow.actual_harmonic_flow_lawsAutoSamplingTheory.ExampleCases.ProximalBPS.ActualBounceRate.actual_bounce_rate_energy_laws
Mathlib API called (external library)
- MeasurePreserving.skew_product
- MeasurePreserving.prod
- MeasurePreserving.comp
- Measure.measurePreserving_swap
- measurePreserving_add_left
- measurePreserving_add_right
- LinearIsometryEquiv.measurePreserving
- Submodule.reflection_orthogonal_apply
- Submodule.reflection_singleton_apply
- MeasurePreserving.integrable_comp_of_integrable
- MeasurableEquiv.ofInvolutive
- MeasurePreserving.integral_comp
Mathematical sources
- Chen-Chewi-Lu-Zhang arXiv2609.06905v1 Appendix A.1 actual harmonic flow, A5 rate pairing, A6 bounce volume and direct elementary A8 reversal dependencies. — No false unscaled harmonic isometry; no naive pointwise time reversal at right-continuous jump values; no stationary law, semigroup, hypocoercivity, unbounded cost or main/composition result.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.