# Gauss Sums and the Pólya–Vinogradov Inequality

 Title: Gauss Sums and the Pólya–Vinogradov Inequality Authors: Rodrigo Raya and Manuel Eberl Submission date: 2019-12-10 Abstract: This article provides a full formalisation of Chapter 8 of Apostol's Introduction to Analytic Number Theory. Subjects that are covered are: periodic arithmetic functions and their finite Fourier series (generalised) Ramanujan sums Gauss sums and separable characters induced moduli and primitive characters the Pólya—Vinogradov inequality BibTeX: ```@article{Gauss_Sums-AFP, author = {Rodrigo Raya and Manuel Eberl}, title = {Gauss Sums and the Pólya–Vinogradov Inequality}, journal = {Archive of Formal Proofs}, month = dec, year = 2019, note = {\url{http://isa-afp.org/entries/Gauss_Sums.html}, Formal proof development}, ISSN = {2150-914x}, }``` License: BSD License Depends on: Dirichlet_L, Dirichlet_Series, Polynomial_Interpolation