OAI/NumberTheory/JointDickman/Amplification/ArithmeticSquareHits.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The exact rare-square error for the arithmetic amplification

  1. def OAI.JointDickman.AuxiliarySquareHit line 12
  2. theorem OAI.JointDickman.auxiliarySquare_dvd_period line 15
  3. theorem OAI.JointDickman.residue_square_divisor_mean line 21
  4. theorem OAI.JointDickman.squareHit_indicator_le line 38
  5. theorem OAI.JointDickman.residue_squareHit_mean_bound line 55