Documentation

Mathlib.NumberTheory.ModularForms.QExpansion

q-expansions of functions on the upper half plane #

We show that a function on the upper half plane with strict period n can be written as τ ↦ F (𝕢 n τ) where F is analytic on the open unit disc, and 𝕢 n is the parameter τ ↦ exp (2 * I * π * τ / n). As an application, we show that cusp forms decay exponentially to 0 as im τ → ∞.

We also define the q-expansion of a function f on the upper half plane, either as a power series or as a FormalMultilinearSeries, and show that it converges to f if f is periodic, holomorphic and bounded at infinity.

Main definitions and results #

UpperHalfPlane.cuspFunction: for a function on the upper half plane with strict period n, this is the function F such that f τ = F (exp (2 * π * I * τ / n)), extended by a choice of limit at 0.
UpperHalfPlane.differentiableAt_cuspFunction: when f is periodic, holomorphic and bounded at infinity, its cuspFunction is differentiable on the open unit disc (including at 0).
UpperHalfPlane.qExpansion: the q-expansion of a function on the upper half plane (defined as the Taylor series of its cuspFunction), bundled as a PowerSeries.
UpperHalfPlane.hasSum_qExpansion: the q-expansion evaluated at 𝕢 n τ sums to f τ, for τ in the upper half plane.
ModularForm.qExpansionRingHom defines the ring homomorphism from the graded ring of modular forms to power series given by taking q-expansions.
UpperHalfPlane.qExpansion_coeff_unique shows that q-expansion coefficients are uniquely determined.
There are also more specialized versions of some of these lemmas in the ModularFormClass namespace.

noncomputable def UpperHalfPlane.valueAtInfty (f : UpperHalfPlane → ℂ) :

The value of f at the cusp ∞ (or an arbitrary choice of value if this limit is not well-defined).

Equations

UpperHalfPlane.valueAtInfty f = UpperHalfPlane.atImInfty.limUnder f

Instances For

theorem UpperHalfPlane.IsZeroAtImInfty.valueAtInfty_eq_zero {f : UpperHalfPlane → ℂ} (hf : IsZeroAtImInfty f) :

valueAtInfty f = 0

theorem UpperHalfPlane.qParam_tendsto_atImInfty {h : ℝ} (hh : 0 < h) :

Filter.Tendsto (fun (τ : UpperHalfPlane) => Function.Periodic.qParam h ↑τ) atImInfty (nhds 0)

noncomputable def UpperHalfPlane.cuspFunction (h : ℝ) (f : UpperHalfPlane → ℂ) :

The analytic function F such that f τ = F (exp (2 * π * I * τ / h)), extended by a choice of limit at 0.

Equations

UpperHalfPlane.cuspFunction h f = Function.Periodic.cuspFunction h (f ∘ ↑UpperHalfPlane.ofComplex)

Instances For

theorem UpperHalfPlane.eq_cuspFunction {h : ℝ} {f : UpperHalfPlane → ℂ} (τ : UpperHalfPlane) (hh : h ≠ 0) (hfper : Function.Periodic (f ∘ ↑ofComplex) ↑h) :

cuspFunction h f (Function.Periodic.qParam h ↑τ) = f τ

theorem UpperHalfPlane.differentiableAt_cuspFunction {h : ℝ} {f : UpperHalfPlane → ℂ} (hh : 0 < h) (hfper : Function.Periodic (f ∘ ↑ofComplex) ↑h) (hfhol : MDiff f) (hfbdd : IsBoundedAtImInfty f) {q : ℂ} (hq : ‖q‖ < 1) :

DifferentiableAt ℂ (cuspFunction h f) q

theorem UpperHalfPlane.differentiableOn_cuspFunction_ball {h : ℝ} {f : UpperHalfPlane → ℂ} (hh : 0 < h) (hfper : Function.Periodic (f ∘ ↑ofComplex) ↑h) (hfhol : MDiff f) (hfbdd : IsBoundedAtImInfty f) :

DifferentiableOn ℂ (cuspFunction h f) (Metric.ball 0 1)

theorem UpperHalfPlane.analyticAt_cuspFunction_zero {h : ℝ} {f : UpperHalfPlane → ℂ} (hh : 0 < h) (hfper : Function.Periodic (f ∘ ↑ofComplex) ↑h) (hfhol : MDiff f) (hfbdd : IsBoundedAtImInfty f) :

