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

Actual SPHMC smoothed Hessian bounds

Fan Chen, Sinho Chewi, Jianfeng Lu, Matthew S. Zhang; actual analytic Lemma4.1, source beta1/kappa/eta cap.

arXiv:2609.06906v1 · SPHMC arXiv:2609.06906v1 Sections1-3 standing beta=1/alpha=kappa^-1/RGO/smoothing and Section4.1 S4.E1, Lemma4.1 S4.Thmtheorem1, S4.Ex4-6; actual unreflected posterior covariance and source unnormalized V_eta. Primary-first Smoothed_Hessian_lower_source_preread.md. · faithful paraphrase

Complete source statement (Samplinglib restatement)

For the actual source Gaussian-smoothed unnormalized potential and true RGO posterior, produce probability and vectorL2, covariance upper norma^2/(kappa^-1+eta^-1), C2 regularity and (kappa+eta)^-1*norma^2<=D2V_eta(y)[a,a]<=(1+eta)^-1*norma^2, and true1-Lipschitz gradient. This is the analytic Lemma4.1, not an algorithm/main theorem.

  • Source C2 V with beta=1 and alpha=kappa^-1; kappa>=1; actual allpoint/allvector curvature kappa^-1*norma^2<=D2V[a,a]<=norma^2; source0<eta<=1 retained.
  • Actual source UNNORMALIZED exp(-V_eta)=exp(-V)*Gaussian_eta, normalized Gibbs mu=volume.tilted(-V), unreflected R_y=mu.tilted(-norm(x-y)^2/(2eta)). Finite Hilbert/Borel including0 is disclosed representation extension.
  • No partition, covariance, moment, derivative or PI certificate on this source theorem. Actual probability, posterior vectorL2, C2, U=V_eta+logZV, both true Hessian bounds and global Lipschitz are produced internally. No joint measurable posterior kernel selector, higher derivative, numerical kernel, cost or main claim.

Actual SPHMC smoothed Hessian bounds

\[R_y(dx)\propto e^{-V(x)-\|x-y\|^2/(2\eta)}dx,\quad (\kappa+\eta)^{-1}I\preceq D^2V_\eta\preceq(1+\eta)^{-1}I,\quad \operatorname{Lip}(\nabla V_\eta)\le1.\]

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 SPHMC smoothed Hessian bounds

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.SmoothedHessianBounds.smoothed_hessian_bounds · theorem · Teaching coverage

Read this first

Mathematical statement

For the actual source Gaussian-smoothed unnormalized potential and true RGO posterior, produce probability and vectorL2, covariance upper norma^2/(kappa^-1+eta^-1), C2 regularity and (kappa+eta)^-1*norma^2≤D2V_eta(y)[a,a]≤(1+eta)^-1*norma^2, and true1-Lipschitz gradient. This is the analytic Lemma4.1, not an algorithm/main theorem.

\[R_y(dx)\propto e^{-V(x)-\|x-y\|^2/(2\eta)}dx,\quad (\kappa+\eta)^{-1}I\preceq D^2V_\eta\preceq(1+\eta)^{-1}I,\quad \operatorname{Lip}(\nabla V_\eta)\le1.\]
Lean statement · smoothed_hessian_bounds

For the actual source Gaussian-smoothed unnormalized potential and true RGO posterior, produce probability and vectorL2, covariance upper norma^2/(kappa^-1+eta^-1), C2 regularity and (kappa+eta)^-1*norma^2<=D2V_eta(y)[a,a]<=(1+eta)^-1*norma^2, and true1-Lipschitz gradient. This is the analytic Lemma4.1, not an algorithm/main theorem.

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 smoothed_hessian_bounds
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace E]
    {V : E → ℝ} {κ η : ℝ}
    (hκ : 1 ≤ κ) (hV : ContDiff ℝ 2 V)
    (hH : ∀ x a : E, κ⁻¹*‖a‖^2 ≤ fderiv ℝ (fderiv ℝ V) x a a ∧
      fderiv ℝ (fderiv ℝ V) x a a ≤ ‖a‖^2)
    (hη : 0 < η) (hη1 : η ≤ 1) :
    let μ := (volume : Measure E).tilted (fun x => -V x)
    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 => -Real.log (A y)
    let R := fun y : E => μ.tilted (fun x => -‖x-y‖^2/(2*η))
    IsProbabilityMeasure μ ∧ ContDiff ℝ 2 Vη ∧
      (∀ y, IsProbabilityMeasure (R y) ∧ MemLp id 2 (R y) ∧
        (∀ a, ProbabilityTheory.covarianceBilin (R y) a a ≤ ‖a‖^2/(κ⁻¹+η⁻¹)) ∧
        ∀ a, (1/(κ+η))*‖a‖^2 ≤ fderiv ℝ (fderiv ℝ Vη) y a a ∧
          fderiv ℝ (fderiv ℝ Vη) y a a ≤ (1/(1+η))*‖a‖^2) ∧
      LipschitzWith (1 : ℝ≥0) (gradient Vη)

