Formalization of p-adic L-functions in Lean 3

MaRDI QIDQ6427890zbMATH OpenFDO

Authors Ashvni Narayanan

Publication date 28 February 2023

Abstract: The Euler--Riemann zeta function is a largely studied numbertheoretic object, and the birthplace of several conjectures, such as the Riemann Hypothesis. Different approaches are used to study it, including $p$-adic analysis : deriving information from $p$-adic zeta functions. A generalized version of $p$-adic zeta functions (Riemann zeta function) are $p$-adic $L$-functions (resp. Dirichlet $L$-functions). This paper describes formalization of $p$-adic $L$-functions in an interactive theorem prover Lean 3. Kubota--Leopoldt $p$-adic $L$-functions are meromorphic functions emerging from the special values they take at negative integers in terms of generalized Bernoulli numbers. They also take twisted values of the Dirichlet $L$-function at negative integers. This work has never been done before in any theorem prover. Our work is done with the support of lean{mathlib} 3, one of Lean's mathematical libraries. It required formalization of a lot of associated topics, such as Dirichlet characters, Bernoulli polynomials etc. We formalize these first, then the definition of a $p$-adic $L$-function in terms of an integral with respect to the Bernoulli measure, proving that they take the required values at negative integers.

This page was built for publication: Formalization of $p$-adic $L$-functions in Lean 3

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6427890)