OAI/Combinatorics/Progressions/Estimates/FiniteReciprocalTenthTail.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.one_sub_sum_mul_prod_one_add_le_one line 9
  2. theorem OAI.Erdos3.prod_one_add_le_one_add_twice_sum line 25
  3. theorem OAI.Erdos3.one_sub_sum_le_positive_prod line 34
  4. theorem OAI.Erdos3.positive_prod_sub_one_le_twice_sum line 53
  5. theorem OAI.Erdos3.reciprocal_square_le_reciprocal_difference line 77
  6. theorem OAI.Erdos3.finite_shifted_reciprocal_square_tail line 86
  7. theorem OAI.Erdos3.finite_reciprocal_square_tail line 109
  8. theorem OAI.Erdos3.finite_positive_product_tail line 133
  9. theorem OAI.Erdos3.exists_uniform_positive_product_cutoff line 145
  10. theorem OAI.Erdos3.finite_reciprocal_power_tail line 175
  11. theorem OAI.Erdos3.finite_divisor_error_tail line 200
  12. theorem OAI.Erdos3.reciprocal_tenth_le_difference line 225
  13. theorem OAI.Erdos3.finite_reciprocal_tenth_tail line 241