∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] {f : UpperHalfPlane → E},
  Continuous f →
    ∀ {t : ℝ}, (f =O[UpperHalfPlane.atImInfty] fun z => z.im ^ t) → ∃ F, ∀ τ ∈ ModularGroup.fd, ‖f τ‖ ≤ F * τ.im ^ t