AnalyticAt ℂ (cuspFunction h f) 0

theorem UpperHalfPlane.cuspFunction_apply_zero {h : ℝ} {f : UpperHalfPlane → ℂ} (hh : 0 < h) (hfanalytic : AnalyticAt ℂ (cuspFunction h f) 0) (hfper : Function.Periodic (f ∘ ↑ofComplex) ↑h) :

cuspFunction h f 0 = valueAtInfty f

theorem SlashInvariantFormClass.periodic_comp_ofComplex {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (f : F) [SlashInvariantFormClass F Γ k] (hΓ : h ∈ Γ.strictPeriods) :

Function.Periodic (⇑f ∘ ↑UpperHalfPlane.ofComplex) ↑h

theorem SlashInvariantFormClass.eq_cuspFunction {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (f : F) [SlashInvariantFormClass F Γ k] (τ : UpperHalfPlane) (hΓ : h ∈ Γ.strictPeriods) (hh : h ≠ 0) :

UpperHalfPlane.cuspFunction h (⇑f) (Function.Periodic.qParam h ↑τ) = f τ

@[deprecated ModularFormClass.bdd_at_infty (since := "2026-04-19")]

theorem ModularFormClass.bounded_at_infty_comp_ofComplex {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} (f : F) [ModularFormClass F Γ k] (hi : IsCusp OnePoint.infty Γ) :

(Filter.comap Complex.im Filter.atTop).BoundedAtFilter (⇑f ∘ ↑UpperHalfPlane.ofComplex)

theorem ModularFormClass.differentiableAt_cuspFunction {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (f : F) [ModularFormClass F Γ k] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) {q : ℂ} (hq : ‖q‖ < 1) :

DifferentiableAt ℂ (UpperHalfPlane.cuspFunction h ⇑f) q

theorem ModularFormClass.analyticAt_cuspFunction_zero {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (f : F) [ModularFormClass F Γ k] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) :

AnalyticAt ℂ (UpperHalfPlane.cuspFunction h ⇑f) 0

noncomputable def UpperHalfPlane.qExpansion (h : ℝ) (f : UpperHalfPlane → ℂ) :

PowerSeries ℂ

The q-expansion of a function on the upper half plane with strict period h, bundled as a PowerSeries. The m-th coefficient is the Taylor coefficient of the cuspFunction at q = 0, where q = exp(2πiτ/h) is the local parameter at the cusp.

Equations

UpperHalfPlane.qExpansion h f = PowerSeries.mk fun (m : ℕ) => (↑m.factorial)⁻¹ * iteratedDeriv m (UpperHalfPlane.cuspFunction h f) 0

Instances For

theorem UpperHalfPlane.qExpansion_coeff {h : ℝ} (f : UpperHalfPlane → ℂ) (m : ℕ) :

(PowerSeries.coeff m) (qExpansion h f) = (↑m.factorial)⁻¹ * iteratedDeriv m (cuspFunction h f) 0

theorem UpperHalfPlane.qExpansion_coeff_zero {h : ℝ} {f : UpperHalfPlane → ℂ} (hh : 0 < h) (hfanalytic : AnalyticAt ℂ (cuspFunction h f) 0) (hfper : Function.Periodic (f ∘ ↑ofComplex) ↑h) :

(PowerSeries.coeff 0) (qExpansion h f) = valueAtInfty f

theorem UpperHalfPlane.hasSum_qExpansion_of_norm_lt {h : ℝ} {f : UpperHalfPlane → ℂ} (hh : 0 < h) (hfper : Function.Periodic (f ∘ ↑ofComplex) ↑h) (hfhol : MDiff f) (hfbdd : IsBoundedAtImInfty f) {q : ℂ} (hq : ‖q‖ < 1) :

HasSum (fun (m : ℕ) => (PowerSeries.coeff m) (qExpansion h f) • q ^ m) (cuspFunction h f q)

theorem UpperHalfPlane.hasSum_qExpansion {h : ℝ} {f : UpperHalfPlane → ℂ} (hh : 0 < h) (hfper : Function.Periodic (f ∘ ↑ofComplex) ↑h) (hfhol : MDiff f) (hfbdd : IsBoundedAtImInfty f) (τ : UpperHalfPlane) :

HasSum (fun (m : ℕ) => (PowerSeries.coeff m) (qExpansion h f) • Function.Periodic.qParam h ↑τ ^ m) (f τ)

noncomputable def UpperHalfPlane.qExpansionFormalMultilinearSeries {F : Type u_1} [FunLike F UpperHalfPlane ℂ] (h : ℝ) (f : F) :

FormalMultilinearSeries ℂ ℂ ℂ

The q-expansion of a function on the upper half plane, bundled as a FormalMultilinearSeries.

TODO: Maybe get rid of this and instead define a general API for converting PowerSeries to FormalMultilinearSeries.

Equations

UpperHalfPlane.qExpansionFormalMultilinearSeries h f = FormalMultilinearSeries.ofScalars ℂ fun (m : ℕ) => (PowerSeries.coeff m) (UpperHalfPlane.qExpansion h ⇑f)

Instances For

@[simp]

theorem UpperHalfPlane.qExpansionFormalMultilinearSeries_coeff {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {h : ℝ} (f : F) (m : ℕ) :

(qExpansionFormalMultilinearSeries h f).coeff m = (PowerSeries.coeff m) (qExpansion h ⇑f)

theorem UpperHalfPlane.qExpansionFormalMultilinearSeries_apply_norm {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {h : ℝ} (f : F) (m : ℕ) :

‖qExpansionFormalMultilinearSeries h f m‖ = ‖(PowerSeries.coeff m) (qExpansion h ⇑f)‖

theorem UpperHalfPlane.qExpansionFormalMultilinearSeries_radius {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {h : ℝ} (f : F) (hh : 0 < h) (hfper : Function.Periodic (⇑f ∘ ↑ofComplex) ↑h) (hfhol : MDiff ⇑f) (hfbdd : IsBoundedAtImInfty ⇑f) :

1 ≤ (qExpansionFormalMultilinearSeries h f).radius

theorem UpperHalfPlane.hasFPowerSeriesOnBall_cuspFunction {h : ℝ} {f : UpperHalfPlane → ℂ} {c : ℕ → ℂ} (hh : 0 < h) (hfanalytic : AnalyticAt ℂ (cuspFunction h f) 0) (hf : ∀ (τ : UpperHalfPlane), HasSum (fun (m : ℕ) => c m • Function.Periodic.qParam h ↑τ ^ m) (f τ)) :

HasFPowerSeriesOnBall (cuspFunction h f) (FormalMultilinearSeries.ofScalars ℂ c) 0 1

theorem UpperHalfPlane.qExpansion_coeff_eq_circleIntegral {h : ℝ} {f : UpperHalfPlane → ℂ} (hh : 0 < h) (hfper : Function.Periodic (f ∘ ↑ofComplex) ↑h) (hfhol : MDiff f) (hfbdd : IsBoundedAtImInfty f) (n : ℕ) {R : ℝ} (hR : 0 < R) (hR' : R < 1) :

(PowerSeries.coeff n) (qExpansion h f) = (2 * ↑Real.pi * Complex.I)⁻¹ * ∮ (z : ℂ) in C(0, R), cuspFunction h f z / z ^ (n + 1)

The q-expansion coefficient can be expressed as a circleIntegral for any radius 0 < R < 1.

theorem UpperHalfPlane.qExpansion_coeff_eq_intervalIntegral {h : ℝ} {f : UpperHalfPlane → ℂ} (hh : 0 < h) (hfper : Function.Periodic (f ∘ ↑ofComplex) ↑h) (hfhol : MDiff f) (hfbdd : IsBoundedAtImInfty f) (n : ℕ) {t : ℝ} (ht : 0 < t) :

(PowerSeries.coeff n) (qExpansion h f) = 1 / ↑h * ∫ (u : ℝ) in 0..h, 1 / Function.Periodic.qParam h (↑u + ↑t * ↑I) ^ n * f { coe := ↑u + ↑t * ↑I, coe_im_pos := ⋯ }

If h is a positive strict period of f, then the q-expansion coefficient can be expressed as an integral along a horizontal line in the upper half-plane from t * I to h + t * I, for any 0 < t.

theorem UpperHalfPlane.exp_decay_sub_atImInfty {h : ℝ} {f : UpperHalfPlane → ℂ} (hh : 0 < h) (hfper : Function.Periodic (f ∘ ↑ofComplex) ↑h) (hfhol : MDiff f) (hfbdd : IsBoundedAtImInfty f) :

(fun (τ : UpperHalfPlane) => f τ - valueAtInfty f) =O[atImInfty ] fun (τ : UpperHalfPlane) => Real.exp (-2 * Real.pi * τ.im / h)

theorem UpperHalfPlane.IsZeroAtImInfty.zero_at_infty_comp_ofComplex {f : UpperHalfPlane → ℂ} (hf : IsZeroAtImInfty f) :

(Filter.comap Complex.im Filter.atTop).ZeroAtFilter (f ∘ ↑ofComplex)

theorem UpperHalfPlane.IsZeroAtImInfty.cuspFunction_apply_zero {h : ℝ} {f : UpperHalfPlane → ℂ} (hf : IsZeroAtImInfty f) (hh : 0 < h) :

cuspFunction h f 0 = 0

theorem UpperHalfPlane.IsZeroAtImInfty.exp_decay_atImInfty {h : ℝ} {f : UpperHalfPlane → ℂ} (hf : IsZeroAtImInfty f) (hh : 0 < h) (hfper : Function.Periodic (f ∘ ↑ofComplex) ↑h) (hfhol : MDiff f) (hfbdd : IsBoundedAtImInfty f) :

f =O[atImInfty ] fun (τ : UpperHalfPlane) => Real.exp (-2 * Real.pi * τ.im / h)

theorem ModularFormClass.qExpansion_coeff_eq_intervalIntegral {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (f : F) [ModularFormClass F Γ k] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) (n : ℕ) {t : ℝ} (ht : 0 < t) :

(PowerSeries.coeff n) (UpperHalfPlane.qExpansion h ⇑f) = 1 / ↑h * ∫ (u : ℝ) in 0..h, 1 / Function.Periodic.qParam h (↑u + ↑t * Complex.I) ^ n * f { coe := ↑u + ↑t * Complex.I, coe_im_pos := ⋯ }

theorem ModularFormClass.exp_decay_sub_atImInfty' {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} (f : F) [ModularFormClass F Γ k] [Γ.HasDetPlusMinusOne] [DiscreteTopology ↥Γ] [Fact (IsCusp OnePoint.infty Γ)] :

∃ c > 0, (fun (τ : UpperHalfPlane) => f τ - UpperHalfPlane.valueAtInfty ⇑f) =O[UpperHalfPlane.atImInfty ] fun (τ : UpperHalfPlane) => Real.exp (-c * τ.im)

Version of exp_decay_sub_atImInfty stating a less precise result but easier to apply in practice (not specifying the growth rate precisely).

Note that the Fact hypothesis is automatically synthesized for arithmetic subgroups. The discreteness hypothesis may be unnecessary, but it is satisfied in the cases of interest.

theorem ModularFormClass.exp_decay_atImInfty' {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} (f : F) [ModularFormClass F Γ k] [Γ.HasDetPlusMinusOne] [DiscreteTopology ↥Γ] [Fact (IsCusp OnePoint.infty Γ)] (hf : UpperHalfPlane.IsZeroAtImInfty ⇑f) :

∃ c > 0, ⇑f =O[UpperHalfPlane.atImInfty ] fun (τ : UpperHalfPlane) => Real.exp (-c * τ.im)

Version of exp_decay_atImInfty stating a less precise result but easier to apply in practice (not specifying the growth rate precisely). Note that the Fact hypothesis is automatically synthesized for arithmetic subgroups.

theorem CuspFormClass.zero_at_infty_comp_ofComplex {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} (f : F) [CuspFormClass F Γ k] [Fact (IsCusp OnePoint.infty Γ)] :

(Filter.comap Complex.im Filter.atTop).ZeroAtFilter (⇑f ∘ ↑UpperHalfPlane.ofComplex)

theorem CuspFormClass.cuspFunction_apply_zero {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (f : F) [CuspFormClass F Γ k] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) :

UpperHalfPlane.cuspFunction h (⇑f) 0 = 0

theorem CuspFormClass.exp_decay_atImInfty {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (f : F) [CuspFormClass F Γ k] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) :

⇑f =O[UpperHalfPlane.atImInfty ] fun (τ : UpperHalfPlane) => Real.exp (-2 * Real.pi * τ.im / h)

theorem CuspFormClass.exp_decay_atImInfty' {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} (f : F) [CuspFormClass F Γ k] [Γ.HasDetPlusMinusOne] [DiscreteTopology ↥Γ] [Fact (IsCusp OnePoint.infty Γ)] :

∃ c > 0, ⇑f =O[UpperHalfPlane.atImInfty ] fun (τ : UpperHalfPlane) => Real.exp (-c * τ.im)

theorem UpperHalfPlane.cuspFunction_mul_zero {h : ℝ} {f g : ℂ → ℂ} (hfcts : ContinuousAt (Function.Periodic.cuspFunction h f) 0) (hgcts : ContinuousAt (Function.Periodic.cuspFunction h g) 0) :

Function.Periodic.cuspFunction h (f * g) 0 = Function.Periodic.cuspFunction h f 0 * Function.Periodic.cuspFunction h g 0

theorem UpperHalfPlane.qExpansion_mul_coeff_zero {h : ℝ} {f g : UpperHalfPlane → ℂ} (hfcts : ContinuousAt (cuspFunction h f) 0) (hgcts : ContinuousAt (cuspFunction h g) 0) :

(PowerSeries.coeff 0) (qExpansion h (f * g)) = (PowerSeries.coeff 0) (qExpansion h f) * (PowerSeries.coeff 0) (qExpansion h g)

theorem UpperHalfPlane.cuspFunction_mul {h : ℝ} {f g : UpperHalfPlane → ℂ} (hfcts : ContinuousAt (cuspFunction h f) 0) (hgcts : ContinuousAt (cuspFunction h g) 0) :

cuspFunction h (f * g) = cuspFunction h f * cuspFunction h g

theorem UpperHalfPlane.cuspFunction_smul {h : ℝ} {f : UpperHalfPlane → ℂ} (hfcts : ContinuousAt (cuspFunction h f) 0) (a : ℂ) :

cuspFunction h (a • f) = a • cuspFunction h f

theorem UpperHalfPlane.cuspFunction_neg {h : ℝ} {f : UpperHalfPlane → ℂ} (hfcts : ContinuousAt (cuspFunction h f) 0) :

cuspFunction h (-f) = -cuspFunction h f

theorem UpperHalfPlane.cuspFunction_add {h : ℝ} {f g : UpperHalfPlane → ℂ} (hfcts : ContinuousAt (cuspFunction h f) 0) (hgcts : ContinuousAt (cuspFunction h g) 0) :

cuspFunction h (f + g) = cuspFunction h f + cuspFunction h g

theorem UpperHalfPlane.cuspFunction_sub {h : ℝ} {f g : UpperHalfPlane → ℂ} (hfcts : ContinuousAt (cuspFunction h f) 0) (hgcts : ContinuousAt (cuspFunction h g) 0) :

cuspFunction h (f - g) = cuspFunction h f - cuspFunction h g

theorem UpperHalfPlane.qExpansion_mul {h : ℝ} {f g : UpperHalfPlane → ℂ} (hf : AnalyticAt ℂ (cuspFunction h f) 0) (hg : AnalyticAt ℂ (cuspFunction h g) 0) :

qExpansion h (f * g) = qExpansion h f * qExpansion h g

theorem UpperHalfPlane.qExpansion_smul {h : ℝ} {f : UpperHalfPlane → ℂ} (hf : AnalyticAt ℂ (cuspFunction h f) 0) (a : ℂ) :

qExpansion h (a • f) = a • qExpansion h f

theorem UpperHalfPlane.qExpansion_neg {h : ℝ} {f : UpperHalfPlane → ℂ} (hf : AnalyticAt ℂ (cuspFunction h f) 0) :

qExpansion h (-f) = -qExpansion h f

theorem UpperHalfPlane.qExpansion_add {h : ℝ} {f g : UpperHalfPlane → ℂ} (hf : AnalyticAt ℂ (cuspFunction h f) 0) (hg : AnalyticAt ℂ (cuspFunction h g) 0) :

qExpansion h (f + g) = qExpansion h f + qExpansion h g

theorem UpperHalfPlane.qExpansion_sub {h : ℝ} {f g : UpperHalfPlane → ℂ} (hf : AnalyticAt ℂ (cuspFunction h f) 0) (hg : AnalyticAt ℂ (cuspFunction h g) 0) :

qExpansion h (f - g) = qExpansion h f - qExpansion h g

theorem UpperHalfPlane.qExpansion_zero (h : ℝ) :

qExpansion h 0 = 0

theorem UpperHalfPlane.qExpansion_eq_zero_iff {h : ℝ} {f : UpperHalfPlane → ℂ} (hh : 0 < h) (hfper : Function.Periodic (f ∘ ↑ofComplex) ↑h) (hfhol : MDiff f) (hfbdd : IsBoundedAtImInfty f) :

qExpansion h f = 0 ↔ f = 0

theorem UpperHalfPlane.qExpansion_one (h : ℝ) :

qExpansion h 1 = 1

theorem ModularForm.cuspFunction_smul {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) (a : ℂ) (f : F) [ModularFormClass F Γ k] :

UpperHalfPlane.cuspFunction h (a • ⇑f) = a • UpperHalfPlane.cuspFunction h ⇑f

theorem ModularForm.cuspFunction_neg {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) (f : F) [ModularFormClass F Γ k] :

UpperHalfPlane.cuspFunction h (-⇑f) = -UpperHalfPlane.cuspFunction h ⇑f

theorem ModularForm.cuspFunction_add {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} {G : Type u_2} [FunLike G UpperHalfPlane ℂ] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) {a b : ℤ} (f : F) [ModularFormClass F Γ a] (g : G) [ModularFormClass G Γ b] :

UpperHalfPlane.cuspFunction h (⇑f + ⇑g) = UpperHalfPlane.cuspFunction h ⇑f + UpperHalfPlane.cuspFunction h ⇑g

theorem ModularForm.cuspFunction_sub {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} {G : Type u_2} [FunLike G UpperHalfPlane ℂ] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) {a b : ℤ} (f : F) [ModularFormClass F Γ a] (g : G) [ModularFormClass G Γ b] :

UpperHalfPlane.cuspFunction h (⇑f - ⇑g) = UpperHalfPlane.cuspFunction h ⇑f - UpperHalfPlane.cuspFunction h ⇑g

theorem ModularForm.cuspFunction_mul {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} [Γ.HasDetPlusMinusOne] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) {a b : ℤ} (f : ModularForm Γ a) (g : ModularForm Γ b) :

UpperHalfPlane.cuspFunction h ⇑(f.mul g) = UpperHalfPlane.cuspFunction h ⇑f * UpperHalfPlane.cuspFunction h ⇑g

theorem ModularForm.qExpansion_smul {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) (a : ℂ) (f : F) [ModularFormClass F Γ k] :

UpperHalfPlane.qExpansion h (a • ⇑f) = a • UpperHalfPlane.qExpansion h ⇑f

theorem ModularForm.qExpansion_neg {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) (f : F) [ModularFormClass F Γ k] :

UpperHalfPlane.qExpansion h (-⇑f) = -UpperHalfPlane.qExpansion h ⇑f

theorem ModularForm.qExpansion_add {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} {G : Type u_2} [FunLike G UpperHalfPlane ℂ] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) {a b : ℤ} (f : F) [ModularFormClass F Γ a] (g : G) [ModularFormClass G Γ b] :

UpperHalfPlane.qExpansion h (⇑f + ⇑g) = UpperHalfPlane.qExpansion h ⇑f + UpperHalfPlane.qExpansion h ⇑g

theorem ModularForm.qExpansion_sub {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} {G : Type u_2} [FunLike G UpperHalfPlane ℂ] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) {a b : ℤ} (f : F) [ModularFormClass F Γ a] (g : G) [ModularFormClass G Γ b] :

UpperHalfPlane.qExpansion h (⇑f - ⇑g) = UpperHalfPlane.qExpansion h ⇑f - UpperHalfPlane.qExpansion h ⇑g

theorem ModularForm.qExpansion_mul {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} [Γ.HasDetPlusMinusOne] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) {a b : ℤ} (f : ModularForm Γ a) (g : ModularForm Γ b) :

