Theorem. The retained Gaussian marginal [fdip-000E]

Use the orthogonal sum \(E=X\mathbin \perp Y\), positive precision \(Q\), effective precision \(S\) and exact scalar \(c_C\) of Gaussian elimination. Let \(\pi =p_X:E\to X\) and let \(\mu _Q,\mu _S\) be the independently defined Gaussian probability laws. Then \[Z_Q=c_CZ_S,\qquad \pi _*\mu _Q=\mu _S.\] Thus the retained marginal law is \(\mu _S\): for every Borel \(D\subseteq X\), \(\mu _Q(\pi ^{-1}D)=\mu _S(D)\). Here pushforward assigns \(D\) the mass of its inverse image, extending the finite pushforward convention to these Borel spaces.

Every real Borel function \(F:X\to \mathbb R\) satisfies the extended nonnegative identity \[\int _E|F\circ \pi |\,d\mu _Q =\int _X|F|\,d\mu _S\ \in [0,\infty ].\] Consequently \(F\in L^1(\mu _S)\) if and only if \(F\circ \pi \in L^1(\mu _Q)\). Under these equivalent conditions, \[\int _E F\circ \pi \,d\mu _Q=\int _X F\,d\mu _S.\] We use actual Borel functions; \(L^1\) here denotes their integrable vector space. It is not asserted to be an algebra.

For a finite real vector space \(W\), write \(\mathcal P(W)\) for its intrinsic polynomial function algebra, generated by linear functionals. The actual map on observables is \[\begin {aligned} \pi ^*:\mathcal P(X)&\longrightarrow \mathcal P(E),\\ P&\longmapsto P\circ \pi . \end {aligned}\] It is an injective unital real algebra homomorphism preserving the identity involutions. For the Gaussian polynomial states, \[\omega _S=\omega _Q\circ \pi ^*.\] The field projection goes \(E\to X\); this observable inclusion goes in the opposite direction.

The inverse-compression and covariance identities are \[\begin {aligned} p_XQ^{-1}i_X&=S^{-1},\\ \operatorname {Cov}_{\mu _Q}(\ell _j\circ \pi ,\ell _k\circ \pi ) &=h_X(j,S^{-1}k), \end {aligned}\] where \(\ell _j(x)=h_X(j,x)\). The means vanish. In counting coordinates this is \((Q^{-1})_{RR}=S^{-1}\).

Fixing the eliminated field is a different operation from averaging it. The conditional-law calculation gives its parameters; the four-cycle comparison exhibits a difference even when the fixed value is zero.

[rasmussen2006gaussian, Appendix A.2, equations (A.5)-(A.6), p. 200] gives Gaussian marginal and conditional parameters. The inverse block formula is in [rasmussen2006gaussian, Appendix A.3, equation (A.13), p. 202]. Its joint parameter is covariance \(\Sigma =Q^{-1}\). Retained covariance is therefore \(p_X\Sigma i_X=S^{-1}\), not \(S\).

In orthonormal coordinates, \(\Sigma ^{-1}=Q\) and \(\det \Sigma =(\det Q)^{-1}\) turn the provider density into \(Z_Q^{-1}w_Q\); the density and volume comparison identifies the probability laws. Mathlib's ProbabilityTheory.measurePreserving_restrict₂_multivariateGaussian then supports coordinate restriction with covariance \(\Sigma \). TauCeti's TauCeti.Probability.map_affine_multivariateGaussian supports rectangular affine images with positive-semidefinite covariance. Apply its linear map as the orthonormal presentation of \(p_X\) and its translation as zero. These concern Gaussian probability measures, not volume preservation by a projection.

Mathlib's MeasureTheory.integral_prod supports signed Fubini under integrability. None of these declarations supplies the raw factor \(c_C\) or removes the preceding absolute-value argument.