OAI/NumberTheory/CubicMoment/Theta/CubicThetaNonzeroHeat.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The nonzero Fourier heat integral is entire in the Eisenstein parameter: its positive and reciprocal exponential factors control both ends of the Mellin integral.

  1. def OAI.CubicFirstMoment.cubicThetaDoubleHeat line 14
  2. lemma OAI.CubicFirstMoment.cubicThetaDoubleHeat_continuous line 17
  3. lemma OAI.CubicFirstMoment.cubicThetaDoubleHeat_top line 25
  4. lemma OAI.CubicFirstMoment.cubicThetaDoubleHeat_bottom line 34
  5. lemma OAI.CubicFirstMoment.cubicThetaDoubleHeat_mellinConvergent line 51
  6. lemma OAI.CubicFirstMoment.cubicThetaDoubleHeat_mellin_entire line 58
  7. lemma OAI.CubicFirstMoment.cubicThetaDualHeat_eq_mellin line 66
  8. theorem OAI.CubicFirstMoment.cubicThetaNonzeroHeat_entire line 74