UpperHalfPlane.qExpansion h ⇑(f.mul g) = UpperHalfPlane.qExpansion h ⇑f * UpperHalfPlane.qExpansion h ⇑g

theorem ModularForm.qExpansion_eq_zero_iff {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) {k : ℤ} (f : ModularForm Γ k) :

UpperHalfPlane.qExpansion h ⇑f = 0 ↔ f = 0

theorem ModularForm.qExpansion_one {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} [Γ.HasDetPlusMinusOne] :

UpperHalfPlane.qExpansion h ⇑1 = 1

theorem ModularForm.qExpansion_pow {k : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} [Γ.HasDetPlusMinusOne] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) (f : ModularForm Γ k) (n : ℕ) :

UpperHalfPlane.qExpansion h ⇑(f.pow n) = UpperHalfPlane.qExpansion h ⇑f ^ n

noncomputable def ModularForm.qExpansionAddHom {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) (k : ℤ) :

ModularForm Γ k →+ PowerSeries ℂ

The qExpansion map as an additive group hom. to power series over ℂ.

Equations

ModularForm.qExpansionAddHom hh hΓ k = { toFun := fun (f : ModularForm Γ k) => UpperHalfPlane.qExpansion h ⇑f, map_zero' := ⋯, map_add' := ⋯ }

