OAI/NumberTheory/PrimePackets/SubquadraticGrowth.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PrimeDegreePackets.AnalyticGrowth.tendsto_affine_div_sq line 104
  2. lemma OAI.PrimeDegreePackets.AnalyticGrowth.hasSubquadraticGrowth_id line 114
  3. lemma OAI.PrimeDegreePackets.AnalyticGrowth.hasSubquadraticGrowth_exp_affine line 120
  4. lemma OAI.PrimeDegreePackets.AnalyticGrowth.hasSubquadraticGrowth_const_cpow line 132
  5. lemma OAI.PrimeDegreePackets.AnalyticGrowth.HasSubquadraticGrowth.congr line 137
  6. lemma OAI.PrimeDegreePackets.AnalyticGrowth.HasSubquadraticGrowth.pow line 142
  7. lemma OAI.PrimeDegreePackets.ThetaConstruction.averagedNormalizedThetaTail_mellin_hasSubquadraticGrowth line 156
  8. theorem OAI.PrimeDegreePackets.ThetaConstruction.averagedThetaMellinXi_hasSubquadraticGrowth line 165
  9. theorem OAI.PrimeDegreePackets.arithmeticFlowThetaXi_boundedAverage_hasSubquadraticGrowth line 220
  10. lemma OAI.PrimeDegreePackets.HeckeMellin.idealThetaXi_hasSubquadraticGrowth line 288
  11. lemma OAI.PrimeDegreePackets.HeckeMellin.classThetaXi_hasSubquadraticGrowth line 301
  12. theorem OAI.PrimeDegreePackets.HeckeMellin.completedThetaXi_hasSubquadraticGrowth line 314
  13. theorem OAI.PrimeDegreePackets.HeckeMellin.dedekindXi_hasSum_realZeroPole line 335
  14. lemma OAI.PrimeDegreePackets.HeckeMellin.dedekindXi_realZeroPole_nonneg line 353
  15. lemma OAI.PrimeDegreePackets.AnalyticGrowth.near_one_kernel_lower line 366
  16. lemma OAI.PrimeDegreePackets.AnalyticGrowth.real_inverse_pole_scaled line 375
  17. lemma OAI.PrimeDegreePackets.AnalyticGrowth.near_one_complex_pole_lower line 390
  18. def OAI.PrimeDegreePackets.AnalyticGrowth.InNearOneBox line 414
  19. lemma OAI.PrimeDegreePackets.AnalyticGrowth.nearOneBox_multiplicity_sum_le_one line 417
  20. theorem OAI.PrimeDegreePackets.AnalyticGrowth.nearOneBox_real_simple_unique line 446
  21. lemma OAI.PrimeDegreePackets.HeckeMellin.completedThetaXi_logDeriv_base_le line 491
  22. theorem OAI.PrimeDegreePackets.HeckeMellin.dedekind_near_one_zero_real_simple_unique line 516