OAI/NumberTheory/CubicMoment/Theta/CubicThetaCentralSemiprimePrimeEstimate.lean

GitHub source file

1 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. theorem OAI.CubicFirstMoment.semiprime_prime_bilinear_actual line 15