OAI/NumberTheory/CubicMoment/Estimates/SemiprimeHeightEstimate.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The height mean of 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_height_bilinear line 15