Actual cosine-integral high-pass operators

Abstract

The positive cosine-integral kernel is the actual L2 limit of the finite cutoffs. Its ordinary convolution and original Gaussian weighted integral operator inherit the high-pass bound.

Write q(c,x)=2 Ci(c|x|), where Ci is the existing sine-tail cosine integral. The totalized origin value is immaterial in Lebesgue L2 and in the Gaussian product measure.$q\left(c,x\right)=2\cdot \mathrm{Ci}\left(c\cdot \left|x\right|\right)$D5/S3/Fourier/Asymptotics/CosineCutoffKernel/Highpass.highpassKernel``D5/S3/Fourier/Asymptotics/CosineIntegralLattice.cosineIntegral

Theorem 1.1 (Exact cutoff error and every real cutoff filter).

$$\forall c\in \mathbb{R},0<c\Rightarrow \left(\mathrm{Measurable}\left(\mathrm{highpassKernel}\left(c\right)\right)\wedge \left(\exists hq\in \mathrm{MemLp}\left(\mathrm{highpassKernel}\left(c\right),2,volume\right),\left(\forall N\in \mathbb{R},c\le N\Rightarrow \left(\forall hNq\in \mathrm{MemLp}\left(\mathrm{kernel}\left(c,N\right),2,volume\right),\mathrm{square}\left(\mathrm{norm}\left(\mathrm{toLp}\left(hNq,\mathrm{kernel}\left(c,N\right)\right)-\mathrm{toLp}\left(hq,\mathrm{highpassKernel}\left(c\right)\right)\right)\right)=\frac{4\cdot \pi }{N}\right)\right)\wedge \left(\forall iota\in Type,\forall l\in \mathrm{Filter}\left(iota\right),\forall Ns\in iota\to \mathbb{R},\forall hNs\in \left(\forall i\in iota,c\le \mathrm{apply}\left(Ns,i\right)\right),\forall hcuts\in \left(\forall i\in iota,\mathrm{MemLp}\left(\mathrm{kernel}\left(c,\mathrm{apply}\left(Ns,i\right)\right),2,volume\right)\right),\mathrm{Tendsto}\left(Ns,l,atTop\right)\Rightarrow \mathrm{Tendsto}\left((i:iota\mapsto \mathrm{toLp}\left(\mathrm{apply}\left(hcuts,i\right),\mathrm{kernel}\left(c,\mathrm{apply}\left(Ns,i\right)\right)\right)),l,\mathrm{nhds}\left(\mathrm{toLp}\left(hq,\mathrm{highpassKernel}\left(c\right)\right)\right)\right)\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

For every c>0, q(c) is measurable and belongs to real Lebesgue L2. For every N>=c and every MemLp witness for the actual kernel(c,N), the squared L2 error is 4*pi/N. Every filter of real upper cutoffs tending to infinity gives L2 convergence, without requiring a nontrivial filter.

The finite interval cancellation uses the existing positive Euler normalization. Away from x=0, kernel(c,N,x)=q(c,x)-q(N,x). The exact Gram integral at the scale N gives the squared error. At N=c the finite kernel is zero; closed frequency endpoints remain qualified almost everywhere.D5/S3/Fourier/Asymptotics/CosineNormalizedRemainder.positive_normalization``D5/S3/Fourier/Asymptotics/CosineIntegralGram.result``D5/S3/Fourier/Asymptotics/CosineCutoffKernel.result

This lemma is consumed by the actual high-pass convolution construction and by Gaussian kernel convergence. Its direct reuse and normalization steps receive no separate mathematical-content credit.

Theorem 1.2 (Ordinary convolution on the full complex and real L2 spaces).

$$\forall c\in \mathbb{R},0<c\Rightarrow \left(\exists C\in \mathrm{ContinuousLinearMap}\left(\mathbb{C},\mathrm{Lp}\left(\mathbb{C},2,volume\right),\mathrm{Lp}\left(\mathbb{C},2,volume\right)\right),\left(\forall f\in \mathrm{Lp}\left(\mathbb{C},2,volume\right),\forall x\in \mathbb{R},\mathrm{Integrable}\left((y:\mathbb{R}\mapsto \mathrm{apply}\left((z:\mathbb{R}\mapsto \mathrm{ofReal}\left(\mathrm{apply}\left(\mathrm{highpassKernel}\left(c\right),z\right)\right)),x-y\right)\cdot \mathrm{apply}\left(f,y\right)),volume\right)\right)\wedge \left(\left(\forall f\in \mathrm{Lp}\left(\mathbb{C},2,volume\right),\mathrm{AEEq}\left(\mathrm{coeFn}\left(\mathrm{apply}\left(C,f\right)\right),(x:\mathbb{R}\mapsto \mathrm{integral}\left((y:\mathbb{R}\mapsto \mathrm{apply}\left((z:\mathbb{R}\mapsto \mathrm{ofReal}\left(\mathrm{apply}\left(\mathrm{highpassKernel}\left(c\right),z\right)\right)),x-y\right)\cdot \mathrm{apply}\left(f,y\right)),volume\right)),volume\right)\right)\wedge \left(\mathrm{norm}\left(C\right)\le \frac{2\cdot \pi }{c}\wedge \left(\exists Cr\in \mathrm{ContinuousLinearMap}\left(\mathbb{R},\mathrm{Lp}\left(\mathbb{R},2,volume\right),\mathrm{Lp}\left(\mathbb{R},2,volume\right)\right),\left(\forall f\in \mathrm{Lp}\left(\mathbb{R},2,volume\right),\mathrm{AEEq}\left(\mathrm{coeFn}\left(\mathrm{apply}\left(Cr,f\right)\right),(x:\mathbb{R}\mapsto \mathrm{integral}\left((y:\mathbb{R}\mapsto \mathrm{apply}\left(\mathrm{highpassKernel}\left(c\right),x-y\right)\cdot \mathrm{apply}\left(f,y\right)),volume\right)),volume\right)\right)\wedge \mathrm{norm}\left(Cr\right)\le \frac{2\cdot \pi }{c}\right)\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

HC=Lp(C,2,volume) and HR=Lp(R,2,volume). The complex convolution rows are integrable for every L2 input and every real x. One bounded complex operator represents these ordinary integrals almost everywhere. Its real restriction is obtained using the ofReal and real-part maps and has the same bound 2*pi/c.

The finite operators are Cauchy in operator norm by the existing cutoff tail estimate. Their L2 kernel limit identifies the ordinary convolution integral through the continuous bilinear L2 pairing and translation-reflection isometry. An almost-everywhere convergent subsequence of each operator output identifies its L2 representative with that pointwise integral limit.D5/S3/Fourier/Asymptotics/CosineCutoffKernel.actual_cutoff_convolution``D5/S3/Fourier/Asymptotics/CosineCutoffKernel.pair``D5/S3/Fourier/Asymptotics/CosineCutoffKernel.pair_eq``D5/S3/Fourier/Asymptotics/CosineCutoffKernel.product_integrable

No absolute integrability of q is assumed. The pinned forward Fourier convention is exp(-2piixxi); the finite physical cutoff c is therefore at c/(2pi) in xi, or at c in the original variable zeta=2pi*xi.

Theorem 1.3 (The actual weighted operator, onto density isometry, and cutoff limit).

$$\forall r\in \mathbb{R},\forall alpha\in \mathbb{R},0<r\Rightarrow \left(r<1\Rightarrow \left(\exists A\in \mathrm{ContinuousLinearMap}\left(\mathbb{R},\mathrm{Lp}\left(\mathbb{R},2,\mathrm{prod}\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{prod}\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),\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(\mathrm{apply}\left(A,K\right),f\right)\right),(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(f,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(\forall c\in \mathbb{R},0<c\Rightarrow \left(\exists C\in \mathrm{ContinuousLinearMap}\left(\mathbb{R},\mathrm{Lp}\left(\mathbb{R},2,volume\right),\mathrm{Lp}\left(\mathbb{R},2,volume\right)\right),\exists K\in \mathrm{Lp}\left(\mathbb{R},2,\mathrm{prod}\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),\left(\forall f\in \mathrm{Lp}\left(\mathbb{R},2,volume\right),\mathrm{AEEq}\left(\mathrm{coeFn}\left(\mathrm{apply}\left(C,f\right)\right),(x:\mathbb{R}\mapsto \mathrm{integral}\left((y:\mathbb{R}\mapsto \mathrm{apply}\left(\mathrm{highpassKernel}\left(c\right),x-y\right)\cdot \mathrm{apply}\left(f,y\right)),volume\right)),volume\right)\right)\wedge \left(\mathrm{norm}\left(C\right)\le \frac{2\cdot \pi }{c}\wedge \left(\mathrm{AEEq}\left(\mathrm{coeFn}\left(K\right),(z:\mathrm{Product}\left(\mathbb{R},\mathbb{R}\right)\mapsto \mathrm{apply}\left(\mathrm{highpassKernel}\left(c\right),\mathrm{fst}\left(z\right)-\mathrm{snd}\left(z\right)\right)),\mathrm{prod}\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(\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(\mathrm{apply}\left(A,K\right),f\right)\right),(x:\mathbb{R}\mapsto \mathrm{integral}\left((y:\mathbb{R}\mapsto \mathrm{apply}\left(\mathrm{highpassKernel}\left(c\right),x-y\right)\cdot \mathrm{apply}\left(f,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 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{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(\mathrm{highpassKernel}\left(c\right),x-y\right)\cdot \mathrm{apply}\left(f,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)\right)\wedge \left(\mathrm{norm}\left(\mathrm{apply}\left(A,K\right)\right)\le \frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \frac{2\cdot \pi }{c}\wedge \left(\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),\exists M\in \mathrm{ContinuousLinearMap}\left(\mathbb{R},\mathrm{Lp}\left(\mathbb{R},2,volume\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(f,x\right)),volume\right)\right)\wedge \left(\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(h,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)\wedge \left(\left(\forall h\in \mathrm{Lp}\left(\mathbb{R},2,volume\right),\mathrm{AEEq}\left(\mathrm{coeFn}\left(\mathrm{apply}\left(M,h\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(h,x\right)),volume\right)\right)\wedge \left(\mathrm{norm}\left(M\right)\le \mathrm{sqrt}\left(\frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\right)\wedge \mathrm{compose}\left(\mathrm{asCLM}\left(U\right),\mathrm{compose}\left(\mathrm{apply}\left(A,K\right),\mathrm{asCLM}\left(\mathrm{symm}\left(U\right)\right)\right)\right)=\mathrm{compose}\left(M,\mathrm{compose}\left(C,M\right)\right)\right)\right)\right)\right)\wedge \left(\exists Ks\in \left(\forall N\in \mathbb{R},c\le N\to \mathrm{Lp}\left(\mathbb{R},2,\mathrm{prod}\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),\left(\forall N\in \mathbb{R},\forall hN\in c\le N,\mathrm{AEEq}\left(\mathrm{coeFn}\left(\mathrm{apply}\left(Ks,N,hN\right)\right),(z:\mathrm{Product}\left(\mathbb{R},\mathbb{R}\right)\mapsto \mathrm{apply}\left(\mathrm{kernel}\left(c,N\right),\mathrm{fst}\left(z\right)-\mathrm{snd}\left(z\right)\right)),\mathrm{prod}\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)\wedge \left(\left(\forall N\in \mathbb{R},\forall hN\in c\le N,\mathrm{norm}\left(\mathrm{apply}\left(A,\mathrm{apply}\left(Ks,N,hN\right)\right)\right)\le \frac{1}{4\cdot \pi \cdot \mathrm{sqrt}\left(\frac{1+r}{2}\cdot \frac{1-r}{2}\right)}\cdot \frac{2\cdot \pi }{c}\right)\wedge \left(\forall iota\in Type,\forall l\in \mathrm{Filter}\left(iota\right),\forall Ns\in iota\to \mathbb{R},\forall hNs\in \left(\forall i\in iota,c\le \mathrm{apply}\left(Ns,i\right)\right),\mathrm{Tendsto}\left(Ns,l,atTop\right)\Rightarrow \left(\mathrm{Tendsto}\left((i:iota\mapsto \mathrm{apply}\left(Ks,\mathrm{apply}\left(Ns,i\right),\mathrm{apply}\left(hNs,i\right)\right)),l,\mathrm{nhds}\left(K\right)\right)\wedge \mathrm{Tendsto}\left((i:iota\mapsto \mathrm{apply}\left(A,\mathrm{apply}\left(Ks,\mathrm{apply}\left(Ns,i\right),\mathrm{apply}\left(hNs,i\right)\right)\right)),l,\mathrm{nhds}\left(\mathrm{apply}\left(A,K\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

For every r,alpha with 0<r<1, 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(ENNReal.ofReal(rho)). This is the finite, unnormalized original Gaussian measure.

A is the existing continuous linear factory for the actual integral kernel operators. For every c>0 the displayed kernel K represents q(c,x-y); A(K) has that weighted integral representative and almost-everywhere integrable rows. C is the actual ordinary real convolution supplied above. U is an onto real linear isometry, with both forward density and inverse division representatives. M multiplies by sqrt(rho). The identity conjugates A(K) with U; A(K) is not defined as the sandwich.

For every N>=c, Ks(N,hN) represents the actual finite kernel(c,N,x-y), has the same bound, and converges with A(Ks) for every real cutoff filter tending to infinity. This uses the Gaussian difference-kernel L2 estimate and the actual operator factory continuity.D5/S3/Fourier/Asymptotics/CosineCutoffKernel.actual_cutoff_real``D5/S3/Fourier/Asymptotics/CosineCutoffKernel.actual_weighted_cutoff``D5/S3/Fourier/Asymptotics/CosineCutoffKernel/GaussianWeight.gaussian_weighted_kernel``D5/S3/Fourier/Asymptotics/CosineCutoffKernel/GaussianWeight.weighted_integral_operator``D5/S3/Fourier/Asymptotics/CosineCutoffKernel/GaussianWeight.density_unitary``D5/S3/Fourier/Asymptotics/CosineCutoffKernel/GaussianWeight.cutoff_conjugacy

The norm bound is c0*(2pi/c). Substituting c=(pi/2)exp(s+t) gives the first original operator bound for every real s,t. Scaling the actual kernel by exp((s+t)/2) and using t>=t0 gives the compact-window bound with C_I=(2pic0/(pi/2))*exp(-t0/2), including singleton windows. These substitutions are exact applications. This result makes no spectral-series, covariance-asymptotic, path-convergence or completed-field mixing claim.

References

• Truth anchor: D5/S3/Fourier/Asymptotics/CosineCutoffKernel.actual_cutoff_convolution
• Truth anchor: D5/S3/Fourier/Asymptotics/CosineCutoffKernel.actual_cutoff_real
• Truth anchor: D5/S3/Fourier/Asymptotics/CosineCutoffKernel.actual_weighted_cutoff
• Truth anchor: D5/S3/Fourier/Asymptotics/CosineCutoffKernel.pair
• Truth anchor: D5/S3/Fourier/Asymptotics/CosineCutoffKernel.pair_eq
• Truth anchor: D5/S3/Fourier/Asymptotics/CosineCutoffKernel.product_integrable
• Truth anchor: D5/S3/Fourier/Asymptotics/CosineCutoffKernel.result
• Truth anchor: D5/S3/Fourier/Asymptotics/CosineCutoffKernel/GaussianWeight.cutoff_conjugacy
• Truth anchor: D5/S3/Fourier/Asymptotics/CosineCutoffKernel/GaussianWeight.density_unitary
• Truth anchor: D5/S3/Fourier/Asymptotics/CosineCutoffKernel/GaussianWeight.gaussian_weighted_kernel
• Truth anchor: D5/S3/Fourier/Asymptotics/CosineCutoffKernel/GaussianWeight.weighted_integral_operator
• Truth anchor: D5/S3/Fourier/Asymptotics/CosineCutoffKernel/Highpass.actual_highpass_convolution
• Truth anchor: D5/S3/Fourier/Asymptotics/CosineCutoffKernel/Highpass.actual_highpass_operator
• Truth anchor: D5/S3/Fourier/Asymptotics/CosineCutoffKernel/Highpass.highpassKernel
• Truth anchor: D5/S3/Fourier/Asymptotics/CosineCutoffKernel/Highpass.highpass_limit
• Truth anchor: D5/S3/Fourier/Asymptotics/CosineIntegralGram.result
• Truth anchor: D5/S3/Fourier/Asymptotics/CosineIntegralLattice.cosineIntegral
• Truth anchor: D5/S3/Fourier/Asymptotics/CosineNormalizedRemainder.positive_normalization
• Dependency: D5/S3/Fourier/Asymptotics/CosineCutoffKernel
• Dependency: D5/S3/Fourier/Asymptotics/CosineIntegralGram