OAI/Computability/FourierTransform/FourierIdentities.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.PowerSaving.Line line 11
2. def OAI.PowerSaving.Spectral.freq line 15
3. def OAI.PowerSaving.Spectral.winds line 18
4. def OAI.PowerSaving.Spectral.front line 21
5. lemma OAI.PowerSaving.Spectral.front_freq line 23
6. lemma OAI.PowerSaving.Spectral.root_primitive line 28
7. lemma OAI.PowerSaving.Spectral.root_four line 31
8. lemma OAI.PowerSaving.Spectral.root_mul_pow line 37
9. lemma OAI.PowerSaving.Spectral.root_factor line 47
10. lemma OAI.PowerSaving.Spectral.power_mod line 57
11. lemma OAI.PowerSaving.Spectral.norm_of_root line 62
12. lemma OAI.PowerSaving.Spectral.conj_of_root line 67
13. lemma OAI.PowerSaving.Spectral.freq_congr line 73
14. lemma OAI.PowerSaving.Spectral.freq_add line 78
15. lemma OAI.PowerSaving.Spectral.freq_scale line 82
16. lemma OAI.PowerSaving.Spectral.freq_period line 86
17. lemma OAI.PowerSaving.Spectral.orth line 91

    Source comment

    Orthogonality in inverse formula

    lemma orth {n : ℕ} {u : ℂ} (hu : IsPrimitiveRoot u n) (i j : ℕ)
        (hi : i<n) (hj : j<n) :
        (∑ l ∈ range n, u⁻¹ ^ (i*l) * u ^ (l*j)) =
        if i=j then (n:ℂ) else 0 := by
    …

18. lemma OAI.PowerSaving.Spectral.freq_back line 111
19. lemma OAI.PowerSaving.Spectral.freq_inv line 121
20. def OAI.PowerSaving.Spectral.predAt line 128

    Source comment

    Circulant acts by difference of row & column

    def predAt (n i j : ℕ) := if j ≤ i then i-j else i+n-j

21. lemma OAI.PowerSaving.Spectral.pred_lt line 130
22. lemma OAI.PowerSaving.Spectral.sum_pred line 133
23. lemma OAI.PowerSaving.Spectral.pow_pred line 147
24. def OAI.PowerSaving.Spectral.cyclic line 155
25. lemma OAI.PowerSaving.Spectral.freq_cyclic line 158
26. lemma OAI.PowerSaving.Spectral.sum_eo line 174

    Source comment

    Binary recursion

    lemma sum_eo (n : ℕ) (f : ℕ→ℂ) :
        ∑ i ∈ range (n+n), f i =
        ∑ i ∈ range n, f (2*i) + ∑ i ∈ range n, f (2*i+1) := by
    …

27. lemma OAI.PowerSaving.Spectral.freq_eo line 184
28. lemma OAI.PowerSaving.Spectral.even_prim line 193
29. lemma OAI.PowerSaving.Spectral.half_power line 198
30. lemma OAI.PowerSaving.Spectral.freq_eo' line 204