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

Poincare for the actual Gaussian Gibbs marginal

ASTIS-authored actual marginal centered-domain PI for Fan Chen, Sinho Chewi, Jianfeng Lu and Matthew S. Zhang, fixed PBPS Eq2.13/D6/D10/C3; genuine compact closure and finite Hilbert/Borel/rank0 explicitly scoped. Actual same-law C3/C4 consumers, not fullH1/B13/Gamma/main/composition.

PBPS arXiv2609.06905v1; fixedMathlib; Lean4.33.0 · PBPS2609.06905v1 Eq2.13 and AppendixD.2 D6/D10 feeding C3; original C2, two Hessian bounds,0<alpha<=beta and capped positive eta remain. · faithful paraphrase

Complete source statement (Samplinglib restatement)

Let E be a finite-dimensional real Hilbert Borel space with canonical volume, including rank zero. Let V:E→ℝ be C2, 0<α≤β, α‖a‖²≤D²V(x)[a,a]≤β‖a‖² for every x,a, η>0 and βη≤1. Define μ=volume.tilted(−V), J=law(X,X+√ηZ) for independent X∼μ,Z∼N(0,I), and ν=J.snd. Then ν is a probability. There exists one densely defined closable real linear gradient G:L²(ν)⇀L²(ν;E), whose graph consists exactly of AE classes (φ,∇φ) for smooth compactly supported φ, and whose closure has closed graph. For every z in domḠ with ∫z dν=0, [α/(1+αη)]‖z‖²≤‖Ḡz‖². The same G is chosen before every such z. No caller normalization, curvature, Poincare, law, domain, convergence or extra moment certificate is assumed. This is the genuine compact-gradient closure formulation of the source marginal PI; equivalence with a separately defined weighted H1 remains open.

  • Finite real Hilbert/Borel E with canonical volume, including rank0 explicit source extension.
  • V C2,0<α≤β and both global Hessian bounds;η>0 andβη≤1. The cap is retained although standalone PI needs less; actual sharp source consumer uses it.
  • Uniform genuine G before all centered z in its closed domain. Centering restricts the PI conclusion; no supplied operator/domain/law/PI or extra moment certificate.
  • Ḡ is exactly the closed smooth-compact gradient. Separately defined source weakH1 and onto macro range equivalences are not inferred.

Poincare for the actual Gaussian Gibbs marginal

\[\nu=\operatorname{Law}(X+\sqrt\eta Z),\quad m_\eta=\frac{\alpha}{1+\alpha\eta};\qquad\forall z\in\operatorname{dom}\overline G,\ \int z\,d\nu=0\Rightarrow m_\eta\|z\|_{L^2(\nu)}^2\le\|\overline Gz\|_{L^2(\nu;E)}^2.\]

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

Poincare for the actual Gaussian Gibbs marginal

AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GaussianMarginalPoincare.actual_gaussian_marginal_centered_poincare · theorem · Teaching coverage

Read this first

Mathematical statement

Let E be a finite-dimensional real Hilbert Borel space with canonical volume, including rank zero. Let V:E→ℝ be C2, 0<α≤β, α‖a‖²≤D²V(x)[a,a]≤β‖a‖² for every x,a, η>0 and βη≤1. Define μ=volume.tilted(−V), J=law(X,X+√ηZ) for independent X∼μ,Z∼N(0,I), and ν=J.snd. Then ν is a probability. There exists one densely defined closable real linear gradient G:L²(ν)⇀L²(ν;E), whose graph consists exactly of AE classes (φ,∇φ) for smooth compactly supported φ, and whose closure has closed graph. For every z in domḠ with ∫z dν=0, [α/(1+αη)]‖z‖²≤‖Ḡz‖². The same G is chosen before every such z. No caller normalization, curvature, Poincare, law, domain, convergence or extra moment certificate is assumed. This is the genuine compact-gradient closure formulation of the source marginal PI; equivalence with a separately defined weighted H1 remains open.

\[\nu=\operatorname{Law}(X+\sqrt\eta Z),\quad m_\eta=\frac{\alpha}{1+\alpha\eta};\qquad\forall z\in\operatorname{dom}\overline G,\ \int z\,d\nu=0\Rightarrow m_\eta\|z\|_{L^2(\nu)}^2\le\|\overline Gz\|_{L^2(\nu;E)}^2.\]
Lean statement · actual_gaussian_marginal_centered_poincare

