Fixed-noise exponential-Gramian information expansion
Abstract
Fixed-noise exponential-Gramian information expansion
Theorem 1.1 (Fixed-noise exponential-Gramian information expansion).
Proof. Machine-checked in Lean as D5/S3/Observer/Linear/PhysicalFixedNoiseInformation.physical_fixed_noise_information (✓ std3). ∎
Source. Repository-derived.
Commentary.
Let V be a finite-dimensional real inner-product space, W a complete real inner-product space, and B:V→V and C:V→W bounded linear maps. Zero-dimensional spaces and unobserved directions are allowed. Fix a positive prior precision beta and a positive coordinate-noise variance eta.
Define H as the adjoint of C composed with C. Define G(T) as the actual Bochner integral from zero to T of the adjoint of C exp(t B) composed with C exp(t B). The determinant and trace are those of the finite-dimensional state operator, and the norm is the induced Hilbert operator norm.
There are K at least zero and delta greater than zero such that for every positive T at most delta, the absolute difference between one half log det(id+(beta eta)^(-1)G(T)) and T trace(H)/(2 beta eta) is at most K T squared.
Differentiability of the exponential integrand yields a uniform bound for G(T)-T H of order T squared. Positivity of G(T), its actual orthonormal eigenbasis, and a scalar logarithmic remainder bound control the determinant. An orthonormal trace estimate combines these errors.
The result concerns the actual exponential-Gramian log determinant. In a finite-coordinate linear Gaussian observation model with state covariance beta^(-1)I, independent isotropic coordinate noise covariance eta I, and observation-coordinate Gramian G(T), this expression is mutual information in nats. Polynomial moment compression requires its own finite-time estimate.