∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] {f : UpperHalfPlane → E},
  Continuous f →
    ∀ {t : ℝ},
      0 ≤ t →
        (∀ (g : Matrix.SpecialLinearGroup (Fin 2) ℤ),
            (fun τ => f (g • τ)) =O[UpperHalfPlane.atImInfty] fun z => z.im ^ t) →
          ∀ {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} [Γ.FiniteIndex],
            (∀ g ∈ Γ, ∀ (τ : UpperHalfPlane), f (g • τ) = f τ) →
              ∃ C, ∀ (τ : UpperHalfPlane), ‖f τ‖ ≤ C * max τ.im (1 / τ.im) ^ t