OAI/NumberTheory/CubicMoment/Estimates/PrimeGroupTailEnvelope.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Full-line Mellin restoration for the enlarged-range height tail. The original smooth product envelope and every height window remain present.

  1. theorem OAI.CubicFirstMoment.primeGroupTail_envelope_log_saving line 14