OAI/NumberTheory/CubicMoment/Theta/CubicThetaCuspTypes.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The three translated inversion types needed for primary bottom rows. The actual constant is retained at the trivial type.

  1. lemma OAI.CubicFirstMoment.cubicThetaFullTranslation_add line 13
  2. lemma OAI.CubicFirstMoment.cubicThetaShiftedInversion_factor line 21
  3. lemma OAI.CubicFirstMoment.cubicThetaNormalizedSeries_integer_translation line 29
  4. lemma OAI.CubicFirstMoment.cubicThetaNormalizedSeries_triple_translation line 42
  5. lemma OAI.CubicFirstMoment.cubicThetaNormalizedSeries_shifted_trivial line 50
  6. lemma OAI.CubicFirstMoment.cubicThetaNormalizedSeries_shifted_nontrivial line 62
  7. def OAI.CubicFirstMoment.cubicThetaCuspExpansion line 74
  8. theorem OAI.CubicFirstMoment.cubicThetaNormalizedSeries_shifted_complete line 80
  9. theorem OAI.CubicFirstMoment.cubicThetaNormalizedSeries_primaryBottom_complete line 89