OAI/NumberTheory/CubicMoment/Estimates/SemiprimeCentralWindow.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Summing every actual semiprime norm piece in the central Mellin window. Only zero original pieces are omitted, and their complementary Mellin remainder stays explicit in the exact decomposition.

  1. def OAI.CubicFirstMoment.semiprimeCentralMellinSum line 15
  2. def OAI.CubicFirstMoment.semiprimeMellinRemainder line 21
  3. theorem OAI.CubicFirstMoment.centralSemiprimeProduct_mellin_decomposition line 27
  4. lemma OAI.CubicFirstMoment.semiprimePartitionCount_log_bound line 42
  5. theorem OAI.CubicFirstMoment.semiprime_central_mellin_isLittleO line 55