IndisputableMonolith.Spectral.DFT8

declarations in this module (46)

• def omega8 L41
• theorem omega8_pow_8 L44
• theorem omega8_pow_4 L53
• theorem omega8_abs L62
• def dft8_entry L72
• lemma dft8_entry_sym L76
• def dft8_matrix L82
• def dft8_mode L86
• def cyclic_shift L90
• def shift_matrix L94
• theorem omega8_pow_ne_one L102
• theorem omega8_pow_ne_one_axiom L143
• lemma star_omega8 L149
• lemma star_omega8_pow L161
• lemma omega8_mul_inv L165
• lemma star_omega8_mul_self L170
• lemma star_omega8_pow_mul_self L176
• lemma omega8_inv_eq_pow7 L180
• lemma star_omega8_pow_mul_pow L193
• lemma sum_star_omega8_pow_prod L200
• theorem roots_of_unity_sum L211
• lemma roots_of_unity_sum_zero L242
• lemma star_dft8_entry_mul L247
• lemma star_omega8_pow_mul_same L258
• theorem dft8_column_orthonormal L267
• theorem dft8_unitary L339
• theorem dft8_row_orthonormal L349
• def shift_eigenvalue L363
• lemma mod8_mul_eq L366
• theorem dft8_shift_eigenvector L385
• lemma shift_mul_dft8_entry L396
• lemma conjTranspose_shift_mul L424
• theorem dft8_diagonalizes_shift L444
• lemma dft8_mode_zero_constant L457
• lemma dft8_mode_neutral L464
• def dft_coefficients L485
• lemma dft_coeff_zero L489
• lemma dft_coeff_zero_of_neutral L506
• lemma inverse_dft_expansion L513
• theorem dft8_neutral_subspace L541
• def dft8_neutral_subspace_hypothesis L570
• theorem dft8_neutral_subspace_hypothesis_holds L576
• def dft8_unique_up_to_phase_hypothesis L592
• structure EightTickBasis L607
• def standardDFT8Basis L620
• def standardDFT8Basis_canonical_hypothesis L630