OAI/NumberTheory/CubicMoment/Angular/AngularPrimeTailHighProduct.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A single power-width exponent for every actual independent prime product. The exponent is chosen before the coordinate types and arities; all finite energies follow from unit weights and actual support counting.

  1. theorem OAI.CubicFirstMoment.angular_high_full_prime_envelope_tail_uniform line 16