Order at infinity

We define the "order at infinity" of a function ℍ → ℂ as the supremum of t such that f = O(exp (-(2 * π * τ.im * t))) as Im τ → ∞. This definition is deliberately chosen to be independent of any holomorphy or periodicity hypotheses; but if f is periodic and holomorphic on ℍ ∪ ∞, we show that the order of vanishing is determined by the order of vanishing of its q-expansion (divided by the period).

Main statements (general functions)

• UpperHalfPlane.le_orderAtInfty_iff: the order is at least t iff there is an exponential bound at every rate s < t.
• orderAtInfty_eq_of_isTheta: matching exponential upper and lower bounds determine the order at infinity.

Main statements (periodic holomorphic functions)

Here the functions are holomorphic on ℍ, bounded at infinity, and periodic with positive period h. (The obvious examples are modular forms, but we keep the hypotheses un-bundled, since only the periodicity is relevant here.)

• UpperHalfPlane.orderAtInfty_eq_qExpansion_order: the order at infinity equals the order of the q-expansion divided by h.
• UpperHalfPlane.isTheta_orderAtInfty: a nonzero function has exact exponential decay rate given by its order at infinity.
• UpperHalfPlane.orderAtInfty_eq_top_iff_eq_zero: the order is infinite iff the function is zero.
• UpperHalfPlane.orderAtInfty_mul_of_holo: the order of a product equals the sum of the orders.

Elementary theory for arbitrary functions

noncomputable def UpperHalfPlane.orderAtInfty {E : Type u_1} [Norm E] (f : UpperHalfPlane → E) : EReal

The supremum of t such that f = O (exp (-(2 * π * τ.im * t))) as Im τ → ∞. We take the supremum as an EReal, so the zero function has order +∞, and a function with no exponential bound has order -∞. See lt_orderAtInfty_iff and le_orderAtInfty_iff for characterizations.

Equations

• UpperHalfPlane.orderAtInfty f = ⨆ (t : { t : ℝ // f =O[UpperHalfPlane.atImInfty] fun (τ : UpperHalfPlane) => Real.exp (-(2 * Real.pi * τ.im * t)) }), ↑↑t

theorem UpperHalfPlane.le_orderAtInfty_of_isBigO {E : Type u_1} {f : UpperHalfPlane → E} {t : ℝ} [Norm E] (ht : f =O[atImInfty] fun (τ : UpperHalfPlane) => Real.exp (-(2 * Real.pi * τ.im * t))) : ↑t ≤ orderAtInfty f

theorem UpperHalfPlane.le_orderAtInfty_iff {E : Type u_1} {f : UpperHalfPlane → E} {t : ℝ} [Norm E] : ↑t ≤ orderAtInfty f ↔ ∀ s < t, f =O[atImInfty] fun (τ : UpperHalfPlane) => Real.exp (-(2 * Real.pi * τ.im * s))

theorem UpperHalfPlane.lt_orderAtInfty_iff {E : Type u_1} {f : UpperHalfPlane → E} {t : ℝ} [Norm E] : ↑t < orderAtInfty f ↔ ∃ s > t, f =O[atImInfty] fun (τ : UpperHalfPlane) => Real.exp (-(2 * Real.pi * τ.im * s))

@[simp]

theorem UpperHalfPlane.orderAtInfty_exp {t : ℝ} : (orderAtInfty fun (τ : UpperHalfPlane) => Real.exp (-(2 * Real.pi * τ.im * t))) = ↑t

The model function τ ↦ exp (-(2 * π * τ.im * t)) has order at infinity t.

theorem UpperHalfPlane.orderAtInfty_eq_top_iff {E : Type u_1} {f : UpperHalfPlane → E} [Norm E] : orderAtInfty f = ⊤ ↔ ∀ (t : ℝ), f =O[atImInfty] fun (τ : UpperHalfPlane) => Real.exp (-(2 * Real.pi * τ.im * t))

theorem UpperHalfPlane.IsBoundedAtImInfty.orderAtInfty_nonneg {E : Type u_1} {f : UpperHalfPlane → E} [Norm E] (hf : IsBoundedAtImInfty f) : 0 ≤ orderAtInfty f

theorem UpperHalfPlane.orderAtInfty_comp_equiv {E : Type u_1} (f : UpperHalfPlane → E) [Norm E] (e : UpperHalfPlane ≃ UpperHalfPlane) {a : ℝ} (ha : 0 < a) (he : ∀ (τ : UpperHalfPlane), (e τ).im = a * τ.im) : orderAtInfty (f ∘ ⇑e) = ↑a * orderAtInfty f

A change of variables which scales imaginary parts scales the order by the same factor.

theorem UpperHalfPlane.orderAtInfty_vadd {E : Type u_1} {f : UpperHalfPlane → E} [Norm E] (x : ℝ) : (orderAtInfty fun (τ : UpperHalfPlane) => f (x +ᵥ τ)) = orderAtInfty f

Real translations preserve the order at infinity.

theorem Asymptotics.IsBigO.orderAtInfty_le {E : Type u_1} {f : UpperHalfPlane → E} {F : Type u_2} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] {g : UpperHalfPlane → F} (hfg : f =O[UpperHalfPlane.atImInfty] g) : UpperHalfPlane.orderAtInfty g ≤ UpperHalfPlane.orderAtInfty f

theorem Asymptotics.IsTheta.orderAtInfty_eq {E : Type u_1} {f : UpperHalfPlane → E} {F : Type u_2} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] {g : UpperHalfPlane → F} (hfg : f =Θ[UpperHalfPlane.atImInfty] g) : UpperHalfPlane.orderAtInfty f = UpperHalfPlane.orderAtInfty g

