Laguerre-Chebyshev Duality

Abstract

The Laguerre time observation equals the Chebyshev derivative jet of one budget curve.

Theorem 1.1 (Laguerre-Chebyshev duality).

$$\forall nu\in \mathrm{Measure}\left(\mathrm{Real}\left(\right)\right),n\in \mathrm{Nat}\left(\right),u\in \mathrm{Real}\left(\right),p\in \mathrm{Fin}\left(n+1\right)\to \mathrm{Real}\left(\right),\left(\mathrm{map}\left(\mathrm{lambda}\left(xi,\mathrm{neg}\left(xi\right)\right),nu\right)=nu\wedge \left(1\le n\wedge \left(0<u\wedge \left(\left(\forall x\in \mathrm{Real}\left(\right),\mathrm{ChebyshevT}\left(\mathrm{Int}\left(\right),n,1-2\cdot x\right)=\mathrm{sum}\left(\mathrm{Fin}\left(n+1\right),\mathrm{lambda}\left(k,p\left(k\right)\cdot \mathrm{pow}\left(x,k\right)\right)\right)\right)\wedge \mathrm{Integrable}\left(\mathrm{lambda}\left(xi,\frac{1}{\mathrm{pow}\left(xi,2\right)+u}\right),nu\right)\right)\right)\right)\right)\Rightarrow letscale:\mathrm{Real}\left(\right)=\mathrm{sqrt}\left(u\right);letbudget:\mathrm{Real}\left(\right)\to \mathrm{Real}\left(\right)=\mathrm{lambda}\left(v,\mathrm{integral}\left(nu,\mathrm{lambda}\left(xi,\frac{1}{\mathrm{pow}\left(xi,2\right)+v}\right)\right)\right);\mathrm{complex}\left(budget\left(u\right)\right)-\mathrm{complex}\left(2\cdot scale\right)\cdot \mathrm{integral}\left(t,\mathrm{Real}\left(\right),\mathrm{complex}\left(\exp \left(\mathrm{neg}\left(scale\cdot t\right)\right)\cdot \mathrm{laguerreOne}\left(n-1,2\cdot scale\cdot t\right)\right)\cdot \mathrm{resolventCorrelation}\left(\mathrm{resolventWeightedMeasure}\left(nu,scale\right),t\right),\mathrm{restrict}\left(\mathrm{volume}\left(\right),\mathrm{Ioi}\left(0\right)\right)\right)=\mathrm{complex}\left(\mathrm{sum}\left(\mathrm{Fin}\left(n+1\right),\mathrm{lambda}\left(k,p\left(k\right)\cdot \mathrm{pow}\left(u,k\right)\cdot \frac{\mathrm{pow}\left(\mathrm{neg}\left(1\right),k\right)}{\mathrm{factorial}\left(k\right)}\cdot \mathrm{iteratedDeriv}\left(k,budget,u\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Weil/CayleyLaguerre/LaguerreChebyshevDuality.laguerre_chebyshev_duality (✓ std3). ∎

Source. Repository-derived.

Commentary.

The positive square scale is passed to the frozen resolventWeightedMeasure owner. The proof reuses the second conjunct of the frozen laguerre_moment_tomography theorem for the time observation, then the scale-jet identity identifies its Cayley moment with the derivative sum.

References

• Truth anchor: D5/S3/Weil/CayleyLaguerre/LaguerreChebyshevDuality.laguerre_chebyshev_duality
• Dependency: D5/S3/Analytic/LiCausalTrichotomy
• Dependency: D5/S3/Weil/Budget/PositiveCayleyScaleTransport
• Dependency: D5/S3/Weil/CayleyLaguerre/CayleyMomentTransport
• Dependency: D5/S3/Weil/TestFunctions/CayleyLaguerreMomentTomography