OAI/NumberTheory/JointDickman/Amplification/RectangleRemainder.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Absorbing the explicit rectangular sieve remainder

  1. theorem OAI.JointDickman.rectangle_remainder_bound line 12
  2. theorem OAI.JointDickman.coefficient_rectangle_remainder_small line 30