Can the SPHMC smoothing argument survive weak convexity?

1. Set \(W_{y}(x)=V(x)+\|x-y\|^{2}/(2η)\). Its Hessian in x lies between cI and bI, where \(c=m+η^{-1}>0\) and \(b=M+η^{-1}\ge c\). Positive posterior curvature is available even when V itself is concave. In particular both \(1+mη\) and \(1+Mη\) are positive.

2. The lower Taylor bound \(V(x)\ge V(0)+⟨\nabla V(0),x⟩+(m/2)\|x\|^{2}\) implies \[W_y(x)\ge\frac c2\|x\|^2+\langle\nabla V(0)-y/\eta,x\rangle+V(0)+\frac{\|y\|^2}{2\eta}.\] On every ball \(\|y\|\le R\), Young's inequality absorbs the linear term and gives \(W_{y}(x)\ge (c/4)\|x\|^{2}-A_{R}\) for a finite constant \(A_{R}\). Thus the posterior normalizer is finite and strictly positive for every y, with all polynomial position moments finite.

3. The integrand is positive and continuous. Its first y derivatives are \((x_{i}-y_{i})/η\) times itself; its second derivatives have factors \((x_{i}-y_{i})(x_{j}-y_{j})/η^{2}-δ_{ij}/η\). On \(\|y\|\le R\) their absolute values are bounded by \(B_{R}(1+\|x\|^{2})exp(-c\|x\|^{2}/4)\), an integrable function independent of y. Dominated parameter differentiation, including continuity of these derivatives, gives \(qη\in C^{2}\) and \(qη>0\); hence \(Uη\in C^{2}\). This establishes an unnormalized analytic interface without first declaring \(exp(-V)\) integrable.

4. Normalize \(exp(-W_{y})\) to obtain the actual posterior \(Π_{y}\); its position is in \(L^{2}\) by the same Gaussian bound. Differentiating \(qη\) and then its logarithm gives \[\begin{gathered}\nabla U_\eta(y)=\eta^{-1}(y-\mathbb E_{\Pi_y}X),\\\nabla^2U_\eta(y)=\eta^{-1}I-\eta^{-2}\operatorname{Cov}_{\Pi_y}(X).\end{gathered}\] The moments and dominated differentiation justify these identities; they are not merely identities assigned to totalized derivatives.

5. Apply the Gibbs covariance upper producer to \(W_{y}\), retaining its normalization, vector \(L^{2}\) and both curvature hypotheses. Apply the covariance lower producer to the same potential, representing c,b as positive nonnegative-real parameters where its Lean interface requires them. They give \[b^{-1}I\preceq\operatorname{Cov}_{\Pi_y}(X)\preceq c^{-1}I.\] The upper covariance bound is the Poincaré ingredient; the reverse bound is a separate Cramér–Rao ingredient. Neither direction supplies the other.

6. Subtracting a covariance from \(η^{-1}I\) reverses its order. Substitution and exact algebra therefore yield \[\frac{m}{1+m\eta}I\preceq\nabla^2U_\eta(y)\preceq\frac{M}{1+M\eta}I.\] For example the lower endpoint is \(η^{-1}-η^{-2}/c=m/(1+mη)\). These signed bounds remain meaningful when m or M is negative; denominators are positive by the first step.

7. A one-sided Hessian upper bound is not an operator-norm bound in the presence of negative eigenvalues. Since the Hessian is self-adjoint, the two-sided bounds imply \[\|\nabla^2U_\eta(y)\|_{\rm op}\le L_\eta:=\max\!\left\{\left|\frac m{1+m\eta}\right|,\left|\frac M{1+M\eta}\right|\right\}.\] Integrating the genuine derivative of \(\nabla Uη\) along a line segment proves global \(Lη\)-Lipschitz continuity. If \(m\ge 0\) this reduces to \(M/(1+Mη)\), but not in general.

8. For the exact failure example take \(V(x)=-a\|x\|^{2}/2\), \(a>0\) and \(0<η<1/a\), so \(m=M=-a\) and \(c>0\). Completing the square gives \[q_\eta(y)=(1-a\eta)^{-d/2}\exp\!\left(\frac{a\|y\|^2}{2(1-a\eta)}\right).\] Hence \[\begin{gathered}U_\eta(y)=\frac d2\log(1-a\eta)-\frac{a\|y\|^2}{2(1-a\eta)},\\\nabla^2U_\eta=-\frac a{1-a\eta}I.\end{gathered}\] Its gradient has Lipschitz constant \(a/(1-aη)>0\), whereas the proposed \(M/(1+Mη)\) is negative. The two-sided Hessian bound is attained exactly.

