The L-function of a modular form

noncomputable def ModularForm.weakFEPair {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {k : ℤ} (hk : 0 < k) {F : Type u_1} [FunLike F UpperHalfPlane ℂ] (f : F) [ModularFormClass F Γ k] : WeakFEPair ℂ

A WeakFEPair structure associated to a modular form.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ModularForm.weakFEPair_f {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {k : ℤ} (hk : 0 < k) {F : Type u_1} [FunLike F UpperHalfPlane ℂ] (f : F) [ModularFormClass F Γ k] (t : ℝ) : (weakFEPair hk f).f t = f (↑UpperHalfPlane.ofComplex (Complex.I * ↑t))

@[simp]

theorem ModularForm.weakFEPair_ε {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {k : ℤ} (hk : 0 < k) {F : Type u_1} [FunLike F UpperHalfPlane ℂ] (f : F) [ModularFormClass F Γ k] : (weakFEPair hk f).ε = Complex.I ^ k

@[simp]

theorem ModularForm.weakFEPair_g {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {k : ℤ} (hk : 0 < k) {F : Type u_1} [FunLike F UpperHalfPlane ℂ] (f : F) [ModularFormClass F Γ k] (t : ℝ) : (weakFEPair hk f).g t = (translate f (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S))) (↑UpperHalfPlane.ofComplex (Complex.I * ↑t))

@[simp]

theorem ModularForm.weakFEPair_f₀ {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {k : ℤ} (hk : 0 < k) {F : Type u_1} [FunLike F UpperHalfPlane ℂ] (f : F) [ModularFormClass F Γ k] : (weakFEPair hk f).f₀ = UpperHalfPlane.valueAtInfty ⇑f

@[simp]

theorem ModularForm.weakFEPair_k {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {k : ℤ} (hk : 0 < k) {F : Type u_1} [FunLike F UpperHalfPlane ℂ] (f : F) [ModularFormClass F Γ k] : (weakFEPair hk f).k = ↑k

@[simp]

theorem ModularForm.weakFEPair_g₀ {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {k : ℤ} (hk : 0 < k) {F : Type u_1} [FunLike F UpperHalfPlane ℂ] (f : F) [ModularFormClass F Γ k] : (weakFEPair hk f).g₀ = UpperHalfPlane.valueAtInfty ⇑(translate f (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S)))

noncomputable def ModularForm.Λ {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {k : ℤ} (hk : 0 < k) {F : Type u_1} [FunLike F UpperHalfPlane ℂ] (f : F) [ModularFormClass F Γ k] : ℂ → ℂ

The L-series of a modular form (including its Archimedean Γ-factor).

Equations

• ModularForm.Λ hk f = (ModularForm.weakFEPair hk f).Λ

theorem ModularForm.hasSum_Λ {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {k : ℤ} (hk : 0 < k) {F : Type u_1} [FunLike F UpperHalfPlane ℂ] (f : F) {s : ℂ} [ModularFormClass F Γ k] (hs : ↑k + 1 < s.re) : HasSum (fun (n : ℕ) => ↑Real.pi ^ (-s) * Complex.Gamma s * (PowerSeries.coeff n) (UpperHalfPlane.qExpansion Γ.strictWidthInfty ⇑f) / ↑(2 * ↑n / Γ.strictWidthInfty) ^ s) (Λ hk f s)

noncomputable def ModularForm.L {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {k : ℤ} (hk : 0 < k) {F : Type u_1} [FunLike F UpperHalfPlane ℂ] (f : F) [ModularFormClass F Γ k] (s : ℂ) : ℂ

The L-series of a modular form (without its Archimedean Γ-factor).

Equations

• ModularForm.L hk f s = ModularForm.Λ hk f s * (2 / s.Gammaℂ)

theorem ModularForm.hasSum_L {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {k : ℤ} (hk : 0 < k) {F : Type u_1} [FunLike F UpperHalfPlane ℂ] (f : F) {s : ℂ} [ModularFormClass F Γ k] (hs : ↑k + 1 < s.re) : HasSum (fun (n : ℕ) => (PowerSeries.coeff n) (UpperHalfPlane.qExpansion Γ.strictWidthInfty ⇑f) / ↑n ^ s) (↑Γ.strictWidthInfty ^ (-s) * L hk f s)

theorem CuspForm.isStrongFEPair {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {k : ℤ} (hk : 0 < k) {F : Type u_1} [FunLike F UpperHalfPlane ℂ] (f : F) [CuspFormClass F Γ k] : IsStrongFEPair (ModularForm.weakFEPair hk f)

For cusp forms the FE-pair is a strong FE-pair.

theorem CuspForm.differentiable_Λ {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {k : ℤ} (hk : 0 < k) {F : Type u_1} [FunLike F UpperHalfPlane ℂ] (f : F) [CuspFormClass F Γ k] : Differentiable ℂ (ModularForm.Λ hk f)

theorem CuspForm.Λ_eq_mellin {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {k : ℤ} (hk : 0 < k) {F : Type u_1} [FunLike F UpperHalfPlane ℂ] (f : F) [CuspFormClass F Γ k] : ModularForm.Λ hk f = mellin fun (t : ℝ) => f (↑UpperHalfPlane.ofComplex (Complex.I * ↑t))

theorem CuspForm.hasSum_Λ {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] (f : F) {s : ℂ} [CuspFormClass F Γ k] (hk : 0 < k) (hs : ↑k / 2 + 1 < s.re) : HasSum (fun (n : ℕ) => ↑Real.pi ^ (-s) * Complex.Gamma s * (PowerSeries.coeff n) (UpperHalfPlane.qExpansion Γ.strictWidthInfty ⇑f) / ↑(2 * ↑n / Γ.strictWidthInfty) ^ s) (ModularForm.Λ hk f s)

theorem CuspForm.differentiable_L {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {k : ℤ} (hk : 0 < k) {F : Type u_1} [FunLike F UpperHalfPlane ℂ] (f : F) [CuspFormClass F Γ k] : Differentiable ℂ (ModularForm.L hk f)

theorem CuspForm.hasSum_L {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {k : ℤ} (hk : 0 < k) {F : Type u_1} [FunLike F UpperHalfPlane ℂ] (f : F) {s : ℂ} [CuspFormClass F Γ k] (hs : ↑k / 2 + 1 < s.re) : HasSum (fun (n : ℕ) => (PowerSeries.coeff n) (UpperHalfPlane.qExpansion Γ.strictWidthInfty ⇑f) / ↑n ^ s) (↑Γ.strictWidthInfty ^ (-s) * ModularForm.L hk f s)