OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/BadFrequencies.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OrdinaryRestrictedCofactor.badFrequencies line 24
  2. def OAI.OrdinaryRestrictedCofactor.restrictedEnergy line 29
  3. def OAI.OrdinaryRestrictedCofactor.powersAndCofactors line 33
  4. def OAI.OrdinaryRestrictedCofactor.productLocation line 36
  5. def OAI.OrdinaryRestrictedCofactor.productWeight line 39
  6. def OAI.OrdinaryRestrictedCofactor.productCoefficient line 44
  7. lemma OAI.OrdinaryRestrictedCofactor.phase_log_mul line 48
  8. lemma OAI.OrdinaryRestrictedCofactor.tupleProduct_pos line 57
  9. lemma OAI.OrdinaryRestrictedCofactor.primeMellin_pow_expansion line 62
  10. lemma OAI.OrdinaryRestrictedCofactor.actual_product_polynomial line 76
  11. lemma OAI.OrdinaryRestrictedCofactor.actual_support_bounds line 97
  12. lemma OAI.OrdinaryRestrictedCofactor.dyadic_log_band line 112
  13. lemma OAI.OrdinaryRestrictedCofactor.actual_support_band line 126
  14. def OAI.OrdinaryRestrictedCofactor.collectedEnergy line 146
  15. theorem OAI.OrdinaryRestrictedCofactor.actual_mixed_spaced_energy line 151
  16. theorem OAI.OrdinaryRestrictedCofactor.actual_restricted_cofactor_energy line 175