OAI/NumberTheory/CubicMoment/Estimates/SemiprimeRange.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Actual nonzero semiprime pieces lie in the balanced prime range. The upper bilinear constraint follows from a strict power gap, uniformly for every fixed logarithmic exponent required by the published inputs.

  1. lemma OAI.CubicFirstMoment.semiprimePartitionCoefficient_range line 14
  2. lemma OAI.CubicFirstMoment.semiprime_kernel_product_range line 30
  3. lemma OAI.CubicFirstMoment.semiprime_piece_lengths line 48
  4. theorem OAI.CubicFirstMoment.eventually_semiprime_upper_range line 67
  5. lemma OAI.CubicFirstMoment.semiprimePartitionPiece_symm line 104
  6. lemma OAI.CubicFirstMoment.semiprimePartitionPiece_nonzero_lengths line 115
  7. theorem OAI.CubicFirstMoment.eventually_semiprime_admissible line 133
  8. lemma OAI.CubicFirstMoment.semiprime_log_comparison line 165
  9. lemma OAI.CubicFirstMoment.eventually_semiprime_height_comparison line 173
  10. lemma OAI.CubicFirstMoment.semiprime_bilinear_scale line 197