OAI/NumberTheory/JointDickman/Arithmetic/LogarithmicReduction.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Removing a logarithmic weight from a bounded exponential sum

  1. lemma OAI.JointDickman.sum_log_Icc_factorial line 9
  2. lemma OAI.JointDickman.sum_log_quotient_le line 20
  3. theorem OAI.JointDickman.logarithmic_weight_error line 29
  4. theorem OAI.JointDickman.unweighted_sum_le_logarithmic_sum line 50