OAI/NumberTheory/CubicMoment/Estimates/HeckeZeroFreePair.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The zero-free step for a nonreal character and its square. The inputs are the actual entire continuations and proved disk bounds; no prime-sum or zero-free assertion is assumed.

  1. def OAI.CubicFirstMoment.principalPoleConstant line 12
  2. def OAI.CubicFirstMoment.principalPoleRadius line 14
  3. lemma OAI.CubicFirstMoment.principalPoleConstant_pos line 16
  4. lemma OAI.CubicFirstMoment.principalPoleRadius_pos line 19
  5. lemma OAI.CubicFirstMoment.principalPoleBound line 22
  6. lemma OAI.CubicFirstMoment.diskLogDerivativeConstant_pos line 26
  7. def OAI.CubicFirstMoment.heckePairZeroFreeError line 31
  8. lemma OAI.CubicFirstMoment.heckePairZeroFreeError_ge_one line 36
  9. theorem OAI.CubicFirstMoment.hecke_zero_free_of_disk_pair line 49