OAI/NumberTheory/CubicMoment/Theta/CubicThetaRadialProfileSeries.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Compact radial profiles give actual automorphic sections by a locally finite Poincaré sum. No spectral input is used.

  1. def OAI.CubicFirstMoment.cubicThetaRadialProfileTerm line 16
  2. def OAI.CubicFirstMoment.cubicThetaRadialProfileSeries line 19
  3. lemma OAI.CubicFirstMoment.cubicThetaRadialProfileTerm_translate line 22
  4. theorem OAI.CubicFirstMoment.cubicThetaRadialProfileSeries_automorphy line 38
  5. theorem OAI.CubicFirstMoment.cubicThetaRadialProfileSeries_compact_sum line 48
  6. lemma OAI.CubicFirstMoment.cubicThetaRadialProfileSeries_continuousOn line 59
  7. theorem OAI.CubicFirstMoment.cubicThetaRadialProfileSeries_core line 80
  8. def OAI.CubicFirstMoment.cubicThetaRadialProfileSection line 105
  9. lemma OAI.CubicFirstMoment.cubicThetaRadialProfileSection_compact line 116
  10. lemma OAI.CubicFirstMoment.cubicThetaRadialProfileSeries_high line 128