OAI/NumberTheory/DirichletL/Moments/FirstDivisorSupport.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SevenEighths.CenteredMomentFirstDivisorSupport.common_coefficient_zero line 23
2. theorem OAI.SevenEighths.CenteredMomentFirstDivisorSupport.commonEnergy_zero line 36
3. lemma OAI.SevenEighths.CenteredMomentFirstDivisorSupport.right_coefficient_zero line 45
4. theorem OAI.SevenEighths.CenteredMomentFirstDivisorSupport.rightWindowChild_zero line 62
5. theorem OAI.SevenEighths.CenteredMomentFirstDivisorSupport.signed_right_window_filter line 74
6. theorem OAI.SevenEighths.CenteredMomentFirstDivisorSupport.supported_harmonic_mass line 92
7. theorem OAI.SevenEighths.CenteredMomentFirstDivisorSupport.input_commonEnergy_zero line 106
8. theorem OAI.SevenEighths.CenteredMomentFirstDivisorSupport.input_rightWindowChild_zero line 115