Theorem. The real Gaussian law is a product over orthogonal sectors [fdip-000M]

Let \(H\) be a finite-dimensional real inner-product space, \(P:H\to H\) an orthogonal involution, and \(Q:H\to H\) a positive self-adjoint precision with \(QP=PQ\). Put \(H_\varepsilon =\ker (P-\varepsilon I)\) and \(E_\varepsilon =(I+\varepsilon P)/2\). Use induced Euclidean volumes on the uncompleted Borel sigma-algebras. The restrictions \(Q_\varepsilon =Q|_{H_\varepsilon }\) are positive self-adjoint. For their Gaussian laws, \[\begin {aligned} D:H&\longrightarrow H_+\times H_-,\\ z&\longmapsto (E_+z,E_-z),\\ D_*\mu _Q&=\mu _{Q_+}\otimes \mu _{Q_-},\qquad Z_Q=Z_{Q_+}Z_{Q_-}. \end {aligned}\] Thus the sector-valued random variables \(E_+,E_-\) are independent with the indicated marginal laws. The four-cycle recovery computes both blocks, their normalizers and their retained scalar laws explicitly.

For the actual polynomial function algebras, write \(\omega _R(p)=\int p\,d\mu _R\). Then \[\omega _Q\bigl ((p_+\circ E_+)(p_-\circ E_-)\bigr ) =\omega _{Q_+}(p_+)\omega _{Q_-}(p_-).\] Indeed linear precomposition takes polynomial generators to polynomial generators. Every polynomial, product and square has finite absolute Gaussian integral by Proposition [fdip-002W], applied on the full space and on each sector. Tonelli applied first to the absolute product therefore justifies signed Fubini, which gives the formula from the product law. These are real polynomial states: they are linear, normalized and nonnegative on \(p^2\), with the identity star. No algebra structure on all integrable functions, or state on \(\operatorname {End}(H)\), is being used.

[friedli2017statistical, Proposition B.55, p. 505] uses covariance as its positive parameter. In an orthonormal chart, set \(\Sigma =Q^{-1}\). Its eigenvalues are positive, \(\Sigma ^{-1}=Q\) and \(\det \Sigma =(\det Q)^{-1}\), so its normalized density is exactly \(Z_Q^{-1}w_Q\). The inverse-precision covariance theorem identifies \(\Sigma \) as the covariance. The product proof above uses densities, not an inference from zero covariance for an unspecified law.

Mathlib's OrthonormalBasis.measurePreserving_repr supports passage to orthonormal coordinates. Index coordinates by the disjoint union of orthonormal bases of \(H_+\) and \(H_-\). Then \(\Sigma =\operatorname {diag}(Q_+^{-1},Q_-^{-1})\) is positive definite, hence positive semidefinite, with zero cross block and mean zero. After the density identification, TauCeti's TauCeti.Probability.indepFun_sumEquivProd_multivariateGaussian_iff gives the corresponding coordinate independence. It concerns this Gaussian covariance, not an arbitrary algebraic splitting or Schur fiber integral.

The integration convention is [tao2011measure, Theorem 1.7.15, pp. 200-201, preliminary version]. All probability assertions here are finite-dimensional and real, with strictly positive precision and specified volume. They supply no Lebesgue probability over a general coefficient ring; a singular precision needs a separately specified constrained space and law.