OAI/NumberTheory/Ostmann/Supply/FourierKernelBounds.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Ostmann.Supply.fourierKernel_eq_dftline 11 - theorem
OAI.Ostmann.Supply.fourierKernel_energyline 17 - theorem
OAI.Ostmann.Supply.fourierKernel_norm_leline 31 - theorem
OAI.Ostmann.Supply.convolution_fourierKernelline 41 - theorem
OAI.Ostmann.Supply.squareKernel_norm_leline 46