OAI/NumberTheory/CubicMoment/Angular/AngularPrimeTailLowProduct.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The logarithmic-height tail for the actual independent prime products. The bound is uniform over unit coordinate weights and preserves the full product envelope, without requiring a new analytic input.

  1. theorem OAI.CubicFirstMoment.angular_low_full_prime_envelope_tail line 17