OAI/NumberTheory/PrimePackets/AnalyticLogarithms.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PrimeDegreePackets.AnalyticGrowth.exists_disk_logarithm line 92
  2. lemma OAI.PrimeDegreePackets.AnalyticGrowth.disk_logarithm_re line 128
  3. lemma OAI.PrimeDegreePackets.AnalyticGrowth.deriv_sub_le_of_re_le line 146
  4. lemma OAI.PrimeDegreePackets.AnalyticGrowth.logDeriv_sub_le_of_log_norm_le line 183
  5. lemma OAI.PrimeDegreePackets.AnalyticGrowth.entire_order_ne_top line 203
  6. lemma OAI.PrimeDegreePackets.AnalyticGrowth.divisor_sphere_eq_zero line 211
  7. lemma OAI.PrimeDegreePackets.AnalyticGrowth.exists_entire_ecanonicalDecomp line 220
  8. lemma OAI.PrimeDegreePackets.AnalyticGrowth.ecanonical_log_norm_eq_on_sphere line 226
  9. lemma OAI.PrimeDegreePackets.AnalyticGrowth.norm_canonicalFactor_zero line 245
  10. lemma OAI.PrimeDegreePackets.AnalyticGrowth.ecanonical_log_norm_zero_ge line 253
  11. lemma OAI.PrimeDegreePackets.AnalyticGrowth.ecanonical_log_norm_le line 281
  12. def OAI.PrimeDegreePackets.AnalyticGrowth.canonicalCorrection line 303
  13. lemma OAI.PrimeDegreePackets.AnalyticGrowth.canonicalNumerator_norm_lower line 305
  14. lemma OAI.PrimeDegreePackets.AnalyticGrowth.canonicalNumerator_ne_zero line 314
  15. lemma OAI.PrimeDegreePackets.AnalyticGrowth.norm_canonicalCorrection_sub_le line 318
  16. lemma OAI.PrimeDegreePackets.AnalyticGrowth.logDeriv_canonicalFactor line 340
  17. lemma OAI.PrimeDegreePackets.AnalyticGrowth.ecanonical_logDeriv line 365
  18. def OAI.PrimeDegreePackets.AnalyticGrowth.zeroMultiplicity line 444
  19. lemma OAI.PrimeDegreePackets.AnalyticGrowth.zeroMultiplicity_nonneg line 446
  20. lemma OAI.PrimeDegreePackets.AnalyticGrowth.zeroMultiplicity_eq_zero_iff line 453
  21. lemma OAI.PrimeDegreePackets.AnalyticGrowth.zeroMultiplicity_ne_zero_iff line 459
  22. lemma OAI.PrimeDegreePackets.AnalyticGrowth.exists_zero_free_sphere line 463
  23. def OAI.PrimeDegreePackets.AnalyticGrowth.diskZeroCount line 480
  24. lemma OAI.PrimeDegreePackets.AnalyticGrowth.diskZeroCount_eq_finsum line 483
  25. lemma OAI.PrimeDegreePackets.AnalyticGrowth.diskZeroCount_nonneg line 488
  26. lemma OAI.PrimeDegreePackets.AnalyticGrowth.diskZeroCount_le line 496