Assume finite length signals $x \in \mathbb{C}^N$.
Then the DFT is:
$$X(k) = \sum_{n=0}^{N-1} x(n) * e^{-i 2 \pi n k / N} \quad k = 0,1,2,\ldots,N-1$$and the inverse DFT is:
$$x(n) = \frac{1}{N} \sum_{k=0}^{N-1} X(k) * e^{i 2 \pi n k / N} \quad k = 0,1,2,\ldots,N-1$$ We ignore sampling interval, etc... as standard.No problem found, all the proofs straigforward.
No problem either, a couple of tweaks here and there.
Slight problem. Q: Do we need to resort to Coq (classical) reals? A: Look at what we need for the required theorems.
C_prim_root_exists: <- closed_field_poly_normal [poly.v] {poly is factorizable} <- root_prod_XsubC [poly.v] {factors are roots} <- has_prim_root [cyclic.v] {be n' (>=n) diff n.-unity roots, one is primitive} <- separable_prod_XsubC [separable.v] {separable factored form = uniqueness of factors} <- separable_Xn_sub_1 [cyclotomic.v] {X^n - 1 is separable}
Definition expz_def (z : F) (i : 'I_n) := z ^+ i.
Definition expz := nosimpl expz_def.
Notation "x @+ n" := (expz x n) : ring_scope.
Notation "x @- n" := (expz x (-n)) : ring_scope.
Hypothesis zP : N.-primitive_root z.
Lemma expzD m n : z @+ (m + n) = z @+ m * z @+ n.
Lemma expzM m n : z @+ (m * n) = z @+ m @+ n.
Lemma expzV n : (z @+ n)^-1 = z @- n.
Notation n := N.+2.
Hypothesis zP : n.-primitive_root z.
Lemma sum_expr_z_zero : \sum_(0 <= j < n) z ^+ j = 0.
Lemma norm_primX k : `|z @+ k| = 1.
Lemma prim_conjC : z^* = z^-1.
Lemma expz_conjC : (z @+ k)^* = z @- k.
Lemma z_ortho: \sum_k (z @+ (i * k)) * (z @+ (j * k))^* = n * (i == j).
Definition dft x k := \sum_n (x n 0) * 'ω ^+ (k*n).
Lemma dft_scale a x k : a * dft x k = dft (a *: x) k.
Lemma dft_sum x y k : dft (x + y) k = dft x k + dft y k.
Lemma dft_shifts x m k : dft (shifts x m) k = 'ω ^+ (k * m) * dft x k.
Lemma dft_flips x (k : 'I_N) : dft (flips x) k = dft x (-k).
Definition convs x y := \col_k \sum_m x m 0 * y (k-m) 0.
Lemma convsC : commutative convs.
Lemma dft_convs x y k : dft (convs x y) k = dft x k * dft y k.
[5 lines of proof...]
Satisfying the usual identities, with $algC^N$ we have a pre-Hilbert space.
Most properties are an immediate consequency of matrix multiplication lemmas.
Definition W := \matrix_(i < n, j < n) 'ω ^+ (i*j).
Lemma dftE x k : (W *m x) k 0 = dft x k.
Lemma dftDr x y : W *m (x + y) = W *m x + W *m y.
Proof. exact: linearD. Qed.
We'd use a theory of unitary matrices to derive the rest of the results.
Definition isometry f u v: '[f u, f v] = '[u,v].
Lemma unitary_dotP : reflect (isometry (mulmx A)) (A^* *m A == 1).
Lemma unitary_W : W^* *m W = N%:M.
[4 lines/using z_ortho]
/