Instances For

noncomputable def ModularForm.qExpansionRingHom {Γ : Subgroup (GL (Fin 2) ℝ)} (h : ℝ) [Γ.HasDetPlusMinusOne] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) :

(DirectSum ℤ fun (k : ℤ) => ModularForm Γ k) →+* PowerSeries ℂ

The qExpansion map as a map from the graded ring of modular forms to power series over ℂ.

Equations

ModularForm.qExpansionRingHom h hh hΓ = DirectSum.toSemiring (ModularForm.qExpansionAddHom hh hΓ) ⋯ ⋯

Instances For

@[simp]

theorem ModularForm.qExpansionRingHom_apply {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} [Γ.HasDetPlusMinusOne] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) (k : ℤ) (f : ModularForm Γ k) :

(qExpansionRingHom h hh hΓ) ((DirectSum.of (ModularForm Γ) k) f) = UpperHalfPlane.qExpansion h ⇑f

theorem ModularForm.qExpansion_of_mul {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} [Γ.HasDetPlusMinusOne] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) (a b : ℤ) (f : ModularForm Γ a) (g : ModularForm Γ b) :

UpperHalfPlane.qExpansion h ⇑(((DirectSum.of (ModularForm Γ) a) f * (DirectSum.of (ModularForm Γ) b) g) (a + b)) = UpperHalfPlane.qExpansion h ⇑f * UpperHalfPlane.qExpansion h ⇑g

