The vanishing order of a modular form

TauCeti.orderOfVanishingAt f z is the order of vanishing of f : ℍ → ℂ at z ∈ ℍ, read as the meromorphic order of f ∘ ofComplex at z. For a nonzero holomorphic function it detects vanishing (orderOfVanishingAt_eq_zero_iff), and it transports along the slash action of any positive-determinant matrix (orderOfVanishingAt_slash); for a slash-invariant form it is therefore constant along the group action (orderOfVanishingAt_smul, a corollary) — the interior half of the order dictionary feeding the valence formula. The order at the cusps (ℚ-normalized at irregular cusps in odd weight) belongs to the general-level layer and is not defined here.

Main declarations

• TauCeti.orderOfVanishingAt.
• TauCeti.orderOfVanishingAt_eq_zero_iff: for a nonzero holomorphic function, the order at z vanishes exactly when the function does not vanish at z.
• TauCeti.orderOfVanishingAt_mul: orders add under multiplication, with the Finset.prod and power versions.
• TauCeti.orderOfVanishingAt_pos_iff: for a nonzero holomorphic function, positive order characterizes the zeros.
• TauCeti.orderOfVanishingAt_slash: the order of a slash translate at z is the order at γ • z, for any positive-determinant γ.
• TauCeti.orderOfVanishingAt_smul: invariance along the action of the group, a corollary of the slash statement.
• TauCeti.orderOfVanishingAt_eq_of_coe_eq_add: invariance under the period translation, for a periodic function.

References

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

noncomputable def TauCeti.orderOfVanishingAt (f : UpperHalfPlane → ℂ) (z : UpperHalfPlane) : ℤ

The order of vanishing of f : ℍ → ℂ at z ∈ ℍ: the meromorphic order of f ∘ ofComplex at z, with the conventions that a function vanishing in a neighborhood of z (in particular the zero function) and a function not meromorphic at z both get order 0.

Equations

• TauCeti.orderOfVanishingAt f z = (meromorphicOrderAt (f ∘ ↑UpperHalfPlane.ofComplex) ↑z).untop₀

theorem TauCeti.orderOfVanishingAt_def (f : UpperHalfPlane → ℂ) (z : UpperHalfPlane) : orderOfVanishingAt f z = (meromorphicOrderAt (f ∘ ↑UpperHalfPlane.ofComplex) ↑z).untop₀

The defining equality of orderOfVanishingAt: the definition is sealed by the module system, so this restatement is the supported cross-module rewrite for it.

theorem TauCeti.orderOfVanishingAt_eq_zero_of_ne_zero {f : UpperHalfPlane → ℂ} {z : UpperHalfPlane} (hf : MeromorphicNFAt (f ∘ ↑UpperHalfPlane.ofComplex) ↑z) (hz : f z ≠ 0) : orderOfVanishingAt f z = 0

At a point where a function in meromorphic normal form does not vanish, its order is zero.

theorem TauCeti.orderOfVanishingAt_ne_zero_of_eq_zero {f : UpperHalfPlane → ℂ} (hf : MDiff f) (hne : f ≠ 0) {z : UpperHalfPlane} (hz : f z = 0) : orderOfVanishingAt f z ≠ 0

A zero of a nonzero holomorphic function on ℍ has nonzero vanishing order.

@[simp]

theorem TauCeti.orderOfVanishingAt_eq_zero_iff {f : UpperHalfPlane → ℂ} (hf : MDiff f) (hne : f ≠ 0) {z : UpperHalfPlane} : orderOfVanishingAt f z = 0 ↔ f z ≠ 0

For a nonzero holomorphic function on ℍ, the vanishing order at z is zero exactly when the function does not vanish at z.

theorem TauCeti.orderOfVanishingAt_mul {f g : UpperHalfPlane → ℂ} (hf : MDiff f) (hg : MDiff g) (hfne : f ≠ 0) (hgne : g ≠ 0) (z : UpperHalfPlane) : orderOfVanishingAt (f * g) z = orderOfVanishingAt f z + orderOfVanishingAt g z