Let E be a finite-dimensional real Hilbert Borel space with canonical volume, including rank zero. Let V:E→ℝ be C2, 0<α≤β, α‖a‖²≤D²V(x)[a,a]≤β‖a‖² for every x,a, η>0 and βη≤1. Define μ=volume.tilted(−V), J=law(X,X+√ηZ) for independent X∼μ,Z∼N(0,I), and ν=J.snd. Then ν is a probability. There exists one densely defined closable real linear gradient G:L²(ν)⇀L²(ν;E), whose graph consists exactly of AE classes (φ,∇φ) for smooth compactly supported φ, and whose closure has closed graph. For every z in domḠ with ∫z dν=0, [α/(1+αη)]‖z‖²≤‖Ḡz‖². The same G is chosen before every such z. No caller normalization, curvature, Poincare, law, domain, convergence or extra moment certificate is assumed. This is the genuine compact-gradient closure formulation of the source marginal PI; equivalence with a separately defined weighted H1 remains open.

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 actual_gaussian_marginal_centered_poincare
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {V : E → ℝ} {α β : ℝ≥0} {η : ℝ}
    (hα : 0 < (α : ℝ)) (hαβ : α ≤ β) (hV : ContDiff ℝ 2 V)
    (hH : ∀ x v : E,
      (α : ℝ)*‖v‖^2 ≤ (fderiv ℝ (fderiv ℝ V) x v) v ∧
      (fderiv ℝ (fderiv ℝ V) x v) v ≤ (β : ℝ)*‖v‖^2)
    (hη : 0 < η) (hβη : (β : ℝ)*η ≤ 1) :
    let μ := (volume : Measure E).tilted (fun x => -V x)
    let J := (μ.prod (stdGaussian E)).map
      (fun p : E × E => (p.1,p.1+Real.sqrt η • p.2))
    let ν := J.snd
    IsProbabilityMeasure ν ∧
      ∃ G : Lp ℝ 2 ν →ₗ.[ℝ] Lp E 2 ν,
        Dense (G.domain : Set (Lp ℝ 2 ν)) ∧ G.IsClosable ∧ G.closure.IsClosed ∧
        (∀ (u : Lp ℝ 2 ν) (v : Lp E 2 ν), (u,v) ∈ G.graph ↔
          ∃ φ : E → ℝ, ContDiff ℝ ∞ φ ∧ HasCompactSupport φ ∧
            u =ᵐ[ν] φ ∧ v =ᵐ[ν] gradient φ) ∧
        ∀ z : G.closure.domain,
          (∫ x, (z : Lp ℝ 2 ν) x ∂ν) = 0 →
          ((α : ℝ)/(1+(α : ℝ)*η))*‖(z : Lp ℝ 2 ν)‖^2 ≤ ‖G.closure z‖^2

Exact module and namespace context

