OAI/NumberTheory/CubicMoment/Angular/AngularShortOuterWindow.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Sum the actual Gauss cutoff window over short outer levels. The squarefree restriction is justified by the Gauss sum, and the coefficient mass comes from the published primary-prime input.

  1. theorem OAI.CubicFirstMoment.angular_short_outer_window_bound line 15