OAI/NumberTheory/PrimePackets/ZeroSeparation.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PrimeDegreePackets.AnalyticGrowth.outside_nearOneBox_scaled_gap line 111
  2. lemma OAI.PrimeDegreePackets.AnalyticGrowth.realZeroPole_le_base_of_outside_box line 131
  3. def OAI.PrimeDegreePackets.AnalyticGrowth.nearOneZeroPole line 155
  4. def OAI.PrimeDegreePackets.AnalyticGrowth.separatedZeroPole line 158
  5. lemma OAI.PrimeDegreePackets.AnalyticGrowth.zeroPole_split line 161
  6. lemma OAI.PrimeDegreePackets.AnalyticGrowth.nearOneZeroPole_summable line 166
  7. lemma OAI.PrimeDegreePackets.AnalyticGrowth.separatedZeroPole_summable line 170
  8. lemma OAI.PrimeDegreePackets.HeckeMellin.dedekind_separated_zero_sum_bound line 186
  9. theorem OAI.PrimeDegreePackets.HeckeMellin.dedekind_regularized_deriv_remove_exceptional line 228
  10. lemma OAI.PrimeDegreePackets.AnalyticGrowth.nearOneZeroPole_sum_of_no_zero line 266
  11. lemma OAI.PrimeDegreePackets.AnalyticGrowth.nearOneZeroPole_sum_of_unique line 280
  12. theorem OAI.PrimeDegreePackets.HeckeMellin.dedekind_regularized_deriv_dichotomy line 307
  13. theorem OAI.PrimeDegreePackets.residue_log_comparison_remove_pole line 364
  14. theorem OAI.PrimeDegreePackets.residue_comparison_remove_pole line 406
  15. theorem OAI.PrimeDegreePackets.HeckeMellin.dedekind_residue_dichotomy line 442
  16. def OAI.PrimeDegreePackets.anchorNormalize line 507
  17. lemma OAI.PrimeDegreePackets.anchorNormalize_anchor line 509
  18. lemma OAI.PrimeDegreePackets.anchorNormalize_finite line 513
  19. theorem OAI.PrimeDegreePackets.anchorNormalize_restrict line 522
  20. theorem OAI.PrimeDegreePackets.restricted_conditional_anchor line 546