OAI/NumberTheory/JointDickman/Arithmetic/LogarithmicScaleBounds.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The elementary logarithmic losses used in the minor-arc specialization

  1. theorem OAI.JointDickman.eventually_nat_log_linear line 10
  2. theorem OAI.JointDickman.eventually_nat_one_add_log_power line 21