OAI/NumberTheory/CubicMoment/Theta/CubicThetaHeatSmallHeight.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

At small height the normalized nonzero-frequency heat integral tends to the ordinary Gamma integral. This supplies nonvanishing without any assumption on special-function zeros.

  1. def OAI.CubicFirstMoment.cubicThetaNormalizedHeat line 13
  2. lemma OAI.CubicFirstMoment.cubicThetaNormalizedHeat_bound line 16
  3. theorem OAI.CubicFirstMoment.cubicThetaNormalizedHeat_gamma_limit line 25