OAI/NumberTheory/DirichletL/Moments/CommonMaskExpansion.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentCommonMaskExpansion.naturalSlot line 13
2. def OAI.SevenEighths.CenteredMomentCommonMaskExpansion.profileSlot line 16
3. lemma OAI.SevenEighths.CenteredMomentCommonMaskExpansion.outside_prime line 20
4. lemma OAI.SevenEighths.CenteredMomentCommonMaskExpansion.deleted_prime line 29
5. theorem OAI.SevenEighths.CenteredMomentCommonMaskExpansion.naturalSlot_delete line 35
6. lemma OAI.SevenEighths.CenteredMomentCommonMaskExpansion.prod_sub_expansion line 48
7. def OAI.SevenEighths.CenteredMomentCommonMaskExpansion.plainCoefficient line 57
8. def OAI.SevenEighths.CenteredMomentCommonMaskExpansion.signedCoefficient line 62
9. theorem OAI.SevenEighths.CenteredMomentCommonMaskExpansion.simultaneous_deletion line 67
10. def OAI.SevenEighths.CenteredMomentCommonMaskExpansion.slotMass line 100
11. lemma OAI.SevenEighths.CenteredMomentCommonMaskExpansion.slotMass_nonneg line 103
12. lemma OAI.SevenEighths.CenteredMomentCommonMaskExpansion.naturalSlot_norm line 106
13. lemma OAI.SevenEighths.CenteredMomentCommonMaskExpansion.plainCoefficient_norm line 117
14. lemma OAI.SevenEighths.CenteredMomentCommonMaskExpansion.slot_point_mass line 125
15. lemma OAI.SevenEighths.CenteredMomentCommonMaskExpansion.slotMass_bound line 147
16. lemma OAI.SevenEighths.CenteredMomentCommonMaskExpansion.one_add_sum_weight line 162
17. lemma OAI.SevenEighths.CenteredMomentCommonMaskExpansion.deletion_le_euler line 172
18. lemma OAI.SevenEighths.CenteredMomentCommonMaskExpansion.euler_ge_one line 180
19. lemma OAI.SevenEighths.CenteredMomentCommonMaskExpansion.one_add_slotMass line 186
20. def OAI.SevenEighths.CenteredMomentCommonMaskExpansion.coefficientMajorant line 198
21. lemma OAI.SevenEighths.CenteredMomentCommonMaskExpansion.signedCoefficient_norm line 203
22. lemma OAI.SevenEighths.CenteredMomentCommonMaskExpansion.majorant_mass line 216
23. def OAI.SevenEighths.CenteredMomentCommonMaskExpansion.uniformMajorant line 227
24. lemma OAI.SevenEighths.CenteredMomentCommonMaskExpansion.uniformMajorant_nonneg line 232
25. lemma OAI.SevenEighths.CenteredMomentCommonMaskExpansion.signedCoefficient_uniform line 241
26. lemma OAI.SevenEighths.CenteredMomentCommonMaskExpansion.uniformMajorant_mass line 255
27. lemma OAI.SevenEighths.CenteredMomentCommonMaskExpansion.uniformMajorant_mass_le line 266
28. theorem OAI.SevenEighths.CenteredMomentCommonMaskExpansion.uniform_mass_subpower line 297
29. theorem OAI.SevenEighths.CenteredMomentCommonMaskExpansion.signed_mass_subpower line 326
30. lemma OAI.SevenEighths.CenteredMomentCommonMaskExpansion.profile_bounds line 351
31. theorem OAI.SevenEighths.CenteredMomentCommonMaskExpansion.profile_signed_mass_subpower line 365