AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.SmoothedGibbsPotential

Samplinglib mathematical lesson

Actual source smoothed Gibbs potential and preserved partition

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.SmoothedGibbsPotential.smoothed_gibbs_potential · theorem · Teaching coverage

Read this first

Mathematical statement

The original Gibbs mass Z_V is strictly positive and mu is a probability measure. The actual Gaussian add-noise law equals volume.withDensity(ofReal(exp(-V_eta)/Z_V)). The source unnormalized weight A_eta is integrable with integral exactly Z_V, so this same law is volume.tilted(-V_eta). A_eta is positive everywhere, V_eta is globally C2, and at every y the normalized negative-log density U_eta(y)=V_eta(y)+log Z_V.

\[A_\eta(y)=C_\eta\!\int e^{-V(x)-\|y-x\|^2/(2\eta)}dx,\quad V_\eta=-\log A_\eta,\quad \int A_\eta\,dy=Z_V>0,\quad \pi_\eta=\frac{e^{-V_\eta}}{Z_V}dy,\quad V_\eta\in C^2,\quad U_\eta=V_\eta+\log Z_V.\]

Lean statement · smoothed_gibbs_potential

Actual source unnormalized Gaussian convolution positive/integrable, preserved original Gibbs partition, actual smoothed Gibbs law, C2 potential and exact normalized constant shift.

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_gibbs_potential {V : E → ℝ} {α η : ℝ} (hα : 0 < α) (hV : ContDiff ℝ 2 V)
    (hH : ∀ x v : E, α*‖v‖^2 ≤ fderiv ℝ (fderiv ℝ V) x v v) (hη : 0 < η) :
    let ZV := ∫ x, Real.exp (-V x) ∂(volume : Measure E)
    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)
    0 < ZV ∧ IsProbabilityMeasure μ ∧
      (μ.prod (stdGaussian E)).map (fun p => p.1+Real.sqrt η • p.2) =
        (volume : Measure E).withDensity
          (fun y => ENNReal.ofReal (Real.exp (-(-Real.log (A y)))/ZV)) ∧
      Integrable A (volume : Measure E) ∧
      (∫ y, A y ∂(volume : Measure E)) = ZV ∧
      (μ.prod (stdGaussian E)).map (fun p => p.1+Real.sqrt η • p.2) =
        (volume : Measure E).tilted (fun y => -(-Real.log (A y))) ∧
      (∀ y, 0 < A y) ∧
      ContDiff ℝ 2 (fun y => -Real.log (A y)) ∧
      ∀ y, -Real.log (C*∫ x, Real.exp (-‖y-x‖^2/(2*η)) ∂μ) =
        -Real.log (A y)+Real.log ZV

Exact module and namespace context

Proof roadmap

1Derive the original Gibbs probability
The genuine lower Hessian produces strong convexity of V; the existing Gibbs-integrability producer yields integrable exp(-V) without a minimizer premise. The positive exponential integral gives Z_V>0, and the exact exponential tilt is therefore a probability measure.
2Use the actual Gaussian density and regularity producer
Apply the independently admitted shared arbitrary-probability Gaussian result to this derived mu. It identifies the true pushforward law, gives positive density and C2 of the normalizer and normalized negative-log density. These facts concern the actual two independent variables x and standard Gaussian g.
3Connect the source unnormalized convolution exactly
The tilted Bochner-integral identity inserts the actual original Gibbs density. Exponential additivity and moving the fixed Z_V outside the integral yield C_eta Z_mu=A_eta/Z_V at every observation, with the exact Gaussian prefactor retained. Positivity of this density and Z_V gives A_eta>0 everywhere.
4Derive integrability and partition preservation from probability
The true smoothed pushforward is a probability measure. Evaluating its withDensity identification on the whole space gives lintegral ofReal(A_eta/Z_V)=1. Its continuous nonnegative density and this finite mass imply actual Bochner integrability, then ordinary integral(A_eta/Z_V)=1. Multiplication by positive Z_V gives integrability of A_eta and integral A_eta=Z_V.
5Identify the actual source Gibbs law
Everywhere positivity gives exp(-V_eta)=A_eta exactly. Insert the derived integral A_eta=Z_V into the definition of exponential tilt: the actual Gaussian-smoothed law is precisely volume.tilted(-V_eta), with no supplied Gibbs or normalizer witness.
6Preserve the source potential convention and derive C2
Real log_div at positive A_eta and Z_V gives the exact additive constant U_eta=V_eta+log Z_V. The shared theorem already proved C2 of U_eta; subtraction of the fixed log Z_V therefore proves C2 of the actual source V_eta. The potentials are not asserted literally equal. Neither this constant identity nor C2 proves the source score/covariance or Hessian inequalities.