@[simp]

theorem UpperHalfPlane.orderAtInfty_zero {E : Type u_1} [SeminormedAddCommGroup E] : orderAtInfty 0 = ⊤

theorem UpperHalfPlane.orderAtInfty_eq_of_isTheta {E : Type u_1} {f : UpperHalfPlane → E} {t : ℝ} [SeminormedAddCommGroup E] (hf : f =Θ[atImInfty] fun (τ : UpperHalfPlane) => Real.exp (-(2 * Real.pi * τ.im * t))) : orderAtInfty f = ↑t

Matching exponential upper and lower bounds determine the order at infinity.

theorem UpperHalfPlane.orderAtInfty_norm {E : Type u_1} (f : UpperHalfPlane → E) [SeminormedAddCommGroup E] : (orderAtInfty fun (τ : UpperHalfPlane) => ‖f τ‖) = orderAtInfty f

Taking norms preserves the order at infinity.

theorem UpperHalfPlane.orderAtInfty_const_mul {E : Type u_1} [NormedRing E] [NormMulClass E] {c : E} (hc : c ≠ 0) (f : UpperHalfPlane → E) : (orderAtInfty fun (τ : UpperHalfPlane) => c * f τ) = orderAtInfty f

Scalar multiplication by a nonzero constant preserves the order.

theorem UpperHalfPlane.orderAtInfty_slash_neg (f : UpperHalfPlane → ℂ) (k : ℤ) (g : GL (Fin 2) ℝ) : orderAtInfty (SlashAction.map k (-g) f) = orderAtInfty (SlashAction.map k g f)

Negating the matrix in a slash operator preserves the order at infinity.

theorem UpperHalfPlane.orderAtInfty_slash_of_upperTriangular (f : UpperHalfPlane → ℂ) (k : ℤ) (g : GL (Fin 2) ℝ) (hg : ↑g 1 0 = 0) : orderAtInfty (SlashAction.map k g f) = ↑|↑g 0 0 / ↑g 1 1| * orderAtInfty f

An upper triangular slash operator scales the order by its scale factor on imaginary parts.

Theory for periodic holomorphic functions

If we assume f is periodic, and holomorphic on ℍ ∪ ∞, then its order at infinity is related to the order of vanishing of its cusp function.

theorem UpperHalfPlane.analyticOrderAt_cuspFunction_ne_top {h : ℝ} {f : UpperHalfPlane → ℂ} (hh : 0 < h) (hfper : Function.Periodic (f ∘ ↑ofComplex) ↑h) (hfhol : MDiff f) (hfbdd : IsBoundedAtImInfty f) (hfne : f ≠ 0) : analyticOrderAt (cuspFunction h f) 0 ≠ ⊤

A nonzero periodic function holomorphic on ℍ ∪ ∞ has finite order in the cusp coordinate.

