OAI/NumberTheory/JointDickman/Probability/OppositeResidueProduct.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Product estimates at the opposite endpoint Fourier frequency

  1. theorem OAI.JointDickman.sum_neg_residue_square line 10
  2. theorem OAI.JointDickman.restricted_opposite_residue_product_error_bound line 14