Full assumptions and notation

All objects and hypotheses

E is a finite-dimensional real inner-product space equipped with its Borel measurable space, including dimension zero. V:E→R is globally C2. alpha>0, eta>0, and for every x,v, alpha norm(v)^2≤D2V(x)[v,v]. The source upper Hessian bound and eta upper cap are not required for this normalization/regularity adapter.
Z_V=integral exp(-V(x))dx, mu=volume.tilted(-V), C_eta=(sqrt(2*pi*eta))^(-dim E), A_eta(y)=C_eta integral exp(-V(x)-norm(y-x)^2/(2eta))dx, and the SOURCE potential is V_eta(y)=-log A_eta(y). These are actual functions and measures, not supplied normalized Gibbs certificates.
Original Gibbs integrability, positive Z_V, mu probability, actual Gaussian add-noise density, integrable A_eta and preserved partition are derived. The normalized probability-density potential is U_eta=-log(C_eta integral exp(-norm(y-x)^2/(2eta))dmu(x)); the exact identity U_eta=V_eta+log Z_V is a conclusion. No moments, minimizer, input law, conditional representative, smoothed regularity or smoothed Hessian certificate is passed.

Mathematical proof

1. Derive the original Gibbs probability

The genuine lower Hessian produces strong convexity of V; the existing Gibbs-integrability producer yields integrable exp(-V) without a minimizer premise. The positive exponential integral gives Z_V>0, and the exact exponential tilt is therefore a probability measure.

\[D^2V\succeq\alpha I,\ \alpha>0\ \Longrightarrow\ e^{-V}\in L^1(dx),\quad Z_V>0,\quad \mu(dx)=Z_V^{-1}e^{-V(x)}dx.\]

Corresponding Lean step

HessianStrongConvexity.strongConvexOn_univ_of_fderiv2_lower; StrongConvexGibbsIntegrability.integrable_exp_neg_of_strongConvexOn; integral_exp_pos; isProbabilityMeasure_tilted

2. Use the actual Gaussian density and regularity producer

Apply the independently admitted shared arbitrary-probability Gaussian result to this derived mu. It identifies the true pushforward law, gives positive density and C2 of the normalizer and normalized negative-log density. These facts concern the actual two independent variables x and standard Gaussian g.

