A WeakFEPair structure associated to a modular form.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The L-series of a modular form (including its Archimedean Γ-factor).
Equations
- ModularForm.Λ hk f = (ModularForm.weakFEPair hk f).Λ
Instances For
The L-function of a modular form f of weight k: the completed L-function ModularForm.Λ
without its Archimedean factor Gammaℂ s / 2 = (2 * π) ^ (-s) * Gamma s, i.e.
L hk f s = Λ hk f s * (2 / Gammaℂ s) for s ≠ 0 (ModularForm.L_apply_of_ne_zero).
Normalization: for k + 1 < re s, L hk f s = ∑ aₙ (n / h) ^ (-s), where h = Γ.strictWidthInfty
is the strict width of the cusp ∞ and aₙ are the coefficients of qExpansion h f, the expansion
of f in q = exp (2πiτ / h). This is ModularForm.hasSum_L, stated as
∑ aₙ / n ^ s = h ^ (-s) * L hk f s (for cusp forms, CuspForm.hasSum_L only needs
k / 2 + 1 < re s); for h ≠ 1 it is thus h ^ s times the classical ∑ aₙ / n ^ s.
At s = 0, Λ hk f has at most a simple pole, with residue -valueAtInfty f, which cancels the
zero of 1 / Gammaℂ. As for riemannZeta, we define L hk f 0 to be the limit -valueAtInfty f
(ModularForm.L_apply_zero, ModularForm.tendsto_L_nhdsNE_zero). Use these lemmas rather than
unfolding L.
Equations
- ModularForm.L hk f = Function.update (fun (s : ℂ) => ModularForm.Λ hk f s * (2 / s.Gammaℂ)) 0 (-UpperHalfPlane.valueAtInfty ⇑f)
Instances For
For s ≠ 0, L hk f s is the completed L-function Λ hk f s divided by its Archimedean
factor Gammaℂ s / 2. At s = 0 use ModularForm.L_apply_zero instead: there the right-hand side
is 0 (as Gammaℂ 0 = 0), whereas L hk f 0 = -valueAtInfty f.
The value of L hk f at s = 0: L(f, 0) = -a₀, where a₀ = valueAtInfty f is the constant
term of the q-expansion of f (UpperHalfPlane.qExpansion_coeff_zero); in particular it is 0
for cusp forms. It is the limit of L hk f s as s → 0 (ModularForm.tendsto_L_nhdsNE_zero),
so L hk f is continuous at 0 (ModularForm.continuousAt_L_zero).
The limit lim_{s → 0} L hk f s = -valueAtInfty f, which is the value L hk f 0
(ModularForm.L_apply_zero).
L hk f is continuous at s = 0: its value L hk f 0 = -valueAtInfty f is not a junk value
but fills in the removable singularity of Λ hk f s * (2 / Gammaℂ s) at s = 0.
For cusp forms the FE-pair is a strong FE-pair.