Actual centered original-gradient Poincare

For every genuinely centered z in the SAME original closed weighted-gradient domain, prove m*normz^2<=normDclosurez^2 from actual positive-epsilon solutions, SAME variational uniqueness, global coercivity and true strong scaled residual limit.

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 centered original-gradient Poincare

AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.CenteredDomainPoincare.gibbs_centered_domain_poincare · theorem · Teaching coverage

Read this first

Mathematical statement

For every genuinely centered z in the SAME original closed weighted-gradient domain, prove m*normz^2≤normDclosurez^2 from actual positive-epsilon solutions, SAME variational uniqueness, global coercivity and true strong scaled residual limit.

\[\mu=Z^{-1}e^{-W}dx,\quad mI\preceq\nabla^2W\preceq MI,\quad\int z\,d\mu=0\Longrightarrow m\|z\|_{L^2(\mu)}^2\le\|\overline Dz\|_{L^2(\mu)}^2.\]

Lean statement · gibbs_centered_domain_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_centered_domain_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)
    ∀ (D : Lp ℝ 2 μ →ₗ.[ℝ] Lp E 2 μ), D.IsClosable →
      (∀ (a : Lp ℝ 2 μ) (G : Lp E 2 μ), (a,G) ∈ D.graph ↔
        ∃ φ : E → ℝ, ContDiff ℝ ∞ φ ∧ HasCompactSupport φ ∧
          a =ᵐ[μ] φ ∧ G =ᵐ[μ] gradient φ) →
      ∀ z : D.closure.domain, (∫ x, (z : Lp ℝ 2 μ) x ∂μ)=0 →
        m*‖(z : Lp ℝ 2 μ)‖^2 ≤ ‖D.closure z‖^2

Exact module and namespace context

Proof roadmap

1Use actual positive-epsilon solutions
Take epsilon_n=1/(n+1). The accepted centered Gibbs residual producer gives actual solutions in SAME original closure domain and genuine strong epsilon_n*u_n→0. No zero-epsilon solution or uniform unscaled bound is assumed.
2Identify the two genuine witnesses
Global weighted coercivity constructs another solution v_n with m*normDvn^2≤normz^2. Both solve ALL tests in SAME D/epsilon/forcing. Actual closed-graph resolvent uniqueness identifies u_n=v_n, so no existential witnesses or operators are silently identified.
3Test against the centered domain element
The true all-domain variational equation allows v=z and gives its squared norm. No requirement that the resolvent itself have mean0 is introduced.
4Use the actual scalar Cauchy-Schwarz bound
Since m>0, the squared gradient estimate gives sqrtm*normDun≤normz. Multiply the real inner-product bound by positive sqrtm and normDz.
5Pass the strong scaled-residual limit
Continuity of inner evaluation sends the first right-hand term to0. Preserve the same actual z/domain throughout; no cluster/limit certificate is substituted.
6Split zero norm before cancellation
When normz=0 the claim is nonnegativity. Otherwise normz>0, cancel it and square the nonnegative inequality, using (sqrtm)^2=m.

Full assumptions and notation

All objects and hypotheses

Finite-dimensional real Hilbert/Borel full E including0. Actual C2 potential W, ordinary-volume exp(-W) integrability and positive partition. Actual normalized probability mu=volume.tilted(-W).
BOTH actual global mI≤HessW≤MI and0<m≤M. SAME exact original compact-smooth closable weighted gradient D BEFORE ALL mean-zero z in D.closure.domain. No input Poincare or supplied resolvent/coercivity/limit certificate. This canonical library contract is narrower than lower-only source D6.

Mathematical proof

1. Use actual positive-epsilon solutions

Take epsilon_n=1/(n+1). The accepted centered Gibbs residual producer gives actual solutions in SAME original closure domain and genuine strong epsilon_n*u_n→0. No zero-epsilon solution or uniform unscaled bound is assumed.

\[\varepsilon_n=(n+1)^{-1},\quad\varepsilon_nu_n\to0.\]

