OAI/NumberTheory/CubicMoment/Decomposition/PrimeProductHeight.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The exact sharp comparison through a smooth total-product weight. The model tail and the endpoint error remain negligible uniformly in this fixed weight, so the remaining integrals are precisely the detector kernels.

  1. def OAI.CubicFirstMoment.primeProductLowHeight line 15
  2. def OAI.CubicFirstMoment.primeProductGaussTail line 18
  3. lemma OAI.CubicFirstMoment.primeProductLowHeight_eq line 22
  4. lemma OAI.CubicFirstMoment.sharp_prime_product_low_tail line 35
  5. theorem OAI.CubicFirstMoment.prime_product_model_log_tail_isLittleO line 68
  6. theorem OAI.CubicFirstMoment.sharp_prime_product_log_height_remainder line 93