OAI/NumberTheory/CubicMoment/Estimates/SemiprimePartition.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The finite smooth partition of the original semiprime kernel. Every prime coordinate retains both its roughness weight and the total-product cutoff; the displayed number of pieces is the actual finite partition.

  1. def OAI.CubicFirstMoment.semiprimePartitionScale line 12
  2. lemma OAI.CubicFirstMoment.semiprimePartitionScale_pos line 14
  3. def OAI.CubicFirstMoment.semiprimePartitionCoefficient line 18
  4. lemma OAI.CubicFirstMoment.semiprimePartitionCoefficient_sum line 22
  5. def OAI.CubicFirstMoment.semiprimePartitionPiece line 39
  6. theorem OAI.CubicFirstMoment.centralSemiprimeProduct_partition line 44