OAI/NumberTheory/CubicMoment/Angular/AngularStoppedDivisorTotal.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.angular_stopped_divisor_noncube_total line 19