Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0

Identify the source Gaussian law with its literal precision density

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.

arXiv:2610.20492v1 · Eq4, Appendix B.2.2 density p_O of N(0,A_O^-1), and Eq26 regularity. Standard SPD Gaussian density background is expanded explicitly. · faithful paraphrase

Complete source statement (Samplinglib restatement)

For every natural n>=3, real kappa>=4 and every member O of the full real orthogonal group, let A_O=((kappa+1)/2)I-((kappa-1)/4)(O+O transpose). The actual canonical centered multivariate Gaussian with covariance A_O inverse equals canonical Euclidean volume with density sqrt(det A_O)/(2pi)^(n/2) exp(-x^T A_O x/2), using real n/2. Positive definiteness is proved from the existing exact lower quadratic bound; it is not an extra premise supplied by the caller. Both determinant signs are allowed.

  • n>=3 and kappa>=4, exactly the standing source range.
  • Every member of full real O(n), with both determinant signs.
  • No caller SPD, inverse, density, Jacobian or normalization premise. Existing source regularity supplies strict SPD internally.

Exact actual Gaussian density

\[A_O=\frac{\kappa+1}{2}I-\frac{\kappa-1}{4}(O+O^\top),\quad \mathcal N(0,A_O^{-1})(dx)=\frac{\sqrt{\det A_O}}{(2\pi)^{n/2}}e^{-x^\top A_Ox/2}\,dx\]

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

Identify the source Gaussian law with its literal precision density

AutoSamplingTheory.ExampleCases.GaussianComplexity.GaussianLawDensity.gaussian_law_eq_density · theorem · Teaching coverage

Read this first

Mathematical statement

For every natural n≥3, real kappa≥4 and every member O of the full real orthogonal group, let A_O=((kappa+1)/2)I-((kappa-1)/4)(O+O transpose). The actual canonical centered multivariate Gaussian with covariance A_O inverse equals canonical Euclidean volume with density sqrt(det A_O)/(2pi)^(n/2) exp(-x^T A_O x/2), using real n/2. Positive definiteness is proved from the existing exact lower quadratic bound; it is not an extra premise supplied by the caller. Both determinant signs are allowed.

\[A_O=\frac{\kappa+1}{2}I-\frac{\kappa-1}{4}(O+O^\top),\quad \mathcal N(0,A_O^{-1})(dx)=\frac{\sqrt{\det A_O}}{(2\pi)^{n/2}}e^{-x^\top A_Ox/2}\,dx\]
Lean statement · gaussian_law_eq_density

For every natural n>=3, real kappa>=4 and every member O of the full real orthogonal group, let A_O=((kappa+1)/2)I-((kappa-1)/4)(O+O transpose). The actual canonical centered multivariate Gaussian with covariance A_O inverse equals canonical Euclidean volume with density sqrt(det A_O)/(2pi)^(n/2) exp(-x^T A_O x/2), using real n/2. Positive definiteness is proved from the existing exact lower quadratic bound; it is not an extra premise supplied by the caller. Both determinant signs are allowed.

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 gaussian_law_eq_density {n : ℕ} (hn : 3 ≤ n) {κ : ℝ}
    (hκ : 4 ≤ κ) (O : Matrix.orthogonalGroup (Fin n) ℝ) :
    ProbabilityTheory.multivariateGaussian (0 : EuclideanSpace ℝ (Fin n))
        (singleBlockPrecision κ O)⁻¹ =
      (volume : Measure (EuclideanSpace ℝ (Fin n))).withDensity (fun x =>
        ENNReal.ofReal (Real.sqrt (singleBlockPrecision κ O).det /
          (2 * Real.pi) ^ ((n : ℝ) / 2) *
            Real.exp (-((WithLp.ofLp x) ⬝ᵥ
              (singleBlockPrecision κ O *ᵥ WithLp.ofLp x)) / 2)))

Exact module and namespace context

Proof roadmap

  1. 1Reuse the exact source precision lower bound

    The existing source regularity theorem gives Hermitian A_O and v transpose A_O v at least v transpose v for every real coordinate vector. These hold under the unchanged n≥3 and kappa≥4 bounds on all of full O(n).

  2. 2Produce strict positive definiteness internally

    A nonzero coordinate vector determines a nonzero actual Euclidean vector. Its squared Euclidean norm is positive and equals v transpose v. The existing lower bound is therefore strictly positive for every nonzero v, proving A_O.PosDef.

  3. 3Consume the identical canonical precision-density theorem

    Apply the new shared SPD Gaussian precision-density node to this same A_O and the internally proved SPD witness. This identifies the existing actual Gaussian covariance law with the exact literal p_O used by the analytic kernel and Fubini packets. Target-mixture and TV interpretations still require their own adapters.

Full assumptions and notation

All objects and hypotheses

  • n≥3 and kappa≥4, exactly the standing source range.
  • Every member of full real O(n), with both determinant signs.
  • No caller SPD, inverse, density, Jacobian or normalization premise. Existing source regularity supplies strict SPD internally.

