OAI/NumberTheory/CubicMoment/Estimates/PrimeTailHighProduct.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.high_full_prime_envelope_tail_uniform line 14