OAI/NumberTheory/CubicMoment/Angular/AngularPrimeGroupTailProductEnvelope.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The full retained-envelope high tail for the actual two independent prime convolutions. Every Mellin frequency is retained; the energies are derived.

  1. theorem OAI.CubicFirstMoment.angular_primeGroupTail_full_prime_envelope_tail line 17