OAI/NumberTheory/CubicMoment/Theta/CubicThetaPrimeCubeFirstPeriodization.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The first character branch as an actual periodic finite sum. The coefficient is extended by zero on nonunits before additive reindexing.

  1. def OAI.CubicFirstMoment.cubicThetaPrimeCubeFirstTerm line 12
  2. def OAI.CubicFirstMoment.cubicThetaPrimeCubeFirstPeriodization line 15
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeFirstTerm_congr line 18
  4. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeFirstTerm_shift line 39
  5. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeFirstPeriodization_periodic line 57
  6. lemma OAI.CubicFirstMoment.cubicThetaPrimeCubeFirstPeriodization_continuous line 81