Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412

IsotropicGaussianDensity: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

  1. The explicit density of isotropic Gaussian noise
ASTIS mathematical exposition

The explicit density of isotropic Gaussian noise

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

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

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

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

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.

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

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.

Source and reuse

ASTIS 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

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