Proof roadmap

  1. 1Derive the actual marginal law and its potential

    Original lower curvature and C2 yield positive finite ZV and probability μ. The existing smoothed Gibbs producer gives Aη(y)=cη∫exp(−V(x)−‖y−x‖²/(2η))dx, positive C2 Vη=−logAη, ∫Aη=ZV and the exact actual add-noise law ν=volume.tilted(−Vη). The normalized negative-log density Uη differs from Vη by logZV; no normalizer or law equality is supplied.

  2. 2Produce the true conditional covariance bound

    The actual Gaussian derivative producer supplies probability and vectorL2 moments of R_y=μ.tilted(x↦−‖x−y‖²/(2η)). Derive R_y=volume.tilted(−W_y) with W_y(x)=V(x)+‖x−y‖²/(2η). Its genuine Hessian lies between α+η⁻¹ and β+η⁻¹. Strong convexity gives exp-L1 and a positive partition internally. Existing original-domain covariance upper applies to the actual posterior and its produced moments; no covariance or moment certificate is a theorem premise.

  3. 3Obtain both exact marginal curvature constants

    The actual normalized Hessian identity and additive partition shift imply D²Vη(y)[a,a]=‖a‖²/η−CovR_y(a,a)/η². The produced covariance upper gives mη=α/(1+αη). Reuse the already verified generic SmoothedHessianUpper producer for Mη=β/(1+βη); it retains the true Cramer-Rao/posterior inputs and is not replaced by a coarse certificate. α≤β gives mη≤Mη.

  4. 4Apply Poincare on the genuine closed gradient domain

    The actual Gaussian marginal gradient producer constructs the dense smooth-compact graph G, closability and its closed closure. The actual potential has exp-L1 and a positive partition from step1. The existing centered-domain Poincare producer applies to this exact G under both derived curvature bounds. Thus one G works for every centered member of its genuine closed domain. This is a scoped closure result; the original source weakH1 identification remains a separate obligation.

  5. 5Derive domain agreement and centeredness for the real mean

    The real consumer obtains G56,T56,K56 from the actual rough mean-gradient theorem. The two exact compact graph iff statements over the same ν imply G56=G57 and hence equality of their closures; the genuine pair (T56u,K56u) transfers internally. Actual55 constructs the literal reflected Markov S with a conditional joint Λ and both marginals ν. Using actual56 AE source means and actual disintegration gives ∫T56u dν=∫u dν for every L2 input. Thus centered u gives centered T56u; no output-centering/domain certificate is supplied.

  6. 6Consume the exact source C3 and sharp C4 estimate

    For centered u the preceding derived domain and centering allow PI on Tu: mη‖Tu‖²≤‖Ku‖². Combine it with actual56 sharp energy η‖Ku‖²≤c(‖u‖²−‖Tu‖²), c=(1−αη)²/[4(1+αη)]. Explicit scalar algebra yields (1+αη)²‖Tu‖²≤(1−αη)²‖u‖². Original α≤β and βη≤1 make ρ=(1−αη)/(1+αη) nonnegative, so squared comparison gives ‖Tu‖≤ρ‖u‖, including αη=1 without dividing by1−αη. Full macro-range, H1 and Γ identity are separate.

Full assumptions and notation

All objects and hypotheses

  • Finite real Hilbert/Borel E with canonical volume, including rank0 explicit source extension.
  • V C2,0<α≤β and both global Hessian bounds;η>0 andβη≤1. The cap is retained although standalone PI needs less; actual sharp source consumer uses it.
  • Uniform genuine G before all centered z in its closed domain. Centering restricts the PI conclusion; no supplied operator/domain/law/PI or extra moment certificate.
  • Ḡ is exactly the closed smooth-compact gradient. Separately defined source weakH1 and onto macro range equivalences are not inferred.

Mathematical proof

1. Derive the actual marginal law and its potential

Original lower curvature and C2 yield positive finite ZV and probability μ. The existing smoothed Gibbs producer gives Aη(y)=cη∫exp(−V(x)−‖y−x‖²/(2η))dx, positive C2 Vη=−logAη, ∫Aη=ZV and the exact actual add-noise law ν=volume.tilted(−Vη). The normalized negative-log density Uη differs from Vη by logZV; no normalizer or law equality is supplied.

\[\nu=\mathrm{vol}.\mathrm{tilted}(-V_\eta),\quad A_\eta=e^{-V_\eta}>0,\quad\int A_\eta=Z_V>0,\quad U_\eta=V_\eta+\log Z_V.\]
Corresponding Lean step

SmoothedGibbsPotential.smoothed_gibbs_potential; htilt; hIA; hIntA; hA; hC2; hshift; Measure.map_map

2. Produce the true conditional covariance bound

The actual Gaussian derivative producer supplies probability and vectorL2 moments of R_y=μ.tilted(x↦−‖x−y‖²/(2η)). Derive R_y=volume.tilted(−W_y) with W_y(x)=V(x)+‖x−y‖²/(2η). Its genuine Hessian lies between α+η⁻¹ and β+η⁻¹. Strong convexity gives exp-L1 and a positive partition internally. Existing original-domain covariance upper applies to the actual posterior and its produced moments; no covariance or moment certificate is a theorem premise.

\[W_y(x)=V(x)+\frac{\|x-y\|^2}{2\eta},\quad(\alpha+\eta^{-1})I\preceq D^2W_y\preceq(\beta+\eta^{-1})I,\quad\operatorname{Var}_{R_y}\langle a,X\rangle\le\frac{\|a\|^2}{\alpha+\eta^{-1}}.\]
Corresponding Lean step

GaussianConvolutionRegularity.gaussian_convolution_derivatives; hRm; hcov; hWdd; hb; hiW; hRW; GibbsLinearCovarianceUpper.gibbs_linear_covariance_upper

3. Obtain both exact marginal curvature constants