Exact module and namespace context

Proof roadmap

  1. 1Construct the actual source smoothing

    Positive source curvature gives the true partition and probability. The accepted convolution producer gives C2 V_eta and the literal normalized-U constant shift, with no input normalizer.

  2. 2Produce true posterior moments and derivative identity

    The Gaussian convolution producer gives R_y probability and vectorL2 for every actualy, and true Hessian of U. The produced constant shift identifies both Hessians.

  3. 3Keep the unreflected quadratic law

    Set W_y=V+norm(x-y)^2/(2eta). Derive its C2 Hessian shift and both positive curvature bounds. True strong convexity gives its exponential integrability/positive partition; tilted_tilted proves literal R_y equality.

  4. 4Apply the canonical covariance producer

    Transport the internally produced posterior vectorL2 through the actual law equality, then apply the new Poincare-derived covariance theorem. This suffices for the source isotropic bound; full anisotropic BL remains open.

  5. 5Derive the exact lower Hessian constant

    Subtract the covariance upper bound in the true identity. kappa/eta and both sum denominators are positive, so algebra preserves inequality and yields the exact source lower constant.

  6. 6Reuse the actual reverse-Cramer-Rao half

    The independently checked actual posterior covariance lower and source smoothed Hessian upper theorem is specialized to beta1. No duplicated abstract Hessian field or assumed upper bound.

  7. 7Prove true global gradient Lipschitz

    The produced C2 potential has nonnegative Hessian and upper quadratic bound bynorma^2. Existing Riesz/selfadjoint Rayleigh norm and global mean-value producer yields1-Lipschitz gradient with zero extra regularization. The source eta cap remains an explicit premise.

Full assumptions and notation

All objects and hypotheses

  • Source C2 V with beta=1 and alpha=kappa^-1; kappa≥1; actual allpoint/allvector curvature kappa^-1*norma^2≤D2V[a,a]≤norma^2; source0<eta≤1 retained.
  • Actual source UNNORMALIZED exp(-V_eta)=exp(-V)*Gaussian_eta, normalized Gibbs mu=volume.tilted(-V), unreflected R_y=mu.tilted(-norm(x-y)^2/(2eta)). Finite Hilbert/Borel including0 is disclosed representation extension.
  • No partition, covariance, moment, derivative or PI certificate on this source theorem. Actual probability, posterior vectorL2, C2, U=V_eta+logZV, both true Hessian bounds and global Lipschitz are produced internally. No joint measurable posterior kernel selector, higher derivative, numerical kernel, cost or main claim.

Mathematical proof

1. Construct the actual source smoothing

Positive source curvature gives the true partition and probability. The accepted convolution producer gives C2 V_eta and the literal normalized-U constant shift, with no input normalizer.

\[e^{-V_\eta}=e^{-V}*\gamma_\eta,\quad U=V_\eta+\log Z_V.\]
Corresponding Lean step

SmoothedGibbsPotential.smoothed_gibbs_potential

2. Produce true posterior moments and derivative identity

The Gaussian convolution producer gives R_y probability and vectorL2 for every actualy, and true Hessian of U. The produced constant shift identifies both Hessians.

\[D^2V_\eta(y)[a,a]=\|a\|^2/\eta-\operatorname{Cov}_{R_y}(a,a)/\eta^2.\]
Corresponding Lean step

GaussianConvolutionRegularity.gaussian_convolution_derivatives; fderiv_add_const

3. Keep the unreflected quadratic law

Set W_y=V+norm(x-y)^2/(2eta). Derive its C2 Hessian shift and both positive curvature bounds. True strong convexity gives its exponential integrability/positive partition; tilted_tilted proves literal R_y equality.

\[(\kappa^{-1}+\eta^{-1})I\preceq D^2W_y\preceq(1+\eta^{-1})I,\quad R_y=Z_y^{-1}e^{-W_y}dx.\]
Corresponding Lean step

HasFDerivAt.norm_sq; tilted_tilted; StrongConvexGibbsIntegrability.integrable_exp_neg_of_strongConvexOn

4. Apply the canonical covariance producer

Transport the internally produced posterior vectorL2 through the actual law equality, then apply the new Poincare-derived covariance theorem. This suffices for the source isotropic bound; full anisotropic BL remains open.

