OAI/NumberTheory/CubicMoment/Theta/CubicThetaRamifiedResidueFormula.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Explicit solution of the actual ramified residue system. The phase is obtained from the finite rows and uniqueness from their strict contraction.

  1. instance OAI.CubicFirstMoment.(instance at line 11) line 11
  2. def OAI.CubicFirstMoment.cubicThetaRamifiedPhaseCandidate line 14
  3. lemma OAI.CubicFirstMoment.cubicThetaRamifiedPhaseCandidate_neg line 18
  4. lemma OAI.CubicFirstMoment.cubicThetaRamifiedPhaseCandidate_system line 23
  5. theorem OAI.CubicFirstMoment.cubicThetaArithmeticFourierResidue_lambda_square_unit line 66
  6. theorem OAI.CubicFirstMoment.cubicThetaArithmeticFourierResidue_lambda_square line 96