OAI/NumberTheory/CubicMoment/Theta/CubicThetaRowGaussBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Elementary bounds and the exact norm of the fixed dual frequency.

  1. lemma OAI.CubicFirstMoment.cubicThetaEisensteinWeight_norm line 10
  2. lemma OAI.CubicFirstMoment.cubicThetaEisensteinGaussCoefficient_norm line 17
  3. def OAI.CubicFirstMoment.cubicThetaRowFrequency line 36
  4. def OAI.CubicFirstMoment.cubicThetaRowHeatScale line 38
  5. lemma OAI.CubicFirstMoment.cubicThetaRowHeatScale_eq line 41
  6. lemma OAI.CubicFirstMoment.cubicThetaRowHeatScale_pos line 49
  7. lemma OAI.CubicFirstMoment.cubicThetaRowHeatScale_zero line 54