Why construct a p-adic L-function?

A modular form has a complex L-function whose critical values carry arithmetic information. To compare those values in p-adic families, their transcendental period factors must first be removed. The remaining algebraic numbers can then be embedded into a p-adic field. The result sought here is a single bounded measure encoding the critical values of all twists by characters of p-power conductor. This is the existence and interpolation theorem underlying the cyclotomic p-adic L-function (one of the most fundamental objects of Iwasawa theory).

The reference is the famous paper of Mazur, Tate and Teitelbaum, Chapter I, especially §§10–14 (MTT); but for simplicity we are treating only the ordinary case here (not the more general finite-slope case), and not attacking the results later in MTT (exceptional-zero conjectures, etc).

Modular forms, periods, and measures

Fix a prime $p$, a positive integer $N$, and a weight $k\ge2$. Let $f$ be a normalized cuspidal Hecke eigenform of weight $k$ on $\Gamma_1(N)$ with nebentypus $\epsilon$ and Fourier coefficients $a_n$ (necessarily algebraic). Fix embeddings $\iota_\infty:\overline{\mathbb Q}\hookrightarrow\mathbb C$ and $\iota_p:\overline{\mathbb Q}\hookrightarrow\mathbb C_p$. No condition $p\nmid N$ is imposed. The character $\epsilon$ is extended by zero on nonunits modulo $N$.

The form is ordinary when $|\iota_p(a_p)|_p=1$. The ordinary root $\alpha$ is the root of

$$X^2-\iota_p(a_p)X+\iota_p(\epsilon(p))p^{k-1}$$

with $|\alpha|_p=1$. This convention also covers the $U_p$ case: if $p\mid N$, then $\epsilon(p)=0$ and the unit root is $\iota_p(a_p)$ (MTT I.§12).

A measure means a continuous $\mathbb C_p$-linear functional on the continuous functions $C(\mathbb Z_p^\times,\mathbb C_p)$. It is a bounded p-adic measure, rather than a positive real-valued measure. The Lean representation is Mathlib's AbstractMeasure on (PadicInt p)ˣ.

The two periods $\Omega^+$ and $\Omega^-$ normalize the signed modular integrals. Write

$$\Phi_j(r)=2\pi\int_0^\infty f(r+it)(r+it)^j\,dt,$$

and use $(\Phi_j(r)+s(-1)^j\Phi_j(-r))/2$ for sign $s\in\{+1,-1\}$. A period system specifies nonzero periods, algebraic normalized values for $0\le j\le k-2$, and finite generation over $\mathbb Z$ of the lattice generated by these values. Period rationality and finite generation are separate mathematical obligations, combining Manin–Shimura rationality with the module-of-values construction in MTT I.§2; see also the explicit treatment of general eigenforms in Williams, §11.7.

Formalization targets

The goal is to construct an ordinary root, a period system, and a measure $\mu$ with the following interpolation property. Let $\chi$ be a primitive Dirichlet character of conductor $m=p^n$, where $n\ge0$, and let $0\le j\le k-2$. Put $s=\chi(-1)(-1)^j$. With the positive-exponential Gauss sum $\tau(\chi)=\sum_{a\bmod m}\chi(a)e^{2\pi ia/m}$, define the algebraic number $A_{\chi,j}$ by

$$\iota_\infty(A_{\chi,j})= \frac{m^{j+1}j!}{(-2\pi i)^j\tau(\chi^{-1})\Omega^s} L(f_{\chi^{-1}},j+1).$$

The required identity is

$$\int_{\mathbb Z_p^\times}\iota_p(\chi(x))x^j\,d\mu(x) =e_p(\alpha,\chi,j)\,\iota_p(A_{\chi,j}),$$

where all algebraic character values in the following expression are transported by $\iota_p$:

$$e_p(\alpha,\chi,j)=\alpha^{-n} \left(1-\frac{\iota_p(\chi^{-1}(p)\epsilon(p))p^{k-2-j}}{\alpha}\right) \left(1-\frac{\iota_p(\chi(p))p^j}{\alpha}\right).$$

This is the scalar period-normalized form of MTT I.§14. At $n>0$ both character values at $p$ vanish, leaving $\alpha^{-n}$. At $n=0$ the primitive character is the character of modulus one, and both Euler factors remain. The latter case is included explicitly.

Seven milestones isolate period rationality and its finite lattice; existence and uniqueness of the ordinary root; the distribution relation for polynomial disk moments; uniform boundedness of constant disk masses; unique extension to a measure with every critical polynomial moment; the complex Birch–Mellin identity; and the deduction of interpolation from the two signed measures. Their source locations are recorded individually. The period milestone combines two standard inputs; the boundedness and extension milestones specialize the MTT construction to slope zero.

What the formalization supplies

The result supplies the analytic input for studying p-adic special values and their variation. It also supplies reusable infrastructure for normalized modular integrals, rational period systems, finite-order twists, and bounded measures on p-adic units. The classical existence theorem is known. The work proposed here is to prove the stated Lean theorems and connect the existing Mathlib analytic and algebraic infrastructure. Local compilation establishes that the declarations are well-typed; the mission statements remain unproved targets.

Where the difficulty lies

Listing algebraic critical values does not establish that one bounded measure interpolates them. Values on nested residue disks must satisfy compatibility, and ordinary boundedness must control the extension to continuous functions. Polynomial moments of positive degree must agree with that same extension. The unramified character requires its own Euler-factor calculation; simply applying the ramified formula at conductor one loses factors. On the complex side, rationality requires genuine periods of the modular form, not arbitrary chosen scaling constants. These are the obligations represented by the milestones.

Formalization scope and conventions

The cusp form is Mathlib's analytic CuspForm, with Fourier coefficients tied to its width-one q-expansion. The nebentypus transformation law and every prime Hecke eigenvalue equation are written explicitly. The prime Hecke operator includes both its translated sum and its second term; when the prime divides the level, the second term vanishes. The complex twist is the finite-translate expression for $f_{\chi^{-1}}$, and its critical L-value is defined by the actual Mellin integral. Neither an arbitrary L-value table nor the desired measure is an input assumption.

The embeddings share the abstract algebraic closure of $\mathbb Q$; there is no asserted continuous map from $\mathbb C$ to $\mathbb C_p$. The algebraic bridge in each interpolation identity is existential and constrained by a complex equality. Test functions are existential continuous maps constrained pointwise to equal the specified character or disk function; this makes their continuity part of the conclusion instead of an unproved definition. All primes, including $2$, are allowed. Natural-number subtractions occur only in theorem contexts with $k\ge2$ and $j\le k-2$.

The signed projections use a factor of $1/2$. Their normalized measures are added, and the period sign is $\chi(-1)(-1)^j$. These conventions fix the powers, sign, Gauss sum, and periods in the displayed interpolation formula. Periods are not asserted to be canonical integral periods; rescaling by algebraic constants changes the normalization. Exceptional-zero derivative formulas, positive-slope distributions, tame-conductor twists, and Iwasawa main conjectures are outside this mission.

Selected references

• B. Mazur, J. Tate and J. Teitelbaum, On p-adic analogues of the conjectures of Birch and Swinnerton-Dyer, Inventiones Mathematicae 84 (1986), 1–48, Chapter I, §§1–4 and 7–14. DOI; digitized original.
• G. Shimura, On the periods of modular forms, Mathematische Annalen 229 (1977), 211–221. DOI.
• C. Williams, An introduction to p-adic L-functions II: Modular forms, lecture notes, §§11.6–11.8, particularly Proposition 11.21, for period normalization of general eigenforms. Author's notes.