OAI/NumberTheory/Ostmann/ZeroDensity/CharacterGammaShift.lean
4 declarations, 0 contain sorry, 0 declared as axioms
Uniform shifted Gamma factors for actual primitive characters
- theorem
OAI.Ostmann.character_gamma_shiftline 13 - def
OAI.Ostmann.densityCompletedSquareWeightline 27 - theorem
OAI.Ostmann.gaussian_linear_abs_boundline 32 - theorem
OAI.Ostmann.densityCompletedSquareWeight_boundline 39