OAI/NumberTheory/PrimeGaps/MellinSmoothing.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LargePrimeGaps.rieszKernel line 9
  2. lemma OAI.LargePrimeGaps.hasMellin_rieszKernel line 11
  3. lemma OAI.LargePrimeGaps.rieszKernel_eq_max line 27
  4. lemma OAI.LargePrimeGaps.rieszKernel_continuousAt line 32
  5. lemma OAI.LargePrimeGaps.rieszDenominator_bound line 38
  6. lemma OAI.LargePrimeGaps.rieszDenominator_verticalIntegrable line 51
  7. lemma OAI.LargePrimeGaps.rieszKernel_mellinInv line 73
  8. lemma OAI.LargePrimeGaps.principal_logRiesz_bound line 88
  9. lemma OAI.LargePrimeGaps.primitive_logRiesz_bound line 155
  10. lemma OAI.LargePrimeGaps.logRiesz_poleRemoved_analyticAt line 182
  11. lemma OAI.LargePrimeGaps.analyticAt_iteratedDeriv_local line 197
  12. lemma OAI.LargePrimeGaps.vertical_contDiff line 203
  13. lemma OAI.LargePrimeGaps.vertical_iteratedDeriv line 212
  14. def OAI.LargePrimeGaps.decayMajorant line 227
  15. lemma OAI.LargePrimeGaps.decayMajorant_nonneg line 229
  16. lemma OAI.LargePrimeGaps.decayMajorant_integrable line 231
  17. lemma OAI.LargePrimeGaps.integrable_of_decay_bound line 236
  18. lemma OAI.LargePrimeGaps.integral_norm_le_of_decay_bound line 240
  19. lemma OAI.LargePrimeGaps.fourierInv_decay line 247
  20. lemma OAI.LargePrimeGaps.mellinInv_const_mul line 271
  21. lemma OAI.LargePrimeGaps.mellinInv_term_riesz line 275
  22. lemma OAI.LargePrimeGaps.riesz_inverse_integrand_norm line 294
  23. lemma OAI.LargePrimeGaps.riesz_inverse_integrand_summable line 302
  24. lemma OAI.LargePrimeGaps.mellinInv_LSeries_riesz line 333
  25. def OAI.LargePrimeGaps.rieszSum line 346
  26. lemma OAI.LargePrimeGaps.rieszKernel_tsum_eq line 349
  27. lemma OAI.LargePrimeGaps.rieszSum_mellinInv line 374
  28. def OAI.LargePrimeGaps.poleRieszKernel line 381
  29. lemma OAI.LargePrimeGaps.hasMellin_poleRieszKernel line 384
  30. lemma OAI.LargePrimeGaps.poleRieszKernel_continuousAt line 408
  31. lemma OAI.LargePrimeGaps.poleRiesz_verticalIntegrable line 417
  32. lemma OAI.LargePrimeGaps.poleRiesz_mellinInv line 437
  33. lemma OAI.LargePrimeGaps.poleRieszKernel_inv line 449
  34. lemma OAI.LargePrimeGaps.mellinInv_integrable line 461
  35. lemma OAI.LargePrimeGaps.mellinInv_add_of_verticalIntegrable line 473