AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GibbsC1Poincare

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.

GibbsC1Poincare: mathematical reading route

Actual normalized Gibbs C1 variance Poincare

Mathematical statement

Proof roadmap

All objects and hypotheses

Mathematical proof

1. Construct the original graph before observables

2. Center with the actual normalized mean

3. Derive real integrability and meanzero

4. Enter the SAME original closed graph

5. Apply actual centered-domain Poincare

6. Convert quotient norms to true integrals

Lean verification

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Mathematical sources