Gaussian Quadratic Mixed Defect
Abstract
A uniform bound quantifies the dependence between Gaussian linear coordinates and diagonal quadratic sums.
Theorem 1.1 (Correlated old coordinates and a finite Gaussian row).
Proof. Machine-checked in Lean as D5/S3/Fourier/Asymptotics/GaussianQuadraticMixedDefect.result (✓ std3). ∎
Source. Repository-derived.
Commentary.
Let P be a probability measure on an arbitrary measurable space. Let G(j) be a finite independent family of standard real Gaussian variables. Let Y be any real random variable such that the actual pair of Y and the whole row G is jointly Gaussian. The mean of Y is unrestricted, and its variance may vanish. No independence of Y and G is assumed.
For arbitrary signed coefficients a(j) with absolute value at most a nonnegative M, set Q equal to the sum of a(j)(G(j)^2-1). The difference between the characteristic function of Y+Q at one and the product of the characteristic functions of Y and Q at one has norm at most M Var(Y) exp(M Var(Y)). The estimate is independent of the number of row coordinates and includes the empty row.
Regression uses b(j)=Cov(Y,G(j)). Its residual Y minus the sum of b(j)G(j) is jointly Gaussian and uncorrelated with the row, hence independent of it. Its nonnegative variance implies that the sum of b(j)^2 is at most Var(Y). The linear-plus-quadratic Gaussian integral and the exponential remainder bound then give the displayed estimate.
Scaling a by a test frequency gives the mixed characteristic-function estimate at that frequency. Passing the bound through L2 truncations allows countable quadratic sums; the finite estimate itself does not assert convergence in distribution.