Gaussian integral for a positive-definite quadratic form

Given: Countable Choice, an integer $d\ge 1$, and a real symmetric positive-definite matrix $H\in M_d(\mathbb{R})$.

The Axiom of Countable Choice (${\mathrm{A}\mathrm{C}}_{\omega }$): every countable family of nonempty sets has a choice function.

The Euclidean inner product $⟨x,y⟩={\sum }_{k<n}{x}_k{y}_k$ on ${\mathbb{R}}^n$: the standard inner product is $⟨x,y⟩={\sum }_{j<d}{x}_j{y}_j$, with norm $\mathrm{\parallel }x{\mathrm{\parallel }}_2=\sqrt{⟨x,x⟩}$.

Self-adjoint and normal endomorphisms of a finite-dimensional real or complex inner product space defines self-adjointness by $T=T^{\ast }$, and In an orthonormal basis, self-adjoint means conjugate-transpose symmetry and normal means commuting with the conjugate transpose says a real symmetric matrix in an orthonormal basis represents a self-adjoint endomorphism.

Real spectral theorem: a self-adjoint endomorphism of a finite-dimensional real inner product space has an orthonormal eigenbasis: a self-adjoint endomorphism of a finite-dimensional real inner-product space has an orthonormal eigenbasis.

Hermitian positive-definite matrices and Cholesky factorisation A = LL* with positive diagonal defines real positive definiteness by symmetry and $v^{\mathsf{T}}Hv>0$ for every nonzero $v$; A matrix admits a Cholesky factorisation with positive diagonal exactly when it is Hermitian positive definite, and that factor is unique supplies a factorization $H=L{L}^{\mathsf{T}}$ with $L$ lower triangular and positive diagonal.

For $n\ge 1$, the determinant over a commutative ring by the Leibniz formula, and $\mathrm{\mid }\det A\mathrm{\mid }$ for a real matrix, For same-sized finite square matrices over a commutative ring, $\det (AB)=\det (A)\det (B)$, For every square matrix over a commutative ring, $\det (A^{\mathsf{T}})=\det (A)$, and The determinant of a triangular matrix is the product of its diagonal entries: the determinant is defined by the Leibniz formula, determinants multiply, are unchanged by transpose, and a triangular determinant is the product of its diagonal entries.

Square roots exist: a unique $\sqrt{a}\ge 0$ with $(\sqrt{a}{)}^2=a$; the positives are $\{x^2:x\mathrm{\ne }0\}$: every nonnegative real has a unique nonnegative square root.

The Gaussian integral ${\int }_{-\mathrm{\infty }}^{\mathrm{\infty }}{e}^{-x^2}dx=\sqrt{\pi }$: ${\int }_{\mathbb{R}}{e}^{-x^2}dx=\sqrt{\pi }$.

Change of variable in an improper integral: a monotone differentiable surjection between intervals carries a convergent improper integral to the corresponding transformed integral when the proper substitution hypotheses hold on compact truncations.

Assuming countable choice, $\mathcal{L}({\mathbb{R}}^n)$ is a sigma-algebra containing every elementary set and ${\lambda }_n$ is a complete measure extending elementary volume and A box in ${\mathbb{R}}^n$ with parameters $a_i\le b_i$ is Lebesgue measurable of measure ${\prod }_{i<n}(b_i-a_i)$, whichever of its faces are included: under Countable Choice, ${\lambda }_k$ is a measure and every bounded box is measurable with its volume; the boxes $[-m,m{]}^k$ therefore give a countable finite-measure cover of ${\mathbb{R}}^k$.

Tonelli's theorem for nonnegative measurable functions on a sigma-finite product: for nonnegative product-measurable functions on sigma-finite measure spaces, the product and iterated integrals agree.

A C^1 diffeomorphism satisfies the change-of-variables formula for nonnegative Lebesgue measurable functions: under Countable Choice, a $C^1$ diffeomorphism transforms a nonnegative Lebesgue integral by the absolute Jacobian determinant.

A finite square real matrix is invertible if and only if its determinant is nonzero: a real square matrix is invertible exactly when its determinant is nonzero.

Rectangular matrix multiplication and the identity matrix $I_n$, including zero-sized shapes: matrix products are the usual finite coordinate sums and $I$ is the identity matrix.

Cauchy-Schwarz $\mid ⟨x,y⟩\mid \le \parallel x{\parallel }_2\parallel y{\parallel }_2$ with its equality case, the triangle inequality for $\parallel \cdot {\parallel }_2$, the parallelogram law and polarisation, ${\mathbb{R}}^n$ as the set of functions $n\to \mathbb{R}$, and $d_1$, $d_2$, $d_{\mathrm{\infty }}$ are metrics on it, Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function, A composite of continuous functions is continuous, with no side hypothesis of the kind the composition of limits needs, The exponential function is strictly increasing, A continuous map has Borel preimages of Borel sets, The Borel sigma-algebra of a topological space, Assuming countable choice, every Borel subset of ${\mathbb{R}}^n$ is Lebesgue measurable, The product sigma-algebra and its finite iterates, A measurable function between measurable spaces, and Arithmetic and lattice operations preserve measurability whenever they are defined: the Euclidean norm is continuous for the Euclidean metric, so $z\mapsto e^{-\mathrm{\parallel }z{\mathrm{\parallel }}_2^2\mathrm{/}2}$ is continuous on each ${\mathbb{R}}^k$, hence Borel and Lebesgue measurable under Countable Choice; on ${\mathbb{R}}^k\times \mathbb{R}$, the product $e^{-\mathrm{\parallel }z{\mathrm{\parallel }}_2^2\mathrm{/}2}{e}^{-t^2\mathrm{/}2}$ is measurable for the product sigma-algebra because the coordinate projections are measurable by the measurable-rectangle definition and products of measurable functions are measurable.

The Euclidean Lebesgue measure is the completion of the product of the factor Lebesgue measures: under the canonical identification ${\mathbb{R}}^{k+1}={\mathbb{R}}^k\times \mathbb{R}$, ${\lambda }_{k+1}$ is the completion of ${\lambda }_k\times {\lambda }_1$, so the measures agree on product-measurable sets.

The integral of a nonnegative simple function and The nonnegative Lebesgue integral: the integral of a nonnegative simple function is the sum of its coefficients times the measures of its level sets, and the nonnegative integral is the supremum over simple minorants.

Every nonnegative measurable function admits an explicit increasing sequence of simple approximations and Monotone convergence for the integral: an increasing simple approximation to a nonnegative product-measurable function has the same simple integrals under ${\lambda }_{k+1}$ and ${\lambda }_k\times {\lambda }_1$ by [F15]–[F16]; monotone convergence therefore makes its two nonnegative integrals equal.

A continuous function on $[a,b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion and A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral: under Countable Choice, a continuous function on $[-m,m]$, $m\ge 1$, is bounded and Riemann integrable, and its Riemann and Lebesgue integrals agree.