Vanishing orders add under multiplication of nonzero holomorphic functions.

@[simp]

theorem TauCeti.orderOfVanishingAt_const (c : ℂ) (z : UpperHalfPlane) : orderOfVanishingAt (fun (x : UpperHalfPlane) => c) z = 0

Constant functions have vanishing order zero everywhere (including the zero function, by the order-zero convention).

@[simp]

theorem TauCeti.orderOfVanishingAt_zero (z : UpperHalfPlane) : orderOfVanishingAt 0 z = 0

The zero function has vanishing order zero everywhere, by the order-zero convention.

This is what lets the finiteness and finite-support statements downstream drop their nonvanishing hypotheses: the degenerate case is not excluded, it is trivially true.

theorem TauCeti.orderOfVanishingAt_nonneg {f : UpperHalfPlane → ℂ} (hf : MDiff f) (z : UpperHalfPlane) : 0 ≤ orderOfVanishingAt f z

The vanishing order of a holomorphic function is nonnegative.

@[simp]

theorem TauCeti.orderOfVanishingAt_pos_iff {f : UpperHalfPlane → ℂ} (hf : MDiff f) (hne : f ≠ 0) {z : UpperHalfPlane} : 0 < orderOfVanishingAt f z ↔ f z = 0

For a nonzero holomorphic function, the vanishing order at z is positive exactly when the function vanishes at z.

theorem TauCeti.orderOfVanishingAt_prod {ι : Type u_1} {s : Finset ι} {F : ι → UpperHalfPlane → ℂ} (hF : ∀ i ∈ s, MDiff (F i)) (hFne : ∀ i ∈ s, F i ≠ 0) (z : UpperHalfPlane) : orderOfVanishingAt (∏ i ∈ s, F i) z = ∑ i ∈ s, orderOfVanishingAt (F i) z

Vanishing orders sum over finite products of nonzero holomorphic functions.

theorem TauCeti.orderOfVanishingAt_pow {f : UpperHalfPlane → ℂ} (hf : MDiff f) (n : ℕ) (z : UpperHalfPlane) : orderOfVanishingAt (f ^ n) z = ↑n * orderOfVanishingAt f z

Vanishing orders scale under powers of a holomorphic function.

@[simp]

theorem TauCeti.orderOfVanishingAt_slash {k : ℤ} (g : UpperHalfPlane → ℂ) {γ : GL (Fin 2) ℝ} (hdet : 0 < (↑γ).det) (z : UpperHalfPlane) : orderOfVanishingAt (SlashAction.map k γ g) z = orderOfVanishingAt g (γ • z)

The vanishing order of a slash translate: the order of g ∣[k] γ at z is the order of g at γ • z. Positive determinant makes the slash's σ γ twist trivial and keeps the Möbius action on ℍ; no invariance of g under γ is assumed.

theorem TauCeti.orderOfVanishingAt_smul {F : Type u_1} {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [FunLike F UpperHalfPlane ℂ] [SlashInvariantFormClass F Γ k] (f : F) {γ : GL (Fin 2) ℝ} (hγ : γ ∈ Γ) (hdet : 0 < (↑γ).det) (z : UpperHalfPlane) : orderOfVanishingAt (⇑f) (γ • z) = orderOfVanishingAt (⇑f) z

The vanishing order of a slash-invariant form is constant along the action of any positive-determinant element of the group.

theorem TauCeti.orderOfVanishingAt_eq_of_coe_eq_add {f : UpperHalfPlane → ℂ} {c : ℂ} (hper : Function.Periodic (f ∘ ↑UpperHalfPlane.ofComplex) c) {z w : UpperHalfPlane} (hzw : ↑w = ↑z + c) : orderOfVanishingAt f w = orderOfVanishingAt f z

The vanishing order of a c-periodic function on ℍ agrees at z and at z + c. For a level-one form and c = 1 this is what makes the two ρ-corners of the fundamental domain contribute equally to the valence formula.