OAI/NumberTheory/CubicMoment/Angular/AngularStoppedLargeDivisorPower.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

At the fixed cutoff b^(1/8), the actual large-divisor rows save a fixed power uniformly in the ambient set of primes.

  1. theorem OAI.CubicFirstMoment.angular_stopped_large_divisor_power_mass line 18