The vanishing order at the cusp

The vanishing order of a modular form at the cusp is the order of its q-expansion, as an integer with junk value 0 at the identically vanishing expansion — the convention of the interior dictionary orderOfVanishingAt. It is computed by the analytic order of the cusp function at 0, vanishes when the constant term is nonzero, and rescales linearly in the width — the cusp term of the level-one valence formula. The lemmas take the raw analytic, periodicity, and boundedness hypotheses of the underlying q-expansion theorems; for a modular form all of them are supplied by the ModularFormClass machinery.

qExpansionOrderAtCusp is the integral exponent of the width-h expansion, the correct primitive at every cusp; orderAtCusp supplies the width-normalized ℚ-valued convention on top of it — the doubled-width exponent halved, which is the integral order for an h-periodic function and the conventional half-integer at an irregular cusp of odd weight.

Main declarations

• TauCeti.qExpansionOrderAtCusp.
• TauCeti.qExpansionOrderAtCusp_eq_analyticOrderAt: the analytic-order dictionary.
• TauCeti.qExpansionOrderAtCusp_nat_mul: linear rescaling in the width.
• TauCeti.orderAtCusp: the ℚ-valued cusp order — the doubled-width exponent halved, the conventional half-integral order at irregular cusps.
• TauCeti.ModularForm.qExpansionOrderAtCusp_eq_zero_iff: for a nonzero modular form, order zero is a nonzero constant term (the class-level interface lives in TauCeti.ModularForm).
• TauCeti.qExpansionOrderAtCusp_mul: additivity on products (with qExpansionOrderAtCusp_pow and qExpansionOrderAtCusp_prod).

References

• AINTLIB LeanModularForms — the valence-formula development this file ports onto the current Mathlib pin.

noncomputable def TauCeti.qExpansionOrderAtCusp (h : ℝ) (f : UpperHalfPlane → ℂ) : ℤ

The vanishing order at the cusp: the order of the q-expansion at width h, as an integer, with junk value 0 when the expansion vanishes identically — the untop₀ convention of orderOfVanishingAt. This is the exponent of the width-h uniformizer; normalized orders at other widths (half-integral at irregular cusps) are conversion layers over this primitive.

Equations

• TauCeti.qExpansionOrderAtCusp h f = ↑(UpperHalfPlane.qExpansion h f).order.toNat

theorem TauCeti.qExpansionOrderAtCusp_def (h : ℝ) (f : UpperHalfPlane → ℂ) : qExpansionOrderAtCusp h f = ↑(UpperHalfPlane.qExpansion h f).order.toNat

qExpansionOrderAtCusp unfolded to the q-expansion order. The definition is sealed by the module system; this equation is the supported cross-module rewrite.

theorem TauCeti.qExpansionOrderAtCusp_nonneg (h : ℝ) (f : UpperHalfPlane → ℂ) : 0 ≤ qExpansionOrderAtCusp h f

The cusp order is nonnegative.

theorem TauCeti.qExpansionOrderAtCusp_eq_analyticOrderAt {h : ℝ} {g : UpperHalfPlane → ℂ} (hg : AnalyticAt ℂ (UpperHalfPlane.cuspFunction h g) 0) : qExpansionOrderAtCusp h g = ↑(analyticOrderAt (UpperHalfPlane.cuspFunction h g) 0).toNat

The cusp order is the analytic order of the cusp function at 0. For a modular form the analyticity is ModularFormClass.analyticAt_cuspFunction_zero.

theorem TauCeti.qExpansionOrderAtCusp_eq_zero_of_cuspFunction_ne_zero {h : ℝ} {g : UpperHalfPlane → ℂ} (h0 : UpperHalfPlane.cuspFunction h g 0 ≠ 0) : qExpansionOrderAtCusp h g = 0

A nonzero constant term at the cusp forces cusp order zero, with no analyticity hypothesis: the constant coefficient of the q-expansion is the value at 0.

