OAI/NumberTheory/Ostmann/ZeroDensity/CanonicalRieszKernelBound.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform kernel bounds for the canonical exceptional zeros

For large conductors the Page cutoff is to the right of one half. The remaining finitely many moduli contribute a finite constant.

  1. def OAI.Ostmann.pageRieszKernelNorm line 15
  2. theorem OAI.Ostmann.page_beta_half_for_large_modulus line 18
  3. theorem OAI.Ostmann.canonical_riesz_kernel_bound line 39
  4. theorem OAI.Ostmann.canonicalCharacterRieszTerm_norm_bound line 57