Holomorphic SL₂(ℤ)-invariant functions with a limit at i∞

A holomorphic function F on the upper half-plane with F (γ τ) = F τ for every γ ∈ SL₂(ℤ) that converges to c at i∞ is the constant c: it is a level-one modular form of weight zero, and these are constant (Mathlib's ModularFormClass.levelOne_weight_zero_const). This is how identities between modular functions are proved from their behaviour at the cusp: a combination of modular functions whose poles at i∞ cancel is determined by its constant term there.

Main results

• TauCeti.ModularForm.levelOne_eq_of_tendsto_atImInfty: a holomorphic SL₂(ℤ)-invariant function on the upper half-plane with limit c at i∞ is the constant c.

theorem TauCeti.ModularForm.levelOne_eq_of_tendsto_atImInfty {F : UpperHalfPlane → ℂ} (hF : MDiff F) (hinv : ∀ (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (τ : UpperHalfPlane), F (γ • τ) = F τ) {c : ℂ} (hc : Filter.Tendsto F UpperHalfPlane.atImInfty (nhds c)) (τ : UpperHalfPlane) : F τ = c

A holomorphic function on the upper half-plane that is invariant under SL₂(ℤ) and tends to c at i∞ is the constant function c.