OAI/NumberTheory/CubicMoment/Theta/CubicThetaHighHeatNonzero.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

For each parameter in Re(s)>1, the genuine Fourier heat kernel is nonzero at some height above two. This removes the possible common-zero obstruction for compact radial tests.

  1. lemma OAI.CubicFirstMoment.cubicThetaComplexHeightIntegral_real line 14
  2. lemma OAI.CubicFirstMoment.cubicThetaComplexHeightIntegral_real_zero_iff line 25
  3. theorem OAI.CubicFirstMoment.cubicThetaHighHeat_nonzero line 40