OAI/NumberTheory/DirichletL/Moments/CommonHarmonicMass.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SevenEighths.CenteredMomentCommonHarmonicMass.Label line 15
  2. def OAI.SevenEighths.CenteredMomentCommonHarmonicMass.Valid line 17
  3. def OAI.SevenEighths.CenteredMomentCommonHarmonicMass.weight line 21
  4. lemma OAI.SevenEighths.CenteredMomentCommonHarmonicMass.commonRadical_norm_le line 23
  5. lemma OAI.SevenEighths.CenteredMomentCommonHarmonicMass.min_le_sqrt_mul line 39
  6. lemma OAI.SevenEighths.CenteredMomentCommonHarmonicMass.shell_scalar line 46
  7. theorem OAI.SevenEighths.CenteredMomentCommonHarmonicMass.shell_bound line 60
  8. def OAI.SevenEighths.CenteredMomentCommonHarmonicMass.key line 99
  9. def OAI.SevenEighths.CenteredMomentCommonHarmonicMass.keys line 100
  10. def OAI.SevenEighths.CenteredMomentCommonHarmonicMass.shell line 101
  11. lemma OAI.SevenEighths.CenteredMomentCommonHarmonicMass.norm_scale_bounds line 103
  12. lemma OAI.SevenEighths.CenteredMomentCommonHarmonicMass.shell_norm_bounds line 112
  13. theorem OAI.SevenEighths.CenteredMomentCommonHarmonicMass.sum_shells line 121
  14. lemma OAI.SevenEighths.CenteredMomentCommonHarmonicMass.keys_card_log line 125
  15. theorem OAI.SevenEighths.CenteredMomentCommonHarmonicMass.polynomial_cap_log_bound line 152
  16. lemma OAI.SevenEighths.CenteredMomentCommonHarmonicMass.log_square_subpower line 188
  17. theorem OAI.SevenEighths.CenteredMomentCommonHarmonicMass.common_harmonic_mass line 209