GibbsGradientMoment: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

Actual Gibbs gradient second moment
Actual Gibbs covariance lower

Samplinglib mathematical lesson

Actual Gibbs gradient second moment

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

Read this first

Mathematical statement

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.

\[\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

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.

Samplinglib mathematical lesson

Actual Gibbs covariance lower

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

Read this first

Mathematical statement

The actual Gibbs mu=volume.tilted(-U) is probability and id belongs to L2(mu). For every direction v, covarianceBilin(mu)(v,v)≥norm(v)^2/beta. This is the linear-observable covariance corollary of Cramer-Rao, not the full nonlinear-observable theorem or a matrix-inverse result.

\[\mu(dx)=Z_U^{-1}e^{-U(x)}dx,\quad X\in L^2(\mu),\quad \forall v,\ \operatorname{Cov}_{\mu}(\langle v,X\rangle,\langle v,X\rangle)\ge\beta^{-1}\|v\|^2.\]

Lean statement · gibbs_covariance_lower

The actual Gibbs mu=volume.tilted(-U) is probability and id belongs to L2(mu). For every direction v, covarianceBilin(mu)(v,v)>=norm(v)^2/beta. This is the linear-observable covariance corollary of Cramer-Rao, not the full nonlinear-observable theorem or a matrix-inverse result.

Download module (.lean)

theorem gibbs_covariance_lower [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)
    IsProbabilityMeasure μ ∧ MemLp id 2 μ ∧
      ∀ v : E, ‖v‖^2/(β:ℝ) ≤ ProbabilityTheory.covarianceBilin μ v v

Exact module and namespace context

Proof roadmap

1Derive actual Gibbs probability and score second moment
The existing canonical Gibbs gradient theorem derives the positive integrable exponential weight and actual score-square integrability from C2 Hessian bounds, using genuine weighted domination and full-space score integration by parts. Reuse that producer, without supplying a probability or moment certificate.
2Derive position L2 without a minimizer
Strong gradient monotonicity between zero and x gives alpha norm(x)≤norm(gradient U(x))+norm(gradient U(0)). Square this and dominate by the integrable score square plus a constant under the actual probability law. Thus id is genuinely L2 and its Bochner mean exists. Zero norm is handled separately.
3Prove centered linear-score pairing with all IBP products integrable
For a unit direction v put p=E_mu X, q(x)=inner(x-p,v), a(x)=DU(x)[v]. Actual position and score L2 imply q, a, qa are integrable as required. The full-space integration-by-parts API is applied only after deriving the weighted q, weight times derivative q, and derivative weight times q integrability. Since Dq[v]=1 and D(exp(-U))[v]=-exp(-U)a, normalize by the true positive Z_U to obtain E_mu qa=1. No mean-score-zero hypothesis is needed.
4Bound the actual directional score second moment
The existing genuine score IBP identifies the weighted score square with the actual Hessian directional integral. The upper Hessian beta bound and probability normalization give E_mu a^2≤beta. All score-square, Hessian and product integrability are proved before integral algebra.
5Integrate an actual nonnegative square
Expand the integrable nonnegative square (a-beta q)^2. Combining E qa=1 with E a^2≤beta yields beta^2 E q^2≥beta. Positivity of beta follows from 0<alpha≤beta, so divide to get variance≥1/beta. Actual covarianceBilin is identified with the centered q square using proved id L2.
6Scale every direction and include dimension zero
Handle v=0 directly. For v nonzero use u=v/norm(v), apply the unit-direction result and use the true covariance bilinear map scaling. This quantifies all v without assuming a unit vector exists, so dimension zero is included. This does not establish general nonlinear Cramer-Rao or any Brascamp-Lieb upper covariance.

Full assumptions and notation

All objects and hypotheses

E is a complete finite-dimensional real inner-product space with its Borel measurable space and canonical volume, including dimension zero. alpha,beta are NNReal, 0<alpha≤beta. U or V is genuinely C2; actual Hessian at every point and direction lies between alpha*norm(v)^2 and beta*norm(v)^2.
Every Gibbs law is the actual volume.tilted(-potential). Probability, finite second moments, score integrability, centered score pairing and covariance bounds are derived. No minimizer, finite input moments, partition constant, derivative/score/covariance or well-behaved certificate is supplied.

Mathematical proof

1. Derive actual Gibbs probability and score second moment

The existing canonical Gibbs gradient theorem derives the positive integrable exponential weight and actual score-square integrability from C2 Hessian bounds, using genuine weighted domination and full-space score integration by parts. Reuse that producer, without supplying a probability or moment certificate.

\[0<Z_U<\infty,\quad \mu\text{ probability},\quad\mathbb E_\mu\|\nabla U\|^2\le\beta d.\]

Corresponding Lean step

gibbs_gradient_moment; weighted_gradient; directional_ibp

2. Derive position L2 without a minimizer

Strong gradient monotonicity between zero and x gives alpha norm(x)≤norm(gradient U(x))+norm(gradient U(0)). Square this and dominate by the integrable score square plus a constant under the actual probability law. Thus id is genuinely L2 and its Bochner mean exists. Zero norm is handled separately.

\[\|x\|^2\le\frac{2}{\alpha^2}(\|\nabla U(x)\|^2+\|\nabla U(0)\|^2),\quad X\in L^2(\mu).\]

Corresponding Lean step

gibbs_position_l2; StrongConvexFirstOrder.gradient_inner_lower_bound_of_strongConvexOn; memLp_two_iff_integrable_sq_norm

3. Prove centered linear-score pairing with all IBP products integrable

For a unit direction v put p=E_mu X, q(x)=inner(x-p,v), a(x)=DU(x)[v]. Actual position and score L2 imply q, a, qa are integrable as required. The full-space integration-by-parts API is applied only after deriving the weighted q, weight times derivative q, and derivative weight times q integrability. Since Dq[v]=1 and D(exp(-U))[v]=-exp(-U)a, normalize by the true positive Z_U to obtain E_mu qa=1. No mean-score-zero hypothesis is needed.

\[\mathbb E_\mu[q a]=1,\quad q=\langle X-\mathbb EX,v\rangle,\quad a=DU(X)[v],\quad\|v\|=1.\]

Corresponding Lean step

coordinate_position_ibp; integral_mul_fderiv_eq_neg_fderiv_mul_of_integrable; integrable_tilted_iff; integral_tilted

4. Bound the actual directional score second moment

The existing genuine score IBP identifies the weighted score square with the actual Hessian directional integral. The upper Hessian beta bound and probability normalization give E_mu a^2≤beta. All score-square, Hessian and product integrability are proved before integral algebra.

\[\mathbb E_\mu a^2=\mathbb E_\mu D^2U(X)[v,v]\le\beta.\]

Corresponding Lean step

directional_ibp; integral_mono; integral_tilted; gibbs_covariance_unit

5. Integrate an actual nonnegative square

Expand the integrable nonnegative square (a-beta q)^2. Combining E qa=1 with E a^2≤beta yields beta^2 E q^2≥beta. Positivity of beta follows from 0<alpha≤beta, so divide to get variance≥1/beta. Actual covarianceBilin is identified with the centered q square using proved id L2.

\[0\le\mathbb E(a-\beta q)^2=\mathbb Ea^2-2\beta+\beta^2\mathbb Eq^2\le-\beta+\beta^2\mathbb Eq^2\ \Longrightarrow\ \operatorname{Cov}_\mu(v,v)\ge\beta^{-1}.\]

Corresponding Lean step

gibbs_covariance_unit; integral_add; integral_sub; covarianceBilin_apply

6. Scale every direction and include dimension zero

Handle v=0 directly. For v nonzero use u=v/norm(v), apply the unit-direction result and use the true covariance bilinear map scaling. This quantifies all v without assuming a unit vector exists, so dimension zero is included. This does not establish general nonlinear Cramer-Rao or any Brascamp-Lieb upper covariance.

\[\operatorname{Cov}_\mu(v,v)=\|v\|^2\operatorname{Cov}_\mu(v/\|v\|,v/\|v\|)\ge\|v\|^2/\beta.\]

Corresponding Lean step

gibbs_covariance_lower; map_smul; smul_apply

Lean verification

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

Lean proof · gibbs_covariance_lower

Actual Gibbs integrability and score L2, position L2 via gradient monotonicity, centered-linear and score IBP, nonnegative scalar square, bilinear scaling; actual quadratic posterior and exact source potential Hessian adapter.

Download module (.lean)

theorem gibbs_covariance_lower [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)
    IsProbabilityMeasure μ ∧ MemLp id 2 μ ∧
      ∀ v : E, ‖v‖^2/(β:ℝ) ≤ ProbabilityTheory.covarianceBilin μ v v := by
  let μ := (volume : Measure E).tilted (fun x => -U x)
  have hp := gibbs_position_l2 hα hαβ hU hH
  refine ⟨hp.1,hp.2,?_⟩
  intro v
  by_cases hvzero : v=0
  · subst v
    simp
  · have hn : ‖v‖≠0 := norm_ne_zero_iff.mpr hvzero
    let u := ‖v‖⁻¹ • v
    have hu : ‖u‖=1 := by
      dsimp only [u]
      rw [norm_smul,Real.norm_eq_abs,abs_inv,abs_of_nonneg (norm_nonneg v),inv_mul_cancel₀ hn]
    have hv : ‖v‖ • u = v := by
      dsimp only [u]
      rw [smul_smul,mul_inv_cancel₀ hn,one_smul]
    have hc := gibbs_covariance_unit hα hαβ hU hH u hu
    have hscale : ProbabilityTheory.covarianceBilin μ v v =
        ‖v‖^2*ProbabilityTheory.covarianceBilin μ u u := by
      calc
        ProbabilityTheory.covarianceBilin μ v v =
            ProbabilityTheory.covarianceBilin μ (‖v‖ • u) (‖v‖ • u) := by rw [hv]
        _ = _ := by
          simp only [map_smul,smul_apply,smul_eq_mul]
          ring
    rw [hscale,div_eq_mul_inv]
    exact mul_le_mul_of_nonneg_left hc (sq_nonneg _)


end AutoSamplingTheory.TechnicalLemmas.Analysis.GibbsGradientMoment

Exact module and namespace context

Scope and omitted-condition boundaries

Actual Gibbs all-direction covariance lower bound and its actual RGO/source V_eta Hessian upper consumer only. No Brascamp-Lieb covariance upper/Hessian lower, full Lemma4.1, general nonlinear Cramer-Rao, higher regularity, exact stationarity, approximate/stochastic/history work, PBPS process or either complete main/composition. TV never transfers unbounded expected cost.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

integral_mul_fderiv_eq_neg_fderiv_mul_of_integrable
integrable_tilted_iff
integral_tilted
memLp_two_iff_integrable_sq_norm
memLp_two_iff_integrable_sq
covarianceBilin_apply
integral_add
integral_sub
integral_const_mul
map_smul
smul_apply

Mathematical sources

SPHMC Lemma4.1 Cramer-Rao half — Actual Gibbs all-direction covariance lower bound and its actual RGO/source V_eta Hessian upper consumer only. No Brascamp-Lieb covariance upper/Hessian lower, full Lemma4.1, general nonlinear Cramer-Rao, higher regularity, exact stationarity, approximate/stochastic/history work, PBPS process or either complete main/composition. TV never transfers unbounded expected cost.
Auxiliary pinned author book Theorem3.5.8 / Corollary3.5.9 — Linear-observable corollary only; genuine hidden regularity proved; not a Lean dependency.

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