OAI/NumberTheory/CubicMoment/Angular/AngularStoppedLargeDivisorMass.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Sum the large-divisor rows using genuine quotient lengths. The distinct-prime-subset map is injective, so the estimates involve convergent lattice norm series and no cardinality of the ambient prime set.

  1. theorem OAI.CubicFirstMoment.angular_stopped_large_divisor_mass line 19