OAI/NumberTheory/CubicMoment/Angular/AngularPrimeCoordinateCollection.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Exact collection of angular coordinate tuples. The same fixed theta factor occurs on each original coordinate and hence on their product.

  1. def OAI.CubicFirstMoment.primaryAngularCoefficientTuple line 14
  2. def OAI.CubicFirstMoment.primaryAngularPrimeIndicatorTuple line 23
  3. lemma OAI.CubicFirstMoment.angular_coordinate_convolution_collection line 28
  4. def OAI.CubicFirstMoment.angularPrimeCoordinateError line 63
  5. lemma OAI.CubicFirstMoment.angular_normalized_prime_tuple_difference line 70
  6. lemma OAI.CubicFirstMoment.angular_primeIndicatorTuple_eq_prime_convolution line 103
  7. def OAI.CubicFirstMoment.primaryAngularSquarefreePrimeTuple line 122
  8. def OAI.CubicFirstMoment.angularSquarefreeCoordinateError line 129
  9. lemma OAI.CubicFirstMoment.angular_primeIndicator_sub_squarefree_cutoff line 136