Actual Gibbs gradient second moment

ASTIS expanded mathematical proof component for Fan Chen, Sinho Chewi, Jianfeng Lu and Matthew S. Zhang, Smoothed Picard Hamiltonian Monte Carlo. Explicit integrability, normalization and domain extensions are disclosed; the full initialization/history and summed-cost argument is not asserted.

Complete source statement (Samplinglib restatement)

The actual measure mu is a probability measure. Both norm(grad U)^2 and H are integrable under mu. Their expectations are equal, and the expected squared gradient is at most beta*finrank(E). These are five public conclusions; bare exponential integrability, weighted linear integrability and directional integration by parts are proved internally.

Actual ideal-law gradient moment

Read the formalized proofs

Each statement and proof below has its own closed Lean disclosure. Samplinglib parents, Mathlib calls and external mathematical sources are distinguished in each proof.

Samplinglib mathematical lesson

Actual Gibbs gradient second moment

AutoSamplingTheory.TechnicalLemmas.Analysis.GibbsGradientMoment.gibbs_gradient_moment · theorem · Teaching coverage

Read this first

Mathematical statement

\[\mu=(\mathrm{vol}).\mathrm{tilted}(-U),\qquad H(x)=\sum_i D^2U(x)[e_i,e_i],\qquad \mathbb E_\mu\|\nabla U\|^2=\mathbb E_\mu H\le\beta\dim E.\]

Lean statement · gibbs_gradient_moment

Actual normalized Gibbs probability, gradient-square and Hessian-diagonal-sum L1, expectation identity and beta*finrank bound.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)

theorem gibbs_gradient_moment [CompleteSpace E] {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) :
    let μ := (volume : Measure E).tilted (fun x => -U x)
    let H := fun x => ∑ i, fderiv ℝ (fderiv ℝ U) x
      ((stdOrthonormalBasis ℝ E) i) ((stdOrthonormalBasis ℝ E) i)
    IsProbabilityMeasure μ ∧ Integrable (fun x => ‖gradient U x‖^2) μ ∧
      Integrable H μ ∧ (∫ x, ‖gradient U x‖^2 ∂μ) = (∫ x, H x ∂μ) ∧
      (∫ x, ‖gradient U x‖^2 ∂μ) ≤ (β : ℝ)*Module.finrank ℝ E

Exact module and namespace context

Proof roadmap

1Obtain actual curvature, gradient growth and a Gaussian envelope
Instantiate QuadraticRegularization at zero regularization precision to obtain strong convexity and Lipschitz continuity of the actual gradient. Thus norm(grad U(x))≤G+beta*norm(x), with G=norm(grad U(0)). The first-order strong-convexity inequality at zero and Young inequality give U(x)≥b+a*norm(x)^2, where a=alpha/4>0 and b=U(0)-G^2/alpha. No minimizer is chosen. The existing Gibbs-integrability theorem supplies integrability of exp(-U).
2Prove weighted square and first-power integrability
The inequality t≤exp(t), with t=a*r^2/2, absorbs r^2 into a Gaussian with half the exponent. For a continuous scalar q with norm(q(x))≤A+B*norm(x) and exp(w(x))≤C*exp(-a*norm(x)^2), expand the square and use this absorption to obtain the displayed integrable majorant. Apply it to q=norm(grad U), w=-U. Then norm(grad U)≤1+norm(grad U)^2 gives the weighted first-power L1 bound. Each domination is against a genuinely integrable Gaussian, not merely a bounded function.
3Apply full-space integration by parts only after all three L1 checks
Fix a unit basis direction v and put f=exp(-U), q=DU[v]. C2 gives q in C1 and its actual directional derivative D2U[v,v]; the derivative of f is -f*q. The three products needed by the Haar-volume IBP theorem are -f*q^2, f*D2U[v,v], and f*q. Weighted gradient-square and gradient-norm integrability bound the first and third; 0≤D2U[v,v]≤beta and bare weight integrability bound the second. Only then apply the full-space IBP identity. There is no assumed vanishing boundary term, cutoff or third derivative.
4Sum the directional identities and identify the actual gradient square
The standard orthonormal basis has finitely many vectors. Each weighted directional square and Hessian diagonal term is integrable, so their sums may pass through the integral. Parseval identifies the sum of squared genuine directional derivatives with the squared norm of the actual gradient. This proves the unnormalized weighted identity and integrability of the weighted Hessian diagonal sum, including the empty basis in dimension zero.
5Normalize the actual exponential measure and transfer L1
Canonical volume is nonzero, also in dimension zero. The positive integrable exponential therefore has a positive finite normalizer, as used by isProbabilityMeasure_tilted. The tilted-integrability equivalence converts the two proved weighted L1 statements into actual Gibbs L1 statements. integral_tilted rewrites both expectations with the same normalizing denominator; their equality follows from the already proved weighted identity. No undefined-integral fallback or supplied probability assumption is used.
6Use the Hessian upper bound under the same Gibbs law
Every basis vector has unit norm, so each Hessian diagonal entry is at most beta. Their sum is at most beta times finrank(E). Integrate this inequality under the actual probability measure and use the moment identity. The result concerns the ideal Gibbs law; the actual approximate initialization law still needs its own moment-transfer proof before supplying a reference-descent cost bound.

