Samplinglib mathematical lesson

Actual Gibbs linear covariance upper

AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GibbsLinearCovarianceUpper.gibbs_linear_covariance_upper · theorem · Teaching coverage

Read this first

Mathematical statement

For each direction a, the genuine covariance bilinear form of the normalized BOTH-curvature Gibbs law satisfies Cov_mu(a,a)≤norma^2/m, using the actual linear observable, constant gradient and proven C1 Poincare.

\[\mu=Z^{-1}e^{-W}dx,\quad mI\preceq D^2W\preceq MI,\quad X\in L^2(\mu)\Longrightarrow \operatorname{Cov}_\mu(a,a)\le \|a\|^2/m.\]

Lean statement · gibbs_linear_covariance_upper

For each direction a, the genuine covariance bilinear form of the normalized BOTH-curvature Gibbs law satisfies Cov_mu(a,a)<=norma^2/m, using the actual linear observable, constant gradient and proven C1 Poincare.

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_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

Exact module and namespace context

Proof roadmap

1Normalize the actual Gibbs measure
True exponential integrability gives probability. The canonical moment premise is real vectorL2, rather than a certificate of a covariance estimate.
2Take the genuine linear observable
The continuous linear functional f(x)=inner(a,x) is C1. Actual vectorL2 yields scalarL2 by MemLp.const_inner.
3Identify its actual gradient
The real Riesz isometry and true continuous-linear derivative show gradientf is constanta. It therefore has genuine weighted vectorL2.
4Use the proved curvature Poincare producer
The accepted original-gradient/C1 theorem derives actual integrability and m*variance≤energy, using BOTH curvature bounds. Poincare.Satisfies is not assumed.
5Preserve exact normalization
The genuine constant gradient and probability mass1 make the Dirichlet integral exactly norma^2, with no missing energy prefactor.
6Bridge actual covariance and variance
covarianceBilin_self requires the real vectorL2 premise; variance_eq_integral matches the genuine centered-square definition. Divide by positivem.

Full assumptions and notation

All objects and hypotheses

Finite real Hilbert/Borel full E including0, actual C2 W, true exp(-W) volume integrability and positive partition, BOTH global mI≤HessW≤MI with0<m≤M.
Genuine vector id in L2 of normalized tilted Gibbs law. This canonical node keeps the moment premise explicit to rule out totalized covariance outside its integrable domain; the actual paper consumer produces it internally. No covariance/Poincare certificate input.

Mathematical proof

1. Normalize the actual Gibbs measure

True exponential integrability gives probability. The canonical moment premise is real vectorL2, rather than a certificate of a covariance estimate.

\[\mu=Z^{-1}e^{-W}dx,\quad \mu(E)=1,\quad X\in L^2(\mu).\]

Corresponding Lean step

isProbabilityMeasure_tilted

2. Take the genuine linear observable

The continuous linear functional f(x)=inner(a,x) is C1. Actual vectorL2 yields scalarL2 by MemLp.const_inner.

\[f_a(x)=\langle a,x\rangle,\quad f_a\in C^1\cap L^2(\mu).\]

Corresponding Lean step

ContinuousLinearMap.contDiff; MemLp.const_inner

3. Identify its actual gradient

The real Riesz isometry and true continuous-linear derivative show gradientf is constanta. It therefore has genuine weighted vectorL2.

\[\nabla f_a(x)=a,\quad\nabla f_a\in L^2(\mu).\]

Corresponding Lean step

toDual_gradient; ContinuousLinearMap.fderiv; memLp_const

4. Use the proved curvature Poincare producer

The accepted original-gradient/C1 theorem derives actual integrability and m*variance≤energy, using BOTH curvature bounds. Poincare.Satisfies is not assumed.

\[m\operatorname{Var}_\mu(f_a)\le\int\|\nabla f_a\|^2d\mu.\]

Corresponding Lean step

GibbsC1Poincare.gibbs_c1_variance_poincare

5. Preserve exact normalization

The genuine constant gradient and probability mass1 make the Dirichlet integral exactly norma^2, with no missing energy prefactor.

\[\int\|\nabla f_a\|^2d\mu=\|a\|^2.\]

Corresponding Lean step

integral_const; probReal_univ; Poincare.dirichletEnergy

6. Bridge actual covariance and variance

covarianceBilin_self requires the real vectorL2 premise; variance_eq_integral matches the genuine centered-square definition. Divide by positivem.

\[\operatorname{Cov}_\mu(a,a)=\operatorname{Var}_\mu(f_a)\le\|a\|^2/m.\]

Corresponding Lean step

covarianceBilin_self; variance_eq_integral; le_div_iff₀

Lean verification

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

Lean proof · gibbs_linear_covariance_upper

Normalize the actual Gibbs measure; Take the genuine linear observable; Identify its actual gradient; Use the proved curvature Poincare producer; Preserve exact normalization; Bridge actual covariance and variance

Download module (.lean)

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

Exact module and namespace context

Scope and omitted-condition boundaries

Canonical BOTH-curvature Gibbs linear covariance upper with genuine vectorL2, actual positive partition and probability normalization; not full anisotropic Brascamp-Lieb. Actual source beta=1 alpha=kappa^-1, 1≤kappa, 0<eta≤1; genuine posterior law R_y, internally produced probability/vectorL2/positive partitions/C2 and normalized-U versus unnormalized-V_eta constant shift. Derive true covariance upper and both Hessian bounds (kappa+eta)^-1 and (1+eta)^-1, then true 1-Lipschitz gradient. Finite real Hilbert/Borel including zero dimension is disclosed representation extension. No input covariance/PI/oracle/moment/normalizer certificate on source Anchor. No joint measurable posterior kernel selector, higher smoothing derivatives, algorithm/Wp/proxy-warmness/main/querycost/composition. PBPS reflected quarter law and source-score remain separate. TV never transfers unbounded expected cost.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GibbsC1Poincare.gibbs_c1_variance_poincare

Mathlib API called (external library)

covarianceBilin_self
variance_eq_integral
MemLp.const_inner
toDual_gradient
ContinuousLinearMap.fderiv
integral_const
le_div_iff₀

Mathematical sources

SPHMC actual Lemma4.1 and explicit covariance prerequisite — Canonical BOTH-curvature Gibbs linear covariance upper with genuine vectorL2, actual positive partition and probability normalization; not full anisotropic Brascamp-Lieb. Actual source beta=1 alpha=kappa^-1, 1<=kappa, 0<eta<=1; genuine posterior law R_y, internally produced probability/vectorL2/positive partitions/C2 and normalized-U versus unnormalized-V_eta constant shift. Derive true covariance upper and both Hessian bounds (kappa+eta)^-1 and (1+eta)^-1, then true 1-Lipschitz gradient. Finite real Hilbert/Borel including zero dimension is disclosed representation extension. No input covariance/PI/oracle/moment/normalizer certificate on source Anchor. No joint measurable posterior kernel selector, higher smoothing derivatives, algorithm/Wp/proxy-warmness/main/querycost/composition. PBPS reflected quarter law and source-score remain separate. TV never transfers unbounded expected cost.

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