Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

A uniform Gaussian-cosh local kernel

Abstract

The Gaussian positive-part cosh integral has a uniform local expansion on every positive compact interval.

Write phi for the existing standard normal density, with the exact normalization

Use the following kernel, with the positive part taken before integration:

Definition 1.1 (The actual clipped Gaussian integral).

Formalization. D5/S3/TotalVariation/Asymptotics/GaussianCoshKernel.gaussianCoshIntegral (✓ std3).

Source. Repository-derived.

Commentary.

The integral uses Lebesgue measure on the whole real line. Its integrand is bounded by exp(d) times the standard normal density, so it is integrable for every real q and d.

Theorem 1.2 (Integrability for every real parameter).

Proof. Machine-checked in Lean as D5/S3/TotalVariation/Asymptotics/GaussianCoshKernel.kernel_integrable (✓ std3). ∎

Source. Repository-derived.

Commentary.

The nonnegative clipped integrand is at most exp(d) times the standard normal density. This gives integrability without any sign or smallness restriction on either real parameter.

Theorem 1.3 (The quadratic lower bound for cosh).

Proof. Machine-checked in Lean as D5/S3/TotalVariation/Asymptotics/GaussianCoshKernel.cosh_quadratic_lower (✓ std3). ∎

Source. Repository-derived.

Commentary.

The length-two even factorial sum gives the exact quadratic lower bound.

Theorem 1.4 (The exact coefficient and a uniform fifth-half-power remainder).

Proof. Machine-checked in Lean as D5/S3/TotalVariation/Asymptotics/GaussianCoshKernel.gaussian_cosh_uniform_remainder (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every fixed positive lower endpoint, one choice is delta=1/4 and C=4 phi(0)(5+2/lo^2)/lo. The same constants work for every q in the closed interval, including a singleton interval. The theorem also allows an upper endpoint below the lower endpoint, in which case the interval is empty.

Compare the clipped kernel with phi(0) times the positive part of d-(qu)^2/2. For d at most 1/4, both vanish outside the interval |u| at most 2 sqrt(d)/q. The cosh series gives cosh(x) at least 1+x^2/2. The upper bound cosh(x) at most exp(x^2/2), combined with the quadratic exponential remainder, bounds the clipped-kernel discrepancy by 5d^2.

The density changes by at most phi(0)u^2/2 from its value at zero. On the common interval, u^2 is at most 4d/lo^2. Thus the weighted integrand error is at most phi(0)(5+2/lo^2)d^2. Its integration interval has length 4 sqrt(d)/q. The exact integral of the leading clipped parabola is 4 sqrt(2)d^(3/2)/(3q), giving the stated coefficient and remainder.

This is the local-kernel estimate in equation 14.5 of the categorical decision blindness theory, strengthened to arbitrary positive compact intervals. It does not assert a Bayes-risk identity or either complete crossover theorem. The powers are real powers and d is strictly positive.

References