Full assumptions and notation

All objects and hypotheses

E is a complete finite-dimensional real inner-product space with its Borel sigma-algebra and canonical Lebesgue volume. Dimension zero is included. U:E→R is twice continuously differentiable.
The nonnegative real parameters alpha,beta satisfy 0<alpha and alpha≤beta. At every x,v the genuine Hessian obeys alpha*norm(v)^2≤D2U(x)[v,v]≤beta*norm(v)^2. The alpha≤beta assumption remains in the public statement, despite its unused binder name.
Define mu=volume.tilted(-U), the actual normalized exponential Gibbs measure. For the standard orthonormal basis (e_i), define H(x)=sum_i D2U(x)[e_i,e_i]. No minimizer, normalizing constant, weighted integrability or moment bound is supplied as an assumption.

Mathematical proof

1. Obtain actual curvature, gradient growth and a Gaussian envelope

Instantiate QuadraticRegularization at zero regularization precision to obtain strong convexity and Lipschitz continuity of the actual gradient. Thus norm(grad U(x))≤G+beta*norm(x), with G=norm(grad U(0)). The first-order strong-convexity inequality at zero and Young inequality give U(x)≥b+a*norm(x)^2, where a=alpha/4>0 and b=U(0)-G^2/alpha. No minimizer is chosen. The existing Gibbs-integrability theorem supplies integrability of exp(-U).

\[\|\nabla U(x)\|\le G+\beta\|x\|,\quad U(x)\ge b+a\|x\|^2,\quad a=\alpha/4,\quad b=U(0)-G^2/\alpha.\]

Corresponding Lean step

weighted_gradient; QuadraticRegularization.strongConvexOn_and_lipschitzWith_gradient_add_quadratic; StrongConvexFirstOrder.firstOrder_lower_bound_of_strongConvexOn; StrongConvexGibbsIntegrability.integrable_exp_neg_of_strongConvexOn

2. Prove weighted square and first-power integrability

The inequality t≤exp(t), with t=a*r^2/2, absorbs r^2 into a Gaussian with half the exponent. For a continuous scalar q with norm(q(x))≤A+B*norm(x) and exp(w(x))≤C*exp(-a*norm(x)^2), expand the square and use this absorption to obtain the displayed integrable majorant. Apply it to q=norm(grad U), w=-U. Then norm(grad U)≤1+norm(grad U)^2 gives the weighted first-power L1 bound. Each domination is against a genuinely integrable Gaussian, not merely a bounded function.

\[r^2e^{-ar^2}\le\frac2a e^{-ar^2/2},\qquad e^{w(x)}q(x)^2\le C\left(2A^2+\frac{4B^2}{a}\right)e^{-a\|x\|^2/2}.\]

Corresponding Lean step

absorb_quadratic; weighted_square; weighted_gradient; Integrability.integrable_exp_neg_mul_norm_sq; MeasureTheory.Integrable.mono'

3. Apply full-space integration by parts only after all three L1 checks

