OAI/NumberTheory/CubicMoment/Estimates/HeckeDiskGrowth.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Polynomial and logarithmic conductor-height bounds for the actual normalized Hecke disks. The constants depend only on the fixed ideal lattice.

  1. def OAI.CubicFirstMoment.heckeDiskPolynomialConstant line 10
  2. lemma OAI.CubicFirstMoment.heckeDiskPolynomialConstant_gt_one line 12
  3. theorem OAI.CubicFirstMoment.normalizedHeckeDiskBound_polynomial line 17
  4. theorem OAI.CubicFirstMoment.normalizedHeckeDiskBound_log line 46
  5. def OAI.CubicFirstMoment.heckePairLogConstant line 58
  6. lemma OAI.CubicFirstMoment.heckePairLogConstant_pos line 63
  7. theorem OAI.CubicFirstMoment.heckePairZeroFreeError_log line 72