OAI/NumberTheory/Jacobsthal/Sieve/ExponentialTailBound.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.ErdosOmissionTail.expTerm line 16
  2. def OAI.Erdos970.ErdosOmissionTail.firstExpTerm line 17
  3. def OAI.Erdos970.ErdosOmissionTail.secondExpTerm line 18
  4. def OAI.Erdos970.ErdosOmissionTail.weightedExpTerm line 19
  5. theorem OAI.Erdos970.ErdosOmissionTail.expTerm_hasSum line 21
  6. theorem OAI.Erdos970.ErdosOmissionTail.firstExpTerm_succ line 24
  7. theorem OAI.Erdos970.ErdosOmissionTail.secondExpTerm_add_two line 30
  8. theorem OAI.Erdos970.ErdosOmissionTail.firstExpTerm_hasSum line 39
  9. theorem OAI.Erdos970.ErdosOmissionTail.secondExpTerm_hasSum line 45
  10. theorem OAI.Erdos970.ErdosOmissionTail.weightedExpTerm_hasSum line 52
  11. theorem OAI.Erdos970.ErdosOmissionTail.weighted_log_two_tail_hasSum line 61
  12. theorem OAI.Erdos970.ErdosOmissionTail.weighted_log_two_tail_lt line 70
  13. theorem OAI.Erdos970.ErdosOmissionTail.log_two_mean_factor_bounds line 80
  14. theorem OAI.Erdos970.ErdosOmissionTail.numerical_tail_majorant_lt line 90