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.