OAI/NumberTheory/CubicMoment/Angular/AngularNumeratorCharacter.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The angular numerator character on the original modulus 9*v. The finite correction at three is absorbed into this modulus, so its norm bound remains 81*N(v).

  1. def OAI.CubicFirstMoment.angularNumeratorLift line 12
  2. lemma OAI.CubicFirstMoment.angularNumeratorLift_congr line 15
  3. lemma OAI.CubicFirstMoment.angularNumeratorLift_mul line 24
  4. def OAI.CubicFirstMoment.angularNumeratorChar line 29
  5. lemma OAI.CubicFirstMoment.angularNumeratorChar_mk line 49
  6. lemma OAI.CubicFirstMoment.angularNumeratorChar_primary line 55
  7. lemma OAI.CubicFirstMoment.angularNumeratorChar_compatible line 61