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

GibbsLinearCovarianceUpper: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

  1. Actual Gibbs linear covariance upper
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

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.