9. For nonnegative densities Tonelli and the unit-mass Gaussian kernel give, as extended nonnegative integrals, \[\int q_\eta(y)\,dy=\int e^{-V(x)}\,dx.\] Pointwise finiteness of \(qη\) therefore does not imply a probability law. In the example both total masses are infinite. To define the normalized smoothed sampling law one separately needs \(0<Z=\int e^{-}ⱽ<\infty \) and then uses \(qη/Z\); its potential \(Uη+log\) Z has the same derivatives. These extended-integral conclusions must not be read as Lean real Bochner integrals returning infinity: those real integrals are totalized outside integrability.

10. The local GaussianConvolutionRegularity.gaussian_convolution_derivatives assumes a probability input \(μ\); it cannot be called on an unnormalizable prior to replace the new domination proof above. SmoothedHessianUpper.smoothed_hessian_upper assumes positive lower curvature of V, and the paper-specialized SmoothedHessianBounds also assumes its \(κ\) and \(η\) regime; neither is an unchanged weak-convexity interface. Their posterior covariance ingredients can be reused after the new analytic/normalization adapters, whose complete Lean realization is absent here. No SPHMC dynamics, warm-start, error, query-cost or main-theorem claim follows from this QA.

import AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GibbsC1Poincare
import Mathlib.Probability.Moments.CovarianceBilin

/-! Actual isotropic covariance upper from the original closed-gradient Poincare
producer. The observable is the genuine linear functional, its gradient is the
constant direction, and normalized Dirichlet energy is exactly its squared norm.
Actual vectorL2 is explicit in this canonical interface because Mathlib's
covarianceBilin is totalized outside that domain. The source SPHMC consumer must
produce this moment internally. BOTH curvature bounds are explicit; no full
anisotropic Brascamp-Lieb or sampler/main claim. -/

namespace AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GibbsLinearCovarianceUpper
open MeasureTheory ProbabilityTheory InnerProductSpace
open scoped RealInnerProductSpace
noncomputable section
set_option autoImplicit false
set_option backward.isDefEq.respectTransparency false

theorem gibbs_linear_covariance_upper
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace E]
    (W : E → ℝ) (hW : ContDiff ℝ 2 W)
    (hI : Integrable (fun x => Real.exp (-W x)))
    (hZ : 0 < ∫ x, Real.exp (-W x))
    (m M : ℝ) (hm : 0 < m) (hmM : m ≤ M)
    (hlower : ∀ x a, m*‖a‖^2 ≤ fderiv ℝ (fderiv ℝ W) x a a)
    (hupper : ∀ x a, fderiv ℝ (fderiv ℝ W) x a a ≤ M*‖a‖^2)
    (hX : MemLp id 2 ((volume : Measure E).tilted (fun x => -W x))) :
    let μ := (volume : Measure E).tilted (fun x => -W x)
    ∀ a : E, ProbabilityTheory.covarianceBilin μ a a ≤ ‖a‖^2/m := by
  let μ := (volume : Measure E).tilted (fun x => -W x)
  let : IsProbabilityMeasure μ := isProbabilityMeasure_tilted hI
  dsimp only
  intro a
  let f : E → ℝ := fun x => inner ℝ a x
  have hf : ContDiff ℝ 1 f := (innerSL ℝ a).contDiff
  have hp : MemLp f 2 μ := hX.const_inner a
  have hgrad : gradient f = fun _ => a := by
    funext x
    apply (toDual ℝ E).injective
    rw [toDual_gradient]
    exact (innerSL ℝ a).fderiv
  have hq : MemLp (gradient f) 2 μ := hgrad ▸ memLp_const a
  obtain ⟨_, hb⟩ := GibbsC1Poincare.gibbs_c1_variance_poincare
    W hW hI hZ m M hm hmM hlower hupper f hf hp hq
  have henergy : Poincare.dirichletEnergy μ f = ‖a‖^2 := by
    simp only [Poincare.dirichletEnergy, hgrad]
    simp
  rw [henergy] at hb
  have hcov : covarianceBilin μ a a = Poincare.variance μ f := by
    rw [covarianceBilin_self hX a, variance_eq_integral hp.aemeasurable]
    rfl
  rw [hcov]
  exact (le_div_iff₀ hm).2 (by simpa only [mul_comm] using hb)

