OAI/NumberTheory/PiExponent/Analysis/LogTailAnalytic.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.LogTailAnalytic.logTail line 11
  2. theorem OAI.PiExponent.LogTailAnalytic.eval_trunc_log line 14
  3. theorem OAI.PiExponent.LogTailAnalytic.analyticAt_logTail line 27
  4. theorem OAI.PiExponent.LogTailAnalytic.norm_logTail_le line 36
  5. theorem OAI.PiExponent.LogTailAnalytic.norm_logTail_le_one line 44
  6. theorem OAI.PiExponent.LogTailAnalytic.norm_prod_logTail_le_one line 61
  7. theorem OAI.PiExponent.LogTailAnalytic.analyticAt_prod_logTail line 72
  8. theorem OAI.PiExponent.LogTailAnalytic.norm_rowTest_prod_logTail_le line 79
  9. theorem OAI.PiExponent.LogTailAnalytic.logTail_isBigO line 90
  10. theorem OAI.PiExponent.LogTailAnalytic.order_formal_logTail line 96
  11. theorem OAI.PiExponent.LogTailAnalytic.hasSum_formal_log line 100
  12. theorem OAI.PiExponent.LogTailAnalytic.hasSum_trunc_log line 110
  13. theorem OAI.PiExponent.LogTailAnalytic.hasSum_formal_logTail line 129
  14. theorem OAI.PiExponent.LogTailAnalytic.hasFPowerSeriesAt_logTail line 137
  15. theorem OAI.PiExponent.LogTailAnalytic.hasSum_coeff_mul line 147
  16. theorem OAI.PiExponent.LogTailAnalytic.hasSum_coeff_one line 166
  17. theorem OAI.PiExponent.LogTailAnalytic.hasSum_coeff_pow line 172
  18. theorem OAI.PiExponent.LogTailAnalytic.hasSum_formal_prod_logTail line 179
  19. theorem OAI.PiExponent.LogTailAnalytic.hasFPowerSeriesAt_prod_logTail line 191
  20. theorem OAI.PiExponent.LogTailAnalytic.rowTest_prod_logTail_eq_coeff line 202
  21. theorem OAI.PiExponent.LogTailAnalytic.norm_coeff_prod_formal_logTail_le line 219
  22. theorem OAI.PiExponent.LogTailAnalytic.rowTest_tail_budget line 226