Cayley-Laguerre Moment Tomography

Abstract

Scaled Laguerre kernels recover even Cayley moments and control finite windows.

Theorem 1.1 (Cayley-Laguerre identity).

$$\forall n\in \mathrm{Natural}\left(\right),a\in \mathrm{Real}\left(\right),xi\in \mathrm{Real}\left(\right),\left(1\le n\wedge 0<a\right)\Rightarrow \mathrm{pow}\left(\mathrm{cayleyCharacter}\left(a,xi\right),n\right)=1-\mathrm{integral}\left(t,\mathrm{Real}\left(\right),\mathrm{complex}\left(\mathrm{laguerreKernel}\left(n,a,t\right)\right)\cdot \exp \left(\mathrm{neg}\left(I\left(\right)\cdot xi\cdot t\right)\right),\mathrm{restrict}\left(\mathrm{volume}\left(\right),\mathrm{Ioi}\left(0\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Weil/TestFunctions/CayleyLaguerreMomentTomography.cayley_laguerre_identity (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every positive scale and positive natural order, the all-pass Cayley power is one minus the negative-sign Fourier transform of the causal scaled Laguerre kernel. The kernel is constructed from the repository’s canonical generalized Laguerre finite sum.

Theorem 1.2 (Laguerre moment tomography).

$$\forall rho\in \mathrm{Measure}\left(\mathrm{Real}\left(\right)\right),n\in \mathrm{Natural}\left(\right),a\in \mathrm{Real}\left(\right),\left(\mathrm{IsFiniteMeasure}\left(rho\right)\wedge \left(\mathrm{map}\left(\mathrm{lambda}\left(xi,\mathrm{neg}\left(xi\right)\right),rho\right)=rho\wedge \left(1\le n\wedge 0<a\right)\right)\right)\Rightarrow \left(\mathrm{cayleyMoment}\left(rho,n,a\right)=\mathrm{complex}\left(\mathrm{spectralMass}\left(rho\right)\right)-\mathrm{integral}\left(t,\mathrm{Real}\left(\right),\mathrm{complex}\left(\mathrm{laguerreKernel}\left(n,a,t\right)\right)\cdot \mathrm{resolventCorrelation}\left(rho,t\right),\mathrm{restrict}\left(\mathrm{volume}\left(\right),\mathrm{Ioi}\left(0\right)\right)\right)\wedge \mathrm{cayleyMoment}\left(rho,n,a\right)=\mathrm{complex}\left(\mathrm{spectralMass}\left(rho\right)\right)-\mathrm{complex}\left(2\cdot a\right)\cdot \mathrm{integral}\left(t,\mathrm{Real}\left(\right),\mathrm{complex}\left(\exp \left(\mathrm{neg}\left(a\cdot t\right)\right)\cdot \mathrm{laguerreOne}\left(n-1,2\cdot a\cdot t\right)\right)\cdot \mathrm{resolventCorrelation}\left(rho,t\right),\mathrm{restrict}\left(\mathrm{volume}\left(\right),\mathrm{Ioi}\left(0\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Weil/TestFunctions/CayleyLaguerreMomentTomography.laguerre_moment_tomography (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let rho be a finite even positive measure on the real line. Both source equalities are public: first in named kernel form and then with the factor 2a and the generalized Laguerre polynomial displayed. Evenness identifies the negative-sign Fourier integral with the positive-sign resolvent correlation.

Theorem 1.3 (Finite-window moment tube).

$$\forall rho\in \mathrm{Measure}\left(\mathrm{Real}\left(\right)\right),n\in \mathrm{Natural}\left(\right),a\in \mathrm{Real}\left(\right),L\in \mathrm{Real}\left(\right),\left(\mathrm{IsFiniteMeasure}\left(rho\right)\wedge \left(\mathrm{map}\left(\mathrm{lambda}\left(xi,\mathrm{neg}\left(xi\right)\right),rho\right)=rho\wedge \left(1\le n\wedge \left(0<a\wedge 0\le L\right)\right)\right)\right)\Rightarrow \mathrm{norm}\left(\mathrm{cayleyMoment}\left(rho,n,a\right)-\mathrm{windowMoment}\left(rho,n,a,L\right)\right)\le \mathrm{spectralMass}\left(rho\right)\cdot \mathrm{laguerreTail}\left(n,a,L\right)$$

Proof. Machine-checked in Lean as D5/S3/Weil/TestFunctions/CayleyLaguerreMomentTomography.finite_window_moment_tube (✓ std3). ∎

Source. Repository-derived.

Commentary.

For a nonnegative window length, subtracting the truncated estimator leaves exactly the kernel-correlation tail. The norm of every correlation value is bounded by the total spectral mass, giving the displayed mass-times-tail estimate.

Theorem 1.4 (Moment affine budget law).

$$\forall n\in \mathrm{Natural}\left(\right),a\in \mathrm{Real}\left(\right),L\in \mathrm{Real}\left(\right),H0\in \mathrm{Real}\left(\right)\to \mathrm{Real}\left(\right),R\in \mathrm{Real}\left(\right),\left(0<a\wedge \mathrm{ContinuousOn}\left(H0,\mathrm{Icc}\left(0,2\cdot L\right)\right)\right)\Rightarrow letA:\mathrm{Real}\left(\right)=\mathrm{neg}\left(\mathrm{integral}\left(t,\mathrm{Real}\left(\right),\mathrm{laguerreKernel}\left(n,a,t\right)\cdot H0\left(t\right),\mathrm{restrict}\left(\mathrm{volume}\left(\right),\mathrm{Ioc}\left(0,2\cdot L\right)\right)\right)\right);letB:\mathrm{Real}\left(\right)=1-\mathrm{integral}\left(t,\mathrm{Real}\left(\right),\mathrm{laguerreKernel}\left(n,a,t\right)\cdot \cosh \left(a\cdot t\right),\mathrm{restrict}\left(\mathrm{volume}\left(\right),\mathrm{Ioc}\left(0,2\cdot L\right)\right)\right);\mathrm{budgetWindowMoment}\left(n,a,L,H0,R\right)=A+B\cdot R$$

Proof. Machine-checked in Lean as D5/S3/Weil/TestFunctions/CayleyLaguerreMomentTomography.moment_affine_budget_law (✓ std3). ∎

Source. Repository-derived.

Commentary.

The particular correlation H0 is real-valued and continuous on the finite window, as supplied by the local second-order equation in the source. The estimator is constructed from H0 plus R cosh(at). The displayed definitions of A and B are literal finite-window integrals, and integral linearity proves the affine equality.

References

• Truth anchor: D5/S3/Weil/TestFunctions/CayleyLaguerreMomentTomography.cayley_laguerre_identity
• Truth anchor: D5/S3/Weil/TestFunctions/CayleyLaguerreMomentTomography.finite_window_moment_tube
• Truth anchor: D5/S3/Weil/TestFunctions/CayleyLaguerreMomentTomography.laguerre_moment_tomography
• Truth anchor: D5/S3/Weil/TestFunctions/CayleyLaguerreMomentTomography.moment_affine_budget_law
• Dependency: D5/S3/Analytic/LiCausalTrichotomy