Actual Gibbs covariance lower

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.

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

Proof roadmap

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

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

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

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

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

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