OAI/NumberTheory/CubicMoment/Angular/AngularHeightCoefficient.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Literal angular prime coefficients and the two signed Mellin rows. Only unit phases are removed; the angular index remains fixed.

  1. def OAI.CubicFirstMoment.angularHeightPrimeCoefficient line 15
  2. lemma OAI.CubicFirstMoment.angularHeightPrimeCoefficient_norm line 18
  3. lemma OAI.CubicFirstMoment.angularHeightPrimeCoefficient_l1 line 23
  4. lemma OAI.CubicFirstMoment.angularHeightPrimeCoefficient_energy line 30
  5. lemma OAI.CubicFirstMoment.angularHeightPrimeCoefficient_sum_squarefree line 39
  6. lemma OAI.CubicFirstMoment.angular_fullStructured_gram_twist line 47
  7. theorem OAI.CubicFirstMoment.angular_fullStructuredPrimeRow_norm line 65
  8. theorem OAI.CubicFirstMoment.angular_fullStructuredPrimeRow_reverse_norm line 97
  9. lemma OAI.CubicFirstMoment.angular_fullPrimeSliceRow_norm_le line 110
  10. lemma OAI.CubicFirstMoment.angular_fullPrimeSliceRow_reverse_norm_le line 142