The actual normalized Gibbs augmentation law

Fan Chen, Sinho Chewi, Jianfeng Lu and Matthew S. Zhang. ASTIS mathematical restatement with explicit normalization details, not copied prose or author endorsement.

Complete source statement (Samplinglib restatement)

In the paper's Euclidean C² setting αI≤D²V≤βI with 0<α≤β and 0<η≤1/β, the target μ has normalized density Z_V^{-1}exp(-V). The joint density proportional to exp(-V(x)-||x-y||²/(2η)) is the law of X~μ and Y=X+sqrt(η)N for independent standard Gaussian N. Its exact normalizing factor is (2πη)^(-d/2)/Z_V. ASTIS makes finite positive Gibbs mass and probability of this law explicit.

(2.6)-(2.7), explicit normalizer

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

From a genuine Hessian bound to the normalized augmented Gibbs law

AutoSamplingTheory.ExampleCases.ProximalBPS.GibbsAugmentation.normalized_augmentation_density · theorem · Teaching coverage

Read this first

Mathematical statement

Let E be a finite-dimensional real inner-product space with its Borel sigma algebra and canonical volume. Let V:E→R be twice continuously differentiable, with D²V(x)[v,v]≥α||v||² for every x,v and some α>0. For any η>0, the Gibbs integral Z_V is strictly positive; independently drawing X from volume tilted by -V and standard Gaussian N, then setting Y=X+sqrt(η)N, gives a probability joint law. This joint law has the following exact density with respect to product volume. No minimizer, integrability, normalizer, or probability-law identity is supplied as a hypothesis.

\[Z_V=\int_E e^{-V(x)}\,dx>0,\quad C_\eta=((\sqrt{2\pi\eta})^{-1})^d,\quad \mu(dx)=Z_V^{-1}e^{-V(x)}dx,\quad \mathcal L(X,X+\sqrt\eta N)(dx,dy)=\frac{C_\eta}{Z_V}\exp\!\left(-V(x)-\frac{\|y-x\|^2}{2\eta}\right)dx\,dy.\]

Lean statement · normalized_augmentation_density