The actual normalized Hessian identity and additive partition shift imply D²Vη(y)[a,a]=‖a‖²/η−CovR_y(a,a)/η². The produced covariance upper gives mη=α/(1+αη). Reuse the already verified generic SmoothedHessianUpper producer for Mη=β/(1+βη); it retains the true Cramer-Rao/posterior inputs and is not replaced by a coarse certificate. α≤β gives mη≤Mη.

\[D^2V_\eta(y)[a,a]=\frac{\|a\|^2}{\eta}-\frac{\operatorname{Cov}_{R_y}(a,a)}{\eta^2},\quad0<m_\eta=\frac\alpha{1+\alpha\eta}\le M_\eta=\frac\beta{1+\beta\eta},\quad m_\eta I\preceq D^2V_\eta\preceq M_\eta I.\]
Corresponding Lean step

hDD; he; hd; hlower; SmoothedHessianUpper.smoothed_hessian_upper; hupper; hm; hmM

4. Apply Poincare on the genuine closed gradient domain

The actual Gaussian marginal gradient producer constructs the dense smooth-compact graph G, closability and its closed closure. The actual potential has exp-L1 and a positive partition from step1. The existing centered-domain Poincare producer applies to this exact G under both derived curvature bounds. Thus one G works for every centered member of its genuine closed domain. This is a scoped closure result; the original source weakH1 identification remains a separate obligation.

\[\operatorname{graph}G=\{([\varphi],[\nabla\varphi]):\varphi\in C_c^\infty\},\quad\overline{\operatorname{dom}G}=L^2(\nu),\quad\int z\,d\nu=0\Rightarrow m_\eta\|z\|^2\le\|\overline Gz\|^2.\]
Corresponding Lean step

GaussianMarginalGradient.gaussian_marginal_gradient_closable; hI; hZη; CenteredDomainPoincare.gibbs_centered_domain_poincare; hPI

5. Derive domain agreement and centeredness for the real mean

The real consumer obtains G56,T56,K56 from the actual rough mean-gradient theorem. The two exact compact graph iff statements over the same ν imply G56=G57 and hence equality of their closures; the genuine pair (T56u,K56u) transfers internally. Actual55 constructs the literal reflected Markov S with a conditional joint Λ and both marginals ν. Using actual56 AE source means and actual disintegration gives ∫T56u dν=∫u dν for every L2 input. Thus centered u gives centered T56u; no output-centering/domain certificate is supplied.

\[G_{56}=G_{57},\quad(Tu,Ku)\in\operatorname{graph}\overline G;\quad\Lambda=\nu\otimes S,\ \Lambda_2=\nu\Rightarrow\int Tu\,d\nu=\int u\,d\nu.\]
Corresponding Lean step

Tests.GaussianMarginalPoincare.actual_same_mean_centered_contraction; hSameG; LinearPMap.eq_of_eq_graph; hcompS; hMean; hPreserve; Measure.integral_compProd; integral_map

6. Consume the exact source C3 and sharp C4 estimate

For centered u the preceding derived domain and centering allow PI on Tu: mη‖Tu‖²≤‖Ku‖². Combine it with actual56 sharp energy η‖Ku‖²≤c(‖u‖²−‖Tu‖²), c=(1−αη)²/[4(1+αη)]. Explicit scalar algebra yields (1+αη)²‖Tu‖²≤(1−αη)²‖u‖². Original α≤β and βη≤1 make ρ=(1−αη)/(1+αη) nonnegative, so squared comparison gives ‖Tu‖≤ρ‖u‖, including αη=1 without dividing by1−αη. Full macro-range, H1 and Γ identity are separate.

\[m_\eta\|Tu\|^2\le\|Ku\|^2,\quad\eta\|Ku\|^2\le\frac{(1-\alpha\eta)^2}{4(1+\alpha\eta)}(\|u\|^2-\|Tu\|^2)\Rightarrow\|Tu\|\le\frac{1-\alpha\eta}{1+\alpha\eta}\|u\|.\]
Corresponding Lean step

hC3; hSharp; hP; hSharp′; hSq; hSq′; sq_le_sq₀

Lean verification

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

Lean proof · actual_gaussian_marginal_centered_poincare

