lean-matrix-cookbook
lean-matrix-cookbook copied to clipboard
DFT Matrices and Surrounding Lemmas
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
andshiftk_equiv
allows shifting the summation overfin N
by arbitrary k. -
dft_idft
andidft_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 Equationseq_397
andeq_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!