Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0

Actual Gibbs linear covariance upper

Fan Chen, Sinho Chewi, Jianfeng Lu, Matthew S. Zhang; canonical isotropic BOTH-curvature node.

arXiv:2609.06906v1 · SPHMC arXiv:2609.06906v1 Sections1-3 standing beta=1/alpha=kappa^-1/RGO/smoothing and Section4.1 S4.E1, Lemma4.1 S4.Thmtheorem1, S4.Ex4-6; actual unreflected posterior covariance and source unnormalized V_eta. Primary-first Smoothed_Hessian_lower_source_preread.md. · faithful paraphrase

Complete source statement (Samplinglib restatement)

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.

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

Actual Gibbs linear covariance upper

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

Read the formalized proofs

Each statement and proof below has its own closed Lean disclosure. Samplinglib parents, Mathlib calls and external mathematical sources are distinguished in each proof.

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

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

  2. 2Take the genuine linear observable

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

  3. 3Identify its actual gradient

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

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

  5. 5Preserve exact normalization

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

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

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 := 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

Source assumptions versus formal assumptions

SourceActual LeanDifference kindWhy it matters
Isotropic covariance estimate invoked through Brascamp-Lieb; source standing curvature beta1/alpha=kappa^-1.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.generalizationCanonical B explicitly includes actual vectorL2 and BOTH curvature, not full anisotropic BL. Source A has no added proof premise and produces genuine moments/normalizers internally.
Printed covariance upper invocation and reverse-Cramer-Rao lower yield both Hessian bounds.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.source-implicitPoincare-derived isotropic covariance route is a sufficient authored OR-route; it does not certify full BL or external book theorem.
Higher regularity, algorithms and both main/cost composition.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.unresolvedOnly actual analytic Lemma4.1 and its canonical covariance prerequisite are covered.

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.

Encoder–denoiser: accepted · equivalent-after-elaboration

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

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

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.

Which proof obligations and prerequisites are covered?

  • Independently verified prerequisite Actual Lemma4.1 analytic bounds
  • TODO — not closed by these contributions Full anisotropic BL remaining
  • TODO — not closed by these contributions Both main results and actual-input expectedcost composition remaining