From Gibbs Poincaré to a directional covariance bound

1. The density assumptions make \(μ\) the normalized Gibbs probability measure. This is used in the energy calculation; the notation tilted alone is not permission to treat an arbitrary totalized density expression as a probability measure.

2. For a fixed a, set \(f_{a}(x)=⟨a,x⟩\). The continuous linear functional is genuinely \(C^{1}\) with derivative \(v\mapsto ⟨a,v⟩\) and gradient a at every x. These derivative facts are proved from the continuous-linear-map API, not from a fallback value of totalized fderiv.

3. The supplied vector \(L^{2}\) hypothesis implies \(f_{a}\in L^{2}(μ)\), by continuity of inner product with a. The gradient is the constant vector a; a constant is in \(L^{2}\) of a probability measure. Thus both integrability interfaces of Gibbs \(C^{1}\) Poincaré have been checked.

4. Normalization and the constant gradient give the exact energy \[\mathcal E_\mu(f_a)=\int\|\nabla f_a(x)\|^2\,d\mu(x)=\|a\|^2.\] There is no hidden dimension factor.

5. With these \(L^{2}\) hypotheses, the actual covariance bilinear form satisfies \[\operatorname{Cov}_\mu(a,a)=\operatorname{Var}_\mu(f_a).\] The proof uses \(covarianceBilin_{self}\) followed by the integral formula for variance. The vector \(L^{2}\) hypothesis is important for interpreting this totalized covariance API as the intended second moment.

6. Apply the imported Poincaré estimate and substitute the energy identity: \[m\operatorname{Cov}_\mu(a,a)\le\|a\|^2.\] Since \(m>0\), division preserves the inequality and gives the required bound. This also covers \(a=0\) and the zero-dimensional space.

7. Both curvature bounds and the position \(L^{2}\) premise remain part of this exact Lean interface, although the final constant depends only on m. This proof neither establishes their sharp mathematical necessity nor produces the vector moment from scratch. The SPHMC posterior consumer separately supplies that moment before applying this lemma.

/- SamplingOptimisationGeometryBench public-dev reference.
   Reuses the existing project proof; retain LICENSE and NOTICE. -/
import AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GibbsC1Poincare
import Mathlib.Probability.Moments.CovarianceBilin

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

example
    {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)

1. Uses normalized probability and genuine smoothness to identify the linear observable's constant gradient a. (1 point)
2. Checks scalar \(L^{2}\) from the supplied vector \(L^{2}\) hypothesis and gradient \(L^{2}\) from finite probability mass. (1 point)
3. Computes energy exactly \(\|a\|^{2}\) and justifies covarianceBilin(a,a)=variance of the linear observable on the \(L^{2}\) domain. (1 point)
4. Applies the stated Poincaré estimate and positive-m division with constant 1/m, retaining the actual API premises and not asserting full anisotropic Brascamp–Lieb. (1 point)

/- SamplingOptimisationGeometryBench public-dev reference.
   Reuses the existing project proof; retain LICENSE and NOTICE. -/
import AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GibbsC1Poincare
import Mathlib.Probability.Moments.CovarianceBilin

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

example
    {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
  -- Replace this comment with your proof.

Download task template

The exact existing theorem is extracted with its own imports; its module and conclusion are not imported as a shortcut. The proof installs IsProbabilityMeasure \(μ\), introduces f as the continuous linear functional innerSL, derives MemLp f by hX.const_inner, and proves gradient f is constant through \(toDual_{gradient}\) and the genuine fderiv of innerSL. \(memLp_{const}\) supplies the gradient domain. GibbsC1Poincare gives the scalar variance estimate; henergy uses probability normalization. \(covarianceBilin_{self}\) and variance_eq_integral connect the actual covariance to that variance, then le_div_iff₀ hm performs the final positive division. These are imported ASTIS/Mathlib ingredients, not new Bench-owned lemmas.

/- SamplingOptimisationGeometryBench public-dev reference.
   Reuses the existing project proof; retain LICENSE and NOTICE. -/
import AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GibbsC1Poincare
import Mathlib.Probability.Moments.CovarianceBilin

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

example
    {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)

Download runnable reference