Meromorphic functions on the upper half-plane

A function f : ℍ → E is meromorphic at τ, as a function on the Riemann surface ℍ (TauCeti.RiemannSurface.MeromorphicAt), exactly when its extension f ∘ ofComplex to ℂ is meromorphic at τ in the sense of Mathlib's MeromorphicAt, and the two orders at τ agree. This is the form in which orders of modular functions, stated for f ∘ ofComplex, enter the theory of Riemann surfaces, in the same way as UpperHalfPlane.mdifferentiableAt_iff does for holomorphy.

theorem TauCeti.UpperHalfPlane.meromorphicAt_iff_meromorphicAt_comp_ofComplex {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : UpperHalfPlane → E} {τ : UpperHalfPlane} : RiemannSurface.MeromorphicAt f τ ↔ MeromorphicAt (f ∘ ↑UpperHalfPlane.ofComplex) ↑τ

A function on the upper half-plane is meromorphic at τ exactly when its extension by ofComplex is meromorphic at τ.

theorem TauCeti.UpperHalfPlane.meromorphicOrderAt_eq_meromorphicOrderAt_comp_ofComplex {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : UpperHalfPlane → E} {τ : UpperHalfPlane} : RiemannSurface.meromorphicOrderAt f τ = meromorphicOrderAt (f ∘ ↑UpperHalfPlane.ofComplex) ↑τ

The order of a function on the upper half-plane at τ is the meromorphic order of its extension by ofComplex at τ.