Derive the actual marginal law and its potential; Produce the true conditional covariance bound; Obtain both exact marginal curvature constants; Apply Poincare on the genuine closed gradient domain; Derive domain agreement and centeredness for the real mean; Consume the exact source C3 and sharp C4 estimate

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 actual_gaussian_marginal_centered_poincare
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {V : E → ℝ} {α β : ℝ≥0} {η : ℝ}
    (hα : 0 < (α : ℝ)) (hαβ : α ≤ β) (hV : ContDiff ℝ 2 V)
    (hH : ∀ x v : E,
      (α : ℝ)*‖v‖^2 ≤ (fderiv ℝ (fderiv ℝ V) x v) v ∧
      (fderiv ℝ (fderiv ℝ V) x v) v ≤ (β : ℝ)*‖v‖^2)
    (hη : 0 < η) (hβη : (β : ℝ)*η ≤ 1) :
    let μ := (volume : Measure E).tilted (fun x => -V x)
    let J := (μ.prod (stdGaussian E)).map
      (fun p : E × E => (p.1,p.1+Real.sqrt η • p.2))
    let ν := J.snd
    IsProbabilityMeasure ν ∧
      ∃ G : Lp ℝ 2 ν →ₗ.[ℝ] Lp E 2 ν,
        Dense (G.domain : Set (Lp ℝ 2 ν)) ∧ G.IsClosable ∧ G.closure.IsClosed ∧
        (∀ (u : Lp ℝ 2 ν) (v : Lp E 2 ν), (u,v) ∈ G.graph ↔
          ∃ φ : E → ℝ, ContDiff ℝ ∞ φ ∧ HasCompactSupport φ ∧
            u =ᵐ[ν] φ ∧ v =ᵐ[ν] gradient φ) ∧
        ∀ z : G.closure.domain,
          (∫ x, (z : Lp ℝ 2 ν) x ∂ν) = 0 →
          ((α : ℝ)/(1+(α : ℝ)*η))*‖(z : Lp ℝ 2 ν)‖^2 ≤ ‖G.closure z‖^2 := by
  classical
  letI : CompleteSpace E := FiniteDimensional.complete ℝ E
  dsimp only
  let μ := (volume : Measure E).tilted (fun x => -V x)
  let J := (μ.prod (stdGaussian E)).map
    (fun p : E × E => (p.1,p.1+Real.sqrt η • p.2))
  let ν := J.snd
  let C := ((Real.sqrt (2*Real.pi*η))⁻¹)^Module.finrank ℝ E
  let A := fun y : E => C*∫ x, Real.exp (-V x-‖y-x‖^2/(2*η)) ∂(volume : Measure E)
  let Vη := fun y : E => -Real.log (A y)
  let R := fun y : E => μ.tilted (fun x => -‖x-y‖^2/(2*η))
  let U := fun y : E => -Real.log (C*∫ x, Real.exp (-‖y-x‖^2/(2*η)) ∂μ)
  let ZV := ∫ x, Real.exp (-V x) ∂(volume : Measure E)
  obtain ⟨hZ,hμ,_hlaw,hIA,hIntA,hTilt,hA,hC2,hshift⟩ :=
    AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.SmoothedGibbsPotential.smoothed_gibbs_potential
      hα hV (fun x a => (hH x a).1) hη
  letI : IsProbabilityMeasure μ := hμ
  have hpair : Measurable (fun p : E × E => (p.1,p.1+Real.sqrt η • p.2)) := by fun_prop
  letI : IsProbabilityMeasure J := Measure.isProbabilityMeasure_map hpair.aemeasurable
  letI : IsProbabilityMeasure ν := Measure.isProbabilityMeasure_map measurable_snd.aemeasurable
  have htilt : ν = (volume : Measure E).tilted (fun y => -Vη y) :=
    (Measure.map_map measurable_snd hpair).trans hTilt
  have hC : 0<C := by dsimp only [C]; positivity
  obtain ⟨hRm,_hD,hDD⟩ :=
    AutoSamplingTheory.TechnicalLemmas.Measure.GaussianConvolutionRegularity.gaussian_convolution_derivatives μ hη hC
  have hi := AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexGibbsIntegrability.integrable_exp_neg_of_strongConvexOn
    hα (hV.differentiable (by norm_num))
    (AutoSamplingTheory.TechnicalLemmas.Analysis.HessianStrongConvexity.strongConvexOn_univ_of_fderiv2_lower hV (fun x a => (hH x a).1))
  have hcov (y : E) : ∀ a : E, covarianceBilin (R y) a a ≤ ‖a‖^2/((α : ℝ)+η⁻¹) := by
    let W := fun x => V x+η⁻¹/2*‖x-y‖^2
    have hW : ContDiff ℝ 2 W := hV.add (contDiff_const.mul ((contDiff_id.sub contDiff_const).norm_sq (𝕜:=ℝ)))
    have hVd : Differentiable ℝ V := hV.differentiable (by norm_num)
    have hVdd : Differentiable ℝ (fderiv ℝ V) := (hV.fderiv_right (m:=1) (by norm_num)).differentiable_one
    have hq (x : E) : HasFDerivAt (fun z => η⁻¹/2*‖z-y‖^2)
        (η⁻¹ • innerSL ℝ (x-y)) x := by
      convert (((hasFDerivAt_id x).sub_const y).norm_sq).const_mul (η⁻¹/2)
        using 1 <;> first | rfl | (ext a; simp;ring)
    have hWfd (x : E) : fderiv ℝ W x = fderiv ℝ V x+η⁻¹ • innerSL ℝ (x-y) :=
      ((hVd x).hasFDerivAt.add (hq x)).fderiv
    let J : E →L[ℝ] (E →L[ℝ] ℝ) :=
      {toFun := fun a => innerSL ℝ a
       map_add' := by intros;ext;simp
       map_smul' := by intros;ext;simp
       cont := (innerSL ℝ (E:=E)).continuous}
    have hWdd (x : E) : HasFDerivAt (fderiv ℝ W)
        (fderiv ℝ (fderiv ℝ V) x+η⁻¹ • J) x := by
      rw [show fderiv ℝ W=(fun z => fderiv ℝ V z+η⁻¹ • innerSL ℝ (z-y)) from funext hWfd]
      convert (hVdd x).hasFDerivAt.add ((J.hasFDerivAt.comp x ((hasFDerivAt_id x).sub_const y)).const_smul η⁻¹) using 1 <;> rfl
    have hb (x a : E) : ((α : ℝ)+η⁻¹)*‖a‖^2 ≤ fderiv ℝ (fderiv ℝ W) x a a ∧
        fderiv ℝ (fderiv ℝ W) x a a ≤ ((β : ℝ)+η⁻¹)*‖a‖^2 := by
      rw [(hWdd x).fderiv]
      change ((α : ℝ)+η⁻¹)*‖a‖^2 ≤ fderiv ℝ (fderiv ℝ V) x a a+η⁻¹*inner ℝ a a ∧
        fderiv ℝ (fderiv ℝ V) x a a+η⁻¹*inner ℝ a a ≤ ((β : ℝ)+η⁻¹)*‖a‖^2
      rw [real_inner_self_eq_norm_sq]
      constructor <;> nlinarith [(hH x a).1,(hH x a).2]
    have hm : 0<(α : ℝ)+η⁻¹ := add_pos hα (inv_pos.mpr hη)
    have hmM : (α : ℝ)+η⁻¹≤(β : ℝ)+η⁻¹ := by
      simpa only [add_comm] using (add_le_add_right (show (α : ℝ) ≤ (β : ℝ) from hαβ) η⁻¹)
    have hiW := AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexGibbsIntegrability.integrable_exp_neg_of_strongConvexOn
      hm (hW.differentiable (by norm_num))
      (AutoSamplingTheory.TechnicalLemmas.Analysis.HessianStrongConvexity.strongConvexOn_univ_of_fderiv2_lower hW (fun x a => (hb x a).1))
    have hRW : R y=(volume : Measure E).tilted (fun x => -W x) := by
      dsimp only [R,μ]
      rw [tilted_tilted hi]
      congr 1
      funext x
      simp only [Pi.add_apply,W]
      field_simp [hη.ne']
      ring
    have hX : MemLp id 2 ((volume : Measure E).tilted (fun x => -W x)) := hRW ▸ (hRm y).2
    rw [hRW]
    exact AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GibbsLinearCovarianceUpper.gibbs_linear_covariance_upper
      W hW hiW (integral_exp_pos hiW) ((α : ℝ)+η⁻¹) ((β : ℝ)+η⁻¹) hm hmM
      (fun x a => (hb x a).1) (fun x a => (hb x a).2) hX
  have he : U=(fun y => Vη y+Real.log ZV) := funext hshift
  have hd : fderiv ℝ U=fderiv ℝ Vη := by
    rw [he]
    funext y
    exact fderiv_add_const _
  change ∀ y a b, fderiv ℝ (fderiv ℝ U) y a b = _ at hDD
  rw [hd] at hDD
  let m := (α : ℝ)/(1+(α : ℝ)*η)
  let M := (β : ℝ)/(1+(β : ℝ)*η)
  have hden : 0<1+(α : ℝ)*η := by positivity
  have hbden : 0<1+(β : ℝ)*η := by positivity
  have hm : 0<m := div_pos hα hden
  have hmM : m≤M := by
    dsimp only [m,M]
    apply (div_le_div_iff₀ hden hbden).2
    nlinarith [show (α : ℝ) ≤ (β : ℝ) from hαβ]
  have hlower (y a : E) : m*‖a‖^2 ≤ fderiv ℝ (fderiv ℝ Vη) y a a := by
    rw [hDD y a a,real_inner_self_eq_norm_sq]
    have hp : 0<(α : ℝ)+η⁻¹ := add_pos hα (inv_pos.mpr hη)
    calc
      m*‖a‖^2 = ‖a‖^2/η-(‖a‖^2/((α : ℝ)+η⁻¹))/η^2 := by
        dsimp only [m]
        field_simp [hη.ne',hp.ne',hden.ne']
        ring
      _ ≤ ‖a‖^2/η-covarianceBilin (R y) a a/η^2 :=
        sub_le_sub_left (div_le_div_of_nonneg_right (hcov y a) (sq_nonneg η)) _
  have hupper : ∀ y a : E, fderiv ℝ (fderiv ℝ Vη) y a a ≤ M*‖a‖^2 :=
    (AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.SmoothedHessianUpper.smoothed_hessian_upper
      (show 0<α from hα) hαβ hV hH hη).2
  have hI : Integrable (fun y => Real.exp (-Vη y)) (volume : Measure E) := by
    have hexp (y : E) : Real.exp (-Vη y)=A y := by
      dsimp only [Vη];rw [neg_neg,Real.exp_log (hA y)]
    simpa only [hexp] using hIA
  have hZη : 0<∫ y, Real.exp (-Vη y) ∂(volume : Measure E) := integral_exp_pos hI
  obtain ⟨G,hDense,hClose,hClosed,hGraph⟩ :=
    GaussianMarginalGradient.gaussian_marginal_gradient_closable μ hη
  refine ⟨inferInstance,G,hDense,hClose,hClosed,hGraph,?_⟩
  have hPI : ∀ (D : Lp ℝ 2 ν →ₗ.[ℝ] Lp E 2 ν), D.IsClosable →
      (∀ (a : Lp ℝ 2 ν) (F : Lp E 2 ν), (a,F) ∈ D.graph ↔
        ∃ φ : E → ℝ, ContDiff ℝ ∞ φ ∧ HasCompactSupport φ ∧
          a =ᵐ[ν] φ ∧ F =ᵐ[ν] gradient φ) →
      ∀ z : D.closure.domain, (∫ x, (z : Lp ℝ 2 ν) x ∂ν)=0 →
        m*‖(z : Lp ℝ 2 ν)‖^2 ≤ ‖D.closure z‖^2 := by
    rw [htilt]
    exact CenteredDomainPoincare.gibbs_centered_domain_poincare
      Vη hC2 hI hZη m M hm hmM hlower hupper
  exact hPI G hClose hGraph

end
end AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GaussianMarginalPoincare

Exact module and namespace context

Source assumptions versus formal assumptions

SourceActual LeanDifference kindWhy it matters
PBPS2609.06905v1 Eq2.13 and AppendixD.2 D6/D10 feeding C3; original C2, two Hessian bounds,0<alpha<=beta and capped positive eta remain.mu=tilt-volume(-V), J=law(X,X+sqrtetaZ), nu=J.snd; G exact smooth compact scalar/vector-L2 graph, actual closure and actual normalized mean.sameOriginal assumptions and coefficient retained; all real density/normalization/moments/curvature/domain ingredients produced internally.
Source Euclidean weighted-H1 marginal Poincare and C3.Finite real Hilbert/Borel including rank0 explicit; exact compact-gradient closure Poincare, not equality to a separately defined weighted H1. Uniform genuine G selected before all centered domain z.unresolvedFinite Hilbert/Borel/rank0 extension disclosed. Genuine compact-gradient closure advertized; equality with separately defined weakH1 remains open.
C3 applies PI to centered actual Af; C4 sharp energy yields macroscopic contraction.Test identifies SAME56 compact gradient, derives integral preservation and centeredness from actual55 law, then exactrho on real L2(nu).sameTwo missing prerequisite paths preserved as original negative plus separately reviewed overlay; no caller input certificates.
Whole macro-range, fullB13/Gamma/dynamics/main/errors/cost/composition.Actual normalized Gibbs/Gaussian marginal nu has one genuine dense closable compact-gradient G and closed closure, selected before every centered z in its domain; alpha/(1+alpha eta)||z||²<=||Gbar z||². Original C2/two global Hessian bounds,0<alpha<=beta,eta>0,beta eta<=1 retained; finite Hilbert/Borel/rank0 explicitly extends source Euclidean setting. Actual56 SAME T/K image and internally derived stationarity/centering consume this for C3 and exactrho contraction. Full weakH1/macro-range/B13/Gamma/dynamics/main/errors/cost/composition remain open.unresolvedNo full-paper or separate inverse/spectral/domain/cost claim.

Actual normalized Gibbs/Gaussian marginal nu has one genuine dense closable compact-gradient G and closed closure, selected before every centered z in its domain; alpha/(1+alpha eta)||z||²<=||Gbar z||². Original C2/two global Hessian bounds,0<alpha<=beta,eta>0,beta eta<=1 retained; finite Hilbert/Borel/rank0 explicitly extends source Euclidean setting. Actual56 SAME T/K image and internally derived stationarity/centering consume this for C3 and exactrho contraction. Full weakH1/macro-range/B13/Gamma/dynamics/main/errors/cost/composition remain open.

Encoder–denoiser: accepted · equivalent-after-elaboration

Detected semantic differences

  • domains: Finite real Hilbert/Borel including rank0 explicitly extends printed Euclidean presentation; ambientL2 not finite-dimensional. — Independent source classification: explicit-attributed-background-extension; explicitly nonblocking.
  • scopes: Genuine compact-gradient closure PI and actualL2nu SAME56 C3/C4 consumer; separately defined weakH1 and onto macroH_P equivalence/fullB13/Gamma are not claimed. — Independent source classification: explicit-scoped-authored-integration; explicitly nonblocking.
  • objects: Reused source unnormalized SPHMC Veta differs from PBPS normalized marginal negative-log Ueta by logZV; actualtilted law and Hessian identities are matched internally, no literal potential equality assumed. — Independent source classification: notation-resolution; explicitly nonblocking.

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
  • Actual normalized Gibbs/Gaussian marginal nu has one genuine dense closable compact-gradient G and closed closure, selected before every centered z in its domain; alpha/(1+alpha eta)||z||²≤||Gbar z||². Original C2/two global Hessian bounds,0<alpha≤beta,eta>0,beta eta≤1 retained; finite Hilbert/Borel/rank0 explicitly extends source Euclidean setting. Actual56 SAME T/K image and internally derived stationarity/centering consume this for C3 and exactrho contraction. Full weakH1/macro-range/B13/Gamma/dynamics/main/errors/cost/composition remain open.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

  • Measure.map_map
  • Measure.tilted_tilted
  • integral_exp_pos
  • fderiv_add_const
  • LinearPMap.eq_of_eq_graph
  • Measure.disintegrate
  • Measure.integral_compProd
  • integral_map
  • sq_le_sq₀

Mathematical sources

  • PBPS2609.06905v1 Eq2.13 and AppendixD.2 D6/D10 feeding C3; original C2, two Hessian bounds,0<alpha<=beta and capped positive eta remain. — Actual normalized Gibbs/Gaussian marginal nu has one genuine dense closable compact-gradient G and closed closure, selected before every centered z in its domain; alpha/(1+alpha eta)||z||²<=||Gbar z||². Original C2/two global Hessian bounds,0<alpha<=beta,eta>0,beta eta<=1 retained; finite Hilbert/Borel/rank0 explicitly extends source Euclidean setting. Actual56 SAME T/K image and internally derived stationarity/centering consume this for C3 and exactrho contraction. Full weakH1/macro-range/B13/Gamma/dynamics/main/errors/cost/composition remain open.

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.

Which proof obligations and prerequisites are covered?

  • Formalized proof edge; source adapter/review separate Actual normalized marginal centered compact-domain PI and real SAME56 consumer
  • TODO — not closed by these contributions FullH1/macro-range/B13/Gamma/main/error/cost/composition open