OAI/NumberTheory/PrimeGaps/RieszDecay.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LargePrimeGaps.logRieszVertical line 23
  2. lemma OAI.LargePrimeGaps.logRieszVertical_contDiff line 26
  3. lemma OAI.LargePrimeGaps.logRieszVertical_iteratedDeriv line 38
  4. lemma OAI.LargePrimeGaps.logRieszVertical_bound line 53
  5. lemma OAI.LargePrimeGaps.logRieszVertical_integrable line 78
  6. lemma OAI.LargePrimeGaps.logRiesz_mellinInv_bound line 86
  7. def OAI.LargePrimeGaps.primeCoefficients line 119
  8. def OAI.LargePrimeGaps.characterMain line 122
  9. lemma OAI.LargePrimeGaps.characterMain_norm_le line 126
  10. lemma OAI.LargePrimeGaps.primeCoefficients_summable line 130
  11. lemma OAI.LargePrimeGaps.primeCoefficients_norm_le line 133
  12. lemma OAI.LargePrimeGaps.primeRiesz_identity line 140
  13. lemma OAI.LargePrimeGaps.logRiesz_verticalIntegrable line 152
  14. lemma OAI.LargePrimeGaps.primeRiesz_mellinInv line 167
  15. lemma OAI.LargePrimeGaps.primeRiesz_error_bound line 189
  16. def OAI.LargePrimeGaps.weightedPrefix line 217
  17. lemma OAI.LargePrimeGaps.weightedPrefix_difference line 220
  18. lemma OAI.LargePrimeGaps.weightedPrefix_tail_bound line 248
  19. lemma OAI.LargePrimeGaps.prefix_unsmoothing line 275
  20. lemma OAI.LargePrimeGaps.weightedPrefix_eq_mul_rieszSum line 312
  21. lemma OAI.LargePrimeGaps.rpow_one_add_inv_log line 322
  22. lemma OAI.LargePrimeGaps.primeWeighted_error_bound line 330