OAI/NumberTheory/CubicMoment/Estimates/SemiprimeBilinear.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual detector semiprime kernel has independent prime variables. Its roughness factors can therefore be absorbed into the two coefficients before applying the centered bilinear estimates.

  1. lemma OAI.CubicFirstMoment.prime_pair_tuple_sum line 14
  2. def OAI.CubicFirstMoment.semiprimeRoughWeight line 40
  3. lemma OAI.CubicFirstMoment.semiprimeRoughWeight_norm_le line 43
  4. lemma OAI.CubicFirstMoment.semiprimeRoughWeight_zero line 52
  5. theorem OAI.CubicFirstMoment.centralSemiprimeProduct_eq_bilinear line 58