The statement's let bindings merely name Z_V, μ and the generative joint measure; they add no hypotheses. IsProbabilityMeasure is a proposition-valued typeclass and appears explicitly in the conclusion. withDensity expects an ENNReal-valued density, so ENNReal.ofReal wraps the nonnegative real formula. Module.finrank is the natural dimension. The conclusion is equality of whole measures, not equality only of total masses or a chosen conditional representative.

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 normalized_augmentation_density {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 joint := Measure.map (fun p : E × E => (p.1, p.1 + Real.sqrt η • p.2))
      (μ.prod (stdGaussian E))
    0 < ZV ∧ IsProbabilityMeasure joint ∧
      joint = ((volume : Measure E).prod volume).withDensity (fun p =>
        ENNReal.ofReal
          (((((Real.sqrt (2 * Real.pi * η))⁻¹) ^ Module.finrank ℝ E) / ZV) *
            Real.exp (-V p.1 - ‖p.2 - p.1‖ ^ 2 / (2 * η))))

Exact module and namespace context

Proof roadmap

1Establish the Gibbs probability from curvature
The existing Hessian criterion converts the genuine C² lower bound into strong convexity with the same α. The existing minimizer-free Gibbs integrability theorem then proves exp(-V) is integrable. Its proof already supplies the quadratic tail bound by the first-order estimate at zero and Young's inequality. Since the exponential is strictly positive and volume is nonzero, Z_V>0. Mathlib can therefore normalize it into a probability measure.
2Use the generative Gaussian joint law
The augmentation map Φη(x,n)=(x,x+sqrt(η)n) is continuous and hence measurable. Its pushforward of the independent product of two probability laws is a probability. The already proved Gaussian augmentation theorem identifies its density qη(y-x), initially relative to μ(dx)dy; it includes the exact Gaussian normalization.
3Change the reference measure to product volume
Insert μ(dx)=f(x)dx with f(x)=exp(-V(x))/Z_V. Continuity of V explicitly gives measurability of f; the Gaussian weight is also measurable. The product-density identity moves f to the first coordinate, then density multiplication combines the two weights. No new interchange assumption or conditional probability representative is supplied here: the invoked Mathlib product-density theorem handles its product integration contract, with canonical volume providing the required SFinite instance.
4Combine the exponents and retain nonvacuous normalization
The real factors are nonnegative, so converting their product to an ENNReal density preserves multiplication. The exponential addition rule gives the displayed source density. The theorem returns its measure equality together with Z_V>0 and probability of the joint law: equality alone would not exclude a zero totalized tilt. The focused test transfers both probability and the existing auxiliary reflection identity to this source-density measure.

Full assumptions and notation

All objects and hypotheses

All quantifiers are global: V is C² on E and the genuine second Fréchet derivative lower bound holds for every position x and direction v. Positive α is essential to this normalization route. C² prevents unsupported uses of totalized fderiv.
E has finite real dimension d, including zero. Its measure is the canonical inner-product-space volume; an arbitrary Haar normalization is not silently substituted.
η>0. The source's upper Hessian bound βI and upper scale restriction η≤1/β are unnecessary for this law identity, though they remain assumptions of downstream sampler statements.
Independence is the product μ.prod(stdGaussian E). The normalized target μ is defined using Mathlib tilted; the theorem proves the positive integral and probability conclusions that exclude its zero totalized fallback.

Mathematical proof

1. Establish the Gibbs probability from curvature

The existing Hessian criterion converts the genuine C² lower bound into strong convexity with the same α. The existing minimizer-free Gibbs integrability theorem then proves exp(-V) is integrable. Its proof already supplies the quadratic tail bound by the first-order estimate at zero and Young's inequality. Since the exponential is strictly positive and volume is nonzero, Z_V>0. Mathlib can therefore normalize it into a probability measure.

\[D^2V\succeq\alpha I\ \Longrightarrow\ V\text{ strongly convex}\ \Longrightarrow\ e^{-V}\in L^1(dx),\qquad 0<Z_V<\infty,\quad \mu(E)=1.\]

Corresponding Lean step

HessianStrongConvexity.strongConvexOn_univ_of_fderiv2_lower and StrongConvexGibbsIntegrability.integrable_exp_neg_of_strongConvexOn are existing ASTIS proofs. ContDiff.differentiable supplies genuine differentiability. integral_exp_pos gives hZ; isProbabilityMeasure_tilted installs the actual probability instance. No parent proof is duplicated.

2. Use the generative Gaussian joint law

The augmentation map Φη(x,n)=(x,x+sqrt(η)n) is continuous and hence measurable. Its pushforward of the independent product of two probability laws is a probability. The already proved Gaussian augmentation theorem identifies its density qη(y-x), initially relative to μ(dx)dy; it includes the exact Gaussian normalization.

\[\pi_\eta=(\Phi_\eta)_\#(\mu\otimes\gamma_E),\quad \pi_\eta(E\times E)=1,\quad \pi_\eta(dx,dy)=\mu(dx)q_\eta(y-x)dy,\quad q_\eta(w)=C_\eta e^{-\|w\|^2/(2\eta)}.\]

Corresponding Lean step

The measurable-map witness hΦ is proved by fun_prop. Measure.isProbabilityMeasure_map proves the probability conclusion. GaussianAugmentation.augmentation_eq_withDensity is the third actual ASTIS parent and supplies the joint density, not an assumed law equality.

3. Change the reference measure to product volume

Insert μ(dx)=f(x)dx with f(x)=exp(-V(x))/Z_V. Continuity of V explicitly gives measurability of f; the Gaussian weight is also measurable. The product-density identity moves f to the first coordinate, then density multiplication combines the two weights. No new interchange assumption or conditional probability representative is supplied here: the invoked Mathlib product-density theorem handles its product integration contract, with canonical volume providing the required SFinite instance.

\[(\mu\otimes dx_y)q_\eta(y-x)=((dx_x\,dx_y)f(x))q_\eta(y-x)=(dx_x\,dx_y)[f(x)q_\eta(y-x)].\]

Corresponding Lean step

Unfolding only the existing Measure.tilted definition reveals withDensity(ofReal(exp(-V)/Z_V)). prod_withDensity_left uses hf; the reverse direction of withDensity_mul flattens the two weights, with hf.comp measurable_fst and hq as explicit measurable inputs. These are Mathlib calls, not new ASTIS wrappers.

4. Combine the exponents and retain nonvacuous normalization

The real factors are nonnegative, so converting their product to an ENNReal density preserves multiplication. The exponential addition rule gives the displayed source density. The theorem returns its measure equality together with Z_V>0 and probability of the joint law: equality alone would not exclude a zero totalized tilt. The focused test transfers both probability and the existing auxiliary reflection identity to this source-density measure.

\[\frac{e^{-V(x)}}{Z_V}C_\eta e^{-\|y-x\|^2/(2\eta)}=\frac{C_\eta}{Z_V}e^{-V(x)-\|y-x\|^2/(2\eta)}.\]

Corresponding Lean step

ENNReal.ofReal_mul uses exp positivity and hZ; Real.exp_add and ring perform the exact algebra. The conjunction returns hZ, the proved pushforward probability, and the exact density equality. Tests use all three conclusions and GaussianReflection.reflection_preserves_augmentation; this does not establish PBPS process invariance.

Lean verification

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

Lean proof · normalized_augmentation_density

One source-integration theorem joins three compiled ASTIS parents and existing Mathlib normalization/product-density APIs. Every auxiliary name f,q,Z_V,μ and every measurability/probability witness is local to the proof. The positive integral certifies meaningful normalization before any law identification. The formula uses ||y-x||, equal to the source's ||x-y||; the Gaussian variance is exactly η, not 2η.

Download module (.lean)

theorem normalized_augmentation_density {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 joint := Measure.map (fun p : E × E => (p.1, p.1 + Real.sqrt η • p.2))
      (μ.prod (stdGaussian E))
    0 < ZV ∧ IsProbabilityMeasure joint ∧
      joint = ((volume : Measure E).prod volume).withDensity (fun p =>
        ENNReal.ofReal
          (((((Real.sqrt (2 * Real.pi * η))⁻¹) ^ Module.finrank ℝ E) / ZV) *
            Real.exp (-V p.1 - ‖p.2 - p.1‖ ^ 2 / (2 * η)))) := by
  let ZV := ∫ x, Real.exp (-V x) ∂(volume : Measure E)
  let μ := (volume : Measure E).tilted (fun x => -V x)
  have hi : Integrable (fun x => Real.exp (-V x)) (volume : Measure E) :=
    TechnicalLemmas.Analysis.StrongConvexGibbsIntegrability.integrable_exp_neg_of_strongConvexOn
      hα (hV.differentiable (by norm_num))
      (TechnicalLemmas.Analysis.HessianStrongConvexity.strongConvexOn_univ_of_fderiv2_lower
        hV hH)
  have hZ : 0 < ZV := integral_exp_pos hi
  have : IsProbabilityMeasure μ := isProbabilityMeasure_tilted hi
  have hΦ : Measurable (fun p : E × E => (p.1, p.1 + Real.sqrt η • p.2)) := by
    fun_prop
  refine ⟨hZ, Measure.isProbabilityMeasure_map hΦ.aemeasurable, ?_⟩
  change Measure.map _ (μ.prod (stdGaussian E)) = _
  rw [GaussianAugmentation.augmentation_eq_withDensity μ η hη]
  let f : E → ℝ≥0∞ := fun x => ENNReal.ofReal (Real.exp (-V x) / ZV)
  let q : E × E → ℝ≥0∞ := fun p => ENNReal.ofReal
    (((Real.sqrt (2 * Real.pi * η))⁻¹) ^ Module.finrank ℝ E *
      Real.exp (-‖p.2 - p.1‖ ^ 2 / (2 * η)))
  have hf : Measurable f := by
    exact ((Real.continuous_exp.comp hV.continuous.neg).div_const ZV).measurable.ennreal_ofReal
  have hq : Measurable q := by fun_prop
  have hfp : Measurable (fun p : E × E => f p.1) := hf.comp measurable_fst
  change (((volume : Measure E).withDensity f).prod volume).withDensity q = _
  rw [prod_withDensity_left hf, ← withDensity_mul _ hfp hq]
  congr 1
  funext p
  dsimp only [Pi.mul_apply, f, q]
  rw [← ENNReal.ofReal_mul (div_nonneg (Real.exp_pos _).le hZ.le)]
  congr 1
  rw [show -V p.1 - ‖p.2 - p.1‖ ^ 2 / (2 * η) =
      -V p.1 + (-‖p.2 - p.1‖ ^ 2 / (2 * η)) by ring, Real.exp_add]
  ring

end AutoSamplingTheory.ExampleCases.ProximalBPS.GibbsAugmentation

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
C² Euclidean V and lower matrix bound αI≤D²V, α>0	ContDiff ℝ 2 V, hα:0<α, and ∀x v, α*\|\|v\|\|²≤(fderiv ℝ (fderiv ℝ V) x v) v	same	The quadratic-form version expresses the lower Hessian bound. C² guarantees genuine first and second derivatives; a zero totalized derivative without differentiability cannot replace this hypothesis.
Euclidean space and Lebesgue volume	Any finite-dimensional real inner-product Borel E, including dimension zero, with canonical volume	generalization	The shared analytic and Gaussian parents are coordinate-free and include zero dimension. The volume normalization is fixed by the inner product, not an arbitrary Haar measure.
Upper Hessian bound βI and 0<η≤1/β	No upper Hessian bound; η>0	generalization	Only lower curvature is used to normalize the Gibbs target. Gaussian augmentation and density multiplication hold at every positive scale. The omitted upper constraints are retained in separate sampler/curvature obligations.
Normalized Gibbs notation and joint-density proportionality	Explicit 0<Z_V and IsProbabilityMeasure joint as well as the exact density equality	source-implicit	Existing parent proofs establish exp(-V) integrability without a minimizer. Positive exponential mass excludes zero normalization; the explicit probability conclusion prevents the displayed equality from being satisfied only by a zero totalized tilted law.
Independent Gaussian construction (2.7)	Product measure and proved measurable pushforward, with measurable product-density multiplication	source-implicit	The Borel continuity witnesses and product measure contracts are supplied internally. No conditional representative, boundary integration or exchange of improper integrals is assumed.
Exponent -V(x)-\|\|x-y\|\|²/(2η), Gaussian covariance ηI	Exponent -V p.1-\|\|p.2-p.1\|\|²/(2η), prefactor ((sqrt(2πη))⁻¹)^finrank/Z_V	same	Norm symmetry changes x-y to y-x without changing the value; the natural-power square-root expression is exactly the same Gaussian normalization.

Exact normalized joint-law component (2.6)-(2.7), not conditional kernels, curvature conclusions, process invariance, mixing or query cost. Independent source-blind semantic audit is required for admission.

Encoder–denoiser: accepted · equivalent-after-elaboration

Detected semantic differences

domains: Finite-dimensional real inner-product Borel E, including dimension zero, is an explicit generalization of the paper's Euclidean presentation. — The source extraction, candidate assumptions, module documentation, lesson and anonymous reconstruction all disclose it. Canonical volume, rather than arbitrary Haar scaling, preserves the Gaussian constant. The full Fin 0 test passes.
assumptions: The formal identity omits the upper Hessian bound and upper scale restriction, so it applies to more inputs than the paper's standing regime. — The mathematical proof requires only C², the positive lower bound and eta>0. These broader assumptions are part of the selected source extraction and authored lesson; omitted upper controls are not silently removed from downstream sampler claims.
conclusion: Positive finite normalization, an explicit probability assertion and the exact density factor elaborate the paper's proportional joint-density notation. — The code derives genuine integrability and Z_V>0 before identifying the normalized density. Inserting f(x)=exp(-V(x))/Z_V into the proven Gaussian augmentation density changes the reference from mu×volume to volume×volume; this is the required source-law identification, not a remaining assumption.
scopes: The accepted result is the selected normalized-law proof edge only. Reflection is a tested consumer; conditionals, process invariance and sampler performance remain outside this theorem. — The production conclusion is exactly the triple, and the full lesson explicitly distinguishes its reflection test from PBPS process invariance. Adjacent source statements do not expand the declaration's formal credit.

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

This completes the normalized joint-law identification between the generative construction and the product-volume density, not the whole PBPS paper or Proposition 2.1.
The source upper Hessian bound and η≤1/β remain relevant elsewhere. Their absence here is a disclosed generalization, not a correction of the source sampler assumptions.
Conditional-law kernels and representatives, marginal curvature, process invariance, mixing, tail and moment estimates, and query cost remain separate obligations.
Compilation certifies this Lean proposition; independent source-blind reconstruction and source fidelity review remain distinct admission gates.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

MeasureTheory.integral_exp_pos
MeasureTheory.isProbabilityMeasure_tilted
MeasureTheory.Measure.isProbabilityMeasure_map
MeasureTheory.prod_withDensity_left
MeasureTheory.withDensity_mul
ENNReal.ofReal_mul
Real.exp_add
ContDiff.differentiable
ContDiff.continuous
Real.continuous_exp

Mathematical sources

Chen, Chewi, Lu and Zhang, PBPS v1 §2.2, equations (2.6)-(2.7) — Normalized joint-density and generative-law identification, with the positive Hessian setting in introduction (1.1). Original ASTIS exposition and explicit normalization argument, not copied paper prose.

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

The actual normalized Gibbs augmentation law

Complete source statement (Samplinglib restatement)

(2.6)-(2.7), explicit normalizer

Read the formalized proofs

From a genuine Hessian bound to the normalized augmented Gibbs law

Mathematical statement

Proof roadmap

All objects and hypotheses

Mathematical proof

1. Establish the Gibbs probability from curvature

2. Use the generative Gaussian joint law

3. Change the reference measure to product volume

4. Combine the exponents and retain nonvacuous normalization

Lean verification

Source assumptions versus formal assumptions

Detected semantic differences

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Mathematical sources

Which proof obligations and prerequisites are covered?