theorem UpperHalfPlane.isTheta_analyticOrderAt {h : ℝ} {f : UpperHalfPlane → ℂ} (hh : 0 < h) (hfper : Function.Periodic (f ∘ ↑ofComplex) ↑h) (hfhol : MDiff f) (hfbdd : IsBoundedAtImInfty f) (hfne : f ≠ 0) : f =Θ[atImInfty] fun (τ : UpperHalfPlane) => Real.exp (-(2 * Real.pi * τ.im * ↑(analyticOrderNatAt (cuspFunction h f) 0) / h))

The asymptotic behaviour of a nonzero periodic function holomorphic on ℍ ∪ ∞ is determined by the order of vanishing of its cusp function at zero.

theorem UpperHalfPlane.orderAtInfty_eq_analyticOrderAt_div {h : ℝ} {f : UpperHalfPlane → ℂ} (hh : 0 < h) (hfper : Function.Periodic (f ∘ ↑ofComplex) ↑h) (hfhol : MDiff f) (hfbdd : IsBoundedAtImInfty f) : orderAtInfty f = ↑↑(analyticOrderAt (cuspFunction h f) 0) / ↑h

The order at infinity is the order of the cusp function divided by the period.

theorem UpperHalfPlane.orderAtInfty_eq_top_iff_eq_zero {h : ℝ} {f : UpperHalfPlane → ℂ} (hh : 0 < h) (hfper : Function.Periodic (f ∘ ↑ofComplex) ↑h) (hfhol : MDiff f) (hfbdd : IsBoundedAtImInfty f) : orderAtInfty f = ⊤ ↔ f = 0

A periodic function holomorphic on ℍ ∪ ∞ has infinite order exactly when it is zero.

theorem UpperHalfPlane.isTheta_orderAtInfty {h : ℝ} {f : UpperHalfPlane → ℂ} (hh : 0 < h) (hfper : Function.Periodic (f ∘ ↑ofComplex) ↑h) (hfhol : MDiff f) (hfbdd : IsBoundedAtImInfty f) (hfne : f ≠ 0) : f =Θ[atImInfty] fun (τ : UpperHalfPlane) => Real.exp (-(2 * Real.pi * τ.im * (orderAtInfty f).toReal))

A nonzero periodic function holomorphic on ℍ ∪ ∞ has matching exponential bounds at the rate given by its order at infinity.

theorem UpperHalfPlane.orderAtInfty_prod_of_holo {ι : Type u_2} {s : Finset ι} {f : ι → UpperHalfPlane → ℂ} {h : ι → ℝ} (hh : ∀ i ∈ s, 0 < h i) (hfper : ∀ i ∈ s, Function.Periodic (f i ∘ ↑ofComplex) ↑(h i)) (hfhol : ∀ i ∈ s, MDiff (f i)) (hfbdd : ∀ i ∈ s, IsBoundedAtImInfty (f i)) : orderAtInfty (∏ i ∈ s, f i) = ∑ i ∈ s, orderAtInfty (f i)

The order at infinity is additive for finite products of periodic functions holomorphic on ℍ ∪ ∞. Note that the periods need not be equal (or commensurable).

theorem UpperHalfPlane.orderAtInfty_mul_of_holo {h : ℝ} {f g : UpperHalfPlane → ℂ} (hh : 0 < h) {h' : ℝ} (hh' : 0 < h') (hfper : Function.Periodic (f ∘ ↑ofComplex) ↑h) (hfhol : MDiff f) (hfbdd : IsBoundedAtImInfty f) (hgper : Function.Periodic (g ∘ ↑ofComplex) ↑h') (hghol : MDiff g) (hgbdd : IsBoundedAtImInfty g) : orderAtInfty (f * g) = orderAtInfty f + orderAtInfty g

The order at infinity is additive for the product of two periodic functions holomorphic on ℍ ∪ ∞. Note that the periods need not be equal (or commensurable).

Relation to the q-expansion

theorem UpperHalfPlane.orderAtInfty_eq_qExpansion_order {h : ℝ} {f : UpperHalfPlane → ℂ} (hh : 0 < h) (hfper : Function.Periodic (f ∘ ↑ofComplex) ↑h) (hfhol : MDiff f) (hfbdd : IsBoundedAtImInfty f) : orderAtInfty f = ↑↑(qExpansion h f).order / ↑h

The order at infinity is the order of the q-expansion divided by the period.