離散版Fourierの反転公式

$ \forall N\in\N:{\mathcal{F}_{d,N}}^{-1}(\mathcal{F}_{d,N}(X_\bullet))=X_\bullet

一般に通用する名前はなさそう

証明

$ \forall N\in\N\forall n\in\Z:

$ {\mathcal{F}_{d,N}}^{-1}(\mathcal{F}_N(X_\bullet))_n=\sum_{0\le k<N}\frac1N\sum_{0\le m<N}X_ne^{-2\pi\frac mNki}e^{2\pi\frac kNni}

$ = \frac1N\sum_{(k,m)\in [0,N\llbracket^2}X_ne^{2\pi\frac kN(n-m)i}

$ = \frac1NX_n\sum_{(k,m)\in [0,N\llbracket^2}e^{2\pi\frac kN(n-m)i}

$ = \frac1NX_n\sum_{0\le m<N}\left(\frac{\left(e^{2\pi i\frac{n-m}{N}}\right)^N-\left(e^{2\pi i\frac{n-m}{N}}\right)^0}{e^{2\pi i\frac{n-m}{N}}-1}\llbracket\lnot N\backslash(n-m)\rrbracket+\llbracket N\backslash(n-m)\rrbracket\sum_{0\le k<N}1\right)

$ = \frac1NX_n\sum_{0\le m<N}\left(\frac{e^{2\pi i(n-m)}-1}{e^{2\pi i\frac{n-m}{N}}-1}\llbracket\lnot N\backslash(n-m)\rrbracket+N\llbracket N\backslash(n-m)\rrbracket\right)

$ = \frac1NX_n\sum_{0\le m<N}\left(\frac{1-1}{e^{2\pi i\frac{n-m}{N}}-1}\llbracket\lnot N\backslash(n-m)\rrbracket+N\llbracket N\backslash(n-m)\rrbracket\right)

$ \because n-m\in\Z

$ = \frac1NX_n\sum_{0\le m<N}N\llbracket N\backslash(n-m)\rrbracket

$ = X_n\sum_{0\le m<N}\llbracket N\backslash(n-m)\rrbracket

$ = X_n\sum_{m}\llbracket\exist l\in\Z:0\le m=n+lN<N\rrbracket

$ = X_n\sum_{m}\llbracket\exist l\in\Z:m=n+lN\land-\frac nN\le l<1-\frac nN\rrbracket

$ = X_n

$ \underline{\therefore\forall N\in\N:{\mathcal{F}_{d,N}}^{-1}(\mathcal{F}_{d,N}(X_\bullet))=X_\bullet\quad}_\blacksquare