\[\operatorname{Cov}_{R_y}(a,a)\le\|a\|^2/(\kappa^{-1}+\eta^{-1}).\]
Corresponding Lean step

GibbsLinearCovarianceUpper.gibbs_linear_covariance_upper

5. Derive the exact lower Hessian constant

Subtract the covariance upper bound in the true identity. kappa/eta and both sum denominators are positive, so algebra preserves inequality and yields the exact source lower constant.

\[\frac{\|a\|^2}{\eta}-\frac{\|a\|^2}{\eta^2(\kappa^{-1}+\eta^{-1})}=\frac{\|a\|^2}{\kappa+\eta}.\]
Corresponding Lean step

div_le_div_of_nonneg_right; sub_le_sub_left; field_simp

6. Reuse the actual reverse-Cramer-Rao half

The independently checked actual posterior covariance lower and source smoothed Hessian upper theorem is specialized to beta1. No duplicated abstract Hessian field or assumed upper bound.

\[D^2V_\eta(y)[a,a]\le\|a\|^2/(1+\eta).\]
Corresponding Lean step

SmoothedHessianUpper.smoothed_hessian_upper

7. Prove true global gradient Lipschitz

The produced C2 potential has nonnegative Hessian and upper quadratic bound bynorma^2. Existing Riesz/selfadjoint Rayleigh norm and global mean-value producer yields1-Lipschitz gradient with zero extra regularization. The source eta cap remains an explicit premise.

\[0\preceq D^2V_\eta\preceq I\Longrightarrow\operatorname{Lip}(\nabla V_\eta)\le1.\]
Corresponding Lean step

QuadraticRegularization.strongConvexOn_and_lipschitzWith_gradient_add_quadratic

Lean verification

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

Lean proof · smoothed_hessian_bounds

