OAI/NumberTheory/JointDickman/Arithmetic/NaturalPrimeRectangle.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Natural-index form of the prime rectangle estimate

  1. lemma OAI.JointDickman.sum_Ioc_nat_as_int line 9
  2. lemma OAI.JointDickman.prime_rectangle_nat_int line 25
  3. theorem OAI.JointDickman.natural_prime_rational_rectangle_bound line 43