OAI/NumberTheory/Ostmann/ZeroDensity/SmoothNonprincipalDecay.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The nonprincipal part of manuscript Lemma 5.3

This is derived from the three precisely recorded analytic inputs. The exception is one entire primitive character, uniformly for every finite family.

  1. theorem OAI.Ostmann.smooth_nonprincipal_decay line 16