OAI/NumberTheory/DirichletL/Moments/SupportedCorrelation.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentSupportedCorrelation.supportedModulusCharacter line 13
2. theorem OAI.SevenEighths.CenteredMomentSupportedCorrelation.supportedModulusCharacter_mk line 37
3. lemma OAI.SevenEighths.CenteredMomentSupportedCorrelation.supported_mul_elements line 41
4. theorem OAI.SevenEighths.CenteredMomentSupportedCorrelation.supportedModulusCharacter_mul line 47
5. lemma OAI.SevenEighths.CenteredMomentSupportedCorrelation.sexticReciprocityPhase_symm line 54
6. lemma OAI.SevenEighths.CenteredMomentSupportedCorrelation.star_sexticReciprocityPhase line 58
7. theorem OAI.SevenEighths.CenteredMomentSupportedCorrelation.supported_opposite_phase line 62
8. def OAI.SevenEighths.CenteredMomentSupportedCorrelation.supportedCorrelation line 81
9. theorem OAI.SevenEighths.CenteredMomentSupportedCorrelation.supported_complete_common_support line 86
10. lemma OAI.SevenEighths.CenteredMomentSupportedCorrelation.supported_element_ne_zero line 115
11. def OAI.SevenEighths.CenteredMomentSupportedCorrelation.actualCorrelation line 119
12. def OAI.SevenEighths.CenteredMomentSupportedCorrelation.completeSupportExtension line 127
13. theorem OAI.SevenEighths.CenteredMomentSupportedCorrelation.actual_complete_common_support line 134
14. theorem OAI.SevenEighths.CenteredMomentSupportedCorrelation.actual_complete_support_mobius line 162