Fix a unit basis direction v and put f=exp(-U), q=DU[v]. C2 gives q in C1 and its actual directional derivative D2U[v,v]; the derivative of f is -f*q. The three products needed by the Haar-volume IBP theorem are -f*q^2, f*D2U[v,v], and f*q. Weighted gradient-square and gradient-norm integrability bound the first and third; 0≤D2U[v,v]≤beta and bare weight integrability bound the second. Only then apply the full-space IBP identity. There is no assumed vanishing boundary term, cutoff or third derivative.

\[D_vf=-fq,\quad D_vq=D^2U[v,v],\qquad \int fD^2U[v,v]= -\int (D_vf)q=\int fq^2.\]

Corresponding Lean step

directional_ibp; MeasureTheory.integral_mul_fderiv_eq_neg_fderiv_mul_of_integrable

4. Sum the directional identities and identify the actual gradient square

The standard orthonormal basis has finitely many vectors. Each weighted directional square and Hessian diagonal term is integrable, so their sums may pass through the integral. Parseval identifies the sum of squared genuine directional derivatives with the squared norm of the actual gradient. This proves the unnormalized weighted identity and integrability of the weighted Hessian diagonal sum, including the empty basis in dimension zero.

\[\sum_i(DU[e_i])^2=\|\nabla U\|^2,\qquad \int e^{-U}\|\nabla U\|^2=\int e^{-U}\sum_iD^2U[e_i,e_i].\]

Corresponding Lean step

gibbs_gradient_moment: hdir, hHi, hparseval, heq; OrthonormalBasis.sum_sq_norm_inner_left; MeasureTheory.integral_finsetSum

5. Normalize the actual exponential measure and transfer L1

Canonical volume is nonzero, also in dimension zero. The positive integrable exponential therefore has a positive finite normalizer, as used by isProbabilityMeasure_tilted. The tilted-integrability equivalence converts the two proved weighted L1 statements into actual Gibbs L1 statements. integral_tilted rewrites both expectations with the same normalizing denominator; their equality follows from the already proved weighted identity. No undefined-integral fallback or supplied probability assumption is used.

\[Z=\int e^{-U}>0,\qquad \mathbb E_\mu g=\frac{\int e^{-U}g}{Z},\qquad \|\nabla U\|^2,H\in L^1(\mu).\]

Corresponding Lean step

gibbs_gradient_moment: hgμ, hHμ, htilt, heqμ; MeasureTheory.isProbabilityMeasure_tilted; MeasureTheory.integrable_tilted_iff; MeasureTheory.integral_tilted

6. Use the Hessian upper bound under the same Gibbs law

Every basis vector has unit norm, so each Hessian diagonal entry is at most beta. Their sum is at most beta times finrank(E). Integrate this inequality under the actual probability measure and use the moment identity. The result concerns the ideal Gibbs law; the actual approximate initialization law still needs its own moment-transfer proof before supplying a reference-descent cost bound.

\[H(x)\le\beta\dim E\quad\Longrightarrow\quad \mathbb E_\mu\|\nabla U\|^2=\mathbb E_\mu H\le\beta\dim E.\]

Corresponding Lean step

gibbs_gradient_moment: hdiag, hbound; MeasureTheory.integral_mono; MeasureTheory.probReal_univ

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · gibbs_gradient_moment

Derive noncompact weighted integrability from curvature, apply directional Haar IBP, sum via Parseval, normalize the actual exponential measure and integrate the Hessian bound.

Download module (.lean)

