Gaussian-noise density prerequisite for the proximal augmentation

Fan Chen, Sinho Chewi, Jianfeng Lu and Matthew S. Zhang. ASTIS mathematical expansion of the standard Gaussian-noise prerequisite, not copied paper prose or a claim of complete joint-law formalization.

Complete source statement (Samplinglib restatement)

For eta>0 and Z a standard Gaussian vector in R^d, sqrt(eta) Z has density (sqrt(2*pi*eta))^{-d} exp(-||z||^2/(2*eta)) with respect to Euclidean volume. This is the Gaussian-noise density used when passing from the independent construction (2.7) to the joint density (2.6).

isotropic-noise density prerequisite of (2.6)-(2.7)

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

The explicit density of isotropic Gaussian noise

AutoSamplingTheory.TechnicalLemmas.Measure.IsotropicGaussianDensity.map_sqrt_smul_stdGaussian_eq_withDensity · theorem · Teaching coverage

Read this first

Mathematical statement

Let E be a finite-dimensional real inner-product space, equipped with its Borel sigma algebra and its canonical volume measure, and let eta be a positive real number. If Z has the standard Gaussian law on E, the entire law of sqrt(eta) Z equals canonical volume weighted by the density q_eta below. The dimension d is the real dimension of E and may be zero.

