OAI/NumberTheory/DirichletL/Moments/FirstSectors.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentFirstSectors.residualPool line 12
2. theorem OAI.SevenEighths.CenteredMomentFirstSectors.mem_residualPool line 15
3. def OAI.SevenEighths.CenteredMomentFirstSectors.pairSector line 18
4. def OAI.SevenEighths.CenteredMomentFirstSectors.residualPairDomain line 21
5. theorem OAI.SevenEighths.CenteredMomentFirstSectors.residualPair_image line 26
6. theorem OAI.SevenEighths.CenteredMomentFirstSectors.pairSector_sum line 60
7. theorem OAI.SevenEighths.CenteredMomentFirstSectors.pairSector_double_sum line 70
8. def OAI.SevenEighths.CenteredMomentFirstSectors.commonLabels line 79
9. theorem OAI.SevenEighths.CenteredMomentFirstSectors.commonLabels_data line 82
10. theorem OAI.SevenEighths.CenteredMomentFirstSectors.sum_common_sectors line 89