OAI/NumberTheory/CubicMoment/Estimates/SinglePrimeHeight.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The published-input height mean for a single genuine prime coordinate. This is used for the complementary Mellin frequencies of the semiprime branch.

  1. def OAI.CubicFirstMoment.uniformLogWeights_prime_coordinates line 13
  2. theorem OAI.CubicFirstMoment.single_prime_height_bilinear line 23