OAI/NumberTheory/JointDickman/Amplification/AuxiliaryLogarithms.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Logarithmic scales for the regularity grid

  1. theorem OAI.JointDickman.auxiliaryLogLength_tendsto line 12
  2. theorem OAI.JointDickman.log_auxiliaryCutoff line 15
  3. theorem OAI.JointDickman.auxiliaryLogLength_eq line 19
  4. theorem OAI.JointDickman.logLogCutoff_div_log_tendsto_zero line 27
  5. theorem OAI.JointDickman.auxiliaryLogLength_div_log_tendsto line 40
  6. theorem OAI.JointDickman.log_div_auxiliaryLogLength_tendsto line 52
  7. theorem OAI.JointDickman.logLogCutoff_div_auxiliaryLogLength_tendsto_zero line 57