OAI/NumberTheory/CubicMoment/Theta/CubicThetaShiftedTorus.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The actual continuous Fourier expansion at a translated cusp, parametrized by its period-nine torus. All frequencies, including zero, are retained until the explicit arithmetic support is applied.

  1. def OAI.CubicFirstMoment.cubicThetaShiftedFourierTerm line 17
  2. lemma OAI.CubicFirstMoment.cubicThetaShiftedFourierTerm_summable line 21
  3. def OAI.CubicFirstMoment.cubicThetaShiftedTorusSeries line 29
  4. lemma OAI.CubicFirstMoment.cubicThetaShiftedTorusSeries_summable line 32
  5. lemma OAI.CubicFirstMoment.cubicThetaShifted_frequency_cell line 39
  6. lemma OAI.CubicFirstMoment.cubicThetaShiftedTorusSeries_real line 46
  7. def OAI.CubicFirstMoment.cubicThetaShiftedTorus line 64
  8. lemma OAI.CubicFirstMoment.cubicThetaShiftedTorus_real line 68
  9. lemma OAI.CubicFirstMoment.cubicThetaShiftedTorusSeries_coefficient line 78