OAI/NumberTheory/DirichletL/Moments/Smooth.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentSmooth.rootWindow line 12
2. def OAI.SevenEighths.CenteredMomentSmooth.wholeKernel line 14
3. def OAI.SevenEighths.CenteredMomentSmooth.rowPhase line 19
4. def OAI.SevenEighths.CenteredMomentSmooth.columnPhase line 22
5. def OAI.SevenEighths.CenteredMomentSmooth.separatedKernel line 25
6. theorem OAI.SevenEighths.CenteredMomentSmooth.whole_kernel_separation line 28
7. lemma OAI.SevenEighths.CenteredMomentSmooth.separated_integrable line 60
8. theorem OAI.SevenEighths.CenteredMomentSmooth.finite_pair_separation line 77
9. theorem OAI.SevenEighths.CenteredMomentSmooth.whole_product_pair_separation line 117
10. theorem OAI.SevenEighths.CenteredMomentSmooth.logPhase_norm_ratio line 137
11. theorem OAI.SevenEighths.CenteredMomentSmooth.idealWeight_height_add line 160
12. theorem OAI.SevenEighths.CenteredMomentSmooth.idealWeight_whole_phase line 168
13. theorem OAI.SevenEighths.CenteredMomentSmooth.centered_whole_phase line 178