end
end AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GibbsLinearCovarianceUpper

1. Constructs the posterior Gaussian lower bound locally uniformly in y, checks polynomial-Gaussian domination for first/second y derivatives and \(L^{2}\) moments, and derives the genuine log-Hessian covariance identity without assuming prior normalization. (1 point)
2. Verifies both positive posterior curvature interfaces, uses both covariance directions with the correct order reversal, and derives the exact signed endpoints \(m/(1+mη)\), \(M/(1+Mη)\) with positive denominators. (1 point)
3. Derives the nonnegative operator-norm/Lipschitz constant max of absolute endpoints and computes the concave-quadratic example that falsifies the proposed negative constant and probability claim. (1 point)
4. Uses Tonelli to distinguish finite pointwise convolution from finite total mass, states the separate Z normalization condition, and identifies the actual probability/positive-prior-curvature Lean API gaps without claiming a transferred sampling algorithm theorem. (1 point)

import AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GibbsC1Poincare
import Mathlib.Probability.Moments.CovarianceBilin

/-! Actual isotropic covariance upper from the original closed-gradient Poincare
producer. The observable is the genuine linear functional, its gradient is the
constant direction, and normalized Dirichlet energy is exactly its squared norm.
Actual vectorL2 is explicit in this canonical interface because Mathlib's
covarianceBilin is totalized outside that domain. The source SPHMC consumer must
produce this moment internally. BOTH curvature bounds are explicit; no full
anisotropic Brascamp-Lieb or sampler/main claim. -/

namespace AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GibbsLinearCovarianceUpper
open MeasureTheory ProbabilityTheory InnerProductSpace
open scoped RealInnerProductSpace
noncomputable section
set_option autoImplicit false
set_option backward.isDefEq.respectTransparency false

theorem gibbs_linear_covariance_upper
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace E]
    (W : E → ℝ) (hW : ContDiff ℝ 2 W)
    (hI : Integrable (fun x => Real.exp (-W x)))
    (hZ : 0 < ∫ x, Real.exp (-W x))
    (m M : ℝ) (hm : 0 < m) (hmM : m ≤ M)
    (hlower : ∀ x a, m*‖a‖^2 ≤ fderiv ℝ (fderiv ℝ W) x a a)
    (hupper : ∀ x a, fderiv ℝ (fderiv ℝ W) x a a ≤ M*‖a‖^2)
    (hX : MemLp id 2 ((volume : Measure E).tilted (fun x => -W x))) :
    let μ := (volume : Measure E).tilted (fun x => -W x)
    ∀ a : E, ProbabilityTheory.covarianceBilin μ a a ≤ ‖a‖^2/m := by
  let μ := (volume : Measure E).tilted (fun x => -W x)
  let : IsProbabilityMeasure μ := isProbabilityMeasure_tilted hI
  dsimp only
  intro a
  let f : E → ℝ := fun x => inner ℝ a x
  have hf : ContDiff ℝ 1 f := (innerSL ℝ a).contDiff
  have hp : MemLp f 2 μ := hX.const_inner a
  have hgrad : gradient f = fun _ => a := by
    funext x
    apply (toDual ℝ E).injective
    rw [toDual_gradient]
    exact (innerSL ℝ a).fderiv
  have hq : MemLp (gradient f) 2 μ := hgrad ▸ memLp_const a
  obtain ⟨_, hb⟩ := GibbsC1Poincare.gibbs_c1_variance_poincare
    W hW hI hZ m M hm hmM hlower hupper f hf hp hq
  have henergy : Poincare.dirichletEnergy μ f = ‖a‖^2 := by
    simp only [Poincare.dirichletEnergy, hgrad]
    simp
  rw [henergy] at hb
  have hcov : covarianceBilin μ a a = Poincare.variance μ f := by
    rw [covarianceBilin_self hX a, variance_eq_integral hp.aemeasurable]
    rfl
  rw [hcov]
  exact (le_div_iff₀ hm).2 (by simpa only [mul_comm] using hb)

end
end AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GibbsLinearCovarianceUpper

Download exact supporting module · Uses the project toolchain and its listed imports; not a standalone replacement QA proof.