DFT Matrices and Surrounding Lemmas

[MohanadAhmed]

Main Changes

DFT Matrix properties

Equations 403 through 412 and definitions necessary to state these lemmas such as DFT/IDFT on vectors, the DFT and Inverse DFT matrices.

We define three main matrices $W_n, sW_n = W_n^*, iW_n = \frac{1}{N}sW_n$, the DFT matrix the conjugated DFT matrix and the inverse DFT matrix as a scaled conjugated DFT matrix. Other than the equations themselves there are supporting lemmas:

The comment between eq_411 and eq_412 stating that the DFT matrix is a vandermonde matrix is also formalized.

• Wkn_dot_iWKn_offdiag: which shows that the product of the DFT matrix and its conjugate (or inverse) has zero of diagonal entries. This requires a lot of casting around!!
• Wₙ_mul_sWₙ:
• inverse_Wₙ :
• Wₙ_mul_iWₙ_eq_one:
• Wₙ_symmetric
• sWₙ_symmetric
• iWₙ_mul_Wₙ_eq_one
• inv_Wₙ
• twiddle_comm'
• twiddle_sum
• conj_Wₙ
• two_pi_I_by_N_piInt_pos: the imaginary part of $2 \pi i / N$ is less than $\pi$ only if N is greater than 2.
• two_pi_I_by_N_piInt_neg: the imaginary part of $2 \pi i / N$ is greater than $-\pi$
• twiddle_neg_half_cycle_eq_neg' raising a root of unity of denominator 2 or more to half its denominator gives minus 1
• shiftk and shiftk_equiv allows shifting the summation over fin N by arbitrary k.
• dft_idft and idft_dft shows that the dft and idft are inverse operations.
• notice_between_411_412 the comment that the DFT matrix is a vandermonde matrix

Trace and Determinant as Sum of Eigenavalues in closed fields

Added a file mat_eigs_lib.lean that contains definition of the eigenvalues set for finite matrices as the roots of the characteristic polynomial. Then we show that the sum and prod of these (possibly repeated eigenvalues) are the trace and determinant.

We then use these to prove eq_12 and eq_18

Minor Changes

• Some namespaces and locales open.
• Inclusion of the circulant matrix and vandermonde files. Also the schur_complement file linear_algebra.matrix.schur_complement since it contains the matrix.det_from_blocks₂₂ and matrix.det_from_blocks_one₁₁ identities used by @eric-wieser in Equations eq_397 and eq_398.
• Inclusion of the algebra.geom_sum, for calculating the sum of roots of unity (off diagonal product of DFT and conjugate DFT matrices) to be zero.
• Inclusion of the analysis.special_functions.trigonometric.basic for the constant $\pi$

Style

As you can see it is mostly rewrites. If you have pointers on how to improve my style and make it more efficient and varied in techniques, please share them!

[eric-wieser]

Nice work!