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

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

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

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 — Exact source determinant-family density assertion.

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