OAI/NumberTheory/CubicMoment/Estimates/SemiprimePrimeEstimate.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The centered bilinear estimate for the concrete smooth prime pieces of the semiprime branch. Their coefficient energy is derived from the actual support and the proved norm bound for the roughness transition.

  1. lemma OAI.CubicFirstMoment.bounded_prime_dyad_energy line 14
  2. theorem OAI.CubicFirstMoment.semiprime_prime_bilinear line 28