OAI/NumberTheory/CubicMoment/Estimates/HeckeNormalizedDisk.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Normalize a complete Hecke function at 2+it on a disk of radius 3. The resulting bound is explicit in the finite and archimedean conductor.

  1. def OAI.CubicFirstMoment.normalizedHeckeDisk line 12
  2. def OAI.CubicFirstMoment.normalizedHeckeDiskBound line 15
  3. lemma OAI.CubicFirstMoment.normalizedHeckeDiskBound_gt_one line 18
  4. lemma OAI.CubicFirstMoment.normalizedHeckeDisk_differentiable line 26
  5. lemma OAI.CubicFirstMoment.normalizedHeckeDisk_zero line 31
  6. lemma OAI.CubicFirstMoment.normalizedHeckeDisk_logDeriv line 35
  7. theorem OAI.CubicFirstMoment.normalizedHeckeDisk_bound line 52