Exact volume density of the actual Gaussian with SPD precision

Huanjian Zhou and Taiji Suzuki, On Complexity of Gaussian Sampling; the generic SPD identity is standard Gaussian background, not a new all-matrices theorem attributed to the paper.

Complete source statement (Samplinglib restatement)

For every natural n, including zero, and every real symmetric positive-definite n by n precision matrix A, the actual canonical centered multivariate Gaussian with covariance A inverse equals canonical Euclidean volume with density sqrt(det A)/(2pi)^(n/2) exp(-x^T A x/2). The exponent n/2 is real division. Coordinates are WithLp.ofLp of the genuine Euclidean vector. No density, Jacobian, inverse, square-root or normalization fact is assumed beyond A.PosDef. This is a standard background generalization used by the source density assertion.

Exact actual Gaussian density

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

Exact volume density of the actual Gaussian with SPD precision

AutoSamplingTheory.TechnicalLemmas.Measure.GaussianPrecisionDensity.multivariateGaussian_eq_withDensity_of_posDef · theorem · Teaching coverage

Read this first

Mathematical statement

\[\mathcal N(0,A^{-1})(dx)=\frac{\sqrt{\det A}}{(2\pi)^{n/2}}e^{-x^\top Ax/2}\,dx\qquad(A\succ0,\ n\in\mathbb N)\]

Lean statement · multivariateGaussian_eq_withDensity_of_posDef

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 multivariateGaussian_eq_withDensity_of_posDef {n : ℕ}
    (A : Matrix (Fin n) (Fin n) ℝ) (hA : A.PosDef) :
    ProbabilityTheory.multivariateGaussian (0 : EuclideanSpace ℝ (Fin n)) A⁻¹ =
      (volume : Measure (EuclideanSpace ℝ (Fin n))).withDensity (fun x =>
        ENNReal.ofReal (Real.sqrt A.det / (2 * Real.pi) ^ ((n : ℝ) / 2) *
          Real.exp (-((WithLp.ofLp x) ⬝ᵥ (A *ᵥ WithLp.ofLp x)) / 2)))

Exact module and namespace context

Proof roadmap

1Take the actual covariance square root
Set B to the canonical positive-semidefinite square root of A inverse. SPD gives positive determinant of A inverse. Its square root has positive determinant, B squared equals A inverse, and the inverse square satisfies B inverse times B inverse equals A.
2Build the reversible Euclidean change of variables
The private linear-equivalence provider turns the invertible matrix B into an actual real Euclidean linear equivalence e. Its action and inverse action have exactly the matrix coordinate formulas; its linear determinant equals det B. The canonical volume Jacobian is therefore the inverse absolute determinant.
3Reuse the same standard Gaussian density
Instantiate the existing canonical isotropic Gaussian density theorem at variance one. This identifies the actual stdGaussian with the standard Euclidean volume density, including the zero-dimensional singleton.
4Identify the true Euclidean quadratic form
The inverse square root is symmetric. Expand the actual Euclidean squared norm as the sum of coordinate squares and use transpose/matrix multiplication to obtain x transpose A x. The coordinate map is used only for coordinates; no isometry to a default Pi sup norm is asserted.
5Compute the exact dimension and determinant factors
Positive definiteness makes all square-root and real-power conversions legitimate. The inverse determinant factor is sqrt(det A), and the standard Gaussian coefficient is precisely (2pi) to the real power minus n/2. Dimension zero is retained.
6Transport the actual density measure
Use the existing measurable-equivalence withDensity transport theorem and the actual volume Jacobian. This produces the product of the Jacobian factor and standard density evaluated at e inverse x, as an equality of measures.
7Identify the existing Gaussian constructor
The existing multivariateGaussian zero A inverse is defined as the pushforward of stdGaussian by this same canonical covariance square root. The explicit matrix action agrees with e. Substitute the quadratic, determinant and dimension identities into the transported density.

Full assumptions and notation

All objects and hypotheses

Every natural dimension n, including n=0.
A is a real SPD precision matrix: this is the legitimate domain of the standard background theorem.
Existing canonical multivariateGaussian and stdGaussian, actual Euclidean volume, true Euclidean norm, nonnegative square root and real dimension-half powers.

Mathematical proof

1. Take the actual covariance square root

