OAI/NumberTheory/CubicMoment/Estimates/HeckePrimeScales.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Concrete height and conductor scales for the prime contour.

  1. def OAI.CubicFirstMoment.primeContourHeight line 9
  2. def OAI.CubicFirstMoment.primeContourSize line 10
  3. def OAI.CubicFirstMoment.primeContourDenominator line 11
  4. def OAI.CubicFirstMoment.primeContourDecay line 12
  5. lemma OAI.CubicFirstMoment.primeContourHeight_ge_one line 15
  6. lemma OAI.CubicFirstMoment.primeContourDecay_pos line 18
  7. lemma OAI.CubicFirstMoment.primeContourSize_log line 24
  8. lemma OAI.CubicFirstMoment.primeContourSize_bounds line 30
  9. lemma OAI.CubicFirstMoment.primeContourDenominator_ge_one line 44
  10. lemma OAI.CubicFirstMoment.primeContourSize_log_bound line 51
  11. lemma OAI.CubicFirstMoment.primeContourWidth_lower line 60
  12. lemma OAI.CubicFirstMoment.primeContour_shifted_power line 74
  13. lemma OAI.CubicFirstMoment.primeContour_right_power line 94