Gaussian observation laws and conditional information
Abstract
Gaussian observation laws and conditional information
Theorem 1.1 (Posterior disintegration, likelihood and conditional free energy).
Proof. Machine-checked in Lean as D5/S3/Observer/Linear/GaussianObservationLaw.gaussian_observation_law (✓ std3). ∎
Source. Repository-derived.
Commentary.
Let n and p be arbitrary finite index sets, including empty sets, and let M be any real p by n matrix. Let beta be positive and let sigma be any real number with sigma squared positive. Put tau equal to the inverse of sigma squared. The input is the centered Gaussian law on the Euclidean space indexed by n plus p, with block diagonal covariance beta inverse times the identity on n and tau inverse times the identity on p. Its signal and noise coordinate maps have those respective centered Gaussian laws and are independent. Write X and N for these coordinates, Y=MX+N, P for the actual pushforward law of (Y,X), and mu for the actual law of Y.
Define Q=beta I+tau M transpose M, Sigma=Q inverse, and A=tau Sigma M transpose. The posterior kernel K(y) is the pushforward of the centered Gaussian law with covariance Sigma along x mapped to Ay+x. It disintegrates the same actual joint law: P=mu tensor K. No injectivity or rank condition is imposed on M.
Let ell be the log likelihood ratio obtained from the actual Radon–Nikodym derivative of P with respect to the product of its marginals. It is integrable under P. The ENNReal Kullback–Leibler divergence I is finite before its conversion to a real number. Its real value is both the integral of ell and one half the difference between the log determinant of beta inverse I and the log determinant of Sigma. The display gives the equivalent observation-Gramian formula.
For a probability law nu on the signal space, h(nu) is minus the integral under nu of the logarithm of its Radon–Nikodym density with respect to Euclidean volume. Define F(beta,nu) as the expected squared Euclidean norm divided by two, minus beta inverse times h(nu). The mean posterior value of this same functional, minus its prior value, equals beta inverse times I. All laws, densities and likelihoods refer to the same joint experiment. A negative sigma is allowed, and empty determinants equal one.
The precision is positive definite because its prior term is positive definite and its observation term is positive semidefinite. The innovation X-AY has covariance Sigma and zero cross covariance with Y, hence is independent of Y; reconstructing X gives the posterior disintegration. Integrable products of the scalar standard Gaussian density give the independent Gaussian density, and affine Haar transport with the absolute inverse determinant gives the nondegenerate density. Its Radon–Nikodym ratio yields the actual likelihood. Gaussian second moments prove logarithmic integrability, and integration gives the determinant identity. Mean conditional energy equals prior energy, so the entropy difference also gives the conditional free-energy identity.
The stronger gaussian_observation_law_complete API retains every conjunct of gaussian_observation_law and additionally proves outer integrability of y mapped to physicalFreeEnergy beta (posteriorKernel M beta tau y) under the actual dataLaw M beta tau. Thus the outer expectation is justified before centering by the finite prior free energy; no integrability assumption on an estimator is introduced. The original theorem is the first projection of this complete result.
The exposed translate_gaussian, precision_posDef, translatedKernel_apply, action_apply, action_adjoint, transpose_pairing and map_gaussian helpers identify the same affine Gaussian measures, matrix actions and actual posterior kernels used in the proof. They organize existing Gaussian and linear-algebra arguments and carry no independent novelty claim. The probability and Markov instances are structural support for these laws.
For the original trajectory experiment substitute n=p=Fin d, M=M_T from any chosen orthonormal basis of the actual L2 trajectory image, sigma=sigma(T), and tau=1/v(T), where v(T)=sigma(T)^2>0. On the original probability space, independence of X and xi with their stated Gaussian laws identifies the pushforward law of (Y_T,X), not just its covariance, with jointLaw M_T beta tau. The outer-integrability result then applies to that same data marginal. Tonelli gives the risk identity for all measurable estimators, including infinite-risk competitors. The existing SpectralNoiseAsymptotics application gives all-real-alpha information including occupied thresholds, risk away only from occupied thresholds, and the exact recovery equivalence for arbitrary positive variance schedules without regularity assumptions. Its separate fixed-eta clause has coefficient trace(C transpose C)/(2 beta eta) and a quadratic remainder without observability. These statements concern conditional probability descriptions and do not settle the separate physical implementation or open operator-window alternatives.
Same-delivery information-escape audits for the newly exposed API theorems remain unfinished; see https://github.com/the-omega-institute/trureturing/issues/20111. Existing audit sources are preserved. Neither compilation of candidate registrations nor this issue is declared_validated evidence.
For an independent realization, let X and xi be measurable random vectors on any probability space, with laws N(0,beta inverse I) and N(0,I), respectively, and set Y=MX+sigma xi. Scaling gives sigma xi the covariance sigma squared I and preserves its independence from X. Thus the law of (X,sigma xi) is the product of those two Gaussian laws. Pushing this product forward by (x,n) mapped to (Mx+n,x) identifies the full law of (Y,X) with jointLaw M beta tau in gaussian_observation_law. Consequently its posterior kernel, data marginal and KL mutual information are those of this same Y. This argument uses beta>0 and sigma squared>0 and allows either sign of sigma.
For every measurable estimator a, define R(a) as the nonnegative integral of half the squared norm of X-a(Y), with values in the extended nonnegative reals. Under the posterior N(Ay,Sigma), the conditional integral is trace(Sigma)/2 plus half the squared norm of Ay-a(y): each coordinate contributes its variance and squared displacement of its mean. Apply Tonelli to the joint disintegration to obtain R(a)=trace(Sigma)/2 plus the nonnegative integral under mu of half the squared norm of Ay-a(y). This identity includes infinite-risk competitors and requires no integrability assumption on a. The measurable linear estimator y mapped to Ay has zero excess term and finite risk trace(Sigma)/2, so it attains the infimum over all measurable estimators.
The Gaussian moment and entropy integrability in the free-energy argument also make y mapped to F(beta,K(y)) integrable under mu. Since mu has total mass one, subtracting the constant prior free energy inside this integral gives the centered identity: the expectation of F(beta,K(Y))-F(beta,prior) is beta inverse times the same mutual information. This is the free energy of the conditional probability description; a physical measurement, feedback or erasure protocol requires its own model.
For known dynamics with B transpose equal to -B, put F_t=exp(tB). The adjoint of F_t is exp(-tB), and their product in either order is the identity, so F_t preserves Euclidean distances. For every measurable future estimator a and every t>=0, the loss between F_t X and a(Y) equals the loss between X and F_t inverse applied to a(Y), pointwise. Composition with this continuous inverse is a bijection on measurable estimators. Hence the future infimum is again trace(Sigma)/2, attained by F_t A Y, with the same data and every measurable competitor, including those of infinite risk.
For the quadratic Gibbs application, let I be any finite index set, including the empty set, let Q be a real positive-definite matrix on I, and let beta>0. On the corresponding Euclidean space put E_Q(x)=(sum over i of x_i(Qx)_i)/2 and f_Q(x)=exp(-beta E_Q(x)). Let Z_Q(beta) be the real Bochner integral of f_Q against canonical Euclidean volume, and let M_Q=volume.withDensity(x mapped to ENNReal.ofReal(f_Q(x))). Then f_Q is integrable, Z_Q(beta)>0, and (ENNReal.ofReal(Z_Q(beta))) inverse times M_Q is the centered multivariate Gaussian with covariance beta inverse times Q inverse. These are conclusions for this original energy, volume and partition; neither a normalization hypothesis nor an assumed equality of laws is needed.
To derive the identification from multivariate_gaussian_density, put Sigma=beta inverse times Q inverse. Positive definiteness gives Sigma positive definite and Sigma inverse=beta Q. If A is the inverse of the positive square root of Sigma, then A transpose A=Sigma inverse, so the squared Euclidean norm of Ax is beta times sum over i of x_i(Qx)_i. Consequently the product of standard scalar Gaussian densities at Ax is b f_Q(x), where b=(sqrt(2 pi)) to the power minus card(I) is positive. The density theorem transports canonical Euclidean volume with a positive finite coefficient c, giving the equality of measures multivariateGaussian 0 Sigma=a M_Q, where a=c times ENNReal.ofReal(b) is positive and finite.
Let J be the nonnegative integral of ENNReal.ofReal(f_Q) against the same volume. Taking total masses in that equality gives a J=1, since the Gaussian has mass one. Thus 0<J<infinity. Measurability and nonnegativity of f_Q now give its integrability, and conversion of its Bochner integral yields ENNReal.ofReal(Z_Q(beta))=J. Hence Z_Q(beta)>0 and its inverse normalization is exactly a, proving the stated normalized-law equality. The argument includes empty I with the usual empty sums and products and imposes no Nonempty hypothesis.
For the original symplectic observation data retain the full telescope: natural numbers n and r with 0<r<2n; S a positive-definite real matrix on Fin(n) plus Fin(n); O a real Fin(r) by (Fin(n) plus Fin(n)) matrix with surjective action; K a real matrix on Fin(r) satisfying O(JS)=KO, where J=[[0,I],[-I,0]]=-Matrix.J (Fin n) real; and R a real (Fin(n) plus Fin(n)) by Fin(2n-r) matrix with R transpose R=I and range(R)=kernel(O). Let beta>0, p=O S inverse O transpose, and C_h=R transpose S R. The original_data_symplectic_retract theorem gives p positive definite under these same assumptions. Applying R transpose to Rx=Ry and using R transpose R=I proves R injective, so restriction of the positive-definite form of S makes C_h positive definite. The kernel-range equality is retained in this original application although this positivity argument uses only orthonormality.
Apply the preceding result with Q=S, Q=p inverse and Q=C_h. It proves integrability and positive Bochner partitions on all three spaces and identifies their normalized Gibbs measures with centered Gaussians of covariances beta inverse times S inverse, beta inverse times p, and beta inverse times C_h inverse, respectively. In the visible case positive definiteness of p justifies both inversion and (p inverse) inverse=p. The generic result also applies with Q=q I for every q>0 on any finite I, including empty I.
The complete classical split in the original data
Use the same original data and all the assumptions above. Write E, V and H for the Euclidean spaces on Fin n plus Fin n, Fin r and Fin(2n-r), respectively. Set l=S inverse O transpose p inverse, N=I-lO, D=R transpose N, A=JS and A_h=R transpose A R, with J=[[0,I],[-I,0]]=-Matrix.J. The matrix action on each Euclidean space is the existing action. Define assemble(u,v)=action(l)u+action(R)v and coords(z)=(action(O)z,action(D)z), in that visible-then-hidden order. Write gamma_v=N(0,beta inverse p), gamma_h=N(0,beta inverse C_h inverse), G_Q for the normalized classical Gibbs measure of E_Q, and Z_Q for its original Bochner partition integral. Thus the preceding three Gaussian identifications give G_S, G_(p inverse) and G_(C_h), with no change of energy or reference volume.
The retract identity Ol=I and range(R)=kernel(O) give OR=0. Every Nz=z-lOz lies in kernel(O), so orthonormality of R gives R R transpose N=N. Also Nl=0 and NR=R. These identities show assemble(coords(z))=z for every z in E and coords(assemble(u,v))=(u,v) for every (u,v) in V times H. In particular the hidden coordinate is R transpose Nz; it is not obtained by replacing the energy lift l with an orthogonal lift. The identities S l=O transpose p inverse and Ol=I imply l transpose S l=p inverse. Both mixed blocks l transpose S R and R transpose S l vanish, and the hidden block is exactly C_h. Hence E_S(assemble(u,v))=E_(p inverse)(u)+E_(C_h)(v) for every pair.
The same energy decomposition gives C_h D=R transpose S, hence D=C_h inverse R transpose S. Consequently O S inverse O transpose=p, D S inverse D transpose=C_h inverse, and O S inverse D transpose=0. Apply Gaussian mapping to Sigma=beta inverse S inverse with the two matrices O and D. It gives the actual marginal laws gamma_v and gamma_h. The ordered pair of linear images is jointly Gaussian, and its mixed covariance is zero by the third identity. Gaussian independence therefore identifies the joint pushforward, not only its two marginals: map(coords,G_S)=gamma_v.prod(gamma_h). The earlier equality G_S=N(0,Sigma) also proves that G_S is a probability measure; the earlier integrability and positivity argument proves Z_S>0.
For any finite index set I, positive-definite Q and beta>0, the exact partition constant is Z_Q=(2 pi/beta)^((card(I):real)/2)/sqrt(det Q). To see the constant, put T=CFC.sqrt Q. Positive definiteness gives T transpose T=Q, det(T)=sqrt(det Q)>0, and norm(action(T)x)^2=x transpose Q x. Haar change of variables contributes the absolute inverse determinant of T, and the radial Gaussian integral with parameter beta/2 contributes (2 pi/beta)^((card(I):real)/2). This uses the original Euclidean volume. It includes the empty index set: its sum is zero, determinant and zero power are one, and its Gaussian and volume have mass one.
For the visible space substitute I=Fin r and Q=p inverse; for the hidden space substitute I=Fin(2n-r) and Q=C_h. Since det(p inverse)=(det p) inverse, the two constants are Z_(p inverse)=(2 pi/beta)^((r:real)/2) sqrt(det p) and Z_(C_h)=(2 pi/beta)^(((2n-r:natural):real)/2)/sqrt(det C_h). These are real powers, with the natural subtraction performed before the hidden dimension is cast to a real number. They hold for every positive beta and the actual anisotropic covariance and precision matrices.
Fix the square matrix B on Fin n plus Fin n by the specified concatenation of the l and R columns. For a column j, let q=finSumFinEquiv(j) in Fin(n+n). When q.val<r take column q.val of l; otherwise take column q.val-r of R. Thus this B uses the original ordering and the specified kernel basis. Reindexing only its columns by (Fin r plus Fin(2n-r)) gives B transpose S B with diagonal blocks p inverse and C_h and zero off-diagonal blocks. Matrix determinant multiplication and the block determinant formula give det(B)^2 det(S)=det(C_h)/det(p), hence abs(det(B)) sqrt(det p) sqrt(det S)=sqrt(det C_h). The equality r+(2n-r)=n+n and positivity of 2 pi/beta justify splitting the real power. Substituting the partition constants yields Z_S=abs(det(B)) Z_(p inverse) Z_(C_h). The absolute value retains both orientations; no determinant-one assumption is used.
The dynamics use the same lift and kernel coordinates. The original retract gives A l=l K, while observation closure gives O A=K O. The kernel of O is A-invariant, so A R=R A_h. It follows that N A=A N and D A=A_h D. Exponential intertwining therefore gives, for every real t and every z in E, coords(exp(t action(A))z)=(exp(t action(K))(coords(z).1),exp(t action(A_h))(coords(z).2)). Here exp is NormedSpace.exp on continuous linear endomorphisms; the identities are equalities of the actual flows, with no restriction to nonnegative or discrete time.
Skew symmetry of J and symmetry of S give A transpose S+S A=0. Restriction to the kernel gives A_h transpose C_h+C_h A_h=0, and the reduced identity is K p+p K transpose=0. Equivalently A S inverse+S inverse A transpose=0 and A_h C_h inverse+C_h inverse A_h transpose=0. Exponentiation preserves each actual covariance: F_t Sigma F_t transpose=Sigma for the full, visible and hidden Gaussian laws with their respective generators. Gaussian mapping then gives map(exp(t action(K)),gamma_v)=gamma_v, map(exp(t action(A_h)),gamma_h)=gamma_h and map(exp(t action(A)),G_S)=G_S for every real t. The last equality uses the normalized Gibbs law already identified above, so it is stationarity of that original measure.
The reusable public declarations have a direct parameter correspondence. Apply D5.S3.QuadraticForms.OriginalDataSymplecticSplit.original_data_symplectic_retract to S,O,K and their positive-definiteness, surjectivity and closure hypotheses. In this module, apply multivariate_gaussian_density at mean zero and covariance beta inverse Q inverse for Q=S, p inverse and C_h; apply map_gaussian at mean zero, covariance beta inverse S inverse and mapping matrix O or D. The public action_adjoint and transpose_pairing express the same mixed covariance. Mathlib’s HasGaussianLaw.indepFun_of_covariance_inner applies to that ordered jointly Gaussian pair. CFC.sqrt_mul_sqrt_self, Measure.map_linearMap_addHaar_eq_smul_addHaar, GaussianFourier.integral_rexp_neg_mul_sq_norm, Matrix.det_mul, Matrix.det_fromBlocks_zero and Real.rpow_add supply the square-root, volume, integral, determinant and real-power identities. NormedSpace.exp_series_hasSum_exp’ and NormedSpace.map_exp supply exponential intertwining and transport between matrix and continuous-linear-map exponentials.
The strict bounds 0<r<2n belong to this original split throughout; the finite-index density and integration arguments themselves also include empty index sets. The conclusions impose no simple-spectrum, isotropic-covariance, orthogonal-lift or orientation condition, and they hold for every specified orthonormal basis of kernel(O). Singular S, nonsurjective O and nonpositive beta are outside the assumptions. The coupled Darboux and Williamson coordinate realization is described separately in OriginalDataCoupledCoordinates; its final symplectic coordinate map is distinct from the orthonormal kernel matrix R used here. These are classical finite-dimensional probability and Hamiltonian statements. The physical O-compatible tensor factorization, common operator domains, heat-trace and Gibbs identifications, and their conditional KL and free-energy joins still require their physical hypotheses and derivations. The all-WSS heterogeneous-depth alternative remains unresolved.