\[(z\mapsto\sqrt\eta\,z)_\#\gamma_E=\mathrm{vol}_E\,q_\eta,\qquad q_\eta(z)=\left((\sqrt{2\pi\eta})^{-1}\right)^d\exp\!\left(-\frac{\|z\|^2}{2\eta}\right),\quad d=\dim_{\mathbb R}E.\]

Lean statement · map_sqrt_smul_stdGaussian_eq_withDensity

Measure.map denotes pushforward, stdGaussian is Mathlib's basis-independent standard Gaussian measure, and withDensity takes an ENNReal-valued density. ENNReal.ofReal converts the displayed nonnegative real Gaussian density. Module.finrank is a natural number, so the constant uses a natural power of an inverse square root rather than a real-power notation. The canonical volume instance is inferred from the finite-dimensional inner-product Borel setting; no arbitrary MeasureSpace E is added as a parameter.

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 map_sqrt_smul_stdGaussian_eq_withDensity (η : ℝ) (hη : 0 < η) :
    (stdGaussian E).map (fun z : E => Real.sqrt η • z) =
      (volume : Measure E).withDensity (fun z =>
        ENNReal.ofReal
          (((Real.sqrt (2 * Real.pi * η))⁻¹) ^ Module.finrank ℝ E *
            Real.exp (-‖z‖ ^ 2 / (2 * η))))

Exact module and namespace context

Proof roadmap

1Choose orthonormal coordinates
Choose an orthonormal basis indexed by Fin d. The measurable equivalence e sends a coordinate tuple to its orthonormal linear combination. The standard Gaussian on E is the pushforward under e of independent standard real Gaussians. Scalar multiplication commutes with e.
2Scale each scalar Gaussian
The scalar Gaussian pushforward theorem multiplies variance by the square of the scale. Since eta is positive, (sqrt eta)^2=eta. The finite-product map theorem then identifies the scaled coordinate law with independent variance-eta real Gaussians.
3Combine actual scalar densities
Every variance-eta scalar Gaussian is Lebesgue measure weighted by its known density. The existing ASTIS finite-product density theorem combines these into the product density. Its sigma-finiteness requirements hold because the individual density measures equal probability measures.
4Transport volume and its density
The coordinate equivalence preserves canonical volume: passing between ordinary coordinate tuples and EuclideanSpace preserves volume, as does the orthonormal representation inverse. The existing ASTIS measurable-equivalence density theorem therefore transports the product density by composing it with e inverse.
5Collect the normalizer and quadratic exponent
There are exactly d equal scalar normalizing factors. Products of exponentials add the exponents, and orthonormal coordinates preserve the squared norm. These identities give the stated density pointwise, not only almost everywhere. Empty products and sums also prove the dimension-zero case.

Full assumptions and notation

All objects and hypotheses

E is a normed additive commutative group carrying a real inner product, is finite-dimensional over the reals, and has the Borel measurable structure. The theorem uses Mathlib's canonical inner-product-space volume, not an arbitrary supplied Haar-measure normalization.
eta is a real number with eta>0. This makes the coordinate variance nonzero. In positive dimension eta=0 would give a singular Dirac law, not this Lebesgue density.
No Nontrivial E or positive-dimension assumption is imposed. In dimension zero, the empty product normalizer is one, every vector has norm zero, and canonical volume is the point mass on the unique vector.
No target potential, log-concavity, curvature bound, upper step-size restriction, input distribution, or additional integrability assumption is used. This is a reusable Gaussian-noise dependency, not the full PBPS augmentation identity.

Mathematical proof

1. Choose orthonormal coordinates

Choose an orthonormal basis indexed by Fin d. The measurable equivalence e sends a coordinate tuple to its orthonormal linear combination. The standard Gaussian on E is the pushforward under e of independent standard real Gaussians. Scalar multiplication commutes with e.

\[e(a)=\sum_{i=1}^d a_i b_i,\qquad\gamma_E=e_\#\bigotimes_{i=1}^d\mathcal N(0,1),\qquad\sqrt\eta\,e(a)=e(\sqrt\eta\,a).\]

Corresponding Lean step

The proof uses stdGaussian_eq_map_pi_orthonormalBasis, the measurable equivalence composed from MeasurableEquiv.toLp and the basis representation inverse, and the linear map's scalar-multiplication law. All finite-product and composition maps are shown measurable.

2. Scale each scalar Gaussian

The scalar Gaussian pushforward theorem multiplies variance by the square of the scale. Since eta is positive, (sqrt eta)^2=eta. The finite-product map theorem then identifies the scaled coordinate law with independent variance-eta real Gaussians.

\[(t\mapsto\sqrt\eta\,t)_\#\mathcal N(0,1)=\mathcal N(0,\eta),\qquad(\sqrt\eta\,\cdot)_\#\gamma_E=e_\#\bigotimes_{i=1}^d\mathcal N(0,\eta).\]

Corresponding Lean step

ProbabilityTheory.gaussianReal_map_const_mul and Real.sq_sqrt supply the scalar law. MeasureTheory.Measure.pi_map_pi, followed by Measure.map_map, proves the vector law. The nonnegative variance is explicitly eta with its proved nonnegativity witness.

3. Combine actual scalar densities

Every variance-eta scalar Gaussian is Lebesgue measure weighted by its known density. The existing ASTIS finite-product density theorem combines these into the product density. Its sigma-finiteness requirements hold because the individual density measures equal probability measures.

\[\bigotimes_{i=1}^d\mathcal N(0,\eta)=\mathrm{vol}_{\mathbb R^d}\,\prod_{i=1}^d\left[(\sqrt{2\pi\eta})^{-1}\exp\left(-\frac{a_i^2}{2\eta}\right)\right].\]

Corresponding Lean step

gaussianReal_of_var_ne_zero is applied after proving eta is nonzero. RadonNikodym.pi_withDensity_prod is used in reverse, with measurable Gaussian densities and probability instances obtained from the scalar Gaussian identity. No multidimensional density identity is assumed.

4. Transport volume and its density

The coordinate equivalence preserves canonical volume: passing between ordinary coordinate tuples and EuclideanSpace preserves volume, as does the orthonormal representation inverse. The existing ASTIS measurable-equivalence density theorem therefore transports the product density by composing it with e inverse.

\[e_\#\mathrm{vol}_{\mathbb R^d}=\mathrm{vol}_E,\qquad e_\#(\mathrm{vol}_{\mathbb R^d}f)=\mathrm{vol}_E(f\circ e^{-1}).\]

Corresponding Lean step

PiLp.volume_preserving_toLp and OrthonormalBasis.measurePreserving_repr_symm provide the volume identity. RadonNikodym.measurableEquiv_map_withDensity transports the actual product density. This avoids introducing a Jacobian theorem or an arbitrary volume-normalization assumption.

5. Collect the normalizer and quadratic exponent

There are exactly d equal scalar normalizing factors. Products of exponentials add the exponents, and orthonormal coordinates preserve the squared norm. These identities give the stated density pointwise, not only almost everywhere. Empty products and sums also prove the dimension-zero case.

\[\prod_i(\sqrt{2\pi\eta})^{-1}=((\sqrt{2\pi\eta})^{-1})^d,\qquad\sum_i(e^{-1}z)_i^2=\|z\|^2.\]

Corresponding Lean step

Finset.prod_mul_distrib, Finset.prod_const, Real.exp_sum, ENNReal.ofReal_prod_of_nonneg, EuclideanSpace.real_norm_sq_eq and preservation of the norm by the basis representation complete the equality. The real density is nonnegative before the finite-product ofReal conversion.

Lean verification

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

Lean proof · map_sqrt_smul_stdGaussian_eq_withDensity

All auxiliary names are local to this one proof. The proof identifies distributions through scalar Gaussian scaling, finite-product densities, and a volume-preserving measurable equivalence; it does not infer equality merely from matching total mass. No density normalizing integral or change-of-variables determinant is reproved. Eta positivity is used to obtain a nonzero scalar variance and its square-root square identity.

Download module (.lean)

theorem map_sqrt_smul_stdGaussian_eq_withDensity (η : ℝ) (hη : 0 < η) :
    (stdGaussian E).map (fun z : E => Real.sqrt η • z) =
      (volume : Measure E).withDensity (fun z =>
        ENNReal.ofReal
          (((Real.sqrt (2 * Real.pi * η))⁻¹) ^ Module.finrank ℝ E *
            Real.exp (-‖z‖ ^ 2 / (2 * η)))) := by
  classical
  let ι := Fin (Module.finrank ℝ E)
  let b := stdOrthonormalBasis ℝ E
  let v : ℝ≥0 := ⟨η, hη.le⟩
  have hvcoe : (v : ℝ) = η := rfl
  have hv : v ≠ 0 := by
    intro h
    have : η = 0 := congrArg (fun x : ℝ≥0 => (x : ℝ)) h
    exact hη.ne' this
  let e : (ι → ℝ) ≃ᵐ E :=
    (MeasurableEquiv.toLp 2 (ι → ℝ)).trans b.measurableEquiv.symm
  let T : (ι → ℝ) → (ι → ℝ) := fun x i => Real.sqrt η * x i
  have he (x : ι → ℝ) : e x = ∑ i, x i • b i := by
    exact (b.sum_repr_symm (WithLp.toLp 2 x)).symm
  have hstd : stdGaussian E =
      (Measure.pi (fun _ : ι => gaussianReal 0 1)).map e := by
    rw [stdGaussian_eq_map_pi_orthonormalBasis b]
    congr 1
    funext x
    exact (he x).symm
  have hcomm : (fun z : E => Real.sqrt η • z) ∘ e = e ∘ T := by
    funext x
    change Real.sqrt η • b.repr.symm (WithLp.toLp 2 x) =
      b.repr.symm (WithLp.toLp 2 (T x))
    rw [← map_smul]
    rfl
  have hscalar : (gaussianReal 0 1).map (fun t : ℝ => Real.sqrt η * t) =
      gaussianReal 0 v := by
    rw [gaussianReal_map_const_mul]
    congr 1
    · simp
    · apply NNReal.eq
      change (Real.sqrt η) ^ 2 * 1 = η
      rw [mul_one, Real.sq_sqrt hη.le]
  have hpi : (Measure.pi (fun _ : ι => gaussianReal 0 1)).map T =
      Measure.pi (fun _ : ι => gaussianReal 0 v) := by
    rw [Measure.pi_map_pi (fun _ => by fun_prop)]
    simp_rw [hscalar]
  have hscaled : (stdGaussian E).map (fun z : E => Real.sqrt η • z) =
      (Measure.pi (fun _ : ι => gaussianReal 0 v)).map e := by
    rw [hstd, Measure.map_map (by fun_prop) e.measurable, hcomm,
      ← Measure.map_map e.measurable (by fun_prop : Measurable T), hpi]
  have : IsProbabilityMeasure ((volume : Measure ℝ).withDensity (gaussianPDF 0 v)) := by
    rw [← gaussianReal_of_var_ne_zero 0 hv]
    infer_instance
  have hproduct : Measure.pi (fun _ : ι => gaussianReal 0 v) =
      (volume : Measure (ι → ℝ)).withDensity (fun x => ∏ i, gaussianPDF 0 v (x i)) := by
    rw [volume_pi, RadonNikodym.pi_withDensity_prod (fun _ => measurable_gaussianPDF 0 v)]
    simp_rw [← gaussianReal_of_var_ne_zero 0 hv]
  have hvol : (volume : Measure (ι → ℝ)).map e = (volume : Measure E) :=
    (b.measurePreserving_repr_symm.comp (PiLp.volume_preserving_toLp ι)).map_eq
  rw [hscaled, hproduct,
    RadonNikodym.measurableEquiv_map_withDensity e _ (by fun_prop), hvol]
  congr 1
  funext z
  have hnorm : (∑ i, ((e.symm z) i) ^ 2) = ‖z‖ ^ 2 := by
    rw [← EuclideanSpace.real_norm_sq_eq (WithLp.toLp 2 (e.symm z))]
    change ‖b.repr z‖ ^ 2 = ‖z‖ ^ 2
    rw [b.repr.norm_map]
  simp only [gaussianPDF_def, gaussianPDFReal, sub_zero]
  rw [← ENNReal.ofReal_prod_of_nonneg (fun _ _ => by positivity)]
  congr 1
  rw [Finset.prod_mul_distrib, Finset.prod_const, Finset.card_univ, ← Real.exp_sum]
  simp only [ι, Fintype.card_fin, hvcoe]
  congr 1
  congr 1
  rw [← Finset.sum_div, Finset.sum_neg_distrib, hnorm]

end AutoSamplingTheory.TechnicalLemmas.Measure.IsotropicGaussianDensity

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
A standard Gaussian vector in R^d with d>=1	stdGaussian E for any finite-dimensional real inner-product Borel space E, including dimension zero	generalization	Orthonormal coordinate transport proves the same law with canonical volume. Empty products and sums make the zero-dimensional case valid; a focused test reduces its density to one.
The sampler takes 0<eta<=1/beta	eta is real and eta>0	generalization	The noise law only uses positivity to ensure nonzero variance and (sqrt eta)^2=eta. The upper bound remains an assumption of other source results.
Euclidean Lebesgue volume and the Gaussian density normalizer	Canonical volume supplied by the finite-dimensional real inner-product Borel instance; inverse square-root constant to the natural power Module.finrank R E	same	Orthonormal bases preserve this precise volume normalization. ((sqrt(2pieta))^{-1})^d equals the conventional (2pieta)^{-d/2} for eta>0.
Implicit measurable coordinate maps and independent Gaussian coordinates	Measurable equivalences and finite-product pushforwards, with measurability proved and Gaussian probability instances supplying sigma-finiteness	source-implicit	The change-of-law and product-density theorems require these measure-theoretic contracts; they are established from the displayed objects rather than assumed as the desired density identity.
The full joint law uses the target potential V and the Gibbs normalizer	No input law or potential occurs in the selected Gaussian-noise density statement	same	This binding targets only the noise prerequisite, not the full density-generative identification. The source's Gibbs assumptions and joint adapter are neither removed from their own statement nor claimed proved here.

Only the isotropic-noise density prerequisite. No PBPS joint/conditional law, target normalizer, process invariance, convergence or oracle cost is formalized by this binding.

Encoder–denoiser: accepted · equivalent-after-elaboration

Detected semantic differences

domains: General finite-dimensional E and dimension zero are explicit extensions beyond the source's coordinate presentation. — The extraction and lesson acknowledge the extension; orthonormal transport and empty finite products justify it mathematically. It is not a source repair.
assumptions: The isolated noise law removes the sampler upper bound on eta and target-potential assumptions. — These conditions are unused in scalar Gaussian scaling or the density transport. The complete sampler claim is not asserted under the reduced hypotheses.
constant_dependencies: The Gaussian constant is explicit and tied to canonical inner-product volume. — The proof combines known scalar constants; the volume-preserving coordinate equivalence rules out an unspecified normalization factor.
scopes: The fresh lesson uses exact ASTIS declaration IDs without appended explanatory prose. — Both IDs resolve to the existing RadonNikodym declarations and match visible proof calls. Their mathematical roles are still explained in lesson steps 3 and 4. This correction changes no mathematical boundary.

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 proves only the explicit density of the scaled standard Gaussian law. The equality between the PBPS generative joint law (2.7) and joint density (2.6) still needs the shear/product-density adapter and the target's own density definition.
The paper assumes eta≤1/beta and d≥1. Those are not required for this Gaussian dependency, and the broader scope is explicit rather than a change to the full paper theorem.
No strong-convexity proof of target-normalizer finiteness, conditional-density representative, process invariance, PBPS convergence, or query complexity is asserted.
The PBPS and heat-smoothing consumers are planned dependencies, not claims that their downstream identities already compile. Independent source review and shared publication integration remain separate admission steps.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

ProbabilityTheory.stdGaussian_eq_map_pi_orthonormalBasis; gaussianReal_map_const_mul; gaussianReal_of_var_ne_zero; gaussianPDF_def; gaussianPDFReal.
MeasureTheory.Measure.pi_map_pi; Measure.map_map; MeasureTheory.volume_pi.
PiLp.volume_preserving_toLp; OrthonormalBasis.measurePreserving_repr_symm; OrthonormalBasis.sum_repr_symm.
EuclideanSpace.real_norm_sq_eq; LinearIsometryEquiv.norm_map; Real.sq_sqrt; Real.exp_sum; finite-product and finite-sum algebra.

Mathematical sources

Chen, Chewi, Lu and Zhang, Accelerated High-Accuracy Sampling from a Warm Start via the Proximal Bouncy Particle Sampler v1 — Gaussian-noise density dependency of equations (2.6)-(2.7), Section 2.2. Original ASTIS exposition; not a reproduction of paper prose or a claim to formalize the entire joint-law identity.

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

Gaussian-noise density prerequisite for the proximal augmentation

Complete source statement (Samplinglib restatement)

isotropic-noise density prerequisite of (2.6)-(2.7)

Read the formalized proofs

The explicit density of isotropic Gaussian noise

Mathematical statement

Proof roadmap

All objects and hypotheses

Mathematical proof

1. Choose orthonormal coordinates

2. Scale each scalar Gaussian

3. Combine actual scalar densities

4. Transport volume and its density

5. Collect the normalizer and quadratic exponent

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?