Corresponding Lean step

CenteredGibbsResolventLimit.gibbs_centered_resolvent_sequence

2. Identify the two genuine witnesses

Global weighted coercivity constructs another solution v_n with m*normDvn^2≤normz^2. Both solve ALL tests in SAME D/epsilon/forcing. Actual closed-graph resolvent uniqueness identifies u_n=v_n, so no existential witnesses or operators are silently identified.

\[u_n=v_n,\qquad m\|\overline Du_n\|^2\le\|z\|^2.\]

Corresponding Lean step

GlobalWeightedResolventCoercivity.global_weak_resolvent_coercivity; ClosedGraphResolvent.weak_resolvent

3. Test against the centered domain element

The true all-domain variational equation allows v=z and gives its squared norm. No requirement that the resolvent itself have mean0 is introduced.

\[\|z\|^2=\langle\varepsilon_nu_n,z\rangle+\langle\overline Du_n,\overline Dz\rangle.\]

Corresponding Lean step

poincare_from_actual_variational_limits; real_inner_self_eq_norm_sq

4. Use the actual scalar Cauchy-Schwarz bound

Since m>0, the squared gradient estimate gives sqrtm*normDun≤normz. Multiply the real inner-product bound by positive sqrtm and normDz.

\[\sqrt m\|z\|^2\le\sqrt m\langle\varepsilon_nu_n,z\rangle+\|z\|\,\|\overline Dz\|.\]

Corresponding Lean step

Real.sqrt_pos; real_inner_le_norm; sq_le_sq₀

5. Pass the strong scaled-residual limit

Continuity of inner evaluation sends the first right-hand term to0. Preserve the same actual z/domain throughout; no cluster/limit certificate is substituted.

\[\sqrt m\|z\|^2\le\|z\|\,\|\overline Dz\|.\]

Corresponding Lean step

Tendsto.inner; le_of_tendsto_of_tendsto

6. Split zero norm before cancellation

When normz=0 the claim is nonnegativity. Otherwise normz>0, cancel it and square the nonnegative inequality, using (sqrtm)^2=m.

\[\sqrt m\|z\|\le\|\overline Dz\|\Longrightarrow m\|z\|^2\le\|\overline Dz\|^2.\]

Corresponding Lean step

mul_le_mul_iff_right₀; Real.sq_sqrt; gibbs_centered_domain_poincare

Lean verification

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

Lean proof · gibbs_centered_domain_poincare

Use actual positive-epsilon solutions; Identify the two genuine witnesses; Test against the centered domain element; Use the actual scalar Cauchy-Schwarz bound; Pass the strong scaled-residual limit; Split zero norm before cancellation

Download module (.lean)

