OAI/NumberTheory/DirichletL/Moments/CommonMaskEnergy.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.CenteredMomentCommonMaskEnergy.finite_shared_energy line 15
2. lemma OAI.SevenEighths.CenteredMomentCommonMaskEnergy.triple_sum line 33
3. theorem OAI.SevenEighths.CenteredMomentCommonMaskEnergy.actual_shared_energy line 58
4. lemma OAI.SevenEighths.CenteredMomentCommonMaskEnergy.sqrt_inverse_cpow line 127
5. lemma OAI.SevenEighths.CenteredMomentCommonMaskEnergy.plain_zero_height line 133
6. def OAI.SevenEighths.CenteredMomentCommonMaskEnergy.heightCoefficient line 146
7. lemma OAI.SevenEighths.CenteredMomentCommonMaskEnergy.heightCoefficient_norm line 149
8. lemma OAI.SevenEighths.CenteredMomentCommonMaskEnergy.normalized_twisted_plain line 158
9. theorem OAI.SevenEighths.CenteredMomentCommonMaskEnergy.original_positive_normalized line 167
10. lemma OAI.SevenEighths.CenteredMomentCommonMaskEnergy.deleted_height_phase line 202
11. lemma OAI.SevenEighths.CenteredMomentCommonMaskEnergy.positive_height_phase_norm line 208
12. lemma OAI.SevenEighths.CenteredMomentCommonMaskEnergy.deleted_normalized_twisted_plain line 211
13. theorem OAI.SevenEighths.CenteredMomentCommonMaskEnergy.original_positive_deletion line 221
14. theorem OAI.SevenEighths.CenteredMomentCommonMaskEnergy.original_retained_normalized line 250
15. theorem OAI.SevenEighths.CenteredMomentCommonMaskEnergy.original_retained_zero line 276
16. theorem OAI.SevenEighths.CenteredMomentCommonMaskEnergy.original_positive_energy line 292
17. theorem OAI.SevenEighths.CenteredMomentCommonMaskEnergy.original_positive_deletion_height line 343