OAI/NumberTheory/CubicMoment/Estimates/HeckeUniformLogDerivative.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

A single logarithmic width and a log-squared bound for an entire finite Hecke contour. All zero-free information is derived from the analytic pair.

  1. def OAI.CubicFirstMoment.heckeZeroFreeWidth line 10
  2. def OAI.CubicFirstMoment.heckeLogSquaredConstant line 13
  3. lemma OAI.CubicFirstMoment.heckeZeroFreeWidth_pos line 17
  4. lemma OAI.CubicFirstMoment.heckeZeroFreeWidth_le_one line 23
  5. lemma OAI.CubicFirstMoment.heckeZeroFreeWidth_le_log line 30
  6. lemma OAI.CubicFirstMoment.heckeLogSquaredConstant_pos line 38
  7. lemma OAI.CubicFirstMoment.heckeLogDerivativeBand_le_log_squared line 46
  8. theorem OAI.CubicFirstMoment.hecke_logDeriv_norm_uniform_of_band line 76
  9. theorem OAI.CubicFirstMoment.hecke_logDeriv_norm_uniform_from_analytic_pair line 108