Mathematical proof

1. Reuse the exact source precision lower bound

The existing source regularity theorem gives Hermitian A_O and v transpose A_O v at least v transpose v for every real coordinate vector. These hold under the unchanged n≥3 and kappa≥4 bounds on all of full O(n).

\[A_O^\top=A_O,\qquad v^\top A_Ov\geq v^\top v\]
Corresponding Lean step

hr is exactly singleBlockPrecision_regular hn hκ O, for the unchanged singleBlockPrecision definition. No determinant-sign restriction is added.

2. Produce strict positive definiteness internally

A nonzero coordinate vector determines a nonzero actual Euclidean vector. Its squared Euclidean norm is positive and equals v transpose v. The existing lower bound is therefore strictly positive for every nonzero v, proving A_O.PosDef.

\[v\ne0\Longrightarrow0<\|v\|_2^2=v^\top v\leq v^\top A_Ov\Longrightarrow A_O\succ0\]
Corresponding Lean step

hA uses Matrix.posDef_iff_dotProduct_mulVec. WithLp.toLp is used for the genuine Euclidean vector; EuclideanSpace.real_norm_sq_eq converts its squared norm to the coordinate dot product. SPD is an internal proof, not a public binder.

3. Consume the identical canonical precision-density theorem

Apply the new shared SPD Gaussian precision-density node to this same A_O and the internally proved SPD witness. This identifies the existing actual Gaussian covariance law with the exact literal p_O used by the analytic kernel and Fubini packets. Target-mixture and TV interpretations still require their own adapters.

\[\mathcal N(0,A_O^{-1})(dx)=p_O(x)\,dx\]
Corresponding Lean step

The final exact call is multivariateGaussian_eq_withDensity_of_posDef _ hA. The generic Jacobian/Gaussian proof is shared rather than copied into the source route.

Lean verification

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

Lean proof · gaussian_law_eq_density

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

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 gaussian_law_eq_density {n : ℕ} (hn : 3 ≤ n) {κ : ℝ}
    (hκ : 4 ≤ κ) (O : Matrix.orthogonalGroup (Fin n) ℝ) :
    ProbabilityTheory.multivariateGaussian (0 : EuclideanSpace ℝ (Fin n))
        (singleBlockPrecision κ O)⁻¹ =
      (volume : Measure (EuclideanSpace ℝ (Fin n))).withDensity (fun x =>
        ENNReal.ofReal (Real.sqrt (singleBlockPrecision κ O).det /
          (2 * Real.pi) ^ ((n : ℝ) / 2) *
            Real.exp (-((WithLp.ofLp x) ⬝ᵥ
              (singleBlockPrecision κ O *ᵥ WithLp.ofLp x)) / 2))) := by
  have hr := singleBlockPrecision_regular hn hκ O
  have hA : (singleBlockPrecision κ O).PosDef := by
    apply Matrix.posDef_iff_dotProduct_mulVec.mpr
    refine ⟨hr.1, ?_⟩
    intro v hv
    have hvE : (WithLp.toLp 2 v : EuclideanSpace ℝ (Fin n)) ≠ 0 := by
      intro h
      exact hv (congrArg WithLp.ofLp h)
    have hp := sq_pos_of_pos (norm_pos_iff.mpr hvE)
    rw [EuclideanSpace.real_norm_sq_eq] at hp
    have hdot : 0 < v ⬝ᵥ v := by simpa only [dotProduct, pow_two] using hp
    simpa only [star_trivial] using lt_of_lt_of_le hdot (hr.2 v).1
  exact multivariateGaussian_eq_withDensity_of_posDef _ hA

end AutoSamplingTheory.ExampleCases.GaussianComplexity.GaussianLawDensity

Exact module and namespace context

Source assumptions versus formal assumptions

SourceActual LeanDifference kindWhy it matters
Standing n>=3,kappa>=4, full O(n) and the Eq4 precision.Same standing range and actual precision; strict SPD proved internally from exact lower bound, not added as a premise.sameThe same source Gaussian and exact density on actual Euclidean volume.

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

Detected semantic differences

  • conclusion: The anonymous reconstruction expands equality of measures, nonnegative square root and ENNReal embedding; the source uses conventional Gaussian density notation. — Positive definiteness derived internally makes det and normalizer strictly positive. ENNReal.ofReal encodes the same positive real density and canonical volume.withDensity encodes p_O(x) dx; no change of mathematical conclusion.
  • assumptions: The decoder states the same hypotheses without narrating the internal proof of SPD. — Public signature has no PosDef binder. Whole proof obtains hA from exact regularity lower bound using true Euclidean norm positivity, then applies the shared canonical theorem. This is proof elaboration, not a lost hypothesis or strengthened assumption.

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

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

Which proof obligations and prerequisites are covered?

  • TODO — not closed by these contributions Actual canonical Gaussian equals exact Euclidean-volume density