OAI/NumberTheory/CubicMoment/Estimates/SemiprimeFullSupport.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

In a semiprime piece the full independent smooth prime supports can replace the auxiliary cutoff at 3X. Extra primes give a zero product envelope; missing primes have zero coordinate weight.

  1. def OAI.CubicFirstMoment.semiprimeFullSupport line 14
  2. lemma OAI.CubicFirstMoment.semiprimeFullSupport_mem line 19
  3. lemma OAI.CubicFirstMoment.centeredHeightKernel_large_factor line 25
  4. theorem OAI.CubicFirstMoment.semiprimePartitionPiece_full_support line 39