OAI/NumberTheory/PrimePackets/MellinGrowth.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PrimeDegreePackets.AnalyticGrowth.real_mellin_kernel_bound line 95
  2. theorem OAI.PrimeDegreePackets.AnalyticGrowth.mellin_norm_le line 108
  3. def OAI.PrimeDegreePackets.AnalyticGrowth.HasSubquadraticGrowth line 156
  4. lemma OAI.PrimeDegreePackets.AnalyticGrowth.eventually_const_le_exp_quad line 160
  5. lemma OAI.PrimeDegreePackets.AnalyticGrowth.hasSubquadraticGrowth_const line 165
  6. lemma OAI.PrimeDegreePackets.AnalyticGrowth.HasSubquadraticGrowth.of_bound line 170
  7. lemma OAI.PrimeDegreePackets.AnalyticGrowth.HasSubquadraticGrowth.add line 182
  8. lemma OAI.PrimeDegreePackets.AnalyticGrowth.HasSubquadraticGrowth.mul line 196
  9. lemma OAI.PrimeDegreePackets.AnalyticGrowth.HasSubquadraticGrowth.neg line 208
  10. lemma OAI.PrimeDegreePackets.AnalyticGrowth.HasSubquadraticGrowth.sub line 212
  11. lemma OAI.PrimeDegreePackets.AnalyticGrowth.HasSubquadraticGrowth.finset_sum line 217
  12. lemma OAI.PrimeDegreePackets.AnalyticGrowth.HasSubquadraticGrowth.comp_affine line 227
  13. lemma OAI.PrimeDegreePackets.AnalyticGrowth.tendsto_mellin_bound line 244
  14. theorem OAI.PrimeDegreePackets.AnalyticGrowth.mellin_hasSubquadraticGrowth line 270
  15. lemma OAI.PrimeDegreePackets.AnalyticGrowth.diskZeroCount_subquadratic line 294
  16. lemma OAI.PrimeDegreePackets.AnalyticGrowth.diskZeroCount_div_sq_tendsto_zero line 308
  17. lemma OAI.PrimeDegreePackets.AnalyticGrowth.divisor_ball_eq_closedBall line 327
  18. def OAI.PrimeDegreePackets.AnalyticGrowth.zeroDiskFinset line 344
  19. lemma OAI.PrimeDegreePackets.AnalyticGrowth.mem_zeroDiskFinset line 347
  20. lemma OAI.PrimeDegreePackets.AnalyticGrowth.zeroDiskFinset_norm_le line 351
  21. lemma OAI.PrimeDegreePackets.AnalyticGrowth.divisor_closedBall_eq_multiplicity line 356
  22. lemma OAI.PrimeDegreePackets.AnalyticGrowth.diskZeroCount_eq_sum line 362
  23. def OAI.PrimeDegreePackets.AnalyticGrowth.diskPoleSum line 374
  24. lemma OAI.PrimeDegreePackets.AnalyticGrowth.ecanonical_logDeriv_finite line 377
  25. lemma OAI.PrimeDegreePackets.AnalyticGrowth.correction_sum_sub_le line 397
  26. lemma OAI.PrimeDegreePackets.AnalyticGrowth.diskPoleSum_error_le line 418
  27. lemma OAI.PrimeDegreePackets.AnalyticGrowth.tendsto_diskPoleSum_sub line 456
  28. lemma OAI.PrimeDegreePackets.AnalyticGrowth.exists_good_radii line 497