OAI/NumberTheory/Ostmann/ZeroDensity/SmallDiskLogDerivative.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A fixed small-disk logarithmic-derivative estimate

  1. theorem OAI.Ostmann.logDeriv_norm_le_small_disk line 11
  2. theorem OAI.Ostmann.logDeriv_norm_le_five_quarters_disk line 54