theorem TauCeti.qExpansionOrderAtCusp_nat_mul {h : ℝ} {g : UpperHalfPlane → ℂ} {m : ℕ} (hh : 0 < h) (hm : 0 < m) (hg_per : Function.Periodic (g ∘ ↑UpperHalfPlane.ofComplex) ↑h) (hg_bdd : UpperHalfPlane.IsBoundedAtImInfty g) (hg_mdiff : MDiff g) : qExpansionOrderAtCusp (↑m * h) g = ↑m * qExpansionOrderAtCusp h g

The cusp order rescales linearly in the width. For a modular form the periodicity, boundedness, and holomorphy are SlashInvariantFormClass.periodic_comp_ofComplex, ModularFormClass.bdd_at_infty, and ModularFormClass.holo.

theorem TauCeti.qExpansionOrderAtCusp_mul {h : ℝ} {f g : UpperHalfPlane → ℂ} (hf : AnalyticAt ℂ (UpperHalfPlane.cuspFunction h f) 0) (hg : AnalyticAt ℂ (UpperHalfPlane.cuspFunction h g) 0) (hf' : analyticOrderAt (UpperHalfPlane.cuspFunction h f) 0 ≠ ⊤) (hg' : analyticOrderAt (UpperHalfPlane.cuspFunction h g) 0 ≠ ⊤) : qExpansionOrderAtCusp h (f * g) = qExpansionOrderAtCusp h f + qExpansionOrderAtCusp h g

The cusp order is additive on products. The finiteness hypotheses exclude an identically vanishing factor, where the junk value 0 would break additivity.

@[simp]

theorem TauCeti.qExpansionOrderAtCusp_const (h : ℝ) (c : ℂ) : (qExpansionOrderAtCusp h fun (x : UpperHalfPlane) => c) = 0

Every constant function has cusp order zero: a nonzero constant by the nonvanishing constant term, the zero function by the junk value.

@[simp]

theorem TauCeti.qExpansionOrderAtCusp_one (h : ℝ) : qExpansionOrderAtCusp h 1 = 0

The constant-one function has cusp order zero.

theorem TauCeti.qExpansionOrderAtCusp_pow {h : ℝ} {f : UpperHalfPlane → ℂ} (n : ℕ) (hf : AnalyticAt ℂ (UpperHalfPlane.cuspFunction h f) 0) : qExpansionOrderAtCusp h (f ^ n) = ↑n * qExpansionOrderAtCusp h f

The cusp order multiplies under powers, with no finiteness hypothesis: for an identically vanishing expansion both sides take the junk value at positive exponents, and at exponent zero both sides are genuinely zero.

