OAI/NumberTheory/Ostmann/HybridSieve/FourierPacket.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.HybridSieve.fourierPhase line 9
2. lemma OAI.Ostmann.HybridSieve.norm_fourierPhase line 11
3. lemma OAI.Ostmann.HybridSieve.fourier_translate line 14
4. def OAI.Ostmann.HybridSieve.fourierPacket line 22
5. lemma OAI.Ostmann.HybridSieve.fourierPacket_apply line 26
6. lemma OAI.Ostmann.HybridSieve.fourier_fourierPacket line 31
7. lemma OAI.Ostmann.HybridSieve.fourierPacket_plancherel line 38