Gaussian Quadratic Tilted Density
Abstract
A cardinal core of small variances controls the physical tilted energy density on compact intervals.
Theorem 1.1 (Uniform compact lower bound for the actual convolution).
Proof. Machine-checked in Lean as D5/S3/Fourier/Asymptotics/GaussianQuadraticTiltedDensity.result (✓ std3). ∎
Source. Repository-derived.
Commentary.
Fix real constants kappa, K and R with 0<kappa<=1, K>=1 and R>=0. There are positive deltaZero and c, with deltaZero<=1, chosen before every finite array. For each finite decidable index type J, choose finite subsets H and Core, real arrays v and e, and real delta, sigma, alpha and t. Require 0<delta<=deltaZero, 0<sigma<=1 and 1<=alpha<=2. Every v(j) is nonnegative and is positive on H. Set V=sum v(j) and d(j)=1-2t v(j)/alpha. Require kappa<=V<=K and v(j)<=K delta for every index.
Require Core to be contained in H, its cardinality to be at least kappa/delta, and v(j)>=kappa delta on Core. Require card(H)<=K delta^(-4), abs(e(j))<=K sqrt(v(j)) delta^2, and kappa<=d(j)<=K at every index, including outside H. The signed tilt satisfies abs(t)<=K/delta and the exact full-array saddle equation sum v(j)/(alpha d(j))+sum e(j)^2/d(j)^2+delta sigma^2 t/alpha=V. The omitted mass sum over J outside H of v(j)+e(j)^2 is at most delta^2.
Put nu=delta sigma^2/alpha and let P be the product standard Gaussian measure on the real coordinates indexed by H. Define Xt(z)(j)=sqrt(v(j)/(alpha d(j)))z(j)-e(j)/d(j) and E(x)=sum x(j)^2. At h=V+sqrt(delta)y, define gt to be the integral under P of gaussianPDFReal(nu t,nu.toNNReal,h-E(Xt(z))). For every real y with abs(y)<=R, gt is at least c/sqrt(delta). Sigma has no uniform positive lower bound.
Write w(j)=v(j)/(alpha d(j)), m(j)=-e(j)/d(j), W=2 sum over H of w(j)^2+4 sum over H of w(j)m(j)^2+nu, and tau=sum outside H of w(j)+m(j)^2. With L=kappa^3/(2K^2) and U=1+2K^2/kappa^2+4K^4/kappa^3, the physical variance lies between L delta and U delta. The full saddle gives mean mu=V-tau and 0<=tau<=kappa^(-2)delta^2. Normalize a(j)=w(j)/sqrt(W), b(j)=2m(j)sqrt(w(j))/sqrt(W) and gamma=sqrt(nu)/sqrt(W); then 2 sum a(j)^2+sum b(j)^2+gamma^2=1.
The core supplies the integrable Fourier envelope F(xi)=(1+cF xi^2)^(-8), with A=kappa^2/(4K^2 U) and cF=A kappa/8. For M=K sqrt(delta)/(kappa sqrt(L)), the central logarithmic remainder and the noncentral reciprocal remainder in the exact scalar characteristic function give local error at most 3M abs(xi)^3 exp(3M abs(xi)^3). If n>=7 and M<=1/(n+1), use that estimate only for abs(xi)<=(n+1)/4. Outside this cutoff its n-dependent bound is at least 3, whereas 2F(xi)+exp(-xi^2/2)<=3. The error is therefore globally bounded by the minimum of these two envelopes.
Dominated convergence makes the integral of that minimum arbitrarily small before the arrays are chosen. Set X=(R+kappa^(-2))/sqrt(L), eta=exp(-X^2/2)/sqrt(2pi), choose n with integral at most pi eta, and take deltaZero=min(1,kappa/32,1/(MZero^2(n+1)^2)) and c=eta/(2sqrt(U)), where MZero=K/(kappa sqrt(L)). Gaussian convolution inversion uses nu>0, noise mean nu t and the substitution -xi/(2pi sqrt(W)), whose absolute Jacobian is 1/(2pi sqrt(W)). Its mean phases cancel at mu. The resulting density error is at most eta/2; abs(y)<=R places the target within X standard deviations and yields the stated lower bound.