Gaussian-weighted integral operators

Abstract

Gaussian density gives the actual integral-kernel factory, density isometry, difference-kernel estimates, and convolution conjugacy.

Theorem 1.1 (The actual L2 kernel factory).

$$\forall r\in \mathbb{R},alpha\in \mathbb{R},0<r\Rightarrow \left(r<1\Rightarrow \left(\exists T\in \mathrm{ContinuousLinearMap}\left(\mathbb{R},\mathrm{Lp}\left(\mathbb{R},2,\mathrm{productMeasure}\left(\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right),\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right)\right)\right),\mathrm{ContinuousLinearMap}\left(\mathbb{R},\mathrm{Lp}\left(\mathbb{R},2,\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right)\right),\mathrm{Lp}\left(\mathbb{R},2,\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right)\right)\right)\right),\left(\forall K\in \mathrm{Lp}\left(\mathbb{R},2,\mathrm{productMeasure}\left(\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right),\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right)\right)\right),f\in \mathrm{Lp}\left(\mathbb{R},2,\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right)\right),\mathrm{AEEq}\left(\mathrm{coeFn}\left(\mathrm{apply}\left(\mathrm{apply}\left(T,K\right),f\right)\right),(x:\mathbb{R}\mapsto \mathrm{integral}\left((y:\mathbb{R}\mapsto \mathrm{apply}\left(\mathrm{coeFn}\left(K\right),\mathrm{pair}\left(x,y\right)\right)\cdot \mathrm{apply}\left(\mathrm{coeFn}\left(f\right),y\right)),\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right)\right)),\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right)\right)\right)\wedge \left(\left(\forall K\in \mathrm{Lp}\left(\mathbb{R},2,\mathrm{productMeasure}\left(\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right),\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right)\right)\right),L\in \mathrm{Lp}\left(\mathbb{R},2,\mathrm{productMeasure}\left(\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right),\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right)\right)\right),\mathrm{norm}\left(\mathrm{apply}\left(T,K\right)-\mathrm{apply}\left(T,L\right)\right)\le \mathrm{norm}\left(K-L\right)\right)\wedge \left(\left(\forall iota\in Type,filter\in \mathrm{Filter}\left(iota\right),Ks\in iota\to \mathrm{Lp}\left(\mathbb{R},2,\mathrm{productMeasure}\left(\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right),\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right)\right)\right),K\in \mathrm{Lp}\left(\mathbb{R},2,\mathrm{productMeasure}\left(\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right),\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right)\right)\right),\mathrm{Tendsto}\left(Ks,filter,\mathrm{nhds}\left(K\right)\right)\Rightarrow \mathrm{Tendsto}\left((i:iota\mapsto \mathrm{apply}\left(T,\mathrm{apply}\left(Ks,i\right)\right)),filter,\mathrm{nhds}\left(\mathrm{apply}\left(T,K\right)\right)\right)\right)\wedge \left(\left(\forall K\in \mathrm{Lp}\left(\mathbb{R},2,\mathrm{productMeasure}\left(\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right),\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right)\right)\right),f\in \mathrm{Lp}\left(\mathbb{R},2,\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right)\right),k\in \mathrm{Product}\left(\mathbb{R},\mathbb{R}\right)\to \mathbb{R},g\in \mathbb{R}\to \mathbb{R},hk\in \mathrm{AEEq}\left(k,\mathrm{coeFn}\left(K\right),\mathrm{productMeasure}\left(\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right),\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right)\right)\right),hg\in \mathrm{AEEq}\left(g,\mathrm{coeFn}\left(f\right),\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right)\right),\mathrm{AlmostEverywhere}\left(\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right),(x:\mathbb{R}\mapsto \mathrm{Integrable}\left((y:\mathbb{R}\mapsto \mathrm{apply}\left(k,\mathrm{pair}\left(x,y\right)\right)\cdot \mathrm{apply}\left(g,y\right)),\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right)\right))\right)\wedge \mathrm{AEEq}\left((x:\mathbb{R}\mapsto \mathrm{integral}\left((y:\mathbb{R}\mapsto \mathrm{apply}\left(k,\mathrm{pair}\left(x,y\right)\right)\cdot \mathrm{apply}\left(g,y\right)),\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right)\right)),\mathrm{coeFn}\left(\mathrm{apply}\left(\mathrm{apply}\left(T,K\right),f\right)\right),\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right)\right)\right)\wedge \left(\forall iota\in Type,filter\in \mathrm{Filter}\left(iota\right),nonemptyFilter\in \mathrm{NeBot}\left(filter\right),Ks\in iota\to \mathrm{Lp}\left(\mathbb{R},2,\mathrm{productMeasure}\left(\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right),\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right)\right)\right),K\in \mathrm{Lp}\left(\mathbb{R},2,\mathrm{productMeasure}\left(\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right),\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right)\right)\right),bound\in \mathbb{R},\mathrm{Tendsto}\left(Ks,filter,\mathrm{nhds}\left(K\right)\right)\Rightarrow \left(\mathrm{Eventually}\left(filter,(i:iota\mapsto \mathrm{norm}\left(\mathrm{apply}\left(T,\mathrm{apply}\left(Ks,i\right)\right)\right)\le bound)\right)\Rightarrow \mathrm{norm}\left(\mathrm{apply}\left(T,K\right)\right)\le bound\right)\right)\right)\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Fourier/Asymptotics/CosineCutoffKernel/GaussianWeight.weighted_integral_operator (✓ std3). ∎

