OAI/NumberTheory/CubicMoment/Theta/CubicThetaRamifiedResidueSystem.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The literal three-row ramified expansion at the actual theta pole. All unit twists are retained as frequencies of the same arithmetic residue.

  1. instance OAI.CubicFirstMoment.(instance at line 14) line 14
  2. instance OAI.CubicFirstMoment.(instance at line 16) line 16
  3. lemma OAI.CubicFirstMoment.cubicThetaRamifiedFactor_analytic line 18
  4. def OAI.CubicFirstMoment.cubicThetaRamifiedShortContinuation line 29
  5. lemma OAI.CubicFirstMoment.cubicThetaRamifiedShortContinuation_analytic line 33
  6. lemma OAI.CubicFirstMoment.cubicThetaRamifiedShortContinuation_right line 45
  7. theorem OAI.CubicFirstMoment.cubicThetaRamifiedShortContinuation_eq line 59
  8. theorem OAI.CubicFirstMoment.cubicThetaArithmeticFourierResidue_ramified_finite line 79
  9. theorem OAI.CubicFirstMoment.cubicThetaArithmeticFourierResidue_lambda_square_system line 94