OAI/NumberTheory/DirichletL/Moments/Mask.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.CenteredMomentMask.ideal_coprime_mobius line 14
2. theorem OAI.SevenEighths.CenteredMomentMask.tsum_ideal_divisible line 30
3. theorem OAI.SevenEighths.CenteredMomentMask.masked_ideal_sum_eq line 49
4. theorem OAI.SevenEighths.CenteredMomentMask.annular_ideal_sum_summable line 70
5. theorem OAI.SevenEighths.CenteredMomentMask.masked_plain_ideal_sum line 82
6. theorem OAI.SevenEighths.CenteredMomentMask.polynomial_mask_divisor_bound line 109