Actual Gibbs position moment about a stationary point
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.GibbsPositionMoment.gibbs_position_moment · theorem · Teaching coverage
Mathematical statement
The actual mu is a probability measure. The function exp(-U) is integrable against volume and its integral Z is strictly positive. Both norm(x-p)^2 and inner(x-p,gradient U(x)) are integrable against mu. Their actual integrals satisfy integral inner(x-p,gradient U(x)) dmu=d and integral norm(x-p)^2 dmu≤d/alpha.
Lean statement · gibbs_position_moment
Actual Gibbs normalization,L1,position-gradient=d and position-square<=d/alpha with genuine Hessian and stationary-point assumptions.
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 gibbs_position_moment {U : E → ℝ} {α β : ℝ≥0}
(hα : 0 < α) (hαβ : α ≤ β) (hU : ContDiff ℝ 2 U)
(hH : ∀ x v : E, (α : ℝ)*‖v‖^2 ≤ fderiv ℝ (fderiv ℝ U) x v v ∧
fderiv ℝ (fderiv ℝ U) x v v ≤ (β : ℝ)*‖v‖^2)
(p : E) (hp : gradient U p = 0) :
let μ := (volume : Measure E).tilted (fun x => -U x)
IsProbabilityMeasure μ ∧
Integrable (fun x => Real.exp (-U x)) (volume : Measure E) ∧
0 < (∫ x, Real.exp (-U x)) ∧
Integrable (fun x => ‖x-p‖^2) μ ∧
Integrable (fun x => inner ℝ (x-p) (gradient U x)) μ ∧
(∫ x, inner ℝ (x-p) (gradient U x) ∂μ) = Module.finrank ℝ E ∧
(∫ x, ‖x-p‖^2 ∂μ) ≤ (Module.finrank ℝ E : ℝ)/(α : ℝ)Proof roadmap
- 1Obtain actual Gibbs normalization and gradient integrability
Use QuadraticRegularization at zero added precision to derive strong convexity from the genuine Hessian. StrongConvexGibbsIntegrability gives exponential-weight L1. The previously compiled GibbsGradientMoment theorem supplies probability and gradient-square L1 under this same normalized tilt. Its numerical gradient bound is not the final position bound.
- 2Derive pointwise coercivity from the actual stationary point
Strong convexity gives strong monotonicity of the genuine gradient. Substitute gradient U(p)=0 and use Cauchy-Schwarz. Treat x=p separately before cancelling the positive displacement norm; divide only by alpha>0.
- 3Prove position and pairing integrability
Dominate position square by gradient square divided by alpha squared. Probability and the bound t≤1+t^2 give position-norm L1. Cauchy-Schwarz and Young give L1 for the position-gradient pairing. These estimates establish integrability only; they do not replace the source sharp constant with beta/alpha squared.
- 4Justify every full-space coordinate IBP input
For a unit vector v,set f=exp(-U),q(x)=inner(x-p,v),a(x)=D_vU(x). Position and gradient L1/L2 bounds dominate q and qa under the actual tilt. The tilted-integrability equivalence transfers them to volume using the already proved exponential L1. Differentiate the actual functions: D_vq=1 and D_vf=-fa. Thus fq,f D_vq,and (D_vf)q are all integrable before invoking full-space IBP.
- 5Evaluate each coordinate and sum the finite basis
The justified IBP identity gives integral f*q*a=integral f=Z for every unit basis vector. Sum the finite orthonormal basis and use its inner-product expansion. Every coordinate term is integrable,so finite sums commute with the integral. In dimension zero the sum is empty and yields zero.
- 6Normalize the actual exponential tilt
The exponential integral is strictly positive by integral_exp_pos and finite by the established integrability. Apply the actual integral_tilted formula and factor out this same normalizer. Cancelling Z in dZ/Z proves the position-gradient identity under mu.
- 7Integrate coercivity to obtain the sharp position moment
Both position square and the pairing are integrable. Integrate the pointwise strong-convexity inequality,substitute the exact pairing moment d,and divide by positive alpha. The upper curvature beta was used for the integrability route but does not enter this final constant.
Full assumptions and notation
All objects and hypotheses
- E is a finite-dimensional real inner-product Borel space,with its complete metric structure; d=dim_R E may be zero. Volume is its canonical Lebesgue measure.
- alpha and beta are nonnegative real numbers,0<alpha and alpha≤beta. U:E→R is twice continuously Frechet differentiable. For every x,v,alpha*norm(v)^2≤D2U(x)[v,v]≤beta*norm(v)^2. The derivatives and gradient are genuine derivatives of U.
- p is any supplied point of E satisfying gradient U(p)=0. Existence of a stationary point is not concluded by this theorem. Set Z=integral exp(-U(x)) dx and mu=volume.tilted(-U); the tilt is the actual normalized exponential measure,not an arbitrary probability law.
- All displayed real integrals are Bochner integrals. Integrability is proved explicitly; no moment bound or vanishing boundary term is supplied.
Mathematical proof
1. Obtain actual Gibbs normalization and gradient integrability
Use QuadraticRegularization at zero added precision to derive strong convexity from the genuine Hessian. StrongConvexGibbsIntegrability gives exponential-weight L1. The previously compiled GibbsGradientMoment theorem supplies probability and gradient-square L1 under this same normalized tilt. Its numerical gradient bound is not the final position bound.
Corresponding Lean step
stationary_position_integrability: hdata,hg,hprob,hgrad,hweight
2. Derive pointwise coercivity from the actual stationary point
Strong convexity gives strong monotonicity of the genuine gradient. Substitute gradient U(p)=0 and use Cauchy-Schwarz. Treat x=p separately before cancelling the positive displacement norm; divide only by alpha>0.
Corresponding Lean step
stationary_position_integrability: hcoercive,hbound,hz,hn
3. Prove position and pairing integrability
Dominate position square by gradient square divided by alpha squared. Probability and the bound t≤1+t^2 give position-norm L1. Cauchy-Schwarz and Young give L1 for the position-gradient pairing. These estimates establish integrability only; they do not replace the source sharp constant with beta/alpha squared.
Corresponding Lean step
stationary_position_integrability: hpos,hlin,hpair
4. Justify every full-space coordinate IBP input
For a unit vector v,set f=exp(-U),q(x)=inner(x-p,v),a(x)=D_vU(x). Position and gradient L1/L2 bounds dominate q and qa under the actual tilt. The tilted-integrability equivalence transfers them to volume using the already proved exponential L1. Differentiate the actual functions: D_vq=1 and D_vf=-fa. Thus fq,f D_vq,and (D_vf)q are all integrable before invoking full-space IBP.
Corresponding Lean step
coordinate_position_ibp: hqder,hfder,hqbound,habound,hqμ,hqaμ,hfq,hfqa,hf'q,hfq'
5. Evaluate each coordinate and sum the finite basis
The justified IBP identity gives integral f*q*a=integral f=Z for every unit basis vector. Sum the finite orthonormal basis and use its inner-product expansion. Every coordinate term is integrable,so finite sums commute with the integral. In dimension zero the sum is empty and yields zero.
Corresponding Lean step
coordinate_position_ibp: hid; gibbs_position_moment: b,hdir,hparseval,heq
6. Normalize the actual exponential tilt
The exponential integral is strictly positive by integral_exp_pos and finite by the established integrability. Apply the actual integral_tilted formula and factor out this same normalizer. Cancelling Z in dZ/Z proves the position-gradient identity under mu.
Corresponding Lean step
gibbs_position_moment: hZ,htilt,hid
7. Integrate coercivity to obtain the sharp position moment
Both position square and the pairing are integrable. Integrate the pointwise strong-convexity inequality,substitute the exact pairing moment d,and divide by positive alpha. The upper curvature beta was used for the integrability route but does not enter this final constant.
Corresponding Lean step
gibbs_position_moment: hi,integral_const_mul,le_div_iff₀
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · gibbs_position_moment
Actual gradient L1 implies position L1;full-space coordinate IBP and finite basis sum;positive normalizer and actual tilt;integrate coercivity.
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 gibbs_position_moment {U : E → ℝ} {α β : ℝ≥0}
(hα : 0 < α) (hαβ : α ≤ β) (hU : ContDiff ℝ 2 U)
(hH : ∀ x v : E, (α : ℝ)*‖v‖^2 ≤ fderiv ℝ (fderiv ℝ U) x v v ∧
fderiv ℝ (fderiv ℝ U) x v v ≤ (β : ℝ)*‖v‖^2)
(p : E) (hp : gradient U p = 0) :
let μ := (volume : Measure E).tilted (fun x => -U x)
IsProbabilityMeasure μ ∧
Integrable (fun x => Real.exp (-U x)) (volume : Measure E) ∧
0 < (∫ x, Real.exp (-U x)) ∧
Integrable (fun x => ‖x-p‖^2) μ ∧
Integrable (fun x => inner ℝ (x-p) (gradient U x)) μ ∧
(∫ x, inner ℝ (x-p) (gradient U x) ∂μ) = Module.finrank ℝ E ∧
(∫ x, ‖x-p‖^2 ∂μ) ≤ (Module.finrank ℝ E : ℝ)/(α : ℝ) := by
classical
let μ := (volume : Measure E).tilted (fun x => -U x)
let b := stdOrthonormalBasis ℝ E
rcases stationary_position_integrability hα hαβ hU hH p hp with
⟨hprob,hw,hpos,hlin,hpair,hcoerce⟩
have hgrad := (GibbsGradientMoment.gibbs_gradient_moment hα hαβ hU hH).2.1
have hdir (i) := coordinate_position_ibp hU p (b i) (b.orthonormal.norm_eq_one i)
hw hpos hlin hgrad
have hparseval (x : E) :
(∑ i, inner ℝ (x-p) (b i)*fderiv ℝ U x (b i)) = inner ℝ (x-p) (gradient U x) := by
simpa [inner_gradient_right] using b.sum_inner_mul_inner (x-p) (gradient U x)
have heq : (∫ x, Real.exp (-U x)*inner ℝ (x-p) (gradient U x)) =
(Module.finrank ℝ E : ℝ)*(∫ x, Real.exp (-U x)) := by
calc
(∫ x, Real.exp (-U x)*inner ℝ (x-p) (gradient U x)) =
∫ x, ∑ i, Real.exp (-U x)*inner ℝ (x-p) (b i)*fderiv ℝ U x (b i) := by
apply integral_congr_ae
filter_upwards with x
rw [← hparseval x,Finset.mul_sum]
simp only [mul_assoc]
_ = ∑ i, ∫ x, Real.exp (-U x)*inner ℝ (x-p) (b i)*fderiv ℝ U x (b i) :=
integral_finsetSum _ (fun i _ => (hdir i).1)
_ = ∑ _i : Fin (Module.finrank ℝ E), ∫ x, Real.exp (-U x) := by
apply Finset.sum_congr rfl
intro i _
exact (hdir i).2
_ = (Module.finrank ℝ E : ℝ)*(∫ x, Real.exp (-U x)) := by simp
have hZ : 0 < (∫ x, Real.exp (-U x)) := integral_exp_pos hw
have htilt (g : E → ℝ) : (∫ x, g x ∂μ) =
(∫ x, Real.exp (-U x)*g x)/(∫ x, Real.exp (-U x)) := by
rw [integral_tilted]
simp only [smul_eq_mul]
rw [← integral_div]
apply integral_congr_ae
filter_upwards with x
ring
have hid : (∫ x, inner ℝ (x-p) (gradient U x) ∂μ) = Module.finrank ℝ E := by
rw [htilt,heq]
exact mul_div_cancel_right₀ _ hZ.ne'
refine ⟨hprob,hw,hZ,hpos,hpair,hid,?_⟩
have hi := integral_mono (hpos.const_mul (α : ℝ)) hpair hcoerce
rw [integral_const_mul] at hi
change (∫ x, inner ℝ (x-p) (gradient U x) ∂μ) = Module.finrank ℝ E at hid
rw [hid] at hi
apply (le_div_iff₀ (show (0 : ℝ) < α from hα)).2
nlinarith [hi]
end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.GibbsPositionMomentSource assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| Source uses Euclidean positive dimension. | Finite-dimensional real inner-product Borel space including dimension zero. | generalization | The empty-basis case is proved;no infinite-dimensional statement. |
| Source standardized potential has lower curvature1 and upper curvature1+eta. | Genuine C2 Hessian bounds0<alpha<=beta with arbitrary finite beta. | generalization | Source consumer satisfies this contract;the proof is not advertised as a weakest-hypothesis theorem. |
| The source potential is centered at its stationary point zero. | An arbitrary actual stationary point p is explicitly supplied. | generalization | Stationarity is not assumed of an unrelated reference point and existence is not claimed;the source zero-point cancellation remains a separate adapter. |
| Source (4.6) uses the standardized actual RGO law. | The measure here is actual volume.tilted(-U). | API-limitation | The affine RGO identification is still required;it needs the proximal equation and measure transport. |
| Source needs the bound E norm(u)^2<=d. | The theorem proves the exact pairing moment d and position bound d/alpha. | generalization | At alpha=1 the numerical source constant1 is preserved;beta does not enter the final bound. |
| Full-space integrals and IBP underlie the source moment step. | Exponential L1,positive normalizer,position/pairing L1 and coordinate IBP are proved. | source-implicit | No integrability,boundary disappearance or moment identity is a supplied closure assumption. |
| Lemma4.2 also needs Gaussian transport-Fisher and actual score bias. | Only the actual Gibbs position-moment component is proved. | API-limitation | No full bias theorem,Picard accuracy,initialization or expected query cost is claimed. |
Actual normalized volume.tilted(-U),genuine C2 lower/upper Hessian bounds and an explicitly supplied actual stationary point p. The proof establishes normalization,L1,exact position-gradient moment and sharp dimension/curvature bound. General p,positive alpha,finite beta,coordinate-free and zero-dimensional spaces are disclosed extensions. It is not a weakest-hypothesis strong-log-concavity theorem. The source consumer has standardized potential norm(u)^2/2+rho_y(u),p=0,alpha=1,beta=1+eta;stationarity follows from cancellation of the defining linear term. Identification with the affine image of the actual RGO needs the proximal equation and a separate measure-transport proof. No Gaussian transport-Fisher,smoothed-score identity,estimator bias,Picard accuracy,initialization or query-cost theorem is asserted.
Encoder–denoiser: accepted · domain-mismatch
Detected semantic differences
- domains: Coordinate-free and zero-dimensional extension. — Independent formal source reviewer accepted: Coordinate-free and zero-dimensional extension.
- assumptions: General lower and upper curvature contract. — Independent formal source reviewer accepted: General lower and upper curvature contract.
- quantifiers: General actual stationary point is supplied. — Independent formal source reviewer accepted: General actual stationary point is supplied.
- objects: Actual tilt versus remaining affine RGO identification. — Independent formal source reviewer accepted: Actual tilt versus remaining affine RGO identification.
- conclusion: Exact pairing identity and sharp d/alpha extension. — Independent formal source reviewer accepted: Exact pairing identity and sharp d/alpha extension.
- assumptions: Explicit L1,normalization and IBP justification. — Independent formal source reviewer accepted: Explicit L1,normalization and IBP justification.
- scopes: Position-moment component,not full bias theorem. — Independent formal source reviewer accepted: Position-moment component,not full bias theorem.
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 volume.tilted(-U),genuine C2 lower/upper Hessian bounds and an explicitly supplied actual stationary point p. The proof establishes normalization,L1,exact position-gradient moment and sharp dimension/curvature bound. General p,positive alpha,finite beta,coordinate-free and zero-dimensional spaces are disclosed extensions. It is not a weakest-hypothesis strong-log-concavity theorem. The source consumer has standardized potential norm(u)^2/2+rho_y(u),p=0,alpha=1,beta=1+eta;stationarity follows from cancellation of the defining linear term. Identification with the affine image of the actual RGO needs the proximal equation and a separate measure-transport proof. No Gaussian transport-Fisher,smoothed-score identity,estimator bias,Picard accuracy,initialization or query-cost theorem is asserted.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
AutoSamplingTheory.TechnicalLemmas.Analysis.GibbsGradientMoment.gibbs_gradient_momentAutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticRegularization.strongConvexOn_and_lipschitzWith_gradient_add_quadraticAutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexFirstOrder.gradient_inner_lower_bound_of_strongConvexOnAutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexGibbsIntegrability.integrable_exp_neg_of_strongConvexOn
Mathlib API called (external library)
- MeasureTheory.integrable_tilted_iff
- MeasureTheory.integral_mul_fderiv_eq_neg_fderiv_mul_of_integrable
- OrthonormalBasis.sum_inner_mul_inner
- MeasureTheory.integral_finsetSum
- MeasureTheory.integral_exp_pos
- MeasureTheory.integral_tilted
- MeasureTheory.integral_mono
Mathematical sources
- SPHMC Lemma4.2,(4.6) position moment — Actual normalized volume.tilted(-U),genuine C2 lower/upper Hessian bounds and an explicitly supplied actual stationary point p. The proof establishes normalization,L1,exact position-gradient moment and sharp dimension/curvature bound. General p,positive alpha,finite beta,coordinate-free and zero-dimensional spaces are disclosed extensions. It is not a weakest-hypothesis strong-log-concavity theorem. The source consumer has standardized potential norm(u)^2/2+rho_y(u),p=0,alpha=1,beta=1+eta;stationarity follows from cancellation of the defining linear term. Identification with the affine image of the actual RGO needs the proximal equation and a separate measure-transport proof. No Gaussian transport-Fisher,smoothed-score identity,estimator bias,Picard accuracy,initialization or query-cost theorem is asserted.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.