Set B to the canonical positive-semidefinite square root of A inverse. SPD gives positive determinant of A inverse. Its square root has positive determinant, B squared equals A inverse, and the inverse square satisfies B inverse times B inverse equals A.

\[B=(A^{-1})^{1/2},\quad B^2=A^{-1},\quad \det B=\sqrt{\det(A^{-1})}>0\]

Corresponding Lean step

hAi, hBd, hBpos, hBpsd, hBsq and hBinvsq use actual PosDef.inv, CFC square root, determinant square-root and nonsingular matrix inverse APIs.

2. Build the reversible Euclidean change of variables

The private linear-equivalence provider turns the invertible matrix B into an actual real Euclidean linear equivalence e. Its action and inverse action have exactly the matrix coordinate formulas; its linear determinant equals det B. The canonical volume Jacobian is therefore the inverse absolute determinant.

\[e(z)=Bz,\quad e^{-1}(x)=B^{-1}x,\quad e_*dx=|\det B|^{-1}dx\]

Corresponding Lean step

exists_matrix_linearEquiv proves both inverse laws by nonsingular inverse multiplication and the determinant using the canonical orthonormal basis. hmap uses the actual map_linearMap_addHaar_eq_smul_addHaar on Euclidean volume.

3. Reuse the same standard Gaussian density

Instantiate the existing canonical isotropic Gaussian density theorem at variance one. This identifies the actual stdGaussian with the standard Euclidean volume density, including the zero-dimensional singleton.

\[\gamma_n(dz)=(\sqrt{2\pi})^{-n}e^{-\|z\|_2^2/2}\,dz\]

Corresponding Lean step

hstd calls exactly map_sqrt_smul_stdGaussian_eq_withDensity at eta=1 and simplifies the identity pushforward. No new Gaussian measure is defined.

4. Identify the true Euclidean quadratic form

The inverse square root is symmetric. Expand the actual Euclidean squared norm as the sum of coordinate squares and use transpose/matrix multiplication to obtain x transpose A x. The coordinate map is used only for coordinates; no isometry to a default Pi sup norm is asserted.

\[\|B^{-1}x\|_2^2=x^\top(B^{-1})^\top B^{-1}x=x^\top Ax\]

Corresponding Lean step

hBts uses real Hermitian symmetry. hnorm explicitly uses EuclideanSpace.real_norm_sq_eq and coordinate dotProduct, then hei, dotProduct_transpose_mulVec and hBinvsq.

5. Compute the exact dimension and determinant factors

Positive definiteness makes all square-root and real-power conversions legitimate. The inverse determinant factor is sqrt(det A), and the standard Gaussian coefficient is precisely (2pi) to the real power minus n/2. Dimension zero is retained.

\[|(\det B)^{-1}|=\sqrt{\det A},\qquad(\sqrt{2\pi})^{-n}=\frac1{(2\pi)^{n/2}}\]

Corresponding Lean step

hdetfactor uses det_nonsing_inv, sqrt_inv and positivity. hnormalizer uses positive-base real-power multiplication with (n:R)/2, rather than natural division.

6. Transport the actual density measure

Use the existing measurable-equivalence withDensity transport theorem and the actual volume Jacobian. This produces the product of the Jacobian factor and standard density evaluated at e inverse x, as an equality of measures.

\[e_*\gamma_n=dx\,\bigl[|\det B|^{-1}(\sqrt{2\pi})^{-n}e^{-\|B^{-1}x\|_2^2/2}\bigr]\]

Corresponding Lean step

The main proof calls exactly measurableEquiv_map_withDensity em volume, then hmap and the actual withDensity scalar-transport identities. The nonnegative real factors are combined using ENNReal.ofReal_mul.

7. Identify the existing Gaussian constructor

The existing multivariateGaussian zero A inverse is defined as the pushforward of stdGaussian by this same canonical covariance square root. The explicit matrix action agrees with e. Substitute the quadratic, determinant and dimension identities into the transported density.

\[\mathcal N(0,A^{-1})=B_*\gamma_n=dx\,\frac{\sqrt{\det A}}{(2\pi)^{n/2}}e^{-x^\top Ax/2}\]

Corresponding Lean step

hem proves the actual CFC matrix action equals em. The proof unfolds the existing multivariateGaussian constructor, then uses hstd, transport and withDensity_congr_ae. It never introduces a replacement Gaussian constructor.

Lean verification

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

