OAI/NumberTheory/DirichletL/Moments/SecondWholeKernel.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentSecondWholeKernel.secondEffectiveScale line 16
2. theorem OAI.SevenEighths.CenteredMomentSecondWholeKernel.secondEffectiveScale_pos line 19
3. theorem OAI.SevenEighths.CenteredMomentSecondWholeKernel.primary_norm_sq line 24
4. theorem OAI.SevenEighths.CenteredMomentSecondWholeKernel.second_kernel_argument line 28
5. theorem OAI.SevenEighths.CenteredMomentSecondWholeKernel.common_normalized_kernel line 38
6. theorem OAI.SevenEighths.CenteredMomentSecondWholeKernel.second_frequency_whole_kernel line 56