theorem gibbs_centered_domain_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)
    ∀ (D : Lp ℝ 2 μ →ₗ.[ℝ] Lp E 2 μ), D.IsClosable →
      (∀ (a : Lp ℝ 2 μ) (G : Lp E 2 μ), (a,G) ∈ D.graph ↔
        ∃ φ : E → ℝ, ContDiff ℝ ∞ φ ∧ HasCompactSupport φ ∧
          a =ᵐ[μ] φ ∧ G =ᵐ[μ] gradient φ) →
      ∀ z : D.closure.domain, (∫ x, (z : Lp ℝ 2 μ) x ∂μ)=0 →
        m*‖(z : Lp ℝ 2 μ)‖^2 ≤ ‖D.closure z‖^2 := by
  let μ := (volume : Measure E).tilted (fun x => -W x)
  dsimp only
  intro D hD hgraph z hz
  let ε : ℕ → ℝ := fun n => 1/((n:ℝ)+1)
  have hε (n : ℕ) : 0 < ε n := by dsimp [ε];positivity
  have hε0 : Tendsto ε atTop (𝓝 0) := by
    have hinf : Tendsto (fun n : ℕ => (n : ℝ) + 1) atTop atTop :=
      tendsto_atTop_add_const_right atTop (1:ℝ) tendsto_natCast_atTop_atTop
    have hinv : Tendsto (fun n : ℕ => ((n : ℝ) + 1)⁻¹) atTop (𝓝 (0 : ℝ)) :=
      tendsto_inv_atTop_zero.comp hinf
    convert hinv using 1
    funext n
    exact one_div _
  obtain ⟨_,u,hu,ht⟩ :=
    AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.CenteredGibbsResolventLimit.gibbs_centered_resolvent_sequence
      W (hW.of_le (by norm_num)) hI D hD hgraph (z:Lp ℝ 2 μ) hz ε hε hε0
  have hb (n : ℕ) : m*‖D.closure (u n)‖^2 ≤ ‖(z:Lp ℝ 2 μ)‖^2 := by
    obtain ⟨v,hv,_,_,_,_,_,_,hg,hr,_⟩ :=
      AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GlobalWeightedResolventCoercivity.global_weak_resolvent_coercivity
        W hW hI hZ m M hm hmM hlower hupper μ rfl D hD hgraph (ε n) (hε n) (z:Lp ℝ 2 μ)
    obtain ⟨w,_,_,_,_,hwunique⟩ :=
      AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.ClosedGraphResolvent.weak_resolvent
        D.closure hD.closure_isClosed (ε n) (hε n) (z:Lp ℝ 2 μ)
    have hid : u n=v := (hwunique (u n) (hu n).1).trans (hwunique v hv).symm
    rw [hid]
    exact hg.trans hr
  exact poincare_from_actual_variational_limits D.closure m hm z ε u
    (fun n => (hu n).1) hb ht

end AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.CenteredDomainPoincare

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
Actual source C2 alpha-beta reflected law invokes lower-curvature Poincare background D6.	Finite-dimensional real Hilbert/Borel full E including0. Actual C2 potential W, ordinary-volume exp(-W) integrability and positive partition. Actual normalized probability mu=volume.tilted(-W). BOTH actual global mI<=HessW<=MI and0<m<=M. SAME exact original compact-smooth closable weighted gradient D BEFORE ALL mean-zero z in D.closure.domain. No input Poincare or supplied resolvent/coercivity/limit certificate. This canonical library contract is narrower than lower-only source D6.	generalization	Canonical nodes explicitly require BOTH curvature bounds, actual partition/graph context; source consumer derives all ingredients from actual source hypotheses. No full lower-only D6/anisotropic BL is claimed.
Source uses Bakry-Emery/background Poincare.	For every genuinely centered z in the SAME original closed weighted-gradient domain, prove m*normz^2<=normDclosurez^2 from actual positive-epsilon solutions, SAME variational uniqueness, global coercivity and true strong scaled residual limit.	source-implicit	Authored same-D uniqueness/residual limit proof is a sufficient OR-route, not a claim to formalize the printed Bakry-Emery proof.
Normalized conditional density differentiation/marginal Poincare/sampler/main/composition.	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 mnormz^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 mVar<=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)^2norma^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.	unresolved	Only centered-domain Poincare, genuine C1 variance and unnormalized parameter-y score variance admitted.

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.

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

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)

tendsto_inv_atTop_zero
real_inner_le_norm
Real.sqrt_pos
sq_le_sq₀
le_of_tendsto_of_tendsto
mul_le_mul_iff_right₀

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.

Actual centered original-gradient Poincare

Complete source statement (Samplinglib restatement)

Actual centered original-gradient Poincare

Read the formalized proofs

Actual centered original-gradient Poincare

Mathematical statement

Proof roadmap

All objects and hypotheses

Mathematical proof

1. Use actual positive-epsilon solutions

2. Identify the two genuine witnesses

3. Test against the centered domain element

4. Use the actual scalar Cauchy-Schwarz bound

5. Pass the strong scaled-residual limit

6. Split zero norm before cancellation

Lean verification

Source assumptions versus formal assumptions

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Mathematical sources

Which proof obligations and prerequisites are covered?