OAI/NumberTheory/CubicMoment/Decomposition/StoppedDivisorTotal.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Full early-stopped effective-frequency series for a small square divisor. The divisor cost in the absolute tail is absorbed by an explicit power bound.

  1. theorem OAI.CubicFirstMoment.stopped_divisor_noncube_total line 15