Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412
ASTIS mathematical exposition

Actual Gibbs position moment about a stationary point

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.GibbsPositionMoment.gibbs_position_moment · theorem · Teaching coverage

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.

\[\mu(dx)=Z^{-1}e^{-U(x)}dx,\qquad\int\langle x-p,\nabla U(x)\rangle\,d\mu=d,\qquad\int\|x-p\|^2\,d\mu\le d/\alpha.\]

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.

\[e^{-U}\in L^1(dx),\qquad\|\nabla U\|^2\in L^1(\mu).\]
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.

\[\alpha\|x-p\|^2\le\langle x-p,\nabla U(x)\rangle,\qquad\|x-p\|\le\|\nabla U(x)\|/\alpha.\]
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.

\[\|x-p\|^2\le\alpha^{-2}\|\nabla U(x)\|^2,\qquad|\langle x-p,\nabla U(x)\rangle|\le\|x-p\|^2+\|\nabla U(x)\|^2.\]
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.

\[D_vq=1,\quad D_vf=-fa,\quad fq,\ fD_vq,\ (D_vf)q\in L^1(dx).\]
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.

\[\int e^{-U}\langle x-p,v\rangle D_vU\,dx=Z,\qquad\int e^{-U}\langle x-p,\nabla U\rangle\,dx=dZ.\]
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.

\[0<Z<\infty,\qquad\int\langle x-p,\nabla U(x)\rangle\,d\mu=dZ/Z=d.\]
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.

\[\alpha\int\|x-p\|^2d\mu\le d\quad\Longrightarrow\quad\int\|x-p\|^2d\mu\le d/\alpha.\]
Corresponding Lean step

gibbs_position_moment: hi,integral_const_mul,le_div_iff₀

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 : ℝ)/(α : ℝ)

Exact module and namespace context

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.GibbsPositionMoment

Exact module and namespace context

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.

Source and reuse

ASTIS parents called

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.

ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.