OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/Poly.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OrdinaryCorrelations.SourceRoughFourier.poly line 25
  2. def OAI.OrdinaryCorrelations.SourceRoughFourier.shortEnvelope line 28
  3. def OAI.OrdinaryCorrelations.SourceRoughFourier.progressionCoeff line 32
  4. def OAI.OrdinaryCorrelations.SourcePrimeFactor.primeCount line 39
  5. theorem OAI.OrdinaryCorrelations.SourcePrimeFactor.primeCount_mul line 41
  6. theorem OAI.OrdinaryCorrelations.SourcePrimeFactor.primeCount_pos line 59
  7. theorem OAI.OrdinaryCorrelations.SourcePrimeFactor.weighted_partition line 62
  8. def OAI.OrdinaryCorrelations.SourcePrimeFactor.binnedRamareCoefficient line 75
  9. lemma OAI.OrdinaryCorrelations.SourcePrimeFactor.primeCount_mul_le line 79
  10. lemma OAI.OrdinaryCorrelations.SourcePrimeFactor.binnedRamare_norm line 89
  11. lemma OAI.OrdinaryCorrelations.SourcePrimeFactor.binnedRamare_zero_of_rough line 121
  12. lemma OAI.OrdinaryCorrelations.SourcePrimeFactor.binnedRamare_exact line 129
  13. lemma OAI.OrdinaryCorrelations.SourcePrimeFactor.bin_cutoff_same line 165