theorem ModularForm.qExpansion_of_pow {k : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} [Γ.HasDetPlusMinusOne] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) (f : ModularForm Γ k) (n : ℕ) :

UpperHalfPlane.qExpansion h ⇑(((DirectSum.of (ModularForm Γ) k) f ^ n) (↑n * k)) = UpperHalfPlane.qExpansion h ⇑f ^ n

@[deprecated ModularForm.cuspFunction_smul (since := "2026-05-05")]

theorem ModularFormClass.cuspFunction_smul {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) (a : ℂ) (f : F) [ModularFormClass F Γ k] :

UpperHalfPlane.cuspFunction h (a • ⇑f) = a • UpperHalfPlane.cuspFunction h ⇑f

Alias of ModularForm.cuspFunction_smul.

@[deprecated ModularForm.cuspFunction_neg (since := "2026-05-05")]

theorem ModularFormClass.cuspFunction_neg {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) (f : F) [ModularFormClass F Γ k] :

UpperHalfPlane.cuspFunction h (-⇑f) = -UpperHalfPlane.cuspFunction h ⇑f

Alias of ModularForm.cuspFunction_neg.

@[deprecated ModularForm.cuspFunction_add (since := "2026-05-05")]

theorem ModularFormClass.cuspFunction_add {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} {G : Type u_2} [FunLike G UpperHalfPlane ℂ] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) {a b : ℤ} (f : F) [ModularFormClass F Γ a] (g : G) [ModularFormClass G Γ b] :

