OAI/NumberTheory/JointDickman/Analysis/ZetaLogFrequency.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Zeta growth on polynomial logarithmic frequency ranges away from the pole

The regularized Dirichlet series has small power growth, and the pole term is bounded when the frequency has absolute value at least one.

  1. lemma OAI.JointDickman.zeta_log_frequency_norm line 14