OAI/NumberTheory/CubicMoment/Theta/CubicThetaShiftedModelSeries.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The absolutely convergent arithmetic series determined by the proved other-cusp coefficients. Its constant coefficient is explicitly zero.

  1. lemma OAI.CubicFirstMoment.cubicThetaShiftedFrequency_third line 15
  2. lemma OAI.CubicFirstMoment.cubicThetaShiftedNormalizedCoefficient_bound line 21
  3. def OAI.CubicFirstMoment.cubicThetaShiftedBareTerm line 34
  4. lemma OAI.CubicFirstMoment.cubicThetaShiftedBareTerm_summable line 37
  5. def OAI.CubicFirstMoment.cubicThetaShiftedModelTerm line 56
  6. lemma OAI.CubicFirstMoment.cubicThetaShiftedModelTerm_summable line 60
  7. def OAI.CubicFirstMoment.cubicThetaShiftedModelTorus line 72
  8. lemma OAI.CubicFirstMoment.cubicThetaShiftedModelTorus_summable line 75
  9. lemma OAI.CubicFirstMoment.cubicThetaShiftedModelTorus_coefficient line 81
  10. def OAI.CubicFirstMoment.cubicThetaShiftedModelSeries line 96
  11. lemma OAI.CubicFirstMoment.cubicThetaShiftedModelTorus_real line 100