OAI/NumberTheory/CubicMoment/Theta/CubicThetaShiftedInvertedRows.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Primitive rows at the translated inverted cusps used by the primary coefficient projector. The phase is kept as the actual cubic symbol; its ramified evaluation is a subsequent arithmetic step.

  1. lemma OAI.CubicFirstMoment.cubicTheta_primary_add_three_mul line 12
  2. def OAI.CubicFirstMoment.cubicThetaShiftedInvertedRowEquiv line 19
  3. def OAI.CubicFirstMoment.cubicThetaShiftedInversion line 42
  4. lemma OAI.CubicFirstMoment.cubicThetaShiftedInversion_complex line 45
  5. lemma OAI.CubicFirstMoment.cubicThetaMobius_shiftedInversion line 56
  6. lemma OAI.CubicFirstMoment.cubicThetaBottomRow_height_shiftedInverted line 62
  7. def OAI.CubicFirstMoment.cubicThetaShiftedInvertedTerm line 75
  8. theorem OAI.CubicFirstMoment.cubicThetaEisenstein_shiftedInverted line 79