OAI/NumberTheory/CubicMoment/Angular/AngularStoppedSmallDivisorMass.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Sum the hybrid core bound over actual short divisor rows. The rough lower cutoff is used only in the elementary small-core term; the two hybrid terms are summed by convergent norm series.

  1. theorem OAI.CubicFirstMoment.angular_stopped_small_divisor_mass line 19