OAI/NumberTheory/DirichletL/Moments/Twist.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentTwist.twistedMaskedSum line 12
2. lemma OAI.SevenEighths.CenteredMomentTwist.normPowerProfile_support line 18
3. lemma OAI.SevenEighths.CenteredMomentTwist.normPowerProfile_norm line 24
4. lemma OAI.SevenEighths.CenteredMomentTwist.norm_real_imaginary_power line 30
5. theorem OAI.SevenEighths.CenteredMomentTwist.twistedMaskedSum_scale line 35
6. theorem OAI.SevenEighths.CenteredMomentTwist.twistedMaskedSum_volume line 57
7. theorem OAI.SevenEighths.CenteredMomentTwist.twistedMaskedSum_absolute line 77
8. theorem OAI.SevenEighths.CenteredMomentTwist.twisted_volumeCoefficient_norm_le line 89
9. theorem OAI.SevenEighths.CenteredMomentTwist.twisted_rectangle_saving line 106