Source. Repository-derived.

Commentary.

For the original parameters 0<r<1 and arbitrary real alpha, set a=(1+r)/2, b=(1-r)/2, c0=1/(4pisqrt(ab)), kappa=1/a+alpha^2/b, rho(x)=c0exp(-kappa*x^2/2), and mu=volume.withDensity(ofReal(rho)). The displayed T is a continuous linear map from real L2(mu times mu) to continuous operators on real L2(mu). Its representatives are the actual kernel integrals, it is 1-Lipschitz in the kernel, it preserves arbitrary filter limits, and its raw-representative clause proves row integrability and equality for any almost-everywhere-equal representatives. An eventual uniform bound passes to the limit only under the displayed nonempty-filter hypothesis.

Theorem 1.2 (An onto density isometry).

$$\forall r\in \mathbb{R},alpha\in \mathbb{R},0<r\Rightarrow \left(r<1\Rightarrow \left(\exists U\in \mathrm{LinearIsometryEquiv}\left(\mathbb{R},\mathrm{Lp}\left(\mathbb{R},2,\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right)\right),\mathrm{Lp}\left(\mathbb{R},2,volume\right)\right),\left(\forall f\in \mathrm{Lp}\left(\mathbb{R},2,\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right)\right),\mathrm{AEEq}\left(\mathrm{coeFn}\left(\mathrm{apply}\left(U,f\right)\right),(x:\mathbb{R}\mapsto \mathrm{sqrt}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right)\cdot \mathrm{apply}\left(\mathrm{coeFn}\left(f\right),x\right)),volume\right)\right)\wedge \left(\forall h\in \mathrm{Lp}\left(\mathbb{R},2,volume\right),\mathrm{AEEq}\left(\mathrm{coeFn}\left(\mathrm{apply}\left(\mathrm{symm}\left(U\right),h\right)\right),(x:\mathbb{R}\mapsto \frac{\mathrm{apply}\left(\mathrm{coeFn}\left(h\right),x\right)}{\mathrm{sqrt}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right)}),\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right)\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Fourier/Asymptotics/CosineCutoffKernel/GaussianWeight.density_unitary (✓ std3). ∎

Source. Repository-derived.

Commentary.

With exactly the same density and measure, the real linear isometry equivalence U multiplies a weighted-L2 representative by sqrt(rho) almost everywhere for Lebesgue measure. Its inverse divides a Lebesgue-L2 representative by sqrt(rho) almost everywhere for mu. The strictly positive Gaussian density makes both directions lawful; surjectivity and the inverse formula are included in the equivalence, not assumed separately.

Theorem 1.3 (Gaussian difference kernels and their limits).

