OAI/NumberTheory/DirichletL/Moments/FirstScale.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentFirstScale.firstNominalScale line 13
2. theorem OAI.SevenEighths.CenteredMomentFirstScale.norm_pos line 17
3. theorem OAI.SevenEighths.CenteredMomentFirstScale.active_norm_pos line 20
4. theorem OAI.SevenEighths.CenteredMomentFirstScale.firstNominalScale_pos line 25
5. theorem OAI.SevenEighths.CenteredMomentFirstScale.first_kernel_ratio line 31
6. theorem OAI.SevenEighths.CenteredMomentFirstScale.first_kernel_lower line 50
7. theorem OAI.SevenEighths.CenteredMomentFirstScale.first_kernel_sector_lower line 72