theorem gibbs_gradient_moment [CompleteSpace E] {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) :
    let μ := (volume : Measure E).tilted (fun x => -U x)
    let H := fun x => ∑ i, fderiv ℝ (fderiv ℝ U) x
      ((stdOrthonormalBasis ℝ E) i) ((stdOrthonormalBasis ℝ E) i)
    IsProbabilityMeasure μ ∧ Integrable (fun x => ‖gradient U x‖^2) μ ∧
      Integrable H μ ∧ (∫ x, ‖gradient U x‖^2 ∂μ) = (∫ x, H x ∂μ) ∧
      (∫ x, ‖gradient U x‖^2 ∂μ) ≤ (β : ℝ)*Module.finrank ℝ E := by
  classical
  let μ := (volume : Measure E).tilted (fun x => -U x)
  let b := stdOrthonormalBasis ℝ E
  let H := fun x => ∑ i, fderiv ℝ (fderiv ℝ U) x (b i) (b i)
  have hw := weighted_gradient hα hU hH
  have hunit (i) : ‖b i‖ = 1 := b.orthonormal.norm_eq_one i
  have hdiag (x : E) (i) : 0 ≤ fderiv ℝ (fderiv ℝ U) x (b i) (b i) ∧
      fderiv ℝ (fderiv ℝ U) x (b i) (b i) ≤ β := by
    have hh := hH x (b i)
    rw [hunit,one_pow,mul_one,mul_one] at hh
    exact ⟨(NNReal.coe_nonneg α).trans hh.1,hh.2⟩
  have hdir (i) := directional_ibp hU (b i) (hunit i) (fun x => hdiag x i)
    hw.1 hw.2.1 hw.2.2
  have hHi : Integrable (fun x => Real.exp (-U x)*H x) (volume : Measure E) := by
    have hi := integrable_finsetSum Finset.univ (fun i _ => (hdir i).2.1)
    simpa only [H,Finset.mul_sum] using hi
  have hparseval (x : E) : (∑ i, (fderiv ℝ U x (b i))^2) = ‖gradient U x‖^2 := by
    simpa only [inner_gradient_left,Real.norm_eq_abs,sq_abs] using
      b.sum_sq_norm_inner_left (gradient U x)
  have heq : (∫ x, Real.exp (-U x)*‖gradient U x‖^2) = ∫ x, Real.exp (-U x)*H x := by
    calc
      (∫ x, Real.exp (-U x)*‖gradient U x‖^2) =
          ∫ x, ∑ i, Real.exp (-U x)*(fderiv ℝ U x (b i))^2 := by
        simp only [← Finset.mul_sum,hparseval]
      _ = ∑ i, ∫ x, Real.exp (-U x)*(fderiv ℝ U x (b i))^2 :=
        integral_finsetSum _ (fun i _ => (hdir i).1)
      _ = ∑ i, ∫ x, Real.exp (-U x)*fderiv ℝ (fderiv ℝ U) x (b i) (b i) := by
        apply Finset.sum_congr rfl
        intro i _
        exact (hdir i).2.2
      _ = ∫ x, ∑ i, Real.exp (-U x)*fderiv ℝ (fderiv ℝ U) x (b i) (b i) :=
        (integral_finsetSum _ (fun i _ => (hdir i).2.1)).symm
      _ = ∫ x, Real.exp (-U x)*H x := by simp only [H,Finset.mul_sum]
  have : IsProbabilityMeasure μ := isProbabilityMeasure_tilted hw.1
  have hgμ : Integrable (fun x => ‖gradient U x‖^2) μ := by
    apply (integrable_tilted_iff hw.1 _).2
    simpa only [smul_eq_mul] using hw.2.1
  have hHμ : Integrable H μ := by
    apply (integrable_tilted_iff hw.1 _).2
    simpa only [smul_eq_mul] using hHi
  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 heqμ : (∫ x, ‖gradient U x‖^2 ∂μ) = ∫ x, H x ∂μ := by
    rw [htilt,htilt,heq]
  refine ⟨inferInstance,hgμ,hHμ,heqμ,?_⟩
  change (∫ x, ‖gradient U x‖^2 ∂μ) ≤ (β : ℝ)*Module.finrank ℝ E
  rw [heqμ]
  have hbound (x : E) : H x ≤ (β : ℝ)*Module.finrank ℝ E := by
    calc
      H x ≤ ∑ _i : Fin (Module.finrank ℝ E), (β : ℝ) :=
        Finset.sum_le_sum (fun i _ => (hdiag x i).2)
      _ = (β : ℝ)*Module.finrank ℝ E := by simp [mul_comm]
  simpa only [integral_const,probReal_univ,one_smul] using
    integral_mono hHμ (integrable_const ((β : ℝ)*Module.finrank ℝ E)) hbound

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
The paper uses Euclidean space of positive dimension.	Complete finite-dimensional real inner-product Borel space, including dimension zero.	generalization	Coordinate-free and zero-dimensional extensions are explicit; the actual proof handles the empty basis and canonical nonzero volume.
Section6.3 uses a normalized smoothness bound for its recursive potential.	Actual Hessian upper bound beta with 0<alpha<=beta.	generalization	The explicit beta*finrank bound specializes to beta=1. The alpha<=beta hypothesis is retained, not silently removed.
The ideal Gibbs gradient moment is used in the initial-gradient estimate.	Actual tilted probability, both Gibbs L1 statements, and a moment identity preceding the bound.	source-implicit	Weighted noncompact integrability and normalization are proved before IBP and expectation; they are not added as hypotheses.
The Hessian trace interpretation underlies the standard gradient-moment calculation.	Actual standard-orthonormal-basis Hessian diagonal sum H.	source-implicit	No independent abstract trace/Laplacian or basis-invariance API theorem is claimed.
The Gibbs moment is one input to the larger reference-initialization estimate.	Ideal Gibbs moment component only.	same	Approximate/smoothed output moments, Gaussian perturbations, conditional histories and summed gradient cost remain separate.

