OAI/NumberTheory/CubicMoment/Theta/CubicThetaShiftedUnfold.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Literal primary-row unfolding at every translated inverted cusp. Absolute convergence follows from equality of the actual row norms.

  1. def OAI.CubicFirstMoment.cubicThetaShiftedGridTerm line 13
  2. lemma OAI.CubicFirstMoment.cubicThetaShiftedGridTerm_admissible line 20
  3. lemma OAI.CubicFirstMoment.cubicThetaShiftedInvertedTerm_norm line 28
  4. lemma OAI.CubicFirstMoment.cubicThetaShiftedInvertedTerm_summable line 37
  5. lemma OAI.CubicFirstMoment.cubicThetaShiftedGrid_summable line 43
  6. theorem OAI.CubicFirstMoment.cubicThetaEisenstein_shifted_grid line 60
  7. lemma OAI.CubicFirstMoment.cubicThetaShiftedGridTerm_triple line 78