OAI/NumberTheory/CubicMoment/Theta/CubicThetaHighWindowSeries.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The high defect is an actual compact automorphic section supported in the single principal cusp above height two.

  1. def OAI.CubicFirstMoment.cubicThetaHighWindowTerm line 13
  2. def OAI.CubicFirstMoment.cubicThetaHighWindowSeries line 16
  3. lemma OAI.CubicFirstMoment.cubicThetaHighWindowTerm_translate line 19
  4. theorem OAI.CubicFirstMoment.cubicThetaHighWindowSeries_automorphy line 35
  5. theorem OAI.CubicFirstMoment.cubicThetaHighWindowSeries_compact_sum line 45
  6. lemma OAI.CubicFirstMoment.cubicThetaHighWindowSeries_continuousOn line 56
  7. theorem OAI.CubicFirstMoment.cubicThetaHighWindowSeries_core line 76
  8. def OAI.CubicFirstMoment.cubicThetaHighWindowSection line 96
  9. lemma OAI.CubicFirstMoment.cubicThetaHighWindowSection_compact line 106
  10. lemma OAI.CubicFirstMoment.cubicThetaHighWindowSeries_high line 117