OAI/NumberTheory/CubicMoment/Theta/CubicThetaPoincareSections.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Compactly supported seeds produce actual continuous automorphic sections by a locally finite sum with the cubic multiplier.

  1. lemma OAI.CubicFirstMoment.cubicTheta_compact_translates_locallyFinite line 13
  2. def OAI.CubicFirstMoment.cubicThetaPoincareTerm line 22
  3. lemma OAI.CubicFirstMoment.cubicThetaPoincareTerm_locallyFinite line 26
  4. lemma OAI.CubicFirstMoment.cubicThetaPoincareTerm_continuous line 34
  5. lemma OAI.CubicFirstMoment.cubicThetaPoincareTerm_translate line 38
  6. def OAI.CubicFirstMoment.cubicThetaPoincareSection line 52
  7. lemma OAI.CubicFirstMoment.cubicThetaPoincareSection_compact line 64