OAI/NumberTheory/CubicMoment/Theta/CubicThetaShiftedRowFourier.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual inverted row Fourier expansion, with absolute integrated summability proved before interchanging its heat integral and lattice sum.

  1. def OAI.CubicFirstMoment.cubicThetaShiftedRowFourierCoefficient line 14
  2. lemma OAI.CubicFirstMoment.cubicThetaShiftedWeightedHeat_summable line 18
  3. lemma OAI.CubicFirstMoment.cubicThetaShiftedRowHeat_factor line 33
  4. lemma OAI.CubicFirstMoment.cubicThetaShiftedRow_heat_poisson line 58
  5. theorem OAI.CubicFirstMoment.cubicThetaShiftedRow_fourier line 83