UpperHalfPlane.cuspFunction h (⇑f + ⇑g) = UpperHalfPlane.cuspFunction h ⇑f + UpperHalfPlane.cuspFunction h ⇑g

Alias of ModularForm.cuspFunction_add.

@[deprecated ModularForm.cuspFunction_sub (since := "2026-05-05")]

theorem ModularFormClass.cuspFunction_sub {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} {G : Type u_2} [FunLike G UpperHalfPlane ℂ] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) {a b : ℤ} (f : F) [ModularFormClass F Γ a] (g : G) [ModularFormClass G Γ b] :

UpperHalfPlane.cuspFunction h (⇑f - ⇑g) = UpperHalfPlane.cuspFunction h ⇑f - UpperHalfPlane.cuspFunction h ⇑g

Alias of ModularForm.cuspFunction_sub.

@[deprecated ModularForm.qExpansion_smul (since := "2026-05-05")]

theorem ModularFormClass.qExpansion_smul {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) (a : ℂ) (f : F) [ModularFormClass F Γ k] :

UpperHalfPlane.qExpansion h (a • ⇑f) = a • UpperHalfPlane.qExpansion h ⇑f

Alias of ModularForm.qExpansion_smul.

@[deprecated ModularForm.qExpansion_neg (since := "2026-05-05")]

