Laguerre-Li Bridge

Abstract

The natural half-scale Cayley moments give the Laguerre formula for Li curvature.

Theorem 1.1 (Laguerre-Li bridge).

$$\forall rho\in \mathrm{Measure}\left(\mathrm{Real}\left(\right)\right),liCoefficient\in \mathrm{Natural}\left(\right)\to \mathrm{Real}\left(\right),\left(\left(\left(\mathrm{IsFiniteMeasure}\left(rho\right)\wedge \mathrm{map}\left(\mathrm{lambda}\left(xi,\mathrm{neg}\left(xi\right)\right),rho\right)=rho\right)\wedge \mathrm{spectralMass}\left(rho\right)=2\cdot liCoefficient\left(1\right)\right)\wedge \left(\forall k\in \mathrm{Natural}\left(\right),1\le k\Rightarrow \mathrm{realPart}\left(\mathrm{cayleyMoment}\left(rho,k,\frac{1}{2}\right)\right)=liCoefficient\left(k+1\right)-2\cdot liCoefficient\left(k\right)+liCoefficient\left(k-1\right)\right)\right)\Rightarrow \left(\forall n\in \mathrm{Natural}\left(\right),1\le n\Rightarrow liCoefficient\left(n+1\right)-2\cdot liCoefficient\left(n\right)+liCoefficient\left(n-1\right)=2\cdot liCoefficient\left(1\right)-\mathrm{integral}\left(t,\mathrm{Real}\left(\right),\exp \left(\mathrm{neg}\left(\frac{t}{2}\right)\right)\cdot \mathrm{laguerreOne}\left(n-1,t\right)\cdot \mathrm{realPart}\left(\mathrm{resolventCorrelation}\left(rho,t\right)\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/LaguerreLiBridge.laguerre_li_bridge (✓ std3). ∎

Source. Repository-derived.

Commentary.

For a finite even real-line spectral measure, assume the natural half-scale Cayley moments are the discrete curvatures of the supplied Li sequence and the total mass is twice its first coefficient. Specializing the canonical Cayley-Laguerre tomography identity gives the displayed real resolvent-correlation integral.

References

• Truth anchor: D5/S3/Weil/TestFunctions/LaguerreLiBridge.laguerre_li_bridge
• Dependency: D5/S3/Weil/TestFunctions/CayleyLaguerreMomentTomography