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

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

  1. 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.

  2. 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.

  3. 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.

  4. 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.

  5. 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.

  6. 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

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 := 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.