Samplinglib mathematical lesson

Actual normalized Gibbs C1 variance Poincare

AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GibbsC1Poincare.gibbs_c1_variance_poincare · theorem · Teaching coverage

Read this first

Mathematical statement

For every genuine C1 scalar/gradient weightedL2 observable, derive real Admissible integrability and m*Var_mu(f)≤DirichletEnergy_mu(f) on the actual normalized Gibbs law, using actual centered graph membership and AE quotient identities.

\[m\,\operatorname{Var}_\mu(f)\le\int\|\nabla f\|^2\,d\mu,\qquad f,\nabla f\in L^2(\mu),\ f\in C^1.\]

Lean statement · gibbs_c1_variance_poincare

For every genuine C1 scalar/gradient weightedL2 observable, derive real Admissible integrability and m*Var_mu(f)<=DirichletEnergy_mu(f) on the actual normalized Gibbs law, using actual centered graph membership and AE quotient identities.

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_c1_variance_poincare
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace 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) :
    let μ := (volume : Measure E).tilted (fun x => -W x)
    ∀ f : E → ℝ, ContDiff ℝ 1 f → MemLp f 2 μ → MemLp (gradient f) 2 μ →
      AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.Admissible μ f ∧
      m*AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.variance μ f ≤
        AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.dirichletEnergy μ f

Exact module and namespace context

Proof roadmap

1Construct the original graph before observables
Actual integrable Gibbs exponential normalizes to a probability. Accepted compact-gradient closability constructs genuine original D before ALL C1 scalar f. Both curvature bounds remain explicit.
2Center with the actual normalized mean
Put c=integral f and g=f-c. True probability/L2 gives fL1; g is C1/L2 and its true gradient equals gradientf.
3Derive real integrability and meanzero
L2 facts give centered-square and gradient-square integrability. Actual probability mass1 and integral_sub give integralg=0. Admissible records these facts only, never an assumed estimate.
4Enter the SAME original closed graph
The accepted C1 graph producer admits actual g/gradientg L2 quotient pair. mem_graph_iff gives z in SAME D.closure.domain with genuine representative equalities, and actual meanzero follows by AE substitution.
5Apply actual centered-domain Poincare
Use the first new canonical theorem on this exact z and actual law. It proves the estimate from curvature instead of consuming Poincare.Satisfies.
6Convert quotient norms to true integrals
L2.inner_def and actual toLp AE identities identify both squared norms with actual scalar/vector integrals. Real abs-square equals square and gradientg=gradientf yield the claimed variance/Dirichlet formula.

Full assumptions and notation

All objects and hypotheses

Same actual C2 normalized Gibbs law, positive integrable partition and BOTH global positive m/M curvature bounds; finite-dimensional real Hilbert/Borel E including0.
ALL actual C1 scalar functions f with true scalar and gradient MemLp2. No supplied centering, Poincare, Admissible, variance or extra spatial moments. Original compact-smooth D is constructed before all f.

Mathematical proof

1. Construct the original graph before observables

Actual integrable Gibbs exponential normalizes to a probability. Accepted compact-gradient closability constructs genuine original D before ALL C1 scalar f. Both curvature bounds remain explicit.

\[\mu(E)=1,\qquad D\phi=\nabla\phi\quad(\phi\in C_c^\infty).\]

Corresponding Lean step

WeightedGradient.compact_gradient_closable; isProbabilityMeasure_tilted

2. Center with the actual normalized mean

Put c=integral f and g=f-c. True probability/L2 gives fL1; g is C1/L2 and its true gradient equals gradientf.

\[c=\int f\,d\mu,\quad g=f-c,\quad\nabla g=\nabla f.\]

Corresponding Lean step

MemLp.integrable; fderiv_sub_const

3. Derive real integrability and meanzero

L2 facts give centered-square and gradient-square integrability. Actual probability mass1 and integral_sub give integralg=0. Admissible records these facts only, never an assumed estimate.

\[\int g\,d\mu=0,\quad g^2,\|\nabla g\|^2\in L^1(\mu).\]

Corresponding Lean step

