Discrete orthogonality of roots of unity

theorem Chapter3.discrete_orthogonality (n : ℕ) (hn : 0 < n) (k : ℤ) (hk : ¬↑n ∣ k) : ∑ s : Fin n, Complex.exp (2 * ↑Real.pi * Complex.I * ↑k * ↑↑s / ↑n) = 0

Discrete orthogonality of roots of unity.

theorem Chapter3.cos_sum_zero (n : ℕ) (hn : 0 < n) (k : ℤ) (hk : ¬↑n ∣ k) : ∑ s : Fin n, Real.cos (2 * Real.pi * ↑k * ↑↑s / ↑n) = 0

Cosine discrete orthogonality: Σ cos(2πks/n) = 0 when n ∤ k.

theorem Chapter3.sin_sum_zero (n : ℕ) (hn : 0 < n) (k : ℤ) (hk : ¬↑n ∣ k) : ∑ s : Fin n, Real.sin (2 * Real.pi * ↑k * ↑↑s / ↑n) = 0

Sine discrete orthogonality: Σ sin(2πks/n) = 0 when n ∤ k.

Arithmetic helpers

theorem Chapter3.not_dvd (n : ℕ) (k : ℤ) (hk_ne : k ≠ 0) (hk_abs : k.natAbs < n) : ¬↑n ∣ k

Non-divisibility: if k ≠ 0 and |k| < n then n ∤ k.

theorem Chapter3.natAbs_coe_add_coe_lt {a b n : ℕ} (h : a + b < n) : (↑a + ↑b).natAbs < n

theorem Chapter3.natAbs_coe_sub_coe_lt {a b n : ℕ} (h : a + b < n) : (↑a - ↑b).natAbs < n

theorem Chapter3.natAbs_two_mul_coe_lt {a n : ℕ} (h : a + a < n) : (2 * ↑a).natAbs < n

Trigonometric sum identities

theorem Chapter3.cos_sq_sum (n : ℕ) (hn : 0 < n) (k : ℤ) (hk : ¬↑n ∣ 2 * k) : ∑ s : Fin n, Real.cos (2 * Real.pi * ↑k * ↑↑s / ↑n) ^ 2 = ↑n / 2

Sum of cos² = n/2 when n ∤ 2k

theorem Chapter3.sin_sq_sum (n : ℕ) (hn : 0 < n) (k : ℤ) (hk : ¬↑n ∣ 2 * k) : ∑ s : Fin n, Real.sin (2 * Real.pi * ↑k * ↑↑s / ↑n) ^ 2 = ↑n / 2

Sum of sin² = n/2 when n ∤ 2k

theorem Chapter3.cos_cos_cross_sum_zero (n : ℕ) (hn : 0 < n) (k k' : ℤ) (hkm : ¬↑n ∣ k - k') (hkp : ¬↑n ∣ k + k') : ∑ s : Fin n, Real.cos (2 * Real.pi * ↑k * ↑↑s / ↑n) * Real.cos (2 * Real.pi * ↑k' * ↑↑s / ↑n) = 0

Cross-frequency cosine sum

theorem Chapter3.sin_sin_cross_sum_zero (n : ℕ) (hn : 0 < n) (k k' : ℤ) (hkm : ¬↑n ∣ k - k') (hkp : ¬↑n ∣ k + k') : ∑ s : Fin n, Real.sin (2 * Real.pi * ↑k * ↑↑s / ↑n) * Real.sin (2 * Real.pi * ↑k' * ↑↑s / ↑n) = 0

Cross-frequency sine sum

theorem Chapter3.cos_sin_sum_zero (n : ℕ) (hn : 0 < n) (k k' : ℤ) (hkp : ¬↑n ∣ k + k') (habs : (k' - k).natAbs < n) : ∑ s : Fin n, Real.cos (2 * Real.pi * ↑k * ↑↑s / ↑n) * Real.sin (2 * Real.pi * ↑k' * ↑↑s / ↑n) = 0

Cross-frequency cos·sin sum. Only needs ¬ n ∣ (k+k') and |k'-k| < n.

Trigonometric design matrix and ORT

theorem Chapter3.sqrt2_factor (a b : ℝ) : √2 * a * (√2 * b) = 2 * (a * b)

Helper: √2·a · √2·b = 2·(a·b)

noncomputable def Chapter3.trigDesignMatrix (n M : ℕ) : Matrix (Fin n) (Fin M) ℝ

The trigonometric design matrix Φ. Column 0: constant 1. Column j (j odd, j≥1): √2·cos(2π·((j+1)/2)·i/n). Column j (j even, j≥2): √2·sin(2π·(j/2)·i/n).

theorem Chapter3.lemma_3_13 (n M : ℕ) (hn : 0 < n) (hM : M ≤ n - 1) : (trigDesignMatrix n M).transpose * trigDesignMatrix n M = ↑n • 1

Lemma 3.13. Under the regular design X_i = i/n, for M ≤ n-1, Φᵀ Φ = n · I_M (the ORT condition).