OAI/NumberTheory/DirichletL/Moments/CommonRadicalHarmonicMass.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentCommonRadicalHarmonicMass.weight line 15
2. def OAI.SevenEighths.CenteredMomentCommonRadicalHarmonicMass.key line 16
3. def OAI.SevenEighths.CenteredMomentCommonRadicalHarmonicMass.keys line 17
4. def OAI.SevenEighths.CenteredMomentCommonRadicalHarmonicMass.shell line 18
5. lemma OAI.SevenEighths.CenteredMomentCommonRadicalHarmonicMass.radical_ne_zero line 20
6. lemma OAI.SevenEighths.CenteredMomentCommonRadicalHarmonicMass.shell_scalar line 23
7. theorem OAI.SevenEighths.CenteredMomentCommonRadicalHarmonicMass.shell_bound line 31
8. lemma OAI.SevenEighths.CenteredMomentCommonRadicalHarmonicMass.shell_norm_bounds line 63
9. theorem OAI.SevenEighths.CenteredMomentCommonRadicalHarmonicMass.sum_shells line 68
10. lemma OAI.SevenEighths.CenteredMomentCommonRadicalHarmonicMass.keys_card_log line 72
11. theorem OAI.SevenEighths.CenteredMomentCommonRadicalHarmonicMass.polynomial_cap_log_bound line 91
12. theorem OAI.SevenEighths.CenteredMomentCommonRadicalHarmonicMass.common_radical_harmonic_mass line 127