OAI/NumberTheory/CubicMoment/Angular/AngularTypeILow.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The fixed nonzero-angular low-height Type-I estimate. The short and long inverse sums are actual finite sums, and the coefficient masses are deduced from the literal primary-divisor bound.

  1. theorem OAI.CubicFirstMoment.angular_typeI_low_squarefree_of_published line 19
  2. theorem OAI.CubicFirstMoment.angular_typeI_low_of_published line 117