This is the ideal Gibbs gradient-moment component used in SPHMC Section6.3. The coordinate-free finite-dimensional formulation includes dimension zero. The general beta bound specializes to the source normalized beta=1 setting. The alpha<=beta hypothesis is retained. H is the genuine Hessian diagonal sum in the standard orthonormal basis; no separate abstract trace/Laplacian API or basis-independence theorem is asserted. All weighted L1 and normalization prerequisites are proved from actual curvature. The Gaussian domination constants may depend on alpha,beta,U(0),grad U(0), but the final expectation bound is beta*finrank(E). Approximate or smoothed output moments, random-history conditioning, Gaussian perturbation, and summed reference-query cost remain separate obligations. This does not complete either paper.

Encoder–denoiser: accepted · equivalent-after-elaboration

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

This is the ideal Gibbs gradient-moment component used in SPHMC Section6.3. The coordinate-free finite-dimensional formulation includes dimension zero. The general beta bound specializes to the source normalized beta=1 setting. The alpha≤beta hypothesis is retained. H is the genuine Hessian diagonal sum in the standard orthonormal basis; no separate abstract trace/Laplacian API or basis-independence theorem is asserted. All weighted L1 and normalization prerequisites are proved from actual curvature. The Gaussian domination constants may depend on alpha,beta,U(0),grad U(0), but the final expectation bound is beta*finrank(E). Approximate or smoothed output moments, random-history conditioning, Gaussian perturbation, and summed reference-query cost remain separate obligations. This does not complete either paper.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

MeasureTheory.integral_mul_fderiv_eq_neg_fderiv_mul_of_integrable
OrthonormalBasis.sum_sq_norm_inner_left
MeasureTheory.integrable_finsetSum
MeasureTheory.integral_finsetSum
MeasureTheory.isProbabilityMeasure_tilted
MeasureTheory.integrable_tilted_iff
MeasureTheory.integral_tilted
MeasureTheory.integral_mono

Mathematical sources

SPHMC Section6.3 ideal Gibbs gradient moment — Ideal-law moment input to reference-point initialization; actual history and total cost remain separate.

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

Actual Gibbs gradient second moment

Complete source statement (Samplinglib restatement)

Actual ideal-law gradient moment

Read the formalized proofs

Actual Gibbs gradient second moment

Mathematical statement

Proof roadmap

All objects and hypotheses

Mathematical proof

1. Obtain actual curvature, gradient growth and a Gaussian envelope

2. Prove weighted square and first-power integrability

3. Apply full-space integration by parts only after all three L1 checks

4. Sum the directional identities and identify the actual gradient square

5. Normalize the actual exponential measure and transfer L1

6. Use the Hessian upper bound under the same Gibbs law

Lean verification

Source assumptions versus formal assumptions

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Mathematical sources

Which proof obligations and prerequisites are covered?