OAI/NumberTheory/CubicGram/FrequencyGauss.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Prime, squarefree and mixed frequency Gauss evaluation.

  1. def OAI.CubicFirstMoment.frequencyGauss line 19
  2. lemma OAI.CubicFirstMoment.frequencyGauss_prime line 24
  3. lemma OAI.CubicFirstMoment.frequencyGauss_mul_of_isCoprime line 69
  4. lemma OAI.CubicFirstMoment.frequencyGauss_one line 120
  5. lemma OAI.CubicFirstMoment.frequencyGauss_prod_primaryPrimes line 130
  6. theorem OAI.CubicFirstMoment.frequencyGauss_squarefree line 152
  7. def OAI.CubicFirstMoment.conjugateFrequencyGauss line 159
  8. lemma OAI.CubicFirstMoment.conjugateFrequencyGauss_eq line 164
  9. lemma OAI.CubicFirstMoment.conjugateFrequencyGauss_squarefree line 176
  10. def OAI.CubicFirstMoment.mixedFrequencyGauss line 182
  11. lemma OAI.CubicFirstMoment.mixedFrequencyGauss_CRT line 188
  12. theorem OAI.CubicFirstMoment.mixedFrequencyGauss_squarefree line 260
  13. lemma OAI.CubicFirstMoment.mixedFrequencyGauss_zero line 275