OAI/NumberTheory/CubicMoment/Estimates/SemiprimeGaussTailRange.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The original nonzero Gauss window supplies its actual prime lengths. No range is inferred from the centered semiprime kernel.

  1. lemma OAI.CubicFirstMoment.semiprimeGaussTail_kernel_product_range line 14
  2. lemma OAI.CubicFirstMoment.semiprimeGaussTail_piece_lengths line 32
  3. lemma OAI.CubicFirstMoment.semiprimeGaussTailPiece_symm line 51
  4. lemma OAI.CubicFirstMoment.semiprimeGaussTailPiece_nonzero_lengths line 62
  5. theorem OAI.CubicFirstMoment.eventually_semiprimeGaussTail_admissible line 80