Lean proof · multivariateGaussian_eq_withDensity_of_posDef

Actual canonical constructor, matrix and measure transport; exact proof is folded below.

Download module (.lean)

theorem multivariateGaussian_eq_withDensity_of_posDef {n : ℕ}
    (A : Matrix (Fin n) (Fin n) ℝ) (hA : A.PosDef) :
    ProbabilityTheory.multivariateGaussian (0 : EuclideanSpace ℝ (Fin n)) A⁻¹ =
      (volume : Measure (EuclideanSpace ℝ (Fin n))).withDensity (fun x =>
        ENNReal.ofReal (Real.sqrt A.det / (2 * Real.pi) ^ ((n : ℝ) / 2) *
          Real.exp (-((WithLp.ofLp x) ⬝ᵥ (A *ᵥ WithLp.ofLp x)) / 2))) := by
  classical
  let B : Matrix (Fin n) (Fin n) ℝ := CFC.sqrt A⁻¹
  have hAi : A⁻¹.PosDef := hA.inv
  have hBd : B.det = Real.sqrt A⁻¹.det := by
    simpa only [B, RCLike.sqrt_of_nonneg hAi.posSemidef.det_nonneg, RCLike.re_to_real,
      RCLike.ofReal_real_eq_id, id_eq] using
      hAi.posSemidef.det_sqrt
  have hBpos : 0 < B.det := by rw [hBd]; exact Real.sqrt_pos.2 hAi.det_pos
  have hBpsd : B.PosSemidef := (CFC.sqrt_nonneg A⁻¹).posSemidef
  have hBsq : B * B = A⁻¹ := CFC.sqrt_mul_sqrt_self A⁻¹ hAi.posSemidef.nonneg
  have hBinvsq : B⁻¹ * B⁻¹ = A := by
    rw [← Matrix.mul_inv_rev, hBsq,
      Matrix.nonsing_inv_nonsing_inv _ (isUnit_iff_ne_zero.mpr hA.det_pos.ne')]
  have hBts : (B⁻¹).transpose = B⁻¹ := by
    rw [Matrix.transpose_nonsing_inv,
      (Matrix.isHermitian_iff_isSymm.mp hBpsd.isHermitian)]
  obtain ⟨e, he, hei, hedet⟩ := exists_matrix_linearEquiv B hBpos.ne'
  let em : EuclideanSpace ℝ (Fin n) ≃ᵐ EuclideanSpace ℝ (Fin n) :=
    e.toContinuousLinearEquiv.toHomeomorph.toMeasurableEquiv
  have hnorm (x : EuclideanSpace ℝ (Fin n)) :
      ‖em.symm x‖ ^ 2 = (WithLp.ofLp x) ⬝ᵥ (A *ᵥ WithLp.ofLp x) := by
    calc
      _ = (WithLp.ofLp (e.symm x)) ⬝ᵥ (WithLp.ofLp (e.symm x)) := by
        rw [EuclideanSpace.real_norm_sq_eq]
        simp only [dotProduct, pow_two]
        rfl
      _ = _ := by
        rw [hei, dotProduct_comm, ← Matrix.dotProduct_transpose_mulVec,
          hBts, Matrix.mulVec_mulVec, hBinvsq]
  have hdetfactor : |(B.det)⁻¹| = Real.sqrt A.det := by
    rw [hBd, Matrix.det_nonsing_inv, Ring.inverse_eq_inv, Real.sqrt_inv, inv_inv,
      abs_of_nonneg (Real.sqrt_nonneg _)]
  have hmap : (volume : Measure (EuclideanSpace ℝ (Fin n))).map em =
      ENNReal.ofReal |(B.det)⁻¹| • volume := by
    change (volume : Measure (EuclideanSpace ℝ (Fin n))).map e.toLinearMap = _
    simpa only [hedet] using
      (Measure.map_linearMap_addHaar_eq_smul_addHaar (volume : Measure (EuclideanSpace ℝ (Fin n)))
        (f := e.toLinearMap) (by rw [hedet]; exact hBpos.ne'))
  have hstd : stdGaussian (EuclideanSpace ℝ (Fin n)) =
      (volume : Measure (EuclideanSpace ℝ (Fin n))).withDensity (fun x =>
        ENNReal.ofReal (((Real.sqrt (2 * Real.pi))⁻¹) ^ n * Real.exp (-‖x‖ ^ 2 / 2))) := by
    simpa only [Real.sqrt_one, one_smul, Measure.map_id', mul_one,
      finrank_euclideanSpace, Fintype.card_fin] using
      (map_sqrt_smul_stdGaussian_eq_withDensity (E := EuclideanSpace ℝ (Fin n))
        (1 : ℝ) zero_lt_one)
  have hnormalizer : ((Real.sqrt (2 * Real.pi))⁻¹) ^ n =
      1 / (2 * Real.pi) ^ ((n : ℝ) / 2) := by
    rw [inv_pow, ← Real.rpow_natCast, Real.sqrt_eq_rpow,
      ← Real.rpow_mul (by positivity : 0 ≤ 2 * Real.pi)]
    simp only [show (2 : ℝ)⁻¹ * (n : ℝ) = (n : ℝ) / 2 by ring, one_div]
  have hem : (fun x : EuclideanSpace ℝ (Fin n) => Matrix.toEuclideanCLM (𝕜 := ℝ) B x) =
      (em : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) := by
    funext x
    apply WithLp.ofLp_injective
    exact (he x).symm
  rw [multivariateGaussian]
  simp only [zero_add]
  change (stdGaussian (EuclideanSpace ℝ (Fin n))).map (fun x => Matrix.toEuclideanCLM (𝕜 := ℝ) B x) = _
  rw [hem]
  rw [hstd, measurableEquiv_map_withDensity em volume (by fun_prop), hmap,
    withDensity_smul_measure, ← withDensity_smul _ (by fun_prop)]
  apply withDensity_congr_ae
  exact Filter.Eventually.of_forall fun x => by
    change ENNReal.ofReal |(B.det)⁻¹| *
      ENNReal.ofReal (((Real.sqrt (2 * Real.pi))⁻¹) ^ n *
        Real.exp (-‖em.symm x‖ ^ 2 / 2)) = _
    rw [← ENNReal.ofReal_mul (abs_nonneg _), hdetfactor, hnorm, hnormalizer]
    congr 1
    ring

end AutoSamplingTheory.TechnicalLemmas.Measure.GaussianPrecisionDensity

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
Standard nondegenerate Gaussian density used implicitly in Appendix B.2.2.	Every natural n and any real SPD precision, including dimension zero, for the existing actual constructor.	generalization	A canonical reusable background generalization, explicitly distinguished from the source-specific assertion. Its immediate actual consumer is the determinant-family adapter; the fixed-spectrum route is only a planned second consumer.

Exact actual Gaussian-law/volume-density identification only. Target-mixture construction and its relation to H and TV, sphere/Poisson, parameter choice, amplification/transcript, fixed-spectrum hidden-eigenbasis and both main lower bounds remain open. No determinant-sign lower bound is transported to the eigenbasis route.

Encoder–denoiser: accepted · equivalent-after-elaboration

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

Exact actual Gaussian-law/volume-density identification only. Target-mixture construction and its relation to H and TV, sphere/Poisson, parameter choice, amplification/transcript, fixed-spectrum hidden-eigenbasis and both main lower bounds remain open. No determinant-sign lower bound is transported to the eigenbasis route.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

ProbabilityTheory.multivariateGaussian
CFC.sqrt_mul_sqrt_self
Matrix.PosSemidef.det_sqrt
Matrix.PosDef.inv
MeasureTheory.Measure.map_linearMap_addHaar_eq_smul_addHaar
EuclideanSpace.real_norm_sq_eq

Mathematical sources

Standard Gaussian background and source density — Standard SPD Gaussian density background, generalized to all natural n; not an all-matrices theorem stated by the paper.

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

Exact volume density of the actual Gaussian with SPD precision

Complete source statement (Samplinglib restatement)

Exact actual Gaussian density

Read the formalized proofs

Exact volume density of the actual Gaussian with SPD precision

Mathematical statement

Proof roadmap

All objects and hypotheses

Mathematical proof

1. Take the actual covariance square root

2. Build the reversible Euclidean change of variables

3. Reuse the same standard Gaussian density

4. Identify the true Euclidean quadratic form

5. Compute the exact dimension and determinant factors

6. Transport the actual density measure

7. Identify the existing Gaussian constructor

Lean verification

Source assumptions versus formal assumptions

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Mathematical sources

Which proof obligations and prerequisites are covered?