OAI/NumberTheory/JointDickman/Amplification/AuxiliaryOdds.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Bounded odds corrections at the manuscript's auxiliary scale

  1. theorem OAI.JointDickman.coefficientScale_mul_sqrt_ratio line 13
  2. theorem OAI.JointDickman.primeNormalizer_coefficientScale_bound line 20
  3. theorem OAI.JointDickman.auxiliary_selected_odds_bound line 38