OAI/NumberTheory/Ostmann/ZeroDensity/InducedCharacterRieszDecay.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform Riesz estimates for all characters at the ambient modulus

  1. def OAI.Ostmann.reducedRieszMain line 12
  2. theorem OAI.Ostmann.induced_character_riesz_decay line 17