theorem ModularFormClass.qExpansion_neg {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) (f : F) [ModularFormClass F Γ k] :

UpperHalfPlane.qExpansion h (-⇑f) = -UpperHalfPlane.qExpansion h ⇑f

Alias of ModularForm.qExpansion_neg.

@[deprecated ModularForm.qExpansion_add (since := "2026-05-05")]

theorem ModularFormClass.qExpansion_add {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} {G : Type u_2} [FunLike G UpperHalfPlane ℂ] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) {a b : ℤ} (f : F) [ModularFormClass F Γ a] (g : G) [ModularFormClass G Γ b] :

UpperHalfPlane.qExpansion h (⇑f + ⇑g) = UpperHalfPlane.qExpansion h ⇑f + UpperHalfPlane.qExpansion h ⇑g

Alias of ModularForm.qExpansion_add.

@[deprecated ModularForm.qExpansion_sub (since := "2026-05-05")]

theorem ModularFormClass.qExpansion_sub {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} {G : Type u_2} [FunLike G UpperHalfPlane ℂ] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) {a b : ℤ} (f : F) [ModularFormClass F Γ a] (g : G) [ModularFormClass G Γ b] :

UpperHalfPlane.qExpansion h (⇑f - ⇑g) = UpperHalfPlane.qExpansion h ⇑f - UpperHalfPlane.qExpansion h ⇑g

