Theorem. Independent Gaussian laws on real isotypic sectors [fdip-0055]
✍️source

  • November 1, 2026

Let a finite group \(G\) act orthogonally on a finite-dimensional real inner-product space \(H\), and let \(Q>0\) be self-adjoint and \(G\)-equivariant. Write the orthogonal isotypic projectors as \(E_\Xi \), put \(H_\Xi =E_\Xi H\), and omit the zero sectors. Use induced Euclidean volumes and uncompleted Borel sigma-algebras. For the normalized Gaussian law \(\mu _Q\), the map \[\mathcal D:H\longrightarrow \prod _\Xi H_\Xi , \qquad z\longmapsto (E_\Xi z)_\Xi \] satisfies \[\mathcal D_*\mu _Q=\bigotimes _\Xi \mu _{Q|_{H_\Xi }}. \qquad Z_Q=\prod _\Xi Z_{Q|_{H_\Xi }}.\] Thus the projected fields are independent. Each has covariance \((Q|_{H_\Xi })^{-1}\) on its own real sector.

In the multiplicity coordinates, set \(D_\Xi =\operatorname {End}_G(W_\Xi )\), \(r_\Xi =\dim _{D_\Xi }W_\Xi \), and \(d_\Xi =\dim _{\mathbb R}D_\Xi \in \{1,2,4\}\). Write \(Q_\Xi \in M_{m_\Xi }(D_\Xi )\) for the multiplicity matrix; it is not the entire real-sector matrix. Then \[\begin {aligned} \det _{\mathbb R}Q &=\prod _\Xi \det _{\mathbb R} (Q_\Xi :D_\Xi ^{m_\Xi }\to D_\Xi ^{m_\Xi })^{r_\Xi },\\ Z_{Q|_{H_\Xi }} &=\frac {(2\pi )^{m_\Xi r_\Xi d_\Xi/2}} {\det _{\mathbb R}(Q_\Xi )^{r_\Xi/2}}. \end {aligned}\] The determinants in these formulas are ordinary determinants of real linear operators, including when \(D_\Xi =\mathbb H\).

Proof. 

  • November 1, 2026

The projectors are self-adjoint, mutually orthogonal and sum to \(I\). Addition from the product of their images is an isometry inverse to \(\mathcal D\). Concatenated orthonormal bases identify the orthogonal product volume with volume on \(H\); finite products of these Borel spaces have the product Borel sigma-algebra. Commutation with every projector makes \(Q\) block diagonal, so its positive quadratic form is the sum of its sector quadratic forms. The exponential weight therefore factors.

Each restricted precision is positive, and the Gaussian normalizer theorem makes every sector integral finite and positive. Nonnegative Tonelli gives the product of normalizers. Integrating the factored density on a Borel rectangle gives the product of its sector probabilities; uniqueness of finite measures on the rectangle-generated sigma-algebra gives the stated product law. This is the same measure argument as in Theorem [fdip-000M], now for the finite family of projectors. The inverse-precision covariance theorem applies to each factor. Empty sectors have unit normalizer and their one-point law.

For the determinant, the real-sector matrix is the direct sum of \(r_\Xi \) identical real operators \(Q_\Xi \) on \(D_\Xi ^{m_\Xi }\), by the orthonormal scalar-column construction of Corollary [fdip-0050]. Determinants multiply under real direct sums. If the positive Hermitian eigenvalues of \(Q_\Xi \) are \(\lambda _1,\ldots ,\lambda _{m_\Xi }\), its real determinant is \(\prod _j\lambda _j^{d_\Xi }\). Substitution into the real Gaussian normalizer gives the displayed formula.

For the twisted prism, the trivial multiplicity matrix has determinant \(4\), while the complex matrix has complex determinant \(46\). Both have \(r_\Xi =1\), so \(\det _{\mathbb R}Q=4\cdot 46^2=8464\) and \(Z_Q=(2\pi )^3/92\). For the binary tetrahedral Cayley graph, write \(a=m^2>0\). The 5 real sectors give the following factors: \[\begin {array}{c|c|c} D_\Xi &r_\Xi &\det _{\mathbb R}(Q|_{H_\Xi })\\\hline \mathbb R&1&a\\ \mathbb C&1&(a+3)^2\\ \mathbb R&3&[(a+8)(a+11)^2]^3\\ \mathbb H&1&(a+9)^4\\ \mathbb C&2&[(a+6)(a+9)]^4 \end {array}\] Their product is \[\det _{\mathbb R}Q =a(a+3)^2(a+6)^4(a+8)^3(a+9)^8(a+11)^6.\] The exponents sum to \(24\), the real field dimension. The normalizer is \[Z_Q=\frac {(2\pi )^{12}}{\sqrt {\det _{\mathbb R}Q}}.\] These factors use the mass-shifted precision, not the singular Laplacian alone.

The density convention agrees with [friedli2017statistical, Theorem 8.4, p. 385] after setting its mean to zero and its covariance to \(\Sigma =Q^{-1}\). That theorem identifies the Gaussian density; the finite-group projectors and real determinant exponents are supplied by the proofs above and in Corollary [fdip-0050].

Mathlib's ProbabilityTheory.HasGaussianLaw.iIndepFun_of_covariance_inner supports the independence step for a finite family of jointly Gaussian real Hilbert-space variables. Here the family is \(z\mapsto (E_\Xi z)_\Xi \), a linear image of the Gaussian field. For distinct sectors and \(u\in H_\Xi \), \(v\in H_\Psi \), its scalar cross covariance is \(\langle u,Q^{-1}v\rangle =0\), because \(Q^{-1}\) preserves the orthogonal sectors. Thus the declaration's zero-cross-covariance hypothesis matches this family. It does not assert the representation-theoretic decomposition or the real determinant exponents.