OAI/NumberTheory/CubicMoment/Angular/AngularStoppedRoughDivisorLog.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Summed nonempty divisor rows have arbitrary logarithmic savings. No cancellation is assumed for the empty row in this arithmetic estimate.

  1. theorem OAI.CubicFirstMoment.angular_stopped_rough_divisor_log line 20