$$\forall r\in \mathbb{R},alpha\in \mathbb{R},0<r\Rightarrow \left(r<1\Rightarrow \left(\left(\forall z\in \mathbb{R},\mathrm{integral}\left((x:\mathbb{R}\mapsto \frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\cdot \frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot \left(x-z\right)\cdot \left(x-z\right)}{2}\right)),volume\right)=\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \mathrm{sqrt}\left(\frac{\pi }{\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}}\right)\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot z\cdot z}{4}\right)\right)\wedge \left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \mathrm{sqrt}\left(\frac{\pi }{\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}}\right)=\mathrm{integral}\left((x:\mathbb{R}\mapsto \frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\cdot \frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)),volume\right)\wedge \left(\left(\forall q\in \mathbb{R}\to \mathbb{R},measurableQ\in \mathrm{Measurable}\left(q\right),hq\in \mathrm{MemLp}\left(q,2,volume\right),\exists K\in \mathrm{Lp}\left(\mathbb{R},2,\mathrm{productMeasure}\left(\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right),\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right)\right)\right),\mathrm{AEEq}\left(\mathrm{coeFn}\left(K\right),(z:\mathrm{Product}\left(\mathbb{R},\mathbb{R}\right)\mapsto \mathrm{apply}\left(q,\mathrm{first}\left(z\right)-\mathrm{second}\left(z\right)\right)),\mathrm{productMeasure}\left(\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right),\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right)\right)\right)\wedge \left(\mathrm{norm}\left(K\right)\cdot \mathrm{norm}\left(K\right)=\mathrm{integral}\left((z:\mathbb{R}\mapsto \mathrm{apply}\left(q,z\right)\cdot \mathrm{apply}\left(q,z\right)\cdot \frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \mathrm{sqrt}\left(\frac{\pi }{\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}}\right)\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot z\cdot z}{4}\right)),volume\right)\wedge \mathrm{norm}\left(K\right)\cdot \mathrm{norm}\left(K\right)\le \frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \mathrm{sqrt}\left(\frac{\pi }{\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}}\right)\cdot \mathrm{norm}\left(\mathrm{toLp}\left(hq,q\right)\right)\cdot \mathrm{norm}\left(\mathrm{toLp}\left(hq,q\right)\right)\right)\right)\wedge \left(\left(\forall q\in \mathbb{R}\to \mathbb{R},p\in \mathbb{R}\to \mathbb{R},measurableQ\in \mathrm{Measurable}\left(q\right),measurableP\in \mathrm{Measurable}\left(p\right),hq\in \mathrm{MemLp}\left(q,2,volume\right),hp\in \mathrm{MemLp}\left(p,2,volume\right),K\in \mathrm{Lp}\left(\mathbb{R},2,\mathrm{productMeasure}\left(\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right),\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right)\right)\right),L\in \mathrm{Lp}\left(\mathbb{R},2,\mathrm{productMeasure}\left(\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right),\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right)\right)\right),hK\in \mathrm{AEEq}\left(\mathrm{coeFn}\left(K\right),(z:\mathrm{Product}\left(\mathbb{R},\mathbb{R}\right)\mapsto \mathrm{apply}\left(q,\mathrm{first}\left(z\right)-\mathrm{second}\left(z\right)\right)),\mathrm{productMeasure}\left(\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right),\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right)\right)\right),hL\in \mathrm{AEEq}\left(\mathrm{coeFn}\left(L\right),(z:\mathrm{Product}\left(\mathbb{R},\mathbb{R}\right)\mapsto \mathrm{apply}\left(p,\mathrm{first}\left(z\right)-\mathrm{second}\left(z\right)\right)),\mathrm{productMeasure}\left(\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right),\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right)\right)\right),\mathrm{norm}\left(K-L\right)\cdot \mathrm{norm}\left(K-L\right)\le \frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \mathrm{sqrt}\left(\frac{\pi }{\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}}\right)\cdot \mathrm{norm}\left(\mathrm{toLp}\left(hq,q\right)-\mathrm{toLp}\left(hp,p\right)\right)\cdot \mathrm{norm}\left(\mathrm{toLp}\left(hq,q\right)-\mathrm{toLp}\left(hp,p\right)\right)\right)\wedge \left(\forall iota\in Type,filter\in \mathrm{Filter}\left(iota\right),q\in iota\to \mathbb{R}\to \mathbb{R},p\in \mathbb{R}\to \mathbb{R},measurableQ\in \left(\forall i\in iota,\mathrm{Measurable}\left(\mathrm{apply}\left(q,i\right)\right)\right),measurableP\in \mathrm{Measurable}\left(p\right),hq\in \left(\forall i\in iota,\mathrm{MemLp}\left(\mathrm{apply}\left(q,i\right),2,volume\right)\right),hp\in \mathrm{MemLp}\left(p,2,volume\right),Ks\in iota\to \mathrm{Lp}\left(\mathbb{R},2,\mathrm{productMeasure}\left(\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right),\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right)\right)\right),K\in \mathrm{Lp}\left(\mathbb{R},2,\mathrm{productMeasure}\left(\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right),\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right)\right)\right),hKs\in \left(\forall i\in iota,\mathrm{AEEq}\left(\mathrm{coeFn}\left(\mathrm{apply}\left(Ks,i\right)\right),(z:\mathrm{Product}\left(\mathbb{R},\mathbb{R}\right)\mapsto \mathrm{apply}\left(\mathrm{apply}\left(q,i\right),\mathrm{first}\left(z\right)-\mathrm{second}\left(z\right)\right)),\mathrm{productMeasure}\left(\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right),\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right)\right)\right)\right),hK\in \mathrm{AEEq}\left(\mathrm{coeFn}\left(K\right),(z:\mathrm{Product}\left(\mathbb{R},\mathbb{R}\right)\mapsto \mathrm{apply}\left(p,\mathrm{first}\left(z\right)-\mathrm{second}\left(z\right)\right)),\mathrm{productMeasure}\left(\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right),\mathrm{withDensity}\left(volume,(x:\mathbb{R}\mapsto \mathrm{ennrealOfReal}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \exp \left(-\frac{\left(\frac{1}{\frac{1+r}{2}}+\frac{alpha\cdot alpha}{\frac{1-r}{2}}\right)\cdot x\cdot x}{2}\right)\right))\right)\right)\right),\mathrm{Tendsto}\left((i:iota\mapsto \mathrm{toLp}\left(\mathrm{apply}\left(hq,i\right),\mathrm{apply}\left(q,i\right)\right)),filter,\mathrm{nhds}\left(\mathrm{toLp}\left(hp,p\right)\right)\right)\Rightarrow \mathrm{Tendsto}\left(Ks,filter,\mathrm{nhds}\left(K\right)\right)\right)\right)\right)\right)\right)\right)$$