Alias of ModularForm.qExpansion_sub.

theorem UpperHalfPlane.hasFPowerSeries_cuspFunction {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {h : ℝ} (f : F) {c : ℕ → ℂ} (hh : 0 < h) (hfanalytic : AnalyticAt ℂ (cuspFunction h ⇑f) 0) (hf : ∀ (τ : UpperHalfPlane), HasSum (fun (m : ℕ) => c m • Function.Periodic.qParam h ↑τ ^ m) (f τ)) :

HasFPowerSeriesOnBall (cuspFunction h ⇑f) (qExpansionFormalMultilinearSeries h f) 0 1

The q-expansion of f is an FPowerSeries representing cuspFunction n f.

theorem UpperHalfPlane.qExpansion_coeff_unique {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {h : ℝ} (f : F) {c : ℕ → ℂ} (hh : 0 < h) (hfanalytic : AnalyticAt ℂ (cuspFunction h ⇑f) 0) (hf : ∀ (τ : UpperHalfPlane), HasSum (fun (m : ℕ) => c m • Function.Periodic.qParam h ↑τ ^ m) (f τ)) (m : ℕ) :

c m = (PowerSeries.coeff m) (qExpansion h ⇑f)

theorem ModularFormClass.qExpansion_coeff_unique {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} {c : ℕ → ℂ} (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) {f : F} [ModularFormClass F Γ k] (hf : ∀ (τ : UpperHalfPlane), HasSum (fun (m : ℕ) => c m • Function.Periodic.qParam h ↑τ ^ m) (f τ)) (m : ℕ) :

c m = (PowerSeries.coeff m) (UpperHalfPlane.qExpansion h ⇑f)