OAI/NumberTheory/CubicMoment/Theta/CubicThetaGridJets.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Relative bounds for all actual grid summands, with the zero row and the inadmissible-pair extension included.

  1. lemma OAI.CubicFirstMoment.cubicThetaHeightPower_first_norm line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaHeightPower_second_norm line 18
  3. lemma OAI.CubicFirstMoment.cubicThetaHeightPower_jetBound line 26
  4. lemma OAI.CubicFirstMoment.cubicThetaZero_jetBound line 54
  5. theorem OAI.CubicFirstMoment.cubicThetaEisensteinGrid_jetBound line 59