OAI/NumberTheory/JointDickman/Amplification/AuxiliaryCostSum.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Summing the auxiliary costs without an extra logarithmic loss

  1. lemma OAI.JointDickman.card_mul_sum_le_of_square line 10
  2. theorem OAI.JointDickman.auxiliary_cost_sum_bound line 23