Exponential bounds on the upper half-plane #
A function dominated by a strictly decreasing real exponential in the imaginary coordinate tends to zero as that coordinate tends to infinity. This supplies the general asymptotic step used when exponential decay in a cusp coordinate is converted into vanishing at the cusp.
An exponential growth bound with real rate k also remains valid after increasing k. This
monotonicity feeds the independence of a cusp Laurent expansion from the chosen growth bound.
theorem
TauCeti.UpperHalfPlane.isZeroAtImInfty_of_isBigO_exp_neg
{E : Type u_1}
[NormedAddCommGroup E]
{f : UpperHalfPlane → E}
{c : ℝ}
(hc : 0 < c)
(hf : f =O[UpperHalfPlane.atImInfty] fun (z : UpperHalfPlane) => Real.exp (-c * z.im))
:
A function bounded by exp (-c * im z) for some c > 0 tends to zero at imaginary
infinity.
theorem
TauCeti.UpperHalfPlane.isBigO_exp_of_le
{E : Type u_1}
[NormedAddCommGroup E]
(w : ℝ)
(hw : 0 < w)
{k k' : ℝ}
(hkk' : k ≤ k')
{f : UpperHalfPlane → E}
(hf : f =O[UpperHalfPlane.atImInfty] fun (z : UpperHalfPlane) => Real.exp (2 * Real.pi * k * z.im / w))
:
An exponential growth bound at i∞ remains valid after increasing its real rate.