Cayley Moment Transport

Abstract

Cayley moments have a finite derivative jet and a geometric scale-transport tail bound.

Theorem 1.1 (Chebyshev-Stieltjes jet).

$$\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(\mathrm{add}\left(n,1\right)\right)\to \mathrm{Real}\left(\right),\left(\mathrm{map}\left(\mathrm{lambda}\left(\mathrm{typed}\left(xi,\mathrm{Real}\left(\right)\right),\mathrm{neg}\left(xi\right)\right),nu\right)=nu\wedge \left(0<u\wedge \left(\left(\forall x\in \mathrm{Real}\left(\right),\mathrm{ChebyshevT}\left(\mathrm{Int}\left(\right),n,\mathrm{sub}\left(1,\mathrm{mul}\left(2,x\right)\right)\right)=\mathrm{sum}\left(\mathrm{Fin}\left(\mathrm{add}\left(n,1\right)\right),\mathrm{lambda}\left(\mathrm{typed}\left(k,\mathrm{Fin}\left(\mathrm{add}\left(n,1\right)\right)\right),\mathrm{mul}\left(p\left(k\right),\mathrm{pow}\left(x,k\right)\right)\right)\right)\right)\wedge \mathrm{Integrable}\left(\mathrm{lambda}\left(\mathrm{typed}\left(xi,\mathrm{Real}\left(\right)\right),\frac{1}{\mathrm{add}\left(\mathrm{pow}\left(xi,2\right),u\right)}\right),nu\right)\right)\right)\right)\Rightarrow \mathrm{integral}\left(nu,\mathrm{lambda}\left(\mathrm{typed}\left(xi,\mathrm{Real}\left(\right)\right),\frac{\mathrm{pow}\left(\frac{\mathrm{add}\left(\mathrm{ofReal}\left(xi\right),\mathrm{mul}\left(I\left(\right),\mathrm{sqrt}\left(u\right)\right)\right)}{\mathrm{sub}\left(\mathrm{ofReal}\left(xi\right),\mathrm{mul}\left(I\left(\right),\mathrm{sqrt}\left(u\right)\right)\right)},n\right)}{\mathrm{add}\left(\mathrm{pow}\left(xi,2\right),u\right)}\right)\right)=\mathrm{ofReal}\left(\mathrm{sum}\left(\mathrm{Fin}\left(\mathrm{add}\left(n,1\right)\right),\mathrm{lambda}\left(\mathrm{typed}\left(k,\mathrm{Fin}\left(\mathrm{add}\left(n,1\right)\right)\right),\mathrm{mul}\left(p\left(k\right),\mathrm{pow}\left(u,k\right),\frac{\mathrm{pow}\left(\mathrm{neg}\left(1\right),k\right)}{\mathrm{factorial}\left(k\right)},\mathrm{iteratedDeriv}\left(k,\mathrm{lambda}\left(\mathrm{typed}\left(v,\mathrm{Real}\left(\right)\right),\mathrm{integral}\left(nu,\mathrm{lambda}\left(\mathrm{typed}\left(xi,\mathrm{Real}\left(\right)\right),\frac{1}{\mathrm{add}\left(\mathrm{pow}\left(xi,2\right),v\right)}\right)\right)\right),u\right)\right)\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

The even measure, positive square scale, coefficient family, polynomial identity, and resolvent integrability condition at that scale are all displayed.

Evenness identifies the full complex Cayley moment with its real part; the proof then uses the shifted Chebyshev polynomial and differentiates under a locally dominated integral.

Theorem 1.2 (Budget transport error).

$$\forall nu\in \mathrm{Measure}\left(\mathrm{Real}\left(\right)\right),a\in \mathrm{Real}\left(\right),b\in \mathrm{Real}\left(\right),M\in \mathrm{Nat}\left(\right),\left(\mathrm{map}\left(\mathrm{lambda}\left(\mathrm{typed}\left(xi,\mathrm{Real}\left(\right)\right),\mathrm{neg}\left(xi\right)\right),nu\right)=nu\wedge \left(0<a\wedge \left(0<b\wedge \mathrm{Integrable}\left(\mathrm{lambda}\left(\mathrm{typed}\left(xi,\mathrm{Real}\left(\right)\right),\frac{1}{\mathrm{add}\left(\mathrm{pow}\left(xi,2\right),\mathrm{pow}\left(a,2\right)\right)}\right),nu\right)\right)\right)\right)\Rightarrow \mathrm{norm}\left(\mathrm{sub}\left(\mathrm{ofReal}\left(\mathrm{integral}\left(nu,\mathrm{lambda}\left(\mathrm{typed}\left(xi,\mathrm{Real}\left(\right)\right),\frac{1}{\mathrm{add}\left(\mathrm{pow}\left(xi,2\right),\mathrm{pow}\left(b,2\right)\right)}\right)\right)\right),\mathrm{mul}\left(\mathrm{ofReal}\left(\frac{a}{b}\right),\mathrm{add}\left(\mathrm{ofReal}\left(\mathrm{integral}\left(nu,\mathrm{lambda}\left(\mathrm{typed}\left(xi,\mathrm{Real}\left(\right)\right),\frac{1}{\mathrm{add}\left(\mathrm{pow}\left(xi,2\right),\mathrm{pow}\left(a,2\right)\right)}\right)\right)\right),\mathrm{mul}\left(2,\mathrm{sum}\left(\mathrm{range}\left(M\right),\mathrm{lambda}\left(\mathrm{typed}\left(k,\mathrm{Nat}\left(\right)\right),\mathrm{mul}\left(\mathrm{ofReal}\left(\mathrm{pow}\left(\mathrm{neg}\left(\frac{\mathrm{sub}\left(a,b\right)}{\mathrm{add}\left(a,b\right)}\right),\mathrm{add}\left(k,1\right)\right)\right),\mathrm{integral}\left(nu,\mathrm{lambda}\left(\mathrm{typed}\left(xi,\mathrm{Real}\left(\right)\right),\frac{\mathrm{pow}\left(\frac{\mathrm{add}\left(\mathrm{ofReal}\left(xi\right),\mathrm{mul}\left(I\left(\right),a\right)\right)}{\mathrm{sub}\left(\mathrm{ofReal}\left(xi\right),\mathrm{mul}\left(I\left(\right),a\right)\right)},\mathrm{add}\left(k,1\right)\right)}{\mathrm{add}\left(\mathrm{pow}\left(xi,2\right),\mathrm{pow}\left(a,2\right)\right)}\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\le \mathrm{mul}\left(\frac{\mathrm{mul}\left(2,a\right)}{b},\mathrm{integral}\left(nu,\mathrm{lambda}\left(\mathrm{typed}\left(xi,\mathrm{Real}\left(\right)\right),\frac{1}{\mathrm{add}\left(\mathrm{pow}\left(xi,2\right),\mathrm{pow}\left(a,2\right)\right)}\right)\right),\frac{\mathrm{pow}\left(\mathrm{abs}\left(\frac{\mathrm{sub}\left(a,b\right)}{\mathrm{add}\left(a,b\right)}\right),\mathrm{add}\left(M,1\right)\right)}{\mathrm{sub}\left(1,\mathrm{abs}\left(\frac{\mathrm{sub}\left(a,b\right)}{\mathrm{add}\left(a,b\right)}\right)\right)}\right)$$

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

Source. Repository-derived.

Commentary.

The two positive scales, truncation order, even measure, and resolvent integrability premise are displayed explicitly.

The proof expands every moment from the Cayley coordinate, reduces scale transport to the Poisson kernel, and integrates its finite geometric remainder.

References

• Truth anchor: D5/S3/Weil/CayleyLaguerre/CayleyMomentTransport.budget_transport_error
• Truth anchor: D5/S3/Weil/CayleyLaguerre/CayleyMomentTransport.chebyshev_stieltjes_jet