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 domḠ with ∫z dν=0, [α/(1+αη)]‖z‖²≤‖Ḡ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

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

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.
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.
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η.
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.
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.
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.
Ḡ 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

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

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.