OAI/NumberTheory/CubicMoment/Decomposition/StoppedRoughDivisorLog.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.stopped_rough_divisor_log line 16