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

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.

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

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.