OAI/NumberTheory/CubicMoment/Theta/CubicThetaFarCoordinateTail.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Summable quantitative tails outside the two finite coordinate boxes.

  1. lemma OAI.CubicFirstMoment.cubicThetaPrimary_box_geometric line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaRamified_box_geometric line 28
  3. lemma OAI.CubicFirstMoment.cubicThetaPrimary_far_tail line 45
  4. lemma OAI.CubicFirstMoment.cubicThetaRamified_far_tail line 67