OAI/NumberTheory/CubicMoment/Theta/CubicThetaNonzeroRowHeat.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The literal two-coordinate Gaussian behind the nonzero-first-row bound.

  1. abbrev OAI.CubicFirstMoment.CubicThetaNonzeroRow line 9
  2. def OAI.CubicFirstMoment.cubicThetaNonzeroRowQuadratic line 11
  3. def OAI.CubicFirstMoment.cubicThetaNonzeroRowHeatTerm line 14
  4. lemma OAI.CubicFirstMoment.cubicThetaNonzeroRowHeatTerm_factor line 17
  5. lemma OAI.CubicFirstMoment.cubicThetaNonzeroRowHeatTerm_row_summable line 29
  6. lemma OAI.CubicFirstMoment.cubicThetaNonzeroRowHeatTerm_row line 35
  7. lemma OAI.CubicFirstMoment.cubicThetaNonzeroRowHeatTerm_summable line 43
  8. theorem OAI.CubicFirstMoment.cubicThetaNonzeroRowHeatTerm_tsum line 52