OAI/NumberTheory/CubicMoment/Theta/CubicThetaAdaptedMultiplier.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A principal-level decomposition evaluates the common multiplier for cusp lifts with both diagonal entries zero modulo three.

  1. lemma OAI.CubicFirstMoment.cubicThetaFullTranslation_neg line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaRightInversion_matrix line 20
  3. lemma OAI.CubicFirstMoment.cubicThetaRightInversion_mem line 29
  4. def OAI.CubicFirstMoment.cubicThetaRightInversionPrincipal line 43
  5. lemma OAI.CubicFirstMoment.cubicThetaRightInversion_value line 47
  6. theorem OAI.CubicFirstMoment.cubicThetaPrimaryBottom_multiplier_adapted line 57