MemLp.integrable_sq; memLp_two_iff_integrable_sq_norm; integral_sub

4. Enter the SAME original closed graph

The accepted C1 graph producer admits actual g/gradientg L2 quotient pair. mem_graph_iff gives z in SAME D.closure.domain with genuine representative equalities, and actual meanzero follows by AE substitution.

\[(g,\nabla g)\in\operatorname{graph}\overline D.\]

Corresponding Lean step

WeightedC1GradientDomain.c1_in_closed_gradient; LinearPMap.mem_graph_iff

5. Apply actual centered-domain Poincare

Use the first new canonical theorem on this exact z and actual law. It proves the estimate from curvature instead of consuming Poincare.Satisfies.

\[m\|g\|_{L^2}^2\le\|\nabla g\|_{L^2}^2.\]

Corresponding Lean step

CenteredDomainPoincare.gibbs_centered_domain_poincare

6. Convert quotient norms to true integrals

L2.inner_def and actual toLp AE identities identify both squared norms with actual scalar/vector integrals. Real abs-square equals square and gradientg=gradientf yield the claimed variance/Dirichlet formula.

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

Corresponding Lean step

norm_sq_toLp_integral; L2.inner_def; integral_congr_ae; gibbs_c1_variance_poincare

Lean verification

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

Lean proof · gibbs_c1_variance_poincare

Construct the original graph before observables; Center with the actual normalized mean; Derive real integrability and meanzero; Enter the SAME original closed graph; Apply actual centered-domain Poincare; Convert quotient norms to true integrals

Download module (.lean)

theorem gibbs_c1_variance_poincare
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace 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) :
    let μ := (volume : Measure E).tilted (fun x => -W x)
    ∀ f : E → ℝ, ContDiff ℝ 1 f → MemLp f 2 μ → MemLp (gradient f) 2 μ →
      AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.Admissible μ f ∧
      m*AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.variance μ f ≤
        AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.dirichletEnergy μ f := by
  let μ := (volume : Measure E).tilted (fun x => -W x)
  let : IsProbabilityMeasure μ := isProbabilityMeasure_tilted hI
  obtain ⟨D,_,hD,_,hgraph⟩ :=
    AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedGradient.compact_gradient_closable
      W (hW.of_le (by norm_num)) hI
  dsimp only
  intro f hf hp hq
  let c : ℝ := ∫ x, f x ∂μ
  let g : E → ℝ := fun x => f x-c
  have hg : ContDiff ℝ 1 g := hf.sub contDiff_const
  have hgp : MemLp g 2 μ := hp.sub (memLp_const c)
  have hgrad : gradient g=gradient f := by
    funext x
    simp only [g,gradient,fderiv_sub_const]
  have hgq : MemLp (gradient g) 2 μ := hgrad ▸ hq
  have hfi : Integrable f μ := hp.integrable (by norm_num)
  refine ⟨⟨hfi,hgp.integrable_sq,
    (memLp_two_iff_integrable_sq_norm hq.aestronglyMeasurable).mp hq⟩,?_⟩
  have hgm : (∫ x, g x ∂μ)=0 := by
    rw [integral_sub hfi (integrable_const c),integral_const]
    simp [c]
  have hmem :=
    AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedC1GradientDomain.c1_in_closed_gradient
      μ D hD hgraph hg hgp hgq
  obtain ⟨z,hz,hDz⟩ := (LinearPMap.mem_graph_iff D.closure).mp hmem
  have hzmean : (∫ x, (z:Lp ℝ 2 μ) x ∂μ)=0 := by
    rw [hz]
    exact (integral_congr_ae hgp.coeFn_toLp).trans hgm
  have hb := AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.CenteredDomainPoincare.gibbs_centered_domain_poincare W hW hI hZ m M hm hmM hlower hupper
    D hD hgraph z hzmean
  rw [hz,hDz,norm_sq_toLp_integral μ g hgp,norm_sq_toLp_integral μ (gradient g) hgq] at hb
  simpa only [g,hgrad,Real.norm_eq_abs,sq_abs,
    AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.variance,
    AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.dirichletEnergy] using hb

end AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GibbsC1Poincare

Exact module and namespace context

Scope and omitted-condition boundaries

Finite-dimensional real Hilbert/Borel full E including0, genuine C2 W with actual exponential integrability/positive partition, normalized tilted probability, BOTH global mI≤HessW≤MI and0<m≤M. SAME original exact compact-smooth closable weighted gradient D BEFORE all truly mean-zero domain z. Actual positiveepsilon variational solutions from residual/globalcoercivity producers are identified by SAME D/epsilon/forcing uniqueness, then tested against z; strong scaled residual limit and genuine scalar Cauchy-Schwarz/zero-norm branch give m*normz^2≤normDclosurez^2. No uniform unscaled solution bound, centered resolvent, epsilon0 solution, core/range/adjoint certificate or input Poincare. Actual C1 scalar/gradientL2 pairs and centered function are admitted to a genuine original graph, actual probability/AE quotient identities and real integrability produce Admissible and m*Var≤DirichletEnergy. Actual common Gaussian J/R/S, sourceC2 alpha-beta eta cap, reflected W_y, positive partitions and one original D_y precede allcentered z/score directions; actual unnormalized parameter-y score variance ≤(eta^-1-alpha)^2*norma^2/(4*(alpha+eta^-1)), with exact reflected m=(alpha+eta^-1)/4 and source-derived upper M=(beta+eta^-1)/4. Auxiliary normalized density equality only; no R2=R/alternateD identification/jointselector or normalized conditional density derivative. BOTH-curvature generic statement is narrower than lower-only source D6 and is disclosed; source companion models supply the upper bound. Anisotropic BL, unreflected linear moments/covariance-upper and SPHMC Hessian lower, outer-y/marginal Poincare, PBPS sampler/reflection/invariance/nonexplosion/hypocoercivity/implementation/cost, SPHMC complete algorithm/Wp/proxywarmness, main results/composition/expectedcost remainopen. TV does not transfer unbounded cost.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

MemLp.integrable
MemLp.integrable_sq
memLp_two_iff_integrable_sq_norm
LinearPMap.mem_graph_iff
L2.inner_def
fderiv_sub_const

Mathematical sources

PBPS reflected score variance and explicitly bounded canonical background — Finite-dimensional real Hilbert/Borel full E including0, genuine C2 W with actual exponential integrability/positive partition, normalized tilted probability, BOTH global mI<=HessW<=MI and0<m<=M. SAME original exact compact-smooth closable weighted gradient D BEFORE all truly mean-zero domain z. Actual positiveepsilon variational solutions from residual/globalcoercivity producers are identified by SAME D/epsilon/forcing uniqueness, then tested against z; strong scaled residual limit and genuine scalar Cauchy-Schwarz/zero-norm branch give m*normz^2<=normDclosurez^2. No uniform unscaled solution bound, centered resolvent, epsilon0 solution, core/range/adjoint certificate or input Poincare. Actual C1 scalar/gradientL2 pairs and centered function are admitted to a genuine original graph, actual probability/AE quotient identities and real integrability produce Admissible and m*Var<=DirichletEnergy. Actual common Gaussian J/R/S, sourceC2 alpha-beta eta cap, reflected W_y, positive partitions and one original D_y precede allcentered z/score directions; actual unnormalized parameter-y score variance <=(eta^-1-alpha)^2*norma^2/(4*(alpha+eta^-1)), with exact reflected m=(alpha+eta^-1)/4 and source-derived upper M=(beta+eta^-1)/4. Auxiliary normalized density equality only; no R2=R/alternateD identification/jointselector or normalized conditional density derivative. BOTH-curvature generic statement is narrower than lower-only source D6 and is disclosed; source companion models supply the upper bound. Anisotropic BL, unreflected linear moments/covariance-upper and SPHMC Hessian lower, outer-y/marginal Poincare, PBPS sampler/reflection/invariance/nonexplosion/hypocoercivity/implementation/cost, SPHMC complete algorithm/Wp/proxywarmness, main results/composition/expectedcost remainopen. TV does not transfer unbounded 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.