OAI/NumberTheory/JointDickman/Amplification/ArithmeticAmplificationBounds.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Uniform bounds for the actual arithmetic amplification

  1. def OAI.JointDickman.arithmeticSiteWeight line 12
  2. theorem OAI.JointDickman.arithmeticSiteWeight_nonneg line 20
  3. theorem OAI.JointDickman.arithmeticSiteWeight_le line 29
  4. theorem OAI.JointDickman.arithmeticSubsetAmplification_nonneg line 57
  5. theorem OAI.JointDickman.arithmeticSubsetAmplification_le line 73