OAI/NumberTheory/JointDickman/Amplification/FiniteProductTail.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

An exponential bound for tails of finite positive Euler products

  1. theorem OAI.JointDickman.prod_one_add_le_exp_sum line 9
  2. theorem OAI.JointDickman.exp_sub_one_le_exp_mul line 19
  3. theorem OAI.JointDickman.prod_one_add_difference_bound line 24