Construct the actual source smoothing; Produce true posterior moments and derivative identity; Keep the unreflected quadratic law; Apply the canonical covariance producer; Derive the exact lower Hessian constant; Reuse the actual reverse-Cramer-Rao half; Prove true global gradient Lipschitz

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 smoothed_hessian_bounds
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [CompleteSpace E]
    {V : E → ℝ} {κ η : ℝ}
    (hκ : 1 ≤ κ) (hV : ContDiff ℝ 2 V)
    (hH : ∀ x a : E, κ⁻¹*‖a‖^2 ≤ fderiv ℝ (fderiv ℝ V) x a a ∧
      fderiv ℝ (fderiv ℝ V) x a a ≤ ‖a‖^2)
    (hη : 0 < η) (hη1 : η ≤ 1) :
    let μ := (volume : Measure E).tilted (fun x => -V x)
    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 => -Real.log (A y)
    let R := fun y : E => μ.tilted (fun x => -‖x-y‖^2/(2*η))
    IsProbabilityMeasure μ ∧ ContDiff ℝ 2 Vη ∧
      (∀ y, IsProbabilityMeasure (R y) ∧ MemLp id 2 (R y) ∧
        (∀ a, ProbabilityTheory.covarianceBilin (R y) a a ≤ ‖a‖^2/(κ⁻¹+η⁻¹)) ∧
        ∀ a, (1/(κ+η))*‖a‖^2 ≤ fderiv ℝ (fderiv ℝ Vη) y a a ∧
          fderiv ℝ (fderiv ℝ Vη) y a a ≤ (1/(1+η))*‖a‖^2) ∧
      LipschitzWith (1 : ℝ≥0) (gradient Vη) := by
  have hk : 0<κ := lt_of_lt_of_le zero_lt_one hκ
  have ha : 0<κ⁻¹ := inv_pos.mpr hk
  let α : ℝ≥0 := ⟨κ⁻¹,ha.le⟩
  have hα : 0<α := ha
  have hα1 : α≤1 := (inv_le_one₀ hk).2 hκ
  have hHV : ∀ x a : E, (α:ℝ)*‖a‖^2 ≤ fderiv ℝ (fderiv ℝ V) x a a ∧
      fderiv ℝ (fderiv ℝ V) x a a ≤ ((1:ℝ≥0):ℝ)*‖a‖^2 := by
    intro x a
    change κ⁻¹*‖a‖^2 ≤ fderiv ℝ (fderiv ℝ V) x a a ∧
      fderiv ℝ (fderiv ℝ V) x a a ≤ 1*‖a‖^2
    simpa only [one_mul] using hH x a
  let μ := (volume : Measure E).tilted (fun x => -V x)
  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 => -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,_hI,_hInt,_hTilt,_hA,hC2,hshift⟩ :=
    SmoothedGibbsPotential.smoothed_gibbs_potential ha hV (fun x a => (hH x a).1) hη
  have : IsProbabilityMeasure μ := hμ
  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
    ha (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 ≤ (1+η⁻¹)*‖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 ≤ (1+η⁻¹)*‖a‖^2
      rw [real_inner_self_eq_norm_sq]
      constructor <;> nlinarith [(hH x a).1,(hH x a).2]
    have hm : 0<κ⁻¹+η⁻¹ := add_pos ha (inv_pos.mpr hη)
    have hmM : κ⁻¹+η⁻¹≤1+η⁻¹ := by
      simpa only [add_comm] using (add_le_add_right ((inv_le_one₀ hk).2 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) (κ⁻¹+η⁻¹) (1+η⁻¹) 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
  have hlower (y a : E) : (1/(κ+η))*‖a‖^2 ≤ fderiv ℝ (fderiv ℝ Vη) y a a := by
    rw [hDD y a a,real_inner_self_eq_norm_sq]
    have hm : 0<κ⁻¹+η⁻¹ := add_pos ha (inv_pos.mpr hη)
    have hke : 0<κ+η := add_pos hk hη
    calc
      (1/(κ+η))*‖a‖^2 = ‖a‖^2/η-(‖a‖^2/(κ⁻¹+η⁻¹))/η^2 := by
        field_simp [hk.ne',hη.ne',hm.ne',hke.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 ≤ (1/(1+η))*‖a‖^2 := by
    have hu := (SmoothedHessianUpper.smoothed_hessian_upper hα hα1 hV hHV hη).2
    simpa only [NNReal.coe_one,one_mul] using hu
  have hHVη : ∀ y a : E, ((0:ℝ≥0):ℝ)*‖a‖^2 ≤ fderiv ℝ (fderiv ℝ Vη) y a a ∧
      fderiv ℝ (fderiv ℝ Vη) y a a ≤ ((1:ℝ≥0):ℝ)*‖a‖^2 := by
    intro y a
    have hp : 0≤(1/(κ+η))*‖a‖^2 := by positivity
    have hu : 1/(1+η)≤1 := by
      apply (div_le_iff₀ (by positivity : 0<1+η)).2
      linarith
    simpa only [NNReal.coe_zero,zero_mul,NNReal.coe_one,one_mul] using
      And.intro (hp.trans (hlower y a)) ((hupper y a).trans (mul_le_mul_of_nonneg_right hu (sq_nonneg ‖a‖)))
  have hLip := (AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticRegularization.strongConvexOn_and_lipschitzWith_gradient_add_quadratic
    (m:=0) (L:=1) (r:=0) hC2 hHVη (0:E)).2
  simp only [NNReal.coe_zero,zero_div,zero_mul,add_zero] at hLip
  exact ⟨hμ,hC2,fun y => ⟨(hRm y).1,(hRm y).2,hcov y,fun a => ⟨hlower y a,hupper y a⟩⟩,hLip⟩

end
end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.SmoothedHessianBounds

Exact module and namespace context

Source assumptions versus formal assumptions

SourceActual LeanDifference kindWhy it matters
Isotropic covariance estimate invoked through Brascamp-Lieb; source standing curvature beta1/alpha=kappa^-1.Source C2 V with beta=1 and alpha=kappa^-1; kappa>=1; actual allpoint/allvector curvature kappa^-1*norma^2<=D2V[a,a]<=norma^2; source0<eta<=1 retained. Actual source UNNORMALIZED exp(-V_eta)=exp(-V)*Gaussian_eta, normalized Gibbs mu=volume.tilted(-V), unreflected R_y=mu.tilted(-norm(x-y)^2/(2eta)). Finite Hilbert/Borel including0 is disclosed representation extension. No partition, covariance, moment, derivative or PI certificate on this source theorem. Actual probability, posterior vectorL2, C2, U=V_eta+logZV, both true Hessian bounds and global Lipschitz are produced internally. No joint measurable posterior kernel selector, higher derivative, numerical kernel, cost or main claim.source-implicitCanonical B explicitly includes actual vectorL2 and BOTH curvature, not full anisotropic BL. Source A has no added proof premise and produces genuine moments/normalizers internally.
Printed covariance upper invocation and reverse-Cramer-Rao lower yield both Hessian bounds.For the actual source Gaussian-smoothed unnormalized potential and true RGO posterior, produce probability and vectorL2, covariance upper norma^2/(kappa^-1+eta^-1), C2 regularity and (kappa+eta)^-1*norma^2<=D2V_eta(y)[a,a]<=(1+eta)^-1*norma^2, and true1-Lipschitz gradient. This is the analytic Lemma4.1, not an algorithm/main theorem.source-implicitPoincare-derived isotropic covariance route is a sufficient authored OR-route; it does not certify full BL or external book theorem.
Higher regularity, algorithms and both main/cost composition.Canonical BOTH-curvature Gibbs linear covariance upper with genuine vectorL2, actual positive partition and probability normalization; not full anisotropic Brascamp-Lieb. Actual source beta=1 alpha=kappa^-1, 1<=kappa, 0<eta<=1; genuine posterior law R_y, internally produced probability/vectorL2/positive partitions/C2 and normalized-U versus unnormalized-V_eta constant shift. Derive true covariance upper and both Hessian bounds (kappa+eta)^-1 and (1+eta)^-1, then true 1-Lipschitz gradient. Finite real Hilbert/Borel including zero dimension is disclosed representation extension. No input covariance/PI/oracle/moment/normalizer certificate on source Anchor. No joint measurable posterior kernel selector, higher smoothing derivatives, algorithm/Wp/proxy-warmness/main/querycost/composition. PBPS reflected quarter law and source-score remain separate. TV never transfers unbounded expected cost.unresolvedOnly actual analytic Lemma4.1 and its canonical covariance prerequisite are covered.

Canonical BOTH-curvature Gibbs linear covariance upper with genuine vectorL2, actual positive partition and probability normalization; not full anisotropic Brascamp-Lieb. Actual source beta=1 alpha=kappa^-1, 1<=kappa, 0<eta<=1; genuine posterior law R_y, internally produced probability/vectorL2/positive partitions/C2 and normalized-U versus unnormalized-V_eta constant shift. Derive true covariance upper and both Hessian bounds (kappa+eta)^-1 and (1+eta)^-1, then true 1-Lipschitz gradient. Finite real Hilbert/Borel including zero dimension is disclosed representation extension. No input covariance/PI/oracle/moment/normalizer certificate on source Anchor. No joint measurable posterior kernel selector, higher smoothing derivatives, algorithm/Wp/proxy-warmness/main/querycost/composition. PBPS reflected quarter law and source-score remain separate. TV never transfers unbounded expected 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
  • Canonical BOTH-curvature Gibbs linear covariance upper with genuine vectorL2, actual positive partition and probability normalization; not full anisotropic Brascamp-Lieb. Actual source beta=1 alpha=kappa^-1, 1≤kappa, 0<eta≤1; genuine posterior law R_y, internally produced probability/vectorL2/positive partitions/C2 and normalized-U versus unnormalized-V_eta constant shift. Derive true covariance upper and both Hessian bounds (kappa+eta)^-1 and (1+eta)^-1, then true 1-Lipschitz gradient. Finite real Hilbert/Borel including zero dimension is disclosed representation extension. No input covariance/PI/oracle/moment/normalizer certificate on source Anchor. No joint measurable posterior kernel selector, higher smoothing derivatives, algorithm/Wp/proxy-warmness/main/querycost/composition. PBPS reflected quarter law and source-score remain separate. TV never transfers unbounded expected cost.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

  • tilted_tilted
  • integral_exp_pos
  • HasFDerivAt.norm_sq
  • fderiv_add_const
  • div_le_div_of_nonneg_right
  • sub_le_sub_left
  • field_simp

Mathematical sources

  • SPHMC actual Lemma4.1 and explicit covariance prerequisite — Canonical BOTH-curvature Gibbs linear covariance upper with genuine vectorL2, actual positive partition and probability normalization; not full anisotropic Brascamp-Lieb. Actual source beta=1 alpha=kappa^-1, 1<=kappa, 0<eta<=1; genuine posterior law R_y, internally produced probability/vectorL2/positive partitions/C2 and normalized-U versus unnormalized-V_eta constant shift. Derive true covariance upper and both Hessian bounds (kappa+eta)^-1 and (1+eta)^-1, then true 1-Lipschitz gradient. Finite real Hilbert/Borel including zero dimension is disclosed representation extension. No input covariance/PI/oracle/moment/normalizer certificate on source Anchor. No joint measurable posterior kernel selector, higher smoothing derivatives, algorithm/Wp/proxy-warmness/main/querycost/composition. PBPS reflected quarter law and source-score remain separate. TV never transfers unbounded expected 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.

Which proof obligations and prerequisites are covered?

  • Formalized proof edge; source adapter/review separate Actual Lemma4.1 analytic bounds
  • TODO — not closed by these contributions Full anisotropic BL remaining
  • TODO — not closed by these contributions Both main results and actual-input expectedcost composition remaining