OAI/NumberTheory/DirichletL/Moments/FixedRay.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SevenEighths.CenteredMomentFixedRay.supported_coprime_four line 16
  2. theorem OAI.SevenEighths.CenteredMomentFixedRay.supported_coprime_twelve line 26
  3. theorem OAI.SevenEighths.CenteredMomentFixedRay.supported_rayMask line 33
  4. def OAI.SevenEighths.CenteredMomentFixedRay.phaseTable line 37
  5. theorem OAI.SevenEighths.CenteredMomentFixedRay.phaseTable_mk line 45
  6. theorem OAI.SevenEighths.CenteredMomentFixedRay.phaseTable_norm line 52
  7. theorem OAI.SevenEighths.CenteredMomentFixedRay.phaseTable_expansion line 56
  8. theorem OAI.SevenEighths.CenteredMomentFixedRay.phaseTable_mass line 66
  9. def OAI.SevenEighths.CenteredMomentFixedRay.primaryRayHom line 71
  10. theorem OAI.SevenEighths.CenteredMomentFixedRay.primaryRayHom_primary line 76
  11. theorem OAI.SevenEighths.CenteredMomentFixedRay.primaryRayHom_unit_mul line 82
  12. theorem OAI.SevenEighths.CenteredMomentFixedRay.primaryRayHom_periodic line 88
  13. def OAI.SevenEighths.CenteredMomentFixedRay.primaryRayCharacter line 108
  14. theorem OAI.SevenEighths.CenteredMomentFixedRay.primaryRayCharacter_modulus line 114
  15. theorem OAI.SevenEighths.CenteredMomentFixedRay.primaryRayCharacter_primary line 117
  16. theorem OAI.SevenEighths.CenteredMomentFixedRay.completeSupportExtension_separated line 124