OAI/NumberTheory/CubicMoment/Theta/CubicThetaShiftedSeriesIdentity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Reconstruction of the actual translated-cusp section from its computed coefficients. The nontrivial cusp has no constant mode.

  1. lemma OAI.CubicFirstMoment.cubicThetaShiftedCell_integral_scaled line 16
  2. lemma OAI.CubicFirstMoment.cubicThetaShiftedModelHorizontal_term line 23
  3. lemma OAI.CubicFirstMoment.cubicThetaShiftedModelSeries_coefficient line 38
  4. theorem OAI.CubicFirstMoment.cubicThetaShiftedSeriesIdentity line 47