OAI/NumberTheory/DirichletL/Moments/Primary.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.CenteredMomentPrimary.primaryIdealCharacter line 15
  2. theorem OAI.SevenEighths.CenteredMomentPrimary.primaryIdealCharacter_apply line 20
  3. theorem OAI.SevenEighths.CenteredMomentPrimary.primaryIdealCharacter_norm_le_one line 25
  4. theorem OAI.SevenEighths.CenteredMomentPrimary.primaryIdealCharacter_zero_of_bad line 32
  5. theorem OAI.SevenEighths.CenteredMomentPrimary.tsum_primaryIdealCharacter_all line 38
  6. theorem OAI.SevenEighths.CenteredMomentPrimary.primaryIdealCharacter_ray_trivial line 52
  7. theorem OAI.SevenEighths.CenteredMomentPrimary.primaryIdealCharacter_mul line 66
  8. def OAI.SevenEighths.CenteredMomentPrimary.primaryResidueValue line 72
  9. theorem OAI.SevenEighths.CenteredMomentPrimary.primaryResidueValue_mk line 76
  10. theorem OAI.SevenEighths.CenteredMomentPrimary.primary_lattice_eq_ideal_sum line 93
  11. theorem OAI.SevenEighths.CenteredMomentPrimary.primary_ideal_volume_error line 120
  12. theorem OAI.SevenEighths.CenteredMomentPrimary.primary_ideal_volume_error_all line 134