OAI/NumberTheory/JointDickman/Amplification/TwoFormLocalBound.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Two distinct affine roots and their weighted interval bound

  1. theorem OAI.JointDickman.sum_two_residueWeights_bound line 13
  2. theorem OAI.JointDickman.affine_residue_root line 23
  3. theorem OAI.JointDickman.formRootWeight_two line 29
  4. theorem OAI.JointDickman.two_form_interval_sieve line 38