\[\pi_\eta=(x+\sqrt\eta\,g)_\#(\mu\otimes\gamma)=C_\eta Z_\mu\,dy,\quad Z_\mu(y)=\int e^{-\|y-x\|^2/(2\eta)}\mu(dx).\]

Corresponding Lean step

GaussianConvolutionRegularity.gaussian_convolution_potential_c2; hc

3. Connect the source unnormalized convolution exactly

The tilted Bochner-integral identity inserts the actual original Gibbs density. Exponential additivity and moving the fixed Z_V outside the integral yield C_eta Z_mu=A_eta/Z_V at every observation, with the exact Gaussian prefactor retained. Positivity of this density and Z_V gives A_eta>0 everywhere.

\[C_\eta Z_\mu(y)=\frac{C_\eta}{Z_V}\int e^{-V(x)-\|y-x\|^2/(2\eta)}dx=\frac{A_\eta(y)}{Z_V}>0.\]

Corresponding Lean step

integral_tilted; Real.exp_add; integral_div; he; hA; hlaw

4. Derive integrability and partition preservation from probability

The true smoothed pushforward is a probability measure. Evaluating its withDensity identification on the whole space gives lintegral ofReal(A_eta/Z_V)=1. Its continuous nonnegative density and this finite mass imply actual Bochner integrability, then ordinary integral(A_eta/Z_V)=1. Multiplication by positive Z_V gives integrability of A_eta and integral A_eta=Z_V.

\[\int^{\!-}\!\operatorname{ofReal}(A_\eta/Z_V)\,dy=1\ \Longrightarrow\ A_\eta\in L^1(dy),\quad\int A_\eta\,dy=Z_V.\]

Corresponding Lean step

Measure.isProbabilityMeasure_map; withDensity_apply; lintegral_ofReal_ne_top_iff_integrable; ofReal_integral_eq_lintegral_ofReal; hiD; hIntD; hiA; hIntA

5. Identify the actual source Gibbs law

Everywhere positivity gives exp(-V_eta)=A_eta exactly. Insert the derived integral A_eta=Z_V into the definition of exponential tilt: the actual Gaussian-smoothed law is precisely volume.tilted(-V_eta), with no supplied Gibbs or normalizer witness.

\[e^{-V_\eta(y)}=A_\eta(y),\quad \pi_\eta(dy)=\frac{e^{-V_\eta(y)}}{\int e^{-V_\eta}}dy=\operatorname{tilt}_{dy}(-V_\eta).\]

Corresponding Lean step

Measure.tilted; Real.exp_log; hIntA; hTilt

6. Preserve the source potential convention and derive C2

Real log_div at positive A_eta and Z_V gives the exact additive constant U_eta=V_eta+log Z_V. The shared theorem already proved C2 of U_eta; subtraction of the fixed log Z_V therefore proves C2 of the actual source V_eta. The potentials are not asserted literally equal. Neither this constant identity nor C2 proves the source score/covariance or Hessian inequalities.

\[U_\eta=-\log(A_\eta/Z_V)=V_\eta+\log Z_V,\quad V_\eta=U_\eta-\log Z_V\in C^2.\]

Corresponding Lean step

Real.log_div; hv; ContDiff.sub; contDiff_const

Lean verification

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

Lean proof · smoothed_gibbs_potential

Genuine Hessian-to-Gibbs normalization, shared actual Gaussian law, exact tilted integral, true probability total mass, derived integrability/partition, source tilt and positive logarithm.

Download module (.lean)

theorem smoothed_gibbs_potential {V : E → ℝ} {α η : ℝ} (hα : 0 < α) (hV : ContDiff ℝ 2 V)
    (hH : ∀ x v : E, α*‖v‖^2 ≤ fderiv ℝ (fderiv ℝ V) x v v) (hη : 0 < η) :
    let ZV := ∫ x, Real.exp (-V x) ∂(volume : Measure E)
    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)
    0 < ZV ∧ IsProbabilityMeasure μ ∧
      (μ.prod (stdGaussian E)).map (fun p => p.1+Real.sqrt η • p.2) =
        (volume : Measure E).withDensity
          (fun y => ENNReal.ofReal (Real.exp (-(-Real.log (A y)))/ZV)) ∧
      Integrable A (volume : Measure E) ∧
      (∫ y, A y ∂(volume : Measure E)) = ZV ∧
      (μ.prod (stdGaussian E)).map (fun p => p.1+Real.sqrt η • p.2) =
        (volume : Measure E).tilted (fun y => -(-Real.log (A y))) ∧
      (∀ y, 0 < A y) ∧
      ContDiff ℝ 2 (fun y => -Real.log (A y)) ∧
      ∀ y, -Real.log (C*∫ x, Real.exp (-‖y-x‖^2/(2*η)) ∂μ) =
        -Real.log (A y)+Real.log ZV := by
  let ZV := ∫ x, Real.exp (-V x) ∂(volume : Measure E)
  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)
  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 hH)
  have hZ : 0 < ZV := integral_exp_pos hi
  have : IsProbabilityMeasure μ := isProbabilityMeasure_tilted hi
  have hc := AutoSamplingTheory.TechnicalLemmas.Measure.GaussianConvolutionRegularity.gaussian_convolution_potential_c2 μ hη
  have he (y : E) : C*∫ x, Real.exp (-‖y-x‖^2/(2*η)) ∂μ = A y/ZV := by
    rw [show μ = (volume : Measure E).tilted (fun x => -V x) from rfl,integral_tilted]
    dsimp only [A,ZV]
    rw [show (C*∫ x, Real.exp (-V x-‖y-x‖^2/(2*η)) ∂(volume : Measure E))/
        (∫ x, Real.exp (-V x) ∂(volume : Measure E)) =
      C*((∫ x, Real.exp (-V x-‖y-x‖^2/(2*η)) ∂(volume : Measure E))/
        (∫ x, Real.exp (-V x) ∂(volume : Measure E))) by ring]
    congr 1
    rw [← integral_div]
    apply integral_congr_ae
    filter_upwards with x
    rw [smul_eq_mul,show Real.exp (-V x-‖y-x‖^2/(2*η)) =
      Real.exp (-V x)*Real.exp (-‖y-x‖^2/(2*η)) by
        rw [show -V x-‖y-x‖^2/(2*η) = -V x+(-‖y-x‖^2/(2*η)) by ring,Real.exp_add]]
    ring
  have hA (y : E) : 0 < A y :=
    (div_pos_iff_of_pos_right hZ).mp (he y ▸ hc.2.1 y)
  have hv (y : E) : -Real.log (C*∫ x, Real.exp (-‖y-x‖^2/(2*η)) ∂μ) =
      -Real.log (A y)+Real.log ZV := by
    rw [he,Real.log_div (hA y).ne' hZ.ne']; ring
  have hlaw : (μ.prod (stdGaussian E)).map (fun p => p.1+Real.sqrt η • p.2) =
      (volume : Measure E).withDensity (fun y => ENNReal.ofReal (A y/ZV)) := by
    convert hc.1 using 1
    congr 1
    funext y
    exact congrArg ENNReal.ofReal (he y).symm
  have hDcont : Continuous (fun y => A y/ZV) := by
    have hefun : (fun y => A y/ZV) =
        (fun y => C*∫ x, Real.exp (-‖y-x‖^2/(2*η)) ∂μ) :=
      funext (fun y => (he y).symm)
    rw [hefun]
    exact continuous_const.mul hc.2.2.1.continuous
  have hnonneg : ∀ y, 0 ≤ A y/ZV := fun y => (div_pos (hA y) hZ).le
  have : IsProbabilityMeasure ((μ.prod (stdGaussian E)).map
      (fun p => p.1+Real.sqrt η • p.2)) := Measure.isProbabilityMeasure_map (by fun_prop)
  have hm : ∫⁻ y, ENNReal.ofReal (A y/ZV) ∂(volume : Measure E) = 1 := by
    have hm := (congrArg (fun m : Measure E => m Set.univ) hlaw).symm
    simpa only [withDensity_apply _ MeasurableSet.univ,setLIntegral_univ,
      measure_univ] using hm
  have hiD : Integrable (fun y => A y/ZV) (volume : Measure E) :=
    (lintegral_ofReal_ne_top_iff_integrable hDcont.aestronglyMeasurable
      (Filter.Eventually.of_forall hnonneg)).mp (by rw [hm]; exact ENNReal.one_ne_top)
  have hIntD : (∫ y, A y/ZV ∂(volume : Measure E)) = 1 := by
    have hp := ofReal_integral_eq_lintegral_ofReal hiD (Filter.Eventually.of_forall hnonneg)
    rw [hm] at hp
    have ht := congrArg ENNReal.toReal hp
    simpa only [ENNReal.toReal_ofReal (integral_nonneg hnonneg),ENNReal.toReal_one] using ht
  have hiA : Integrable A (volume : Measure E) := by
    convert hiD.mul_const ZV using 1
    funext y
    exact (div_mul_cancel₀ (A y) hZ.ne').symm
  have hIntA : (∫ y, A y ∂(volume : Measure E)) = ZV := by
    rw [integral_div] at hIntD
    simpa only [one_mul] using (div_eq_iff hZ.ne').mp hIntD
  have hTilt : (μ.prod (stdGaussian E)).map (fun p => p.1+Real.sqrt η • p.2) =
      (volume : Measure E).tilted (fun y => -(-Real.log (A y))) := by
    rw [Measure.tilted]
    simp_rw [neg_neg,Real.exp_log (hA _)]
    rw [hIntA]
    exact hlaw
  refine ⟨hZ,inferInstance,?_,hiA,hIntA,hTilt,hA,?_,hv⟩
  · change (μ.prod (stdGaussian E)).map (fun p => p.1+Real.sqrt η • p.2) =
      (volume : Measure E).withDensity (fun y => ENNReal.ofReal (Real.exp (-(-Real.log (A y)))/ZV))
    convert hlaw using 1
    congr 1
    funext y
    rw [neg_neg,Real.exp_log (hA y)]
  have hg : (fun y => -Real.log (A y)) =
      (fun y => -Real.log (C*∫ x, Real.exp (-‖y-x‖^2/(2*η)) ∂μ)-Real.log ZV) := by
    funext y; rw [hv]; ring
  rw [hg]
  exact hc.2.2.2.sub contDiff_const

end
end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.SmoothedGibbsPotential

Exact module and namespace context

Scope and omitted-condition boundaries

Actual source unnormalized smoothed potential V_eta, positive finite partition Z_V preserved by smoothing, genuine original and smoothed Gibbs probability laws, normalized U_eta=V_eta+log Z_V and source V_eta C2. No posterior score/covariance, curvature/higher derivative inequalities, exact-flow stationarity, numerical accuracy/stochastic errors/history/work, PBPS process or either complete main/composition. TV never transfers unbounded expected cost.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

integral_exp_pos
isProbabilityMeasure_tilted
integral_tilted
Real.exp_add
Measure.isProbabilityMeasure_map
withDensity_apply
lintegral_ofReal_ne_top_iff_integrable
ofReal_integral_eq_lintegral_ofReal
integral_div
Real.exp_log
Measure.tilted
Real.log_div
ContDiff.sub

Mathematical sources

SPHMC source smoothing definition and Gibbs normalization — Actual source unnormalized smoothed potential V_eta, positive finite partition Z_V preserved by smoothing, genuine original and smoothed Gibbs probability laws, normalized U_eta=V_eta+log Z_V and source V_eta C2. No posterior score/covariance, curvature/higher derivative inequalities, exact-flow stationarity, numerical accuracy/stochastic errors/history/work, PBPS process or either complete main/composition. 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.

SmoothedGibbsPotential: mathematical reading route

Actual source smoothed Gibbs potential and preserved partition

Mathematical statement

Proof roadmap

All objects and hypotheses

Mathematical proof

1. Derive the original Gibbs probability

2. Use the actual Gaussian density and regularity producer

3. Connect the source unnormalized convolution exactly

4. Derive integrability and partition preservation from probability

5. Identify the actual source Gibbs law

6. Preserve the source potential convention and derive C2

Lean verification

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Mathematical sources