ASTIS mathematical exposition

From a genuine Hessian bound to the normalized augmented Gibbs law

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

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.\]

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 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.

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

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

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

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.

Source and reuse

ASTIS 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.

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