theorem TauCeti.qExpansionOrderAtCusp_prod {h : ℝ} {ι : Type u_1} {f : ι → UpperHalfPlane → ℂ} (s : Finset ι) (hf : ∀ i ∈ s, AnalyticAt ℂ (UpperHalfPlane.cuspFunction h (f i)) 0) (hf' : ∀ i ∈ s, analyticOrderAt (UpperHalfPlane.cuspFunction h (f i)) 0 ≠ ⊤) : qExpansionOrderAtCusp h (∏ i ∈ s, f i) = ∑ i ∈ s, qExpansionOrderAtCusp h (f i)

The cusp order is additive on finite products. The finiteness hypotheses exclude an identically vanishing factor, where the junk value 0 would break additivity.

noncomputable def TauCeti.orderAtCusp (h : ℝ) (f : UpperHalfPlane → ℂ) : ℚ

The ℚ-valued cusp order: the width-2h exponent, halved. For an h-periodic function this is the integral order at width h (orderAtCusp_eq_qExpansionOrderAtCusp); at an irregular cusp of odd weight, where the form is only 2h-periodic, it is the conventional half-integral order.

Equations

• TauCeti.orderAtCusp h f = ↑(TauCeti.qExpansionOrderAtCusp (2 * h) f) / 2

theorem TauCeti.orderAtCusp_def (h : ℝ) (f : UpperHalfPlane → ℂ) : orderAtCusp h f = ↑(qExpansionOrderAtCusp (2 * h) f) / 2

orderAtCusp unfolded to the halved doubled-width exponent.

theorem TauCeti.orderAtCusp_eq_qExpansionOrderAtCusp {h : ℝ} {g : UpperHalfPlane → ℂ} (hh : 0 < h) (hg_per : Function.Periodic (g ∘ ↑UpperHalfPlane.ofComplex) ↑h) (hg_bdd : UpperHalfPlane.IsBoundedAtImInfty g) (hg_mdiff : MDiff g) : orderAtCusp h g = ↑(qExpansionOrderAtCusp h g)

For an h-periodic bounded holomorphic function the ℚ-valued cusp order is the integral one: the doubled-width exponent doubles.

theorem TauCeti.orderAtCusp_eq_half_analyticOrderAt {h : ℝ} {g : UpperHalfPlane → ℂ} (hg : AnalyticAt ℂ (UpperHalfPlane.cuspFunction (2 * h) g) 0) : orderAtCusp h g = ↑(analyticOrderAt (UpperHalfPlane.cuspFunction (2 * h) g) 0).toNat / 2

The rational cusp order is the halved doubled-width analytic order.

theorem TauCeti.orderAtCusp_nonneg (h : ℝ) (f : UpperHalfPlane → ℂ) : 0 ≤ orderAtCusp h f

The rational cusp order is nonnegative.

@[simp]

theorem TauCeti.orderAtCusp_const (h : ℝ) (c : ℂ) : (orderAtCusp h fun (x : UpperHalfPlane) => c) = 0

Every constant function has rational cusp order zero.

@[simp]

theorem TauCeti.orderAtCusp_one (h : ℝ) : orderAtCusp h 1 = 0

The constant-one function has rational cusp order zero.

theorem TauCeti.orderAtCusp_mul {h : ℝ} {f g : UpperHalfPlane → ℂ} (hf : AnalyticAt ℂ (UpperHalfPlane.cuspFunction (2 * h) f) 0) (hg : AnalyticAt ℂ (UpperHalfPlane.cuspFunction (2 * h) g) 0) (hf' : analyticOrderAt (UpperHalfPlane.cuspFunction (2 * h) f) 0 ≠ ⊤) (hg' : analyticOrderAt (UpperHalfPlane.cuspFunction (2 * h) g) 0 ≠ ⊤) : orderAtCusp h (f * g) = orderAtCusp h f + orderAtCusp h g

The rational cusp order is additive on products.

theorem TauCeti.orderAtCusp_pow {h : ℝ} {f : UpperHalfPlane → ℂ} (n : ℕ) (hf : AnalyticAt ℂ (UpperHalfPlane.cuspFunction (2 * h) f) 0) : orderAtCusp h (f ^ n) = ↑n * orderAtCusp h f

The rational cusp order multiplies under powers.

theorem TauCeti.orderAtCusp_prod {h : ℝ} {ι : Type u_1} {f : ι → UpperHalfPlane → ℂ} (s : Finset ι) (hf : ∀ i ∈ s, AnalyticAt ℂ (UpperHalfPlane.cuspFunction (2 * h) (f i)) 0) (hf' : ∀ i ∈ s, analyticOrderAt (UpperHalfPlane.cuspFunction (2 * h) (f i)) 0 ≠ ⊤) : orderAtCusp h (∏ i ∈ s, f i) = ∑ i ∈ s, orderAtCusp h (f i)

The rational cusp order is additive on finite products.

theorem TauCeti.qExpansionOrderAtCusp_eq_zero_iff {h : ℝ} {g : UpperHalfPlane → ℂ} (hg : AnalyticAt ℂ (UpperHalfPlane.cuspFunction h g) 0) (hg' : analyticOrderAt (UpperHalfPlane.cuspFunction h g) 0 ≠ ⊤) : qExpansionOrderAtCusp h g = 0 ↔ UpperHalfPlane.cuspFunction h g 0 ≠ 0

The exponent vanishes iff the constant term — the value of the cusp function at 0 — is nonzero, for any function whose cusp function is analytic with finite order.

theorem TauCeti.qExpansionOrderAtCusp_pos_iff {h : ℝ} {g : UpperHalfPlane → ℂ} (hg : AnalyticAt ℂ (UpperHalfPlane.cuspFunction h g) 0) (hg' : analyticOrderAt (UpperHalfPlane.cuspFunction h g) 0 ≠ ⊤) : 0 < qExpansionOrderAtCusp h g ↔ UpperHalfPlane.cuspFunction h g 0 = 0

The exponent is positive iff the function vanishes at the cusp, for any function whose cusp function is analytic with finite order.

theorem TauCeti.ModularForm.cuspFunction_eventually_ne_zero {h : ℝ} {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {f : F} [ModularFormClass F Γ k] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) (hf : ⇑f ≠ 0) : ∀ᶠ (q : ℂ) in nhdsWithin 0 {0}ᶜ, UpperHalfPlane.cuspFunction h (⇑f) q ≠ 0

The cusp function of a nonzero modular form is nonvanishing on a punctured neighborhood of 0.

theorem TauCeti.ModularForm.qExpansionOrderAtCusp_nat_mul_of_mem_strictPeriods {h : ℝ} {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {f : F} [ModularFormClass F Γ k] {m : ℕ} (hh : 0 < h) (hm : 0 < m) (hΓ : h ∈ Γ.strictPeriods) : qExpansionOrderAtCusp (↑m * h) ⇑f = ↑m * qExpansionOrderAtCusp h ⇑f

The width rescaling for a modular form, with the periodicity, boundedness, and holomorphy supplied by the class machinery.

theorem TauCeti.ModularForm.analyticOrderAt_cuspFunction_ne_top {h : ℝ} {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {f : F} [ModularFormClass F Γ k] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) (hf : ⇑f ≠ 0) : analyticOrderAt (UpperHalfPlane.cuspFunction h ⇑f) 0 ≠ ⊤

For a nonzero modular form the cusp function does not vanish identically near 0, so its analytic order there is finite.

@[simp]

theorem TauCeti.ModularForm.qExpansionOrderAtCusp_eq_zero_iff {h : ℝ} {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {f : F} [ModularFormClass F Γ k] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) (hf : ⇑f ≠ 0) : qExpansionOrderAtCusp h ⇑f = 0 ↔ UpperHalfPlane.cuspFunction h (⇑f) 0 ≠ 0

For a nonzero modular form the exponent vanishes iff the constant term is nonzero.

@[simp]

theorem TauCeti.ModularForm.qExpansionOrderAtCusp_pos_iff {h : ℝ} {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {f : F} [ModularFormClass F Γ k] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) (hf : ⇑f ≠ 0) : 0 < qExpansionOrderAtCusp h ⇑f ↔ UpperHalfPlane.cuspFunction h (⇑f) 0 = 0

For a nonzero modular form the exponent is positive iff the form vanishes at the cusp.

@[simp]

theorem TauCeti.ModularForm.orderAtCusp_eq_zero_iff {h : ℝ} {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {f : F} [ModularFormClass F Γ k] (hh : 0 < h) (hΓ : 2 * h ∈ Γ.strictPeriods) (hf : ⇑f ≠ 0) : orderAtCusp h ⇑f = 0 ↔ UpperHalfPlane.cuspFunction (2 * h) (⇑f) 0 ≠ 0

For a nonzero modular form the rational cusp order vanishes iff the doubled-width constant term is nonzero.

@[simp]

theorem TauCeti.ModularForm.orderAtCusp_pos_iff {h : ℝ} {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {f : F} [ModularFormClass F Γ k] (hh : 0 < h) (hΓ : 2 * h ∈ Γ.strictPeriods) (hf : ⇑f ≠ 0) : 0 < orderAtCusp h ⇑f ↔ UpperHalfPlane.cuspFunction (2 * h) (⇑f) 0 = 0

For a nonzero modular form the rational cusp order is positive iff the form vanishes at the cusp in the doubled-width reading.