Finite Lag Autocorrelation

Abstract

A finite real signal has its exact lag autocorrelation as the Fourier coefficients of its squared modulus.

Theorem 1.1 (Finite signals expand by lag autocorrelation).

$$\begin{gathered} \forall T\in \mathbb{N},f:\mathrm{Fin}\left(T+1\right)\Rightarrow \mathbb{R},theta\in \mathbb{R},\text{let }p:\mathbb{C}[X,X^{-1}]=\sum _{0\le n\le T}{f}_n{X}^n,A=\mathrm{invert}\left(p\right)\times p,(\forall m\in \mathbb{Z},A_m=\sum _{n\in \mathrm{Fin}\left(T+1\right)}{f}_n{p}_{n+m})\wedge \\ (\mathrm{normSq}\left(\mathrm{finiteSignal}\left(f,\exp \left(itheta\right)\right)\right)=\sum _{-T\le m\le T}{A}_m\exp {\left(itheta\right)}^m). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S0/Asymptotics/Interference/FiniteLagAutocorrelation.finite_lag_autocorrelation_expansion (✓ std3). ∎

Source. Repository-derived.

Commentary.

For a real signal indexed by Fin(T+1), p is its Laurent coefficient polynomial, extended by zero away from indices zero through T. The Laurent product A = invert(p) times p is constructed from that signal.

The first public conjunct proves that the coefficient A_m is the lag sum of f_n times f_(n+m), with the zero extension supplied by p. The second public conjunct evaluates the same Laurent product on the unit circle and obtains the squared modulus over exactly the possible lags.

The proof imports the earlier finite pairwise expansion only as the canonical finite-signal primitive. Laurent convolution, inversion, support bounds, and unit-circle conjugation establish the stronger lag-indexed statement.

References

• Truth anchor: D5/S0/Asymptotics/Interference/FiniteLagAutocorrelation.finite_lag_autocorrelation_expansion
• Dependency: D5/S0/Asymptotics/Interference/FiniteAutocorrelation